| 945 | // / Then, assert <tt>not(x = y)</tt>, and find another model. |
| 946 | |
| 947 | public void findModelExample2(Context ctx) throws TestFailedException |
| 948 | { |
| 949 | System.out.println("FindModelExample2"); |
| 950 | Log.append("FindModelExample2"); |
| 951 | |
| 952 | IntExpr x = ctx.mkIntConst("x"); |
| 953 | IntExpr y = ctx.mkIntConst("y"); |
| 954 | IntNum one = ctx.mkInt(1); |
| 955 | IntNum two = ctx.mkInt(2); |
| 956 | |
| 957 | ArithExpr<IntSort> y_plus_one = ctx.mkAdd(y, one); |
| 958 | |
| 959 | BoolExpr c1 = ctx.mkLt(x, y_plus_one); |
| 960 | BoolExpr c2 = ctx.mkGt(x, two); |
| 961 | |
| 962 | BoolExpr q = ctx.mkAnd(c1, c2); |
| 963 | |
| 964 | System.out.println("model for: x < y + 1, x > 2"); |
| 965 | Model model = check(ctx, q, Status.SATISFIABLE); |
| 966 | System.out.printf("x = %s, y =%s%n", model.evaluate(x, false), model.evaluate(y, false)); |
| 967 | |
| 968 | /* assert not(x = y) */ |
| 969 | BoolExpr x_eq_y = ctx.mkEq(x, y); |
| 970 | BoolExpr c3 = ctx.mkNot(x_eq_y); |
| 971 | |
| 972 | q = ctx.mkAnd(q, c3); |
| 973 | |
| 974 | System.out.println("model for: x < y + 1, x > 2, not(x = y)"); |
| 975 | model = check(ctx, q, Status.SATISFIABLE); |
| 976 | System.out.printf("x = %s, y = %s%n", model.evaluate(x, false), model.evaluate(y, false)); |
| 977 | } |
| 978 | |
| 979 | // / Prove <tt>x = y implies g(x) = g(y)</tt>, and |
| 980 | // / disprove <tt>x = y implies g(g(x)) = g(y)</tt>. |