From f0e49547916c713dc53e81192adde66950caaa9b Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 22 Feb 2013 10:52:46 -0500 Subject: [PATCH] Fix for quantifiers containing Boolean terms. --- src/smt/boolean_terms.cpp | 18 ++++++++++++++---- 1 file 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: -- 2.30.2