| Age | Commit message (Collapse) | Author |
|---|
|
This PR adds variants for the CAD projection operator to use Lazard's projection operator.
|
|
Fixes #6788
|
|
This rewrites the word blasting function FpConverter::convert to be
easier to follow and read. It further cleans up several things.
This additionally prepares for allowing to convert incoming facts rather
than terms registered with theory FP. That is, when word blasting more
lazily, in preNotifyFact rather than in registerTerm.
|
|
This PR introduces a rewrite from (^ 2 t) to (pow2 t) in order to make use of the specialized pow2 solver.
One regression that expects an error when t is not a constant is changed accordingly.
|
|
This commit replaces (old) internal string kind names to match the API / smt2 standard names.
|
|
There's one spot left in issue #6453, that is the call to `std::allocator<T>::destroy` in `mkMetaKind`. And this commit fixes it.
|
|
In preparation for further changes in the printer.
|
|
This commit adds the remaining changes for a working and integrated `pow2` solver.
In particular, it adds a rewrite and a lemma that identify `pow2(x)` with `0` whenever `x<0`.
Regressions are added as well, including `pow2-native-0.smt2` that shows the semantics of `pow2` on negative values.
The next steps are new rewrites and and more lemma schemas.
|
|
We add the lemma x<=y --> pow2(x)<=pow2(y) to the pow2 solver.
Additionally, some renaming of variables is introduced for better clarity.
|
|
|
|
This commit adds the following new code coverage targets:
- coverage-reset: Resets the code coverage counters
- coverage: Generates code coverage report for all cvc5 executions since the
last coverage-reset
- coverage-test: This was previously the coverage target that runs the
tests and generates the coverage report (as used for
nightlies).
By using `make coverage-reset` and `make coverage` it is now possible to
generate coverage reports for arbitrary executions of cvc5.
|
|
The linear arithmetic solver was not robust to cases where a duplicate lemma is emitted. This leads to non-linear arithmetic not being called to check at full effort, leading to potential model soundness issues.
Fixes #6773.
|
|
This PR adds the actual implementation for the Lazard evaluation based on CoCoALib. It is only used if CoCoALib is available and falls back to a default libpoly-based implementation otherwise.
|
|
Fixes #6536
|
|
This PR adds implementations of functions from the pow2 solver, rewriter and type checker.
|
|
|
|
|
|
(#6790)
Fixes #6526
|
|
|
|
|
|
Recent experiments have shown that `--tear-down-incremental` is actually
not really helping anymore and it has always been a bit of a workaround.
It is also broken on current master. This commit removes the option.
|
|
This ensures that we don't apply lambda rewriting, which involves array value normalization, to lambda terms returned by TheoryModel::getValue.
This can significantly speed up our time to return function terms for getValue.
|
|
Unit tests are translated from https://github.com/cvc5/cvc5/blob/master/test/unit/api/op_black.cpp
to python.
The only thing that is not faithfully translated is that the `cpp` tests expect the template function `[getIndices](https://github.com/cvc5/cvc5/blob/master/src/api/cpp/cvc5.h#L841)` to fail when an inappropriate type is given to it, while in the [`python` API](https://github.com/cvc5/cvc5/blob/90d19f7cdbaf41e389bdcbd099471f658a35ce98/src/api/python/cvc5.pxi#L343) this function is not a template, but just tries every supported type.
For example, the following line is not translated:
https://github.com/cvc5/cvc5/blob/90d19f7cdbaf41e389bdcbd099471f658a35ce98/test/unit/api/op_black.cpp#L206
|
|
This PR adds the file int_blaster.cpp. Most of the functions are not yet implemented. Two main functions are implemented.
Additionally, code that will no longer be needed is removed from the BV rewriter.
|
|
This removes the d_performNotify flag from equality engine which was supposedly used to guard a very old dependency concerning notifications during initialization. We are now robust to this and hence the flag can be removed.
|
|
Fixes #6699.
|
|
Fixes #6690.
|
|
This PR translates the cpp API unit tests about results to python.
The original cpp file is: https://github.com/cvc5/cvc5/blob/master/test/unit/api/result_black.cpp
The translation made rise to one addition to the python API:
The UnknownExplanation object from the cpp API was represented by a string in the python API.
Now we have a more faithful representation, as an enum.
|
|
Fixes #6776.
Our computation of when a regular expression was constant did not account for when ITE was embedded in an RE, leading to an unsound rewrite.
That benchmark now gives:
(error "Regular expression variables are not supported.")
|
|
This adds fields to equality engine setup information which will be used to hook up theories to the central equality engine.
This PR does not impact any behavior.
This is in preparation for the central equality engine.
|
|
|
|
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)...
|
