diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-02 09:46:15 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-04-02 09:46:15 -0500 |
| commit | 9720e341d9cda3de7e7b2b0c25afe190cc2021e4 (patch) | |
| tree | cb44e6cd092956a05ac00d4104d19bd0e1f36eb4 /src/theory/theory_model.cpp | |
| parent | 796703fc72cfd67dc05357b10a5f0311200f2865 (diff) | |
| parent | aa6fb6fa3df0b1519e6763e72541c022396ab1dc (diff) | |
Merge branch 'master' into rmAliasesrmAliases
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); |