From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 20 Apr 2012 01:44:32 +0000 (+0000)
Subject: Extra cpp interface constructor
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=32d29c54fe471a9ebde1a911c76fc1c4b116118f;p=francis%2Fstp.git

Extra cpp interface constructor

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

diff --git a/src/cpp_interface/cpp_interface.cpp b/src/cpp_interface/cpp_interface.cpp
index c96a8b2..4da3685 100644
--- a/src/cpp_interface/cpp_interface.cpp
+++ b/src/cpp_interface/cpp_interface.cpp
@@ -1,4 +1,5 @@
 #include "cpp_interface.h"
+#include "../to-sat/AIG/ToSATAIG.h"
 
 namespace BEEV
 {
@@ -62,5 +63,24 @@ namespace BEEV
     (GlobalSTP->tosat)->PrintOutput(last_run.result);
     bm.GetRunTimes()->start(RunTimes::Parsing);
   }
+
+  // This method sets up some of the globally required data.
+  Cpp_interface::Cpp_interface(STPMgr &bm_) :
+      bm(bm_), nf(bm_.defaultNodeFactory), letMgr(bm.ASTUndefined)
+  {
+    nf = bm.defaultNodeFactory;
+    startup();
+    BEEV::parserInterface = this;
+
+    Simplifier *simp = new Simplifier(&bm);
+    ArrayTransformer * at = new ArrayTransformer(&bm, simp);
+    AbsRefine_CounterExample* abs = new AbsRefine_CounterExample(&bm, simp, at);
+    ToSATAIG* tosat = new ToSATAIG(&bm, at);
+
+    BEEV::ParserBM = &bm_;
+
+    GlobalSTP = new STP(&bm, simp, at, tosat, abs);
+    init();
+  }
 }
 ;