summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/trigger.h
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2016-07-05 15:11:28 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2016-07-05 15:11:38 -0500
commit967747b7b279256bd9368e2d392ae71dec1bb1c1 (patch)
tree18a811b16d7552c1ae52fadfe34e54acde68e6a8 /src/theory/quantifiers/trigger.h
parenta58abbe71fb1fc07129ff9c7568ac544145fb57c (diff)
Add option --trigger-active-sel. Recognize simple triggers with polarity. Do not drop patterns from merged prenex (fixes bug 743).
Diffstat (limited to 'src/theory/quantifiers/trigger.h')
-rw-r--r--src/theory/quantifiers/trigger.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index a3da4d398..6d7bf1f4d 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -134,6 +134,7 @@ class Trigger {
}
Trace(c) << " )";
}
+ int getActiveScore();
private:
/** trigger constructor */
Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback