From b36dcc10012937f74bf67301329f4d9c95ffedd1 Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Tue, 11 Aug 2009 17:11:54 +0000 Subject: [PATCH] moved sources into the src directory git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@107 e59a4935-1847-0410-ae03-e826735625c1 --- Makefile.in | 38 +++-- {AST => src/AST}/AST.cpp | 0 {AST => src/AST}/AST.h | 0 {AST => src/AST}/ASTKind.kinds | 0 {AST => src/AST}/ASTUtil.cpp | 0 {AST => src/AST}/ASTUtil.h | 0 {AST => src/AST}/BitBlast.cpp | 0 {AST => src/AST}/Makefile | 2 +- {AST => src/AST}/STLport_config.h | 0 {AST => src/AST}/SimpBool.cpp | 0 {AST => src/AST}/ToCNF.cpp | 0 {AST => src/AST}/ToSAT.cpp | 0 {AST => src/AST}/Transform.cpp | 0 {AST => src/AST}/asttest.cpp | 0 {AST => src/AST}/bbtest.cpp | 0 {AST => src/AST}/cnftest.cpp | 0 {AST => src/AST}/genkinds.pl | 0 {AST => src/AST}/printer/CPrinter.cpp | 0 {AST => src/AST}/printer/SMTLIBPrinter.cpp | 0 {AST => src/AST}/printer/dotPrinter.cpp | 0 {AST => src/AST}/printer/printers.h | 0 {bitvec => src/bitvec}/Makefile | 2 +- {bitvec => src/bitvec}/consteval.cpp | 0 {c_interface => src/c_interface}/Makefile | 2 +- .../c_interface}/c_interface.cpp | 0 .../c_interface}/c_interface.h | 0 {c_interface => src/c_interface}/fdstream.h | 0 {constantbv => src/constantbv}/Makefile | 2 +- {constantbv => src/constantbv}/constantbv.cpp | 0 {constantbv => src/constantbv}/constantbv.h | 0 {parser => src/parser}/.PL.y.swp | Bin {parser => src/parser}/.parsePL.cpp.swp | Bin {parser => src/parser}/CVC.lex | 0 {parser => src/parser}/CVC.y | 0 {parser => src/parser}/Makefile | 5 +- {parser => src/parser}/let-funcs.cpp | 0 {parser => src/parser}/main.cpp | 0 {parser => src/parser}/smtlib.lex | 0 {parser => src/parser}/smtlib.y | 0 {sat => src/sat}/LICENSE | 0 src/sat/Makefile | 12 ++ {sat => src/sat}/README | 0 {sat => src/sat}/core/Makefile | 0 {sat => src/sat}/core/Solver.C | 0 {sat => src/sat}/core/Solver.h | 0 {sat => src/sat}/core/SolverTypes.h | 0 {sat => src/sat}/mtl/Alg.h | 0 {sat => src/sat}/mtl/BasicHeap.h | 0 {sat => src/sat}/mtl/BoxedVec.h | 0 {sat => src/sat}/mtl/Heap.h | 0 {sat => src/sat}/mtl/Map.h | 0 {sat => src/sat}/mtl/Queue.h | 0 {sat => src/sat}/mtl/Sort.h | 0 {sat => src/sat}/mtl/Vec.h | 0 {sat => src/sat}/mtl/template.mk | 0 {sat => src/sat}/simp/Makefile | 0 {sat => src/sat}/simp/SimpSolver.C | 0 {sat => src/sat}/simp/SimpSolver.h | 0 {sat => src/sat}/simp/depend.mk | 0 {simplifier => src/simplifier}/Makefile | 2 +- {simplifier => src/simplifier}/bvsolver.cpp | 0 {simplifier => src/simplifier}/bvsolver.h | 0 {simplifier => src/simplifier}/simplifier.cpp | 0 tests/bio-tests/Makefile.cvc | 145 ------------------ .../generated_tests}/ArrayGenerator.java | 0 .../generated_tests}/extract.pl | 0 .../form_128.var_32.bits_32.cvc | 0 .../form_16.var_32.bits_32.cvc | 0 .../form_256.var_32.bits_32.cvc | 0 .../form_32.var_128.bits_32.cvc | 0 .../form_32.var_16.bits_32.cvc | 0 .../form_32.var_256.bits_32.cvc | 0 .../form_32.var_32.bits_32.cvc | 0 .../form_32.var_4.bits_32.cvc | 0 .../form_32.var_64.bits_32.cvc | 0 .../form_32.var_8.bits_32.cvc | 0 .../form_4.var_32.bits_32.cvc | 0 .../form_64.var_32.bits_32.cvc | 0 .../form_8.var_32.bits_32.cvc | 0 .../generated_tests}/g.cvc | 0 .../generated_tests}/gen2.cvc | 0 .../generated_tests}/run-experiments.pl | 0 .../generated_tests}/testgen.pl | 0 83 files changed, 37 insertions(+), 173 deletions(-) rename {AST => src/AST}/AST.cpp (100%) rename {AST => src/AST}/AST.h (100%) rename {AST => src/AST}/ASTKind.kinds (100%) rename {AST => src/AST}/ASTUtil.cpp (100%) rename {AST => src/AST}/ASTUtil.h (100%) rename {AST => src/AST}/BitBlast.cpp (100%) rename {AST => src/AST}/Makefile (98%) rename {AST => src/AST}/STLport_config.h (100%) rename {AST => src/AST}/SimpBool.cpp (100%) rename {AST => src/AST}/ToCNF.cpp (100%) rename {AST => src/AST}/ToSAT.cpp (100%) rename {AST => src/AST}/Transform.cpp (100%) rename {AST => src/AST}/asttest.cpp (100%) rename {AST => src/AST}/bbtest.cpp (100%) rename {AST => src/AST}/cnftest.cpp (100%) rename {AST => src/AST}/genkinds.pl (100%) rename {AST => src/AST}/printer/CPrinter.cpp (100%) rename {AST => src/AST}/printer/SMTLIBPrinter.cpp (100%) rename {AST => src/AST}/printer/dotPrinter.cpp (100%) rename {AST => src/AST}/printer/printers.h (100%) rename {bitvec => src/bitvec}/Makefile (85%) rename {bitvec => src/bitvec}/consteval.cpp (100%) rename {c_interface => src/c_interface}/Makefile (87%) rename {c_interface => src/c_interface}/c_interface.cpp (100%) rename {c_interface => src/c_interface}/c_interface.h (100%) rename {c_interface => src/c_interface}/fdstream.h (100%) rename {constantbv => src/constantbv}/Makefile (84%) rename {constantbv => src/constantbv}/constantbv.cpp (100%) rename {constantbv => src/constantbv}/constantbv.h (100%) rename {parser => src/parser}/.PL.y.swp (100%) rename {parser => src/parser}/.parsePL.cpp.swp (100%) rename {parser => src/parser}/CVC.lex (100%) rename {parser => src/parser}/CVC.y (100%) rename {parser => src/parser}/Makefile (95%) rename {parser => src/parser}/let-funcs.cpp (100%) rename {parser => src/parser}/main.cpp (100%) rename {parser => src/parser}/smtlib.lex (100%) rename {parser => src/parser}/smtlib.y (100%) rename {sat => src/sat}/LICENSE (100%) create mode 100644 src/sat/Makefile rename {sat => src/sat}/README (100%) rename {sat => src/sat}/core/Makefile (100%) rename {sat => src/sat}/core/Solver.C (100%) rename {sat => src/sat}/core/Solver.h (100%) rename {sat => src/sat}/core/SolverTypes.h (100%) rename {sat => src/sat}/mtl/Alg.h (100%) rename {sat => src/sat}/mtl/BasicHeap.h (100%) rename {sat => src/sat}/mtl/BoxedVec.h (100%) rename {sat => src/sat}/mtl/Heap.h (100%) rename {sat => src/sat}/mtl/Map.h (100%) rename {sat => src/sat}/mtl/Queue.h (100%) rename {sat => src/sat}/mtl/Sort.h (100%) rename {sat => src/sat}/mtl/Vec.h (100%) rename {sat => src/sat}/mtl/template.mk (100%) rename {sat => src/sat}/simp/Makefile (100%) rename {sat => src/sat}/simp/SimpSolver.C (100%) rename {sat => src/sat}/simp/SimpSolver.h (100%) rename {sat => src/sat}/simp/depend.mk (100%) rename {simplifier => src/simplifier}/Makefile (86%) rename {simplifier => src/simplifier}/bvsolver.cpp (100%) rename {simplifier => src/simplifier}/bvsolver.h (100%) rename {simplifier => src/simplifier}/simplifier.cpp (100%) delete mode 100644 tests/bio-tests/Makefile.cvc rename {generated_tests => tests/generated_tests}/ArrayGenerator.java (100%) rename {generated_tests => tests/generated_tests}/extract.pl (100%) rename {generated_tests => tests/generated_tests}/form_128.var_32.bits_32.cvc (100%) rename {generated_tests => tests/generated_tests}/form_16.var_32.bits_32.cvc (100%) rename {generated_tests => tests/generated_tests}/form_256.var_32.bits_32.cvc (100%) rename {generated_tests => tests/generated_tests}/form_32.var_128.bits_32.cvc (100%) rename {generated_tests => tests/generated_tests}/form_32.var_16.bits_32.cvc (100%) rename {generated_tests => tests/generated_tests}/form_32.var_256.bits_32.cvc (100%) rename {generated_tests => tests/generated_tests}/form_32.var_32.bits_32.cvc (100%) rename {generated_tests => tests/generated_tests}/form_32.var_4.bits_32.cvc (100%) rename {generated_tests => tests/generated_tests}/form_32.var_64.bits_32.cvc (100%) rename {generated_tests => tests/generated_tests}/form_32.var_8.bits_32.cvc (100%) rename {generated_tests => tests/generated_tests}/form_4.var_32.bits_32.cvc (100%) rename {generated_tests => tests/generated_tests}/form_64.var_32.bits_32.cvc (100%) rename {generated_tests => tests/generated_tests}/form_8.var_32.bits_32.cvc (100%) rename {generated_tests => tests/generated_tests}/g.cvc (100%) rename {generated_tests => tests/generated_tests}/gen2.cvc (100%) rename {generated_tests => tests/generated_tests}/run-experiments.pl (100%) rename {generated_tests => tests/generated_tests}/testgen.pl (100%) diff --git a/Makefile.in b/Makefile.in index 1b99b56..71c5b8c 100644 --- a/Makefile.in +++ b/Makefile.in @@ -10,27 +10,25 @@ BIN_DIR=$(PREFIX)/bin LIB_DIR=$(PREFIX)/lib INCLUDE_DIR=$(PREFIX)/include/stp +SRC=src BINARIES=bin/stp LIBRARIES=lib/libstp.a -HEADERS=c_interface/*.h +HEADERS=$(SRC)/c_interface/*.h -# NB: the TAGS target is a hack to get around this recursive make nonsense -# we want all the source and header files generated before we make tags .PHONY: all all: - $(MAKE) -C AST - $(MAKE) -C sat core - $(MAKE) -C simplifier - $(MAKE) -C bitvec - $(MAKE) -C c_interface - $(MAKE) -C constantbv - $(MAKE) -C parser - #$(AR) rc libstp.a AST/*.o sat/core/*.or simplifier/*.o bitvec/*.o constantbv/*.o c_interface/*.o parser/let-funcs.o parser/parseCVC.o parser/lexCVC.o - $(AR) rc libstp.a AST/*.o sat/*.a simplifier/*.o bitvec/*.o constantbv/*.o c_interface/*.o parser/let-funcs.o parser/parseCVC.o parser/lexCVC.o + $(MAKE) -C $(SRC)/AST + $(MAKE) -C $(SRC)/sat core + $(MAKE) -C $(SRC)/simplifier + $(MAKE) -C $(SRC)/bitvec + $(MAKE) -C $(SRC)/c_interface + $(MAKE) -C $(SRC)/constantbv + $(MAKE) -C $(SRC)/parser + $(AR) rc libstp.a $(SRC)/AST/*.o $(SRC)/sat/*.a $(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 $(RANLIB) libstp.a @mkdir -p lib @mv libstp.a lib/ -# $(MAKE) TAGS @echo "" @echo "Compilation successful." @echo "Type 'make install' to install STP." @@ -55,13 +53,13 @@ clean: #rm -rf Makefile #rm -rf config.info rm -f TAGS - $(MAKE) clean -C AST - $(MAKE) clean -C sat - $(MAKE) clean -C simplifier - $(MAKE) clean -C bitvec - $(MAKE) clean -C parser - $(MAKE) clean -C c_interface - $(MAKE) clean -C constantbv + $(MAKE) clean -C $(SRC)/AST + $(MAKE) clean -C $(SRC)/sat + $(MAKE) clean -C $(SRC)/simplifier + $(MAKE) clean -C $(SRC)/bitvec + $(MAKE) clean -C $(SRC)/parser + $(MAKE) clean -C $(SRC)/c_interface + $(MAKE) clean -C $(SRC)/constantbv # this is make way too difficult because of the recursive Make junk, it # should be removed diff --git a/AST/AST.cpp b/src/AST/AST.cpp similarity index 100% rename from AST/AST.cpp rename to src/AST/AST.cpp diff --git a/AST/AST.h b/src/AST/AST.h similarity index 100% rename from AST/AST.h rename to src/AST/AST.h diff --git a/AST/ASTKind.kinds b/src/AST/ASTKind.kinds similarity index 100% rename from AST/ASTKind.kinds rename to src/AST/ASTKind.kinds diff --git a/AST/ASTUtil.cpp b/src/AST/ASTUtil.cpp similarity index 100% rename from AST/ASTUtil.cpp rename to src/AST/ASTUtil.cpp diff --git a/AST/ASTUtil.h b/src/AST/ASTUtil.h similarity index 100% rename from AST/ASTUtil.h rename to src/AST/ASTUtil.h diff --git a/AST/BitBlast.cpp b/src/AST/BitBlast.cpp similarity index 100% rename from AST/BitBlast.cpp rename to src/AST/BitBlast.cpp diff --git a/AST/Makefile b/src/AST/Makefile similarity index 98% rename from AST/Makefile rename to src/AST/Makefile index aa2f5c9..a91aa50 100644 --- a/AST/Makefile +++ b/src/AST/Makefile @@ -1,4 +1,4 @@ -include ../Makefile.common +include ../../Makefile.common #SRCS = AST.cpp ASTKind.cpp ASTUtil.cpp BitBlast.cpp SimpBool.cpp ToCNF.cpp DPLLMgr.cpp ToSAT.cpp Transform.cpp SRCS = AST.cpp ASTKind.cpp ASTUtil.cpp BitBlast.cpp SimpBool.cpp ToCNF.cpp ToSAT.cpp Transform.cpp printer/SMTLIBPrinter.cpp printer/dotPrinter.cpp printer/CPrinter.cpp diff --git a/AST/STLport_config.h b/src/AST/STLport_config.h similarity index 100% rename from AST/STLport_config.h rename to src/AST/STLport_config.h diff --git a/AST/SimpBool.cpp b/src/AST/SimpBool.cpp similarity index 100% rename from AST/SimpBool.cpp rename to src/AST/SimpBool.cpp diff --git a/AST/ToCNF.cpp b/src/AST/ToCNF.cpp similarity index 100% rename from AST/ToCNF.cpp rename to src/AST/ToCNF.cpp diff --git a/AST/ToSAT.cpp b/src/AST/ToSAT.cpp similarity index 100% rename from AST/ToSAT.cpp rename to src/AST/ToSAT.cpp diff --git a/AST/Transform.cpp b/src/AST/Transform.cpp similarity index 100% rename from AST/Transform.cpp rename to src/AST/Transform.cpp diff --git a/AST/asttest.cpp b/src/AST/asttest.cpp similarity index 100% rename from AST/asttest.cpp rename to src/AST/asttest.cpp diff --git a/AST/bbtest.cpp b/src/AST/bbtest.cpp similarity index 100% rename from AST/bbtest.cpp rename to src/AST/bbtest.cpp diff --git a/AST/cnftest.cpp b/src/AST/cnftest.cpp similarity index 100% rename from AST/cnftest.cpp rename to src/AST/cnftest.cpp diff --git a/AST/genkinds.pl b/src/AST/genkinds.pl similarity index 100% rename from AST/genkinds.pl rename to src/AST/genkinds.pl diff --git a/AST/printer/CPrinter.cpp b/src/AST/printer/CPrinter.cpp similarity index 100% rename from AST/printer/CPrinter.cpp rename to src/AST/printer/CPrinter.cpp diff --git a/AST/printer/SMTLIBPrinter.cpp b/src/AST/printer/SMTLIBPrinter.cpp similarity index 100% rename from AST/printer/SMTLIBPrinter.cpp rename to src/AST/printer/SMTLIBPrinter.cpp diff --git a/AST/printer/dotPrinter.cpp b/src/AST/printer/dotPrinter.cpp similarity index 100% rename from AST/printer/dotPrinter.cpp rename to src/AST/printer/dotPrinter.cpp diff --git a/AST/printer/printers.h b/src/AST/printer/printers.h similarity index 100% rename from AST/printer/printers.h rename to src/AST/printer/printers.h diff --git a/bitvec/Makefile b/src/bitvec/Makefile similarity index 85% rename from bitvec/Makefile rename to src/bitvec/Makefile index 7e4fa85..ac885f5 100644 --- a/bitvec/Makefile +++ b/src/bitvec/Makefile @@ -1,4 +1,4 @@ -include ../Makefile.common +include ../../Makefile.common SRCS = consteval.cpp OBJS = $(SRCS:.cpp=.o) diff --git a/bitvec/consteval.cpp b/src/bitvec/consteval.cpp similarity index 100% rename from bitvec/consteval.cpp rename to src/bitvec/consteval.cpp diff --git a/c_interface/Makefile b/src/c_interface/Makefile similarity index 87% rename from c_interface/Makefile rename to src/c_interface/Makefile index 3849557..11cca91 100644 --- a/c_interface/Makefile +++ b/src/c_interface/Makefile @@ -1,4 +1,4 @@ -include ../Makefile.common +include ../../Makefile.common SRCS = c_interface.cpp OBJS = $(SRCS:.cpp=.o) diff --git a/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp similarity index 100% rename from c_interface/c_interface.cpp rename to src/c_interface/c_interface.cpp diff --git a/c_interface/c_interface.h b/src/c_interface/c_interface.h similarity index 100% rename from c_interface/c_interface.h rename to src/c_interface/c_interface.h diff --git a/c_interface/fdstream.h b/src/c_interface/fdstream.h similarity index 100% rename from c_interface/fdstream.h rename to src/c_interface/fdstream.h diff --git a/constantbv/Makefile b/src/constantbv/Makefile similarity index 84% rename from constantbv/Makefile rename to src/constantbv/Makefile index cd94ad9..9ddcb79 100644 --- a/constantbv/Makefile +++ b/src/constantbv/Makefile @@ -1,4 +1,4 @@ -include ../Makefile.common +include ../../Makefile.common SRCS = constantbv.cpp OBJS = $(SRCS:.cpp=.o) diff --git a/constantbv/constantbv.cpp b/src/constantbv/constantbv.cpp similarity index 100% rename from constantbv/constantbv.cpp rename to src/constantbv/constantbv.cpp diff --git a/constantbv/constantbv.h b/src/constantbv/constantbv.h similarity index 100% rename from constantbv/constantbv.h rename to src/constantbv/constantbv.h diff --git a/parser/.PL.y.swp b/src/parser/.PL.y.swp similarity index 100% rename from parser/.PL.y.swp rename to src/parser/.PL.y.swp diff --git a/parser/.parsePL.cpp.swp b/src/parser/.parsePL.cpp.swp similarity index 100% rename from parser/.parsePL.cpp.swp rename to src/parser/.parsePL.cpp.swp diff --git a/parser/CVC.lex b/src/parser/CVC.lex similarity index 100% rename from parser/CVC.lex rename to src/parser/CVC.lex diff --git a/parser/CVC.y b/src/parser/CVC.y similarity index 100% rename from parser/CVC.y rename to src/parser/CVC.y diff --git a/parser/Makefile b/src/parser/Makefile similarity index 95% rename from parser/Makefile rename to src/parser/Makefile index 8ad9a9a..f803700 100644 --- a/parser/Makefile +++ b/src/parser/Makefile @@ -1,5 +1,4 @@ - -include ../Makefile.common +include ../../Makefile.common LEX=flex YACC=bison -d -y --debug -v @@ -13,7 +12,7 @@ all: parseSMT.cpp lexSMT.cpp parseCVC.cpp lexCVC.cpp let-funcs.cpp parser parseC parser: lexCVC.o parseCVC.o lexSMT.o parseSMT.o let-funcs.o main.o $(CXX) $(CFLAGS) $(LDFLAGS) lexCVC.o lexSMT.o parseCVC.o parseSMT.o main.o let-funcs.o $(LIBS) -o parser - @mv parser ../bin/stp + @mv parser ../../bin/stp lexCVC.cpp: CVC.lex parseCVC_defs.h ../AST/AST.h $(LEX) -o lexCVC.cpp --prefix cvc CVC.lex diff --git a/parser/let-funcs.cpp b/src/parser/let-funcs.cpp similarity index 100% rename from parser/let-funcs.cpp rename to src/parser/let-funcs.cpp diff --git a/parser/main.cpp b/src/parser/main.cpp similarity index 100% rename from parser/main.cpp rename to src/parser/main.cpp diff --git a/parser/smtlib.lex b/src/parser/smtlib.lex similarity index 100% rename from parser/smtlib.lex rename to src/parser/smtlib.lex diff --git a/parser/smtlib.y b/src/parser/smtlib.y similarity index 100% rename from parser/smtlib.y rename to src/parser/smtlib.y diff --git a/sat/LICENSE b/src/sat/LICENSE similarity index 100% rename from sat/LICENSE rename to src/sat/LICENSE diff --git a/src/sat/Makefile b/src/sat/Makefile new file mode 100644 index 0000000..9f48c4b --- /dev/null +++ b/src/sat/Makefile @@ -0,0 +1,12 @@ +.PHONY: core +core: + $(MAKE) -C core lib all +.PHONY: simp +simp: + $(MAKE) -C simp lib all + +.PHONY: clean +clean: + rm -rf *~ libminisat.a + $(MAKE) -C core clean + $(MAKE) -C simp clean \ No newline at end of file diff --git a/sat/README b/src/sat/README similarity index 100% rename from sat/README rename to src/sat/README diff --git a/sat/core/Makefile b/src/sat/core/Makefile similarity index 100% rename from sat/core/Makefile rename to src/sat/core/Makefile diff --git a/sat/core/Solver.C b/src/sat/core/Solver.C similarity index 100% rename from sat/core/Solver.C rename to src/sat/core/Solver.C diff --git a/sat/core/Solver.h b/src/sat/core/Solver.h similarity index 100% rename from sat/core/Solver.h rename to src/sat/core/Solver.h diff --git a/sat/core/SolverTypes.h b/src/sat/core/SolverTypes.h similarity index 100% rename from sat/core/SolverTypes.h rename to src/sat/core/SolverTypes.h diff --git a/sat/mtl/Alg.h b/src/sat/mtl/Alg.h similarity index 100% rename from sat/mtl/Alg.h rename to src/sat/mtl/Alg.h diff --git a/sat/mtl/BasicHeap.h b/src/sat/mtl/BasicHeap.h similarity index 100% rename from sat/mtl/BasicHeap.h rename to src/sat/mtl/BasicHeap.h diff --git a/sat/mtl/BoxedVec.h b/src/sat/mtl/BoxedVec.h similarity index 100% rename from sat/mtl/BoxedVec.h rename to src/sat/mtl/BoxedVec.h diff --git a/sat/mtl/Heap.h b/src/sat/mtl/Heap.h similarity index 100% rename from sat/mtl/Heap.h rename to src/sat/mtl/Heap.h diff --git a/sat/mtl/Map.h b/src/sat/mtl/Map.h similarity index 100% rename from sat/mtl/Map.h rename to src/sat/mtl/Map.h diff --git a/sat/mtl/Queue.h b/src/sat/mtl/Queue.h similarity index 100% rename from sat/mtl/Queue.h rename to src/sat/mtl/Queue.h diff --git a/sat/mtl/Sort.h b/src/sat/mtl/Sort.h similarity index 100% rename from sat/mtl/Sort.h rename to src/sat/mtl/Sort.h diff --git a/sat/mtl/Vec.h b/src/sat/mtl/Vec.h similarity index 100% rename from sat/mtl/Vec.h rename to src/sat/mtl/Vec.h diff --git a/sat/mtl/template.mk b/src/sat/mtl/template.mk similarity index 100% rename from sat/mtl/template.mk rename to src/sat/mtl/template.mk diff --git a/sat/simp/Makefile b/src/sat/simp/Makefile similarity index 100% rename from sat/simp/Makefile rename to src/sat/simp/Makefile diff --git a/sat/simp/SimpSolver.C b/src/sat/simp/SimpSolver.C similarity index 100% rename from sat/simp/SimpSolver.C rename to src/sat/simp/SimpSolver.C diff --git a/sat/simp/SimpSolver.h b/src/sat/simp/SimpSolver.h similarity index 100% rename from sat/simp/SimpSolver.h rename to src/sat/simp/SimpSolver.h diff --git a/sat/simp/depend.mk b/src/sat/simp/depend.mk similarity index 100% rename from sat/simp/depend.mk rename to src/sat/simp/depend.mk diff --git a/simplifier/Makefile b/src/simplifier/Makefile similarity index 86% rename from simplifier/Makefile rename to src/simplifier/Makefile index 0dc964c..b573996 100644 --- a/simplifier/Makefile +++ b/src/simplifier/Makefile @@ -1,4 +1,4 @@ -include ../Makefile.common +include ../../Makefile.common SRCS = simplifier.cpp bvsolver.cpp OBJS = $(SRCS:.cpp=.o) diff --git a/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp similarity index 100% rename from simplifier/bvsolver.cpp rename to src/simplifier/bvsolver.cpp diff --git a/simplifier/bvsolver.h b/src/simplifier/bvsolver.h similarity index 100% rename from simplifier/bvsolver.h rename to src/simplifier/bvsolver.h diff --git a/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp similarity index 100% rename from simplifier/simplifier.cpp rename to src/simplifier/simplifier.cpp diff --git a/tests/bio-tests/Makefile.cvc b/tests/bio-tests/Makefile.cvc deleted file mode 100644 index 184666d..0000000 --- a/tests/bio-tests/Makefile.cvc +++ /dev/null @@ -1,145 +0,0 @@ - # STP (Simple Theorem Prover) top level makefile - # - # To make in debug mode, type 'make "CLFAGS=-ggdb" - # To make in optimized mode, type 'make "CFLAGS=-O2" - - -include Makefile.common config.info - -BIN_DIR=$(PREFIX)/bin -LIB_DIR=$(PREFIX)/lib -INCLUDE_DIR=$(PREFIX)/include/stp - -BINARIES=bin/stp -LIBRARIES=lib/libstp.a -HEADERS=c_interface/*.h - -# NB: the TAGS target is a hack to get around this recursive make nonsense -# we want all the source and header files generated before we make tags -.PHONY: all -all: - $(MAKE) -C AST - $(MAKE) -C sat/simp libp - $(MAKE) -C simplifier - $(MAKE) -C bitvec - $(MAKE) -C c_interface - $(MAKE) -C constantbv - $(MAKE) -C parser - $(AR) rc libstp.a AST/*.o sat/simp/*.op sat/core/*.op simplifier/*.o bitvec/*.o constantbv/*.o c_interface/*.o - $(RANLIB) libstp.a - @mkdir -p lib - @mv libstp.a lib/ -# $(MAKE) TAGS - @echo "" - @echo "Compilation successful." - @echo "Type 'make install' to install STP." - - -.PHONY: install -install: all - @cp -f $(BINARIES) $(BIN_DIR) - @cp -f $(LIBRARIES) $(LIB_DIR) - @cp -f $(HEADERS) $(INCLUDE_DIR) - @echo "STP installed successfully." - -.PHONY: clean -clean: - rm -rf *~ - rm -rf *.a - rm -rf lib/*.a - rm -rf test/*~ - rm -rf bin/*~ - rm -rf bin/stp - rm -rf *.log - #rm -rf Makefile - #rm -rf config.info - rm -f TAGS - $(MAKE) clean -C AST - $(MAKE) clean -C sat/simp - $(MAKE) clean -C simplifier - $(MAKE) clean -C bitvec - $(MAKE) clean -C parser - $(MAKE) clean -C c_interface - $(MAKE) clean -C constantbv - -# this is make way too difficult because of the recursive Make junk, it -# should be removed -TAGS: FORCE - find . -name "*.[h]" -or -name "*.cpp" -or -name "*.C" | grep -v SCCS | etags - - -FORCE: - -# The higher the level, the more tests are run (3 = all) -REGRESS_TESTS0 = test \ - test/EGT -REGRESS_LEVEL=4 -REGRESS_TESTS=$(REGRESS_TESTS0) -REGRESS_LOG = `date +%Y-%m-%d`"-regress.log" -PROGNAME=bin/stp -ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS) - -.PHONY: regress -regress: - @echo "*********************************************************" \ - | tee -a $(REGRESS_LOG) - @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG) - @echo "*********************************************************" \ - | tee -a $(REGRESS_LOG) - bin/run_tests $(ALL_OPTIONS) 2>&1 | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ] - @echo "*********************************************************" \ - | tee -a $(REGRESS_LOG) - @echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG) - @echo "*********************************************************" \ - | tee -a $(REGRESS_LOG) - -# The higher the level, the more tests are run (3 = all) -REGRESS_TESTS0 = test \ - test/EGT -REGRESS_LEVEL=4 -REGRESS_TESTS=$(REGRESS_TESTS0) -#REGRESS_LOG = `date +%Y-%m-%d`"-regress-bigarray.log" -PROGNAME=bin/stp -ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS) - -.PHONY: regressbigarray -regressbigarray: - @echo "*********************************************************" \ - | tee -a $(REGRESS_LOG) - @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG) - @echo "*********************************************************" \ - | tee -a $(REGRESS_LOG) - bin/run_bigarray_tests $(ALL_OPTIONS) 2>&1 | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ] - @echo "*********************************************************" \ - | tee -a $(REGRESS_LOG) - @echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG) - @echo "*********************************************************" \ - | tee -a $(REGRESS_LOG) - -.PHONY: regressall -regressall: - $(MAKE) install - $(MAKE) regress - -GRIND_LOG = `date +%Y-%m-%d`"-grind.log" -GRINDPROG = valgrind --leak-check=full --undef-value-errors=no -GRIND_TAR = $(BIN_DIR)/stp -d -GRIND_CALL = -vc "$(GRINDPROG) $(GRIND_TAR)" -GRIND_OPTIONS = -l $(REGRESS_LEVEL) -rt $(GRIND_CALL) $(REGRESS_TESTS) - - -.PHONY: grind -grind: - - $(MAKE) install CFLAGS="-ggdb -pg -g" - @echo "*********************************************************" \ - | tee -a $(GRIND_LOG) - @echo "Starting tests at" `date` | tee -a $(GRIND_LOG) - @echo "*********************************************************" \ - | tee -a $(GRIND_LOG) - bin/run_tests $(GRIND_OPTIONS) 2>&1 | tee -a $(GRIND_LOG); [ $${PIPESTATUS[0]} -eq 0 ] - @echo "*********************************************************" \ - | tee -a $(GRIND_LOG) - @echo "Output is saved in $(GRIND_LOG)" | tee -a $(GRIND_LOG) - @echo "*********************************************************" \ - | tee -a $(GRIND_LOG) - diff --git a/generated_tests/ArrayGenerator.java b/tests/generated_tests/ArrayGenerator.java similarity index 100% rename from generated_tests/ArrayGenerator.java rename to tests/generated_tests/ArrayGenerator.java diff --git a/generated_tests/extract.pl b/tests/generated_tests/extract.pl similarity index 100% rename from generated_tests/extract.pl rename to tests/generated_tests/extract.pl diff --git a/generated_tests/form_128.var_32.bits_32.cvc b/tests/generated_tests/form_128.var_32.bits_32.cvc similarity index 100% rename from generated_tests/form_128.var_32.bits_32.cvc rename to tests/generated_tests/form_128.var_32.bits_32.cvc diff --git a/generated_tests/form_16.var_32.bits_32.cvc b/tests/generated_tests/form_16.var_32.bits_32.cvc similarity index 100% rename from generated_tests/form_16.var_32.bits_32.cvc rename to tests/generated_tests/form_16.var_32.bits_32.cvc diff --git a/generated_tests/form_256.var_32.bits_32.cvc b/tests/generated_tests/form_256.var_32.bits_32.cvc similarity index 100% rename from generated_tests/form_256.var_32.bits_32.cvc rename to tests/generated_tests/form_256.var_32.bits_32.cvc diff --git a/generated_tests/form_32.var_128.bits_32.cvc b/tests/generated_tests/form_32.var_128.bits_32.cvc similarity index 100% rename from generated_tests/form_32.var_128.bits_32.cvc rename to tests/generated_tests/form_32.var_128.bits_32.cvc diff --git a/generated_tests/form_32.var_16.bits_32.cvc b/tests/generated_tests/form_32.var_16.bits_32.cvc similarity index 100% rename from generated_tests/form_32.var_16.bits_32.cvc rename to tests/generated_tests/form_32.var_16.bits_32.cvc diff --git a/generated_tests/form_32.var_256.bits_32.cvc b/tests/generated_tests/form_32.var_256.bits_32.cvc similarity index 100% rename from generated_tests/form_32.var_256.bits_32.cvc rename to tests/generated_tests/form_32.var_256.bits_32.cvc diff --git a/generated_tests/form_32.var_32.bits_32.cvc b/tests/generated_tests/form_32.var_32.bits_32.cvc similarity index 100% rename from generated_tests/form_32.var_32.bits_32.cvc rename to tests/generated_tests/form_32.var_32.bits_32.cvc diff --git a/generated_tests/form_32.var_4.bits_32.cvc b/tests/generated_tests/form_32.var_4.bits_32.cvc similarity index 100% rename from generated_tests/form_32.var_4.bits_32.cvc rename to tests/generated_tests/form_32.var_4.bits_32.cvc diff --git a/generated_tests/form_32.var_64.bits_32.cvc b/tests/generated_tests/form_32.var_64.bits_32.cvc similarity index 100% rename from generated_tests/form_32.var_64.bits_32.cvc rename to tests/generated_tests/form_32.var_64.bits_32.cvc diff --git a/generated_tests/form_32.var_8.bits_32.cvc b/tests/generated_tests/form_32.var_8.bits_32.cvc similarity index 100% rename from generated_tests/form_32.var_8.bits_32.cvc rename to tests/generated_tests/form_32.var_8.bits_32.cvc diff --git a/generated_tests/form_4.var_32.bits_32.cvc b/tests/generated_tests/form_4.var_32.bits_32.cvc similarity index 100% rename from generated_tests/form_4.var_32.bits_32.cvc rename to tests/generated_tests/form_4.var_32.bits_32.cvc diff --git a/generated_tests/form_64.var_32.bits_32.cvc b/tests/generated_tests/form_64.var_32.bits_32.cvc similarity index 100% rename from generated_tests/form_64.var_32.bits_32.cvc rename to tests/generated_tests/form_64.var_32.bits_32.cvc diff --git a/generated_tests/form_8.var_32.bits_32.cvc b/tests/generated_tests/form_8.var_32.bits_32.cvc similarity index 100% rename from generated_tests/form_8.var_32.bits_32.cvc rename to tests/generated_tests/form_8.var_32.bits_32.cvc diff --git a/generated_tests/g.cvc b/tests/generated_tests/g.cvc similarity index 100% rename from generated_tests/g.cvc rename to tests/generated_tests/g.cvc diff --git a/generated_tests/gen2.cvc b/tests/generated_tests/gen2.cvc similarity index 100% rename from generated_tests/gen2.cvc rename to tests/generated_tests/gen2.cvc diff --git a/generated_tests/run-experiments.pl b/tests/generated_tests/run-experiments.pl similarity index 100% rename from generated_tests/run-experiments.pl rename to tests/generated_tests/run-experiments.pl diff --git a/generated_tests/testgen.pl b/tests/generated_tests/testgen.pl similarity index 100% rename from generated_tests/testgen.pl rename to tests/generated_tests/testgen.pl -- 2.47.3