From: bdemsky <bdemsky@uci.edu>
Date: Wed, 20 Sep 2017 05:37:55 +0000 (-0700)
Subject: backout changes
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=16486cd2b25f9fc04819e811d519947704679bed

backout changes
---

diff --git a/src/AST/element.cc b/src/AST/element.cc
index 922f0a1..ed0a741 100644
--- a/src/AST/element.cc
+++ b/src/AST/element.cc
@@ -5,7 +5,6 @@
 #include "function.h"
 #include "table.h"
 #include "csolver.h"
-#include "boolean.h"
 
 Element::Element(ASTNodeType _type) :
 	ASTNode(_type),
diff --git a/src/AST/element.h b/src/AST/element.h
index 6d25328..72b2ea6 100644
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -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:
diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index 2aee670..9231ad6 100644
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -9,7 +9,6 @@
 #include "qsort.h"
 #include "subgraph.h"
 #include "elementencoding.h"
-#include "boolean.h"
 
 EncodingGraph::EncodingGraph(CSolver * _solver) :
 	solver(_solver) {
diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h
index 9506042..2f61d72 100644
--- a/src/Backend/constraint.h
+++ b/src/Backend/constraint.h
@@ -10,6 +10,9 @@
 
 typedef int Literal;
 
+struct Edge;
+typedef struct Edge Edge;
+
 struct Node;
 typedef struct Node Node;
 
diff --git a/src/Collections/vector.h b/src/Collections/vector.h
index 58e7abd..80ec918 100644
--- a/src/Collections/vector.h
+++ b/src/Collections/vector.h
@@ -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);                     \
diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h
index 37fff60..6797c66 100644
--- a/src/Encoders/elementencoding.h
+++ b/src/Encoders/elementencoding.h
@@ -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:
diff --git a/src/classlist.h b/src/classlist.h
index 2c9a000..69c710e 100644
--- a/src/classlist.h
+++ b/src/classlist.h
@@ -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
diff --git a/src/csolver.cc b/src/csolver.cc
index d0d2c06..8ea79e4 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -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();
diff --git a/src/mymemory.h b/src/mymemory.h
index e0a60bd..7c63aa1 100644
--- a/src/mymemory.h
+++ b/src/mymemory.h
@@ -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);