summaryrefslogtreecommitdiff
path: root/src/theory/arith/theory_arith.cpp
AgeCommit message (Expand)Author
2020-09-01Removes old proof code (#4964)Haniel Barbosa
2020-08-24Extend the standard Theory template based on equality engine (#4929)Andrew Reynolds
2020-08-20Add TheoryState objects to each Theory (#4920)Andrew Reynolds
2020-08-17Dynamic allocation of equality engine in Theory (#4890)Andrew Reynolds
2020-08-09Make valuation class more robust to null underlying TheoryEngine. (#4864)Andrew Reynolds
2020-07-27(proof-new) Arithmetic operator elim proof producing (#4783)Andrew Reynolds
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-06-29Add internal support for integer and operator (#4668)Andrew Reynolds
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-16Update copyright headers.Aina Niemetz
2020-05-19Do not eliminate variables that are equal to unevaluatable terms (#4267)Andrew Reynolds
2020-04-08Perform theory widening eagerly (#4044)Andres Noetzli
2020-04-03Update theory rewriter ownership, add stats to strings (#4202)Andres Noetzli
2020-04-01Initialize theory rewriters in theories (#4197)Andres Noetzli
2020-02-19resource manager: Add statistic for every resource. (#3772)Mathias Preiner
2019-03-26Update copyright headers.Aina Niemetz
2018-12-14 [LRA Proof] Storage for LRA proofs (#2747)Alex Ozdemir
2018-07-06Split ext theory to own file and document (#1809)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-02-07Add remaining transcendental functions (#1551)Andrew Reynolds
2017-12-08Make collect model info return a Bool (#1421)Andrew Reynolds
2017-07-10Merge ntExt branch. Adds support for transcendental functions. Refactoring of...ajreynol
2017-07-07Update copyright headers.Mathias Preiner
2017-04-07Change option names for nl.ajreynol
2017-04-04Simplify Theory::collectModelInfo interface to not take deprecated fullModel ...ajreynol
2017-04-02Adding a model based axiom instantiation scheme for multiplication. Merge com...Tim King
2016-04-20update from the masterPaulMeng
2016-01-28Adding listeners to Options.Tim King
2016-01-08Removing StatisticsRegistry's static functions current() and registerStat().Tim King
2016-01-05Add SmtGlobals ClassTim King
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-05-28added options for controlling resource step-count for various solving stagesLiana Hadarean
2014-07-01Update copyrights.Morgan Deters
2014-04-30T-entailment work, and QCF (quant conflict find) work that uses it.Tim King
2014-03-19Refactor the theory specific parts of definition expansion into the theory so...Martin Brain
2014-03-04Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (r...Morgan Deters
2014-01-22Delay QuantifiersEngine and UF strong solver initialization until after final...Morgan Deters
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-09-27adds model generation for strings, and a hacked way in arith engine for modelsTianyi Liang
2013-06-24Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk al...Morgan Deters
2013-04-26FCSimplex branch mergeTim King
2013-04-02Making arithmetic model reversion on unsat checks an option.Tim King
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-04-01Cleaning up the demand restart code.Tim King
2013-04-01Adding a restart test strategy to integers.Tim King
2013-01-31Adding a heuristic to more eagerly split bounded integer variables.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback