diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-04-10 15:50:56 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-04-10 15:51:08 -0500 |
| commit | 6ae07a91cdd4f20f8fdccd7e31d217c6ca34ee45 (patch) | |
| tree | 0f4f929831ba092b54a5919809a01f089e023b84 /src/smt/boolean_terms.cpp | |
| parent | 65128efc1d0a4c2007ebb7b47712888481c07843 (diff) | |
Expand definitions in theory datatypes, now has the expected semantics for incorrectly applied selector terms.
Diffstat (limited to 'src/smt/boolean_terms.cpp')
| -rw-r--r-- | src/smt/boolean_terms.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 111324dfa..e46a76ed7 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -152,7 +152,7 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() { NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR); appctorb << (*dt2)[i].getConstructor(); for(size_t j = 0; j < ctor.getNumArgs(); ++j) { - appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType())); + appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType())); } Node appctor = appctorb; if(i == 0) { @@ -191,7 +191,7 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() { for(size_t j = 0; j < ctor.getNumArgs(); ++j) { TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()); asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end()); - appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, ctor[j].getSelector(), in), asType); + appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), asType); } Node appctor = appctorb; if(i == 0) { |