| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
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.
|
|
This is further work towards decoupling the Expr layer from the Node layer.
This commit makes it so that ExprManager does memory management for Datatype while NodeManager maintains a list of DType.
As a reminder, the ownership policy (and level of indirection through DatatypeIndex) is necessary due to not being able to store Datatype within Node since this leads to circular dependencies in the Node AST.
|
|
This ensures that the Evaluator always returns the result of substitution + rewriting for constant substitutions.
This requires a few further extensions to the code, namely:
(1) Applying substutitions to operators,
(2) Reconstructing all nodes that fail to evaluate by taking into account evaluation of their children.
|
|
|
|
This would add tracing options to print the decision tree in [org-mode](https://orgmode.org/) format which can be viewed with emacs or [vim-orgmode](https://github.com/jceb/vim-orgmode).
In the raw format, the number of asterisks denote the decision level of a decision, and within a propagation node, the number of spaces denote the level. Most viewers render the asterisks as indented bullets.
There are some options for controlling verbosity:
`dtview` - prints the decisions (basic option)
`dtview::command` - also prints smt-lib commands as they're issued
`dtview::conflict` - also prints conflicts
`dtview::prop` - also prints propagations
Example usage:
`cvc4 -t dtview -t dtview::command -t dtview::conflict -t dtview::prop <example smt2 file> &> example-trace.org`
The resulting file when opened with an org-mode viewer has collapsible nodes, where "..." marks a node with children.
|
|
Fixes a bug where we don't return the partially evaluated version (for unevaluatable nodes). Also adds `NONLINEAR_MULT` whose semantics is identical to `MULT`.
|
|
In some SyGuS applications, the bottleneck is the rewriter. This PR makes a few simple optimizations to the core rewriter, namely:
(1) Minimize the overhead of `theoryOf` calls, which take about 10-15% of the runtime in the rewriter. This PR avoids many calls to `theoryOf` by the observation that nodes with zero children never rewrite, hence we can return the node itself immediately. Furthermore, the `theoryOf` call can be simplified to hardcode the context under which we were using it: get the theory (based on type) where due to the above, we can assume that the node is not a variable.
The one (negligible) change in behavior due to this change is that nodes with more than one child for which `isConst` returns true (this is limited to the case of `APPLY_CONSTRUCTOR` in datatypes) lookup their theory based on the Kind, not their type, which should always be the same theory unless a theory had a way of constructing constant nodes of a type belonging to another theory.
(2) Remove deprecated infrastrastructure for a "neverIsConst" function, which was adding about a 1% of the runtime for some SyGuS benchmarks.
This makes SyGuS for some sets of benchmarks roughly 3% faster.
|
|
|
|
|
|
|
|
The word-blasting function `FpConverter::convert` used a `std::stack` with `deque` as an underlying data structure (default) for node traversal. Previous experiments suggested that using `std::stack<T, std::deque<T>>` performs worse than using `std::vector<T>`, and we decided, as a guideline, to always use `std::vector` for stacks: https://github.com/CVC4/CVC4/wiki/Code-Style-Guidelines#stack.
This PR refactors `FpConverter::convert` to use `std::vector`. Runs on all incremental and non-incremental FP logics in SMT-LIB showed a slight improvement over the previous (`std::stack<T, std::deque<T>>`) implementation, and an even greater (albeit still slight) improvement over using `std::stack<T, std::vector<T>>`.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Fixes #3537.
This benchmark triggers a potential unsoundness caused by instantiating with an uninterpreted constant (which is unsound).
|
|
This commit changes theory rewriters to be non-static. This refactoring
is needed as a stepping stone to making our rewriter configurable: If we
have multiple solver objects with different rewrite configurations, we
cannot use `static` variables for the rewriter table in the BV rewriter
for example. It is also in line with our goal of getting rid of
singletons in general. Note that the `Rewriter` class is still a
singleton, which will be changed in a future commit.
|
|
|
|
|
