| Age | Commit message (Collapse) | Author |
|---|
|
This restructures the entry page for the C++ API documentation in
preparation for adding a quickstart and linking to examples and adding
more content.
|
|
After commit d70a63324c95210f1d78c2efc46395d2369d2e2b, context-dependent
attributes have not been supported and, as a result, the template
parameter `context_dependent` of `Attribute` has not been used.
Context-dependent attributes also do not fit with our current design of
sharing attributes across different solvers, so it is unlikely that we
will add that feature back in the future. This commit removes the unused
template parameter.
|
|
For model construction we only compute model values for relevant terms. The set of relevant terms is computed in https://github.com/cvc5/cvc5/blob/master/src/theory/model_manager_distributed.cpp#L58, which skips equalities by default because equalities are usually handled by the equality engine.
When --bitblast=eager is enabled all assertions are wrapped into BITVECTOR_EAGER_ATOM nodes and passed to the BV solver, which results in equalities below BITVECTOR_EAGER_ATOM nodes not being handled by the equality engine but by the BV solver directly. These equalities, however, are skipped when computing the relevant terms and therefore the BV solver is not asked to compute model values for variables below these equalities.
If --bitblast=eager is enabled the BV solver now additionally adds the variables encountered during bit-blasting to the relevant terms via computeRelevantTerms.
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
|
|
This commit adds Grammar.java GrammarTest.java and cvc5_Grammar.cpp to the java api.
|
|
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 (follow #6553) adds more functions and unit tests for python API.
Subsequent PR will include additional missing functions and unit tests.
1. Adding getNullSort() and mkEmptyBag() functions.
2. Allowing mkOp() with a list of arguments (previously allowed at most 2).
3. Allowing mkString() with additional boolean argument useEscSequences.
4. Corresponding changes to the tests.
|
|
|
|
macOS virtual machines have three available cores but we were only using two of them for our CI. This commit changes the CI to retrieve the number of available cores and then to use that to number to build and test cvc5.
|
|
We don't upload the source files to the website, so this will always be
a 404.
|
|
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
|
|
The following commit made our libpoly patch for our Windows builds
obsolete:
https://github.com/SRI-CSL/libpoly/commit/ce7e620c54bd907200ce8b11812d123bf5f4ec8e
This resulted in our build getting stuck because it detected that the
patch had already been applied and was prompting the user what to do.
This commit removes that patch file and the corresponding command.
|
|
The Windows version of CaDiCaL does not require the `sys/resource.h`
file, so this commit removes that check. It does, however, require
linking against the Process Status API (psapi), because of a call to
`GetProcessMemoryInfo()`, so this commit adds that dependency for
Windows builds.
|
|
Commit f10087c3b347da6ef625a2ad92846551ad324d73 added new files that do
not compile without libpoly. This commit excludes those files when
building without libpoly. It also updates one of the regressions to
ignore a warning about approximate values in the model.
|
|
|
|
This commit copies the run-script-smtcomp-current* scripts to run-script-smtcomp2021* to archive them.
|
|
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.
|
