Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Address
Browse files Browse the repository at this point in the history
ajreynol committed Nov 18, 2024
1 parent d7ce784 commit bc259af
Showing 7 changed files with 17 additions and 5 deletions.
3 changes: 3 additions & 0 deletions src/preprocessing/assertion_pipeline.cpp
Original file line number Diff line number Diff line change
@@ -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));
}
}
6 changes: 5 additions & 1 deletion src/preprocessing/assertion_pipeline.h
Original file line number Diff line number Diff line change
@@ -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);

2 changes: 1 addition & 1 deletion src/preprocessing/passes/static_learning.cpp
Original file line number Diff line number Diff line change
@@ -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;
1 change: 1 addition & 0 deletions src/preprocessing/passes/unconstrained_simplifier.cpp
Original file line number Diff line number Diff line change
@@ -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
4 changes: 2 additions & 2 deletions src/proof/trust_id.cpp
Original file line number Diff line number Diff line change
@@ -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:
2 changes: 1 addition & 1 deletion src/proof/trust_id.h
Original file line number Diff line number Diff line change
@@ -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,
4 changes: 4 additions & 0 deletions src/smt/preprocess_proof_generator.h
Original file line number Diff line number Diff line change
@@ -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,

0 comments on commit bc259af

Please sign in to comment.