Map Elimination Implementation

srk/src/arraylift.ml

@@ -0,0 +1,178 @@
+open Syntax
+open Iteration
+
+(* bubble_sym is an internal helper function for lowering formulas in the skolem array fragment
+    to quantified numerical formulas. 
+    [bubble_sym srk form] returns a triple of the form (syms, fr, form') in which:
+        - form ==> \exists syms. \forall fr.  form' 
+        - form' contains no array terms
+*) 
+let bubble_sym (srk : 'a context) (form : 'a formula) : (symbol list * (symbol) * 'a formula) = 
+  (* rep_map : arr_var -> (index_term -> var) *)
+  let (rep_map : (symbol, ('a, Syntax.typ_arith, symbol) Expr.HT.t) Hashtbl.t) = Hashtbl.create 16 in 
+  let leading_existentials = ref [] in 
+  let forall_symbol = mk_symbol srk `TyInt ~name:"forall_index" in
+
+  let get_or_create_replacement array_symbol index_term = 
+    let replacement_map = Hashtbl.find rep_map array_symbol in 
+    match Expr.HT.mem replacement_map index_term with 
+      | true -> mk_const srk (Expr.HT.find replacement_map index_term)
+      | false -> (
+        let name = Format.asprintf "rep_%a_%a"
+          (pp_symbol srk) array_symbol
+          (ArithTerm.pp srk) index_term
+        in
+        let replacement = mk_symbol srk `TyInt ~name in
+        Expr.HT.add replacement_map index_term replacement;
+        leading_existentials := replacement :: !leading_existentials; (* Update the mutable list *)
+        mk_const srk replacement
+      )
+  in
+
+  (* All variables are turned into symbols as we recurse across the formula.
+    env maps from variable indices to symbols. 
+    qo is the index of the forall variable. 
+    Variables with index > qo are existentially quantified outside the forall.
+    Note that replace functions only get run after we have found the forall.
+  *)
+  (* [replace_access arr i env qo] returns a substitute term for arr[i] *)
+  let rec replace_access (arr : 'a arr_term) (index : 'a arith_term) (env : (symbol Env.t)) (qo : int) : 'a arith_term = 
+    match ArrTerm.destruct srk arr with 
+    | `Var (i, _) -> 
+        if (i <= qo) then (failwith "Array term is not quantified inside the forall") else ( 
+          let array_symbol = Env.find env (i - qo) in 
+          match ArithTerm.destruct srk index with 
+            | `Var (indi, _) -> 
+              ((if indi < qo then failwith "Array index variable is bound but should be free");
+              let index_symbol = Env.find env (indi - qo) in 
+              get_or_create_replacement array_symbol (mk_const srk index_symbol))
+            | `App (_, []) | `Real _ -> 
+              get_or_create_replacement array_symbol index
+            | _ -> failwith "Array index should be a variable, symbol, or constant"
+        ) 
+    | `App (_, _) -> failwith "Array applications not supported"
+    | `Ite (f, l, r) -> mk_ite srk f (replace_access l index env qo) (replace_access r index env qo)
+    | `Store (a, store_index, value) ->
+      let ae = replace_access a index env qo in 
+      mk_ite srk (mk_eq srk store_index index) value ae 
+    in
+  let replace env f = 
+    fold_rewrite srk 
+    ~down:(fun e qo -> match destruct srk e with | `Var (i, t) -> if i >= qo && t != `TyArr then (mk_const srk (Env.find env (i - qo))) else e | _ -> e)
+    ~up:(fun e qo -> match destruct srk e with | `Select (arr, index) -> replace_access arr index env qo | _ -> e)
+    ~combine:(fun e qo -> match destruct srk e with | `Quantify (`Exists, _, _, _) -> qo + 1 | `Quantify (`Forall, _, _, _) -> failwith "Nested foralls" | _ -> qo)
+    0 f
+  in
+
+  (* go contains the core "bubbling" logic of this algorithm: 
+    we process leading existentials, skolemizing them and adding them to env.
+    Once we reach a forall, we stop processing existentials and switch over to replace functions
+    to eliminate array terms.
+  *)
+  (* [go form env] considers the formula \exists env . form
+     and returns form' where
+        - form' contains no array terms
+        - \exists env . form ==> \exists syms. \forall forall_sym. form' 
+         *)
+  let rec go (f : 'a formula) (env : (symbol Env.t)): ('a formula) = 
+     match Formula.destruct srk f with 
+    | `Quantify (`Exists, name, typ, body) -> 
+      let new_sym = mk_symbol srk ~name (typ :> typ) in 
+      (if typ = `TyArr then (
+        Hashtbl.add rep_map new_sym (Expr.HT.create 16);
+        let name = Format.asprintf "rep_%a_univ"
+          (pp_symbol srk) new_sym
+        in
+        Expr.HT.add (Hashtbl.find rep_map new_sym) (mk_const srk forall_symbol) (mk_symbol srk `TyInt ~name);
+        let body' = go body (Env.push new_sym env) in 
+        let ai = get_or_create_replacement new_sym (mk_const srk forall_symbol) in 
+        let fc = BatEnum.fold (fun acc (index, replacement) ->
+            (mk_if srk (mk_eq srk index (mk_const srk forall_symbol)) (mk_eq srk (mk_const srk replacement) ai)) :: acc
+          ) [] (Expr.HT.enum (Hashtbl.find rep_map new_sym)) in 
+        let body'' = mk_exists_const srk (Expr.HT.find (Hashtbl.find rep_map new_sym) (mk_const srk forall_symbol)) 
+          (mk_and srk ((body') :: fc))
+      in 
+        body''
+      ) else (
+        leading_existentials := new_sym :: !leading_existentials; 
+        go body (Env.push new_sym env) 
+        ))
+    | `Quantify (`Forall, _, typ, body) -> 
+      assert (typ = `TyInt);
+      replace (Env.push forall_symbol env) body
+    | `And ls -> 
+      let (parts) = List.fold_left (fun parts f -> 
+         go f env :: parts
+      ) [] ls in 
+      (mk_and srk parts)
+    | `Or ls ->
+      let branch_var = mk_symbol srk ~name:"branch" `TyInt in 
+      (leading_existentials := branch_var :: !leading_existentials);
+      let (parts) = List.fold_left (fun parts f -> 
+          go f env :: parts  
+        ) [] ls in 
+      let parts = List.mapi (fun i part -> mk_and srk [part; mk_eq srk (mk_const srk branch_var) (mk_int srk i)]) parts in 
+      (mk_or srk parts)
+    | `Atom _ | `Proposition _ -> 
+      (* At this point, we want to run replace but cannot because we haven't yet seen a forall.
+        We use the equivalence f <=> \forall d. f where f is d-free
+        to map back to the forall case.
+      *)
+      let f' = substitute srk (fun (i, typ) -> mk_var srk (i + 1) typ) f in 
+      go (mk_forall srk `TyInt f') env 
+    | `Tru | `Fls -> (f)
+    | `Ite (f, l, r) -> 
+      let f' = mk_or srk [mk_and srk [f ; l]; mk_and srk [mk_not srk f; r]] in 
+      let f' = rewrite srk ~down:(pos_rewriter srk) f' in 
+      go f' env
+    | `Not _ -> failwith "Not is not supported in Skolem fragment"
+  in
+  let retf = go form Syntax.Env.empty in 
+  (!leading_existentials, forall_symbol, retf)
+
+
+
+(* 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) = 
+  fun (tf : 'a TransitionFormula.t) (k : 'a arith_term) ->
+    let f = TransitionFormula.formula tf in 
+    let array_symbols = List.filter (fun (s, s') -> typ_symbol srk s = `TyArr && typ_symbol srk s' = `TyArr) (TransitionFormula.symbols tf) in 
+    let zs = List.fold_left (fun acc (s, s') -> (s, mk_symbol srk `TyInt) :: (s', mk_symbol srk `TyInt) :: acc) [] array_symbols in 
+    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 = Symbol.Set.fold (fun s acc->
+      if typ_symbol srk s = `TyArr then mk_exists_const srk s acc else acc
+      ) (Syntax.symbols projected_formula) projected_formula in 
+
+    let existentials, forall, skol = bubble_sym srk projected_formula in
+    let with_universal = mk_forall_const srk forall skol in
+
+    let with_everything = List.fold_left (fun acc s -> mk_exists_const srk s acc) with_universal existentials in 
+
+    let eliminated = SrkZ3.qe srk with_everything in 
+
+    let tf'_symbols = (j, j') :: List.map (fun (s, s') -> if (typ_symbol srk s = `TyArr) then (((List.find (fun (sym, _) -> sym = s') zs) |> snd), ((List.find (fun (sym, _) -> sym = s') zs) |> snd)) else (s, s')) (TransitionFormula.symbols tf) in 
+    let tf' = TransitionFormula.make ~exists:(fun sym -> (not (List.exists (fun (s, s') -> s = sym || s' = sym) tf'_symbols)) && TransitionFormula.exists tf sym) eliminated tf'_symbols in 
+    let solver' = Solver.make srk tf' in
+
+    let exponentiated = e solver' k in 
+
+    let ret = substitute_sym srk (fun s ->
+      match List.find_opt (fun (_, z) -> s = z) zs with 
+        | Some (a, _) -> mk_select srk (mk_const srk a) (mk_const srk j)
+        | None -> mk_const srk s
+      ) exponentiated in 
+    let ret = substitute_sym srk (fun s -> 
+        if s = j' then mk_const srk j else mk_const srk s) ret in 
+
+    mk_forall_const srk j ret 
+
+
+  (* [map_elim ctx f] takes a formula in the array skolem fragment and returns an equivalent formula over numerical variables. *)
+  let map_elim (srk : 'a context) (f : 'a formula) : 'a formula = 
+    let syms, forall, f = bubble_sym srk f in 
+    let f = mk_forall_const srk forall f in
+
+    let f = List.fold_left (fun acc sym -> mk_exists_const srk sym acc) f syms in 
+    f

srk/src/arraylift.mli

@@ -0,0 +1,17 @@
+open Syntax
+
+
+(** [array_exponentiate ctx exp_op] takes an exponentiation operation [exp_op]
+  , and returns an exponentiation operator which numerically abstracts the array variables
+  in the formula, applies exp_op, then reintroduces the array variables 
+*)
+val array_exponentiate :
+  'a context ->
+  'a Iteration.exp_op ->
+  ('a TransitionFormula.t -> 'a arith_term -> 'a formula)
+
+
+(** [map_elim ctx formula] computes an equisatisfiable formula to [formula]
+  in which all array variables are replaced with numerical abstractions.
+*)
+val map_elim : 'a context -> 'a formula -> 'a formula

srk/src/syntax.ml

@@ -554,6 +554,7 @@ let destruct _srk sexpr =
   | Node (App func, args, _) -> `App (func, args)
   | Node (Var (v, `TyReal), [], _) -> `Var (v, `TyReal)
   | Node (Var (v, `TyInt), [], _) -> `Var (v, `TyInt)
+  | Node (Var (v, `TyArr), [], _) -> `Var (v, `TyArr)
   | Node (Var (v, `TyBool), [], _) -> `Proposition (`Var v)
   | Node (Add, sum, _) -> `Add sum
   | Node (Mul, product, _) -> `Mul product
@@ -1608,6 +1609,15 @@ let rec rewrite srk ?down:(down=fun x -> x) ?up:(up=fun x -> x) sexpr =
   let (Node (label, children, _)) = (down sexpr).obj in
   up (srk.mk label (List.map (rewrite srk ~down ~up) children))
 
+let fold_rewrite srk ?down:(down=fun x _ ->x) ?up:(up=fun x _ -> x) ?combine:(combine=fun _ a -> a) acc sexpr = 
+  let rec go acc e = 
+    let d = (down e acc) in 
+    let (Node (label, children, _)) = d.obj in
+    let acc' = combine d acc in 
+    up (srk.mk label (List.map (go acc') children)) acc 
+  in
+  go acc sexpr
+
 let mk_compare op =
   match op with
   | `Eq -> mk_eq

srk/src/syntax.mli

@@ -227,6 +227,14 @@ type ('a, 'b) rewriter = ('a, 'b) expr -> ('a, 'b) expr
 val rewrite : 'a context -> ?down:(('a, 'b) rewriter) -> ?up:(('a, 'b) rewriter) ->
   ('a, 'typ) expr -> ('a, 'typ) expr
 
+(** Rewrite an expression while folding over the tree. The {i down} rewriter is applied to each
+    expression goign down the expression tree and the {i up} rewriter is
+    applied to each expression going up the tree. The accumulator is updated at each node after
+    the down rewrite.
+*)
+val fold_rewrite: 'a context -> ?down:(('a, 'b) expr -> 'c -> ('a, 'b) expr) -> ?up:(('a, 'b) expr -> 'c -> ('a, 'b) expr) -> 
+  ?combine:(('a, 'typ) expr -> 'c -> 'c) -> 'c -> ('a, 'typ) expr -> ('a, 'typ) expr
+
 (** Convert to negation normal form ({i down} pass). *)
 val nnf_rewriter : 'a context -> ('a, typ_fo) rewriter
 

srk/src/transitionFormula.ml

@@ -7,6 +7,14 @@ type 'a t =
 
 include Log.Make(struct let name = "srk.transitionFormula" end)
 
+let pp srk formatter tf =
+  let open Format in
+  let pp_symbol_pair formatter (s, s') =
+    fprintf formatter "%s -> %s" (show_symbol srk s) (show_symbol srk s')
+  in
+  fprintf formatter "TransitionFormula(@[<v 2>\n  symbols = [@[<hov>%a@]],@ formula = %a@])"
+    (pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt ",@ ") pp_symbol_pair) tf.symbols
+    (Formula.pp srk) tf.formula
 
 let identity srk symbols =
   let formula = 

srk/src/transitionFormula.mli

@@ -13,6 +13,7 @@ open Syntax
    as existentially quantified variables). *)
 type 'a t
 
+val show : 'a context -> 'a t -> string
 (** Construct a transition formula.  The [exists] predicate identifies
    Skolem constants ([exists s] fails if [s] is a Skolem constant),
    with the default behavior that no symbols are Skolem consntas; the