orderPairTable(NULL),
elementTable(NULL),
graph(NULL),
- order(this) {
+ order(this)
+{
+ auxSet = new Set(_type,(uint64_t) 1,(uint64_t) _set->getSize());
}
void Order::initializeOrderHashTable() {
~Order();
OrderType type;
Set *set;
+ Set* auxSet;
HashTableOrderPair *orderPairTable;
HashSetOrderElement* elementTable;
OrderGraph *graph;
delete iterator;
}
-void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
- Vector<Order *> ordervec;
- Vector<Order *> partialcandidatevec;
- uint size = order->constraints.getSize();
- for (uint i = 0; i < size; i++) {
- BooleanOrder *orderconstraint = order->constraints.get(i);
- OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
- OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
- model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
- if (from->sccNum != to->sccNum) {
- OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
- if (edge->polPos) {
- replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
- } else if (edge->polNeg) {
- replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
- } else {
- //This case should only be possible if constraint isn't in AST
- ASSERT(0);
- }
- } else {
- //Build new order and change constraint's order
- Order *neworder = NULL;
- if (ordervec.getSize() > from->sccNum)
- neworder = ordervec.get(from->sccNum);
- if (neworder == NULL) {
- MutableSet *set = new MutableSet(order->set->type);
- neworder = new Order(order->type, set);
- This->allOrders.push(neworder);
- ordervec.setExpand(from->sccNum, neworder);
- if (order->type == PARTIAL)
- partialcandidatevec.setExpand(from->sccNum, neworder);
- else
- partialcandidatevec.setExpand(from->sccNum, NULL);
- }
- if (from->status != ADDEDTOSET) {
- from->status = ADDEDTOSET;
- ((MutableSet *)neworder->set)->addElementMSet(from->id);
- }
- if (to->status != ADDEDTOSET) {
- to->status = ADDEDTOSET;
- ((MutableSet *)neworder->set)->addElementMSet(to->id);
- }
- if (order->type == PARTIAL) {
- OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
- if (edge->polNeg)
- partialcandidatevec.setExpand(from->sccNum, NULL);
- }
- orderconstraint->order = neworder;
- neworder->addOrderConstraint(orderconstraint);
- }
- }
-
- uint pcvsize=partialcandidatevec.getSize();
- for(uint i=0;i<pcvsize;i++) {
- Order * neworder=partialcandidatevec.get(i);
- if (neworder != NULL){
- neworder->type = TOTAL;
- model_print("i=%u\t", i);
- }
- }
-}
-
void orderAnalysis(CSolver *This) {
uint size = This->allOrders.getSize();
for (uint i = 0; i < size; i++) {
Order *order = This->allOrders.get(i);
- bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff);
- if (!doDecompose)
- continue;
- OrderGraph *graph = buildOrderGraph(order);
- if (order->type == PARTIAL) {
- //Required to do SCC analysis for partial order graphs. It
- //makes sure we don't incorrectly optimize graphs with negative
- //polarity edges
- completePartialOrderGraph(graph);
- }
-
-
+ OrderGraph *graph;
+ if(order->graph == NULL){
+ graph= buildOrderGraph(order);
+ if (order->type == PARTIAL) {
+ //Required to do SCC analysis for partial order graphs. It
+ //makes sure we don't incorrectly optimize graphs with negative
+ //polarity edges
+ completePartialOrderGraph(graph);
+ }
+ }else
+ graph = order->graph;
+
bool mustReachGlobal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHGLOBAL, &onoff);
if (mustReachGlobal)
if (mustReachPrune)
removeMustBeTrueNodes(This, graph);
- //This is needed for splitorder
- computeStronglyConnectedComponentGraph(graph);
-
- decomposeOrder(This, order, graph);
-
- deleteOrderGraph(graph);
}
}
This->nodes = new HashSetOrderNode();
This->edges = new HashSetOrderEdge();
This->order = order;
+ order->graph = This;
return This;
}
--- /dev/null
+#include "asttransform.h"
+#include "order.h"
+#include "tunable.h"
+#include "csolver.h"
+#include "ordergraph.h"
+#include "orderencoder.h"
+#include "orderdecompose.h"
+#include "integerencoding.h"
+
+void ASTTransform(CSolver *This){
+ uint size = This->allOrders.getSize();
+ for (uint i = 0; i < size; i++) {
+ Order *order = This->allOrders.get(i);
+ bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff);
+ if (!doDecompose)
+ continue;
+
+ OrderGraph *graph;
+ if(order->graph == NULL){
+ graph= buildOrderGraph(order);
+ if (order->type == PARTIAL) {
+ //Required to do SCC analysis for partial order graphs. It
+ //makes sure we don't incorrectly optimize graphs with negative
+ //polarity edges
+ completePartialOrderGraph(graph);
+ }
+ }else{
+ graph = order->graph;
+ }
+ //This is needed for splitorder
+ computeStronglyConnectedComponentGraph(graph);
+ decomposeOrder(This, order, graph);
+
+ bool doIntegerEncoding = GETVARTUNABLE(This->tuner, order->order.type, ORDERINTEGERENCODING, &onoff );
+ if(!doIntegerEncoding)
+ continue;
+ uint size = order->constraints.getSize();
+ for(uint i=0; i<size; i++){
+ orderIntegerEncodingSATEncoder(This->satEncoder, order->constraints.get(i));
+ }
+ }
+
+
+}
+
--- /dev/null
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/*
+ * File: asttransform.h
+ * Author: hamed
+ *
+ * Created on August 24, 2017, 5:48 PM
+ */
+
+#ifndef ASTTRANSFORM_H
+#define ASTTRANSFORM_H
+#include "classlist.h"
+
+void ASTTransform(CSolver *This);
+
+#endif /* ASTTRANSFORM_H */
+
--- /dev/null
+#include "integerencoding.h"
+#include "orderelement.h"
+#include "order.h"
+#include "satencoder.h"
+#include "csolver.h"
+#include "predicate.h"
+#include "element.h"
+
+void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
+ Order* order = boolOrder->order;
+ if (order->elementTable == NULL) {
+ order->initializeOrderElementsHashTable();
+ }
+ //getting two elements and using LT predicate ...
+ Element* elem1 = getOrderIntegerElement(This, order, boolOrder->first);
+ Element* elem2 = getOrderIntegerElement(This, order, boolOrder->second);
+ Set * sarray[]={order->auxSet, order->auxSet};
+ Predicate *predicate =new PredicateOperator(LT, sarray, 2);
+ Element * parray[]={elem1, elem2};
+ BooleanPredicate * boolean=new BooleanPredicate(predicate, parray, 2, NULL);
+ {//Adding new elements and boolean/predicate to solver regarding memory management
+ This->solver->allBooleans.push(boolean);
+ This->solver->allPredicates.push(predicate);
+ This->solver->allElements.push(elem1);
+ This->solver->allElements.push(elem2);
+ This->solver->constraints.add(boolean);
+ }
+}
+
+
+Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) {
+ HashSetOrderElement* eset = order->elementTable;
+ OrderElement oelement ={item, NULL};
+ if( !eset->contains(&oelement)){
+ Element* elem = new ElementSet(order->auxSet);
+ eset->add(allocOrderElement(item, elem));
+ return elem;
+ } else
+ return eset->get(&oelement)->elem;
+}
+
--- /dev/null
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/*
+ * File: integerencoding.h
+ * Author: hamed
+ *
+ * Created on August 24, 2017, 5:31 PM
+ */
+
+#ifndef INTEGERENCODING_H
+#define INTEGERENCODING_H
+#include "classlist.h"
+#include "structs.h"
+
+Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item);
+void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder);
+
+
+#endif /* INTEGERENCODING_H */
+
--- /dev/null
+#include "orderdecompose.h"
+#include "common.h"
+#include "order.h"
+#include "boolean.h"
+#include "ordergraph.h"
+#include "ordernode.h"
+#include "rewriter.h"
+#include "orderedge.h"
+#include "mutableset.h"
+#include "ops.h"
+#include "csolver.h"
+
+void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
+ Vector<Order *> ordervec;
+ Vector<Order *> partialcandidatevec;
+ uint size = order->constraints.getSize();
+ for (uint i = 0; i < size; i++) {
+ BooleanOrder *orderconstraint = order->constraints.get(i);
+ OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
+ OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
+ model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
+ if (from->sccNum != to->sccNum) {
+ OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
+ if (edge->polPos) {
+ replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
+ } else if (edge->polNeg) {
+ replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
+ } else {
+ //This case should only be possible if constraint isn't in AST
+ ASSERT(0);
+ }
+ } else {
+ //Build new order and change constraint's order
+ Order *neworder = NULL;
+ if (ordervec.getSize() > from->sccNum)
+ neworder = ordervec.get(from->sccNum);
+ if (neworder == NULL) {
+ MutableSet *set = new MutableSet(order->set->type);
+ neworder = new Order(order->type, set);
+ This->allOrders.push(neworder);
+ ordervec.setExpand(from->sccNum, neworder);
+ if (order->type == PARTIAL)
+ partialcandidatevec.setExpand(from->sccNum, neworder);
+ else
+ partialcandidatevec.setExpand(from->sccNum, NULL);
+ }
+ if (from->status != ADDEDTOSET) {
+ from->status = ADDEDTOSET;
+ ((MutableSet *)neworder->set)->addElementMSet(from->id);
+ }
+ if (to->status != ADDEDTOSET) {
+ to->status = ADDEDTOSET;
+ ((MutableSet *)neworder->set)->addElementMSet(to->id);
+ }
+ if (order->type == PARTIAL) {
+ OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
+ if (edge->polNeg)
+ partialcandidatevec.setExpand(from->sccNum, NULL);
+ }
+ orderconstraint->order = neworder;
+ neworder->addOrderConstraint(orderconstraint);
+ }
+ }
+
+ uint pcvsize=partialcandidatevec.getSize();
+ for(uint i=0;i<pcvsize;i++) {
+ Order * neworder=partialcandidatevec.get(i);
+ if (neworder != NULL){
+ neworder->type = TOTAL;
+ model_print("i=%u\t", i);
+ }
+ }
+}
+
--- /dev/null
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/*
+ * File: orderdecompose.h
+ * Author: hamed
+ *
+ * Created on August 24, 2017, 5:33 PM
+ */
+
+#ifndef ORDERDECOMPOSE_H
+#define ORDERDECOMPOSE_H
+#include "classlist.h"
+#include "structs.h"
+
+void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph);
+
+#endif /* ORDERDECOMPOSE_H */
+
model_print("Encoding All ...\n\n");
Edge c = encodeConstraintSATEncoder(This, constraint);
model_print("Returned Constraint in EncodingAll:\n");
- addConstraintCNF(This->cnf, c);
+ if( equalsEdge(c, E_BOGUS) )
+ addConstraintCNF(This->cnf, c);
}
delete iterator;
}
#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);
- case TOTAL:
- return encodeTotalOrderSATEncoder(This, 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);
+ switch (constraint->order->order.type){
+ case PAIRWISE:
+ switch ( constraint->order->type) {
+ case PARTIAL:
+ return encodePartialOrderSATEncoder(This, constraint);
+ case TOTAL:
+ return encodeTotalOrderSATEncoder(This, constraint);
+ default:
+ ASSERT(0);
+ }
+ case INTEGERENCODING:{
+ //Infer the value from graph ...
+ Order* order = constraint->order;
+ Edge gvalue = inferOrderConstraintFromGraph(order, constraint->first, constraint->second);
+ if(!edgeIsNull(gvalue))
+ return gvalue;
+ //If we couldn't infer the value from graph, we have already generated a predicate for that ...
+ // So, we should do nothing
+ return E_BOGUS;
}
+ default:
+ ASSERT(0);
}
- Order* order = boolOrder->order;
- Edge gvalue = inferOrderConstraintFromGraph(order, boolOrder->first, boolOrder->second);
- if(!edgeIsNull(gvalue))
- return gvalue;
-
- if (boolOrder->order->elementTable == NULL) {
- boolOrder->order->initializeOrderElementsHashTable();
- }
- //getting two elements and using LT predicate ...
- Element* elem1 = getOrderIntegerElement(This, order, boolOrder->first);
- ElementEncoding *encoding = getElementEncoding(elem1);
- if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
- encoding->setElementEncodingType(BINARYINDEX);
- encoding->encodingArrayInitialization();
- }
- Element* elem2 = getOrderIntegerElement(This, order, boolOrder->second);
- encoding = getElementEncoding(elem2);
- if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
- encoding->setElementEncodingType(BINARYINDEX);
- encoding->encodingArrayInitialization();
- }
- Set * sarray[]={order->set, order->set};
- Predicate *predicate =new PredicateOperator(LT, sarray, 2);
- Element * parray[]={elem1, elem2};
- BooleanPredicate * boolean=new BooleanPredicate(predicate, parray, 2, NULL);
- boolean->getFunctionEncoding()->setFunctionEncodingType(CIRCUIT);
- {//Adding new elements and boolean/predicate to solver regarding memory management
- This->solver->allBooleans.push(boolean);
- This->solver->allPredicates.push(predicate);
- This->solver->allElements.push(elem1);
- This->solver->allElements.push(elem2);
- }
- return encodeConstraintSATEncoder(This, boolean);
+ return E_BOGUS;
}
Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _second){
return E_NULL;
}
-Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) {
- HashSetOrderElement* eset = order->elementTable;
- OrderElement oelement ={item, NULL};
- if( !eset->contains(&oelement)){
- Element* elem = new ElementSet(order->set);
- ElementEncoding* encoding = getElementEncoding(elem);
- encoding->setElementEncodingType(BINARYINDEX);
- encoding->encodingArrayInitialization();
- encodeElementSATEncoder(This, elem);
- eset->add(allocOrderElement(item, elem));
- return elem;
- } else
- return eset->get(&oelement)->elem;
-}
-
Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
if(!edgeIsNull(gvalue))
#define SATORDERENCODER_H
Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
-Edge orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder);
Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _second);
-Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item);
Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair);
Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
/** @brief Adds a new key to the hashset. Returns false if the key
* is already present. */
- void addAll(HashSet<_Key, _KeyInt, _Shift, hash_function, equals> * table) {
+ void addAll(HashSet<_Key, _KeyInt, _Shift, hash_function, equals> * table) {
HSIterator<_Key, _KeyInt, _Shift, hash_function, equals> * it=iterator();
while(it->hasNext())
add(it->next());
delete it;
- }
+ }
/** @brief Adds a new key to the hashset. Returns false if the key
* is already present. */
static TunableDesc onoff={0, 1, 1};
static TunableDesc offon={0, 1, 0};
-enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE};
+enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING};
typedef enum Tunables Tunables;
#endif
#include "tunable.h"
#include "orderencoder.h"
#include "polarityassignment.h"
+#include "asttransform.h"
CSolver::CSolver() : unsat(false) {
tuner = allocTuner();
}
int CSolver::startEncoding() {
- naiveEncodingDecision(this);
computePolarities(this);
+ ASTTransform(this);
+ naiveEncodingDecision(this);
orderAnalysis(this);
encodeAllSATEncoder(this, satEncoder);
int result = solveCNF(satEncoder->cnf);
projects / satune.git / commitdiff