Fix bugs
authorbdemsky <bdemsky@uci.edu>
Mon, 23 Oct 2017 22:32:25 +0000 (15:32 -0700)
committerbdemsky <bdemsky@uci.edu>
Mon, 23 Oct 2017 22:32:25 +0000 (15:32 -0700)
src/ASTAnalyses/Encoding/subgraph.h
src/config.h
src/csolver.cc

index 88a1291..9327b97 100644 (file)
@@ -9,6 +9,7 @@ public:
        NodeValuePair(EncodingNode *n, uint64_t val) : node(n), value(val) {}
        EncodingNode *node;
        uint64_t value;
+       CMEMALLOC;
 };
 
 class EncodingValue;
@@ -27,6 +28,7 @@ public:
        HashsetEncodingNode nodes;
        HashsetEncodingValue larger;
        HashsetEncodingValue notequals;
+       CMEMALLOC;
 };
 
 uint hashNodeValuePair(NodeValuePair *nvp);
index 0c53dd6..6eafa57 100644 (file)
@@ -19,7 +19,9 @@
 //#define CONFIG_DEBUG
 #define TRACE_DEBUG
 #endif
-//#define SATCHECK_CONFIG
+
+#define SATCHECK_CONFIG
+
 #ifndef CONFIG_ASSERT
 #define CONFIG_ASSERT
 #endif
index 8af2c71..25c9b1e 100644 (file)
@@ -95,7 +95,7 @@ CSolver* CSolver::deserialize(const char * file){
 
 void CSolver::serialize() {
        model_print("serializing ...\n");
-        printConstraints();
+       printConstraints();
        Serializer serializer("dump");
        SetIteratorBooleanEdge *it = getConstraints();
        while (it->hasNext()) {
@@ -412,9 +412,6 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
 }
 
 void CSolver::addConstraint(BooleanEdge constraint) {
-       if(constraint.isNegated())
-               model_print("!");
-       constraint.getBoolean()->print();
        if (isTrue(constraint))
                return;
        else if (isFalse(constraint)) {
@@ -472,8 +469,8 @@ int CSolver::solve() {
        DecomposeOrderTransform dot(this);
        dot.doTransform();
 
-       //IntegerEncodingTransform iet(this);
-       //iet.doTransform();
+       IntegerEncodingTransform iet(this);
+       iet.doTransform();
 
        EncodingGraph eg(this);
        eg.buildGraph();