summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/theory_quantifiers.cpp
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2016-08-25 15:41:27 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2016-08-25 15:41:27 -0500
commit2e7ec13174e165cccc74159b5c6590d12894a674 (patch)
treeb6c8603af05019571671798ac373ffa3e51d3335 /src/theory/quantifiers/theory_quantifiers.cpp
parentdce53c4de6dd7482d9784388cc61753352f241d8 (diff)
Minor cleanup preprocessing, add ppNotifyAssertions.
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.cpp')
-rw-r--r--src/theory/quantifiers/theory_quantifiers.cpp4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 7ad13b3a8..f6ee639b6 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -88,6 +88,10 @@ void TheoryQuantifiers::presolve() {
}
}
+void TheoryQuantifiers::ppNotifyAssertions( std::vector< Node >& assertions ) {
+ getQuantifiersEngine()->ppNotifyAssertions( assertions );
+}
+
Node TheoryQuantifiers::getValue(TNode n) {
//NodeManager* nodeManager = NodeManager::currentNM();
switch(n.getKind()) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback