Age | Commit message (Collapse) | Author |
|
Fixes #4105.
It appears that the two (experimental) options in that issue were incompatible.
A block of code changed indentation in this PR and was updated to guidelines.
|
|
|
|
This option was unimplemented and was equivalent to setting the instantiation level of all quantified formulas to 0.
|
|
All things related to the current BV solver are obsolete in the sense
that we are working on a new BV solver implementation. The BV abstraction
module has several issues and is quite hacky, it should only be enabled
in experimental settings. We don't want to remove it yet though, we want
to keep it around for future evaluation purposes. This commit
categorizes the option to enable the module and a second option related
to the module as 'undocumented'.
|
|
This never impacted performance positively. Fixes #3997 and fixes #4015.
There was a folder that the symmetry breaker was used on regress1/sym. These are simple examples that show when it is possible to find symmetries in SMT; the symmetry breaker is not critical for solving these. For now I'm leaving them as regressions documenting possible benchmarks to target if we revisit this technique.
|
|
Fixes #4019.
This feature was never fully implemented.
|
|
This option enables the sygus solver (previous name was ceGuidedInst, deprecated from CAV 15 specific approach).
It also improves when this option is set. In particular we ensure it is enabled when sygus is enabled for any reason.
|
|
Fixes #3914. The pass was only applicable to inputs with UFs that were
exclusively applied to single integer values. This limitation seems to
make the preprocessing pass not very useful in practice and it is
subsumed by our Ackermannization pass, which can remove UFs from more
complex inputs. Thus, this commit removes the preprocessing pass.
|
|
Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally.
Co-authored-by: Clark Barrett <barrett@cs.stanford.edu>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Co-authored-by: makaimann <makaim@stanford.edu>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: AleksandarZeljic <zeljic@stanford.edu>
Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com>
Co-authored-by: Amalee <amaleewilson@gmail.com>
Co-authored-by: Scott Kovach <dskovach@gmail.com>
Co-authored-by: ntsis <nekuna@gmail.com>
|
|
(#3841)
Fixes #3839.
Previously, the quantifiers rewriter had a rewriting step that was an ad-hoc version of some of the rewrites that have been incorporated into the extended rewriter. Moreover, the code for that pass was buggy.
This eliminates the previous conditional rewriting step from the "term process" rewrite pass in quantifiers. It additional adds an optional (disabled by default) rewriting pass that calls the extended rewriter on the body of quantified formulas. This subsumes the previous behavior and should not be buggy.
Notice that the indentation in computeProcessTerms changed and subsequently has been updated to the new coding standards.
This PR relies on #3840.
|
|
Fixes #3300.
This adds an option --model-witness-choice that ensures that choices in models are of the form (choice ((x Int)) (or (= x c) P)), which is helpful if the user wants to know a potential value in the range of the choice.
|
|
Commit 1c09572e0e2031519a103caa2a4af0d9bd34a9c5 removed the portfolio
build but there were some leftovers. This commit removes them.
|
|
Introduces a preprocessing pass that translates bv problems to integer problems.
|
|
selected SAT solver is compiled-in (#3771)
|
|
This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`).
Fixes #3751.
|
|
|
|
|
|
|
|
|
|
|
|
This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This commit adds support for compiling CVC4 with ThreadSanitizer
instrumentation. This is useful for debugging issues when CVC4 is used
in a multi-threaded context (e.g. #3292).
|
|
|
|
|
|
definitions (#3399)
Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
|
|
This commit adds support for compiling CVC4 with UBSan instrumentation.
The commit also adds a dummy version of `AigBitblaster`. Previously,
when CVC4 was built without ABC, `AigBitblaster` was not fully defined
(the class was declared but the implementation was not being compiled).
This lead to missing RTTI information when compiling with UBSan
instrumentation.
|
|
The ackermannization process is currently already support general theories rather than specifically for BV. In this pull request, an option has been added to turn on ackermannization independently.
|
|
|
|
|
|
|
|
|
|
|
|
This commit removes the SMT1 parser infrastructure and adds the SMT2 translations of the SMT1 regression tests. For now this commit removes regression test regress3/pp-regfile.smt since the SMT2 translation has a file size of 887M (vs. 172K for the SMT1 version).
Fixes #2948 and fixes #1313.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
* Removes incremental API check (#3011)
* Fixes toSatValueLit to use the new semantics of CaDiCaL's val()
Fixes #3011
|
|
|
|
|
|
|