backout changes
authorbdemsky <bdemsky@uci.edu>
Wed, 20 Sep 2017 05:37:55 +0000 (22:37 -0700)
committerbdemsky <bdemsky@uci.edu>
Wed, 20 Sep 2017 05:48:39 +0000 (22:48 -0700)
src/AST/element.cc
src/AST/element.h
src/ASTAnalyses/Encoding/encodinggraph.cc
src/Backend/constraint.h
src/Collections/vector.h
src/Encoders/elementencoding.h
src/classlist.h
src/csolver.cc
src/mymemory.h

index 922f0a1..ed0a741 100644 (file)
@@ -5,7 +5,6 @@
 #include "function.h"
 #include "table.h"
 #include "csolver.h"
-#include "boolean.h"
 
 Element::Element(ASTNodeType _type) :
        ASTNode(_type),
index 6d25328..72b2ea6 100644 (file)
@@ -4,9 +4,9 @@
 #include "mymemory.h"
 #include "structs.h"
 #include "astnode.h"
-#include "corestructs.h"
 #include "functionencoding.h"
 #include "elementencoding.h"
+#include "boolean.h"
 
 class Element : public ASTNode {
 public:
index 2aee670..9231ad6 100644 (file)
@@ -9,7 +9,6 @@
 #include "qsort.h"
 #include "subgraph.h"
 #include "elementencoding.h"
-#include "boolean.h"
 
 EncodingGraph::EncodingGraph(CSolver * _solver) :
        solver(_solver) {
index 9506042..2f61d72 100644 (file)
@@ -10,6 +10,9 @@
 
 typedef int Literal;
 
+struct Edge;
+typedef struct Edge Edge;
+
 struct Node;
 typedef struct Node Node;
 
index 58e7abd..80ec918 100644 (file)
@@ -18,7 +18,7 @@
        type getVector ## name(Vector ## name * vector, uint index);           \
        void setExpandVector ## name(Vector ## name * vector, uint index, type item); \
        void setVector ## name(Vector ## name * vector, uint index, type item); \
-       uint getSizeVector ## name(Vector ## name * vector);                   \
+       uint getSizeVector ## name(const Vector ## name * vector);                   \
        void setSizeVector ## name(Vector ## name * vector, uint size);        \
        void deleteVector ## name(Vector ## name * vector);                    \
        void clearVector ## name(Vector ## name * vector);                     \
index 37fff60..6797c66 100644 (file)
@@ -1,7 +1,8 @@
 #ifndef ELEMENTENCODING_H
 #define ELEMENTENCODING_H
 #include "classlist.h"
-#include "common.h"
+#include "naiveencoder.h"
+#include "constraint.h"
 
 class ElementEncoding {
 public:
index 2c9a000..69c710e 100644 (file)
@@ -10,6 +10,7 @@
 #ifndef CLASSLIST_H
 #define CLASSLIST_H
 
+#include "mymemory.h"
 #include <inttypes.h>
 #include "classes.h"
 #include "astnode.h"
@@ -66,14 +67,9 @@ class EncodingGraph;
 class EncodingNode;
 class EncodingEdge;
 
-class ElementEncoding;
-class FunctionEncoding;
-
 struct IncrementalSolver;
 typedef struct IncrementalSolver IncrementalSolver;
 struct TableEntry;
 typedef struct TableEntry TableEntry;
 typedef int TunableParam;
-struct Edge;
-typedef struct Edge Edge;
 #endif
index d0d2c06..8ea79e4 100644 (file)
@@ -21,7 +21,7 @@
 #include "preprocess.h"
 #include "serializer.h"
 #include "deserializer.h"
-#include "naiveencoder.h"
+#include "encodinggraph.h"
 
 CSolver::CSolver() :
        boolTrue(BooleanEdge(new BooleanConst(true))),
@@ -439,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();
index e0a60bd..7c63aa1 100644 (file)
@@ -26,7 +26,7 @@
    void * ourrealloc(void *ptr, size_t size);
 */
 
-#if 1
+#if 0
 void * model_malloc(size_t size);
 void model_free(void *ptr);
 void * model_calloc(size_t count, size_t size);