| Age | Commit message (Collapse) | Author |
|---|
|
Leads to free variables in assertions when using `str.<=` whose reduction uses EXISTS not FORALL.
Fixes #5483.
|
|
This PR fixes #5460 by adding posRewriteEqual to bags rewriter
|
|
(#5502)
|
|
|
|
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).
|
|
|
|
This works towards having the symFPU headers only included where it's
absolutely needed (only in the .cpp files, not in any other headers).
Note: src/util/floatingpoint.h.in will be converted to a regular .h file
in the next step to simplify reviewing.
|
|
|
|
Uses new nested-qe utility for eliminating nested quantification before doing quantifier elimination.
Fixes CVC4/cvc4-wishues#26
Fixes #5484.
|
|
printModel no longer makes sense if the list of declared symbols is managed outside the solver.
Also, mkConst needs a variant to distinguish a provided name of "" vs. a name that is not provided.
|
|
|
|
This is required to make the cvc parser work properly with the new version of getting models based on the symbol manager.
|
|
This PR replaces the LazyCDProofSet, that was hardcoded to use LazyCDProof objects, by a templated CDProofSet.
|
|
This PR prepares the addition of proofs for the arithmetic theory by making addPendingArithLemma() accept a ProofGenerator*.
|
|
(#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.
|
|
(#5478)
|
|
Also fixes some whitespace issues in printing quantified formulas.
|
|
This further removes obsolete explicit includes of stdint.h.
|
|
This has static utilities for doing nested quantifier elimination and some data structures for maintaining a context-dependent set of quantified formulas that have been processed.
This is work towards CVC4/cvc4-wishues#26, and work reimplementation of the option --ceqgi-nested-qe.
|
|
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 uses the symbol manager for handling names for unsat cores.
This replaces interfaces in SmtEngine for managing expression names. It removes the SetExpressionName command.
|
|
|
|
This utility will replace the dagification visitor for printing lets for Node in the smt2 printer, and will be used further in e.g. LFSC proof printing.
|
|
|
|
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.
|
|
This replaces the previous methods for get-assignment which involving making a DefinedNamedFunctIonCommand and storing the expression names map in the SmtEngine.
Note: we now limit :named terms to those not beneath quantifiers and let-bindings.
|
|
Should fix the nightlies.
|
|
|
|
This cleans up the src/util/floatingpoint.h.in header to conform to the
code style guidelines of CVC4. This further attempts to fully document
the header. The main changes (except for added documentation) are
renames of member variables, getting rid of the redundant functions
FloatingPointSize::exponent() and FloatingPointSize::significand(),
and a more explicit naming of CVC4 wrapper types vs symFPU trait
types. Else, it's mainly reordering and formatting.
|
|
The previous refactoring of tangent plane lemmas introduced incorrect lemmas.
This PR fixes this issue and actually generated the lemmas described in the comment.
Fixes #5452.
|
|
The original lemma only proposed an implication for the tangent plane lemmas, while our implementation adds the inverse implication as well (in a somewhat verbose way).
This PR replaces this by simply constructing the equivalence.
|
|
This changes the default of Parser::pushScope and prepares symbol manager further for maintaining expression names.
|
|
The main goal of the resource limitation mechanism (via `--rlimit`) is to have a deterministic limitation on runtime. The ultimate goal would be that the actual runtime grows linearly with the spent resources.
To achieve this, this PR does the following:
- introduce new resources spent in places that are not yet covered
- find resource weights that best approximate the runtime
It provides a contrib script `learn_resource_weights.py` that uses statistics from a given benchmark run and uses linear regression to find good resource weights. The script also evaluates this estimate and identifies outliers, benchmarks for which this approximation is particularly bad. This probably indicates that on such a benchmark, some part of the code takes a significant amount of time but is not yet represented by a resource.
Eventually, we should use the resulting resource weights as defaults for the options like `--rewrite-step`, `--theory-check-step`, etc.
|
|
Fixes #5384.
Previously we were not breaking on conflict in all cases.
|
|
Adds proof support in non-clausal simplification, connecting the proofs from circuit propagator.
|
|
This enables initial proof support in datatypes, which includes connecting the inference-to-proof constructor to the inference manager and making the proper calls to the inference manager using TheoryDatatypes.
|
|
This PR relates to #4987 .
Our plan is to:
delete the model keyword
avoid printing extra declarations by default
wrap UF values with as expressions.
This PR is step 2. It allows the user to choose the model printing style in case of uninterpreted elements: either using datatypes, or using declare-sorts and declare-funs or just using declare-funs.
The default option, which is closest to the standard, is just using declare-funs. In step 3, these will be replaced by abstract values using as.
|
|
This is in preparation for having the symbol manager manage expression names at the parser level instead of inside SmtEngine.
This adds some necessary features regarding scopes and global declarations.
This PR still does not change the behavior of the parser.
|
|
Fixes #5428.
|
|
This simplifies the sygus solver based on the fact that verification lemmas are always processed in a separate subsolver.
In particular, this means that the implementation of --sygus-stream can be simplified signficantly.
|
|
Fixes the case where the type of the function is not a function type.
|
|
This PR relates to #4987 .
Our plan is to:
delete the model keyword
avoid printing extra declarations by default
wrap UF values with as expressions.
This PR does step 1, and fixes regressions accordingly.
|
|
This fixes potential cycles in assertLemma commands in the proof equality engine by using separate proof data structures for the topmost 2 stages of proof generation for equality engine proofs. This fix is required to support datatype proofs for lemmas.
This PR also removes support for the ProofStepBuffer interface in ProofEqEngine, since it is unused, and suffers similar issues and would require a different unique fix.
|
|
This ensures we do manual exclusion of candidate solutions that have counterexamples that are repeated, in particular in the case where the synthesis conjecture has no free variables.
This PR removes special casing for ground synthesis conjectures and fixes the exclusion during the refinement stage of sygus.
This is a prerequisite for updating arithmetic to not eliminate extended operators at expand definitions, which forces this feature to be exercised in a number of regressions.
|
|
This adds support for proofs in the quantifiers module that performs skolemization.
Also fixes a bug in the proof checker for skolemization.
|
|
This ensures we construct proper proofs for propagations whose conclusions are of the form (=> true lit). Literals may be propagated with "true" as an explanation in datatypes, e.g. discriminators for datatypes with 1 constructor.
|
|
This improves trace/error messages for proof-new-pedantic, and also merges the proof-new-pedantic-eager with the proof-new-eager-checking option.
|
|
This adds the module that constructs proofs from inference steps.
A followup PR will integrate proof support into the datatypes inference manager.
|
|
This follows a similar style to symbol_table.h/cpp. This is required since context dependent data structures are cvc4_private, and symbol manager is cvc4_public.
|
|
This is required since symbol manager will use context dependent data structures (in its cpp).
This is required since classes in src/parser/ are not allowed to include private headers.
|
