Age | Commit message (Collapse) | Author |
|
|
|
In certain cases, the nonlinear extension would not re-check properly but only repeat an (already failed) model repair. The result lemma would then already be in cache and thus not be sent to the solver.
This PR ensures that modelBasedRefinement is always run and entirely removes the d_builtModel flag that was responsible for this behavior. Additionally, it asserts that the lemma that (tries to) force the model to be reconciled during theory combination is actually sent.
Fixes #6192.
|
|
After this PR, with only a few exceptions, all calls to output channel for lemmas, conflicts are made through inference manager.
This is work towards standardizing the statistics for theories.
|
|
This fixes a subtle issue with non-linear and theory combination.
It currently could use irrelevant terms preregistered to the ExtTheory for its model-based refinement. This means that the non-linear extension could accidentally modify values for terms that are not included in its term set, violating theory combination.
In particular, in the minimized example from #5662, (* a k) was a stale term in ExtTheory, and non-linear extension falsely believed that a was a term whose model value could be modified, since moreover a was not a shared term. In reality, a was not a shared term since it only was registered to UF.
Fixes #5662.
|
|
This PR refactors the linear arithmetic solver to properly use its inference manager, instead of directly sending lemmas to the output channel. To do this, it introduces new InferenceIds for the various linear lemmas.
|
|
Preparation for making ARITH_SCALE_SUM_UB a macro.
Adds a proof rule for summing upper bounds: ARITH_SUM_UB.
Moves ARITH_MULT_* rules from the non-linear extension to the main
arithmetic checker, since they will be needed for all of arith now.
Aligns the ARITH_SCALE_SUM_UB documentation with its checker.
|
|
Ensures that all checks are performed in production builds with enabled assertions.
|
|
The proof rules for ARITH_MULT_POS and ARITH_MULT_NEG were complex than necessary in that they incorporated a rewriting step. This PR removes rewriting from these rules, making them cleaner and easier to understand.
The proof now applies these simpler rule and uses MACRO_SR_PRED_TRANSFORM to prove the lemma that is actually added.
|
|
This PR does some more cleanup of the includes.
|
|
|
|
When adding libpoly, we forgot to add a proper define to cvc4autoconfig and included real_algebraic_number.h everywhere to get this define. This PR introduces the CVC4_POLY_IMP define and removes all obsolete includes to real_algebraic_number.h.
|
|
Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.
|
|
This PR cleans up a ton of includes, based on the suggestions of iwyu.
Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.
|
|
|
|
This PR adds proofs for the CAD solver, based on the proof generator from the previous PR.
Note that the level of detail of these CAD proofs is significantly higher than for other proofs. Making these proofs more fine-grained and maybe at some point accessible to proof checkers is probably still quite a bit of work.
Thus, the CAD proof rules are both trusted rules for now.
|
|
This PR adds the proof for a nonlinear refinement lemma that infers the sign of a monomial from the sign of the variables.
|
|
This PR adds proofs for a nonlinear refinement lemma that deals with multiplication of inequalities with some term. This lemma is split into two proof rules for positive or negative factors.
|
|
This PR adds a proof generator for the CAD solver, including two new proof rules. The code is not yet used, but will be integrated into the CAD solver itself in another PR.
|
|
This PR adds proofs for secant lemmas in the transcendental lemmas for both exponential and sine functions.
It also adds proof rules and corresponding proof checkers.
|
|
This PR adds proofs for lemmas concerned with the exponential function. If also adds the necessary proof rules and corresponding proof checker.
|
|
This PR adds proofs for the lemmas related to the sine function in the transcendental solver.
It introduces several new proof rules with corresponding proof checkers and produces proofs in the sine solver.
|
|
This PR merges some cleanup in the transcendental solver from proof-new.
It adds a new struct ApproximationBounds that replaces an opaque std::vector and does some general refactoring in the TaylorGenerator class, removing dead code and using fixed-width integers.
|
|
Adds a simple helper for CAD to prune redundant intervals. It is just a wrapper for cleanIntervals right now, but will be responsible to making sure the CAD proof is pruned as well.
|
|
This PR refactors TheoryInference so that it is not responsible for calling back into InferenceManager, instead it sets data so that InferenceManagerBuffered has enough information to do this itself. It also makes the decision of whether to cache lemmas in theory inference manager a global choice per-theory instead of per-lemma.
|
|
This PR cleans up several issues in the arithmetic theory mostly related to its usage of InferenceId and the TheoryInferenceManager:
remove the ArithLemma class and uses SimpleTheoryLemma instead
only use NlLemma if we actually need it
use proper InferenceIds everywhere
remove unused code in the nonlinear extension
|
|
This PR removes some obsolete code from the nonlinear solver.
The statistics will soon be replaced by a generic statistic in the theory inference manager.
|
|
This PR adds a new InferenceId member to the TheoryInference class.
All classes derived from TheoryInference are adapted accordingly.
|
|
This PR is the first step in consolidating the various variants of Inferences, InferenceIds and InferenceManagers of the theories.
It merges all InferencedIds into one global enum and makes all theories use them.
|
|
We need to add to the current proof, regardless of whether we have used the factor skolem previously.
Fixes bugs found by @HanielB on SMT-LIB runs.
|
|
This simplifies a few places in the code which unecessarily traverse terms during preregistration (which already traverses terms).
|
|
This makes it so that -t nl-ext is a concise summary of what the nl-ext solver is doing, which I use frequently for debugging.
This is a temporary solution, we should consider a deeper refactoring of traces throughout NL at some point.
|
|
This is now possible since we always preprocess lemmas.
Note that the LemmaProperty on inferences may be redundant throughout the non-linear solver now.
|
|
CAD theory (used in nl-cad) requires that polynomials are properly factorized (a finest square-free basis). This PR replaces usage of raw std::vector by a new wrapper PolyVector that ensures proper factorization whenever a polynomial is added. This fixes one piece of code that omitted factorization, leading to soundness issues as in #5726.
Fixes #5726.
|
|
This PR adds proof support for NL_SIGN lemmas.
|
|
This PR adds proofs for lemmas that introduce bounds on the constant representing pi.
|
|
This PR adds proofs for the sine shift lemmas that add equivalent instances of the sine function where the argument is in its "main phase" between minus pi and pi.
|
|
This PR adds proofs for the lemmas from the nonlinear factoring check.
|
|
This PR introduces the infrastructure for adding proofs to the transcendental solver:
a CDProofSet to easily create new proofs
a proof checker
|
|
This PR is a follow-up to #5700 which lacked the proof checker for the proof that was added for nonlinear tangent plane lemmas.
|
|
This PR adds a proof for the tangent plane lemmas from nl-ext.
As this lemma uses some insight about the tangent plane of a multiplication term, this PR adds a new proof rule.
|
|
This PR adds a proof for the nl-ext check to split at zero. As we can use the SPLIT rule, this requires no new proof rule.
|
|
This PR prepares the nonlinear extension itself and the nl-ext part for proofs. In particular
we add a proof checker for nl-ext
we add a CDProofSet for nl-ext
|
|
|
|
This PR refactors the initial lemmas for the exponential function, very similar to the sine lemmas.
|
|
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 PR refactors the initialization of the transcendental solver, decoupling the setup of generic caches from initial lemmas for exponential and sine functions.
|
|
|
|
This PR does another round of refactoring on the transcendental solver. It cleans up some variable names, introduces an enum type for Convexity and passes both the intended taylor degree and the actual taylor degree (which will be needed for proofs).
|
|
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 .
|
|
The refactoring of the transcendental solver introduced a subtle issue that lead to incorrect secant plane lemmas.
This PR fixes this issue, so that we now produce the correct lemmas again.
|