From b2db63e779aa10e1c1388301ac9448251e08a828 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 5 Apr 2010 12:00:26 +0000
Subject: [PATCH] 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
---
 scripts/Makefile.common      |  2 +-
 scripts/Makefile.in          |  2 +-
 src/parser/ParserInterface.h | 91 ++++++++++++++++++++++++++++++++++++
 3 files changed, 93 insertions(+), 2 deletions(-)
 create mode 100644 src/parser/ParserInterface.h

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 72d186e..e0b59f0 100644
--- 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 c810823..8400872 100644
--- 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
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_ */
-- 
2.47.3