Merge branch 'main' of https://github.com/cvc5/cvc5 into interfaceSim…

…p-1119

include/cvc5/cvc5_proof_rule.h

@@ -2677,6 +2677,19 @@ enum ENUM(ProofRewriteRule)
    * \endverbatim
    */
   EVALUE(DT_CONS_EQ),
+  /**
+   * \verbatim embed:rst:leading-asterisk
+   * **Datatypes -- cycle**
+   *
+   * .. math::
+   *   (x = t[x]) = \bot
+   *
+   * where all terms on the path to :math:`x` in :math:`t[x]` are applications
+   * of constructors, and this path is non-empty.
+   *
+   * \endverbatim
+   */
+  EVALUE(DT_CYCLE),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Datatypes -- collapse tester**

src/api/cpp/cvc5_proof_rule_template.cpp

@@ -257,6 +257,7 @@ const char* toString(cvc5::ProofRewriteRule rule)
     case ProofRewriteRule::DT_COLLAPSE_TESTER_SINGLETON:
       return "dt-collapse-tester-singleton";
     case ProofRewriteRule::DT_CONS_EQ: return "dt-cons-eq";
+    case ProofRewriteRule::DT_CYCLE: return "dt-cycle";
     case ProofRewriteRule::DT_COLLAPSE_UPDATER: return "dt-collapse-updater";
     case ProofRewriteRule::DT_UPDATER_ELIM: return "dt-updater-elim";
     case ProofRewriteRule::DT_MATCH_ELIM: return "dt-match-elim";

src/main/signal_handlers.cpp

@@ -213,7 +213,7 @@ void ill_handler(int sig, siginfo_t* info, void*)
 
 #endif /* __WIN32__ */
 
-static terminate_handler default_terminator;
+static thread_local terminate_handler default_terminator;
 
 void cvc5terminate()
 {

src/preprocessing/assertion_pipeline.cpp

@@ -52,7 +52,8 @@ void AssertionPipeline::clear()
 
 void AssertionPipeline::push_back(Node n,
                                   bool isInput,
-                                  ProofGenerator* pgen)
+                                  ProofGenerator* pgen,
+                                  TrustId trustId)
 {
   if (d_conflict)
   {
@@ -74,7 +75,8 @@ void AssertionPipeline::push_back(Node n,
     {
       if (!isInput)
       {
-        d_andElimEpg->addLazyStep(n, pgen, TrustId::PREPROCESS_LEMMA);
+        Assert(pgen != nullptr || trustId != TrustId::UNKNOWN_PREPROCESS_LEMMA);
+        d_andElimEpg->addLazyStep(n, pgen, trustId);
       }
     }
     std::vector<Node> toProcess;
@@ -124,7 +126,7 @@ void AssertionPipeline::push_back(Node n,
     if (!isInput)
     {
       // notice this is always called, regardless of whether pgen is nullptr
-      d_pppg->notifyNewAssert(n, pgen);
+      d_pppg->notifyNewAssert(n, pgen, trustId);
     }
     else
     {
@@ -135,14 +137,17 @@ void AssertionPipeline::push_back(Node n,
   }
 }
 
-void AssertionPipeline::pushBackTrusted(TrustNode trn)
+void AssertionPipeline::pushBackTrusted(TrustNode trn, TrustId trustId)
 {
   Assert(trn.getKind() == TrustNodeKind::LEMMA);
   // push back what was proven
-  push_back(trn.getProven(), false, trn.getGenerator());
+  push_back(trn.getProven(), false, trn.getGenerator(), trustId);
 }
 
-void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen)
+void AssertionPipeline::replace(size_t i,
+                                Node n,
+                                ProofGenerator* pgen,
+                                TrustId trustId)
 {
   Assert(i < d_nodes.size());
   if (n == d_nodes[i])
@@ -154,7 +159,8 @@ void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen)
                            << n << std::endl;
   if (isProofEnabled())
   {
-    d_pppg->notifyPreprocessed(d_nodes[i], n, pgen);
+    Assert(pgen != nullptr || trustId != TrustId::UNKNOWN_PREPROCESS);
+    d_pppg->notifyPreprocessed(d_nodes[i], n, pgen, trustId);
   }
   if (n == d_false)
   {
@@ -166,7 +172,7 @@ void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen)
   }
 }
 
-void AssertionPipeline::replaceTrusted(size_t i, TrustNode trn)
+void AssertionPipeline::replaceTrusted(size_t i, TrustNode trn, TrustId trustId)
 {
   Assert(i < d_nodes.size());
   if (trn.isNull())
@@ -176,7 +182,13 @@ void AssertionPipeline::replaceTrusted(size_t i, TrustNode trn)
   }
   Assert(trn.getKind() == TrustNodeKind::REWRITE);
   Assert(trn.getProven()[0] == d_nodes[i]);
-  replace(i, trn.getNode(), trn.getGenerator());
+  replace(i, trn.getNode(), trn.getGenerator(), trustId);
+}
+
+void AssertionPipeline::ensureRewritten(size_t i)
+{
+  Assert(i < d_nodes.size());
+  replace(i, rewrite(d_nodes[i]), d_rewpg.get());
 }
 
 void AssertionPipeline::enableProofs(smt::PreprocessProofGenerator* pppg)
@@ -187,6 +199,10 @@ void AssertionPipeline::enableProofs(smt::PreprocessProofGenerator* pppg)
     d_andElimEpg.reset(
         new LazyCDProof(d_env, nullptr, userContext(), "AssertionsAndElim"));
   }
+  if (d_rewpg == nullptr)
+  {
+    d_rewpg.reset(new RewriteProofGenerator(d_env));
+  }
 }
 
 bool AssertionPipeline::isProofEnabled() const { return d_pppg != nullptr; }
@@ -202,17 +218,19 @@ void AssertionPipeline::disableStoreSubstsInAsserts()
   d_storeSubstsInAsserts = false;
 }
 
-void AssertionPipeline::addSubstitutionNode(Node n, ProofGenerator* pg)
+void AssertionPipeline::addSubstitutionNode(Node n,
+                                            ProofGenerator* pg,
+                                            TrustId trustId)
 {
   Assert(d_storeSubstsInAsserts);
   Assert(n.getKind() == Kind::EQUAL);
   size_t prevNodeSize = d_nodes.size();
-  push_back(n, false, pg);
+  push_back(n, false, pg, trustId);
   // remember this is a substitution index
   for (size_t i = prevNodeSize, newSize = d_nodes.size(); i < newSize; i++)
   {
     // ensure rewritten
-    replace(i, rewrite(d_nodes[i]));
+    replace(i, rewrite(d_nodes[i]), d_rewpg.get());
     d_substsIndices.insert(i);
   }
 }

src/preprocessing/assertion_pipeline.h

@@ -23,6 +23,7 @@
 
 #include "expr/node.h"
 #include "proof/lazy_proof.h"
+#include "proof/rewrite_proof_generator.h"
 #include "proof/trust_node.h"
 #include "smt/env_obj.h"
 
@@ -61,17 +62,25 @@ class AssertionPipeline : protected EnvObj
   /**
    * Adds an assertion/assumption to be preprocessed.
    *
+   * Note that if proofs are provided, a preprocess pass using this method
+   * is required to either provide a proof generator or a trust id that is not
+   * TrustId::UNKNOWN_PREPROCESS_LEMMA.
+   *
    * @param n The assertion/assumption
    * @param isInput If true, n is an input formula (an assumption in the main
    * body of the overall proof).
    * @param pg The proof generator who can provide a proof of n. The proof
    * generator is not required and is ignored if isInput is true.
+   * @param trustId The trust id to use if pg is not provided when isInput
+   * is false and proofs are enabled.
    */
   void push_back(Node n,
                  bool isInput = false,
-                 ProofGenerator* pg = nullptr);
+                 ProofGenerator* pg = nullptr,
+                 TrustId trustId = TrustId::UNKNOWN_PREPROCESS_LEMMA);
   /** Same as above, with TrustNode */
-  void pushBackTrusted(TrustNode trn);
+  void pushBackTrusted(TrustNode trn,
+                       TrustId trustId = TrustId::UNKNOWN_PREPROCESS_LEMMA);
 
   /**
    * Get the constant reference to the underlying assertions. It is only
@@ -86,17 +95,34 @@ class AssertionPipeline : protected EnvObj
    * Replaces assertion i with node n and records the dependency between the
    * original assertion and its replacement.
    *
+   * Note that if proofs are provided, a preprocess pass using this method
+   * is required to either provide a proof generator or a trust id that is not
+   * TrustId::UNKNOWN_PREPROCESS_LEMMA.
+   *
    * @param i The position of the assertion to replace.
    * @param n The replacement assertion.
    * @param pg The proof generator who can provide a proof of d_nodes[i] == n,
    * where d_nodes[i] is the assertion at position i prior to this call.
+   * @param trustId The trust id to use if pg is not provided and proofs are
+   * enabled.
    */
-  void replace(size_t i, Node n, ProofGenerator* pg = nullptr);
+  void replace(size_t i,
+               Node n,
+               ProofGenerator* pg = nullptr,
+               TrustId trustId = TrustId::UNKNOWN_PREPROCESS);
   /**
    * Same as above, with TrustNode trn, which is of kind REWRITE and proves
    * d_nodes[i] = n for some n.
    */
-  void replaceTrusted(size_t i, TrustNode trn);
+  void replaceTrusted(size_t i,
+                      TrustNode trn,
+                      TrustId trustId = TrustId::UNKNOWN_PREPROCESS);
+  /**
+   * Ensure assertion at index i is rewritten. If it is not already in
+   * rewritten form, the assertion is replaced by its rewritten form.
+   * @param i The index of the assertion.
+   */
+  void ensureRewritten(size_t i);
 
   IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; }
   const IteSkolemMap& getIteSkolemMap() const { return d_iteSkolemMap; }
@@ -124,8 +150,12 @@ class AssertionPipeline : protected EnvObj
    *
    * @param n The substitution node
    * @param pg The proof generator that can provide a proof of n.
+   * @param trustId The trust id to use if pg is not provided and proofs are
+   * enabled.
    */
-  void addSubstitutionNode(Node n, ProofGenerator* pg = nullptr);
+  void addSubstitutionNode(Node n,
+                           ProofGenerator* pg = nullptr,
+                           TrustId trustId = TrustId::UNKNOWN_PREPROCESS_LEMMA);
 
   /**
    * Checks whether the assertion at a given index represents substitutions.
@@ -209,6 +239,10 @@ class AssertionPipeline : protected EnvObj
    * Maintains proofs for eliminating top-level AND from inputs to this class.
    */
   std::unique_ptr<LazyCDProof> d_andElimEpg;
+  /**
+   * Maintains proofs for rewrite steps.
+   */
+  std::unique_ptr<RewriteProofGenerator> d_rewpg;
 }; /* class AssertionPipeline */
 
 }  // namespace preprocessing

src/preprocessing/passes/ackermann.cpp

@@ -88,7 +88,8 @@ void addLemmaForPair(TNode args1,
   }
   Node func_eq = nm->mkNode(Kind::EQUAL, args1, args2);
   Node lemma = nm->mkNode(Kind::IMPLIES, args_eq, func_eq);
-  assertionsToPreprocess->push_back(lemma);
+  assertionsToPreprocess->push_back(
+      lemma, false, nullptr, TrustId::PREPROCESS_ACKERMANN_LEMMA);
 }
 
 void storeFunctionAndAddLemmas(TNode func,
@@ -286,7 +287,7 @@ void usortsToBitVectors(NodeManager* nm,
       Node newA = usVarsToBVVars.apply((*assertions)[i]);
       if (newA != old)
       {
-        assertions->replace(i, newA);
+        assertions->replace(i, newA, nullptr, TrustId::PREPROCESS_ACKERMANN);
         Trace("uninterpretedSorts-to-bv")
             << "  " << old << " => " << (*assertions)[i] << "\n";
       }
@@ -327,7 +328,10 @@ PreprocessingPassResult Ackermann::applyInternal(
   for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
   {
     assertionsToPreprocess->replace(
-        i, d_funcToSkolem.apply((*assertionsToPreprocess)[i]));
+        i,
+        d_funcToSkolem.apply((*assertionsToPreprocess)[i]),
+        nullptr,
+        TrustId::PREPROCESS_ACKERMANN);
   }
 
   /* replace uninterpreted sorts with bit-vectors */

src/preprocessing/passes/bool_to_bv.cpp

@@ -58,7 +58,9 @@ PreprocessingPassResult BoolToBV::applyInternal(
     {
       newAssertion = lowerIte((*assertionsToPreprocess)[i]);
     }
-    assertionsToPreprocess->replace(i, rewrite(newAssertion));
+    assertionsToPreprocess->replace(
+        i, newAssertion, nullptr, TrustId::PREPROCESS_BOOL_TO_BV);
+    assertionsToPreprocess->ensureRewritten(i);
     if (assertionsToPreprocess->isInConflict())
     {
       return PreprocessingPassResult::CONFLICT;

src/preprocessing/passes/bv_gauss.cpp

@@ -755,7 +755,8 @@ PreprocessingPassResult BVGauss::applyInternal(
       if (ret == BVGauss::Result::NONE)
       {
         Node n = nm->mkConst<bool>(false);
-        assertionsToPreprocess->push_back(n);
+        assertionsToPreprocess->push_back(
+            n, false, nullptr, TrustId::PREPROCESS_BV_GUASS_LEMMA);
         return PreprocessingPassResult::CONFLICT;
       }
       else
@@ -770,7 +771,8 @@ PreprocessingPassResult BVGauss::applyInternal(
           Node a = nm->mkNode(Kind::EQUAL, p.first, p.second);
           Trace("bv-gauss-elim") << "added assertion: " << a << std::endl;
           // add new assertion
-          assertionsToPreprocess->push_back(a);
+          assertionsToPreprocess->push_back(
+              a, false, nullptr, TrustId::PREPROCESS_BV_GUASS_LEMMA);
         }
       }
     }
@@ -785,7 +787,8 @@ PreprocessingPassResult BVGauss::applyInternal(
       Node a = aref[i];
       Node as = a.substitute(subst.begin(), subst.end());
       // replace the assertion
-      assertionsToPreprocess->replace(i, as);
+      assertionsToPreprocess->replace(
+          i, as, nullptr, TrustId::PREPROCESS_BV_GUASS);
     }
   }
   return PreprocessingPassResult::NO_CONFLICT;

src/preprocessing/passes/bv_intro_pow2.cpp

@@ -45,8 +45,9 @@ PreprocessingPassResult BvIntroPow2::applyInternal(
     Node res = pow2Rewrite(cur, cache);
     if (res != cur)
     {
-      res = rewrite(res);
-      assertionsToPreprocess->replace(i, res);
+      assertionsToPreprocess->replace(
+          i, res, nullptr, TrustId::PREPROCESS_BV_INTRO_POW2);
+      assertionsToPreprocess->ensureRewritten(i);
     }
   }
   return PreprocessingPassResult::NO_CONFLICT;

src/preprocessing/passes/bv_to_bool.cpp

@@ -52,7 +52,9 @@ PreprocessingPassResult BVToBool::applyInternal(
   liftBvToBool(assertionsToPreprocess->ref(), new_assertions);
   for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
   {
-    assertionsToPreprocess->replace(i, rewrite(new_assertions[i]));
+    assertionsToPreprocess->replace(
+        i, new_assertions[i], nullptr, TrustId::PREPROCESS_BV_TO_BOOL);
+    assertionsToPreprocess->ensureRewritten(i);
     if (assertionsToPreprocess->isInConflict())
     {
       return PreprocessingPassResult::CONFLICT;

src/preprocessing/passes/bv_to_int.cpp

@@ -58,13 +58,8 @@ PreprocessingPassResult BVToInt::applyInternal(
   for (uint64_t i = 0; i < assertionsToPreprocess->size(); ++i)
   {
     // ensure bv rewritten
+    assertionsToPreprocess->ensureRewritten(i);
     Node bvNode = (*assertionsToPreprocess)[i];
-    Node bvnr = rewrite(bvNode);
-    if (bvnr != bvNode)
-    {
-      assertionsToPreprocess->replace(i, bvnr);
-      bvNode = bvnr;
-    }
     TrustNode tr =
         d_intBlaster.trustedIntBlast(bvNode, additionalConstraints, skolems);
     if (tr.isNull())
@@ -76,12 +71,7 @@ PreprocessingPassResult BVToInt::applyInternal(
     Trace("bv-to-int-debug") << "int node: " << tr.getProven()[1] << std::endl;
     assertionsToPreprocess->replaceTrusted(i, tr);
     // ensure integer rewritten
-    Node intNode = (*assertionsToPreprocess)[i];
-    Node inr = rewrite(intNode);
-    if (inr != intNode)
-    {
-      assertionsToPreprocess->replace(i, inr);
-    }
+    assertionsToPreprocess->ensureRewritten(i);
   }
   addFinalizeAssertions(assertionsToPreprocess, additionalConstraints);
   addSkolemDefinitions(skolems);

src/preprocessing/passes/ff_bitsum.cpp

@@ -121,7 +121,8 @@ PreprocessingPassResult FfBitsum::applyInternal(
     Node newFact = cache[fact];
     if (newFact != fact)
     {
-      assertionsToPreprocess->replace(i, newFact);
+      assertionsToPreprocess->replace(
+          i, newFact, nullptr, TrustId::PREPROCESS_FF_BITSUM);
     }
   }
 

src/preprocessing/passes/ff_disjunctive_bit.cpp

@@ -46,7 +46,10 @@ PreprocessingPassResult FfDisjunctiveBit::applyInternal(
     {
       Trace("ff::disjunctive-bit") << "rw bit constr: " << *var << std::endl;
       Node var2 = nm->mkNode(Kind::FINITE_FIELD_MULT, *var, *var);
-      assertionsToPreprocess->replace(i, var2.eqNode(*var));
+      assertionsToPreprocess->replace(i,
+                                      var2.eqNode(*var),
+                                      nullptr,
+                                      TrustId::PREPROCESS_FF_DISJUNCTIVE_BIT);
     }
   }
   return PreprocessingPassResult::NO_CONFLICT;