From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 7 Dec 2016 19:43:31 +0000 (-0600)
Subject: Fix boolean term conversion for INST_ATTRIBUTE, fixes bug 764.
X-Git-Tag: cvc5-1.0.0~5948
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d2e45128356c725d479a3efff475d8e5f430e4f3;p=cvc5.git

Fix boolean term conversion for INST_ATTRIBUTE, fixes bug 764.
---

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index ba7902d32..bcacd4bd4 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -706,7 +706,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
         goto next_worklist;
       }
       switch(k) {
-      case kind::INST_ATTRIBUTE:
+      //case kind::INST_ATTRIBUTE:
       case kind::BOUND_VAR_LIST:
         result.top() << top;
         worklist.pop();
@@ -819,7 +819,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
         // push children
         for(int i = top.getNumChildren() - 1; i >= 0; --i) {
           Debug("bt") << "rewriting: " << top[i] << endl;
-          worklist.push(triple<TNode, theory::TheoryId, bool>(top[i], top.getKind() == kind::CHAIN ? parentTheory : (isBoolean(top, i) ? theory::THEORY_BOOL : (top.getKind() == kind::APPLY_CONSTRUCTOR ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN)), false));
+          worklist.push(triple<TNode, theory::TheoryId, bool>(top[i], top.getKind() == kind::CHAIN ? parentTheory : ((isBoolean(top, i) || top.getKind()==kind::INST_ATTRIBUTE) ? theory::THEORY_BOOL : (top.getKind() == kind::APPLY_CONSTRUCTOR ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN)), false));
           //b << rewriteBooleanTermsRec(top[i], isBoolean(top, i) ? , quantBoolVars);
           //Debug("bt") << "got: " << b[b.getNumChildren() - 1] << endl;
         }
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index d734a6b95..218dde7d4 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -62,7 +62,8 @@ TESTS =	\
 	fmf-strange-bounds.smt2 \
 	fmf-strange-bounds-2.smt2 \
 	fmf-bound-2dim.smt2 \
-	memory_model-R_cpp-dd.cvc
+	memory_model-R_cpp-dd.cvc \
+	bug764.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/fmf/bug764.smt2 b/test/regress/regress0/fmf/bug764.smt2
new file mode 100644
index 000000000..d030c3e88
--- /dev/null
+++ b/test/regress/regress0/fmf/bug764.smt2
@@ -0,0 +1,28 @@
+; COMMAND-LINE: --fmf-fun --no-check-models
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+
+(define-fun BoolToString ((b Bool)) String (ite b "true" "false") )
+
+(declare-datatypes () (
+    (Color (red) (white) (blue))
+) )
+
+(define-fun ColorToString ((c Color)) String (ite (is-red c) "red" (ite (is-white c) "white" "blue")) )
+
+(declare-datatypes () (
+    (CP (cp (b Bool) (c Color)))
+) )
+
+(define-fun-rec CPToString ((cp CP)) String (str.++ "cp(" (BoolToString (b cp)) "," (ColorToString (c cp)) ")"))
+
+(declare-fun CPFromString (String) CP)
+
+(assert (forall ((cp1 CP)) (= cp1 (CPFromString (CPToString cp1)))))
+
+(declare-fun cpx() CP)
+(assert (= cpx (CPFromString "cp(true,white)")))
+
+(check-sat)
+