1 #include "satencoder.h"
9 #include "orderencoder.h"
10 #include "ordergraph.h"
11 #include "orderedge.h"
13 #include "predicate.h"
14 #include "orderelement.h"
16 Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
17 if(constraint->order->order.type == INTEGERENCODING){
18 return orderIntegerEncodingSATEncoder(This, constraint);
20 switch ( constraint->order->type) {
22 return encodePartialOrderSATEncoder(This, constraint);
24 return encodeTotalOrderSATEncoder(This, constraint);
31 Edge orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
32 if(boolOrder->order->graph == NULL){
33 bool doOptOrderStructure=GETVARTUNABLE(This->solver->tuner, boolOrder->order->type,
34 OPTIMIZEORDERSTRUCTURE, &onoff);
35 if (doOptOrderStructure ) {
36 boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
37 reachMustAnalysis(This->solver, boolOrder->order->graph, true);
40 Order* order = boolOrder->order;
41 Edge gvalue = inferOrderConstraintFromGraph(order, boolOrder->first, boolOrder->second);
42 if(!edgeIsNull(gvalue))
45 if (boolOrder->order->elementTable == NULL) {
46 boolOrder->order->initializeOrderElementsHashTable();
48 //getting two elements and using LT predicate ...
49 Element* elem1 = getOrderIntegerElement(This, order, boolOrder->first);
50 ElementEncoding *encoding = getElementEncoding(elem1);
51 if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
52 setElementEncodingType(encoding, BINARYINDEX);
53 encodingArrayInitialization(encoding);
55 Element* elem2 = getOrderIntegerElement(This, order, boolOrder->second);
56 encoding = getElementEncoding(elem2);
57 if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
58 setElementEncodingType(encoding, BINARYINDEX);
59 encodingArrayInitialization(encoding);
61 Set * sarray[]={order->set, order->set};
62 Predicate *predicate =new PredicateOperator(LT, sarray, 2);
63 Element * parray[]={elem1, elem2};
64 BooleanPredicate * boolean=new BooleanPredicate(predicate, parray, 2, NULL);
65 setFunctionEncodingType(boolean->getFunctionEncoding(), CIRCUIT);
66 {//Adding new elements and boolean/predicate to solver regarding memory management
67 pushVectorBoolean(This->solver->allBooleans, boolean);
68 pushVectorPredicate(This->solver->allPredicates, predicate);
69 pushVectorElement(This->solver->allElements, elem1);
70 pushVectorElement(This->solver->allElements, elem2);
72 return encodeConstraintSATEncoder(This, boolean);
75 Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _second){
76 if (order->graph != NULL) {
77 OrderGraph *graph=order->graph;
78 OrderNode *first=lookupOrderNodeFromOrderGraph(graph, _first);
79 OrderNode *second=lookupOrderNodeFromOrderGraph(graph, _second);
80 if ((first != NULL) && (second != NULL)) {
81 OrderEdge *edge=lookupOrderEdgeFromOrderGraph(graph, first, second);
85 else if (edge->mustNeg)
88 OrderEdge *invedge=getOrderEdgeFromOrderGraph(graph, second, first);
89 if (invedge != NULL) {
92 else if (invedge->mustNeg)
100 Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) {
101 HashSetOrderElement* eset = order->elementTable;
102 OrderElement oelement ={item, NULL};
103 if( !containsHashSetOrderElement(eset, &oelement)){
104 Element* elem = new ElementSet(order->set);
105 ElementEncoding* encoding = getElementEncoding(elem);
106 setElementEncodingType(encoding, BINARYINDEX);
107 encodingArrayInitialization(encoding);
108 encodeElementSATEncoder(This, elem);
109 addHashSetOrderElement(eset, allocOrderElement(item, elem));
112 return getHashSetOrderElement(eset, &oelement)->elem;
114 Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
115 Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
116 if(!edgeIsNull(gvalue))
119 HashTableOrderPair *table = order->orderPairTable;
122 if (pair->first < pair->second) {
124 flipped.first = pair->second;
125 flipped.second = pair->first;
129 if (!containsOrderPair(table, pair)) {
130 constraint = getNewVarSATEncoder(This);
131 OrderPair *paircopy = allocOrderPair(pair->first, pair->second, constraint);
132 putOrderPair(table, paircopy, paircopy);
134 constraint = getOrderPair(table, pair)->constraint;
136 return negate ? constraintNegate(constraint) : constraint;
139 Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) {
140 ASSERT(boolOrder->order->type == TOTAL);
141 if (boolOrder->order->orderPairTable == NULL) {
142 boolOrder->order->initializeOrderHashTable();
143 bool doOptOrderStructure=GETVARTUNABLE(This->solver->tuner, boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
144 if (doOptOrderStructure) {
145 boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
146 reachMustAnalysis(This->solver, boolOrder->order->graph, true);
148 createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
150 OrderPair pair = {boolOrder->first, boolOrder->second, E_NULL};
151 Edge constraint = getPairConstraint(This, boolOrder->order, &pair);
156 void createAllTotalOrderConstraintsSATEncoder(SATEncoder *This, Order *order) {
158 model_print("in total order ...\n");
160 ASSERT(order->type == TOTAL);
161 VectorInt *mems = order->set->members;
162 uint size = getSizeVectorInt(mems);
163 for (uint i = 0; i < size; i++) {
164 uint64_t valueI = getVectorInt(mems, i);
165 for (uint j = i + 1; j < size; j++) {
166 uint64_t valueJ = getVectorInt(mems, j);
167 OrderPair pairIJ = {valueI, valueJ};
168 Edge constIJ = getPairConstraint(This, order, &pairIJ);
169 for (uint k = j + 1; k < size; k++) {
170 uint64_t valueK = getVectorInt(mems, k);
171 OrderPair pairJK = {valueJ, valueK};
172 OrderPair pairIK = {valueI, valueK};
173 Edge constIK = getPairConstraint(This, order, &pairIK);
174 Edge constJK = getPairConstraint(This, order, &pairJK);
175 addConstraintCNF(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK));
181 Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair) {
182 ASSERT(pair->first != pair->second);
185 if (pair->first < pair->second) {
187 flipped.first = pair->second;
188 flipped.second = pair->first;
191 if (!containsOrderPair(table, pair)) {
194 Edge constraint = getOrderPair(table, pair)->constraint;
195 ASSERT(!edgeIsNull(constraint));
196 return negate ? constraintNegate(constraint) : constraint;
199 Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK) {
200 Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
201 Edge loop1 = constraintOR(This->cnf, 3, carray);
202 Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK};
203 Edge loop2 = constraintOR(This->cnf, 3, carray2 );
204 return constraintAND2(This->cnf, loop1, loop2);
207 Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
208 ASSERT(constraint->order->type == PARTIAL);