Bug fix in merge heuristic
[satune.git] / 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         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         void encodeOperatorElementFunctionSATEncoder(ElementFunction *This);
48         Edge encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constraint);
49         Edge encodeOrderSATEncoder(BooleanOrder *constraint);
50         Edge inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second);
51         Edge getPairConstraint(Order *order, OrderPair *pair);
52         Edge getPartialPairConstraint(Order *order, OrderPair *pair);
53         Edge encodeTotalOrderSATEncoder(BooleanOrder *constraint);
54         Edge encodePartialOrderSATEncoder(BooleanOrder *constraint);
55         void createAllTotalOrderConstraintsSATEncoder(Order *order);
56         void createAllPartialOrderConstraintsSATEncoder(Order *order);
57         Edge getOrderConstraint(HashtableOrderPair *table, OrderPair *pair);
58         Edge generateTransOrderConstraintSATEncoder(Edge constIJ, Edge constJK, Edge constIK);
59         Edge generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge jk, Edge kj,Edge ik, Edge ki);
60         Edge encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *constraint);
61         Edge encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint);
62         void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
63         void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This);
64         void generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding);
65         void generateAnyValueBinaryValueEncoding(ElementEncoding *encoding);
66         CNF *cnf;
67         CSolver *solver;
68         BooleanToEdgeMap booledgeMap;
69         VectorEdge *vector;
70 };
71
72 void allocElementConstraintVariables(ElementEncoding *ee, uint numVars);
73 #endif