Model blocker feature (#3112)

6 files changed, 660 insertions, 41 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 044062f77..8baaeb1e9 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1662,16 +1662,18 @@ void GetValueCommand::invoke(SmtEngine* smtEngine)
 {
   try
   {
-    vector<Expr> result;
     ExprManager* em = smtEngine->getExprManager();
     NodeManager* nm = NodeManager::fromExprManager(em);
-    for (const Expr& e : d_terms)
+    smt::SmtScope scope(smtEngine);
+    vector<Expr> result = smtEngine->getValues(d_terms);
+    Assert(result.size() == d_terms.size());
+    for (int i = 0, size = d_terms.size(); i < size; i++)
     {
+      Expr e = d_terms[i];
       Assert(nm == NodeManager::fromExprManager(e.getExprManager()));
-      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(result[i]);
       if (value.getType().isInteger() && request.getType() == nm->realType())
       {
         // Need to wrap in division-by-one so that output printers know this
@@ -1679,7 +1681,7 @@ void GetValueCommand::invoke(SmtEngine* smtEngine)
         // a rational.  Necessary for SMT-LIB standards compliance.
         value = nm->mkNode(kind::DIVISION, value, nm->mkConst(Rational(1)));
       }
-      result.push_back(nm->mkNode(kind::SEXPR, request, value).toExpr());
+      result[i] = nm->mkNode(kind::SEXPR, request, value).toExpr();
     }
     d_result = em->mkExpr(kind::SEXPR, result);
     d_commandStatus = CommandSuccess::instance();
@@ -1870,6 +1872,109 @@ Command* GetModelCommand::clone() const
 std::string GetModelCommand::getCommandName() const { return "get-model"; }
 
 /* -------------------------------------------------------------------------- */
+/* class BlockModelCommand */
+/* -------------------------------------------------------------------------- */
+
+BlockModelCommand::BlockModelCommand() {}
+void BlockModelCommand::invoke(SmtEngine* smtEngine)
+{
+  try
+  {
+    smtEngine->blockModel();
+    d_commandStatus = CommandSuccess::instance();
+  }
+  catch (RecoverableModalException& e)
+  {
+    d_commandStatus = new CommandRecoverableFailure(e.what());
+  }
+  catch (UnsafeInterruptException& e)
+  {
+    d_commandStatus = new CommandInterrupted();
+  }
+  catch (exception& e)
+  {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+Command* BlockModelCommand::exportTo(ExprManager* exprManager,
+                                     ExprManagerMapCollection& variableMap)
+{
+  BlockModelCommand* c = new BlockModelCommand();
+  return c;
+}
+
+Command* BlockModelCommand::clone() const
+{
+  BlockModelCommand* c = new BlockModelCommand();
+  return c;
+}
+
+std::string BlockModelCommand::getCommandName() const { return "block-model"; }
+
+/* -------------------------------------------------------------------------- */
+/* class BlockModelValuesCommand */
+/* -------------------------------------------------------------------------- */
+
+BlockModelValuesCommand::BlockModelValuesCommand(const std::vector<Expr>& terms)
+    : d_terms(terms)
+{
+  PrettyCheckArgument(terms.size() >= 1,
+                      terms,
+                      "cannot block-model-values of an empty set of terms");
+}
+
+const std::vector<Expr>& BlockModelValuesCommand::getTerms() const
+{
+  return d_terms;
+}
+void BlockModelValuesCommand::invoke(SmtEngine* smtEngine)
+{
+  try
+  {
+    smtEngine->blockModelValues(d_terms);
+    d_commandStatus = CommandSuccess::instance();
+  }
+  catch (RecoverableModalException& e)
+  {
+    d_commandStatus = new CommandRecoverableFailure(e.what());
+  }
+  catch (UnsafeInterruptException& e)
+  {
+    d_commandStatus = new CommandInterrupted();
+  }
+  catch (exception& e)
+  {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+Command* BlockModelValuesCommand::exportTo(
+    ExprManager* exprManager, ExprManagerMapCollection& variableMap)
+{
+  vector<Expr> exportedTerms;
+  for (std::vector<Expr>::const_iterator i = d_terms.begin();
+       i != d_terms.end();
+       ++i)
+  {
+    exportedTerms.push_back((*i).exportTo(exprManager, variableMap));
+  }
+  BlockModelValuesCommand* c = new BlockModelValuesCommand(exportedTerms);
+  return c;
+}
+
+Command* BlockModelValuesCommand::clone() const
+{
+  BlockModelValuesCommand* c = new BlockModelValuesCommand(d_terms);
+  return c;
+}
+
+std::string BlockModelValuesCommand::getCommandName() const
+{
+  return "block-model-values";
+}
+
+/* -------------------------------------------------------------------------- */
 /* class GetProofCommand                                                      */
 /* -------------------------------------------------------------------------- */
 
diff --git a/src/smt/command.h b/src/smt/command.h
index eb3199944..d82399135 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -958,6 +958,37 @@ class CVC4_PUBLIC GetModelCommand : public Command
   SmtEngine* d_smtEngine;
 }; /* class GetModelCommand */
 
+/** The command to block models. */
+class CVC4_PUBLIC BlockModelCommand : public Command
+{
+ public:
+  BlockModelCommand();
+
+  void invoke(SmtEngine* smtEngine) override;
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap) override;
+  Command* clone() const override;
+  std::string getCommandName() const override;
+}; /* class BlockModelCommand */
+
+/** The command to block model values. */
+class CVC4_PUBLIC BlockModelValuesCommand : public Command
+{
+ public:
+  BlockModelValuesCommand(const std::vector<Expr>& terms);
+
+  const std::vector<Expr>& getTerms() const;
+  void invoke(SmtEngine* smtEngine) override;
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap) override;
+  Command* clone() const override;
+  std::string getCommandName() const override;
+
+ protected:
+  /** The terms we are blocking */
+  std::vector<Expr> d_terms;
+}; /* class BlockModelValuesCommand */
+
 class CVC4_PUBLIC GetProofCommand : public Command
 {
  public:
diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp
new file mode 100644
index 000000000..cb962ee45
--- /dev/null
+++ b/src/smt/model_blocker.cpp
@@ -0,0 +1,288 @@
+/*********************                                                        */
+/*! \file model_blocker.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of utility for blocking models.
+ **
+ **/
+
+#include "smt/model_blocker.h"
+
+#include "expr/node.h"
+#include "expr/node_algorithm.h"
+#include "theory/quantifiers/term_util.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+
+Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
+                                   theory::TheoryModel* m,
+                                   BlockModelsMode mode,
+                                   const std::vector<Expr>& exprToBlock)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  // convert to nodes
+  std::vector<Node> tlAsserts;
+  for (const Expr& a : assertions)
+  {
+    Node an = Node::fromExpr(a);
+    tlAsserts.push_back(an);
+  }
+  std::vector<Node> nodesToBlock;
+  for (const Expr& eb : exprToBlock)
+  {
+    nodesToBlock.push_back(Node::fromExpr(eb));
+  }
+  Trace("model-blocker") << "Compute model blocker, assertions:" << std::endl;
+  Node blocker;
+  if (mode == BLOCK_MODELS_LITERALS)
+  {
+    Assert(nodesToBlock.empty());
+    // optimization: filter out top-level unit assertions, as they cannot
+    // contribute to model blocking.
+    unsigned counter = 0;
+    std::vector<Node> asserts;
+    while (counter < tlAsserts.size())
+    {
+      Node cur = tlAsserts[counter];
+      counter++;
+      Node catom = cur.getKind() == NOT ? cur[0] : cur;
+      bool cpol = cur.getKind() != NOT;
+      if (catom.getKind() == NOT)
+      {
+        tlAsserts.push_back(catom[0]);
+      }
+      else if (catom.getKind() == AND && cpol)
+      {
+        tlAsserts.insert(tlAsserts.end(), catom.begin(), catom.end());
+      }
+      else if (theory::quantifiers::TermUtil::isBoolConnectiveTerm(catom))
+      {
+        asserts.push_back(cur);
+        Trace("model-blocker") << "  " << cur << std::endl;
+      }
+    }
+    if (asserts.empty())
+    {
+      Node blockTriv = nm->mkConst(false);
+      Trace("model-blocker")
+          << "...model blocker is (trivially) " << blockTriv << std::endl;
+      return blockTriv.toExpr();
+    }
+
+    Node formula = asserts.size() > 1 ? nm->mkNode(AND, asserts) : asserts[0];
+    std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+    std::unordered_map<TNode, Node, TNodeHashFunction> implicant;
+    std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+    std::vector<TNode> visit;
+    TNode cur;
+    visit.push_back(formula);
+    do
+    {
+      cur = visit.back();
+      visit.pop_back();
+      it = visited.find(cur);
+
+      Trace("model-blocker-debug") << "Visit : " << cur << std::endl;
+
+      if (it == visited.end())
+      {
+        visited[cur] = Node::null();
+        Node catom = cur.getKind() == NOT ? cur[0] : cur;
+        bool cpol = cur.getKind() != NOT;
+        // compute the implicant
+        // impl is a formula that implies cur that is also satisfied by m
+        Node impl;
+        if (catom.getKind() == NOT)
+        {
+          // double negation
+          impl = catom[0];
+        }
+        else if (catom.getKind() == OR || catom.getKind() == AND)
+        {
+          // if disjunctive
+          if ((catom.getKind() == OR) == cpol)
+          {
+            // take the first literal that is satisfied
+            for (Node n : catom)
+            {
+              // rewrite, this ensures that e.g. the propositional value of
+              // quantified formulas can be queried
+              n = theory::Rewriter::rewrite(n);
+              Node vn = Node::fromExpr(m->getValue(n.toExpr()));
+              Assert(vn.isConst());
+              if (vn.getConst<bool>() == cpol)
+              {
+                impl = cpol ? n : n.negate();
+                break;
+              }
+            }
+          }
+          else if (catom.getKind() == OR)
+          {
+            // one step NNF
+            std::vector<Node> children;
+            for (const Node& cn : catom)
+            {
+              children.push_back(cn.negate());
+            }
+            impl = nm->mkNode(AND, children);
+          }
+        }
+        else if (catom.getKind() == ITE)
+        {
+          Node vcond = Node::fromExpr(m->getValue(cur[0].toExpr()));
+          Assert(vcond.isConst());
+          Node cond = cur[0];
+          Node branch;
+          if (vcond.getConst<bool>())
+          {
+            branch = cur[1];
+          }
+          else
+          {
+            cond = cond.negate();
+            branch = cur[2];
+          }
+          impl = nm->mkNode(AND, cond, cpol ? branch : branch.negate());
+        }
+        else if ((catom.getKind() == EQUAL && catom[0].getType().isBoolean())
+                 || catom.getKind() == XOR)
+        {
+          // based on how the children evaluate in the model
+          std::vector<Node> children;
+          for (const Node& cn : catom)
+          {
+            Node vn = Node::fromExpr(m->getValue(cn.toExpr()));
+            Assert(vn.isConst());
+            children.push_back(vn.getConst<bool>() ? cn : cn.negate());
+          }
+          impl = nm->mkNode(AND, children);
+        }
+        else
+        {
+          // literals justified by themselves
+          visited[cur] = cur;
+          Trace("model-blocker-debug") << "...self justified" << std::endl;
+        }
+        if (visited[cur].isNull())
+        {
+          visit.push_back(cur);
+          if (impl.isNull())
+          {
+            Assert(cur.getKind() == AND);
+            Trace("model-blocker-debug") << "...recurse" << std::endl;
+            visit.insert(visit.end(), cur.begin(), cur.end());
+          }
+          else
+          {
+            Trace("model-blocker-debug")
+                << "...implicant : " << impl << std::endl;
+            implicant[cur] = impl;
+            visit.push_back(impl);
+          }
+        }
+      }
+      else if (it->second.isNull())
+      {
+        Node ret = cur;
+        it = implicant.find(cur);
+        if (it != implicant.end())
+        {
+          Node impl = it->second;
+          it = visited.find(impl);
+          Assert(it != visited.end());
+          Assert(!it->second.isNull());
+          ret = it->second;
+          Trace("model-blocker-debug")
+              << "...implicant res: " << ret << std::endl;
+        }
+        else
+        {
+          bool childChanged = false;
+          std::vector<Node> children;
+          // we never recurse to parameterized nodes
+          Assert(cur.getMetaKind() != metakind::PARAMETERIZED);
+          for (const Node& cn : cur)
+          {
+            it = visited.find(cn);
+            Assert(it != visited.end());
+            Assert(!it->second.isNull());
+            childChanged = childChanged || cn != it->second;
+            children.push_back(it->second);
+          }
+          if (childChanged)
+          {
+            ret = nm->mkNode(cur.getKind(), children);
+          }
+          Trace("model-blocker-debug") << "...recons res: " << ret << std::endl;
+        }
+        visited[cur] = ret;
+      }
+    } while (!visit.empty());
+    Assert(visited.find(formula) != visited.end());
+    Assert(!visited.find(formula)->second.isNull());
+    blocker = visited[formula].negate();
+  }
+  else
+  {
+    Assert(mode == BLOCK_MODELS_VALUES);
+    std::vector<Node> blockers;
+    // if specific terms were not specified, block all variables of
+    // the model
+    if (nodesToBlock.empty())
+    {
+      Trace("model-blocker")
+          << "no specific terms to block 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 : nodesToBlock)
+      {
+        Node v = m->getValue(n);
+        Node a = nm->mkNode(DISTINCT, n, v);
+        blockers.push_back(a);
+      }
+    }
+    if (blockers.size() == 0)
+    {
+      blocker = nm->mkConst<bool>(true);
+    }
+    else if (blockers.size() == 1)
+    {
+      blocker = blockers[0];
+    }
+    else
+    {
+      blocker = nm->mkNode(OR, blockers);
+    }
+  }
+  Trace("model-blocker") << "...model blocker is " << blocker << std::endl;
+  return blocker.toExpr();
+}
+
+} /* namespace CVC4 */
diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h
new file mode 100644
index 000000000..ca201ec66
--- /dev/null
+++ b/src/smt/model_blocker.h
@@ -0,0 +1,70 @@
+/*********************                                                        */
+/*! \file model_blocker.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Utility for blocking the current model
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__MODEL_BLOCKER_H
+#define __CVC4__THEORY__MODEL_BLOCKER_H
+
+#include <vector>
+
+#include "expr/expr.h"
+#include "options/smt_options.h"
+#include "theory/theory_model.h"
+
+namespace CVC4 {
+
+/**
+ * A utility for blocking the current model.
+ */
+class ModelBlocker
+{
+ public:
+  /** get model blocker
+   *
+   * This returns a disjunction of literals ~L1 V ... V ~Ln with the following
+   * properties:
+   * (1) L1 ... Ln hold in the current model (given by argument m),
+   * (2) if mode is set to "literals", L1 ... Ln are literals that occur in
+   * assertions and propositionally entail all non-unit top-level assertions.
+   * (3) if mode is set to "values", L1 ... Ln are literals of the form x=c,
+   * where c is the value of x in the current model.
+   * (4) if exprToBlock is not empty, L1 ... Ln are literals of the form t=c,
+   * where c is the value of t in the current model. If exprToBlock is
+   * non-empty, then L1 ... Ln are t1=c1 ... tn=cn where exprToBlock is
+   * { t1 ... tn }; if exprToBlock is empty, then t1 ... tn are the free
+   * variables of assertions.
+   *
+   * We expect exprToBlock to be non-empty only if mode is BLOCK_MODELS_VALUES.
+   *
+   * For example, if our input is:
+   *    x > 0 ^ ( y < 0 V z < 0 V w < 0 )
+   * and m is { x -> 1, y -> 2, z -> -1, w -> -1 }, then this method may
+   * return ~(z < 0) or ~(w < 0) when set to mode "literals".
+   *
+   * Notice that we do not require that L1...Ln entail unit top-level assertions
+   * since these literals are trivially entailed to be true in all models of
+   * 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,
+      const std::vector<Expr>& exprToBlock = std::vector<Expr>());
+}; /* class TheoryModelCoreBuilder */
+
+}  // namespace CVC4
+
+#endif /* __CVC4__THEORY__MODEL_BLOCKER_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5db3fc43d..560cb0599 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -85,6 +85,7 @@
 #include "smt/command_list.h"
 #include "smt/logic_request.h"
 #include "smt/managed_ostreams.h"
+#include "smt/model_blocker.h"
 #include "smt/model_core_builder.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/term_formula_removal.h"
@@ -1278,11 +1279,12 @@ void SmtEngine::setDefaults() {
 
   if ((options::checkModels() || options::checkSynthSol()
        || options::produceAbducts()
-       || options::modelCoresMode() != MODEL_CORES_NONE)
+       || options::modelCoresMode() != MODEL_CORES_NONE
+       || options::blockModelsMode() != BLOCK_MODELS_NONE)
       && !options::produceAssertions())
   {
     Notice() << "SmtEngine: turning on produce-assertions to support "
-             << "check-models, check-synth-sol or produce-model-cores." << endl;
+             << "option requiring assertions." << endl;
     setOption("produce-assertions", SExpr("true"));
   }
 
@@ -3055,6 +3057,34 @@ Result SmtEngine::quickCheck() {
   return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK, d_filename);
 }
 
+theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const
+{
+  if (!options::assignFunctionValues())
+  {
+    std::stringstream ss;
+    ss << "Cannot " << c << " when --assign-function-values is false.";
+    throw RecoverableModalException(ss.str().c_str());
+  }
+
+  if (d_status.isNull() || d_status.asSatisfiabilityResult() == Result::UNSAT
+      || d_problemExtended)
+  {
+    std::stringstream ss;
+    ss << "Cannot " << c
+       << " unless immediately preceded by SAT/INVALID or UNKNOWN response.";
+    throw RecoverableModalException(ss.str().c_str());
+  }
+  if (!options::produceModels())
+  {
+    std::stringstream ss;
+    ss << "Cannot " << c << " when produce-models options is off.";
+    throw ModalException(ss.str().c_str());
+  }
+
+  TheoryModel* m = d_theoryEngine->getBuiltModel();
+
+  return m;
+}
 
 void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, unordered_map<Node, bool, NodeHashFunction>& cache)
 {
@@ -4200,6 +4230,16 @@ Expr SmtEngine::getValue(const Expr& ex) const
   return resultNode.toExpr();
 }
 
+vector<Expr> SmtEngine::getValues(const vector<Expr>& exprs)
+{
+  vector<Expr> result;
+  for (const Expr& e : exprs)
+  {
+    result.push_back(getValue(e));
+  }
+  return result;
+}
+
 bool SmtEngine::addToAssignment(const Expr& ex) {
   SmtScope smts(this);
   finalOptionsAreSet();
@@ -4337,27 +4377,7 @@ Model* SmtEngine::getModel() {
     Dump("benchmark") << GetModelCommand();
   }
 
-  if (!options::assignFunctionValues())
-  {
-    const char* msg =
-        "Cannot get the model when --assign-function-values is false.";
-    throw RecoverableModalException(msg);
-  }
-
-  if(d_status.isNull() ||
-     d_status.asSatisfiabilityResult() == Result::UNSAT ||
-     d_problemExtended) {
-    const char* msg =
-      "Cannot get the current model unless immediately "
-      "preceded by SAT/INVALID or UNKNOWN response.";
-    throw RecoverableModalException(msg);
-  }
-  if(!options::produceModels()) {
-    const char* msg =
-      "Cannot get model when produce-models options is off.";
-    throw ModalException(msg);
-  }
-  TheoryModel* m = d_theoryEngine->getBuiltModel();
+  TheoryModel* m = getAvailableModel("get model");
 
   // Since model m is being returned to the user, we must ensure that this
   // model object remains valid with future check-sat calls. Hence, we set
@@ -4367,23 +4387,67 @@ Model* SmtEngine::getModel() {
   if (options::modelCoresMode() != MODEL_CORES_NONE)
   {
     // If we enabled model cores, we compute a model core for m based on our
-    // assertions using the model core builder utility
-    std::vector<Expr> easserts = getAssertions();
-    // must expand definitions
-    std::vector<Expr> eassertsProc;
-    std::unordered_map<Node, Node, NodeHashFunction> cache;
-    for (unsigned i = 0, nasserts = easserts.size(); i < nasserts; i++)
-    {
-      Node ea = Node::fromExpr(easserts[i]);
-      Node eae = d_private->expandDefinitions(ea, cache);
-      eassertsProc.push_back(eae.toExpr());
-    }
+    // (expanded) assertions using the model core builder utility
+    std::vector<Expr> eassertsProc = getExpandedAssertions();
     ModelCoreBuilder::setModelCore(eassertsProc, m, options::modelCoresMode());
   }
   m->d_inputName = d_filename;
   return m;
 }
 
+Result SmtEngine::blockModel()
+{
+  Trace("smt") << "SMT blockModel()" << endl;
+  SmtScope smts(this);
+
+  finalOptionsAreSet();
+
+  if (Dump.isOn("benchmark"))
+  {
+    Dump("benchmark") << BlockModelCommand();
+  }
+
+  TheoryModel* m = getAvailableModel("block model");
+
+  if (options::blockModelsMode() == BLOCK_MODELS_NONE)
+  {
+    std::stringstream ss;
+    ss << "Cannot block model when block-models is set to none.";
+    throw ModalException(ss.str().c_str());
+  }
+
+  // get expanded assertions
+  std::vector<Expr> eassertsProc = getExpandedAssertions();
+  Expr eblocker = ModelBlocker::getModelBlocker(
+      eassertsProc, m, options::blockModelsMode());
+  return assertFormula(eblocker);
+}
+
+Result SmtEngine::blockModelValues(const std::vector<Expr>& exprs)
+{
+  Trace("smt") << "SMT blockModelValues()" << endl;
+  SmtScope smts(this);
+
+  finalOptionsAreSet();
+
+  PrettyCheckArgument(
+      !exprs.empty(),
+      "block model values must be called on non-empty set of terms");
+  if (Dump.isOn("benchmark"))
+  {
+    Dump("benchmark") << BlockModelValuesCommand(exprs);
+  }
+
+  TheoryModel* m = getAvailableModel("block model values");
+
+  // get expanded assertions
+  std::vector<Expr> eassertsProc = getExpandedAssertions();
+  // we always do block model values mode here
+  Expr eblocker = ModelBlocker::getModelBlocker(
+      eassertsProc, m, BLOCK_MODELS_VALUES, exprs);
+  return assertFormula(eblocker);
+}
+
 std::pair<Expr, Expr> SmtEngine::getSepHeapAndNilExpr(void)
 {
   if (!d_logic.isTheoryEnabled(THEORY_SEP))
@@ -4406,6 +4470,21 @@ std::pair<Expr, Expr> SmtEngine::getSepHeapAndNilExpr(void)
       "expressions from theory model.");
 }
 
+std::vector<Expr> SmtEngine::getExpandedAssertions()
+{
+  std::vector<Expr> easserts = getAssertions();
+  // must expand definitions
+  std::vector<Expr> eassertsProc;
+  std::unordered_map<Node, Node, NodeHashFunction> cache;
+  for (const Expr& e : easserts)
+  {
+    Node ea = Node::fromExpr(e);
+    Node eae = d_private->expandDefinitions(ea, cache);
+    eassertsProc.push_back(eae.toExpr());
+  }
+  return eassertsProc;
+}
+
 Expr SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; }
 
 Expr SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 566777a89..316ca16d1 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -402,6 +402,16 @@ class CVC4_PUBLIC SmtEngine {
    * that).
    */
   Result quickCheck();
+  /** get the model, if it is available and return a pointer to it
+   *
+   * This ensures that the model is currently available, which means that
+   * CVC4 is producing models, and is in "SAT mode", otherwise an exception
+   * is thrown.
+   *
+   * The flag c is used for giving an error message to indicate the context
+   * this method was called.
+   */
+  theory::TheoryModel* getAvailableModel(const char* c) const;
 
   /**
    * Fully type-check the argument, and also type-check that it's
@@ -480,6 +490,12 @@ class CVC4_PUBLIC SmtEngine {
    */
   std::pair<Expr, Expr> getSepHeapAndNilExpr();
 
+  /** get expanded assertions
+   *
+   * Returns the set of assertions, after expanding definitions.
+   */
+  std::vector<Expr> getExpandedAssertions();
+
  public:
 
   /**
@@ -553,12 +569,37 @@ class CVC4_PUBLIC SmtEngine {
   std::string getFilename() const;
   /**
    * Get the model (only if immediately preceded by a SAT
-   * or INVALID query).  Only permitted if CVC4 was built with model
-   * support and produce-models is on.
+   * or INVALID query).  Only permitted if produce-models is on.
    */
   Model* getModel();
 
   /**
+   * Block the current model. Can be called only if immediately preceded by
+   * a SAT or INVALID query. Only permitted if produce-models is on, and the
+   * block-models option is set to a mode other than "none".
+   *
+   * This adds an assertion to the assertion stack that blocks the current
+   * model based on the current options configured by CVC4.
+   *
+   * The return value has the same meaning as that of assertFormula.
+   */
+  Result blockModel();
+
+  /**
+   * Block the current model values of (at least) the values in exprs.
+   * Can be called only if immediately preceded by a SAT or INVALID query. Only
+   * permitted if produce-models is on, and the block-models option is set to a
+   * mode other than "none".
+   *
+   * This adds an assertion to the assertion stack of the form:
+   *  (or (not (= exprs[0] M0)) ... (not (= exprs[n] Mn)))
+   * where M0 ... Mn are the current model values of exprs[0] ... exprs[n].
+   *
+   * The return value has the same meaning as that of assertFormula.
+   */
+  Result blockModelValues(const std::vector<Expr>& exprs);
+
+  /**
    * When using separation logic, obtain the expression for the heap.
    */
   Expr getSepHeapExpr();
@@ -775,6 +816,11 @@ class CVC4_PUBLIC SmtEngine {
       ;
 
   /**
+   * Same as getValue but for a vector of expressions
+   */
+  std::vector<Expr> getValues(const std::vector<Expr>& exprs);
+
+  /**
    * Add a function to the set of expressions whose value is to be
    * later returned by a call to getAssignment().  The expression
    * should be a Boolean zero-ary defined function or a Boolean