From 3179bfe0fff1372b4080196dd28f0079d859830f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 2 Dec 2017 06:14:12 -0600 Subject: [PATCH] Minor improvements to inst match generator (#1415) --- src/theory/quantifiers/ho_trigger.cpp | 14 ++-- src/theory/quantifiers/ho_trigger.h | 2 +- .../quantifiers/inst_match_generator.cpp | 77 +++++++++---------- src/theory/quantifiers/inst_match_generator.h | 37 +++------ .../quantifiers/inst_strategy_e_matching.cpp | 6 +- src/theory/quantifiers/model_builder.cpp | 2 +- src/theory/quantifiers/trigger.cpp | 26 +++---- src/theory/quantifiers/trigger.h | 14 +--- 8 files changed, 76 insertions(+), 102 deletions(-) diff --git a/src/theory/quantifiers/ho_trigger.cpp b/src/theory/quantifiers/ho_trigger.cpp index 6354047cf..6456fb2f6 100644 --- a/src/theory/quantifiers/ho_trigger.cpp +++ b/src/theory/quantifiers/ho_trigger.cpp @@ -186,10 +186,10 @@ void HigherOrderTrigger::collectHoVarApplyTerms( } } -int HigherOrderTrigger::addInstantiations(InstMatch& baseMatch) +int HigherOrderTrigger::addInstantiations() { // call the base class implementation - int addedFoLemmas = Trigger::addInstantiations(baseMatch); + int addedFoLemmas = Trigger::addInstantiations(); // also adds predicate lemms to force app completion int addedHoLemmas = addHoTypeMatchPredicateLemmas(); return addedHoLemmas + addedFoLemmas; @@ -202,11 +202,11 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) // get substitution corresponding to m std::vector vars; std::vector subs; - for (unsigned i = 0, size = d_f[0].getNumChildren(); i < size; i++) + quantifiers::TermUtil* tutil = d_quantEngine->getTermUtil(); + for (unsigned i = 0, size = d_quant[0].getNumChildren(); i < size; i++) { subs.push_back(m.d_vals[i]); - vars.push_back( - d_quantEngine->getTermUtil()->getInstantiationConstant(d_f, i)); + vars.push_back(tutil->getInstantiationConstant(d_quant, i)); } Trace("ho-unif-debug") << "Run higher-order unification..." << std::endl; @@ -353,7 +353,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) else { // do not run higher-order matching - return d_quantEngine->getInstantiate()->addInstantiation(d_f, m); + return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m); } } @@ -364,7 +364,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m, unsigned var_index) if (var_index == d_ho_var_list.size()) { // we now have an instantiation to try - return d_quantEngine->getInstantiate()->addInstantiation(d_f, m); + return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m); } else { diff --git a/src/theory/quantifiers/ho_trigger.h b/src/theory/quantifiers/ho_trigger.h index e5112abce..4db3a660f 100644 --- a/src/theory/quantifiers/ho_trigger.h +++ b/src/theory/quantifiers/ho_trigger.h @@ -122,7 +122,7 @@ class HigherOrderTrigger : public Trigger * Extends Trigger::addInstantiations to also send * lemmas based on addHoTypeMatchPredicateLemmas. */ - virtual int addInstantiations(InstMatch& baseMatch) override; + virtual int addInstantiations() override; protected: /** diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 5cdb2a64b..884ed29f5 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -48,7 +48,6 @@ InstMatchGenerator::InstMatchGenerator( Node pat ){ d_match_pattern = pat; d_match_pattern_type = pat.getType(); d_next = NULL; - d_matchPolicy = MATCH_GEN_DEFAULT; d_independent_gen = false; } @@ -57,7 +56,6 @@ InstMatchGenerator::InstMatchGenerator() { d_needsReset = true; d_active_add = true; d_next = NULL; - d_matchPolicy = MATCH_GEN_DEFAULT; d_independent_gen = false; } @@ -135,7 +133,8 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< //now, collect children of d_match_pattern if (d_match_pattern.getKind() == INST_CONSTANT) { - d_var_num[0] = d_match_pattern.getAttribute(InstVarNumAttribute()); + d_children_types.push_back( + d_match_pattern.getAttribute(InstVarNumAttribute())); } else { @@ -151,13 +150,12 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< { d_children.push_back(cimg); d_children_index.push_back(i); - d_children_types.push_back(1); + d_children_types.push_back(-2); }else{ if (d_match_pattern[i].getKind() == INST_CONSTANT && qa == q) { - d_var_num[i] = - d_match_pattern[i].getAttribute(InstVarNumAttribute()); - d_children_types.push_back(0); + d_children_types.push_back( + d_match_pattern[i].getAttribute(InstVarNumAttribute())); } else { @@ -204,9 +202,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern ); } }else{ - d_cg = new CandidateGeneratorQueue( qe ); Trace("inst-match-gen-warn") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; - d_matchPolicy = MATCH_GEN_INTERNAL_ERROR; } } gens.insert( gens.end(), d_children.begin(), d_children.end() ); @@ -219,7 +215,8 @@ int InstMatchGenerator::getMatch( Trace("matching") << "Matching " << t << " against pattern " << d_match_pattern << " (" << m << ")" << ", " << d_children.size() << ", pattern is " << d_pattern << std::endl; Assert( !d_match_pattern.isNull() ); - if( d_matchPolicy==MATCH_GEN_INTERNAL_ERROR ){ + if (d_cg == nullptr) + { Trace("matching-fail") << "Internal error for match generator." << std::endl; return -2; }else{ @@ -235,21 +232,28 @@ int InstMatchGenerator::getMatch( Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() ); //first, check if ground arguments are not equal, or a match is in conflict Trace("matching-debug2") << "Setting immediate matches..." << std::endl; - for( unsigned i=0; i= 0) + { + Trace("matching-debug2") << "Setting " << ct << " to " << t[i] << "..." + << std::endl; + bool addToPrev = m.get(ct).isNull(); + if (!m.set(q, ct, t[i])) { //match is in conflict - Trace("matching-fail") << "Match fail: " << m.get(d_var_num[i]) << " and " << t[i] << std::endl; + Trace("matching-fail") << "Match fail: " << m.get(ct) << " and " + << t[i] << std::endl; success = false; break; }else if( addToPrev ){ Trace("matching-debug2") << "Success." << std::endl; - prev.push_back( d_var_num[i] ); + prev.push_back(ct); } - }else if( d_children_types[i]==-1 ){ + } + else if (ct == -1) + { if( !q->areEqual( d_match_pattern[i], t[i] ) ){ Trace("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl; //ground arguments are not equal @@ -261,13 +265,13 @@ int InstMatchGenerator::getMatch( Trace("matching-debug2") << "Done setting immediate matches, success = " << success << "." << std::endl; //for variable matching if( d_match_pattern.getKind()==INST_CONSTANT ){ - bool addToPrev = m.get( d_var_num[0] ).isNull(); - if (!m.set(q, d_var_num[0], t)) + bool addToPrev = m.get(d_children_types[0]).isNull(); + if (!m.set(q, d_children_types[0], t)) { success = false; }else{ if( addToPrev ){ - prev.push_back( d_var_num[0] ); + prev.push_back(d_children_types[0]); } } //for relational matching @@ -312,7 +316,8 @@ int InstMatchGenerator::getMatch( Trace("matching-debug2") << "Reset children..." << std::endl; //now, fit children into match //we will be requesting candidates for matching terms for each child - for( unsigned i=0; ireset( t[ d_children_index[i] ], qe ) ){ success = false; break; @@ -324,9 +329,9 @@ int InstMatchGenerator::getMatch( } } if( ret_val<0 ){ - //m = InstMatch( &prev ); - for( unsigned i=0; i 0) { if( !d_active_add ){ - m.add( baseMatch ); if (sendInstantiation(tparent, m)) { addedLemmas++; @@ -563,7 +566,7 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Node q, Node n) VarMatchGeneratorBooleanTerm::VarMatchGeneratorBooleanTerm( Node var, Node comp ) : InstMatchGenerator(), d_comp( comp ), d_rm_prev( false ) { - d_var_num[0] = var.getAttribute(InstVarNumAttribute()); + d_children_types.push_back(var.getAttribute(InstVarNumAttribute())); } int VarMatchGeneratorBooleanTerm::getNextMatch(Node q, @@ -575,8 +578,8 @@ int VarMatchGeneratorBooleanTerm::getNextMatch(Node q, if( !d_eq_class.isNull() ){ Node s = NodeManager::currentNM()->mkConst(qe->getEqualityQuery()->areEqual( d_eq_class, d_pattern )); d_eq_class = Node::null(); - d_rm_prev = m.get( d_var_num[0] ).isNull(); - if (!m.set(qe->getEqualityQuery(), d_var_num[0], s)) + d_rm_prev = m.get(d_children_types[0]).isNull(); + if (!m.set(qe->getEqualityQuery(), d_children_types[0], s)) { return -1; }else{ @@ -587,7 +590,7 @@ int VarMatchGeneratorBooleanTerm::getNextMatch(Node q, } } if( d_rm_prev ){ - m.d_vals[d_var_num[0]] = Node::null(); + m.d_vals[d_children_types[0]] = Node::null(); d_rm_prev = false; } return ret_val; @@ -595,7 +598,7 @@ int VarMatchGeneratorBooleanTerm::getNextMatch(Node q, VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs( Node var, Node subs ) : InstMatchGenerator(), d_var( var ), d_subs( subs ), d_rm_prev( false ){ - d_var_num[0] = d_var.getAttribute(InstVarNumAttribute()); + d_children_types.push_back(d_var.getAttribute(InstVarNumAttribute())); d_var_type = d_var.getType(); } @@ -612,8 +615,8 @@ int VarMatchGeneratorTermSubs::getNextMatch(Node q, Trace("var-trigger-matching") << "...got " << s << ", " << s.getKind() << std::endl; d_eq_class = Node::null(); //if( s.getType().isSubtypeOf( d_var_type ) ){ - d_rm_prev = m.get( d_var_num[0] ).isNull(); - if (!m.set(qe->getEqualityQuery(), d_var_num[0], s)) + d_rm_prev = m.get(d_children_types[0]).isNull(); + if (!m.set(qe->getEqualityQuery(), d_children_types[0], s)) { return -1; }else{ @@ -624,7 +627,7 @@ int VarMatchGeneratorTermSubs::getNextMatch(Node q, } } if( d_rm_prev ){ - m.d_vals[d_var_num[0]] = Node::null(); + m.d_vals[d_children_types[0]] = Node::null(); d_rm_prev = false; } return -1; @@ -838,7 +841,6 @@ bool InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){ } int InstMatchGeneratorMulti::addInstantiations(Node q, - InstMatch& baseMatch, QuantifiersEngine* qe, Trigger* tparent) { @@ -1033,7 +1035,6 @@ void InstMatchGeneratorSimple::resetInstantiationRound( QuantifiersEngine* qe ) } int InstMatchGeneratorSimple::addInstantiations(Node q, - InstMatch& baseMatch, QuantifiersEngine* qe, Trigger* tparent) { @@ -1052,7 +1053,6 @@ int InstMatchGeneratorSimple::addInstantiations(Node q, for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){ if( it->first!=r ){ InstMatch m( q ); - m.add( baseMatch ); addInstantiations( m, qe, addedLemmas, 0, &(it->second) ); if( qe->inConflict() ){ break; @@ -1066,7 +1066,6 @@ int InstMatchGeneratorSimple::addInstantiations(Node q, Debug("simple-trigger-debug") << "Adding instantiations based on " << tat << " from " << d_op << " " << d_eqc << std::endl; if( tat ){ InstMatch m( q ); - m.add( baseMatch ); addInstantiations( m, qe, addedLemmas, 0, tat ); } return addedLemmas; diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index e36ee2b58..95faf0279 100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -89,14 +89,10 @@ public: * using the implemented matching algorithm. It typically is implemented as a * fixed point of getNextMatch above. * - * baseMatch is a mapping of default values that should be used for variables - * that are not bound by this (not frequently used). (TODO remove #1389) - * * It returns the number of instantiations added using calls to calls to * Instantiate::addInstantiation(...). */ virtual int addInstantiations(Node q, - InstMatch& baseMatch, QuantifiersEngine* qe, Trigger* tparent) { @@ -198,13 +194,6 @@ class InstMatchGenerator : public IMGenerator { public: /** destructor */ virtual ~InstMatchGenerator() throw(); - enum - { - // options for producing matches - MATCH_GEN_DEFAULT = 0, - // others (internally used) - MATCH_GEN_INTERNAL_ERROR, - }; /** Reset instantiation round. */ void resetInstantiationRound(QuantifiersEngine* qe) override; @@ -217,7 +206,6 @@ public: Trigger* tparent) override; /** Add instantiations. */ int addInstantiations(Node q, - InstMatch& baseMatch, QuantifiersEngine* qe, Trigger* tparent) override; @@ -329,11 +317,6 @@ protected: * (e.g. a matchable term, a variable, a relation, etc.). */ CandidateGenerator* d_cg; - /** policy to use for matching - * This is one of MATCH_GEN_* above. - * TODO: this can be simplified/removed (#1283). - */ - int d_matchPolicy; /** children generators * These match generators correspond to the children of the term * we are matching with this generator. @@ -347,7 +330,16 @@ protected: * of the term. */ std::vector d_children_index; - /** children types 0 : variable, 1 : child term, -1 : ground term */ + /** children types + * + * If d_match_pattern is an instantiation constant, then this is a singleton + * vector containing the variable number of the d_match_pattern itself. + * If d_match_patterm is a term of the form f( t1, ..., tn ), then for each + * index i, d_children[i] stores the type of node ti is, where: + * >= 0 : variable (indicates its number), + * -1 : ground term, + * -2 : child term. + */ std::vector d_children_types; /** The next generator in the linked list * that this generator is a part of. @@ -358,13 +350,6 @@ protected: /** If non-null, then this is a relational trigger of the form x ~ * d_eq_class_rel. */ Node d_eq_class_rel; - /** For each child index of this node, the variable numbers of the children. - * For example, if this is generator is for the term f( x3, a, x1, x2 ) - * the quantified formula - * forall x1 x2 x3. (...). - * Then d_var_num[0] = 2, d_var_num[2] = 0 and d_var_num[3] = 1. - */ - std::map d_var_num; /** Excluded matches * Stores the terms we are not allowed to match. * These can for instance be specified by the smt2 @@ -575,7 +560,6 @@ class InstMatchGeneratorMulti : public IMGenerator { bool reset(Node eqc, QuantifiersEngine* qe) override; /** Add instantiations. */ int addInstantiations(Node q, - InstMatch& baseMatch, QuantifiersEngine* qe, Trigger* tparent) override; @@ -663,7 +647,6 @@ class InstMatchGeneratorSimple : public IMGenerator { void resetInstantiationRound(QuantifiersEngine* qe) override; /** Add instantiations. */ int addInstantiations(Node q, - InstMatch& baseMatch, QuantifiersEngine* qe, Trigger* tparent) override; /** Get active score. */ diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index f7e5891f9..c39df58c6 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -106,8 +106,7 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){ Trace("process-trigger") << " Process (user) "; d_user_gen[f][i]->debugPrint("process-trigger"); Trace("process-trigger") << "..." << std::endl; - InstMatch baseMatch( f ); - int numInst = d_user_gen[f][i]->addInstantiations( baseMatch ); + int numInst = d_user_gen[f][i]->addInstantiations(); Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl; d_quantEngine->d_statistics.d_instantiations_user_patterns += numInst; if( d_user_gen[f][i]->isMultiTrigger() ){ @@ -249,8 +248,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) Trace("process-trigger") << " Process "; tr->debugPrint("process-trigger"); Trace("process-trigger") << "..." << std::endl; - InstMatch baseMatch( f ); - int numInst = tr->addInstantiations( baseMatch ); + int numInst = tr->addInstantiations(); hasInst = numInst>0 || hasInst; Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl; d_quantEngine->d_statistics.d_instantiations_auto_gen += numInst; diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index dba04ce51..fbd122bd6 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -717,7 +717,7 @@ int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ tr->reset( Node::null() ); //d_qe->d_optInstMakeRepresentative = false; //d_qe->d_optMatchIgnoreModelBasis = true; - addedLemmas += tr->addInstantiations( d_quant_basis_match[f] ); + addedLemmas += tr->addInstantiations(); } } } diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 40079933e..2d97bd160 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -48,24 +48,25 @@ void TriggerTermInfo::init( Node q, Node n, int reqPol, Node reqPolEq ){ } /** trigger class constructor */ -Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes ) - : d_quantEngine( qe ), d_f( f ) { +Trigger::Trigger(QuantifiersEngine* qe, Node q, std::vector& nodes) + : d_quantEngine(qe), d_quant(q) +{ d_nodes.insert( d_nodes.begin(), nodes.begin(), nodes.end() ); - Trace("trigger") << "Trigger for " << f << ": " << std::endl; + Trace("trigger") << "Trigger for " << q << ": " << std::endl; for( unsigned i=0; i& nodes ) ++(qe->d_statistics.d_simple_triggers); } }else{ - Trace("multi-trigger") << "Trigger for " << f << ": " << std::endl; + Trace("multi-trigger") << "Trigger for " << q << ": " << std::endl; for( unsigned i=0; id_statistics.d_multi_triggers); } - //Notice() << "Trigger : " << (*this) << " for " << f << std::endl; + // Notice() << "Trigger : " << (*this) << " for " << q << std::endl; Trace("trigger-debug") << "Finished making trigger." << std::endl; } @@ -102,10 +103,9 @@ Node Trigger::getInstPattern(){ return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes ); } -int Trigger::addInstantiations(InstMatch& baseMatch) +int Trigger::addInstantiations() { - int addedLemmas = - d_mg->addInstantiations(d_f, baseMatch, d_quantEngine, this); + int addedLemmas = d_mg->addInstantiations(d_quant, d_quantEngine, this); if( addedLemmas>0 ){ if (Debug.isOn("inst-trigger")) { @@ -123,7 +123,7 @@ int Trigger::addInstantiations(InstMatch& baseMatch) bool Trigger::sendInstantiation(InstMatch& m) { - return d_quantEngine->getInstantiate()->addInstantiation(d_f, m); + return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m); } bool Trigger::mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_vars, std::vector< Node >& trNodes ) { diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 2beafb984..e897c0b06 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -118,10 +118,9 @@ class TriggerTermInfo { * t->resetInstantiationRound(); * // will produce instantiations based on matching with all terms * t->reset( Node::null() ); -* InstMatch baseMatch; * // add all instantiations based on E-matching with this trigger and the * // current context -* t->addInstantiations( baseMatch ); +* t->addInstantiations(); * * This will result in (a set of) calls to * Instantiate::addInstantiation(q, m1)...Instantiate::addInstantiation(q, mn), @@ -187,13 +186,8 @@ class Trigger { * of the underlying match generator. It can be extended to * produce instantiations beyond what is produced by the match generator * (for example, see theory/quantifiers/ho_trigger.h). - * - * baseMatch : a mapping of default values that should be used for variables - * that are not bound as a result of matching terms from this - * trigger. These default values are not frequently used in - * instantiations. (TODO : remove #1389) */ - virtual int addInstantiations(InstMatch& baseMatch); + virtual int addInstantiations(); /** Return whether this is a multi-trigger. */ bool isMultiTrigger() { return d_nodes.size()>1; } /** Get instantiation pattern list associated with this trigger. @@ -367,7 +361,7 @@ class Trigger { protected: /** trigger constructor, intentionally protected (use Trigger::mkTrigger). */ - Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes ); + Trigger(QuantifiersEngine* ie, Node q, std::vector& nodes); /** is subterm of trigger usable (helper function for isUsableTrigger) */ static bool isUsable( Node n, Node q ); /** returns an equality that is equivalent to the equality eq and @@ -437,7 +431,7 @@ class Trigger { /** The quantifiers engine associated with this trigger. */ QuantifiersEngine* d_quantEngine; /** The quantified formula this trigger is for. */ - Node d_f; + Node d_quant; /** match generator * * This is the back-end utility that implements the underlying matching -- 2.30.2