Format

4 files changed, 31 insertions, 27 deletions

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 112ec2347..f9f4a064f 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -1006,30 +1006,30 @@ void CoreSolver::getNormalForms(Node eqc,
 void CoreSolver::processNEqc(std::vector<NormalForm>& normal_forms,
                              TypeNode stype)
 {
-  if (normal_forms.size()<=1)
+  if (normal_forms.size() <= 1)
   {
     return;
   }
   // compute normal forms that are effectively unique
-  std::unordered_map<Node,size_t,NodeHashFunction> nfCache;
+  std::unordered_map<Node, size_t, NodeHashFunction> nfCache;
   std::vector<size_t> nfIndices;
   bool foundConflict = false;
   size_t nfConfJ = 0;
   size_t nfConfI = 0;
-  for (size_t i=0, nnforms=normal_forms.size(); i<nnforms; i++)
+  for (size_t i = 0, nnforms = normal_forms.size(); i < nnforms; i++)
   {
     NormalForm& nfi = normal_forms[i];
-    Node ni = utils::mkNConcat(nfi.d_nf,stype);
-    if (nfCache.find(ni)==nfCache.end())
+    Node ni = utils::mkNConcat(nfi.d_nf, stype);
+    if (nfCache.find(ni) == nfCache.end())
     {
       // compare against previous to see if already conflicting
       if (!foundConflict)
       {
-        for (const std::pair<const Node, size_t >& nj : nfCache)
+        for (const std::pair<const Node, size_t>& nj : nfCache)
         {
           Node eq = ni.eqNode(nj.first);
           eq = Rewriter::rewrite(eq);
-          if (eq==d_false)
+          if (eq == d_false)
           {
             nfConfJ = nj.second;
             nfConfI = i;
@@ -1043,15 +1043,17 @@ void CoreSolver::processNEqc(std::vector<NormalForm>& normal_forms,
     }
   }
   size_t nnfs = nfIndices.size();
-  Trace("strings-solve") << "CoreSolver::processNEqc: " << nnfs << "/" << normal_forms.size() << " normal forms are unique." << std::endl;
+  Trace("strings-solve") << "CoreSolver::processNEqc: " << nnfs << "/"
+                         << normal_forms.size() << " normal forms are unique."
+                         << std::endl;
 
   //the possible inferences
   std::vector<CoreInferInfo> pinfer;
-  // loop over all pairs 
-  for(unsigned i=0; i<nnfs-1; i++) 
+  // loop over all pairs
+  for (unsigned i = 0; i < nnfs - 1; i++)
   {
     //unify each normalform[j] with normal_forms[i]
-    for(unsigned j=i+1; j<nnfs; j++ ) 
+    for (unsigned j = i + 1; j < nnfs; j++)
     {
       NormalForm& nfi = normal_forms[nfIndices[i]];
       NormalForm& nfj = normal_forms[nfIndices[j]];
@@ -1062,7 +1064,8 @@ void CoreSolver::processNEqc(std::vector<NormalForm>& normal_forms,
         Trace("strings-solve") << "Strings: Already cached." << std::endl;
         continue;
       }
-      //process the reverse direction first (check for easy conflicts and inferences)
+      // process the reverse direction first (check for easy conflicts and
+      // inferences)
       unsigned rindex = 0;
       nfi.reverse();
       nfj.reverse();
@@ -1073,8 +1076,8 @@ void CoreSolver::processNEqc(std::vector<NormalForm>& normal_forms,
       {
         break;
       }
-      //AJR: for less aggressive endpoint inference
-      //rindex = 0;
+      // AJR: for less aggressive endpoint inference
+      // rindex = 0;
 
       unsigned index = 0;
       processSimpleNEq(nfi, nfj, index, false, rindex, pinfer, stype);
@@ -1099,8 +1102,8 @@ void CoreSolver::processNEqc(std::vector<NormalForm>& normal_forms,
     std::vector<Node> exp;
     NormalForm& nfj = normal_forms[nfConfJ];
     NormalForm& nfi = normal_forms[nfConfI];
-    exp.insert(exp.end(),nfj.d_exp.begin(),nfj.d_exp.end());
-    exp.insert(exp.end(),nfi.d_exp.begin(),nfi.d_exp.end());
+    exp.insert(exp.end(), nfj.d_exp.begin(), nfj.d_exp.end());
+    exp.insert(exp.end(), nfi.d_exp.begin(), nfi.d_exp.end());
     exp.push_back(nfi.d_base.eqNode(nfj.d_base));
     d_im.sendInference(exp, d_false, Inference::N_EQ_CONF);
     return;
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index e3d0a1a6c..102e8b27d 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -306,7 +306,8 @@ Node InferProofCons::convert(Inference infer,
           // 2+ children.
         }
       }
-      else if (infer == Inference::N_CONST || infer == Inference::F_CONST || infer == Inference::N_EQ_CONF)
+      else if (infer == Inference::N_CONST || infer == Inference::F_CONST
+               || infer == Inference::N_EQ_CONF)
       {
         // should be a constant conflict
         std::vector<Node> childrenC;
diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp
index 70675e22c..f709dce32 100644
--- a/src/theory/uf/eq_proof.cpp
+++ b/src/theory/uf/eq_proof.cpp
@@ -207,8 +207,8 @@ bool EqProof::foldTransitivityChildren(
     inSubstCase = true;
     Node premiseTermEq = premises[offending][termPos];
     Node conclusionTermEq = conclusion[0].getKind() == kind::CONST_BOOLEAN
-                              ? conclusion[1]
-                              : conclusion[0];
+                                ? conclusion[1]
+                                : conclusion[0];
     Trace("eqproof-conv") << "EqProof::foldTransitivityChildren: Substitition "
                              "case. Need to build subst from "
                           << premiseTermEq << " to " << conclusionTermEq
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index 041268114..b2bf09219 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -439,8 +439,9 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc,
         itf = ac.find(aeqSym);
         if (itf != ac.end())
         {
-          Trace("pfee-proof") << "- reorient assumption " << aeqSym << " via "
-                              << a << " for " << fa.second.size() << " proof nodes" << std::endl;
+          Trace("pfee-proof")
+              << "- reorient assumption " << aeqSym << " via " << a << " for "
+              << fa.second.size() << " proof nodes" << std::endl;
           std::shared_ptr<ProofNode> pfaa = d_pnm->mkAssume(aeqSym);
           for (ProofNode* pfs : fa.second)
           {
@@ -466,7 +467,7 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc,
       AlwaysAssert(false) << "Generated a non-closed proof: " << ss.str()
                           << std::endl;
     }
-    if (acu.size()<ac.size())
+    if (acu.size() < ac.size())
     {
       // All assumptions should match a free assumption; if one does not, then
       // the explanation could have been smaller. This assertion should be
@@ -475,15 +476,14 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc,
       // method.
       for (const Node& a : ac)
       {
-        if (acu.find(a)==acu.end())
+        if (acu.find(a) == acu.end())
         {
           Notice() << "pfee::ensureProofForFact: assumption " << a
-                  << " does not match a free assumption in proof" 
-                  << std::endl;
+                   << " does not match a free assumption in proof" << std::endl;
         }
       }
     }
-    scopeAssumps.insert(scopeAssumps.end(),acu.begin(),acu.end());
+    scopeAssumps.insert(scopeAssumps.end(), acu.begin(), acu.end());
     exp = mkAnd(scopeAssumps);
   }
   else
@@ -534,7 +534,7 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc,
     Assert(pf != nullptr);
     // Should be a closed proof now. If it is not, then the overall proof
     // is malformed.
-    Assert (pf->isClosed());
+    Assert(pf->isClosed());
     pfg = this;
     // set the proof for the conflict or lemma, which can be queried later
     switch (tnk)