Format

9 files changed, 74 insertions, 58 deletions

diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp
index dda2ccd2d..15e996684 100644
--- a/src/expr/proof.cpp
+++ b/src/expr/proof.cpp
@@ -384,8 +384,8 @@ bool CDProof::isAssumption(ProofNode* pn)
 bool CDProof::isSame(TNode f, TNode g)
 {
   return f == g
-         || (f.getKind() == EQUAL && g.getKind() == EQUAL
-             && f[0] == g[1] && f[1] == g[0]);
+         || (f.getKind() == EQUAL && g.getKind() == EQUAL && f[0] == g[1]
+             && f[1] == g[0]);
 }
 
 }  // namespace CVC4
diff --git a/src/expr/proof.h b/src/expr/proof.h
index 20bbb4996..2ff3604f8 100644
--- a/src/expr/proof.h
+++ b/src/expr/proof.h
@@ -206,12 +206,13 @@ class CDProof
   /** Get the proof manager for this proof */
   ProofNodeManager* getManager() const;
 
-  /** 
+  /**
    * Is same? Returns true if f and g are the same formula, or if they are
    * symmetric equalities. If two nodes f and g are the same, then a proof for
    * f suffices as a proof for g according to this class.
    */
   static bool isSame(TNode f, TNode g);
+
  protected:
   typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>, NodeHashFunction>
       NodeProofNodeMap;
diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp
index b473ffc56..9e4e56543 100644
--- a/src/theory/engine_output_channel.cpp
+++ b/src/theory/engine_output_channel.cpp
@@ -308,9 +308,9 @@ void EngineOutputChannel::trustedConflict(TrustNode pconf)
 }
 
 LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem,
-                                                   bool removable,
-                                                   bool preprocess,
-                                                   bool sendAtoms)
+                                              bool removable,
+                                              bool preprocess,
+                                              bool sendAtoms)
 {
   Assert(plem.getKind() == TrustNodeKind::LEMMA);
   d_engine->processTrustNode(plem, d_theory);
diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h
index 1be4ec1d3..2d07d3f63 100644
--- a/src/theory/engine_output_channel.h
+++ b/src/theory/engine_output_channel.h
@@ -31,7 +31,7 @@ namespace theory {
 /**
  * An output channel for Theory that passes messages back to a TheoryEngine
  * for a given Theory.
- * 
+ *
  * Notice that is has interfaces trustedConflict and trustedLemma which are
  * used for ensuring that proof generators are associated with the lemmas
  * and conflicts sent on this output channel.
@@ -87,6 +87,7 @@ class EngineOutputChannel : public theory::OutputChannel
                            bool removable = false,
                            bool preprocess = false,
                            bool sendAtoms = false) override;
+
  protected:
   /**
    * Statistics for a particular theory.
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index 16afb0817..43950383b 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -27,7 +27,7 @@ SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine,
                                          context::Context* context,
                                          context::UserContext* userContext,
                                          ProofNodeManager* pnm,
-                      bool pfEnabled)
+                                         bool pfEnabled)
     : ContextNotifyObj(context),
       d_statSharedTerms("theory::shared_terms", 0),
       d_addedSharedTermsSize(context, 0),
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index ce9ac3da7..982931d4a 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -48,11 +48,11 @@
 #include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
+#include "theory/theory_engine_proof_generator.h"
 #include "theory/theory_model.h"
 #include "theory/theory_traits.h"
 #include "theory/uf/equality_engine.h"
 #include "util/resource_manager.h"
-#include "theory/theory_engine_proof_generator.h"
 
 using namespace std;
 
@@ -202,9 +202,13 @@ TheoryEngine::TheoryEngine(context::Context* context,
           options::proofNew()
               ? new LazyCDProof(d_pNodeManager.get(), nullptr, d_userContext)
               : nullptr),
-      d_tepg(new TheoryEngineProofGenerator(d_pNodeManager.get(), d_userContext)),
-      d_sharedTerms(
-          this, context, userContext, d_pNodeManager.get(), d_lazyProof!=nullptr),
+      d_tepg(
+          new TheoryEngineProofGenerator(d_pNodeManager.get(), d_userContext)),
+      d_sharedTerms(this,
+                    context,
+                    userContext,
+                    d_pNodeManager.get(),
+                    d_lazyProof != nullptr),
       d_masterEqualityEngine(nullptr),
       d_masterEENotify(*this),
       d_quantEngine(nullptr),
@@ -1797,10 +1801,11 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   std::shared_ptr<LazyCDProof> lcp;
   if (d_lazyProof != nullptr)
   {
-    Trace("te-proof-exp") << "TheoryEngine::lemma: process " << node << std::endl;
+    Trace("te-proof-exp") << "TheoryEngine::lemma: process " << node
+                          << std::endl;
     lcp.reset(new LazyCDProof(d_pNodeManager.get()));
   }
-  
+
   AssertionPipeline additionalLemmas;
 
   // Run theory preprocessing, maybe
@@ -1856,7 +1861,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
 }
 
 void TheoryEngine::processTrustNode(theory::TrustNode trn,
-                            theory::TheoryId from)
+                                    theory::TheoryId from)
 {
   if (d_lazyProof == nullptr)
   {
@@ -1876,7 +1881,7 @@ void TheoryEngine::processTrustNode(theory::TrustNode trn,
   else
   {
     // all BUILTIN should be handled
-    Assert (from!=THEORY_BUILTIN);
+    Assert(from != THEORY_BUILTIN);
     // untrusted theory lemma
     std::vector<Node> children;
     std::vector<Node> args;
@@ -1936,11 +1941,9 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
     PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe));
 
     // FIXME: have ~( F ) and E => F, prove ~( E )
-    if (d_lazyProof!=nullptr)
+    if (d_lazyProof != nullptr)
     {
-      
     }
-    
 
     Node fullConflict = tnc.getNode();
     Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl;
@@ -2040,7 +2043,8 @@ theory::TrustNode TheoryEngine::getExplanation(
   TrustNode simpleTrn;
   if (d_lazyProof != nullptr)
   {
-    Trace("te-proof-exp") << "TheoryEngine::getExplanation " << conclusion << std::endl;
+    Trace("te-proof-exp") << "TheoryEngine::getExplanation " << conclusion
+                          << std::endl;
     lcp.reset(new LazyCDProof(d_pNodeManager.get()));
   }
   unsigned i = 0; // Index of the current literal we are processing
@@ -2073,7 +2077,8 @@ theory::TrustNode TheoryEngine::getExplanation(
       ++ i;
       if (lcp != nullptr)
       {
-        Trace("te-proof-exp") << "- explain " << toExplain.d_node << " trivially..." << std::endl;
+        Trace("te-proof-exp")
+            << "- explain " << toExplain.d_node << " trivially..." << std::endl;
         // ------------------MACRO_SR_PRED_INTRO
         // toExplain.d_node
         std::vector<Node> children;
@@ -2111,7 +2116,8 @@ theory::TrustNode TheoryEngine::getExplanation(
       }
       if (lcp != nullptr)
       {
-        Trace("te-proof-exp") << "- AND expand " << toExplain.d_node << std::endl;
+        Trace("te-proof-exp")
+            << "- AND expand " << toExplain.d_node << std::endl;
         // toExplain.d_node[0] ... toExplain.d_node[n]
         // --------------------------------------------MACRO_SR_PRED_INTRO
         // toExplain.d_node
@@ -2161,11 +2167,13 @@ theory::TrustNode TheoryEngine::getExplanation(
             }
           }
         })
-        if (lcp !=nullptr)
+        if (lcp != nullptr)
         {
-          if (!CDProof::isSame(toExplain.d_node,(*find).second.d_node))
+          if (!CDProof::isSame(toExplain.d_node, (*find).second.d_node))
           {
-            Trace("te-proof-exp") << "- t-explained cached: " << toExplain.d_node << " by " << (*find).second.d_node << std::endl;
+            Trace("te-proof-exp")
+                << "- t-explained cached: " << toExplain.d_node << " by "
+                << (*find).second.d_node << std::endl;
             // does this ever happen?
             Assert(false);
             simpleExplain = false;
@@ -2194,7 +2202,9 @@ theory::TrustNode TheoryEngine::getExplanation(
     }
     if (lcp != nullptr)
     {
-      Trace("te-proof-exp") << "- t-explained[" << toExplain.d_theory << "]: " << toExplain.d_node << " by " << texplanation.getNode() << std::endl;
+      Trace("te-proof-exp")
+          << "- t-explained[" << toExplain.d_theory << "]: " << toExplain.d_node
+          << " by " << texplanation.getNode() << std::endl;
       // if not a trivial explanation
       if (!CDProof::isSame(texplanation.getNode(), toExplain.d_node))
       {
@@ -2203,7 +2213,7 @@ theory::TrustNode TheoryEngine::getExplanation(
         // ---------------------------------MACRO_SR_PRED_TRANSFORM
         // lit
         Node proven = texplanation.getProven();
-        if (texplanation.getGenerator()!=nullptr)
+        if (texplanation.getGenerator() != nullptr)
         {
           lcp->addLazyStep(proven, texplanation.getGenerator());
         }
@@ -2217,7 +2227,7 @@ theory::TrustNode TheoryEngine::getExplanation(
           unsigned tid = static_cast<unsigned>(toExplain.d_theory);
           Node tidn = NodeManager::currentNM()->mkConst(Rational(tid));
           args.push_back(tidn);
-          lcp->addStep(proven,PfRule::THEORY_LEMMA,children,args);
+          lcp->addStep(proven, PfRule::THEORY_LEMMA, children, args);
         }
         std::vector<Node> children;
         children.push_back(proven);
@@ -2320,12 +2330,12 @@ theory::TrustNode TheoryEngine::getExplanation(
     {
       // single call to a theory's explain method, skip the proof generator
       Assert (!simpleTrn.isNull());
-      Trace("te-proof-exp") << "...simple explain " << simpleTrn.getNode() << std::endl;
-      return simpleTrn;
+      Trace("te-proof-exp") << "...simple explain " << simpleTrn.getNode() <<
+    std::endl; return simpleTrn;
     }
     */
     // store in the proof generator
-    TrustNode trn = d_tepg->mkTrustExplain(conclusion,exp,lcp);
+    TrustNode trn = d_tepg->mkTrustExplain(conclusion, exp, lcp);
     // return the trust node
     return trn;
   }
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index be5206461..a5b9c393f 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -37,6 +37,7 @@
 #include "smt/command.h"
 #include "theory/atom_requests.h"
 #include "theory/decision_manager.h"
+#include "theory/engine_output_channel.h"
 #include "theory/interrupted.h"
 #include "theory/rewriter.h"
 #include "theory/shared_terms_database.h"
@@ -44,7 +45,6 @@
 #include "theory/substitutions.h"
 #include "theory/term_registration_visitor.h"
 #include "theory/theory.h"
-#include "theory/engine_output_channel.h"
 #include "theory/trust_node.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/valuation.h"
@@ -362,19 +362,18 @@ class TheoryEngine {
                             bool preprocess,
                             theory::TheoryId atomsTo);
 
-  /** 
+  /**
    * Process trust node. This method ensures that the proof for the proven node
    * of trn is stored as a lazy step in the lazy proof (d_lazyProof) maintained
    * by this class, referencing the proof generator of the trust node. The
    * argument from specifies the theory responsible for this trust node. If
    * no generator is provided, then a (eager) THEORY_LEMMA step is added to
    * the lazy proof.
-   * 
+   *
    * @param trn The trust node to process
    * @param from The id of the theory responsible for the trust node.
    */
-  void processTrustNode(theory::TrustNode trn,
-                            theory::TheoryId from);
+  void processTrustNode(theory::TrustNode trn, theory::TheoryId from);
 
   /** Enusre that the given atoms are send to the given theory */
   void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);
@@ -417,8 +416,7 @@ class TheoryEngine {
   inline void addTheory(theory::TheoryId theoryId)
   {
     Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL);
-    d_theoryOut[theoryId] =
-        new theory::EngineOutputChannel(this, theoryId);
+    d_theoryOut[theoryId] = new theory::EngineOutputChannel(this, theoryId);
     d_theoryTable[theoryId] = new TheoryClass(d_context,
                                               d_userContext,
                                               *d_theoryOut[theoryId],
diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp
index af737e53b..144fe0cc2 100644
--- a/src/theory/theory_engine_proof_generator.cpp
+++ b/src/theory/theory_engine_proof_generator.cpp
@@ -16,21 +16,22 @@
 
 using namespace CVC4::kind;
 
-namespace CVC4 
-{
+namespace CVC4 {
 
-TheoryEngineProofGenerator::TheoryEngineProofGenerator(ProofNodeManager* pnm, context::UserContext* u) : d_pnm(pnm), d_proofs(u)
+TheoryEngineProofGenerator::TheoryEngineProofGenerator(ProofNodeManager* pnm,
+                                                       context::UserContext* u)
+    : d_pnm(pnm), d_proofs(u)
 {
-  
 }
 
-theory::TrustNode TheoryEngineProofGenerator::mkTrustExplain(TNode lit, Node exp, std::shared_ptr<LazyCDProof> lpf)
+theory::TrustNode TheoryEngineProofGenerator::mkTrustExplain(
+    TNode lit, Node exp, std::shared_ptr<LazyCDProof> lpf)
 {
-  theory::TrustNode trn = theory::TrustNode::mkTrustPropExp(lit,exp,this);
+  theory::TrustNode trn = theory::TrustNode::mkTrustPropExp(lit, exp, this);
   Node p = trn.getProven();
   // should not already be proven
   NodeLazyCDProofMap::iterator it = d_proofs.find(p);
-  if (it!=d_proofs.end())
+  if (it != d_proofs.end())
   {
     Assert(false);
   }
@@ -44,16 +45,16 @@ theory::TrustNode TheoryEngineProofGenerator::mkTrustExplain(TNode lit, Node exp
 
 std::shared_ptr<ProofNode> TheoryEngineProofGenerator::getProofFor(Node f)
 {
-  Assert (f.getKind()==IMPLIES && f.getNumChildren()==2);
+  Assert(f.getKind() == IMPLIES && f.getNumChildren() == 2);
   NodeLazyCDProofMap::iterator it = d_proofs.find(f);
-  if (it==d_proofs.end())
+  if (it == d_proofs.end())
   {
     return nullptr;
   }
   std::shared_ptr<LazyCDProof> lcp = (*it).second;
   // finalize it via scope
   std::vector<Node> scopeAssumps;
-  if (f[0].getKind()==AND)
+  if (f[0].getKind() == AND)
   {
     for (const Node& fc : f[0])
     {
@@ -78,4 +79,4 @@ std::string TheoryEngineProofGenerator::identify() const
   return "TheoryEngineProofGenerator";
 }
 
-}
+}  // namespace CVC4
diff --git a/src/theory/theory_engine_proof_generator.h b/src/theory/theory_engine_proof_generator.h
index 0dd6e0dd8..c81a2c09b 100644
--- a/src/theory/theory_engine_proof_generator.h
+++ b/src/theory/theory_engine_proof_generator.h
@@ -19,35 +19,40 @@
 
 #include <memory>
 
-#include "expr/lazy_proof.h"
-#include "expr/proof_node_manager.h"
-#include "expr/proof_generator.h"
 #include "context/cdhashmap.h"
 #include "context/context.h"
+#include "expr/lazy_proof.h"
+#include "expr/proof_generator.h"
+#include "expr/proof_node_manager.h"
 #include "theory/trust_node.h"
 
 namespace CVC4 {
 
 class TheoryEngineProofGenerator : public ProofGenerator
 {
-  typedef context::CDHashMap<Node, std::shared_ptr<LazyCDProof>, NodeHashFunction>
-      NodeLazyCDProofMap;
+  typedef context::
+      CDHashMap<Node, std::shared_ptr<LazyCDProof>, NodeHashFunction>
+          NodeLazyCDProofMap;
+
  public:
   TheoryEngineProofGenerator(ProofNodeManager* pnm, context::UserContext* u);
-  ~TheoryEngineProofGenerator(){}
+  ~TheoryEngineProofGenerator() {}
   /** Set proof */
-  theory::TrustNode mkTrustExplain(TNode lit, Node exp, std::shared_ptr<LazyCDProof> lpf);
+  theory::TrustNode mkTrustExplain(TNode lit,
+                                   Node exp,
+                                   std::shared_ptr<LazyCDProof> lpf);
   /** Get proof for */
   std::shared_ptr<ProofNode> getProofFor(Node f) override;
   /** Identify this generator (for debugging, etc..) */
   std::string identify() const override;
+
  private:
   /** The proof manager, used for allocating new ProofNode objects */
   ProofNodeManager* d_pnm;
   /** Map from formulas to lazy CD proofs */
   NodeLazyCDProofMap d_proofs;
 };
-  
-}
+
+}  // namespace CVC4
 
 #endif /* CVC4__THEORY_ENGINE_PROOF_GENERATOR_H */