| Age | Commit message (Collapse) | Author |
|---|
|
Some internal inferences had a non-standard way of providing (disjunctive) reasons and a custom way of explaining them.
This PR simplifies the array solver so that its explanations are analogous to the other equality engine based theory solvers (strings, datatypes, sets, ...). This is done in preparation for the incorporation of the proof equality engine in arrays, which follows a standard design for reasons/explanations.
The performance impact on QF arrays is negligible
|
|
This option has model soundness issues (#4771) and moreover is overall worse performance on SMT-LIB {QF_ABV QF_ABVFP QF_ABVFPLRA QF_ALIA QF_ANIA QF_AUFBV QF_AUFLIA QF_AUFNIA QF_AX}:
Configuration #unsat time #sat time #solved #total
CVC4-072720_def 9428 9405.46 24932 16631.6 34360 35399
CVC4-072720_nalr1 9446 9536.41 24924 16146.3 34370 35399
where def = default, nalr1 = --no-arrays-lazy-rintro1.
Fixes #4771.
FYI @barrettcw
|
|
There are 3 Boolean flags for OutputChannel::lemma, and plans to add another for relevance.
This makes them into a enum.
|
|
This commit changes ArrayStoreAll to use Node/TypeNode instead of
Expr/Type.
|
|
This includes 4 changes:
Theory constructor takes a ProofNodeManager,
Theory::explain returns a TrustNode (of kind PROP_EXP),
Theory::expandDefinitions returns a TrustNode (of kind REWRITE),
Theory::ppRewrite returns a TrustNode (of kind REWRITE).
These are all currently planned updates to the interface of Theory.
This PR also connects some of the existing proof rule checkers into the proof checker, if one is provided to the constructor. It updates TheoryEngine and other places to process TrustNode in trivial ways (converting them into Node). These calls will later be updated as needed for proof support.
This PR is also contingent on the performance tests for proof-new on SMT-LIB.
|
|
This commit adds support for an eqrange predicate. (eqrange a b i j) is true if arrays a and b are equal on all indices within indices i and j, i.e., \forall k . i <= k <= j --> a[k] = b[k]. Requires option --arrays-exp to be enabled.
|
|
|
|
When we eliminate a variable x -> v during simplification, it may be the case that v contains "unevaluated" operators like forall, choice, etc. Thus, we do not produce correct models for such inputs unless simplification is disabled.
This PR ensures we only eliminate variables when v contains only evaluated operators.
Additionally, the kinds registered as unevaluated were slightly modified so that when we are in a logic like QF_LIA, there are no registered unevaluated operators, hence the check above is unnecessary. This is to minimize the performance impact of this change.
Fixes #4500.
|
|
This commit adds statistics for string rewrites. This is work towards proof
support in the string solver. At a high level, this commit adds a pointer to a
`SequenceStatistics` in the rewriters and modifies
`SequencesRewriter::returnRewrite()` to count the rewrites done. In practice,
to make this work requires a couple of changes, some of them temporary:
- We can't have a single `Rewriter` instance shared between different
`SmtEngine` instances anymore. Thus the `Rewriter` is now owned by the
`SmtEngine` and calling the rewriter retrieves the rewriter associated with
the current `SmtEngine`. This is a temporary workaround before we get rid of
singletons.
- Methods in the `SequencesRewriter` and the `StringsRewriter` are made
non-`static` because they need access to the statistics instance.
- `StringsEntail` now has non-`static` methods because it needs a reference to
the sequences rewriter that it can call.
- The interaction between the `StringsRewriter` and the `SequencesRewriter`
changed: the `StringsRewriter` is now a proper `TheoryRewriter` that inherits
from `SequencesRewriter` and calls its `postRewrite()` before applying its
own rewrites (this is essentially a reversal of roles from before: the
`SequencesRewriter` used to call `static` methods in the `StringsRewriter`).
- The theory rewriters are now owned by the individual theories. This design
mirrors the `EqualityEngine`s owned by the individual theories.
|
|
Until now, the `Rewriter` was responsible for creating `TheoryRewriter`
instances. This commit adds a method `mkTheoryRewriter()` that theories
override to create an instance of their corresponding theory rewriter.
The advantage is that the theories can pass additional information to
their theory rewriter (e.g. a statistics object).
|
|
Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally.
Co-authored-by: Clark Barrett <barrett@cs.stanford.edu>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Co-authored-by: makaimann <makaim@stanford.edu>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: AleksandarZeljic <zeljic@stanford.edu>
Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com>
Co-authored-by: Amalee <amaleewilson@gmail.com>
Co-authored-by: Scott Kovach <dskovach@gmail.com>
Co-authored-by: ntsis <nekuna@gmail.com>
|
|
|
|
This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`).
Fixes #3751.
|
|
|
|
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.
|
|
|
|
Detected with cppcheck static analyser, which said: (performance) Prefer
prefix ++/-- operators for non-primitive types. Reformat with clang-format
as needed.
Signed-off-by: Piotr Trojanek <piotr.trojanek@gmail.com>
|
|
|
|
Fixes 2887.
|
|
|
|
|
|
|
|
|
|
|
|
Since we are using C++11, we can replace the triple and quad classes
with std::tuple.
|
|
|
|
|
|
|
|
* Fixes --hide-zero-stats (and really skips the 0 values)
* Removes the additional newline after each statistic
* Introduces theory::getStatsPrefix(TheoryId) to generate consistent
prefixes for statistics based on the theory id
(e.g., THEORY_BV -> "theory::bv").
|
|
Adds missing override keywords.
|
|
|
|
|
|
|
|
Removing more miscellaneous throw specifiers.
|
|
|
|
|
|
This clarifies the memory ownership of EqProofs.
|
|
|
|
* Replacing __gnu_cxx::hash_map with std::unordered_map.
* Replacing __gnu_cxx::hash_set with std::unordered_set.
* Replacing __gnu_cxx::hash with std::hash.
* Adding missing includes.
|
|
Disable support for subrange and predicate subtypes (which were only partially supported previously).
|
|
|
|
cbqi, tptp parser), fix full saturation instantiation to not loop in rare case, update regressions, update casc scripts.
|
|
|
|
|
|
arrays).
|
|
|
|
argument.
|
|
This addresses Coverity issues:
- 1172154
- 1172156
- 1172157
- 1172158
- 1172159
- 1379612
- 1379612
- 1421430
- 1172166
- 1172144
- 1362709
- 1362696
- 1172145
- 1172147
- 1172148
- 1379610
- 1362772
- 1362676
- 1362704
- 1362749
- 1362876
- 1362843
- 1362837
- 1362881
- 1172223
- 1172155
|
|
|
|
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
|
