Age | Commit message (Collapse) | Author | |
---|---|---|---|
2019-09-28 | Introduce 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-24 | fix mismatch between "delete" and "new []" (#2795) | Piotr Trojanek | |
2019-08-23 | Fix argument in nonlinear extension. (#3216) | Andrew Reynolds | |
2019-06-11 | NA Tangent reverse implication (#3050) | Ahmed Irfan | |
2019-04-24 | Do not use __ prefix for header guards. (#2974) | Mathias Preiner | |
Fixes 2887. | |||
2019-03-26 | Update copyright headers. | Aina Niemetz | |
2019-03-14 | Use 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-20 | Add 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-14 | Fixed typos. | Aina Niemetz | |
2018-12-06 | Arith 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-01 | Fix compiler warnings. (#2555) | Aina Niemetz | |
2018-09-27 | Fix Taylor overapproximation for large exponentials (#2538) | Andrew Reynolds | |
2018-09-24 | Improve non-linear check model error handling (#2497) | Andrew Reynolds | |
2018-09-22 | cmake: Remove unused CMakeLists.txt | Mathias Preiner | |
2018-09-22 | cmake: Added initial build infrastructure. | Aina Niemetz | |
2018-09-13 | Simplify storing of transcendental function applications that occur in ↵ | Andrew Reynolds | |
assertions (#2458) | |||
2018-09-13 | Decision strategy: incorporate CEGQI (#2460) | Andrew Reynolds | |
2018-09-05 | Use std::uniqe_ptr for d_eq_infer to make Coverity happy. (#2432) | Mathias Preiner | |
2018-08-30 | Use useBland option in FCSimplexDecisionProcedure (#2405) | Andres Noetzli | |
2018-08-23 | Refactor ITE simplification preprocessing pass. (#2360) | Aina Niemetz | |
2018-08-16 | Move node algorithms to separate file (#2311) | Andres Noetzli | |
2018-08-07 | Require 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-26 | Changing the arithmetic static learner to use CDHashMap. This is 2/3 PRs for ↵ | Tim King | |
deprecating CDTrailHashMap. (#2207) | |||
2018-07-25 | Changing 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-06 | Split ext theory to own file and document (#1809) | Andrew Reynolds | |
2018-06-25 | Updated copyright headers. | Aina Niemetz | |
2018-06-02 | Fix corner case of mixed int/real cegqi. (#2046) | Andrew Reynolds | |
2018-05-25 | Fix various nl assertions. (#1980) | Andrew Reynolds | |
2018-05-24 | Fix (#1975) | Andrew Reynolds | |
2018-05-24 | Fixes for non-linear check model (#1974) | Andrew Reynolds | |
2018-05-23 | Remove spurious assertion in nonlinear extension (#1972) | Andrew Reynolds | |
2018-05-23 | Generalize check-model in NonLinearExtension for quadratic equations (#1892) | Andrew Reynolds | |
2018-05-03 | Option to interleave tangent plane inferences (#1833) | Andrew Reynolds | |
2018-05-01 | Improve tangent planes for transcendental functions (#1832) | Andrew Reynolds | |
2018-04-29 | Make factoring inference more aggressive (#1825) | Andrew Reynolds | |
2018-04-29 | Refactor nonlinear check (#1814) | Andrew Reynolds | |
2018-04-29 | Improvements to simple transcendental function check model. (#1823) | Andrew Reynolds | |
2018-04-27 | Simplify tangent plane direction (#1824) | Andrew Reynolds | |
2018-04-25 | Remove nl solve subs option. (#1803) | Andrew Reynolds | |
2018-04-19 | Refactor 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-03 | Use choice when expanding definitions for inverse transcendental functions ↵ | Andrew Reynolds | |
(#1742) | |||
2018-03-30 | Do not use factoring inference for transcendental functions (#1707) | Andrew Reynolds | |
2018-03-20 | Internally remove redundant assertions and infer equalities in ↵ | Andrew Reynolds | |
NonLinearExtension (#1633) | |||
2018-03-05 | Enable -Wsuggest-override by default. (#1643) | Mathias Preiner | |
Adds missing override keywords. | |||
2018-02-27 | Option to not use partial function semantics for arithmetic div by zero (#1620) | Andrew Reynolds | |
2018-02-20 | Minor fixes and additions for transcendental functions (#1612) | Andrew Reynolds | |
Also adds parsing support for PI in smt2 with syntax "real.pi". |