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