| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This PR adds missing API functions from the cpp Term API to the python API.
Corresponding tests are translated from term_black.cpp.
|
|
|
|
|
|
This is the last test file that we move from the old directory to the new one, and so the old directory is deleted.
|
|
This PR fixes the driver which used an incorrect variable name in competition mode.
|
|
Fixes cases of satisfiable unsat cores when proofs are enabled.
Unfortunately, this bug was also preventing us from doing the final scope check for all proof checking. As this was not being tested, this PR uncovers that proof checking is now failing on 6 regressions. I'm disabling proof checking here and will address these issues on later PRs.
|
|
Fixes #6643. The STRINGS_CTN_DECOMPOSE inference is always a conflict
but we sometimes sent it as an inference. To make sure that the
inference manager actually recognizes the inference as a conflict, this
commit ensures that the conclusion is always false and modifies the
explanation accordingly.
|
|
This PR removes the next heavily specialized template function Options::operator[] in favor of direct access to the option data.
|
|
This PR moves options wrapper functions out of the Options class. These wrapper functions are meant to be called by "external" code that should not access the options modules. This PR thereby significantly reduces the interface of the Options class.
|
|
This PR fixes a subtle issue with double negations when producing proofs in the circuit propagator.
Adds the test case as a new regression, as well as some similar instances.
Fixes cvc5/cvc5-projects#277.
|
|
Recent changes introduced issues when libpoly is disabled.
|
|
This PR removes the next two heavily specialized template functions. Both Options::assign() and Options::assignBool() are only used within options.cpp now and there is thus no reason to keep them in the public interface. Furthermore, we can just make them properly named functions instead of template functions.
|
|
This PR abandons the attempt to do the cleanup in a single rebase command, and instead squashes the old commits manually. The current solution does not handle conflicts properly. The new approach (which seems to be more robust) proceeds as follows (to squash $first..$last):
- checkout $last
- soft reset to $first (checkout $first, but keep changes in working copy)
- commit to squashed commit
- cherry-pick $last..HEAD from main branch
|
|
Fixes #6661. The option `--strings-inm` could be used to ignore negative
membership constraints. However, this option made the string solver
model-unsound or produced incorrect models if the user provided a
benchmark that actually contained negative membership constraints. The
solver did not check for negative membership constraints and did not
warn the user about them. Because the option is not really being used,
this commit removes it.
|
|
This migrates page https://cvc4.github.io/input-languages.
|
|
|
|
This commit makes the following additions, in order to sync the python API with the cpp API.
1. adding `getName` functions to datatypes related classes
2. allowing `mkDatatypeSorts` with 1 or 2 arguments (previously allowed only 2).
3. In case there is a second argument to `mkDatatypeSorts`, we make sure it is a set.
4. Corresponding changes to the tests.
|
|
With this PR, we use the central top-level substitutions instance in the ITE simplification preprocessing pass. Previously the ITE simplification pass maintained its own copy of the substitutions.
Since the top-level substitutions now are the authority on models, this led to model failures after this change: ac8cf53#diff-30677c5a1752b1d0e83ef25fd2cfb8949576ea42cf7821fe0ac00ebbd0122f8aL276.
This PR corrects the issue.
This is required for SMT-COMP.
|
|
Disables two regressions that have been timing out causing nightlies to fail.
|
|
This PR adds new is* functions from the cpp API to the python API.
In particular, it adds getFloatingPointValue() function from the cpp API.
A test (translated from term_black.cpp) is added.
getFloatingPointValue() returns a tuple, and so this requires importing an instance of tuples into cython.
|
|
This PR gets rid of the templated Options::ref() method (and all its specializations for every option).
|
|
This commit removes some of the options in the run scripts that are not
supported anymore: `--bv-div-zero-const` and `--rewrite-divk`. Both of
those options are effectively enabled by default in cvc5.
|
|
Following #6496 , this PR adds new getters to the python API, as well as tests for them. This makes toPythonObj simpler.
A future PR will add more getters to the python API.
Co-authored-by: Gereon Kremer nafur42@gmail.com
|
|
Fixes #6337 (the other benchmarks in this issue are either solved
correctly or time out after the changes in #6615) and fixes #5665.
While computing the model for a nested equivalence class containing
seq.unit, we were looking up the representative of the argument in
(seq.unit (seq.unit j)) and the representative was simpliy (seq.unit j). However, we had assigned (seq.unit 0) to (seq.unit j) earlier.
A second equivalence class of type (Seq (Seq Int)) and length 1 was
later assigned (seq.unit (seq.unit 0)) and we didn't detect that
(seq.unit (seq.unit j)) and (seq.unit (seq.unit 0)) have the same
value. This was incorrect because we do not allow assigning the same
value to different equivalence classes. In this case, it led to one of
the assertions being false.
This commit fixes the issues in two ways: it ensures that types are
processed in ascending order of nesting (e.g., (Seq Int) terms are
processed before (Seq (Seq Int)) terms) and it changes the procedure
to look up the representative in the model instead of the theory state
to take into account the model values assigned to the elements of
sequences.
cc @yoni206
|
|
This PR gets rid of the Options::set() method, replacing it by direct access to the options data.
This method was only used internally and did nothing except for resolving the options data from the option tag type via template specializations (via ref()), which is no longer necessary.
|
|
pushObjective => addObjective (#6634)
In order for OptimizationSolver to support pushing & popping,
we could remove popObjective because it might be difficult to handle cases like:
optSlv->pushObjective(...);
optSlv->push();
optSlv->popObjective();
optSlv->pop();
In this case we need to add back the popped objective...
If push/pop is supported, pop does not bring back objectives if you resetObjective
but it will revert the objs you add.
just like assertFormula and resetAssertions.
|
|
This PR fixes an issue in the python API for datatypes, and also introduces tests translated from https://github.com/cvc5/cvc5/blob/master/test/unit/api/datatype_api_black.cpp
The next PR will translate more tests and will also introduce missing functions in the python API for datatypes.
|
|
This PR replaces the templated Options::setDefault() methods by new non-templated free functions options::{module}::setDefault{option}().
These methods should be used instead of the common if (!set by user) { set option value } pattern.
|
|
This commit adds --no-jh-rlv-order to two string regressions that take
over 2 minutes to run in debug after #6613, which increases the overall
regression runtime significantly.
|
|
Fixes #5508. `STRINGS_CTN_DECOMPOSE` could be triggered multiple times
by the same term, which resulted in an assertion failure. This commit
returns immediately after the first conflict to avoid the assertion
failure.
|
|
Fixes #6620, fixes #6622. Fixes cvc5/cvc5-projects#254.
The benchmarks from the 2 issues timeout, a regression is added for the projects issue.
|
|
Fixes #6057. The reductions of `str.replace_re` and `str.replace_re_all`
were not correctly enforcing that the operations replace the _first_
occurrence of some regular expression in a string. This commit fixes the
issue by introducing a new operator `str.indexof_re(s, r, n)`, which,
analoguously to `str.indexof`, returns the index of the first match of
the regular expression `r` in `s`. The commit adds basic rewrites for
evaluating the operator as well as its reduction. Additionally, it
converts the reductions of `str.replace_re` and `str.replace_re_all` to
use that new operator. This simplifies the reductions of the two
operators and ensures that the semantics are consistent between the two.
|
|
Lexicographic optimizations: Optimize the objectives one-by-one, in the order they are pushed.
Pareto optimizations: Optimize the objectives to the extend that further optimization on any objective will worsen the other objective.
Units tests are of course added.
Lexicographic optimization is using iterative implementation, pretty similar to the naive box optimization.
|
|
This removes namespace theory from proof utilities, and moves MethodId to its own file in src/proof/.
|
|
Fixes a solution soundness issue caused by allowing ineligible terms of kind BOOLEAN_TERM_VARIABLE to appear in instantiations.
This also corrects the expected solution on a benchmark that had an incorrect status.
Fixes #6603.
|
|
Fixes 2nd benchmark from #6605.
|
|
This is to make it consistent with the name of the SMT-LIB operator
(fp.add).
|
|
This commit fixes an assertion failure in the rewriter on some of the
SMT-LIB QF_ABVFP benchmarks (the regression in this commit is the
minified version of
`non_incremental/QF_ABVFP/20170428-Liew-KLEE/imperial_gsl_benchmarks_statistics_klee.x86_64/query.14.smt2`).
The problem was that after applying the `BvComp` rewrite, the bit-vector
rewriter was returning `REWRITE_DONE` instead of `REWRITE_AGAIN`. The
rewrite simplifies expressions of the form `bvcomp(t, c)` where `c` is a
constant of bit-width 1. If `c` is zero, then the rewrite returns
`bvnot(t)`. This node can potentially be rewritten further, e.g., if `t`
is `bvnot(x)`. This commit fixes the response and adds the corresponding
tests.
|
|
Add support for box optimization -- independently optimize each goal as if the other goals do not exist.
Single minimize() / maximize() now maintains the pushed / popped context.
Of course unit tests are here as well.
|
|
Fixes an oversight from #6601.
|
|
This enables the new implementation of justification heuristic by default.
Fixes #5454, fixes #5785. Fixes wishues 114, 115, 149, 160.
|
|
This PR follows a suggestions of @ajreynol to use public references instead of getter functions to access the individual option modules.
|
|
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 PR adds (most of) the existing examples to the documentation, and does some other minor updates on the documentation. Some details:
- for consistency, all cpp examples are moved from examples/api to examples/api/cpp
- add capabilities for SMT-LIB examples, and two simple smt2 examples
- more docs/examples/*.rst files
- two new documentation categories: installation (how to obtain, compile and install cvc5) and binary (about the cvc5 binary)
|
|
This PR fixes a type mixup (the usual long vs long long mixup on macos systems) in the unit tests for the new api::Term getters.
Fixes #6594.
|
|
This PR reduces the disk size of the docs generated by make sphinx-gh.
Apart from reformatting the cmake source, we now not only remove the _sources folder, but also .doctrees (essentially the sphinx cache) and _static/fonts/ (the fonts that are actually used live in _static/css/fonts).
In combination, this now reduces the disk size from about 20MB (sphinx) to less than 6MB (sphinx-gh).
Furthermore this PR only uploads the generated documentation if it differs from whatever we currently have for master.
This is relevant to make the docs-ci repository smaller (which already has more than 5GB...)
|
|
|
|
Fixes #6453. This commit replaces all calls to std::allocator with calls to
std::allocator_traits. Strictly speaking, allocate() and deallocate() are
not deprecated but the commit replaces them for uniformity.
|
|
Currently, when configuring cvc5 with Java bindings, CMake complains
about `get_filename_component(CVC5_JNI_PATH ${CVC5_JAR_PATH} DIRECTORY)`
not using the correct number of arguments in the Java unit tests. The
issue is that `${CVC5_JAR_PATH}` is empty. The value of
`${CVC5_JAR_PATH}` was computed in the Java API bindings but then not
shared with the rest of the build system. Because `${CVC5_JAR_PATH}` is
not used anywhere else, this commit moves the computation of
`${CVC5_JAR_PATH}` to the unit tests. The commit also ensures that the
API subdirectories are processed before the test subdirectories.
|
