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