| Age | Commit message (Collapse) | Author |
|---|
|
Fixes #7002.
|
|
Since the internal bitblaster can be way slower, the regressions that would have slow runs when --check-proofs is passed now have the command line that forces the use of the default bitblaster.
|
|
When enabled, this does not word-blast when registering term but at preNotifyFact (= more lazily) instead.
This is enabled via option --fp-lazy-wb.
|
|
|
|
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 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.
|
|
|
|
|
|
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.
|
|
This commit removes parser and printer support for old SMT-LIB standards and also converts all regression tests to 2.6.
|
|
Moves regressions taking >4 seconds (summing all configs) in debug to regress1.
|
|
Currently --check-models is implemented by replaying several preprocessing steps, including theory-specific expand definitions, and then checking whether the result evaluates to true.
However, by having --check-models rely on complex preprocessing machinery defeats its purpose, as these steps are part of its trusted base.
Moreover, issue #5645 demonstrates that this may lead to spurious errors where we incorrectly conclude that an input assertion is false, when it is not.
This PR significantly simplifies --check-models so that it only relies on define-fun expansion + rewriting + evaluation. This ensures that --check-models is "sound" i.e. it does not falsely report a formula as evaluating to false. As a consequence, this makes check-models give warnings more often, i.e. when partial operators are involved, thus -q is added to silence warnings on some regressions.
A followup PR will use a satisfiability check on the input formula post-expand-definitions to properly implement a trustworthy version of check-models that is robust for partial operators.
Fixes #5645.
|
|
Fixes #5524.
|
|
Fixes #4620.
The extended rewrite (and A B) ---> (and A (B * { A -> true } ) triggers an unsoundness when B contains witness terms. More generally, contextual substitution into witness terms is unsound since the skolemization of witness terms is added globally whereas the substitution corresponds to a fact that holds locally. This means that A -> true above may be added as a global constraint indirectly through witness skolemization.
A general example of this unsoundness:
(or (and (>= x 0) (P (witness ((z Int)) (=> (>= x 0) (= (* z z) x))))) F)
rewrites to
(or (and (>= x 0) (P (witness ((z Int)) (= (* z z) x)))) F)
preprocesses to
(and (or (and (>= x 0) (P k)) F) (= (* k k) x))
which now implies that (>= x 0) by the last conjunct, whereas this was not implied in the original formula
This PR limits the kinds that can be traversed when applying substitutions in the extended rewriter, including from the rewrite above. In particular, the fix ensures that the partialSubstitute method is used in the extended rewriter when applicable, which now explicitly disallows recursion on WITNESS.
Notice that this fixes contextual substitutions in the extended rewriter, but does not fix the more general issue. In particular, we still should be careful to check if contextual substitutions are applied by any other preprocessing passes.
|
|
This error is a bit inexplicable but very very definitely wrong.
A test case from the original bug report is included.
|
|
Fixes #4277.
|
|
Fixes #3536. The type checker for the chain operator was calling the
rewriter. However, the floating-point rewriter was expecting
`TheoryFp::expandDefinition()` to be applied before rewriting. If the
chain operator had subterms that were supposed to be removed by
`TheoryFp::expandDefinition()`, the FP rewriter was throwing an
exception. This commit fixes the issue by not calling the full rewriter
in the type checker but by just expanding the chain operator. This is a
bit less efficient than before because the rewriter does not cache the
result of expanding the chain operator anymore but assuming that there
are no long chains, the performance impact should be negligible. It also
seemed like a reasonable assumption that the rewriter can expect to run
after `expandDefinition()` because otherwise the rewriter has to expand
definitions, which may be too restrictive.
|
|
Fixes #2932. fp.roundToIntegral was rounding some very small subnormals up to
between 1 and 2, which is A. wrong and B. not idempotent. The
corresponding symfpu update fixes this as it was an overflow caused
by the unpacked significand not being able to represent an extra
significand bits.
|
|
|
|
Although CVC4's behaviour is actually correct, this is to make
things a bit clearer and prevent confusion in the future.
|
|
|
|
For a simple query `(not (= (fp.isSubnormal x) false))`, we were getting
a wrong model. The issue was that `(sign x)` was not assigned a value
and did not appear in the shared terms. In
`TheoryFp::collectModelInfo()`, however, we generate an expression that
connects the components of `x` to `x`, which contains `(sign x)`. As a
result, the normalization while building a model did not result in a
constant. This commit fixes the issue by marking `(sign x)` (and
`(significand x)`) as assignable. Assignable terms can take any value
while building a model if there is no existing value.
|
|
|
|
This is work towards #2305.
With this PR, CVC4's performance is fairly reasonable on the Kind2 BMC benchmarks with --decision=internal --ext-rew-prep --ext-rew-prep-agg.
|
|
|
|
This commit adds supprt for the `REQUIRES` directive in our regression
benchmarks. This directive can be used to enable certain benchmarks only
if CVC4 has been configured with certain features enabled.
|
