model blocker with get values

5 files changed, 50 insertions, 14 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index b1936d8cc..6b5c14f3f 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1671,7 +1671,7 @@ void GetValueCommand::invoke(SmtEngine* smtEngine)
       smt::SmtScope scope(smtEngine);
       Node request = Node::fromExpr(
           options::expandDefinitions() ? smtEngine->expandDefinitions(e) : e);
-      Node value = Node::fromExpr(smtEngine->getValue(e));
+      Node value = Node::fromExpr(smtEngine->getValue(e, true));
       if (value.getType().isInteger() && request.getType() == nm->realType())
       {
         // Need to wrap in division-by-one so that output printers know this
diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp
index 33831b918..0e7c76f89 100644
--- a/src/smt/model_blocker.cpp
+++ b/src/smt/model_blocker.cpp
@@ -24,7 +24,8 @@ namespace CVC4 {
 
 Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
                                    theory::TheoryModel* m,
-                                   BlockModelsMode mode)
+                                   BlockModelsMode mode,
+                                   std::vector<Node> getValueNodes)
 {
   NodeManager* nm = NodeManager::currentNM();
   // convert to nodes
@@ -37,6 +38,7 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
   Trace("model-blocker") << "Compute model blocker, assertions:" << std::endl;
   Node blocker;
   if (mode == BLOCK_MODELS_LITERALS) {
+    Assert(getValueNodes.size() == 0);
     // optimization: filter to only top-level disjunctions
     unsigned counter = 0;
     std::vector<Node> asserts;
@@ -227,15 +229,28 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
     blocker = visited[formula].negate();
   } else {
     Assert(mode == BLOCK_MODELS_VALUES);
-    std::unordered_set<Node, NodeHashFunction> symbols;
-    for (Node n: tlAsserts) {
-      expr::getSymbols(n, symbols);
-    }
     std::vector<Node> blockers;
-    for (Node s : symbols) {
-      if (s.getType().getKind() != kind::FUNCTION_TYPE) {
-        Node v = m->getValue(s);
-        Node a = nm->mkNode(DISTINCT, s, v);
+    //if specific terms were not specified in get-value, block all variables of the model
+    if (getValueNodes.size() == 0) {
+      Trace("model-blocker") << "no get-value recognized" << std::endl;
+      std::unordered_set<Node, NodeHashFunction> symbols;
+      for (Node n: tlAsserts) {
+        expr::getSymbols(n, symbols);
+      }
+      for (Node s : symbols) {
+        if (s.getType().getKind() != kind::FUNCTION_TYPE) {
+          Node v = m->getValue(s);
+          Node a = nm->mkNode(DISTINCT, s, v);
+          blockers.push_back(a);
+        }
+      }
+    } 
+    //otherwise, block all terms that were specified in get-value
+    else {
+      std::unordered_set<Node, NodeHashFunction> terms;
+      for (Node n : getValueNodes) {
+        Node v = m->getValue(n);
+        Node a = nm->mkNode(DISTINCT, n, v);
         blockers.push_back(a);
       }
     }
diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h
index 9c760aaa5..a037e9446 100644
--- a/src/smt/model_blocker.h
+++ b/src/smt/model_blocker.h
@@ -22,6 +22,7 @@
 #include "expr/expr.h"
 #include "options/smt_options.h"
 #include "theory/theory_model.h"
+#include "context/cdlist_forward.h"
 
 namespace CVC4 {
 
@@ -30,6 +31,9 @@ namespace CVC4 {
  */
 class ModelBlocker
 {
+ 
+ typedef context::CDList<Node> NodeList;
+
  public:
   /** get model blocker
    *
@@ -49,7 +53,7 @@ class ModelBlocker
    * our input. In other words, we do not return ~(x < 0) V ~(w < 0) since the
    * left disjunct is always false.
    */
-  static Expr getModelBlocker(const std::vector<Expr>& assertions, theory::TheoryModel* m, BlockModelsMode mode);
+  static Expr getModelBlocker(const std::vector<Expr>& assertions, theory::TheoryModel* m, BlockModelsMode mode, std::vector<Node> getValueNodes);
 }; /* class TheoryModelCoreBuilder */
 
 }  // namespace CVC4
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index efd31a9e5..9acfa09e5 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -876,6 +876,7 @@ SmtEngine::SmtEngine(ExprManager* em)
       d_assignments(NULL),
       d_modelGlobalCommands(),
       d_modelCommands(NULL),
+      d_getValueNodes(),
       d_dumpCommands(),
       d_defineCommands(),
       d_logic(),
@@ -1074,6 +1075,7 @@ SmtEngine::~SmtEngine()
       delete d_dumpCommands[i];
       d_dumpCommands[i] = NULL;
     }
+    d_getValueNodes.clear();
     d_dumpCommands.clear();
 
     DeleteAndClearCommandVector(d_modelGlobalCommands);
@@ -4131,7 +4133,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex)
 }
 
 // TODO(#1108): Simplify the error reporting of this method.
-Expr SmtEngine::getValue(const Expr& ex) const
+Expr SmtEngine::getValue(const Expr& ex, bool isCommand) const
 {
   Assert(ex.getExprManager() == d_exprManager);
   SmtScope smts(this);
@@ -4205,6 +4207,10 @@ Expr SmtEngine::getValue(const Expr& ex) const
     Trace("smt") << "--- abstract value >> " << resultNode << endl;
   }
 
+  if (options::blockModelsMode() != BLOCK_MODELS_NONE && isCommand)
+  {
+      d_getValueNodes.push_back(n);
+  }
   return resultNode.toExpr();
 }
 
@@ -4393,8 +4399,9 @@ Model* SmtEngine::getModel() {
     }
     if (options::blockModelsMode() != BLOCK_MODELS_NONE)
     {
-      Expr eblocker = ModelBlocker::getModelBlocker(eassertsProc, m, options::blockModelsMode());
+      Expr eblocker = ModelBlocker::getModelBlocker(eassertsProc, m, options::blockModelsMode(), d_getValueNodes);
       assertFormula(eblocker);
+      d_getValueNodes.clear();
     }
   }
   m->d_inputName = d_filename;
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 165e93997..7eb5656e7 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -185,6 +185,15 @@ class CVC4_PUBLIC SmtEngine {
    */
   smt::CommandList* d_modelCommands;
 
+
+  /**
+   * If there is a (get-value (t1 t2 ... tn)) command in the current
+   * context, then this vector includes t1,...,tn.
+   * This field is changed in getValue function, which is const, 
+   * therefore it is declared mutable.
+   */
+  mutable std::vector<Node> d_getValueNodes;
+
   /**
    * A vector of declaration commands waiting to be dumped out.
    * Once the SmtEngine is fully initialized, we'll dump them.
@@ -736,8 +745,9 @@ class CVC4_PUBLIC SmtEngine {
    * Get the assigned value of an expr (only if immediately preceded
    * by a SAT or INVALID query).  Only permitted if the SmtEngine is
    * set to operate interactively and produce-models is on.
+   * if isCommand == true then this call came from a get-value command
    */
-  Expr getValue(const Expr& e) const
+  Expr getValue(const Expr& e, bool isCommand = false) const
       /* throw(ModalException, TypeCheckingException, LogicException, UnsafeInterruptException) */
       ;