This fixes things I broke in r662:

* Add ParserInterface.h which I missed.
* Revert back Makefile.common, which I didn't mean to change.
* Rename let-funcs in Makefile.in

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

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 72d186ea28c44f306e89fc2f1e382a06bc3ac810..e0b59f0b9ca649048b66ff2795e967cf9140bd34 100644 (file)
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -13,7 +13,7 @@
 #OPTIMIZE      = -O3 -fPIC         # Maximum optimization
 #OPTIMIZE      = -O3 -march=native -fomit-frame-pointer # Maximum optimization
 #OPTIMIZE      = -O3 -march=native -DNDEBUG -DLESSBYTES_PERNODE
-OPTIMIZE      = -O3 -g               # Maximum optimization
+OPTIMIZE      = -O3               # Maximum optimization
 #CFLAGS_M32   = -m32
 CFLAGS_BASE   = $(OPTIMIZE)
 

diff --git a/scripts/Makefile.in b/scripts/Makefile.in
index c810823edc5737e380a24dbf177e0fcdcd576401..840087250f36eb74a100963ee4fde2e2753f5616 100644 (file)
--- a/scripts/Makefile.in
+++ b/scripts/Makefile.in
@@ -50,7 +50,7 @@ endif
                           $(SRC)/extlib-constbv/*.o \
                           $(SRC)/extlib-abc/*/*/*.o \
                           $(SRC)/c_interface/*.o \
-                          $(SRC)/parser/let-funcs.o  \
+                          $(SRC)/parser/LetMgr.o  \
                           $(SRC)/parser/parseCVC.o  \
                           $(SRC)/parser/lexCVC.o \
                           $(SRC)/parser/parseSMT.o \

diff --git a/src/parser/ParserInterface.h b/src/parser/ParserInterface.h
new file mode 100644 (file)
index 0000000..500d8fe
--- /dev/null
+++ b/src/parser/ParserInterface.h
@@ -0,0 +1,91 @@
+// 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_
+
+#include "../AST/AST.h"
+#include "../AST/NodeFactory/NodeFactory.h"
+#include <cassert>
+#include "LetMgr.h"
+#include "../STPManager/STPManager.h"
+
+namespace BEEV
+{
+using BEEV::STPMgr;
+
+// There's no BVTypeCheck() function. Use a typechecking node factory instead.
+
+class ParserInterface
+{
+       STPMgr& bm;
+
+public:
+       LETMgr letMgr;
+       NodeFactory* nf;
+
+       ParserInterface(STPMgr &bm_, NodeFactory* factory)
+       : bm(bm_),
+         nf(factory),
+         letMgr(bm.ASTUndefined)
+       {
+               assert(nf != NULL);
+       }
+
+       const ASTVec GetAsserts(void)
+       {
+               return bm.GetAsserts();
+       }
+
+       void AddAssert(const ASTNode& assert)
+       {
+               bm.AddAssert(assert);
+       }
+
+    void AddQuery(const ASTNode& q)
+    {
+       bm.AddQuery(q);
+    }
+
+       //NODES//
+    ASTNode CreateNode(BEEV::Kind kind, const BEEV::ASTVec& children = _empty_ASTVec)
+    {
+        return nf->CreateNode(kind,children);
+    }
+
+    // These belong in the node factory..
+
+    //TERMS//
+    ASTNode CreateZeroConst(unsigned int width)
+    {
+       return bm.CreateZeroConst(width);
+    }
+
+    ASTNode CreateOneConst(unsigned int width)
+    {
+        return bm.CreateOneConst(width);
+    }
+
+    ASTNode CreateBVConst(string*& strval, int base, int bit_width)
+    {
+       return bm.CreateBVConst(strval, base, bit_width);
+    }
+
+    ASTNode CreateBVConst(const char* const strval, int base)
+    {
+       return bm.CreateBVConst(strval, base);
+    }
+
+    ASTNode CreateBVConst(unsigned int width, unsigned long long int bvconst)
+    {
+       return bm.CreateBVConst(width, bvconst);
+    }
+
+    ASTNode CreateSymbol(const char * const name)
+    {
+       return bm.CreateSymbol(name);
+    }
+};
+}
+
+#endif /* PARSERINTERFACE_H_ */