Format

7 files changed, 93 insertions, 77 deletions

diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index d9a2d1711..f1ec78aab 100644
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -60,9 +60,10 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkAssume(Node fact)
   return mkNode(PfRule::ASSUME, children, args, fact);
 }
 
-std::shared_ptr<ProofNode> ProofNodeManager::mkScope(std::shared_ptr<ProofNode> pf,
-                                                     std::vector<Node>& assumps,
-                                     bool ensureClosed)
+std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
+    std::shared_ptr<ProofNode> pf,
+    std::vector<Node>& assumps,
+    bool ensureClosed)
 {
   std::vector<std::shared_ptr<ProofNode>> pfChildren;
   pfChildren.push_back(pf);
@@ -108,9 +109,9 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(std::shared_ptr<ProofNode>
       itf = ac.find(aeqSym);
       if (itf != ac.end())
       {
-        Trace("pnm-scope")
-            << "- reorient assumption " << aeqSym << " via " << a << " for "
-            << fa.second.size() << " proof nodes" << std::endl;
+        Trace("pnm-scope") << "- reorient assumption " << aeqSym << " via " << a
+                           << " for " << fa.second.size() << " proof nodes"
+                           << std::endl;
         std::shared_ptr<ProofNode> pfaa = mkAssume(aeqSym);
         for (ProofNode* pfs : fa.second)
         {
@@ -120,8 +121,7 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(std::shared_ptr<ProofNode>
           children.push_back(pfaa);
           std::vector<Node> args;
           args.push_back(a);
-          updateNode(
-              pfs, PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
+          updateNode(pfs, PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
         }
         Trace("pnm-scope") << "...finished" << std::endl;
         acu.insert(aeqSym);
@@ -136,9 +136,8 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(std::shared_ptr<ProofNode>
     {
       ss << "- assumption: " << aprint << std::endl;
     }
-    AlwaysAssert(false)
-        << "Generated a proof that is not closed by the scope: " << ss.str()
-        << std::endl;
+    AlwaysAssert(false) << "Generated a proof that is not closed by the scope: "
+                        << ss.str() << std::endl;
   }
   if (acu.size() < ac.size())
   {
@@ -149,15 +148,15 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(std::shared_ptr<ProofNode>
       if (acu.find(a) == acu.end())
       {
         Notice() << "ProofNodeManager::mkScope: assumption " << a
-                  << " does not match a free assumption in proof" << std::endl;
+                 << " does not match a free assumption in proof" << std::endl;
       }
     }
   }
   assumps.clear();
-  assumps.insert(assumps.end(), acu.begin(), acu.end());  
+  assumps.insert(assumps.end(), acu.begin(), acu.end());
   return mkNode(PfRule::SCOPE, pfChildren, assumps);
 }
-  
+
 bool ProofNodeManager::updateNode(
     ProofNode* pn,
     PfRule id,
diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h
index 7cf6574cb..527f2562d 100644
--- a/src/expr/proof_node_manager.h
+++ b/src/expr/proof_node_manager.h
@@ -83,9 +83,8 @@ class ProofNodeManager
   /** Make scope */
   std::shared_ptr<ProofNode> mkScope(std::shared_ptr<ProofNode> pf,
                                      std::vector<Node>& assumps,
-                                     bool ensureClosed = true
-                                    );
-  
+                                     bool ensureClosed = true);
+
   /**
    * This method updates pn to be a proof of the form <id>( children, args ),
    * while maintaining its d_proven field. This method returns false if this
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index b57bb112b..b05dbf7e7 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -81,7 +81,8 @@ Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp, MethodId ids)
 }
 
 Node BuiltinProofRuleChecker::applySubstitution(Node n,
-                                                const std::vector<Node>& exp, MethodId ids)
+                                                const std::vector<Node>& exp,
+                                                MethodId ids)
 {
   Node nk = ProofSkolemCache::getSkolemForm(n);
   Node nks = applySubstitutionExternal(nk, exp, ids);
@@ -119,36 +120,38 @@ Node BuiltinProofRuleChecker::applyRewriteExternal(Node n, MethodId idr)
   }
   // unknown rewriter
   Assert(false)
-      << "BuiltinProofRuleChecker::applyRewriteExternal: no rewriter for " << idr
-      << std::endl;
+      << "BuiltinProofRuleChecker::applyRewriteExternal: no rewriter for "
+      << idr << std::endl;
   return n;
 }
 
-Node BuiltinProofRuleChecker::applySubstitutionExternal(Node n, Node exp, MethodId ids)
+Node BuiltinProofRuleChecker::applySubstitutionExternal(Node n,
+                                                        Node exp,
+                                                        MethodId ids)
 {
   Assert(!exp.isNull());
   Node expk = ProofSkolemCache::getSkolemForm(exp);
   TNode var, subs;
-  if (ids==MethodId::SB_DEFAULT)
+  if (ids == MethodId::SB_DEFAULT)
   {
-    if (expk.getKind()!=EQUAL)
+    if (expk.getKind() != EQUAL)
     {
       return Node::null();
     }
     var = expk[0];
     subs = expk[1];
   }
-  else if (ids==MethodId::SB_PREDICATE)
+  else if (ids == MethodId::SB_PREDICATE)
   {
-    bool polarity = expk.getKind()!=NOT;
+    bool polarity = expk.getKind() != NOT;
     var = polarity ? expk : expk[0];
     subs = NodeManager::currentNM()->mkConst(polarity);
   }
   else
   {
-  Assert(false)
-      << "BuiltinProofRuleChecker::applySubstitutionExternal: no substitution for " << ids
-      << std::endl;
+    Assert(false) << "BuiltinProofRuleChecker::applySubstitutionExternal: no "
+                     "substitution for "
+                  << ids << std::endl;
   }
   return n.substitute(var, subs);
 }
@@ -217,7 +220,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     Assert(children.size() > 0);
     Assert(1 <= args.size() && args.size() <= 2);
     MethodId ids = MethodId::SB_DEFAULT;
-    if (args.size()==2 && !getMethodId(args[1], ids))
+    if (args.size() == 2 && !getMethodId(args[1], ids))
     {
       return Node::null();
     }
@@ -234,7 +237,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     Assert(children.empty());
     Assert(1 <= args.size() && args.size() <= 2);
     MethodId ids = MethodId::RW_REWRITE;
-    if (args.size()==2 && !getMethodId(args[1], ids))
+    if (args.size() == 2 && !getMethodId(args[1], ids))
     {
       return Node::null();
     }
@@ -350,7 +353,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
   return Node::null();
 }
 
-bool BuiltinProofRuleChecker::getMethodIds(const std::vector<Node>& args, MethodId& ids, MethodId& idr, size_t index)
+bool BuiltinProofRuleChecker::getMethodIds(const std::vector<Node>& args,
+                                           MethodId& ids,
+                                           MethodId& idr,
+                                           size_t index)
 {
   ids = MethodId::SB_DEFAULT;
   idr = MethodId::RW_REWRITE;
@@ -363,12 +369,12 @@ bool BuiltinProofRuleChecker::getMethodIds(const std::vector<Node>& args, Method
       return false;
     }
   }
-  if (args.size() >= index+1)
+  if (args.size() >= index + 1)
   {
-    if (!getMethodId(args[index+1], idr))
+    if (!getMethodId(args[index + 1], idr))
     {
       Trace("builtin-pfcheck")
-          << "Failed to get id from " << args[index+1] << std::endl;
+          << "Failed to get id from " << args[index + 1] << std::endl;
       return false;
     }
   }
diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h
index 9291bbf9f..afd9bad5a 100644
--- a/src/theory/builtin/proof_checker.h
+++ b/src/theory/builtin/proof_checker.h
@@ -30,8 +30,8 @@ namespace theory {
  * is semantically equivalent to the input. The identifiers below list
  * various methods that have this contract. This identifier is used
  * in a number of the builtin rules.
- * 
- * A substitution is a method for turning a formula into 
+ *
+ * A substitution is a method for turning a formula into
  */
 enum class MethodId : uint32_t
 {
@@ -83,10 +83,12 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
    * substitution
    * @return The substituted form of n.
    */
-  static Node applySubstitution(Node n, Node exp,
-                                       MethodId ids = MethodId::SB_DEFAULT);
-  static Node applySubstitution(Node n, const std::vector<Node>& exp,
-                                       MethodId ids = MethodId::SB_DEFAULT);
+  static Node applySubstitution(Node n,
+                                Node exp,
+                                MethodId ids = MethodId::SB_DEFAULT);
+  static Node applySubstitution(Node n,
+                                const std::vector<Node>& exp,
+                                MethodId ids = MethodId::SB_DEFAULT);
   /** Apply substitution + rewriting
    *
    * Combines the above two steps.
@@ -113,7 +115,10 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
                      const std::vector<Node>& children,
                      const std::vector<Node>& args) override;
   /** get method ids */
-  bool getMethodIds(const std::vector<Node>& args, MethodId& ids, MethodId& idr, size_t index);
+  bool getMethodIds(const std::vector<Node>& args,
+                    MethodId& ids,
+                    MethodId& idr,
+                    size_t index);
   /**
    * Apply rewrite (on Skolem form). id is the identifier of the rewriter.
    */
@@ -124,7 +129,9 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
    * n * { exp[0] -> exp[1] } in Skolem form.
    */
   static Node applySubstitutionExternal(Node n, Node exp, MethodId ids);
-  static Node applySubstitutionExternal(Node n, const std::vector<Node>& exp, MethodId ids);
+  static Node applySubstitutionExternal(Node n,
+                                        const std::vector<Node>& exp,
+                                        MethodId ids);
 };
 
 }  // namespace builtin
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index bad121d65..281b1abff 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -306,8 +306,11 @@ Node InferProofCons::convert(Inference infer,
         // optimization in processSimpleNEq. Alternatively, this could
         // possibly be done by CONCAT_EQ with !isRev.
         std::vector<Node> cexp;
-        if (convertPredTransform(
-                mainEqCeq, conc, cexp, MethodId::SB_DEFAULT, MethodId::RW_REWRITE_EQ_EXT))
+        if (convertPredTransform(mainEqCeq,
+                                 conc,
+                                 cexp,
+                                 MethodId::SB_DEFAULT,
+                                 MethodId::RW_REWRITE_EQ_EXT))
         {
           Trace("strings-ipc-core") << "Transformed to " << conc
                                     << " via pred transform" << std::endl;
@@ -916,16 +919,16 @@ bool InferProofCons::convertPredTransform(Node src,
   // try to prove that tgt rewrites to src
   children.insert(children.end(), exp.begin(), exp.end());
   args.push_back(tgt);
-  addMethodIds(args,ids,idr);
+  addMethodIds(args, ids, idr);
   Node res = d_psb.tryStep(PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
   if (res.isNull())
   {
     // failed to apply
     return false;
   }
-  Trace("strings-ipc-debug")
-      << "InferProofCons::convertPredTransform: success " << src
-      << " == " << tgt << " under " << exp << " via " << ids << "/" << idr << std::endl;
+  Trace("strings-ipc-debug") << "InferProofCons::convertPredTransform: success "
+                             << src << " == " << tgt << " under " << exp
+                             << " via " << ids << "/" << idr << std::endl;
   // should definitely have concluded tgt
   Assert(res == tgt);
   return true;
@@ -938,7 +941,7 @@ bool InferProofCons::convertPredIntro(Node tgt,
 {
   std::vector<Node> args;
   args.push_back(tgt);
-  addMethodIds(args,ids,idr);
+  addMethodIds(args, ids, idr);
   Node res = d_psb.tryStep(PfRule::MACRO_SR_PRED_INTRO, exp, args);
   if (res.isNull())
   {
@@ -950,14 +953,14 @@ bool InferProofCons::convertPredIntro(Node tgt,
 
 Node InferProofCons::convertPredElim(Node src,
                                      const std::vector<Node>& exp,
-                                    MethodId ids,
+                                     MethodId ids,
                                      MethodId idr)
 {
   std::vector<Node> children;
   children.push_back(src);
   children.insert(children.end(), exp.begin(), exp.end());
   std::vector<Node> args;
-  addMethodIds(args,ids,idr);
+  addMethodIds(args, ids, idr);
   Node srcRew = d_psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, children, args);
   if (isSymm(src, srcRew))
   {
@@ -967,9 +970,9 @@ Node InferProofCons::convertPredElim(Node src,
   return srcRew;
 }
 
-void InferProofCons::addMethodIds(std::vector<Node>& args, 
-                      MethodId ids,
-                      MethodId idr)
+void InferProofCons::addMethodIds(std::vector<Node>& args,
+                                  MethodId ids,
+                                  MethodId idr)
 {
   bool ndefRewriter = (idr != MethodId::RW_REWRITE);
   if (ids != MethodId::SB_DEFAULT || ndefRewriter)
diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h
index f5bb57996..ed38fdb96 100644
--- a/src/theory/strings/infer_proof_cons.h
+++ b/src/theory/strings/infer_proof_cons.h
@@ -141,9 +141,7 @@ class InferProofCons : public ProofGenerator
                        MethodId ids = MethodId::SB_DEFAULT,
                        MethodId idr = MethodId::RW_REWRITE);
   /** Add method ids */
-  void addMethodIds(std::vector<Node>& args, 
-                       MethodId ids,
-                       MethodId idr);
+  void addMethodIds(std::vector<Node>& args, MethodId ids, MethodId idr);
   /**
    */
   Node convertTrans(Node eqa, Node eqb);
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index b571fc2b8..3b1c5bfaa 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1915,7 +1915,6 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
 
     // FIXME: have ~( l1 ^ ... ^ ln ) and ( E1 ^ ... ^ En ) => l1 ^ ... ^ ln
     // Prove ~( E1 ^ ... ^ En )
-    
 
     Node fullConflict = tnc.getNode();
     Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl;
@@ -2008,13 +2007,13 @@ theory::TrustNode TheoryEngine::getExplanation(
     LemmaProofRecipe* proofRecipe)
 {
   Assert(explanationVector.size() == 1);
-  
+
   Node conclusion = explanationVector[0].d_node;
   std::unique_ptr<LazyCDProof> lcp;
-  if (d_lazyProof!=nullptr)
+  if (d_lazyProof != nullptr)
   {
     // FIXME
-    //lcp.reset(new LazyCDProof(d_pNodeManager.get()));
+    // lcp.reset(new LazyCDProof(d_pNodeManager.get()));
   }
   unsigned i = 0; // Index of the current literal we are processing
   unsigned j = 0; // Index of the last literal we are keeping
@@ -2038,19 +2037,21 @@ theory::TrustNode TheoryEngine::getExplanation(
         << toExplain.d_theory << endl;
 
     // If a true constant or a negation of a false constant we can ignore it
-    if ((toExplain.d_node.isConst() && toExplain.d_node.getConst<bool>()) ||
-      (toExplain.d_node.getKind() == kind::NOT && toExplain.d_node[0].isConst()
-        && !toExplain.d_node[0].getConst<bool>()))
+    if ((toExplain.d_node.isConst() && toExplain.d_node.getConst<bool>())
+        || (toExplain.d_node.getKind() == kind::NOT
+            && toExplain.d_node[0].isConst()
+            && !toExplain.d_node[0].getConst<bool>()))
     {
       ++ i;
-      if (lcp!=nullptr)
+      if (lcp != nullptr)
       {
         // ------------------MACRO_SR_PRED_INTRO
         // toExplain.d_node
         std::vector<Node> children;
         std::vector<Node> args;
         args.push_back(toExplain.d_node);
-        lcp->addStep(toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args);
+        lcp->addStep(
+            toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args);
       }
       continue;
     }
@@ -2076,7 +2077,7 @@ theory::TrustNode TheoryEngine::getExplanation(
             toExplain.d_node[k], toExplain.d_theory, toExplain.d_timestamp);
         explanationVector.push_back(newExplain);
       }
-      if (lcp!=nullptr)
+      if (lcp != nullptr)
       {
         // toExplain.d_node[0] ... toExplain.d_node[n]
         // --------------------------------------------MACRO_BSR_PRED_INTRO
@@ -2088,7 +2089,8 @@ theory::TrustNode TheoryEngine::getExplanation(
         }
         std::vector<Node> args;
         args.push_back(toExplain.d_node);
-        lcp->addStep(toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args);
+        lcp->addStep(
+            toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args);
       }
       ++ i;
       continue;
@@ -2146,20 +2148,21 @@ theory::TrustNode TheoryEngine::getExplanation(
           << theoryOf(toExplain.d_theory)->getId()
           << ". Explanation: " << texplanation.getNode() << std::endl;
     }
-    if (lcp!=nullptr)
+    if (lcp != nullptr)
     {
       // ----------- Via theory
       // exp => lit                exp
       // ---------------------------------MACRO_BSR_PRED_TRANSFORM
       // lit
       Node proven = texplanation.getProven();
-      lcp->addLazyStep(proven,texplanation.getGenerator());
+      lcp->addLazyStep(proven, texplanation.getGenerator());
       std::vector<Node> children;
       children.push_back(proven);
       children.push_back(texplanation.getNode());
       std::vector<Node> args;
       args.push_back(toExplain.d_node);
-      lcp->addStep(toExplain.d_node,PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
+      lcp->addStep(
+          toExplain.d_node, PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
     }
     Node explanation = texplanation.getNode();
 
@@ -2229,22 +2232,23 @@ theory::TrustNode TheoryEngine::getExplanation(
     });
 
   Node exp = mkExplanation(explanationVector);
-  
-  if (lcp!=nullptr)
+
+  if (lcp != nullptr)
   {
-    Assert (lcp!=nullptr);
+    Assert(lcp != nullptr);
     // FIXME
     // get the proof for conclusion
     std::shared_ptr<ProofNode> pfConc = lcp->mkProof(conclusion);
     std::vector<Node> scopeAssumps;
-    for (size_t k = 0, esize = explanationVector.size(); k < esize; ++ k) 
+    for (size_t k = 0, esize = explanationVector.size(); k < esize; ++k)
     {
       scopeAssumps.push_back(explanationVector[k].d_node);
     }
     // call the scope method of proof node manager
-    std::shared_ptr<ProofNode> pf = d_pNodeManager->mkScope(pfConc, scopeAssumps);
+    std::shared_ptr<ProofNode> pf =
+        d_pNodeManager->mkScope(pfConc, scopeAssumps);
   }
-  
+
   return theory::TrustNode::mkTrustLemma(exp, nullptr);
 }