| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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 changes the front end of prop engine to distinguish input formulas from skolem definitions, which is required by the decision engine. This PR breaks the dependency of PropEngine on the AssertionsPipeline, as now the determining of whether an input formula is a skolem definition is handled externally, in SmtSolver.
With this PR, we should not be required to satisfy skolem definitions that are not relevant based on the techniques already implemented in the decision engine. Currently, we are not distinguishing input formulas from skolem definitions properly, meaning we assert more literals than we need to.
This also simplifies related interfaces within decision engine.
We should test this PR with --decision=justification on SMT-LIB.
|
|
This does a minor simplification to the interface for preprocessor. It has a postProcess call that is called after another unrelated call at the SmtSolver level (notifyPreprocessedAssertions) is made. This makes it so that Preprocessor::postProcess is inlined as the last step of process.
|
|
In particular, theory_engine.h is included many places spuriously.
A few blocks of code changed indentation, updated to guidelines.
|
|
This reorganizes calls to QuantifiersEngine from SmtEngine. Our policy has changed recently that the SmtEngine layer is allowed to make calls directly to QuantifiersEngine, which eliminates the need for TheoryEngine to have forwarding calls. This PR makes this policy more consistent.
This also makes quantifier-specific calls more safe by throwing modal exceptions in the cases where quantifiers are present.
Marking "major" since we currently segfault when e.g. dumping instantiations in non-quantified logics. This PR makes it so that we throw a modal exception.
|
|
This is work towards refactoring ITE removal (more generally, term formula removal) so that it happens at a configurable time, preferably post-CNF conversion.
This moves the TermFormulaRemover to the TheoryPreprocessor and changes several interfaces as a consequence of this move.
The next step will move the TheoryPreprocessor inside prop::TheoryProxy.
There are no behavior changes to solving in this PR. One aspect of CheckModels is simplified.
|
|
This is in preparation to make the prop engine proof producing. This PR also renames "DPLLSatSolverInterface" to the more appropriate name "CDCLTSatSolverInterface".
Note that most of the diff is due to formatting of the previously super ad-hoc formatting of the minisat code.
|
|
This PR makes decision engine independent of AssertionsPipeline, which consequently allows some of the key PropEngine interfaces to be consolidated. It also modifies PropEngine to take TrustNode for assertLemma, which is the first step for making PropEngine manage proofs from TheoryEngine.
This is in preparation for modifying the interplay between PropEngine, TheoryEngine, TheoryPreprocessor, and new proposed SAT relevancy heuristic.
There are no intended behavior changes in this PR.
Marking "major" since this impacts several current directions (including proof-new integration, lazy theory preprocessing, SAT relevancy).
|
|
This utility will be undergoing major additions to make it more robust. Thus it should be moved to its own file.
There are no major code changes in this PR, a few things were changed to be consistent to the coding standard.
|
|
This completes proof support in TheoryEngine.
The main addition in this PR is to make its getExplanation method proof producing.
|
|
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 is work towards migrating commands to the new API. Internal code that creates command objects just for dumping is replaced with direct calls to functions that print the those commands.
|
|
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 changes an initialization issue in regarding PropEngine and TheoryEngine.
In the constructor for PropEngine, we convert and assert literals for true and false to CNF stream. Doing so triggers several things, including calls that preregister these literals with the associated TheoryEngine. This means that literals are preregistered to TheoryEngine before it has been fully initialized (TheoryEngine::finishInit). This is not currently an issue since this only involves modules that are constructed statically (e.g. SharedTermsDatabase), but this will lead to issues when the TheoryEngine is more configurable.
The solution is to additionally have a PropEngine::finishInit, which is called after TheoryEngine::finishInit, which does this step. The PropEngine should not assert anything to CNF before this method is called.
|
|
This class is responsible for maintaining TheoryEngine and PropEngine and implementing the check-sat command. It also has an interface for processing/pushing the current assertions into the PropEngine.
This class will be used directly by other extension solvers (for abduction, interpolation, qe, sygus, etc.).
|
