summaryrefslogtreecommitdiff
path: root/src/theory/arith
AgeCommit message (Collapse)Author
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
2018-08-23Refactor ITE simplification preprocessing pass. (#2360)Aina Niemetz
2018-08-16Move node algorithms to separate file (#2311)Andres Noetzli
2018-08-07Require Swig 3 (#2283)Andres Noetzli
Removes some hacks due to Swig 2's incomplete C++11 support and adds checks for version 3 at configuration time as well as in swig.h
2018-07-26Changing the arithmetic static learner to use CDHashMap. This is 2/3 PRs for ↵Tim King
deprecating CDTrailHashMap. (#2207)
2018-07-25Changing ArithIteUtils to use CDInsertHashMap. (#2206)Tim King
This is 1/3 PRs for deprecating CDTrailHashMap.
2018-07-17 Purify applications of exp to transcendental arguments (#2097)Andrew Reynolds
2018-07-06Split ext theory to own file and document (#1809)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-06-02Fix corner case of mixed int/real cegqi. (#2046)Andrew Reynolds
2018-05-25Fix various nl assertions. (#1980)Andrew Reynolds
2018-05-24Fix (#1975)Andrew Reynolds
2018-05-24Fixes for non-linear check model (#1974)Andrew Reynolds
2018-05-23Remove spurious assertion in nonlinear extension (#1972)Andrew Reynolds
2018-05-23Generalize check-model in NonLinearExtension for quadratic equations (#1892)Andrew Reynolds
2018-05-03Option to interleave tangent plane inferences (#1833)Andrew Reynolds
2018-05-01Improve tangent planes for transcendental functions (#1832)Andrew Reynolds
2018-04-29Make factoring inference more aggressive (#1825)Andrew Reynolds
2018-04-29Refactor nonlinear check (#1814)Andrew Reynolds
2018-04-29Improvements to simple transcendental function check model. (#1823)Andrew Reynolds
2018-04-27Simplify tangent plane direction (#1824)Andrew Reynolds
2018-04-25Remove nl solve subs option. (#1803)Andrew Reynolds
2018-04-19Refactor pbRewrites preprocessing pass (#1767)Andres Noetzli
This commit refactors the pbRewrites preprocessing pass into the new style. This commit is essentially just a code move and adds a regression test for the preprocessing pass. It also makes use of the AssertionPipeline::replace function to do proper dependency tracking.
2018-04-03Use choice when expanding definitions for inverse transcendental functions ↵Andrew Reynolds
(#1742)
2018-03-30Do not use factoring inference for transcendental functions (#1707)Andrew Reynolds
2018-03-20Internally remove redundant assertions and infer equalities in ↵Andrew Reynolds
NonLinearExtension (#1633)
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
Adds missing override keywords.
2018-02-27Option to not use partial function semantics for arithmetic div by zero (#1620)Andrew Reynolds
2018-02-20Minor fixes and additions for transcendental functions (#1612)Andrew Reynolds
Also adds parsing support for PI in smt2 with syntax "real.pi".
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback