From 49197c68a01c5b67eb471c34bf4928ecd9247f33 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 23 Apr 2012 02:05:42 +0000 Subject: [PATCH] Improvements to code for running experiments. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1652 e59a4935-1847-0410-ae03-e826735625c1 --- src/util/BBAsProp.h | 117 +++++++++++++++++++++++++++++++++++++++++++ src/util/measure.cpp | 81 +++--------------------------- 2 files changed, 124 insertions(+), 74 deletions(-) create mode 100644 src/util/BBAsProp.h diff --git a/src/util/BBAsProp.h b/src/util/BBAsProp.h new file mode 100644 index 0000000..fa341bd --- /dev/null +++ b/src/util/BBAsProp.h @@ -0,0 +1,117 @@ +/* + * Use the Bitblasted encoding as a propagator. + */ + +#ifndef BBASPROP_H_ +#define BBASPROP_H_ + +class BBAsProp +{ +public: + + SATSolver::vec_literals assumptions; + ToSATAIG aig; + MinisatCore* ss; + ASTNode i0, i1,r; + ToSAT::ASTNodeToSATVar m; + + BBAsProp(Kind k, STPMgr* mgr, int bits): + aig(mgr, GlobalSTP->arrayTransformer) + { + + const bool term = is_Term_kind(k); + + i0 = mgr->CreateSymbol("i0", 0, bits); + i1 = mgr->CreateSymbol("i1", 0, bits); + + ASTNode 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); + } + + ss = new MinisatCore(mgr->soft_timeout_expired); + + aig.CallSAT(*ss, eq, false); + m = aig.SATVar_to_SymbolIndexMap(); + } + + bool + unitPropagate() + { + return ss->unitPropagate(assumptions); + } + + void + toAssumptions(FixedBits& a, FixedBits& b, FixedBits& output) + { + assumptions.clear(); + int bits = a.getWidth(); + + for (int i = 0; i < bits; i++) + { + if (a[i] == '1') + { + assumptions.push(SATSolver::mkLit(m.find(i0)->second[i], false)); + } + else if (a[i] == '0') + { + assumptions.push(SATSolver::mkLit(m.find(i0)->second[i], true)); + } + + if (b[i] == '1') + { + assumptions.push(SATSolver::mkLit(m.find(i1)->second[i], false)); + } + else if (b[i] == '0') + { + assumptions.push(SATSolver::mkLit(m.find(i1)->second[i], true)); + } + } + for (int i = 0; i < output.getWidth(); i++) + { + if (output[i] == '1') + { + assumptions.push(SATSolver::mkLit(m.find(r)->second[i], false)); + } + else if (output[i] == '0') + { + assumptions.push(SATSolver::mkLit(m.find(r)->second[i], true)); + } + } + } + + int + addToClauseCount() + { + return addToClauseCount(i0) +addToClauseCount(i1) + addToClauseCount(r); + } + + int + addToClauseCount( ASTNode n) + { + int result =0; + const int bits = std::max(1U, n.GetValueWidth()); + for (int i = bits - 1; i >= 0; i--) + { + SATSolver::lbool r = ss->value(m.find(n)->second[i]); + + if (r == ss->true_literal() || r == ss->false_literal()) + result++; + } + return result; + } + + +}; + +#endif /* BBASPROP_H_ */ diff --git a/src/util/measure.cpp b/src/util/measure.cpp index 1d4da9e..f1f048f 100644 --- a/src/util/measure.cpp +++ b/src/util/measure.cpp @@ -8,6 +8,7 @@ #include "Functions.h" #include "../printer/printers.h" #include "StopWatch.h" +#include "BBAsProp.h" using namespace BEEV; @@ -37,42 +38,12 @@ print(MinisatCore * ss, ASTNode i0, ToSAT::ASTNodeToSATVar& m) out << ">"; } -void -addToClauseCount(MinisatCore * 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&), 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); - } + BBAsProp bbP(k,mgr,bits); Relations relations(iterations, bits, k, mgr, prob); @@ -80,55 +51,18 @@ go(Kind k, Result int transfer = 0; int clause = 0; - MinisatCore* ss = new MinisatCore(mgr->soft_timeout_expired); - ToSATAIG aig(mgr, GlobalSTP->arrayTransformer); - aig.CallSAT(*ss, eq, false); - ToSAT::ASTNodeToSATVar m = aig.SATVar_to_SymbolIndexMap(); - Stopwatch2 bb; Stopwatch2 prop; list::iterator it = relations.relations.begin(); while (it != relations.relations.end()) { - //Relations::Relation rel = FixedBits& a = it->a; FixedBits& b = it->b; FixedBits& output = it->output; - SATSolver::vec_literals assumptions; + bbP.toAssumptions(a,b,output); - for (int i = 0; i < bits; i++) - { - if (a[i] == '1') - { - assumptions.push(SATSolver::mkLit(m.find(i0)->second[i], false)); - } - else if (a[i] == '0') - { - assumptions.push(SATSolver::mkLit(m.find(i0)->second[i], true)); - } - - if (b[i] == '1') - { - assumptions.push(SATSolver::mkLit(m.find(i1)->second[i], false)); - } - else if (b[i] == '0') - { - assumptions.push(SATSolver::mkLit(m.find(i1)->second[i], true)); - } - } - for (int i = 0; i < output.getWidth(); i++) - { - if (output[i] == '1') - { - assumptions.push(SATSolver::mkLit(m.find(r)->second[i], false)); - } - else if (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; @@ -138,15 +72,14 @@ go(Kind k, Result // simplify does propagate. bb.start(); - bool ok = ss->unitPropagate(assumptions); + bool ok = bbP.unitPropagate(); bb.stop(); assert(ok); // After unit propagation. int clauseCount = 0; - addToClauseCount(ss, i0, aig.SATVar_to_SymbolIndexMap(), clauseCount); - addToClauseCount(ss, i1, aig.SATVar_to_SymbolIndexMap(), clauseCount); - addToClauseCount(ss, r, aig.SATVar_to_SymbolIndexMap(), clauseCount); + clauseCount = bbP.addToClauseCount(); + clause += clauseCount; // After unit propagation. @@ -218,7 +151,7 @@ work(int p) out << "\\hline" << endl; out << "\\end{tabular}" << endl; out << "\\caption{Comparison of unit propagation and bit-blasting at "<< p << "\\%. "; - out << iterations << " iterations at " << bits << " bits. \label{tbl:p"<< p << "}}}" << endl; + out << iterations << " iterations at " << bits << " bits. \\label{tbl:p"<< p << "}}}" << endl; out << "\\end{center}" << endl; out << "\\end{table}" << endl; } -- 2.47.3