| 1154 | // / Then, assert <tt>not(x = y)</tt>, and find another model. |
| 1155 | |
| 1156 | public void findModelExample2(Context ctx) throws TestFailedException |
| 1157 | { |
| 1158 | System.out.println("FindModelExample2"); |
| 1159 | Log.append("FindModelExample2"); |
| 1160 | |
| 1161 | IntExpr x = ctx.mkIntConst("x"); |
| 1162 | IntExpr y = ctx.mkIntConst("y"); |
| 1163 | IntExpr one = ctx.mkInt(1); |
| 1164 | IntExpr two = ctx.mkInt(2); |
| 1165 | |
| 1166 | ArithExpr y_plus_one = ctx.mkAdd(y, one); |
| 1167 | |
| 1168 | BoolExpr c1 = ctx.mkLt(x, y_plus_one); |
| 1169 | BoolExpr c2 = ctx.mkGt(x, two); |
| 1170 | |
| 1171 | BoolExpr q = ctx.mkAnd(c1, c2); |
| 1172 | |
| 1173 | System.out.println("model for: x < y + 1, x > 2"); |
| 1174 | Model model = check(ctx, q, Status.SATISFIABLE); |
| 1175 | System.out.println("x = " + model.evaluate(x, false) + ", y =" |
| 1176 | + model.evaluate(y, false)); |
| 1177 | |
| 1178 | /* assert not(x = y) */ |
| 1179 | BoolExpr x_eq_y = ctx.mkEq(x, y); |
| 1180 | BoolExpr c3 = ctx.mkNot(x_eq_y); |
| 1181 | |
| 1182 | q = ctx.mkAnd(q, c3); |
| 1183 | |
| 1184 | System.out.println("model for: x < y + 1, x > 2, not(x = y)"); |
| 1185 | model = check(ctx, q, Status.SATISFIABLE); |
| 1186 | System.out.println("x = " + model.evaluate(x, false) + ", y = " |
| 1187 | + model.evaluate(y, false)); |
| 1188 | } |
| 1189 | |
| 1190 | // / Prove <tt>x = y implies g(x) = g(y)</tt>, and |
| 1191 | // / disprove <tt>x = y implies g(g(x)) = g(y)</tt>. |