| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This PR makes sure that option handlers have access to both the canonical option name and the option name that was actually used. It also updates the options README and gets rid of the base_handlers.h of which only a fraction was used.
|
|
OptimizationResult now contains:
- cvc5::Result
- optimal value for objective
- whether the objective is unbounded
This gets benefit from cvc5::Result (e.g., we could get explanation for UNKNOWN) and it's slightly easier to integrate to the current API.
Also refactors BV optimizer so that it uses switch statement (instead of if-then-else) to judge the checkSat results (I was planning to do this a long while ago)...
|
|
solver (#6736)
This PR is the sequel of #6676 .
It adds the `POW2` kind, inference rules that will be used in the `pow2` solver, an implementation of one function of the solver, as well as stubs for the others. The next PR will include more implementations.
|
|
|
|
This PR updates to the latest version of libpoly, which has a memory leak fixed.
|
|
This PR adds CoCoALib as an optional dependency. It will be used in the CAD-based nonlinear solver for computer algebra routines beyond the capabilities of libpoly like quotient rings and polynomial factorization.
|
|
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.
|
|
|
|
|
|
|
|
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
|
|
This commit:
- Disables `--tear-down-incremental=X` for the competition since
it currently does not work correctly on master and a fixed version did
not show significant benefits.
- Changes the occurrences of `--nl-ext` to `--nl-ext=full` because it
is now a mode option.
- Removes the use of `--bv-assert-input` because the option currently
has some issues in incremental mode (#6738)
- Removes the use of `--bitblast=eager` for the model validation track
because it produces invalid models (#6741)
|
|
|
|
This commit adds a new parser option, --hol, which marks that HOL is being used. This option has the effect of prepending the problem's logic with "HO_", which teels the solver that the logic is higher order. The parser builder, base parser, and SMT2 and TPTP parsers are all updated to work with this new setting, as is the logic info class.
For now this parser option is enabling the --uf-ho option for internal use, since for now higher-order solving relies it. In a future PR this dependency will be removed (since this information is already given to the SMT solver via the logic).
|
|
This PR add the interface and a dummy implementation for the new Lazard evaluation. The dummy implementation is used when CoCoALib is not available and simply falls back to poly::infeasible_regions. The proper implementation that actually does that the comment says will be added with subsequent PRs.
|
|
solve-int-as-bv is now the preferred method for solving these benchmarks.
Adds solve-int-as-bv to a regression that became slow in my previous commit.
|
|
This PR ensures we do not eagerly rewrite bv2nat and int2bv when using solve-bv-as-int. Instead they are rewritten during expandDefinitions (at the end of preprocessing).
It also updates regressions that relied on lazy extended function reductions in the lazy solver to use solve-bv-as-int, and adds a missing case (INT_TO_BITVECTOR) in the solve-int-as-bv preprocessing pass.
A followup PR will remove support for lazy extended function reductions for bv2nat / int2bv altogether.
|
|
|
|
This migrates page https://cvc4.github.io/sets-and-relations.
It further adds the SMT2 version of examples/api/cpp/sets.cpp and adds
test/regress/regress0/rels/relations-ops.smt2 as smtlib example for
relations.
|
|
After commit 327a24508ed1d02a3fa233e680ffd0b30aa685a9, the int-to-bv
preprocessing pass is getting rewritten terms. As a result, the terms
can contain negative constants (instead of `(- c)`, i.e., `UMINUS` of a
positive constant) and `NONLINEAR_MULT`. The commit adds support for
those cases, does some minor cleanup, and adds regressions. The
regressions should allow us to detect if/when the preprocessing pass
breaks in the future.
|
|
|
|
Fixes #6717. Commit 11c1fba added some
new rewrites for ITE. Due to the new rewrites taking precedence over
existing rewrites, it could happen that some of the previous rewrites
did not apply anymore even though they would have further simplified the
ITE. In the example from the issue, (ite c c true) was rewritten to
(or (not T) T) instead of (ite T true true) and then true. The
commit fixes the issue by moving rewrites resulting in
conjunctions/disjunctions to the end.
|
|
This PR makes squashing olds commits in the docs-cleanup CI job more robust: it makes sure that the squash commit has a proper commit date and that we gracefully handle if there is nothing to squash.
|
|
Towards "learned rewrite" preprocessing pass / improvements to Int <-> BV.
|
|
This PR fixes some initial issues with printing datatypes in smt2.
It does not yet address further issues on printing define-fun as a result of dump=raw-benchmark, which requires deeper refactoring of the implementation of the API / SmtEngine.
|
|
This PR pushes a rather complex check from the CommandExecutor inside the GetInstantiationsCommand.
The aim is to only use the instFormatMode option in the library (command.cpp) but not the main driver (command_executor.cpp).
|
|
This commit removes obsolete options for BV and strings logics, and
updates QF_NIA to spend more time on our best configuration.
Co-authored-by: Gereon Kremer nafur42@gmail.com
Co-authored-by: Mathias Preiner mathias.preiner@gmail.com
|
|
Use CDList for optimization objectives so that optimization solver supports push and pop (just use SmtEngine's push/pop).
SmtEngine::resetAssertions will also clears the optimization objectives, so no need to have the reset objectives function.
|
|
|
|
This PR makes a new regression explicitly require statistics.
|
|
This migrates page https://cvc4.github.io/separation-logic.
|
|
This commit changes the Kind description not to include C/C++
preprocessor statements and updates the kind of bit-vector addtion.
It also marks some of the information as internal to exclude it from the
public documentation.
|
|
This updates 2-dim dependent bounded quantifiers to not map constants to terms when computing ranges, when the type of the variable is closed enumerable. This is require to fix an incorrect model (possible solution unsoundness) issue in the reduction of str.indexof_re.
Fixes the 1st, 4th and 5th benchmarks from #6653. Fixes #6635.
|
|
This is a simple class to maintain a list of literals that we have learned that may be useful during preprocessing.
This is work towards a "learned rewrite" preprocessing pass / better support for Int/BV translations during preprocessing.
|
|
This PR fixes a typo in the option handler for the statistics options, which lead to options not properly propagating.
|
|
subsolvers (#6705)
This PR extends the Env class to hold a pointer to the original options that are owned by the api::Solver. These original options will be used to properly initialize subsolvers as using the current options leads to subtle issues as setDefaults is not (in general) idempotent.
|
|
The binary_name is solely used as a temporary storage to pass the data from the options parser back to the runCvc5 method where it is put in a static variable. This PR gets rid of the option and the public option getter in favor of directly storing the program name in the static variable using an additional argument to parseOptions().
|
|
Our documentation for `toPythonObj` says that real values are represented as Fractions. However, getRealValue yields a float approximation thereof.
We should probably stick to Fractions, since they allow us to precisely capture values in LRA. Also, that's more aligned with the C++ API, which returns a string representation of the (unapproximated) Rational.
Also, document some (potential) weirdness with calling mkReal on floating-point values.
|
|
Work towards central equality engine.
This does some minor reorganization to TheoryUF, related to UF+cardinality constraints that makes it compatible with central equality engine. In particular, preNotifyFact is removed in favor of adding conflicts after cardinality constraints are added to the equality engine. This ensures that the central equality engine can explain conflicts that involve cardinality constraints (which will no longer be the responsibility of UF when --ee-mode=central).
|
|
Fixes the 2nd benchmark from #6653.
|
|
This PR fixes a missing connection in trust substitution proofs, which was the cause of open proofs when solved equalities from ppAssert were not justified by proofs.
Also distinguishes TRUST_SUBS_EQ from TRUST_SUBS_MAP for clarity.
|
|
This PR removes the next heavily specialized template function Options::wasSetByUser() in favor of direct access to the *WasSetByUser flags.
|
|
|
|
This PR adds the possibility to make option modules public. As shown on the example of the main driver options, this allows to get rid of the wrappers from options_public.h. We plan to make only very few option modules public (i.e. main and parser).
|
|
Fixes #6681. When checking whether SPLIT_EQ_STRIP_L applies, we were
using sripSymbolicLength, which changes its inputs depending on how
many elements of the concatenation it could strip. However, one of the
arguments, pfxv0, was reused across multiple checks if the strip did
not result in a rewrite. Later invocations were wrong as a result. This
commit changes the call to stripSymbolicLength() to use a new copy of
the vector instead.
|
|
Minor reorganization to make calls to theory engine from combination engine / shared solver more organized.
|
|
This PR adds a header file for the pow2 solver. It also includes an empty test file, to trigger compilation of the header file. The next PR will include implementations and tests.
|
|
This commit enables the new bitblast solver by default. This commit also fixes model generation for Boolean variables when --bitblast=eager is enabled.
Fixes #3958, #5396, #5736, #5743, #5947.
|
|
|
