From 03a8787579038655fff814fbad05047ce24bf532 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 29 Nov 2012 21:34:16 +0000 Subject: [PATCH] fix for andy: boolean terms stuff really shouldn't look at datatypes at all in this release --- src/smt/boolean_terms.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index f90b5ff51..15a1244e2 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -166,6 +166,7 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw } else if(t.isRecord()) { return top; } else if(t.isDatatype()) { + return top;// no support for datatypes at present const Datatype& dt = t.getConst(); const Datatype& dt2 = booleanTermsConvertDatatype(dt); if(dt != dt2) { @@ -185,6 +186,7 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw return top; } } else if(t.isConstructor()) { + return top;// no support for datatypes at present Assert(!boolParent); const Datatype& dt = t[t.getNumChildren() - 1].getConst(); const Datatype& dt2 = booleanTermsConvertDatatype(dt); @@ -197,6 +199,7 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw return top; } } else if(t.isTester() || t.isSelector()) { + return top;// no support for datatypes at present Assert(!boolParent); const Datatype& dt = t[0].getConst(); const Datatype& dt2 = booleanTermsConvertDatatype(dt); @@ -242,6 +245,7 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw Debug("bt") << "looking at: " << top << std::endl; if(mk == kind::metakind::PARAMETERIZED) { if(kindToTheoryId(k) != THEORY_BV && + k != kind::APPLY_TYPE_ASCRIPTION && k != kind::TUPLE_SELECT && k != kind::TUPLE_UPDATE && k != kind::RECORD_SELECT && -- 2.30.2