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