summaryrefslogtreecommitdiff
path: root/src/theory/arith/theory_arith_private.cpp
AgeCommit message (Expand)Author
2019-01-03[LRA proof] Recording & Printing LRA Proofs (#2758)Alex Ozdemir
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-06Split ext theory to own file and document (#1809)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-04-03Use choice when expanding definitions for inverse transcendental functions (#...Andrew Reynolds
2018-02-27Option to not use partial function semantics for arithmetic div by zero (#1620)Andrew Reynolds
2018-02-20Minor fixes and additions for transcendental functions (#1612)Andrew Reynolds
2018-02-14Quantifiers subdirectories (#1608)Andrew Reynolds
2018-02-07Add remaining transcendental functions (#1551)Andrew Reynolds
2018-01-23Commenting out throw specifiers for DeltaRationExceptions. These functions ca...Tim King
2018-01-09Cleaning up throw specifiers on Exception and subclasses. (#1475)Tim King
2018-01-07Removes RationalFromDoubleException. Replaces this with an explicit M… (#1476)Tim King
2018-01-03Global negate (#1466)Andrew Reynolds
2017-12-08Make collect model info return a Bool (#1421)Andrew Reynolds
2017-11-17Add random number generator. (#1370)Aina Niemetz
2017-08-30Use thread_local instead of compiler extensions (#210)Andres Noetzli
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
2017-07-10Merge ntExt branch. Adds support for transcendental functions. Refactoring of...ajreynol
2017-07-07Update copyright headers.Mathias Preiner
2017-05-31Minor fix to last commit.ajreynol
2017-05-31Change to-int, div, int-div skolems from CDAttribute to stored in CDHashMap. ...ajreynol
2017-05-26Checking that equalities belong to the arithmetic theory in the solve() routine.Tim King
2017-05-15Cleanup handling of division (possible fix for bugs 803, 804, 805).ajreynol
2017-04-28Fix bug for real division.ajreynol
2017-04-22Updating TheoryArithPrivate::getDeltaValue() to eagerly use the partial model...Tim King
2017-04-07Change option names for nl.ajreynol
2017-04-05Fix bug 698.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-09-25Fixing a potential use after free coming from a pop_back() call invalidating ...Tim King
2016-04-03Updating the copyright headers and scripts.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-11-03Fixing typo.Tim King
2015-06-14Handing the case in replay where a cut is directly in conflict with an existi...Tim King
2015-06-14Fixes for shared term normalization in replay for constraint construction.Tim King
2015-06-13Restricting TheoryArith to computeRelevantTerms.Tim King
2015-06-12In TheoryArithPrivate::vectorToIntHoleConflict, adding check for whether or n...Tim King
2015-04-18Farkas proof coefficients.Tim King
2014-11-17Short-circuit in TheoryArithPrivate::check(), care of Tim.Morgan Deters
2014-11-17New, uniform checkTime statistic for all theories (as discussed in meeting).Morgan Deters
2014-08-24improvements to sets sharingKshitij Bansal
2014-07-01Update copyrights.Morgan Deters
2014-06-25Fixing the previous bugfix.Tim King
2014-06-24Fixing a soundness bug in arithmetic and a roubustness problem in rings.Tim King
2014-06-19disable unate lemmas when using incremental modeKshitij Bansal
2014-05-12Merging in additional glpk options and statistics from CAV submission.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback