diff --git a/.merlin b/.merlin index d7ed7f73..6457aa65 100644 --- a/.merlin +++ b/.merlin @@ -4,7 +4,6 @@ S src/sat S src/smt S src/backend S src/util -S src/util/smtlib S tests B _build/src/ @@ -13,6 +12,7 @@ B _build/src/solver B _build/src/sat B _build/src/smt B _build/src/util -B _build/src/util/smtlib B _build/src/backend B _build/tests + +PKG dolmen diff --git a/_tags b/_tags index 6511633d..47e25776 100644 --- a/_tags +++ b/_tags @@ -9,10 +9,9 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20) : include : include : include -: include : include +: include : include -: include # Pack options : for-pack(Msat) @@ -22,6 +21,10 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20) : for-pack(Msat_sat) : for-pack(Msat_smt) +# Bin options +: package(dolmen) +: package(dolmen) + # more warnings : warn_K, warn_Y, warn_X : short_paths, safe_string, strict_sequence diff --git a/src/main.ml b/src/main.ml index 16a0ed8d..0a8676db 100644 --- a/src/main.ml +++ b/src/main.ml @@ -5,45 +5,27 @@ Copyright 2014 Simon Cruanes *) module F = Expr + (* module T = Msat_smt.Cnf.S module Sat = Msat_sat.Sat.Make(struct end) module Smt = Msat_smt.Smt.Make(struct end) module Mcsat = Msat_smt.Mcsat.Make(struct end) + *) + +module P = + Dolmen.Logic.Make(Dolmen.ParseLocation) + (Dolmen.Id)(Dolmen.Term)(Dolmen.Statement) exception Incorrect_model exception Out_of_time exception Out_of_space -(* IO wrappers *) -(* Types for input/output languages *) -type sat_input = - | Auto - | Dimacs - | Smtlib - -type sat_output = - | Standard (* Only output problem status *) - | Dedukti - | Dot - type solver = | Sat | Smt | Mcsat -let input = ref Auto -let output = ref Standard let solver = ref Smt - -let input_list = [ - "auto", Auto; - "dimacs", Dimacs; - "smtlib", Smtlib; -] -let output_list = [ - "dot", Dot; - "dk", Dedukti; -] let solver_list = [ "sat", Sat; "smt", Smt; @@ -61,86 +43,8 @@ let set_flag opt arg flag l = with Not_found -> invalid_arg (error_msg opt arg l) -let set_input s = set_flag "Input" s input input_list -let set_output s = set_flag "Output" s output output_list let set_solver s = set_flag "Solver" s solver solver_list -(* Input Parsing *) -let rec rev_flat_map f acc = function - | [] -> acc - | a :: r -> rev_flat_map f (List.rev_append (f a) acc) r - -let format_of_filename s = - let last n = - try String.sub s (String.length s - n) n - with Invalid_argument _ -> "" - in - if last 4 = ".cnf" then - Dimacs - else if last 5 = ".smt2" then - Smtlib - else (* Default choice *) - Dimacs - -let parse_with_input file = function - | Auto -> assert false - | Dimacs -> List.rev_map (List.rev_map F.mk_prop) (Parsedimacs.parse file) - | Smtlib -> rev_flat_map T.make_cnf [] (Smtlib.parse file) - -let parse_input file = - parse_with_input file (match !input with - | Auto -> format_of_filename file - | f -> f) - -(* Printing wrappers *) -let std = Format.std_formatter - -let print format = match !output with - | Standard -> - Format.kfprintf (fun fmt -> Format.fprintf fmt "@.") std format - | Dot -> - Format.fprintf std "/* "; - Format.kfprintf (fun fmt -> Format.fprintf fmt " */@.") std format - | Dedukti -> - Format.fprintf std "(; "; - Format.kfprintf (fun fmt -> Format.fprintf fmt " ;)@.") std format - -let print_proof proof = match !output with - | Standard -> () - | Dot -> Smt.print_dot std proof - | Dedukti -> Smt.print_dedukti std proof - -let print_mcproof proof = match !output with - | Standard -> () - | Dot -> Mcsat.print_dot std proof - | Dedukti -> Mcsat.print_dedukti std proof - -let rec print_cl fmt = function - | [] -> Format.fprintf fmt "[]" - | [a] -> F.print fmt a - | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" F.print a print_cl r - -let print_lcl l = - List.iter (fun c -> Format.fprintf std "%a@\n" print_cl c) l - -let print_lclause l = - List.iter (fun c -> Format.fprintf std "%a@\n" Smt.print_clause c) l - -let print_mclause l = - List.iter (fun c -> Format.fprintf std "%a@\n" Mcsat.print_clause c) l - -let print_cnf cnf = match !output with - | Standard -> print_lcl cnf - | Dot | Dedukti -> () - -let print_unsat_core u = match !output with - | Standard -> print_lclause u - | Dot | Dedukti -> () - -let print_mc_unsat_core u = match !output with - | Standard -> print_mclause u - | Dot | Dedukti -> () - (* Arguments parsing *) let file = ref "" let p_cnf = ref false @@ -170,7 +74,7 @@ let int_arg r arg = | 'd' -> multiplier 86400. | '0'..'9' -> r := float_of_string arg | _ -> raise (Arg.Bad "bad numeric argument") - with Failure "float_of_string" -> raise (Arg.Bad "bad numeric argument") + with Failure _ -> raise (Arg.Bad "bad numeric argument") let setup_gc_stat () = at_exit (fun () -> @@ -189,12 +93,8 @@ let argspec = Arg.align [ " Build, check and print the proof (if output is set), if unsat"; "-gc", Arg.Unit setup_gc_stat, " Outputs statistics about the GC"; - "-i", Arg.String set_input, - " Sets the input format (default auto)"; - "-o", Arg.String set_output, - " Sets the output format (default none)"; "-s", Arg.String set_solver, - "{smt,mcsat} Sets the solver to use (default smt)"; + "{sat,smt,mcsat} Sets the solver to use (default smt)"; "-size", Arg.String (int_arg size_limit), "[kMGT] Sets the size limit for the sat solver"; "-time", Arg.String (int_arg time_limit), @@ -215,9 +115,6 @@ let check () = else if s > !size_limit then raise Out_of_space -(* Entry file parsing *) -let get_cnf () = parse_input !file - let main () = (* Administrative duties *) Arg.parse argspec input_file usage; @@ -228,6 +125,12 @@ let main () = let al = Gc.create_alarm check in (* Interesting stuff happening *) + let _, _input = P.parse_file !file in + Gc.delete_alarm al; + () + + (* Old code ... + let cnf = get_cnf () in if !p_cnf then print_cnf cnf; @@ -257,7 +160,6 @@ let main () = | Mcsat -> Mcsat.assume cnf; let res = Mcsat.solve () in - Gc.delete_alarm al; begin match res with | Mcsat.Sat sat -> let t = Sys.time () in @@ -275,18 +177,21 @@ let main () = print_mc_unsat_core (Mcsat.unsat_core p) end; print "Unsat (%f/%f)" t (Sys.time () -. t) - end + end + +*) let () = try main () with | Incorrect_model -> - print "Internal error : incorrect *sat* model"; + Format.printf "Internal error : incorrect *sat* model@."; exit 4 | Out_of_time -> - print "Timeout"; + Format.printf "Timeout@."; exit 2 | Out_of_space -> - print "Spaceout"; + Format.printf "Spaceout@."; exit 3 + diff --git a/src/smt/cnf.ml b/src/smt/cnf.ml deleted file mode 100644 index 999271ac..00000000 --- a/src/smt/cnf.ml +++ /dev/null @@ -1,9 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -open Msat - -module S = Tseitin.Make(Expr) diff --git a/src/smt/cnf.mli b/src/smt/cnf.mli deleted file mode 100644 index 6eb68976..00000000 --- a/src/smt/cnf.mli +++ /dev/null @@ -1,9 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -open Msat - -module S : Tseitin.S with type atom = Expr.Formula.t diff --git a/src/smt/expr.ml b/src/smt/expr.ml deleted file mode 100644 index dda3d7fc..00000000 --- a/src/smt/expr.ml +++ /dev/null @@ -1,87 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) -open Msat - -module I = Formula_intf -module Term = Term - -exception Invalid_prop - -type term = Term.t - -(* atomic formula - - Prop: - - sign of int determines sign of formula - - odd numbers --> fresh atoms (for Tseitin CNF) - - even numbers --> used for regular int-mapping -*) -type formula = - | Prop of int - | Equal of term * term - | Distinct of term * term - -type t = formula -type proof = unit - -let dummy = Prop 0 - -let max_fresh = ref 0 - -let fresh () = - incr max_fresh; - Prop (2 * !max_fresh + 1) - -let mk_prop i = - if i <> 0 && i < max_int / 2 then Prop (2 * i) - else raise Invalid_prop - -let order_ t1 t2 = if Term.compare t1 t2 > 0 then t2,t1 else t1,t2 - -let mk_eq a b = - let a, b = order_ a b in - Equal (a, b) - -let mk_neq a b = - let a, b = order_ a b in - Distinct (a, b) - -let mk_true = mk_eq Term.true_ Term.true_ -let mk_false = mk_eq Term.true_ Term.false_ -let mk_atom = mk_eq Term.true_ -let mk_atom_neg = mk_eq Term.false_ - -let neg = function - | Prop i -> Prop (-i) - | Equal (a, b) -> Distinct (a, b) - | Distinct (a, b) -> Equal (a, b) - -let norm = function - | Prop i -> Prop (abs i), if i < 0 then I.Negated else I.Same_sign - | Equal (a, b) -> Equal (a, b), I.Same_sign - | Distinct (a, b) -> Equal (a, b), I.Negated - -(* Only used after normalisation, so usual functions should work *) -let hash = Hashtbl.hash -let equal = (=) -let compare = Pervasives.compare - -let print fmt = function - | Prop i -> - Format.fprintf fmt "%s%s%d" - (if i < 0 then "¬ " else "") - (if i mod 2 = 0 then "v" else "f") ((abs i) / 2) - | Equal (a, b) -> Format.fprintf fmt "(@[=@ %a@ %a@])" Term.print a Term.print b - | Distinct (a, b) -> Format.fprintf fmt "(@[!=@ %a@ %a@])" Term.print a Term.print b - -module Formula = struct - type t = formula - let hash = Hashtbl.hash - let equal = (=) - let compare = Pervasives.compare - let print = print -end - diff --git a/src/smt/expr.mli b/src/smt/expr.mli deleted file mode 100644 index 0f01ae83..00000000 --- a/src/smt/expr.mli +++ /dev/null @@ -1,42 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) -open Msat - -type term = Term.t - -type formula = private - | Prop of int (* prop or tseitin atom *) - | Equal of term * term - | Distinct of term * term - -type t = formula -type proof = unit - -include Formula_intf.S with type t := formula and type proof := proof - -val dummy : t - -val fresh : unit -> t - -val mk_prop : int -> t -(** [mk_prop i] makes a prop literal from [i], whose sign matters. - @raise Invalid_prop if [i=0] or if [i] is too large *) - -val mk_true : t -val mk_false : t -val mk_atom : term -> t -val mk_atom_neg : term -> t -val mk_eq : term -> term -> t -val mk_neq : term -> term -> t - -module Term = Term -module Formula : sig - type t = formula - val hash : t -> int - val equal : t -> t -> bool - val compare : t -> t -> int - val print : Format.formatter -> t -> unit -end diff --git a/src/util/.merlin b/src/util/.merlin deleted file mode 100644 index 962d669c..00000000 --- a/src/util/.merlin +++ /dev/null @@ -1,11 +0,0 @@ -S ./ -S ./smtlib/ -S ../sat/ -S ../common/ - -B ../_build/ -B ../_build/util/ -B ../_build/util/smtlib/ -B ../_build/sat/ -B ../_build/smt/ -B ../_build/common/ diff --git a/src/util/expr.ml b/src/util/expr.ml new file mode 100644 index 00000000..752b55e7 --- /dev/null +++ b/src/util/expr.ml @@ -0,0 +1,522 @@ +(* + Base modules that defines the terms used in the prover. +*) + +(* Type definitions *) +(* ************************************************************************ *) + +(* Private aliases *) +type hash = int +type index = int + +(* Identifiers, parametrized by the kind of the type of the variable *) +type 'ty id = { + id_type : 'ty; + id_name : string; + index : index; (** unique *) +} + +(* Type for first order types *) +type ttype = Type + +(* The type of functions *) +type 'ty function_descr = { + fun_vars : ttype id list; (* prenex forall *) + fun_args : 'ty list; + fun_ret : 'ty; +} + +(* Types *) +type ty_descr = + | TyVar of ttype id (** Bound variables *) + | TyApp of ttype function_descr id * ty list + +and ty = { + ty : ty_descr; + mutable ty_hash : hash; (** lazy hash *) +} + +(* Terms & formulas *) +type term_descr = + | Var of ty id + | App of ty function_descr id * ty list * term list + +and term = { + term : term_descr; + t_type : ty; + mutable t_hash : hash; (* lazy hash *) +} + +type atom_descr = + | Pred of term + | Equal of term * term + +and atom = { + sign : bool; + atom : atom_descr; + mutable f_hash : hash; (* lazy hash *) +} + +(* Utilities *) +(* ************************************************************************ *) + +let rec list_cmp ord l1 l2 = + match l1, l2 with + | [], [] -> 0 + | [], _ -> -1 + | _, [] -> 1 + | x1::l1', x2::l2' -> + let c = ord x1 x2 in + if c = 0 + then list_cmp ord l1' l2' + else c + +(* Exceptions *) +(* ************************************************************************ *) + +exception Type_mismatch of term * ty * ty +exception Bad_arity of ty function_descr id * ty list * term list +exception Bad_ty_arity of ttype function_descr id * ty list + +(* Printing functions *) +(* ************************************************************************ *) + +module Print = struct + let rec list f sep fmt = function + | [] -> () + | [x] -> f fmt x + | x :: ((y :: _) as r) -> + Format.fprintf fmt "%a%s" f x sep; + list f sep fmt r + + let id fmt v = Format.fprintf fmt "%s" v.id_name + let ttype fmt = function Type -> Format.fprintf fmt "Type" + + let rec ty fmt t = match t.ty with + | TyVar v -> id fmt v + | TyApp (f, []) -> + Format.fprintf fmt "%a" id f + | TyApp (f, l) -> + Format.fprintf fmt "%a(%a)" id f (list ty ", ") l + + let params fmt = function + | [] -> () + | l -> Format.fprintf fmt "∀ %a. " (list id ", ") l + + let signature print fmt f = + match f.fun_args with + | [] -> Format.fprintf fmt "%a%a" params f.fun_vars print f.fun_ret + | l -> Format.fprintf fmt "%a%a -> %a" params f.fun_vars + (list print " -> ") l print f.fun_ret + + let fun_ty = signature ty + let fun_ttype = signature ttype + + let id_type print fmt v = Format.fprintf fmt "%a : %a" id v print v.id_type + + let id_ty = id_type ty + let id_ttype = id_type ttype + let const_ty = id_type fun_ty + let const_ttype = id_type fun_ttype + + let rec term fmt t = match t.term with + | Var v -> id fmt v + | App (f, [], []) -> + Format.fprintf fmt "%a" id f + | App (f, [], args) -> + Format.fprintf fmt "%a(%a)" id f + (list term ", ") args + | App (f, tys, args) -> + Format.fprintf fmt "%a(%a; %a)" id f + (list ty ", ") tys + (list term ", ") args + + let atom_aux fmt f = + match f.atom with + | Equal (a, b) -> Format.fprintf fmt "%a = %a" term a term b + | Pred t -> Format.fprintf fmt "%a" term t + + let atom fmt f = Format.fprintf fmt "⟦%a⟧" atom_aux f + +end + +(* Substitutions *) +(* ************************************************************************ *) + +module Subst = struct + module Mi = Map.Make(struct + type t = int * int + let compare (a, b) (c, d) = match compare a c with 0 -> compare b d | x -> x + end) + + type ('a, 'b) t = ('a * 'b) Mi.t + + (* Usual functions *) + let empty = Mi.empty + + let is_empty = Mi.is_empty + + let iter f = Mi.iter (fun _ (key, value) -> f key value) + + let fold f = Mi.fold (fun _ (key, value) acc -> f key value acc) + + let bindings s = Mi.fold (fun _ (key, value) acc -> (key, value) :: acc) s [] + + (* Comparisons *) + let equal f = Mi.equal (fun (_, value1) (_, value2) -> f value1 value2) + let compare f = Mi.compare (fun (_, value1) (_, value2) -> f value1 value2) + let hash h s = Mi.fold (fun i (_, value) acc -> Hashtbl.hash (acc, i, h value)) s 1 + + let choose m = snd (Mi.choose m) + + (* Iterators *) + let exists pred s = + try + iter (fun m s -> if pred m s then raise Exit) s; + false + with Exit -> + true + + let for_all pred s = + try + iter (fun m s -> if not (pred m s) then raise Exit) s; + true + with Exit -> + false + + let print print_key print_value fmt map = + let aux _ (key, value) = + Format.fprintf fmt "%a -> %a@ " print_key key print_value value + in + Format.fprintf fmt "@[%a@]" (fun _ -> Mi.iter aux) map + + module type S = sig + type 'a key + val get : 'a key -> ('a key, 'b) t -> 'b + val mem : 'a key -> ('a key, 'b) t -> bool + val bind : 'a key -> 'b -> ('a key, 'b) t -> ('a key, 'b) t + val remove : 'a key -> ('a key, 'b) t -> ('a key, 'b) t + end + + (* Variable substitutions *) + module Id = struct + type 'a key = 'a id + let tok v = (v.index, 0) + let get v s = snd (Mi.find (tok v) s) + let mem v s = Mi.mem (tok v) s + let bind v t s = Mi.add (tok v) (v, t) s + let remove v s = Mi.remove (tok v) s + end + +end + +(* Dummies *) +(* ************************************************************************ *) + +module Dummy = struct + + let id_ttype = + { index = -1; id_name = ""; id_type = Type; } + + let ty = + { ty = TyVar id_ttype; ty_hash = -1; } + + let id = + { index = -2; id_name = ""; id_type = ty; } + + let term = + { term = Var id; t_type = ty; t_hash = -1; } + + let atom = + { atom = Pred term; sign = true; f_hash = -1; } + +end + +(* Variables *) +(* ************************************************************************ *) + +module Id = struct + type 'a t = 'a id + + (* Hash & comparisons *) + let hash v = v.index + + let compare: 'a. 'a id -> 'a id -> int = + fun v1 v2 -> compare v1.index v2.index + + let equal v1 v2 = compare v1 v2 = 0 + + (* Printing functions *) + let print = Print.id + + (* Id count *) + let _count = ref 0 + + (* Constructors *) + let mk_new id_name id_type = + incr _count; + let index = !_count in + { index; id_name; id_type } + + let ttype name = mk_new name Type + let ty name ty = mk_new name ty + + let const name fun_vars fun_args fun_ret = + mk_new name { fun_vars; fun_args; fun_ret; } + + let ty_fun name n = + let rec replicate acc n = + if n <= 0 then acc + else replicate (Type :: acc) (n - 1) + in + const name [] (replicate [] n) Type + + let term_fun = const + + (* Builtin Types *) + let prop = ty_fun "Prop" 0 + let base = ty_fun "$i" 0 + +end + +(* Types *) +(* ************************************************************************ *) + +module Ty = struct + type t = ty + type subst = (ttype id, ty) Subst.t + + (* Hash & Comparisons *) + let rec hash_aux t = match t.ty with + | TyVar v -> Id.hash v + | TyApp (f, args) -> + Hashtbl.hash (Id.hash f, List.map hash args) + + and hash t = + if t.ty_hash = -1 then + t.ty_hash <- hash_aux t; + t.ty_hash + + let discr ty = match ty.ty with + | TyVar _ -> 1 + | TyApp _ -> 2 + + let rec compare u v = + let hu = hash u and hv = hash v in + if hu <> hv then Pervasives.compare hu hv + else match u.ty, v.ty with + | TyVar v1, TyVar v2 -> Id.compare v1 v2 + | TyApp (f1, args1), TyApp (f2, args2) -> + begin match Id.compare f1 f2 with + | 0 -> list_cmp compare args1 args2 + | x -> x + end + | _, _ -> Pervasives.compare (discr u) (discr v) + + let equal u v = + u == v || (hash u = hash v && compare u v = 0) + + (* Printing functions *) + let print = Print.ty + + (* Constructors *) + let mk_ty ty = { ty; ty_hash = -1; } + + let of_id v = mk_ty (TyVar v) + + let apply f args = + assert (f.id_type.fun_vars = []); + if List.length args <> List.length f.id_type.fun_args then + raise (Bad_ty_arity (f, args)) + else + mk_ty (TyApp (f, args)) + + (* Builtin types *) + let prop = apply Id.prop [] + let base = apply Id.base [] + + (* Substitutions *) + let rec subst_aux map t = match t.ty with + | TyVar v -> begin try Subst.Id.get v map with Not_found -> t end + | TyApp (f, args) -> + let new_args = List.map (subst_aux map) args in + if List.for_all2 (==) args new_args then t + else apply f new_args + + let subst map t = if Subst.is_empty map then t else subst_aux map t + + (* Typechecking *) + let instantiate f tys args = + if List.length f.id_type.fun_vars <> List.length tys || + List.length f.id_type.fun_args <> List.length args then + raise (Bad_arity (f, tys, args)) + else + let map = List.fold_left2 (fun acc v ty -> Subst.Id.bind v ty acc) Subst.empty f.id_type.fun_vars tys in + let fun_args = List.map (subst map) f.id_type.fun_args in + List.iter2 (fun t ty -> + if not (equal t.t_type ty) then raise (Type_mismatch (t, t.t_type, ty))) + args fun_args; + subst map f.id_type.fun_ret + +end + +(* Terms *) +(* ************************************************************************ *) + +module Term = struct + type t = term + type subst = (ty id, term) Subst.t + + (* Hash & Comparisons *) + let rec hash_aux t = match t.term with + | Var v -> Id.hash v + | App (f, tys, args) -> + let l = List.map Ty.hash tys in + let l' = List.map hash args in + Hashtbl.hash (Id.hash f, l, l') + + and hash t = + if t.t_hash = -1 then + t.t_hash <- hash_aux t; + t.t_hash + + let discr t = match t.term with + | Var _ -> 1 + | App _ -> 2 + + let rec compare u v = + let hu = hash u and hv = hash v in + if hu <> hv then Pervasives.compare hu hv + else match u.term, v.term with + | Var v1, Var v2 -> Id.compare v1 v2 + | App (f1, tys1, args1), App (f2, tys2, args2) -> + begin match Id.compare f1 f2 with + | 0 -> + begin match list_cmp Ty.compare tys1 tys2 with + | 0 -> list_cmp compare args1 args2 + | x -> x + end + | x -> x + end + | _, _ -> Pervasives.compare (discr u) (discr v) + + let equal u v = + u == v || (hash u = hash v && compare u v = 0) + + (* Printing functions *) + let print = Print.term + + (* Constructors *) + let mk_term term t_type = + { term; t_type; t_hash = -1; } + + let of_id v = + mk_term (Var v) v.id_type + + let apply f ty_args t_args = + mk_term (App (f, ty_args, t_args)) (Ty.instantiate f ty_args t_args) + + (* Substitutions *) + let rec subst_aux ty_map t_map t = match t.term with + | Var v -> begin try Subst.Id.get v t_map with Not_found -> t end + | App (f, tys, args) -> + let new_tys = List.map (Ty.subst ty_map) tys in + let new_args = List.map (subst_aux ty_map t_map) args in + if List.for_all2 (==) new_tys tys && List.for_all2 (==) new_args args then t + else apply f new_tys new_args + + let subst ty_map t_map t = + if Subst.is_empty ty_map && Subst.is_empty t_map then + t + else + subst_aux ty_map t_map t + + let rec replace (t, t') t'' = match t''.term with + | _ when equal t t'' -> t' + | App (f, ty_args, t_args) -> + apply f ty_args (List.map (replace (t, t')) t_args) + | _ -> t'' + +end + +(* Formulas *) +(* ************************************************************************ *) + +module Atom = struct + type t = atom + + type proof = unit + + (* Hash & Comparisons *) + let h_eq = 2 + let h_pred = 3 + + let rec hash_aux f = match f.atom with + | Equal (t1, t2) -> + Hashtbl.hash (h_eq, Term.hash t1, Term.hash t2) + | Pred t -> + Hashtbl.hash (h_pred, Term.hash t) + + and hash f = + if f.f_hash = -1 then + f.f_hash <- hash_aux f; + f.f_hash + + let discr f = match f.atom with + | Equal _ -> 1 + | Pred _ -> 2 + + let compare f g = + let hf = hash f and hg = hash g in + if hf <> hg then Pervasives.compare hf hg + else match f.atom, g.atom with + | Equal (u1, v1), Equal(u2, v2) -> + list_cmp Term.compare [u1; v1] [u2; v2] + | Pred t1, Pred t2 -> Term.compare t1 t2 + | _, _ -> Pervasives.compare (discr f) (discr g) + + let equal u v = + u == v || (hash u = hash v && compare u v = 0) + + (* Printing functions *) + let print = Print.atom + + (* Constructors *) + let mk_formula f = { + sign = true; + atom = f; + f_hash = -1; + } + + let dummy = Dummy.atom + + let pred t = + if not (Ty.equal Ty.prop t.t_type) then + raise (Type_mismatch (t, t.t_type, Ty.prop)) + else + mk_formula (Pred t) + + let fresh () = + let id = Id.ty "fresh" Ty.prop in + pred (Term.of_id id) + + let neg f = + { f with sign = not f.sign } + + let eq a b = + if not (Ty.equal a.t_type b.t_type) then + raise (Type_mismatch (b, b.t_type, a.t_type)) + else if Term.compare a b < 0 then + mk_formula (Equal (a, b)) + else + mk_formula (Equal (b, a)) + + let norm f = + { f with sign = true }, + if f.sign then Msat.Formula_intf.Same_sign + else Msat.Formula_intf.Negated + +end + +module Formula = Msat.Tseitin.Make(Atom) + diff --git a/src/util/expr.mli b/src/util/expr.mli new file mode 100644 index 00000000..1f819b2c --- /dev/null +++ b/src/util/expr.mli @@ -0,0 +1,319 @@ + +(** Expressions for TabSat *) + +(** {2 Type definitions} *) + +(** These are custom types used in functions later. *) + +(** {3 Identifiers} *) + +(** Identifiers are the basic building blocks used to build types terms and expressions. *) + +type hash +type index = private int + +(** Private aliases to provide access. You should not have any need + to use these, instead use the functions provided by this module. *) + +type 'ty id = private { + id_type : 'ty; + id_name : string; + index : index; (** unique *) +} + +(** The type of identifiers. An ['a id] is an identifier whose solver-type + is represented by an inhabitant of type ['a]. + All identifier have an unique [index] which is used for comparison, + so that the name of a variable is only there for tracability + and/or pretty-printing. *) + +(** {3 Types} *) + +type ttype = Type + +(** The caml type of solver-types. *) + +type 'ty function_descr = private { + fun_vars : ttype id list; (* prenex forall *) + fun_args : 'ty list; + fun_ret : 'ty; +} + +(** This represents the solver-type of a function. + Functions can be polymorphic in the variables described in the + [fun_vars] field. *) + +type ty_descr = private + | TyVar of ttype id + (** bound variables (i.e should only appear under a quantifier) *) + | TyApp of ttype function_descr id * ty list + (** application of a constant to some arguments *) + +and ty = private { + ty : ty_descr; + mutable ty_hash : hash; (** Use Ty.hash instead *) +} + +(** These types defines solver-types, i.e the representation of the types + of terms in the solver. Record definition for [type ty] is shown in order + to be able to use the [ty.ty] field in patter matches. Other fields shoud not + be accessed directly, but throught the functions provided by the [Ty] module. *) + +(** {3 Terms} *) + +type term_descr = private + | Var of ty id + (** bound variables (i.e should only appear under a quantifier) *) + | App of ty function_descr id * ty list * term list + (** application of a constant to some arguments *) + +and term = private { + term : term_descr; + t_type : ty; + mutable t_hash : hash; (** Do not use this filed, call Term.hash instead *) +} + +(** Types defining terms in the solver. The definition is vary similar to that + of solver-types, except for type arguments of polymorphic functions which + are explicit. This has the advantage that there is a clear and typed distinction + between solver-types and terms, but may lead to some duplication of code + in some places. *) + +(** {3 Formulas} *) + +type atom_descr = private + (** Atoms *) + | Pred of term + | Equal of term * term + +and atom = private { + sign : bool; + atom : atom_descr; + mutable f_hash : hash; (** Use Formula.hash instead *) +} + +(** The type of atoms in the solver. The list of free arguments in quantifiers + is a bit tricky, so you should not touch it (see full doc for further + explanations). *) + +(** {3 Exceptions} *) + +exception Type_mismatch of term * ty * ty +(* Raised when as Type_mismatch(term, actual_type, expected_type) *) + +exception Bad_arity of ty function_descr id * ty list * term list +exception Bad_ty_arity of ttype function_descr id * ty list +(** Raised when trying to build an application with wrong arity *) + +(** {2 Printing} *) + +module Print : sig + (** Pretty printing functions *) + + val id : Format.formatter -> 'a id -> unit + val id_ty : Format.formatter -> ty id -> unit + val id_ttype : Format.formatter -> ttype id -> unit + + val const_ty : Format.formatter -> ty function_descr id -> unit + val const_ttype : Format.formatter -> ttype function_descr id -> unit + + val ty : Format.formatter -> ty -> unit + val fun_ty : Format.formatter -> ty function_descr -> unit + + val ttype : Format.formatter -> ttype -> unit + val fun_ttype : Format.formatter -> ttype function_descr -> unit + + val term : Format.formatter -> term -> unit + val atom : Format.formatter -> atom -> unit +end + +(** {2 Identifiers & Metas} *) + +module Id : sig + type 'a t = 'a id + (* Type alias *) + + val hash : 'a t -> int + val equal : 'a t -> 'a t -> bool + val compare : 'a t -> 'a t -> int + (** Usual functions for hash/comparison *) + + val print : Format.formatter -> 'a t -> unit + (** Printing for variables *) + + val prop : ttype function_descr id + val base : ttype function_descr id + (** Constants representing the type for propositions and a default type + for term, respectively. *) + + val ttype : string -> ttype id + (** Create a fresh type variable with the given name. *) + + val ty : string -> ty -> ty id + (** Create a fresh variable with given name and type *) + + val ty_fun : string -> int -> ttype function_descr id + (** Create a fresh type constructor with given name and arity *) + + val term_fun : string -> ttype id list -> ty list -> ty -> ty function_descr id + (** [ty_fun name type_vars arg_types return_type] returns a fresh constant symbol, + possibly polymorphic with respect to the variables in [type_vars] (which may appear in the + types in [arg_types] and in [return_type]). *) + +end + +(** {2 Substitutions} *) + +module Subst : sig + (** Module to handle substitutions *) + + type ('a, 'b) t + (** The type of substitutions from values of type ['a] to values of type ['b]. *) + + val empty : ('a, 'b) t + (** The empty substitution *) + + val is_empty : ('a, 'b) t -> bool + (** Test wether a substitution is empty *) + + val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit + (** Iterates over the bindings of the substitution. *) + + val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c + (** Fold over the elements *) + + val bindings : ('a, 'b) t -> ('a * 'b) list + (** Returns the list of bindings ofa substitution. *) + + val exists : ('a -> 'b -> bool) -> ('a, 'b) t -> bool + (** Tests wether the predicate holds for at least one binding. *) + + val for_all : ('a -> 'b -> bool) -> ('a, 'b) t -> bool + (** Tests wether the predicate holds for all bindings. *) + + val hash : ('b -> int) -> ('a, 'b) t -> int + val compare : ('b -> 'b -> int) -> ('a, 'b) t -> ('a, 'b) t -> int + val equal : ('b -> 'b -> bool) -> ('a, 'b) t -> ('a, 'b) t -> bool + (** Comparison and hash functions, with a comparison/hash function on values as parameter *) + + val print : + (Format.formatter -> 'a -> unit) -> + (Format.formatter -> 'b -> unit) -> + Format.formatter -> ('a, 'b) t -> unit + (** Prints the substitution, using the given functions to print keys and values. *) + + val choose : ('a, 'b) t -> 'a * 'b + (** Return one binding of the given substitution, or raise Not_found if the substitution is empty.*) + + (** {5 Concrete subtitutions } *) + module type S = sig + type 'a key + val get : 'a key -> ('a key, 'b) t -> 'b + (** [get v subst] returns the value associated with [v] in [subst], if it exists. + @raise Not_found if there is no binding for [v]. *) + val mem : 'a key -> ('a key, 'b) t -> bool + (** [get v subst] returns wether there is a value associated with [v] in [subst]. *) + val bind : 'a key -> 'b -> ('a key, 'b) t -> ('a key, 'b) t + (** [bind v t subst] returns the same substitution as [subst] with the additional binding from [v] to [t]. + Erases the previous binding of [v] if it exists. *) + val remove : 'a key -> ('a key, 'b) t -> ('a key, 'b) t + (** [remove v subst] returns the same substitution as [subst] except for [v] which is unbound in the returned substitution. *) + end + + module Id : S with type 'a key = 'a id +end + +(** {2 Types} *) + +module Ty : sig + type t = ty + (** Type alias *) + + type subst = (ttype id, ty) Subst.t + (** The type of substitutions over types. *) + + val hash : t -> int + val equal : t -> t -> bool + val compare : t -> t -> int + (** Usual hash/compare functions *) + + val print : Format.formatter -> t -> unit + + val prop : ty + val base : ty + (** The type of propositions and individuals *) + + val of_id : ttype id -> ty + (** Creates a type from a variable *) + + val apply : ttype function_descr id -> ty list -> ty + (** Applies a constant to a list of types *) + + val subst : subst -> ty -> ty + (** Substitution over types. *) + +end + +(** {2 Terms} *) + +module Term : sig + type t = term + (** Type alias *) + + type subst = (ty id, term) Subst.t + (** The type of substitutions in types. *) + + val hash : t -> int + val equal : t -> t -> bool + val compare : t -> t -> int + (** Usual hash/compare functions *) + + val print : Format.formatter -> t -> unit + (** Printing functions *) + + val of_id : ty id -> term + (** Create a term from a variable *) + + val apply : ty function_descr id -> ty list -> term list -> term + (** Applies a constant function to type arguments, then term arguments *) + + val subst : Ty.subst -> subst -> term -> term + (** Substitution over types. *) + + val replace : term * term -> term -> term + (** [replace (t, t') t''] returns the term [t''] where every occurence of [t] + has been replace by [t']. *) + +end + +(** {2 Formulas} *) + +module Atom : sig + type t = atom + (** Type alias *) + + val hash : t -> int + val equal : t -> t -> bool + val compare : t -> t -> int + (** Usual hash/compare functions *) + + val print : Format.formatter -> t -> unit + (** Printing functions *) + + val eq : term -> term -> atom + (** Create an equality over two terms. The two given terms + must have the same type [t], which must be different from {!Ty.prop} *) + + val pred : term -> atom + (** Create a atom from a term. The given term must have type {!Ty.prop} *) + + val neg : atom -> atom + (** Returns the negation of the given atom *) + + val norm : atom -> atom * Msat.Formula_intf.negated + (** Normalization functions as required by msat. *) + +end + +module Formula : Msat.Tseitin.S with type atom = atom + diff --git a/src/util/parsedimacs.ml b/src/util/parsedimacs.ml deleted file mode 100644 index df5c3c8c..00000000 --- a/src/util/parsedimacs.ml +++ /dev/null @@ -1,75 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -exception Syntax_error of int - -type line = - | Empty - | Comment - | Pcnf of int * int - | Clause of int list - -let rec _read_word s acc i len = - assert (len>0); - if i+len=String.length s - then String.sub s i len :: acc - else match s.[i+len] with - | ' ' | '\t' -> - let acc = String.sub s i len :: acc in - _skip_space s acc (i+len+1) - | _ -> _read_word s acc i (len+1) - -and _skip_space s acc i = - if i=String.length s - then acc - else match s.[i] with - | ' ' | '\t' -> _skip_space s acc (i+1) - | _ -> _read_word s acc i 1 - -let ssplit s = List.rev (_skip_space s [] 0) - -let of_input f = - match ssplit (input_line f) with - | [] -> Empty - | "c" :: _ -> Comment - | "p" :: "cnf" :: i :: j :: [] -> - begin try - Pcnf (int_of_string i, int_of_string j) - with Failure _ -> - raise (Syntax_error (-1)) - end - | l -> - begin try - begin match List.rev_map int_of_string l with - | 0 :: r -> Clause r - | _ -> raise (Syntax_error (-1)) - end - with Failure _ -> raise (Syntax_error (-1)) - end - -let parse_with todo file = - let f = open_in file in - let line = ref 0 in - try - while true do - incr line; - todo (of_input f) - done - with - | Syntax_error _ -> - raise (Syntax_error !line) - | End_of_file -> - close_in f - -let cnf = ref [] -let parse_line = function - | Empty | Comment | Pcnf _ -> () - | Clause l -> cnf := l :: !cnf - -let parse f = - cnf := []; - parse_with parse_line f; - !cnf diff --git a/src/util/parsedimacs.mli b/src/util/parsedimacs.mli deleted file mode 100644 index 84a7b222..00000000 --- a/src/util/parsedimacs.mli +++ /dev/null @@ -1,9 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -exception Syntax_error of int - -val parse : string -> int list list diff --git a/src/util/smtlib/.merlin b/src/util/smtlib/.merlin deleted file mode 100644 index 23ddf6ef..00000000 --- a/src/util/smtlib/.merlin +++ /dev/null @@ -1,9 +0,0 @@ -S ./ -S ../ -S ../../sat/ - -B ../../_build/ -B ../../_build/util/ -B ../../_build/util/smtlib/ -B ../../_build/sat/ -B ../../_build/smt/ diff --git a/src/util/smtlib/lexsmtlib.mli b/src/util/smtlib/lexsmtlib.mli deleted file mode 100644 index a53450a7..00000000 --- a/src/util/smtlib/lexsmtlib.mli +++ /dev/null @@ -1,3 +0,0 @@ -(* Copyright 2014 INIA *) - -val token : Lexing.lexbuf -> Parsesmtlib.token diff --git a/src/util/smtlib/lexsmtlib.mll b/src/util/smtlib/lexsmtlib.mll deleted file mode 100644 index b192c3f3..00000000 --- a/src/util/smtlib/lexsmtlib.mll +++ /dev/null @@ -1,48 +0,0 @@ -{ - (* auto-generated by gt *) - -open Parsesmtlib;; -} - -rule token = parse -| ['\t' ' ' ]+ { token lexbuf } -| ';' (_ # '\n')* { token lexbuf } -| ['\n']+ as str { Smtlib_util.line := (!Smtlib_util.line + (String.length str)); token lexbuf } -| "_" { UNDERSCORE } -| "(" { LPAREN } -| ")" { RPAREN } -| "as" { AS } -| "let" { LET } -| "forall" { FORALL } -| "exists" { EXISTS } -| "!" { EXCLIMATIONPT } -| "set-logic" { SETLOGIC } -| "set-option" { SETOPTION } -| "set-info" { SETINFO } -| "declare-sort" { DECLARESORT } -| "define-sort" { DEFINESORT } -| "declare-fun" { DECLAREFUN } -| "define-fun" { DEFINEFUN } -| "push" { PUSH } -| "pop" { POP } -| "assert" { ASSERT } -| "check-sat" { CHECKSAT } -| "get-assertions" { GETASSERT } -| "get-proof" { GETPROOF } -| "get-unsat-core" { GETUNSATCORE } -| "get-value" { GETVALUE } -| "get-assignment" { GETASSIGN } -| "get-option" { GETOPTION } -| "get-info" { GETINFO } -| "exit" { EXIT } -| '#' 'x' ['0'-'9' 'A'-'F' 'a'-'f']+ as str { HEXADECIMAL(str) } -| '#' 'b' ['0'-'1']+ as str { BINARY(str) } -| '|' ([ '!'-'~' ' ' '\n' '\t' '\r'] # ['\\' '|'])* '|' as str { ASCIIWOR(str) } -| ':' ['a'-'z' 'A'-'Z' '0'-'9' '+' '-' '/' '*' '=' '%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@']+ as str { KEYWORD(str) } -| ['a'-'z' 'A'-'Z' '+' '-' '/' '*' '=''%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@'] ['a'-'z' 'A'-'Z' '0'-'9' '+' '-' '/' '*' '=''%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@']* as str { SYMBOL(str) } -| '"' (([ '!'-'~' ' ' '\n' '\t' '\r' ] # ['\\' '"']) | ('\\' ['!'-'~' ' ' '\n' '\t' '\r'] ))* '"' as str { STRINGLIT(str) } -| ( '0' | ['1'-'9'] ['0'-'9']* ) as str { NUMERAL(str) } -| ( '0' | ['1'-'9'] ['0'-'9']* ) '.' ['0'-'9']+ as str { DECIMAL(str) } -| eof { EOF } -| _ {failwith((Lexing.lexeme lexbuf) ^ - ": lexing error on line "^(string_of_int !Smtlib_util.line))}{} diff --git a/src/util/smtlib/parsesmtlib.mly b/src/util/smtlib/parsesmtlib.mly deleted file mode 100644 index 65a14660..00000000 --- a/src/util/smtlib/parsesmtlib.mly +++ /dev/null @@ -1,330 +0,0 @@ -%{ - (* auto-generated by gt *) - -open Smtlib_syntax;; -let parse_error s = - print_string s; - print_string " on line "; - print_int !Smtlib_util.line; - print_string "\n";; - -%} - -%start main - -%token EOF AS ASSERT CHECKSAT DECLAREFUN DECLARESORT DEFINEFUN DEFINESORT EXCLIMATIONPT EXISTS EXIT FORALL GETASSERT GETASSIGN GETINFO GETOPTION GETPROOF GETUNSATCORE GETVALUE LET LPAREN POP PUSH RPAREN SETINFO SETLOGIC SETOPTION UNDERSCORE -%token ASCIIWOR BINARY DECIMAL HEXADECIMAL KEYWORD NUMERAL STRINGLIT SYMBOL - - %type main - - %type an_option - - %type attribute - - %type attributevalsexpr_attributevalue_sexpr5 - - %type attributevalue - - %type command - - %type commanddeclarefun_command_sort13 - - %type commanddefinefun_command_sortedvar15 - - %type commanddefinesort_command_symbol11 - - %type commandgetvalue_command_term24 - - %type commands - - %type commands_commands_command30 - - %type identifier - - %type idunderscoresymnum_identifier_numeral33 - - %type infoflag - - %type qualidentifier - - %type sexpr - - %type sexprinparen_sexpr_sexpr41 - - %type sort - - %type sortedvar - - %type sortidsortmulti_sort_sort44 - - %type specconstant - - %type symbol - - %type term - - %type termexclimationpt_term_attribute64 - - %type termexiststerm_term_sortedvar62 - - %type termforallterm_term_sortedvar60 - - %type termletterm_term_varbinding58 - - %type termqualidterm_term_term56 - - %type varbinding - - %type cur_position - - %% - - main: - | commands { Some($1) } - | EOF { None } - - cur_position: - | { Smtlib_util.cur_pd() } - - an_option: - | attribute { AnOptionAttribute(pd_attribute $1, $1) } - - attribute: - | cur_position KEYWORD { AttributeKeyword($1, $2) } - - attribute: - | cur_position KEYWORD attributevalue { AttributeKeywordValue($1, $2, $3) } - - attributevalue: - | specconstant { AttributeValSpecConst(pd_specconstant $1, $1) } - - attributevalue: - | symbol { AttributeValSymbol(pd_symbol $1, $1) } - - attributevalue: - | cur_position LPAREN attributevalsexpr_attributevalue_sexpr5 RPAREN { AttributeValSexpr($1, $3) } - - command: - | cur_position LPAREN SETLOGIC symbol RPAREN { CommandSetLogic($1, $4) } - - command: - | cur_position LPAREN SETOPTION an_option RPAREN { CommandSetOption($1, $4) } - - command: - | cur_position LPAREN SETINFO attribute RPAREN { CommandSetInfo($1, $4) } - - command: - | cur_position LPAREN DECLARESORT symbol NUMERAL RPAREN { CommandDeclareSort($1, $4, $5) } - - command: - | cur_position LPAREN DEFINESORT symbol LPAREN commanddefinesort_command_symbol11 RPAREN sort RPAREN { CommandDefineSort($1, $4, $6, $8) } - - command: - | cur_position LPAREN DECLAREFUN symbol LPAREN commanddeclarefun_command_sort13 RPAREN sort RPAREN { CommandDeclareFun($1, $4, $6, $8) } - - command: - | cur_position LPAREN DEFINEFUN symbol LPAREN commanddefinefun_command_sortedvar15 RPAREN sort term RPAREN { CommandDefineFun($1, $4, $6, $8, $9) } - - command: - | cur_position LPAREN PUSH NUMERAL RPAREN { CommandPush($1, $4) } - - command: - | cur_position LPAREN POP NUMERAL RPAREN { CommandPop($1, $4) } - - command: - | cur_position LPAREN ASSERT term RPAREN { CommandAssert($1, $4) } - - command: - | cur_position LPAREN CHECKSAT RPAREN { CommandCheckSat($1) } - - command: - | cur_position LPAREN GETASSERT RPAREN { CommandGetAssert($1) } - - command: - | cur_position LPAREN GETPROOF RPAREN { CommandGetProof($1) } - - command: - | cur_position LPAREN GETUNSATCORE RPAREN { CommandGetUnsatCore($1) } - - command: - | cur_position LPAREN GETVALUE LPAREN commandgetvalue_command_term24 RPAREN RPAREN { CommandGetValue($1, $5) } - - command: - | cur_position LPAREN GETASSIGN RPAREN { CommandGetAssign($1) } - - command: - | cur_position LPAREN GETOPTION KEYWORD RPAREN { CommandGetOption($1, $4) } - - command: - | cur_position LPAREN GETINFO infoflag RPAREN { CommandGetInfo($1, $4) } - - command: - | cur_position LPAREN EXIT RPAREN { CommandExit($1) } - - commands: - | commands_commands_command30 { Commands(pd_commands_commands_command30 $1, $1) } - - identifier: - | symbol { IdSymbol(pd_symbol $1, $1) } - - identifier: - | cur_position LPAREN UNDERSCORE symbol idunderscoresymnum_identifier_numeral33 RPAREN { IdUnderscoreSymNum($1, $4, $5) } - - infoflag: - | cur_position KEYWORD { InfoFlagKeyword($1, $2) } - - qualidentifier: - | identifier { QualIdentifierId(pd_identifier $1, $1) } - - qualidentifier: - | cur_position LPAREN AS identifier sort RPAREN { QualIdentifierAs($1, $4, $5) } - - sexpr: - | specconstant { SexprSpecConst(pd_specconstant $1, $1) } - - sexpr: - | symbol { SexprSymbol(pd_symbol $1, $1) } - - sexpr: - | cur_position KEYWORD { SexprKeyword($1, $2) } - - sexpr: - | cur_position LPAREN sexprinparen_sexpr_sexpr41 RPAREN { SexprInParen($1, $3) } - - sort: - | identifier { SortIdentifier(pd_identifier $1, $1) } - - sort: - | cur_position LPAREN identifier sortidsortmulti_sort_sort44 RPAREN { SortIdSortMulti($1, $3, $4) } - - sortedvar: - | cur_position LPAREN symbol sort RPAREN { SortedVarSymSort($1, $3, $4) } - - specconstant: - | cur_position DECIMAL { SpecConstsDec($1, $2) } - - specconstant: - | cur_position NUMERAL { SpecConstNum($1, $2) } - - specconstant: - | cur_position STRINGLIT { SpecConstString($1, $2) } - - specconstant: - | cur_position HEXADECIMAL { SpecConstsHex($1, $2) } - - specconstant: - | cur_position BINARY { SpecConstsBinary($1, $2) } - - symbol: - | cur_position SYMBOL { Symbol($1, $2) } - - symbol: - | cur_position ASCIIWOR { SymbolWithOr($1, $2) } - - term: - | specconstant { TermSpecConst(pd_specconstant $1, $1) } - - term: - | qualidentifier { TermQualIdentifier(pd_qualidentifier $1, $1) } - - term: - | cur_position LPAREN qualidentifier termqualidterm_term_term56 RPAREN { TermQualIdTerm($1, $3, $4) } - - term: - | cur_position LPAREN LET LPAREN termletterm_term_varbinding58 RPAREN term RPAREN { TermLetTerm($1, $5, $7) } - - term: - | cur_position LPAREN FORALL LPAREN termforallterm_term_sortedvar60 RPAREN term RPAREN { TermForAllTerm($1, $5, $7) } - - term: - | cur_position LPAREN EXISTS LPAREN termexiststerm_term_sortedvar62 RPAREN term RPAREN { TermExistsTerm($1, $5, $7) } - - term: - | cur_position LPAREN EXCLIMATIONPT term termexclimationpt_term_attribute64 RPAREN { TermExclimationPt($1, $4, $5) } - - varbinding: - | cur_position LPAREN symbol term RPAREN { VarBindingSymTerm($1, $3, $4) } - - termexclimationpt_term_attribute64: - | attribute { (pd_attribute $1, ($1)::[]) } - - termexclimationpt_term_attribute64: - | attribute termexclimationpt_term_attribute64 { let (p, ( l1 )) = $2 in (pd_attribute $1, ($1)::(l1)) } - - termexiststerm_term_sortedvar62: - | sortedvar { (pd_sortedvar $1, ($1)::[]) } - - termexiststerm_term_sortedvar62: - | sortedvar termexiststerm_term_sortedvar62 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) } - - termforallterm_term_sortedvar60: - | sortedvar { (pd_sortedvar $1, ($1)::[]) } - - termforallterm_term_sortedvar60: - | sortedvar termforallterm_term_sortedvar60 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) } - - termletterm_term_varbinding58: - | varbinding { (pd_varbinding $1, ($1)::[]) } - - termletterm_term_varbinding58: - | varbinding termletterm_term_varbinding58 { let (p, ( l1 )) = $2 in (pd_varbinding $1, ($1)::(l1)) } - - termqualidterm_term_term56: - | term { (pd_term $1, ($1)::[]) } - - termqualidterm_term_term56: - | term termqualidterm_term_term56 { let (p, ( l1 )) = $2 in (pd_term $1, ($1)::(l1)) } - - sortidsortmulti_sort_sort44: - | sort { (pd_sort $1, ($1)::[]) } - - sortidsortmulti_sort_sort44: - | sort sortidsortmulti_sort_sort44 { let (p, ( l1 )) = $2 in (pd_sort $1, ($1)::(l1)) } - - sexprinparen_sexpr_sexpr41: - | cur_position { ($1, []) } - - sexprinparen_sexpr_sexpr41: - | sexpr sexprinparen_sexpr_sexpr41 { let (p, ( l1 )) = $2 in (pd_sexpr $1, ($1)::(l1)) } - - idunderscoresymnum_identifier_numeral33: - | cur_position NUMERAL { ($1, ($2)::[]) } - - idunderscoresymnum_identifier_numeral33: - | cur_position NUMERAL idunderscoresymnum_identifier_numeral33 { let (p, ( l1 )) = $3 in ($1, ($2)::(l1)) } - - commands_commands_command30: - | cur_position { ($1, []) } - - commands_commands_command30: - | command commands_commands_command30 { let (p, ( l1 )) = $2 in (pd_command $1, ($1)::(l1)) } - - commandgetvalue_command_term24: - | term { (pd_term $1, ($1)::[]) } - - commandgetvalue_command_term24: - | term commandgetvalue_command_term24 { let (p, ( l1 )) = $2 in (pd_term $1, ($1)::(l1)) } - - commanddefinefun_command_sortedvar15: - | cur_position { ($1, []) } - - commanddefinefun_command_sortedvar15: - | sortedvar commanddefinefun_command_sortedvar15 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) } - - commanddeclarefun_command_sort13: - | cur_position { ($1, []) } - - commanddeclarefun_command_sort13: - | sort commanddeclarefun_command_sort13 { let (p, ( l1 )) = $2 in (pd_sort $1, ($1)::(l1)) } - - commanddefinesort_command_symbol11: - | cur_position { ($1, []) } - - commanddefinesort_command_symbol11: - | symbol commanddefinesort_command_symbol11 { let (p, ( l1 )) = $2 in (pd_symbol $1, ($1)::(l1)) } - - attributevalsexpr_attributevalue_sexpr5: - | cur_position { ($1, []) } - - attributevalsexpr_attributevalue_sexpr5: - | sexpr attributevalsexpr_attributevalue_sexpr5 { let (p, ( l1 )) = $2 in (pd_sexpr $1, ($1)::(l1)) } diff --git a/src/util/smtlib/smtlib.ml b/src/util/smtlib/smtlib.ml deleted file mode 100644 index 49057058..00000000 --- a/src/util/smtlib/smtlib.ml +++ /dev/null @@ -1,112 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -open Smtlib_syntax - -module F = Expr -module T = Cnf.S - -exception Bad_arity of string -exception Unknown_command -exception Incomplete_translation - -(* Environment *) -let env : (string, T.t) Hashtbl.t = Hashtbl.create 57;; -Hashtbl.add env "true" T.f_true;; -Hashtbl.add env "false" T.f_false;; - -let get_atom s = - try - Hashtbl.find env s - with Not_found -> - let f = T.make_atom (F.fresh ()) in - Hashtbl.add env s f; - f - -(* Term translation *) -let translate_const = function - | SpecConstsDec(_, s) - | SpecConstNum(_, s) - | SpecConstString(_, s) - | SpecConstsHex(_, s) - | SpecConstsBinary(_, s) -> s - -let translate_symbol = function - | Symbol(_, s) - | SymbolWithOr(_, s) -> s - -let translate_id = function - | IdSymbol(_, s) -> translate_symbol s - | IdUnderscoreSymNum(_, s, n) -> raise Incomplete_translation - -let translate_qualid = function - | QualIdentifierId(_, id) -> translate_id id - | QualIdentifierAs(_, id, s) -> raise Incomplete_translation - -let left_assoc s f = function - | x :: r -> List.fold_left f x r - | _ -> raise (Bad_arity s) - -let rec right_assoc s f = function - | [] -> raise (Bad_arity s) - | [x] -> x - | x :: r -> f x (right_assoc s f r) - -let translate_atom = function - | TermSpecConst(_, const) -> translate_const const - | TermQualIdentifier(_, id) -> translate_qualid id - | _ -> raise Incomplete_translation - -let rec translate_term = function - | TermQualIdTerm(_, f, (_, l)) -> - begin match (translate_qualid f) with - | "=" -> - begin match (List.map translate_atom l) with - | [a; b] -> T.make_atom (F.mk_eq a b) - | _ -> assert false - end - | s -> - begin match s, (List.map translate_term l) with - (* CORE theory translation - 'distinct','ite' not yet implemented *) - | "not", [e] -> T.make_not e - | "not", _ -> raise (Bad_arity "not") - | "and", l -> T.make_and l - | "or", l -> T.make_or l - | "xor" as s, l -> left_assoc s T.make_xor l - | "=>" as s, l -> right_assoc s T.make_imply l - | _ -> - Format.printf "unknown : %s@." s; - raise Unknown_command - end - end - | e -> (get_atom (translate_atom e)) - -(* Command Translation *) -let translate_command = function - | CommandDeclareFun(_, s, (_, []), _) -> - None - | CommandAssert(_, t) -> - Some (translate_term t) - | _ -> None - -let rec translate_command_list acc = function - | [] -> acc - | c :: r -> - begin match translate_command c with - | None -> translate_command_list acc r - | Some t -> translate_command_list (t :: acc) r - end - -let translate = function - | Some Commands (_, (_, l)) -> List.rev (translate_command_list [] l) - | None -> [] - -let parse file = - let f = open_in file in - let lexbuf = Lexing.from_channel f in - let commands = Parsesmtlib.main Lexsmtlib.token lexbuf in - close_in f; - translate commands diff --git a/src/util/smtlib/smtlib.mli b/src/util/smtlib/smtlib.mli deleted file mode 100644 index c5c5bfed..00000000 --- a/src/util/smtlib/smtlib.mli +++ /dev/null @@ -1,7 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -val parse : string -> Cnf.S.t list diff --git a/src/util/smtlib/smtlib_syntax.ml b/src/util/smtlib/smtlib_syntax.ml deleted file mode 100644 index 6f33e693..00000000 --- a/src/util/smtlib/smtlib_syntax.ml +++ /dev/null @@ -1,229 +0,0 @@ -(* auto-generated by gt *) - -open Smtlib_util;; - -type dummy = Dummy -and an_option = | AnOptionAttribute of pd * attribute -and attribute = | AttributeKeyword of pd * string | AttributeKeywordValue of pd * string * attributevalue -and attributevalue = | AttributeValSpecConst of pd * specconstant | AttributeValSymbol of pd * symbol | AttributeValSexpr of pd * attributevalsexpr_attributevalue_sexpr5 -and command = | CommandSetLogic of pd * symbol | CommandSetOption of pd * an_option | CommandSetInfo of pd * attribute | CommandDeclareSort of pd * symbol * string | CommandDefineSort of pd * symbol * commanddefinesort_command_symbol11 * sort | CommandDeclareFun of pd * symbol * commanddeclarefun_command_sort13 * sort | CommandDefineFun of pd * symbol * commanddefinefun_command_sortedvar15 * sort * term | CommandPush of pd * string | CommandPop of pd * string | CommandAssert of pd * term | CommandCheckSat of pd | CommandGetAssert of pd | CommandGetProof of pd | CommandGetUnsatCore of pd | CommandGetValue of pd * commandgetvalue_command_term24 | CommandGetAssign of pd | CommandGetOption of pd * string | CommandGetInfo of pd * infoflag | CommandExit of pd -and commands = | Commands of pd * commands_commands_command30 -and identifier = | IdSymbol of pd * symbol | IdUnderscoreSymNum of pd * symbol * idunderscoresymnum_identifier_numeral33 -and infoflag = | InfoFlagKeyword of pd * string -and qualidentifier = | QualIdentifierId of pd * identifier | QualIdentifierAs of pd * identifier * sort -and sexpr = | SexprSpecConst of pd * specconstant | SexprSymbol of pd * symbol | SexprKeyword of pd * string | SexprInParen of pd * sexprinparen_sexpr_sexpr41 -and sort = | SortIdentifier of pd * identifier | SortIdSortMulti of pd * identifier * sortidsortmulti_sort_sort44 -and sortedvar = | SortedVarSymSort of pd * symbol * sort -and specconstant = | SpecConstsDec of pd * string | SpecConstNum of pd * string | SpecConstString of pd * string | SpecConstsHex of pd * string | SpecConstsBinary of pd * string -and symbol = | Symbol of pd * string | SymbolWithOr of pd * string -and term = | TermSpecConst of pd * specconstant | TermQualIdentifier of pd * qualidentifier | TermQualIdTerm of pd * qualidentifier * termqualidterm_term_term56 | TermLetTerm of pd * termletterm_term_varbinding58 * term | TermForAllTerm of pd * termforallterm_term_sortedvar60 * term | TermExistsTerm of pd * termexiststerm_term_sortedvar62 * term | TermExclimationPt of pd * term * termexclimationpt_term_attribute64 -and varbinding = | VarBindingSymTerm of pd * symbol * term -and termexclimationpt_term_attribute64 = pd * ( attribute) list -and termexiststerm_term_sortedvar62 = pd * ( sortedvar) list -and termforallterm_term_sortedvar60 = pd * ( sortedvar) list -and termletterm_term_varbinding58 = pd * ( varbinding) list -and termqualidterm_term_term56 = pd * ( term) list -and sortidsortmulti_sort_sort44 = pd * ( sort) list -and sexprinparen_sexpr_sexpr41 = pd * ( sexpr) list -and idunderscoresymnum_identifier_numeral33 = pd * ( string) list -and commands_commands_command30 = pd * ( command) list -and commandgetvalue_command_term24 = pd * ( term) list -and commanddefinefun_command_sortedvar15 = pd * ( sortedvar) list -and commanddeclarefun_command_sort13 = pd * ( sort) list -and commanddefinesort_command_symbol11 = pd * ( symbol) list -and attributevalsexpr_attributevalue_sexpr5 = pd * ( sexpr) list;; - -(* pd stands for pos (position) and extradata *) -let dummy () = () -and pd_an_option = function - | AnOptionAttribute(d,_) -> d - -and pd_attribute = function - | AttributeKeyword(d,_) -> d - - | AttributeKeywordValue(d,_,_) -> d - -and pd_attributevalue = function - | AttributeValSpecConst(d,_) -> d - - | AttributeValSymbol(d,_) -> d - - | AttributeValSexpr(d,_) -> d - -and pd_command = function - | CommandSetLogic(d,_) -> d - - | CommandSetOption(d,_) -> d - - | CommandSetInfo(d,_) -> d - - | CommandDeclareSort(d,_,_) -> d - - | CommandDefineSort(d,_,_,_) -> d - - | CommandDeclareFun(d,_,_,_) -> d - - | CommandDefineFun(d,_,_,_,_) -> d - - | CommandPush(d,_) -> d - - | CommandPop(d,_) -> d - - | CommandAssert(d,_) -> d - - | CommandCheckSat(d) -> d - - | CommandGetAssert(d) -> d - - | CommandGetProof(d) -> d - - | CommandGetUnsatCore(d) -> d - - | CommandGetValue(d,_) -> d - - | CommandGetAssign(d) -> d - - | CommandGetOption(d,_) -> d - - | CommandGetInfo(d,_) -> d - - | CommandExit(d) -> d - -and pd_commands = function - | Commands(d,_) -> d - -and pd_identifier = function - | IdSymbol(d,_) -> d - - | IdUnderscoreSymNum(d,_,_) -> d - -and pd_infoflag = function - | InfoFlagKeyword(d,_) -> d - -and pd_qualidentifier = function - | QualIdentifierId(d,_) -> d - - | QualIdentifierAs(d,_,_) -> d - -and pd_sexpr = function - | SexprSpecConst(d,_) -> d - - | SexprSymbol(d,_) -> d - - | SexprKeyword(d,_) -> d - - | SexprInParen(d,_) -> d - -and pd_sort = function - | SortIdentifier(d,_) -> d - - | SortIdSortMulti(d,_,_) -> d - -and pd_sortedvar = function - | SortedVarSymSort(d,_,_) -> d - -and pd_specconstant = function - | SpecConstsDec(d,_) -> d - - | SpecConstNum(d,_) -> d - - | SpecConstString(d,_) -> d - - | SpecConstsHex(d,_) -> d - - | SpecConstsBinary(d,_) -> d - -and pd_symbol = function - | Symbol(d,_) -> d - - | SymbolWithOr(d,_) -> d - -and pd_term = function - | TermSpecConst(d,_) -> d - - | TermQualIdentifier(d,_) -> d - - | TermQualIdTerm(d,_,_) -> d - - | TermLetTerm(d,_,_) -> d - - | TermForAllTerm(d,_,_) -> d - - | TermExistsTerm(d,_,_) -> d - - | TermExclimationPt(d,_,_) -> d - -and pd_varbinding = function - | VarBindingSymTerm(d,_,_) -> d - -and pd_termexclimationpt_term_attribute64 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_termexiststerm_term_sortedvar62 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_termforallterm_term_sortedvar60 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_termletterm_term_varbinding58 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_termqualidterm_term_term56 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_sortidsortmulti_sort_sort44 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_sexprinparen_sexpr_sexpr41 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_idunderscoresymnum_identifier_numeral33 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_commands_commands_command30 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_commandgetvalue_command_term24 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_commanddefinefun_command_sortedvar15 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_commanddeclarefun_command_sort13 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_commanddefinesort_command_symbol11 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_attributevalsexpr_attributevalue_sexpr5 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d -;; -let pd e = pd_commands e;; diff --git a/src/util/smtlib/smtlib_syntax.mli b/src/util/smtlib/smtlib_syntax.mli deleted file mode 100644 index 05ad8cc7..00000000 --- a/src/util/smtlib/smtlib_syntax.mli +++ /dev/null @@ -1,123 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -type dummy = Dummy -and an_option = AnOptionAttribute of Smtlib_util.pd * attribute -and attribute = - AttributeKeyword of Smtlib_util.pd * string - | AttributeKeywordValue of Smtlib_util.pd * string * attributevalue -and attributevalue = - AttributeValSpecConst of Smtlib_util.pd * specconstant - | AttributeValSymbol of Smtlib_util.pd * symbol - | AttributeValSexpr of Smtlib_util.pd * - attributevalsexpr_attributevalue_sexpr5 -and command = - CommandSetLogic of Smtlib_util.pd * symbol - | CommandSetOption of Smtlib_util.pd * an_option - | CommandSetInfo of Smtlib_util.pd * attribute - | CommandDeclareSort of Smtlib_util.pd * symbol * string - | CommandDefineSort of Smtlib_util.pd * symbol * - commanddefinesort_command_symbol11 * sort - | CommandDeclareFun of Smtlib_util.pd * symbol * - commanddeclarefun_command_sort13 * sort - | CommandDefineFun of Smtlib_util.pd * symbol * - commanddefinefun_command_sortedvar15 * sort * term - | CommandPush of Smtlib_util.pd * string - | CommandPop of Smtlib_util.pd * string - | CommandAssert of Smtlib_util.pd * term - | CommandCheckSat of Smtlib_util.pd - | CommandGetAssert of Smtlib_util.pd - | CommandGetProof of Smtlib_util.pd - | CommandGetUnsatCore of Smtlib_util.pd - | CommandGetValue of Smtlib_util.pd * commandgetvalue_command_term24 - | CommandGetAssign of Smtlib_util.pd - | CommandGetOption of Smtlib_util.pd * string - | CommandGetInfo of Smtlib_util.pd * infoflag - | CommandExit of Smtlib_util.pd -and commands = Commands of Smtlib_util.pd * commands_commands_command30 -and identifier = - IdSymbol of Smtlib_util.pd * symbol - | IdUnderscoreSymNum of Smtlib_util.pd * symbol * - idunderscoresymnum_identifier_numeral33 -and infoflag = InfoFlagKeyword of Smtlib_util.pd * string -and qualidentifier = - QualIdentifierId of Smtlib_util.pd * identifier - | QualIdentifierAs of Smtlib_util.pd * identifier * sort -and sexpr = - SexprSpecConst of Smtlib_util.pd * specconstant - | SexprSymbol of Smtlib_util.pd * symbol - | SexprKeyword of Smtlib_util.pd * string - | SexprInParen of Smtlib_util.pd * sexprinparen_sexpr_sexpr41 -and sort = - SortIdentifier of Smtlib_util.pd * identifier - | SortIdSortMulti of Smtlib_util.pd * identifier * - sortidsortmulti_sort_sort44 -and sortedvar = SortedVarSymSort of Smtlib_util.pd * symbol * sort -and specconstant = - SpecConstsDec of Smtlib_util.pd * string - | SpecConstNum of Smtlib_util.pd * string - | SpecConstString of Smtlib_util.pd * string - | SpecConstsHex of Smtlib_util.pd * string - | SpecConstsBinary of Smtlib_util.pd * string -and symbol = - Symbol of Smtlib_util.pd * string - | SymbolWithOr of Smtlib_util.pd * string -and term = - TermSpecConst of Smtlib_util.pd * specconstant - | TermQualIdentifier of Smtlib_util.pd * qualidentifier - | TermQualIdTerm of Smtlib_util.pd * qualidentifier * - termqualidterm_term_term56 - | TermLetTerm of Smtlib_util.pd * termletterm_term_varbinding58 * term - | TermForAllTerm of Smtlib_util.pd * termforallterm_term_sortedvar60 * term - | TermExistsTerm of Smtlib_util.pd * termexiststerm_term_sortedvar62 * term - | TermExclimationPt of Smtlib_util.pd * term * - termexclimationpt_term_attribute64 -and varbinding = VarBindingSymTerm of Smtlib_util.pd * symbol * term -and termexclimationpt_term_attribute64 = Smtlib_util.pd * attribute list -and termexiststerm_term_sortedvar62 = Smtlib_util.pd * sortedvar list -and termforallterm_term_sortedvar60 = Smtlib_util.pd * sortedvar list -and termletterm_term_varbinding58 = Smtlib_util.pd * varbinding list -and termqualidterm_term_term56 = Smtlib_util.pd * term list -and sortidsortmulti_sort_sort44 = Smtlib_util.pd * sort list -and sexprinparen_sexpr_sexpr41 = Smtlib_util.pd * sexpr list -and idunderscoresymnum_identifier_numeral33 = Smtlib_util.pd * string list -and commands_commands_command30 = Smtlib_util.pd * command list -and commandgetvalue_command_term24 = Smtlib_util.pd * term list -and commanddefinefun_command_sortedvar15 = Smtlib_util.pd * sortedvar list -and commanddeclarefun_command_sort13 = Smtlib_util.pd * sort list -and commanddefinesort_command_symbol11 = Smtlib_util.pd * symbol list -and attributevalsexpr_attributevalue_sexpr5 = Smtlib_util.pd * sexpr list -val dummy : unit -> unit -val pd_an_option : an_option -> Smtlib_util.pd -val pd_attribute : attribute -> Smtlib_util.pd -val pd_attributevalue : attributevalue -> Smtlib_util.pd -val pd_command : command -> Smtlib_util.pd -val pd_commands : commands -> Smtlib_util.pd -val pd_identifier : identifier -> Smtlib_util.pd -val pd_infoflag : infoflag -> Smtlib_util.pd -val pd_qualidentifier : qualidentifier -> Smtlib_util.pd -val pd_sexpr : sexpr -> Smtlib_util.pd -val pd_sort : sort -> Smtlib_util.pd -val pd_sortedvar : sortedvar -> Smtlib_util.pd -val pd_specconstant : specconstant -> Smtlib_util.pd -val pd_symbol : symbol -> Smtlib_util.pd -val pd_term : term -> Smtlib_util.pd -val pd_varbinding : varbinding -> Smtlib_util.pd -val pd_termexclimationpt_term_attribute64 : 'a * 'b list -> 'a -val pd_termexiststerm_term_sortedvar62 : 'a * 'b list -> 'a -val pd_termforallterm_term_sortedvar60 : 'a * 'b list -> 'a -val pd_termletterm_term_varbinding58 : 'a * 'b list -> 'a -val pd_termqualidterm_term_term56 : 'a * 'b list -> 'a -val pd_sortidsortmulti_sort_sort44 : 'a * 'b list -> 'a -val pd_sexprinparen_sexpr_sexpr41 : 'a * 'b list -> 'a -val pd_idunderscoresymnum_identifier_numeral33 : 'a * 'b list -> 'a -val pd_commands_commands_command30 : 'a * 'b list -> 'a -val pd_commandgetvalue_command_term24 : 'a * 'b list -> 'a -val pd_commanddefinefun_command_sortedvar15 : 'a * 'b list -> 'a -val pd_commanddeclarefun_command_sort13 : 'a * 'b list -> 'a -val pd_commanddefinesort_command_symbol11 : 'a * 'b list -> 'a -val pd_attributevalsexpr_attributevalue_sexpr5 : 'a * 'b list -> 'a -val pd : commands -> Smtlib_util.pd diff --git a/src/util/smtlib/smtlib_util.ml b/src/util/smtlib/smtlib_util.ml deleted file mode 100644 index 8e1da4d5..00000000 --- a/src/util/smtlib/smtlib_util.ml +++ /dev/null @@ -1,12 +0,0 @@ -(* auto-generated by gt *) - -(* no extra data from grammar file. *) -type extradata = unit;; -let initial_data() = ();; - -let file = ref "stdin";; -let line = ref 1;; -type pos = int;; -let string_of_pos p = "line "^(string_of_int p);; -let cur_pd() = (!line, initial_data());; (* "pd": pos + extradata *) -type pd = pos * extradata;; diff --git a/src/util/smtlib/smtlib_util.mli b/src/util/smtlib/smtlib_util.mli deleted file mode 100644 index 24ff66b8..00000000 --- a/src/util/smtlib/smtlib_util.mli +++ /dev/null @@ -1,14 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -type extradata = unit -val initial_data : unit -> unit -val file : string ref -val line : int ref -type pos = int -val string_of_pos : int -> string -val cur_pd : unit -> int * unit -type pd = pos * extradata diff --git a/src/util/type.ml b/src/util/type.ml new file mode 100644 index 00000000..584bc1aa --- /dev/null +++ b/src/util/type.ml @@ -0,0 +1,619 @@ + +(* Log&Module Init *) +(* ************************************************************************ *) + +module Ast = Dolmen.Term +module Id = Dolmen.Id +module M = Map.Make(Id) +module H = Hashtbl.Make(Id) + +(* Types *) +(* ************************************************************************ *) + +(* The type of potentially expected result type for parsing an expression *) +type expect = + | Nothing + | Type + | Typed of Expr.ty + +(* The type returned after parsing an expression. *) +type res = + | Ttype + | Ty of Expr.ty + | Term of Expr.term + | Formula of Expr.Formula.t + + +(* The local environments used for type-checking. *) +type env = { + + (* local variables (mostly quantified variables) *) + type_vars : (Expr.ttype Expr.id) M.t; + term_vars : (Expr.ty Expr.id) M.t; + + (* Bound variables (through let constructions) *) + term_lets : Expr.term M.t; + prop_lets : Expr.Formula.t M.t; + + (* Typing options *) + expect : expect; +} + +type 'a typer = env -> Dolmen.Term.t -> 'a + +(* Exceptions *) +(* ************************************************************************ *) + +(* Internal exception *) +exception Found of Ast.t + +(* Exception for typing errors *) +exception Typing_error of string * Ast.t + +(* Convenience functions *) +let _expected s t = raise (Typing_error ( + Format.asprintf "Expected a %s" s, t)) +let _bad_arity s n t = raise (Typing_error ( + Format.asprintf "Bad arity for operator '%s' (expected %d arguments)" s n, t)) +let _type_mismatch t ty ty' ast = raise (Typing_error ( + Format.asprintf "Type Mismatch: '%a' has type %a, but an expression of type %a was expected" + Expr.Print.term t Expr.Print.ty ty Expr.Print.ty ty', ast)) +let _fo_term s t = raise (Typing_error ( + Format.asprintf "Let-bound variable '%a' is applied to terms" Id.print s, t)) + +(* Global Environment *) +(* ************************************************************************ *) + +(* Global identifier table; stores declared types and aliases. *) +let global_env = H.create 42 + +let find_global name = + try H.find global_env name + with Not_found -> `Not_found + +(* Symbol declarations *) +let decl_ty_cstr id c = + if H.mem global_env id then + Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition" + (fun k -> k Id.print id); + H.add global_env id (`Ty c); + Log.debugf 1 "New type constructor : %a" (fun k -> k Expr.Print.const_ttype c) + +let decl_term id c = + if H.mem global_env id then + Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition" + (fun k -> k Id.print id); + H.add global_env id (`Term c); + Log.debugf 1 "New constant : %a" (fun k -> k Expr.Print.const_ty c) + +(* Symbol definitions *) +let def_ty id args body = + if H.mem global_env id then + Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition" + (fun k -> k Id.print id); + H.add global_env id (`Ty_alias (args, body)) + +let def_term id ty_args args body = + if H.mem global_env id then + Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition" + (fun k -> k Id.print id); + H.add global_env id (`Term_alias (ty_args, args, body)) + +(* Local Environment *) +(* ************************************************************************ *) + +(* Make a new empty environment *) +let empty_env ?(expect=Nothing) = { + type_vars = M.empty; + term_vars = M.empty; + term_lets = M.empty; + prop_lets = M.empty; + expect; +} + +let expect env expect = { env with expect = expect } + +(* Generate new fresh names for shadowed variables *) +let new_name pre = + let i = ref 0 in + (fun () -> incr i; pre ^ (string_of_int !i)) + +let new_ty_name = new_name "ty#" +let new_term_name = new_name "term#" + +(* Add local variables to environment *) +let add_type_var env id v = + let v' = + if M.mem id env.type_vars then + Expr.Id.ttype (new_ty_name ()) + else + v + in + Log.debugf 1 "New binding : %a -> %a" + (fun k -> k Id.print id Expr.Print.id_ttype v'); + v', { env with type_vars = M.add id v' env.type_vars } + +let add_type_vars env l = + let l', env' = List.fold_left (fun (l, acc) (id, v) -> + let v', acc' = add_type_var acc id v in + v' :: l, acc') ([], env) l in + List.rev l', env' + +let add_term_var env id v = + let v' = + if M.mem id env.type_vars then + Expr.Id.ty (new_term_name ()) Expr.(v.id_type) + else + v + in + Log.debugf 1 "New binding : %a -> %a" + (fun k -> k Id.print id Expr.Print.id_ty v'); + v', { env with term_vars = M.add id v' env.term_vars } + +let find_var env name = + try `Ty (M.find name env.type_vars) + with Not_found -> + begin + try + `Term (M.find name env.term_vars) + with Not_found -> + `Not_found + end + +(* Add local bound variables to env *) +let add_let_term env id t = + Log.debugf 1 "New let-binding : %s -> %a" + (fun k -> k id.Id.name Expr.Print.term t); + { env with term_lets = M.add id t env.term_lets } + +let add_let_prop env id t = + Log.debugf 1 "New let-binding : %s -> %a" + (fun k -> k id.Id.name Expr.Formula.print t); + { env with prop_lets = M.add id t env.prop_lets } + +let find_let env name = + try `Term (M.find name env.term_lets) + with Not_found -> + begin + try + `Prop (M.find name env.prop_lets) + with Not_found -> + `Not_found + end + +let pp_expect fmt = function + | Nothing -> Format.fprintf fmt "<>" + | Type -> Format.fprintf fmt "" + | Typed ty -> Expr.Print.ty fmt ty + +let pp_map pp fmt map = + M.iter (fun k v -> + Format.fprintf fmt "%s->%a;" k.Id.name pp v) map + +let pp_env fmt env = + Format.fprintf fmt "(%a) %a%a%a%a" + pp_expect env.expect + (pp_map Expr.Print.id_ttype) env.type_vars + (pp_map Expr.Print.id_ty) env.term_vars + (pp_map Expr.Print.term) env.term_lets + (pp_map Expr.Formula.print) env.prop_lets + +(* Some helper functions *) +(* ************************************************************************ *) + +let flat_map f l = List.flatten (List.map f l) + +let take_drop n l = + let rec aux acc = function + | 0, _ | _, [] -> List.rev acc, [] + | m, x :: r -> aux (x :: acc) (m - 1, r) + in + aux [] (n, l) + +let diagonal l = + let rec single x acc = function + | [] -> acc + | y :: r -> single x ((x, y) :: acc) r + and aux acc = function + | [] -> acc + | x :: r -> aux (single x acc r) r + in + aux [] l + +(* Wrappers for expression building *) +(* ************************************************************************ *) + +let arity f = + List.length Expr.(f.id_type.fun_vars) + + List.length Expr.(f.id_type.fun_args) + +let ty_apply env ast f args = + try + Expr.Ty.apply f args + with Expr.Bad_ty_arity _ -> + _bad_arity Expr.(f.id_name) (arity f) ast + +let term_apply env ast f ty_args t_args = + try + Expr.Term.apply f ty_args t_args + with + | Expr.Bad_arity _ -> + _bad_arity Expr.(f.id_name) (arity f) ast + | Expr.Type_mismatch (t, ty, ty') -> + _type_mismatch t ty ty' ast + +let ty_subst ast_term id args f_args body = + let aux s v ty = Expr.Subst.Id.bind v ty s in + match List.fold_left2 aux Expr.Subst.empty f_args args with + | subst -> + Expr.Ty.subst subst body + | exception Invalid_argument _ -> + _bad_arity id.Id.name (List.length f_args) ast_term + +let term_subst ast_term id ty_args t_args f_ty_args f_t_args body = + let aux s v ty = Expr.Subst.Id.bind v ty s in + match List.fold_left2 aux Expr.Subst.empty f_ty_args ty_args with + | ty_subst -> + begin + let aux s v t = Expr.Subst.Id.bind v t s in + match List.fold_left2 aux Expr.Subst.empty f_t_args t_args with + | t_subst -> + Expr.Term.subst ty_subst t_subst body + | exception Invalid_argument _ -> + _bad_arity id.Id.name (List.length f_ty_args + List.length f_t_args) ast_term + end + | exception Invalid_argument _ -> + _bad_arity id.Id.name (List.length f_ty_args + List.length f_t_args) ast_term + +let make_eq ast_term a b = + try + Expr.Formula.make_atom @@ Expr.Atom.eq a b + with Expr.Type_mismatch (t, ty, ty') -> + _type_mismatch t ty ty' ast_term + +let make_pred ast_term p = + try + Expr.Formula.make_atom @@ Expr.Atom.pred p + with Expr.Type_mismatch (t, ty, ty') -> + _type_mismatch t ty ty' ast_term + +let infer env s args = + match env.expect with + | Nothing -> `Nothing + | Type -> + let n = List.length args in + let res = Expr.Id.ty_fun s.Id.name n in + decl_ty_cstr s res; + `Ty res + | Typed ty -> + let n = List.length args in + let rec replicate acc n = + if n <= 0 then acc else replicate (Expr.Ty.base :: acc) (n - 1) + in + let res = Expr.Id.term_fun s.Id.name [] (replicate [] n) ty in + decl_term s res; + `Term res + +(* Expression parsing *) +(* ************************************************************************ *) + +let rec parse_expr (env : env) t = + match t with + + (* Basic formulas *) + | { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.True }, []) } + | { Ast.term = Ast.Builtin Ast.True } -> + Formula Expr.Formula.f_true + + | { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.False }, []) } + | { Ast.term = Ast.Builtin Ast.False } -> + Formula Expr.Formula.f_false + + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.And}, l) } -> + Formula (Expr.Formula.make_and (List.map (parse_formula env) l)) + + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Or}, l) } -> + Formula (Expr.Formula.make_or (List.map (parse_formula env) l)) + + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Xor}, l) } as t -> + begin match l with + | [p; q] -> + let f = parse_formula env p in + let g = parse_formula env q in + Formula (Expr.Formula.make_not (Expr.Formula.make_equiv f g)) + | _ -> _bad_arity "xor" 2 t + end + + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Imply}, l) } as t -> + begin match l with + | [p; q] -> + let f = parse_formula env p in + let g = parse_formula env q in + Formula (Expr.Formula.make_imply f g) + | _ -> _bad_arity "=>" 2 t + end + + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Equiv}, l) } as t -> + begin match l with + | [p; q] -> + let f = parse_formula env p in + let g = parse_formula env q in + Formula (Expr.Formula.make_equiv f g) + | _ -> _bad_arity "<=>" 2 t + end + + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Not}, l) } as t -> + begin match l with + | [p] -> + Formula (Expr.Formula.make_not (parse_formula env p)) + | _ -> _bad_arity "not" 1 t + end + + (* (Dis)Equality *) + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Eq}, l) } as t -> + begin match l with + | [a; b] -> + Formula ( + make_eq t + (parse_term env a) + (parse_term env b) + ) + | _ -> _bad_arity "=" 2 t + end + + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Distinct}, args) } as t -> + let l' = List.map (parse_term env) args in + let l'' = diagonal l' in + Formula ( + Expr.Formula.make_and + (List.map (fun (a, b) -> + Expr.Formula.make_not + (make_eq t a b)) l'') + ) + + (* General case: application *) + | { Ast.term = Ast.Symbol s } as ast -> + parse_app env ast s [] + | { Ast.term = Ast.App ({ Ast.term = Ast.Symbol s }, l) } as ast -> + parse_app env ast s l + + (* Local bindings *) + | { Ast.term = Ast.Binder (Ast.Let, vars, f) } -> + parse_let env f vars + + (* Other cases *) + | ast -> raise (Typing_error ("Couldn't parse the expression", ast)) + +and parse_var env = function + | { Ast.term = Ast.Colon ({ Ast.term = Ast.Symbol s }, e) } -> + begin match parse_expr env e with + | Ttype -> `Ty (s, Expr.Id.ttype s.Id.name) + | Ty ty -> `Term (s, Expr.Id.ty s.Id.name ty) + | _ -> _expected "type (or Ttype)" e + end + | { Ast.term = Ast.Symbol s } -> + begin match env.expect with + | Nothing -> assert false + | Type -> `Ty (s, Expr.Id.ttype s.Id.name) + | Typed ty -> `Term (s, Expr.Id.ty s.Id.name ty) + end + | t -> _expected "(typed) variable" t + +and parse_quant_vars env l = + let ttype_vars, typed_vars, env' = List.fold_left ( + fun (l1, l2, acc) v -> + match parse_var acc v with + | `Ty (id, v') -> + let v'', acc' = add_type_var acc id v' in + (v'' :: l1, l2, acc') + | `Term (id, v') -> + let v'', acc' = add_term_var acc id v' in + (l1, v'' :: l2, acc') + ) ([], [], env) l in + List.rev ttype_vars, List.rev typed_vars, env' + +and parse_let env f = function + | [] -> parse_expr env f + | x :: r -> + begin match x with + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Eq}, [ + { Ast.term = Ast.Symbol s }; e]) } -> + let t = parse_term env e in + let env' = add_let_term env s t in + parse_let env' f r + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Equiv}, [ + { Ast.term = Ast.Symbol s }; e]) } -> + let t = parse_formula env e in + let env' = add_let_prop env s t in + parse_let env' f r + | { Ast.term = Ast.Colon ({ Ast.term = Ast.Symbol s }, e) } -> + begin match parse_expr env e with + | Term t -> + let env' = add_let_term env s t in + parse_let env' f r + | Formula t -> + let env' = add_let_prop env s t in + parse_let env' f r + | _ -> _expected "term of formula" e + end + | t -> _expected "let-binding" t + end + +and parse_app env ast s args = + match find_let env s with + | `Term t -> + if args = [] then Term t + else _fo_term s ast + | `Prop p -> + if args = [] then Formula p + else _fo_term s ast + | `Not_found -> + begin match find_var env s with + | `Ty f -> + if args = [] then Ty (Expr.Ty.of_id f) + else _fo_term s ast + | `Term f -> + if args = [] then Term (Expr.Term.of_id f) + else _fo_term s ast + | `Not_found -> + begin match find_global s with + | `Ty f -> + parse_app_ty env ast f args + | `Term f -> + parse_app_term env ast f args + | `Ty_alias (f_args, body) -> + parse_app_subst_ty env ast s args f_args body + | `Term_alias (f_ty_args, f_t_args, body) -> + parse_app_subst_term env ast s args f_ty_args f_t_args body + | `Not_found -> + begin match infer env s args with + | `Ty f -> parse_app_ty env ast f args + | `Term f -> parse_app_term env ast f args + | `Nothing -> + raise (Typing_error ( + Format.asprintf "Scoping error: '%a' not found" Id.print s, ast)) + end + end + end + +and parse_app_ty env ast f args = + let l = List.map (parse_ty env) args in + Ty (ty_apply env ast f l) + +and parse_app_term env ast f args = + let n = List.length Expr.(f.id_type.fun_vars) in + let ty_l, t_l = take_drop n args in + let ty_args = List.map (parse_ty env) ty_l in + let t_args = List.map (parse_term env) t_l in + Term (term_apply env ast f ty_args t_args) + +and parse_app_subst_ty env ast id args f_args body = + let l = List.map (parse_ty env) args in + Ty (ty_subst ast id l f_args body) + +and parse_app_subst_term env ast id args f_ty_args f_t_args body = + let n = List.length f_ty_args in + let ty_l, t_l = take_drop n args in + let ty_args = List.map (parse_ty env) ty_l in + let t_args = List.map (parse_term env) t_l in + Term (term_subst ast id ty_args t_args f_ty_args f_t_args body) + +and parse_ty env ast = + match parse_expr { env with expect = Type } ast with + | Ty ty -> ty + | _ -> _expected "type" ast + +and parse_term env ast = + match parse_expr { env with expect = Typed Expr.Ty.base } ast with + | Term t -> t + | _ -> _expected "term" ast + +and parse_formula env ast = + match parse_expr { env with expect = Typed Expr.Ty.prop } ast with + | Term t when Expr.(Ty.equal Ty.prop t.t_type) -> + make_pred ast t + | Formula p -> p + | _ -> _expected "formula" ast + +let parse_ttype_var env t = + match parse_var env t with + | `Ty (id, v) -> (id, v) + | `Term _ -> _expected "type variable" t + +let rec parse_sig_quant env = function + | { Ast.term = Ast.Binder (Ast.Pi, vars, t) } -> + let ttype_vars = List.map (parse_ttype_var env) vars in + let ttype_vars', env' = add_type_vars env ttype_vars in + let l = List.combine vars ttype_vars' in + parse_sig_arrow l [] env' t + | t -> + parse_sig_arrow [] [] env t + +and parse_sig_arrow ttype_vars (ty_args: (Ast.t * res) list) env = function + | { Ast.term = Ast.Binder (Ast.Arrow, args, ret) } -> + let t_args = parse_sig_args env args in + parse_sig_arrow ttype_vars (ty_args @ t_args) env ret + | t -> + begin match parse_expr env t with + | Ttype -> + begin match ttype_vars with + | (h, _) :: _ -> + raise (Typing_error ( + "Type constructor signatures cannot have quantified type variables", h)) + | [] -> + let aux n = function + | (_, Ttype) -> n + 1 + | (ast, _) -> raise (Found ast) + in + begin + match List.fold_left aux 0 ty_args with + | n -> `Ty_cstr n + | exception Found err -> + raise (Typing_error ( + Format.asprintf + "Type constructor signatures cannot have non-ttype arguments,", err)) + end + end + | Ty ret -> + let aux acc = function + | (_, Ty t) -> t :: acc + | (ast, _) -> raise (Found ast) + in + begin + match List.fold_left aux [] ty_args with + | exception Found err -> _expected "type" err + | l -> `Fun_ty (List.map snd ttype_vars, List.rev l, ret) + end + | _ -> _expected "Ttype of type" t + end + +and parse_sig_args env l = + flat_map (parse_sig_arg env) l + +and parse_sig_arg env = function + | { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.Product}, l) } -> + List.map (fun x -> x, parse_expr env x) l + | t -> + [t, parse_expr env t] + +let parse_sig = parse_sig_quant + +let rec parse_fun ty_args t_args env = function + | { Ast.term = Ast.Binder (Ast.Fun, l, ret) } -> + let ty_args', t_args', env' = parse_quant_vars env l in + parse_fun (ty_args @ ty_args') (t_args @ t_args') env' ret + | ast -> + begin match parse_expr env ast with + | Ttype -> raise (Typing_error ("Cannot redefine Ttype", ast)) + | Ty body -> + if t_args = [] then `Ty (ty_args, body) + else _expected "term" ast + | Term body -> `Term (ty_args, t_args, body) + | Formula _ -> _expected "type or term" ast + end + +(* High-level parsing functions *) +(* ************************************************************************ *) + +let new_decl env t id = + Log.debugf 5 "Typing declaration: %s : %a" + (fun k -> k id.Id.name Ast.print t); + begin match parse_sig env t with + | `Ty_cstr n -> decl_ty_cstr id (Expr.Id.ty_fun id.Id.name n) + | `Fun_ty (vars, args, ret) -> + decl_term id (Expr.Id.term_fun id.Id.name vars args ret) + end + +let new_def env t id = + Log.debugf 5 "Typing definition: %s = %a" + (fun k -> k id.Id.name Ast.print t); + begin match parse_fun [] [] env t with + | `Ty (ty_args, body) -> def_ty id ty_args body + | `Term (ty_args, t_args, body) -> def_term id ty_args t_args body + end + +let new_formula env t = + Log.debugf 5 "Typing top-level formula: %a" (fun k -> k Ast.print t); + let res = parse_formula env t in + res + diff --git a/src/util/type.mli b/src/util/type.mli new file mode 100644 index 00000000..26fd6ad6 --- /dev/null +++ b/src/util/type.mli @@ -0,0 +1,15 @@ + +(** Typechecking of terms from Dolmen.Term.t + This module provides functions to parse terms from the untyped syntax tree + defined in Dolmen, and generate formulas as defined in the Expr module. *) + +exception Typing_error of string * Dolmen.Term.t + +(** {2 High-level functions} *) + +val new_decl : Dolmen.Id.t -> Dolmen.Term.t -> unit + +val new_def : Dolmen.Id.t -> Dolmen.Term.t -> unit + +val new_formula : Dolmen.Term.t -> Expr.Formula.t +