From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 7 Apr 2012 00:21:57 +0000 (+0000)
Subject: Adds a utility to parse smt-lib2, constant bit propagate, then output the result.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=51ce7bf0e190e00b0dba1aca7de9ddfcdd7c7dd0;p=francis%2Fstp.git

Adds a utility to parse smt-lib2, constant bit propagate, then output the result.

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

diff --git a/src/util/Makefile b/src/util/Makefile
index 1aa5979..bcbaaa7 100644
--- a/src/util/Makefile
+++ b/src/util/Makefile
@@ -1,12 +1,16 @@
 TOP = ../../
 include $(TOP)scripts/Makefile.common
 
-SRCS =  time_cbitp.cpp test_cbitp.cpp
+SRCS =  time_cbitp.cpp test_cbitp.cpp apply.cpp
 OBJS = $(SRCS:.cpp=.o)
 CXXFLAGS += -L../../lib/ 
 
 .PHONY: clean
 
+apply:  $(OBJS)  $(TOP)lib/libstp.a 
+	$(CXX) $(CXXFLAGS) $@.o -o $@ -lstp -static
+
+
 time_cbitp: $(OBJS)  $(TOP)lib/libstp.a 
 	$(CXX) $(CXXFLAGS) $@.o -o $@ -lstp 
 
diff --git a/src/util/apply.cpp b/src/util/apply.cpp
new file mode 100644
index 0000000..142afe1
--- /dev/null
+++ b/src/util/apply.cpp
@@ -0,0 +1,88 @@
+// Parses, runs constant bit propagation, then outputs the result.
+
+#include "../simplifier/constantBitP/ConstantBitPropagation.h"
+#include "../AST/AST.h"
+#include "../printer/printers.h"
+
+#include "../STPManager/STPManager.h"
+#include "../to-sat/AIG/ToSATAIG.h"
+#include "../sat/MinisatCore.h"
+#include "../STPManager/STP.h"
+#include "../cpp_interface/cpp_interface.h"
+
+using namespace simplifier::constantBitP;
+
+int
+main(int argc, char ** argv)
+{
+  extern int
+  smt2parse();
+  extern int
+  smt2lex_destroy(void);
+  extern FILE *smt2in;
+
+  BEEV::STPMgr stp;
+  STPMgr * mgr = &stp;
+
+  Cpp_interface interface(*mgr, mgr->defaultNodeFactory);
+  interface.startup();
+  interface.ignoreCheckSat();
+  BEEV::parserInterface = &interface;
+
+  Simplifier *simp = new Simplifier(mgr);
+  ArrayTransformer * at = new ArrayTransformer(mgr, simp);
+  AbsRefine_CounterExample* abs = new AbsRefine_CounterExample(mgr, simp, at);
+  ToSATAIG* tosat = new ToSATAIG(mgr);
+  tosat->setArrayTransformer(at);
+
+  GlobalSTP = new STP(mgr, simp, at, tosat, abs);
+
+  srand(time(NULL));
+  BEEV::ParserBM = &stp;
+
+  stp.UserFlags.disableSimplifications();
+  stp.UserFlags.bitConstantProp_flag = true;
+
+  // Parse SMTLIB2-----------------------------------------
+  mgr->GetRunTimes()->start(RunTimes::Parsing);
+  if (argc > 1)
+    {
+    smt2in = fopen(argv[1], "r");
+    smt2parse();
+    }
+  else
+    {
+    smt2in = NULL; // from stdin.
+    smt2parse();
+    }
+  smt2lex_destroy();
+  //-----------------------------------------------------
+
+  ASTNode n;
+
+  ASTVec v = interface.GetAsserts();
+  if (v.size() > 1)
+    n = interface.CreateNode(AND, v);
+  else
+    n = v[0];
+
+  // Apply cbitp ----------------------------------------
+  simplifier::constantBitP::ConstantBitPropagation cb(simp, mgr->defaultNodeFactory, n);
+  if (cb.isUnsatisfiable())
+    n = mgr->ASTFalse;
+  else
+    n = cb.topLevelBothWays(n, true, true);
+
+  if (simp->hasUnappliedSubstitutions())
+    {
+    n = simp->applySubstitutionMap(n);
+    simp->haveAppliedSubstitutionMap();
+    }
+
+  // Print back out.
+  printer::SMTLIB2_PrintBack(cout, n);
+  cout << "(check-sat)\n";
+  cout << "(exit)\n";
+  return 0;
+}
+