src/Backend/satencoder.h

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