diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/kinds | 21 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.cpp | 40 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.h | 12 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 133 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/rewrite_engine.cpp | 309 | ||||
-rw-r--r-- | src/theory/quantifiers/rewrite_engine.h | 86 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers_type_rules.h | 85 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 21 | ||||
-rw-r--r-- | src/theory/term_registration_visitor.cpp | 4 |
10 files changed, 19 insertions, 693 deletions
diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds index dc11ed562..1534d2d4d 100644 --- a/src/theory/quantifiers/kinds +++ b/src/theory/quantifiers/kinds @@ -55,25 +55,4 @@ typerule INST_ATTRIBUTE ::CVC4::theory::quantifiers::QuantifierInstAttributeType typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule typerule INST_CLOSURE ::CVC4::theory::quantifiers::QuantifierInstClosureTypeRule -# for rewrite rules -# types... -sort RRHB_TYPE \ - Cardinality::INTEGERS \ - not-well-founded \ - "head and body of the rule type (for rewrite-rules theory)" - -# operators... - -# variables, guards, RR_REWRITE/REDUCTION_RULE/DEDUCTION_RULE -operator REWRITE_RULE 3 "general rewrite rule (for rewrite-rules theory)" -#HEAD/BODY/TRIGGER -operator RR_REWRITE 2:3 "actual rewrite rule (for rewrite-rules theory)" -operator RR_REDUCTION 2:3 "actual reduction rule (for rewrite-rules theory)" -operator RR_DEDUCTION 2:3 "actual deduction rule (for rewrite-rules theory)" - -typerule REWRITE_RULE ::CVC4::theory::quantifiers::RewriteRuleTypeRule -typerule RR_REWRITE ::CVC4::theory::quantifiers::RRRewriteTypeRule -typerule RR_REDUCTION ::CVC4::theory::quantifiers::RRRedDedTypeRule -typerule RR_DEDUCTION ::CVC4::theory::quantifiers::RRRedDedTypeRule - endtheory diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index 0e6eb1581..af4011bd9 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -16,7 +16,6 @@ #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" -#include "theory/quantifiers/rewrite_engine.h" #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" @@ -80,12 +79,6 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve Trace("quant-attr-debug") << "Set instantiation level " << n << " to " << lvl << std::endl; QuantInstLevelAttribute qila; n.setAttribute( qila, lvl ); - }else if( attr=="rr-priority" ){ - Assert(node_values.size() == 1); - uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong(); - Trace("quant-attr-debug") << "Set rewrite rule priority " << n << " to " << lvl << std::endl; - RrPriorityAttribute rrpa; - n.setAttribute( rrpa, lvl ); }else if( attr=="quant-elim" ){ Trace("quant-attr-debug") << "Set quantifier elimination " << n << std::endl; QuantElimAttribute qea; @@ -97,21 +90,6 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve } } -bool QuantAttributes::checkRewriteRule( Node q ) { - return !getRewriteRule( q ).isNull(); -} - -Node QuantAttributes::getRewriteRule( Node q ) { - if (q.getKind() == FORALL && q.getNumChildren() == 3 - && q[2][0].getNumChildren() > 0 - && q[2][0][0].getKind() == REWRITE_RULE) - { - return q[2][0][0]; - }else{ - return Node::null(); - } -} - bool QuantAttributes::checkFunDef( Node q ) { return !getFunDefHead( q ).isNull(); } @@ -275,10 +253,6 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){ qa.d_qinstLevel = avar.getAttribute(QuantInstLevelAttribute()); Trace("quant-attr") << "Attribute : quant inst level " << qa.d_qinstLevel << " : " << q << std::endl; } - if( avar.hasAttribute(RrPriorityAttribute()) ){ - qa.d_rr_priority = avar.getAttribute(RrPriorityAttribute()); - Trace("quant-attr") << "Attribute : rr priority " << qa.d_rr_priority << " : " << q << std::endl; - } if( avar.getAttribute(QuantElimAttribute()) ){ Trace("quant-attr") << "Attribute : quantifier elimination : " << q << std::endl; qa.d_quant_elim = true; @@ -294,11 +268,6 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){ qa.d_qid_num = avar; Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num.getAttribute(QuantIdNumAttribute()) << " : " << q << std::endl; } - if( avar.getKind()==REWRITE_RULE ){ - Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl; - Assert(i == 0); - qa.d_rr = avar; - } } } } @@ -349,15 +318,6 @@ int QuantAttributes::getQuantInstLevel( Node q ) { } } -int QuantAttributes::getRewriteRulePriority( Node q ) { - std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); - if( it==d_qattr.end() ){ - return -1; - }else{ - return it->second.d_rr_priority; - } -} - bool QuantAttributes::isQuantElim( Node q ) { std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); if( it==d_qattr.end() ){ diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 827c5e7f4..fc0f85956 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -111,7 +111,6 @@ struct QAttributes d_conjecture(false), d_axiom(false), d_sygus(false), - d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false) @@ -120,9 +119,6 @@ struct QAttributes ~QAttributes(){} /** does the quantified formula have a pattern? */ bool d_hasPattern; - /** if non-null, this is the rewrite rule representation of the quantified - * formula */ - Node d_rr; /** is this formula marked a conjecture? */ bool d_conjecture; /** is this formula marked an axiom? */ @@ -134,8 +130,6 @@ struct QAttributes bool d_sygus; /** side condition for sygus conjectures */ Node d_sygusSideCondition; - /** if a rewrite rule, then this is the priority value for the rewrite rule */ - int d_rr_priority; /** stores the maximum instantiation level allowed for this quantified formula * (-1 means allow any) */ int d_qinstLevel; @@ -150,8 +144,6 @@ struct QAttributes Node d_name; /** the quantifier id associated with this formula */ Node d_qid_num; - /** is this quantified formula a rewrite rule? */ - bool isRewriteRule() const { return !d_rr.isNull(); } /** is this quantified formula a function definition? */ bool isFunDef() const { return !d_fundef_f.isNull(); } /** @@ -193,10 +185,6 @@ public: /** compute the attributes for q */ void computeAttributes(Node q); - /** is quantifier treated as a rewrite rule? */ - static bool checkRewriteRule( Node q ); - /** get the rewrite rule associated with the quanfied formula */ - static Node getRewriteRule( Node q ); /** is fun def */ static bool checkFunDef( Node q ); /** is fun def */ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index e35595287..e2ee99ceb 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -185,15 +185,13 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { //compute attributes QAttributes qa; QuantAttributes::computeQuantAttributes( in, qa ); - if( !qa.isRewriteRule() ){ - for( int op=0; op<COMPUTE_LAST; op++ ){ - if( doOperation( in, op, qa ) ){ - ret = computeOperation( in, op, qa ); - if( ret!=in ){ - rew_op = op; - status = REWRITE_AGAIN_FULL; - break; - } + for( int op=0; op<COMPUTE_LAST; op++ ){ + if( doOperation( in, op, qa ) ){ + ret = computeOperation( in, op, qa ); + if( ret!=in ){ + rew_op = op; + status = REWRITE_AGAIN_FULL; + break; } } } @@ -2088,102 +2086,6 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut } } - -Node QuantifiersRewriter::rewriteRewriteRule( Node r ) { - Kind rrkind = r[2].getKind(); - - //guards, pattern, body - - // Replace variables by Inst_* variable and tag the terms that contain them - std::vector<Node> vars; - vars.reserve(r[0].getNumChildren()); - for( Node::const_iterator v = r[0].begin(); v != r[0].end(); ++v ){ - vars.push_back(*v); - }; - - // Body/Remove_term/Guards/Triggers - Node body = r[2][1]; - TNode new_terms = r[2][1]; - std::vector<Node> guards; - std::vector<Node> pattern; - Node true_node = NodeManager::currentNM()->mkConst(true); - // shortcut - TNode head = r[2][0]; - switch(rrkind){ - case kind::RR_REWRITE: - // Equality - pattern.push_back( head ); - body = head.eqNode(body); - break; - case kind::RR_REDUCTION: - case kind::RR_DEDUCTION: - // Add head to guards and pattern - switch(head.getKind()){ - case kind::AND: - for( unsigned i = 0; i<head.getNumChildren(); i++ ){ - guards.push_back(head[i]); - pattern.push_back(head[i]); - } - break; - default: - if( head!=true_node ){ - guards.push_back(head); - pattern.push_back( head ); - } - break; - } - break; - default: Unreachable() << "RewriteRules can be of only three kinds"; break; - } - // Add the other guards - TNode g = r[1]; - switch(g.getKind()){ - case kind::AND: - for( unsigned i = 0; i<g.getNumChildren(); i++ ){ - guards.push_back(g[i]); - } - break; - default: - if( g != true_node ){ - guards.push_back( g ); - } - break; - } - // Add the other triggers - if( r[2].getNumChildren() >= 3 ){ - for( unsigned i=0; i<r[2][2][0].getNumChildren(); i++ ) { - pattern.push_back( r[2][2][0][i] ); - } - } - - Trace("rr-rewrite") << "Rule is " << r << std::endl; - Trace("rr-rewrite") << "Head is " << head << std::endl; - Trace("rr-rewrite") << "Patterns are "; - for( unsigned i=0; i<pattern.size(); i++ ){ - Trace("rr-rewrite") << pattern[i] << " "; - } - Trace("rr-rewrite") << std::endl; - - NodeBuilder<> forallB(kind::FORALL); - forallB << r[0]; - Node gg = guards.size()==0 ? true_node : ( guards.size()==1 ? guards[0] : NodeManager::currentNM()->mkNode( AND, guards ) ); - gg = NodeManager::currentNM()->mkNode( OR, gg.negate(), body ); - gg = Rewriter::rewrite( gg ); - forallB << gg; - NodeBuilder<> patternB(kind::INST_PATTERN); - patternB.append(pattern); - NodeBuilder<> patternListB(kind::INST_PATTERN_LIST); - //the entire rewrite rule is the first pattern - if( options::quantRewriteRules() ){ - patternListB << NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, r ); - } - patternListB << static_cast<Node>(patternB); - forallB << static_cast<Node>(patternListB); - Node rn = (Node) forallB; - - return rn; -} - bool QuantifiersRewriter::isPrenexNormalForm( Node n ) { if( n.getKind()==FORALL ){ return n[1].getKind()!=FORALL && isPrenexNormalForm( n[1] ); @@ -2272,17 +2174,14 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { Node prev = n; - if( n.getKind() == kind::REWRITE_RULE ){ - n = quantifiers::QuantifiersRewriter::rewriteRewriteRule( n ); - }else{ - if( options::preSkolemQuant() ){ - if( !isInst || !options::preSkolemQuantNested() ){ - Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl; - //apply pre-skolemization to existential quantifiers - std::vector< TypeNode > fvTypes; - std::vector< TNode > fvs; - n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs ); - } + + if( options::preSkolemQuant() ){ + if( !isInst || !options::preSkolemQuantNested() ){ + Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl; + //apply pre-skolemization to existential quantifiers + std::vector< TypeNode > fvTypes; + std::vector< TNode > fvs; + n = preSkolemizeQuantifiers( prev, true, fvTypes, fvs ); } } //pull all quantifiers globally @@ -2291,7 +2190,7 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { { Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl; std::map< unsigned, std::map< Node, Node > > visited; - n = quantifiers::QuantifiersRewriter::computePrenexAgg( n, true, visited ); + n = computePrenexAgg( n, true, visited ); n = Rewriter::rewrite( n ); Trace("quantifiers-prenex") << "Prenexing returned : " << n << std::endl; //Assert( isPrenexNormalForm( n ) ); diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index e8f069882..69e057c76 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -204,7 +204,6 @@ private: private: static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs); public: - static Node rewriteRewriteRule( Node r ); static bool isPrenexNormalForm( Node n ); /** preprocess * diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp deleted file mode 100644 index 9903456c9..000000000 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ /dev/null @@ -1,309 +0,0 @@ -/********************* */ -/*! \file rewrite_engine.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Rewrite engine module - ** - ** This class manages rewrite rules for quantifiers - **/ - -#include "theory/quantifiers/rewrite_engine.h" - -#include "options/quantifiers_options.h" -#include "theory/quantifiers_engine.h" - -using namespace CVC4; -using namespace std; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; -using namespace CVC4::kind; - -struct PrioritySort { - std::vector< double > d_priority; - bool operator() (int i,int j) { - return d_priority[i] < d_priority[j]; - } -}; - -RewriteEngine::RewriteEngine(context::Context* c, - QuantifiersEngine* qe, - QuantConflictFind* qcf) - : QuantifiersModule(qe), d_qcf(qcf) -{ - d_needsSort = false; -} - -double RewriteEngine::getPriority( Node f ) { - Node rr = QuantAttributes::getRewriteRule( f ); - Node rrr = rr[2]; - Trace("rr-priority") << "Get priority : " << rrr << " " << rrr.getKind() << std::endl; - bool deterministic = rrr[1].getKind()!=OR; - - if( rrr.getKind()==RR_REWRITE ){ - return deterministic ? 0.0 : 3.0; - }else if( rrr.getKind()==RR_DEDUCTION ){ - return deterministic ? 1.0 : 4.0; - }else if( rrr.getKind()==RR_REDUCTION ){ - return deterministic ? 2.0 : 5.0; - }else{ - return 6.0; - } - - //return deterministic ? 0.0 : 1.0; -} - -bool RewriteEngine::needsCheck( Theory::Effort e ){ - return e==Theory::EFFORT_FULL; - //return e>=Theory::EFFORT_LAST_CALL; -} - -void RewriteEngine::check(Theory::Effort e, QEffort quant_e) -{ - if (quant_e == QEFFORT_STANDARD) - { - Assert(!d_quantEngine->inConflict()); - Trace("rewrite-engine") << "---Rewrite Engine Round, effort = " << e << "---" << std::endl; - //if( e==Theory::EFFORT_LAST_CALL ){ - // if( !d_quantEngine->getModel()->isModelSet() ){ - // d_quantEngine->getTheoryEngine()->getModelBuilder()->buildModel( d_quantEngine->getModel(), true ); - // } - //} - if( d_needsSort ){ - d_priority_order.clear(); - PrioritySort ps; - std::vector< int > indicies; - for( int i=0; i<(int)d_rr_quant.size(); i++ ){ - ps.d_priority.push_back( getPriority( d_rr_quant[i] ) ); - indicies.push_back( i ); - } - std::sort( indicies.begin(), indicies.end(), ps ); - for( unsigned i=0; i<indicies.size(); i++ ){ - d_priority_order.push_back( d_rr_quant[indicies[i]] ); - } - d_needsSort = false; - } - - //apply rewrite rules - int addedLemmas = 0; - //per priority level - int index = 0; - bool success = true; - while( !d_quantEngine->inConflict() && success && index<(int)d_priority_order.size() ) { - addedLemmas += checkRewriteRule( d_priority_order[index], e ); - index++; - if( index<(int)d_priority_order.size() ){ - success = addedLemmas==0 || getPriority( d_priority_order[index] )==getPriority( d_priority_order[index-1] ); - } - } - - Trace("rewrite-engine") << "Finished rewrite engine, added " << addedLemmas << " lemmas." << std::endl; - } -} - -int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) { - Trace("rewrite-engine-inst") << "Check " << d_qinfo_n[f] << ", priority = " << getPriority( f ) << ", effort = " << e << "..." << std::endl; - - // get the proper quantifiers info - std::map<Node, QuantInfo>::iterator it = d_qinfo.find(f); - if (it == d_qinfo.end()) - { - Trace("rewrite-engine-inst-debug") << "...No qinfo." << std::endl; - return 0; - } - // reset QCF module - QuantInfo* qi = &it->second; - if (!qi->matchGeneratorIsValid()) - { - Trace("rewrite-engine-inst-debug") << "...Invalid qinfo." << std::endl; - return 0; - } - d_qcf->setEffort(QuantConflictFind::EFFORT_CONFLICT); - Node rr = QuantAttributes::getRewriteRule(f); - Trace("rewrite-engine-inst-debug") << " Reset round..." << std::endl; - qi->reset_round(d_qcf); - Trace("rewrite-engine-inst-debug") << " Get matches..." << std::endl; - int addedLemmas = 0; - while (!d_quantEngine->inConflict() && qi->getNextMatch(d_qcf) - && (addedLemmas == 0 || !options::rrOneInstPerRound())) - { - Trace("rewrite-engine-inst-debug") - << " Got match to complete..." << std::endl; - qi->debugPrintMatch("rewrite-engine-inst-debug"); - std::vector<int> assigned; - if (!qi->isMatchSpurious(d_qcf)) - { - bool doContinue = false; - bool success = true; - int tempAddedLemmas = 0; - while (!d_quantEngine->inConflict() && tempAddedLemmas == 0 && success - && (addedLemmas == 0 || !options::rrOneInstPerRound())) - { - success = qi->completeMatch(d_qcf, assigned, doContinue); - doContinue = true; - if (success) - { - Trace("rewrite-engine-inst-debug") - << " Construct match..." << std::endl; - std::vector<Node> inst; - qi->getMatch(inst); - if (Trace.isOn("rewrite-engine-inst-debug")) - { - Trace("rewrite-engine-inst-debug") - << " Add instantiation..." << std::endl; - for (unsigned i = 0, nchild = f[0].getNumChildren(); i < nchild; - i++) - { - Trace("rewrite-engine-inst-debug") << " " << f[0][i] << " -> "; - if (i < inst.size()) - { - Trace("rewrite-engine-inst-debug") << inst[i] << std::endl; - } - else - { - Trace("rewrite-engine-inst-debug") - << "OUT_OF_RANGE" << std::endl; - Assert(false); - } - } - } - // resize to remove auxiliary variables - if (inst.size() > f[0].getNumChildren()) - { - inst.resize(f[0].getNumChildren()); - } - if (d_quantEngine->getInstantiate()->addInstantiation(f, inst)) - { - addedLemmas++; - tempAddedLemmas++; - } - else - { - Trace("rewrite-engine-inst-debug") << " - failed." << std::endl; - } - Trace("rewrite-engine-inst-debug") - << " Get next completion..." << std::endl; - } - } - Trace("rewrite-engine-inst-debug") - << " - failed to complete." << std::endl; - } - else - { - Trace("rewrite-engine-inst-debug") - << " - match is spurious." << std::endl; - } - Trace("rewrite-engine-inst-debug") << " Get next match..." << std::endl; - } - d_quantEngine->d_statistics.d_instantiations_rr += addedLemmas; - Trace("rewrite-engine-inst") << "-> Generated " << addedLemmas << " lemmas." << std::endl; - return addedLemmas; -} - -void RewriteEngine::registerQuantifier( Node f ) { - Node rr = QuantAttributes::getRewriteRule( f ); - if (rr.isNull()) - { - return; - } - Trace("rr-register") << "Register quantifier " << f << std::endl; - Trace("rr-register") << " rewrite rule is : " << rr << std::endl; - d_rr_quant.push_back(f); - d_rr[f] = rr; - d_needsSort = true; - Trace("rr-register") << " guard is : " << d_rr[f][1] << std::endl; - - std::vector<Node> qcfn_c; - - std::vector<Node> bvl; - bvl.insert(bvl.end(), f[0].begin(), f[0].end()); - - NodeManager* nm = NodeManager::currentNM(); - std::vector<Node> cc; - // add patterns - for (unsigned i = 1, nchild = f[2].getNumChildren(); i < nchild; i++) - { - std::vector<Node> nc; - for (const Node& pat : f[2][i]) - { - Node nn; - Node nbv = nm->mkBoundVar(pat.getType()); - if (pat.getType().isBoolean() && pat.getKind() != APPLY_UF) - { - nn = pat.negate(); - } - else - { - nn = pat.eqNode(nbv).negate(); - bvl.push_back(nbv); - } - nc.push_back(nn); - } - if (!nc.empty()) - { - Node n = nc.size() == 1 ? nc[0] : nm->mkNode(AND, nc); - Trace("rr-register-debug") << " pattern is " << n << std::endl; - if (std::find(cc.begin(), cc.end(), n) == cc.end()) - { - cc.push_back(n); - } - } - } - qcfn_c.push_back(nm->mkNode(BOUND_VAR_LIST, bvl)); - - std::vector<Node> body_c; - // add the guards - if (d_rr[f][1].getKind() == AND) - { - for (const Node& g : d_rr[f][1]) - { - if (MatchGen::isHandled(g)) - { - body_c.push_back(g.negate()); - } - } - } - else if (d_rr[f][1] != d_quantEngine->getTermUtil()->d_true) - { - if (MatchGen::isHandled(d_rr[f][1])) - { - body_c.push_back(d_rr[f][1].negate()); - } - } - // add the patterns to the body - body_c.push_back(cc.size() == 1 ? cc[0] : nm->mkNode(AND, cc)); - // make the body - qcfn_c.push_back(body_c.size() == 1 ? body_c[0] : nm->mkNode(OR, body_c)); - // make the quantified formula - d_qinfo_n[f] = nm->mkNode(FORALL, qcfn_c); - Trace("rr-register") << " qcf formula is : " << d_qinfo_n[f] << std::endl; - d_qinfo[f].initialize(d_qcf, d_qinfo_n[f], d_qinfo_n[f][1]); -} - -void RewriteEngine::assertNode( Node n ) { - -} - -bool RewriteEngine::checkCompleteFor( Node q ) { - // by semantics of rewrite rules, saturation -> SAT - return std::find( d_rr_quant.begin(), d_rr_quant.end(), q )!=d_rr_quant.end(); -} - -Node RewriteEngine::getInstConstNode( Node n, Node q ) { - std::map< Node, Node >::iterator it = d_inst_const_node[q].find( n ); - if( it==d_inst_const_node[q].end() ){ - Node nn = - d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants( - n, q); - d_inst_const_node[q][n] = nn; - return nn; - }else{ - return it->second; - } -} diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h deleted file mode 100644 index 29aba0f1a..000000000 --- a/src/theory/quantifiers/rewrite_engine.h +++ /dev/null @@ -1,86 +0,0 @@ -/********************* */ -/*! \file rewrite_engine.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** [[ Add lengthier description here ]] - ** \todo document this file -**/ - -#include "cvc4_private.h" - -#ifndef CVC4__REWRITE_ENGINE_H -#define CVC4__REWRITE_ENGINE_H - -#include <map> -#include <vector> - -#include "expr/attribute.h" -#include "theory/quantifiers/ematching/trigger.h" -#include "theory/quantifiers/quant_conflict_find.h" -#include "theory/quantifiers/quant_util.h" - -namespace CVC4 { -namespace theory { - -/** - * An attribute for marking a priority value for rewrite rules. - */ -struct RrPriorityAttributeId -{ -}; -typedef expr::Attribute<RrPriorityAttributeId, uint64_t> RrPriorityAttribute; - -namespace quantifiers { - -class RewriteEngine : public QuantifiersModule -{ - std::vector< Node > d_rr_quant; - std::vector< Node > d_priority_order; - std::map< Node, Node > d_rr; - /** explicitly provided patterns */ - std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers; - /** get the quantifer info object */ - std::map< Node, Node > d_qinfo_n; - std::map< Node, QuantInfo > d_qinfo; - double getPriority( Node f ); - bool d_needsSort; - std::map< Node, std::map< Node, Node > > d_inst_const_node; - Node getInstConstNode( Node n, Node q ); - - private: - int checkRewriteRule( Node f, Theory::Effort e ); - - public: - RewriteEngine(context::Context* c, - QuantifiersEngine* qe, - QuantConflictFind* qcf); - - bool needsCheck(Theory::Effort e) override; - void check(Theory::Effort e, QEffort quant_e) override; - void registerQuantifier(Node f) override; - void assertNode(Node n) override; - bool checkCompleteFor(Node q) override; - /** Identify this module */ - std::string identify() const override { return "RewriteEngine"; } - - private: - /** - * A pointer to the quantifiers conflict find module of the quantifiers - * engine. This is the module that computes instantiations for rewrite rule - * quantifiers. - */ - QuantConflictFind* d_qcf; -}; - -} -} -} - -#endif diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index a83dbf541..e2c9043a1 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -141,91 +141,6 @@ struct QuantifierInstClosureTypeRule { } };/* struct QuantifierInstClosureTypeRule */ - -class RewriteRuleTypeRule { -public: - - /** - * Compute the type for (and optionally typecheck) a term belonging - * to the theory of rewriterules. - * - * @param nodeManager the NodeManager in use - * @param n the node to compute the type of - * @param check if true, the node's type should be checked as well - * as computed. - */ - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) - { - Debug("typecheck-r") << "type check for rr " << n << std::endl; - Assert(n.getKind() == kind::REWRITE_RULE && n.getNumChildren() == 3); - if( check ){ - if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){ - throw TypeCheckingExceptionPrivate(n[0], - "first argument of rewrite rule is not bound var list"); - } - if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){ - throw TypeCheckingExceptionPrivate(n[1], - "guard of rewrite rule is not an actual guard"); - } - if( n[2].getType(check) != - TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE))){ - throw TypeCheckingExceptionPrivate(n[2], - "not a correct rewrite rule"); - } - } - return nodeManager->booleanType(); - } -};/* class RewriteRuleTypeRule */ - -class RRRewriteTypeRule { -public: - - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::RR_REWRITE); - if( check ){ - if( n[0].getType(check)!=n[1].getType(check) ){ - throw TypeCheckingExceptionPrivate(n, - "terms of rewrite rule are not equal"); - } - if( n.getNumChildren() == 3 && n[2].getType(check)!=nodeManager->instPatternListType() ){ - throw TypeCheckingExceptionPrivate(n, "third argument of rewrite rule is not instantiation pattern list"); - } - if( n[0].getKind()!=kind::APPLY_UF ){ - throw TypeCheckingExceptionPrivate(n[0], "head of rewrite rules must start with an uninterpreted symbols. If you want to write a propagation rule, add the guard [true] for disambiguation"); - } - } - return TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE)); - } -};/* struct QuantifierReductionRuleRule */ - -class RRRedDedTypeRule { -public: - - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::RR_REDUCTION - || n.getKind() == kind::RR_DEDUCTION); - if( check ){ - if( n[ 0 ].getType(check)!=nodeManager->booleanType() ){ - throw TypeCheckingExceptionPrivate(n, "head of reduction rule is not boolean"); - } - if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){ - throw TypeCheckingExceptionPrivate(n, "body of reduction rule is not boolean"); - } - if( n.getNumChildren() == 3 && n[2].getType(check)!=nodeManager->instPatternListType() ){ - throw TypeCheckingExceptionPrivate(n, "third argument of rewrite rule is not instantiation pattern list"); - } - if( n.getNumChildren() < 3 && n[ 0 ] == nodeManager->mkConst<bool>(true) ){ - throw TypeCheckingExceptionPrivate(n, "A rewrite rule must have one head or one trigger at least"); - } - } - return TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE)); - } -};/* struct QuantifierReductionRuleRule */ - - }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index c7eafc3b8..80a493496 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -30,7 +30,6 @@ #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/quant_split.h" #include "theory/quantifiers/quantifiers_rewriter.h" -#include "theory/quantifiers/rewrite_engine.h" #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/sep/theory_sep.h" #include "theory/theory_engine.h" @@ -53,7 +52,6 @@ class QuantifiersEnginePrivate d_model_engine(nullptr), d_bint(nullptr), d_qcf(nullptr), - d_rr_engine(nullptr), d_sg_gen(nullptr), d_synth_e(nullptr), d_lte_part_inst(nullptr), @@ -81,8 +79,6 @@ class QuantifiersEnginePrivate std::unique_ptr<quantifiers::BoundedIntegers> d_bint; /** Conflict find mechanism for quantifiers */ std::unique_ptr<quantifiers::QuantConflictFind> d_qcf; - /** rewrite rules utility */ - std::unique_ptr<quantifiers::RewriteEngine> d_rr_engine; /** subgoal generator */ std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen; /** ceg instantiation */ @@ -111,7 +107,7 @@ class QuantifiersEnginePrivate bool& needsBuilder) { // add quantifiers modules - if (options::quantConflictFind() || options::quantRewriteRules()) + if (options::quantConflictFind()) { d_qcf.reset(new quantifiers::QuantConflictFind(qe, c)); modules.push_back(d_qcf.get()); @@ -150,11 +146,6 @@ class QuantifiersEnginePrivate // finite model finder has special ways of building the model needsBuilder = true; } - if (options::quantRewriteRules()) - { - d_rr_engine.reset(new quantifiers::RewriteEngine(c, qe, d_qcf.get())); - modules.push_back(d_rr_engine.get()); - } if (options::ltePartialInst()) { d_lte_part_inst.reset(new quantifiers::LtePartialInst(qe, c)); @@ -397,16 +388,6 @@ void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m, int priority ) void QuantifiersEngine::setOwner(Node q, quantifiers::QAttributes& qa) { - if (!qa.d_rr.isNull()) - { - if (d_private->d_rr_engine.get() == nullptr) - { - Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : " - << q << std::endl; - } - // set rewrite engine as owner - setOwner(q, d_private->d_rr_engine.get(), 2); - } if (qa.d_sygus || (options::sygusRecFun() && !qa.d_fundef_f.isNull())) { if (d_private->d_synth_e.get() == nullptr) diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 3b11d8e54..6a404104f 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -35,7 +35,7 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl; - if ((parent.isClosure() || parent.getKind() == kind::REWRITE_RULE + if ((parent.isClosure() || parent.getKind() == kind::SEP_STAR || parent.getKind() == kind::SEP_WAND || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean()) @@ -178,7 +178,7 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl; - if ((parent.isClosure() || parent.getKind() == kind::REWRITE_RULE + if ((parent.isClosure() || parent.getKind() == kind::SEP_STAR || parent.getKind() == kind::SEP_WAND || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean()) |