| Age | Commit message (Collapse) | Author |
|---|
|
When testing the API examples, Python examples were not included. This
commit changes that and fixes multiple minor issues that came up once
the tests were enabled:
- It adds `Solver::supportsFloatingPoint()` as an API method that
returns whether CVC4 is configured to support floating-point numbers
or not (this is useful for failing gracefully when floating-point
support is not available, e.g. in the case of our floating-point
example).
- It updates the `expections.py` example to use the new API.
- It fixes the `sygus-fun.py` example. The example was passing a _set_
of non-terminals to `Solver::mkSygusGrammar()` but the order in which
the non-terminals are passed in matters because the first non-terminal
is considered to be the starting terminal. The commit also updates the
documentation of that function.
- It fixes the Python API for datatypes. The `__getitem__` function had
a typo and the `datatypes.py` example was crashing as a result.
|
|
This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure.
It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).
|
|
equal selects (#4981)
The implementation of --ackermann mishandled selects in a subtle way:
If select is applied to two syntactically different arrays (that may be semantically equal), the ackermann preprocessing failed to generate the "all arguments equal implies terms equal" lemmas.
The problem is that we used the first argument (that is: the array) as lookup to identify terms that need to be considered for these lemmas. Instead we now use their operator (select) just like for uninterpreted function applications.
Fixes #4957 . Also adds a regression.
|
|
This PR adds support for incremental solving in bv_to_int.
This amounts to:
using context dependent data structures
adding a test
In addition, we check for parametrized operations in a more robust way (using kind::metakind::PARAMETERIZED) and rename some tests for convenience.
|
|
This PR makes two simultaneous changes:
The new API uses Node-level DType instead of Expr-level Datatype. This required converting 2 of the last remaining calls in the parser that used Expr to use the new API.
Internally constructed datatypes (e.g. for sygus) use Node-level DType instead of Expr-level Datatype. Note this required moving a block of code for handling a corner case of sygus from Datatype -> DType.
This PR removes :
ExprManger::mkDatatypeType.
The Expr-level datatype itself. This PR removes all references to its include file.
It also updates one remaining unit test from Expr -> Node.
This PR will enable further removal of other datatype-specific things in the Expr layer.
|
|
|
|
arithmetic (#4930)
This PR activates the use of the relevance manager in TheoryEngine and makes use of it (via Valuation) in the non-linear extension in arith. It removes a deprecated hack (addTautology) for doing this.
This addresses CVC4/cvc4-projects#113.
Note that the best method for relevance is interleaving, where roughly you gain on SMT-LIB:
QF_NIA: +484-53 unsat +792-440 sat
QF_NRA: +32-19 unsat +57-23 sat
However, this PR does not (yet) enable this method by default.
Note that more work is necessary to determine which lemmas require NEEDS_JUSTIFY, this PR identifies 2 cases of lemmas that need justification (skolemization and strings reductions). Regardless, the use of the relevance manager is limited to non-linear arithmetic for now, which is only able to answer "sat" when only arithmetic is present in assertions.
|
|
We now separate APPLY_UF and HO_APPLY. We do not generate care pairs based on comparing APPLY_UF terms with HO_APPLY terms, which led to type errors previously.
Fixes #4990.
|
|
str.at expands to str.substr, thus this benchmark (may) require strings-exp if things do not rewrite/preprocess. This triggers a regress0 failure on proof-new currently.
|
|
Fixes #4915. Previously, `str.substr` did not require `--strings-exp`.
However, when `--strings-exp` is not active, we do not send terms to the
extended solver for registration, which meant that `str.substr` was
never reduced. This commit adds `str.substr` to the operators that
require `--strings-exp`.
|
|
Changes the assertion that checks for the maximum cardinality of set models to an exception, following #4374.
Also cleans up the code around it: previously, the Rational was checked against LONG_MAX, converted to std::uint32_t and then stored into an unsigned. Now we use std::uint32_t all the way.
Fixes #4374.
|
|
In preparation of removing the old proof module, this commit changes the
regression runner to not add the flag --check-proofs anymore when
running the regressions.
|
|
Calling (reset) multiple times produced parsing problems (#4866) and could probably lead to all kinds of interesting issues.
In a nutshell, reset() failed to properly reset d_initialOptions (which is used to properly reset d_options) so that all options defaulted after the second call to reset().
This PR properly sets d_initialOptions after a reset (and the filename as well).
Fixes #4866.
|
|
```
(! sc (^ ...)
^ this is the identifier!
```
We require that side-conditions have an identifier. We usually provide
this identifier, but in this one case we did not.
The old lexer accepted the side condition without the identifier. The
new one does not.
|
|
This class is responsible for maintaining TheoryEngine and PropEngine and implementing the check-sat command. It also has an interface for processing/pushing the current assertions into the PropEngine.
This class will be used directly by other extension solvers (for abduction, interpolation, qe, sygus, etc.).
|
|
Fixes #4790.
Fixes two bugs in the decision tree learning solver for sygus, one involving evaluation of "templated" enumerators, and one involving ITE strategies where child types are different than the root.
|
|
This PR would add an option to only build the CVC4 library and not the parser or executable. This can be used for projects that only intend to use CVC4 through the API.
It seems to be working now, but it's not necessarily the cleanest solution. In particular, if you'd like the polarity to be different I'm happy to change that. Polarity meaning something like "${WITH_BINARY}" STREQUAL "YES" instead of NOT "${LIB_ONLY} STREQUAL "YES" which is admittedly a little strange.
|
|
Fixes regress1.
|
|
This splits a utility for tracking the "basic" state of the SmtEngine. This class tracks its high-level state, including the "SMT mode", last/expected status and manages the contexts. It is not responsible more detailed state information (e.g. the assertions).
|
|
In preparation for eliminating the Expr-level datatype.
|
|
This further removes redundant API functions with a `const char*`
parameter. These are redundant (and can create ambiguity) since they
have `const string&` counterparts.
|
|
This updates remaining uses of the Expr-level Datatype that are not related to their creation / memory management in ExprManager.
This required updating a unit test from Expr -> Node.
|
|
This refactors the regular expression operation class so that some of its key methods are static, so that they can used by both the regular expression solver and the strings proof checker.
Notice that many cases of regular expression unfolding are deleted by this PR, since they are unnecessary. This is due to the fact that all regular expression memberships are rewritten except those whose RHS are re.++ or re.*.
|
|
We have had a few issues where essentially users misinterpreted the error message about which types of exponents are supported for (^ base exp). Given that this is rewritten to a multiplication of length exp, we only support reasonably small natural numbers.
This PR improves the error message.
Fixes #4692
|
|
This is an interface to get the instantiated parametric datatype constructor operator to apply when the type of this operator cannot be inferred without a cast.
This is required for eliminating the Expr-level datatype and calls to ExprManager from the parsers.
|
|
|
|
Fixes #4820. The performance issue was caused by
0988217562006d3f59e01dc261f39121df6d75f5. That commit introduced an
option (`--strings-len-conc`) that optionally moves the length
constraint for skolems to the conclusion of an inference instead of
making it part of the term registration. However, for
`DEQ_DISL_STRINGS_SPLIT`, we were only asserting that `LENGTH_GEQ_ONE`
in the case where this option was not enabled, instead of asserting that
the length of the skolem is equal to the component on the other side of
the disequality. This lead to an infinite loop of inferences because we
effectively were just splitting a component into two skolems and the
only restriction was that the first one was non-empty. We guessed the
second skolem to be empty, so the first skolem was equal to the
component, the skolem was marked congruent, and we ended up with the
same normal form as before.
The commit fixes the issue by adding an argument to
`getDecomposeConclusion()` that specifies whether to add the length
constraint or not. This option is used to always add the length
constraint in the case of `DEQ_DISL_STRINGS_SPLIT`.
|
|
Fixes #4701. That benchmark now times out.
|
|
This commit extends the Python API with support for SyGuS functionality.
This required the addition of a nullary constructor for `Grammar` in the C++ API.
A unit test is also included, and is a translation of the corresponding C++ API unit test.
Examples are not added yet, but are ready and planned for a next PR (in order to keep this one shorter).
|
|
Commit 9678f58a7fedab4fc061761c58382f4023686108 added front end support
for sequences. This commit extends that support to the Python API. It
also adds simple C++ and Python examples that demonstrate how the API
works for sequences.
|
|
Fixes #4759 .
Also refactors this method.
|
|
This PR adds support for seq.nth operator by eliminating it during expandDefinitions, based on sub-sequences.
Tests that use this operator are also included.
|
|
There are 3 Boolean flags for OutputChannel::lemma, and plans to add another for relevance.
This makes them into a enum.
|
|
The current arith proof machinery can prove conflicts which are
explained by assumptions and tightened assumptions.
Previously we verified that the conflict constraint was explained in
terms of assumptions and tightened assumptions, before trying to
save/produce a proof.
We did not verify that the negated constraint was an assumption or
tightened assumption.
This caused us to attempt to prove conflicts around constraints whose
negations where proven by general means (in the case of #4714, by the
equality engine), which the proof machinery was not prepared to handle.
This PR also checks that the negate constraint is an assumption or
tightened assumption, before saving the proof.
Thanks, Gereon, for doing the initial investigation into this!
fixes 4714
Co-authored-by: Gereon Kremer <nafur42@gmail.com>
|
|
|
|
* wait() deadlocks if the OS pipe fills
* communicate() does not
This is essentially a duplicate of [this](https://github.com/CVC4/LFSC/pull/38).
|
|
This replaces the old options listener infrastructure with the OptionsManager introduced in cb8d041.
It eliminates a "beforeSearchListener", which was a custom way of some options throwing a modal exception if they were set after initialization. Now all options are consistent: no option can be set after initialization.
It also moves managed ostream objects to the OptionsManager.
@mpreiner The next step will be to remove the "notifies" field from the Options build system and then proceed with cleaning src/options/.
|
|
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
|
|
This commit integrates LibPoly into CVC4. It adds `contrib/get-poly`, adds it to the configure script, cmake and places where CVC4 inspects its own build configuration.
Furthermore, it adds `CVC4::RealAlgebraicNumber` (which wraps `poly::AlgebraicNumber`) including some basic unit tests and some utilities.
|
|
This commit changes SmtEngine::assertFormula() to use Nodes rather
than Exprs and changes AssertionList to be Node-based. This is
work towards removing the Expr layer.
|
|
This commit changes UninterpretedConstant to use TypeNode instead of
Type.
|
|
This regression output was unexpected previously since conflict-based instantiation caught a conflict early, this makes it so that the output of this regression should be deterministic.
Fixes regress1.
|
|
This commit changes EmptySet to use TypeNode instead of Type.
|
|
This prints # instantiations per round (during solving) for each quantified formula with `--debug-inst`, giving output like this:
```
(num-instantiations myQuant1 1)
(num-instantiations myQuant2 1)
unsat
```
It also changes the default value of print-inst-full to match the behavior of unsat-cores vs unsat-cores-full (by default, nameless quantifiers are ignored).
It fixes an issue with qid, where mkVar was accidentally used instead of mkConst, leading to assertion failures in debug. Marking major since this fixes debug regress1.
|
|
Commit 64a7db86206aa0993f75446a3e7f77f3c0c023c6 introduced a caching
mechanism in `TheoryEngine::getExplanation()`. However, there seem to be
issues related to the timestamps of the explanations. This commit fixes
the issue by making the timestamp part of the cache. The change ensures
that explanations for a certain node never rely on other explanations
for that node with a later timestamp.
|
|
This commit changes ArrayStoreAll to use Node/TypeNode instead of
Expr/Type.
|
|
This makes an option --debug-sygus available to the user for tracing the sygus solver. For the classic max2 example the option is:
(sygus-enum 0)
(sygus-candidate (max 0))
(sygus-enum 0)
(sygus-enum 1)
(sygus-enum x)
(sygus-enum x)
(sygus-candidate (max x))
(sygus-enum x)
(sygus-enum y)
(sygus-enum y)
(sygus-candidate (max y))
(sygus-enum y)
(sygus-enum (+ x x))
(sygus-enum (+ x 1))
(sygus-enum (+ 1 1))
...
(sygus-enum (ite (<= x y) y 1))
(sygus-candidate (max (ite (<= x y) y 1)))
(sygus-enum (ite (<= x y) y 1))
(sygus-enum (ite (<= x y) y x))
(sygus-enum (ite (<= x y) y x))
(sygus-enum (ite (<= x y) y x))
(sygus-candidate (max (ite (<= x y) y x)))
unsat
(define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
Where sygus-enum denotes enumerated terms and sygus-candidate is one that passes a CEGIS refinement check.
|
|
This adds a new print format for instantiations --print-instantiations=num, which prints the total number of instantations of quantified formulas. This count is user-context-dependent, which is in sync with the existing print-instantiation format (list).
It also simplifies and improves printing of Instantiation Tries.
|
|
This adds basic support for string/sequence updating, which has a semantics that is length preserving.
|
|
This PR changes --solve-bv-as-int from a numerical option (specifying the granularity) to an enum (specifying the approach). Currently we support only two modes: OFF and SUM. Future PRs will add more modes.
The numerical value of the granularity is now captured by the new option --bvand-integer-granularity.
Tests are updated accordingly.
|
