From 2cadcc4bc7b0d8126e2449feaaee1af64966e547 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sat, 3 Mar 2012 00:50:53 +0000 Subject: [PATCH] Extra utility code for manipulating rewrite rules. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1575 e59a4935-1847-0410-ae03-e826735625c1 --- src/util/Makefile | 4 +- src/util/find_rewrites/Functionlist.h | 308 ++++++ src/util/find_rewrites/Makefile | 17 + src/util/find_rewrites/VariableAssignment.h | 77 ++ src/util/{ => find_rewrites}/rewrite.cpp | 1043 ++++++++++--------- src/util/find_rewrites/rewrite_data_new.cpp | 102 ++ src/util/find_rewrites/rewrite_rule.h | 146 +++ src/util/find_rewrites/rewrite_system.h | 190 ++++ 8 files changed, 1386 insertions(+), 501 deletions(-) create mode 100644 src/util/find_rewrites/Functionlist.h create mode 100644 src/util/find_rewrites/Makefile create mode 100644 src/util/find_rewrites/VariableAssignment.h rename src/util/{ => find_rewrites}/rewrite.cpp (62%) create mode 100644 src/util/find_rewrites/rewrite_data_new.cpp create mode 100644 src/util/find_rewrites/rewrite_rule.h create mode 100644 src/util/find_rewrites/rewrite_system.h diff --git a/src/util/Makefile b/src/util/Makefile index 231e6df..1aa5979 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -1,7 +1,7 @@ TOP = ../../ include $(TOP)scripts/Makefile.common -SRCS = rewrite.cpp time_cbitp.cpp test_cbitp.cpp +SRCS = time_cbitp.cpp test_cbitp.cpp OBJS = $(SRCS:.cpp=.o) CXXFLAGS += -L../../lib/ @@ -10,8 +10,6 @@ CXXFLAGS += -L../../lib/ time_cbitp: $(OBJS) $(TOP)lib/libstp.a $(CXX) $(CXXFLAGS) $@.o -o $@ -lstp -rewrite: $(OBJS) $(TOP)lib/libstp.a - $(CXX) $(CXXFLAGS) $@.o -o $@ -lstp test_cbitp: $(OBJS) $(TOP)lib/libstp.a $(CXX) $(CXXFLAGS) $@.o -o $@ -lstp diff --git a/src/util/find_rewrites/Functionlist.h b/src/util/find_rewrites/Functionlist.h new file mode 100644 index 0000000..9086793 --- /dev/null +++ b/src/util/find_rewrites/Functionlist.h @@ -0,0 +1,308 @@ +/* + * Functionlist.h + * + */ + +#ifndef FUNCTIONLIST_H_ +#define FUNCTIONLIST_H_ + +extern const int bits; +extern Simplifier *simp; +extern Rewrite_system to_write; + +ASTNode +widen(const ASTNode& w, int width); + +ASTNode +create(Kind k, const ASTNode& n0, const ASTNode& n1); + + +class Function_list +{ + + // Because v and w might come from "result", if "result" is resized, they will + // be moved. So we can't use references to them. + void + getAllFunctions(const ASTNode v, const ASTNode w, ASTVec& result) + { + + Kind types[] = {BVMULT, BVPLUS, BVXOR, BVAND, BVOR ,BVRIGHTSHIFT, BVLEFTSHIFT}; + + //Kind types[] = {BVMULT, BVDIV, SBVDIV, SBVREM, SBVMOD, BVPLUS, BVMOD, BVRIGHTSHIFT, BVLEFTSHIFT, BVOR, BVAND, BVXOR, BVSRSHIFT}; + const int number_types = sizeof(types) / sizeof(Kind); + + // all two argument functions. + for (int i = 0; i < number_types; i++) + result.push_back(create(types[i], v, w)); + } + + + ASTNode + rewriteThroughWithAIGS(const ASTNode &n_) + { + assert(n_.GetType() == BITVECTOR_TYPE); + ASTNode f = mgr->LookupOrCreateSymbol("rewriteThroughWithAIGS"); + f.SetValueWidth(n_.GetValueWidth()); + ASTNode n = create(EQ, n_, f); + + BBNodeManagerAIG nm; + BitBlaster bb(&nm, simp, mgr->defaultNodeFactory, &mgr->UserFlags); + ASTNodeMap fromTo; + ASTNodeMap equivs; + bb.getConsts(n, fromTo, equivs); + + ASTNode result = n_; + if (equivs.size() > 0) + { + ASTNodeMap cache; + result = SubstitutionMap::replace(result, equivs, cache, nf, false, true); + } + + if (fromTo.size() > 0) + { + ASTNodeMap cache; + result = SubstitutionMap::replace(result, fromTo, cache, nf); + } + return result; + } + + void + applyBigRewrite() + { + BEEV::BigRewriter b; + + for (int i = 0; i < functions.size(); i++) + { + if (functions[i] == mgr->ASTUndefined) + continue; + + if (i % 100000 == 0) + cerr << "BigRewrite:" << i << " of " << functions.size(); + + ASTNodeMap fromTo; + ASTNode s = b.rewrite(functions[i], fromTo, nf, mgr); + if (s != functions[i]) + { + functions[i] = s; + } + } + } + + void + applyRewritesToAll(ASTVec& functions) + { + to_write.buildRules(); + cerr << "Applying:" << to_write.size() <<"rewrite rules" << endl; + + for (int i = 0; i < functions.size(); i++) + { + if (functions[i] == mgr->ASTUndefined) + continue; + + if (i % 100000 == 0) + cerr << "applyRewritesToAll:" << i << " of " << functions.size() << endl; + + ASTNode r = to_write.rewriteNode(functions[i]); + if (r!= functions[i]) + { + // cerr << "changed" << functions[i] << " to "<< r; + + functions[i] =r; + } + } + } + + + // If there only w variables in the problem. We can delete it because + // we will have another with just v's. + // NB: Can only apply at the top level. + void + removeSingleVariable() + { + for (int i = 0; i < functions.size(); i++) + { + vector symbols = getVariables(functions[i]); + + if (i % 100000 == 0) + cout << "removeSingleVariable:" << i << " of " << functions.size() << "\n"; + + if (symbols.size() == 1 && symbols[0] == w) + { + functions[i] = mgr->ASTUndefined; // We can't widen it later. So remove it. + continue; + } + } + } + + void + removeSingleUndefined() + { + for (int i = 0; i < functions.size(); i++) + { + if (functions[i] == mgr->ASTUndefined) + { + functions.erase(functions.begin() + i); + break; + } + } + } + + void + applySpeculative() + { + for (int i = 0; i < functions.size(); i++) + { + if (functions[i] == mgr->ASTUndefined) + continue; + + if (i % 100000 == 0) + cerr << "applySpeculative:" << i << " of " << functions.size() << "\n"; + + functions[i] = simp->SimplifyTerm_TopLevel(functions[i]); + } + } + + void + checkFunctions() + { + for (int i = 0; i < functions.size(); i++) + { + assert(functions[i].GetType() == BITVECTOR_TYPE); + assert(functions[i].GetValueWidth() == bits); + assert(BVTypeCheckRecursive(functions[i])); + } + } + + void + removeNonWidened() + { + for (int i = 0; i < functions.size(); i++) + { + if (mgr->ASTUndefined == functions[i]) + continue; + + if (i % 100000 == 0) + cerr << "Widen check:" << i << " of " << functions.size() << endl; + + if (mgr->ASTUndefined == widen(functions[i], bits + 1)) + { + cerr << "Can't widen" << functions[i]; + functions[i] = mgr->ASTUndefined; // We can't widen it later. So remove it. + continue; + } + } + } + + + // Triples the number of functions by adding all the unary ones. + void + allUnary() + { + for (int i = 0, size = functions.size(); i < size; i++) + { + if (functions[i] == mgr->ASTUndefined) + continue; + + functions.push_back(nf->CreateTerm(BEEV::BVNEG, bits, functions[i])); + functions.push_back(nf->CreateTerm(BEEV::BVUMINUS, bits, functions[i])); + } + } + + + void + applyAIGs() + { + ASTNode f = mgr->LookupOrCreateSymbol("rewriteThroughWithAIGS"); + f.SetValueWidth(bits); + + for (int i = 0; i < functions.size(); i++) + { + if (functions[i] == mgr->ASTUndefined) + continue; + + if (i % 100000 == 0) + cerr << "ApplyAigs:" << i << " of " << functions.size() << endl; + + rewriteThroughWithAIGS(functions[i]); + } + } + +public: + + void + buildAll() + { + /////////////////////////// BV, BV -> BV. + functions.push_back(w); + functions.push_back(v); + + functions.push_back(mgr->CreateBVConst(bits, 0)); + functions.push_back(mgr->CreateBVConst(bits, 1)); + functions.push_back(mgr->CreateMaxConst(bits)); + + // All unary of the leaves. + allUnary(); + removeDuplicates(functions); + cerr << "Leaves:" << functions.size() << endl; + + // We've got the leaves, and their unary operations, + // now get the binary operations of all of those. + int size = functions.size(); + for (int i = 0; i < size; i++) + for (int j = 0; j < size; j++) + getAllFunctions(functions[i], functions[j], functions); + + allUnary(); + + + applyAIGs(); + applySpeculative(); + applyRewritesToAll(functions); + checkFunctions(); + removeDuplicates(functions); + removeSingleUndefined(); + + cerr << "One Level:" << functions.size() << endl; + + const bool two_level = false; + + if (two_level) + { + int last = 0; + ASTVec functions_copy(functions); + size = functions_copy.size(); + for (int i = 0; i < size; i++) + for (int j = 0; j < size; j++) + getAllFunctions(functions_copy[i], functions_copy[j], functions); + + cerr << "Removing single variables" <ASTUndefined || w == mgr->ASTUndefined); + } + + VariableAssignment() + { + } + + // 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_ */ diff --git a/src/util/rewrite.cpp b/src/util/find_rewrites/rewrite.cpp similarity index 62% rename from src/util/rewrite.cpp rename to src/util/find_rewrites/rewrite.cpp index aeb7eb1..1b139fa 100644 --- a/src/util/rewrite.cpp +++ b/src/util/find_rewrites/rewrite.cpp @@ -8,16 +8,27 @@ #include #include -#include "../AST/AST.h" -#include "../printer/printers.h" +#include "../../AST/AST.h" +#include "../../printer/printers.h" -#include "../STPManager/STPManager.h" -#include "../to-sat/AIG/ToSATAIG.h" -#include "../sat/MinisatCore.h" -#include "../STPManager/STP.h" -#include "../STPManager/DifficultyScore.h" -#include "../simplifier/BigRewriter.h" +#include "../../STPManager/STPManager.h" +#include "../../to-sat/AIG/ToSATAIG.h" +#include "../../sat/MinisatCore.h" +#include "../../STPManager/STP.h" +#include "../../STPManager/DifficultyScore.h" +#include "../../simplifier/BigRewriter.h" +#include "../../AST/NodeFactory/TypeChecker.h" +#include "../../cpp_interface/cpp_interface.h" +#include "VariableAssignment.h" + +#include "rewrite_rule.h" +#include "rewrite_system.h" +#include "Functionlist.h" + +extern FILE *smt2in; +extern int +smt2parse(); using namespace std; using namespace BEEV; @@ -27,7 +38,11 @@ bool finished = false; // Holds the rewrite that was disproved at the largest bitwidth. ASTNode highestDisproved; -int highestLevel =0; +int highestLevel = 0; +int discarded = 0; + +//static +int Rewrite_rule::static_id; ////////////////////////////////// const int bits = 6; @@ -42,9 +57,18 @@ vector saved_array; // Stores the difficulties that have already been generated. map difficulty_cache; +Rewrite_system to_write; + void clearSAT(); +template + void + removeDuplicates(T & big); + +bool +is_candidate(ASTNode from, ASTNode to); + bool isConstantToSat(const ASTNode & query); @@ -52,9 +76,22 @@ string containsNode(const ASTNode& n, const ASTNode& hunting, string& current); void -writeOutRules(); +applyRewritesToAll(ASTVec & v); + +void +writeOutRules(string fileName); -void applyBigRewrite(ASTVec& functions); +int +getDifficulty(const ASTNode& n_); + +vector +getVariables(const ASTNode& n); + +bool +unifyNode(const ASTNode& n0, const ASTNode& n1, ASTNodeMap& fromTo, const int term_variable_width); + +int +findNewRewrites(); typedef HASHMAP ASTNodeString; @@ -64,114 +101,44 @@ SATSolver * ss; ASTNodeSet stored; // Store nodes so they aren't garbage collected. Simplifier *simp; -ASTNode zero, one, maxNode, v, w; - -struct ToWrite -{ - ASTNode from; - ASTNode to; - ASTNode n; - int time; - - ToWrite() - { - } - - ToWrite(ASTNode from_, ASTNode to_, int t) - { - from = from_; - to = to_; - time = t; - n = mgr->CreateNode(EQ,to,from); - } - - bool isEmpty() - { - return (n == mgr->ASTUndefined); - } - - bool - operator==(const ToWrite t) const - { - return (n == t.n); - } - - bool - operator<(const ToWrite t) const - { - return (n < t.n); - } -}; - -// Rules to write out when we get the chance. -vector toWrite; +ASTNode zero, one, maxNode, v, w, v0, w0; // Width of the rewrite rules that were output last time. int lastOutput = 0; -struct Assignment -{ -private: - ASTNode v; - ASTNode w; - -public: - ASTNode - getV() const - { - assert(v.isConstant()); - return v; - } +bool +checkRule(const ASTNode & from, const ASTNode & to, VariableAssignment& ass, bool& bad); - ASTNode - getW() const - { - assert(w.isConstant()); - return w; - } +ASTNode +renameVars(const ASTNode &n) +{ + ASTNodeMap ft; - void - setV(const ASTNode& nv) - { - assert(nv.isConstant()); - v = nv; - } + assert(v.GetValueWidth() == v0.GetValueWidth()); + assert(w.GetValueWidth() == w0.GetValueWidth()); - void - setW(const ASTNode& nW) - { - assert(nW.isConstant()); - w = nW; - } + ft.insert(make_pair(v, v0)); + ft.insert(make_pair(w, w0)); - bool isEmpty() - { - return (v == mgr->ASTUndefined || w == mgr->ASTUndefined); - } + ASTNodeMap cache; + return SubstitutionMap::replace(n, ft, cache, nf); +} - Assignment() - { - } +ASTNode +renameVarsBack(const ASTNode &n) +{ + ASTNodeMap ft; - // Generate w from v a bit randomly. - explicit - Assignment(const ASTNode & n) - { - setV(n); - srand(v.GetUnsignedConst()); - w = BEEV::ParserBM->CreateBVConst(n.GetValueWidth(), rand()); - } + assert(v.GetValueWidth() == v0.GetValueWidth()); + assert(w.GetValueWidth() == w0.GetValueWidth()); - Assignment(ASTNode & n0, ASTNode & n1) - { - setV(n0); - setV(n1); - } -}; + ft.insert(make_pair(v0, v)); + ft.insert(make_pair(w0, w)); -bool -checkAndStoreRule(const ASTNode & from, const ASTNode & to, Assignment& ass); + ASTNodeMap cache; + return SubstitutionMap::replace(n, ft, cache, nf); +} // Helper functions. Don't need to specify the width. @@ -229,6 +196,16 @@ getVariables(const ASTNode& n, vector& symbols, ASTNodeSet& visited) getVariables(n[i], symbols, visited); } +vector +getVariables(const ASTNode& n) +{ + vector symbols; + ASTNodeSet visited; + getVariables(n, symbols, visited); + + return symbols; +} + // Get the constant from replacing values in the map. ASTNode eval(const ASTNode &n, ASTNodeMap& map, int count = 0) @@ -244,7 +221,7 @@ eval(const ASTNode &n, ASTNodeMap& map, int count = 0) return (*map.find(n)).second; } - if(n.Degree() == 0 ) + if (n.Degree() == 0) { cerr << n; assert(false); @@ -311,28 +288,28 @@ checkProp(const ASTNode& n) // True if it's always true. Otherwise fills the assignment. bool -isConstant(const ASTNode& n, Assignment& different) +isConstant(const ASTNode& n, VariableAssignment& different) { if (isConstantToSat(n)) return true; else { - vector symbols; - ASTNodeSet visited; - getVariables(n,symbols,visited); + mgr->ValidFlag = false; + + vector symbols = getVariables(n); assert(symbols.size() > 0); // Both of them might not be contained in the assignment. - different.setV(mgr->CreateBVConst(symbols[0].GetValueWidth(),0)); - different.setW(mgr->CreateBVConst(symbols[0].GetValueWidth(),0)); + different.setV(mgr->CreateBVConst(symbols[0].GetValueWidth(), 0)); + different.setW(mgr->CreateBVConst(symbols[0].GetValueWidth(), 0)); // It might have been widened. - for (int i =0; i < symbols.size();i++) + for (int i = 0; i < symbols.size(); i++) { - if (strncmp(symbols[i].GetName(), "v", 1) ==0) - different.setV(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])); + if (strncmp(symbols[i].GetName(), "v", 1) == 0) + different.setV(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])); } return false; } @@ -396,49 +373,112 @@ widen(const ASTNode& w, int width) } if (w.GetKind() == BVCONCAT && ((ch[0].GetValueWidth() + ch[1].GetValueWidth()) != width)) - return mgr->ASTUndefined; // Didn't widen properly. + return mgr->ASTUndefined; // Didn't widen properly. + // We got to the trouble below because sometimes we get 1-bit wide expressions which we don't + // want to widen to "bits". ASTNode result; if (w.GetType() == BOOLEAN_TYPE) result = nf->CreateNode(w.GetKind(), ch); else if (w.GetKind() == BVEXTRACT) { int new_width = ch[1].GetUnsignedConst() - ch[2].GetUnsignedConst() + 1; - result = nf->CreateTerm(w.GetKind(), new_width, ch); + result = nf->CreateTerm(BVEXTRACT, new_width, ch); } + else if (w.GetKind() == BVCONCAT) + result = nf->CreateTerm(BVCONCAT, ch[1].GetValueWidth() + ch[0].GetValueWidth(), ch); + else if (w.GetKind() == ITE) + result = nf->CreateTerm(ITE, ch[1].GetValueWidth(), ch); + else if (w.GetKind() == BVSX) + result = nf->CreateTerm(BVSX, ch[1].GetUnsignedConst(), ch); else - result = nf->CreateTerm(w.GetKind(), width, ch); + result = nf->CreateTerm(w.GetKind(), ch[0].GetValueWidth(), ch); - BVTypeCheck(result); + BVTypeCheck(result); return result; } -ASTNode -rewriteThroughWithAIGS(const ASTNode &n) +bool +orderEquivalence(ASTNode& from, ASTNode& to) { - assert(n.GetKind() == EQ); + vector s_from; // The variables in the from node. + ASTNodeSet visited; + getVariables(from, s_from, visited); + std::sort(s_from.begin(), s_from.end()); - BBNodeManagerAIG nm; - BitBlaster bb(&nm, simp, mgr->defaultNodeFactory, &mgr->UserFlags); - ASTNode input = n; - ASTNodeMap fromTo; - ASTNodeMap equivs; - bb.getConsts(input, fromTo,equivs); + vector s_to; // The variables in the to node. + visited.clear(); + getVariables(to, s_to, visited); + sort(s_to.begin(), s_to.end()); + + vector result(s_to.size() + s_from.size()); + // We must map from most variables to fewer variables. + vector::iterator it = std::set_intersection(s_from.begin(), s_from.end(), s_to.begin(), s_to.end(), + result.begin()); + int intersection = it - result.begin(); - if (equivs.size() > 0) + if (intersection != s_from.size() && intersection != s_to.size()) + return false; + + if (to.isAtom()) + return true; + + if (from.isAtom()) { - ASTNodeMap cache; - input = SubstitutionMap::replace(input, equivs, cache,nf,false,true); + std::swap(from, to); + return true; } - if (fromTo.size() > 0) + // Is one a subgraph of another. + if (is_candidate(from, to)) { - ASTNodeMap cache; - input = SubstitutionMap:: replace(input, fromTo, cache,nf); + return true; + } + + if (is_candidate(to, from)) + { + std::swap(from, to); + return true; + } + + if (s_from.size() < s_to.size()) + { + swap(to, from); + return true; + } + + if (s_from.size() > s_to.size()) + return true; + + if (getDifficulty(from) < getDifficulty(to)) + { + swap(from, to); + return true; + } + + if (getDifficulty(from) > getDifficulty(to)) + { + return true; + } + + // Difficulty is equal. Order based on the number of nodes. + vector symbols; + visited.clear(); + getVariables(from, symbols, visited); + int from_c = visited.size(); + + symbols.clear(); + visited.clear(); + getVariables(to, symbols, visited); + int to_c = visited.size(); + + if (to_c > from_c) + { + swap(from, to); } - return input; + return true; } int @@ -450,7 +490,7 @@ getDifficulty(const ASTNode& n_) return difficulty_cache.find(n_)->second; // Calculate the difficulty over the widened version. - ASTNode n = widen(n_,widen_to); + ASTNode n = widen(n_, widen_to); if (n.GetKind() == UNDEFINED) return -1; @@ -476,7 +516,7 @@ getDifficulty(const ASTNode& n_) // Why we go to all this trouble. The number of clauses. int score = cnfData->nClauses; - Cnf_ClearMemory(); + //Cnf_ClearMemory(); Cnf_DataFree(cnfData); cnfData = NULL; @@ -530,20 +570,6 @@ doIte(ASTNode a) } } - -void -getAllFunctions(ASTNode v, ASTNode w, ASTVec& result) -{ - - Kind types[] = - { BVMULT , BVDIV, SBVDIV, SBVREM, SBVMOD, BVPLUS, BVMOD, BVRIGHTSHIFT, BVLEFTSHIFT, BVOR, BVAND, BVXOR, BVSRSHIFT }; - int number_types = sizeof(types) / sizeof(Kind); - - // all two argument functions. - for (int i = 0; i < number_types; i++) - result.push_back(create(types[i], v, w)); -} - int startup() { @@ -566,8 +592,13 @@ startup() GlobalSTP = new STP(mgr, simp, at, tosat, abs); +#ifndef NOTSIMPLIFYING_NF nf = new SimplifyingNodeFactory(*(mgr->hashingNodeFactory), *mgr); - mgr->defaultNodeFactory =nf; + mgr->defaultNodeFactory = nf; +#else + nf = mgr->hashingNodeFactory; + mgr->defaultNodeFactory = mgr->hashingNodeFactory; +#endif mgr->UserFlags.stats_flag = false; mgr->UserFlags.optimize_flag = true; @@ -584,10 +615,19 @@ startup() one = mgr->CreateOneConst(bits); maxNode = mgr->CreateMaxConst(bits); - v = mgr->CreateSymbol("v", 0, bits); - w = mgr->CreateSymbol("w", 0, bits); - srand(time(NULL)); + + v0 = mgr->LookupOrCreateSymbol("v0"); + v0.SetValueWidth(bits); + w0 = mgr->LookupOrCreateSymbol("w0"); + w0.SetValueWidth(bits); + + //v = mgr->LookupOrCreateSymbol("v"); + // v.SetValueWidth(bits); + // w = mgr->LookupOrCreateSymbol("w"); + // w.SetValueWidth(bits); + + } void @@ -602,7 +642,7 @@ bool isConstantToSat(const ASTNode & query) { assert(query.GetType() == BOOLEAN_TYPE); - cerr << "to"; + cout << "to"; GlobalSTP->ClearAllTables(); clearSAT(); @@ -611,25 +651,24 @@ isConstantToSat(const ASTNode & query) SOLVER_RETURN_TYPE r = GlobalSTP->Ctr_Example->CallSAT_ResultCheck(*ss, query2, query2, GlobalSTP->tosat, false); - cerr << "from"; + cout << "from"; return (r == SOLVER_VALID); // unsat, always true } - // Replaces the symbols in n, by each of the values, and concatenates them // to turn it into a single 64-bit value. uint64_t -getHash(const ASTNode& n_, const vector& values) +getHash(const ASTNode& n_, const vector& values) { assert(values.size() > 0); - const int ass_bitwidth =values[0].getV().GetValueWidth(); - assert (ass_bitwidth >= bits); + const int ass_bitwidth = values[0].getV().GetValueWidth(); + assert(ass_bitwidth >= bits); ASTNode n = n_; // The values might be at a higher bit-width. if (ass_bitwidth > bits) - n = widen(n_,ass_bitwidth); + n = widen(n_, ass_bitwidth); if (n == mgr->ASTUndefined) // Can't be widened. return 0; @@ -645,22 +684,22 @@ getHash(const ASTNode& n_, const vector& values) ASTNodeMap mapToVal; for (int j = 0; j < symbols.size(); j++) { - if (strncmp(symbols[j].GetName(), "v", 1) ==0) + if (strncmp(symbols[j].GetName(), "v", 1) == 0) { mapToVal.insert(make_pair(symbols[j], values[i].getV())); - assert(symbols[j].GetValueWidth() == values[i].getV().GetValueWidth() ); + assert(symbols[j].GetValueWidth() == values[i].getV().GetValueWidth()); } - else if (strncmp(symbols[j].GetName(), "w", 1) ==0) + else if (strncmp(symbols[j].GetName(), "w", 1) == 0) { mapToVal.insert(make_pair(symbols[j], values[i].getW())); - assert(symbols[j].GetValueWidth() == values[i].getW().GetValueWidth() ); + assert(symbols[j].GetValueWidth() == values[i].getW().GetValueWidth()); } else { cerr << "Unknown symbol!" << symbols[j]; FatalError("f"); } - assert(symbols[j].GetValueWidth() == ass_bitwidth ); + assert(symbols[j].GetValueWidth() == ass_bitwidth); } ASTNode r = eval(n, mapToVal); @@ -678,14 +717,13 @@ contained_in(ASTNode from, ASTNode to) if (from == to) return true; - for (int i = 0; i < to.Degree(); i++) - if (contained_in(from, to[i])) + for (int i = 0; i < from.Degree(); i++) + if (contained_in(from[i], to)) return true; return false; } - // Is mapping from "From" to "to" a rule we are interested in?? bool is_candidate(ASTNode from, ASTNode to) @@ -705,16 +743,18 @@ lessThan(const ASTNode& n1, const ASTNode& n2) return (((unsigned) n1.GetNodeNum()) < ((unsigned) n2.GetNodeNum())); } - - // Breaks the expressions into buckets recursively, then pairwise checks that they are equivalent. void -findRewrites(ASTVec& expressions, const vector& values, const int depth = 0) +findRewrites(ASTVec& expressions, const vector& values, const int depth = 0) { if (expressions.size() < 2) - return; + { + discarded += expressions.size(); + return; + } - cout << '\n' << "depth:" << depth << ", size:" << expressions.size() << " values:" << values.size() << " found: " << toWrite.size() << '\n'; + cout << '\n' << "depth:" << depth << ", size:" << expressions.size() << " values:" << values.size() << " found: " + << to_write.size() << '\n'; assert(expressions.size() >0); @@ -744,7 +784,7 @@ findRewrites(ASTVec& expressions, const vector& values, const int de for (it2 = map.begin(); it2 != map.end(); it2++) { ASTVec& equiv = it2->second; - vector a; + vector a; findRewrites(equiv, a, depth + 1); equiv.clear(); } @@ -758,60 +798,55 @@ findRewrites(ASTVec& expressions, const vector& values, const int de for (int i = 0; i < equiv.size(); i++) { if (equiv[i].GetKind() == UNDEFINED) - continue; + continue; + + // nb. I haven't rebuilt the map, it's done by writeOutRules(). + equiv[i] == to_write.rewriteNode(equiv[i]); for (int j = i + 1; j < equiv.size(); j++) /// commutative so skip some. { if (equiv[i].GetKind() == UNDEFINED || equiv[j].GetKind() == UNDEFINED) continue; + equiv[j] = to_write.rewriteNode(equiv[j]); + ASTNode n = nf->CreateNode(EQ, equiv[i], equiv[j]); if (n.GetKind() != EQ) continue; - n = rewriteThroughWithAIGS(n); + ASTNode from = equiv[i]; + ASTNode to = equiv[j]; + bool r = orderEquivalence(from, to); - if (n.GetKind() != EQ) - continue; + VariableAssignment different; + bool bad = false; + const int st = getCurrentTime(); - ASTNode from, to; - if (getDifficulty(n[0]) < getDifficulty(n[1])) - { - to = n[0]; - from = n[1]; - } - else if (getDifficulty(n[0]) > getDifficulty(n[1])) - { - from = n[0]; - to = n[1]; - } - else + if (checkRule(from, to, different, bad)) { - // Difficulty is equal. Try it both ways and see if it's a candidate. - if (is_candidate(n[0], n[1])) + to_write.push_back(Rewrite_rule(mgr, from, to, getCurrentTime() - st)); + + // Remove the more difficult expression. + if (from == equiv[i]) { - from = n[0]; - to = n[1]; + cerr << "."; + equiv[i] = mgr->ASTUndefined; } - else + if (from == equiv[j]) { - from = n[1]; - to = n[0]; + cerr << "."; + equiv[j] = mgr->ASTUndefined; } } - - Assignment different; - if (checkAndStoreRule(from,to, different)) + else if (!r) { - // Remove the more difficult expression. - if (from == equiv[i]) - equiv[i] = mgr->ASTUndefined; - if (from == equiv[j]) - equiv[j] = mgr->ASTUndefined; + // It probably shouldn't get to here.. + cerr << "can't be ordered" << from << to; + continue; // can't be ordered. } - else if (!different.isEmpty()) + else if (!bad) { - vector ass; + vector ass; ass.push_back(different); // Discard the ones we've checked entirely. @@ -823,17 +858,16 @@ findRewrites(ASTVec& expressions, const vector& values, const int de } // Write out the rules intermitently. - if (lastOutput + 500 < toWrite.size()) + if (lastOutput + 5000 < to_write.size()) { - writeOutRules(); - lastOutput = toWrite.size(); + writeOutRules("array.smt2"); + lastOutput = to_write.size(); } } } } - // Converts the node into an IF statement that matches the node. void rule_to_string(const ASTNode & n, ASTNodeString& names, string& current, string& sofar) @@ -850,7 +884,7 @@ rule_to_string(const ASTNode & n, ASTNodeString& names, string& current, string& return; } - if (n.isConstant() && (n.GetValueWidth() == bits || n.GetValueWidth() == bits-1)) + if (n.isConstant() && (n.GetValueWidth() == bits || n.GetValueWidth() == bits - 1)) { sofar += "&& " + current + " == "; stringstream constant; @@ -873,7 +907,6 @@ rule_to_string(const ASTNode & n, ASTNodeString& names, string& current, string& return; } - if (n == mgr->CreateBVConst(32, bits)) { sofar += "&& " + current + " == bm->CreateBVConst(32, width) "; @@ -958,15 +991,13 @@ containsNode(const ASTNode& n, const ASTNode& hunting, string& current) // Check it holds at higher bit-widths. // If so, then save the rule for later. bool -checkAndStoreRule(const ASTNode & from, const ASTNode & to, Assignment& assignment) +checkRule(const ASTNode & from, const ASTNode & to, VariableAssignment& assignment, bool&bad) { - const ASTNode n = create(EQ,from,to); + const ASTNode n = create(EQ, from, to); assert(n.GetKind() == BEEV::EQ); assert(widen_to > bits); - const int st = getCurrentTime(); - for (int i = bits; i < widen_to; i++) { const ASTNode& widened = widen(n, i); @@ -976,6 +1007,7 @@ checkAndStoreRule(const ASTNode & from, const ASTNode & to, Assignment& assignme { cerr << "can't widen"; cerr << n; + bad = true; return false; } @@ -991,12 +1023,13 @@ checkAndStoreRule(const ASTNode & from, const ASTNode & to, Assignment& assignme } // Detected it's not a constant, or is constant FALSE. - cerr << "*" << i - bits << "*"; + if (i-bits > 0) + cerr << "*" << i - bits << "*"; + return false; } } - toWrite.push_back(ToWrite(from,to,getCurrentTime() - st)); return true; } @@ -1007,7 +1040,7 @@ template cerr << "Before removing duplicates:" << big.size(); std::sort(big.begin(), big.end()); typename T::iterator it = std::unique(big.begin(), big.end()); - big.resize(it - big.begin()); + big.erase(it, big.end()); cerr << ".After removing duplicates:" << big.size() << endl; } @@ -1045,11 +1078,11 @@ bucket(string substring, vector& inputs, hash_map } } - string name(const ASTNode& n) { - assert(n.GetValueWidth() ==32); // Widen a constant used in an extract only. + assert(n.GetValueWidth() ==32); + // Widen a constant used in an extract only. if (n == mgr->CreateBVConst(32, bits)) return "width"; @@ -1065,7 +1098,6 @@ name(const ASTNode& n) FatalError("@!#$@#$@#"); } - // Turns "n" into a statement in STP's C++ language to create it. string createString(ASTNode n, map& val) @@ -1073,46 +1105,53 @@ createString(ASTNode n, map& val) if (val.find(n) != val.end()) return val.find(n)->second; - string result =""; + string result = ""; if (n.GetKind() == BVCONST) { if (n.isConstant() && n.GetValueWidth() == 1 && n == mgr->CreateZeroConst(1)) { - result = "bm->CreateZeroConst(1"; + result = "bm->CreateZeroConst(1"; } if (n.isConstant() && n.GetValueWidth() == 1 && n == mgr->CreateOneConst(1)) { - result = "bm->CreateOneConst(1"; + result = "bm->CreateOneConst(1"; } - if (n.isConstant() && (n.GetValueWidth() == bits || n.GetValueWidth() == bits-1)) + if (n.isConstant() && (n.GetValueWidth() == bits)) { stringstream constant; constant << "bm->CreateBVConst(" << bits << "," << n.GetUnsignedConst() << ")"; result += "bm->CreateTerm(BVSX,width," + constant.str() + ""; } + if (n.isConstant() && (n.GetValueWidth() == bits - 1)) + { + stringstream constant; + constant << "bm->CreateBVConst(" << bits - 1 << "," << n.GetUnsignedConst() << ")"; + result += "bm->CreateTerm(BVSX,width-1," + constant.str() + ""; + } + if (n.isConstant() && n.GetValueWidth() == 32) // Extract DEFINATELY. { if (n == mgr->CreateZeroConst(32)) - result += " bm->CreateZeroConst(32 "; + result += " bm->CreateZeroConst(32 "; if (n == mgr->CreateOneConst(32)) - result += " bm->CreateOneConst(32 "; + result += " bm->CreateOneConst(32 "; if (n == mgr->CreateBVConst(32, bits)) - result = " bm->CreateBVConst(32, width "; + result = " bm->CreateBVConst(32, width "; if (n == mgr->CreateBVConst(32, bits - 1)) - result = " bm->CreateBVConst(32, width-1 "; + result = " bm->CreateBVConst(32, width-1 "; if (n == mgr->CreateBVConst(32, bits - 2)) - result = " bm->CreateBVConst(32, width-2 "; + result = " bm->CreateBVConst(32, width-2 "; } - if (result =="") + if (result == "") { // uh oh. result = "~~~~~~~!!!!!!!!~~~~~~~~~~~"; @@ -1134,7 +1173,7 @@ createString(ASTNode n, map& val) ss << name(n[2]) << " +1 - (" << name(n[1]) << "),"; // width. ss << createString(n[0], val) << ","; - ss << "bm->CreateBVConst(32," << name(n[1]) << "),"; // top then bottom. + ss << "bm->CreateBVConst(32," << name(n[1]) << "),"; // top then bottom. ss << "bm->CreateBVConst(32," << name(n[2]) << ")"; result += ss.str(); @@ -1153,13 +1192,13 @@ createString(ASTNode n, map& val) } if (n.GetKind() != BVEXTRACT) - for (int i = 0; i < n.Degree(); i++) - { - if (i > 0) - result += ","; + for (int i = 0; i < n.Degree(); i++) + { + if (i > 0) + result += ","; - result += createString(n[i], val); - } + result += createString(n[i], val); + } result += ")"; val.insert(make_pair(n, result)); @@ -1185,39 +1224,36 @@ visit_all(const ASTNode& n, map& visited, string current) } template -std::string to_string(T i) -{ + std::string + to_string(T i) + { std::stringstream ss; ss << i; return ss.str(); -} - - + } // Write out all the rules that have been discovered to file. void -writeOutRules() +writeOutRules(string fileName) { - removeDuplicates(toWrite); + to_write.rewriteAll(); + to_write.eraseDuplicates(); - vector output; + std::vector output; + std::map dup; - for (int i = 0; i < toWrite.size(); i++) + for (int i = 0; i < to_write.size(); i++) { - if (toWrite[i].isEmpty()) - continue; - - ASTNode to = toWrite[i].to; - ASTNode from = toWrite[i].from; - - if (getDifficulty(to) > getDifficulty(from)) + if (!to_write.toWrite[i].isOK()) { - // Want the easier one on the lhs. Which is the opposite of what you expect.. - ASTNode t = to; - to = from; - from = t; + to_write.toWrite.erase(to_write.toWrite.begin() + i); + i--; + continue; } + ASTNode to = to_write.toWrite[i].getTo(); + ASTNode from = to_write.toWrite[i].getFrom(); + // If the RHS is just part of the LHS, then we output something like children[0][1][0][1] as the RHS. string to_name = getToName(to, from); @@ -1237,33 +1273,52 @@ writeOutRules() val.insert(make_pair(zero, "zero")); // loads all the expressions in the rhs into the list of available expressions. - visit_all(from, val, "children"); + visit_all(from, val, "n"); to_name = createString(to, val); } ASTNodeString names; string current = "n"; - string sofar = "if ( width >= " + to_string(bits) + " " ; + string sofar = "if ( width >= " + to_string(bits) + " "; rule_to_string(from, names, current, sofar); sofar += ") set(result, " + to_name + ");"; + // if (sofar.find("!!!") == std::string::npos && sofar.length() < 500) { - assert(getDifficulty(from) >= getDifficulty(to)); - - if (mgr->ASTTrue == rewriteThroughWithAIGS(toWrite[i].n)) - { - toWrite[i] = ToWrite(mgr->ASTUndefined,mgr->ASTUndefined,0); - continue; - } - { char buf[100]; sprintf(buf, "//%d -> %d | %d ms\n", getDifficulty(from), getDifficulty(to), 0 /*toWrite[i].time*/); sofar += buf; output.push_back(sofar); + + if (dup.find(sofar) != dup.end()) + { + cerr << "-----"; + cerr << sofar; + + ASTNode f = to_write.toWrite[i].getFrom(); + cerr << f << std::endl; + cerr << dup.find(sofar)->second.getFrom(); + + ASTNodeMap fromTo; + + f = renameVars(f); + //cerr << "renamed" << f; + bool result = unifyNode(f,dup.find(sofar)->second.getFrom(),fromTo,2) ; + cerr << "unified" << result << endl; + ASTNodeMap seen; + cerr << rewrite(f,to_write.toWrite[i],seen ); + + // The text of this rule is the same as another rule. + to_write.toWrite.erase(to_write.toWrite.begin() + i); + i--; + continue; + } + else + dup.insert(make_pair(sofar,to_write.toWrite[i])); } } } @@ -1271,7 +1326,7 @@ writeOutRules() // Remove the duplicates from output. removeDuplicates(output); - cerr << "Rules Discovered in total: " << toWrite.size() << endl; + cerr << "Rules Discovered in total: " << to_write.size() << endl; // Group functions of the same kind all together. hash_map, hashF > buckets; @@ -1297,128 +1352,184 @@ writeOutRules() ofstream outputFileSMT2; outputFileSMT2.open("rewrite_data.smt2", ios::trunc); - for (int i = 0; i < toWrite.size(); i++) + for (int i = 0; i < to_write.size(); i++) + { + assert(to_write.toWrite[i].isOK()); + outputFileSMT2 << "; " << "bits:" << bits << "->" << widen_to << " time to verify:" << to_write.toWrite[i].getTime() + << '\n'; + for (int j = widen_to; j < widen_to + 5; j++) { - if (toWrite[i].isEmpty()) - continue; - - outputFileSMT2 << "; " << "bits:" << bits << "->" << widen_to << " time to verify:" << toWrite[i].time << '\n'; - for (int j= widen_to; j < widen_to+ 5;j++) - { - outputFileSMT2 << "(push 1)\n"; - printer::SMTLIB2_PrintBack(outputFileSMT2, mgr->CreateNode(NOT, widen(toWrite[i].n,j)),true,false); - outputFileSMT2 << "(pop 1)\n"; - } + outputFileSMT2 << "(push 1)\n"; + printer::SMTLIB2_PrintBack(outputFileSMT2, mgr->CreateNode(NOT, w), true, false); + outputFileSMT2 << "(pop 1)\n"; } + } - outputFileSMT2.close(); + outputFileSMT2.close(); - outputFileSMT2.open("array.smt2", ios::trunc); - ASTVec v; - for (int i = 0; i < toWrite.size(); i++) - { - if (toWrite[i].isEmpty()) - continue; - - v.push_back(toWrite[i].n); - } + outputFileSMT2.open(fileName.c_str(), ios::trunc); + ASTVec v; + for (int i = 0; i < to_write.size(); i++) + { + v.push_back(to_write.toWrite[i].getN()); + } - if (v.size() > 0) - { - ASTNode n = mgr->CreateNode(AND,v); - printer::SMTLIB2_PrintBack(outputFileSMT2, n,true); - } - outputFileSMT2.close(); + if (v.size() > 0) + { + ASTNode n = mgr->CreateNode(AND, v); + printer::SMTLIB2_PrintBack(outputFileSMT2, n, true); + } + outputFileSMT2.close(); } -// Triples the number of functions by adding all the unary ones. -void -allUnary(ASTVec& functions) -{ - for (int i = 0, size = functions.size(); i < size; i++) - { - if (functions[i] == mgr->ASTUndefined) - continue; +// ASSUMES that buildRewrite() has recently been run on the rules.. - functions.push_back(nf->CreateTerm(BEEV::BVNEG, bits, functions[i])); - functions.push_back(nf->CreateTerm(BEEV::BVUMINUS, bits, functions[i])); - } +ASTNode +rename_then_rewrite(ASTNode n, const Rewrite_rule& original_rule) +{ + n = renameVars(n); + ASTNodeMap seen; + n = rewrite(n,original_rule,seen); + return renameVarsBack(n); } -void -removeNonWidened(ASTVec & functions) +// assumes the variables in n are two characters wide. +ASTNode +rewrite(const ASTNode&n, const Rewrite_rule& original_rule, ASTNodeMap& seen) { - for (int i = 0; i < functions.size(); i++) + if (n.isAtom()) + return n; + + // nb. won't rewrite through EQ etc. + if (n.GetType() != BITVECTOR_TYPE) + return n; + + ASTVec v; + for (int i = 0; i < n.Degree(); i++) + v.push_back(rewrite(n[i],original_rule,seen)); + + assert(v.size() > 0); + ASTNode n2; + + if (v!=n.GetChildren()) + n2 = mgr->CreateTerm(n.GetKind(), n.GetValueWidth(), v); + else + n2 = n; + + ASTNodeMap fromTo; + + vector& rr = + n[0].Degree() > 0 ? + (to_write.kind_kind_to_rr[n.GetKind()][n[0].GetKind()]) : + (to_write.kind_to_rr[n.GetKind()]) ; + + + for (int i = 0; i < rr.size(); i++) { - if (mgr->ASTUndefined == functions[i]) + // If they are the same rule. Then don't match them. + if (original_rule.sameID(rr[i])) continue; - if (mgr->ASTUndefined == widen(functions[i], bits + 1)) - { - functions[i] = mgr->ASTUndefined; // We can't widen it later. So remove it. - continue; - } - } -} + if (fromTo.size() > 0) + fromTo.clear(); -// If there only w variables in the problem. We can delete it because -// we will have another with just v's. -// NB: Can only apply at the top level. -void -removeSingleVariable(ASTVec & functions) -{ - for (int i = 0; i < functions.size(); i++) - { - vector symbols; - ASTNodeSet visited; + const ASTNode& f = rr[i].getFrom(); - getVariables(functions[i], symbols, visited); - if (symbols.size() == 1 && symbols[0] == w) + if (unifyNode(f, n2, fromTo,1)) { - functions[i] = mgr->ASTUndefined; // We can't widen it later. So remove it. - continue; + /* + cerr << "Unifying" << f; + cerr << "with:" << n2; + + cerr << "Now" << rr[i].getTo(); + cerr << "reducing rule" << rr[i].getN(); + + for (ASTNodeMap::iterator it = fromTo.begin(); it != fromTo.end(); it++) + { + cerr << it->first << "to" << it->second << endl; + } + + cerr << "--------------"; + */ + + // This doesn't distinguish between the second time it's seen in the term, and seeing it again. + ASTNodeMap cache; + if (seen.find(n) != seen.end()) + return seen.find(n)->second; + ASTNode r= SubstitutionMap::replace(rr[i].getTo(), fromTo, cache, nf, false, true); + seen.insert(make_pair(n,r)); + ASTNode r2= rewrite(r,original_rule,seen); + seen.erase(n); + seen.insert(make_pair(n,r2)); + return r2; } } + + return n2; } -void -removeSingleUndefined(ASTVec& functions) +// loads the already existing rules. +void loadExistingRules(string fileName) { - for (int i = 0; i < functions.size(); i++) + if(!ifstream(fileName.c_str())) + return; // file doesn't exist. + + smt2in = fopen(fileName.c_str(), "r"); + TypeChecker nfTypeCheckDefault(*mgr->hashingNodeFactory, *mgr); + Cpp_interface piTypeCheckDefault(*mgr, &nfTypeCheckDefault); + parserInterface = &piTypeCheckDefault; + + parserInterface->push(); // so the rules can be de-asserted. + + mgr->GetRunTimes()->start(RunTimes::Parsing); + smt2parse(); + + ASTVec values = piTypeCheckDefault.GetAsserts(); + values = FlattenKind(AND, values); + + cerr << "Rewrite rule size:" << values.size() << endl; + + for (int i = 0; i < values.size(); i++) { - if (functions[i] == mgr->ASTUndefined) + if ((values[i].GetKind() != EQ)) { - functions.erase(functions.begin() + i); - break; + cerr << "Not equality??"; + cerr << values[i]; + continue; } - } -} -void applyBigRewrite(ASTVec& functions) -{ - BEEV::BigRewriter b; + ASTNode from = values[i][0]; + ASTNode to = values[i][1]; - for (int i = 0; i < functions.size(); i++) - { - if (functions[i] == mgr->ASTUndefined) - continue; + // Rule should be orderable. + bool ok = orderEquivalence(from, to); + assert(ok); + Rewrite_rule r(mgr, from, to, 0); + + + if (r.isOK()); + to_write.push_back(r); - ASTNodeMap fromTo; - ASTNode s = b.rewrite(functions[i], fromTo, nf, mgr); - if (s != functions[i]) - { - functions[i] = s; - } } -} + mgr->PopQuery(); + parserInterface->popToFirstLevel(); + parserInterface->cleanUp(); -int -main(void) -{ - startup(); + to_write.buildRules(); + + ASTVec vvv = mgr->GetAsserts(); + for (int i=0; i < vvv.size() ;i++) + cerr << vvv[i]; + + // So we don't output as soon as one is discovered... + lastOutput = to_write.size(); +} +void +testProps() +{ ASTNode a = mgr->CreateSymbol("a", 0, 0); ASTNode b = mgr->CreateSymbol("b", 0, 0); @@ -1433,172 +1544,108 @@ main(void) // Check that the propositions don't evaluate to true/false. for (int k = 0; k < number_types; k++) doProp(propKinds[k], a); +} - /////////////////////////// BV, BV -> BV. - ASTVec functions; - - functions.push_back(w); - functions.push_back(v); - functions.push_back(mgr->CreateBVConst(bits, 0)); - functions.push_back(mgr->CreateBVConst(bits, 1)); - functions.push_back(mgr->CreateMaxConst(bits)); - - // All unary of the leaves. - allUnary(functions); - removeDuplicates(functions); - cerr << "Leaves:" << functions.size() << endl; - - // We've got the leaves, and their unary operations, - // now get the binary operations of all of those. - int size = functions.size(); - for (int i = 0; i < size; i++) - for (int j = 0; j < size; j++) - getAllFunctions(functions[i], functions[j], functions); - - allUnary(functions); - - // Duplicates removed, rewrite rules applied, non-widenable removed, - //removeNonWidened(functions); - //applyBigRewrite(functions); - removeDuplicates(functions); - removeSingleUndefined(functions); +int test() +{ + // Test code. + loadExistingRules("test.smt2"); - cerr << "One Level:" << functions.size() << endl; - applyBigRewrite(functions); - removeDuplicates(functions); - cerr << "After rewrite:" << functions.size() << endl; + v = mgr->LookupOrCreateSymbol("v"); + v.SetValueWidth(bits); - const bool two_level = true; + v0 = mgr->LookupOrCreateSymbol("v0"); + v0.SetValueWidth(bits); - if (two_level) - { - int last = 0; - ASTVec functions_copy(functions); - size = functions_copy.size(); - for (int i = 0; i < size; i++) - for (int j = 0; j < size; j++) - getAllFunctions(functions_copy[i], functions_copy[j], functions); - - //applyBigRewrite(functions); - removeSingleVariable(functions); - removeDuplicates(functions); - removeSingleUndefined(functions); - - // All the unary combinations of the binaries. - //allUnary(functions); - //removeNonWidened(functions); - //removeDuplicates(functions); - cerr << "Two Level:" << functions.size() << endl; - } + w = mgr->LookupOrCreateSymbol("w"); + w.SetValueWidth(bits); - // The hash is generated on these values. - vector values; - findRewrites(functions, values); - writeOutRules(); - - cerr << "Initial:" << bits << " widening to :" << widen_to << endl; - cerr << "Highest disproved @ level: " << highestLevel << endl; - cerr << highestDisproved << endl; + w0 = mgr->LookupOrCreateSymbol("w0"); + w0.SetValueWidth(bits); - return 0; + writeOutRules("test-2.smt2"); + to_write.verifyAllwithSAT(); + to_write.clear(); } - -#if 0 -// Shortcut. Don't examine the rule if it isn't a candidate. -bool -isCandidateSizePreserving(const ASTNode& n) +int +main() { - if (n.GetKind() != EQ) - return false; - - if (n[0].isConstant()) - return true; + startup(); + //test(); + //exit(1); - visited.clear(); - if (lhsInRHS(n[1], n[0])) - return true; + loadExistingRules("array.smt2"); - return false; -} + v = mgr->LookupOrCreateSymbol("v"); + v.SetValueWidth(bits); -ASTNodeSet visited; + v0 = mgr->LookupOrCreateSymbol("v0"); + v0.SetValueWidth(bits); -bool -lhsInRHS(const ASTNode& n, const ASTNode& lookFor) -{ - if (lookFor == n) - return true; + w = mgr->LookupOrCreateSymbol("w"); + w.SetValueWidth(bits); - if (visited.find(n) != visited.end()) - return false; + w0 = mgr->LookupOrCreateSymbol("w0"); + w0.SetValueWidth(bits); - for (int i = 0; i < n.Degree(); i++) - if (lhsInRHS(n[i], lookFor)) - return true; + testProps(); - visited.insert(n); - return false; + findNewRewrites(); + writeOutRules("array.smt2"); + to_write.verifyAllwithSAT(); } int -getDifficulty_approximate(const ASTNode&n) +findNewRewrites() { - if (difficulty_cache.find(n) != difficulty_cache.end()) - return difficulty_cache.find(n)->second; + Function_list functionList; + functionList.buildAll(); - DifficultyScore ds; - int score = ds.score(n); - difficulty_cache.insert(make_pair(n, score)); - return score; + // The hash is generated on these values. + vector values; + findRewrites(functionList.functions, values); + writeOutRules("array.smt2"); + + cerr << "Initial:" << bits << " widening to :" << widen_to << endl; + cerr << "Highest disproved @ level: " << highestLevel << endl; + cerr << highestDisproved << endl; + return 0; } -// Shortcut. Don't examine the rule if it isn't a candidate. + +// Term variables have a specified width!!! bool -isCandidateDifficultyPreserving(const ASTNode& n) +unifyNode(const ASTNode& n0, const ASTNode& n1, ASTNodeMap& fromTo, const int term_variable_width) { - if (n.GetKind() != EQ) - return false; - - if (getDifficulty(n[0]) != getDifficulty(n[1])) + // Pointers to the same value. OK. + if (n0 == n1) return true; - return false; -} + if (n0.GetKind() == SYMBOL && strlen(n0.GetName()) == term_variable_width) + { + if (fromTo.find(n0) != fromTo.end()) + return unifyNode(fromTo.find(n0)->second, n1, fromTo, term_variable_width); -void -getSomeFunctions(ASTNode v, ASTNode w, ASTVec& result) -{ + fromTo.insert(make_pair(n0, n1)); + return unifyNode(fromTo.find(n0)->second, n1, fromTo, term_variable_width); + } - Kind types[] = - { BVMULT, BVDIV, SBVDIV, SBVREM, SBVMOD, BVPLUS, BVMOD }; - int number_types = sizeof(types) / sizeof(Kind); + // Here: + // They could be different BVConsts, different symbols, or + // different functions. - // all two argument functions. - for (int i = 0; i < number_types; i++) - result.push_back(create(types[i], v, w)); -} + if (n0.Degree() != n1.Degree() || (n0.Degree() == 0)) + return false; -// True if "to" is a single function of "n" -bool -single_fn_of(ASTNode from, ASTNode to) -{ - for (int i = 0; i < to.Degree(); i++) - { - if (to[i].isConstant()) - continue; + if (n0.GetKind() != n1.GetKind()) + return false; - // Special case equalities are cheap so allow them through. - if (to[i].GetKind() == EQ && to[i][0].isConstant()) - { - if (!contained_in(to[i][1], from)) - return false; - } - else if (!contained_in(to[i], from)) + for (int i = 0; i < n0.Degree(); i++) + { + if (!unifyNode(n0[i], n1[i], fromTo, term_variable_width)) return false; } + return true; } - - -#endif diff --git a/src/util/find_rewrites/rewrite_data_new.cpp b/src/util/find_rewrites/rewrite_data_new.cpp new file mode 100644 index 0000000..857d570 --- /dev/null +++ b/src/util/find_rewrites/rewrite_data_new.cpp @@ -0,0 +1,102 @@ +if (n.GetKind() == BVPLUS ) +{ +if ( width >= 3 && n.GetKind() == BVPLUS && n.Degree() ==2 && n[0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,1))&& n[1].GetKind() == BVNEG ) set(result, bm->CreateTerm(BVUMINUS,width,n[1][0]));//107 -> 107 | 0 ms +if ( width >= 3 && n.GetKind() == BVPLUS && n.Degree() ==2 && n[0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,1))&& n[1].GetKind() == BVOR && n[1].Degree() ==2 && n[1][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6))) set(result, bm->CreateTerm(BVNEG,width,bm->CreateTerm(SBVMOD,width,n[1][1],children[1][0])));//33 -> 33 | 0 ms +if ( width >= 3 && n.GetKind() == BVPLUS && n.Degree() ==2 && n[0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,1))&& n[1].GetKind() == BVPLUS && n[1].Degree() ==2 ) set(result, bm->CreateTerm(BVNEG,width,bm->CreateTerm(BVPLUS,width,bm->CreateTerm(BVNEG,width,n[1][0]),bm->CreateTerm(BVNEG,width,n[1][1]))));//233 -> 176 | 0 ms +if ( width >= 3 && n.GetKind() == BVPLUS && n.Degree() ==2 && n[0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,1))&& n[1].GetKind() == BVSX && n[1][0].GetKind() == BVEXTRACT && n[1][0][1] == bm->CreateBVConst(32, width-1) && n[1][0][2] == bm->CreateBVConst(32, width-1) && n[1][1] == bm->CreateBVConst(32, width) ) set(result, bm->CreateTerm(BVCONCAT,width,bm->CreateTerm(BVSX,width-1,bm->CreateBVConst(2,0)),bm->CreateTerm(BVNEG,width,children[1][0])));//21 -> 21 | 0 ms +if ( width >= 3 && n.GetKind() == BVPLUS && n.Degree() ==2 && n[0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,1))&& n[1].GetKind() == BVXOR && n[1].Degree() ==2 && n[1][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6))) set(result, bm->CreateTerm(BVUMINUS,width,bm->CreateTerm(BVXOR,width,one,n[1][1])));//107 -> 107 | 0 ms +if ( width >= 3 && n.GetKind() == BVPLUS && n.Degree() ==2 && n[0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,1))&& n[1].GetKind() == SBVMOD && n[1][1] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6))) set(result, bm->CreateTerm(BVNEG,width,bm->CreateTerm(BVOR,width,children[1][1],n[1][0])));//21 -> 21 | 0 ms +if ( width >= 3 && n.GetKind() == BVPLUS && n.Degree() ==2 && n[0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,1))) set(result, bm->CreateTerm(BVNEG,width,bm->CreateTerm(BVPLUS,width,bm->CreateTerm(BVNEG,width,n[1]),bm->CreateTerm(BVNEG,width,n[2]))));//237 -> 176 | 0 ms +if ( width >= 3 && n.GetKind() == BVPLUS && n.Degree() ==2 && n[0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,7))&& n[1].GetKind() == BVMULT && n[1].Degree() ==2 && n[1][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,2))) set(result, bm->CreateTerm(BVNEG,width,bm->CreateTerm(BVMULT,width,bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6)),n[1][1])));//99 -> 99 | 0 ms +if ( width >= 3 && n.GetKind() == BVPLUS && n.Degree() ==2 && n[0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,7))&& n[1].GetKind() == BVMULT && n[1].Degree() ==2 && n[1][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6))) set(result, bm->CreateTerm(BVNEG,width,bm->CreateTerm(BVMULT,width,bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,2)),n[1][1])));//121 -> 45 | 0 ms +if ( width >= 3 && n.GetKind() == BVPLUS && n.Degree() ==2 && n[0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,7))&& n[1].GetKind() == BVNEG ) set(result, bm->CreateTerm(BVNEG,width,bm->CreateTerm(BVPLUS,width,one,n[1][0])));//107 -> 107 | 0 ms +if ( width >= 3 && n.GetKind() == BVPLUS && n.Degree() ==2 && n[0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,7))&& n[1].GetKind() == SBVMOD && n[1][1] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6))) set(result, bm->CreateTerm(BVOR,width,children[1][1],bm->CreateTerm(BVNEG,width,n[1][0])));//21 -> 21 | 0 ms +if ( width >= 3 && n.GetKind() == BVPLUS && n.Degree() ==2 && n[0].GetKind() == BVNEG && n[1].GetKind() == BVUMINUS ) set(result, bm->CreateTerm(BVNEG,width,bm->CreateTerm(BVPLUS,width,n[0][0],n[1][0])));//237 -> 176 | 0 ms +if ( width >= 3 && n.GetKind() == BVPLUS && n.Degree() ==2 && n[0].GetKind() == BVUMINUS && n[1].GetKind() == BVNEG ) set(result, bm->CreateTerm(BVNEG,width,bm->CreateTerm(BVPLUS,width,n[0][0],n[1][0])));//237 -> 176 | 0 ms +if ( width >= 3 && n.GetKind() == BVPLUS && n.Degree() ==2 && n[1].GetKind() == BVUMINUS ) set(result, bm->CreateTerm(BVNEG,width,bm->CreateTerm(BVPLUS,width,n[1][0],bm->CreateTerm(BVNEG,width,n[0]))));//237 -> 176 | 0 ms +} +if (n.GetKind() == BVSRSHIFT ) +{ +if ( width >= 3 && n.GetKind() == BVSRSHIFT && n[0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6))&& n[1].GetKind() == BVUMINUS ) set(result, bm->CreateTerm(BVSRSHIFT,width,children[0],n[1][0]));//66 -> 36 | 0 ms +if ( width >= 3 && n.GetKind() == BVSRSHIFT && n[0].GetKind() == BVNEG ) set(result, bm->CreateTerm(BVNEG,width,bm->CreateTerm(BVSRSHIFT,width,n[0][0],n[1])));//224 -> 224 | 0 ms +if ( width >= 3 && n.GetKind() == BVSRSHIFT && n[1].GetKind() == BVNEG && n[1][0] == n[0] ) set(result, bm->CreateTerm(BVSX,width,bm->CreateTerm(BVEXTRACT,width-1 +1 - (width-1),n[0],bm->CreateBVConst(32,width-1),bm->CreateBVConst(32,width-1)), bm->CreateBVConst(32, width )));//216 -> 33 | 0 ms +} +if (n.GetKind() == BVCONCAT ) +{ +if ( width >= 3 && n.GetKind() == BVCONCAT && n[0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,0))&& n[1].GetKind() == BVEXTRACT && n[1][1] == bm->CreateZeroConst(32) && n[1][2] == bm->CreateZeroConst(32) ) set(result, bm->CreateTerm(BVUMINUS,width,bm->CreateTerm(SBVMOD,width,n[1][0],bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6)))));//21 -> 21 | 0 ms +if ( width >= 3 && n.GetKind() == BVCONCAT && n[0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,0))&& n[1].GetKind() == BVNEG && n[1][0].GetKind() == BVEXTRACT && n[1][0][1] == bm->CreateZeroConst(32) && n[1][0][2] == bm->CreateZeroConst(32) ) set(result, bm->CreateTerm(BVNEG,width,bm->CreateTerm(BVOR,width,bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6)),n[1][0][0])));//21 -> 21 | 0 ms +if ( width >= 3 && n.GetKind() == BVCONCAT && n[0].GetKind() == BVNEG && n[0][0].GetKind() == BVEXTRACT && n[0][0][1] == bm->CreateBVConst(32, width-1) && n[0][0][2] == bm->CreateOneConst(32) && n[1] == bm->CreateZeroConst(1) ) set(result, bm->CreateTerm(BVNEG,width,bm->CreateTerm(BVOR,width,one,n[0][0][0])));//45 -> 45 | 0 ms +} +if (n.GetKind() == ITE ) +{ +if ( width >= 3 && n.GetKind() == ITE && n[0].GetKind() == EQ && n[0][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,0))&& n[1] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,1))&& n[2] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,0))) set(result, bm->CreateTerm(BVNEG,width,bm->CreateTerm(BVSRSHIFT,width,bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6)),n[0][1])));//36 -> 36 | 0 ms +if ( width >= 3 && n.GetKind() == ITE && n[0].GetKind() == EQ && n[0][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,0))&& n[1] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6))&& n[2] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,7))) set(result, bm->CreateTerm(BVSRSHIFT,width,children[1],n[0][1]));//36 -> 36 | 0 ms +if ( width >= 3 && n.GetKind() == ITE && n[0].GetKind() == EQ && n[0][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,7))&& n[1] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,1))&& n[2] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,0))) set(result, bm->CreateTerm(BVNEG,width,bm->CreateTerm(BVSRSHIFT,width,bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6)),bm->CreateTerm(BVNEG,width,n[0][1]))));//36 -> 36 | 0 ms +if ( width >= 3 && n.GetKind() == ITE && n[0].GetKind() == EQ && n[0][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,7))&& n[1] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6))&& n[2] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,7))) set(result, bm->CreateTerm(BVSRSHIFT,width,children[1],bm->CreateTerm(BVNEG,width,n[0][1])));//36 -> 36 | 0 ms +} +if (n.GetKind() == BVDIV ) +{ +if ( width >= 3 && n.GetKind() == BVDIV && n[0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,1))) set(result, bm->CreateTerm(ITE,width,bm->CreateNode(BVGT,bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6)),bm->CreateTerm(BVNEG,width,n[1])),zero,one));//51 -> 35 | 0 ms +} +if (n.GetKind() == SBVDIV ) +{ +if ( width >= 3 && n.GetKind() == SBVDIV && n[0].GetKind() == BVNEG && n[1] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,0))) set(result, bm->CreateTerm(BVUMINUS,width,bm->CreateTerm(SBVDIV,width,n[0][0],zero)));//33 -> 33 | 0 ms +} +if (n.GetKind() == BVMOD ) +{ +if ( width >= 3 && n.GetKind() == BVMOD && n[0].GetKind() == BVUMINUS && n[1].GetKind() == BVNEG && n[1][0] == n[0][0] ) set(result, bm->CreateTerm(SBVREM,width,one,children[1]));//80 -> 80 | 0 ms +} +if (n.GetKind() == SBVMOD ) +{ +if ( width >= 3 && n.GetKind() == SBVMOD && n[0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,1))&& n[1].GetKind() == BVNEG ) set(result, bm->CreateTerm(BVUMINUS,width,bm->CreateTerm(SBVREM,width,n[1][0],children[1])));//187 -> 187 | 0 ms +if ( width >= 3 && n.GetKind() == SBVMOD && n[0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,7))) set(result, bm->CreateTerm(SBVMOD,width,bm->CreateTerm(BVNEG,width,n[1]),n[1]));//204 -> 204 | 0 ms +if ( width >= 3 && n.GetKind() == SBVMOD && n[0].GetKind() == BVPLUS && n[0].Degree() ==2 && n[0][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,7))&& n[1].GetKind() == BVUMINUS && n[1][0] == n[0][1] ) set(result, bm->CreateTerm(SBVMOD,width,bm->CreateTerm(BVNEG,width,n[0][1]),children[1]));//1848 -> 272 | 0 ms +if ( width >= 3 && n.GetKind() == SBVMOD && n[0].GetKind() == BVUMINUS && n[1] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6))) set(result, bm->CreateTerm(SBVMOD,width,n[0][0],children[1]));//33 -> 33 | 0 ms +} +if (n.GetKind() == BVAND ) +{ +if ( width >= 3 && n.GetKind() == BVAND && n.Degree() ==2 && n[0].GetKind() == BVNEG && n[1].GetKind() == BVNEG ) set(result, bm->CreateTerm(BVNEG,width,bm->CreateTerm(BVOR,width,n[0][0],n[1][0])));//79 -> 79 | 0 ms +} +if (n.GetKind() == BVUMINUS ) +{ +if ( width >= 3 && n.GetKind() == BVUMINUS && n[0].GetKind() == BVOR && n[0].Degree() ==2 && n[0][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,1))) set(result, bm->CreateTerm(BVOR,width,one,bm->CreateTerm(BVNEG,width,n[0][1])));//45 -> 45 | 0 ms +if ( width >= 3 && n.GetKind() == BVUMINUS && n[0].GetKind() == BVXOR && n[0].Degree() ==2 && n[0][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6))) set(result, bm->CreateTerm(BVPLUS,width,one,bm->CreateTerm(BVXOR,width,one,n[0][1])));//107 -> 107 | 0 ms +if ( width >= 3 && n.GetKind() == BVUMINUS && n[0].GetKind() == ITE && n[0][0].GetKind() == BVGT && n[0][0][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6))&& n[0][1] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,0))&& n[0][2] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,1))) set(result, bm->CreateTerm(ITE,width,children[0][0],zero,max));//47 -> 47 | 0 ms +if ( width >= 3 && n.GetKind() == BVUMINUS && n[0].GetKind() == SBVDIV && n[0][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,1))) set(result, bm->CreateTerm(SBVDIV,width,max,n[0][1]));//155 -> 155 | 0 ms +if ( width >= 3 && n.GetKind() == BVUMINUS && n[0].GetKind() == SBVDIV && n[0][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,7))) set(result, bm->CreateTerm(SBVDIV,width,one,n[0][1]));//155 -> 155 | 0 ms +if ( width >= 3 && n.GetKind() == BVUMINUS && n[0].GetKind() == SBVMOD && n[0][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,1))) set(result, bm->CreateTerm(SBVREM,width,bm->CreateTerm(BVNEG,width,n[0][1]),n[0][1]));//244 -> 244 | 0 ms +if ( width >= 3 && n.GetKind() == BVUMINUS && n[0].GetKind() == SBVMOD && n[0][0].GetKind() == BVNEG && n[0][1] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6))) set(result, bm->CreateTerm(BVNEG,width,bm->CreateTerm(BVOR,width,children[0][1],n[0][0][0])));//21 -> 21 | 0 ms +if ( width >= 3 && n.GetKind() == BVUMINUS && n[0].GetKind() == SBVREM && n[0][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,1))) set(result, bm->CreateTerm(SBVREM,width,max,n[0][1]));//92 -> 92 | 0 ms +if ( width >= 3 && n.GetKind() == BVUMINUS && n[0].GetKind() == SBVREM && n[0][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,7))) set(result, bm->CreateTerm(SBVREM,width,one,n[0][1]));//80 -> 80 | 0 ms +if ( width >= 3 && n.GetKind() == BVUMINUS && n[0].GetKind() == SBVREM && n[0][0].GetKind() == BVNEG && n[0][1] == n[0][0][0] ) set(result, bm->CreateTerm(SBVMOD,width,one,n[0][0][0]));//187 -> 187 | 0 ms +} +if (n.GetKind() == SBVREM ) +{ +if ( width >= 3 && n.GetKind() == SBVREM && n[0].GetKind() == BVUMINUS && n[1] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6))) set(result, bm->CreateTerm(BVUMINUS,width,bm->CreateTerm(SBVREM,width,n[0][0],children[1])));//55 -> 39 | 0 ms +} +if (n.GetKind() == BVNEG ) +{ +if ( width >= 3 && n.GetKind() == BVNEG && n[0].GetKind() == BVAND && n[0].Degree() ==2 && n[0][1].GetKind() == BVNEG ) set(result, bm->CreateTerm(BVOR,width,n[0][1][0],bm->CreateTerm(BVNEG,width,n[0][0])));//79 -> 79 | 0 ms +if ( width >= 3 && n.GetKind() == BVNEG && n[0].GetKind() == BVCONCAT && n[0][0].GetKind() == BVEXTRACT && n[0][0][1] == bm->CreateBVConst(32, width-1) && n[0][0][2] == bm->CreateOneConst(32) && n[0][1] == bm->CreateZeroConst(1) ) set(result, bm->CreateTerm(BVUMINUS,width,bm->CreateTerm(BVOR,width,one,n[0][0][0])));//45 -> 45 | 0 ms +if ( width >= 3 && n.GetKind() == BVNEG && n[0].GetKind() == BVMULT && n[0].Degree() ==2 && n[0][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,2))&& n[0][1].GetKind() == BVNEG ) set(result, bm->CreateTerm(BVPLUS,width,one,bm->CreateTerm(BVMULT,width,children[0][0],n[0][1][0])));//45 -> 45 | 0 ms +if ( width >= 3 && n.GetKind() == BVNEG && n[0].GetKind() == BVOR && n[0].Degree() ==2 && n[0][1].GetKind() == BVNEG ) set(result, bm->CreateTerm(BVAND,width,n[0][1][0],bm->CreateTerm(BVNEG,width,n[0][0])));//79 -> 79 | 0 ms +if ( width >= 3 && n.GetKind() == BVNEG && n[0].GetKind() == BVPLUS && n[0].Degree() ==2 && n[0][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6))&& n[0][1].GetKind() == BVNEG ) set(result, bm->CreateTerm(BVPLUS,width,bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,2)),n[0][1][0]));//103 -> 103 | 0 ms +if ( width >= 3 && n.GetKind() == BVNEG && n[0].GetKind() == BVXOR && n[0].Degree() ==2 && n[0][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6))) set(result, bm->CreateTerm(BVXOR,width,one,n[0][1]));//49 -> 49 | 0 ms +if ( width >= 3 && n.GetKind() == BVNEG && n[0].GetKind() == BVXOR && n[0].Degree() ==2 ) set(result, bm->CreateTerm(BVXOR,width,n[0][0],bm->CreateTerm(BVNEG,width,n[0][1])));//89 -> 89 | 0 ms +if ( width >= 3 && n.GetKind() == BVNEG && n[0].GetKind() == ITE && n[0][0].GetKind() == BVGT && n[0][0][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6))&& n[0][1] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,0))&& n[0][2] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,1))) set(result, bm->CreateTerm(ITE,width,children[0][0],max,children[0][0][0]));//35 -> 35 | 0 ms +if ( width >= 3 && n.GetKind() == BVNEG && n[0].GetKind() == SBVMOD && n[0][1] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6))) set(result, bm->CreateTerm(SBVMOD,width,bm->CreateTerm(BVNEG,width,n[0][0]),children[0][1]));//33 -> 33 | 0 ms +} +if (n.GetKind() == BVXOR ) +{ +if ( width >= 3 && n.GetKind() == BVXOR && n.Degree() ==2 && n[0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,1))&& n[1].GetKind() == BVNEG ) set(result, bm->CreateTerm(BVXOR,width,bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6)),n[1][0]));//49 -> 49 | 0 ms +if ( width >= 3 && n.GetKind() == BVXOR && n.Degree() ==2 && n[0].GetKind() == BVNEG && n[1].GetKind() == BVPLUS && n[1].Degree() ==2 && n[1][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,7))) set(result, bm->CreateTerm(BVXOR,width,n[0][0],bm->CreateTerm(BVUMINUS,width,n[1][1])));//150 -> 150 | 0 ms +if ( width >= 3 && n.GetKind() == BVXOR && n.Degree() ==2 && n[0].GetKind() == BVNEG && n[1].GetKind() == BVUMINUS ) set(result, bm->CreateTerm(BVNEG,width,bm->CreateTerm(BVXOR,width,n[0][0],children[1])));//150 -> 150 | 0 ms +if ( width >= 3 && n.GetKind() == BVXOR && n.Degree() ==2 && n[0].GetKind() == BVUMINUS && n[1].GetKind() == BVNEG ) set(result, bm->CreateTerm(BVNEG,width,bm->CreateTerm(BVXOR,width,n[1][0],children[0])));//150 -> 150 | 0 ms +if ( width >= 3 && n.GetKind() == BVXOR && n.Degree() ==2 && n[1].GetKind() == BVNEG ) set(result, bm->CreateTerm(BVNEG,width,bm->CreateTerm(BVXOR,width,n[1][0],n[0])));//89 -> 89 | 0 ms +if ( width >= 3 && n.GetKind() == BVXOR && n.Degree() ==2 && n[1].GetKind() == BVPLUS && n[1].Degree() ==2 && n[1][0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,7))) set(result, bm->CreateTerm(BVXOR,width,bm->CreateTerm(BVNEG,width,n[0]),bm->CreateTerm(BVUMINUS,width,n[1][1])));//150 -> 150 | 0 ms +} +if (n.GetKind() == BVOR ) +{ +if ( width >= 3 && n.GetKind() == BVOR && n.Degree() ==2 && n[0] == bm->CreateTerm(BVSX,width,bm->CreateBVConst(3,6))&& n[1].GetKind() == BVUMINUS ) set(result, bm->CreateTerm(BVOR,width,children[0],n[1][0]));//21 -> 21 | 0 ms +if ( width >= 3 && n.GetKind() == BVOR && n.Degree() ==2 && n[0].GetKind() == BVNEG && n[1].GetKind() == BVNEG ) set(result, bm->CreateTerm(BVNEG,width,bm->CreateTerm(BVAND,width,n[0][0],n[1][0])));//79 -> 79 | 0 ms +} diff --git a/src/util/find_rewrites/rewrite_rule.h b/src/util/find_rewrites/rewrite_rule.h new file mode 100644 index 0000000..2f0b2a6 --- /dev/null +++ b/src/util/find_rewrites/rewrite_rule.h @@ -0,0 +1,146 @@ +#ifndef REWRITERULE_H +#define REWRITERULE_H + +#include "../../STPManager/STPManager.h" + +extern const int widen_to; +extern const int bits; + +ASTNode +widen(const ASTNode& w, int width); + +vector +getVariables(const ASTNode& n); + +class Rewrite_rule +{ +private: + ASTNode from; + ASTNode to; + ASTNode n; + + int id; + + static int static_id; + +public: + + int time; + + const ASTNode& + getFrom() const + {return from;} + + const ASTNode& + getTo() const + {return to;} + + int + getTime() const + {return time;} + + ASTNode + getN() const + { + return n; + } + + bool + sameID(const Rewrite_rule& t) const + { + if (id == t.id) + { + assert(n == t.n); + return true; + } + return false; + } + + bool + operator==(const Rewrite_rule& t) const + { + return (n == t.n); + } + + bool + isOK() + { + if (getN().GetKind() != EQ) + return false; + + ASTNode w = widen(getN(), widen_to); + + BVTypeCheckRecursive(n); + BVTypeCheckRecursive(w); + + if (w.IsNull() || w.GetKind() == UNDEFINED) + return false; + + if (from.isAtom() && to.isAtom()) + return false; + + if (from == to) + return false; + + return true; + + } + + Rewrite_rule(BEEV::STPMgr* bm, const BEEV::ASTNode& from_, const BEEV::ASTNode& to_, const int t) + : from(from_), to(to_), n ( bm->CreateNode(BEEV::EQ,to_,from_)) + { + id = static_id++; + + time = t; + + //// + assert(!from.IsNull()); + assert(from.GetKind() != UNDEFINED); + + //// + assert(!to.IsNull()); + assert(to.GetKind() != UNDEFINED); + + //// + assert(!n.IsNull()); + assert(n.GetKind() != UNDEFINED); + //// + + if (from.GetKind() == SYMBOL) + { + assert(to == from); // If it's a symbol. It should be the same one. + } + + if (from.isAtom()) + { + assert(to.isAtom()); // sometimes its easiest to make it 0->0 rather than deleting it. + } + + // only v or w + vector s_from= getVariables(from); + for (vector::iterator it = s_from.begin(); it != s_from.end() ;it++) + { + assert(strlen(it->GetName()) ==1); + assert(it->GetName()[0] =='v' || it->GetName()[0] =='w'); + assert(it->GetValueWidth() == bits); + } + + vector s_to= getVariables(to); + for (vector::iterator it = s_to.begin(); it != s_to.end() ;it++) + { + assert(strlen(it->GetName()) ==1); + assert(it->GetName()[0] =='v' || it->GetName()[0] =='w'); + assert(it->GetValueWidth() == bits); + } + + // The "to" side should have fewer nodes. + assert(s_from.size() >= s_to.size()); + } + + bool + operator<(const Rewrite_rule& t) const + { + return (n < t.n); + } +}; +#endif diff --git a/src/util/find_rewrites/rewrite_system.h b/src/util/find_rewrites/rewrite_system.h new file mode 100644 index 0000000..a9785f2 --- /dev/null +++ b/src/util/find_rewrites/rewrite_system.h @@ -0,0 +1,190 @@ +#ifndef REWRITESYSTEM_H +#define REWRITESYSTEM_H + +#include "rewrite_rule.h" + +extern const int widen_to; +extern ASTNode v, v0, w, w0; +extern NodeFactory* nf; +extern BEEV::STPMgr* mgr; + +bool +orderEquivalence(ASTNode& from, ASTNode& to); + +ASTNode +create(Kind k, const ASTNode& n0, const ASTNode& n1); + + +template + void + removeDuplicates(T & big); + +ASTNode +widen(const ASTNode& w, int width); + +bool +unifyNode(const ASTNode& n0, const ASTNode& n1, ASTNodeMap& fromTo); + +ASTNode +renameVars(const ASTNode &n); + +ASTNode +rewrite(const ASTNode&n, const Rewrite_rule& original_rule, ASTNodeMap& seen); + +bool +checkRule(const ASTNode & from, const ASTNode & to, VariableAssignment& assignment, bool&bad); + +ASTNode +renameVarsBack(const ASTNode &n); + +ASTNode +rename_then_rewrite(ASTNode n, const Rewrite_rule& original_rule); + +bool +isConstantToSat(const ASTNode & query); + + +class Rewrite_system +{ +private: + + friend void writeOutRules(string fileName); + + friend ASTNode rewrite(const ASTNode&n, const Rewrite_rule& original_rule, ASTNodeMap& seen); + + // Rules to write out when we get the chance. + vector toWrite; + std::map< Kind, vector > kind_to_rr; + std::map< Kind, std::map< Kind, vector > > kind_kind_to_rr; + +public: + + Rewrite_system() + { + } + + void + buildRules() + { + kind_to_rr.clear(); + kind_kind_to_rr.clear(); + + for (int i = 0; i < toWrite.size(); i++) + { + ASTNode from = toWrite[i].getFrom(); + kind_to_rr[from.GetKind()].push_back(toWrite[i]); + + if (from[0].Degree() > 0) + kind_kind_to_rr[from.GetKind()][from[0].GetKind()].push_back(toWrite[i]); + } + } + + void + eraseDuplicates() + { + removeDuplicates(toWrite); + } + + void + push_back(Rewrite_rule rr) + { + toWrite.push_back(rr); + } + + int + size() const + { + return toWrite.size(); + } + + ASTNode rewriteNode(ASTNode n) + { + Rewrite_rule null_rule( Rewrite_rule(mgr,mgr->CreateZeroConst(1), mgr->CreateZeroConst(1),0)); + return rename_then_rewrite(n,null_rule); + } + + void + rewriteAll() + { + eraseDuplicates(); + cerr << "Size before rewriteAll:" << toWrite.size() << endl; + + buildRules(); + + for (int i = 0; i < toWrite.size(); i++) + { + if (i % 1000 == 0) + cerr << "rewrite all:" << i << " of " << toWrite.size() << endl; + + if (!toWrite[i].isOK()) + { + toWrite.erase(toWrite.begin() + i); + i--; + continue; + } + + ASTNode n = renameVars(toWrite[i].getFrom()); + ASTNodeMap seen; + ASTNode rewritten_from = rewrite(n, toWrite[i],seen); + + if (n != rewritten_from) + { + assert (isConstantToSat(create(EQ, rewritten_from,n))); + + rewritten_from = renameVarsBack(rewritten_from); + ASTNode to = toWrite[i].getTo(); + bool r = orderEquivalence(rewritten_from, to); + if (r) + { + Rewrite_rule rr(mgr, rewritten_from, to, 0); + if (rr.isOK()) + { + toWrite[i] = rr; + buildRules(); // Otherwise two rules will remove each other? + } + else + { + cout << "Erasing rule"; + toWrite.erase(toWrite.begin() + i); + i--; + } + } + else + { + cerr << "Mapped but couldn't order"; + cerr << rewritten_from << to; + } + } + } + + eraseDuplicates(); + cerr << "Size after rewriteAll:" << toWrite.size() << endl; + } + + void clear() + { + toWrite.clear(); + } + + void + verifyAllwithSAT() + { + for (int i = 0; i < toWrite.size(); i++) + { + VariableAssignment assignment; + bool bad = false; + const int st = getCurrentTime(); + bool r = checkRule(toWrite[i].getFrom(), toWrite[i].getTo(), assignment, bad); + if (!r || bad) + { + cerr << "Bad to, then from" << endl; + cerr << toWrite[i].getFrom(); + cerr << toWrite[i].getTo(); + assert(r); + assert(!bad); + } + toWrite[i].time = getCurrentTime() - st; + } + } +}; +#endif -- 2.47.3