summaryrefslogtreecommitdiff
path: root/src/theory/arith
AgeCommit message (Expand)Author
2019-12-05Make nonlinear solver intercept model assignments from the linear arithmetic ...Andrew Reynolds
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++ AP...makaimann
2019-11-22Minor refactoring of compute model value for nl (#3489)Andrew Reynolds
2019-11-18Fix reduction of `sqrt` (#3478)Andres Noetzli
2019-11-18Use -Wimplicit-fallthrough (#3464)Andres Noetzli
2019-11-12Refactor non-linear extension for model-based refinement (#3452)Andrew Reynolds
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
2019-10-28Fix for non-linear models (#3410)Andrew Reynolds
2019-10-28Fix integer division rewrite (#3415)Andres Noetzli
2019-10-13Eliminate negative constant coefficients in div/mod (#2929)Andrew Reynolds
2019-10-08prefer prefix ++ operator for iteratorsPiotr Trojanek
2019-09-28Introduce template classes for simple type rules (#2835)Andres Noetzli
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
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
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
2018-12-14Fixed typos.Aina Niemetz
2018-12-06Arith Constraint Proof Loggin (#2732)Alex Ozdemir
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 assert...Andrew Reynolds
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
2018-07-26Changing the arithmetic static learner to use CDHashMap. This is 2/3 PRs for ...Tim King
2018-07-25Changing ArithIteUtils to use CDInsertHashMap. (#2206)Tim King
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback