diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-23 10:04:38 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-23 10:04:38 +0100 |
| commit | 7ff0098a91df9c912cbe98fb128fcf2cbc71e95c (patch) | |
| tree | 07aee959b4e48eda5ccc1580f4bc56adb7c53387 /src/theory/quantifiers/theory_quantifiers.cpp | |
| parent | 732dc4232ccf62d9b4a3ddf49fcfbd56efabcd41 (diff) | |
Rework inst-closure.
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.cpp')
| -rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 89549a71b..12edaa31c 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -129,12 +129,22 @@ 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: default: Unhandled(assertion[0].getKind()); break; |