| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
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.
|
|
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`.
|
|
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.
|
|
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 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 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.
|
|
With this PR, we now support a preliminary draft of a theory of sequences.
This PR adds front end support for sequences in the smt2 parser, in the new API, adds regressions and unit tests for them.
As discussed offline, many of the string kinds are given a sequence version in the external API, but not in the internal one. This means that a special case for such kinds, getKindHelper was added to Term.
We do not yet support proper smt2 printing of sequences, which will require access to this code for Kind conversions (to distinguish e.g. str.++ from seq.++).
|
|
Fixes #4674.
|
|
There were two issues related to RE in bodies of re.* that accepted the empty string that led to non-termination in the rewriter for regular expressions.
This also improves trace messages for simpleRegExpConsume.
Fixes #4662.
|
|
Fixes #4644. This commit fixes an issue where the set `d_unconstrained`
in the unconstrained simplification pass was not computed correctly. The
problem was that visiting the same term multiple times did not remove
the variables appearing in that term from the visited-once set. A simple
example that triggers the issue is the following:
```
(set-logic ALL)
(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (not (= a b)))
(assert (= a (= a b)))
(check-sat)
```
After running `UnconstrainedSimplifier::visitAll()` on both assertions,
we end up with `[b]` as our `d_unconstrained` set. We end up inferring
the substitution `(= a b) --> b` and get `(not b)` and `b`, which is
unsat even though the original problem is sat.
This commit fixes the issue by visiting all the children of a node if we
visit a node for a second time. This makes sure that we remove any
children from the visisted-once set.
|
|
This commit adds support for an eqrange predicate. (eqrange a b i j) is true if arrays a and b are equal on all indices within indices i and j, i.e., \forall k . i <= k <= j --> a[k] = b[k]. Requires option --arrays-exp to be enabled.
|
|
Fixes #4636.
This adds transcendental function kinds to the list of unevaluated operators (operators that don't necessarily rewrite to constants when applied to constant children). One consequence of this is that when models are enabled, we cannot solve for equations like (= a (cos b)), since the value of (cos b) is not necessarily evaluable, and hence must be approximated. As a result, we answer the benchmark on #4636 instead of generating an incorrect model (when models are enabled). When models are disabled, we answer "sat". A regression had a similar issue which happened to be succeeding. I've added --no-check-models to this regression (or otherwise we would answer unknown for this benchmark).
|
|
fix 1:
------
The wrong flag was checked in the traversal, causing an assertion error [here](https://github.com/CVC4/CVC4/blob/8236d7f9bff3aef4f7b37a15d509b8a11551401f/src/preprocessing/passes/bv_to_int.cpp#L247)
This is fixed in this PR. A test was added as well.
fix 2:
------
It is desirable that bv-to-bool runs before bv-to-int, but this was not the case, and is fixed in this PR.
Do not merge until after competition release (label added).
|
|
This commit adds a logic check for `define-fun-rec`/`define-funs-rec` at
the level of the new API that checks whether the logic is quantified and
includes UF. To make sure that the parser actually executes that check,
this commit converts the `DefineFunctionRecCommand` command to use the
new API instead of the old one. This temporarily breaks the `exportTo`
functionality for `DefineFunctionRecCommand` but this is not currently
used within the CVC4 code base (and it seems unlikely that users use
commands).
|
|
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.
|
|
|
|
Fixes #4076.
In the lazy bit-blaster, when querying the equality status, if the SAT
solver has a full model, it is queried for the model values of the
operands of the equality. However, the check if the bit-blaster has a
full model did not consider the case where no assertions have yet been
added, which leads to querying values of bits that are still unassigned
in the SAT solver.
Co-authored-by: <mathias.preiner@gmail.com>
|
|
Fixes #4075.
|
|
Fixes #4130.
This further makes an attempt at more consistent error printing.
|
|
Fixes #4576. ASan was reporting memory leaks because the skolem manager
was being destroyed after the attributes and zombies were already
cleaned up in the destructor of NodeManager. This commit changes the
destruction order to ensure that the skolem manager is destroyed before
the rest of the cleanup.
Note: this issue did not only make the benchmark in #4576 fail but
several tests in our regressions.
|
|
Fixes #4552. Fixes #4555. The SMT-LIB standard mandates that definitions
are kept when `:global-declarations` are enabled. Until now, CVC4 was
keeping track of the symbols of a definition correctly but lost the body
of the definition when the user context was popped. This commit fixes
the issue by adding a `global` parameter to
`SmtEngine::defineFunction()` and `SmtEngine::defineFunctionRec()`. If
that parameter is set, the definitions of functions are added at level 0
to `d_definedFunctions` and the lemmas for recursive function
definitions are kept in an additional list and asserted during each
`checkSat` call. The commit also updates new API, the commands, and the
parsers to reflect this change.
|
|
Fixes nightlies. Competition builds do not report parsing errors like
other builds. As a result, one of the regression tests that is testing
for parse errors was failing for competition builds. In this particular
example, we just report `unknown`. This commit marks the regression to
be skipped for competition builds.
|
|
|
|
Fixes #4446. This commit fixes two issues related to the handling of
Boolean term variables:
Removing Boolean subterms and replacing them with a Boolean term
variable introduces an equality of the form (= v t) where v is the
Boolean term variable and t is the term. It is important that these
equalities do not get removed. This commit changes
Theory::isLegalElimination() to take this into account.
The incorrect model reported in the issue was caused by some of the
Boolean term variables not being assigned values by the SAT solver
when we decided that the benchmark is satisfiable. Our justification
heuristic (correctly) decided that it is enough to satisfy one of the
disjuncts in the assertion to satisfy the whole assertion. However,
the assignments that we received from the SAT solver restricted us to
pick a specific value for one of the Boolean constants:
Literal | Value | Expr
---------------------------------------------------------
'7 ' 0 c
'0 ' 1 true
'1 ' 0 false
'2 ' 0 (a BOOLEAN_TERM_VARIABLE_274)
'5 ' _ b
'3 ' 1 (a BOOLEAN_TERM_VARIABLE_277)
'4 ' _ BOOLEAN_TERM_VARIABLE_274
'6 ' 0 BOOLEAN_TERM_VARIABLE_277
This meant that we had to pick true for BOOLEAN_TERM_VARIABLE_274
but we picked false since we simply treated it as an unassigned
variable. In general, the justification heuristic handles embedded
skolems introduced by term removal first and asks the SAT solver to
decide on Boolean term variables. However, for some logics, such as
QF_AUFLIA, we use the justification heuristic not for decisions but
only to decide when to stop, so those decisions were not done. This
commit introduces a conservative fix that adds a check after
satsifying all the assertions that makes sure that the equalities
introduced for Boolean terms are satisfied as well. Due to the eager
treatment of Boolean term variables when we use the justification
heuristic also for decisions, it is likely that we don't really have
the problem in that case but it doesn't hurt to enable the fix. It is
also possible that this fix is only required with models but it is
definitely safer to just always enable it (there could be tricky
corner cases involving the theory combination between UF and Boolean
terms). Additionally, this commit changes the ITE-specific naming in
the justification heuristic to reflect more accurately that we are in
general dealing with skolems introduced by term removals and not only
due to ITE removal.
|
|
Fixes #4437.
This is a simpler fix that aborts the preprocessing pass when a quantifier is encountered.
It also updates our smt2 parser to throw a logic exception when forall/exists is used in non-quantified logics. This is required to ensure that unconstrained simplification does not throw an exception to a user as a result of accidentally setting the wrong logic.
|
|
Fixes #4476.
|
|
Fixes #4367. We set the theoryof-mode depending on whether sharing is
enabled or not. However, we were checking whether sharing was enabled
before theory widening, leading to unexpected results. This commit moves
the check after widening the theories.
For the benchmark in the issue, setting the theoryof-mode before theory
widening lead to problems because of the following:
The main solver checks the condition for enabling term-based
theoryof-mode, decides not to do it because sharing is not enabled
Main solver adds UF to the logic
Main solver does a check-sat all
Unsat core check runs, sees both UF and NRA enabled, and switches
to term-based mode
Main solver gets to second check-sat call, now the theoryof-mode is
suddenly changed, which leads to problems in the equality engine
This commit fixes the issue in this particular instance but it is important
to note that it does not address the issue of the subsolver changing
settings in general. This can only really be solved by separating the
options from the ExprManager/NodeManager and having separate
options for each SmtEngine/Solver instance.
|
|
Fixes #4477. Logic ALL includes higher-order but we currently do not
support solving higher-order problems unless --uf-ho is enabled. This
commit changes the condition under which we parse -> and lambda to
only enabled parsing of those symbols if the logic allows higher-order
constraints and --uf-ho is enabled.
|
|
Fixes #4525. The actual problem in the issue is not that the unsat core
is satisfiable but that our unsat core check is not working as intended.
Our unsat core check uses the same `ExprManager` as the main `SmtEngine`
and thus also shares the same attributes for nodes. However, since we
have a different `SmtEngine` instance for the check, we also have
different instances of `TheoryArith`. This leads to the check failing
due to the following:
- Our only input assertion is `(> (cot 0.0) (/ 1 0)))`.
- `TheoryArith::expandDefinition()` gets called on `(> (cot 0.0) (/ 1
0))` but nothing happens.
- `TheoryArith::expandDefinition()` gets called on `(/ 1 0)`, which gets
expanded as expected but no attribute is set because it happens in a
simple `TheoryArith::eliminateOperators()` call.
- `TheoryArith::expandDefinition()` on `(cot (/ 0 1))` first expands to
`(/ 1 0)` (not cached) and then we expand it recursively to the
expected term and cache `(/ 1 0) ---> (ite (= 0 0) (divByZero 1.0) (/
1 0))`.
Up to this point, things are suboptimal but there are no correctness
issues. The problem starts when we do the same process in the unsat core
check:
- Our only input assertion is again `(> (cot 0.0) (/ 1 0)))`.
- `TheoryArith::expandDefinition()` gets called on `(> (cot 0.0) (/ 1
0))` but nothing happens.
- `TheoryArith::expandDefinition()` gets called on `(/ 1 0)`, which gets
expanded as expected but no attribute is set or checked because it
happens in a simple `TheoryArith::eliminateOperators()` call. Note
that the skolem introduced here for the division-by-zero case is
different from the skolem introduced above because this is in a
different `TheoryArith` instance that does not know the existing
skolems.
- `TheoryArith::expandDefinition()` on `(cot (/ 0 1))` first expands to
`(/ 1 0)` (not cached) and then we use the cache from our solving call
to expand it `(/ 1 0) ---> (ite (= 0 0) (divByZero 1.0) (/ 1 0))`.
Note that `divByZero` here is the skolem from the main solver.
As a result, the preprocessed assertions mix skolems from the main
`SmtEngine` with the `SmtEngine` of the unsat core check, making the
constraints satisfiable.
To solve this problem, this commit removes the caching-by-attribute
mechanism. The reason for removing it is that it is currently
ineffective (since most eliminations do not seem to be cached) and there
are caches at other levels, e.g. when expanding definitions. If we deem
the operator elimination to be a bottleneck, we can introduce a similar
mechanism at the level of `TheoryArith`.
|
|
This error is a bit inexplicable but very very definitely wrong.
A test case from the original bug report is included.
|
|
This is a major refactor of how operators are eliminated in arithmetic. Currently there were (at least) two things wrong:
(1) ppRewriteTerm sent lemmas on the output channel. This behavior is incompatible with how preprocessing works. In particular, this caused unconstrained simplification to be unaware of terms from such lemmas, leading to incorrect "sat" answers.
(2) Lemmas used to eliminate certain "div-like" terms were processed in a context-independent way. However, lemmas should be cached in a user-context-dependent way. This was leading to incorrect "sat" answers in incremental.
The solution to these issues is to eliminate operators via the construction of witness terms. No lemmas are sent out, and instead these lemmas are the consequence of term formula removal in the standard way.
As a result of the refactor, 2 quantifiers regressions time out due to infinite branch and bound issues (one only during --check-unsat-cores). These appear to be random and I've changed the options to avoid these issues. 3 others now have check-model warnings, which I've added --quiet to. Improving check-model will be addressed on a future PR.
This PR is not required for SMT COMP since we have workarounds that avoid both the incorrect behaviors in our scripts.
Also notice that --rewrite-divk is effectively now enabled by default always.
Fixes #4484, fixes #4486, fixes #4481.
|
|
This introduces a rewrite based on regular expression inclusion (using calls to the RegExpEntail utility function).
This allows us to justify the regular expression inclusion inference as a rewrite.
|
|
Fixes #4482.
|
|
This adds a new inference schema to strings that was discovered by the internal proof checker. It says that we are in conflict when an equality between the normal forms of two terms in the same equivalence class rewrites to false.
It also improves the efficiency of processing normal forms by only considering normal forms that are unique up to rewriting.
|
|
A bug was introduced when adding the Node-level datatype implementation in d803e7f. The code did not probably get the arity of a sort constructor. This adds TypeNode::getSortConstructorArity and uses it during parametric datatype type resolution.
|
|
When we eliminate a variable x -> v during simplification, it may be the case that v contains "unevaluated" operators like forall, choice, etc. Thus, we do not produce correct models for such inputs unless simplification is disabled.
This PR ensures we only eliminate variables when v contains only evaluated operators.
Additionally, the kinds registered as unevaluated were slightly modified so that when we are in a logic like QF_LIA, there are no registered unevaluated operators, hence the check above is unnecessary. This is to minimize the performance impact of this change.
Fixes #4500.
|
|
Fixes an issue with over-pruning in SyGuS where using multiple sygus types that map to the same builtin type. Our mapping sygusToBuiltin did not ensure that free variables were unique.
Fixes #4383.
|
|
Renamed operator CHOICE to WITNESS, and removed it from the front end
|
|
Fixes an unsoundness in unconstrained simplification, fixes #4469.
|
|
This PR merges --lang=smt2.6.1 and --lang=smt2.6 (default). It makes it so that 2.6 always expects the syntax of the string standard http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml.
I've updated the regressions so that the 2.6 benchmarks are now compliant with the standard. Some of the <=2.5 benchmarks I've updated to 2.6. Others I have left for now, in particular the ones that rely on special characters or ad-hoc escape sequences. The old formats will be supported in the release but removed shortly afterwards.
This PR is a prerequisite for the release, but not necessarily SMT-COMP (which will use --lang=smt2.6.1 if needed). Notice that we still do not have parsing support for str.replace_re or str.replace_re_all. This is required to be fully compliant.
|
|
This commit converts all v2.5 smt2 regressions to v2.6 (except for regress/regress0/lang_opts_2_5.smt2).
|
|
Fixes #4376. Commit 6255c0356bd78140a9cf075491c1d4608ac27704 removed
support for conjunctions in the conclusion of facts. However,
`F_ENDPOINT_EMP` generates a conjunction in the conclusion of the
inference if multiple components are inferred to be empty. This commit
reinstantiates support for conjunctions in the conclusion of facts.
|
|
This updates option names to be consistent across uses of counterexample-guided quantifier instantiation (ceqgi), which was previously called "counterexample-based quantifier instantiation" (cbqi), and sygus.
Notably, the trace "cegqi-engine" is changed to "sygus-engine" by this commit.
The changes were done by these commands in the given directories:
src/:
for f in $(find -name '.'); do sed -i 's/options::cbqi/options::cegqi/g' $f;sed -i 's/cegqi-engine/sygus-engine/g' $f; done;sed -i 's/"cbqi/"cegqi/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/--cbqi/--cegqi/g' $f; done
src/: and test/regress/:
for f in $(find -name '.'); do sed -i 's/cegqi-si/sygus-si/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/no-cbqi/no-cegqi/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/:cbqi/:cegqi/g' $f; done
And a few minor fixes afterwards.
This should be merged close to the time of the next stable release.
|
|
|
|
conflict-based instantiation (#4280)
Conflict-based instantiation would sometimes initialize a match x -> getRepresentative(t) when a quantified formula contained x = t. This leads to issues where getRepresentative(t) is an illegal term (say, in combination with CEGQI). This makes it so the representative is accessed when necessary instead of being set as part of the match.
Fixes #4275.
|
|
Fixes #4277.
|
|
This adds a fix to ensure dump-unsat-cores-full works by modifying the public options function. This options currently does not work since dumpUnsatCores is only set internally now. This fix is only required until options are refactored so that SmtEngine owns the authoritative copy of options.
|
|
A recent change made it so that defined functions would print as the anonymous lambda corresponding to their definition if the SyGuS v1 parser was used. This was caused by comparison with the wrong kind in the new API.
Notice that the v2 parser does not have this issue.
This also adds a regression to ensure this behavior is maintained by the SyGuS v2 parser.
|
