| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This never impacted performance positively. Fixes #3997 and fixes #4015.
There was a folder that the symmetry breaker was used on regress1/sym. These are simple examples that show when it is possible to find symmetries in SMT; the symmetry breaker is not critical for solving these. For now I'm leaving them as regressions documenting possible benchmarks to target if we revisit this technique.
|
|
Fixes #4021.
We were previously constructing a malformed HO_APPLY as part of a subgoal for induction.
|
|
Fixes #4019.
This feature was never fully implemented.
|
|
Fixes #4001.
This assertion was more of a conjecture (stating that easy cases of miniscoping are already handled). However some option combinations can break this invariant, regardless the code should do the correct thing.
|
|
|
|
This commit adds tables in the rewriter that store which function should
be used to rewrite which kind. We have separate tables for `EQUAL`
because every theory has its own equality rewriter.
|
|
Fixes #3814. `CnfProof` has a stack of assertions that are being
converted to clauses. `CnfStream::ensureLiteral()` can result in clauses
being added to the SAT solver. When adding a clause, we require an
assertion that can be associated with the clause
(https://github.com/CVC4/CVC4/blob/ba6ade0fc3f4cd339885652bb9bf5c87113c498d/src/prop/minisat/core/Solver.cc#L471-L476).
However, in the issue that was reported, the stack was empty, resulting
in an assertion failure. This commit fixes the issue by setting the
current assertion to be the null node when a literal is being ensured
(and changing the proof code to update the assertion associated with a
literal if it is currently null). This should be ok since the clauses
are not inputs or lemmas (if they are, the assertion associated with the
clause will be updated).
|
|
|
|
Fixes #4028. `TheoryEngine`'s pointer was not updated to the new
`PropEngine` when resetting assertions. This commit fixes that. As far
as I can tell, this was the only class storing a `PropEngine*` that
isn't owned by `PropEngine`, so we should hopefully not have other
similar issues.
|
|
This fixes the case when all rows are inconsistent.
Fixes #3999.
|
|
|
|
Fixes #4010.
|
|
Calling (reset-assertions) in start mode was not handled correctly.
Additionally, when calling (check-sat) after (reset-assertions) after a
(check-sat) call that answered unsat, we answered unsat instead of sat.
This cleans up and fixes reset-assertions) handling.
|
|
Fixes #4003.
Protects against a (class of) nonsensical option combinations.
|
|
* Fix assertion in resolution bound inferences
* Format
* Minor
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
|
|
Also adds --sort-inference to this list, fixes #3936.
|
|
Fixes #3990.
|
|
|
|
Fixes #3803.
When non-linear arithmetic determines there is a model, then it should not send model values for multiplication terms that the linear solver assigned when abstracting (non-linear) multiplication. This avoids conflicts if the non-linear solver changed a value for a variable occurring in a non-linear monomial. This avoids check-model failures.
|
|
Fixes #3956 and fixes #3969.
|
|
|
|
Fixes #3953.
|
|
The BV-to-bool pass is implemented recursively.
This commit documents that.
We may want to change it at some point.
|
|
This pull request is an improvement to the bool-to-bv preprocessing pass. The existing pass is both too weak and too strong, depending on the circumstance. Throughout this description, "lower" refers to lowering a boolean to a bit-vector.
|
|
This option enables the sygus solver (previous name was ceGuidedInst, deprecated from CAV 15 specific approach).
It also improves when this option is set. In particular we ensure it is enabled when sygus is enabled for any reason.
|
|
|
|
Fixes #3947.
|
|
|
|
|
|
Fixes #3952 and fixes #3940 and fixes #3941 and fixes #3968.
|
|
Fixes #3959. It can happen that we generate a lemma that results in a
unit clause that matches a unit clause that was added as an input.
However, we are asserting that a unit clause can only be registered as
either one of them. This commit fixes the issue by only registering a
unit clause from a lemma if it is not already satisfied. I chose this
fix because the existing code doesn't seem to do anything (in terms of
solving) for the case where we have a unit clause that is already
satisfied because of an input unit clause.
|
|
Towards parser migration.
Beyond Datatypes, there are still a handful of calls to the ExprManager in the parsers.
This eliminates a few missing cases from TPTP and also inlines the access of ExprManager in the places its used.
|
|
Towards theory of sequences.
Also adds documentation to strncmp/rstrncmp and adds them to the Word interface.
|
|
This PR refactors and fixes how bounds are set for transcendental functions. The new code ensures that all transcendental function applications are given bounds. (Our previous failures to do so were hindering our ability to say "sat", due to NlModel::checkModel failures).
There were previously two issues on why transcendental function applications were not being assigned bounds:
"Slave" transcendental functions (e.g. those that we reduce via sin(t) = sin(y) ^ -pi <= y <= pi ^ y + 2*pi*N = t) were not being given bounds explicitly,
Transcendental functions that are congruent to others (e.g. f(x) where f(y) exists and x=y in the current context) were being ignored and hence not bound.
This PR clarifies the master/slave relationship that tracks which transcendental function applications have been purified, and furthermore tracks congruence classes.
The setting of bounds and the check-model is further simplified by setting bounds on the original terms, whereas the current code sets bounds on the model values of terms. In other words, previously if we had term sin(y) and y^M = c, then we'd set bounds for sin(c), whereas the new code sets the bound on sin(y) directly.
Fixes #3783. We answer unknown without an assertion failure on that benchmark now. Further work based on ignoring literals from internally generated lemmas is necessary for solving it sat.
|
|
Fixes #3944.
|
|
Fixes https://github.com/CVC4/cvc4-wishues/issues/9.
When communicating with CVC4 using pipes and the CVC language, it was not possible to determine when all the lines of a model have been printed.
This change adds begin and end markers as the example below:
```
MODEL BEGIN
x : INT = -3;
y : INT = 0;
z : INT = 0;
MODEL END;
```
|
|
Flattens a block of code and refactors the main check loop, will make it easier to incorporate new extensions.
It also avoids a needless call to check() for Relations when there are no relations constraints.
|
|
The new API does not use inheritence for Sorts. The current DatatypeDeclarationCommand uses DatatypeType, which inherits from Type. This commit simplifies the class DatatypeType -> Type and updates the necessary code (e.g. in the printers). Notice we are not yet converting commands Type -> Sort here.
It also makes the main call for constructing datatypes in the parser from DatatypeType -> api::Sort.
This is in preparation for converting Expr-level Datatype to Term-level DatatypeDecl in the parsers.
|
|
This removes the field "tester name" from the Expr-level and Term-level APIs. This field is an artifact of parsing and thus should be handled in the parsers.
This refactor uncovered an issue in our regressions, namely our smt version >= 2.6 was not strictly complaint, since the symbol is-cons was being automatically defined for testers of constructors cons. This disables this behavior when strict mode is enabled. It updates the regressions with this issue.
This is work towards parser migration.
|
|
The current sygus v2 called the parser's mkMututalDatatypeTypes function, which unecessarily created the datatype and bound its (internally generated) constructor/selector symbols in the symbol tables of the parser. This resolves this dependency.
The same issue also exists in the sygus v1 parser but is harder to resolve; I am leaving this for now since that code will be deleted in the next version of CVC4.
This is work towards the SyGuS API.
|
|
Fixes #3645.
|
|
Fixes #3914. The pass was only applicable to inputs with UFs that were
exclusively applied to single integer values. This limitation seems to
make the preprocessing pass not very useful in practice and it is
subsumed by our Ackermannization pass, which can remove UFs from more
complex inputs. Thus, this commit removes the preprocessing pass.
|
|
This rule is used when a bound on an integer expression is tightened
because of integer reasoning.
Before this rule was subsumed by IntHoleAP, a catch-all rule for integer
reasoning. We are now articulating IntTightenAP separately, because we
can produce proofs for it.
For IntHoleAP, we will have to omit a hole.
|
|
This reverts commit c360b3af4371cf871935a8bae96be5f8fecf741b.
|
|
This rule is used when a bound on an integer expression is tightened
because of integer reasoning.
Before this rule was subsumed by IntHoleAP, a catch-all rule for integer
reasoning. We are now articulating IntTightenAP separately, because we
can produce proofs for it.
For IntHoleAP, we will have to omit a hole.
|
|
This PR migrates a majority of the functionality of the parsers (cvc, tptp, smt2/sygus) to the new API. The main omitted functionality not addressed in this PR is the datatypes. Largely, the Expr-level Datatype is still used throughout.
Remaining tasks:
Migrate the Datatypes to the new API in cvc/smt2.
Eliminate the use of ExprManager::mkVar (with flags for DEFINED/GLOBAL).
For the latter, I have made a utility function in Parser::mkVar that captures all calls to this function. Notice that the existing mkVar/mkBoundVar/mkDefinedFun have been renamed to the more fitting names bindVar/bindBoundVar/bindDefinedFun etc.
Note: this PR contains no major code changes, each line of code should roughly correspond one-to-one with the changed version.
This fixes CVC4/cvc4-projects#77, fixes CVC4/cvc4-projects#78, fixes CVC4/cvc4-projects#80, fixes CVC4/cvc4-projects#85.
|
|
This is in preparation of fixing the issue we currently have with
reset-assertions. This also removes a competition hack for QF_LRA.
|
|
This reverts commit bbba915f44f9e75eaa6238a10ba667643dacb00b.
|
|
This is in preparation of fixing the issue we currently have with reset-assertions.
This also removes a competition hack for QF_LRA.
|
