#include "ops.h"
class ASTNode {
- public:
- ASTNode(ASTNodeType _type) : type(_type) {}
+public:
+ ASTNode(ASTNodeType _type) : type(_type) {}
ASTNodeType type;
MEMALLOC;
};
#define GETBOOLEANVALUE(b) (b->boolVal)
class Boolean : public ASTNode {
- public:
+public:
Boolean(ASTNodeType _type);
virtual ~Boolean() {}
Polarity polarity;
};
class BooleanVar : public Boolean {
- public:
+public:
BooleanVar(VarType t);
VarType vtype;
Edge var;
};
class BooleanOrder : public Boolean {
- public:
+public:
BooleanOrder(Order *_order, uint64_t _first, uint64_t _second);
Order *order;
uint64_t first;
};
class BooleanPredicate : public Boolean {
- public:
+public:
BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, Boolean *_undefinedStatus);
~BooleanPredicate();
Predicate *predicate;
FunctionEncoding encoding;
Array<Element *> inputs;
Boolean *undefStatus;
- FunctionEncoding * getFunctionEncoding() {return &encoding;}
+ FunctionEncoding *getFunctionEncoding() {return &encoding;}
MEMALLOC;
};
class BooleanLogic : public Boolean {
- public:
+public:
BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint asize);
LogicOp op;
Array<Boolean *> inputs;
}
ElementConst::ElementConst(uint64_t _value, VarType _type) : Element(ELEMCONST), value(_value) {
- uint64_t array[]={value};
+ uint64_t array[] = {value};
set = new Set(_type, array, 1);
}
#define GETELEMENTTYPE(o) (o->type)
#define GETELEMENTPARENTS(o) (&((Element *)o)->parents)
class Element : public ASTNode {
- public:
+public:
Element(ASTNodeType type);
virtual ~Element();
Vector<ASTNode *> parents;
};
class ElementConst : public Element {
- public:
+public:
ElementConst(uint64_t value, VarType type);
~ElementConst();
Set *set;
};
class ElementSet : public Element {
- public:
+public:
ElementSet(Set *s);
Set *set;
MEMALLOC;
};
class ElementFunction : public Element {
- public:
+public:
ElementFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus);
~ElementFunction();
Function *function;
#define GETFUNCTIONTYPE(o) (((Function *)o)->type)
class Function {
- public:
- Function(FunctionType _type) : type(_type) {}
+public:
+ Function(FunctionType _type) : type(_type) {}
FunctionType type;
MEMALLOC;
virtual ~Function() {}
};
class FunctionOperator : public Function {
- public:
+public:
ArithOp op;
Array<Set *> domains;
Set *range;
};
class FunctionTable : public Function {
- public:
+public:
Table *table;
UndefinedBehavior undefBehavior;
FunctionTable (Table *table, UndefinedBehavior behavior);
#include "set.h"
class MutableSet : public Set {
- public:
+public:
MutableSet(VarType t);
void addElementMSet(uint64_t element);
MEMALLOC;
#include "orderpair.h"
class Order {
- public:
+public:
Order(OrderType type, Set *set);
~Order();
OrderType type;
Set *set;
HashTableOrderPair *orderPairTable;
- HashSetOrderElement* elementTable;
+ HashSetOrderElement *elementTable;
OrderGraph *graph;
Vector<BooleanOrder *> constraints;
OrderEncoding order;
#include "set.h"
#include "table.h"
-PredicateOperator::PredicateOperator(CompOp _op, Set **domain, uint numDomain) : Predicate(OPERATORPRED) , op(_op), domains(domain, numDomain) {
+PredicateOperator::PredicateOperator(CompOp _op, Set **domain, uint numDomain) : Predicate(OPERATORPRED), op(_op), domains(domain, numDomain) {
}
PredicateTable::PredicateTable(Table *_table, UndefinedBehavior _undefBehavior) : Predicate(TABLEPRED), table(_table), undefinedbehavior(_undefBehavior) {
#define GETPREDICATETYPE(o) (((Predicate *)(o))->type)
class Predicate {
- public:
- Predicate(PredicateType _type) : type(_type) {}
+public:
+ Predicate(PredicateType _type) : type(_type) {}
virtual ~Predicate() {}
PredicateType type;
MEMALLOC;
};
class PredicateOperator : public Predicate {
- public:
+public:
PredicateOperator(CompOp op, Set **domain, uint numDomain);
bool evalPredicateOperator(uint64_t *inputs);
CompOp op;
};
class PredicateTable : public Predicate {
- public:
+public:
PredicateTable(Table *table, UndefinedBehavior undefBehavior);
Table *table;
UndefinedBehavior undefinedbehavior;
setUnSAT();
constraints.remove(bexpr);
}
-
+
uint size = bexpr->parents.getSize();
for (uint i = 0; i < size; i++) {
Boolean *parent = bexpr->parents.get(i);
#include "mymemory.h"
class Set {
- public:
+public:
Set(VarType t);
Set(VarType t, uint64_t *elements, uint num);
Set(VarType t, uint64_t lowrange, uint64_t highrange);
bool exists(uint64_t element);
uint getSize();
uint64_t getElement(uint index);
-
+
VarType type;
bool isRange;
uint64_t low;//also used to count unique items
ASSERT(status);
}
-TableEntry * Table::getTableEntry(uint64_t *inputs, uint inputSize) {
+TableEntry *Table::getTableEntry(uint64_t *inputs, uint inputSize) {
TableEntry *temp = allocTableEntry(inputs, inputSize, -1);
TableEntry *result = entries->get(temp);
deleteTableEntry(temp);
#include "structs.h"
class Table {
- public:
+public:
Table(Set **domains, uint numDomain, Set *range);
void addNewTableEntry(uint64_t *inputs, uint inputSize, uint64_t result);
TableEntry *getTableEntry(uint64_t *inputs, uint inputSize);
#include "mymemory.h"
class OrderEdge {
- public:
+public:
OrderEdge(OrderNode *begin, OrderNode *end);
OrderNode *source;
if (!edge->mustPos)
continue;
} else
- if (!edge->polPos && !edge->pseudoPos)//Ignore edges that do not have positive polarity
- continue;
+ if (!edge->polPos && !edge->pseudoPos) //Ignore edges that do not have positive polarity
+ continue;
OrderNode *child = isReverse ? edge->source : edge->sink;
resetNodeInfoStatusSCC(graph);
}
-bool isMustBeTrueNode(OrderNode* node){
- HSIteratorOrderEdge* iterator = node->inEdges.iterator();
- while(iterator->hasNext()){
- OrderEdge* edge = iterator->next();
- if(!edge->mustPos)
+bool isMustBeTrueNode(OrderNode *node) {
+ HSIteratorOrderEdge *iterator = node->inEdges.iterator();
+ while (iterator->hasNext()) {
+ OrderEdge *edge = iterator->next();
+ if (!edge->mustPos)
return false;
}
delete iterator;
iterator = node->outEdges.iterator();
- while(iterator->hasNext()){
- OrderEdge* edge = iterator->next();
- if(!edge->mustPos)
+ while (iterator->hasNext()) {
+ OrderEdge *edge = iterator->next();
+ if (!edge->mustPos)
return false;
}
delete iterator;
return true;
}
-void bypassMustBeTrueNode(CSolver *This, OrderGraph* graph, OrderNode* node){
- HSIteratorOrderEdge* iterin = node->inEdges.iterator();
- while(iterin->hasNext()){
- OrderEdge* inEdge = iterin->next();
- OrderNode* srcNode = inEdge->source;
+void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node) {
+ HSIteratorOrderEdge *iterin = node->inEdges.iterator();
+ while (iterin->hasNext()) {
+ OrderEdge *inEdge = iterin->next();
+ OrderNode *srcNode = inEdge->source;
srcNode->outEdges.remove(inEdge);
- HSIteratorOrderEdge* iterout = node->outEdges.iterator();
- while(iterout->hasNext()){
- OrderEdge* outEdge = iterout->next();
- OrderNode* sinkNode = outEdge->sink;
+ HSIteratorOrderEdge *iterout = node->outEdges.iterator();
+ while (iterout->hasNext()) {
+ OrderEdge *outEdge = iterout->next();
+ OrderNode *sinkNode = outEdge->sink;
sinkNode->inEdges.remove(outEdge);
//Adding new edge to new sink and src nodes ...
OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
}
void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph) {
- HSIteratorOrderNode* iterator = graph->getNodes();
- while(iterator->hasNext()) {
- OrderNode* node = iterator->next();
- if(isMustBeTrueNode(node)){
+ HSIteratorOrderNode *iterator = graph->getNodes();
+ while (iterator->hasNext()) {
+ OrderNode *node = iterator->next();
+ if (isMustBeTrueNode(node)) {
bypassMustBeTrueNode(This, graph, node);
}
}
}
/** This function computes a source set for every nodes, the set of
- nodes that can reach that node via pospolarity edges. It then
- looks for negative polarity edges from nodes in the the source set
- to determine whether we need to generate pseudoPos edges. */
+ nodes that can reach that node via pospolarity edges. It then
+ looks for negative polarity edges from nodes in the the source set
+ to determine whether we need to generate pseudoPos edges. */
void completePartialOrderGraph(OrderGraph *graph) {
Vector<OrderNode *> finishNodes;
HashTableNodeToNodeSet *table = new HashTableNodeToNodeSet(128, 0.25);
Vector<OrderNode *> sccNodes;
-
+
uint size = finishNodes.getSize();
uint sccNum = 1;
for (int i = size - 1; i >= 0; i--) {
OrderNode *node = finishNodes.get(i);
HashSetOrderNode *sources = new HashSetOrderNode(4, 0.25);
table->put(node, sources);
-
+
if (node->status == NOTVISITED) {
//Need to do reverse traversal here...
node->status = VISITED;
}
delete iterator;
}
- for (uint j=0; j < rSize; j++) {
+ for (uint j = 0; j < rSize; j++) {
//Copy in set of entire SCC
OrderNode *rnode = sccNodes.get(j);
- HashSetOrderNode * set = (j==0) ? sources : sources->copy();
+ HashSetOrderNode *set = (j == 0) ? sources : sources->copy();
table->put(rnode, set);
//Use source sets to compute pseudoPos edges
}
delete iterator;
}
-
+
sccNodes.clear();
}
}
}
{
//Use source sets to compute mustPos edges
- HSIteratorOrderEdge *iterator =node->inEdges.iterator();
+ HSIteratorOrderEdge *iterator = node->inEdges.iterator();
while (iterator->hasNext()) {
OrderEdge *edge = iterator->next();
OrderNode *parent = edge->source;
must be true because of transitivity from other must be true
edges. */
-void reachMustAnalysis(CSolver * solver, OrderGraph *graph, bool computeTransitiveClosure) {
+void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure) {
Vector<OrderNode *> finishNodes;
//Topologically sort the mustPos edge graph
DFSMust(graph, &finishNodes);
void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
void completePartialOrderGraph(OrderGraph *graph);
void resetNodeInfoStatusSCC(OrderGraph *graph);
-bool isMustBeTrueNode(OrderNode* node);
-void bypassMustBeTrueNode(CSolver *This, OrderGraph* graph, OrderNode* node);
+bool isMustBeTrueNode(OrderNode *node);
+void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node);
void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph);
void completePartialOrderGraph(OrderGraph *graph);
void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
#include "mymemory.h"
class OrderGraph {
- public:
+public:
OrderGraph(Order *order);
~OrderGraph();
void addOrderConstraintToOrderGraph(BooleanOrder *bOrder);
void addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
OrderEdge *getInverseOrderEdge(OrderEdge *edge);
Order *getOrder() {return order;}
- HSIteratorOrderNode * getNodes() {return nodes->iterator();}
- HSIteratorOrderEdge * getEdges() {return edges->iterator();}
-
+ HSIteratorOrderNode *getNodes() {return nodes->iterator();}
+ HSIteratorOrderEdge *getEdges() {return edges->iterator();}
+
MEMALLOC;
- private:
+private:
HashSetOrderNode *nodes;
HashSetOrderEdge *edges;
Order *order;
typedef enum NodeStatus NodeStatus;
class OrderNode {
- public:
+public:
OrderNode(uint64_t id);
void addNewIncomingEdge(OrderEdge *edge);
void addNewOutgoingEdge(OrderEdge *edge);
#include "csolver.h"
void computePolarities(CSolver *This) {
- HSIteratorBoolean *iterator=This->getConstraints();
- while(iterator->hasNext()) {
+ HSIteratorBoolean *iterator = This->getConstraints();
+ while (iterator->hasNext()) {
Boolean *boolean = iterator->next();
updatePolarity(boolean, P_TRUE);
updateMustValue(boolean, BV_MUSTBETRUE);
#include "set.h"
-void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
- Order* order = boolOrder->order;
+void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) {
+ Order *order = boolOrder->order;
if (order->elementTable == NULL) {
order->initializeOrderElementsHashTable();
}
//getting two elements and using LT predicate ...
- ElementSet* elem1 = (ElementSet*)getOrderIntegerElement(This, order, boolOrder->first);
- ElementSet* elem2 = (ElementSet*)getOrderIntegerElement(This, order, boolOrder->second);
- Set * sarray[]={elem1->set, elem2->set};
- Predicate *predicate =This->solver->createPredicateOperator(LT, sarray, 2);
- Element * parray[]={elem1, elem2};
- Boolean * boolean=This->solver->applyPredicate(predicate, parray, 2);
+ ElementSet *elem1 = (ElementSet *)getOrderIntegerElement(This, order, boolOrder->first);
+ ElementSet *elem2 = (ElementSet *)getOrderIntegerElement(This, order, boolOrder->second);
+ Set *sarray[] = {elem1->set, elem2->set};
+ Predicate *predicate = This->solver->createPredicateOperator(LT, sarray, 2);
+ Element *parray[] = {elem1, elem2};
+ Boolean *boolean = This->solver->applyPredicate(predicate, parray, 2);
This->solver->addConstraint(boolean);
This->solver->replaceBooleanWithBoolean(boolOrder, boolean);
}
-Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) {
- HashSetOrderElement* eset = order->elementTable;
+Element *getOrderIntegerElement(SATEncoder *This,Order *order, uint64_t item) {
+ HashSetOrderElement *eset = order->elementTable;
OrderElement oelement(item, NULL);
- if( !eset->contains(&oelement)){
- Set* set = This->solver->createRangeSet(order->set->type, 1, (uint64_t) order->set->getSize());
- Element* elem = This->solver->getElementVar(set);
+ if ( !eset->contains(&oelement)) {
+ Set *set = This->solver->createRangeSet(order->set->type, 1, (uint64_t) order->set->getSize());
+ Element *elem = This->solver->getElementVar(set);
eset->add(new OrderElement(item, elem));
return elem;
} else
* and open the template in the editor.
*/
-/*
+/*
* File: integerencoding.h
* Author: hamed
*
#include "classlist.h"
#include "structs.h"
-Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item);
+Element *getOrderIntegerElement(SATEncoder *This,Order *order, uint64_t item);
void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder);
-#endif /* INTEGERENCODING_H */
+#endif/* INTEGERENCODING_H */
#include "integerencoding.h"
void orderAnalysis(CSolver *This) {
- Vector<Order *> * orders=This->getOrders();
+ Vector<Order *> *orders = This->getOrders();
uint size = orders->getSize();
for (uint i = 0; i < size; i++) {
Order *order = orders->get(i);
- bool doDecompose=GETVARTUNABLE(This->getTuner(), order->type, DECOMPOSEORDER, &onoff);
+ bool doDecompose = GETVARTUNABLE(This->getTuner(), 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
}
- bool mustReachGlobal=GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
+ bool mustReachGlobal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
if (mustReachGlobal)
reachMustAnalysis(This, graph, false);
- bool mustReachLocal=GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
-
+ bool mustReachLocal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
+
if (mustReachLocal) {
//This pair of analysis is also optional
if (order->type == PARTIAL) {
}
}
- bool mustReachPrune=GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
-
+ bool mustReachPrune = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
+
if (mustReachPrune)
removeMustBeTrueNodes(This, graph);
-
+
//This is needed for splitorder
computeStronglyConnectedComponentGraph(graph);
decomposeOrder(This, order, graph);
delete graph;
-
+
/*
- OrderIntegerEncodingSATEncoder wants a private field that it really shoukldn't need...
+ OrderIntegerEncodingSATEncoder wants a private field that it really shoukldn't need...
- bool doIntegerEncoding = GETVARTUNABLE(This->getTuner(), order->order.type, ORDERINTEGERENCODING, &offon );
- if(!doIntegerEncoding)
- continue;
- uint size = order->constraints.getSize();
- for(uint i=0; i<size; i++){
- orderIntegerEncodingSATEncoder(This->satEncoder, order->constraints.get(i));
- }*/
+ bool doIntegerEncoding = GETVARTUNABLE(This->getTuner(), order->order.type, ORDERINTEGERENCODING, &offon );
+ if(!doIntegerEncoding)
+ continue;
+ uint size = order->constraints.getSize();
+ for(uint i=0; i<size; i++){
+ orderIntegerEncodingSATEncoder(This->satEncoder, order->constraints.get(i));
+ }*/
}
}
OrderNode *to = graph->getOrderNodeFromOrderGraph(orderconstraint->second);
model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
if (from->sccNum != to->sccNum) {
- OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
+ OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
if (edge->polPos) {
This->replaceBooleanWithTrue(orderconstraint);
} else if (edge->polNeg) {
}
}
- uint pcvsize=partialcandidatevec.getSize();
- for(uint i=0;i<pcvsize;i++) {
- Order * neworder=partialcandidatevec.get(i);
- if (neworder != NULL){
+ 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);
}
* and open the template in the editor.
*/
-/*
+/*
* File: orderdecompose.h
* Author: hamed
*
void orderAnalysis(CSolver *This);
void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph);
-#endif /* ORDERDECOMPOSE_H */
+#endif/* ORDERDECOMPOSE_H */
return constraintAND(cnf, numvars, array);
}
-Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2){
- if(numvars == 0 )
+Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
+ if (numvars == 0 )
return E_False;
- Edge result =constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
+ Edge result = constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
for (uint i = 1; i < numvars; i++) {
Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
- Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
- result = constraintOR2(cnf, lt, eq);
+ Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
+ result = constraintOR2(cnf, lt, eq);
}
return result;
}
-Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2){
- if(numvars == 0 )
+Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
+ if (numvars == 0 )
return E_True;
- Edge result =constraintIMPLIES(cnf, var1[0], var2[0]);
+ Edge result = constraintIMPLIES(cnf, var1[0], var2[0]);
for (uint i = 1; i < numvars; i++) {
Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
- Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
- result = constraintOR2(cnf, lt, eq);
+ Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
+ result = constraintOR2(cnf, lt, eq);
}
return result;
}
#include "orderelement.h"
-OrderElement::OrderElement(uint64_t _item, Element* _elem) {
+OrderElement::OrderElement(uint64_t _item, Element *_elem) {
elem = _elem;
item = _item;
}
#include "constraint.h"
class OrderElement {
- public:
- OrderElement(uint64_t item, Element* elem);
+public:
+ OrderElement(uint64_t item, Element *elem);
uint64_t item;
- Element* elem;
+ Element *elem;
MEMALLOC;
};
#include "constraint.h"
class OrderPair {
- public:
+public:
OrderPair(uint64_t first, uint64_t second, Edge constraint);
OrderPair();
- uint64_t first;
+ uint64_t first;
uint64_t second;
Edge constraint;
MEMALLOC;
}
void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This) {
- HSIteratorBoolean *iterator=csolver->getConstraints();
- while(iterator->hasNext()) {
+ HSIteratorBoolean *iterator = csolver->getConstraints();
+ while (iterator->hasNext()) {
Boolean *constraint = iterator->next();
model_print("Encoding All ...\n\n");
Edge c = encodeConstraintSATEncoder(This, constraint);
model_print("Returned Constraint in EncodingAll:\n");
- ASSERT( ! equalsEdge(c, E_BOGUS));
+ ASSERT( !equalsEdge(c, E_BOGUS));
addConstraintCNF(This->cnf, c);
}
delete iterator;
bool notfinished = true;
while (notfinished) {
Edge carray[numDomains];
-
+
if (predicate->evalPredicateOperator(vals) != generateNegation) {
//Include this in the set of terms
for (uint i = 0; i < numDomains; i++) {
ASSERT(ee0->numVars == ee1->numVars);
uint numVars = ee0->numVars;
switch (predicate->op) {
- case EQUALS:
- return generateEquivNVConstraint(This->cnf, numVars, ee0->variables, ee1->variables);
- case LT:
- return generateLTConstraint(This->cnf, numVars, ee0->variables, ee1->variables);
- case GT:
- return generateLTConstraint(This->cnf, numVars, ee1->variables, ee0->variables);
- default:
- ASSERT(0);
+ case EQUALS:
+ return generateEquivNVConstraint(This->cnf, numVars, ee0->variables, ee1->variables);
+ case LT:
+ return generateLTConstraint(This->cnf, numVars, ee0->variables, ee1->variables);
+ case GT:
+ return generateLTConstraint(This->cnf, numVars, ee1->variables, ee0->variables);
+ default:
+ ASSERT(0);
}
exit(-1);
}
ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
Table *table = ((PredicateTable *)constraint->predicate)->table;
FunctionEncodingType encType = constraint->encoding.type;
- Array<Element*> * inputs = &constraint->inputs;
+ Array<Element *> *inputs = &constraint->inputs;
uint inputNum = inputs->getSize();
uint size = table->entries->getSize();
bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
switch ( constraint->order->type) {
- case PARTIAL:
- return encodePartialOrderSATEncoder(This, constraint);
- case TOTAL:
- return encodeTotalOrderSATEncoder(This, constraint);
- default:
- ASSERT(0);
+ case PARTIAL:
+ return encodePartialOrderSATEncoder(This, constraint);
+ case TOTAL:
+ return encodeTotalOrderSATEncoder(This, constraint);
+ default:
+ ASSERT(0);
}
return E_BOGUS;
}
-Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _second){
+Edge inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second) {
if (order->graph != NULL) {
- OrderGraph *graph=order->graph;
- OrderNode *first=graph->lookupOrderNodeFromOrderGraph(_first);
- OrderNode *second=graph->lookupOrderNodeFromOrderGraph(_second);
+ OrderGraph *graph = order->graph;
+ OrderNode *first = graph->lookupOrderNodeFromOrderGraph(_first);
+ OrderNode *second = graph->lookupOrderNodeFromOrderGraph(_second);
if ((first != NULL) && (second != NULL)) {
- OrderEdge *edge=graph->lookupOrderEdgeFromOrderGraph(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=graph->lookupOrderEdgeFromOrderGraph(second, first);
+ OrderEdge *invedge = graph->lookupOrderEdgeFromOrderGraph(second, first);
if (invedge != NULL) {
if (invedge->mustPos)
return E_False;
Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
- if(!edgeIsNull(gvalue))
+ if (!edgeIsNull(gvalue))
return gvalue;
-
+
HashTableOrderPair *table = order->orderPairTable;
bool negate = false;
OrderPair flipped;
table->put(paircopy, paircopy);
} else
constraint = table->get(pair)->constraint;
-
+
return negate ? constraintNegate(constraint) : constraint;
}
ASSERT(boolOrder->order->type == TOTAL);
if (boolOrder->order->orderPairTable == NULL) {
boolOrder->order->initializeOrderHashTable();
- bool doOptOrderStructure=GETVARTUNABLE(This->solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
+ bool doOptOrderStructure = GETVARTUNABLE(This->solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
if (doOptOrderStructure) {
boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
reachMustAnalysis(This->solver, boolOrder->order->graph, true);
#define SATORDERENCODER_H
Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
-Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _second);
+Edge inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second);
Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair);
Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean);
HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order, uint64_t first, uint64_t second);
/**
- * most significant bit is represented by variable index 0
+ * most significant bit is represented by variable index 0
*/
uint64_t getElementValueBinaryIndexSATTranslator(CSolver *This, ElementEncoding *elemEnc);
uint64_t getElementValueBinaryValueSATTranslator(CSolver *This, ElementEncoding *elemEnc);
template<typename type>
class Array {
- public:
- Array(uint _size) :
- array((type *)ourcalloc(1, sizeof(type) * _size)),
+public:
+ Array(uint _size) :
+ array((type *)ourcalloc(1, sizeof(type) * _size)),
size(_size)
- {
- }
-
- Array(type * _array, uint _size) :
- array((type *)ourcalloc(1, sizeof(type) * _size)),
+ {
+ }
+
+ Array(type *_array, uint _size) :
+ array((type *)ourcalloc(1, sizeof(type) * _size)),
size(_size) {
- memcpy(array, _array, _size * sizeof(type));
- }
-
- ~Array() {
- ourfree(array);
- }
-
- void remove(uint index) {
- size--;
- for (; index < size; index++) {
- array[index] = array[index + 1];
- }
- }
-
- type get(uint index) {
- return array[index];
- }
-
- void set(uint index, type item) {
- array[index] = item;
- }
-
- uint getSize() {
- return size;
- }
-
- type *expose() {
- return array;
- }
-
- private:
- type *array;
- uint size;
+ memcpy(array, _array, _size * sizeof(type));
+ }
+
+ ~Array() {
+ ourfree(array);
+ }
+
+ void remove(uint index) {
+ size--;
+ for (; index < size; index++) {
+ array[index] = array[index + 1];
+ }
+ }
+
+ type get(uint index) {
+ return array[index];
+ }
+
+ void set(uint index, type item) {
+ array[index] = item;
+ }
+
+ uint getSize() {
+ return size;
+ }
+
+ type *expose() {
+ return array;
+ }
+
+private:
+ type *array;
+ uint size;
};
template<typename type>
class Vector {
- public:
- Vector(uint _capacity = VECTOR_DEFCAP) :
- size(0),
+public:
+ Vector(uint _capacity = VECTOR_DEFCAP) :
+ size(0),
capacity(_capacity),
array((type *) ourmalloc(sizeof(type) * _capacity)) {
- }
+ }
- Vector(uint _capacity, type * _array) :
- size(_capacity),
+ Vector(uint _capacity, type *_array) :
+ size(_capacity),
capacity(_capacity),
array((type *) ourmalloc(sizeof(type) * _capacity)) {
- memcpy(array, _array, capacity * sizeof(type));
+ memcpy(array, _array, capacity * sizeof(type));
}
-
+
void pop() {
size--;
- }
+ }
type last() {
- return array[size - 1];
+ return array[size - 1];
}
-
- void setSize(uint _size) {
- if (_size <= size) {
- size = _size;
- return;
- } else if (_size > capacity) {
- array = (type *)ourrealloc(array, _size * sizeof(type));
- capacity = _size;
- }
- bzero(&array[size], (_size - size) * sizeof(type));
+
+ void setSize(uint _size) {
+ if (_size <= size) {
+ size = _size;
+ return;
+ } else if (_size > capacity) {
+ array = (type *)ourrealloc(array, _size * sizeof(type));
+ capacity = _size;
+ }
+ bzero(&array[size], (_size - size) * sizeof(type));
size = _size;
- }
+ }
- void push(type item) {
- if (size >= capacity) {
- uint newcap = capacity << 1;
- array = (type *)ourrealloc(array, newcap * sizeof(type));
- capacity = newcap;
- }
- array[size++] = item;
+ void push(type item) {
+ if (size >= capacity) {
+ uint newcap = capacity << 1;
+ array = (type *)ourrealloc(array, newcap * sizeof(type));
+ capacity = newcap;
+ }
+ array[size++] = item;
}
-
- type get(uint index) {
- return array[index];
+
+ type get(uint index) {
+ return array[index];
}
-
- void setExpand(uint index, type item) {
- if (index >= size)
- setSize(index + 1);
- set(index, item);
+
+ void setExpand(uint index, type item) {
+ if (index >= size)
+ setSize(index + 1);
+ set(index, item);
}
-
- void set(uint index, type item) {
- array[index] = item;
+
+ void set(uint index, type item) {
+ array[index] = item;
}
-
+
uint getSize() {
- return size;
+ return size;
}
-
+
~Vector() {
- ourfree(array);
+ ourfree(array);
}
-
+
void clear() {
- size = 0;
+ size = 0;
}
-
+
type *expose() {
- return array;
- }
-
- private:
+ return array;
+ }
+
+private:
uint size;
uint capacity;
type *array;
template<typename _Key, typename _KeyInt, int _Shift, unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = default_equals<_Key> >
class HSIterator {
public:
- HSIterator(LinkNode<_Key> *_curr, HashSet <_Key, _KeyInt, _Shift, hash_function, equals> * _set) :
+ HSIterator(LinkNode<_Key> *_curr, HashSet <_Key, _KeyInt, _Shift, hash_function, equals> *_set) :
curr(_curr),
set(_set)
{
}
/** Override: new operator */
- void * operator new(size_t size) {
+ void *operator new(size_t size) {
return ourmalloc(size);
}
}
/** Override: new[] operator */
- void * operator new[](size_t size) {
+ void *operator new[](size_t size) {
return ourmalloc(size);
}
}
bool hasNext() {
- return curr!=NULL;
+ return curr != NULL;
}
_Key next() {
- _Key k=curr->key;
- last=curr;
- curr=curr->next;
+ _Key k = curr->key;
+ last = curr;
+ curr = curr->next;
return k;
}
}
void remove() {
- _Key k=last->key;
+ _Key k = last->key;
set->remove(k);
}
private:
LinkNode<_Key> *curr;
LinkNode<_Key> *last;
- HashSet <_Key, _KeyInt, _Shift, hash_function, equals> * set;
+ HashSet <_Key, _KeyInt, _Shift, hash_function, equals> *set;
};
template<typename _Key, typename _KeyInt, int _Shift = 0, unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = default_equals<_Key> >
/** @brief Hashset destructor */
~HashSet() {
- LinkNode<_Key> *tmp=list;
- while(tmp!=NULL) {
- LinkNode<_Key> *tmpnext=tmp->next;
+ LinkNode<_Key> *tmp = list;
+ while (tmp != NULL) {
+ LinkNode<_Key> *tmpnext = tmp->next;
ourfree(tmp);
- tmp=tmpnext;
+ tmp = tmpnext;
}
delete table;
}
- HashSet<_Key, _KeyInt, _Shift, hash_function, equals> * copy() {
- HashSet<_Key, _KeyInt, _Shift, hash_function, equals> *copy=new HashSet<_Key, _KeyInt, _Shift, hash_function, equals>(table->getCapacity(), table->getLoadFactor());
- HSIterator<_Key, _KeyInt, _Shift, hash_function, equals> * it=iterator();
- while(it->hasNext())
+ HashSet<_Key, _KeyInt, _Shift, hash_function, equals> *copy() {
+ HashSet<_Key, _KeyInt, _Shift, hash_function, equals> *copy = new HashSet<_Key, _KeyInt, _Shift, hash_function, equals>(table->getCapacity(), table->getLoadFactor());
+ HSIterator<_Key, _KeyInt, _Shift, hash_function, equals> *it = iterator();
+ while (it->hasNext())
copy->add(it->next());
delete it;
return copy;
}
void reset() {
- LinkNode<_Key> *tmp=list;
- while(tmp!=NULL) {
- LinkNode<_Key> *tmpnext=tmp->next;
+ LinkNode<_Key> *tmp = list;
+ while (tmp != NULL) {
+ LinkNode<_Key> *tmpnext = tmp->next;
ourfree(tmp);
- tmp=tmpnext;
+ tmp = tmpnext;
}
- list=tail=NULL;
+ list = tail = NULL;
table->reset();
}
/** @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) {
- HSIterator<_Key, _KeyInt, _Shift, hash_function, equals> * it=iterator();
- while(it->hasNext())
+ 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;
}
* is already present. */
bool add(_Key key) {
- LinkNode<_Key> * val=table->get(key);
- if (val==NULL) {
- LinkNode<_Key> * newnode=(LinkNode<_Key> *)ourmalloc(sizeof(struct LinkNode<_Key>));
- newnode->prev=tail;
- newnode->next=NULL;
- newnode->key=key;
- if (tail!=NULL)
- tail->next=newnode;
+ LinkNode<_Key> *val = table->get(key);
+ if (val == NULL) {
+ LinkNode<_Key> *newnode = (LinkNode<_Key> *)ourmalloc(sizeof(struct LinkNode<_Key>));
+ newnode->prev = tail;
+ newnode->next = NULL;
+ newnode->key = key;
+ if (tail != NULL)
+ tail->next = newnode;
else
- list=newnode;
- tail=newnode;
+ list = newnode;
+ tail = newnode;
table->put(key, newnode);
return true;
} else
* hashset. Returns NULL if not present. */
_Key get(_Key key) {
- LinkNode<_Key> * val=table->get(key);
- if (val!=NULL)
+ LinkNode<_Key> *val = table->get(key);
+ if (val != NULL)
return val->key;
else
return NULL;
}
bool contains(_Key key) {
- return table->get(key)!=NULL;
+ return table->get(key) != NULL;
}
bool remove(_Key key) {
- LinkNode<_Key> * oldlinknode;
- oldlinknode=table->get(key);
- if (oldlinknode==NULL) {
+ LinkNode<_Key> *oldlinknode;
+ oldlinknode = table->get(key);
+ if (oldlinknode == NULL) {
return false;
}
table->remove(key);
//remove link node from the list
- if (oldlinknode->prev==NULL)
- list=oldlinknode->next;
+ if (oldlinknode->prev == NULL)
+ list = oldlinknode->next;
else
- oldlinknode->prev->next=oldlinknode->next;
- if (oldlinknode->next!=NULL)
- oldlinknode->next->prev=oldlinknode->prev;
+ oldlinknode->prev->next = oldlinknode->next;
+ if (oldlinknode->next != NULL)
+ oldlinknode->next->prev = oldlinknode->prev;
else
- tail=oldlinknode->prev;
+ tail = oldlinknode->prev;
ourfree(oldlinknode);
return true;
}
}
bool isEmpty() {
- return getSize()==0;
+ return getSize() == 0;
}
- HSIterator<_Key, _KeyInt, _Shift, hash_function, equals> * iterator() {
+ HSIterator<_Key, _KeyInt, _Shift, hash_function, equals> *iterator() {
return new HSIterator<_Key, _KeyInt, _Shift, hash_function, equals>(list, this);
}
/** Override: new operator */
- void * operator new(size_t size) {
+ void *operator new(size_t size) {
return ourmalloc(size);
}
}
/** Override: new[] operator */
- void * operator new[](size_t size) {
+ void *operator new[](size_t size) {
return ourmalloc(size);
}
ourfree(p);
}
private:
- HashTable<_Key, LinkNode<_Key>*, _KeyInt, _Shift, hash_function, equals> * table;
+ HashTable<_Key, LinkNode<_Key> *, _KeyInt, _Shift, hash_function, equals> *table;
LinkNode<_Key> *list;
LinkNode<_Key> *tail;
};
}
/** Override: new operator */
- void * operator new(size_t size) {
+ void *operator new(size_t size) {
return ourmalloc(size);
}
}
/** Override: new[] operator */
- void * operator new[](size_t size) {
+ void *operator new[](size_t size) {
return ourmalloc(size);
}
}
void resetanddelete() {
- for(unsigned int i=0;i<capacity;i++) {
+ for (unsigned int i = 0; i < capacity; i++) {
struct hashlistnode<_Key, _Val> *bin = &table[i];
if (bin->key != NULL) {
bin->key = NULL;
}
void resetandfree() {
- for(unsigned int i=0;i<capacity;i++) {
+ for (unsigned int i = 0; i < capacity; i++) {
struct hashlistnode<_Key, _Val> *bin = &table[i];
if (bin->key != NULL) {
bin->key = NULL;
/* HashTable cannot handle 0 as a key */
if (!key) {
if (!zero) {
- zero=(struct hashlistnode<_Key, _Val> *)ourmalloc(sizeof(struct hashlistnode<_Key, _Val>));
+ zero = (struct hashlistnode<_Key, _Val> *)ourmalloc(sizeof(struct hashlistnode<_Key, _Val>));
size++;
}
- zero->key=key;
- zero->val=val;
+ zero->key = key;
+ zero->val = val;
return;
}
}
unsigned int oindex = hash_function(key) & capacitymask;
- unsigned int index=oindex;
+ unsigned int index = oindex;
do {
search = &table[index];
if (!search->key) {
return search->val;
index++;
index &= capacitymask;
- if (index==oindex)
+ if (index == oindex)
break;
} while (true);
return (_Val)0;
if (!zero) {
return (_Val)0;
} else {
- _Val v=zero->val;
+ _Val v = zero->val;
ourfree(zero);
- zero=NULL;
+ zero = NULL;
size--;
return v;
}
break;
} else
if (equals(search->key, key)) {
- _Val v=search->val;
+ _Val v = search->val;
//empty out this bin
- search->val=(_Val) 1;
- search->key=0;
+ search->val = (_Val) 1;
+ search->key = 0;
size--;
return v;
}
/* HashTable cannot handle 0 as a key */
if (!key) {
- return zero!=NULL;
+ return zero != NULL;
}
unsigned int index = hash_function(key);
struct hashlistnode<_Key, _Val> *bin = &oldtable[0];
struct hashlistnode<_Key, _Val> *lastbin = &oldtable[oldcapacity];
- for (;bin < lastbin;bin++) {
+ for (; bin < lastbin; bin++) {
_Key key = bin->key;
struct hashlistnode<_Key, _Val> *search;
return key1->sink == key2->sink && key1->source == key2->source;
}
-unsigned int order_element_hash_function(OrderElement* This) {
+unsigned int order_element_hash_function(OrderElement *This) {
return (uint)This->item;
}
-bool order_element_equals(OrderElement* key1, OrderElement* key2) {
+bool order_element_equals(OrderElement *key1, OrderElement *key2) {
return key1->item == key2->item;
}
bool order_node_equals(OrderNode *key1, OrderNode *key2);
unsigned int order_edge_hash_function(OrderEdge *This);
bool order_edge_equals(OrderEdge *key1, OrderEdge *key2);
-unsigned int order_element_hash_function(OrderElement* This);
-bool order_element_equals(OrderElement* key1, OrderElement* key2);
+unsigned int order_element_hash_function(OrderElement *This);
+bool order_element_equals(OrderElement *key1, OrderElement *key2);
unsigned int order_pair_hash_function(OrderPair *This);
bool order_pair_equals(OrderPair *key1, OrderPair *key2);
typedef enum ElementEncodingType ElementEncodingType;
class ElementEncoding {
- public:
+public:
ElementEncoding(Element *element);
ElementEncodingType getElementEncodingType() {return type;}
~ElementEncoding();
return -1;
}
-
+
ElementEncodingType type;
Element *element;
Edge *variables;/* List Variables Used To Encode Element */
typedef union ElementPredicate ElementPredicate;
class FunctionEncoding {
- public:
+public:
FunctionEncodingType type;
bool isFunction;//true for function, false for predicate
ElementPredicate op;
#include <strings.h>
void naiveEncodingDecision(CSolver *This) {
- HSIteratorBoolean *iterator=This->getConstraints();
- while(iterator->hasNext()) {
+ HSIteratorBoolean *iterator = This->getConstraints();
+ while (iterator->hasNext()) {
Boolean *boolean = iterator->next();
naiveEncodingConstraint(boolean);
}
typedef enum OrderEncodingType OrderEncodingType;
class OrderEncoding {
- public:
+public:
OrderEncoding(Order *order);
OrderEncodingType type;
Boolean *b3 = solver->getBooleanVar(0);
Boolean *b4 = solver->getBooleanVar(0);
//L_AND, L_OR, L_NOT, L_XOR, L_IMPLIES
- Boolean * barray1[]={b1,b2};
+ Boolean *barray1[] = {b1,b2};
Boolean *andb1b2 = solver->applyLogicalOperation(L_AND, barray1, 2);
- Boolean * barray2[]={andb1b2, b3};
+ Boolean *barray2[] = {andb1b2, b3};
Boolean *imply = solver->applyLogicalOperation(L_IMPLIES, barray2, 2);
solver->addConstraint(imply);
- Boolean * barray3[] ={b3};
+ Boolean *barray3[] = {b3};
Boolean *notb3 = solver->applyLogicalOperation(L_NOT, barray3, 1);
- Boolean * barray4[] ={notb3, b4};
+ Boolean *barray4[] = {notb3, b4};
solver->addConstraint(solver->applyLogicalOperation(L_OR, barray4, 2));
- Boolean * barray5[] ={b1, b4};
+ Boolean *barray5[] = {b1, b4};
solver->addConstraint(solver->applyLogicalOperation(L_XOR, barray5, 2));
if (solver->startEncoding() == 1)
printf("b1=%d b2=%d b3=%d b4=%d\n",
Boolean *o81 = solver->orderConstraint(order, 8, 1);
/* Not Valid c++...Let Hamed fix...
- addConstraint(solver, applyLogicalOperation(solver, L_OR,(Boolean *[]) {o12, o13, o24, o34}, 4) );
- Boolean *b1 = applyLogicalOperation(solver, L_XOR, (Boolean *[]) {o41, o57}, 2);
- Boolean *o34n = applyLogicalOperation(solver, L_NOT, (Boolean *[]) {o34}, 1);
- Boolean *o24n = applyLogicalOperation(solver, L_NOT, (Boolean *[]) {o24}, 1);
- Boolean *b2 = applyLogicalOperation(solver, L_OR, (Boolean *[]) {o34n, o24n}, 2);
- addConstraint(solver, applyLogicalOperation(solver, L_IMPLIES,(Boolean *[]) {b1, b2}, 2) );
- addConstraint(solver, applyLogicalOperation(solver, L_AND,(Boolean *[]) {o12, o13}, 2) );
- addConstraint(solver, applyLogicalOperation(solver, L_OR,(Boolean *[]) {o76, o65}, 2) );
- Boolean* b3= applyLogicalOperation(solver, L_AND,(Boolean *[]) {o76, o65}, 2) ;
- Boolean* o57n= applyLogicalOperation(solver, L_NOT,(Boolean *[]) {o57}, 1);
- addConstraint(solver, applyLogicalOperation(solver, L_IMPLIES,(Boolean *[]) {b3, o57n}, 2) );
- addConstraint(solver, applyLogicalOperation(solver, L_AND,(Boolean *[]) {o58, o81}, 2) );
-
- if (solver->startEncoding() == 1)
- printf("SAT\n");
- else
- printf("UNSAT\n");
- */
+ addConstraint(solver, applyLogicalOperation(solver, L_OR,(Boolean *[]) {o12, o13, o24, o34}, 4) );
+ Boolean *b1 = applyLogicalOperation(solver, L_XOR, (Boolean *[]) {o41, o57}, 2);
+ Boolean *o34n = applyLogicalOperation(solver, L_NOT, (Boolean *[]) {o34}, 1);
+ Boolean *o24n = applyLogicalOperation(solver, L_NOT, (Boolean *[]) {o24}, 1);
+ Boolean *b2 = applyLogicalOperation(solver, L_OR, (Boolean *[]) {o34n, o24n}, 2);
+ addConstraint(solver, applyLogicalOperation(solver, L_IMPLIES,(Boolean *[]) {b1, b2}, 2) );
+ addConstraint(solver, applyLogicalOperation(solver, L_AND,(Boolean *[]) {o12, o13}, 2) );
+ addConstraint(solver, applyLogicalOperation(solver, L_OR,(Boolean *[]) {o76, o65}, 2) );
+ Boolean* b3= applyLogicalOperation(solver, L_AND,(Boolean *[]) {o76, o65}, 2) ;
+ Boolean* o57n= applyLogicalOperation(solver, L_NOT,(Boolean *[]) {o57}, 1);
+ addConstraint(solver, applyLogicalOperation(solver, L_IMPLIES,(Boolean *[]) {b3, o57n}, 2) );
+ addConstraint(solver, applyLogicalOperation(solver, L_AND,(Boolean *[]) {o58, o81}, 2) );
+
+ if (solver->startEncoding() == 1)
+ printf("SAT\n");
+ else
+ printf("UNSAT\n");
+ */
delete solver;
}
solver->addTableEntry(t1, row5, 2, 3);
solver->addTableEntry(t1, row6, 2, 5);
Function *f1 = solver->completeTable(t1, FLAGIFFUNDEFINED);
- Element * tmparray[]={e1, e2};
+ Element *tmparray[] = {e1, e2};
Element *e3 = solver->applyFunction(f1, tmparray, 2, overflow);
Set *deq[] = {s3,s2};
solver->addTableEntry(t1, row6, 3, true);
Predicate *p1 = solver->createPredicateTable(t1, FLAGIFFUNDEFINED);
Boolean *undef = solver->getBooleanVar(2);
- Element * tmparray[] = {e1, e2, e3};
+ Element *tmparray[] = {e1, e2, e3};
Boolean *b1 = solver->applyPredicateTable(p1, tmparray, 3, undef);
solver->addConstraint(b1);
Set *d1[] = {s1, s2};
Predicate *eq = solver->createPredicateOperator(EQUALS, d1, 2);
- Element * tmparray2[] = {e1, e2};
+ Element *tmparray2[] = {e1, e2};
Boolean *pred2 = solver->applyPredicate(eq, tmparray2, 2);
solver->addConstraint(pred2);
Tuner::Tuner() {
}
-int Tuner::getTunable(TunableParam param, TunableDesc * descriptor) {
+int Tuner::getTunable(TunableParam param, TunableDesc *descriptor) {
return descriptor->defaultValue;
}
-int Tuner::getVarTunable(VarType vartype, TunableParam param, TunableDesc * descriptor) {
+int Tuner::getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor) {
return descriptor->defaultValue;
}
class Tuner {
- public:
+public:
Tuner();
- int getTunable(TunableParam param, TunableDesc * descriptor);
- int getVarTunable(VarType vartype, TunableParam param, TunableDesc * descriptor);
+ int getTunable(TunableParam param, TunableDesc *descriptor);
+ int getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor);
MEMALLOC;
};
class TunableDesc {
- public:
- TunableDesc(int _lowValue, int _highValue, int _defaultValue) : lowValue(_lowValue), highValue(_highValue), defaultValue(_defaultValue) {}
+public:
+ TunableDesc(int _lowValue, int _highValue, int _defaultValue) : lowValue(_lowValue), highValue(_highValue), defaultValue(_defaultValue) {}
int lowValue;
int highValue;
int defaultValue;
}
Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) {
- Boolean * boolean=new BooleanLogic(this, op, array, asize);
+ Boolean *boolean = new BooleanLogic(this, op, array, asize);
allBooleans.push(boolean);
return boolean;
}
#include "structs.h"
class CSolver {
- public:
+public:
CSolver();
~CSolver();
-
+
/** This function creates a set containing the elements passed in the array. */
Set *createSet(VarType type, uint64_t *elements, uint num);
/** This function creates a set from lowrange to highrange (inclusive). */
Set *createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange);
-
+
/** This function creates a mutable set. */
-
+
MutableSet *createMutableSet(VarType type);
/** This function adds a new item to a set. */
void addItem(MutableSet *set, uint64_t element);
/** This function adds a new unique item to the set and returns it.
- This function cannot be used in conjunction with manually adding
- items to the set. */
-
+ This function cannot be used in conjunction with manually adding
+ items to the set. */
+
uint64_t createUniqueItem(MutableSet *set);
/** This function creates an element variable over a set. */
Boolean *applyLogicalOperation(LogicOp op, Boolean **array, uint asize);
/** This function adds a boolean constraint to the set of constraints
- to be satisfied */
+ to be satisfied */
void addConstraint(Boolean *constraint);
bool isUnSAT() { return unsat; }
- Vector<Order *> * getOrders() { return & allOrders;}
+ Vector<Order *> *getOrders() { return &allOrders;}
- Tuner * getTuner() { return tuner; }
+ Tuner *getTuner() { return tuner; }
- HSIteratorBoolean * getConstraints() { return constraints.iterator(); }
+ HSIteratorBoolean *getConstraints() { return constraints.iterator(); }
- SATEncoder * getSATEncoder() {return satEncoder;}
+ SATEncoder *getSATEncoder() {return satEncoder;}
void replaceBooleanWithTrue(Boolean *bexpr);
void replaceBooleanWithFalse(Boolean *bexpr);
void replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb);
-
+
MEMALLOC;
- private:
+private:
void handleXORFalse(BooleanLogic *bexpr, Boolean *child);
void handleIMPLIESTrue(BooleanLogic *bexpr, Boolean *child);
void handleIMPLIESFalse(BooleanLogic *bexpr, Boolean *child);
static inline void *ourcalloc(size_t count, size_t size) { return calloc(count, size); }
static inline void *ourrealloc(void *ptr, size_t size) { return realloc(ptr, size); }
-#define MEMALLOC \
- void * operator new(size_t size) { \
- return ourmalloc(size); \
- } \
- void operator delete(void *p, size_t size) { \
- ourfree(p); \
- } \
- void * operator new[](size_t size) { \
- return ourmalloc(size); \
- } \
- void operator delete[](void *p, size_t size) { \
- ourfree(p); \
- } \
- void * operator new(size_t size, void *p) { /* placement new */ \
- return p; \
+#define MEMALLOC \
+ void *operator new(size_t size) { \
+ return ourmalloc(size); \
+ } \
+ void operator delete(void *p, size_t size) { \
+ ourfree(p); \
+ } \
+ void *operator new[](size_t size) { \
+ return ourmalloc(size); \
+ } \
+ void operator delete[](void *p, size_t size) { \
+ ourfree(p); \
+ } \
+ void *operator new(size_t size, void *p) { /* placement new */ \
+ return p; \
}
#endif/* _MY_MEMORY_H */