Map Elimination Implementation#74
Conversation
| let ae = replace_access a index env qo in | ||
| mk_ite srk (mk_eq srk store_index index) value ae | ||
| (* replace_at recurses over arith_terms, performing substitution *) | ||
| and replace_at (t : 'a arith_term) (env : (symbol Env.t)) (qo : int) : 'a arith_term = |
There was a problem hiding this comment.
I think this is: rewrite srk ~up:(function Select(arr, index) -> replace_access arr index env qo | x -> x) t
There was a problem hiding this comment.
There's some details in the handling of Var and Ite that aren't so easy to express as a rewriter - I think it's more readable to leave everything explicit.
There was a problem hiding this comment.
Well, Var (i, t) needs to search in the environment to find the relevant skolem constant, which is easy to put in a rewriter.
But Ite (f, l, r) needs to apply replace (for formulas) to f and replace_at to l and r. I'm not sure exactly how to put that as a rewriter.
Does changing the implementation of replace_at to use rewriter buy us anything in terms of performance? Because otherwise we'll have a match statement regardless.
There was a problem hiding this comment.
My understanding is that the purpose of replace/replace_at is to replace every array selection term according to replace_access (but the reason they're two separate functions is that replace operates on formulas and replace_at operates on terms). If that's the case,
fun expr -> rewrite srk ~up:(function Select(arr, index) -> replace_access arr index env qo | x -> x) expr
does the same thing, and works for both formulas and terms.
There was a problem hiding this comment.
That is true, but it is also responsible for replacing existential variables with the new skolem constants that were introduced in go. The logic for this is in the Var case of replace_at and the Exists case of replace. This is difficult to implement as a rewriter because we need additional context about the quantifier offset (qo) of variables we should replace versus leave unchanged.
|
@zkincaid I'm done making edits based on your review - it's ready to be looked over again. All tests pass. |
| *) | ||
| let bubble_sym (srk : 'a context) (form : 'a formula) : (symbol list * (symbol option) * 'a formula) = | ||
| (* rep_map : arr_var -> (index_term -> var) *) | ||
| let (rep_map : (symbol, ('a arith_term, symbol) Hashtbl.t) Hashtbl.t) = Hashtbl.create 16 in |
There was a problem hiding this comment.
arith_term should not be used as a key for hashtbl -- use Expr.HT (this gives constant-time hashing).
(Or use Expr.ExprMemo to memoize get_or_create_replacement)
| let ae = replace_access a index env qo in | ||
| mk_ite srk (mk_eq srk store_index index) value ae | ||
| (* replace_at recurses over arith_terms, performing substitution *) | ||
| and replace_at (t : 'a arith_term) (env : (symbol Env.t)) (qo : int) : 'a arith_term = |
| | `Quantify (`Forall, _, typ, body) -> | ||
| assert (typ = `TyInt); | ||
| let (body) = replace (Env.push forall_symbol env) 0 body in | ||
| let functional_correctness = (Hashtbl.fold (fun array_symbol m (acc) -> |
There was a problem hiding this comment.
The logic is not correct here. Functional consistency axioms for the array a need to be inserted at the existential for a, not the universal quantifier.
Test case that should reveal the problem: exists n,m : int. exists a : array. n = m /\ a[n] != a[m]
There was a problem hiding this comment.
That test case was unproblematic - after applying map_elim it was still UNSAT.
Because our algorithm automatically assumes a universal at any atom, we treat the above test case as exists n,m : int. exists a : array. forall i. n = m /\ a[n] != a[m].
The result of calling map elim looks like:
exists b, n, m, a_n, a_m. forall i. exists a_i . n = m /\ ((b=0 /\ a_n < a_m /\ FC) / (b = 1 /\ a_m < a_n /\ FC))
where:
FC: (m = i => a_m = a_i) /\ (n = i => a_n = a_i)
And this formula is UNSAT as expected.
There was a problem hiding this comment.
Ah, I see -- atomic formulas are treated as being universally quantified per line 140. But then shouldn' this be treated the same as
exists n,m : int. exists a : array. (forall i. n = m) /\ (forall i. a[n] != a[m]).
(which should also give the incorrect result?).
Is the existentially-quantified "b" variable really introduced for this example? It shouldn't be -- if the formula is unsat because it's asserting both b=0 and b=1, then it's masking the problem.
There was a problem hiding this comment.
Yes, it does get treated as (forall i. n = m) /\ (forall i. a[n] != a[m]), but this gets "bubbled" to forall i. (n = m /\ a[n] != a[m]) per one of the rewrite rules. It is true that this results in the functional consistency axioms being duplicated in each conjuct.
The FC axioms need to appear inside the forall, right? Because the universal "i" is needed within the definition of FC.
The existential b gets introduced because a[n] != a[m] gets rewritten to a[n] < a[m] / a[n] > a[m] to get rid of the negation.
|
@zkincaid Finished changes as discussed in meeting. |
|
|
||
| (* array_exponentiate lifts exponentiation operator e to work over formulas with arrays. *) | ||
| let array_exponentiate (srk : 'a context) (e : 'a exp_op) : ('a TransitionFormula.t -> 'a Syntax.arith_term -> 'a Syntax.formula) = | ||
| let e' (tf : 'a TransitionFormula.t) (k : 'a arith_term) : ('a formula) = |
| let j = mk_symbol srk ~name:"j" `TyInt in | ||
| let j' = mk_symbol srk ~name:"j'" `TyInt in | ||
| let projected_formula = mk_and srk (f :: (mk_eq srk (mk_const srk j) (mk_const srk j')) :: (List.map (fun (a, z) -> mk_eq srk (mk_select srk (mk_const srk a) (mk_const srk j)) (mk_const srk z)) zs)) in | ||
| let projected_formula = List.fold_left (fun acc (s, s') -> |
There was a problem hiding this comment.
TransitionFormula.symbols includes symbols corresponding to unprimed/primed "program variables", but not Skolem constants -- array-sorted Skolem constants also need to be removed. Can do this Syntax.symbols f should give you what you need.
| ) projected_formula (TransitionFormula.symbols tf) in | ||
|
|
||
| let existentials, forall, skol = bubble_sym srk projected_formula in | ||
| let with_universal = match forall with |
There was a problem hiding this comment.
I'm not confident in the logic here. A formula that starts without a forall might need one in the end (since we can introduce functional consistency axioms that talk about the universally quantified variable, which will be left as a skolem constant if we don't apply mk_forall_const).
There was a problem hiding this comment.
With that in mind -- does bubble_sym need to compute that middle "forall" value?
There was a problem hiding this comment.
This is true - we don't need to do any computation for the forall value, it will always exist and it will always be the forall_symbol instantiated at the top of bubble_sym. I changed bubble_sym to just return this value, and removed forall from the internal go loop.
2 participants
array_lift.ml - implementation of the "bubble" algorithm for map elimination, and two handlers: map_elim which eliminates array variables from a formula and array_exponentiate which lifts exponentiation operators to work over arrays.
test_arraylist.ml - some initial tests for these functions
transitionFormula - added a printing function for transition formulas.