| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Commit cfeaf40ed6a9d4d7fec925352e30d2470a1ca567 renamed
`Result::Validity` and `SmtEngine::query()` to `Result::Entailment` and
`SmtEngine::checkEntailed()`, respectively. The commit did not update
the Java tests which lead to issues in debug builds with Java bindings.
The commit also adds a corresponding `NEWS` entry.
|
|
When running `node_traversal_black` with ASan and UBSan, there were two
distinct issues being reported. UBSan was complaining that we were
assigning an invalid value to a Boolean. This happened because
`d_initialized` in `NodeDfsIterator` was uninitialized and the default
copy constructor tried to copy it. This commit removes that data member.
ASan was complainig that `NodeDfsIterator::begin()` was trying to access
a skip function that had been freed. In particular, this happened when
`NodeDfsIterable` was used in a range-based for loop like so:
```
for (auto n : NodeDfsIterable(n).inPostorder())
{
...
}
```
The problem here is that the lifetime of a temporary _within_ the range
expression is not extended (the lifetime of the result of the range
expression is extended, however) [0]. This is a problem because
`NodeDfsIterable(n)` is a temporary and `inPostorder()` returns a
reference to that temporary. It makes sense that the compiler cannot
possibly know that the reference from `inPostorder()` corresponds to
`NodeDfsIterable(n)`, so it cannot extend its lifetime. See [1] for more
details on the problem with chained functions.
This commit fixes the issue by replacing the fluent interface of
`NodeDfsIterable` by a constructor with default arguments. Additionally,
it introduces an enum to represent the visit order to avoid having a
nondescript Boolean argument.
[0] https://en.cppreference.com/w/cpp/language/range-for#Temporary_range_expression
[1] http://cpptruths.blogspot.com/2018/10/chained-functions-break-reference.html?m=1
|
|
This adds the remaining API guards in the Solver object (incl. unit tests).
|
|
Previously we were treating constructor/selector/tester symbols as arguments to the abduct-to-synthesize.
|
|
This is the first batch of API guards, mainly extending existing guards
in the Solver object with checks that Ops, Terms, Sorts, and datatype objects
are associated to this solver object.
This further changes how DatatypeConstructorDecl objects are created. Previously,
they were not created via the Solver object (while DatatypeDecl was). Now, they are
created via Solver::mkDatatypeConstructorDecl, consistent with how DatatypeDecl
objects are created.
|
|
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 #4225, fixes CVC4/cvc4-projects#159, fixes CVC4/cvc4-projects#157, fixes #4289, fixes #4483.
This makes it so that the main model-based instantiation algorithm is not applied to quantified formulas with universally quantified functions.
Identation changed in a FMF function, this was refactored to conform to guidelines, and further cleaned.
|
|
This is in preparation for adding guards to ensure that sort and term
arguments belong to the same solver.
|
|
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.
|
|
Also renames a function mkWord -> mkWordFlatten.
|
|
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`.
|
|
An example for restricting timeout in tests uses the old `make regress0` instead of the new `ctest -L regress0`
|
|
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.
|
|
Disabling re-elim performs better overall in many recent experiments.
|
|
This PR modifies the Grammar implementation to make it reusable (i.e., can be copied or passed multiple times to synthFun/synthInv) with the catch that it becomes read-only after the first use.
|
|
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.
|
|
Notice this also updates our regression script to use --debug-check-model, preserving previous behavior.
Fixes #4461, fixes #4470, fixes #4471, fixes #4475, fixes #4448, fixes #4466, fixes #4460, fixes #4458, fixes #4455, fixes #4456, fixes #4386, fixes #4385, fixes #4478, fixes #4474.
|
|
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 #3692 and an assertion failure that came up during the test runs
for SMT-COMP. The bit-vector rewrites `SolveEq` and
`PlusCombineLikeTerms` were not always idempotent. At a high level,
`SolveEq` combines common terms from two sides of an equality and
`PlusCombineLikeTerms` combines common terms within an addition.
However, in doing so, these rewrites were reordering the operands of the
bit-vector addition based on the node ids of the terms that were
multiplied with their coefficients. Consider the addition `3 * x * y + 5
* y * z` (the bit-width does not matter). `PlusCombineLikeTerms` would
reorder this addition to `5 * y * z + 3 * x * y` if the node id of `y *
z` was smaller than the node id of `x * y`. The issue is that node ids
are not fixed for a given term: If we have a term `x * y` and that term
reaches ref count 0, we may get a different id for that same term if we
recreate it later on. When terms reach ref count 0, we don't immediately
delete them but add them to our set of zombies to be deleted whenever
the list of zombies grows larger than some fixed size. When applying
`SolveEq` and `PlusCombineLikeTerms` multiple times (even in direct
succession without doing anything else), the node order may change
because some of the terms like `x * y` may be zombies while others have
been deleted and get new ids, leading to the relative order of node ids
changing. I suspect that we could construct a case where we get into an
infinite rewrite loop.
This commit addresses the issue as follows: It does not perform the
rewrites `SolveEq` and `PlusCombineLikeTerms` if none of the operands
change. This makes the rewrites idempotent. Note however that we are
still not guaranteeing that a term has the same rewritten form
throughout an execution because the node ids may change if the term has
been freed in the meantime. However, this limitation is consistent with
other rewrites such as the reordering of equalities.
I am including the minimized test case from our run on SMT-LIB. I am
ommittin the test case from #3692 because I couldn't trigger it on
master (not surprising since the issue requires very specific
circumstances to actually occur). However, I was able to reproduce the
issue on the CVC4 version mentioned in the issue and confirmed that this
fix worked for that older version.
|
|
Fixes an unsoundness in unconstrained simplification, fixes #4469.
|
|
|
|
Fixes regress1.
|
|
This fixes a soundness issue in strings caused by an incorrect skolem share.
This adds a regression that corresponds to the rewrite that this skolem share was justified by, which is "sat" (the rewrite does not hold). This benchmark in fact was answered "unsat" by CVC4 prior to this PR.
|
|
(#4415)
An incorrect answer of "sat" could be found after 8 seconds on the given benchmark (with --strings-fmf) due to a circular justification for why an extended function was reduced. In particular, we ran checkExtfInference on the same term twice and then marked it as reduced since we had already seen it. This makes the code more conservative.
Notice I'm making the code doubly conservative in case there is any chance for duplication again (e.g. if ExtTheory provides duplicate terms).
|
|
Fixes nightlies.
|
|
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 updates the default cardinality in strings to match the Unicode standard, 196608.
This avoids a check-model failure from 25 benchmarks in SMT-LIB, which were related to a split due to insufficient constants being required during collectModelInfo.
This also makes a few places throw an AlwaysAssert(false) that otherwise would lead to incorrect models. These regardless should never throw, but it would be better to have an assertion failure.
|
|
|
|
Fixes #4391.
The sets cardinality cycle rule is analogous to the S-Cycle rule for strings (see Liang et al CAV 2014). This rule is typically never applied but can be applied in rare cases where theory combination does not determine a correct arrangement of equalities over sets terms that is consistent with the arithmetic arrangement of their cardinalities at full effort. Notice the regression from #4391 has non-linear arithmetic, (mod 0 d), which is translated to UF.
The cardinality cycle rule had a bug: it assumed that cycles that were encountered were loops e1 = e2 = ... = e1 but in general they can be lassos e1 = ... = e2 = ... = e2. This ensures the Venn region cycle e2 = ... = e2 is the conclusion in this case, instead of unsoundly concluding e1 = ... = e2.
Strings does not have a similar issue:
https://github.com/CVC4/CVC4/blob/master/src/theory/strings/core_solver.cpp#L488
Here, when a cycle is encountered, it is processed at the point in traversal where the loop is closed.
This is not critical for SMT-COMP but should be in the 1.8 release.
|
|
Fixes #4379. This was caused by a splitting lemma rewriting to a conjunction, being processed as a fact, and having a pending phase requirement sent out assuming the inference was to be processed as a lemma. This forces 2 of the splits in the core solver to be always processed as lemmas.
|
|
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 commit addresses issue #38 in cvc4-projects by introducing public API for Sygus commands. It also includes two simple examples of how to use the API.
|
|
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.
|
|
Should fix the nightlies.
|
|
|
|
|
|
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.
|
|
Fixes #4243.
|
