diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-28 17:31:57 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-22 18:54:52 -0400 |
commit | f44a81d1b62058fa56af952aa92be965690481e5 (patch) | |
tree | dc4b56e27701abd61ebd69675f86a9366d90998f /src/smt/model_postprocessor.cpp | |
parent | 36816ad2537a2e6163037e9592c513b9a69aa9dc (diff) |
Support for Boolean term conversion in datatypes.
Diffstat (limited to 'src/smt/model_postprocessor.cpp')
-rw-r--r-- | src/smt/model_postprocessor.cpp | 151 |
1 files changed, 142 insertions, 9 deletions
diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp index 26f5c9c60..fb80b27f7 100644 --- a/src/smt/model_postprocessor.cpp +++ b/src/smt/model_postprocessor.cpp @@ -17,37 +17,170 @@ #include "smt/model_postprocessor.h" #include "smt/boolean_terms.h" +using namespace std; using namespace CVC4; using namespace CVC4::smt; +Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) { + if(n.getType().isSubtypeOf(asType)) { + // good to go, we have the right type + return n; + } + if(!n.isConst()) { + // we don't handle non-const right now + return n; + } + if(asType.isBoolean()) { + if(n.getType().isBitVector(1u)) { + // type mismatch: should only happen for Boolean-term conversion under + // datatype constructor applications; rewrite from BV(1) back to Boolean + bool tf = (n.getConst<BitVector>().getValue() == 1); + return NodeManager::currentNM()->mkConst(tf); + } + if(n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())) { + // type mismatch: should only happen for Boolean-term conversion under + // datatype constructor applications; rewrite from datatype back to Boolean + Assert(n.getKind() == kind::APPLY_CONSTRUCTOR); + Assert(n.getNumChildren() == 0); + // we assume (by construction) false is first; see boolean_terms.cpp + bool tf = (Datatype::indexOf(n.getOperator().toExpr()) == 1); + Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << " ==> " << tf << endl; + return NodeManager::currentNM()->mkConst(tf); + } + } + Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << endl; + if(n.getType().isArray()) { + Assert(asType.isArray()); + if(n.getKind() == kind::STORE) { + return NodeManager::currentNM()->mkNode(kind::STORE, + rewriteAs(n[0], asType), + rewriteAs(n[1], asType[0]), + rewriteAs(n[2], asType[1])); + } + Assert(n.getKind() == kind::STORE_ALL); + const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>(); + Node val = rewriteAs(asa.getExpr(), asType[1]); + return NodeManager::currentNM()->mkConst(ArrayStoreAll(asType.toType(), val.toExpr())); + } + if(asType.getNumChildren() != n.getNumChildren() || + n.getMetaKind() == kind::metakind::CONSTANT) { + return n; + } + NodeBuilder<> b(n.getKind()); + TypeNode::iterator t = asType.begin(); + for(TNode::iterator i = n.begin(); i != n.end(); ++i, ++t) { + Assert(t != asType.end()); + b << rewriteAs(*i, *t); + } + Assert(t == asType.end()); + Debug("boolean-terms") << "+++ constructing " << b << endl; + Node out = b; + return out; +} + void ModelPostprocessor::visit(TNode current, TNode parent) { - Debug("tuprec") << "visiting " << current << std::endl; + Debug("tuprec") << "visiting " << current << endl; Assert(!alreadyVisited(current, TNode::null())); if(current.getType().hasAttribute(expr::DatatypeTupleAttr())) { Assert(current.getKind() == kind::APPLY_CONSTRUCTOR); + TypeNode expectType = current.getType().getAttribute(expr::DatatypeTupleAttr()); NodeBuilder<> b(kind::TUPLE); - for(TNode::iterator i = current.begin(); i != current.end(); ++i) { + TypeNode::iterator t = expectType.begin(); + for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) { Assert(alreadyVisited(*i, TNode::null())); + Assert(t != expectType.end()); TNode n = d_nodes[*i]; - b << (n.isNull() ? *i : n); + n = n.isNull() ? *i : n; + if(!n.getType().isSubtypeOf(*t)) { + Assert(n.getType().isBitVector(1u) || + (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr()))); + Assert(n.isConst()); + Assert((*t).isBoolean()); + if(n.getType().isBitVector(1u)) { + b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1)); + } else { + // we assume (by construction) false is first; see boolean_terms.cpp + b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1)); + } + } else { + b << n; + } } + Assert(t == expectType.end()); d_nodes[current] = b; - Debug("tuprec") << "returning " << d_nodes[current] << std::endl; + Debug("tuprec") << "returning " << d_nodes[current] << endl; + Assert(d_nodes[current].getType() == expectType); } else if(current.getType().hasAttribute(expr::DatatypeRecordAttr())) { Assert(current.getKind() == kind::APPLY_CONSTRUCTOR); + TypeNode expectType = current.getType().getAttribute(expr::DatatypeRecordAttr()); + const Record& expectRec = expectType.getConst<Record>(); NodeBuilder<> b(kind::RECORD); b << current.getType().getAttribute(expr::DatatypeRecordAttr()); - for(TNode::iterator i = current.begin(); i != current.end(); ++i) { + Record::const_iterator t = expectRec.begin(); + for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) { Assert(alreadyVisited(*i, TNode::null())); + Assert(t != expectRec.end()); TNode n = d_nodes[*i]; - b << (n.isNull() ? *i : n); + n = n.isNull() ? *i : n; + if(!n.getType().isSubtypeOf(TypeNode::fromType((*t).second))) { + Assert(n.getType().isBitVector(1u) || + (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr()))); + Assert(n.isConst()); + Assert((*t).second.isBoolean()); + if(n.getType().isBitVector(1u)) { + b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1)); + } else { + // we assume (by construction) false is first; see boolean_terms.cpp + b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1)); + } + } else { + b << n; + } } + Assert(t == expectRec.end()); d_nodes[current] = b; - Debug("tuprec") << "returning " << d_nodes[current] << std::endl; + Debug("tuprec") << "returning " << d_nodes[current] << endl; + Assert(d_nodes[current].getType() == expectType); + } else if(current.getKind() == kind::APPLY_CONSTRUCTOR && + ( current.getOperator().hasAttribute(BooleanTermAttr()) || + ( current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION && + current.getOperator()[0].hasAttribute(BooleanTermAttr()) ) )) { + NodeBuilder<> b(kind::APPLY_CONSTRUCTOR); + Node realOp; + if(current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION) { + TNode oldAsc = current.getOperator().getOperator(); + Debug("boolean-terms") << "old asc: " << oldAsc << endl; + Node newCons = current.getOperator()[0].getAttribute(BooleanTermAttr()); + Node newAsc = NodeManager::currentNM()->mkConst(AscriptionType(newCons.getType().toType())); + Debug("boolean-terms") << "new asc: " << newAsc << endl; + if(newCons.getType().getRangeType().isParametricDatatype()) { + vector<TypeNode> oldParams = TypeNode::fromType(oldAsc.getConst<AscriptionType>().getType()).getRangeType().getParamTypes(); + vector<TypeNode> newParams = newCons.getType().getRangeType().getParamTypes(); + Assert(oldParams.size() == newParams.size() && oldParams.size() > 0); + newAsc = NodeManager::currentNM()->mkConst(AscriptionType(newCons.getType().substitute(newParams.begin(), newParams.end(), oldParams.begin(), oldParams.end()).toType())); + } + realOp = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, newAsc, newCons); + } else { + realOp = current.getOperator().getAttribute(BooleanTermAttr()); + } + b << realOp; + Debug("boolean-terms") << "+ op " << b.getOperator() << endl; + TypeNode::iterator j = realOp.getType().begin(); + for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++j) { + Assert(j != realOp.getType().end()); + Assert(alreadyVisited(*i, TNode::null())); + TNode repl = d_nodes[*i]; + repl = repl.isNull() ? *i : repl; + Debug("boolean-terms") << "+ adding " << repl << " expecting " << *j << endl; + b << rewriteAs(repl, *j); + } + Node n = b; + Debug("boolean-terms") << "model-post: " << current << endl + << "- returning " << n << endl; + d_nodes[current] = n; } else { - Debug("tuprec") << "returning self" << std::endl; + Debug("tuprec") << "returning self for kind " << current.getKind() << endl; // rewrite to self d_nodes[current] = Node::null(); } }/* ModelPostprocessor::visit() */ - |