Added --omit-dont-cares option which doesn't print model values for

variables known to be don't-cares.

diff --git a/src/options/smt_options b/src/options/smt_options
index bc2586fe07e1d64bece100347829be12f8b3333f..74711934490699941e466a1073398ac49150a533 100644 (file)
--- 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 d4b99536e0423bd39c9ec9d95d1b344a64862f9f..a2734160fdeb2741535868a216e2dd4116d1bd7c 100644 (file)
--- 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 33a9312a62281104d2c20a2b5c89d6629f30f359..4bbcb5f7dd41f711d7357a2b15b5e0980ef3da58 100644 (file)
--- 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 18ed6714da5f47716c1ad80c0b9c710b5eab6234..a61df11d8161ef7775b42144578fbf1d7883ed1c 100644 (file)
--- 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 0c2f109bbdcd2ee9fa89fdaff3011efe50c31561..4b27aeacb9a8eb9c4bdc1da729e7b6e6fef0ce87 100644 (file)
--- 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 */