Warning message when value of element is undefined in results retrieved from SAT...

[satune.git] / src / csolver.cc

diff --git a/src/csolver.cc b/src/csolver.cc
index b74df47f37c6c22cb20c2e5391b2c0d4e09533ea..b42dbe0974224df3560d5f95b96aed1e5fce56f2 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -25,7 +25,9 @@
 #include "ordergraph.h"
 #include "orderedge.h"
 #include "orderanalysis.h"
+#include "elementopt.h"
 #include <time.h>
+#include <stdarg.h>
 
 CSolver::CSolver() :
        boolTrue(BooleanEdge(new BooleanConst(true))),
@@ -182,6 +184,10 @@ Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange
        return set;
 }
 
+bool CSolver::itemExistInSet(Set *set, uint64_t item){
+        return set->exists(item);
+}
+
 VarType CSolver::getSetVarType(Set *set) {
        return set->getType();
 }
@@ -217,6 +223,10 @@ Element *CSolver::getElementVar(Set *set) {
        return element;
 }
 
+void CSolver::mustHaveValue(Element *element){
+       element->getElementEncoding()->anyValue = true;
+}
+
 Set *CSolver::getElementRange (Element *element) {
        return element->getRange();
 }
@@ -254,14 +264,14 @@ Element *CSolver::applyFunction(Function *function, Element **array, uint numArr
        }
 }
 
-Function *CSolver::createFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range,OverFlowBehavior overflowbehavior) {
-       Function *function = new FunctionOperator(op, domain, numDomain, range, overflowbehavior);
+Function *CSolver::createFunctionOperator(ArithOp op, Set *range, OverFlowBehavior overflowbehavior) {
+       Function *function = new FunctionOperator(op, range, overflowbehavior);
        allFunctions.push(function);
        return function;
 }
 
-Predicate *CSolver::createPredicateOperator(CompOp op, Set **domain, uint numDomain) {
-       Predicate *predicate = new PredicateOperator(op, domain,numDomain);
+Predicate *CSolver::createPredicateOperator(CompOp op) {
+       Predicate *predicate = new PredicateOperator(op);
        allPredicates.push(predicate);
        return predicate;
 }
@@ -272,14 +282,14 @@ Predicate *CSolver::createPredicateTable(Table *table, UndefinedBehavior behavio
        return predicate;
 }
 
-Table *CSolver::createTable(Set **domains, uint numDomain, Set *range) {
-       Table *table = new Table(domains,numDomain,range);
+Table *CSolver::createTable(Set *range) {
+       Table *table = new Table(range);
        allTables.push(table);
        return table;
 }
 
-Table *CSolver::createTableForPredicate(Set **domains, uint numDomain) {
-       return createTable(domains, numDomain, NULL);
+Table *CSolver::createTableForPredicate() {
+       return createTable(NULL);
 }
 
 void CSolver::addTableEntry(Table *table, uint64_t *inputs, uint inputSize, uint64_t result) {
@@ -342,9 +352,11 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg) {
        return applyLogicalOperation(op, array, 1);
 }
 
-static int ptrcompares(const void *p1, const void *p2) {
-       uintptr_t b1 = *(uintptr_t const *) p1;
-       uintptr_t b2 = *(uintptr_t const *) p2;
+static int booleanEdgeCompares(const void *p1, const void *p2) {
+       BooleanEdge be1 = *(BooleanEdge const *) p1;
+       BooleanEdge be2 = *(BooleanEdge const *) p2;
+       uint64_t b1 = be1->id;
+       uint64_t b2 = be2->id;
        if (b1 < b2)
                return -1;
        else if (b1 == b2)
@@ -416,7 +428,7 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
                } else if (newindex == 1) {
                        return newarray[0];
                } else {
-                       bsdqsort(newarray, newindex, sizeof(BooleanEdge), ptrcompares);
+                       bsdqsort(newarray, newindex, sizeof(BooleanEdge), booleanEdgeCompares);
                        array = newarray;
                        asize = newindex;
                }
@@ -578,7 +590,6 @@ int CSolver::solve() {
                }
                delete orderit;
        }
-
        computePolarities(this);
        long long time2 = getTimeNano();
        model_print("Polarity time: %f\n", (time2 - starttime) / NANOSEC);
@@ -595,6 +606,9 @@ int CSolver::solve() {
        IntegerEncodingTransform iet(this);
        iet.doTransform();
 
+       ElementOpt eop(this);
+       eop.doTransform();
+       
        EncodingGraph eg(this);
        eg.buildGraph();
        eg.encode();
@@ -612,7 +626,7 @@ int CSolver::solve() {
 
        model_print("Is problem UNSAT after encoding: %d\n", unsat);
        int result = unsat ? IS_UNSAT : satEncoder->solve();
-       model_print("Result Computed in CSolver: %d\n", result);
+       model_print("Result Computed in SAT solver: %d\n", result);
 
        if (deleteTuner) {
                delete tuner;
@@ -677,3 +691,21 @@ void CSolver::autoTune(uint budget) {
        autotuner->tune();
        delete autotuner;
 }
+
+//Set* CSolver::addItemsToRange(Element* element, uint num, ...){
+//        va_list args;
+//        va_start(args, num);
+//        element->getRange()
+//        uint setSize = set->getSize();
+//        uint newSize = setSize+ num;
+//        uint64_t members[newSize];
+//        for(uint i=0; i<setSize; i++){
+//                members[i] = set->getElement(i);
+//        }
+//        for( uint i=0; i< num; i++){
+//                uint64_t arg = va_arg(args, uint64_t);
+//                members[setSize+i] = arg;
+//        }
+//        va_end(args);
+//        return createSet(set->getType(), members, newSize);
+//}