summaryrefslogtreecommitdiff
path: root/src/theory/arith/nl/nonlinear_extension.cpp
AgeCommit message (Collapse)Author
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Add identifiers for extended function reductions (#6314)Andrew Reynolds
This adds identifiers for extended function reductions, which are reasons for why an extended term no longer needs to be processed. The motivation is help understand check-model failures. This PR adds identifiers to the ExtTheory utility. It also cleans up some unused parts of this utility. Some blocks of code changed indentation in this class.
2021-04-08Add identifiers for sources of incompleteness (#6311)Andrew Reynolds
This PR classifies all internal kinds of incompleteness as identifiers. It makes it so TheoryEngine records an identifier when its incomplete flag is set. The next step will be to possibly communicate this value to the user.
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-04-01Fix non-linear for unknown case (#6252)Andrew Reynolds
As a result of this issue, currently we are incorrectly trying to repair a model when one is not guaranteed to exist, leading to a spurious assertion failure. Fixes #6228. The benchmarks on that issue now answer "unknown" without an assertion failure.
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-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-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-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-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-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-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.
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 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-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-11-16Improve accuracy of resource limitation (#4763)Gereon Kremer
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.
2020-11-05Remove mkSingleton from the API (#5366)mudathirmahgoub
This PR removes mkSingleton from the API after removing subtyping from set theory and introducing mkInteger to the API. Instead the user needs to use Solver::mkTerm(api::SINGLETON, element) where element has the right type. Internally NodeManager::mkSingleton(type, element) is still needed to determine the type of the set. Other changes: Renamed Solver::mkTerm(Op op, .. functions to Solver::mkTermFromOp(Op op, ... Added mkTermFromOp to the python API
2020-11-03Reset built model flag at presolve in nonlinear (#5386)Andrew Reynolds
Fixes a bug in incremental with non-linear where the built model flag would still be true on the first call to check in a 2nd call to check-sat in incremental mode. This occurs when we are under the same SAT context when the model was built (likely level 0) on the subsequent check-sat call. Fixes #5372
2020-10-30Use BoundInference in nonlinear extension (#5359)Gereon Kremer
Currently the NonlinearExtensions uses a custom logic to eliminate redundant bounds and perform tightening on bound integer terms. As these replacements are not recorded, incorrect conflicts are being sent to the InferenceManager. This PR replaces this logic by the BoundInference class and fixes the issues with conflicts by - allowing BoundInference to collect bounds on arbitrary left hand sides (instead of only variables), - improving origin tracking in BoundInference by explicitly constructing the new bound constraints, - adding tightening of integer bounds, - emitting lemmas instead of conflicts, and finally - replacing the current logic by using the BoundInference class.
2020-10-28Fixes for unconstrained variables in nonlinear model (#5351)Andrew Reynolds
This ensures that we explicitly mark x -> 0 as part of the arithmetic model coming from nonlinear for unconstrained variables x that nonlinear extension assumes to be 0. This fixes #5348.
2020-10-28Split NlSolver in multiple subsolvers (#5315)Gereon Kremer
The NlSolver started as one place for nonlinear reasoning, but has grown significantly since. This PR splits the NlSolver class into multiple smaller classes.
2020-09-30Add strategy for nonlinear extension (#5160)Gereon Kremer
This PR adds a flexible strategy for the nonlinear extension that replaces the handwritten code in checkLastCall().
2020-09-29Clean up nonlinear extension (#5149)Gereon Kremer
This PR performs some cleanups in the nonlinear extension, in particular it removes the old lemma collection scheme. It is no longer needed, as all subsolvers use the inference manager.
2020-09-26Use inference manager for nl_solver (#5125)Gereon Kremer
This PR migrates the nl_solver part of the nonlinear extension to use the new inference manager as well. It adds a new method clearWaitingLemmas to the inference manager and uses ArithLemma (though NlLemma exists) as we don't need the additional functionality of NlLemma.
2020-09-23Make IAND solver use inference manager. (#5126)Gereon Kremer
This PR moves the iand solver (within the nonlinear extension) to use the new inference manager to send lemmas.
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
2020-09-22ICP-based solver for nonlinear arithmetic (#5017)Gereon Kremer
This PR adds a new icp-based solver to be integrated into the nonlinear extension. It is not meant to be used as a stand-alone ICP solver. It does not implement splits (only propagations) and implements a rather aggressive budget mechanism that aims to quickly stop propagation to allow other solvers to take over. Additionally, it enforces a maximum bit size to avoid divergence.
2020-09-17Use new inference manager in transcendental solver (#5022)Gereon Kremer
This refactors the transcendental solver to add lemmas to the new inference manager instead of using the old lemma collection scheme.
2020-09-04Use arith::InferenceManager for CAD lemmas (#5015)Gereon Kremer
This makes the CAD solver use the new arith::InferenceManager instead of the previously used lemma collection scheme.
2020-09-03Basic integration of arith::InferenceManager (#4999)Gereon Kremer
This PR adds a first basic integration of the arith::InferenceManager into the arithmetic theory and the nonlinear extension in particular. While the lemma collection mechanism (in the nonlinear extension) remains unchanged, the lemmas are ultimately not directly pushed to the output channel but instead added to the inference manager. Additionally, we no longer use the cache within the nonlinear extension but instead rely on the inference manager. This PR is based on #4960.
2020-09-03Make nonlinear extension (more) deterministic (#4996)Gereon Kremer
This PR tries to make the nonlinear extension more deterministic by keeping the order of input assertion (instead of taking them from a hash set). This makes the ordering somewhat more robust against varying node ids, which proved to be a problem for debugging... Also adds a few logging messages at interesting places.
2020-09-02Make ExtTheory independent of Theory (#5010)Andrew Reynolds
This makes it so that ExtTheory uses a generic callback instead of relying on Theory. The primary purpose of this commit is to eliminate the connection of TheoryBV and ExtTheory. This commit moves all things related to ExtTheory in BV into CoreSolver. It also refactors the use of ExtTheory in strings and arithmetic.
2020-09-02Add ArithLemma and arith::InferenceManager (#4960)Gereon Kremer
This PR adds a new ArithLemma that is essentiall NlLemma, but derived from the new theory::Lemma and meant to be used all across the arithmetic theory. Also, based on theory::InferenceManagerBuffered this PR adds arith::InferenceManager that shall become the sole interface between the arithmetic theory and the OutputChannel.
2020-08-24Do not use relevance during non-linear check model (#4938)Andrew Reynolds
This led to a model soundness issue in rare cases where a relevant literal was dropped due to an entailment check by an irrelevant literal.
2020-08-21Connect the relevance manager to TheoryEngine and use it in non-linear ↵Andrew Reynolds
arithmetic (#4930) This PR activates the use of the relevance manager in TheoryEngine and makes use of it (via Valuation) in the non-linear extension in arith. It removes a deprecated hack (addTautology) for doing this. This addresses CVC4/cvc4-projects#113. Note that the best method for relevance is interleaving, where roughly you gain on SMT-LIB: QF_NIA: +484-53 unsat +792-440 sat QF_NRA: +32-19 unsat +57-23 sat However, this PR does not (yet) enable this method by default. Note that more work is necessary to determine which lemmas require NEEDS_JUSTIFY, this PR identifies 2 cases of lemmas that need justification (skolemization and strings reductions). Regardless, the use of the relevance manager is limited to non-linear arithmetic for now, which is only able to answer "sat" when only arithmetic is present in assertions.
2020-08-04Add CAD-based solver (#4834)Gereon Kremer
Based on #4774, this PR adds a new CadSolver class that allows the NonlinearExtension to actually employ the CAD-based method. In more detail: add --nl-cad option add CadSolver class that wraps cad::CDCAC with support for checks, model construction and conflict generation add new Inference types for the NlLemma class use CadSolver in NonlinearExtension (if --nl-cad is given)
2020-07-28Use lemma property enum for OutputChannel::lemma (#4755)Andrew Reynolds
There are 3 Boolean flags for OutputChannel::lemma, and plans to add another for relevance. This makes them into a enum.
2020-07-21Preparations for a CAD-based arithmetic solver (#4762)Gereon Kremer
Based on #4679, this PR contains further preparations for a CAD-based arithmetic solver that extends the current NonlinearExtension. In detail, it provides: a Constraints class that manages all (polynomial) constraints visible to the cad solver, a collection of methods used for cad projections, a VariableOrdering class that provides different variable ordering heuristics tailored to cad, an extension to the NlModel class, allowing for witness terms, further conversion methods, in particular between Node and poly::Polynomial, poly::Value and RealAlgebraicNumber.
2020-07-16Make ExtTheory a utility and not a member of Theory (#4753)Andrew Reynolds
Previously, we assumed that ExtTheory, the module for doing context-dependent simplification, was one-to-one with Theory. This design is not necessary. This makes this class a utility, which can be used as needed. This makes e.g. the initialization of TheoryStrings much easier, since the ExtTheory object can be created first.
2020-07-09Associate all lemmas in non-linear arithmetic with an inference identifier ↵Andrew Reynolds
(#4712) This marks all lemmas in non-linear arithmetic with an identifier, which indicates informally the kind of justification that was used for them. The main motivation for this is for debugging the behavior of the non-linear solver. The number of inferences can then be seen with --stats: nl::inferences, [(SPLIT_ZERO : 19), (SIGN : 4), (COMPARISON : 29)] The same design was used in strings and has been quite helpful. This also adds a few high level stats to the new statistics class for non-linear.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback