| Age | Commit message (Collapse) | Author |
|---|
|
This PR changes ResetCommand to not call SmtEngine::reset but instead reconstruct the api::Solver object. This makes SmtEngine::reset obsolete and removes it, and moves the original options from SmtEngine to api::Solver.
The motivation for this change is twofold:
The ResetCommand should not use SmtEngine directly, but only through the API (i.e. Solver).
As soon as the statistics data lives within the registry, we need to re-register statistics after resetting the SmtEngine. We can now do this within the api::Solver constructor.
|
|
|
|
We require tracking of instantiation lemmas for quantifier elimination. Recently, this feature was removed in favor of reconstructing instantiations via substitutions. This does not quite work if instantiation lemmas have more complex post-processing, e.g. virtual term substitution.
This PR reimplements a much simpler form of instantiation tracking that simply adds instantiation bodies to a vector, per quantified formula. It uses this vector for quantifier elimination.
Fixes #5899.
|
|
This PR adds includes that are missing from source files, but currently provided by other includes.
This mostly concerns <sstream> which is currently included by the statistics, which will change in the future.
|
|
|
|
|
|
This PR does some refactoring on how we handle statistics in the driver, and some minor cleanup along the way.
The SmtEngine now has dedicated statistics for the data collected within the driver and provides utility functions to set them.
The driver pushes the collected statistics to the SmtEngine instead of adding them itself to the statistics registry.
The node manager no longer holds a statistics registry (that nobody used anymore anyway)
The command executor no longer holds a pointer to the SmtEngine itself. The pointer is not necessary and seems to become stale after we call reset on the command executor (which, luckily, we don't seem to do usually)
The main motivation for this change is to make the whole statistics infrastructure private to the library and not exporting it to the outside world.
|
|
This creates a central utility for managing "skolem definitions", e.g. mapping between skolems and the lemmas that define their behavior.
This utility is taken from the satRlv branch. It will also be used for the new implementation of the justification decision heuristic.
Note that this PR takes some helper functions out of term formula removal (e.g. hasSkolems) Prior to this PR, these helper functions were incorrect since term formula removal does not account for all introduced skolems. For instance, Theory::ppRewrite may introduce skolems directly. This PR consolidates these cases into the new class, which is called from PropEngine when lemmas and assertions are added. At the moment, the only use of this method is for CEGQI, which needs to do its own tracking of skolems in certain literals.
It also makes some minor reorganization to prop engine.
|
|
In rare cases, we may reuse skolems for different terms (those that are the same up to purification) due to recent changes in how skolem are generated. This guards for this case in the term formula remover, which avoids assertion failures in cd insert hash map.
Fixes #6132.
|
|
Warning if not a supported version.
|
|
This PR moves the statistics registry from SmtEngine to Env.
|
|
This PR eliminates all remaining uses of SExpr outside of statistics.
|
|
This copies most of the remaining changes to set_defaults.cpp from proof-new.
In particular, it recognizes when proofs must be disabled.
This is required to fix the regressions (locally) and the nightlies.
|
|
|
|
The build system (cmake) will automatically generate an export header
cvc4_export.h, which makes sure that the correct export features are
defined depending on the compiler and target platform. The macro CVC4_EXPORT
replaces CVC4_PUBLIC and its usage is reduced by 2/3.
Co-authored-by: Gereon Kremer <nafur42@gmail.com>
|
|
|
|
This PR uses IntegralHistogramStat instead of HistogramStat when appropriate, that is everywhere.
|
|
Adds a dot printer for proof nodes. Also adds an option to choose the proof format (as a mode).
Signed-off-by: Diego Della Rocca de Camargos <diegodellarocc@gmail.com>
|
|
Towards having proofs working on master.
|
|
This PR does a first round of refactoring on the statistics, in particular the Stat class and derived classes.
It significantly shrinks the class hierarchy, modernizes some code (e.g. use std::chrono instead of clock_gettime), removes unused features (e.g. nesting of statistics) and does some general cleanup and consolidation.
Subsequent PRs are planned to change the ownership model (right now every module owns the Stat object) which makes the whole register / unregister mechanism obsolete.
|
|
|
|
This class contains all globally available utilities for internal code.
|
|
This fixes two issues for preprocessing:
(1) The term preregistration visitor was calling preRegister on terms multiple times in a SAT context, which the linear arithmetic solver is sensitive to.
(2) It was possible for non-preprocessed terms to appear in assertions if they were on the RHS of substitutions learned by non-clausal simplification, and substituted into assertions post-theory-preprocessing.
To fix (1), the SharedTermsVisitor is update to track which theories has preregistered each term, as is done in the PreRegisterVisitor. To fix (2), we no longer apply-subst after theory preprocessing.
These two fixes are required to fix #6071.
Note: we should performance test this on SMT-LIB.
|
|
calculus (#6051)
This makes a simplification to the internal proof calculus. In particular, purification skolems are no longer are special case of witness skolems. They are now independent concepts. The concept of "witness form" is replaced in most places by "original form".
This is required for fixing two issues:
(1) variable shadowing issues in skolemization.
(2) bookkeeping issues for bound variables introduced to construct witness terms. This made the LFSC proof conversion extremely cumbersome for e.g. string reductions.
In this PR, the main changes:
The internals of SkolemManager are changed to use original form vs witness form when necessary. This eliminates the need to do variable renaming in SkolemManager::skolemize.
the rule WITNESS_INTRO is replaced by SKOLEM_INTRO
MACRO_SR_* rules use original form
Proof post processing is simplified
These changes imply that ppRewrite should not return WITNESS terms. Followup PRs will modify arithmetic preprocessing so that its ppRewrite method returns skolems instead.
|
|
This removes use of the logic request utility.
It generally bad practice to change the logic dynamically, e.g. during preprocessing, since it makes it so that CVC4 does not properly initialize. We now insist that logic is changed upfront in set_defaults.
This is in preparation for the smt::Env class, which will change the ownership of logic.
|
|
This is in preparation for enabling CI / proofs on master.
This does not throw an option exception when proofs are enabled, it also makes a fix that was missing on master and needed for regressions to pass on master.
This is partially taken from #5980.
|
|
This PR does some more cleanup of the includes.
|
|
|
|
This commit removes parser and printer support for old SMT-LIB standards and also converts all regression tests to 2.6.
|
|
|
|
This disables the temporarily available internals of Term.
Note: getExpr() is still available and will be disabled when the API is
fully converted to Nodes.
|
|
This disables the temporarily available internals of Sort.
|
|
This disables the temporarily available internals of Result.
It further changes the interface for getUnknownExplanation, which now
returns an enum value instead of a string.
|
|
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 is a step towards removing SExpr class. It replaces SExpr with std::string for set-info and set-option commands.
|
|
This PR cleans up a ton of includes, based on the suggestions of iwyu.
Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.
|
|
Also moves several proof-specific options to proof_options.
|
|
This commit adds support for bit-level propagation for the BV bitblast solver to quickly detect conflicts on effort levels != FULL. Bit-level propagation for the bitblast solver is by default disabled for now. Further, bit-blasting of facts is now handled more lazily with a bit-blast queue.
|
|
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.
|
|
This was used in the old method for unsat core tracking for instantiation lemmas, which will soon be subsumed.
This is also work towards eliminating the dependencies on quantifiers engine from Instantiate.
|
|
This method is used to determine which skolems have definitions according to term formula removal. This optimizes the method using attributes similar to how expr::getFreeVariables works.
It will be used heavily for SAT relevancy. We should also consider updating the justification heuristic to use this method.
|
|
Our current policy for term formula removal leaves quantifier bodies unchanged. This simplifies the code based on this observation.
|
|
Previously we were unable to dump assertions in ProcessAssertions::apply for the definition-expansion, simplify and repeat-simplify passes.
|
|
This PR adds a new bit-blasting BV solver, which can be enabled via --bv-solver=bitblast. The new bit-blast solver can be used instead of the lazy BV solver and currently supports CaDiCaL and CryptoMiniSat as SAT back end.
|
|
(#5850)
Evaluating the proof infrastructure in SMT-LIB has uncovered a rare case (i.e., not previously in our regressions!!) in which the resulting clause from crowding literal elimination is a singleton. This commit makes the expansion code robust to that and adds an example of a problematic benchmark as a regression.
Also improves a bit tracing and some comments.
|
|
In particular, theory_engine.h is included many places spuriously.
A few blocks of code changed indentation, updated to guidelines.
|
|
Evaluating the proof infrastructure in SMT-LIB has uncovered a rare case (i.e., not previously in our regressions!!) in which a crowding literal occurs in an OR node that represents a single-literal clause subsequent to the last clause that includes the crowding literal. This was leading to the clause that eliminates the crowding literal not being found. The commit fixes this issue by excluding single-literal clauses from those that can introduce crowding literals (which was already marked as necessary but not properly enforced).
|
|
This PR modifies sexprToString to use Term::getString to get string constants instead of Term::toString, which depends on the output language. The previous behavior caused CVC4 to crash when AST is picked as the output language.
|
|
Allows one to generate unsat cores from the new proof infrastructure. For new this is controlled by a new option, --check-unsat-cores-new.
|
