summaryrefslogtreecommitdiff
path: root/src/theory/arith/nl
AgeCommit message (Collapse)Author
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-25Ensure nonlinear extensions properly reconsiders its model (#6204)Gereon Kremer
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.
2021-03-21Clean up remaining raw uses of output channel (#6161)Andrew Reynolds
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.
2021-03-15Make nonlinear extension account for relevant term set (#6147)Andrew Reynolds
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.
2021-03-11Make linear arithmetic use its inference manager (#5934)Gereon Kremer
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.
2021-03-11arith proof rules shuffle & add ARITH_SUM_UB (#6118)Alex Ozdemir
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.
2021-03-11Use CVC4_ASSERTIONS instead of NDEBUG. (#6099)Mathias Preiner
Ensures that all checks are performed in production builds with enabled assertions.
2021-03-10Improve arithmetic proofs (#6106)Gereon Kremer
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.
2021-03-09Some more cleanup of includes (#6083)Gereon Kremer
This PR does some more cleanup of the includes.
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-04Add proper define for libpoly usage (#6050)Gereon Kremer
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.
2021-03-03More cleanup of includes to reduce compilation times (#6037)Gereon Kremer
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.
2021-03-02Clean up includes to reduce compile times (#6031)Gereon Kremer
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.
2021-02-24Enable -Werror. (#5969)Mathias Preiner
2021-02-24(proof-new) Add proofs for CAD solver (#5981)Gereon Kremer
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.
2021-02-23Add proof for mult sign lemma (#5966)Gereon Kremer
This PR adds the proof for a nonlinear refinement lemma that infers the sign of a monomial from the sign of the variables.
2021-02-23Add proof for monomial bounds check (#5965)Gereon Kremer
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.
2021-02-23(proof-new) Add proof generator for CAD solver (#5964)Gereon Kremer
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.
2021-02-22Add trans secant proofs. (#5957)Gereon Kremer
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.
2021-02-22(proof-new) Add proofs for exponential functions (#5956)Gereon Kremer
This PR adds proofs for lemmas concerned with the exponential function. If also adds the necessary proof rules and corresponding proof checker.
2021-02-22(proof-new) Add proofs for sine lemmas in the transcendental solver (#5952)Gereon Kremer
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.
2021-02-22Cleanup in transcendental solver, add ApproximationBounds struct. (#5945)Gereon Kremer
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.
2021-02-22add pruneRedundantIntervals (#5950)Gereon Kremer
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.
2021-02-19Refactoring theory inference process (#5920)Andrew Reynolds
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.
2021-02-19Cleanup of inferences in arithmetic theory (#5927)Gereon Kremer
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
2021-02-15Remove now obsolete sendLemmas and inferences stat from arith::nl (#5903)Gereon Kremer
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.
2021-02-11Add InferenceId member to TheoryInference, adapt all derived classes. (#5894)Gereon Kremer
This PR adds a new InferenceId member to the TheoryInference class. All classes derived from TheoryInference are adapted accordingly.
2021-02-11Merge InferenceIds into one enum (#5892)Gereon Kremer
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.
2021-02-10Fix open proof for factoring lemma (#5885)Andrew Reynolds
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.
2021-02-08Avoid spurious traversal of terms during preregistration (#5860)Andrew Reynolds
This simplifies a few places in the code which unecessarily traverse terms during preregistration (which already traverses terms).
2021-02-02Improvements for NL traces (#5846)Andrew Reynolds
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.
2021-02-01Eliminate PREPROCESS lemma property (#5827)Andrew Reynolds
This is now possible since we always preprocess lemmas. Note that the LemmaProperty on inferences may be redundant throughout the non-linear solver now.
2021-01-07Make sure polynomials are properly factorized in nl-cad (#5733)Gereon Kremer
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.
2020-12-22Add proofs for nonlinear sign lemmas. (#5707)Gereon Kremer
This PR adds proof support for NL_SIGN lemmas.
2020-12-21Add proof for pi bound lemma (#5709)Gereon Kremer
This PR adds proofs for lemmas that introduce bounds on the constant representing pi.
2020-12-21Add proof for sine shift lemmas. (#5710)Gereon Kremer
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.
2020-12-21(proof-new) Make nl-ext factoring lemmas proof producing. (#5698)Gereon Kremer
This PR adds proofs for the lemmas from the nonlinear factoring check.
2020-12-18(proof-new) Setup proof infrastructure for transcendental solver (#5703)Gereon Kremer
This PR introduces the infrastructure for adding proofs to the transcendental solver: a CDProofSet to easily create new proofs a proof checker
2020-12-18Add proof checker for nl tangent lemma (#5704)Gereon Kremer
This PR is a follow-up to #5700 which lacked the proof checker for the proof that was added for nonlinear tangent plane lemmas.
2020-12-18(proof-new) Add proof for tangent plane lemmas (#5700)Gereon Kremer
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.
2020-12-18Add proof for split zero check. (#5699)Gereon Kremer
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.
2020-12-17(proof-new) Prepare nonlinear extension and nl-ext for proofs. (#5697)Gereon Kremer
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
2020-12-09Fixed a bunch of clang warnings. (#5637)Gereon Kremer
2020-12-08Split initial exp lemma into separate lemmas. (#5622)Gereon Kremer
This PR refactors the initial lemmas for the exponential function, very similar to the sine lemmas.
2020-12-07Add bitwise refinement mode for IAND (#5328)makaimann
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.
2020-12-07Refactor initial phase of transcendental solver (#5599)Gereon Kremer
This PR refactors the initialization of the transcendental solver, decoupling the setup of generic caches from initial lemmas for exponential and sine functions.
2020-12-02Update copyright headers.Aina Niemetz
2020-12-01Refactor transcendental solver (#5539)Gereon Kremer
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).
2020-11-26Make CAD solver work for empty set of assertions (#5535)Gereon Kremer
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 .
2020-11-25Fix transcendental secant plane lemmas (#5525)Gereon Kremer
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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback