summaryrefslogtreecommitdiff
path: root/src/theory/arith/theory_arith.cpp
AgeCommit message (Expand)Author
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
2013-01-23Adding substitution size cap.Tim King
2012-12-14Merging in patch from branch '1.0.x'.Tim King
2012-12-14Changing the rewriter to use Boute's Euclidean definition of division.Tim King
2012-12-05Improved garbage collection for TheoryArith. The merges all of the code over...Tim King
2012-12-05This commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses ...Tim King
2012-11-26Adding support for a master equality engine. Each theory gets the master equa...Dejan Jovanović
2012-11-26Improving arithmetic debugging output.Tim King
2012-11-25This commit fixes two incompleteness bugs (461, 459) introduced in r4611 dues...Tim King
2012-11-21- Removes getDeltaValueWithNonlinear() entirelyTim King
2012-11-19Fix for bug452.Tim King
2012-11-14replaced all static member data from rewrite rule triggers, added infrastruct...Andrew Reynolds
2012-11-14Fixed a typo in r4576Tim King
2012-11-14Fix to bug449. Adds shared constants to the set of DeltaRationals that must b...Tim King
2012-11-12Improved error reporting for improperly using non-linear division in linear a...Tim King
2012-11-12Delta is now generated in arithmetic to keep consistent the total order of De...Tim King
2012-11-10Fix for bug 439. Delta computation now includes disequality information.Tim King
2012-11-08Turns on TheoryUF when non-linear arithmetic is turned on. Adds test cases fo...Tim King
2012-11-08Improved support for division by zero. This adds the *_TOTAL kinds and unint...Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback