summaryrefslogtreecommitdiff
path: root/src/smt/boolean_terms.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/boolean_terms.cpp')
-rw-r--r--src/smt/boolean_terms.cpp75
1 files changed, 10 insertions, 65 deletions
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 4372c0c18..07d78a6fd 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -139,14 +139,15 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode,
processing[in_t] = true;
if(in.getType().isRecord()) {
Assert(as.isRecord());
- const Record& inRec = in.getType().getConst<Record>();
- const Record& asRec = as.getConst<Record>();
+ const Record& inRec = in.getType().getRecord();
+ const Record& asRec = as.getRecord();
Assert(inRec.getNumFields() == asRec.getNumFields());
- NodeBuilder<> nb(kind::RECORD);
+ const Datatype & dt = ((DatatypeType)in.getType().toType()).getDatatype();
+ NodeBuilder<> nb(kind::APPLY_CONSTRUCTOR);
nb << NodeManager::currentNM()->mkConst(asRec);
for(size_t i = 0; i < asRec.getNumFields(); ++i) {
Assert(inRec[i].first == asRec[i].first);
- Node arg = NodeManager::currentNM()->mkNode(NodeManager::currentNM()->mkConst(RecordSelect(inRec[i].first)), in);
+ Node arg = NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, dt[0][i].getSelector(), in);
if(inRec[i].second != asRec[i].second) {
arg = rewriteAs(arg, TypeNode::fromType(asRec[i].second), processing);
}
@@ -156,21 +157,6 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode,
processing.erase( in_t );
return out;
}
- if(in.getType().isTuple()) {
- Assert(as.isTuple());
- Assert(in.getType().getNumChildren() == as.getNumChildren());
- NodeBuilder<> nb(kind::TUPLE);
- for(size_t i = 0; i < as.getNumChildren(); ++i) {
- Node arg = NodeManager::currentNM()->mkNode(NodeManager::currentNM()->mkConst(TupleSelect(i)), in);
- if(in.getType()[i] != as[i]) {
- arg = rewriteAs(arg, as[i], processing);
- }
- nb << arg;
- }
- Node out = nb;
- processing.erase( in_t );
- return out;
- }
if(in.getType().isDatatype()) {
if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) {
processing.erase( in_t );
@@ -387,25 +373,6 @@ TypeNode BooleanTermConverter::convertType(TypeNode type, bool datatypesContext)
} else Debug("boolean-terms") << "OUT is DIFFERENT FROM TYPE" << endl;
return out;
}
- if(type.isRecord()) {
- const Record& rec = type.getConst<Record>();
- const Record::FieldVector& fields = rec.getFields();
- vector< pair<string, Type> > flds;
- for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
- TypeNode converted = convertType(TypeNode::fromType((*i).second), true);
- if(TypeNode::fromType((*i).second) != converted) {
- flds.push_back(make_pair((*i).first, converted.toType()));
- } else {
- flds.push_back(*i);
- }
- }
- TypeNode newRec = NodeManager::currentNM()->mkRecordType(Record(flds));
- Debug("tuprec") << "converted " << type << " to " << newRec << endl;
- if(newRec != type) {
- outNode = newRec;// cache it
- }
- return newRec;
- }
if(!type.isSort() && type.getNumChildren() > 0) {
Debug("boolean-terms") << "here at A for " << type << ":" << type.getId() << endl;
// This should handle tuples and arrays ok.
@@ -460,7 +427,9 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
stack< triple<TNode, theory::TheoryId, bool> > worklist;
worklist.push(triple<TNode, theory::TheoryId, bool>(top, parentTheory, false));
stack< NodeBuilder<> > result;
- result.push(NodeBuilder<>(kind::TUPLE));
+ //AJR: not sure what the significance of "TUPLE" is here, seems to be a placeholder. Since TUPLE is no longer a kind, replacing this with "AND".
+ //result.push(NodeBuilder<>(kind::TUPLE));
+ result.push(NodeBuilder<>(kind::AND));
NodeManager* nm = NodeManager::currentNM();
@@ -670,26 +639,6 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
result.top() << top;
worklist.pop();
goto next_worklist;
- } else if(t.isTuple() || t.isRecord()) {
- TypeNode newType = convertType(t, true);
- if(t != newType) {
- Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
- newType, "a tuple/record variable introduced by Boolean-term conversion",
- NodeManager::SKOLEM_EXACT_NAME);
- top.setAttribute(BooleanTermAttr(), n);
- n.setAttribute(BooleanTermAttr(), top);
- Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl;
- d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
- Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
- d_varCache[top] = n;
- result.top() << n;
- worklist.pop();
- goto next_worklist;
- }
- d_varCache[top] = Node::null();
- result.top() << top;
- worklist.pop();
- goto next_worklist;
} else if(t.isDatatype() || t.isParametricDatatype()) {
Debug("boolean-terms") << "found a var of datatype type" << endl;
TypeNode newT = convertType(t, parentTheory == theory::THEORY_DATATYPES);
@@ -857,17 +806,13 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
Debug("bt") << "looking at: " << top << endl;
// rewrite the operator, as necessary
if(mk == kind::metakind::PARAMETERIZED) {
- if(k == kind::RECORD) {
- result.top() << convertType(top.getType(), parentTheory == theory::THEORY_DATATYPES);
- } else if(k == kind::APPLY_TYPE_ASCRIPTION) {
+ if(k == kind::APPLY_TYPE_ASCRIPTION) {
Node asc = nm->mkConst(AscriptionType(convertType(TypeNode::fromType(top.getOperator().getConst<AscriptionType>().getType()), parentTheory == theory::THEORY_DATATYPES).toType()));
result.top() << asc;
Debug("boolean-terms") << "setting " << top.getOperator() << ":" << top.getOperator().getId() << " to point to " << asc << ":" << asc.getId() << endl;
asc.setAttribute(BooleanTermAttr(), top.getOperator());
} else if(kindToTheoryId(k) != THEORY_BV &&
- k != kind::TUPLE_SELECT &&
k != kind::TUPLE_UPDATE &&
- k != kind::RECORD_SELECT &&
k != kind::RECORD_UPDATE &&
k != kind::DIVISIBLE &&
// Theory parametric functions go here
@@ -899,7 +844,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
} else {
Node n = result.top();
result.pop();
- Debug("boolean-terms") << "constructed: " << n << endl;
+ Debug("boolean-terms") << "constructed: " << n << " of type " << n.getType() << endl;
if(parentTheory == theory::THEORY_BOOL) {
if(n.getType().isBitVector() &&
n.getType().getBitVectorSize() == 1) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback