diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-22 11:47:39 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-22 11:47:39 +0100 |
commit | d9d13027f1f1e3cc462dc5885dfd0b529bf57512 (patch) | |
tree | 656f7c02d1522c5c52eb7952947a8a76a4693521 /src/theory/quantifiers/theory_quantifiers.cpp | |
parent | 9867d5a61ccde30f7e4616a652ef86a9b15ae6d8 (diff) |
Add option --lte-partial-inst. Remove inst-closure.
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.cpp')
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index de0f98af6..89549a71b 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -129,22 +129,12 @@ void TheoryQuantifiers::check(Effort e) { case kind::FORALL: assertUniversal( assertion ); break; - case kind::INST_CLOSURE: - getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true ); - break; - case kind::EQUAL: - //do nothing - break; case kind::NOT: { switch( assertion[0].getKind()) { case kind::FORALL: assertExistential( assertion ); break; - case kind::EQUAL: - //do nothing - break; - case kind::INST_CLOSURE: //cannot negate inst closure default: Unhandled(assertion[0].getKind()); break; |