| Age | Commit message (Collapse) | Author |
|---|
|
This PR changes the design of ProofSkolemCache so that it has facilities for tracking proofs. This is required so that the term formula removal pass can be made proof-producing.
This makes it so that ProofSkolemCache is renamed to SkolemManager, which lives in NodeManager. Creating (most) skolems must be accompanied by a corresponding ProofGenerator that can provide the proof for the existential corresponding to their witness form.
Further updates will include refactoring the mkSkolemExists method of SkolemManager so that its contract wrt proofs is simpler.
Once all calls to mkSkolem go through the standard interface, then NodeManager::mkSkolem will be moved to SkolemManager::mkSkolemInternal.
|
|
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.
|
|
This makes the method for substiutiton and generalization of sygus datatypes a generic utility method. It updates the abduction method to use it. Interpolation is another target user of this utility.
|
|
Previously we were treating constructor/selector/tester symbols as arguments to the abduct-to-synthesize.
|
|
This makes it so that the main reduce function in TheoryStringsPreprocess is static, so that it can be used both by the solver and the proof checker.
It also updates the functions to make use of IndexVar for constructing canonical universal variables.
|
|
|
|
|
|
This adds the proof checker for TheoryBuiltin, which handles the core proof rules (SCOPE and ASSUME) and all proof rules corresponding to generic operations on Node objects. This includes proof rules for rewriting and substitution, which are added in this PR.
|
|
This PR removes a hack in counterexample-guided quantifier instantiation.
The issue is the CEGQI needs to know the form of certain lemmas, after theory preprocessing. CEGQI needs to know this since it must construct solutions (e.g. solved form of equalities) for free variables in these lemmas, which includes fresh variables in the lemma after postprocess like ITE skolems.
Previously, CEGQI was hacked so that it applied the preprocessing eagerly so that it had full knowledge of the postprocessed lemma. This PR updates CEGQI so that it uses the returned LemmaStatus as the way of getting the lemma after postprocess. It also fixes the lemma status returned by TheoryEngine so that all lemmas not just the "main lemma" are returned as a conjunction.
This PR is in preparation for major refactoring to theory preprocessing for the sake of proofs.
|
|
Previously, we used a specialized variant of prenex normal form that allowed top level disjunctions. However, the method to put quantifiers into this form led to variable shadowing on some benchmarks in SMT-LIB LRA.
This simplifies the code so that we use standard prenex normal form when cegqi-nested-qe is used and deletes the old variant (DISJ_NORMAL).
|
|
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.
|
|
Also makes CVC4::theory::arith::nl namespace.
This includes some formatting changes.
|
|
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`.
|
|
This adds basic infrastructure for the sequence type, including its type rules, type enumerator and extensions to type functions.
The next step will be to finalize the support in TheoryStrings for sequences and then add front end support for sequences in the API/parsers.
|
|
We were getting an assertion failure (causing nightlies to fail) due to the recent optimization to the strings skolem cache (978f455). This ensures we ignore constant strings in TermRegistry::getRegisterTermAtomicLemma.
It also removes a deprecated option that is deleted in the proof-new branch.
|
|
This adds the expr-level sequence datatypes. This is required for further progress on sequences. However, note that this class may be deleted in the further when the Expr level is replaced.
|
|
|
|
This PR makes strings skolem cache call the ProofSkolemCache. This is required for proper proof checking, as it makes all skolems be associated with their formal definition, encapsulated by a witness term.
It furthermore makes skolem sharing more uniform and aggressive by noting that most string skolems correspond to purification variables (typically for some substr term). A purification variable for a term that rewrites to a constant can be replaced by the constant itself.
It also introduces an attribute IndexVarAttribute which is used to ensure reductions involving universal variables are deterministic.
|
|
Remove unused field d_emp_exp in TheorySetsPrivate
|
|
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 #4503.
|
|
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.
|
|
|
|
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 #4288.
When applying miniscoping, we previously were reusing variables across quantified formulas in the resulting conjunction. This ensures our miniscoping ensures fresh variables.
|
|
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.
|
|
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.
|
|
This fixes a potential model soundness issue in strings where a justification for why a string term was reduced relied on a circular argument. The issue involved "reduced by congruence" which states that when f(a) = f(b) ^ a = b in the current context, then one of f(a) or f(b) can be ignored.
However, it may be the case that a is an extended function whose reduction relies on f(b). If we were to assume that f(b) can be ignored due to f(a), then our reduction of f(a) is circular: the reduction of f(a) in the context where a=b relies on itself.
This was causing an incorrect model for QF_S/2020-sygus-qgen/queries/query3214.smt2. The sequence of dependencies was:
[1] (str.contains (str.substr x 1 (+ (- 1) (str.len x))) "CA")
is congruent to
(str.contains (str.substr x (+ 2 (str.indexof x "CA" 1)) (+ (- 2) (str.len x) (* (- 1) (str.indexof x "CA" 1)))) "CA")
in the current context since they are equal and their arguments are equal.
[2] (str.substr x (+ 2 (str.indexof x "CA" 1)) (+ (- 2) (str.len x) (* (- 1) (str.indexof x "CA" 1))))
reduction relies on the length constraint:
(= (str.indexof x "CA" 1) (+ (- 2) (str.len sspre_66)))
[3] (str.indexof x "CA" 1)
reduction relies on:
(not (str.contains (str.substr x 1 (+ (- 1) (str.len x))) "CA"))
which was marked congruent above.
The benchmark now solves in 5 minutes 30 seconds (sat, with a correct model):
andrew@andrew-Latitude-7480:~/misc/strings$ time ajr-cvc4 query3214.smt2 --strings-exp --rewrite-divk --check-models --dump-models
sat
(model
(define-fun x () String "QACOACA")
)
|
|
(#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).
|
|
This commit changes the term registration for str.to_int terms. Before, we were not sending out any lemmas when registering str.to_int terms. Now, we send a simple lemma that asserts that the value is greater or equal to negative one.
|
|
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.
|
|
* Introduce best content heuristic for strings
This commit introduces a "best content heuristic" to perform
context-dependent simplifications. The high-level idea is that for each
equivalence class for strings, we compute a representation that is a
string concatentation of constants and other string terms. For this
representation, we try to get as many letters in the string constants as
we can (i.e. the best approximation of the content). This "best content"
representation is then used by `EXTF_EVAL` to perform simplifications.
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
|
|
This commit fixes a performance regression introduced by commit 6255c03. The issue seems to be that registering terms manually after sending the lemma on the output channel is too late because the output channel processes the lemma eagerly.
|
|
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.
|
|
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.
|
|
This is a key refactoring towards proofs for strings.
This ensures that InferInfo is maintained until just before facts, lemmas and conflicts are processed. This allows us both to:
(1) track more accurate stats and debug information,
(2) have enough information to ensure that proofs can be constructed at the moment facts, lemmas, and conflicts are processed.
Changes in this PR:
PendingInfer and InferInfo were merged, CoreInferInfo is now the previous equivalent of InferInfo, extended with core-solver-specific information, which is only used by CoreSolver.
sendInference( const InferInfo& info, ... ) is now the central method for sending inferences which is called by the other variants, not the other way around.
sendLemma is inlined into sendInference(...) for clarity.
doPendingLemmas and doPendingFacts are extended to process the side effects of the inference infos.
There is actually a further issue with pending inferences related to eagerly processing the side effect of CoreInferInfo before we know the lemma is sent. I believe this issue does not occur in practice based on our strategy. Further refactoring could tighten this, e.g. virtual void InferInfo::processSideEffect. I will do this in another PR.
Further refactoring can address whether asLemma should be a field of InferInfo (it probably should), and whether we should explicitly check for AND in conclusions instead of making it the responsibility of the user of this class.
|
|
This improves our tracking of pending inferences in strings so that we record pending inferences as a triple (id, fact, exp). This will ensure that proof steps can be constructed at the time we decide to process facts. It also inlines the sendInfer method into sendInference for simplicity.
This also improves the policy for reference counting facts and their explanations: we add them to d_keep when they are added to the equality engine. Previously, we were adding them when they were registered as pending. This means we would collect facts in this pending set that were added but later abandoned, which is unnecessary.
|
|
|
|
|
|
This PR makes it so that the module dependencies in the theory of strings are acyclic. This is important for further organization towards proofs for strings.
The main change in this PR is to ensure that InferenceManager has a pointer to ExtTheory, which is needed for several of its methods. This required changing several solvers into unique_ptr to properly initialize.
|
