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