backout changes

[satune.git] / src / csolver.cc

diff --git a/src/csolver.cc b/src/csolver.cc
index bcd8f3fe33043298383aa85e0d7a0cd989573a8e..8ea79e439069e0ccb5baac8d0028c82fbdf9793b 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -21,6 +21,7 @@
 #include "preprocess.h"
 #include "serializer.h"
 #include "deserializer.h"
+#include "encodinggraph.h"
 
 CSolver::CSolver() :
        boolTrue(BooleanEdge(new BooleanConst(true))),
@@ -87,6 +88,7 @@ CSolver *CSolver::clone() {
 }
 
 void CSolver::serialize() {
+       model_print("serializing ...\n");
        {
                Serializer serializer("dump");
                SetIteratorBooleanEdge *it = getConstraints();
@@ -137,6 +139,10 @@ uint64_t CSolver::createUniqueItem(MutableSet *set) {
        return element;
 }
 
+void CSolver::finalizeMutableSet(MutableSet* set){
+       set->finalize();
+}
+
 Element *CSolver::getElementVar(Set *set) {
        Element *element = new ElementSet(set);
        allElements.push(element);
@@ -146,7 +152,7 @@ Element *CSolver::getElementVar(Set *set) {
 Element *CSolver::getElementConst(VarType type, uint64_t value) {
        uint64_t array[] = {value};
        Set *set = new Set(type, array, 1);
-       Element *element = new ElementConst(value, type, set);
+       Element *element = new ElementConst(value, set);
        Element *e = elemMap.get(element);
        if (e == NULL) {
                allSets.push(set);
@@ -227,7 +233,7 @@ BooleanEdge CSolver::getBooleanFalse() {
 }
 
 BooleanEdge CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) {
-       return applyPredicateTable(predicate, inputs, numInputs, NULL);
+       return applyPredicateTable(predicate, inputs, numInputs, BooleanEdge(NULL));
 }
 
 BooleanEdge CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, BooleanEdge undefinedStatus) {
@@ -433,6 +439,10 @@ int CSolver::solve() {
        IntegerEncodingTransform iet(this);
        iet.doTransform();
 
+       EncodingGraph eg(this);
+       eg.buildGraph();
+       eg.encode();
+       
        naiveEncodingDecision(this);
        satEncoder->encodeAllSATEncoder(this);
        int result = unsat ? IS_UNSAT : satEncoder->solve();