]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commitdiff
Extra cpp interface constructor
authortrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Fri, 20 Apr 2012 01:44:32 +0000 (01:44 +0000)
committertrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Fri, 20 Apr 2012 01:44:32 +0000 (01:44 +0000)
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1646 e59a4935-1847-0410-ae03-e826735625c1

src/cpp_interface/cpp_interface.cpp

index c96a8b20339d78e46bca96b5b3b751ffebbeeb07..4da368536851f969716b2c76205a1628759bce66 100644 (file)
@@ -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();
+  }
 }
 ;