#include "structs.h"
#include "common.h"
#include "order.h"
+#include "csolver.h"
#include "orderpair.h"
#include "set.h"
+#include "tunable.h"
+#include "orderencoder.h"
+#include "ordergraph.h"
+#include "orderedge.h"
+#include "element.h"
+#include "predicate.h"
+#include "orderelement.h"
Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
+ if(constraint->order->order.type == INTEGERENCODING){
+ return orderIntegerEncodingSATEncoder(This, constraint);
+ }
switch ( constraint->order->type) {
case PARTIAL:
return encodePartialOrderSATEncoder(This, constraint);
return E_BOGUS;
}
-Edge getPairConstraint(SATEncoder *This, HashTableOrderPair *table, OrderPair *pair) {
+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);
+ }
+ Predicate *predicate =allocPredicateOperator(LT, (Set*[]){order->set, order->set}, 2);
+ Boolean * boolean=allocBooleanPredicate(predicate, (Element *[]){elem1,elem2}, 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){
+ if (order->graph != NULL) {
+ OrderGraph *graph=order->graph;
+ OrderNode *first=lookupOrderNodeFromOrderGraph(graph, _first);
+ OrderNode *second=lookupOrderNodeFromOrderGraph(graph, _second);
+ if ((first != NULL) && (second != NULL)) {
+ OrderEdge *edge=lookupOrderEdgeFromOrderGraph(graph, first, second);
+ if (edge != NULL) {
+ if (edge->mustPos)
+ return E_True;
+ else if (edge->mustNeg)
+ return E_False;
+ }
+ OrderEdge *invedge=getOrderEdgeFromOrderGraph(graph, second, first);
+ if (invedge != NULL) {
+ if (invedge->mustPos)
+ return E_False;
+ else if (invedge->mustNeg)
+ return E_True;
+ }
+ }
+ }
+ 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 gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
+ if(!edgeIsNull(gvalue))
+ return gvalue;
+
+ HashTableOrderPair *table = order->orderPairTable;
bool negate = false;
OrderPair flipped;
if (pair->first < pair->second) {
ASSERT(boolOrder->order->type == TOTAL);
if (boolOrder->order->orderPairTable == NULL) {
initializeOrderHashTable(boolOrder->order);
+ 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);
+ }
createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
}
- HashTableOrderPair *orderPairTable = boolOrder->order->orderPairTable;
OrderPair pair = {boolOrder->first, boolOrder->second, E_NULL};
- Edge constraint = getPairConstraint(This, orderPairTable, &pair);
+ Edge constraint = getPairConstraint(This, boolOrder->order, &pair);
return constraint;
}
#endif
ASSERT(order->type == TOTAL);
VectorInt *mems = order->set->members;
- HashTableOrderPair *table = order->orderPairTable;
uint size = getSizeVectorInt(mems);
for (uint i = 0; i < size; i++) {
uint64_t valueI = getVectorInt(mems, i);
for (uint j = i + 1; j < size; j++) {
uint64_t valueJ = getVectorInt(mems, j);
OrderPair pairIJ = {valueI, valueJ};
- Edge constIJ = getPairConstraint(This, table, &pairIJ);
+ Edge constIJ = getPairConstraint(This, 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, table, &pairIK);
- Edge constJK = getPairConstraint(This, table, &pairJK);
+ Edge constIK = getPairConstraint(This, order, &pairIK);
+ Edge constJK = getPairConstraint(This, order, &pairJK);
addConstraintCNF(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK));
}
}
projects / satune.git / blobdiff