From c89492a8484e1f9ae765c5878cd5cee05796791b Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 14 Mar 2012 14:11:17 +0000 Subject: [PATCH] Miscellaneous fixes to rewrite generation. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1593 e59a4935-1847-0410-ae03-e826735625c1 --- src/util/find_rewrites/rewrite.cpp | 139 +++++++++++++++++++----- src/util/find_rewrites/rewrite_rule.h | 7 +- src/util/find_rewrites/rewrite_system.h | 26 +++-- 3 files changed, 130 insertions(+), 42 deletions(-) diff --git a/src/util/find_rewrites/rewrite.cpp b/src/util/find_rewrites/rewrite.cpp index c6287fe..2da4758 100644 --- a/src/util/find_rewrites/rewrite.cpp +++ b/src/util/find_rewrites/rewrite.cpp @@ -40,9 +40,6 @@ ASTNode highestDisproved; int highestLevel = 0; int discarded = 0; -//static -int Rewrite_rule::static_id; - ////////////////////////////////// const int bits = 6; const int widen_to = 10; @@ -64,6 +61,10 @@ Rewrite_system rewrite_system; void clearSAT(); +bool +is_subgraph(const ASTNode& g, const ASTNode& h); + + void createVariables(); @@ -96,7 +97,6 @@ typedef HASHMAP BEEV::STPMgr* mgr; NodeFactory* nf; -NodeFactory* simpNf; SATSolver * ss; ASTNodeSet stored; // Store nodes so they aren't garbage collected. @@ -343,10 +343,16 @@ widen(const ASTNode& w, int width) return w; if (w.isConstant() && w.GetValueWidth() == bits) - return nf->CreateTerm(BVSX, width, w); + { + ASTNode width_n = mgr->CreateBVConst(32,width); + return nf->CreateTerm(BVSX, width, w,width_n); + } if (w.isConstant() && w.GetValueWidth() == bits - 1) - return nf->CreateTerm(BVSX, width - 1, w); + { + ASTNode width_n = mgr->CreateBVConst(32,width-1); + return nf->CreateTerm(BVSX, width-1, w,width_n); + } if (w.isConstant() && w.GetValueWidth() == 32) // Extract DEFINATELY. { @@ -416,9 +422,59 @@ widen(const ASTNode& w, int width) return result; } +/* + * Accepts t_0 -> t_1, + * when: + * 1) t_0 and t_1 aren't the syntactically equal. + * 2) t_1 is a constant (t_0 isn't). + * 3) t_1 is a subgraph of t_0. + */ bool orderEquivalence(ASTNode& from, ASTNode& to) +{ + if(from.IsNull()) + return false; + if(from.GetKind() == UNDEFINED) + return false; + if(to.IsNull()) + return false; + if(to.GetKind() == UNDEFINED) + return false; + + if (from == to) + return false; + + if (from.isConstant()) + { + assert(!to.isConstant()); + swap(from,to); + return true; + } + + if (to.isConstant()) + { + assert(!from.isConstant()); + return true; + } + + if (is_subgraph(to,from)) + { + return true; + } + + if (is_subgraph(from,to)) + { + swap(from,to); + return true; + } + + return false; +} + + +bool +orderEquivalence_not_yet(ASTNode& from, ASTNode& to) { if(from.IsNull()) return false; @@ -681,9 +737,8 @@ startup() GlobalSTP = new STP(mgr, simp, at, tosat, abs); - simpNf = new SimplifyingNodeFactory(*(mgr->hashingNodeFactory), *mgr); - nf = new TypeChecker(*simpNf, *mgr); - mgr->defaultNodeFactory = simpNf; + mgr->defaultNodeFactory = new SimplifyingNodeFactory (*mgr->hashingNodeFactory, *mgr); + nf = new TypeChecker(*mgr->defaultNodeFactory, *mgr); mgr->UserFlags.stats_flag = false; mgr->UserFlags.optimize_flag = true; @@ -822,6 +877,21 @@ is_candidate(ASTNode from, ASTNode to) return false; } +bool +is_subgraph(const ASTNode& g, const ASTNode& h) +{ + if (g==h) + return true; + + for (int i = 0; i < h.Degree(); i++) + if (is_subgraph(g,h[i])) + return true; + + return false; + } + + + bool lessThan(const ASTNode& n1, const ASTNode& n2) { @@ -962,14 +1032,7 @@ findRewrites(ASTVec& expressions, const vector& values, cons // We've added it. Now the lhs should map to the rhs. // Sometimes it doesn't. Not sure why.. - if(t != rewrite_system.rewriteNode(f)) - { - cerr << "!!!!!!!!!Term doesn't map to itself"; - cerr << f; - cerr << t; - cerr << rewrite_system.rewriteNode(f); - - } + assert(t == rewrite_system.rewriteNode(f)); // Remove the more difficult expression. if (f == equiv[i]) @@ -1602,22 +1665,45 @@ rewrite(const ASTNode&n, const Rewrite_rule& original_rule, ASTNodeMap& seen, in cerr << "--------------"; } - ASTNodeMap::const_iterator it; - if ((it = seen.find(n2)) != seen.end()) - return it->second; - // The substitution map replace should never infinite loop. ASTNodeMap cache; ASTNode r = SubstitutionMap::replace(rr[i].getTo(), fromTo, cache, nf, false, true); + + if (debug_usr2 && (getDifficulty(n2) < getDifficulty(r))) + { + cerr << rr[i].getFrom() << rr[i].getTo(); + cerr << getDifficulty(rr[i].getFrom()) << "to" << getDifficulty(rr[i].getTo()) << "\n"; + cerr << n2 << r; + cerr << getDifficulty(n2) << "to" << getDifficulty(r); + assert (getDifficulty(n2) >= getDifficulty(r)); + } + seen.insert(make_pair(n2, r)); + if (debug_usr2) + { + cerr << "Term after replacing (1/2) :"; + cerr << n2 << ":" << r; + } + r = rewrite(r, original_rule, seen, depth + 1); seen.erase(n2); seen.insert(make_pair(n2, r)); + if (debug_usr2) + { + cerr << "inserting (2/2)" << n2 << r; + cerr << "+++++++!!!!!!!!!!++++++++"; + } + return r; } } + if (debug_usr2) + { + cerr << "^^^^^^^^"; + cerr << "Matches Nothing" << n2; + } return n2; } @@ -1744,6 +1830,7 @@ load_new_rules(const string fileName = "rules_new.smt2") smt2lex_destroy(); parserInterface->cleanUp(); + parserInterface = NULL; if (opended) { cout << "New Style Rules Loaded:" << rewrite_system.size() << endl; @@ -1793,6 +1880,7 @@ void t2() createVariables(); ASTNode r = rename_then_rewrite(n,Rewrite_rule::getNullRule()); cerr << r; + parserInterface = NULL; } @@ -1850,6 +1938,7 @@ void load_old_rules(string fileName) mgr->PopQuery(); parserInterface->popToFirstLevel(); parserInterface->cleanUp(); + parserInterface = NULL; rewrite_system.buildLookupTable(); @@ -2007,14 +2096,6 @@ main(int argc, const char* argv[]) rewrite_system.rewriteAll(); writeOutRules(); // have the times now.. } - else if (argc == 2 && !strcmp("renumber",argv[1])) - { - // Intended to merge two sets of rules, then renumber them. - load_new_rules(); - createVariables(); - rewrite_system.renumber(); - writeOutRules(); - } else if (argc == 2 && !strcmp("test",argv[1])) { testProps(); diff --git a/src/util/find_rewrites/rewrite_rule.h b/src/util/find_rewrites/rewrite_rule.h index d135f94..5c4bc8b 100644 --- a/src/util/find_rewrites/rewrite_rule.h +++ b/src/util/find_rewrites/rewrite_rule.h @@ -19,8 +19,6 @@ class Rewrite_rule ASTNode to; ASTNode n; - static int static_id; - int time_to_verify; int verified_to_bits; @@ -40,7 +38,6 @@ public: return Rewrite_rule(); } - int id; void writeOut(ostream& outputFileSMT2) const { outputFileSMT2 << ";id:0" @@ -98,13 +95,15 @@ public: Rewrite_rule(BEEV::STPMgr* bm, const BEEV::ASTNode& from_, const BEEV::ASTNode& to_, const int t, int _id=-1) : from(from_), to(to_) { - if (_id ==-1) +#if 0 + if (_id ==-1) id = static_id++; else { id =_id; // relied on to be unique. So be careful. static_id =id+1; // assuming we are loading them all up.. } +#endif verified_to_bits = 0; time_to_verify = t; diff --git a/src/util/find_rewrites/rewrite_system.h b/src/util/find_rewrites/rewrite_system.h index a389580..1e21ba4 100644 --- a/src/util/find_rewrites/rewrite_system.h +++ b/src/util/find_rewrites/rewrite_system.h @@ -85,6 +85,23 @@ private: public: + bool + checkInvariant() + { + int size=0; + std::map< Kind, vector >::iterator it; + for(it=kind_to_rr.begin();it != kind_to_rr.end();it++) + { + for (int i=0; i < it->second.size();i++) + { + assert(it->second[i].getFrom().GetKind() == it->first); // All have the same kind as the lookup kind. + } + size+= it->second.size(); + } + + return size == toWrite.size(); + } + Rewrite_system() { lookups_invalid = false; @@ -107,15 +124,6 @@ public: return lookups_invalid; } - void - renumber() - { - int id=0; - for (RewriteRuleContainer::iterator it = toWrite.begin() ; it != toWrite.end(); it++) - it->id = id++; - lookups_invalid=true; - } - void buildLookupTable() { -- 2.47.3