Exta utility code.

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

diff --git a/src/util/Functions.cpp b/src/util/Functions.cpp
new file mode 100644 (file)
index 0000000..c3cd3cf
--- /dev/null
+++ b/src/util/Functions.cpp
@@ -0,0 +1,44 @@
+#include "Functions.h"
+/*
+ * Functions.cpp
+ *
+ *  Created on: 11/04/2012
+ *      Author: thansen
+ */
+
+Result
+multiply(vector<FixedBits*>& children, FixedBits& output)
+{
+  return bvMultiplyBothWays(children, output, ParserBM, 0);
+}
+
+Result
+unsignedDivide(vector<FixedBits*>& children, FixedBits& output)
+{
+  return bvUnsignedDivisionBothWays(children, output, ParserBM);
+}
+
+
+Result
+signedDivide(vector<FixedBits*>& children, FixedBits& output)
+{
+  return bvSignedDivisionBothWays(children, output, ParserBM);
+}
+
+Result
+signedRemainder(vector<FixedBits*>& children, FixedBits& output)
+{
+  return bvSignedRemainderBothWays(children, output, ParserBM);
+}
+
+Result
+signedModulus(vector<FixedBits*>& children, FixedBits& output)
+{
+  return bvSignedModulusBothWays(children, output, ParserBM);
+}
+
+Result
+unsignedModulus(vector<FixedBits*>& children, FixedBits& output)
+{
+  return bvUnsignedModulusBothWays(children, output, ParserBM);
+}

diff --git a/src/util/Functions.h b/src/util/Functions.h
new file mode 100644 (file)
index 0000000..18ccefc
--- /dev/null
+++ b/src/util/Functions.h
@@ -0,0 +1,87 @@
+/*
+ * Functions.h
+ *
+ *  Created on: 11/04/2012
+ *      Author: thansen
+ */
+
+#ifndef FUNCTIONS_H_
+#define FUNCTIONS_H_
+
+#include "../simplifier/constantBitP/FixedBits.h"
+#include "../cpp_interface/cpp_interface.h"
+#include "../simplifier/constantBitP/ConstantBitP_TransferFunctions.h"
+#include "../simplifier/constantBitP/ConstantBitPropagation.h"
+#include <list>
+
+using simplifier::constantBitP::FixedBits;
+using namespace simplifier::constantBitP;
+
+using namespace BEEV;
+
+Result
+multiply(vector<FixedBits*>& children, FixedBits& output);
+
+
+Result
+unsignedDivide(vector<FixedBits*>& children, FixedBits& output);
+
+
+Result
+signedDivide(vector<FixedBits*>& children, FixedBits& output);
+
+
+Result
+signedRemainder(vector<FixedBits*>& children, FixedBits& output);
+
+Result
+signedModulus(vector<FixedBits*>& children, FixedBits& output);
+
+Result
+unsignedModulus(vector<FixedBits*>& children, FixedBits& output);
+
+
+
+struct Functions
+{
+  struct Function
+  {
+    Kind k;
+    string name;
+    Result (*fn)(vector<FixedBits*>&, FixedBits&);
+
+    Function (Kind k_, string name_, Result (*fn_)(vector<FixedBits*>&, FixedBits&) )
+    {
+      name = name_;
+      k = k_;
+      fn = fn_;
+    }
+  };
+
+  std::list<Function> l;
+
+
+  Functions()
+  {
+    l.push_back(Function(BVSGE, "signed greater than equals", &bvSignedGreaterThanEqualsBothWays));
+    l.push_back(Function(BVLT, "unsigned less than", &bvLessThanEqualsBothWays));
+    l.push_back(Function(EQ, "equals", &bvEqualsBothWays));
+    l.push_back(Function(BVXOR, "bit-vector xor", &bvXorBothWays));
+    l.push_back(Function(BVOR, "bit-vector or", &bvOrBothWays));
+    l.push_back(Function(BVAND, "bit-vector and", &bvAndBothWays));
+    l.push_back(Function(BVRIGHTSHIFT, "right shift", &bvRightShiftBothWays));
+    l.push_back(Function(BVLEFTSHIFT, "left shift", &bvLeftShiftBothWays));
+    l.push_back(Function(BVSRSHIFT, "arithmetic shift", &bvArithmeticRightShiftBothWays));
+    l.push_back(Function(BVPLUS, "addition", &bvAddBothWays));
+    l.push_back(Function(BVMULT, "multiplication", &multiply));
+    l.push_back(Function(BVDIV, "unsigned division", &unsignedDivide));
+    l.push_back(Function(BVMOD, "unsigned remainder", &unsignedModulus));
+    l.push_back(Function(SBVDIV, "signed division", &signedDivide));
+    l.push_back(Function(SBVREM, "signed remainder",&signedRemainder ));
+}
+
+
+
+};
+
+#endif /* FUNCTIONS_H_ */

diff --git a/src/util/Makefile b/src/util/Makefile
index bcbaaa71c196f334df0c7eb43ddb14f572c60745..3fb94ae6bd6be63cdac1be6044c1924064916c90 100644 (file)
--- 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 apply.cpp
+SRCS =  time_cbitp.cpp test_cbitp.cpp apply.cpp measure.cpp
 OBJS = $(SRCS:.cpp=.o)
 CXXFLAGS += -L../../lib/ 
 
 .PHONY: clean
 
+measure:  measure.o $(TOP)lib/libstp.a Makefile Functions.o
+       $(CXX) $(CXXFLAGS) Functions.o $@.o -o $@ -lstp
+
+
 apply:  $(OBJS)  $(TOP)lib/libstp.a 
        $(CXX) $(CXXFLAGS) $@.o -o $@ -lstp -static
 
@@ -20,4 +24,4 @@ test_cbitp: $(OBJS)  $(TOP)lib/libstp.a
 
 
 clean:
-       rm -f $(OBJS) rewrite time_cbitp test_cbitp
+       rm -f $(OBJS) rewrite time_cbitp test_cbitp measure

diff --git a/src/util/Relations.cpp b/src/util/Relations.cpp
deleted file mode 100644 (file)
index 6464497..0000000
--- a/src/util/Relations.cpp
+++ /dev/null
@@ -1,20 +0,0 @@
-/*
- * Relations.cpp
- *
- *  Created on: 10/04/2012
- *      Author: thansen
- */
-
-#include "Relations.h"
-
-Relations::Relations()
-{
-  // TODO Auto-generated constructor stub
-
-}
-
-Relations::~Relations()
-{
-  // TODO Auto-generated destructor stub
-}
-

diff --git a/src/util/StopWatch.h b/src/util/StopWatch.h
index f00a4b4cedd15a991f1bc55989e71b683da022a5..da0faa08be5eb01dbd8e66b706c0464581a16a65 100644 (file)
--- a/src/util/StopWatch.h
+++ b/src/util/StopWatch.h
@@ -33,4 +33,29 @@ private:
 };
 
 
+
+struct Stopwatch2
+{
+        Stopwatch2() :
+                elapsed(0), start_t(0)
+        {
+        }
+        void stop()
+        {
+                elapsed+= (clock() - start_t);
+                start_t =0;
+        }
+
+        void start()
+        {
+          assert(start_t ==0);
+          start_t =  clock();
+        }
+
+        std::clock_t elapsed;
+        std::clock_t start_t;
+};
+
+
+
 #endif /* STOPWATCH_H_ */

diff --git a/src/util/measure.cpp b/src/util/measure.cpp
new file mode 100644 (file)
index 0000000..d406520
--- /dev/null
+++ b/src/util/measure.cpp
@@ -0,0 +1,239 @@
+// Measures how precise the AIG encodings are compared with the propagators.
+
+#include "../cpp_interface/cpp_interface.h"
+#include "Relations.h"
+#include "../sat/MinisatCore.h"
+#include "../sat/core/Solver.h"
+#include "../to-sat/AIG/ToSATAIG.h"
+#include "Functions.h"
+#include "../printer/printers.h"
+#include "StopWatch.h"
+
+using namespace BEEV;
+
+int bits = 64;
+int iterations = 100000;
+ostream& out = cout;
+STPMgr *mgr = new STPMgr;
+
+void
+print(MinisatCore<Minisat::Solver> * ss, ASTNode i0, ToSAT::ASTNodeToSATVar& m)
+{
+  const int bits = std::max(1U, i0.GetValueWidth());
+  out << "<";
+  for (int i = bits - 1; i >= 0; i--)
+    {
+      if (ss->value(m.find(i0)->second[i]) == ss->true_literal())
+        {
+          out << "1";
+        }
+      else if (ss->value(m.find(i0)->second[i]) == ss->false_literal())
+        {
+          out << "0";
+        }
+      else
+        out << "-";
+    }
+  out << ">";
+}
+
+void
+addToClauseCount(MinisatCore<Minisat::Solver> * ss, ASTNode i0, ToSAT::ASTNodeToSATVar& m, int & count)
+{
+  const int bits = std::max(1U, i0.GetValueWidth());
+  for (int i = bits - 1; i >= 0; i--)
+    {
+      SATSolver::lbool r = ss->value(m.find(i0)->second[i]);
+
+      if (r == ss->true_literal() || r == ss->false_literal())
+        count++;
+    }
+}
+
+void
+go(Kind k, Result
+(*t_fn)(vector<FixedBits*>&, FixedBits&), int prob)
+{
+  const bool term = is_Term_kind(k);
+
+  ASTNode i0 = mgr->CreateSymbol("i0", 0, bits);
+  ASTNode i1 = mgr->CreateSymbol("i1", 0, bits);
+
+  ASTNode r, p, eq;
+
+  if (term)
+    {
+      p = mgr->CreateTerm(k, bits, i0, i1);
+      r = mgr->CreateSymbol("r", 0, bits);
+      eq = mgr->CreateNode(EQ, p, r);
+    }
+  else
+    {
+      p = mgr->CreateNode(k, i0, i1);
+      r = mgr->CreateSymbol("r", 0, 0);
+      eq = mgr->CreateNode(IFF, p, r);
+    }
+
+  Relations relations(iterations, bits, k, mgr, prob);
+
+  int initial = 0;
+  int transfer = 0;
+  int clause = 0;
+
+  MinisatCore<Minisat::Solver>* ss = new MinisatCore<Minisat::Solver>(mgr->soft_timeout_expired);
+  ToSATAIG a(mgr, GlobalSTP->arrayTransformer);
+  a.CallSAT(*ss, eq, false);
+  ToSAT::ASTNodeToSATVar m = a.SATVar_to_SymbolIndexMap();
+
+  Stopwatch2 bb;
+  Stopwatch2 prop;
+
+  list<Relations::Relation>::iterator it = relations.relations.begin();
+  while (it != relations.relations.end())
+    {
+      Relations::Relation rel = *it;
+
+      SATSolver::vec_literals assumptions;
+
+      for (int i = 0; i < bits; i++)
+        {
+          if (rel.a[i] == '1')
+            {
+              assumptions.push(SATSolver::mkLit(m.find(i0)->second[i], false));
+            }
+          else if (rel.a[i] == '0')
+            {
+              assumptions.push(SATSolver::mkLit(m.find(i0)->second[i], true));
+            }
+
+          if (rel.b[i] == '1')
+            {
+              assumptions.push(SATSolver::mkLit(m.find(i1)->second[i], false));
+            }
+          else if (rel.b[i] == '0')
+            {
+              assumptions.push(SATSolver::mkLit(m.find(i1)->second[i], true));
+            }
+        }
+      for (int i = 0; i < rel.output.getWidth(); i++)
+        {
+          if (rel.output[i] == '1')
+            {
+              assumptions.push(SATSolver::mkLit(m.find(r)->second[i], false));
+            }
+          else if (rel.output[i] == '0')
+            {
+              assumptions.push(SATSolver::mkLit(m.find(r)->second[i], true));
+            }
+        }
+
+      //Initial.
+      //cerr << rel.a << _kind_names[k] << rel.b << rel.output << endl;
+
+      const int initialCount = rel.a.countFixed() + rel.b.countFixed() + rel.output.countFixed();
+      initial += initialCount;
+
+      // simplify does propagate.
+      bb.start();
+      bool ok = ss->unitPropagate(assumptions);
+      bb.stop();
+      assert(ok);
+
+      // After unit propagation.
+      int clauseCount = 0;
+      addToClauseCount(ss, i0, a.SATVar_to_SymbolIndexMap(), clauseCount);
+      addToClauseCount(ss, i1, a.SATVar_to_SymbolIndexMap(), clauseCount);
+      addToClauseCount(ss, r, a.SATVar_to_SymbolIndexMap(), clauseCount);
+      clause += clauseCount;
+
+      // After unit propagation.
+      /*
+       print(ss, i0, a.SATVar_to_SymbolIndexMap());
+       cerr <<  _kind_names[k];
+       print(ss, i1, a.SATVar_to_SymbolIndexMap());
+       print(ss, r, a.SATVar_to_SymbolIndexMap());
+       cerr << "\n";
+       */
+
+      // After transfer functions.
+      vector<FixedBits*> ch;
+      ch.push_back(&rel.a);
+      ch.push_back(&rel.b);
+      prop.start();
+      Result rr = t_fn(ch, rel.output);
+      prop.stop();
+
+      assert(rr != CONFLICT);
+      //cerr << rel.a << _kind_names[k] << rel.b << rel.output << endl;
+      int transferCount = rel.a.countFixed() + rel.b.countFixed() + rel.output.countFixed();
+      transfer += transferCount;
+
+      //cerr << initialCount << endl;
+      // cerr << clauseCount << endl;
+      assert(initialCount <= clauseCount);
+      assert(initialCount <= transferCount);
+
+      //delete ss;
+      it++;
+    }
+
+  int percent = 100 * ((float)(clause - initial)) / ((float)(transfer - initial));
+  if (transfer - initial == 0)
+    percent = 100;
+
+  cerr.setf(ios::fixed);
+  cerr << "&" << setprecision(2) << (float(bb.elapsed) / CLOCKS_PER_SEC) << "s";
+
+  cerr.setf(ios::fixed);
+  cerr << "&" << setprecision(2) << (float(prop.elapsed) / CLOCKS_PER_SEC) << "s";
+
+  cerr << "&" << (clause-initial) << "&" << (transfer-initial) << "&" << percent << "\\%\\\\%prob:" << prob << endl;
+}
+
+void
+work(int p)
+{
+  out << "\\begin{table*}[t]" << endl;
+  //out << "\\small" << endl;
+  out << "\\begin{center}" << endl;
+  out << "\\begin{tabular}{|l| r|r|r|r|r|r|r| }" << endl;
+  out << "\\hline" << endl;
+  out << "\\multicolumn{1}{|c|}{Operation} &" << endl;
+  out << "\\multicolumn{5}{c|}{" << p << "\\%} \\\\" << endl;
+  out << "& UP time & prop. time &  UP bits & prop. bits &  \\% \\\\" << endl;
+  out << "\\hline" << endl;
+
+  Functions f;
+  std::list<Functions::Function>::iterator it = f.l.begin();
+  while (it != f.l.end())
+    {
+      Functions::Function& f = *it;
+      out << f.name << endl;
+      go(f.k, f.fn, p);
+      it++;
+    }
+
+  out << "\\hline" << endl;
+  out << "\\end{tabular}" << endl;
+  out << "\\caption{Comparison of unit propagation and bit-blasting at "<<  p <<  "\\%. ";
+  out << iterations << " iterations at " << bits << " bits.}" << endl;
+  out << "\\end{center}" << endl;
+  out << "\\end{table*}" << endl;
+
+}
+
+int
+main()
+{
+  mgr = new STPMgr;
+  Cpp_interface interface(*mgr);
+
+  work(1);
+  work(5);
+  work(50);
+  work(95);
+
+  cerr << "% Iterations:" << iterations << " bit-width:" << bits << endl;
+
+}
+