diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-07 11:30:00 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-08 11:20:53 -0400 |
| commit | 5c7c2c3d0968289b254aeafe10f1267e21123d98 (patch) | |
| tree | ee995f4e46f96403929b2ed7874628fc463a6808 /src/smt | |
| parent | d813626606c5eca8179eec492090b85dbd818867 (diff) | |
Fixes for Boolean terms in arrays (including fix for bug 517).
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/boolean_terms.cpp | 34 |
1 files changed, 33 insertions, 1 deletions
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", |