From 519bfda9c001d90bf32fb68101532b6f3a0f69ba Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sat, 31 Dec 2011 14:51:52 +0000 Subject: [PATCH] Improvement. Bitblasting variants can not be set from the command line. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1457 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/AIGSimplifyPropositionalCore.h | 2 +- src/to-sat/AIG/ToSATAIG.cpp | 2 +- src/to-sat/BitBlaster.cpp | 69 ++++++------------- src/to-sat/BitBlaster.h | 33 +++++---- 4 files changed, 43 insertions(+), 63 deletions(-) diff --git a/src/simplifier/AIGSimplifyPropositionalCore.h b/src/simplifier/AIGSimplifyPropositionalCore.h index 2fead48..4af2f86 100644 --- a/src/simplifier/AIGSimplifyPropositionalCore.h +++ b/src/simplifier/AIGSimplifyPropositionalCore.h @@ -126,7 +126,7 @@ public: Simplifier simplifier(bm); BBNodeManagerAIG mgr; - BitBlaster bb(&mgr,NULL, &simplifier, bm->defaultNodeFactory,&bm->UserFlags); + BitBlaster bb(&mgr, &simplifier, bm->defaultNodeFactory,&bm->UserFlags); BBNodeAIG blasted = bb.BBForm(replaced); Aig_ObjCreatePo(mgr.aigMgr, blasted.n); diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp index 9d9c721..550163a 100644 --- a/src/to-sat/AIG/ToSATAIG.cpp +++ b/src/to-sat/AIG/ToSATAIG.cpp @@ -36,7 +36,7 @@ namespace BEEV Simplifier simp(bm); BBNodeManagerAIG mgr; - BitBlaster bb(&mgr,cb,&simp,bm->defaultNodeFactory,&bm->UserFlags); + BitBlaster bb(&mgr,&simp,bm->defaultNodeFactory,&bm->UserFlags,cb); bm->GetRunTimes()->start(RunTimes::BitBlasting); BBNodeAIG BBFormula = bb.BBForm(input); diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp index 58584ba..0932f19 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -1140,7 +1140,7 @@ const bool debug_multiply = false; * adder_variant1 = true. Solving:115s, 103s, 303s * adder_variant1 = false. Solving:181s, 471s, 215s * */ -bool const adder_variant1 = true; + template BBNodeVec BitBlaster::buildAdditionNetworkResult(stack* products, set& support, @@ -1183,7 +1183,7 @@ void BitBlaster::buildAdditionNetworkResult(stack BBNode carry, sum; - if (adder_variant1) + if (adder_variant) { carry = Majority(a, b, c); sum = nf->CreateNode(XOR, a, b, c); @@ -1607,27 +1607,25 @@ BBNodeVec BitBlaster::BBMult(const BBNodeVec& _x, const B y = _x; } - string mv = uf->get("multiplication_variant","3"); - const int bitWidth = x.size(); std::vector > products(bitWidth); - if (mv == "1") { + if (multiplication_variant == "1") { //cerr << "v1"; return mult_normal(x, y, support); } - else if (mv == "2") { + else if (multiplication_variant == "2") { //cout << "v2"; mult_allPairs(x, y, support,products.data()); return buildAdditionNetworkResult(products.data(),support, bitWidth); } - else if (mv == "3") { + else if (multiplication_variant == "3") { //cout << "v3" << endl; mult_Booth(_x, _y, support,n[0],n[1],products.data()); return buildAdditionNetworkResult(products.data(),support,bitWidth); } - else if (mv == "4") + else if (multiplication_variant == "4") { //cerr << "v4"; mult_Booth(_x, _y, support,n[0],n[1],products.data()); @@ -1642,7 +1640,7 @@ BBNodeVec BitBlaster::BBMult(const BBNodeVec& _x, const B } return buildAdditionNetworkResult(products.data(),support, bitWidth); } - else if (mv == "5") + else if (multiplication_variant == "5") { //cout << "v5"; if (!statsFound(n)) @@ -1658,35 +1656,18 @@ BBNodeVec BitBlaster::BBMult(const BBNodeVec& _x, const B FatalError("sda44f"); } -//====== -// on factoring12bitsx12.cvc with CMS2. -// variant1 = t, variant2 = t, variant3 = f: 7.3 seconds -// variant1 = t, variant2 = f, variant3 = f: 3.7 seconds <--- -// variant1 = f, variant2 = f, variant3 = f: 6.1 seconds -// variant1 = f, variant2 = t, variant3 = f: 9.2 seconds - -// variant1 = t, variant2 = t, variant3 = t: 7.0 seconds -// variant1 = t, variant2 = f, variant3 = t: 6.9 seconds -// variant1 = f, variant2 = f, variant3 = t: 9.9 seconds -// variant1 = f, variant2 = t, variant3 = t: 7.3 seconds -//====== -// on factoring12bitsx12.cvc with MINISAT2. -// variant1 = t, variant2 = t, variant3 = f: 10.6 seconds -// variant1 = t, variant2 = f, variant3 = f: 7.8 seconds -// variant1 = f, variant2 = f, variant3 = f: 10.1 seconds -// variant1 = f, variant2 = t, variant3 = f: 11.6 seconds - -// variant1 = t, variant2 = t, variant3 = t: 10.6 seconds -// variant1 = t, variant2 = f, variant3 = t: 10.7 seconds -// variant1 = f, variant2 = f, variant3 = t: 11.8 seconds -// variant1 = f, variant2 = t, variant3 = t: 11.2 seconds -//====== - - -// You can select these with any combination you want of true & false. -const bool division_variant_1 = true; -const bool division_variant_2 = false; -const bool division_variant_3 = true; +// All combinations of division_variant_1, _2, _3 +/* on factoring12bitsx12.cvc with MINISAT2. +000: 0m2.764s +001: 0m4.060s +010: 0m2.750s +011: 0m4.173s +100: 0m3.064s +101: 0m3.217s +110: 0m3.064s +111: 0m3.230s +*/ + // This implements a variant of binary long division. // q and r are "out" parameters. rwidth puts a bound on the @@ -1831,15 +1812,9 @@ BBNodeVec BitBlaster::BBITE(const BBNode& cond, const BBN } // smt-test/transitive400.smt2 -// Cryptominsat 2: bbbvle_variant1 = true. 220ms -// Cryptominsat 2: bbbvle_variant1 = false. 15 sec - -// Minisat 2: bbbvle_variant1 = true. 13 ms -// Minisat 2: bbbvle_variant1 = false. 48 sec - +// Minisat 2: bbbvle_variant = true. 8 ms +// Minisat 2: bbbvle_variant = false. 577 ms -const bool bbbvle_variant1 = true; -const bool bbbvle_variant2 = !bbbvle_variant1; // Workhorse for comparison routines. This does a signed BVLE if is_signed // is true, else it's unsigned. All other comparison operators can be reduced @@ -1848,7 +1823,7 @@ template BBNode BitBlaster::BBBVLE(const BBNodeVec& left, const BBNodeVec& right, bool is_signed, bool is_bvlt) { - if (bbbvle_variant1) + if (bbbvle_variant) return BBBVLE_variant1(left,right,is_signed,is_bvlt); else return BBBVLE_variant2(left,right,is_signed,is_bvlt); diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h index d9ffa24..587c810 100644 --- a/src/to-sat/BitBlaster.h +++ b/src/to-sat/BitBlaster.h @@ -162,6 +162,16 @@ class BitBlaster { Simplifier* simp; BBNodeManagerT* nf; + // You can select these with any combination you want of true & false. + const bool division_variant_1 ; + const bool division_variant_2 ; + const bool division_variant_3 ; + const bool adder_variant; + const bool bbbvle_variant; + + // This is a number 1->5 (currently). + const string multiplication_variant; + public: simplifier::constantBitP::ConstantBitPropagation* cb; @@ -175,28 +185,23 @@ public: * Public Member Functions * ****************************************************************/ - BitBlaster(BBNodeManagerT* bnm , simplifier::constantBitP::ConstantBitPropagation *cb_, Simplifier* _simp, NodeFactory *astNodeF, UserDefinedFlags *_uf) - { + BitBlaster(BBNodeManagerT* bnm , Simplifier* _simp, NodeFactory *astNodeF, UserDefinedFlags *_uf, simplifier::constantBitP::ConstantBitPropagation *cb_ = NULL) + : uf(_uf), + division_variant_1("1" == _uf->get("division_variant_1","1")), + division_variant_2("1" == _uf->get("division_variant_2","1")), + division_variant_3("1" == _uf->get("division_variant_3","1")), + multiplication_variant(_uf->get("multiplication_variant","3")), + adder_variant("1" == _uf->get("adder_variant","1")), + bbbvle_variant("1" == _uf->get("bbbvle_variant","1")) + { nf = bnm; cb = cb_; BBTrue = nf->getTrue(); BBFalse = nf->getFalse(); simp = _simp; ASTNF = astNodeF; - uf = _uf; } - BitBlaster(BBNodeManagerT* bnm, Simplifier* _simp, NodeFactory *astNodeF, UserDefinedFlags *_uf) - { - nf = bnm; - BBTrue = nf->getTrue(); - BBFalse = nf->getFalse(); - cb = NULL; - simp = _simp; - ASTNF = astNodeF; - uf = _uf; - } - void ClearAllTables() { -- 2.47.3