| Age | Commit message (Collapse) | Author |
|---|
|
This commit should fix the nightlies.
|
|
This makes the sygus-inference preprocessing pass avoid variable shadowing, which technically could happen by forcing unexpected options.
Fixes #4083.
|
|
(#4074)
Fixes #4068 and fixes #4085 and fixes #4063.
|
|
|
|
|
|
Postpone failure in bv-to-int preprocessing pass.
|
|
Fixes #4070. `TheoryStringsRewriter::rewriteConcatRegExp()` rewrites
`(a)* ++ (_)*` to `(_)*`. To do so, it checks whether the elements
preceding `(_)*` match the empty string using
`TheoryStringsRewriter::testConstStringInRegExp()`. However, this method
only expects to be called on constant regular expressions (i.e. regular
expressions without string variables). This commit adds a corresponding
check before calling `TheoryStringsRewriter::testConstStringInRegExp()`.
|
|
CVC4 supports `bv2nat` and `int2bv` to convert bit-vectors to/from
integers. Those operators are not standard. This commit only enables
those operators when parsing is non-strict and both bit-vectors and
integers are enabled in the logic. To achieve this, the commit
simplifies the handling of logics in the parser: Instead of defining a
separate `Logic` enum in the `Smt2` class, we simply use `LogicInfo`
directly.
|
|
Fixes #4086.
Quantifier instantiation involves two symbolic representations of infinities for real and int and was not handled correctly previously.
|
|
Fixes #4077. The master equality engine in `TheoryEngine` was being
created at SAT context level 1. If the context was popped to level zero
by `(reset-assertions)`, `true` and `false` were removed from the master
equality engine, which lead for example to `(= ((_ extract 3 3) x) (_
bv1 1))` and `(_ bv1 4)` being merged (this can be gathered from looking
at `-t equality`). This commit fixes the issue by postponing the global
context pushes until after the theory engine has been initialized.
|
|
Missed this one when real to int was disabled for quantifiers. Fixes regress1.
|
|
Currently an nec benchmark in regress2 is very slow (57 seconds in production) due to disabling the nec-specific options in 67c730c). This reenables these options for this benchmark.
|
|
With quantifiers over real variables, --solve-real-as-int is neither sound nor complete. Thus we should abort in this case.
|
|
If we combine finite model finding and higher-order, then we could try to find a model find operators whose kind was BOUND_VARIABLE.
|
|
Supporting SMT-LIB's (reset) command on the API level is dangerous and not required -- it's sufficient to just destroy the solver object and create a new one if necessary. It's dangerous because invalidated objects can be passed in after a reset, and we would need to find a clean way to guard against this. We want to guard against this in the future, but for now it is cleaner to make it explicit (by not having this functionality in the API but forcing the user to destroy and recreate the solver object) that these objects can't be reused.
|
|
Fixes #3955.
Previously we were getting two calls to notifyNewEqClass from the equality engine for new application nodes, since the notification was being done in an internal call to newNode(...). The proper place to call this is in addTermInternal(...) which is called only once per Node per SAT context.
This bug potentially impacted some performance (due to redundant calls), and also broke the contract that notifyNewEqClass should only be called once per node per SAT context. In most cases, this was being handled in a benign way by theory solvers, although an assertion was failing in EqualityQuery, which is fixed by this PR.
A block of code changed indentation in this commit.
|
|
Moves SMT-COMP-specific options to the SMT-COMP script. Both of these options have led to issues (segfaults or infinite loops).
Issue #789 can be downgraded to "minor" after this PR.
Btw, I did not add these specialized options to the "incremental" script of SMT-COMP, since I'm assuming they should not be used there.
|
|
Fixes #4025.
Also makes our sygus default grammar for strings (slightly) better by including a dummy character, which is required for solving the regression added by this PR. A more robust (but unintuitive to the user) solution would be to include str.from_code( Start_Int ).
|
|
Fixes #4022.
|
|
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 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 #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).
|
|
|
|
cores. (#4011)
|
|
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 #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.
|
|
|
|
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.
|
|
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;
```
|
|
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.
|
|
PR #3918 added a new test case that results in a warning when checking
models, which makes the regression fail. This commit adds a flag to the
test to ignore that warning.
|
|
Fixes #3645.
|
|
The output of the regression script was difficult to read (especially
the diffs). This commit makes the output more readable by adding colors,
separators, and using a unified diff.
|
|
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 fixes a few issues in the real to int preprocessing pass. Previously it was not robust to cases where the input had constraints that were not over the reals.
Fixes #3915 and fixes #3913 and fixes #3916.
|
|
stages (#3844)
Fixes #3729 and fixes #3720.
This updates two more stages of check-model (checking whether values assigned to terms are constants and internally checking whether assertions belonging to theories) to only throw warnings when a term/assertion has a non-constant value in the model. This is to accommodate cases where check-model is infeasible.
|
|
This commit adds support for `str.from_code`. This is work towards
supporting the new strings standard. The code currently just does an
eager expansion of the operator. The commit also renames `STRING_CODE`
to `STRING_TO_CODE` to better reflect the names of the operators in the
new standard.
|
|
Fixes #3813.
It appears that an assertion was hardcoded to check whether a term was a variable or APPLY_UF application whereas this check should use isAssignable. This avoids an assertion failure on the given benchmark.
|
|
(#3841)
Fixes #3839.
Previously, the quantifiers rewriter had a rewriting step that was an ad-hoc version of some of the rewrites that have been incorporated into the extended rewriter. Moreover, the code for that pass was buggy.
This eliminates the previous conditional rewriting step from the "term process" rewrite pass in quantifiers. It additional adds an optional (disabled by default) rewriting pass that calls the extended rewriter on the body of quantified formulas. This subsumes the previous behavior and should not be buggy.
Notice that the indentation in computeProcessTerms changed and subsequently has been updated to the new coding standards.
This PR relies on #3840.
|
