From 540d556006c5f5cee4acb47d5067e548a15d8a42 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Wed, 3 Feb 2016 14:04:27 -0800
Subject: [PATCH] Added --omit-dont-cares option which doesn't print model
 values for variables known to be don't-cares.

---
 src/options/smt_options     |  2 ++
 src/printer/printer.cpp     |  7 ++++++-
 src/smt/model.h             |  2 ++
 src/theory/theory_model.cpp | 14 +++++++++++---
 src/theory/theory_model.h   |  6 ++++--
 5 files changed, 25 insertions(+), 6 deletions(-)

diff --git a/src/options/smt_options b/src/options/smt_options
index bc2586fe0..747119344 100644
--- a/src/options/smt_options
+++ b/src/options/smt_options
@@ -29,6 +29,8 @@ option checkModels check-models --check-models bool :link --produce-models --pro
  after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
 option dumpModels --dump-models bool :default false :link --produce-models :link-smt produce-models
  output models after every SAT/INVALID/UNKNOWN response
+option omitDontCares --omit-dont-cares bool :default false
+ When producing a model, omit variables whose value does not matter
 option proof produce-proofs --proof bool :default false :predicate proofEnabledBuild :notify notifyBeforeSearch
  turn on proof generation
 option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :notify notifyBeforeSearch :read-write
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index d4b99536e..a2734160f 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -71,7 +71,12 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() {
 
 void Printer::toStream(std::ostream& out, const Model& m) const throw() {
   for(size_t i = 0; i < m.getNumCommands(); ++i) {
-    toStream(out, m, m.getCommand(i));
+    const Command* cmd = m.getCommand(i);
+    const DeclareFunctionCommand* dfc = dynamic_cast<const DeclareFunctionCommand*>(cmd);
+    if (dfc != NULL && m.isDontCare(dfc->getFunction())) {
+      continue;
+    }
+    toStream(out, m, cmd);
   }
 }/* Printer::toStream(Model) */
 
diff --git a/src/smt/model.h b/src/smt/model.h
index 33a9312a6..4bbcb5f7d 100644
--- a/src/smt/model.h
+++ b/src/smt/model.h
@@ -60,6 +60,8 @@ public:
   std::string getInputName() const { return d_inputName; }
 
 public:
+  /** Check whether this expr is a don't-care in the model */
+  virtual bool isDontCare(Expr expr) const { return false; }
   /** get value for expression */
   virtual Expr getValue(Expr expr) const = 0;
   /** get cardinality for sort */
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;
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 0c2f109bb..4b27aeacb 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -60,13 +60,13 @@ protected:
   /**
    * Get model value function.  This function is called by getValue
    */
-  Node getModelValue(TNode n, bool hasBoundVars = false) const;
+  Node getModelValue(TNode n, bool hasBoundVars = false, bool useDontCares = false) const;
 public:
   /**
    * Get value function.  This should be called only after a ModelBuilder has called buildModel(...)
    * on this model.
    */
-  Node getValue( TNode n ) const;
+  Node getValue( TNode n, bool useDontCares = false ) const;
 
   /** get existing domain value, with possible exclusions
     *   This function returns a term in d_rep_set.d_type_reps[tn] but not in exclude
@@ -101,6 +101,8 @@ public:
   bool areEqual(TNode a, TNode b);
   bool areDisequal(TNode a, TNode b);
 public:
+  /** return whether this node is a don't-care */
+  bool isDontCare(Expr expr) const;
   /** get value function for Exprs. */
   Expr getValue( Expr expr ) const;
   /** get cardinality for sort */
-- 
2.30.2