summaryrefslogtreecommitdiff
path: root/src/theory/arith
AgeCommit message (Expand)Author
2020-12-01Refactor transcendental solver (#5539)Gereon Kremer
2020-11-30Remove includes for old API from internal code (#5536)Andrew Reynolds
2020-11-26Make CAD solver work for empty set of assertions (#5535)Gereon Kremer
2020-11-25Fix transcendental secant plane lemmas (#5525)Gereon Kremer
2020-11-24Refactor transcendental solver (#5514)Gereon Kremer
2020-11-20Fix #5493. (#5495)Aina Niemetz
2020-11-20Fix compiler warnings. (#5493)Aina Niemetz
2020-11-20Allow to pass ProofGenerator to arithmetic inference manager. (#5488)Gereon Kremer
2020-11-19Include stddef.h (needed for size_t) in cvc4_public.h (#5476)Aina Niemetz
2020-11-19Fix issues related to eliminating extended arithmetic operators (#5475)Andrew Reynolds
2020-11-18Do not expand definitions of extended arithmetic operators (#5433)Andrew Reynolds
2020-11-17Fix tangent plane lemmas (#5455)Gereon Kremer
2020-11-16Refactor tangent plane lemmas (#5449)Gereon Kremer
2020-11-16Improve accuracy of resource limitation (#4763)Gereon Kremer
2020-11-05Remove mkSingleton from the API (#5366)mudathirmahgoub
2020-11-03Reset built model flag at presolve in nonlinear (#5386)Andrew Reynolds
2020-10-30Use BoundInference in nonlinear extension (#5359)Gereon Kremer
2020-10-29Add mkInteger to the API (#5274)mudathirmahgoub
2020-10-28Fixes for unconstrained variables in nonlinear model (#5351)Andrew Reynolds
2020-10-28Split NlSolver in multiple subsolvers (#5315)Gereon Kremer
2020-10-28Add rewrites for div/mod in the arithmetic rewriter (#5352)Andrew Reynolds
2020-10-27Enable --nl-cad by default (#5345)Gereon Kremer
2020-10-21(proof-new) arith: dedup literals in flattenImpl (#5320)Alex Ozdemir
2020-10-20Handle rewrite to bool in BoundInference (#5311)Gereon Kremer
2020-10-15(proof-new) TheoryArithPrivate: farkas lemma proof (#5267)Alex Ozdemir
2020-10-14bv2int: implementing the iand-sum mode (#5265)yoni206
2020-10-14(proof-new) debug statements & docs for INT_TRUST (#5259)Alex Ozdemir
2020-10-14(proof-new) pfs in TheoryArith(Private) explainations (#5258)Alex Ozdemir
2020-10-14Guard uses of printing approximations for constants (#5247)Andrew Reynolds
2020-10-14(proof-new) pfs for conflicts in TheoryArithPrivate (#5257)Alex Ozdemir
2020-10-13(proof-new) Prove lemmas in Constraint (#5254)Alex Ozdemir
2020-10-13bv2int: improving bvand tables (#5235)yoni206
2020-10-11Add conversion of poly polynomial to cvc node. (#5218)Gereon Kremer
2020-10-09bv2int: bvand translation code move (#5227)yoni206
2020-10-09use right arith explanation fn to fix regressions (#5231)Alex Ozdemir
2020-10-09(proof-new) proofs for arith-constraint explanations (#5224)Alex Ozdemir
2020-10-07(proof-new) proofs in ee -> arith pipeline (#5215)Alex Ozdemir
2020-10-07Make sure conflicts are not rewritten (in arithmetic) (#5219)Gereon Kremer
2020-10-06(proof-new) proofs for ArithCongMan -> ee facts (#5207)Alex Ozdemir
2020-10-06(proof-new) Add interface for trusted substitution and update ppAssert (#5193)Andrew Reynolds
2020-10-06Add arithmetic preprocess module (#5188)Andrew Reynolds
2020-10-03Standardization of Theory (#5181)Andrew Reynolds
2020-10-02Decouple modules from TheoryArithPrivate (#5184)Andrew Reynolds
2020-10-02(proof-new) New proofs in arith::Constraint::externalExplain (#5176)Alex Ozdemir
2020-10-01Update theory of arithmetic to standard check (#5178)Andrew Reynolds
2020-10-01Allow to use the initial assignment for CAD (#5177)Gereon Kremer
2020-09-30Remove too strict assertion to allow for approximate models (#5168)Gereon Kremer
2020-09-30Add missing includes. (#5170)Gereon Kremer
2020-09-30Add strategy for nonlinear extension (#5160)Gereon Kremer
2020-09-29(proof-new) Add proof managers and eager gens to arith (#5159)Alex Ozdemir
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback