diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-07 13:43:31 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-07 13:43:37 -0600 |
| commit | d2e45128356c725d479a3efff475d8e5f430e4f3 (patch) | |
| tree | f28916d982f359bad1147a22b3d3526f02f538d0 | |
| parent | 1ce3fb16b0e0e3a51713d643e792499775a7f11b (diff) | |
Fix boolean term conversion for INST_ATTRIBUTE, fixes bug 764.
| -rw-r--r-- | src/smt/boolean_terms.cpp | 4 | ||||
| -rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/fmf/bug764.smt2 | 28 |
3 files changed, 32 insertions, 3 deletions
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) + |