diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2016-02-03 14:04:27 -0800 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2016-02-03 14:04:27 -0800 |
commit | 540d556006c5f5cee4acb47d5067e548a15d8a42 (patch) | |
tree | 0604b14a8ac03296b7fe45a9147e39f2b6dc189c /src/theory/theory_model.cpp | |
parent | e21e99b7dfe45f042260db7eb754e25e7108f288 (diff) |
Added --omit-dont-cares option which doesn't print model values for
variables known to be don't-cares.
Diffstat (limited to 'src/theory/theory_model.cpp')
-rw-r--r-- | src/theory/theory_model.cpp | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 18ed6714d..a61df11d8 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -64,11 +64,12 @@ void TheoryModel::reset(){ d_eeContext->push(); } -Node TheoryModel::getValue(TNode n) const { +Node TheoryModel::getValue(TNode n, bool useDontCares) const { //apply substitutions Node nn = d_substitutions.apply(n); //get value in model - nn = getModelValue(nn); + nn = getModelValue(nn, false, useDontCares); + if (nn.isNull()) return nn; if(options::condenseFunctionValues() || nn.getKind() != kind::LAMBDA) { //normalize nn = Rewriter::rewrite(nn); @@ -78,6 +79,10 @@ Node TheoryModel::getValue(TNode n) const { return nn; } +bool TheoryModel::isDontCare(Expr expr) const { + return getValue(Node::fromExpr(expr), true).isNull(); +} + Expr TheoryModel::getValue( Expr expr ) const{ Node n = Node::fromExpr( expr ); Node ret = getValue( n ); @@ -102,7 +107,7 @@ Cardinality TheoryModel::getCardinality( Type t ) const{ } } -Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const +Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) const { std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_modelCache.find(n); if (it != d_modelCache.end()) { @@ -210,6 +215,9 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const if(n.getType().isRegExp()) { ret = Rewriter::rewrite(ret); } else { + if (options::omitDontCares() && useDontCares) { + return Node(); + } // Unknown term - return first enumerated value for this type TypeEnumerator te(n.getType()); ret = *te; |