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 initializeConstraintVars(CSolver* csolver, SATEncoder* This);
  14 void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This);
  15 Constraint * getNewVarSATEncoder(SATEncoder *This);
  16 void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray);
  17 Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint);
  18 Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
  19 Constraint * generateTransOrderConstraintSATEncoder(SATEncoder *This, Constraint *first,Constraint *second,Constraint *third);
  20 Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
  21 Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
  22 Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint);
  23 Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint);
  24 Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
  25 Constraint * encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
  26 Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
  27 Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
  28
  29 Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value);
  30 Constraint * getElementValueConstraint(Element* This, uint64_t value);
  31
  32 Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This);
  33 Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
  34 Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
  35 Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder,ElementFunction* This);
  36 #endif