diff options
Diffstat (limited to 'src/theory/quantifiers/ematching')
-rw-r--r-- | src/theory/quantifiers/ematching/candidate_generator.cpp | 309 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/candidate_generator.h | 179 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/inst_match_generator.cpp | 44 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/inst_match_generator.h | 26 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/trigger.cpp | 23 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/trigger.h | 2 |
6 files changed, 493 insertions, 90 deletions
diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp new file mode 100644 index 000000000..ea5e8592d --- /dev/null +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -0,0 +1,309 @@ +/********************* */ +/*! \file candidate_generator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 Implementation of theory uf candidate generator class + **/ + +#include "theory/quantifiers/ematching/candidate_generator.h" +#include "options/quantifiers_options.h" +#include "theory/quantifiers/inst_match.h" +#include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" +#include "theory/theory_engine.h" +#include "theory/uf/theory_uf.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::inst; + +bool CandidateGenerator::isLegalCandidate( Node n ){ + return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(n) ); +} + +void CandidateGeneratorQueue::addCandidate( Node n ) { + if( isLegalCandidate( n ) ){ + d_candidates.push_back( n ); + } +} + +void CandidateGeneratorQueue::reset( Node eqc ){ + if( d_candidate_index>0 ){ + d_candidates.erase( d_candidates.begin(), d_candidates.begin() + d_candidate_index ); + d_candidate_index = 0; + } + if( !eqc.isNull() ){ + d_candidates.push_back( eqc ); + } +} +Node CandidateGeneratorQueue::getNextCandidate(){ + if( d_candidate_index<(int)d_candidates.size() ){ + Node n = d_candidates[d_candidate_index]; + d_candidate_index++; + return n; + }else{ + d_candidate_index = 0; + d_candidates.clear(); + return Node::null(); + } +} + +CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node pat ) : +CandidateGenerator( qe ), d_term_iter( -1 ){ + d_op = qe->getTermDatabase()->getMatchOperator( pat ); + Assert( !d_op.isNull() ); + d_op_arity = pat.getNumChildren(); +} + +void CandidateGeneratorQE::resetInstantiationRound(){ + d_term_iter_limit = d_qe->getTermDatabase()->getNumGroundTerms( d_op ); +} + +void CandidateGeneratorQE::reset( Node eqc ){ + d_term_iter = 0; + if( eqc.isNull() ){ + d_mode = cand_term_db; + }else{ + if( isExcludedEqc( eqc ) ){ + d_mode = cand_term_none; + }else{ + eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine(); + if( ee->hasTerm( eqc ) ){ + quantifiers::TermArgTrie * tat = d_qe->getTermDatabase()->getTermArgTrie( eqc, d_op ); + if( tat ){ +#if 1 + //create an equivalence class iterator in eq class eqc + Node rep = ee->getRepresentative( eqc ); + d_eqc_iter = eq::EqClassIterator( rep, ee ); + d_mode = cand_term_eqc; +#else + d_tindex.push_back( tat ); + d_tindex_iter.push_back( tat->d_data.begin() ); + d_mode = cand_term_tindex; +#endif + }else{ + d_mode = cand_term_none; + } + }else{ + //the only match is this term itself + d_n = eqc; + d_mode = cand_term_ident; + } + } + } +} +bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) { + if( n.hasOperator() ){ + if( isLegalCandidate( n ) ){ + return d_qe->getTermDatabase()->getMatchOperator( n )==d_op; + } + } + return false; +} + +Node CandidateGeneratorQE::getNextCandidate(){ + if( d_mode==cand_term_db ){ + Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl; + //get next candidate term in the uf term database + while( d_term_iter<d_term_iter_limit ){ + Node n = d_qe->getTermDatabase()->getGroundTerm( d_op, d_term_iter ); + d_term_iter++; + if( isLegalCandidate( n ) ){ + if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){ + if( d_exclude_eqc.empty() ){ + return n; + }else{ + Node r = d_qe->getEqualityQuery()->getRepresentative( n ); + if( d_exclude_eqc.find( r )==d_exclude_eqc.end() ){ + Debug("cand-gen-qe") << "...returning " << n << std::endl; + return n; + } + } + } + } + } + }else if( d_mode==cand_term_eqc ){ + Debug("cand-gen-qe") << "...get next candidate in eqc" << std::endl; + while( !d_eqc_iter.isFinished() ){ + Node n = *d_eqc_iter; + ++d_eqc_iter; + if( isLegalOpCandidate( n ) ){ + Debug("cand-gen-qe") << "...returning " << n << std::endl; + return n; + } + } + }else if( d_mode==cand_term_tindex ){ + Debug("cand-gen-qe") << "...get next candidate in tindex " << d_op << " " << d_op_arity << std::endl; + //increment the term index iterator + if( !d_tindex.empty() ){ + //populate the vector + while( d_tindex_iter.size()<=d_op_arity ){ + Assert( !d_tindex_iter.empty() ); + Assert( !d_tindex_iter.back()->second.d_data.empty() ); + d_tindex.push_back( &(d_tindex_iter.back()->second) ); + d_tindex_iter.push_back( d_tindex_iter.back()->second.d_data.begin() ); + } + //get the current node + Assert( d_tindex_iter.back()->second.hasNodeData() ); + Node n = d_tindex_iter.back()->second.getNodeData(); + Debug("cand-gen-qe") << "...returning " << n << std::endl; + Assert( !n.isNull() ); + Assert( isLegalOpCandidate( n ) ); + //increment + bool success = false; + do{ + ++d_tindex_iter.back(); + if( d_tindex_iter.back()==d_tindex.back()->d_data.end() ){ + d_tindex.pop_back(); + d_tindex_iter.pop_back(); + }else{ + success = true; + } + }while( !success && !d_tindex.empty() ); + return n; + } + }else if( d_mode==cand_term_ident ){ + Debug("cand-gen-qe") << "...get next candidate identity" << std::endl; + if( !d_n.isNull() ){ + Node n = d_n; + d_n = Node::null(); + if( isLegalOpCandidate( n ) ){ + return n; + } + } + } + return Node::null(); +} + +CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ) : + CandidateGenerator( qe ), d_match_pattern( mpat ){ + Assert( mpat.getKind()==EQUAL ); + for( unsigned i=0; i<2; i++ ){ + if( !quantifiers::TermUtil::hasInstConstAttr(mpat[i]) ){ + d_match_gterm = mpat[i]; + } + } +} +void CandidateGeneratorQELitEq::resetInstantiationRound(){ + +} +void CandidateGeneratorQELitEq::reset( Node eqc ){ + if( d_match_gterm.isNull() ){ + d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() ); + }else{ + d_do_mgt = true; + } +} +Node CandidateGeneratorQELitEq::getNextCandidate(){ + if( d_match_gterm.isNull() ){ + while( !d_eq.isFinished() ){ + Node n = (*d_eq); + ++d_eq; + if( n.getType().isComparableTo( d_match_pattern[0].getType() ) ){ + //an equivalence class with the same type as the pattern, return reflexive equality + return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n ); + } + } + }else{ + if( d_do_mgt ){ + d_do_mgt = false; + return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_gterm, d_match_gterm ); + } + } + return Node::null(); +} + + +CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) : +CandidateGenerator( qe ), d_match_pattern( mpat ){ + + Assert( d_match_pattern.getKind()==EQUAL ); + d_match_pattern_type = d_match_pattern[0].getType(); +} + +void CandidateGeneratorQELitDeq::resetInstantiationRound(){ + +} + +void CandidateGeneratorQELitDeq::reset( Node eqc ){ + Node false_term = d_qe->getEqualityQuery()->getEngine()->getRepresentative( NodeManager::currentNM()->mkConst<bool>(false) ); + d_eqc_false = eq::EqClassIterator( false_term, d_qe->getEqualityQuery()->getEngine() ); +} + +Node CandidateGeneratorQELitDeq::getNextCandidate(){ + //get next candidate term in equivalence class + while( !d_eqc_false.isFinished() ){ + Node n = (*d_eqc_false); + ++d_eqc_false; + if( n.getKind()==d_match_pattern.getKind() ){ + if( n[0].getType().isComparableTo( d_match_pattern_type ) ){ + //found an iff or equality, try to match it + //DO_THIS: cache to avoid redundancies? + //DO_THIS: do we need to try the symmetric equality for n? or will it also exist in the eq class of false? + return n; + } + } + } + return Node::null(); +} + + +CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ) : + CandidateGenerator( qe ), d_match_pattern( mpat ){ + d_match_pattern_type = mpat.getType(); + Assert( mpat.getKind()==INST_CONSTANT ); + d_f = quantifiers::TermUtil::getInstConstAttr( mpat ); + d_index = mpat.getAttribute(InstVarNumAttribute()); + d_firstTime = false; +} + +void CandidateGeneratorQEAll::resetInstantiationRound() { + +} + +void CandidateGeneratorQEAll::reset( Node eqc ) { + d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() ); + d_firstTime = true; +} + +Node CandidateGeneratorQEAll::getNextCandidate() { + while( !d_eq.isFinished() ){ + TNode n = (*d_eq); + ++d_eq; + if( n.getType().isComparableTo( d_match_pattern_type ) ){ + TNode nh = d_qe->getTermDatabase()->getEligibleTermInEqc( n ); + if( !nh.isNull() ){ + if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){ + nh = d_qe->getInternalRepresentative( nh, d_f, d_index ); + //don't consider this if already the instantiation is ineligible + if( !d_qe->getTermDatabase()->isTermEligibleForInstantiation( nh, d_f, false ) ){ + nh = Node::null(); + } + } + if( !nh.isNull() ){ + d_firstTime = false; + //an equivalence class with the same type as the pattern, return it + return nh; + } + } + } + } + if( d_firstTime ){ + //must return something + d_firstTime = false; + return d_qe->getInstantiate()->getTermForType(d_match_pattern_type); + } + return Node::null(); +} diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h new file mode 100644 index 000000000..4662d7c4c --- /dev/null +++ b/src/theory/quantifiers/ematching/candidate_generator.h @@ -0,0 +1,179 @@ +/********************* */ +/*! \file candidate_generator.h + ** \verbatim + ** Top contributors (to current version): + ** Morgan Deters, Andrew Reynolds, Clark Barrett + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 Theory uf candidate generator + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H +#define __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H + +#include "theory/theory.h" +#include "theory/uf/equality_engine.h" + +namespace CVC4 { +namespace theory { + +namespace quantifiers { + class TermArgTrie; +} + +class QuantifiersEngine; + +namespace inst { + +/** base class for generating candidates for matching */ +class CandidateGenerator { +protected: + QuantifiersEngine* d_qe; +public: + CandidateGenerator( QuantifiersEngine* qe ) : d_qe( qe ){} + virtual ~CandidateGenerator(){} + + /** Get candidates functions. These set up a context to get all match candidates. + cg->reset( eqc ); + do{ + Node cand = cg->getNextCandidate(); + //....... + }while( !cand.isNull() ); + + eqc is the equivalence class you are searching in + */ + virtual void reset( Node eqc ) = 0; + virtual Node getNextCandidate() = 0; + /** add candidate to list of nodes returned by this generator */ + virtual void addCandidate( Node n ) {} + /** call this at the beginning of each instantiation round */ + virtual void resetInstantiationRound() = 0; +public: + /** legal candidate */ + bool isLegalCandidate( Node n ); +};/* class CandidateGenerator */ + +/** candidate generator queue (for manual candidate generation) */ +class CandidateGeneratorQueue : public CandidateGenerator { + private: + std::vector< Node > d_candidates; + int d_candidate_index; + + public: + CandidateGeneratorQueue( QuantifiersEngine* qe ) : CandidateGenerator( qe ), d_candidate_index( 0 ){} + + void addCandidate(Node n) override; + + void resetInstantiationRound() override {} + void reset(Node eqc) override; + Node getNextCandidate() override; +};/* class CandidateGeneratorQueue */ + +//the default generator +class CandidateGeneratorQE : public CandidateGenerator +{ + friend class CandidateGeneratorQEDisequal; + + private: + //operator you are looking for + Node d_op; + //the equality class iterator + unsigned d_op_arity; + std::vector< quantifiers::TermArgTrie* > d_tindex; + std::vector< std::map< TNode, quantifiers::TermArgTrie >::iterator > d_tindex_iter; + eq::EqClassIterator d_eqc_iter; + //std::vector< Node > d_eqc; + int d_term_iter; + int d_term_iter_limit; + bool d_using_term_db; + enum { + cand_term_db, + cand_term_ident, + cand_term_eqc, + cand_term_tindex, + cand_term_none, + }; + short d_mode; + bool isLegalOpCandidate( Node n ); + Node d_n; + std::map< Node, bool > d_exclude_eqc; + + public: + CandidateGeneratorQE( QuantifiersEngine* qe, Node pat ); + + void resetInstantiationRound() override; + void reset(Node eqc) override; + Node getNextCandidate() override; + void excludeEqc( Node r ) { d_exclude_eqc[r] = true; } + bool isExcludedEqc( Node r ) { return d_exclude_eqc.find( r )!=d_exclude_eqc.end(); } +}; + +class CandidateGeneratorQELitEq : public CandidateGenerator +{ + private: + //the equality classes iterator + eq::EqClassesIterator d_eq; + //equality you are trying to match equalities for + Node d_match_pattern; + Node d_match_gterm; + bool d_do_mgt; + + public: + CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ); + + void resetInstantiationRound() override; + void reset(Node eqc) override; + Node getNextCandidate() override; +}; + +class CandidateGeneratorQELitDeq : public CandidateGenerator +{ + private: + //the equality class iterator for false + eq::EqClassIterator d_eqc_false; + //equality you are trying to match disequalities for + Node d_match_pattern; + //type of disequality + TypeNode d_match_pattern_type; + + public: + CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ); + + void resetInstantiationRound() override; + void reset(Node eqc) override; + Node getNextCandidate() override; +}; + +class CandidateGeneratorQEAll : public CandidateGenerator +{ + private: + //the equality classes iterator + eq::EqClassesIterator d_eq; + //equality you are trying to match equalities for + Node d_match_pattern; + TypeNode d_match_pattern_type; + // quantifier/index for the variable we are matching + Node d_f; + unsigned d_index; + //first time + bool d_firstTime; + + public: + CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ); + + void resetInstantiationRound() override; + void reset(Node eqc) override; + Node getNextCandidate() override; +}; + +}/* CVC4::theory::inst namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */ diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index c36597e3e..ec0a4039a 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -17,11 +17,11 @@ #include "expr/datatype.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/candidate_generator.h" +#include "theory/quantifiers/ematching/candidate_generator.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers_engine.h" using namespace std; @@ -541,14 +541,6 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Node q, Node n) } Trace("var-trigger-debug") << "Is " << n << " a variable trigger?" << std::endl; - if (Trigger::isBooleanTermTrigger(n)) - { - VarMatchGeneratorBooleanTerm* vmg = - new VarMatchGeneratorBooleanTerm(n[0], n[1]); - Trace("var-trigger") << "Boolean term trigger : " << n << ", var = " << n[0] - << std::endl; - return vmg; - } Node x; if (options::purifyTriggers()) { @@ -565,38 +557,6 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Node q, Node n) return new InstMatchGenerator(n); } -VarMatchGeneratorBooleanTerm::VarMatchGeneratorBooleanTerm( Node var, Node comp ) : - InstMatchGenerator(), d_comp( comp ), d_rm_prev( false ) { - d_children_types.push_back(var.getAttribute(InstVarNumAttribute())); -} - -int VarMatchGeneratorBooleanTerm::getNextMatch(Node q, - InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent) -{ - int ret_val = -1; - 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_children_types[0]).isNull(); - if (!m.set(qe->getEqualityQuery(), d_children_types[0], s)) - { - return -1; - }else{ - ret_val = continueNextMatch(q, m, qe, tparent); - if( ret_val>0 ){ - return ret_val; - } - } - } - if( d_rm_prev ){ - 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_children_types.push_back(d_var.getAttribute(InstVarNumAttribute())); diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index 6c38db13b..cbd5702a0 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -418,32 +418,6 @@ class InstMatchGenerator : public IMGenerator { static InstMatchGenerator* getInstMatchGenerator(Node q, Node n); };/* class InstMatchGenerator */ -/** match generator for Boolean term ITEs -* This handles the special case of triggers that look like ite( x, BV1, BV0 ). -*/ -class VarMatchGeneratorBooleanTerm : public InstMatchGenerator { -public: - VarMatchGeneratorBooleanTerm( Node var, Node comp ); - - /** Reset */ - bool reset(Node eqc, QuantifiersEngine* qe) override - { - d_eq_class = eqc; - return true; - } - /** Get the next match. */ - int getNextMatch(Node q, - InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent) override; - - private: - /** stores the true branch of the Boolean ITE */ - Node d_comp; - /** stores whether we have written a value for var in the current match. */ - bool d_rm_prev; -}; - /** match generator for purified terms * This handles the special case of invertible terms like x+1 (see * Trigger::getTermInversionVariable). diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 430d261a1..4039c632f 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -15,7 +15,7 @@ #include "theory/quantifiers/ematching/trigger.h" #include "theory/arith/arith_msum.h" -#include "theory/quantifiers/candidate_generator.h" +#include "theory/quantifiers/ematching/candidate_generator.h" #include "theory/quantifiers/ematching/ho_trigger.h" #include "theory/quantifiers/ematching/inst_match_generator.h" #include "theory/quantifiers/instantiate.h" @@ -262,9 +262,8 @@ bool Trigger::isUsable( Node n, Node q ){ return true; }else{ std::map< Node, Node > coeffs; - if( isBooleanTermTrigger( n ) ){ - return true; - }else if( options::purifyTriggers() ){ + if (options::purifyTriggers()) + { Node x = getInversionVariable( n ); if( !x.isNull() ){ return true; @@ -522,22 +521,6 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod } } -bool Trigger::isBooleanTermTrigger( Node n ) { - if( n.getKind()==ITE ){ - //check for boolean term converted to ITE - if( n[0].getKind()==INST_CONSTANT && - n[1].getKind()==CONST_BITVECTOR && - n[2].getKind()==CONST_BITVECTOR ){ - if( ((BitVectorType)n[1].getType().toType()).getSize()==1 && - n[1].getConst<BitVector>().toInteger()==1 && - n[2].getConst<BitVector>().toInteger()==0 ){ - return true; - } - } - } - return false; -} - bool Trigger::isPureTheoryTrigger( Node n ) { if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){ //|| !quantifiers::TermUtil::hasInstConstAttr( n ) ){ return false; diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index cd10e4f8a..28d227bf7 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -315,8 +315,6 @@ class Trigger { static bool isRelationalTriggerKind( Kind k ); /** is n a simple trigger (see inst_match_generator.h)? */ static bool isSimpleTrigger( Node n ); - /** is n a Boolean term trigger, e.g. ite( x, BV1, BV0 )? */ - static bool isBooleanTermTrigger( Node n ); /** is n a pure theory trigger, e.g. head( x )? */ static bool isPureTheoryTrigger( Node n ); /** get trigger weight |