diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-29 21:34:16 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-29 21:34:16 +0000 |
commit | 03a8787579038655fff814fbad05047ce24bf532 (patch) | |
tree | e9b632bfd9b7a91e53141bef42f8f7d2b81c5184 /src/smt/boolean_terms.cpp | |
parent | eab3aa931049d9ade69ad0ee5ebf8116c4f54ce6 (diff) |
fix for andy: boolean terms stuff really shouldn't look at datatypes at all in this release
Diffstat (limited to 'src/smt/boolean_terms.cpp')
-rw-r--r-- | src/smt/boolean_terms.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
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<Datatype>(); 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<Datatype>(); 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<Datatype>(); 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 && |