}
}
-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;
// get substitution corresponding to m
std::vector<TNode> vars;
std::vector<TNode> 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;
else
{
// do not run higher-order matching
- return d_quantEngine->getInstantiate()->addInstantiation(d_f, m);
+ return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m);
}
}
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
{
* Extends Trigger::addInstantiations to also send
* lemmas based on addHoTypeMatchPredicateLemmas.
*/
- virtual int addInstantiations(InstMatch& baseMatch) override;
+ virtual int addInstantiations() override;
protected:
/**
d_match_pattern = pat;
d_match_pattern_type = pat.getType();
d_next = NULL;
- d_matchPolicy = MATCH_GEN_DEFAULT;
d_independent_gen = false;
}
d_needsReset = true;
d_active_add = true;
d_next = NULL;
- d_matchPolicy = MATCH_GEN_DEFAULT;
d_independent_gen = false;
}
//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
{
{
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
{
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() );
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{
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<d_match_pattern.getNumChildren(); i++ ){
- if( d_children_types[i]==0 ){
- Trace("matching-debug2") << "Setting " << d_var_num[i] << " to " << t[i] << "..." << std::endl;
- bool addToPrev = m.get( d_var_num[i] ).isNull();
- if (!m.set(q, d_var_num[i], t[i]))
+ for (unsigned i = 0, size = d_match_pattern.getNumChildren(); i < size; i++)
+ {
+ int ct = d_children_types[i];
+ if (ct >= 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
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
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; i<d_children.size(); i++ ){
+ for (unsigned i = 0, size = d_children.size(); i < size; i++)
+ {
if( !d_children[i]->reset( t[ d_children_index[i] ], qe ) ){
success = false;
break;
}
}
if( ret_val<0 ){
- //m = InstMatch( &prev );
- for( unsigned i=0; i<prev.size(); i++ ){
- m.d_vals[prev[i]] = Node::null();
+ for (int& pv : prev)
+ {
+ m.d_vals[pv] = Node::null();
}
}
return ret_val;
}
int InstMatchGenerator::addInstantiations(Node f,
- InstMatch& baseMatch,
QuantifiersEngine* qe,
Trigger* tparent)
{
while (getNextMatch(f, m, qe, tparent) > 0)
{
if( !d_active_add ){
- m.add( baseMatch );
if (sendInstantiation(tparent, m))
{
addedLemmas++;
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,
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{
}
}
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;
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();
}
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{
}
}
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;
}
int InstMatchGeneratorMulti::addInstantiations(Node q,
- InstMatch& baseMatch,
QuantifiersEngine* qe,
Trigger* tparent)
{
}
int InstMatchGeneratorSimple::addInstantiations(Node q,
- InstMatch& baseMatch,
QuantifiersEngine* qe,
Trigger* tparent)
{
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;
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;
* 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)
{
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;
Trigger* tparent) override;
/** Add instantiations. */
int addInstantiations(Node q,
- InstMatch& baseMatch,
QuantifiersEngine* qe,
Trigger* tparent) override;
* (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.
* of the term.
*/
std::vector<int> 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<int> d_children_types;
/** The next generator in the linked list
* that this generator is a part of.
/** 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<int, int> d_var_num;
/** Excluded matches
* Stores the terms we are not allowed to match.
* These can for instance be specified by the smt2
bool reset(Node eqc, QuantifiersEngine* qe) override;
/** Add instantiations. */
int addInstantiations(Node q,
- InstMatch& baseMatch,
QuantifiersEngine* qe,
Trigger* tparent) override;
void resetInstantiationRound(QuantifiersEngine* qe) override;
/** Add instantiations. */
int addInstantiations(Node q,
- InstMatch& baseMatch,
QuantifiersEngine* qe,
Trigger* tparent) override;
/** Get active score. */
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() ){
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;
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();
}
}
}
}
/** 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<Node>& 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<d_nodes.size(); i++ ){
Trace("trigger") << " " << d_nodes[i] << std::endl;
}
if( d_nodes.size()==1 ){
if( isSimpleTrigger( d_nodes[0] ) ){
- d_mg = new InstMatchGeneratorSimple( f, d_nodes[0], qe );
+ d_mg = new InstMatchGeneratorSimple(q, d_nodes[0], qe);
}else{
- d_mg = InstMatchGenerator::mkInstMatchGenerator( f, d_nodes[0], qe );
+ d_mg = InstMatchGenerator::mkInstMatchGenerator(q, d_nodes[0], qe);
}
}else{
if( options::multiTriggerCache() ){
- d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe );
+ d_mg = new InstMatchGeneratorMulti(q, d_nodes, qe);
}else{
- d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti( f, d_nodes, qe );
+ d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti(q, d_nodes, qe);
}
}
if( d_nodes.size()==1 ){
++(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; i<d_nodes.size(); i++ ){
Trace("multi-trigger") << " " << d_nodes[i] << std::endl;
}
++(qe->d_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;
}
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"))
{
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 ) {
* 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),
* 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.
protected:
/** trigger constructor, intentionally protected (use Trigger::mkTrigger). */
- Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes );
+ Trigger(QuantifiersEngine* ie, Node q, std::vector<Node>& 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
/** 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
projects / cvc5.git / commitdiff