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 #include "constraint.h"
   8 #include "satelemencoder.h"
   9 #include "satorderencoder.h"
  10 #include "satfunctableencoder.h"
  11
  12
  13 class SATEncoder {
  14  public:
  15         int solve();
  16         SATEncoder(CSolver *solver);
  17         ~SATEncoder();
  18         void encodeAllSATEncoder(CSolver *csolver);
  19         Edge encodeConstraintSATEncoder(Boolean *constraint);
  20         CNF * getCNF() { return cnf;}
  21         CSolver * getSolver() { return solver; }
  22         long long getSolveTime() { return cnf->solveTime; }
  23         long long getEncodeTime() { return cnf->encodeTime; }
  24
  25         MEMALLOC;
  26  private:
  27         CNF *cnf;
  28         CSolver *solver;
  29 };
  30
  31 Edge getNewVarSATEncoder(SATEncoder *This);
  32 void getArrayNewVarsSATEncoder(SATEncoder *encoder, uint num, Edge *carray);
  33
  34 Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar *constraint);
  35 Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic *constraint);
  36 Edge encodePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
  37 Edge encodeTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
  38 void encodeElementSATEncoder(SATEncoder *encoder, Element *This);
  39 void encodeElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This);
  40 void encodeTableElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This);
  41 #endif