From: trevor_hansen Date: Fri, 20 Apr 2012 01:24:47 +0000 (+0000) Subject: Exta utility code. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=68b8ebfd60f202334e26b3dca49aad7dece0c1b8;p=francis%2Fstp.git 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 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& children, FixedBits& output) +{ + return bvMultiplyBothWays(children, output, ParserBM, 0); +} + +Result +unsignedDivide(vector& children, FixedBits& output) +{ + return bvUnsignedDivisionBothWays(children, output, ParserBM); +} + + +Result +signedDivide(vector& children, FixedBits& output) +{ + return bvSignedDivisionBothWays(children, output, ParserBM); +} + +Result +signedRemainder(vector& children, FixedBits& output) +{ + return bvSignedRemainderBothWays(children, output, ParserBM); +} + +Result +signedModulus(vector& children, FixedBits& output) +{ + return bvSignedModulusBothWays(children, output, ParserBM); +} + +Result +unsignedModulus(vector& children, FixedBits& output) +{ + return bvUnsignedModulusBothWays(children, output, ParserBM); +} diff --git a/src/util/Functions.h b/src/util/Functions.h new file mode 100644 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 + +using simplifier::constantBitP::FixedBits; +using namespace simplifier::constantBitP; + +using namespace BEEV; + +Result +multiply(vector& children, FixedBits& output); + + +Result +unsignedDivide(vector& children, FixedBits& output); + + +Result +signedDivide(vector& children, FixedBits& output); + + +Result +signedRemainder(vector& children, FixedBits& output); + +Result +signedModulus(vector& children, FixedBits& output); + +Result +unsignedModulus(vector& children, FixedBits& output); + + + +struct Functions +{ + struct Function + { + Kind k; + string name; + Result (*fn)(vector&, FixedBits&); + + Function (Kind k_, string name_, Result (*fn_)(vector&, FixedBits&) ) + { + name = name_; + k = k_; + fn = fn_; + } + }; + + std::list 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 bcbaaa7..3fb94ae 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 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 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 f00a4b4..da0faa0 100644 --- 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 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 * 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 * 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); + } + + Relations relations(iterations, bits, k, mgr, prob); + + int initial = 0; + int transfer = 0; + int clause = 0; + + MinisatCore* ss = new MinisatCore(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::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 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::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; + +} +