summaryrefslogtreecommitdiff
path: root/src/theory/arith
AgeCommit message (Collapse)Author
2013-06-24Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk ↵Morgan Deters
allows linearization of div,mod,/ by a constant.
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 ↵Andrew Reynolds
quantification. Minor update to casc script.
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 ↵Tim King
caused arithmetic to think it was in a conflict incorrectly. This lead to it not properly responding to new input and lead to an inconsistency bug. This could be triggered previously by running: ./builds/bin/cvc4 --stats --no-restrict-pivots --enable-miplib-trick --miplib-trick-subs=2 --fc-penalties --collect-pivot-stats --new-prop --dio-decomps --unconstrained-simp --fancy-final /home/taking/benchmarks/smtlib2/QF_LRA/miplib/opt1217--17.smt2
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 ↵Tim King
removing an ugly forward declaration that was needed to get error set bound information on basic variables.
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 ↵Morgan Deters
and src
2013-02-16Some cleanup and copyright updatingMorgan Deters
* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles
2013-02-04Some fixes for the miplib preprocessing pass.Morgan Deters
* TNode violation bug fix (thanks to Tim King for discovery & fix) * change Boolean miplib-trick substitution option into a threshold * ppAssert() the generated miplib constraints to arithmetic
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 ↵Tim King
over from branches/arithmetic/converge except for the new code for simplex.
2012-12-05Cleanup of arithmetic, and some new utility functions for the coming ↵Tim King
fcsimplex code.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback