src/Backend/satencoder.h

   1 #ifndef SATENCODER_H
   2 #define SATENCODER_H
   3
   4 #include "classlist.h"
   5 #include "structs.h"
   6
   7 struct SATEncoder {
   8         uint varcount;
   9 };
  10
  11 SATEncoder * allocSATEncoder();
  12 void deleteSATEncoder(SATEncoder *This);
  13 void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This);
  14 Constraint * getNewVarSATEncoder(SATEncoder *This);
  15 void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray);
  16 Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint);
  17 Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
  18 Constraint * createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order);
  19 Constraint* getOrderConstraint(HashTableBoolConst *table, OrderPair *pair);
  20 Constraint * generateTransOrderConstraintSATEncoder(SATEncoder *This, Constraint *constIJ,Constraint *constJK,Constraint *constIK);
  21 Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
  22 Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
  23 Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint);
  24 Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint);
  25 Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
  26 Constraint * encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
  27 Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
  28 Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
  29 Constraint * encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
  30
  31 Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value);
  32 Constraint * getElementValueConstraint(SATEncoder* encoder, Element* This, uint64_t value);
  33
  34 Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This);
  35 Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
  36 Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
  37 Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder,ElementFunction* This);
  38 #endif