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(long timeout);
  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         void shouldMemoize(Element *elem, uint64_t val, bool &memo);
  26         Edge getNewVarSATEncoder();
  27         void getArrayNewVarsSATEncoder(uint num, Edge *carray);
  28         Edge encodeVarSATEncoder(BooleanVar *constraint);
  29         Edge encodeLogicSATEncoder(BooleanLogic *constraint);
  30         Edge encodePredicateSATEncoder(BooleanPredicate *constraint);
  31         Edge encodeTablePredicateSATEncoder(BooleanPredicate *constraint);
  32         void encodeElementSATEncoder(Element *element);
  33         void encodeElementFunctionSATEncoder(ElementFunction *function);
  34         void encodeTableElementFunctionSATEncoder(ElementFunction *This);
  35         Edge getElementValueOneHotConstraint(Element *elem, Polarity p, uint64_t value);
  36         Edge getElementValueUnaryConstraint(Element *elem, Polarity p, uint64_t value);
  37         Edge getElementValueBinaryIndexConstraint(Element *element, Polarity p, uint64_t value);
  38         Edge getElementValueBinaryValueConstraint(Element *element, Polarity p, uint64_t value);
  39         Edge getElementValueConstraint(Element *element, Polarity p, uint64_t value);
  40         void generateOneHotEncodingVars(ElementEncoding *encoding);
  41         void generateUnaryEncodingVars(ElementEncoding *encoding);
  42         void generateBinaryIndexEncodingVars(ElementEncoding *encoding);
  43         void generateBinaryValueEncodingVars(ElementEncoding *encoding);
  44         void generateElementEncoding(Element *element);
  45         Edge encodeOperatorPredicateSATEncoder(BooleanPredicate *constraint);
  46         Edge encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint);
  47         Edge encodeUnaryPredicateSATEncoder(BooleanPredicate *constraint);
  48         Edge encodeEnumEqualsPredicateSATEncoder(BooleanPredicate *constraint);
  49         void encodeOperatorElementFunctionSATEncoder(ElementFunction *This);
  50         Edge encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constraint);
  51         Edge encodeOrderSATEncoder(BooleanOrder *constraint);
  52         Edge inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second);
  53         Edge getPairConstraint(Order *order, OrderPair *pair);
  54         Edge getPartialPairConstraint(Order *order, OrderPair *pair);
  55         Edge encodeTotalOrderSATEncoder(BooleanOrder *constraint);
  56         Edge encodePartialOrderSATEncoder(BooleanOrder *constraint);
  57         void createAllTotalOrderConstraintsSATEncoder(Order *order);
  58         void createAllPartialOrderConstraintsSATEncoder(Order *order);
  59         void createAllTotalOrderConstraintsSATEncoderSparse(Order *order);
  60         void createAllPartialOrderConstraintsSATEncoderSparse(Order *order);
  61         Edge getOrderConstraint(HashtableOrderPair *table, OrderPair *pair);
  62         Edge generateTransOrderConstraintSATEncoder(Edge constIJ, Edge constJK, Edge constIK);
  63         Edge generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge jk, Edge kj,Edge ik, Edge ki);
  64         Edge encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *constraint);
  65         Edge encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint);
  66         void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
  67         void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This);
  68         void generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding);
  69         int getMaximumUsedSize(ElementEncoding *encoding);
  70         void generateAnyValueBinaryIndexEncodingPositive(ElementEncoding *encoding);
  71         void generateAnyValueBinaryValueEncoding(ElementEncoding *encoding);
  72         CNF *cnf;
  73         CSolver *solver;
  74         BooleanToEdgeMap booledgeMap;
  75         VectorEdge *vector;
  76         friend class VarOrderingOpt;
  77 };
  78
  79 void allocElementConstraintVariables(ElementEncoding *ee, uint numVars);
  80 #endif