Format

10 files changed, 102 insertions, 72 deletions

diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 0cdad4fdf..2c6d22d27 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -79,7 +79,8 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
   LemmaProofRecipe* proofRecipe = NULL;
   PROOF(proofRecipe = new LemmaProofRecipe;);
 
-  theory::TrustNode tte = d_theoryEngine->getExplanationAndRecipe(lNode, proofRecipe);
+  theory::TrustNode tte =
+      d_theoryEngine->getExplanationAndRecipe(lNode, proofRecipe);
   Node theoryExplanation = tte.getNode();
 
   PROOF({
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index c0ba11f72..735f0703c 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -27,7 +27,8 @@ namespace CVC4 {
 SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine,
                                          context::Context* context,
                                          context::UserContext* userContext,
-                ProofNodeManager* pnm, LazyCDProof* lcp)
+                                         ProofNodeManager* pnm,
+                                         LazyCDProof* lcp)
     : ContextNotifyObj(context),
       d_statSharedTerms("theory::shared_terms", 0),
       d_addedSharedTermsSize(context, 0),
@@ -36,11 +37,12 @@ SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine,
       d_registeredEqualities(context),
       d_EENotify(*this),
       d_equalityEngine(d_EENotify, context, "SharedTermsDatabase", true),
-      d_pfee(context,userContext,d_equalityEngine,pnm, lcp!=nullptr),
+      d_pfee(context, userContext, d_equalityEngine, pnm, lcp != nullptr),
       d_theoryEngine(theoryEngine),
       d_inConflict(context, false),
       d_conflictPolarity(),
-      d_lazyPf(lcp) {
+      d_lazyPf(lcp)
+{
   smtStatisticsRegistry()->registerStat(&d_statSharedTerms);
 }
 
@@ -203,7 +205,7 @@ void SharedTermsDatabase::assertEquality(TNode equality, bool polarity, TNode re
 {
   Debug("shared-terms-database::assert") << "SharedTermsDatabase::assertEquality(" << equality << ", " << (polarity ? "true" : "false") << ", " << reason << ")" << endl;
   // Add it to the equality engine
-  //d_equalityEngine.assertEquality(equality, polarity, reason);
+  // d_equalityEngine.assertEquality(equality, polarity, reason);
   d_pfee.assertAssume(reason);
   // Check for conflict
   checkForConflict();
@@ -227,7 +229,7 @@ void SharedTermsDatabase::checkForConflict() {
       conflict = conflict.notNode();
     }
     TrustNode trnc = d_pfee.assertConflict(conflict);
-    if (d_lazyPf!=nullptr)
+    if (d_lazyPf != nullptr)
     {
       // add the step to the proof
       Node ckey = TrustNode::getConflictKeyValue(trnc.getNode());
@@ -248,7 +250,8 @@ bool SharedTermsDatabase::isKnown(TNode literal) const {
   }
 }
 
-theory::TrustNode SharedTermsDatabase::explain(TNode literal) {
+theory::TrustNode SharedTermsDatabase::explain(TNode literal)
+{
   TrustNode trn = d_pfee.explain(literal);
   return trn;
 }
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index 5abf0b281..9bd00962f 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -20,23 +20,21 @@
 #include <unordered_map>
 
 #include "context/cdhashset.h"
+#include "expr/lazy_proof.h"
 #include "expr/node.h"
+#include "expr/proof_node_manager.h"
 #include "theory/theory.h"
+#include "theory/trust_node.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/proof_equality_engine.h"
-#include "theory/trust_node.h"
-#include "expr/proof_node_manager.h"
 #include "util/statistics_registry.h"
-#include "expr/lazy_proof.h"
 
 namespace CVC4 {
 
 class TheoryEngine;
 
 class SharedTermsDatabase : public context::ContextNotifyObj {
-
  public:
-
   /** A container for a list of shared terms */
   typedef std::vector<TNode> shared_terms_list;
 
@@ -44,7 +42,6 @@ class SharedTermsDatabase : public context::ContextNotifyObj {
   typedef shared_terms_list::const_iterator shared_terms_iterator;
 
  private:
-
   /** Some statistics */
   IntStat d_statSharedTerms;
 
@@ -73,7 +70,6 @@ class SharedTermsDatabase : public context::ContextNotifyObj {
   RegisteredEqualitiesSet d_registeredEqualities;
 
  private:
-
   /** This method removes all the un-necessary stuff from the maps */
   void backtrack();
 
@@ -118,7 +114,7 @@ class SharedTermsDatabase : public context::ContextNotifyObj {
 
   /** Equality engine */
   theory::eq::EqualityEngine d_equalityEngine;
-  
+
   /** Proof equality engine */
   theory::eq::ProofEqEngine d_pfee;
 
@@ -163,10 +159,11 @@ class SharedTermsDatabase : public context::ContextNotifyObj {
   void checkForConflict();
 
  public:
-
-  SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context,
-                                         context::UserContext* userContext,
-                ProofNodeManager* pnm, LazyCDProof* lcp);
+  SharedTermsDatabase(TheoryEngine* theoryEngine,
+                      context::Context* context,
+                      context::UserContext* userContext,
+                      ProofNodeManager* pnm,
+                      LazyCDProof* lcp);
   ~SharedTermsDatabase();
 
   /**
@@ -257,7 +254,6 @@ class SharedTermsDatabase : public context::ContextNotifyObj {
   theory::eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; }
 
  protected:
-
   /** Pointer to the lazy proof of TheoryEngine */
   LazyCDProof* d_lazyPf;
   /**
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index cc73da8f2..87d861cf2 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -773,17 +773,20 @@ Node CoreSolver::getConclusion(Node x,
     {
       // we can assume its length is greater than zero
       Node emp = Word::mkEmptyWord(sk1.getType());
-      conc = nm->mkNode(AND, conc, sk1.eqNode(emp).negate(),
-      nm->mkNode(GT,nm->mkNode(STRING_LENGTH,sk1), nm->mkConst(Rational(0))));
+      conc = nm->mkNode(
+          AND,
+          conc,
+          sk1.eqNode(emp).negate(),
+          nm->mkNode(
+              GT, nm->mkNode(STRING_LENGTH, sk1), nm->mkConst(Rational(0))));
     }
   }
-  else if (rule==PfRule::CONCAT_CSPLIT)
+  else if (rule == PfRule::CONCAT_CSPLIT)
   {
-    Assert (y.isConst());
+    Assert(y.isConst());
     size_t yLen = Word::getLength(y);
-    Node firstChar = yLen == 1 ? y
-                                  : (isRev ? Word::suffix(y, 1)
-                                            : Word::prefix(y, 1));
+    Node firstChar =
+        yLen == 1 ? y : (isRev ? Word::suffix(y, 1) : Word::prefix(y, 1));
     Node sk = skc->mkSkolemCached(
         x,
         isRev ? SkolemCache::SK_ID_VC_SPT_REV : SkolemCache::SK_ID_VC_SPT,
@@ -792,17 +795,15 @@ Node CoreSolver::getConclusion(Node x,
     conc = x.eqNode(isRev ? utils::mkNConcat(sk, firstChar)
                           : utils::mkNConcat(firstChar, sk));
   }
-  else if (rule==PfRule::CONCAT_CPROP)
+  else if (rule == PfRule::CONCAT_CPROP)
   {
     // expect (str.++ z c1) and c2
-    Assert (x.getKind()==STRING_CONCAT && x.getNumChildren()==2);
+    Assert(x.getKind() == STRING_CONCAT && x.getNumChildren() == 2);
     Node z = x[isRev ? 1 : 0];
     Node c1 = x[isRev ? 0 : 1];
-    Assert (c1.isConst());
+    Assert(c1.isConst());
     Node c2 = y;
-    Assert (c2.isConst());
-    
-    
+    Assert(c2.isConst());
   }
 
   return conc;
@@ -1556,11 +1557,12 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       // E.g. "abc" ++ ... = nc ++ ... ---> nc = "a" ++ k
       SkolemCache* skc = d_termReg.getSkolemCache();
       std::vector<Node> newSkolems;
-      iinfo.d_conc = getConclusion(nc,nfcv[index],PfRule::CONCAT_CSPLIT,isRev,skc,newSkolems);
+      iinfo.d_conc = getConclusion(
+          nc, nfcv[index], PfRule::CONCAT_CSPLIT, isRev, skc, newSkolems);
       NormalForm::getExplanationForPrefixEq(
           nfi, nfj, index, index, iinfo.d_ant);
       iinfo.d_ant.push_back(expNonEmpty);
-      Assert(newSkolems.size()==1);
+      Assert(newSkolems.size() == 1);
       iinfo.d_new_skolem[LENGTH_SPLIT].push_back(newSkolems[0]);
       iinfo.d_id = Inference::SSPLIT_CST;
       iinfo.d_idRev = isRev;
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 9af4dc565..891f23cd2 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -48,7 +48,7 @@ void InferProofCons::notifyFact(const InferInfo& ii)
     Trace("strings-ipc-debug") << "...duplicate!" << std::endl;
     return;
   }
-  if (fact.getKind()==EQUAL)
+  if (fact.getKind() == EQUAL)
   {
     Node symFact = fact[1].eqNode(fact[0]);
     if (d_lazyFactMap.find(symFact) != d_lazyFactMap.end())
@@ -1012,9 +1012,9 @@ std::shared_ptr<ProofNode> InferProofCons::getProofFor(Node fact)
   CDProof pf(d_pnm);
   // get the inference
   NodeInferInfoMap::iterator it = d_lazyFactMap.find(fact);
-  if (it==d_lazyFactMap.end())
+  if (it == d_lazyFactMap.end())
   {
-    if (fact.getKind()==EQUAL)
+    if (fact.getKind() == EQUAL)
     {
       // Use the symmetric fact. There is no need to explictly make a
       // SYMM proof, as this is handled by CDProof::mkProof below.
diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp
index a5a22dfa0..3b06ea447 100644
--- a/src/theory/strings/proof_checker.cpp
+++ b/src/theory/strings/proof_checker.cpp
@@ -307,8 +307,8 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
     std::vector<Node> newSkolems;
     Node kt0 = ProofSkolemCache::getSkolemForm(t0);
     Node ks0 = ProofSkolemCache::getSkolemForm(s0);
-    Node conc = CoreSolver::getConclusion(
-        kt0, ks0, id, isRev, &skc, newSkolems);
+    Node conc =
+        CoreSolver::getConclusion(kt0, ks0, id, isRev, &skc, newSkolems);
     conc = ProofSkolemCache::getWitnessForm(conc);
     return conc;
   }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 7a0c68f37..789bc8cb1 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -197,8 +197,12 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_logicInfo(logicInfo),
       d_pchecker(new ProofChecker),
       d_pNodeManager(new ProofNodeManager(d_pchecker.get())),
-      d_lazyProof(options::proofNew() ? new LazyCDProof(d_pNodeManager.get(), nullptr, d_userContext) : nullptr),
-      d_sharedTerms(this, context, userContext, d_pNodeManager.get(), d_lazyProof.get()),
+      d_lazyProof(
+          options::proofNew()
+              ? new LazyCDProof(d_pNodeManager.get(), nullptr, d_userContext)
+              : nullptr),
+      d_sharedTerms(
+          this, context, userContext, d_pNodeManager.get(), d_lazyProof.get()),
       d_masterEqualityEngine(nullptr),
       d_masterEENotify(*this),
       d_quantEngine(nullptr),
@@ -1542,8 +1546,10 @@ static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
 
   return conjunction;
 }
-  
-theory::TrustNode TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe) {
+
+theory::TrustNode TheoryEngine::getExplanationAndRecipe(
+    TNode node, LemmaProofRecipe* proofRecipe)
+{
   Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current propagation index = " << d_propagationMapTimestamp << endl;
 
   bool polarity = node.getKind() != kind::NOT;
@@ -1634,7 +1640,8 @@ theory::TrustNode TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRe
   return texplanation;
 }
 
-theory::TrustNode TheoryEngine::getExplanation(TNode node) {
+theory::TrustNode TheoryEngine::getExplanation(TNode node)
+{
   LemmaProofRecipe *dontCareRecipe = NULL;
   return getExplanationAndRecipe(node, dontCareRecipe);
 }
@@ -1745,7 +1752,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
                                         theory::TheoryId atomsTo) {
   // For resource-limiting (also does a time check).
   // spendResource();
-  
+
   // Do we need to check atoms
   if (atomsTo != theory::THEORY_LAST) {
     Debug("theory::atoms") << "TheoryEngine::lemma(" << node << ", " << atomsTo << ")" << endl;
@@ -1774,14 +1781,15 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
     if (!d_lazyProof->hasStep(lemma) && !d_lazyProof->hasGenerator(lemma))
     {
       Trace("te-proof") << "No proof for lemma: " << lemma << std::endl;
-      Trace("te-proof-warn") << "WARNING: No proof for lemma: " << lemma << std::endl;
+      Trace("te-proof-warn")
+          << "WARNING: No proof for lemma: " << lemma << std::endl;
     }
     else
     {
       Trace("te-proof") << "Proof for lemma: " << lemma << std::endl;
     }
   }
-  
+
   AssertionPipeline additionalLemmas;
 
   // Run theory preprocessing, maybe
@@ -1808,10 +1816,12 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   }
 
   // assert to prop engine
-  for (size_t i = 0, lsize = additionalLemmas.size(); i < lsize; ++ i) {
+  for (size_t i = 0, lsize = additionalLemmas.size(); i < lsize; ++i)
+  {
     Node rewritten = Rewriter::rewrite(additionalLemmas[i]);
     additionalLemmas.replace(i, rewritten);
-    d_propEngine->assertLemma(additionalLemmas[i], i==0 && negated, removable, rule, node);
+    d_propEngine->assertLemma(
+        additionalLemmas[i], i == 0 && negated, removable, rule, node);
   }
 
   // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
@@ -1837,9 +1847,10 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
 void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
 
   Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << ")" << endl;
-  // if proofNew is enabled, then d_lazyProof contains a proof of conflict.negate()
-  //Assert (!options::proofNew() || d_lazyProof->hasStep(conflict.negate()) || d_lazyProof->hasGenerator(conflict.negate()) || theoryId==THEORY_ARITH);
-  
+  // if proofNew is enabled, then d_lazyProof contains a proof of
+  // conflict.negate()
+  // Assert (!options::proofNew() || d_lazyProof->hasStep(conflict.negate()) ||
+  // d_lazyProof->hasGenerator(conflict.negate()) || theoryId==THEORY_ARITH);
 
   Trace("dtview::conflict") << ":THEORY-CONFLICT: " << conflict << std::endl;
 
@@ -1872,7 +1883,8 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
   if (d_logicInfo.isSharingEnabled()) {
     // Create the workplace for explanations
     std::vector<NodeTheoryPair> vec;
-    vec.push_back(NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp));
+    vec.push_back(
+        NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp));
 
     // Process the explanation
     TrustNode tnc = getExplanation(vec, proofRecipe);
@@ -1963,7 +1975,10 @@ void TheoryEngine::staticInitializeBVOptions(
   }
 }
 
-theory::TrustNode TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* proofRecipe) {
+theory::TrustNode TheoryEngine::getExplanation(
+    std::vector<NodeTheoryPair>& explanationVector,
+    LemmaProofRecipe* proofRecipe)
+{
   Assert(explanationVector.size() > 0);
 
   unsigned i = 0; // Index of the current literal we are processing
@@ -2064,15 +2079,17 @@ theory::TrustNode TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& expl
     if (toExplain.d_theory == THEORY_BUILTIN)
     {
       texplanation = d_sharedTerms.explain(toExplain.d_node);
-      Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << texplanation.getNode() << std::endl;
+      Debug("theory::explain")
+          << "\tTerm was propagated by THEORY_BUILTIN. Explanation: "
+          << texplanation.getNode() << std::endl;
     }
     else
     {
-      texplanation =
-          theoryOf(toExplain.d_theory)->explain(toExplain.d_node);
-      Debug("theory::explain") << "\tTerm was propagated by owner theory: "
-                               << theoryOf(toExplain.d_theory)->getId()
-                               << ". Explanation: " << texplanation.getNode() << std::endl;
+      texplanation = theoryOf(toExplain.d_theory)->explain(toExplain.d_node);
+      Debug("theory::explain")
+          << "\tTerm was propagated by owner theory: "
+          << theoryOf(toExplain.d_theory)->getId()
+          << ". Explanation: " << texplanation.getNode() << std::endl;
     }
     Node explanation = texplanation.getNode();
 
@@ -2140,11 +2157,10 @@ theory::TrustNode TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& expl
         }
       }
     });
-  
-  
+
   Node exp = mkExplanation(explanationVector);
   // FIXME
-  return theory::TrustNode::mkTrustLemma(exp,nullptr);
+  return theory::TrustNode::mkTrustLemma(exp, nullptr);
 }
 
 void TheoryEngine::setUserAttribute(const std::string& attr,
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 77f597845..edd2a1a12 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -45,13 +45,13 @@
 #include "theory/substitutions.h"
 #include "theory/term_registration_visitor.h"
 #include "theory/theory.h"
+#include "theory/trust_node.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/valuation.h"
 #include "util/hash.h"
 #include "util/resource_manager.h"
 #include "util/statistics_registry.h"
 #include "util/unsafe_interrupt_exception.h"
-#include "theory/trust_node.h"
 
 namespace CVC4 {
 
@@ -157,7 +157,7 @@ class TheoryEngine {
    */
   std::shared_ptr<LazyCDProof> d_lazyProof;
   //--------------------------------- end new proofs
-  
+
   /**
    * The database of shared terms.
    */
@@ -515,9 +515,11 @@ class TheoryEngine {
    * theory that sent the literal. The lemmaProofRecipe will contain a list
    * of the explanation steps required to produce the original node.
    */
-  theory::TrustNode getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* lemmaProofRecipe);
+  theory::TrustNode getExplanation(
+      std::vector<NodeTheoryPair>& explanationVector,
+      LemmaProofRecipe* lemmaProofRecipe);
 
-public:
+ public:
 
   /**
    * Signal the start of a new round of assertion preprocessing
@@ -642,7 +644,8 @@ public:
    * Returns an explanation of the node propagated to the SAT solver and the theory
    * that propagated it.
    */
-  theory::TrustNode getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe);
+  theory::TrustNode getExplanationAndRecipe(TNode node,
+                                            LemmaProofRecipe* proofRecipe);
 
   /**
    * collect model info
diff --git a/src/theory/uf/eq_proof.h b/src/theory/uf/eq_proof.h
index 42783d31f..49529aa2f 100644
--- a/src/theory/uf/eq_proof.h
+++ b/src/theory/uf/eq_proof.h
@@ -97,7 +97,8 @@ class EqProof
       CDProof* p,
       std::unordered_set<Node, NodeHashFunction>& assumptions) const;
 
-  bool buildTransitivityChain(Node conclusion, std::vector<Node>& premises) const;
+  bool buildTransitivityChain(Node conclusion,
+                              std::vector<Node>& premises) const;
 
   // returns whether it did reordering
   void maybeAddSymmOrTrueIntroToProof(unsigned i,
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 504f43d72..ae7477480 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -456,7 +456,11 @@ void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, un
   enqueue(MergeCandidate(t1Id, t2Id, pid, reason));
 }
 
-bool EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, unsigned pid) {
+bool EqualityEngine::assertPredicate(TNode t,
+                                     bool polarity,
+                                     TNode reason,
+                                     unsigned pid)
+{
   Debug("equality") << d_name << "::eq::addPredicate(" << t << "," << (polarity ? "true" : "false") << ")" << std::endl;
   Assert(t.getKind() != kind::EQUAL) << "Use assertEquality instead";
   TNode b = polarity ? d_true : d_false;
@@ -469,7 +473,11 @@ bool EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, unsig
   return true;
 }
 
-bool EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid) {
+bool EqualityEngine::assertEquality(TNode eq,
+                                    bool polarity,
+                                    TNode reason,
+                                    unsigned pid)
+{
   Debug("equality") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl;
   if (polarity) {
     // If two terms are already equal, don't assert anything