| 1926 | |
| 1927 | // / <remarks>Note: this test is specialized to 32-bit bitvectors.</remarks> |
| 1928 | public void checkSmall(Context ctx, Solver solver, BitVecExpr... to_minimize) |
| 1929 | { |
| 1930 | int num_Exprs = to_minimize.length; |
| 1931 | int[] upper = new int[num_Exprs]; |
| 1932 | int[] lower = new int[num_Exprs]; |
| 1933 | for (int i = 0; i < upper.length; ++i) |
| 1934 | { |
| 1935 | upper[i] = Integer.MAX_VALUE; |
| 1936 | lower[i] = 0; |
| 1937 | } |
| 1938 | boolean some_work = true; |
| 1939 | int last_index = -1; |
| 1940 | int last_upper = 0; |
| 1941 | while (some_work) |
| 1942 | { |
| 1943 | solver.push(); |
| 1944 | |
| 1945 | boolean check_is_sat = true; |
| 1946 | while (check_is_sat && some_work) |
| 1947 | { |
| 1948 | // Assert all feasible bounds. |
| 1949 | for (int i = 0; i < num_Exprs; ++i) |
| 1950 | { |
| 1951 | solver.add(ctx.mkBVULE(to_minimize[i], |
| 1952 | ctx.mkBV(upper[i], 32))); |
| 1953 | } |
| 1954 | |
| 1955 | check_is_sat = Status.SATISFIABLE == solver.check(); |
| 1956 | if (!check_is_sat) |
| 1957 | { |
| 1958 | if (last_index != -1) |
| 1959 | { |
| 1960 | lower[last_index] = last_upper + 1; |
| 1961 | } |
| 1962 | break; |
| 1963 | } |
| 1964 | System.out.println(solver.getModel()); |
| 1965 | |
| 1966 | // narrow the bounds based on the current model. |
| 1967 | for (int i = 0; i < num_Exprs; ++i) |
| 1968 | { |
| 1969 | Expr v = solver.getModel().evaluate(to_minimize[i], false); |
| 1970 | int ui = ((BitVecNum) v).getInt(); |
| 1971 | if (ui < upper[i]) |
| 1972 | { |
| 1973 | upper[i] = (int) ui; |
| 1974 | } |
| 1975 | System.out.println(i + " " + lower[i] + " " + upper[i]); |
| 1976 | } |
| 1977 | |
| 1978 | // find a new bound to add |
| 1979 | some_work = false; |
| 1980 | last_index = 0; |
| 1981 | for (int i = 0; i < num_Exprs; ++i) |
| 1982 | { |
| 1983 | if (lower[i] < upper[i]) |
| 1984 | { |
| 1985 | last_upper = (upper[i] + lower[i]) / 2; |