(Context ctx, FuncDecl<R> f, int i)
| 47 | // / Where, <code>finv</code>is a fresh function declaration. |
| 48 | |
| 49 | public <R extends Sort> BoolExpr injAxiom(Context ctx, FuncDecl<R> f, int i) |
| 50 | { |
| 51 | Sort[] domain = f.getDomain(); |
| 52 | int sz = f.getDomainSize(); |
| 53 | |
| 54 | if (i >= sz) |
| 55 | { |
| 56 | System.out.println("failed to create inj axiom"); |
| 57 | return null; |
| 58 | } |
| 59 | |
| 60 | /* declare the i-th inverse of f: finv */ |
| 61 | Sort finv_domain = f.getRange(); |
| 62 | Sort finv_range = domain[i]; |
| 63 | FuncDecl<Sort> finv = ctx.mkFuncDecl("f_fresh", finv_domain, finv_range); |
| 64 | |
| 65 | /* allocate temporary arrays */ |
| 66 | /* fill types, names and xs */ |
| 67 | Sort[] types = domain.clone(); |
| 68 | List<Expr<Sort>> xs = IntStream.range(0, sz).mapToObj(j -> ctx.mkBound(j, types[j])).collect(Collectors.toList()); |
| 69 | Symbol[] names = IntStream.range(0, sz).mapToObj(j -> ctx.mkSymbol(String.format("x_%d", j))).toArray(Symbol[]::new); |
| 70 | |
| 71 | Expr<Sort> x_i = xs.get(i); |
| 72 | |
| 73 | /* create f(x_0, ..., x_i, ..., x_{n-1}) */ |
| 74 | Expr<R> fxs = f.apply(xs.toArray(new Expr[0])); |
| 75 | |
| 76 | /* create f_inv(f(x_0, ..., x_i, ..., x_{n-1})) */ |
| 77 | Expr<Sort> finv_fxs = finv.apply(fxs); |
| 78 | |
| 79 | /* create finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i */ |
| 80 | BoolExpr eq = ctx.mkEq(finv_fxs, x_i); |
| 81 | |
| 82 | /* use f(x_0, ..., x_i, ..., x_{n-1}) as the pattern for the quantifier */ |
| 83 | Pattern p = ctx.mkPattern(fxs); |
| 84 | |
| 85 | /* create & assert quantifier */ |
| 86 | |
| 87 | return ctx.mkForall(types, /* types of quantified variables */ |
| 88 | names, /* names of quantified variables */ |
| 89 | eq, 1, new Pattern[] { p } /* patterns */, null, null, null); |
| 90 | } |
| 91 | |
| 92 | // / Create axiom: function f is injective in the i-th argument. |
| 93 |
no test coverage detected