diff options
author | mudathirmahgoub <mudathir-mahgoubyahia@uiowa.edu> | 2020-03-30 09:04:52 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-30 09:04:52 -0500 |
commit | 0060de329173c0b75c02778d003371f59cc11eff (patch) | |
tree | 92bec1579d0301a4c91e45c349c381a9bd2f1b17 /src/theory/theory_model.cpp | |
parent | 01b257084a0a8ee70bff32e011704330d1544c01 (diff) |
Frontend support for the choice operator (#4175)
Added the operator choice to Smt2.g and Cvc.g.
Removed the unused parameter hasBoundVars from TheoryModel::getModelValue
Diffstat (limited to 'src/theory/theory_model.cpp')
-rw-r--r-- | src/theory/theory_model.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 7bfb0e8f3..dae7261e5 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -147,7 +147,7 @@ Node TheoryModel::getValue(TNode n) const Node nn = d_substitutions.apply(n); Debug("model-getvalue-debug") << "[model-getvalue] getValue : substitute " << n << " to " << nn << std::endl; //get value in model - nn = getModelValue(nn, false); + nn = getModelValue(nn); if (nn.isNull()) return nn; if(options::condenseFunctionValues() || nn.getKind() != kind::LAMBDA) { //normalize @@ -193,7 +193,7 @@ Cardinality TheoryModel::getCardinality( Type t ) const{ } } -Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const +Node TheoryModel::getModelValue(TNode n) const { std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_modelCache.find(n); if (it != d_modelCache.end()) { @@ -220,7 +220,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const std::vector<Node> children; if (n.getKind() == APPLY_UF) { - Node op = getModelValue(n.getOperator(), hasBoundVars); + Node op = getModelValue(n.getOperator()); Debug("model-getvalue-debug") << " operator : " << op << std::endl; children.push_back(op); } @@ -231,7 +231,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const // evaluate the children for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; ++i) { - ret = getModelValue(n[i], hasBoundVars); + ret = getModelValue(n[i]); Debug("model-getvalue-debug") << " " << n << "[" << i << "] is " << ret << std::endl; children.push_back(ret); |