From bc259afb5dcf42832904a9ef48cc55ab87b1b89a Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 18 Nov 2024 14:56:33 -0600 Subject: [PATCH] Address --- src/preprocessing/assertion_pipeline.cpp | 3 +++ src/preprocessing/assertion_pipeline.h | 6 +++++- src/preprocessing/passes/static_learning.cpp | 2 +- src/preprocessing/passes/unconstrained_simplifier.cpp | 1 + src/proof/trust_id.cpp | 4 ++-- src/proof/trust_id.h | 2 +- src/smt/preprocess_proof_generator.h | 4 ++++ 7 files changed, 17 insertions(+), 5 deletions(-) diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index 2fd6deb5d75..824ca073370 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -198,6 +198,9 @@ 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)); } } diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index 5b6ac9496aa..b4aecc9fe35 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -95,6 +95,8 @@ class AssertionPipeline : protected EnvObj * @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, @@ -108,7 +110,9 @@ class AssertionPipeline : protected EnvObj TrustNode trn, TrustId trustId = TrustId::UNKNOWN_PREPROCESS); /** - * Ensure assertion at index i is rewritten. + * 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); diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp index f339e8072b7..efe9a9d411f 100644 --- a/src/preprocessing/passes/static_learning.cpp +++ b/src/preprocessing/passes/static_learning.cpp @@ -60,7 +60,7 @@ PreprocessingPassResult StaticLearning::applyInternal( // add the lemmas to the end for (const TrustNode& trn : tlems) { - assertionsToPreprocess->pushBackTrusted(trn); + assertionsToPreprocess->pushBackTrusted(trn, TrustId::PREPROCESS_STATIC_LEARNING_LEMMA); } } return PreprocessingPassResult::NO_CONFLICT; diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 1f180bab1f6..4dfc485a4f8 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -859,6 +859,7 @@ PreprocessingPassResult UnconstrainedSimplifier::applyInternal( { Node a = assertions[i]; Node as = d_substitutions.apply(a); + // nothing to do if substitutions has no effect, skip if (as != a) { // replace the assertion diff --git a/src/proof/trust_id.cpp b/src/proof/trust_id.cpp index da96f9175eb..c741ae2164f 100644 --- a/src/proof/trust_id.cpp +++ b/src/proof/trust_id.cpp @@ -43,8 +43,8 @@ const char* toString(TrustId id) case TrustId::PREPROCESS_ACKERMANN: return "PREPROCESS_ACKERMANN"; case TrustId::PREPROCESS_ACKERMANN_LEMMA: return "PREPROCESS_ACKERMANN_LEMMA"; - case TrustId::PREPROCESS_STATIC_LEARNING: - return "PREPROCESS_STATIC_LEARNING"; + case TrustId::PREPROCESS_STATIC_LEARNING_LEMMA: + return "PREPROCESS_STATIC_LEARNING_LEMMA"; case TrustId::PREPROCESS_HO_ELIM: return "PREPROCESS_HO_ELIM"; case TrustId::PREPROCESS_HO_ELIM_LEMMA: return "PREPROCESS_HO_ELIM_LEMMA"; case TrustId::PREPROCESS_BITVECTOR_EAGER_ATOMS: diff --git a/src/proof/trust_id.h b/src/proof/trust_id.h index b7ea6bd6ec8..9912f9334c1 100644 --- a/src/proof/trust_id.h +++ b/src/proof/trust_id.h @@ -53,7 +53,7 @@ enum class TrustId : uint32_t PREPROCESS_ACKERMANN, PREPROCESS_ACKERMANN_LEMMA, /** StaticLearning preprocessing pass */ - PREPROCESS_STATIC_LEARNING, + PREPROCESS_STATIC_LEARNING_LEMMA, /** HoElim preprocessing pass */ PREPROCESS_HO_ELIM, PREPROCESS_HO_ELIM_LEMMA, diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h index f0e48c50001..599d205b71b 100644 --- a/src/smt/preprocess_proof_generator.h +++ b/src/smt/preprocess_proof_generator.h @@ -94,6 +94,10 @@ class PreprocessProofGenerator : protected EnvObj, public ProofGenerator /** * Notify that n was replaced by np due to preprocessing, where pg can * provide a proof of the equality n=np. + * @param n The original formula. + * @param np The preprocessed formula. + * @param pg The proof generator that may provide a proof of (= n np). + * @param id The trust id to use, if the proof generator is null. */ void notifyPreprocessed(Node n, Node np,