summaryrefslogtreecommitdiff
path: root/src/theory/arith
AgeCommit message (Expand)Author
2013-06-24Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk al...Morgan Deters
2013-05-22Add regressions for finite model findingAndrew Reynolds
2013-05-16configure fix for building with glpk on redhat, perhaps othersMorgan Deters
2013-05-11Preliminary version of finite model finding over bounded integer quantificati...Andrew Reynolds
2013-05-09Changing the integer normal form to increase matching.Tim King
2013-05-08Removing arithmetic compile warning for releaseMorgan Deters
2013-05-07Fixes a bug with arithmetic's new attempt solution infrastructure. This caus...Tim King
2013-05-07Improving arithmetic debugging output.Tim King
2013-05-07Disabling an incorrect prototyping line from the simplex merges. Fixes bug 510.Tim King
2013-05-06Removing excess verbosity from ApproxSimplex (after discussing with Tim)Morgan Deters
2013-05-06Adding a heuristic for guessing an optimization function when using glpk.Tim King
2013-05-05Adding cut offs for likely integer infeasible paths.Tim King
2013-05-03Adding a smarter technique for pivoting in solutions for glpk.Tim King
2013-05-03More misc. arithmetic cleanup. Removing unused files and functions. Also remo...Tim King
2013-05-03Code cleanup. Reducing misc. warnings in arithmetic.Tim King
2013-05-03Removing arithmetic legacy code and unifying functions.Tim King
2013-05-03Fixing a debug typo.Tim King
2013-05-03Merging branch 'soiquickexplain'.Tim King
2013-05-03Merge branch 'fcexplanations'Tim King
2013-05-02Adding quick explain for soi simplex.Tim King
2013-05-01Working on the new explanation system.Tim King
2013-04-30Making propagation more conversative.Tim King
2013-04-30Draft of the new propagation code.Tim King
2013-04-30Adding has bound counts and tracking for rows.Tim King
2013-04-29Some fixes for GCC 4.2, and for Java on MacMorgan Deters
2013-04-29Fixes to FCSimplex for some versions of compilersMorgan Deters
2013-04-28Fixing the failure for make distcheck.Tim King
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-03-21Better error in case of nonlinear assertions while in linear logicMorgan Deters
2013-03-14Merge branch '1.0.x'Morgan Deters
2013-03-14fix to build system: #include the proper file when they are in both builds an...Morgan Deters
2013-02-16Some cleanup and copyright updatingMorgan Deters
2013-02-04Some fixes for the miplib preprocessing pass.Morgan Deters
2013-02-03Some cleanup of miplib regressions and optionsMorgan Deters
2013-02-03new option for doing top-level miplib substitutions (or not)Morgan Deters
2013-02-03new miplib pass, works for 1 or 2 varsMorgan Deters
2013-02-03Remove old miplibtrick from arith static learnerMorgan Deters
2013-01-31Adding a heuristic to more eagerly split bounded integer variables.Tim King
2013-01-25Fix errors and reduce warnings on clang (merge from mdeters/clang)Morgan Deters
2013-01-23Adding miplibtrick option.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-05Cleanup of arithmetic, and some new utility functions for the coming fcsimple...Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback