}
delete iterator;
}
-
-void orderAnalysis(CSolver *This) {
- uint size = This->allOrders.getSize();
- for (uint i = 0; i < size; i++) {
- Order *order = This->allOrders.get(i);
-
- 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)
- reachMustAnalysis(This, graph, false);
-
- bool mustReachLocal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHLOCAL, &onoff);
-
- if (mustReachLocal) {
- //This pair of analysis is also optional
- if (order->type == PARTIAL) {
- localMustAnalysisPartial(This, graph);
- } else {
- localMustAnalysisTotal(This, graph);
- }
- }
-
- bool mustReachPrune=GETVARTUNABLE(This->tuner, order->type, MUSTREACHPRUNE, &onoff);
-
- if (mustReachPrune)
- removeMustBeTrueNodes(This, graph);
-
- }
-}
void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure);
void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph);
void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph);
-void orderAnalysis(CSolver *This);
-void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph);
#endif/* ORDERGRAPHBUILDER_H */
+++ /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 */
-
#include "mutableset.h"
#include "ops.h"
#include "csolver.h"
+#include "orderencoder.h"
+#include "tunable.h"
+
+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);
+ }
+
+
+ bool mustReachGlobal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHGLOBAL, &onoff);
+
+ if (mustReachGlobal)
+ reachMustAnalysis(This, graph, false);
+
+ bool mustReachLocal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHLOCAL, &onoff);
+
+ if (mustReachLocal) {
+ //This pair of analysis is also optional
+ if (order->type == PARTIAL) {
+ localMustAnalysisPartial(This, graph);
+ } else {
+ localMustAnalysisTotal(This, graph);
+ }
+ }
+
+ bool mustReachPrune=GETVARTUNABLE(This->tuner, order->type, MUSTREACHPRUNE, &onoff);
+
+ if (mustReachPrune)
+ removeMustBeTrueNodes(This, graph);
+
+ //This is needed for splitorder
+ computeStronglyConnectedComponentGraph(graph);
+
+ decomposeOrder(This, order, graph);
+
+ deleteOrderGraph(graph);
+ }
+}
void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
Vector<Order *> ordervec;
#include "classlist.h"
#include "structs.h"
+void orderAnalysis(CSolver *This);
void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph);
#endif /* ORDERDECOMPOSE_H */
* e1=2 e2=7
*/
int main(int numargs, char **argv) {
- CSolver *solver = allocCSolver();
+ CSolver *solver = new CSolver();
uint64_t set1[] = {0, 1, 2};
uint64_t set2[] = {3, 1, 7};
- Set *s1 = createSet(solver, 0, set1, 3);
- Set *s2 = createSet(solver, 0, set2, 3);
- Element *e1 = getElementVar(solver, s1);
- Element *e2 = getElementVar(solver, s2);
+ Set *s1 = solver->createSet(0, set1, 3);
+ Set *s2 = solver->createSet(0, set2, 3);
+ Element *e1 = solver->getElementVar(s1);
+ Element *e2 = solver->getElementVar(s2);
Set *domain[] = {s1, s2};
- Predicate *equals = createPredicateOperator(solver, EQUALS, domain, 2);
+ Predicate *equals = solver->createPredicateOperator(EQUALS, domain, 2);
Element *inputs[] = {e1, e2};
- Boolean *b = applyPredicate(solver, equals, inputs, 2);
- addConstraint(solver, b);
+ Boolean *b = solver->applyPredicate(equals, inputs, 2);
+ solver->addConstraint(b);
- if (startEncoding(solver) == 1)
- printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2));
+ if (solver->startEncoding() == 1)
+ printf("e1=%llu e2=%llu\n", solver->getElementValue(e1), solver->getElementValue(e2));
else
printf("UNSAT\n");
- deleteSolver(solver);
+ delete solver;
}
* Result: b1=1 b2=0 b3=0 b4=0
*/
int main(int numargs, char **argv) {
- CSolver *solver = allocCSolver();
- Boolean *b1 = getBooleanVar(solver, 0);
- Boolean *b2 = getBooleanVar(solver, 0);
- Boolean *b3 = getBooleanVar(solver, 0);
- Boolean *b4 = getBooleanVar(solver, 0);
+ CSolver *solver = new CSolver();
+ Boolean *b1 = solver->getBooleanVar(0);
+ Boolean *b2 = solver->getBooleanVar(0);
+ 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 *andb1b2 = applyLogicalOperation(solver, L_AND, barray1, 2);
+ Boolean *andb1b2 = solver->applyLogicalOperation(L_AND, barray1, 2);
Boolean * barray2[]={andb1b2, b3};
- Boolean *imply = applyLogicalOperation(solver, L_IMPLIES, barray2, 2);
- addConstraint(solver, imply);
+ Boolean *imply = solver->applyLogicalOperation(L_IMPLIES, barray2, 2);
+ solver->addConstraint(imply);
Boolean * barray3[] ={b3};
- Boolean *notb3 = applyLogicalOperation(solver, L_NOT, barray3, 1);
+ Boolean *notb3 = solver->applyLogicalOperation(L_NOT, barray3, 1);
Boolean * barray4[] ={notb3, b4};
- addConstraint(solver, applyLogicalOperation(solver, L_OR, barray4, 2));
+ solver->addConstraint(solver->applyLogicalOperation(L_OR, barray4, 2));
Boolean * barray5[] ={b1, b4};
- addConstraint(solver, applyLogicalOperation(solver, L_XOR, barray5, 2));
- if (startEncoding(solver) == 1)
+ solver->addConstraint(solver->applyLogicalOperation(L_XOR, barray5, 2));
+ if (solver->startEncoding() == 1)
printf("b1=%d b2=%d b3=%d b4=%d\n",
- getBooleanValue(solver,b1), getBooleanValue(solver, b2),
- getBooleanValue(solver, b3), getBooleanValue(solver, b4));
+ solver->getBooleanValue(b1), solver->getBooleanValue(b2),
+ solver->getBooleanValue(b3), solver->getBooleanValue(b4));
else
printf("UNSAT\n");
- deleteSolver(solver);
+ delete solver;
}
* Result: e1=5 e2=6
*/
int main(int numargs, char **argv) {
- CSolver *solver = allocCSolver();
+ CSolver *solver = new CSolver();
uint64_t set1[] = {5};
uint64_t set3[] = {1, 3, 4, 6};
- Set *s1 = createSet(solver, 0, set1, 3);
- Set *s3 = createSet(solver, 0, set3, 4);
- Element *e1 = getElementConst(solver, 4, 5);
- Element *e2 = getElementVar(solver, s3);
+ Set *s1 = solver->createSet(0, set1, 3);
+ Set *s3 = solver->createSet(0, set3, 4);
+ Element *e1 = solver->getElementConst(4, 5);
+ Element *e2 = solver->getElementVar(s3);
Set *domain2[] = {s1, s3};
- Predicate *lt = createPredicateOperator(solver, LT, domain2, 2);
+ Predicate *lt = solver->createPredicateOperator(LT, domain2, 2);
Element *inputs2[] = {e1, e2};
- Boolean *b = applyPredicate(solver, lt, inputs2, 2);
- addConstraint(solver, b);
- if (startEncoding(solver) == 1)
- printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2));
+ Boolean *b = solver->applyPredicate(lt, inputs2, 2);
+ solver->addConstraint(b);
+ if (solver->startEncoding() == 1)
+ printf("e1=%llu e2=%llu\n", solver->getElementValue(e1), solver->getElementValue(e2));
else
printf("UNSAT\n");
- deleteSolver(solver);
-}
\ No newline at end of file
+ delete solver;
+}
#include "csolver.h"
int main(int numargs, char **argv) {
- CSolver *solver = allocCSolver();
+ CSolver *solver = new CSolver();
uint64_t set1[] = {1, 2, 3, 4, 5, 6, 7, 8};
- Set *s = createSet(solver, 0, set1, 8);
- Order *order = createOrder(solver, TOTAL, s);
- Boolean *o12 = orderConstraint(solver, order, 1, 2);
- Boolean *o13 = orderConstraint(solver, order, 1, 3);
- Boolean *o24 = orderConstraint(solver, order, 2, 4);
- Boolean *o34 = orderConstraint(solver, order, 3, 4);
- Boolean *o41 = orderConstraint(solver, order, 4, 1);
- Boolean *o57 = orderConstraint(solver, order, 5, 7);
- Boolean *o76 = orderConstraint(solver, order, 7, 6);
- Boolean *o65 = orderConstraint(solver, order, 6, 5);
- Boolean *o58 = orderConstraint(solver, order, 5, 8);
- Boolean *o81 = orderConstraint(solver, order, 8, 1);
-
- /*
+ Set *s = solver->createSet(0, set1, 8);
+ Order *order = solver->createOrder(TOTAL, s);
+ Boolean *o12 = solver->orderConstraint(order, 1, 2);
+ Boolean *o13 = solver->orderConstraint(order, 1, 3);
+ Boolean *o24 = solver->orderConstraint(order, 2, 4);
+ Boolean *o34 = solver->orderConstraint(order, 3, 4);
+ Boolean *o41 = solver->orderConstraint(order, 4, 1);
+ Boolean *o57 = solver->orderConstraint(order, 5, 7);
+ Boolean *o76 = solver->orderConstraint(order, 7, 6);
+ Boolean *o65 = solver->orderConstraint(order, 6, 5);
+ Boolean *o58 = solver->orderConstraint(order, 5, 8);
+ 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);
addConstraint(solver, applyLogicalOperation(solver, L_IMPLIES,(Boolean *[]) {b3, o57n}, 2) );
addConstraint(solver, applyLogicalOperation(solver, L_AND,(Boolean *[]) {o58, o81}, 2) );
- if (startEncoding(solver) == 1)
+ if (solver->startEncoding() == 1)
printf("SAT\n");
else
- printf("UNSAT\n");*/
- deleteSolver(solver);
+ printf("UNSAT\n");
+ */
+ delete solver;
}
* Result: e1=1, e2=5, e3=7, e4=6, overflow=0
*/
int main(int numargs, char **argv) {
- CSolver *solver = allocCSolver();
+ CSolver *solver = new CSolver();
uint64_t set1[] = {1, 2};
uint64_t set2[] = {3, 5, 7};
uint64_t set3[] = {6, 10, 19};
- Set *s1 = createSet(solver, 0, set1, 2);
- Set *s2 = createSet(solver, 0, set2, 3);
- Set *s3 = createSet(solver, 0, set3, 3);
- Element *e1 = getElementVar(solver, s1);
- Element *e2 = getElementVar(solver, s2);
- Element *e4 = getElementVar(solver, s3);
- Boolean *overflow = getBooleanVar(solver, 2);
+ Set *s1 = solver->createSet(0, set1, 2);
+ Set *s2 = solver->createSet(0, set2, 3);
+ Set *s3 = solver->createSet(0, set3, 3);
+ Element *e1 = solver->getElementVar(s1);
+ Element *e2 = solver->getElementVar(s2);
+ Element *e4 = solver->getElementVar(s3);
+ Boolean *overflow = solver->getBooleanVar(2);
Set *d1[] = {s1, s2};
//change the overflow flag
- Table *t1 = createTable(solver, d1, 2, s2);
+ Table *t1 = solver->createTable(d1, 2, s2);
uint64_t row1[] = {1, 5};
uint64_t row2[] = {2, 3};
uint64_t row3[] = {1, 7};
uint64_t row4[] = {2, 7};
uint64_t row5[] = {2, 5};
uint64_t row6[] = {1, 3};
- addTableEntry(solver, t1, row1, 2, 7);
- addTableEntry(solver, t1, row2, 2, 5);
- addTableEntry(solver, t1, row3, 2, 3);
- addTableEntry(solver, t1, row4, 2, 5);
- addTableEntry(solver, t1, row5, 2, 3);
- addTableEntry(solver, t1, row6, 2, 5);
- Function *f1 = completeTable(solver, t1, FLAGIFFUNDEFINED);
+ solver->addTableEntry(t1, row1, 2, 7);
+ solver->addTableEntry(t1, row2, 2, 5);
+ solver->addTableEntry(t1, row3, 2, 3);
+ solver->addTableEntry(t1, row4, 2, 5);
+ solver->addTableEntry(t1, row5, 2, 3);
+ solver->addTableEntry(t1, row6, 2, 5);
+ Function *f1 = solver->completeTable(t1, FLAGIFFUNDEFINED);
Element * tmparray[]={e1, e2};
- Element *e3 = applyFunction(solver, f1, tmparray, 2, overflow);
+ Element *e3 = solver->applyFunction(f1, tmparray, 2, overflow);
Set *deq[] = {s3,s2};
- Predicate *lte = createPredicateOperator(solver, LTE, deq, 2);
+ Predicate *lte = solver->createPredicateOperator(LTE, deq, 2);
Element *inputs2 [] = {e4, e3};
- Boolean *pred = applyPredicate(solver, lte, inputs2, 2);
- addConstraint(solver, pred);
+ Boolean *pred = solver->applyPredicate(lte, inputs2, 2);
+ solver->addConstraint(pred);
- if (startEncoding(solver) == 1)
+ if (solver->startEncoding() == 1)
printf("e1=%llu e2=%llu e3=%llu e4=%llu overFlow:%d\n",
- getElementValue(solver,e1), getElementValue(solver, e2), getElementValue(solver, e3),
- getElementValue(solver, e4), getBooleanValue(solver, overflow));
+ solver->getElementValue(e1), solver->getElementValue(e2), solver->getElementValue(e3),
+ solver->getElementValue(e4), solver->getBooleanValue(overflow));
else
printf("UNSAT\n");
- deleteSolver(solver);
+ delete solver;
}
* Result: e1=1, e2=1, e3=6 OR 10 OR 19, overflow=1
*/
int main(int numargs, char **argv) {
- CSolver *solver = allocCSolver();
+ CSolver *solver = new CSolver();
uint64_t set1[] = {1, 2};
uint64_t set2[] = {1, 3, 5, 7};
uint64_t set3[] = {6, 10, 19};
- Set *s1 = createSet(solver, 0, set1, 2);
- Set *s2 = createSet(solver, 0, set2, 4);
- Set *s3 = createSet(solver, 0, set3, 3);
- Element *e1 = getElementVar(solver, s1);
- Element *e2 = getElementVar(solver, s2);
- Element *e3 = getElementVar(solver, s3);
+ Set *s1 = solver->createSet(0, set1, 2);
+ Set *s2 = solver->createSet(0, set2, 4);
+ Set *s3 = solver->createSet(0, set3, 3);
+ Element *e1 = solver->getElementVar(s1);
+ Element *e2 = solver->getElementVar(s2);
+ Element *e3 = solver->getElementVar(s3);
Set *d2[] = {s1, s2, s3};
//change the overflow flag
- Table *t1 = createTableForPredicate(solver, d2, 3);
+ Table *t1 = solver->createTableForPredicate(d2, 3);
uint64_t row1[] = {1, 5, 6};
uint64_t row2[] = {2, 3, 19};
uint64_t row3[] = {1, 3, 19};
uint64_t row4[] = {2, 7, 10};
uint64_t row5[] = {1, 7, 6};
uint64_t row6[] = {2, 5, 6};
- addTableEntry(solver, t1, row1, 3, true);
- addTableEntry(solver, t1, row2, 3, true);
- addTableEntry(solver, t1, row3, 3, false);
- addTableEntry(solver, t1, row4, 3, false);
- addTableEntry(solver, t1, row5, 3, false);
- addTableEntry(solver, t1, row6, 3, true);
- Predicate *p1 = createPredicateTable(solver, t1, FLAGIFFUNDEFINED);
- Boolean *undef = getBooleanVar(solver, 2);
+ solver->addTableEntry(t1, row1, 3, true);
+ solver->addTableEntry(t1, row2, 3, true);
+ solver->addTableEntry(t1, row3, 3, false);
+ solver->addTableEntry(t1, row4, 3, false);
+ solver->addTableEntry(t1, row5, 3, false);
+ solver->addTableEntry(t1, row6, 3, true);
+ Predicate *p1 = solver->createPredicateTable(t1, FLAGIFFUNDEFINED);
+ Boolean *undef = solver->getBooleanVar(2);
Element * tmparray[] = {e1, e2, e3};
- Boolean *b1 = applyPredicateTable(solver, p1, tmparray, 3, undef);
- addConstraint(solver, b1);
+ Boolean *b1 = solver->applyPredicateTable(p1, tmparray, 3, undef);
+ solver->addConstraint(b1);
Set *deq[] = {s3,s2};
- Predicate *gte = createPredicateOperator(solver, GTE, deq, 2);
+ Predicate *gte = solver->createPredicateOperator(GTE, deq, 2);
Element *inputs2 [] = {e3, e2};
- Boolean *pred = applyPredicate(solver, gte, inputs2, 2);
- addConstraint(solver, pred);
+ Boolean *pred = solver->applyPredicate(gte, inputs2, 2);
+ solver->addConstraint(pred);
Set *d1[] = {s1, s2};
- Predicate *eq = createPredicateOperator(solver, EQUALS, d1, 2);
+ Predicate *eq = solver->createPredicateOperator(EQUALS, d1, 2);
Element * tmparray2[] = {e1, e2};
- Boolean *pred2 = applyPredicate(solver, eq, tmparray2, 2);
- addConstraint(solver, pred2);
+ Boolean *pred2 = solver->applyPredicate(eq, tmparray2, 2);
+ solver->addConstraint(pred2);
- if (startEncoding(solver) == 1)
+ if (solver->startEncoding() == 1)
printf("e1=%llu e2=%llu e3=%llu undefFlag:%d\n",
- getElementValue(solver,e1), getElementValue(solver, e2),
- getElementValue(solver, e3), getBooleanValue(solver, undef));
+ solver->getElementValue(e1), solver->getElementValue(e2),
+ solver->getElementValue(e3), solver->getBooleanValue(undef));
else
printf("UNSAT\n");
- deleteSolver(solver);
+ delete solver;
}
#include "satencoder.h"
#include "sattranslator.h"
#include "tunable.h"
-#include "orderencoder.h"
#include "polarityassignment.h"
-#include "asttransform.h"
+#include "orderdecompose.h"
CSolver::CSolver() : unsat(false) {
tuner = allocTuner();
int CSolver::startEncoding() {
computePolarities(this);
- ASTTransform(this);
- naiveEncodingDecision(this);
orderAnalysis(this);
+ naiveEncodingDecision(this);
encodeAllSATEncoder(this, satEncoder);
int result = solveCNF(satEncoder->cnf);
model_print("sat_solver's result:%d\tsolutionSize=%d\n", result, satEncoder->cnf->solver->solutionsize);
projects / satune.git / commitdiff