(proof-new) Miscelleneous fixes from proof-new (#5714)

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 01054372556be9f8fef1ccab94770545ea69ce40..7d5b555c23db4961c8a55bbfde990768a0d3efee 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1044,7 +1044,7 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){
         {
           std::vector<Node> conf;
           conf.push_back(t);
-          conf.push_back(c.eqNode(t[0][0]));
+          conf.push_back(t[0][0].eqNode(c));
           Trace("dt-conflict")
               << "CONFLICT: Tester merge eq conflict : " << conf << std::endl;
           d_im.sendDtConflict(conf, InferId::TESTER_CONFLICT);

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 8915fcd02cc11c508362877d7ef532b8cf3c6c26..6187233e0d35789aafd0d71b8e3cf0e885c44350 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -66,6 +66,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
                 d_csolver,
                 d_esolver,
                 d_statistics),
+      d_regexp_elim(options::regExpElimAgg(), pnm, u),
       d_stringsFmf(c, u, valuation, d_termReg)
 {
 

diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp
index b289d83cce9f62a5b74b76c3a86003ab961dc295..4f174e69ef08702d6ce8e3ee97dec28f09185ce5 100644 (file)
--- a/src/theory/trust_substitutions.cpp
+++ b/src/theory/trust_substitutions.cpp
@@ -200,13 +200,14 @@ TrustNode TrustSubstitutionMap::apply(Node n, bool doRewrite)
   }
   if (!d_tspb->applyEqIntro(n, ns, pfChildren, d_ids))
   {
-    return TrustNode::mkTrustRewrite(n, ns, nullptr);
+    // if we fail for any reason, we must use a trusted step instead
+    d_tspb->addStep(PfRule::TRUST_SUBS_MAP, pfChildren, {eq}, eq);
   }
   // -------        ------- from external proof generators
   // x1 = t1 ...    xn = tn
   // ----------------------- AND_INTRO
   //   ...
-  // --------- MACRO_SR_EQ_INTRO
+  // --------- MACRO_SR_EQ_INTRO (or TRUST_SUBS_MAP if we failed above)
   // n == ns
   // add it to the apply proof generator.
   //
@@ -241,6 +242,7 @@ Node TrustSubstitutionMap::getCurrentSubstitution()
   {
     csubsChildren.push_back(tns.getProven());
   }
+  std::reverse(csubsChildren.begin(),csubsChildren.end());
   d_currentSubs = NodeManager::currentNM()->mkAnd(csubsChildren);
   if (d_currentSubs.get().getKind() == kind::AND)
   {

diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h
index 08e2da895c29e170699fdd6f0152c45db9809e19..9b462c6da91b29550c591aa7d037855d8022b839 100644 (file)
--- a/src/theory/trust_substitutions.h
+++ b/src/theory/trust_substitutions.h
@@ -40,7 +40,7 @@ class TrustSubstitutionMap
   TrustSubstitutionMap(context::Context* c,
                        ProofNodeManager* pnm,
                        std::string name = "TrustSubstitutionMap",
-                       PfRule trustId = PfRule::TRUST_SUBS_MAP,
+                       PfRule trustId = PfRule::PREPROCESS_LEMMA,
                        MethodId ids = MethodId::SB_DEFAULT);
   /** Gets a reference to the underlying substitution map */
   SubstitutionMap& get();