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

diff --git a/scripts/Makefile.in b/scripts/Makefile.in
index 470b4678416834ddf9ef8d23fc6383a08b1ada0e..2344481b5a279848c23b1812cae9e9321b6d09bc 100644 (file)
--- 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 9f082c45295711903c87ad893ad9cbb195d05fd2..49e08dd126e35a3bb160e0130e1f3ba3a8604a35 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -12,7 +12,7 @@
 #include <assert.h>
 #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 (file)
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 (file)
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<ASTVec> & 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 8c0e2c292d0e2344977fa63153da0437a111d1ea..9b2215b5010bee0c47d60ed2d88416ee599361b0 100644 (file)
--- 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 <cassert>
-#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<ASTVec> & 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<ASTVec> & assertionsSMT2);
 
     void cleanUp()
     {

diff --git a/src/main/main.cpp b/src/main/main.cpp
index fe1c8c03e0b855e27ab936c44d10157b66bef488..25b49cb52483f90e182a1d5def79b6df294a5ec2 100644 (file)
--- 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 <sys/time.h>
 #include <memory>
 

diff --git a/src/parser/cvc.lex b/src/parser/cvc.lex
index cd08ab46097558c6ca653fbc2727eb34ee59d90c..a71325a896333abf48fca185b0ce32c278417108 100644 (file)
--- a/src/parser/cvc.lex
+++ b/src/parser/cvc.lex
@@ -10,7 +10,7 @@
 #include <iostream>
 #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 41a8ee1163349ee833a47cd247e894b87dc46ef2..eaff1168f15c7de4deeeef830514c102fae9bbc8 100644 (file)
--- 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 c2233326fa057f4180d4fc52ffd6e463953034db..a6e1c69173e71a3fc35006b64fd1bd57cd5b6f9f 100644 (file)
--- a/src/parser/smt.lex
+++ b/src/parser/smt.lex
@@ -36,7 +36,7 @@
 #include <iostream>
 #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 1e056dbc97aef55901da2feaf2841c45e8b9bfdc..2ac01e3adcbf6c87dc9b557d5bec0390e624cb5d 100644 (file)
--- 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 bafd7012b870b8db752eba4019c379e58538c994..2d64ff06e5d4938e11193674def0c2a769a15824 100644 (file)
--- 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 8c6f46590008bbefbfb1aeac6f04ae0b6d95b2fb..332fbb6cec2929ff6575bff3085ffe46b8eb22c1 100644 (file)
--- 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;