| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.
|
|
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
|
|
This module is responsible for constructing the proof checker, proof node manager, and implementing dumping and checking of the final proof.
This PR includes setting up some connections into the various modules for proof production.
|
|
This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure.
It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).
|
|
This splits all things related to storing assertions in the SmtEngine into a separate class "Assertions". It also converts the interface for its methods from Expr to Node.
|
