| 1820 | // / Simplifier example. |
| 1821 | |
| 1822 | @SuppressWarnings("unchecked") |
| 1823 | public void simplifierExample(Context ctx) |
| 1824 | { |
| 1825 | System.out.println("SimplifierExample"); |
| 1826 | Log.append("SimplifierExample"); |
| 1827 | |
| 1828 | IntExpr x = ctx.mkIntConst("x"); |
| 1829 | IntExpr y = ctx.mkIntConst("y"); |
| 1830 | IntExpr z = ctx.mkIntConst("z"); |
| 1831 | @SuppressWarnings("unused") |
| 1832 | IntExpr u = ctx.mkIntConst("u"); |
| 1833 | |
| 1834 | ArithExpr<IntSort> t1 = ctx.mkAdd(x, ctx.mkSub(y, ctx.mkAdd(x, z))); |
| 1835 | Expr<IntSort> t2 = t1.simplify(); |
| 1836 | System.out.printf("%s -> %s%n", t1, t2); |
| 1837 | } |
| 1838 | |
| 1839 | // / Extract unsatisfiable core example |
| 1840 | |