| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This reverts commit c3b24d9aa9d7dc80f870fb578e0a27176341fadc.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
* Merge branch 'master' into lira-pf-arith-pred
* Shorten reify_arith_pred, thanks Yoni!
Use recursion!
* typo
|
|
* LIRA sig: int, real terms, and conversions
* Address Yoni's comments.
* Better description of "reify" functions
* explicit (rather than implicit) `fail` when reifying integer division
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
|
|
|
|
|
|
apps (#3605)
|
|
Regression `regress2/strings/issue3203.smt2` is currently timing out
depending on the version of the libraries loaded (see #3606 for more
info). This commit temporarily disables the regression to get the
nightlies to pass again.
|
|
Fixes #3586. On macOS, `size_t` resolves to `unsigned long` whereas `uint64_t`
resolves to `unsigned long long`. Even though the types have the same bit-width
and signedness, they are not considered the same type. This caused issues with
`Attribute`s that store `size_t` values because we only specialized the
`getTable()` struct for `uint64_t`. This commit changes the specialization to
work for arbitrary unsigned integer types of at most 64-bit. It does that by
generalizing the specialization of `getTable()` and by implementing a
`KindValueToTableValueMapping` for unsigned integer attributes of up to 64-bit
that casts integers between the attributes bit-width and `uint64_t`.
|
|
|
|
|
|
|
|
|
|
This commit optimizes the `str.substr` reduction by replacing the
if-then-else term for the length of the suffix `len(sk2) = ite(len(s) >=
n+m, len(s) - (n + m), 0)` with `(len(sk2) = len(s) - (n + m) v
len(sk2) = 0) ^ len(skt) <= m`. Experiments have shown that the latter
encoding is more efficient.
|
|
|
|
* rewrote set cardinality for finite-types
* small changes and format
|
|
|
|
|
|
Recently, finite model finding via uninterpreted sorts was decoupled from finite bound inference techniques (the BoundedIntegers module in theory/quantifiers/fmf/). This module assumed that finite model finding was enabled in one place. This fixes the issue by adding an additional check. This fixes a model unsoundness issue where bounds on an uninterpreted sort were not being enforced.
This fixes #3587.
|
|
* Bugfix: convert ifte arms to formulas for printing
We have two kinds of ITEs in our LFSC proofs:
* ite: for sort-typed expressions
* ifte: for formulas
Say that we have a Bool-sorted ITE. We had machinery for emitting an
`ifte` for it, but this machinery didn't actually convert the arms of
the ITE into formulas... Facepalm.
Fixed now.
* Test the lifting of ITEs from arithmetic.
This test verifies that booleans ITEs are correctly lifted to formula
ITEs in LRA proofs.
It used to fail, but now passes.
* clang-format
* Typos.
* Add test to CMake
* Set --check-proofs in test
* Address Yoni
* Expand printsAsBool documentation
* Assert ITE typing soundness
* Assert a subtype relation for ITEs, not equality
* Update src/proof/arith_proof.h
Thanks Yoni!
Co-Authored-By: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
|
|
Type rules, parsing and printing, basic rewriting including constant evaluation, reduction for string reverse (`str.rev`).
Also improves support in a few places for tolower/toupper.
|
|
Signed-off-by: Simon Dierl <simon.dierl@cs.tu-dortmund.de>
|
|
|
|
transcendentals (#3577)
|
|
Fixes #3536. The type checker for the chain operator was calling the
rewriter. However, the floating-point rewriter was expecting
`TheoryFp::expandDefinition()` to be applied before rewriting. If the
chain operator had subterms that were supposed to be removed by
`TheoryFp::expandDefinition()`, the FP rewriter was throwing an
exception. This commit fixes the issue by not calling the full rewriter
in the type checker but by just expanding the chain operator. This is a
bit less efficient than before because the rewriter does not cache the
result of expanding the chain operator anymore but assuming that there
are no long chains, the performance impact should be negligible. It also
seemed like a reasonable assumption that the rewriter can expect to run
after `expandDefinition()` because otherwise the rewriter has to expand
definitions, which may be too restrictive.
|
|
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.
|
|
Currently we can't parse constant arrays that store real values that are given as rationals `(/ n m)`. We throw a spurious parse error for `((as const (Array Int Real)) (/ 1 3))`, indicating that the argument of the array is not constant. This is caused by the fact that `(/ 1 3)` is parsed as a *division* term not a rational value.
This adds a special case to constant array construction so that we compute the result of a constant division instead of using the division term `(/ n m)` when constructing an array constant.
|
|
Improves performance on ground conjectures with recursive functions. We use the evalutator to (partially) evaluate bodies of recursive functions, instead of relying on substitution+rewriting.
|
|
This extends the core model building algorithm in CVC4 with "assignment exclusion sets". This functionality is useful for assigning values to terms of finite type that have specific restrictions on what their value cannot be.
In detail, previously, all unassigned terms of finite type were always assigned the first term in the type enumeration. This is done since it is assumed that theories (e.g. datatypes) always do enough work to ensure that *arbitrary* values can be assigned to terms of finite type, and *fresh* values can be assigned to terms of infinite type. However, there are compelling cases (sets+cardinality for finite element types) where one may want to impose restrictions on what values can be assigned to terms of finite types. Thus, we now provide `setAssignmentExclusionSet` as a way of communicating these restrictions.
This commit also refactors a few parts of `TheoryEngineModelBuilder::buildModel` to be clearer, in particular by adding a few helper functions, and by caching certain information early in the function instead of recomputing it.
This is work towards #1123.
|
|
Support ackermannization on uninterpreted sorts in BV. For uninterpreted sorts, we create a bit-vector sort to replace it. For an uninterpreted sort `S`, if the number of variables within sort `S` is `n`, the replacing bit-vector will have size (log n)+1.
|
