| Age | Commit message (Collapse) | Author |
|---|
|
Commit d1eee40cc (PR #6346), in a foolish attempt to prevent speculated issues, introduced an overwriting policy to addition of resolution chains during SAT solving at the SAT proof manager. First, this is nonsensical because the lazy proof chain is context-dependent and at the same level other ways of proving that clause are simply redundant and therefore should be ignored. Second, and catastrophically, this policy, for reasons beyond me, can lead to open SAT proofs when the same clause is rederived at the same level.
So this commit simply reverts the change and adds an optimization that when the clause would be rederived at the same level we do nothing and leave the method.
|
|
Not doing this rewrite for Booleans is probably an artifact of the old IFF kind being removed. This rewrite is important to simplify the generation of proofs for the SAT solver, as clarified in the new comment in the SAT proof manager.
|
|
This also refactors decision engine so that we use inheritance instead of a dummy flag + members to determine which implementation to use.
|
|
The decision level as previously implemented was not accurate since it
did not consider the user context level. This resulted in facts being
incorrectly recognized as input assertions, which happened for
incremental benchmarks.
|
|
The statistic in `smt_solver.cpp` was not accurate.
|
|
Since the new BV solver is enabled by default and uses CaDiCaL
(and optionally CryptoMiniSat) we make CaDiCaL a required dependency.
|
|
This commit makes toCNF() iterative to avoid this issue.
Note that the order in which nodes are visited and thus SatLiterals are
created remains the same.
Fixes #6111
|
|
This PR gets rid of almost all remaining public option wrappers. It does so by
- making base, main and parser options public such that they can directly be used from the driver and the parser
- moving incremental and the resource limiting options to base
- moving dumping options to main
After this PR, the only option wrapper left is becoming obsolete as well after (the follow-up of) #6697.
|
|
This PR removes the next heavily specialized template function Options::wasSetByUser() in favor of direct access to the *WasSetByUser flags.
|
|
This removes namespace theory from proof utilities, and moves MethodId to its own file in src/proof/.
|
|
This enables the new implementation of justification heuristic by default.
Fixes #5454, fixes #5785. Fixes wishues 114, 115, 149, 160.
|
|
We store constants, e.g., BitVector and Rational, in our node infrastructure. As a result, we were indirectly including some headers in almost all files, e.g., the GMP headers. This commit changes that by forward-declaring the classes for the constants. As a result, we have to include headers like util/rational.h explicitly when we use Rational but it saves about 3 minutes in compile time (CPU time).
The commit changes RoundingMode from an enum to an enum class such that it can be forward declared.
|
|
This moves all generic proof utilites from src/expr/ and src/theory/ to src/proof/.
It also changes the include for term conversion proof generator to conv_proof_generator in preparation to rename this utility on a followup PR (to avoid confusion with the use of "Term").
|
|
This PR fixes a missing initialization that lead to a valgrind warning.
|
|
This commit removes the remaining old proof code and the code to produce unsat cores based on it.
|
|
|
|
This commit changes the includes used by MiniSat. This commit changes
the includes from stdint.h/inttypes.h/limits.h to
cstdint/cinttypes/climits. This ensures that the macros in
cinttypes/inttypes.h, e.g., `PRIi64`, are actually defined. The C99
standard suggested that those macros are only defined for C++ code when
`__STDC_FORMAT_MACROS` is defined. This was never adopted by a C++
standard (https://en.cppreference.com/w/cpp/types/integer). However,
certain versions of mingw-w64 seem to require it with inttypes.h but not
cinttypes.
This fixes the nightly Windows build (tested in the Docker container
used by the nightlies).
|
|
The bitblast solver currently uses solving under assumptions for all facts that are sent to the bit-vector solver. For input facts on user-level 0 we can however assert the fact to the SAT solver, which allows the SAT solver to do more preprocessing. This PR adds the option to assert user-level 0 input facts, which is disabled by default.
|
|
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
|
|
The decision engine is the class that contains strategies for doing e.g. justification heuristic.
The current implementation is hardcoded for the old implementation of justification heuristic.
Since both implementations will be maintained in the short term, this splits the parts of DecisionEngine that are specific to the old implementation to a class DecisionEngineOld.
It refactors the interface of DecisionEngine in a way that is compatible with both implementations.
|
|
This is work towards eliminating singletons.
Also, TheoryModel should use the same substitution map as the preprocessor. This is work towards unifying these things, which will be done in a future PR.
|
|
Previously using proof CNF stream together with assumptions-based unsat cores added unnecessary performance overhead.
Co-authored-by: Mathias Preiner mathias.preiner@gmail.com
|
|
This PR adds a reset() method to the ReferenceStat class. It then uses it to properly reset such statistics in the minisat solvers where lifetime is an issue.
|
|
This PR does a first round of refactoring and gets rid of a significant portion of generated code. In particular
- it removes options::optionName.wasSetByUser() (we still have Options::wasSetByUser())
- it removes options::optionName.set() (we still have Options::set())
- it removes options::optionName.getName() in favor of options::optionName.name
- it removes the specializations of Options::assign() and Options::assignBool() from the headers
- it eliminates runHandlerAndPredicates() and runBoolPredicates()
The removed methods are only used in few places with are changed to using Options::current().X() instead.
In the future, we also want to get rid of options::optionName() and use Options::operator[]() instead, and furthermore not use Options::current() but use the options from the Env object. This PR already adds Env::getOption() as a shorthand for Env::getOptions()[...] and uses it as a proof of concept within SmtEngine.
|
|
Due to our recent changes in the unsat core infrastructure we were doing a couple assertions wrong during conflict analysis. This commit fixes them.
|
|
This PR adds an assumption-based unsat cores option. If enabled it will
disable proof logging in the SAT solver and adds input assertions as
assumptions to the SAT solver. When an unsat core is requested we
extract the unsat core in terms of the unsat assumption in the SAT
solver. Assumption-based unsat cores use the proof infrastructure to map
the input assumptions back to the original assertions.
|
|
This PR fixes a very subtle issue with setting the values a ReferenceStat refers to.
ReferenceStat::set() would take a variable by const& and then store the pointer to it. When giving it a different, but implicitly convertible, type, the pointer would assume the wrong type and consequently read incorrect values from it.
This PR makes set() a template function that explicitly checks that the given type is the correct one.
As we can only export int64_t to the API, this forces users of ReferenceStat to use int64_t stats.
|
|
Towards setting up the proper callbacks into the new justification heuristic.
Moves ownership of skolem definition manager from TheoryProxy to PropEngine.
|
|
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 commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
|
|
This PR creates a support library from the utilities in base and context, which will be required in the parser as soon as we move the symbol table/manager to the parser.
Note: I decided to always build static libraries from base and context (and optionally enable -fPIC for shared builds) since I'm not sure if we want to have these libraries installed separately. Right now these are considered as cvc5 internal utilities that can be used in all cvc5 libraries, but not outside.
|
|
This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.
|
|
This PR refactors how we collect statistics.
It splits the current statistic values into the values and a proxy object. The actual values now live inside the registry (making the ownership model way easier) while the proxy object are handed to whoever wants to collect a new statistic.
It also extends the C++ API to obtain and inspect the statistics.
To change the ownership, this PR needs to touch every single statistic in the whole codebase and change how it is registered.
|
|
|
|
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.
|
|
Prevents exponential behavior in SAT proof generation by not reexplaining previously explained literals. Also fix a potential issue in not previously overwriting rederived resolution chains during solving.
|
|
This PR does another round of refactoring of the resource manager and related code.
- it moves the Resource enum out of the ResourceManager class
- it treats the resources in a generic way (storing the statistics in a vector) instead of the manual treatment we had before
- weights no longer live in the options, but in the ResourceManager and are changed accordingly in the ResourceManager constructor
- following the generic treatment of resources, it also removes all the resource-specific options --x-step in favor of a generic --rweight name=weight
- removed several unused methods from the ResourceManager
Note that we handle the Resource enum in a way that allows to easily use other enums as additional resources, for example InferenceId. The general idea is that we will at some point have sensible default weights (so that the cumulative resources somewhat simulate the solver runtime) and users (almost) never need to modify them.
|
|
|
|
This consolidates the interface for asserting input formulas to the PropEngine from SmtSolver.
As a consequence of this PR, this corrects one issue with the justification heuristic where skolem definitions were considered "assertions" by the justification heuristic (e.g. formulas that must be satisfied) instead of just being required for skolems in relevant literals. This was asymmetric from skolem definitions from lemmas, which were not being considered assertions. Now, skolem definitions are never assertions.
I tested this on QF_LIA SMT-LIB with decision=justification with 300 second timeout, essentially no difference in results (+6-5 all close to timeout). Also no difference on QF_S + QF_SLIA.
|
|
|
|
|
|
For some benchmarks, checking MACRO_RESOLUTION can be up to 80% (!!!) of the running time. This commit introduces a new rule that does not perform checking. The old rule and checker are kept for ground truth. Some miscellaneous minor changes are also made in the PR.
|
|
Previously the SMT post-processor would update any assumption as long as it
had a proof for it. This can be a problem when one as assumption introduced in a
scope that should not be expanded. This commit fixes the issue by adding the
option of configuring a proof node updater to track scopes and the assumptions
they introduce, which can be used to determine the prood nodes which should be
updated. It also changes the SMT post-processor to only update assumptions that
have not been introduced in some scope.
This commit fixes an issue found by @Lachnitt during the integration of CVC4 and Isabelle.
|
|
Currently, NodeBuilder takes a single template argument: An integer
that determines the expected number of arguments. This argument is used
to determine the size of the d_inlineNvChildSpace array. This array is
used to construct nodes inline. The advantage of this is that we don't
have to allocate a NodeValue on the heap for the node under
construction until we are sure that the node is new. While templating
the array size may save some stack space (or avoid a heap allocation if
we statically know that we a fixed number of children and that number is
greater than 10), it complicates the code and leads to longer compile
times. Thus, this commit removes the template argument and moves some of
the NodeBuilder code to a source file for faster compilation.
CPU build time before change (debug build): 2429.68s
CPU build time after change (debug build): 2228.44s
Signed-off-by: Andres Noetzli noetzli@amazon.com
|
|
|
|
|
|
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.
|
|
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>
|
|
|
|
Commit d47a8708171f1cf488fe9ce05f56f2566db53093 refactored the interface of
prop engine. In doing so, it changed the order in which preregistration lemmas
were asserted. Before the commit, they were asserted after all the user
assertions. After the commit, they were asserted after each user assertion that
generated them. This, however, seems to have a negative performance impact,
especially for string benchmarks because the justification heuristic tries to
justify the assertions in the order in which they appear. Intuitively, it makes
sense to first try to satisfy the user assertions before trying to satisfy the
preregistration lemmas.
Signed-off-by: Andres Noetzli <noetzli@amazon.com>
|
