Format

17 files changed, 78 insertions, 73 deletions

diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp
index b0ddbc251..afd152da8 100644
--- a/src/expr/lazy_proof.cpp
+++ b/src/expr/lazy_proof.cpp
@@ -18,7 +18,9 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 
-LazyCDProof::LazyCDProof(ProofNodeManager* pnm, ProofGenerator * dpg, context::Context* c)
+LazyCDProof::LazyCDProof(ProofNodeManager* pnm,
+                         ProofGenerator* dpg,
+                         context::Context* c)
     : CDProof(pnm, c), d_gens(c ? c : &d_context), d_defaultGen(dpg)
 {
 }
@@ -145,7 +147,7 @@ ProofGenerator* LazyCDProof::getGeneratorFor(Node fact, bool& isSym)
 
 bool LazyCDProof::hasGenerators() const
 {
-  return d_gens.empty() && d_defaultGen==nullptr;
+  return d_gens.empty() && d_defaultGen == nullptr;
 }
 
 }  // namespace CVC4
diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h
index f9a99b816..1a0e6adf8 100644
--- a/src/expr/lazy_proof.h
+++ b/src/expr/lazy_proof.h
@@ -32,7 +32,9 @@ namespace CVC4 {
 class LazyCDProof : public CDProof
 {
  public:
-  LazyCDProof(ProofNodeManager* pnm, ProofGenerator * dpg = nullptr, context::Context* c = nullptr);
+  LazyCDProof(ProofNodeManager* pnm,
+              ProofGenerator* dpg = nullptr,
+              context::Context* c = nullptr);
   ~LazyCDProof();
   /**
    * Get lazy proof for fact, or nullptr if it does not exist. This may
@@ -50,6 +52,7 @@ class LazyCDProof : public CDProof
                    bool forceOverwrite = false);
   /** Does this have any proof generators? */
   bool hasGenerators() const;
+
  protected:
   typedef context::CDHashMap<Node, ProofGenerator*, NodeHashFunction>
       NodeProofGeneratorMap;
diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp
index e35b72bda..d1fbbb071 100644
--- a/src/expr/proof.cpp
+++ b/src/expr/proof.cpp
@@ -119,7 +119,7 @@ bool CDProof::addStep(Node expected,
     // These rules are implicitly managed by this class. The user of this
     // class should not have to bother with them.
     // FIXME: return or assert here; this currently breaks slow-2020-04-17
-    //return true;
+    // return true;
   }
   // We must always provide expected to this method
   Assert(!expected.isNull());
@@ -148,8 +148,8 @@ bool CDProof::addStep(Node expected,
       if (ensureChildren)
       {
         // failed to get a proof for a child, fail
-        //Trace("cdproof") << "...fail, no child" << std::endl;
-        //FIXME: probably remove this 
+        // Trace("cdproof") << "...fail, no child" << std::endl;
+        // FIXME: probably remove this
         return false;
       }
       Trace("cdproof") << "--- add assume" << std::endl;
@@ -208,8 +208,7 @@ bool CDProof::addStep(Node expected,
   if (expected.getKind() == EQUAL && expected[0] != expected[1])
   {
     Node expectedSym = expected[1].eqNode(expected[0]);
-    Trace("cdproof") << "  check update symmetry "
-                     << expectedSym << std::endl;
+    Trace("cdproof") << "  check update symmetry " << expectedSym << std::endl;
     // if it exists, we may need to update it
     std::shared_ptr<ProofNode> pfs = getProof(expectedSym);
     if (pfs != nullptr)
diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp
index 1a889d257..64bebcfe4 100644
--- a/src/expr/proof_generator.cpp
+++ b/src/expr/proof_generator.cpp
@@ -53,10 +53,9 @@ bool ProofGenerator::addProofTo(Node f, CDProof* pf, bool forceOverwrite)
   return false;
 }
 
+PRefProofGenerator::PRefProofGenerator(CDProof* cd) : d_proof(cd) {}
 
-PRefProofGenerator::PRefProofGenerator(CDProof * cd) : d_proof(cd){}
-
-PRefProofGenerator::~PRefProofGenerator(){}
+PRefProofGenerator::~PRefProofGenerator() {}
 
 std::shared_ptr<ProofNode> PRefProofGenerator::getProofFor(Node f)
 {
diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h
index 8180e0fe3..88a989e87 100644
--- a/src/expr/proof_generator.h
+++ b/src/expr/proof_generator.h
@@ -69,20 +69,20 @@ class ProofGenerator
   virtual std::string identify() const = 0;
 };
 
-
 class CDProof;
 
 /** A "copy on demand" proof generator */
 class PRefProofGenerator : public ProofGenerator
 {
-public:
-  PRefProofGenerator(CDProof * cd);
+ public:
+  PRefProofGenerator(CDProof* cd);
   ~PRefProofGenerator();
   /** Get proof for */
   std::shared_ptr<ProofNode> getProofFor(Node f) override;
-protected:
+
+ protected:
   /** The reference proof */
-  CDProof * d_proof;
+  CDProof* d_proof;
 };
 
 }  // namespace CVC4
diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index 360c6f673..4dc98470b 100644
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -110,9 +110,9 @@ bool ProofNodeManager::updateNode(
     return false;
   }
   // paranoia about ref counting
-  //const std::vector<std::shared_ptr<ProofNode>>& prevc = pn->getChildren();
-  //std::vector<std::shared_ptr<ProofNode>> copy;
-  //copy.insert(copy.end(),prevc.begin(),prevc.end());
+  // const std::vector<std::shared_ptr<ProofNode>>& prevc = pn->getChildren();
+  // std::vector<std::shared_ptr<ProofNode>> copy;
+  // copy.insert(copy.end(),prevc.begin(),prevc.end());
 
   // we update its value
   pn->setValue(id, children, args);
diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/expr/proof_node_to_sexpr.cpp
index 3533a98f2..cf58daa3a 100644
--- a/src/expr/proof_node_to_sexpr.cpp
+++ b/src/expr/proof_node_to_sexpr.cpp
@@ -49,7 +49,8 @@ Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn)
       const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren();
       for (const std::shared_ptr<ProofNode>& cp : pc)
       {
-        if (std::find(constructing.begin(), constructing.end(), cp.get()) != constructing.end())
+        if (std::find(constructing.begin(), constructing.end(), cp.get())
+            != constructing.end())
         {
           AlwaysAssert(false)
               << "ProofNodeToSExpr::convertToSExpr: cyclic proof!" << std::endl;
@@ -60,7 +61,7 @@ Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn)
     }
     else if (it->second.isNull())
     {
-      Assert (!constructing.empty());
+      Assert(!constructing.empty());
       constructing.pop_back();
       std::vector<Node> children;
       // add proof rule
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index e74004385..ba9c50fa5 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -139,8 +139,7 @@ bool BuiltinProofRuleChecker::getRewriterId(TNode n, RewriterId& i)
 
 Node BuiltinProofRuleChecker::mkRewriterId(RewriterId i)
 {
-  return NodeManager::currentNM()->mkConst(
-          Rational(static_cast<uint32_t>(i)));
+  return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(i)));
 }
 
 Node BuiltinProofRuleChecker::checkInternal(PfRule id,
diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h
index dd1c1f3c5..42dcf631e 100644
--- a/src/theory/builtin/proof_checker.h
+++ b/src/theory/builtin/proof_checker.h
@@ -92,6 +92,7 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
   static bool getRewriterId(TNode n, RewriterId& i);
   /** Make a rewriter id node */
   static Node mkRewriterId(RewriterId i);
+
  protected:
   /** Return the conclusion of the given proof step, or null if it is invalid */
   Node checkInternal(PfRule id,
diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp
index cb0ddf2cc..2c0994390 100644
--- a/src/theory/eager_proof_generator.cpp
+++ b/src/theory/eager_proof_generator.cpp
@@ -93,7 +93,7 @@ TrustNode EagerProofGenerator::assertSplit(Node f)
   // make the lemma
   Node lem = f.orNode(f.notNode());
   std::vector<Node> args;
-  return mkTrustNode(lem, PfRule::SPLIT,args,false);
+  return mkTrustNode(lem, PfRule::SPLIT, args, false);
 }
 
 }  // namespace theory
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 7af9dbbc7..00c1482b2 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -40,7 +40,8 @@ InferProofCons::InferProofCons(context::Context* c,
 
 void InferProofCons::notifyFact(const InferInfo& ii)
 {
-  Trace("strings-ipc-debug") << "InferProofCons::notifyFact: " << ii << std::endl;
+  Trace("strings-ipc-debug")
+      << "InferProofCons::notifyFact: " << ii << std::endl;
   std::shared_ptr<InferInfo> iic = std::make_shared<InferInfo>(ii);
   d_lazyFactMap.insert(ii.d_conc, iic);
 }
@@ -138,7 +139,8 @@ Node InferProofCons::convert(Inference infer,
     case Inference::INFER_EMP:
     {
       // need the "extended equality rewrite"
-      ps.d_args.push_back(builtin::BuiltinProofRuleChecker::mkRewriterId(RewriterId::REWRITE_EQ_EXT));
+      ps.d_args.push_back(builtin::BuiltinProofRuleChecker::mkRewriterId(
+          RewriterId::REWRITE_EQ_EXT));
       ps.d_rule = PfRule::MACRO_SR_PRED_ELIM;
     }
     break;
@@ -268,7 +270,8 @@ 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, RewriterId::REWRITE_EQ_EXT))
+          if (convertPredTransform(
+                  mainEqCeq, conc, cexp, RewriterId::REWRITE_EQ_EXT))
           {
             // success
             useBuffer = true;
@@ -569,14 +572,15 @@ bool InferProofCons::convertLengthPf(Node lenReq,
     }
     // x != "" => len(x) != 0
     // FIXME
-    // MODUS_PONENS( P, SCOPE( MACRO_SR_PRED_INTRO( ASSUME(x="") :args len(x)=0) :args x = "") )
+    // MODUS_PONENS( P, SCOPE( MACRO_SR_PRED_INTRO( ASSUME(x="") :args len(x)=0)
+    // :args x = "") )
   }
   return false;
 }
 
 bool InferProofCons::convertPredTransform(Node src,
                                           Node tgt,
-                                          const std::vector<Node>& exp, 
+                                          const std::vector<Node>& exp,
                                           RewriterId id)
 {
   if (src == tgt)
@@ -591,7 +595,7 @@ bool InferProofCons::convertPredTransform(Node src,
   children.insert(children.end(), exp.begin(), exp.end());
   std::vector<Node> args;
   args.push_back(tgt);
-  if (id!=RewriterId::REWRITE)
+  if (id != RewriterId::REWRITE)
   {
     args.push_back(builtin::BuiltinProofRuleChecker::mkRewriterId(id));
   }
@@ -639,7 +643,7 @@ std::shared_ptr<ProofNode> InferProofCons::getProofFor(Node fact)
 bool InferProofCons::addProofTo(Node fact, CDProof* pf, bool forceOverwrite)
 {
   // we copy fresh proofs
-  return ProofGenerator::addProofTo(fact,pf,forceOverwrite);
+  return ProofGenerator::addProofTo(fact, pf, forceOverwrite);
   // get the inference
   NodeInferInfoMap::iterator it = d_lazyFactMap.find(fact);
   AlwaysAssert(it != d_lazyFactMap.end());
diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h
index 9f7d9199a..9ea8e847d 100644
--- a/src/theory/strings/infer_proof_cons.h
+++ b/src/theory/strings/infer_proof_cons.h
@@ -23,10 +23,10 @@
 #include "expr/proof_checker.h"
 #include "expr/proof_rule.h"
 #include "expr/proof_step_buffer.h"
+#include "theory/builtin/proof_checker.h"
 #include "theory/strings/infer_info.h"
 #include "theory/strings/sequences_stats.h"
 #include "theory/uf/proof_equality_engine.h"
-#include "theory/builtin/proof_checker.h"
 
 namespace CVC4 {
 namespace theory {
@@ -50,15 +50,15 @@ class InferProofCons : public ProofGenerator
                  SequencesStatistics& statistics,
                  bool pfEnabled);
   ~InferProofCons() {}
-  /** 
+  /**
    * This is called to notify that ii is an inference that may need a proof
-   * in the future. 
-   * 
+   * in the future.
+   *
    * In detail, this class should be prepared to respond to a call to:
    *   addProofTo(ii.d_conc, ...)
    * in the remainder of the SAT context. This method copies ii and stores it
    * in the context-dependent map d_lazyFactMap below.
-   * 
+   *
    * This is used for lazy proof construction, where proofs are constructed
    * only for facts that are explained.
    */
@@ -123,7 +123,10 @@ class InferProofCons : public ProofGenerator
    * it may attempt to apply MACRO_SR_PRED_TRANSFORM. This method should be
    * applied when src and tgt are equivalent formulas assuming exp.
    */
-  bool convertPredTransform(Node src, Node tgt, const std::vector<Node>& exp, RewriterId id = RewriterId::REWRITE);
+  bool convertPredTransform(Node src,
+                            Node tgt,
+                            const std::vector<Node>& exp,
+                            RewriterId id = RewriterId::REWRITE);
   /** the proof node manager */
   ProofNodeManager* d_pnm;
   /** The lazy fact map */
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index e14a3a4a8..542e113a1 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -396,7 +396,7 @@ void InferenceManager::doPendingLemmas()
     // set up proof step based on inference
     // pfExp is the children of the proof step below. This should be an
     // ordered list of expConj + expn.
-    
+
     // set up the explanation and no-explanation
     TrustNode tlem;
     std::vector<Node> exp;
@@ -409,8 +409,7 @@ void InferenceManager::doPendingLemmas()
     {
       // if we aren't regressing the explanation, we add all literals to
       // noExplain and ignore ii.d_antn.
-      noExplain.insert(
-          noExplain.end(), exp.begin(), exp.end());
+      noExplain.insert(noExplain.end(), exp.begin(), exp.end());
     }
     else
     {
@@ -434,13 +433,11 @@ void InferenceManager::doPendingLemmas()
       Node conc = d_ipc->convert(ii, ps, useBuffer);
       if (useBuffer)
       {
-        tlem = d_pfee->assertLemma(
-            conc, exp, noExplain, *d_ipc->getBuffer());
+        tlem = d_pfee->assertLemma(conc, exp, noExplain, *d_ipc->getBuffer());
       }
       else
       {
-        tlem = d_pfee->assertLemma(
-            conc, ps.d_rule, exp, noExplain, ps.d_args);
+        tlem = d_pfee->assertLemma(conc, ps.d_rule, exp, noExplain, ps.d_args);
       }
     }
     Node lem = tlem.getNode();
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 93e6b78a8..595652994 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -251,7 +251,8 @@ TheoryEngine::TheoryEngine(context::Context* context,
   if (options::proofNew())
   {
     // no default generator
-    d_lazyProof.reset(new LazyCDProof(d_pNodeManager.get(), nullptr, d_userContext));
+    d_lazyProof.reset(
+        new LazyCDProof(d_pNodeManager.get(), nullptr, d_userContext));
   }
 #endif
 
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 830d62de2..6e487c90d 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1958,11 +1958,8 @@ unsigned EqualityEngine::getFreshMergeReasonType() {
   return d_freshMergeReasonType++;
 }
 
-std::string EqualityEngine::identify() const
-{
-  return d_name;
-}
-  
+std::string EqualityEngine::identify() const { return d_name; }
+
 void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
 {
   Debug("equality::trigger") << d_name << "::eq::addTriggerTerm(" << t << ", " << tag << ")" << std::endl;
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index 6d16fa28b..1ddc6e006 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -109,7 +109,7 @@ bool ProofEqEngine::assertFact(Node lit,
   Trace("pfee") << "pfee::assertFact " << lit << " " << id << ", exp = " << exp
                 << ", args = " << args << std::endl;
   // shouldnt use this interface if not doing recursive explanations?
-  Assert (d_recExplain);
+  Assert(d_recExplain);
   // first, register the step in the proof
   if (d_pfEnabled)
   {
@@ -136,7 +136,7 @@ bool ProofEqEngine::assertFact(Node lit, Node exp, ProofStepBuffer& psb)
                 << " via buffer with " << psb.getNumSteps() << " steps"
                 << std::endl;
   // shouldnt use this interface if not doing recursive explanations?
-  Assert (d_recExplain);
+  Assert(d_recExplain);
   if (d_pfEnabled)
   {
     if (!d_proof.addSteps(psb))
@@ -235,8 +235,8 @@ TrustNode ProofEqEngine::assertLemma(Node conc,
   {
     PRefProofGenerator prg(&d_proof);
     LazyCDProof tmpProof(d_pnm, &prg);
-    CDProof * curr;
-    if (conc==d_false || true)
+    CDProof* curr;
+    if (conc == d_false || true)
     {
       curr = &d_proof;
     }
@@ -268,8 +268,8 @@ TrustNode ProofEqEngine::assertLemma(Node conc,
   {
     PRefProofGenerator prg(&d_proof);
     LazyCDProof tmpProof(d_pnm, &prg);
-    CDProof * curr;
-    if (conc==d_false || true)
+    CDProof* curr;
+    if (conc == d_false || true)
     {
       curr = &d_proof;
     }
@@ -292,19 +292,19 @@ TrustNode ProofEqEngine::assertLemma(Node conc,
 }
 
 TrustNode ProofEqEngine::assertLemma(Node conc,
-                      const std::vector<Node>& exp,
-                      const std::vector<Node>& noExplain,
-                      ProofGenerator* pg)
+                                     const std::vector<Node>& exp,
+                                     const std::vector<Node>& noExplain,
+                                     ProofGenerator* pg)
 {
-
   Trace("pfee") << "pfee::assertLemma " << conc << ", exp = " << exp
-                << ", noExplain = " << noExplain << " via buffer with generator" << std::endl;
+                << ", noExplain = " << noExplain << " via buffer with generator"
+                << std::endl;
   if (d_pfEnabled)
   {
     PRefProofGenerator prg(&d_proof);
     LazyCDProof tmpProof(d_pnm, &prg);
-    CDProof * curr;
-    if (conc==d_false || true)
+    CDProof* curr;
+    if (conc == d_false || true)
     {
       curr = &d_proof;
     }
@@ -333,7 +333,7 @@ std::string ProofEqEngine::identify() const
 TrustNode ProofEqEngine::assertLemmaInternal(Node conc,
                                              const std::vector<Node>& exp,
                                              const std::vector<Node>& noExplain,
-                                CDProof * curr)
+                                             CDProof* curr)
 {
   // We are a conflict if the conclusion is false and all literals are
   // explained.
@@ -362,7 +362,7 @@ TrustNode ProofEqEngine::assertLemmaInternal(Node conc,
 TrustNode ProofEqEngine::ensureProofForFact(Node conc,
                                             const std::vector<TNode>& assumps,
                                             bool isConflict,
-                                CDProof * curr)
+                                            CDProof* curr)
 {
   Trace("pfee-proof") << std::endl;
   Trace("pfee-proof") << "pfee::ensureProofForFact: input " << conc << " via "
@@ -378,7 +378,7 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc,
   // if proofs are enabled, generate the proof and clean the assumptions
   if (d_pfEnabled)
   {
-    Assert (curr!=nullptr);
+    Assert(curr != nullptr);
     Trace("pfee-proof") << "pfee::ensureProofForFact: make proof for fact"
                         << std::endl;
     // get the proof for conc
@@ -558,8 +558,9 @@ bool ProofEqEngine::addProofStep(Node lit,
   return true;
 }
 
-void ProofEqEngine::explainWithProof(Node lit, std::vector<TNode>& assumps,
-                                CDProof * curr)
+void ProofEqEngine::explainWithProof(Node lit,
+                                     std::vector<TNode>& assumps,
+                                     CDProof* curr)
 {
   if (std::find(assumps.begin(), assumps.end(), lit) != assumps.end())
   {
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index fd9d9ec24..ea66e5ae0 100644
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -167,13 +167,12 @@ class ProofEqEngine : public EagerProofGenerator
   TrustNode assertLemmaInternal(Node conc,
                                 const std::vector<Node>& exp,
                                 const std::vector<Node>& noExplain,
-                                CDProof * curr
-                               );
+                                CDProof* curr);
   /** ensure proof for fact */
   TrustNode ensureProofForFact(Node conc,
                                const std::vector<TNode>& assumps,
                                bool isConflict,
-                                CDProof * curr);
+                               CDProof* curr);
   /**
    * Make the conjunction of nodes in a. Returns true if a is empty, and a
    * single literal if a has size 1.
@@ -218,8 +217,7 @@ class ProofEqEngine : public EagerProofGenerator
    * This additionally registers the equality proof steps required to
    * regress the explanation of lit.
    */
-  void explainWithProof(Node lit, std::vector<TNode>& assumps,
-                                CDProof * curr);
+  void explainWithProof(Node lit, std::vector<TNode>& assumps, CDProof* curr);
 };
 
 }  // namespace eq