Age | Commit message (Collapse) | Author | |
---|---|---|---|
2013-05-16 | configure fix for building with glpk on redhat, perhaps others | Morgan Deters | |
2013-05-11 | Preliminary version of finite model finding over bounded integer ↵ | Andrew Reynolds | |
quantification. Minor update to casc script. | |||
2013-05-09 | Changing the integer normal form to increase matching. | Tim King | |
2013-05-08 | Removing arithmetic compile warning for release | Morgan Deters | |
2013-05-07 | Fixes 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-07 | Improving arithmetic debugging output. | Tim King | |
2013-05-07 | Disabling an incorrect prototyping line from the simplex merges. Fixes bug 510. | Tim King | |
2013-05-06 | Removing excess verbosity from ApproxSimplex (after discussing with Tim) | Morgan Deters | |
2013-05-06 | Adding a heuristic for guessing an optimization function when using glpk. | Tim King | |
2013-05-05 | Adding cut offs for likely integer infeasible paths. | Tim King | |
2013-05-03 | Adding a smarter technique for pivoting in solutions for glpk. | Tim King | |
2013-05-03 | More 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-03 | Code cleanup. Reducing misc. warnings in arithmetic. | Tim King | |
2013-05-03 | Removing arithmetic legacy code and unifying functions. | Tim King | |
2013-05-03 | Fixing a debug typo. | Tim King | |
2013-05-03 | Merging branch 'soiquickexplain'. | Tim King | |
2013-05-03 | Merge branch 'fcexplanations' | Tim King | |
2013-05-02 | Adding quick explain for soi simplex. | Tim King | |
2013-05-01 | Working on the new explanation system. | Tim King | |
2013-04-30 | Making propagation more conversative. | Tim King | |
2013-04-30 | Draft of the new propagation code. | Tim King | |
2013-04-30 | Adding has bound counts and tracking for rows. | Tim King | |
2013-04-29 | Some fixes for GCC 4.2, and for Java on Mac | Morgan Deters | |
2013-04-29 | Fixes to FCSimplex for some versions of compilers | Morgan Deters | |
2013-04-28 | Fixing the failure for make distcheck. | Tim King | |
2013-04-26 | FCSimplex branch merge | Tim King | |
2013-04-02 | Making arithmetic model reversion on unsat checks an option. | Tim King | |
2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters | |
2013-04-01 | update copyrights | Morgan Deters | |
2013-04-01 | Cleaning up the demand restart code. | Tim King | |
2013-04-01 | Adding a restart test strategy to integers. | Tim King | |
2013-03-21 | Better error in case of nonlinear assertions while in linear logic | Morgan Deters | |
2013-03-14 | Merge branch '1.0.x' | Morgan Deters | |
2013-03-14 | fix to build system: #include the proper file when they are in both builds ↵ | Morgan Deters | |
and src | |||
2013-02-16 | Some cleanup and copyright updating | Morgan Deters | |
* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles | |||
2013-02-04 | Some 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-03 | Some cleanup of miplib regressions and options | Morgan Deters | |
2013-02-03 | new option for doing top-level miplib substitutions (or not) | Morgan Deters | |
2013-02-03 | new miplib pass, works for 1 or 2 vars | Morgan Deters | |
2013-02-03 | Remove old miplibtrick from arith static learner | Morgan Deters | |
2013-01-31 | Adding a heuristic to more eagerly split bounded integer variables. | Tim King | |
2013-01-25 | Fix errors and reduce warnings on clang (merge from mdeters/clang) | Morgan Deters | |
2013-01-23 | Adding miplibtrick option. | Tim King | |
2013-01-23 | Adding substitution size cap. | Tim King | |
2012-12-14 | Merging in patch from branch '1.0.x'. | Tim King | |
2012-12-14 | Changing the rewriter to use Boute's Euclidean definition of division. | Tim King | |
2012-12-05 | Improved 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-05 | Cleanup of arithmetic, and some new utility functions for the coming ↵ | Tim King | |
fcsimplex code. | |||
2012-12-05 | This commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses ↵ | Tim King | |
CDInsertHashMap. CDHashSet<TNode> have been changed to CDHashSet<Node>. Switching CnfStream to use CDInsertSet. Switches a few CDHashMaps in arithmetic to use CDTrailHashMap. Documentation changes to CDHashMap. | |||
2012-12-01 | drastic simplification of quantifiers code regarding equality queries, ↵ | Andrew Reynolds | |
instantiation strategies moved from instantiators to central instantiation engine, removed instantiator objects, simplified rewrite rules candidate generator to use central equality engine, efficient e-matching now uses central equality engine |