| 1729 | |
| 1730 | // / <remarks>Note: this test is specialized to 32-bit bitvectors.</remarks> |
| 1731 | public void checkSmall(Context ctx, Solver solver, BitVecExpr... to_minimize) |
| 1732 | { |
| 1733 | int num_Exprs = to_minimize.length; |
| 1734 | int[] upper = new int[num_Exprs]; |
| 1735 | int[] lower = new int[num_Exprs]; |
| 1736 | for (int i = 0; i < upper.length; ++i) |
| 1737 | { |
| 1738 | upper[i] = Integer.MAX_VALUE; |
| 1739 | lower[i] = 0; |
| 1740 | } |
| 1741 | boolean some_work = true; |
| 1742 | int last_index = -1; |
| 1743 | int last_upper = 0; |
| 1744 | while (some_work) |
| 1745 | { |
| 1746 | solver.push(); |
| 1747 | |
| 1748 | boolean check_is_sat = true; |
| 1749 | while (some_work) |
| 1750 | { |
| 1751 | // Assert all feasible bounds. |
| 1752 | for (int i = 0; i < num_Exprs; ++i) |
| 1753 | { |
| 1754 | solver.add(ctx.mkBVULE(to_minimize[i], |
| 1755 | ctx.mkBV(upper[i], 32))); |
| 1756 | } |
| 1757 | |
| 1758 | check_is_sat = Status.SATISFIABLE == solver.check(); |
| 1759 | if (!check_is_sat) |
| 1760 | { |
| 1761 | if (last_index != -1) |
| 1762 | { |
| 1763 | lower[last_index] = last_upper + 1; |
| 1764 | } |
| 1765 | break; |
| 1766 | } |
| 1767 | System.out.println(solver.getModel()); |
| 1768 | |
| 1769 | // narrow the bounds based on the current model. |
| 1770 | for (int i = 0; i < num_Exprs; ++i) |
| 1771 | { |
| 1772 | Expr<BitVecSort> v = solver.getModel().evaluate(to_minimize[i], false); |
| 1773 | // we still have to cast because we want to use a method in BitVecNum |
| 1774 | // however, we cannot cast to a type which doesn't match the generic, e.g. IntNum |
| 1775 | int ui = ((BitVecNum) v).getInt(); |
| 1776 | if (ui < upper[i]) |
| 1777 | { |
| 1778 | upper[i] = ui; |
| 1779 | } |
| 1780 | System.out.printf("%d %d %d%n", i, lower[i], upper[i]); |
| 1781 | } |
| 1782 | |
| 1783 | // find a new bound to add |
| 1784 | some_work = false; |
| 1785 | last_index = 0; |
| 1786 | for (int i = 0; i < num_Exprs; ++i) |
| 1787 | { |
| 1788 | if (lower[i] < upper[i]) |