summaryrefslogtreecommitdiff
path: root/src/theory/arith
AgeCommit message (Collapse)Author
2020-02-19resource manager: Add statistic for every resource. (#3772)Mathias Preiner
This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`). Fixes #3751.
2020-02-18Fix approximate bounds for transcendental functions whose model values ↵Andrew Reynolds
rewrite (#3747) * Fix bounds for negative sine apps * Format * Comment Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
2020-02-17 Fix soundness bug in reduction of integer div/mod (#3766)Andrew Reynolds
This was introduced 7 years ago in https://github.com/CVC4/CVC4/commit/9098391fe334d829ec4101f190b8f1fa21c30752. This impacted any case of integer div/mod of the form `(mod c t)` or `(div c t)` where c is a constant and `t` is not. Fixes #3765. Also improves `--dump=t-lemmas` trace to result in smt-lib compatible output, which was required for debugging this.
2020-02-11Fix non-linear equality solving that involves mixed real/integer arithmetic ↵Andrew Reynolds
(#3739) * Fix non-linear equality solving that involves mixed real/integer. * Format * Fix * Revert Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
2020-02-06Fix exact sqrt (#3721)Andrew Reynolds
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
2020-02-04Articulate proof-related debug statements in arith (#3700)Alex Ozdemir
2020-02-03Split on model values when repaired model from non-linear is inconsisent (#3668)Andrew Reynolds
2020-01-31Fix arithmetic rewriter for exponential (#3688)Andres Noetzli
2020-01-22Fix substitution in nl solver (#3638)Andrew Reynolds
* Fix for 3614 * Add regression * Remove regression Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
2019-12-18Increment Taylor degree for tangent and secant plane inferences for ↵Andrew Reynolds
transcendentals (#3577)
2019-12-17Generate code for options with modes. (#3561)Mathias Preiner
This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.
2019-12-11Do not substitute beneath arithmetic terms in the non-linear solver (#3324)Andrew Reynolds
2019-12-09Make theory rewriters non-static (#3547)Andres Noetzli
This commit changes theory rewriters to be non-static. This refactoring is needed as a stepping stone to making our rewriter configurable: If we have multiple solver objects with different rewrite configurations, we cannot use `static` variables for the rewriter table in the BV rewriter for example. It is also in line with our goal of getting rid of singletons in general. Note that the `Rewriter` class is still a singleton, which will be changed in a future commit.
2019-12-05Make nonlinear solver intercept model assignments from the linear arithmetic ↵Andrew Reynolds
solver (#3525)
2019-12-03Improve flexibility of lemma output in non-linear solver (#3518)Andrew Reynolds
2019-12-02OpTerm Refactor: Allow retrieving OpTerm used to create Term in public C++ ↵makaimann
API (#3355) * Treat uninterpreted functions as a child in Term iteration * Remove unnecessary const_iterator constructor * Add parameter comments to const_iterator constructor * Use operator[] instead of storing a vector of Expr children * Switch pos member variable from int to uint32_t * Add comment about how UFs are treated in iteration * Allow OpTerm to contain a single Kind, update OpTerm construction * Update mkTerm to use only an OpTerm (and not also a Kind) * Remove unnecessary function checkMkOpTerm * Update mkOpTerm comments to not use _OP Kinds * Update examples to use new mkTerm * First pass on fixing unit test * Override kind for Constructor and Selector Terms * More fixes to unit tests * Updates to parser * Remove old assert (for Kind, OpTerm pattern which was removed) * Remove *_OP kinds from public API * Add hasOpTerm and getOpTerm methods to Term * Add test for UF iteration * Add unit test for getOpTerm * Move OpTerm implementation above Term implemenation to match header file Moved in header because Term::getOpTerm() returns an OpTerm and the compiler complains if OpTerm is not defined earlier. Simply moving the declaration is easier/cleaner than forward declaring within the same file that it's declared. * Fix mkTerm in datatypes-new.cpp example * Use helper function for creating term from Kind to avoid nested API calls * Rename: OpTerm->Op in API * Update OpTerm->Op in examples/tests/parser * Add case for APPLY_TESTER * operator term -> operator * Update src/api/cvc4cpp.h Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com> * Comment comment suggestion Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com> * Add not-null checks and implement Op from a single Kind constructor * Undo sed mistake for OpTerm replacement * Add 'd_' prefix to member vars * Fix comment and remove old commented-out code * Formatting * Revert "Formatting" This reverts commit d1d5fc1fb71496daeba668e97cad84c213200ba9. * More fixes for sed mistakes * Minor formatting * Undo changes in CVC parser * Add isIndexed and prefix with d_ * Create helper function for isIndexed to avoid calling API functions in other API functions
2019-11-22Minor refactoring of compute model value for nl (#3489)Andrew Reynolds
* Refactor compute model value for nl * Format
2019-11-18Fix reduction of `sqrt` (#3478)Andres Noetzli
2019-11-18Use -Wimplicit-fallthrough (#3464)Andres Noetzli
This commit enables compiler warnings for implicit fallthroughs in switch statements that are not explicitly marked as such. The commit introduces a new macro `CVC4_FALLTHROUGH` that can be used to indicate that a fallthrough is intentional. The commit fixes existing warnings and a bug in the arithmetic rewriter for `abs` (the bug likely couldn't be triggered easily because we rewrite `abs` to an `ite` while expanding definitions). To have the new macro also available in the parser, the commit changes `src/base/check.h` to be visible to the parser (it includes `cvc4_private_library.h` now instead of `cvc4_private.h`).
2019-11-12Refactor non-linear extension for model-based refinement (#3452)Andrew Reynolds
* Refactor non-linear extension for model-based refinement * Format * Minor * Address
2019-11-05Separate model object in non-linear extension (#3426)Andrew Reynolds
2019-10-31Fix Unimplemented() macros missed in #3366. (#3424)Mathias Preiner
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-10-29Split some generic utilities from the non-linear extension (#3419)Andrew Reynolds
* Split arith util * Cleaner * cpp * Format * Minor
2019-10-28Fix for non-linear models (#3410)Andrew Reynolds
* Towards fix for non-linear models * Format * Fix * More * Improve * Format * More
2019-10-28Fix integer division rewrite (#3415)Andres Noetzli
2019-10-13Eliminate negative constant coefficients in div/mod (#2929)Andrew Reynolds
Fixes #1399.
2019-10-08prefer prefix ++ operator for iteratorsPiotr Trojanek
Detected with cppcheck static analyser, which said: (performance) Prefer prefix ++/-- operators for non-primitive types. Reformat with clang-format as needed. Signed-off-by: Piotr Trojanek <piotr.trojanek@gmail.com>
2019-09-28Introduce template classes for simple type rules (#2835)Andres Noetzli
This commit introduces two template classes `SimpleTypeRule` and `SimpleTypeRuleVar` to help define simple type rules without writing lots of redundant code. The main advantages of this approach are: - Less code - More consistent error reporting - Easier to extend type checking with other functionality (e.g. getting the type of a symbol)
2019-09-04 Fixes related to destructing null (#3231)Andrew Reynolds
2019-08-24fix mismatch between "delete" and "new []" (#2795)Piotr Trojanek
2019-08-23Fix argument in nonlinear extension. (#3216)Andrew Reynolds
2019-06-11NA Tangent reverse implication (#3050)Ahmed Irfan
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
Fixes 2887.
2019-03-26Update copyright headers.Aina Niemetz
2019-03-14Use zero slope tangent planes for transcendental functions (#2803)Andrew Reynolds
2019-01-03[LRA proof] Recording & Printing LRA Proofs (#2758)Alex Ozdemir
* [LRA proof] Recording & Printing LRA Proofs Now we use the ArithProofRecorder to record and later print arithmetic proofs. If an LRA lemma can be proven by a single farkas proof, then that is done. Otherwise, we `trust` the lemma. I haven't **really** enabled LRA proofs yet, so `--check-proofs` still is a no-op for LRA. To test, do ``` lfsccvc4 <(./bin/cvc4 --dump-proofs ../test/regress/regress0/lemmas/mode_cntrl.induction.smt | tail -n +2) ``` where `lfsccvc4` is an alias invoking `lfscc` with all the necessary signatures. On my machine that is: ``` alias lfsccvc4="/home/aozdemir/repos/LFSC/build/src/lfscc \ /home/aozdemir/repos/CVC4/proofs/signatures/sat.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/smt.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/lrat.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_base.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_bv.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_bv_bitblast.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_arrays.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_int.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_quant.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_real.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_real.plf" ``` * Added guards to proof recording Also reverted some small, unintentional changes. Also had to add printing for STRING_SUBSTR?? * Responding to Yoni's review * SimpleFarkasProof examples * Respond to Aina's comments * Reorder Constraint declarations * fix build * Moved friend declaration in Constraint * Trichotomy example * Lift getNumChildren invocation in PLUS case Credits to aina for spotting it. * Clang-format
2018-12-20Add missing type rules for parameterized operator kinds. (#2766)Aina Niemetz
2018-12-14 [LRA Proof] Storage for LRA proofs (#2747)Alex Ozdemir
* [LRA Proof] Storage for LRA proofs During LRA solving the `ConstraintDatabase` contains the reasoning behind different constraints. Combinations of constraints are periodically used to justify lemmas (conflict clauses, propegations, ... ?). `ConstraintDatabase` is SAT context-dependent. ArithProofRecorder will be used to store concise representations of the proof for each lemma raised by the (LR)A theory. The (LR)A theory will write to it, and the ArithProof class will read from it to produce LFSC proofs. Right now, it's pretty simplistic -- it allows for only Farkas proofs. In future PRs I'll: 1. add logic that stores proofs therein 2. add logic that retrieves and prints proofs 3. enable LRA proof production, checking, and testing * Document ArithProofRecorder use-sites * Update src/proof/arith_proof_recorder.cpp Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu> * Yoni's review * clang-format * Response to Mathias' review.
2018-12-14Fixed typos.Aina Niemetz
2018-12-06Arith Constraint Proof Loggin (#2732)Alex Ozdemir
* Arith Constraint Proof Logging Also a tiny documentation update. * Debug.isOn check around iterated output * reference iteratees
2018-10-01Fix compiler warnings. (#2555)Aina Niemetz
2018-09-27Fix Taylor overapproximation for large exponentials (#2538)Andrew Reynolds
2018-09-24 Improve non-linear check model error handling (#2497)Andrew Reynolds
2018-09-22cmake: Remove unused CMakeLists.txtMathias Preiner
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-09-13Simplify storing of transcendental function applications that occur in ↵Andrew Reynolds
assertions (#2458)
2018-09-13 Decision strategy: incorporate CEGQI (#2460)Andrew Reynolds
2018-09-05Use std::uniqe_ptr for d_eq_infer to make Coverity happy. (#2432)Mathias Preiner
2018-08-30Use useBland option in FCSimplexDecisionProcedure (#2405)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback