Refactor. Rename parserinterface to cpp_interface.

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

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 49e08dd126e35a3bb160e0130e1f3ba3a8604a35..165c8d9d3dc23c9602e3c28134c26a76a66f9e52 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -1549,7 +1549,7 @@ Expr vc_parseExpr(VC vc, const char* infile) {
     return 0;
   }
 
-  BEEV::ParserInterface pi(*b, b->defaultNodeFactory);
+  BEEV::Cpp_interface pi(*b, b->defaultNodeFactory);
   BEEV::parserInterface = π
 
 
@@ -1787,7 +1787,7 @@ int vc_parseMemExpr(VC vc, const char* s, Expr* oquery, Expr* oasserts ) {
   }
 #endif
   
-  BEEV::ParserInterface pi(*b, b->defaultNodeFactory);
+  BEEV::Cpp_interface pi(*b, b->defaultNodeFactory);
   BEEV::parserInterface = π
 
   BEEV::ASTVec AssertsQuery;

diff --git a/src/cpp_interface/cpp_interface.cpp b/src/cpp_interface/cpp_interface.cpp
index 67b2486b6b4bee942e2b417bd38825f6c546fdef..f1ebb5095d38ea0cf89cad90ed133640ea51218f 100644 (file)
--- a/src/cpp_interface/cpp_interface.cpp
+++ b/src/cpp_interface/cpp_interface.cpp
@@ -6,7 +6,7 @@ namespace BEEV
 
 // Does some simple caching of prior results.
     void
-    ParserInterface::checkSat(vector<ASTVec> & assertionsSMT2)
+    Cpp_interface::checkSat(vector<ASTVec> & assertionsSMT2)
     {
       bm.GetRunTimes()->stop(RunTimes::Parsing);
       assert(assertionsSMT2.size() == cache.size());

diff --git a/src/cpp_interface/cpp_interface.h b/src/cpp_interface/cpp_interface.h
index 9b2215b5010bee0c47d60ed2d88416ee599361b0..f1b80d8b2a5e202dcfd11219cfdff769260b2e9b 100644 (file)
--- a/src/cpp_interface/cpp_interface.h
+++ b/src/cpp_interface/cpp_interface.h
@@ -1,8 +1,6 @@
-// Wrapper around the main beevmgr class given to the parsers.
-// Over time I hope the parsers will interact entirely through this class.
 
-#ifndef PARSERINTERFACE_H_
-#define PARSERINTERFACE_H_
+#ifndef CPP_INTERFACE_H_
+#define CPP_INTERFACE_H_
 
 #include "../AST/AST.h"
 #include "../AST/NodeFactory/NodeFactory.h"
@@ -19,7 +17,7 @@ using BEEV::STPMgr;
 
 // There's no BVTypeCheck() function. Use a typechecking node factory instead.
 
-class ParserInterface
+class Cpp_interface
 {
        STPMgr& bm;
        //boost::object_pool<ASTNode> node_pool;
@@ -29,7 +27,7 @@ public:
        LETMgr letMgr;
        NodeFactory* nf;
 
-       ParserInterface(STPMgr &bm_, NodeFactory* factory)
+       Cpp_interface(STPMgr &bm_, NodeFactory* factory)
        : bm(bm_),
          nf(factory),
          letMgr(bm.ASTUndefined)

diff --git a/src/main/Globals.cpp b/src/main/Globals.cpp
index 57d8c882e7a7f45365e484ef9cfc1970dfcac70d..0b981ea954b435176889cb8230c0896f12062bdd 100644 (file)
--- a/src/main/Globals.cpp
+++ b/src/main/Globals.cpp
@@ -20,7 +20,7 @@ namespace BEEV
   STPMgr  * ParserBM;
 
   // Used exclusively for parsing.
-  ParserInterface * parserInterface;
+  Cpp_interface * parserInterface;
 
   void (*vc_error_hdlr)(const char* err_msg) = NULL;
 

diff --git a/src/main/Globals.h b/src/main/Globals.h
index da81672c52c1808f7fefe773c26dc3ea351012f9..efc3143f435d81e25a56b6317cb98cefff7be734 100644 (file)
--- a/src/main/Globals.h
+++ b/src/main/Globals.h
@@ -30,7 +30,7 @@ namespace BEEV
   class ASTBVConst;
   class BVSolver;
   class STP;
-  class ParserInterface;
+  class Cpp_interface;
 
   /***************************************************************
    * ENUM TYPES
@@ -71,7 +71,7 @@ namespace BEEV
   //Useful global variables. Use for parsing only
   extern  STP * GlobalSTP;
   extern  STPMgr * ParserBM;
-  extern ParserInterface * parserInterface;
+  extern Cpp_interface * parserInterface;
 
   //Some constant global vars for the Main function. Once they are
   //set, these globals will remain constants. These vars are not used

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 25b49cb52483f90e182a1d5def79b6df294a5ec2..f043fe50519fad7d77c4a606cf9c9d8ea45019ad 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -422,8 +422,8 @@ int main(int argc, char ** argv) {
                TypeChecker nfTypeCheckSimp(simpNF, *bm);
                TypeChecker nfTypeCheckDefault(*bm->defaultNodeFactory, *bm);
 
-               ParserInterface piTypeCheckSimp(*bm, &nfTypeCheckSimp);
-               ParserInterface piTypeCheckDefault(*bm, &nfTypeCheckDefault);
+               Cpp_interface piTypeCheckSimp(*bm, &nfTypeCheckSimp);
+               Cpp_interface piTypeCheckDefault(*bm, &nfTypeCheckDefault);
 
                // If you are converting formats, you probably don't want it simplifying (at least I dont).
                if (onePrintBack)