From: trevor_hansen Date: Thu, 15 Mar 2012 12:36:26 +0000 (+0000) Subject: Fixes to code for manipulating rewrite rules. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=0d09d693b58576c1e13ad9c4d0b26de147ebe7ec;p=francis%2Fstp.git Fixes to code for manipulating rewrite rules. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1595 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/util/find_rewrites/Functionlist.h b/src/util/find_rewrites/Functionlist.h index ed1f3bd..8716e9a 100644 --- a/src/util/find_rewrites/Functionlist.h +++ b/src/util/find_rewrites/Functionlist.h @@ -21,7 +21,7 @@ private: { Kind types[] = - { BVXOR, BVAND }; + {BVMULT, BVDIV, SBVDIV, SBVREM, SBVMOD, BVMOD, BVLEFTSHIFT}; //Kind types[] = {BVMULT, BVDIV, SBVDIV, SBVREM, SBVMOD, BVPLUS, BVMOD, BVRIGHTSHIFT, BVLEFTSHIFT, BVOR, BVAND, BVXOR, BVSRSHIFT}; const int number_types = sizeof(types) / sizeof(Kind); @@ -220,7 +220,9 @@ public: removeDuplicates(functions); //applySpeculative(); + // Put back in later! Too slow for now... applyAIGs(); + removeDuplicates(functions); // All the unary combinations of the binaries. allUnary(); diff --git a/src/util/find_rewrites/VariableAssignment.h b/src/util/find_rewrites/VariableAssignment.h index 34b6f6a..dd7868c 100644 --- a/src/util/find_rewrites/VariableAssignment.h +++ b/src/util/find_rewrites/VariableAssignment.h @@ -1,74 +1,46 @@ -/* - * VariableAssignment.h - * - */ - #ifndef VARIABLEASSIGNMENT_H_ #define VARIABLEASSIGNMENT_H_ -extern ASTNode v, v0, w, w0; -extern NodeFactory* nf; -extern BEEV::STPMgr* mgr; +// A pair of constants of the same bit-width assigned to v and w.. struct VariableAssignment { private: ASTNode v; ASTNode w; + bool empty; public: ASTNode getV() const { - assert(v.isConstant()); + assert(!empty); return v; } ASTNode getW() const { - assert(w.isConstant()); + assert(!empty); return w; } void - setV(const ASTNode& nv) + setValues(const ASTNode& nv, const ASTNode& nw) { assert(nv.isConstant()); + assert(nw.isConstant()); + assert(nw.GetValueWidth() == nv.GetValueWidth()); + w = nw; v = nv; - } - - void - setW(const ASTNode& nW) - { - assert(nW.isConstant()); - w = nW; - } - - bool - isEmpty() - { - return (v == mgr->ASTUndefined || w == mgr->ASTUndefined); + empty = false; } VariableAssignment() { + empty = true; } - // Generate w from v a bit randomly. - explicit - VariableAssignment(const ASTNode & n) - { - setV(n); - srand(v.GetUnsignedConst()); - w = mgr->CreateBVConst(n.GetValueWidth(), rand()); - } - - VariableAssignment(ASTNode & n0, ASTNode & n1) - { - setV(n0); - setV(n1); - } }; -#endif /* VARIABLEASSIGNMENT_H_ */ +#endif diff --git a/src/util/find_rewrites/rewrite.cpp b/src/util/find_rewrites/rewrite.cpp index 97bc2cb..ba8fd19 100644 --- a/src/util/find_rewrites/rewrite.cpp +++ b/src/util/find_rewrites/rewrite.cpp @@ -301,9 +301,9 @@ checkProp(const ASTNode& n) return true; } -// True if it's always true. Otherwise fills the assignment. +// True if it's always true, otherwise fills the assignment. bool -isConstant(const ASTNode& n, VariableAssignment& different, const int bits) +isConstant(const ASTNode& n, VariableAssignment& different, const int bit_width) { if (isConstantToSat(n)) return true; @@ -313,18 +313,23 @@ isConstant(const ASTNode& n, VariableAssignment& different, const int bits) vector symbols = getVariables(n); - // Both of them might not be contained in the assignment. - different.setV(mgr->CreateZeroConst(bits)); - different.setW(mgr->CreateZeroConst(bits)); + // Both of them might not be contained in the assignment, + // (which might have been widened). + ASTNode vN = mgr->CreateZeroConst(bit_width); + ASTNode wN = mgr->CreateZeroConst(bit_width); - // It might have been widened. for (int i = 0; i < symbols.size(); i++) { + assert(symbols[i].GetValueWidth() == bit_width); + if (strncmp(symbols[i].GetName(), "v", 1) == 0) - different.setV(GlobalSTP->Ctr_Example->GetCounterExample(true, symbols[i])); + vN = GlobalSTP->Ctr_Example->GetCounterExample(true, symbols[i]); else if (strncmp(symbols[i].GetName(), "w", 1) == 0) - different.setW(GlobalSTP->Ctr_Example->GetCounterExample(true, symbols[i])); + wN = GlobalSTP->Ctr_Example->GetCounterExample(true, symbols[i]); } + + different.setValues(vN, wN); + return false; } } @@ -727,7 +732,8 @@ startup() simp = new Simplifier(mgr); ArrayTransformer * at = new ArrayTransformer(mgr, simp); AbsRefine_CounterExample* abs = new AbsRefine_CounterExample(mgr, simp, at); - ToSAT* tosat = new ToSAT(mgr); + ToSATAIG* tosat = new ToSATAIG(mgr); + tosat->setArrayTransformer(at); GlobalSTP = new STP(mgr, simp, at, tosat, abs); @@ -758,9 +764,7 @@ startup() // Write out the work so far.. signal(SIGUSR1, do_write_out); - signal(SIGUSR2, do_usr2); - } void @@ -768,6 +772,11 @@ clearSAT() { delete ss; ss = new MinisatCore(mgr->soft_timeout_expired); + + delete GlobalSTP->tosat; + ToSATAIG* aig = new ToSATAIG(mgr); + aig->setArrayTransformer(GlobalSTP->arrayTransformer); + GlobalSTP->tosat = aig; } // Return true if the negation of the query is unsatisfiable. @@ -979,6 +988,12 @@ findRewrites(ASTVec& expressions, const vector& values, cons if (from.isConstant() && to.isConstant()) continue; + // If they can't be ordered continue. Maybe they could be ordered if we applied + // the rewrites through.. + ASTNode f = from, t = to; + if (!orderEquivalence(f,t)) + continue; + VariableAssignment different; bool bad = false; const int st = getCurrentTime(); @@ -1025,17 +1040,10 @@ findRewrites(ASTVec& expressions, const vector& values, cons // Sometimes it doesn't. Not sure why.. assert(t == rewrite_system.rewriteNode(f)); - // Remove the more difficult expression. - if (f == equiv[i]) - { - cout << "."; - equiv[i] = mgr->ASTUndefined; - } - if (t == equiv[j]) - { - cout << "."; - equiv[j] = mgr->ASTUndefined; - } + + equiv[i] = rewrite_system.rewriteNode(equiv[i]); + equiv[j] = rewrite_system.rewriteNode(equiv[j]); + } else if (!bad) { @@ -1210,7 +1218,7 @@ checkRule(const ASTNode & from, const ASTNode & to, VariableAssignment& assignme } // Send it to the SAT solver to verify that the widening has the same answer. - bool result = isConstant(widened, assignment, bits); + bool result = isConstant(widened, assignment, i); if (!result) { @@ -1442,6 +1450,7 @@ writeOutRules() cout << "Writing out: " << rewrite_system.size() << " rules" << endl; force_writeout = false; +#if 0 std::vector output; std::map dup; @@ -1520,9 +1529,11 @@ writeOutRules() cout << "Rules Discovered in total: " << rewrite_system.size() << endl; + // Group functions of the same kind all together. hash_map, hashF > buckets; bucket("n.GetKind() ==", output, buckets); +#endif ofstream outputFile; diff --git a/src/util/find_rewrites/rewrite_rule.h b/src/util/find_rewrites/rewrite_rule.h index a27ea05..44a9eb7 100644 --- a/src/util/find_rewrites/rewrite_rule.h +++ b/src/util/find_rewrites/rewrite_rule.h @@ -4,6 +4,11 @@ #include "../../STPManager/STPManager.h" #include "misc.h" +extern ASTNode v, v0, w, w0; +extern NodeFactory* nf; +extern BEEV::STPMgr* mgr; + + void soft_time_out(int ignored) { diff --git a/src/util/find_rewrites/rewrite_system.h b/src/util/find_rewrites/rewrite_system.h index 1d376b9..24d3076 100644 --- a/src/util/find_rewrites/rewrite_system.h +++ b/src/util/find_rewrites/rewrite_system.h @@ -246,6 +246,8 @@ public: if (!ok) { cout << "Erasing bad rule.\n"; + cout << "Initially" << it->getFrom() << it->getTo(); + cout << "Now" << from_rewritten << to_rewritten; erase(it--); i--; lookups_invalid = true;