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
   9 typedef Hashtable<Boolean *, Node *, uintptr_t, 4> BooleanToEdgeMap;
  10
  11 class SATEncoder {
  12 public:
  13         int solve();
  14         SATEncoder(CSolver *solver);
  15         ~SATEncoder();
  16         void resetSATEncoder();
  17         void encodeAllSATEncoder(CSolver *csolver);
  18         Edge encodeConstraintSATEncoder(BooleanEdge constraint);
  19         CNF *getCNF() { return cnf;}
  20         long long getSolveTime() { return cnf->solveTime; }
  21         long long getEncodeTime() { return cnf->encodeTime; }
  22
  23         CMEMALLOC;
  24 private:
  25         Edge getNewVarSATEncoder();
  26         void getArrayNewVarsSATEncoder(uint num, Edge *carray);
  27         Edge encodeVarSATEncoder(BooleanVar *constraint);
  28         Edge encodeLogicSATEncoder(BooleanLogic *constraint);
  29         Edge encodePredicateSATEncoder(BooleanPredicate *constraint);
  30         Edge encodeTablePredicateSATEncoder(BooleanPredicate *constraint);
  31         void encodeElementSATEncoder(Element *element);
  32         void encodeElementFunctionSATEncoder(ElementFunction *function);
  33         void encodeTableElementFunctionSATEncoder(ElementFunction *This);
  34         Edge getElementValueOneHotConstraint(Element *elem, uint64_t value);
  35         Edge getElementValueUnaryConstraint(Element *elem, uint64_t value);
  36         Edge getElementValueBinaryIndexConstraint(Element *element, uint64_t value);
  37         Edge getElementValueBinaryValueConstraint(Element *element, uint64_t value);
  38         Edge getElementValueConstraint(Element *element, uint64_t value);
  39         void generateOneHotEncodingVars(ElementEncoding *encoding);
  40         void generateUnaryEncodingVars(ElementEncoding *encoding);
  41         void generateBinaryIndexEncodingVars(ElementEncoding *encoding);
  42         void generateBinaryValueEncodingVars(ElementEncoding *encoding);
  43         void generateElementEncoding(Element *element);
  44         Edge encodeOperatorPredicateSATEncoder(BooleanPredicate *constraint);
  45         Edge encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint);
  46         void encodeOperatorElementFunctionSATEncoder(ElementFunction *This);
  47         Edge encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constraint);
  48         Edge encodeOrderSATEncoder(BooleanOrder *constraint);
  49         Edge inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second);
  50         Edge getPairConstraint(Order *order, OrderPair *pair);
  51         Edge getPartialPairConstraint(Order *order, OrderPair *pair);
  52         Edge encodeTotalOrderSATEncoder(BooleanOrder *constraint);
  53         Edge encodePartialOrderSATEncoder(BooleanOrder *constraint);
  54         void createAllTotalOrderConstraintsSATEncoder(Order *order);
  55         void createAllPartialOrderConstraintsSATEncoder(Order *order);
  56         Edge getOrderConstraint(HashtableOrderPair *table, OrderPair *pair);
  57         Edge generateTransOrderConstraintSATEncoder(Edge constIJ, Edge constJK, Edge constIK);
  58         Edge generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge jk, Edge kj,Edge ik, Edge ki);
  59         Edge encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *constraint);
  60         Edge encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint);
  61         void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
  62         void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This);
  63
  64         CNF *cnf;
  65         CSolver *solver;
  66         BooleanToEdgeMap booledgeMap;
  67         VectorEdge *vector;
  68 };
  69
  70 void allocElementConstraintVariables(ElementEncoding *ee, uint numVars);
  71 #endif