diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-12-01 14:36:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-12-01 14:36:14 +0000 |
commit | ec29471e427bf25034a93c182b424730d439a90a (patch) | |
tree | f4ddc215f2e78b72fdff2fa62fc8561b7dec84be /src/smt/boolean_terms.cpp | |
parent | 265765c9f5c35c4b65934e574dbfabab97b15f7a (diff) |
Fix the way abstract values are typed; fixes some compliance issues.
Also support array-store-all for Boolean terms (related to abstract values, since that's the only way for the user to include an array-store-all in an assertion).
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/smt/boolean_terms.cpp')
-rw-r--r-- | src/smt/boolean_terms.cpp | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index dda9c7a3e..696622cfe 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -121,6 +121,33 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw } if(mk == kind::metakind::CONSTANT) { + if(k == kind::STORE_ALL) { + const ArrayStoreAll& asa = top.getConst<ArrayStoreAll>(); + ArrayType arrType = asa.getType(); + TypeNode indexType = TypeNode::fromType(arrType.getIndexType()); + Type constituentType = arrType.getConstituentType(); + if(constituentType.isBoolean()) { + // we have store_all(true) or store_all(false) + // just turn it into store_all(1) or store_all(0) + Node newConst = nm->mkConst(BitVector(1u, asa.getExpr().getConst<bool>() ? 1u : 0u)); + if(indexType.isBoolean()) { + // change index type to BV(1) also + indexType = nm->mkBitVectorType(1); + } + ArrayStoreAll asaRepl(nm->mkArrayType(indexType, nm->mkBitVectorType(1)).toType(), newConst.toExpr()); + Node n = nm->mkConst(asaRepl); + Debug("boolean-terms") << " returning new store_all: " << n << std::endl; + return n; + } + if(indexType.isBoolean()) { + // must change index type to BV(1) + indexType = nm->mkBitVectorType(1); + ArrayStoreAll asaRepl(nm->mkArrayType(indexType, TypeNode::fromType(constituentType)).toType(), asa.getExpr()); + Node n = nm->mkConst(asaRepl); + Debug("boolean-terms") << " returning new store_all: " << n << std::endl; + return n; + } + } return top; } else if(mk == kind::metakind::VARIABLE) { TypeNode t = top.getType(); |