diff options
Diffstat (limited to 'src/theory/quantifiers/trigger.h')
-rw-r--r-- | src/theory/quantifiers/trigger.h | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 41f2a1c38..902f73e75 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -76,6 +76,8 @@ class Trigger { int addTerm( Node t ); /** return whether this is a multi-trigger */ bool isMultiTrigger() { return d_nodes.size()>1; } + /** get inst pattern list */ + Node getInstPattern(); /** add all available instantiations exhaustively, in any equivalence class if limitInst>0, limitInst is the max # of instantiations to try */ @@ -84,8 +86,6 @@ class Trigger { ie : quantifier engine; f : forall something .... nodes : (multi-)trigger - matchOption : which policy to use for creating matches - (one of InstMatchGenerator::MATCH_GEN_* ) keepAll: don't remove unneeded patterns; trOption : policy for dealing with triggers that already existed (see below) @@ -95,12 +95,12 @@ class Trigger { TR_GET_OLD, //return a previous trigger if it had already been created TR_RETURN_NULL //return null if a duplicate is found }; - static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, - std::vector< Node >& nodes, int matchOption = 0, - bool keepAll = true, int trOption = TR_MAKE_NEW ); - static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n, - int matchOption = 0, bool keepAll = true, - int trOption = TR_MAKE_NEW ); + //nodes input, trNodes output + static bool mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_vars, std::vector< Node >& trNodes ); + static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, + bool keepAll = true, int trOption = TR_MAKE_NEW, unsigned use_n_vars = 0 ); + static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n, bool keepAll = true, + int trOption = TR_MAKE_NEW, unsigned use_n_vars = 0 ); static void collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::map< Node, TriggerTermInfo >& tinfo, bool filterInst = false ); @@ -135,7 +135,7 @@ class Trigger { } private: /** trigger constructor */ - Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, int matchOption = 0 ); + Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes ); /** is subterm of trigger usable */ static bool isUsable( Node n, Node q ); |