diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-28 21:26:43 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-28 21:26:43 +0000 |
commit | 436a0aac57b3217ad7f0e463cf4cf29b807581e4 (patch) | |
tree | 7d07daa5f3220dd029a5031e1749a5296da905b5 | |
parent | cce79b9667a4fd067e75d19926b22f0689756daa (diff) |
Fix for getValue. Now it can handle lambda applications
-rw-r--r-- | src/theory/model.cpp | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 9a420ed02..b117aa1af 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -75,7 +75,8 @@ Cardinality TheoryModel::getCardinality( Type t ) const{ } } -Node TheoryModel::getModelValue( TNode n ) const{ +Node TheoryModel::getModelValue(TNode n) const +{ Assert(n.getKind() != kind::FORALL && n.getKind() != kind::EXISTS); if(n.isConst()) { return n; @@ -111,6 +112,10 @@ Node TheoryModel::getModelValue( TNode n ) const{ std::vector<Node> children; if (n.getKind() == APPLY_UF) { Node op = n.getOperator(); + if (op.getKind() == kind::LAMBDA) { + Node rw = Rewriter::rewrite(n); + return getModelValue(rw); + } std::map< Node, Node >::const_iterator it = d_uf_models.find(op); if (it == d_uf_models.end()) { // Unknown term - return first enumerated value for this type @@ -126,7 +131,7 @@ Node TheoryModel::getModelValue( TNode n ) const{ } //evaluate the children for (unsigned i = 0; i < n.getNumChildren(); ++i) { - Node val = getValue(n[i]); + Node val = getModelValue(n[i]); children.push_back(val); } Node val = Rewriter::rewrite(NodeManager::currentNM()->mkNode(n.getKind(), children)); |