backout changes

diff --git a/src/AST/element.cc b/src/AST/element.cc
index 922f0a107a8635e428c474a01553e8f7bdfdef20..ed0a7416853453316d44d2bb565fa991d8326389 100644 (file)
--- a/src/AST/element.cc
+++ b/src/AST/element.cc
@@ -5,7 +5,6 @@
 #include "function.h"
 #include "table.h"
 #include "csolver.h"
 #include "function.h"
 #include "table.h"
 #include "csolver.h"

-#include "boolean.h"

 
 Element::Element(ASTNodeType _type) :
        ASTNode(_type),
 
 Element::Element(ASTNodeType _type) :
        ASTNode(_type),

diff --git a/src/AST/element.h b/src/AST/element.h
index 6d253280618f74fefd6e99e0f2598ec7f37cf337..72b2ea636c47b238b38a75ebf5dba316c2ac413c 100644 (file)
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -4,9 +4,9 @@
 #include "mymemory.h"
 #include "structs.h"
 #include "astnode.h"
 #include "mymemory.h"
 #include "structs.h"
 #include "astnode.h"

-#include "corestructs.h"

 #include "functionencoding.h"
 #include "elementencoding.h"
 #include "functionencoding.h"
 #include "elementencoding.h"

+#include "boolean.h"

 
 class Element : public ASTNode {
 public:
 
 class Element : public ASTNode {
 public:

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index 2aee67092e41510bbc81d8e6248aaaf0200d2e6d..9231ad6054eeaefef6828445ca92b49bbb83b8f4 100644 (file)
--- 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 "qsort.h"
 #include "subgraph.h"
 #include "elementencoding.h"

-#include "boolean.h"

 
 EncodingGraph::EncodingGraph(CSolver * _solver) :
        solver(_solver) {
 
 EncodingGraph::EncodingGraph(CSolver * _solver) :
        solver(_solver) {

diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h
index 95060423a6fe27902ae1cea4d02c4994e278b7b9..2f61d72a41e31d86acd1ca814a7eb3df43ff38e5 100644 (file)
--- a/src/Backend/constraint.h
+++ b/src/Backend/constraint.h
@@ -10,6 +10,9 @@
 
 typedef int Literal;
 
 
 typedef int Literal;
 

+struct Edge;
+typedef struct Edge Edge;
+

 struct Node;
 typedef struct Node Node;
 
 struct Node;
 typedef struct Node Node;
 

diff --git a/src/Collections/vector.h b/src/Collections/vector.h
index 58e7abd3a6d6f94d9782e9aaeb77ebf558ee176a..80ec9182c9e1d29ee21acdf6e86af75eb24aa865 100644 (file)
--- 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); \
        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);                     \
        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 37fff60943cf250ced384cc78a0fed3c76bcd1a4..6797c66bf530b9024fba0fd3627f43643799ce04 100644 (file)
--- a/src/Encoders/elementencoding.h
+++ b/src/Encoders/elementencoding.h
@@ -1,7 +1,8 @@
 #ifndef ELEMENTENCODING_H
 #define ELEMENTENCODING_H
 #include "classlist.h"
 #ifndef ELEMENTENCODING_H
 #define ELEMENTENCODING_H
 #include "classlist.h"

-#include "common.h"
+#include "naiveencoder.h"
+#include "constraint.h"

 
 class ElementEncoding {
 public:
 
 class ElementEncoding {
 public:

diff --git a/src/classlist.h b/src/classlist.h
index 2c9a00048c8b0bc2d61a52c1dc1470e9653cd6f7..69c710ef3f927232ac5275f5ffaede8a07d151be 100644 (file)
--- a/src/classlist.h
+++ b/src/classlist.h
@@ -10,6 +10,7 @@
 #ifndef CLASSLIST_H
 #define CLASSLIST_H
 
 #ifndef CLASSLIST_H
 #define CLASSLIST_H
 

+#include "mymemory.h"

 #include <inttypes.h>
 #include "classes.h"
 #include "astnode.h"
 #include <inttypes.h>
 #include "classes.h"
 #include "astnode.h"


@@ -66,14 +67,9 @@ class EncodingGraph;
 class EncodingNode;
 class EncodingEdge;
 
 class EncodingNode;
 class EncodingEdge;
 

-class ElementEncoding;
-class FunctionEncoding;
-

 struct IncrementalSolver;
 typedef struct IncrementalSolver IncrementalSolver;
 struct TableEntry;
 typedef struct TableEntry TableEntry;
 typedef int TunableParam;
 struct IncrementalSolver;
 typedef struct IncrementalSolver IncrementalSolver;
 struct TableEntry;
 typedef struct TableEntry TableEntry;
 typedef int TunableParam;

-struct Edge;
-typedef struct Edge Edge;

 #endif
 #endif

diff --git a/src/csolver.cc b/src/csolver.cc
index d0d2c0612497800a6ee891a42f229163443b2797..8ea79e439069e0ccb5baac8d0028c82fbdf9793b 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -21,7 +21,7 @@
 #include "preprocess.h"
 #include "serializer.h"
 #include "deserializer.h"
 #include "preprocess.h"
 #include "serializer.h"
 #include "deserializer.h"

-#include "naiveencoder.h"
+#include "encodinggraph.h"

 
 CSolver::CSolver() :
        boolTrue(BooleanEdge(new BooleanConst(true))),
 
 CSolver::CSolver() :
        boolTrue(BooleanEdge(new BooleanConst(true))),


@@ -439,6 +439,10 @@ int CSolver::solve() {
        IntegerEncodingTransform iet(this);
        iet.doTransform();
 
        IntegerEncodingTransform iet(this);
        iet.doTransform();
 

+       EncodingGraph eg(this);
+       eg.buildGraph();
+       eg.encode();
+       

        naiveEncodingDecision(this);
        satEncoder->encodeAllSATEncoder(this);
        int result = unsat ? IS_UNSAT : satEncoder->solve();
        naiveEncodingDecision(this);
        satEncoder->encodeAllSATEncoder(this);
        int result = unsat ? IS_UNSAT : satEncoder->solve();

diff --git a/src/mymemory.h b/src/mymemory.h
index e0a60bd13294b871199b826e88c0ea13261c1b3d..7c63aa11c10edb99f259ab9a11fffcae8df89794 100644 (file)
--- a/src/mymemory.h
+++ b/src/mymemory.h
@@ -26,7 +26,7 @@
    void * ourrealloc(void *ptr, size_t size);
 */
 
    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);
 void * model_malloc(size_t size);
 void model_free(void *ptr);
 void * model_calloc(size_t count, size_t size);