fixConfig.ml

(*
 * Copyright © 2009 The Regents of the University of California. All rights reserved. 
 *
 * Permission is hereby granted, without written agreement and without 
 * license or royalty fees, to use, copy, modify, and distribute this 
 * software and its documentation for any purpose, provided that the 
 * above copyright notice and the following two paragraphs appear in 
 * all copies of this software. 
 * 
 * IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY 
 * FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES 
 * ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN 
 * IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY 
 * OF SUCH DAMAGE. 
 * 
 * THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, 
 * INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY 
 * AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS 
 * ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION 
 * TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
 *)

module Sy  = Ast.Symbol
module SM  = Sy.SMap
module Q   = Qualifier
module C   = FixConstraint
module So  = Ast.Sort

open Misc.Ops

exception UnmappedKvar of Ast.Symbol.t


type qbind   = Q.t list

type solbind = Ast.Symbol.t * ((Ast.Symbol.t * (Ast.expr list)) list)

type deft = Srt of Ast.Sort.t 
          | Axm of Ast.pred 
          | Cst of FixConstraint.t
          | Wfc of FixConstraint.wf
          | Con of Ast.Symbol.t * Ast.Sort.t
          | Sol of solbind
          (* | Sol of Ast.Symbol.t * (Ast.pred * (Ast.Symbol.t * Ast.Subst.t)) list *)
          | Qul of Q.t
          | Dep of FixConstraint.dep


type 'bind cfg = { 
   a    : int                               (* Tag arity *)
 ; ts   : Ast.Sort.t list                   (* New sorts, now = []*)
 ; ps   : Ast.pred list                     (* New axioms, now = [] *)
 ; cs   : FixConstraint.t list
 ; ws   : FixConstraint.wf list
 ; ds   : FixConstraint.dep list
 ; qs   : Q.t list
 ; bm   : 'bind SM.t                        (* Initial Sol Bindings *)
 ; uops : Ast.Sort.t Ast.Symbol.SMap.t      (* Globals: measures + distinct consts) *)
 ; cons : Ast.Symbol.t list                 (* Distinct Constants, defined in uops *)
 ; assm : FixConstraint.soln                (* Seed Solution -- must be a fixpoint over constraints *)
}

let get_arity = function
  | []   -> Constants.logPrintf "WARNING: NO CONSTRAINTS!"; 0
  | c::_ -> c |> FixConstraint.tag_of_t |> fst |> List.length

(* {{{ 
let qual_rename i q = 
  Q.rename ((Q.name_of_t q)^(string_of_int i)) q

let sift_quals ds = 
  ds |> Misc.map_partial (function Qul q -> Some q | _ -> None)
     |> List.fold_left begin fun (i, m) q -> 
          let n       = Q.name_of_t q in
          let (i',q') = if MSM.mem n m then (i+1, qual_rename i q) else (i, q) in
          (i', MSM.add (Q.name_of_t q') q' m)
        end (0, MSM.empty)
     >> (fun (i, _) -> if i <> 0 then Constants.logPrintf "WARNING: duplicate qualifier names")
     |> snd
}}} *)

let sift_quals ds = 
  ds |> Misc.map_partial (function Qul q -> Some q | _ -> None)
     >> (fun _ -> print_now "BEGIN: Q.normalize\n")
     |> Q.normalize 
     >> (fun _ -> print_now "DONE: Q.normalize\n")
     |> Misc.map (Misc.pad_fst Q.name_of_t)
     |> SM.of_list

let extend f cfg = function
  | Srt t         -> {cfg with ts   = t     :: cfg.ts }
  | Axm p         -> {cfg with ps   = p     :: cfg.ps }
  | Cst c         -> {cfg with cs   = c     :: cfg.cs }
  | Wfc w         -> {cfg with ws   = w     :: cfg.ws }
  | Dep d         -> {cfg with ds   = d     :: cfg.ds }
  | Qul q         -> {cfg with qs   = q     :: cfg.qs }
  | Sol (k, fess) -> {cfg with bm   = SM.add k (List.map f fess) cfg.bm  }
  | Con (s,t)     -> {cfg with cons = if So.is_func t then cfg.cons else s :: cfg.cons
                             ; uops = SM.add s t cfg.uops} 
  
let empty = { a    = 0 ; ts   = []; ps = []
            ; cs   = []; ws   = []; ds = []
            ; qs   = []; bm   = SM.empty
            ; cons = []; uops = SM.empty 
            ; assm = FixConstraint.empty_solution }

let fes2q qm (f, es) =
  let q   = SM.safeFind f qm "name2qual" in
  q |> Q.all_params_of_t
    |> List.map fst 
    |> Misc.flip (Misc.combine "FixConfig.fes2q") es
    |> Q.inst q 

(* API *)
let create ds =
  let qm  = sift_quals ds in
  ds |> List.fold_left (extend (fes2q qm)) empty
     |> (fun cfg -> {cfg with a  = get_arity cfg.cs})
     |> (fun cfg -> {cfg with ws = C.add_wf_ids cfg.ws})


(* API *)
let create_raw ts env ps a ds cs ws qs assm = 
  { empty with 
    a    = a
  ; ts   = ts
  ; uops = env
  ; ps   = ps
  ; ds   = ds
  ; cs   = cs
  ; ws   = C.add_wf_ids ws
  ; qs   = Q.normalize qs 
  ; assm = assm
  }


module type DOMAIN = sig
  type t
  type bind
  val empty        : t 
  (* val meet         : t -> t -> t *)
  val min_read     : t -> FixConstraint.soln
  val read         : t -> FixConstraint.soln
  val read_bind    : t -> Ast.Symbol.t -> bind
  val top          : t -> Ast.Symbol.t list -> t
  val refine       : t -> FixConstraint.t -> (bool * t)
  val unsat        : t -> FixConstraint.t -> bool
  val create       : bind cfg -> FixConstraint.soln option -> t
  val print        : Format.formatter -> t -> unit
  val print_stats  : Format.formatter -> t -> unit
  val dump         : t -> unit
  val ctr_examples : t -> FixConstraint.t list -> FixConstraint.t list -> Counterexample.cex list 
  val mkbind       : qbind -> bind
end

(* type t = Ast.Qualifier.def list list cfg *)

let print ppf me =
  (* Print cs *)
  Format.fprintf ppf "@[%a@] \n" (Misc.pprint_many true "\n" (C.print_t None)) me.cs;
  (* Print ws *)
  Format.fprintf ppf "@[%a@] \n" (Misc.pprint_many true "\n" (C.print_wf None)) me.ws;
  (* Print qs *)
  Format.fprintf ppf "@[%a@] \n" (Misc.pprint_many true "\n" Q.print) (Q.normalize me.qs)