summaryrefslogtreecommitdiff
path: root/src/theory/arith/nl
AgeCommit message (Expand)Author
2020-12-01Merge branch 'master' into fixClangWarningsfixClangWarningsAndres Noetzli
2020-12-01Refactor transcendental solver (#5539)Gereon Kremer
2020-11-29Merge remote-tracking branch 'origin/master' into fixClangWarningsAndres Noetzli
2020-11-29updateAndres Noetzli
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-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-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-28Fixes for unconstrained variables in nonlinear model (#5351)Andrew Reynolds
2020-10-28Split NlSolver in multiple subsolvers (#5315)Gereon Kremer
2020-10-27Enable --nl-cad by default (#5345)Gereon Kremer
2020-10-20Handle rewrite to bool in BoundInference (#5311)Gereon Kremer
2020-10-14bv2int: implementing the iand-sum mode (#5265)yoni206
2020-10-14Guard uses of printing approximations for constants (#5247)Andrew Reynolds
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-07Make sure conflicts are not rewritten (in arithmetic) (#5219)Gereon Kremer
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-30Add missing includes. (#5170)Gereon Kremer
2020-09-30Add strategy for nonlinear extension (#5160)Gereon Kremer
2020-09-29Clean up nonlinear extension (#5149)Gereon Kremer
2020-09-28Add new arithmetic BoundInference class (#5148)Gereon Kremer
2020-09-26Use inference manager for nl_solver (#5125)Gereon Kremer
2020-09-23Make IAND solver use inference manager. (#5126)Gereon Kremer
2020-09-22Fix compilation without LibPoly (#5118)Andres Noetzli
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-09-22ICP-based solver for nonlinear arithmetic (#5017)Gereon Kremer
2020-09-17(cad-solver) Fix square-free-basis computation (#5085)Gereon Kremer
2020-09-17Use new inference manager in transcendental solver (#5022)Gereon Kremer
2020-09-04Add asLemma flag to theory inference process (#5030)Andrew Reynolds
2020-09-04Fix non-lib-poly-build issues (#5028)Haniel Barbosa
2020-09-04Use arith::InferenceManager for CAD lemmas (#5015)Gereon Kremer
2020-09-03Basic integration of arith::InferenceManager (#4999)Gereon Kremer
2020-09-03Make nonlinear extension (more) deterministic (#4996)Gereon Kremer
2020-09-02Make ExtTheory independent of Theory (#5010)Andrew Reynolds
2020-09-02Add ArithLemma and arith::InferenceManager (#4960)Gereon Kremer
2020-09-01Removes old proof code (#4964)Haniel Barbosa
2020-08-28(cad-solver) Fixed excluding lemma generation. (#4958)Gereon Kremer
2020-08-27Make iand lemmas use proper Inference types. (#4956)Gereon Kremer
2020-08-24Do not use relevance during non-linear check model (#4938)Andrew Reynolds
2020-08-21Connect the relevance manager to TheoryEngine and use it in non-linear arithm...Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback