From c6ce9180c6a545f02329ce35f533cfd1784f120a Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Tue, 24 Jan 2012 00:38:46 +0000 Subject: [PATCH] Refactor. First step in moving the parser interface to be the cpp interface. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1516 e59a4935-1847-0410-ae03-e826735625c1 --- scripts/Makefile.in | 3 + src/c_interface/c_interface.cpp | 2 +- src/cpp_interface/Makefile | 20 ++++ src/cpp_interface/cpp_interface.cpp | 92 +++++++++++++++++++ .../cpp_interface.h} | 87 +----------------- src/main/main.cpp | 2 +- src/parser/cvc.lex | 2 +- src/parser/cvc.y | 2 +- src/parser/smt.lex | 2 +- src/parser/smt.y | 2 +- src/parser/smt2.lex | 2 +- src/parser/smt2.y | 2 +- 12 files changed, 125 insertions(+), 93 deletions(-) create mode 100644 src/cpp_interface/Makefile create mode 100644 src/cpp_interface/cpp_interface.cpp rename src/{parser/ParserInterface.h => cpp_interface/cpp_interface.h} (67%) diff --git a/scripts/Makefile.in b/scripts/Makefile.in index 470b467..2344481 100644 --- a/scripts/Makefile.in +++ b/scripts/Makefile.in @@ -38,6 +38,7 @@ lib/libstp.a: $(addprefix $(SRC)/, \ absrefine_counterexample/libabstractionrefinement.a \ to-sat/libtosat.a sat/libminisat.a simplifier/libsimplifier.a \ extlib-constbv/libconstantbv.a extlib-abc/libabc.a \ + cpp_interface/libcppinterface.a \ c_interface/libcinterface.a parser/libparser.a main/libmain.a) mkdir -p $(@D) $(RM) $@ @@ -49,6 +50,7 @@ $(addprefix $(SRC)/, \ STPManager/libstpmgr.a printer/libprinter.a \ absrefine_counterexample/libabstractionrefinement.a \ to-sat/libtosat.a simplifier/libsimplifier.a c_interface/libcinterface.a \ + cpp_interface/libcppinterface.a \ extlib-constbv/libconstantbv.a extlib-abc/libabc.a parser/libparser.a \ main/libmain.a main/main.o): $(SRC)/AST/libast.a @@ -93,6 +95,7 @@ clean: $(MAKE) clean -C $(SRC)/to-sat $(MAKE) clean -C $(SRC)/sat $(MAKE) clean -C $(SRC)/c_interface + $(MAKE) clean -C $(SRC)/cpp_interface $(MAKE) clean -C $(SRC)/parser $(MAKE) clean -C $(SRC)/main $(MAKE) clean -C tests/c-api-tests diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index 9f082c4..49e08dd 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -12,7 +12,7 @@ #include #include "fdstream.h" #include "../printer/printers.h" -#include "../parser/ParserInterface.h" +#include "../cpp_interface/cpp_interface.h" //These typedefs lower the effort of using the keyboard to type (too //many overloaded meanings of the word type) diff --git a/src/cpp_interface/Makefile b/src/cpp_interface/Makefile new file mode 100644 index 0000000..dabc3fc --- /dev/null +++ b/src/cpp_interface/Makefile @@ -0,0 +1,20 @@ +TOP = ../.. +include $(TOP)/scripts/Makefile.common + +SRCS = $(wildcard *.cpp) +OBJS = $(SRCS:.cpp=.o) + + +libcppinterface.a: $(OBJS) + $(RM) $@ + $(AR) qcs $@ $^ + +.PHONY: clean +clean: + $(RM) *.o *~ *.a .#* depend + +depend: $(SRCS) + @$(call makedepend,$@,$(SRCS)) + +-include depend + diff --git a/src/cpp_interface/cpp_interface.cpp b/src/cpp_interface/cpp_interface.cpp new file mode 100644 index 0000000..67b2486 --- /dev/null +++ b/src/cpp_interface/cpp_interface.cpp @@ -0,0 +1,92 @@ +#include "cpp_interface.h" + +namespace BEEV +{ + + +// Does some simple caching of prior results. + void + ParserInterface::checkSat(vector & assertionsSMT2) + { + bm.GetRunTimes()->stop(RunTimes::Parsing); + assert(assertionsSMT2.size() == cache.size()); + + Entry& cacheEntry = cache.back(); + + //cerr << "------------" << endl; + //printStatus(); + + if ((cacheEntry.result == SOLVER_SATISFIABLE || cacheEntry.result == SOLVER_UNSATISFIABLE) + && (assertionsSMT2.back().size() ==1 && assertionsSMT2.back()[0] == cacheEntry.node)) + { // If we already know the answer then return. + if (bm.UserFlags.quick_statistics_flag) + { + bm.GetRunTimes()->print(); + } + + (GlobalSTP->tosat)->PrintOutput(cache.back().result); + bm.GetRunTimes()->start(RunTimes::Parsing); + return; + } + + bm.ClearAllTables(); + GlobalSTP->ClearAllTables(); + + // Loop through the set of assertions converting them to single nodes.. + ASTVec v; + for (int i = 0; i < assertionsSMT2.size(); i++) + { + if (assertionsSMT2[i].size() == 1) + {} + else if (assertionsSMT2[i].size() == 0) + assertionsSMT2[i].push_back(bm.ASTTrue); + else + { + ASTNode v = parserInterface->CreateNode(AND, assertionsSMT2[i]); + assertionsSMT2[i].clear(); + assertionsSMT2[i].push_back(v); + } + assert(assertionsSMT2[i].size() ==1); + v.push_back(assertionsSMT2[i][0]); + } + + ASTNode query; + + if (v.size() > 1) + query = parserInterface->CreateNode(AND, v); + else if (v.size() > 0) + query = v[0]; + else + query = bm.ASTTrue; + + SOLVER_RETURN_TYPE last_result = GlobalSTP->TopLevelSTP(query, bm.ASTFalse); + + // Write in the answer to the current slot. + if (last_result ==SOLVER_SATISFIABLE || last_result ==SOLVER_UNSATISFIABLE) + { + Entry e(last_result); + e.node = assertionsSMT2.back()[0]; + cacheEntry = e; + assert (!cacheEntry.node.IsNull()); + } + + // It's satisfiable, so everything beneath it is satisfiable too. + if (last_result ==SOLVER_SATISFIABLE) + { + for (int i=0; i < cache.size(); i++) + { + assert(cache[i].result != SOLVER_UNSATISFIABLE); + cache[i].result = SOLVER_SATISFIABLE; + } + } + + if (bm.UserFlags.quick_statistics_flag) + { + bm.GetRunTimes()->print(); + } + + (GlobalSTP->tosat)->PrintOutput(last_result); + //printStatus(); + bm.GetRunTimes()->start(RunTimes::Parsing); + } +}; diff --git a/src/parser/ParserInterface.h b/src/cpp_interface/cpp_interface.h similarity index 67% rename from src/parser/ParserInterface.h rename to src/cpp_interface/cpp_interface.h index 8c0e2c2..9b2215b 100644 --- a/src/parser/ParserInterface.h +++ b/src/cpp_interface/cpp_interface.h @@ -7,7 +7,7 @@ #include "../AST/AST.h" #include "../AST/NodeFactory/NodeFactory.h" #include -#include "LetMgr.h" +#include "../parser/LetMgr.h" #include "../STPManager/STPManager.h" #include "../STPManager/STP.h" //#include "../boost/pool/object_pool.hpp" @@ -241,91 +241,8 @@ public: cerr<< endl; } - // Does some simple caching of prior results. void - checkSat(vector & assertionsSMT2) - { - bm.GetRunTimes()->stop(RunTimes::Parsing); - assert(assertionsSMT2.size() == cache.size()); - - Entry& cacheEntry = cache.back(); - - //cerr << "------------" << endl; - //printStatus(); - - if ((cacheEntry.result == SOLVER_SATISFIABLE || cacheEntry.result == SOLVER_UNSATISFIABLE) - && (assertionsSMT2.back().size() ==1 && assertionsSMT2.back()[0] == cacheEntry.node)) - { // If we already know the answer then return. - if (bm.UserFlags.quick_statistics_flag) - { - bm.GetRunTimes()->print(); - } - - (GlobalSTP->tosat)->PrintOutput(cache.back().result); - bm.GetRunTimes()->start(RunTimes::Parsing); - return; - } - - bm.ClearAllTables(); - GlobalSTP->ClearAllTables(); - - // Loop through the set of assertions converting them to single nodes.. - ASTVec v; - for (int i = 0; i < assertionsSMT2.size(); i++) - { - if (assertionsSMT2[i].size() == 1) - {} - else if (assertionsSMT2[i].size() == 0) - assertionsSMT2[i].push_back(bm.ASTTrue); - else - { - ASTNode v = parserInterface->CreateNode(AND, assertionsSMT2[i]); - assertionsSMT2[i].clear(); - assertionsSMT2[i].push_back(v); - } - assert(assertionsSMT2[i].size() ==1); - v.push_back(assertionsSMT2[i][0]); - } - - ASTNode query; - - if (v.size() > 1) - query = parserInterface->CreateNode(AND, v); - else if (v.size() > 0) - query = v[0]; - else - query = bm.ASTTrue; - - SOLVER_RETURN_TYPE last_result = GlobalSTP->TopLevelSTP(query, bm.ASTFalse); - - // Write in the answer to the current slot. - if (last_result ==SOLVER_SATISFIABLE || last_result ==SOLVER_UNSATISFIABLE) - { - Entry e(last_result); - e.node = assertionsSMT2.back()[0]; - cacheEntry = e; - assert (!cacheEntry.node.IsNull()); - } - - // It's satisfiable, so everything beneath it is satisfiable too. - if (last_result ==SOLVER_SATISFIABLE) - { - for (int i=0; i < cache.size(); i++) - { - assert(cache[i].result != SOLVER_UNSATISFIABLE); - cache[i].result = SOLVER_SATISFIABLE; - } - } - - if (bm.UserFlags.quick_statistics_flag) - { - bm.GetRunTimes()->print(); - } - - (GlobalSTP->tosat)->PrintOutput(last_result); - //printStatus(); - bm.GetRunTimes()->start(RunTimes::Parsing); - } + checkSat(vector & assertionsSMT2); void cleanUp() { diff --git a/src/main/main.cpp b/src/main/main.cpp index fe1c8c0..25b49cb 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -14,7 +14,7 @@ #include "../STPManager/STP.h" #include "../AST/NodeFactory/TypeChecker.h" #include "../AST/NodeFactory/SimplifyingNodeFactory.h" -#include "../parser/ParserInterface.h" +#include "../cpp_interface/cpp_interface.h" #include #include diff --git a/src/parser/cvc.lex b/src/parser/cvc.lex index cd08ab4..a71325a 100644 --- a/src/parser/cvc.lex +++ b/src/parser/cvc.lex @@ -10,7 +10,7 @@ #include #include "parser.h" #include "parsecvc.hpp" -#include "ParserInterface.h" +#include "../cpp_interface/cpp_interface.h" using namespace std; using namespace BEEV; diff --git a/src/parser/cvc.y b/src/parser/cvc.y index 41a8ee1..eaff116 100644 --- a/src/parser/cvc.y +++ b/src/parser/cvc.y @@ -9,7 +9,7 @@ ********************************************************************/ #include "parser.h" -#include "ParserInterface.h" +#include "../cpp_interface/cpp_interface.h" using namespace std; using namespace BEEV; diff --git a/src/parser/smt.lex b/src/parser/smt.lex index c223332..a6e1c69 100644 --- a/src/parser/smt.lex +++ b/src/parser/smt.lex @@ -36,7 +36,7 @@ #include #include "parser.h" #include "parsesmt.hpp" -#include "ParserInterface.h" +#include "../cpp_interface/cpp_interface.h" using namespace std; using namespace BEEV; diff --git a/src/parser/smt.y b/src/parser/smt.y index 1e056db..2ac01e3 100644 --- a/src/parser/smt.y +++ b/src/parser/smt.y @@ -35,7 +35,7 @@ ********************************************************************/ // -*- c++ -*- -#include "ParserInterface.h" +#include "../cpp_interface/cpp_interface.h" using namespace std; using namespace BEEV; diff --git a/src/parser/smt2.lex b/src/parser/smt2.lex index bafd701..2d64ff0 100644 --- a/src/parser/smt2.lex +++ b/src/parser/smt2.lex @@ -44,7 +44,7 @@ // -*- c++ -*-L #include "parser.h" #include "parsesmt2.hpp" -#include "ParserInterface.h" +#include "../cpp_interface/cpp_interface.h" extern char *smt2text; extern int smt2error (const char *msg); diff --git a/src/parser/smt2.y b/src/parser/smt2.y index 8c6f465..332fbb6 100644 --- a/src/parser/smt2.y +++ b/src/parser/smt2.y @@ -45,7 +45,7 @@ ********************************************************************/ // -*- c++ -*- -#include "ParserInterface.h" +#include "../cpp_interface/cpp_interface.h" using namespace std; using namespace BEEV; -- 2.47.3