#include "orderpair.h"
#include "set.h"
#include "tunable.h"
-#include "orderencoder.h"
+#include "orderanalysis.h"
#include "ordergraph.h"
#include "orderedge.h"
#include "element.h"
#include "predicate.h"
#include "orderelement.h"
+#include "orderpairresolver.h"
-Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
- if(constraint->order->order.type == INTEGERENCODING){
- return orderIntegerEncodingSATEncoder(This, constraint);
- }
+Edge SATEncoder::encodeOrderSATEncoder(BooleanOrder *constraint) {
switch ( constraint->order->type) {
- case PARTIAL:
- return encodePartialOrderSATEncoder(This, constraint);
- case TOTAL:
- return encodeTotalOrderSATEncoder(This, constraint);
+ case SATC_PARTIAL:
+ return encodePartialOrderSATEncoder(constraint);
+ case SATC_TOTAL:
+ return encodeTotalOrderSATEncoder(constraint);
default:
ASSERT(0);
}
return E_BOGUS;
}
-Edge orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
- if(boolOrder->order->graph == NULL){
- bool doOptOrderStructure=GETVARTUNABLE(This->solver->tuner, boolOrder->order->type,
- OPTIMIZEORDERSTRUCTURE, &onoff);
- if (doOptOrderStructure ) {
- boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
- reachMustAnalysis(This->solver, boolOrder->order->graph, true);
- }
- }
- Order* order = boolOrder->order;
- Edge gvalue = inferOrderConstraintFromGraph(order, boolOrder->first, boolOrder->second);
- if(!edgeIsNull(gvalue))
- return gvalue;
-
- if (boolOrder->order->elementTable == NULL) {
- initializeOrderElementsHashTable(boolOrder->order);
- }
- //getting two elements and using LT predicate ...
- Element* elem1 = getOrderIntegerElement(This, order, boolOrder->first);
- ElementEncoding *encoding = getElementEncoding(elem1);
- if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
- setElementEncodingType(encoding, BINARYINDEX);
- encodingArrayInitialization(encoding);
- }
- Element* elem2 = getOrderIntegerElement(This, order, boolOrder->second);
- encoding = getElementEncoding(elem2);
- if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
- setElementEncodingType(encoding, BINARYINDEX);
- encodingArrayInitialization(encoding);
- }
- Set * sarray[]={order->set, order->set};
- Predicate *predicate =allocPredicateOperator(LT, sarray, 2);
- Element * parray[]={elem1, elem2};
- Boolean * boolean=allocBooleanPredicate(predicate, parray, 2, NULL);
- setFunctionEncodingType(getPredicateFunctionEncoding((BooleanPredicate*)boolean), CIRCUIT);
- {//Adding new elements and boolean/predicate to solver regarding memory management
- pushVectorBoolean(This->solver->allBooleans, boolean);
- pushVectorPredicate(This->solver->allPredicates, predicate);
- pushVectorElement(This->solver->allElements, elem1);
- pushVectorElement(This->solver->allElements, elem2);
- }
- return encodeConstraintSATEncoder(This, boolean);
-}
-
-Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _second){
+Edge SATEncoder::inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second) {
if (order->graph != NULL) {
- OrderGraph *graph=order->graph;
- OrderNode *first=lookupOrderNodeFromOrderGraph(graph, _first);
- OrderNode *second=lookupOrderNodeFromOrderGraph(graph, _second);
+ OrderGraph *graph = order->graph;
+ OrderNode *first = graph->lookupOrderNodeFromOrderGraph(_first);
+ OrderNode *second = graph->lookupOrderNodeFromOrderGraph(_second);
if ((first != NULL) && (second != NULL)) {
- OrderEdge *edge=lookupOrderEdgeFromOrderGraph(graph, first, second);
+ OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(first, second);
if (edge != NULL) {
if (edge->mustPos)
return E_True;
else if (edge->mustNeg)
return E_False;
}
- OrderEdge *invedge=getOrderEdgeFromOrderGraph(graph, second, first);
+ OrderEdge *invedge = graph->lookupOrderEdgeFromOrderGraph(second, first);
if (invedge != NULL) {
if (invedge->mustPos)
return E_False;
return E_NULL;
}
-Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) {
- HashSetOrderElement* eset = order->elementTable;
- OrderElement oelement ={item, NULL};
- if( !containsHashSetOrderElement(eset, &oelement)){
- Element* elem = allocElementSet(order->set);
- ElementEncoding* encoding = getElementEncoding(elem);
- setElementEncodingType(encoding, BINARYINDEX);
- encodingArrayInitialization(encoding);
- encodeElementSATEncoder(This, elem);
- addHashSetOrderElement(eset, allocOrderElement(item, elem));
- return elem;
- }else
- return getHashSetOrderElement(eset, &oelement)->elem;
-}
-Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
+Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) {
Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
- if(!edgeIsNull(gvalue))
+ if (!edgeIsNull(gvalue))
return gvalue;
-
- HashTableOrderPair *table = order->orderPairTable;
+
+ HashtableOrderPair *table = order->getOrderPairTable();
bool negate = false;
OrderPair flipped;
if (pair->first < pair->second) {
flipped.second = pair->first;
pair = &flipped;
}
- Edge constraint;
- if (!containsOrderPair(table, pair)) {
- constraint = getNewVarSATEncoder(This);
- OrderPair *paircopy = allocOrderPair(pair->first, pair->second, constraint);
- putOrderPair(table, paircopy, paircopy);
- } else
- constraint = getOrderPair(table, pair)->constraint;
-
- return negate ? constraintNegate(constraint) : constraint;
+ OrderPair *tmp;
+ if (!(table->contains(pair))) {
+ tmp = new OrderPair(pair->first, pair->second, getNewVarSATEncoder());
+ table->put(tmp, tmp);
+ } else {
+ tmp = table->get(pair);
+ }
+ return negate ? tmp->getNegatedConstraint() : tmp->getConstraint();
+}
+
+Edge SATEncoder::getPartialPairConstraint(Order *order, OrderPair *pair) {
+ Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
+ if (!edgeIsNull(gvalue))
+ return gvalue;
+
+ HashtableOrderPair *table = order->getOrderPairTable();
+
+ OrderPair *tmp;
+ if (!(table->contains(pair))) {
+ Edge constraint = getNewVarSATEncoder();
+ tmp = new OrderPair(pair->first, pair->second, constraint);
+ table->put(tmp, tmp);
+ Edge constraint2 = getNewVarSATEncoder();
+ OrderPair *swap = new OrderPair(pair->second, pair->first, constraint2);
+ table->put(swap, swap);
+ addConstraintCNF(cnf, constraintNegate(constraintAND2(cnf, constraint, constraint2)));
+ } else {
+ tmp = table->get(pair);
+ }
+ return tmp->getConstraint();
}
-Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) {
- ASSERT(boolOrder->order->type == TOTAL);
- if (boolOrder->order->orderPairTable == NULL) {
- initializeOrderHashTable(boolOrder->order);
- bool doOptOrderStructure=GETVARTUNABLE(This->solver->tuner, boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
+Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) {
+ ASSERT(boolOrder->order->type == SATC_TOTAL);
+ if (boolOrder->order->encoding.resolver == NULL) {
+ //This is pairwised encoding ...
+ boolOrder->order->setOrderResolver(new OrderPairResolver(solver, boolOrder->order));
+ bool doOptOrderStructure = GETVARTUNABLE(solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
if (doOptOrderStructure) {
+ ASSERT(boolOrder->order->graph == NULL);
boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
- reachMustAnalysis(This->solver, boolOrder->order->graph, true);
+ reachMustAnalysis(solver, boolOrder->order->graph, true);
}
- createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
+ if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0)
+ createAllTotalOrderConstraintsSATEncoderSparse(boolOrder->order);
+ else
+ createAllTotalOrderConstraintsSATEncoder(boolOrder->order);
}
- OrderPair pair = {boolOrder->first, boolOrder->second, E_NULL};
- Edge constraint = getPairConstraint(This, boolOrder->order, &pair);
+ OrderPair pair(boolOrder->first, boolOrder->second, E_NULL);
+ Edge constraint = getPairConstraint(boolOrder->order, &pair);
return constraint;
}
-void createAllTotalOrderConstraintsSATEncoder(SATEncoder *This, Order *order) {
-#ifdef TRACE_DEBUG
+void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *order) {
+#ifdef CONFIG_DEBUG
model_print("in total order ...\n");
#endif
- ASSERT(order->type == TOTAL);
- VectorInt *mems = order->set->members;
- uint size = getSizeVectorInt(mems);
+ ASSERT(order->type == SATC_TOTAL);
+ Set *set = order->set;
+ uint size = order->set->getSize();
for (uint i = 0; i < size; i++) {
- uint64_t valueI = getVectorInt(mems, i);
+ uint64_t valueI = set->getElement(i);
for (uint j = i + 1; j < size; j++) {
- uint64_t valueJ = getVectorInt(mems, j);
- OrderPair pairIJ = {valueI, valueJ};
- Edge constIJ = getPairConstraint(This, order, &pairIJ);
+ uint64_t valueJ = set->getElement(j);
+ OrderPair pairIJ(valueI, valueJ, E_NULL);
+ Edge constIJ = getPairConstraint(order, &pairIJ);
for (uint k = j + 1; k < size; k++) {
- uint64_t valueK = getVectorInt(mems, k);
- OrderPair pairJK = {valueJ, valueK};
- OrderPair pairIK = {valueI, valueK};
- Edge constIK = getPairConstraint(This, order, &pairIK);
- Edge constJK = getPairConstraint(This, order, &pairJK);
- addConstraintCNF(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK));
+ uint64_t valueK = set->getElement(k);
+ OrderPair pairJK(valueJ, valueK, E_NULL);
+ OrderPair pairIK(valueI, valueK, E_NULL);
+ Edge constIK = getPairConstraint(order, &pairIK);
+ Edge constJK = getPairConstraint(order, &pairJK);
+ addConstraintCNF(cnf, generateTransOrderConstraintSATEncoder(constIJ, constJK, constIK));
}
}
}
}
-Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair) {
- ASSERT(pair->first != pair->second);
- bool negate = false;
- OrderPair flipped;
- if (pair->first < pair->second) {
- negate = true;
- flipped.first = pair->second;
- flipped.second = pair->first;
- pair = &flipped;
+Edge SATEncoder::generateTransOrderConstraintSATEncoder(Edge constIJ,Edge constJK,Edge constIK) {
+ Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
+ Edge loop1 = constraintOR(cnf, 3, carray);
+ Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK};
+ Edge loop2 = constraintOR(cnf, 3, carray2 );
+ return constraintAND2(cnf, loop1, loop2);
+}
+
+Edge SATEncoder::generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge jk, Edge kj,Edge ik, Edge ki) {
+ Edge uoIJ = constraintAND2(cnf, constraintNegate(ij), constraintNegate(ji));
+ Edge uoJK = constraintAND2(cnf, constraintNegate(jk), constraintNegate(kj));
+ Edge uoIK = constraintAND2(cnf, constraintNegate(ik), constraintNegate(ki));
+
+ Edge t1[] = {ij, jk, ik};
+ Edge t2[] = {ji, jk, ik};
+ Edge t3[] = {ij, kj, ki};
+ Edge t4[] = {ij, kj, ik};
+ Edge t5[] = {ji, jk, ki};
+ Edge t6[] = {ji, kj, ki};
+ Edge ct1 = constraintAND(cnf, 3, t1);
+ Edge ct2 = constraintAND(cnf, 3, t2);
+ Edge ct3 = constraintAND(cnf, 3, t3);
+ Edge ct4 = constraintAND(cnf, 3, t4);
+ Edge ct5 = constraintAND(cnf, 3, t5);
+ Edge ct6 = constraintAND(cnf, 3, t6);
+
+ Edge p1[] = {uoIJ, jk, ik};
+ Edge p2[] = {ij, kj, uoIK};
+ Edge p3[] = {ji, uoJK, ki};
+ Edge p4[] = {uoIJ, kj, ki};
+ Edge p5[] = {ji, jk, uoIK};
+ Edge p6[] = {ij, uoJK, ik};
+ Edge cp1 = constraintAND(cnf, 3, p1);
+ Edge cp2 = constraintAND(cnf, 3, p2);
+ Edge cp3 = constraintAND(cnf, 3, p3);
+ Edge cp4 = constraintAND(cnf, 3, p4);
+ Edge cp5 = constraintAND(cnf, 3, p5);
+ Edge cp6 = constraintAND(cnf, 3, p6);
+
+ Edge o1[] = {uoIJ, uoJK, ik};
+ Edge o2[] = {ij, uoJK, uoIK};
+ Edge o3[] = {uoIK, jk, uoIK};
+ Edge o4[] = {ji, uoJK, uoIK};
+ Edge o5[] = {uoIJ, uoJK, ki};
+ Edge o6[] = {uoIJ, kj, uoIK};
+ Edge co1 = constraintAND(cnf, 3, o1);
+ Edge co2 = constraintAND(cnf, 3, o2);
+ Edge co3 = constraintAND(cnf, 3, o3);
+ Edge co4 = constraintAND(cnf, 3, o4);
+ Edge co5 = constraintAND(cnf, 3, o5);
+ Edge co6 = constraintAND(cnf, 3, o6);
+
+ Edge unorder [] = {uoIJ, uoJK, uoIK};
+ Edge cunorder = constraintAND(cnf, 3, unorder);
+
+
+ Edge res[] = {ct1,ct2,ct3,ct4,ct5,ct6,
+ cp1,cp2,cp3,cp4,cp5,cp6,
+ co1,co2,co3,co4,co5,co6,
+ cunorder};
+ return constraintOR(cnf, 19, res);
+}
+
+Edge SATEncoder::encodePartialOrderSATEncoder(BooleanOrder *boolOrder) {
+ ASSERT(boolOrder->order->type == SATC_PARTIAL);
+ if (boolOrder->order->encoding.resolver == NULL) {
+ //This is pairwised encoding ...
+ boolOrder->order->setOrderResolver(new OrderPairResolver(solver, boolOrder->order));
+ bool doOptOrderStructure = GETVARTUNABLE(solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
+ if (doOptOrderStructure) {
+ boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
+ reachMustAnalysis(solver, boolOrder->order->graph, true);
+ }
+ if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0)
+ createAllPartialOrderConstraintsSATEncoderSparse(boolOrder->order);
+ else
+ createAllPartialOrderConstraintsSATEncoder(boolOrder->order);
}
- if (!containsOrderPair(table, pair)) {
- return E_NULL;
+ OrderPair pair(boolOrder->first, boolOrder->second, E_NULL);
+ Edge constraint = getPartialPairConstraint(boolOrder->order, &pair);
+ return constraint;
+}
+
+
+void SATEncoder::createAllPartialOrderConstraintsSATEncoder(Order *order) {
+#ifdef CONFIG_DEBUG
+ model_print("in partial order ...\n");
+#endif
+ ASSERT(order->type == SATC_TOTAL);
+ Set *set = order->set;
+ uint size = order->set->getSize();
+ for (uint i = 0; i < size; i++) {
+ uint64_t valueI = set->getElement(i);
+ for (uint j = i + 1; j < size; j++) {
+ uint64_t valueJ = set->getElement(j);
+ OrderPair pairIJ(valueI, valueJ, E_NULL);
+ OrderPair pairJI(valueJ, valueI, E_NULL);
+ Edge constIJ = getPartialPairConstraint(order, &pairIJ);
+ Edge constJI = getPartialPairConstraint(order, &pairJI);
+ for (uint k = j + 1; k < size; k++) {
+ uint64_t valueK = set->getElement(k);
+ OrderPair pairJK(valueJ, valueK, E_NULL);
+ OrderPair pairIK(valueI, valueK, E_NULL);
+ Edge constIK = getPartialPairConstraint(order, &pairIK);
+ Edge constJK = getPartialPairConstraint(order, &pairJK);
+ OrderPair pairKJ(valueK, valueJ, E_NULL);
+ OrderPair pairKI(valueK, valueI, E_NULL);
+ Edge constKI = getPartialPairConstraint(order, &pairKI);
+ Edge constKJ = getPartialPairConstraint(order, &pairKJ);
+ addConstraintCNF(cnf, generatePartialOrderConstraintsSATEncoder(constIJ, constJI,
+ constJK, constKJ, constIK, constKI));
+ }
+ }
}
- Edge constraint = getOrderPair(table, pair)->constraint;
- ASSERT(!edgeIsNull(constraint));
- return negate ? constraintNegate(constraint) : constraint;
}
-Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK) {
- Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
- Edge loop1 = constraintOR(This->cnf, 3, carray);
- Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK};
- Edge loop2 = constraintOR(This->cnf, 3, carray2 );
- return constraintAND2(This->cnf, loop1, loop2);
+void SATEncoder::createAllTotalOrderConstraintsSATEncoderSparse(Order *order) {
+#ifdef CONFIG_DEBUG
+ model_print("in total order ...\n");
+#endif
+ ASSERT(order->type == SATC_TOTAL);
+ SetIterator64Int *iti = order->getUsedIterator();
+ while (iti->hasNext()) {
+ uint64_t valueI = iti->next();
+ SetIterator64Int *itj = new SetIterator64Int(iti);
+ while (itj->hasNext()) {
+ uint64_t valueJ = itj->next();
+ OrderPair pairIJ(valueI, valueJ, E_NULL);
+ Edge constIJ = getPairConstraint(order, &pairIJ);
+ SetIterator64Int *itk = new SetIterator64Int(itj);
+ while (itk->hasNext()) {
+ uint64_t valueK = itk->next();
+ OrderPair pairJK(valueJ, valueK, E_NULL);
+ OrderPair pairIK(valueI, valueK, E_NULL);
+ Edge constIK = getPairConstraint(order, &pairIK);
+ Edge constJK = getPairConstraint(order, &pairJK);
+ addConstraintCNF(cnf, generateTransOrderConstraintSATEncoder(constIJ, constJK, constIK));
+ }
+ }
+ }
}
-Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
- ASSERT(constraint->order->type == PARTIAL);
- return E_BOGUS;
+void SATEncoder::createAllPartialOrderConstraintsSATEncoderSparse(Order *order) {
+#ifdef CONFIG_DEBUG
+ model_print("in partial order ...\n");
+#endif
+ ASSERT(order->type == SATC_TOTAL);
+ SetIterator64Int *iti = order->getUsedIterator();
+ while (iti->hasNext()) {
+ uint64_t valueI = iti->next();
+ SetIterator64Int *itj = new SetIterator64Int(iti);
+ while (itj->hasNext()) {
+ uint64_t valueJ = itj->next();
+ OrderPair pairIJ(valueI, valueJ, E_NULL);
+ OrderPair pairJI(valueJ, valueI, E_NULL);
+ Edge constIJ = getPartialPairConstraint(order, &pairIJ);
+ Edge constJI = getPartialPairConstraint(order, &pairJI);
+ SetIterator64Int *itk = new SetIterator64Int(itj);
+ while (itk->hasNext()) {
+ uint64_t valueK = itk->next();
+ OrderPair pairJK(valueJ, valueK, E_NULL);
+ OrderPair pairIK(valueI, valueK, E_NULL);
+ Edge constIK = getPartialPairConstraint(order, &pairIK);
+ Edge constJK = getPartialPairConstraint(order, &pairJK);
+ OrderPair pairKJ(valueK, valueJ, E_NULL);
+ OrderPair pairKI(valueK, valueI, E_NULL);
+ Edge constKI = getPartialPairConstraint(order, &pairKI);
+ Edge constKJ = getPartialPairConstraint(order, &pairKJ);
+ addConstraintCNF(cnf, generatePartialOrderConstraintsSATEncoder(constIJ, constJI,
+
+
+ constJK, constKJ, constIK, constKI));
+ }
+ }
+ }
}
projects / satune.git / blobdiff