diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-22 10:52:46 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-26 16:30:16 -0500 |
| commit | f0e49547916c713dc53e81192adde66950caaa9b (patch) | |
| tree | 599210ad254cee10163eff306c1e97caa7bd5601 /src | |
| parent | c542c62d8f7c6dde84406c7e1640c029fe6cab29 (diff) | |
Fix for quantifiers containing Boolean terms.
Diffstat (limited to 'src')
| -rw-r--r-- | src/smt/boolean_terms.cpp | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 696622cfe..262244f42 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -39,6 +39,13 @@ static inline bool isBoolean(TNode top, unsigned i) { case kind::IMPLIES: case kind::OR: case kind::XOR: + case kind::FORALL: + case kind::EXISTS: + case kind::REWRITE_RULE: + case kind::RR_REWRITE: + case kind::RR_DEDUCTION: + case kind::RR_REDUCTION: + case kind::INST_PATTERN: return true; case kind::ITE: @@ -289,13 +296,16 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw } switch(k) { case kind::LAMBDA: - case kind::FORALL: - case kind::EXISTS: + Unreachable("not expecting a LAMBDA in boolean-term conversion: %s", top.toString().c_str()); + + case kind::BOUND_VAR_LIST: + return top; + case kind::REWRITE_RULE: case kind::RR_REWRITE: - case kind::RR_REDUCTION: case kind::RR_DEDUCTION: - //Assert(false, "not yet supported"); + case kind::RR_REDUCTION: + // not yet supported return top; default: |