compiling

7 files changed, 249 insertions, 162 deletions

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 2a59ace11..f43fce867 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1756,6 +1756,53 @@ ModelCoresMode OptionsHandler::stringToModelCoresMode(std::string option,
   }
 }
 
+
+
+
+const std::string OptionsHandler::s_blockModelsHelp =
+    "\
+Blocking models modes are currently supported by the --simplification option:\n\
+\n\
+none (default) \n\
++ do not block models\n\
+\n\
+literals\n\
++ block models based on the SAT skeleton\n\
+\n\
+values\n\
++ block models based on the concrete model values for the free variables.\n\ 
+\n\
+";
+
+BlockModelsMode OptionsHandler::stringToBlockModelsMode(std::string option,
+                                                      std::string optarg)
+{
+  if (optarg == "none")
+  {
+    return BLOCK_MODELS_NONE;
+  }
+  else if (optarg == "literals")
+  {
+    return BLOCK_MODELS_LITERALS;
+  }
+  else if (optarg == "values")
+  {
+    return BLOCK_MODELS_VALUES;;
+  }
+  else if (optarg == "help")
+  {
+    puts(s_blockModelsHelp.c_str());
+    exit(1);
+  }
+  else
+  {
+    throw OptionException(std::string("unknown option for --block-models: `")
+                          + optarg + "'.  Try --block-models help.");
+  }
+}
+
+
+
 const std::string OptionsHandler::s_sygusSolutionOutModeHelp =
     "\
 Modes for finite model finding bound minimization, supported by --sygus-out:\n\
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 06f7ab6e4..8dba60ff1 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -186,6 +186,7 @@ public:
   SimplificationMode stringToSimplificationMode(std::string option,
                                                 std::string optarg);
   ModelCoresMode stringToModelCoresMode(std::string option, std::string optarg);
+  BlockModelsMode stringToBlockModelsMode(std::string option, std::string optarg);
   SygusSolutionOutMode stringToSygusSolutionOutMode(std::string option,
                                                     std::string optarg);
   void setProduceAssertions(std::string option, bool value);
@@ -261,6 +262,7 @@ public:
   static const std::string s_qcfWhenModeHelp;
   static const std::string s_simplificationHelp;
   static const std::string s_modelCoresHelp;
+  static const std::string s_blockModelsHelp;
   static const std::string s_sygusSolutionOutModeHelp;
   static const std::string s_cbqiBvIneqModeHelp;
   static const std::string s_cegqiSingleInvHelp;
diff --git a/src/options/smt_modes.h b/src/options/smt_modes.h
index ed40a28a1..826636723 100644
--- a/src/options/smt_modes.h
+++ b/src/options/smt_modes.h
@@ -53,6 +53,23 @@ enum ModelCoresMode
   MODEL_CORES_NON_IMPLIED
 };
 
+
+/** Block models modes. */
+enum BlockModelsMode
+{
+  /** Do not block models */
+  BLOCK_MODELS_NONE,
+  /**
+   * block models based on literals truth values.
+   */
+  BLOCK_MODELS_LITERALS,
+  /**
+   * block models based on concrete variable values in the model.
+   */
+  BLOCK_MODELS_VALUES,
+};
+
+
 }  // namespace CVC4
 
 #endif /* CVC4__SMT__MODES_H */
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 5f60f7337..7dc5df7d2 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -108,13 +108,16 @@ header = "options/smt_options.h"
   includes   = ["options/smt_modes.h"]
   help       = "mode for producing model cores"
 
+
 [[option]]
-  name       = "blockModels"
+  name       = "blockModelsMode"
   category   = "regular"
-  long       = "block-models"
-  type       = "bool"
-  read_only  = true
-  help       = "add assertion that blocks the current model when get-model is called"
+  long       = "block-models==MODE"
+  type       = "BlockModelsMode"
+  default    = "BLOCK_MODELS_NONE"
+  handler    = "stringToBlockModelsMode"
+  includes   = ["options/smt_modes.h"]
+  help       = "mode for producing several models"
 
 [[option]]
   name       = "proof"
diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp
index 189510dc7..3d59c4dbd 100644
--- a/src/smt/model_blocker.cpp
+++ b/src/smt/model_blocker.cpp
@@ -15,6 +15,7 @@
 #include "smt/model_blocker.h"
 
 #include "expr/node.h"
+#include "expr/node_algorithm.h"
 #include "theory/quantifiers/term_util.h"
 
 using namespace CVC4::kind;
@@ -22,8 +23,10 @@ using namespace CVC4::kind;
 namespace CVC4 {
 
 Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
-                                   Model* m)
+                                   theory::TheoryModel* m,
+                                   BlockModelsMode mode)
 {
+  NodeManager* nm = NodeManager::currentNM();
   // convert to nodes
   std::vector<Node> tlAsserts;
   for (unsigned i = 0, size = assertions.size(); i < size; i++)
@@ -32,195 +35,210 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
     tlAsserts.push_back(a);
   }
   Trace("model-blocker") << "Compute model blocker, assertions:" << std::endl;
-  // optimization: filter to only top-level disjunctions
-  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)
+  Node blocker;
+  if (mode == BLOCK_MODELS_LITERALS) {
+    // optimization: filter to only top-level disjunctions
+    unsigned counter = 0;
+    std::vector<Node> asserts;
+    while (counter < tlAsserts.size())
     {
-      tlAsserts.push_back(catom[0]);
-    }
-    else if (catom.getKind() == AND && cpol)
-    {
-      for (const Node& c : catom)
+      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.push_back(c);
+        for (const Node& c : catom)
+        {
+          tlAsserts.push_back(c);
+        }
+      }
+      else if (theory::quantifiers::TermUtil::isBoolConnectiveTerm(catom))
+      {
+        asserts.push_back(cur);
+        Trace("model-blocker") << "  " << cur << std::endl;
       }
     }
-    else if (theory::quantifiers::TermUtil::isBoolConnectiveTerm(catom))
+    if (asserts.empty())
     {
-      asserts.push_back(cur);
-      Trace("model-blocker") << "  " << cur << std::endl;
+      Node blockTriv = nm->mkConst(false);
+      Trace("model-blocker") << "...model blocker is (trivially) " << blockTriv
+                             << std::endl;
+      return blockTriv.toExpr();
     }
-  }
-  NodeManager* nm = NodeManager::currentNM();
-  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())
+    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
     {
-      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)
+      cur = visit.back();
+      visit.pop_back();
+      it = visited.find(cur);
+      
+      Trace("model-blocker-debug") << "Visit : " << cur << std::endl;
+
+      if (it == visited.end())
       {
-        // if disjunctive
-        if ((catom.getKind() == OR) == cpol)
+        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)
         {
-          // take the first literal that is satisfied
-          for (Node n : catom)
+          // if disjunctive
+          if ((catom.getKind() == OR) == cpol)
           {
-            // 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)
+            // 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)
             {
-              impl = cpol ? n : n.negate();
-              break;
+              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() == OR)
+        else if ((catom.getKind() == EQUAL && catom[0].getType().isBoolean())
+                 || catom.getKind() == XOR)
         {
-          // one step NNF
+          // based on how the children evaluate in the model
           std::vector<Node> children;
           for (const Node& cn : catom)
           {
-            children.push_back(cn.negate());
+            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 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());
+          // literals justified by themselves
+          visited[cur] = cur;
+          Trace("model-blocker-debug") << "...self justified" << std::endl;
         }
-        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())
+        if (visited[cur].isNull())
         {
-          Assert(cur.getKind() == AND);
-          Trace("model-blocker-debug") << "...recurse" << std::endl;
-          for (const Node& cn : cur)
+          visit.push_back(cur);
+          if (impl.isNull())
+          {
+            Assert(cur.getKind() == AND);
+            Trace("model-blocker-debug") << "...recurse" << std::endl;
+            for (const Node& cn : cur)
+            {
+              visit.push_back(cn);
+            }
+          }
+          else
           {
-            visit.push_back(cn);
+            Trace("model-blocker-debug") << "...implicant : " << impl << std::endl;
+            implicant[cur] = impl;
+            visit.push_back(impl);
           }
         }
-        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
+      else if (it->second.isNull())
       {
-        bool childChanged = false;
-        std::vector<Node> children;
-        // we never recurse to parameterized nodes
-        Assert(cur.getMetaKind() != metakind::PARAMETERIZED);
-        for (const Node& cn : cur)
+        Node ret = cur;
+        it = implicant.find(cur);
+        if (it != implicant.end())
         {
-          it = visited.find(cn);
+          Node impl = it->second;
+          it = visited.find(impl);
           Assert(it != visited.end());
           Assert(!it->second.isNull());
-          childChanged = childChanged || cn != it->second;
-          children.push_back(it->second);
+          ret = it->second;
+          Trace("model-blocker-debug") << "...implicant res: " << ret << std::endl;
         }
-        if (childChanged)
+        else
         {
-          ret = nm->mkNode(cur.getKind(), children);
+          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;
         }
-        Trace("model-blocker-debug") << "...recons res: " << ret << std::endl;
+        visited[cur] = ret;
       }
-      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::unordered_set<Node, NodeHashFunction> symbols;
+    for (Node n: tlAsserts) {
+      expr::getSymbols(n, symbols);
     }
-  } while (!visit.empty());
-  Assert(visited.find(formula) != visited.end());
-  Assert(!visited.find(formula)->second.isNull());
-  Node blocker = visited[formula].negate();
+    std::vector<Node> blockers;
+    for (Node s : symbols) {
+      Node v = m->getValue(s);
+      Node a = nm->mkNode(DISTINCT, s, v);
+      blockers.push_back(a);
+    }
+    blocker = nm->mkNode(AND, blockers);
+  }
   Trace("model-blocker") << "...model blocker is " << blocker << std::endl;
   return blocker.toExpr();
 }
diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h
index ce80d2144..9c760aaa5 100644
--- a/src/smt/model_blocker.h
+++ b/src/smt/model_blocker.h
@@ -21,7 +21,7 @@
 
 #include "expr/expr.h"
 #include "options/smt_options.h"
-#include "smt/model.h"
+#include "theory/theory_model.h"
 
 namespace CVC4 {
 
@@ -49,7 +49,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, Model* m);
+  static Expr getModelBlocker(const std::vector<Expr>& assertions, theory::TheoryModel* m, BlockModelsMode mode);
 }; /* class TheoryModelCoreBuilder */
 
 }  // namespace CVC4
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b11105718..efd31a9e5 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1284,7 +1284,7 @@ void SmtEngine::setDefaults() {
 
   if ((options::checkModels() || options::checkSynthSol()
        || options::modelCoresMode() != MODEL_CORES_NONE
-       || options::blockModels())
+       || options::blockModelsMode() != BLOCK_MODELS_NONE)
       && !options::produceAssertions())
   {
     Notice() << "SmtEngine: turning on produce-assertions to support "
@@ -4372,7 +4372,7 @@ Model* SmtEngine::getModel() {
   // the theory engine into "eager model building" mode. TODO #2648: revisit.
   d_theoryEngine->setEagerModelBuilding();
 
-  if (options::modelCoresMode() != MODEL_CORES_NONE || options::blockModels())
+  if (options::modelCoresMode() != MODEL_CORES_NONE || options::blockModelsMode() != BLOCK_MODELS_NONE)
   {
     // If we enabled model cores, we compute a model core for m based on our
     // assertions using the model core builder utility
@@ -4391,9 +4391,9 @@ Model* SmtEngine::getModel() {
       ModelCoreBuilder::setModelCore(
           eassertsProc, m, options::modelCoresMode());
     }
-    if (options::blockModels())
+    if (options::blockModelsMode() != BLOCK_MODELS_NONE)
     {
-      Expr eblocker = ModelBlocker::getModelBlocker(eassertsProc, m);
+      Expr eblocker = ModelBlocker::getModelBlocker(eassertsProc, m, options::blockModelsMode());
       assertFormula(eblocker);
     }
   }