| Age | Commit message (Collapse) | Author |
|---|
|
This PR fixes a missing connection in trust substitution proofs, which was the cause of open proofs when solved equalities from ppAssert were not justified by proofs.
Also distinguishes TRUST_SUBS_EQ from TRUST_SUBS_MAP for clarity.
|
|
This removes the expandOnly flag from expandDefinitions.
The use of expandOnly = true is equivalent to applying top-level substitutions only, which should be done explicitly via Env::getTopLevelSubstitutions. It updates the trust substitutions utility to distinguish apply vs applyTrusted for convenience for this purpose.
This also breaks several dependencies in e.g. expand definitions module.
|
|
This eliminates explicit tracking of defined functions, and instead makes define-fun add to preprocessing substitutions.
In other words, the effect of:
(define-fun f X t)
is to add f -> (lambda X t) to the set of substitutions known by the preprocessor. This is essentially the same as when
(= f (lambda X t)) was an equality solved by non-clausal simplification
The motivation for this change is both uniformity and for performance, as fewer traversals of the input formula.
In this PR:
define-fun are now conceptually higher-order equalities provided to smt::Assertions. These assertions are always added as substitutions instead of being pushed to AssertionPipeline.
Top-level substitutions are moved from PreprocessingContext to Env, since they must be accessed by Assertions. Proofs for this class are enabled dynamically during SmtEngine::finishInit.
The expandDefinitions preprocessing step is replaced by apply-substs. The process assertions module no longer needs access to expand definitions.
The proof manager does not require a special case of using the define-function maps.
Define-function maps are eliminated from SmtEngine.
Further work will reorganize the relationship between the expand definitions module and the rewriter, after which global calls to SmtEngine::expandDefinitions can be cleaned up. There is also further work necessary to better integrate theory expand definitions and top-level substitutions, which will be done on a followup PR.
|
|
This ensures that dependencies are tracked for all inferred substitutions, even if a trusted step is added.
This is required to ensure unsat cores are sound when we use e.g. non-clausal simplification + unsat cores.
|
|
This adds various methods for applying substitution as an options to MACRO_SR_* rules. It extends the proof checker and the proof post processor to eliminate based on these types.
It updates the trust substitutions utility used by non-clausal simplification to use fixed-point semantics for substitution, which is highly important for efficiency.
As a result of this PR, we are orders of magnitude faster for checking proofs for problems where non-clausal substitution infers many substitutions. It also makes our regressions noticeably faster:
|
|
This is work towards addressing a bottleneck when generating proofs for substitutions from non-clausal simplification.
This makes the proof generation in trust substitution map lazy.
Further work is required to allow an alternative fixpoint semantics for substitutions in the proof checker instead of the current sequential one.
|
|
|
|
|
|
|
|
|
|
This PR adds optional rewriting to the SubstitutionMap class. Before, only the new TrustSubstitutionMap added optional rewriting, leading to unexpected inconsistencies between the two. In particular, cases exist where the substitution and the rewriting cancel each other (see #5943).
This PR moves the optional rewriting from TrustSubstitutionMap into SubstitutionMap. While the former enables it by default, it is disabled by default for the latter and thus does not change current behavior.
We now use this new option in an assertion in the non-clausal simplification.
Fixes #5943.
|
|
|
|
|
|
This PR replaces the LazyCDProofSet, that was hardcoded to use LazyCDProof objects, by a templated CDProofSet.
|
|
Ensuring closed proofs should not be enabled by default, it is actually not used very often as a whole. Moreover, the "trust id" argument is the most useful argument and hence should come as the 3rd argument. This updates all uses of addLazyStep for the change in interface, also changes term conversion generator which had a similar issue with default arguments.
Notice that some calls to addLazyStep were checking closed but without providing a debug string, these I've left alone (they no longer check closed).
|
|
Trust substitution is a data structure that is used throughout preprocessing for proofs.
This adds its implementation.
|
|
The current work on proof-new involves proofs for preprocessing. The biggest issue currently is that our preprocessing passes do not track proofs for substitutions.
This adds a "trusted substitution" class with is a layer on substitution map. The proof aspect of this class is not yet implemented, this PR just adds its interface.
This also updates Theory::ppAssert to take a TrustSubstitutionMap instead of a SubstitutionMap, since eventually we will require proofs to be provided for substitutions that are added to this map.
|
