Format

3 files changed, 56 insertions, 51 deletions

diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp
index 46dee937a..e680219a0 100644
--- a/src/smt/model_blocker.cpp
+++ b/src/smt/model_blocker.cpp
@@ -14,15 +14,15 @@
 
 #include "smt/model_blocker.h"
 
-#include "theory/quantifiers/term_util.h"
 #include "expr/node.h"
+#include "theory/quantifiers/term_util.h"
 
 using namespace CVC4::kind;
 
 namespace CVC4 {
 
 Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
-                              Model* m)
+                                   Model* m)
 {
   // convert to nodes
   std::vector<Node> tlAsserts;
@@ -35,98 +35,102 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
   // optimization: filter to only top-level disjunctions
   unsigned counter = 0;
   std::vector<Node> asserts;
-  while( counter<tlAsserts.size() ){
+  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 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 )
+    else if (catom.getKind() == AND && cpol)
     {
-      for( const Node& c : catom ){
+      for (const Node& c : catom)
+      {
         tlAsserts.push_back(c);
       }
     }
-    else if( theory::quantifiers::TermUtil::isBoolConnectiveTerm(catom) )
+    else if (theory::quantifiers::TermUtil::isBoolConnectiveTerm(catom))
     {
       asserts.push_back(cur);
       Trace("model-blocker") << "  " << cur << std::endl;
     }
   }
   NodeManager* nm = NodeManager::currentNM();
-  if( asserts.empty() )
+  if (asserts.empty())
   {
     Node blockTriv = nm->mkConst(false);
-    Trace("model-blocker") << "...model blocker is (trivially) " << blockTriv << std::endl;
+    Trace("model-blocker") << "...model blocker is (trivially) " << blockTriv
+                           << std::endl;
     return blockTriv.toExpr();
   }
 
-  Node formula = asserts.size() > 1? nm->mkNode(AND, asserts) : asserts[0];
+  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 
+  do
   {
     cur = visit.back();
     visit.pop_back();
     it = visited.find(cur);
 
-    if (it == visited.end()) 
+    if (it == visited.end())
     {
       visited[cur] = Node::null();
-      Node catom = cur.getKind()==NOT ? cur[0] : cur;
-      bool cpol = cur.getKind()!=NOT;
+      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 )
+      if (catom.getKind() == NOT)
       {
         // double negation
         impl = catom[0];
       }
-      else if( catom.getKind()==OR || catom.getKind()==AND )
+      else if (catom.getKind() == OR || catom.getKind() == AND)
       {
         // if disjunctive
-        if( (catom.getKind()==OR)==cpol )
+        if ((catom.getKind() == OR) == cpol)
         {
           // take the first literal that is satisfied
-          for( Node n : catom )
+          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 )
+            Assert(vn.isConst());
+            if (vn.getConst<bool>() == cpol)
             {
               impl = cpol ? n : n.negate();
               break;
             }
           }
         }
-        else if( catom.getKind()==OR )
+        else if (catom.getKind() == OR)
         {
           // one step NNF
-          std::vector< Node > children;
-          for (const Node& cn : cur )
+          std::vector<Node> children;
+          for (const Node& cn : cur)
           {
             children.push_back(cn.negate());
           }
-          impl = nm->mkNode( AND, children );
+          impl = nm->mkNode(AND, children);
         }
       }
-      else if( catom.getKind()==ITE )
+      else if (catom.getKind() == ITE)
       {
         Node vcond = Node::fromExpr(m->getValue(cur[0].toExpr()));
-        Assert( vcond.isConst() );
+        Assert(vcond.isConst());
         Node cond = cur[0];
         Node branch;
-        if( vcond.getConst<bool>() )
+        if (vcond.getConst<bool>())
         {
           branch = cur[1];
         }
@@ -135,32 +139,33 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
           cond = cond.negate();
           branch = cur[2];
         }
-        impl = nm->mkNode(AND, cond, cpol ? branch : branch.negate() );
+        impl = nm->mkNode(AND, cond, cpol ? branch : branch.negate());
       }
-      else if( ( catom.getKind()==EQUAL && catom[0].getType().isBoolean() ) || catom.getKind()==XOR )
+      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 )
+        std::vector<Node> children;
+        for (const Node& cn : catom)
         {
           Node vn = Node::fromExpr(m->getValue(cn.toExpr()));
-          Assert( vn.isConst() );
+          Assert(vn.isConst());
           children.push_back(vn.getConst<bool>() ? cn : cn.negate());
         }
-        impl = nm->mkNode( AND, children );
+        impl = nm->mkNode(AND, children);
       }
       else
       {
         // literals justified by themselves
         visited[cur] = cur;
       }
-      if( visited[cur].isNull() )
+      if (visited[cur].isNull())
       {
         visit.push_back(cur);
-        if( impl.isNull() )
+        if (impl.isNull())
         {
-          Assert( cur.getKind()==AND );
-          for (const Node& cn : cur )
+          Assert(cur.getKind() == AND);
+          for (const Node& cn : cur)
           {
             visit.push_back(cn);
           }
@@ -171,12 +176,12 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
           visit.push_back(impl);
         }
       }
-    } 
-    else if (it->second.isNull()) 
+    }
+    else if (it->second.isNull())
     {
       Node ret = cur;
       it = implicant.find(cur);
-      if( it!=implicant.end() )
+      if (it != implicant.end())
       {
         Node impl = it->second;
         it = visited.find(impl);
@@ -190,7 +195,7 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
         std::vector<Node> children;
         // we never recurse to parameterized nodes
         Assert(cur.getMetaKind() != metakind::PARAMETERIZED);
-        for (const Node& cn : cur )
+        for (const Node& cn : cur)
         {
           it = visited.find(cn);
           Assert(it != visited.end());
@@ -198,7 +203,7 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions,
           childChanged = childChanged || cn != it->second;
           children.push_back(it->second);
         }
-        if (childChanged) 
+        if (childChanged)
         {
           ret = nm->mkNode(cur.getKind(), children);
         }
diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h
index 836515013..cc667fbf0 100644
--- a/src/smt/model_blocker.h
+++ b/src/smt/model_blocker.h
@@ -32,14 +32,13 @@ 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) L1 ... Ln are literals that occur in assertions.
    */
-  static Expr getModelBlocker(const std::vector<Expr>& assertions,
-                              Model* m);
+  static Expr getModelBlocker(const std::vector<Expr>& assertions, Model* m);
 }; /* class TheoryModelCoreBuilder */
 
 }  // namespace CVC4
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0f2543be6..b11105718 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -84,8 +84,8 @@
 #include "smt/command_list.h"
 #include "smt/logic_request.h"
 #include "smt/managed_ostreams.h"
-#include "smt/model_core_builder.h"
 #include "smt/model_blocker.h"
+#include "smt/model_core_builder.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/term_formula_removal.h"
 #include "smt/update_ostream.h"
@@ -4386,11 +4386,12 @@ Model* SmtEngine::getModel() {
       Node eae = d_private->expandDefinitions(ea, cache);
       eassertsProc.push_back(eae.toExpr());
     }
-    if( options::modelCoresMode() != MODEL_CORES_NONE )
+    if (options::modelCoresMode() != MODEL_CORES_NONE)
     {
-      ModelCoreBuilder::setModelCore(eassertsProc, m, options::modelCoresMode());
+      ModelCoreBuilder::setModelCore(
+          eassertsProc, m, options::modelCoresMode());
     }
-    if( options::blockModels() )
+    if (options::blockModels())
     {
       Expr eblocker = ModelBlocker::getModelBlocker(eassertsProc, m);
       assertFormula(eblocker);