Demonstrate how to use Push and Pop to control the size of models. Note: this test is specialized to 32-bit bitvectors.
(Context ctx, Solver solver, BitVecExpr[] to_minimize)
| 1823 | /// </summary> |
| 1824 | /// <remarks>Note: this test is specialized to 32-bit bitvectors.</remarks> |
| 1825 | public static void CheckSmall(Context ctx, Solver solver, BitVecExpr[] to_minimize) |
| 1826 | { |
| 1827 | Sort bv32 = ctx.MkBitVecSort(32); |
| 1828 | |
| 1829 | int num_Exprs = to_minimize.Length; |
| 1830 | UInt32[] upper = new UInt32[num_Exprs]; |
| 1831 | UInt32[] lower = new UInt32[num_Exprs]; |
| 1832 | BitVecExpr[] values = new BitVecExpr[num_Exprs]; |
| 1833 | for (int i = 0; i < upper.Length; ++i) |
| 1834 | { |
| 1835 | upper[i] = UInt32.MaxValue; |
| 1836 | lower[i] = 0; |
| 1837 | } |
| 1838 | bool some_work = true; |
| 1839 | int last_index = -1; |
| 1840 | UInt32 last_upper = 0; |
| 1841 | while (some_work) |
| 1842 | { |
| 1843 | solver.Push(); |
| 1844 | |
| 1845 | bool check_is_sat = true; |
| 1846 | while (check_is_sat && some_work) |
| 1847 | { |
| 1848 | // Assert all feasible bounds. |
| 1849 | for (int i = 0; i < num_Exprs; ++i) |
| 1850 | { |
| 1851 | solver.Assert(ctx.MkBVULE(to_minimize[i], ctx.MkBV(upper[i], 32))); |
| 1852 | } |
| 1853 | |
| 1854 | check_is_sat = Status.SATISFIABLE == solver.Check(); |
| 1855 | if (!check_is_sat) |
| 1856 | { |
| 1857 | if (last_index != -1) |
| 1858 | { |
| 1859 | lower[last_index] = last_upper + 1; |
| 1860 | } |
| 1861 | break; |
| 1862 | } |
| 1863 | Console.WriteLine("{0}", solver.Model); |
| 1864 | |
| 1865 | // narrow the bounds based on the current model. |
| 1866 | for (int i = 0; i < num_Exprs; ++i) |
| 1867 | { |
| 1868 | Expr v = solver.Model.Evaluate(to_minimize[i]); |
| 1869 | UInt64 ui = ((BitVecNum)v).UInt64; |
| 1870 | if (ui < upper[i]) |
| 1871 | { |
| 1872 | upper[i] = (UInt32)ui; |
| 1873 | } |
| 1874 | Console.WriteLine("{0} {1} {2}", i, lower[i], upper[i]); |
| 1875 | } |
| 1876 | |
| 1877 | // find a new bound to add |
| 1878 | some_work = false; |
| 1879 | last_index = 0; |
| 1880 | for (int i = 0; i < num_Exprs; ++i) |
| 1881 | { |
| 1882 | if (lower[i] < upper[i]) |