diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-01 17:34:27 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-01 20:09:21 -0400 |
commit | 4d7cff8156c2e409be209f1ee489dcf05f922d50 (patch) | |
tree | b0b7ba4e98cee86b3c37094c90c980c0042db475 /src/smt/model_postprocessor.cpp | |
parent | a197d41f1945dcaf64cc80fff5ac3a828c0ba0d2 (diff) |
Fixes for two bugs:
* one that Tim found in model generation for records containing Booleans
* another that the fuzzer found in quantifiers + check-models
Test cases enabled/added for both.
Diffstat (limited to 'src/smt/model_postprocessor.cpp')
-rw-r--r-- | src/smt/model_postprocessor.cpp | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp index fb80b27f7..de1a60da4 100644 --- a/src/smt/model_postprocessor.cpp +++ b/src/smt/model_postprocessor.cpp @@ -48,6 +48,31 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) { return NodeManager::currentNM()->mkConst(tf); } } + if(n.getType().isBoolean()) { + bool tf = n.getConst<bool>(); + if(asType.isBitVector(1u)) { + return NodeManager::currentNM()->mkConst(BitVector(1u, tf ? 1u : 0u)); + } + if(asType.isDatatype() && asType.hasAttribute(BooleanTermAttr())) { + const Datatype& asDatatype = asType.getConst<Datatype>(); + return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, (tf ? asDatatype[0] : asDatatype[1]).getConstructor()); + } + } + if(n.getType().isRecord() && asType.isRecord()) { + Debug("boolean-terms") << "+++ got a record - rewriteAs " << n << " : " << asType << endl; + const Record& rec CVC4_UNUSED = n.getType().getConst<Record>(); + const Record& asRec = asType.getConst<Record>(); + Assert(rec.getNumFields() == asRec.getNumFields()); + Assert(n.getNumChildren() == asRec.getNumFields()); + NodeBuilder<> b(n.getKind()); + b << asType; + for(size_t i = 0; i < n.getNumChildren(); ++i) { + b << rewriteAs(n[i], TypeNode::fromType(asRec[i].second)); + } + Node out = b; + Debug("boolean-terms") << "+++ returning record " << out << endl; + return out; + } Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << endl; if(n.getType().isArray()) { Assert(asType.isArray()); |