simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-09 04:35:35 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Added Expr and typing module from ArchSat

Browse source
This commit is contained in:
Guillaume Bury 2016-09-07 17:58:07 +02:00
parent bb2c931d68
commit 742f8c469d
24 changed files with 1503 additions and 1249 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
.merlin
View file

@ -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

7
_tags
View file

@ -9,10 +9,9 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20)
<src/core>: include
<src/solver>: include
<src/backend>: include
<src/smt>: include
<src/sat>: include
<src/smt>: include
<src/util>: include
<src/util/smtlib>: include
# Pack options
<src/core/*.cmx>: for-pack(Msat)
@ -22,6 +21,10 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20)
<src/sat/*.cmx>: for-pack(Msat_sat)
<src/smt/*.cmx>: for-pack(Msat_smt)
# Bin options
<src/main.*>: package(dolmen)
<src/util/type.*>: package(dolmen)
# more warnings
<src/**/*.ml>: warn_K, warn_Y, warn_X
<src/**/*.ml>: short_paths, safe_string, strict_sequence

137
src/main.ml
View file

@ -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),
"<s>[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

9
src/smt/cnf.ml
View file

@ -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)

9
src/smt/cnf.mli
View file

@ -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

87
src/smt/expr.ml
View file

@ -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

42
src/smt/expr.mli
View file

@ -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

11
src/util/.merlin
View file

@ -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/

522
src/util/expr.ml Normal file
View file

@ -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 "@[<hov 0>%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 = "<dummy>"; id_type = Type; }
let ty =
{ ty = TyVar id_ttype; ty_hash = -1; }
let id =
{ index = -2; id_name = "<dummy>"; 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)

319
src/util/expr.mli Normal file
View file

@ -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

75
src/util/parsedimacs.ml
View file

@ -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

9
src/util/parsedimacs.mli
View file

@ -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

9
src/util/smtlib/.merlin
View file

@ -1,9 +0,0 @@
S ./
S ../
S ../../sat/
B ../../_build/
B ../../_build/util/
B ../../_build/util/smtlib/
B ../../_build/sat/
B ../../_build/smt/

3
src/util/smtlib/lexsmtlib.mli
View file

@ -1,3 +0,0 @@
(* Copyright 2014 INIA *)
val token : Lexing.lexbuf -> Parsesmtlib.token

48
src/util/smtlib/lexsmtlib.mll
View file

@ -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))}{}

330
src/util/smtlib/parsesmtlib.mly
View file

@ -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 <string> ASCIIWOR BINARY DECIMAL HEXADECIMAL KEYWORD NUMERAL STRINGLIT SYMBOL
%type <Smtlib_syntax.commands option> main
%type <Smtlib_syntax.an_option> an_option
%type <Smtlib_syntax.attribute> attribute
%type <Smtlib_syntax.attributevalsexpr_attributevalue_sexpr5> attributevalsexpr_attributevalue_sexpr5
%type <Smtlib_syntax.attributevalue> attributevalue
%type <Smtlib_syntax.command> command
%type <Smtlib_syntax.commanddeclarefun_command_sort13> commanddeclarefun_command_sort13
%type <Smtlib_syntax.commanddefinefun_command_sortedvar15> commanddefinefun_command_sortedvar15
%type <Smtlib_syntax.commanddefinesort_command_symbol11> commanddefinesort_command_symbol11
%type <Smtlib_syntax.commandgetvalue_command_term24> commandgetvalue_command_term24
%type <Smtlib_syntax.commands> commands
%type <Smtlib_syntax.commands_commands_command30> commands_commands_command30
%type <Smtlib_syntax.identifier> identifier
%type <Smtlib_syntax.idunderscoresymnum_identifier_numeral33> idunderscoresymnum_identifier_numeral33
%type <Smtlib_syntax.infoflag> infoflag
%type <Smtlib_syntax.qualidentifier> qualidentifier
%type <Smtlib_syntax.sexpr> sexpr
%type <Smtlib_syntax.sexprinparen_sexpr_sexpr41> sexprinparen_sexpr_sexpr41
%type <Smtlib_syntax.sort> sort
%type <Smtlib_syntax.sortedvar> sortedvar
%type <Smtlib_syntax.sortidsortmulti_sort_sort44> sortidsortmulti_sort_sort44
%type <Smtlib_syntax.specconstant> specconstant
%type <Smtlib_syntax.symbol> symbol
%type <Smtlib_syntax.term> term
%type <Smtlib_syntax.termexclimationpt_term_attribute64> termexclimationpt_term_attribute64
%type <Smtlib_syntax.termexiststerm_term_sortedvar62> termexiststerm_term_sortedvar62
%type <Smtlib_syntax.termforallterm_term_sortedvar60> termforallterm_term_sortedvar60
%type <Smtlib_syntax.termletterm_term_varbinding58> termletterm_term_varbinding58
%type <Smtlib_syntax.termqualidterm_term_term56> termqualidterm_term_term56
%type <Smtlib_syntax.varbinding> varbinding
%type <Smtlib_util.pd> 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)) }

112
src/util/smtlib/smtlib.ml
View file

@ -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

7
src/util/smtlib/smtlib.mli
View file

@ -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

229
src/util/smtlib/smtlib_syntax.ml
View file

@ -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;;

123
src/util/smtlib/smtlib_syntax.mli
View file

@ -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

12
src/util/smtlib/smtlib_util.ml
View file

@ -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;;

14
src/util/smtlib/smtlib_util.mli
View file

@ -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

619
src/util/type.ml Normal file
View file

@ -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 "<tType>"
| 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

15
src/util/type.mli Normal file
View file

@ -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