| A rudimentary version of MathSAT optimization |
|
More...
|
almost 12 years ago
|
| merged with unstable |
|
More...
|
almost 12 years ago
|
| cleanup macro usage |
|
More...
|
almost 12 years ago
|
| add opt_solver layer |
|
More...
|
almost 12 years ago
|
| added floating point standard draft version 3 function symbols |
|
More...
|
almost 12 years ago
|
| Create placeholders to optimization methods |
|
More...
|
almost 12 years ago
|
| Complete Fu & Malik MAXSAT implementation |
|
More...
|
almost 12 years ago
|
| fill in details on max sat |
|
More...
|
almost 12 years ago
|
| Fu&Malik v1 |
|
More...
|
almost 12 years ago
|
| Create callbacks for min_maximize_cmd |
|
More...
|
almost 12 years ago
|
| fixing bugs with validation code |
|
More...
|
almost 12 years ago
|
| Merge branch 'opt' of https://git01.codeplex.com/z3 into opt |
|
More...
|
almost 12 years ago
|
| initial opt commands |
|
More...
|
almost 12 years ago
|
| test output predicates |
|
More...
|
almost 12 years ago
|
| Bugfix for equality rewriting on floats. |
|
More...
|
almost 12 years ago
|
| rewriter and value recognition bugfixes for floats |
|
More...
|
almost 12 years ago
|
| fixed potential performance problem with fully interpreted sorts in the quantifier instantiation. |
|
More...
|
almost 12 years ago
|
| Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable |
|
More...
|
almost 12 years ago
|
| Example fixed (substitute does not include a rewriter call anymore). |
|
More...
|
almost 12 years ago
|
| Fix z3.py doctests to reflect recent changes in the substitute API |
|
More...
|
almost 12 years ago
|
| Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable |
|
More...
|
almost 12 years ago
|
| use safe replace for external substitution |
|
More...
|
almost 12 years ago
|
| fix bug in ackerman reduction found by Anvesh |
|
More...
|
almost 12 years ago
|
| update join planner to take projected columns into account |
|
More...
|
almost 12 years ago
|
| test case for non-termination of substitution/rewriting |
|
More...
|
almost 12 years ago
|
| add test case for substitution |
|
More...
|
almost 12 years ago
|
| Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable |
|
More...
|
almost 12 years ago
|
| fix default argument identification |
|
More...
|
almost 12 years ago
|
| address incompleteness bug in axiomatization of int2bv |
|
More...
|
almost 12 years ago
|
| fix bugs reported by Anvesh |
|
More...
|
almost 12 years ago
|
