From: vijay_ganesh Date: Mon, 7 Sep 2009 19:59:26 +0000 (+0000) Subject: added new directories abstraction-refinement and to-sat. moved files from AST to... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=139f1c9348bfbf26ddffe40cc7497b68d61dc78c;p=francis%2Fstp.git added new directories abstraction-refinement and to-sat. moved files from AST to these directories 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 1e75568..7917065 100644 --- 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 1e75568..7917065 100644 --- 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 110bdcc..bbffdb1 100644 --- 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 ; + friend class vector; //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 945c3ca..3597c99 100644 --- 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 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 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 03a0665..af26bcf 100644 --- 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 955c7c5..88becd6 100644 --- 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 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 ea486c0..0aa56ff 100644 --- 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 bc1f99a..4bc3cf9 100644 --- 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 289d688..24c0599 100644 --- 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 +#include "../AST/AST.h" +#include "../simplifier/bvsolver.h" #include "../sat/sat.h" namespace BEEV