| Age | Commit message (Collapse) | Author |
|---|
|
|
|
strings (#4702)
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
|
|
With this PR, we now support a preliminary draft of a theory of sequences.
This PR adds front end support for sequences in the smt2 parser, in the new API, adds regressions and unit tests for them.
As discussed offline, many of the string kinds are given a sequence version in the external API, but not in the internal one. This means that a special case for such kinds, getKindHelper was added to Term.
We do not yet support proper smt2 printing of sequences, which will require access to this code for Kind conversions (to distinguish e.g. str.++ from seq.++).
|
|
|
|
This commit removes support for SWIG bindings for the legacy API. The
bindings were already broken by 19054b3b1d427e662d30d4322df2b2f2361353da
and we are not planning on using SWIG for the Java API for the new API.
|
|
|
|
Adds a fix for mkPurifySkolem and introduces new interfaces in preparation for arithmetic operator elimination and term formula removal proofs.
|
|
Previously, the proof rule checkers were run on witness form for convenience. However, it is more flexible for the sake of the internal calculus to run on Skolem forms. The main reason is that the conversion to/from witness form does not preserve terms that contain witness. Our preprocessing steps rely on using witness terms. This design change additionally simplifies a lot of the code of the builtin proof rule checker.
Instead, witness forms can be queried on an as-needed basis, e.g. in MACRO_SR_PRED_TRANSFORM.
|
|
Adds utility for updating proof nodes. The module for post-processing proof nodes in the SmtEngine for the sake of proof conversion to external formats will build on this utility.
Requires #4617.
|
|
This omits certain inference schemas (sum and bitwise lemmas) which depends on an option that will be added later.
|
|
This commit adds testing infrastructure for LFSC signatures that is
enabled when CVC4 is configured with LFSC. The testing infrastructure
adopts run_test.py from https://github.com/CVC4/LFSC with minor
modifications (mainly adding support for a list of include directories
that are searched to resolve *.plf dependencies). The commit uses the
existing examples and test files from proofs/signatures as the initial
set of tests.
Co-authored-by: Alex Ozdemir aozdemir@hmc.edu
|
|
Towards theory of sequences.
This makes the strings solver handle seq.unit, which requires two new inferences and updates to its model construction.
It also fixes a bug in the best content heuristic, which previously failed to update the best score.
|
|
This will be required to separate "evaluation steps" from "rewrite steps" when reconstructing proofs of rewrites.
|
|
Proof checking failures revealed that we are not rewriting witness for Boolean variables (witness ((x Bool)) x) ---> true and (witness ((x Bool)) (not x)) ---> false.
Also adds 2 assertions that are required for elimination (witness ((x T)) (= x t)) ---> t. These assertions should always hold due to the witness terms we construct.
|
|
Fixes #4674.
|
|
|
|
|
|
fmfBound (#4673)
There was a strategy in place for alternating which rounds quantifier instantiation would run on when --fmf-bound is enabled.
However, this made it so that in some cases, no instantiation strategy would be applied, if e.g. fmfBound was enabled but no quantified formulas were handled by that strategy.
It is not clear if this strategy is a good idea, considering all use cases of quantifiers, and hence this PR deletes this block of code.
This makes it so that several eqrange benchmarks are answered "unsat" quickly.
|
|
This is the first step of adding Interpolation. The whole change will be adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack.
The first step creates the API framework, while omits the implementation for getting interpolation.
|
|
|
|
Towards merging iand branch to master. This adds internal support for an "integer AND" operator.
|
|
This commit makes the ExprManager constructor private and updates the
initialization of subsolvers, unit tests, and system tests accordingly.
This is a step towards making options part of SmtEngine instead of
NodeManager.
|
|
This commit ports over the sort_black tests to the pytest infrastructure to test the Python bindings. It also adds missing functionality that was revealed during the testing.
|
|
Commit ccd4500 modified the unit test
node_algorithm_black. It added d_bvTypeNode as a data member to the
class and initialized it in setUp() but did not free it in
tearDown(), which set off ASan. This commit fixes tearDown() to free
d_bvTypeNode.
Marking this as major because it should fix the nightlies.
|
|
There were two issues related to RE in bodies of re.* that accepted the empty string that led to non-termination in the rewriter for regular expressions.
This also improves trace messages for simpleRegExpConsume.
Fixes #4662.
|
|
This PR introduces proof rules for arithmetic and their checker.
The code is dead, since these rules are never used.
|
|
This commit extends the API to support the retrieval of heap/nil term
when separation logic is used and changes the corresponding system test
accordingly. This commit is in preparation of making the constructor of
`ExprManager` private.
|
|
This PR adds support for indexed operators (such as extract) to getOperatorsMap in node_algorithm.cpp. The corresponding test is augmented accordingly.
|
|
|
|
We no longer support sygus v1 inputs. This PR removes support for sygus v1 (as well as a deprecated "z3str" variant of smt lib 2 which is subsumed by the new strings standard).
As mentioned in the release notes, CVC4 1.8 supports a conversion from sygus v1 to v2 script.
This removal is required for further updates to the new API. Further infrastructure (e.g. the sygus print callback) will be removed in a separate PR.
FYI @abdoo8080 .
|
|
only (#4649)
Previously, this option disabled/enabled the entire non-linear solver. This is in preparation for new CAD techniques.
I am intentionally not renaming "--nl-ext" to e.g. "--nl-inc-lin" for the sake of not breaking user configurations.
It makes some minor changes to clean the interface in a few places and to not enable the non-linear solver in linear logics.
|
|
When I created the PR for 733083c, it
did not contain the change from "" -> "-prerelease" because at the
time master still had CVC4_EXTRAVERSION set to "-prerelease". This
commit fixes CVC4_EXTRAVERSION.
|
|
Fixes #4644. This commit fixes an issue where the set `d_unconstrained`
in the unconstrained simplification pass was not computed correctly. The
problem was that visiting the same term multiple times did not remove
the variables appearing in that term from the visited-once set. A simple
example that triggers the issue is the following:
```
(set-logic ALL)
(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (not (= a b)))
(assert (= a (= a b)))
(check-sat)
```
After running `UnconstrainedSimplifier::visitAll()` on both assertions,
we end up with `[b]` as our `d_unconstrained` set. We end up inferring
the substitution `(= a b) --> b` and get `(not b)` and `b`, which is
unsat even though the original problem is sat.
This commit fixes the issue by visiting all the children of a node if we
visit a node for a second time. This makes sure that we remove any
children from the visisted-once set.
|
|
Main feature added is the mkScope interface, which is agnostic to symmetry of (dis)equalities.
It also adds a check for cyclic proofs when using the interface ProofNodeManager::updateNode.
Note that an earlier version of this method was agnostics to predicates vs Boolean equality with constants. This is no longer required.
|
|
This removes obsolete examples for the old API in preparation of making
the old API private. Examples for the new API are renamed from
*-new.cpp to *.cpp.
|
|
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.
|
|
This will be used for a number of purposes, including tracking proofs for rewriting and preprocessing.
|
|
|
|
(#4612)
|
|
Adds proof-new as an option. This is required for adding code that is guarded by this option while we are in the process of merging work on the new proofs infrastructure.
Enabling the option currently throws an option exception.
|
|
Fixes #4636.
This adds transcendental function kinds to the list of unevaluated operators (operators that don't necessarily rewrite to constants when applied to constant children). One consequence of this is that when models are enabled, we cannot solve for equations like (= a (cos b)), since the value of (cos b) is not necessarily evaluable, and hence must be approximated. As a result, we answer the benchmark on #4636 instead of generating an incorrect model (when models are enabled). When models are disabled, we answer "sat". A regression had a similar issue which happened to be succeeding. I've added --no-check-models to this regression (or otherwise we would answer unknown for this benchmark).
|
|
The help message of --bv-print-consts-as-indexed-symbols seems wrong to me, and this PR suggests a fix.
|
|
This commit rips the traversal machinery out of Int-to-Bv, replacing it with traversal iterators.
Also, cleaned `childrenTypesChanged` a bit.
While basically I just cut out some lines, the diff is rather messy (I think the diffing tool doesn't like indentation changes).
|
|
|
|
In preparation for coarse-grained rule for re-elim to be used by the solver and proof checker.
|
|
This design simplifies a number of issues and makes the PRefProofGenerator class obsolete.
|
|
Adds scripts submitted to CASC competition.
Note that this version of CVC4 submitted to CASC was modified to allow models when --sort-inference is enabled, since model output is required.
|
|
This makes it so that methods for constructing term registration lemmas are made into static methods, so that they can be used by both the term registry and proof checker.
|
|
Towards theory of sequences.
This PR also adds support for sequences in default sygus grammars.
Also removes an interface for mkEmptyWord which doesn't have an equivalent for sequences.
|
|
This class will be undergoing further refactoring for the sake of proofs.
This also makes several classes of skolems context-independent instead of user-context-dependent, since this is the expected policy for skolems. Note these skolems will eventually be incorporated into the SkolemManager utility.
|
