added new directories abstraction-refinement and to-sat. moved files from AST to...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@203 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/Makefile b/Makefile
index 1e7556854f23298d2a14b7a2548bc1dd99071ed1..7917065cf4b6252cc3299ec5b165568285ebb7f0 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -18,6 +18,8 @@ HEADERS=$(SRC)/c_interface/*.h
 .PHONY: all
 all:
        $(MAKE) -C $(SRC)/AST
+       $(MAKE) -C $(SRC)/abstraction-refinement
+       $(MAKE) -C $(SRC)/to-sat
        $(MAKE) -C $(SRC)/sat core
 #      $(MAKE) -C $(SRC)/sat simp
 #      $(MAKE) -C $(SRC)/sat unsound
@@ -27,8 +29,9 @@ all:
        $(MAKE) -C $(SRC)/constantbv
        $(MAKE) -C $(SRC)/parser
        $(MAKE) -C $(SRC)/main
-       $(AR) rc libstp.a  $(SRC)/AST/*.o $(SRC)/AST/printer/*.o $(SRC)/sat/*.or $(SRC)/simplifier/*.o $(SRC)/bitvec/*.o $(SRC)/constantbv/*.o \
-                          $(SRC)/c_interface/*.o $(SRC)/parser/let-funcs.o $(SRC)/parser/parseCVC.o $(SRC)/parser/lexCVC.o $(SRC)/main/*.o
+       $(AR) rc libstp.a  $(SRC)/AST/*.o  $(SRC)/AST/printer/*.o $(SRC)/abstraction-refinement/*.o $(SRC)/to-sat/*.o \
+                          $(SRC)/sat/*.or $(SRC)/simplifier/*.o  $(SRC)/bitvec/*.o $(SRC)/constantbv/*.o $(SRC)/c_interface/*.o \
+                          $(SRC)/parser/let-funcs.o $(SRC)/parser/parseCVC.o $(SRC)/parser/lexCVC.o $(SRC)/main/*.o
        $(RANLIB) libstp.a
        @mkdir -p lib
        @mv libstp.a lib/
@@ -55,6 +58,8 @@ clean:
        rm -rf *.log
        rm -f TAGS
        $(MAKE) clean -C $(SRC)/AST
+       $(MAKE) clean -C $(SRC)/abstraction-refinement
+       $(MAKE) clean -C $(SRC)/to-sat
        $(MAKE) clean -C $(SRC)/sat
        $(MAKE) clean -C $(SRC)/simplifier
        $(MAKE) clean -C $(SRC)/bitvec

diff --git a/scripts/Makefile.in b/scripts/Makefile.in
index 1e7556854f23298d2a14b7a2548bc1dd99071ed1..7917065cf4b6252cc3299ec5b165568285ebb7f0 100644 (file)
--- a/scripts/Makefile.in
+++ b/scripts/Makefile.in
@@ -18,6 +18,8 @@ HEADERS=$(SRC)/c_interface/*.h
 .PHONY: all
 all:
        $(MAKE) -C $(SRC)/AST
+       $(MAKE) -C $(SRC)/abstraction-refinement
+       $(MAKE) -C $(SRC)/to-sat
        $(MAKE) -C $(SRC)/sat core
 #      $(MAKE) -C $(SRC)/sat simp
 #      $(MAKE) -C $(SRC)/sat unsound
@@ -27,8 +29,9 @@ all:
        $(MAKE) -C $(SRC)/constantbv
        $(MAKE) -C $(SRC)/parser
        $(MAKE) -C $(SRC)/main
-       $(AR) rc libstp.a  $(SRC)/AST/*.o $(SRC)/AST/printer/*.o $(SRC)/sat/*.or $(SRC)/simplifier/*.o $(SRC)/bitvec/*.o $(SRC)/constantbv/*.o \
-                          $(SRC)/c_interface/*.o $(SRC)/parser/let-funcs.o $(SRC)/parser/parseCVC.o $(SRC)/parser/lexCVC.o $(SRC)/main/*.o
+       $(AR) rc libstp.a  $(SRC)/AST/*.o  $(SRC)/AST/printer/*.o $(SRC)/abstraction-refinement/*.o $(SRC)/to-sat/*.o \
+                          $(SRC)/sat/*.or $(SRC)/simplifier/*.o  $(SRC)/bitvec/*.o $(SRC)/constantbv/*.o $(SRC)/c_interface/*.o \
+                          $(SRC)/parser/let-funcs.o $(SRC)/parser/parseCVC.o $(SRC)/parser/lexCVC.o $(SRC)/main/*.o
        $(RANLIB) libstp.a
        @mkdir -p lib
        @mv libstp.a lib/
@@ -55,6 +58,8 @@ clean:
        rm -rf *.log
        rm -f TAGS
        $(MAKE) clean -C $(SRC)/AST
+       $(MAKE) clean -C $(SRC)/abstraction-refinement
+       $(MAKE) clean -C $(SRC)/to-sat
        $(MAKE) clean -C $(SRC)/sat
        $(MAKE) clean -C $(SRC)/simplifier
        $(MAKE) clean -C $(SRC)/bitvec

diff --git a/src/AST/AST.h b/src/AST/AST.h
index 110bdcc0ec85480e581b160a2b9d7b4034443f7d..bbffdb199e07f3d0b834793a664a5f2905c67745 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -76,7 +76,7 @@ namespace BEEV
     friend class BeevMgr;
     friend class CNFMgr;
     friend class ASTInterior;
-    friend class vector<ASTNode> ;
+    friend class vector<ASTNode>;
     //Print the arguments in lisp format.
     friend ostream &LispPrintVec(ostream &os, 
                                  const ASTVec &v, 

diff --git a/src/AST/AbstractionRefinement.cpp b/src/abstraction-refinement/AbstractionRefinement.cpp
similarity index 99%
rename from src/AST/AbstractionRefinement.cpp
rename to src/abstraction-refinement/AbstractionRefinement.cpp
index 945c3caab306372817babd4d05a469343b244b7b..3597c99f7a743ac644efaead1172c27f13aa7c0b 100644 (file)
--- a/src/AST/AbstractionRefinement.cpp
+++ b/src/abstraction-refinement/AbstractionRefinement.cpp
@@ -6,9 +6,9 @@
  * LICENSE: Please view LICENSE file in the home dir of this Program
  ********************************************************************/
 // -*- c++ -*-
-#include "AST.h"
-#include "ASTUtil.h"
-#include "../simplifier/bvsolver.h"
+#include "../AST/AST.h"
+#include "../AST/ASTUtil.h"
+//#include "../simplifier/bvsolver.h"
 #include <math.h>
 
 namespace BEEV
@@ -21,6 +21,8 @@ namespace BEEV
   /******************************************************************
    * ARRAY READ ABSTRACTION REFINEMENT
    *   
+   * SATBased_ArrayReadRefinement()
+   *
    * What it really does is, for each array, loop over each index i.
    * inside that loop, it finds all the true and false axioms with i
    * as first index.  When it's got them all, it adds the false axioms

diff --git a/src/abstraction-refinement/Makefile b/src/abstraction-refinement/Makefile
new file mode 100644 (file)
index 0000000..2ad3473
--- /dev/null
+++ b/src/abstraction-refinement/Makefile
@@ -0,0 +1,12 @@
+include ../../scripts/Makefile.common
+
+SRCS = AbstractionRefinement.cpp
+OBJS = $(SRCS:.cpp=.o)
+CFLAGS += -I../sat/mtl -I../sat/simp -I../sat/core
+
+libabstractionrefinement.a:    $(OBJS)
+                               $(AR) rc $@ $^
+                               $(RANLIB) $@
+
+clean: 
+                               rm -rf *.o *~ *.a .#*

diff --git a/src/main/Makefile b/src/main/Makefile
index 03a06650ee53a4cc40acd93b4ada02bc4d181022..af26bcf7b15ee0962f260db8aeee1641d223a452 100644 (file)
--- a/src/main/Makefile
+++ b/src/main/Makefile
@@ -2,7 +2,12 @@ include ../../scripts/Makefile.common
 
 SRCS = Globals.cpp main.cpp
 OBJS = $(SRCS:.cpp=.o)
-LIBS = -L../AST -last -L../sat -lminisat -L../simplifier -lsimplifier -L../bitvec -lconsteval -L../constantbv -lconstantbv -L../parser -lparser
+LIBS =         -L../to-sat -ltosat -L../AST -last -L../abstraction-refinement -labstractionrefinement \
+       -L../sat -lminisat  \
+       -L../simplifier -lsimplifier \
+        -L../bitvec -lconsteval \
+       -L../constantbv -lconstantbv \
+       -L../parser -lparser
 CFLAGS += -I../sat/mtl -I../sat/core  -I../sat/simp -I../sat/unsound
 
 parser: Globals.o main.o

diff --git a/src/AST/BitBlast.cpp b/src/to-sat/BitBlast.cpp
similarity index 99%
rename from src/AST/BitBlast.cpp
rename to src/to-sat/BitBlast.cpp
index 955c7c5f0d7fce3893f1f4fae111aea9451ba1b1..88becd69c5af06c9542076019d6ab55303d6c2f3 100644 (file)
--- a/src/AST/BitBlast.cpp
+++ b/src/to-sat/BitBlast.cpp
@@ -18,7 +18,7 @@
 // A bitblasted term is a vector of ASTNodes for formulas.
 // The 0th element of the vector corresponds to bit 0 -- the low-order bit.
 
-#include "AST.h"
+#include "../AST/AST.h"
 namespace BEEV
 {
   //  extern void lpvec(ASTVec &vec);

diff --git a/src/to-sat/Makefile b/src/to-sat/Makefile
new file mode 100644 (file)
index 0000000..803615f
--- /dev/null
+++ b/src/to-sat/Makefile
@@ -0,0 +1,12 @@
+include ../../scripts/Makefile.common
+
+SRCS = BitBlast.cpp SimpBool.cpp ToCNF.cpp ToSAT.cpp
+OBJS = $(SRCS:.cpp=.o)
+CFLAGS += -I../sat/mtl -I../sat/simp -I../sat/core
+
+libtosat.a:    $(OBJS)
+               $(AR) rc $@ $^
+               $(RANLIB) $@
+
+clean: 
+               rm -rf *.o *~ *.a .#*

diff --git a/src/AST/SimpBool.cpp b/src/to-sat/SimpBool.cpp
similarity index 99%
rename from src/AST/SimpBool.cpp
rename to src/to-sat/SimpBool.cpp
index ea486c0d57f6005334a7f9f6f399c6a33ace0fc6..0aa56ff26e322b6675a46fe78fd68e43f43596d2 100644 (file)
--- a/src/AST/SimpBool.cpp
+++ b/src/to-sat/SimpBool.cpp
@@ -18,7 +18,7 @@
 static bool _trace_simpbool = 0;
 static bool _disable_simpbool = 0;
 
-#include "AST.h"
+#include "../AST/AST.h"
 
 // SMTLIB experimental hack.  Try allocating a single stack here for
 // children to reduce growing of vectors.

diff --git a/src/AST/ToCNF.cpp b/src/to-sat/ToCNF.cpp
similarity index 99%
rename from src/AST/ToCNF.cpp
rename to src/to-sat/ToCNF.cpp
index bc1f99a79838c516d8124a124a6bbc07132aae75..4bc3cf96953accfd7bff9543e211d6cfa933b6ea 100644 (file)
--- a/src/AST/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -7,7 +7,7 @@
  ********************************************************************/
 // -*- c++ -*-
 
-#include "AST.h"
+#include "../AST/AST.h"
 #include "../simplifier/bvsolver.h"
 #include "../sat/sat.h"
 

diff --git a/src/AST/ToSAT.cpp b/src/to-sat/ToSAT.cpp
similarity index 99%
rename from src/AST/ToSAT.cpp
rename to src/to-sat/ToSAT.cpp
index 289d6883076d67437c3c9789c892d55c14da0a70..24c059936c62bfb1f0e386601dfffd8d30f9a08f 100644 (file)
--- a/src/AST/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -6,10 +6,9 @@
  * LICENSE: Please view LICENSE file in the home dir of this Program
  ********************************************************************/
 // -*- c++ -*-
-#include "AST.h"
-#include "ASTUtil.h"
-#include "../simplifier/bvsolver.h"
 #include <cmath>
+#include "../AST/AST.h"
+#include "../simplifier/bvsolver.h"
 #include "../sat/sat.h"
 
 namespace BEEV