| Age | Commit message (Collapse) | Author |
|---|
|
This commit adds a new parser option, --hol, which marks that HOL is being used. This option has the effect of prepending the problem's logic with "HO_", which teels the solver that the logic is higher order. The parser builder, base parser, and SMT2 and TPTP parsers are all updated to work with this new setting, as is the logic info class.
For now this parser option is enabling the --uf-ho option for internal use, since for now higher-order solving relies it. In a future PR this dependency will be removed (since this information is already given to the SMT solver via the logic).
|
|
This PR ensures we do not eagerly rewrite bv2nat and int2bv when using solve-bv-as-int. Instead they are rewritten during expandDefinitions (at the end of preprocessing).
It also updates regressions that relied on lazy extended function reductions in the lazy solver to use solve-bv-as-int, and adds a missing case (INT_TO_BITVECTOR) in the solve-int-as-bv preprocessing pass.
A followup PR will remove support for lazy extended function reductions for bv2nat / int2bv altogether.
|
|
After commit 327a24508ed1d02a3fa233e680ffd0b30aa685a9, the int-to-bv
preprocessing pass is getting rewritten terms. As a result, the terms
can contain negative constants (instead of `(- c)`, i.e., `UMINUS` of a
positive constant) and `NONLINEAR_MULT`. The commit adds support for
those cases, does some minor cleanup, and adds regressions. The
regressions should allow us to detect if/when the preprocessing pass
breaks in the future.
|
|
Fixes #6717. Commit 11c1fba added some
new rewrites for ITE. Due to the new rewrites taking precedence over
existing rewrites, it could happen that some of the previous rewrites
did not apply anymore even though they would have further simplified the
ITE. In the example from the issue, (ite c c true) was rewritten to
(or (not T) T) instead of (ite T true true) and then true. The
commit fixes the issue by moving rewrites resulting in
conjunctions/disjunctions to the end.
|
|
This PR makes a new regression explicitly require statistics.
|
|
This PR fixes a typo in the option handler for the statistics options, which lead to options not properly propagating.
|
|
This PR fixes a missing connection in trust substitution proofs, which was the cause of open proofs when solved equalities from ppAssert were not justified by proofs.
Also distinguishes TRUST_SUBS_EQ from TRUST_SUBS_MAP for clarity.
|
|
Fixes #6681. When checking whether SPLIT_EQ_STRIP_L applies, we were
using sripSymbolicLength, which changes its inputs depending on how
many elements of the concatenation it could strip. However, one of the
arguments, pfxv0, was reused across multiple checks if the strip did
not result in a rewrite. Later invocations were wrong as a result. This
commit changes the call to stripSymbolicLength() to use a new copy of
the vector instead.
|
|
This commit enables the new bitblast solver by default. This commit also fixes model generation for Boolean variables when --bitblast=eager is enabled.
Fixes #3958, #5396, #5736, #5743, #5947.
|
|
Fixes #6636, fixes #6637. When the start index was non-zero, the result of
str.indexof_re was not properly restricted to be greater or equal to
the start index. This commit fixes the issue by making the eager
reduction lemma more precise. Additionally, the commit fixes an issue
with the lower bound of the length of the match in str.indexof_re.
|
|
|
|
Fixes cases of satisfiable unsat cores when proofs are enabled.
Unfortunately, this bug was also preventing us from doing the final scope check for all proof checking. As this was not being tested, this PR uncovers that proof checking is now failing on 6 regressions. I'm disabling proof checking here and will address these issues on later PRs.
|
|
Fixes #6643. The STRINGS_CTN_DECOMPOSE inference is always a conflict
but we sometimes sent it as an inference. To make sure that the
inference manager actually recognizes the inference as a conflict, this
commit ensures that the conclusion is always false and modifies the
explanation accordingly.
|
|
This PR fixes a subtle issue with double negations when producing proofs in the circuit propagator.
Adds the test case as a new regression, as well as some similar instances.
Fixes cvc5/cvc5-projects#277.
|
|
Fixes #6337 (the other benchmarks in this issue are either solved
correctly or time out after the changes in #6615) and fixes #5665.
While computing the model for a nested equivalence class containing
seq.unit, we were looking up the representative of the argument in
(seq.unit (seq.unit j)) and the representative was simpliy (seq.unit j). However, we had assigned (seq.unit 0) to (seq.unit j) earlier.
A second equivalence class of type (Seq (Seq Int)) and length 1 was
later assigned (seq.unit (seq.unit 0)) and we didn't detect that
(seq.unit (seq.unit j)) and (seq.unit (seq.unit 0)) have the same
value. This was incorrect because we do not allow assigning the same
value to different equivalence classes. In this case, it led to one of
the assertions being false.
This commit fixes the issues in two ways: it ensures that types are
processed in ascending order of nesting (e.g., (Seq Int) terms are
processed before (Seq (Seq Int)) terms) and it changes the procedure
to look up the representative in the model instead of the theory state
to take into account the model values assigned to the elements of
sequences.
cc @yoni206
|
|
Fixes #5508. `STRINGS_CTN_DECOMPOSE` could be triggered multiple times
by the same term, which resulted in an assertion failure. This commit
returns immediately after the first conflict to avoid the assertion
failure.
|
|
Fixes #6057. The reductions of `str.replace_re` and `str.replace_re_all`
were not correctly enforcing that the operations replace the _first_
occurrence of some regular expression in a string. This commit fixes the
issue by introducing a new operator `str.indexof_re(s, r, n)`, which,
analoguously to `str.indexof`, returns the index of the first match of
the regular expression `r` in `s`. The commit adds basic rewrites for
evaluating the operator as well as its reduction. Additionally, it
converts the reductions of `str.replace_re` and `str.replace_re_all` to
use that new operator. This simplifies the reductions of the two
operators and ensures that the semantics are consistent between the two.
|
|
Fixes a solution soundness issue caused by allowing ineligible terms of kind BOOLEAN_TERM_VARIABLE to appear in instantiations.
This also corrects the expected solution on a benchmark that had an incorrect status.
Fixes #6603.
|
|
Fixes 2nd benchmark from #6605.
|
|
This commit fixes an assertion failure in the rewriter on some of the
SMT-LIB QF_ABVFP benchmarks (the regression in this commit is the
minified version of
`non_incremental/QF_ABVFP/20170428-Liew-KLEE/imperial_gsl_benchmarks_statistics_klee.x86_64/query.14.smt2`).
The problem was that after applying the `BvComp` rewrite, the bit-vector
rewriter was returning `REWRITE_DONE` instead of `REWRITE_AGAIN`. The
rewrite simplifies expressions of the form `bvcomp(t, c)` where `c` is a
constant of bit-width 1. If `c` is zero, then the rewrite returns
`bvnot(t)`. This node can potentially be rewritten further, e.g., if `t`
is `bvnot(x)`. This commit fixes the response and adds the corresponding
tests.
|
|
This enables the new implementation of justification heuristic by default.
Fixes #5454, fixes #5785. Fixes wishues 114, 115, 149, 160.
|
|
Fixes #6604.
Previously, re-elim was solution unsound for cases where the LHS and a component of the RHS were both empty. This ensures a length requirement is given for the LHS to ensure proper containment.
|
|
This updates all regressions that pass check-unsat-cores to enable check-unsat-cores. This includes any incremental benchmark, which was disabled in run_regression.py previously.
It adds --no-check-unsat-cores to a few corner benchmarks that were previously disabled based on --incremental.
It also reverts a change to when proofs are disabled: options like sygus-inference should not permit proofs (or unsat cores).
|
|
This PR does two things:
(1) It eliminates the ad-hoc implementation of printSynthSolutions and removes it from the API. Now, printing response to a check-synth command is done in a more standard way, using the API + symbol manager. This is analogous to recent refactoring to get-model.
(2) It updates cvc5's output in response to check-synth to be compliant with the upcoming sygus 2.1 standard. The standard has changed slightly: responses to check-synth are now closed in parentheses, mirroring the smt2 response to get-model.
It also removes the unused command GetSynthSolutionCommand.
|
|
Previously, echo surpressed leading, trailing and escape quotes of the
string to print. However, the SMT-LIB standard states that the string is
to be printed as is, including those quote characters.
|
|
We can thus close #3455, #3651, #4925, #5079, #5238, #5902, #5908, and #5604.
|
|
Fixes #6560.
|
|
Currently, when a :named attribute is used in a binder, the parser
complains about an illegal argument. This is because an argument check
in the SymbolManager fails. This is not very user friendly. This
commit makes the error message clearer for the user:
Cannot name a term in a binder (e.g., quantifiers, definitions)
To do this, the commit changes the return type for
SymbolManager::setExpressionName to include more information that can
then be used by the parser to generate an appropriate error message.
The commit also changes define-fun to not push/pop the local scope
if it has zero arguments because it is semantically equivalent to a
define-const, which allows :named terms.
|
|
Fixes #6520. The `SPLIT_EQ_STRIP_R`/`SPLIT_EQ_STRIP_L` rewrites were
applied too aggressively. Those rewrites attempt to rewrite string
equalities between concatenations where the prefix on one side is
provably shorter than the prefix on the other side. The length of the
shorter prefix is then stripped from the longer prefix. However, cvc5
was not checking whether it was able to strip the length of the full
prefix. If cvc5 cannot strip the full length of the shorter prefix, then
the rewrite does not apply because parts of the shorter prefix would
have to be kept. This commit adds an additional condition that checks
whether the length of the full prefix was stripped.
|
|
This PR improves the integration of the CAD solver with the nl-ext solver in a simple way: we simply use a few of the simple linearization lemmas in combination with CAD by default, significantly improving the performance on QF_NRA.
|
|
applicable (#6529)
Fixes #6510.
This PR also eliminates a deprecated variant mkBooleanTermVariable from SkolemManager.
|
|
This removes the special case of TUPLE_UPDATE and RECORD_UPDATE in favor of the more general datatype update.
Datatype update is handled analogously to APPLY_SELECTOR / APPLY_TESTER.
|
|
|
|
|
|
SymFPU does not allow to_fp conversion from signed bv of size 1. This
adds rewrites for this case.
Rewrites for the constant and the non-constant cases were tested in
isolation.
|
|
This automatically applies @martin-cs's working patch from 2020-11-14.
It fixes several issues, all covered open issues are added as
regression tests.
Fixes #3582.
Fixes #5511.
Fixes #6164.
|
|
|
|
This makes it so that we attempt evaluation + rewriting on applications of operators that do not always evaluate, and return constants in case the evaluation was successful.
This fixes warnings for check-models on 43 of our regressions, and also uncovered one regression where our model was wrong but check-models silently succeeded. I've opened CVC4/cvc4-projects#276 for fixing the latter.
|
|
In each case, previously we were generating a define-fun, what we needed was to do a model substitution.
This actually meant that check-models was giving false positives. The model was incorrect but check-models succeeded due to its use of expand definitions.
|
|
simplification (#6394)
This PR removes the quantifiers macro preprocessing pass, which had several shortcomings, both in terms of performance and features.
This makes it so that quantifier macros are the (optional) implementation of TheoryQuantifiers::ppAssert.
In other words, quantifiers can now be put into "solved form", forall x. P(x) ---> P = lambda x. true.
This is part of an effort to improve proofs for preprocessing, as well as centralizing our reason about substitutions for the sake of efficiency.
|
|
Previously, preprocessing passes added model substitutions without
expanding definitions for substitutions, which can be a problem.
This adds a wrapper function to take care of it properly.
Fixes #5473.
|
|
This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.
|
|
|
|
This does some refactoring of quantifiers macros preprocessing pass to use up-to-date utility methods, including lambdas, substitutions, methods for getting free variables.
This is work towards adding proofs for macros.
|
|
When a command is invoked, its result/status may be printed depending on its current verbosity, which (for probably an outdated reason) is stored in SMTEngine. One of my previous PRs modified the SMTEngine to return the verbosity as an sexpr. The modification works correctly when the output language is SMT2, but it breaks down with the AST output language, which prints sexprs in a different way. This PR fixes this bug by making SMTEngine return options as strings instead of sexpr.
|
|
This PR generalizes TypeNode::isFinite / TypeNode::isInterpretedFinite with TypeNode::getCardinalityClass. It then uses this method to fix our computation of when a type should be treated as finite.
Fixes #4260, fixes #6100 (that benchmark now says unknown without an error).
|
|
Previously, we were not checking models / proofs / unsat cores for cvc inputs on CI.
|
|
Fixes #6298.
Enables parsing of par in the sygus parser, and adds support for default grammar construction.
Also fixes a bug related to single invocation for non-function types.
|
|
Previously the SMT post-processor would update any assumption as long as it
had a proof for it. This can be a problem when one as assumption introduced in a
scope that should not be expanded. This commit fixes the issue by adding the
option of configuring a proof node updater to track scopes and the assumptions
they introduce, which can be used to determine the prood nodes which should be
updated. It also changes the SMT post-processor to only update assumptions that
have not been introduced in some scope.
This commit fixes an issue found by @Lachnitt during the integration of CVC4 and Isabelle.
|
|
|
