Bug fix, doc

2 files changed, 20 insertions, 2 deletions

diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp
index e680219a0..189510dc7 100644
--- a/src/smt/model_blocker.cpp
+++ b/src/smt/model_blocker.cpp
@@ -79,6 +79,8 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
     cur = visit.back();
     visit.pop_back();
     it = visited.find(cur);
+    
+    Trace("model-blocker-debug") << "Visit : " << cur << std::endl;
 
     if (it == visited.end())
     {
@@ -117,7 +119,7 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
         {
           // one step NNF
           std::vector<Node> children;
-          for (const Node& cn : cur)
+          for (const Node& cn : catom)
           {
             children.push_back(cn.negate());
           }
@@ -158,6 +160,7 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
       {
         // literals justified by themselves
         visited[cur] = cur;
+        Trace("model-blocker-debug") << "...self justified" << std::endl;
       }
       if (visited[cur].isNull())
       {
@@ -165,6 +168,7 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
         if (impl.isNull())
         {
           Assert(cur.getKind() == AND);
+          Trace("model-blocker-debug") << "...recurse" << std::endl;
           for (const Node& cn : cur)
           {
             visit.push_back(cn);
@@ -172,6 +176,7 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
         }
         else
         {
+          Trace("model-blocker-debug") << "...implicant : " << impl << std::endl;
           implicant[cur] = impl;
           visit.push_back(impl);
         }
@@ -188,6 +193,7 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
         Assert(it != visited.end());
         Assert(!it->second.isNull());
         ret = it->second;
+        Trace("model-blocker-debug") << "...implicant res: " << ret << std::endl;
       }
       else
       {
@@ -207,6 +213,7 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
         {
           ret = nm->mkNode(cur.getKind(), children);
         }
+        Trace("model-blocker-debug") << "...recons res: " << ret << std::endl;
       }
       visited[cur] = ret;
     }
diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h
index cc667fbf0..ce80d2144 100644
--- a/src/smt/model_blocker.h
+++ b/src/smt/model_blocker.h
@@ -36,7 +36,18 @@ class ModelBlocker
    * 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) L1 ... Ln are literals that occur in assertions.
+   * (2) L1 ... Ln are literals that occur in assertions and propositionally
+   * entail all non-unit top-level assertions.
+   * 
+   * 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).
+   * 
+   * 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, Model* m);
 }; /* class TheoryModelCoreBuilder */