From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 23 Dec 2020 20:13:03 +0000 (-0600)
Subject: (proof-new) Miscelleneous fixes from proof-new (#5714)
X-Git-Tag: cvc5-1.0.0~2406
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2594c961105110f6fce17983bfa69f68bd9ee15e;p=cvc5.git

(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 010543725..7d5b555c2 100644
--- 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 8915fcd02..6187233e0 100644
--- 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 b289d83cc..4f174e69e 100644
--- 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 08e2da895..9b462c6da 100644
--- 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();