| Age | Commit message (Collapse) | Author |
|---|
|
This simplifies preprocessing so that the only call to theory-preprocess and ite-removal is at the very end. (One exception is early-theory-pp which is used by default in combination with ite-simp to maintain the performance on QF_LIA/nec).
This is in preparation for making theory preprocessing happen lazily, post-CNF conversion.
@HanielB has done SMT-LIB performance runs, see below.
|
|
This avoids a solution soundness issue when disabling all NL strategies and using --nl-rlv=always.
|
|
This is required to avoid failures in the planned refactoring of check-models.
This removes the SMT-LIB 2.5 semantics option for bvdiv/bvrem.
It still remains to merge the BITVECTOR_UDIV / BITVECTOR_UDIV_TOTAL kinds, calling the total version "BITVECTOR_UDIV", and analogously for UREM.
FYI @barrettcw
|
|
This ensures that datatype selectors are properly handled as triggers in E-matching.
This is challenging since selectors in quantified formulas are of kind APPLY_SELECTOR but are theory-preprocessed to APPLY_SELECTOR_TOTAL/APPLY_UF. Hence, we must match on 2 possible operators, and ones that do not match the operator of the trigger. This adds a custom candidate generator for this case.
It also removes a deprecated option that is no longer used (in part due to our use of shared selectors).
This is in preparation for further work on optimizing cvc4 on benchmarks from Facebook.
Note that there is not a convienient way to call expandDefinitions currently (which is required to get the proper operators to match). This PR calls smt::getCurrentSmtEngine() to do this, although we should find a better solution soon, e.g. adding expandDefinitions to the rewriter.
FYI @barrettcw
|
|
This makes preregistration of terms SAT-context dependent in strings instead of user-context dependent.
Fixes #5547.
This is required to avoid model unsoundness on sequence benchmarks, as demonstrated in that issue.
It furthermore impacts how we have been handling theory combination with arithmetic for str.len and impacts how propagation is setup for the strings equality engine.
I will do performance testing on this PR.
|
|
#5293 pointed to assertion failures when employing --bv-to-int, starting from commit 94e3d9a.
The bug is not reproduced on current master, and so we would have this PR close #5293 .
This PR adds the benchmarks from #5293 .
|
|
There is an assumption that is not guaranteed to hold in this rule, thus we should not try to explain in the equality engine.
Fixes #5611.
Note this inference was not previously covered in our coverage build.
|
|
This adds a net +82 regressions to regress[0-2] and adds several additional disabled regressions to regress3 and regress4. This involved fixing the status on several regressions, and ensuring CMakeLists.txt includes all files (exactly once) in the test/regress/ subdirectory.
It also moves several regressions to the proper regression levels (those that take >30 seconds in debug are moved to regress3+).
|
|
This PR makes decision engine independent of AssertionsPipeline, which consequently allows some of the key PropEngine interfaces to be consolidated. It also modifies PropEngine to take TrustNode for assertLemma, which is the first step for making PropEngine manage proofs from TheoryEngine.
This is in preparation for modifying the interplay between PropEngine, TheoryEngine, TheoryPreprocessor, and new proposed SAT relevancy heuristic.
There are no intended behavior changes in this PR.
Marking "major" since this impacts several current directions (including proof-new integration, lazy theory preprocessing, SAT relevancy).
|
|
This removes benchmarks for the following reasons:
- regress1/arith/arith-int are removed since there are many similar regressions (10 from this set are already enabled)
- bitvector cvc benchmarks are removed since their *.smt2 benchmarks are enabled
- other benchmarks are removed due to features we do not plan to support
- one placeholder benchmark is removed
|
|
Previously was a bug computing the argument types of parametric datatypes.
|
|
This PR adds a regression from #1978 that has been fixed in the meantime.
Closes #1978 .
|
|
This PR fixes #5448. SynthFunCommand::toStream used to call d_grammar->resolve even when d_grammar is a nullptr. This PR fixes the issue and modifies the signature of Printer::toStreamCmdSynthFun to make it clear that grammar is an optional argument.
|
|
preprocessing pass (#5620)
#5544 enforces expandDefinition not to run before preprocessing.
The bv-to-int preprocessing pass used to rely on expandDefinition to replace BITVECTOR_UDIV and BITVECTOR_UREM with their _TOTAL versions.
This PR performs the replacement in the preprocessing pass itself.
A regression that timed out is now fixed and is brought back to the regressions.
|
|
This is required for handling inputs that combine strings and sequences.
Fixes #5542.
|
|
Expand definitions for sequences was wrong in two ways: (1) we replaced str.from_code with a witness term. This led to it being unevaluatable in models. (2) we did not handle seq.nth, meaning its model value was unevaluatable if it was out of bounds. Now it evaluates the value of the uninterpreted function we replace with.
This corrects both issues and adds a regression to demonstrate both kinds of terms evaluate correctly.
To do this, I added a helper function to skolem cache as well as a new (internal-only) kind SEQ_NTH_TOTAL. Notice applications of this kind should only be used for model evaluation.
Notice this fixes several check-model warnings in the regressions. It still does not fix others since other things must be corrected for model evaluation (e.g. expandDefinitions must be applied on theory assertions for --debug-check-models). This will be done in later PRs.
|
|
Fixes #5543.
Recently we changed our model construction for sequences here: #5391.
This fix is not safe for sequences of sequences, where Valuation::getModelValue should not be called, since the argument of the seq.unit is not a shared term.
This makes our model construction for sequences more robust, however I'm not sure this is the end solution. In particular, it is still questionable whether we should call Valuation::getModelValue at all (consider sequences of theories whose model construction comes after strings), or for cases of (seq.unit x) where x is a sequence or string that does not have a concrete value. Regardless, this PR could be merged in the meantime since it should definitely fix some of the current issues.
|
|
Fixes #5370, #5462.
|
|
This corrects an issue where terms internal to datatypes were not getting properly registered e.g. as part of the indices that determine the care graph, due to a context-independent cache being used (when a SAT-context-dependent one was required).
This reenables the fact vs lemma optimization in datatypes, as it is conjectured to be correct.
|
|
Adds an option to do "bitwise" comparisons in the lazy IAND solver. Instead of creating an exact match for the value of a term using a sum, this would lazily fix groups of bits using integer extracts (divs and mods) when the abstract and concrete values differ at those bits.
For example, with a 1-bit granularity, you might learn a lemma like:
((_ iand 4) x y), value = 1
actual (2, 3) = 2
bv-value = #b0001
bv-actual (#b0010, #b0011) = #b0010
IAndSolver::Lemma: (let ((_let_1 ((_ iand 4) x y)))
(and (and true
(= (mod _let_1 2) (ite (and (= (mod x 2) 1) (= (mod y 2) 1)) 1 0)))
(= (mod (div _let_1 2) 2) (ite (and (= (mod (div x 2) 2) 1) (= (mod (div y 2) 2) 1)) 1 0))))
; BITWISE_REFINE
which is just forcing the bottom two bits of the iand operator result to implement bitwise-AND semantics.
|
|
This was caused by the quantifiers rewriting eliminating extended arithmetic operators, which was required due to the way counterexample-guided quantifier instantiation used to work with preprocessing. The technique is now more robust and this option can be deleted.
This fixes a debug assertion failure from UFNIA SMT-LIB, a minimized benchmark is included as a regression.
|
|
This updates the preprocessor so that expand definitions does not expand theory symbols at the beginning of preprocessing.
This also restores the previous expandDefinitions method in arithmetic, which is required for correctly interpreting division by zero in models, but should not be applied at the beginning of preprocessing. Moreover it ensures that only partial operators are eliminated in arithmetic expandDefinitions, which required an additional argument partialOnly to arith::OperatorElim.
This adds -q to suppress warnings for many quantified regressions which now emit warnings with --check-model. This will be addressed later as part of CVC4/cvc4-wishues#43.
The purpose of this PR is two-fold:
(1) Currently our responses to get-value are incorrect for partial operators like div, mod, seq.nth since partial operators can be left unevaluated.
(2) The preprocessor should have the opportunity to rewrite and eliminate extended operators before they are expanded. This is required for addressing performance issues for non-linear arithmetic. It is also required for ensuring that trigger selection can be done properly for datatype selectors (to be addressed on a later PR).
|
|
The error from #4927 has been fixed in the meantime, this PR adds the example as regression.
Closes #4927.
|
|
An AND was constructed from a vector that may only hold a single or no element.
This PR uses mkAnd instead.
Fixes #5550 .
|
|
This PR relates to #4987 .
Our plan is to:
delete the model keyword (done in #5415 )
avoid printing extra declarations by default (done in #5432 )
wrap UF values with as expressions.
This PR does step 3, fixes a regression accordingly, and adds the formula from #4987 and a variant of it to the regressions.
|
|
|
|
|
|
Fixes #5524.
|
|
The error from #3687 has been fixed in the meantime.
This PR adds the two examples from this issue as regressions.
Closes #3687
|
|
This corrects two issues related to model declarations:
(1) model declaration terms were mistaken not cleared,
(2) the model needs to be explicitly destructed before the node manager because it contains references to Node.
Fixes #5540
|
|
This commit improves our rewriting of str.<= slightly. If we have
constant prefixes that are different, we can always rewrite the term to
a constant. Previously, we were only doing so when the result was
false.
|
|
The issue from #5099 has been fixed in the meantime, this PR adds the examples as regressions.
Closes #5099.
|
|
The error from #4335 has been fixed in the meantime, this PR adds a regression for this issue.
Closes #4335.
|
|
The error from #4707 has been fixed in the meantime, this PR adds the example inputs as regressions.
Closes #4707.
|
|
Fixes #5506, fixes #5507.
|
|
A COMMAND was used instead of COMMAND-LINE.
|
|
When called with no assertions, the CAD solver would still go to work and then segfault when trying to access the first variable.
This PR adds an explicit check for this case and adds a regression.
Fixes #5534 .
|
|
This optimization needs more work to determine its correctness. It is currently leading to incorrect candidate models on Facebook benchmarks.
|
|
We can close #5520, we can close #5378.
|
|
This makes symbol manager be in charge of determining which sorts and terms to print in response to get-model. This eliminates the need for the parser to call ExprManager::mkVar (and similar methods) with custom flags.
This requires significant simplifications to the printers for models, where instead of a NodeCommand, we take a Sort or Term to print in the model.
This is one of the last remaining steps for migrating the parser to the new API.
The next step will be to remove a lot of the internal infrastructure for managing expression names, commands to print in models, node commands, node listeners, etc.
|
|
The issue was caused by simple regular expression consume being too aggressive when a recursive call was made to the method. In particular, we were assuming that the body of the star must be unrolled to fully consume a string, when it can be skipped if we are not at top level.
Fixes #5510.
|
|
UF uses expandDefinitions to convert fully applied HO_APPLY to APPLY_UF. The more appropriate place to do this is in Theory::ppRewrite.
|
|
Leads to free variables in assertions when using `str.<=` whose reduction uses EXISTS not FORALL.
Fixes #5483.
|
|
Now that extended arithmetic symbols are not eliminated during expandDefinitions, this allowed for a chain of events that would not apply theory preprocessing on certain terms.
In particular, a term t would not have theory preprocessing applied to it if it was a strict subterm of ITE-term s that occurred in a term position in a quantified formula body, and s did not have free variables. In this case, term formula removal would add a lemma corresponding to the ITE skolem definition, whose subterms did not have theory preprocessing applied. This meant that a (div a d) term was not being preprocessed in #5482, leading to solution unsoundness.
This changes the policy in term formula removal to be in sync with theory preprocessing: term formula removal and theory preprocessing only apply to terms that are not beneath quantifiers. In particular, this means that ground terms in quantifier bodies are left untouched until they are introduced e.g. by instantiation.
This fixes the solution soundness issue (fixes #5482).
|
|
Uses new nested-qe utility for eliminating nested quantification before doing quantifier elimination.
Fixes CVC4/cvc4-wishues#26
Fixes #5484.
|
|
(#5477)
This replaces the old implementation of CEGQI based on nested quantifier elimination (--cegqi-nested-qe) with the new implementation.
The previous implementation used some convoluted internal attributes to manage dependencies between quantified formulas, the new implementation is much simpler: it simply eliminates nested quantification eagerly.
Fixes #5365, fixes #5279, fixes #4849, fixes #4433.
This PR also required fixes related to how quantifier elimination is computed.
|
|
Also fixes some whitespace issues in printing quantified formulas.
|
|
This fixes 2 issues related to eliminating arithmetic operators:
(1) counterexample lemmas in CEGQI were not being preprocessed
(2) ensureLiteral was not doing term formula removal.
This corrects these two issues. Now ensureLiteral does full theory preprocessing on the term we are ensuring literal for, meaning this may trigger lemmas if the term contains extended arithmetic operators like div.
Fixes #5469, fixes #5470, fixes #5471.
This adds --sygus-inst to 2 of these benchmarks which moreover makes them solvable.
This also improves our assertions and trace messages.
|
|
|
|
This PR makes it so that extended arithmetic operators are not expanded during expand definitions. Instead they are eliminated at theory preprocessing, which occurs as the last step of preprocessing.
The motivation for this is three fold:
(1) Some quantified LIA benchmarks lead to CVC4 failing to eliminate div functions from quantifier instantiation, this leads to spurious logic failures. A regression is included, which now is correctly solved.
(2) We should allow better rewriting and preprocessing for extended arithmetic functions, especially for div/mod which is important for many users of QF_NIA.
(3) More generally,Theory::expandDefinitions will be deleted. All functionalities in expandDefinitions should move to Theory::ppRewrite.
This changes impacts many benchmarks that involve non-linear and quantifiers:
Many benchmarks (as expected) give a warning during check-models since (/ n 0) cannot be evaluated. I've added -q to disable these warnings. Fully addressing this is part of an agenda to improve our support for --check-models.
Several fuzzing benchmarks involving NL+quantifiers now time out. However, several can be solved by --sygus-inst, which is now the preferred instantiation strategy for NL+quantifiers.
2 other non-linear regressions time out, which are disabled in this PR.
one sygus-inference benchmark (regress1/sygus/issue3498.smt2), now correctly times out (previously it did not timeout since the preprocessor was unable to apply sygus-inference and resorted to normal methods, now sygus-inference can apply but as expected times out).
Fixes #5237.
|
