summaryrefslogtreecommitdiff
path: root/src/theory/arith
AgeCommit message (Expand)Author
2020-09-01Removes old proof code (#4964)Haniel Barbosa
2020-09-01Add arithmetic-specific, runtime, proof-macros. (#4992)Alex Ozdemir
2020-08-31Fix spelling errors (#4977)FabianWolff
2020-08-31Simplify interface for computing relevant terms. (#4966)Andrew Reynolds
2020-08-28Replace Theory::Set with TheoryIdSet (#4959)Andrew Reynolds
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-24Extend the standard Theory template based on equality engine (#4929)Andrew Reynolds
2020-08-21Connect the relevance manager to TheoryEngine and use it in non-linear arithm...Andrew Reynolds
2020-08-20Add TheoryState objects to each Theory (#4920)Andrew Reynolds
2020-08-19Simplify trigger notifications in equality engine (#4921)Andrew Reynolds
2020-08-19(cad solver) Add a partial check method. (#4904)Gereon Kremer
2020-08-17Dynamic allocation of equality engine in Theory (#4890)Andrew Reynolds
2020-08-15(cad solver) Use the current model as initial assignment (#4893)Gereon Kremer
2020-08-14Simplify equality engine notifications (#4896)Andrew Reynolds
2020-08-14Inspect roots to avoid certain resultants (Algorithm 4, lines 8,9). (#4892)Gereon Kremer
2020-08-12Add naive support for integer variables. (#4835)Gereon Kremer
2020-08-12Fix infinite loop in arith_ite_simp (#4805)Gereon Kremer
2020-08-09Make valuation class more robust to null underlying TheoryEngine. (#4864)Andrew Reynolds
2020-08-05Improve error message for unsupported exponents (#4852)Gereon Kremer
2020-08-04Add dummy returns if libpoly is unavailable. (#4845)Gereon Kremer
2020-08-04Add CAD-based solver (#4834)Gereon Kremer
2020-07-30Cad implementation (#4774)Gereon Kremer
2020-07-30Adds the interface for the CAD-based arithmetic solver. (#4773)Gereon Kremer
2020-07-28Use lemma property enum for OutputChannel::lemma (#4755)Andrew Reynolds
2020-07-27(proof-new) Arithmetic operator elim proof producing (#4783)Andrew Reynolds
2020-07-27Consider negation's proof before triggering arith pfs. (#4776)Alex Ozdemir
2020-07-21Preparations for a CAD-based arithmetic solver (#4762)Gereon Kremer
2020-07-16Make ExtTheory a utility and not a member of Theory (#4753)Andrew Reynolds
2020-07-15Simplify entailment check interface (#4744)Andrew Reynolds
2020-07-10(proof-new) Update Theory interface for proof-new (#4648)Andrew Reynolds
2020-07-09Associate all lemmas in non-linear arithmetic with an inference identifier (#...Andrew Reynolds
2020-07-07Improve and fix secant and tangent lemmas in the transcendental solver (#4689)Andrew Reynolds
2020-07-01Add solver for integer AND (#4681)Andrew Reynolds
2020-06-29Add internal support for integer and operator (#4668)Andrew Reynolds
2020-06-28Proof Rules and Checker for Arithmetic (#4665)Alex Ozdemir
2020-06-25Update option --nl-ext to enable/disable incremental linearization solver onl...Andrew Reynolds
2020-06-22Add trascendental function kinds to list of unevaluated operators (#4640)Andrew Reynolds
2020-06-19(proof-new) Split operator elimination from arithmetic (#4581)Andrew Reynolds
2020-06-16Update copyright headers.Aina Niemetz
2020-06-10(proof-new) Remove arith-snorm option. (#4591)Andrew Reynolds
2020-06-08Fix Coverity issues (#4587)Andres Noetzli
2020-06-06Use NlLemma utility for all lemmas in non-linear. (#4573)Andrew Reynolds
2020-06-05(proof-new) Rename ProofSkolemCache to SkolemManager (#4556)Andrew Reynolds
2020-06-01Move non-linear files to src/theory/arith/nl (#4548)Andrew Reynolds
2020-05-31Do not cache operator eliminations in arith (#4542)Andres Noetzli
2020-05-22Refactor operator elimination in arithmetic (#4519)Andrew Reynolds
2020-05-19Do not eliminate variables that are equal to unevaluatable terms (#4267)Andrew Reynolds
2020-05-19Renamed operator CHOICE to WITNESS (#4207)mudathirmahgoub
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback