summaryrefslogtreecommitdiff
path: root/src/theory/arith/normal_form.cpp
AgeCommit message (Expand)Author
2018-02-07Add remaining transcendental functions (#1551)Andrew Reynolds
2017-07-17Use is_sorted, merge, copy from std (#199)Andres Noetzli
2017-07-10Merge ntExt branch. Adds support for transcendental functions. Refactoring of...ajreynol
2017-07-07Update copyright headers.Mathias Preiner
2017-05-26Checking that equalities belong to the arithmetic theory in the solve() routine.Tim King
2017-04-02Adding a model based axiom instantiation scheme for multiplication. Merge com...Tim King
2016-12-09Fixing a use after free bug in Polynomial::denominatorLCM.Tim King
2016-04-20update from the masterPaulMeng
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-04-18Farkas proof coefficients.Tim King
2014-07-01Update copyrights.Morgan Deters
2014-06-19Fix for pre-C++11 is_sorted().Morgan Deters
2014-06-19Final preparations for arithmetic for building with libc++.Morgan Deters
2014-06-06Patch for the subtype theoryof mode to make the equalities over disequal type...Tim King
2014-03-26Merging in a fix from 1.3.x.Tim King
2014-03-07Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into m...Tim King
2014-02-19Stopping non-linear terms from entering the dio solver. Fixes bug 547.Tim King
2013-09-13Documentation fixes, some code typo fixes, file perms, other minor things.Morgan Deters
2013-05-09Changing the integer normal form to increase matching.Tim King
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-03-21Better error in case of nonlinear assertions while in linear logicMorgan Deters
2012-11-12Improved error reporting for improperly using non-linear division in linear a...Tim King
2012-11-11Fixes for the arithmetic normal form and rewriter to handle arbitrary constan...Tim King
2012-11-08Improved support for division by zero. This adds the *_TOTAL kinds and unint...Tim King
2012-11-07Fix to a bug in integer mod lemmas.Tim King
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-09-29This commit add interpretation by lemma for INTS_DIVISION, INTS_MODULUS, and ...Tim King
2012-06-12Fix to yesterday's change in arithmetic.Tim King
2012-06-11Fix to term normalization of integer equalities. Adds a regression test that ...Tim King
2012-05-18This commit removes the dead psuedoboolean code.Tim King
2012-04-17Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Belo...Tim King
2012-03-28Update to the ArithRewriter to remove REWRITE_AGAIN_FULL and limit REWRITE_AG...Tim King
2012-02-15This commit merges into trunk the branch branches/arithmetic/integers2 from r...Tim King
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
2011-09-02Partial merge of integers work; this is simple B&B and some pseudobooleanMorgan Deters
2011-02-133 heuristics were added to arithmetic. A heuristic for detecting an encoding ...Tim King
2011-01-05Commit for the theory engine and rewriter changes. Changes are substantial an...Dejan Jovanović
2010-10-31enable dependence graphs in doxygen; fix lots of doxygen warnings, fix some d...Morgan Deters
2010-10-13Removed vector<Monomial> monos from Polynomial. Now using expr::NodeSelfIter...Tim King
2010-10-12IDENTITY has been removed.Tim King
2010-10-03file header documentation regenerated with contributors names; no code modifi...Morgan Deters
2010-10-02branches/arith-indexed-variables merged into the main trunk.Tim King
2010-09-21part of review (bug #197): coding conventions, file-level documentation, re-r...Morgan Deters
2010-09-16Bug fix to CVC4::theory::arith::VarList as well as some superficial changes. ...Tim King
2010-09-13* New normal form for arithmetic is in place.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback