diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-08-25 12:50:55 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-08-25 12:51:03 +0200 |
| commit | ce6c89be30b18a331fd08f843b9d4ee8d6bb1ced (patch) | |
| tree | 80669b968bc39056b1cf394bc9850bf969849f0d /src/theory/quantifiers/trigger.h | |
| parent | 8fc068f1f70f5f8e6f5494d7709d681cc9d7d7f9 (diff) | |
New option --purify-triggers. Refactoring of InstMatchGenerator.
Diffstat (limited to 'src/theory/quantifiers/trigger.h')
| -rw-r--r-- | src/theory/quantifiers/trigger.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 17da6f0d5..42b7598ea 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -30,6 +30,7 @@ class QuantifiersEngine; namespace inst { class IMGenerator; +class InstMatchGenerator; //a collect of nodes representing a trigger class Trigger { @@ -112,6 +113,10 @@ public: /** get pattern arithmetic */ static bool isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeffs ); static bool isBooleanTermTrigger( Node n ); + /** return data structure for producing matches for this trigger. */ + static InstMatchGenerator* getInstMatchGenerator( Node n ); + static Node getInversionVariable( Node n ); + static Node getInversion( Node n, Node x ); inline void toStream(std::ostream& out) const { /* |