| 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.
|
|
This commit changes how defaults are set and how the SMT solver is initialized so that proofs can be used fully with (new) unsat cores. Three modes of unsat cores are established now:
the upcoming assumption-based cores, which are incompatible with producing proofs (but enable proofs for preprocessing)
cores based on the SAT proof, which are incompatible with producing proofs (but enable proofs for preprocessing and the SAT solver)
cores based on the full proof, which are unrestricted
All the modes activate proofs but lead to errors if the user requires proofs but is not in the full proofs mode for cores.
|
|
|
|
This commit adds a new option to produce unsat cores based on our proof infrastructure (whereas previously we could only do so if we were also checking unsat cores) and the corresponding changes to the default settings to account for it. Since now options::unsatCores() and options::produceProofs() are incompatible, several parts of the code where we tested if we were in "old unsat cores mode", by testing the former and the negation of the latter options, are updated accordingly.
This commit also changes how SMT engine sets things by disabling proofs in the theory engine if we are in unsat core mode.
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
A proof is represented as a string in GetProofCommand. The string is generated by the custom ways in which the SMT engine may choose to print the proof, based on proof-format-mode (to be added in subsequent commits).
|
|
This PR adds infrastructure in SmtEngine and ProofManager for checking and printing proofs. It updates a previous interface that used ProofGenerator in favor of ProofNode.
This makes it so that it only remains to make PropEngine to be proof producing.
|
|
The only code including the old API now are in parser/ and main/ which will require further untangling.
|
|
pipeline (#5136)
This PR makes several fixes to preprocess proof generator, making it user-context dependent and making it avoid cyclic proofs. It additionally makes assertion pipeline a new interface "conjoin" which should always be used when we conjoin a new assertion to an old position in the assertion vector. It also removes an unnecessary interface to assertion pipeline.
Next PRs will clean up the use of assertions pipeline in all preprocessing passes to use the proper interfaces. This includes removing non-constant references to assertions, which has been fixed on proof-new.
|
|
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.
|
