From 5c7c2c3d0968289b254aeafe10f1267e21123d98 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 7 Jun 2013 11:30:00 -0400 Subject: [PATCH] Fixes for Boolean terms in arrays (including fix for bug 517). --- src/expr/type_node.cpp | 9 ++++++ src/smt/boolean_terms.cpp | 34 +++++++++++++++++++++- src/theory/arrays/theory_arrays_rewriter.h | 14 +++++---- 3 files changed, 51 insertions(+), 6 deletions(-) diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index e654b5d71..1d4c330fa 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -123,6 +123,15 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { } return true; } + if(isFunction()) { + // A function is a subtype of another if the args are the same type, and + // the return type is a subtype of the other's. This is enough for now + // (and it's necessary for model generation, since a Real-valued function + // might return a constant Int and thus the model value is typed differently). + return t.isFunction() && + getArgTypes() == t.getArgTypes() && + getRangeType().isSubtypeOf(t.getRangeType()); + } if(isPredicateSubtype()) { return getSubtypeParentType().isSubtypeOf(t); } diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 166a695a4..b3e69619f 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -487,7 +487,39 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa } else if(t.isArray()) { TypeNode indexType = convertType(t.getArrayIndexType(), false); TypeNode constituentType = convertType(t.getArrayConstituentType(), false); - if(indexType != t.getArrayIndexType() || constituentType != t.getArrayConstituentType()) { + if(indexType != t.getArrayIndexType() && constituentType == t.getArrayConstituentType()) { + TypeNode newType = nm->mkArrayType(indexType, constituentType); + Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'", + newType, "an array variable introduced by Boolean-term conversion", + NodeManager::SKOLEM_EXACT_NAME); + top.setAttribute(BooleanTermAttr(), n); + Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; + Node n_ff = nm->mkNode(kind::SELECT, n, d_ff); + Node n_tt = nm->mkNode(kind::SELECT, n, d_tt); + Node base = nm->mkConst(ArrayStoreAll(ArrayType(top.getType().toType()), (*TypeEnumerator(n_ff.getType())).toExpr())); + Node repl = nm->mkNode(kind::STORE, + nm->mkNode(kind::STORE, base, nm->mkConst(true), + n_tt), + nm->mkConst(false), n_ff); + Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl; + d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl); + d_termCache[make_pair(top, parentTheory)] = n; + result.top() << n; + worklist.pop(); + goto next_worklist; + } else if(indexType == t.getArrayIndexType() && constituentType != t.getArrayConstituentType()) { + TypeNode newType = nm->mkArrayType(indexType, constituentType); + Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'", + newType, "an array variable introduced by Boolean-term conversion", + NodeManager::SKOLEM_EXACT_NAME); + top.setAttribute(BooleanTermAttr(), n); + Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; + d_smt.d_theoryEngine->getModel()->addSubstitution(top, n); + d_termCache[make_pair(top, parentTheory)] = n; + result.top() << n; + worklist.pop(); + goto next_worklist; + } else if(indexType != t.getArrayIndexType() && constituentType != t.getArrayConstituentType()) { TypeNode newType = nm->mkArrayType(indexType, constituentType); Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'", newType, "an array variable introduced by Boolean-term conversion", diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 18bbef8cf..5df06bda8 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -36,6 +36,10 @@ namespace attr { typedef expr::Attribute ArrayConstantMostFrequentValueCountAttr; typedef expr::Attribute ArrayConstantMostFrequentValueAttr; +static inline Node mkEqNode(Node a, Node b) { + return a.getType().isBoolean() ? a.iffNode(b) : a.eqNode(b); +} + class TheoryArraysRewriter { static Node normalizeConstant(TNode node) { return normalizeConstant(node, node[1].getType().getCardinality()); @@ -244,7 +248,7 @@ public: val = false; } else { - n = Rewriter::rewrite(store[1].eqNode(index)); + n = Rewriter::rewrite(mkEqNode(store[1], index)); if (n.getKind() != kind::CONST_BOOLEAN) { break; } @@ -301,7 +305,7 @@ public: val = false; } else { - Node eqRewritten = Rewriter::rewrite(store[1].eqNode(index)); + Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index)); if (eqRewritten.getKind() != kind::CONST_BOOLEAN) { Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << node << std::endl; return RewriteResponse(REWRITE_DONE, node); @@ -340,7 +344,7 @@ public: val = false; } else { - n = Rewriter::rewrite(store[1].eqNode(index)); + n = Rewriter::rewrite(mkEqNode(store[1], index)); if (n.getKind() != kind::CONST_BOOLEAN) { break; } @@ -416,7 +420,7 @@ public: val = false; } else { - n = Rewriter::rewrite(store[1].eqNode(index)); + n = Rewriter::rewrite(mkEqNode(store[1], index)); if (n.getKind() != kind::CONST_BOOLEAN) { break; } @@ -466,7 +470,7 @@ public: val = false; } else { - Node eqRewritten = Rewriter::rewrite(store[1].eqNode(index)); + Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index)); if (eqRewritten.getKind() != kind::CONST_BOOLEAN) { break; } -- 2.30.2