diff --git a/src/bin/dune b/src/bin/dune
deleted file mode 100644
index a168a58d3c216ebc6891f3301118b3937547d219..0000000000000000000000000000000000000000
--- a/src/bin/dune
+++ /dev/null
@@ -1,13 +0,0 @@
-; main binary
-
-(executable
- (modes byte exe)
- (name witan)
- (public_name witan)
- (libraries containers gen dolmen cmdliner spelll witan.core
- witan.solver witan.theories.bool witan.theories.LRA)
- (preprocess
- (pps ppx_optcomp))
- (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always)
- (ocamlopt_flags :standard -O3 -color always -unbox-closures
- -unbox-closures-factor 20))
diff --git a/src/bin/options.ml b/src/bin/options.ml
deleted file mode 100644
index 45c3f932c68652c8af2966163eacf3219f61b24d..0000000000000000000000000000000000000000
--- a/src/bin/options.ml
+++ /dev/null
@@ -1,212 +0,0 @@
-(*************************************************************************)
-(* This file is part of Colibrics. *)
-(* *)
-(* Copyright (C) 2017 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(*************************************************************************)
-
-(* Option types *)
-(* ************************************************************************ *)
-
-type language = Witan_solver.Input.language
-
-type input_options = {
- dir : string;
- file : string;
- language : language option;
-}
-
-type t = {
-
- input : input_options;
-
- (* typing *)
- type_only : bool;
-
- (* Time/Memory options *)
- time_limit : float;
- size_limit : float;
-
- (* Step options *)
- step_limit : int;
-
- (* seed for shuffling *)
- seed_shuffle : int option;
-
- (* debug flags *)
- debug_flags : Witan_popop_lib.Debug.flag list;
-}
-
-(* Creating option records *)
-(* ************************************************************************ *)
-
-let mk_input_options f language =
- let dir = Filename.dirname f in
- let file = Filename.basename f in
- { dir; file; language; }
-
-let mk input time_limit size_limit step_limit type_only seed_shuffle debug_flags =
- { input; time_limit; size_limit; step_limit; type_only; seed_shuffle; debug_flags }
-
-(* Argument converters *)
-(* ************************************************************************ *)
-
-let input = Cmdliner.Arg.enum Witan_solver.Input.enum
-
-(* Argument converter for integer with multiplier suffix *)
-(* ************************************************************************ *)
-
-let nb_sec_minute = 60
-let nb_sec_hour = 60 * nb_sec_minute
-let nb_sec_day = 24 * nb_sec_hour
-
-let print_aux suffix fmt n =
- if n = 0 then ()
- else Format.fprintf fmt "%d%s" n suffix
-
-let print_time fmt f =
- let n = int_of_float f in
- let aux n div = n / div, n mod div in
- let n_day, n = aux n nb_sec_day in
- let n_hour, n = aux n nb_sec_hour in
- let n_min, n = aux n nb_sec_minute in
- Format.fprintf fmt "%a%a%a%a"
- (print_aux "d") n_day
- (print_aux "h") n_hour
- (print_aux "m") n_min
- (print_aux "s") n
-
-let parse_time arg =
- let l = String.length arg in
- let multiplier m =
- let arg1 = String.sub arg 0 (l-1) in
- `Ok (m *. (float_of_string arg1))
- in
- assert (l > 0);
- try
- match arg.[l-1] with
- | 's' -> multiplier 1.
- | 'm' -> multiplier 60.
- | 'h' -> multiplier 3600.
- | 'd' -> multiplier 86400.
- | '0'..'9' -> `Ok (float_of_string arg)
- | _ -> `Error "bad numeric argument"
- with Failure _ -> `Error "bad numeric argument"
-
-let print_size fmt f =
- let n = int_of_float f in
- let aux n div = n / div, n mod div in
- let n_tera, n = aux n 1_000_000_000_000 in
- let n_giga, n = aux n 1_000_000_000 in
- let n_mega, n = aux n 1_000_000 in
- let n_kilo, n = aux n 1_000 in
- Format.fprintf fmt "%a%a%a%a%a"
- (print_aux "To") n_tera
- (print_aux "Go") n_giga
- (print_aux "Mo") n_mega
- (print_aux "ko") n_kilo
- (print_aux "") n
-
-let parse_size arg =
- let l = String.length arg in
- let multiplier m =
- let arg1 = String.sub arg 0 (l-1) in
- `Ok (m *. (float_of_string arg1))
- in
- assert (l > 0);
- try
- match arg.[l-1] with
- | 'k' -> multiplier 1e3
- | 'M' -> multiplier 1e6
- | 'G' -> multiplier 1e9
- | 'T' -> multiplier 1e12
- | '0'..'9' -> `Ok (float_of_string arg)
- | _ -> `Error "bad numeric argument"
- with Failure _ -> `Error "bad numeric argument"
-
-let c_time = parse_time, print_time
-let c_size = parse_size, print_size
-
-(* Debug option *)
-let debug_flags_options = "DEBUG FLAGS"
-
-let debug =
- let list_flags =
- List.map (fun (name,flag,_,desc) ->
- let doc = Format.asprintf "%a" Witan_popop_lib.Pp.formatted desc in
- let info = Cmdliner.Arg.info ["debug-"^name] ~doc ~docs:debug_flags_options in
- flag, info
- )
- (Witan_popop_lib.Debug.list_flags ())
-
- in
- Cmdliner.Arg.(value & vflag_all [] list_flags)
-
-
-(* Command terms *)
-(* ************************************************************************ *)
-
-let common_options = "COMMON OPTIONS"
-
-let man = [
- `S common_options;
- `P "Common options for the prover";
- `S debug_flags_options;
-]
-
-let info = Cmdliner.Term.(info ~man ~sdocs:common_options ~version:"0.1" "witan")
-
-let input_options =
- let docs = common_options in
- let fd =
- let doc = "Input problem file" in
- Cmdliner.Arg.(required & pos 0 (some non_dir_file) None & info [] ~docv:"FILE" ~doc)
- in
- let language =
- let doc = Format.asprintf
- "Set the format for the input file to $(docv) (%s)."
- (Cmdliner.Arg.doc_alts_enum ~quoted:false Witan_solver.Input.enum) in
- Cmdliner.Arg.(value & opt (some input) None & info ["i"; "input"] ~docs ~docv:"INPUT" ~doc)
- in
- Cmdliner.Term.(const mk_input_options $ fd $ language)
-
-let all =
- let docs = common_options in
- let time =
- let doc = {|Stop the program after a time lapse of $(docv).
- Accepts usual suffixes for durations : s,m,h,d.
- Without suffix, default to a time in seconds.|} in
- Cmdliner.Arg.(value & opt c_time 300. & info ["t"; "time"] ~docs ~docv:"TIME" ~doc)
- in
- let size =
- let doc = {|Stop the program if it tries and use more the $(docv) memory space.
- Accepts usual suffixes for sizes : k,M,G,T.
- Without suffix, default to a size in octet.|} in
- Cmdliner.Arg.(value & opt c_size 1_000_000_000. & info ["s"; "size"] ~docs ~docv:"SIZE" ~doc)
- in
- let step =
- let doc = {|Stop the program if it tries and use more the $(docv) steps.|} in
- Cmdliner.Arg.(value & opt int (-1) & info ["steps"] ~docs ~docv:"STEPS" ~doc)
- in
- let seed =
- let doc = {|Give a seed for the randomness used in the search (default fixed).|} in
- Cmdliner.Arg.(value & opt (some int) None & info ["seed"] ~docs ~docv:"STEPS" ~doc)
- in
- let type_only =
- let doc = {|Stop the program after parsing and typing.|} in
- Cmdliner.Arg.(value & flag & info ["type-only"] ~doc)
- in
- Cmdliner.Term.(const mk $ input_options $ time $ size $ step $ type_only $ seed $ debug)
diff --git a/src/bin/options.mli b/src/bin/options.mli
deleted file mode 100644
index 20224552e273d928764227df1db1201f0bef56da..0000000000000000000000000000000000000000
--- a/src/bin/options.mli
+++ /dev/null
@@ -1,66 +0,0 @@
-(*************************************************************************)
-(* This file is part of Colibrics. *)
-(* *)
-(* Copyright (C) 2017 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(*************************************************************************)
-
-(** Command line options *)
-
-
-(** {2 Type definitions} *)
-
-type language = Witan_solver.Input.language
-(** Type of format input (taken from dolmen). *)
-
-type input_options = {
- dir : string;
- file : string;
- language : language option;
-}
-(** The various input options. *)
-
-type t = {
-
- input : input_options;
-
- (* typing *)
- type_only : bool;
-
- (* Time/Memory options *)
- time_limit : float;
- size_limit : float;
-
- (* Step options *)
- step_limit : int;
-
- (* seed for shuffling *)
- seed_shuffle : int option;
-
- (* debug flags *)
- debug_flags : Witan_popop_lib.Debug.flag list;
-}
-(** The aggregate type for all command line options *)
-
-
-(** {2 Parsing command line} *)
-
-val all : t Cmdliner.Term.t
-(** The cdmliner term for parsing all command line options. *)
-
-val info : Cmdliner.Term.info
-(** The cmdliner info for parsing command line (includes bin name, version, etc..) *)
-
diff --git a/src/bin/typecheck.ml b/src/bin/typecheck.ml
deleted file mode 100644
index 179c03c98120a3046637810c3d31316c3c2ba983..0000000000000000000000000000000000000000
--- a/src/bin/typecheck.ml
+++ /dev/null
@@ -1,936 +0,0 @@
-(*************************************************************************)
-(* This file is part of Witan. *)
-(* *)
-(* Copyright (C) 2017 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* INRIA (Institut National de Recherche en Informatique et en *)
-(* Automatique) *)
-(* CNRS (Centre national de la recherche scientifique) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(*************************************************************************)
-
-(* Log&Module Init *)
-(* ************************************************************************ *)
-
-module Id = Dolmen.Id
-module Ast = Dolmen.Term
-
-module I = Witan_core.Id
-module Term = Witan_core.Term
-
-let get_loc =
- let default_loc = Dolmen.ParseLocation.mk "<?>" 0 0 0 0 in
- (fun t -> CCOpt.get_or ~default:default_loc t.Ast.loc)
-
-module E = Map.Make(Term.Id)
-module R = Hashtbl.Make(Term.Id)
-
-(* Fuzzy search maps *)
-(* ************************************************************************ *)
-
-module M = struct
-
- module S = Spelll
- module I = S.Index
-
- (** We use fuzzy maps in order to give suggestions in case of typos.
- Since such maps are not trivial to extend to Dolmen identifiers,
- we map strings (identifier names) to list of associations. *)
- type 'a t = (Id.t * 'a) list I.t
-
- let eq = Id.equal
-
- let empty = I.empty
-
- let get t id =
- let s = Id.(id.name) in
- match S.klist_to_list (I.retrieve ~limit:0 t s) with
- | [l] -> l
- | [] -> []
- | _ -> assert false
-
- let mem id t =
- CCList.Assoc.mem ~eq id (get t id)
-
- let find id t =
- CCList.Assoc.get_exn ~eq id (get t id)
-
- let add id v t =
- let l = get t id in
- let l' = CCList.Assoc.set ~eq id v l in
- I.add t Dolmen.Id.(id.name) l'
-
- let iter f t =
- I.iter (fun _ l -> List.iter (fun (id, v) -> f id v) l) t
-
- (** Return a list of suggestions for an identifier. *)
- let suggest ~limit id t =
- let s = Id.(id.name) in
- let l = S.klist_to_list (I.retrieve ~limit t s) in
- CCList.flat_map (List.map fst) l
-
-end
-
-(* Fuzzy search hashtables *)
-(* ************************************************************************ *)
-
-module H = struct
-
- (** Fuzzy hashtables are just references to fuzzy maps.
- The reference is registered on the stack to allow backtracking. *)
- let create () =
- let r = ref M.empty in
- r
-
- let mem r id = M.mem id !r
-
- let find r id = M.find id !r
-
- let suggest r id = M.suggest id !r
-
- let add r id v =
- r := M.add id v !r
-
-end
-
-(* Types *)
-(* ************************************************************************ *)
-
-(* The type of reasons for constant typing *)
-type reason =
- | Inferred of Dolmen.ParseLocation.t
- | Declared of Dolmen.ParseLocation.t
-
-(* The local environments used for type-checking. *)
-type env = {
-
- (* Map from term identifiers to the reason of their type
- (either definition location, or inference location) *)
- locs : reason E.t;
-
- (* Bound variables, either let-bound, or quantified. *)
- vars : Term.t M.t;
-
- (* The current builtin symbols *)
- builtins : builtin_symbols;
-
- (* Additional typing info *)
- expect : Term.t option; (** Expected type of the term to parse *)
- explain : [ `No | `Yes | `Full ];
-}
-
-(* Builtin symbols, i.e symbols understood by some theories,
- but which do not have specific syntax, so end up as special
- cases of application. *)
-and builtin_symbols = env -> Dolmen.Term.t -> Dolmen.Id.t -> Ast.t list -> Term.t option
-
-(* Global Environment *)
-(* ************************************************************************ *)
-
-(* Global identifier table; stores declared types and aliases.
- global locations : stores reason for typing of identifiers *)
-let global_env = H.create ()
-let global_locs = R.create 4013
-
-let find_global name =
- try H.find global_env name
- with Not_found -> `Not_found
-
-(* Symbol declarations *)
-let decl_id id c reason =
- (* TODO: uncomment
- if H.mem global_env id then
- Util.warn ~section
- "Symbol '%a' has already been defined, overwriting previous definition"
- Id.print id;
- *)
- H.add global_env id (`Id c);
- R.add global_locs c reason
-
-(* Symbol definitions *)
-let def_id id args body =
- (* TODO: uncomment
- if H.mem global_env id then
- Util.warn ~section
- "Symbol '%a' has already been defined, overwriting previous definition"
- Id.print id;
- *)
- H.add global_env id (`Alias (args, body))
-
-
-(* Local Environment *)
-(* ************************************************************************ *)
-
-(* Make a new empty environment *)
-let empty_env
- ?(expect=None)
- ?(explain=`No)
- builtins = {
- locs = E.empty;
- vars = M.empty;
- builtins; expect; explain;
-}
-
-let expect ?(force=false) env expect =
- if env.expect = None && not force then env
- else { 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_term_name = new_name "t#"
-
-(* Add local bound variables to env *)
-let add_let_term env id t =
- { env with vars = M.add id t env.vars }
-
-(* Add local variables to environment *)
-let add_term_var env id v loc =
- let v' =
- if M.mem id env.vars then
- I.mk (new_term_name ()) (I.ty v)
- else
- v
- in
- let t = Term.const v' in
- v', { env with
- vars = M.add id t env.vars;
- locs = E.add v' (Declared loc) env.locs;
- }
-
-let find_var env name =
- try Some (M.find name env.vars)
- with Not_found -> None
-
-(* Printing *)
-let print_expect fmt = function
- | None -> Format.fprintf fmt "<>"
- | Some ty -> Term.print fmt ty
-
-let print_map print fmt map =
- let aux k v =
- Format.fprintf fmt "%a ->@ @[<hov>%a@];@ " Id.print k print v
- in
- M.iter aux map
-
-let pp_env fmt env =
- Format.fprintf fmt "@[<hov 2>(%a) %a%a%a%a@]"
- print_expect env.expect (print_map Term.print) env.vars
-
-(* Typo suggestion *)
-(* ************************************************************************ *)
-
-let suggest ~limit env fmt id =
- let l =
- M.suggest ~limit id env.vars @
- H.suggest ~limit global_env id
- in
- if l = [] then
- Format.fprintf fmt "coming up empty, sorry, ^^"
- else
- CCFormat.list Id.print fmt l
-
-(* Typing explanation *)
-(* ************************************************************************ *)
-
-let get_reason_loc = function Inferred l | Declared l -> l
-
-let pp_reason fmt = function
- | Inferred loc -> Format.fprintf fmt "inferred at %a" Dolmen.ParseLocation.fmt loc
- | Declared loc -> Format.fprintf fmt "declared at %a" Dolmen.ParseLocation.fmt loc
-
-let find_reason env v =
- try E.find v env.locs
- with Not_found -> R.find global_locs v
-
-let rec explain ~full env fmt t =
- try
- begin match t with
- | { Term.term = Term.Type; _ } ->
- Format.fprintf fmt "Type: Type"
- | { Term.term = Term.Id v; _ } ->
- let reason = find_reason env v in
- Format.fprintf fmt "%a: %a was %a@\n" I.print v Term.print (I.ty v) pp_reason reason
- | { Term.term = Term.App (f, t); _ } ->
- explain ~full env fmt f;
- if full then explain ~full env fmt t
- | { Term.term = Term.Let (v, e, body); _ } ->
- Format.fprintf fmt "Term let-bound to %a was typed %a@\n"
- I.print v Term.print e.Term.ty
- | { Term.term = Term.Binder (_, _, t); _ } ->
- explain ~full env fmt t
- end with
- | Not_found ->
- Format.fprintf fmt "Couldn't find a typing reason (that's a bug !)"
-
-(* Exceptions *)
-(* ************************************************************************ *)
-
-(* Internal exception *)
-exception Found of Ast.t * Term.t option
-
-(* Exception for typing errors *)
-exception Typing_error of string * env * Ast.t
-
-(* Creating explanations *)
-let mk_expl preface env fmt t =
- match env.explain with
- | `No -> ()
- | `Yes ->
- Format.fprintf fmt "%s\n%a" preface (explain ~full:false env) t
- | `Full ->
- Format.fprintf fmt "%s\n%a" preface (explain ~full:true env) t
-
-(* Convenience functions *)
-let _infer_var env t =
- let msg = Format.asprintf
- "Inferring type for a variable, please check the scope of your quantifications"
- in
- raise (Typing_error (msg, env, t))
-
-let _expected env s t res =
- let msg = match res with
- | None -> "the expression doesn't match what was expected"
- | Some r ->
- let ty = r.Term.ty in
- let tmp =
- match r with
- | { Term.term = Term.Type; _} -> "the Ttype constant"
- | _ when Term.equal ty Term._Type -> "a type"
- | _ when Term.equal ty Term._Prop -> "a first-order formula"
- | _ -> "a first-order term"
- in
- Format.sprintf "got %s" tmp
- in
- let msg = Format.asprintf "Expected a %s, but %s" s msg in
- raise (Typing_error (msg, env, t))
-
-let _bad_op_arity env s n t =
- let msg = Format.asprintf "Bad arity for operator '%s' (expected %d arguments)" s n in
- raise (Typing_error (msg, env, t))
-
-let _bad_id_arity env id n t =
- let msg = Format.asprintf
- "Bad arity for identifier '%a' (expected %d arguments)" Id.print id n
- in
- raise (Typing_error (msg, env, t))
-
-let _bad_term_arity env f n t =
- let msg = Format.asprintf
- "Bad arity for function '%a' (expected %d arguments)" I.print f n
- in
- raise (Typing_error (msg, env, t))
-
-let _fo_let env s t =
- let msg = Format.asprintf "Let-bound variable '%a' is applied to terms" Id.print s in
- raise (Typing_error (msg, env, t))
-
-let _fo_formula env f ast =
- let msg = Format.asprintf "Cannot apply formula '%a' to arguments" Term.print f in
- raise (Typing_error (msg, env, ast))
-
-let _type_mismatch env t ty ty' ast =
- let msg = Format.asprintf
- "Type Mismatch: an expression of type %a was expected, but '%a' has type %a%a"
- Term.print ty' Term.print t Term.print ty (mk_expl ", because:" env) t
- in
- raise (Typing_error (msg, env, ast))
-
-let _cannot_unify env ast ty t =
- let msg = Format.asprintf
- "A term of type '%a'@ was expected, but could not unify it with@ %a:@ %a"
- Term.print ty Term.print t Term.print t.Term.ty
- in
- raise (Typing_error (msg, env, ast))
-
-let _cannot_infer_quant_var env t =
- raise (Typing_error ("Cannot infer the type of a quantified variable", env, t))
-
-(* Wrappers for expression building *)
-(* ************************************************************************ *)
-
-(* Generate fresh variables for wildcards in types. *)
-let gen_wildcard =
- let i = ref 0 in
- (function () -> (* TODO: add location information? *)
- incr i; I.mk (Format.sprintf "?%d" !i) Term._Type)
-
-let wildcard =
- (fun env ast id l ->
- match l with
- | [] ->
- let v = gen_wildcard () in
- Term.const v
- | _ -> _bad_id_arity env id 0 ast
- )
-
-(* Wrapper around term application. Since wildcards are allowed in types,
- there may be some variables in [ty_args], so we have to find an appropriate
- substitution for these variables. To do that, we try and unify the expected type
- and the actual argument types. *)
-let term_apply env ast f ty_args t_args =
- if List.length Expr.(f.id_type.fun_vars) <> List.length ty_args ||
- List.length Expr.(f.id_type.fun_args) <> List.length t_args then
- _bad_term_arity env f (arity f) ast
- else
- let map =
- List.fold_left2
- Mapping.Var.bind_ty Mapping.empty
- Expr.(f.id_type.fun_vars) ty_args
- in
- let expected_types =
- List.map (Mapping.apply_ty map) Expr.(f.id_type.fun_args)
- in
- let subst =
- List.fold_left2 (fun subst expected term ->
- try
- Unif.Robinson.ty subst expected Expr.(term.t_type)
- with
- | Unif.Robinson.Impossible_ty _ ->
- _cannot_unify env ast expected term
- ) map expected_types t_args
- in
- let actual_ty_args = List.map (Mapping.apply_ty subst) ty_args in
- try
- Expr.Term.apply ~status:env.status f actual_ty_args t_args
- with
- | Expr.Bad_arity _ | Expr.Type_mismatch _ ->
- Util.debug ~section "%a, typing:@\n %a :: %a :: %a@\nsubst: %a"
- Dolmen.ParseLocation.fmt (get_loc ast) Expr.Print.const_ty f
- (CCFormat.list Expr.Print.ty) ty_args
- (CCFormat.list Expr.Print.term) t_args
- Mapping.print subst;
- assert false
-
-let ty_subst env ast_term id args f_args body =
- match List.fold_left2 Expr.Subst.Id.bind Expr.Subst.empty f_args args with
- | subst ->
- Expr.Ty.subst subst Expr.Subst.empty body
- | exception Invalid_argument _ ->
- _bad_id_arity env id (List.length f_args) ast_term
-
-let term_subst env ast_term id ty_args t_args f_ty_args f_t_args body =
- match List.fold_left2 Expr.Subst.Id.bind Expr.Subst.empty f_ty_args ty_args with
- | ty_subst ->
- begin
- match List.fold_left2 Expr.Subst.Id.bind Expr.Subst.empty f_t_args t_args with
- | t_subst ->
- Expr.Term.subst ty_subst Expr.Subst.empty t_subst Expr.Subst.empty body
- | exception Invalid_argument _ ->
- _bad_id_arity env id (List.length f_ty_args + List.length f_t_args) ast_term
- end
- | exception Invalid_argument _ ->
- _bad_id_arity env id (List.length f_ty_args + List.length f_t_args) ast_term
-
-let make_eq env ast_term a b =
- try
- Expr.Formula.eq a b
- with Expr.Type_mismatch (t, ty, ty') ->
- _type_mismatch env t ty ty' ast_term
-
-let make_pred env ast_term p =
- try
- Expr.Formula.pred p
- with Expr.Type_mismatch (t, ty, ty') ->
- _type_mismatch env t ty ty' ast_term
-
-let mk_quant_ty env mk vars body =
- (* Check that all quantified variables are actually used *)
- let fv_ty, fv_t = Expr.Formula.fv body in
- let unused = List.filter (fun v -> not @@ CCList.mem ~eq:Expr.Id.equal v fv_ty) vars in
- List.iter (fun v ->
- Util.warn "%a:@\nQuantified variables unused: %a"
- Dolmen.ParseLocation.fmt (get_reason_loc (E.find v env.type_locs))
- Expr.Print.id v) unused;
- mk vars body
-
-let mk_quant_term env mk vars body =
- (* Check that all quantified variables are actually used *)
- let fv_ty, fv_t = Expr.Formula.fv body in
- let unused = List.filter (fun v -> not @@ CCList.mem ~eq:Expr.Id.equal v fv_t) vars in
- List.iter (fun v ->
- Util.warn "%a:@\nQuantified variables unused: %a"
- Dolmen.ParseLocation.fmt (get_reason_loc (F.find v env.term_locs))
- Expr.Print.id v) unused;
- mk vars body
-
-let promote env ast t =
- match t with
- | Term t when Expr.(Ty.equal Ty.prop t.t_type) ->
- Formula (make_pred env ast t)
- | _ -> t
-
-let infer env ast s args loc =
- if Dolmen.Id.(s.ns = Var) then _infer_var env ast;
- match env.expect with
- | Nothing -> None
- | Type ->
- let n = List.length args in
- let ret = Expr.Id.ty_fun (Id.full_name s) n in
- let res = Ty_fun ret in
- env.infer_hook env res;
- decl_ty_cstr s ret (Inferred loc);
- Some res
- | Typed ty ->
- let n = List.length args in
- let ret = Expr.Id.term_fun (Id.full_name s) [] (CCList.replicate n Expr.Ty.base) ty in
- let res = Term_fun ret in
- env.infer_hook env res;
- decl_term s ret (Inferred loc);
- Some res
-
-
-(* Tag application *)
-(* ************************************************************************ *)
-
-let apply_tag env ast tag v = function
- | Ttype -> raise (Typing_error ("Cannot tag Ttype", env, ast))
- | Tags _ -> raise (Typing_error ("Cannot tag a tag list", env, ast))
- | Ty ty -> Expr.Ty.tag ty tag v
- | Term t -> Expr.Term.tag t tag v
- | Formula f -> Expr.Formula.tag f tag v
-
-(* Expression parsing *)
-(* ************************************************************************ *)
-
-let rec parse_expr (env : env) t =
- Util.debug ~section
- "parsing: @[<hov>%a@]@\nin env: @[<hov>%a@]"
- Ast.print t pp_env env;
- let res = match t with
-
- (* Ttype & builtin types *)
- | { Ast.term = Ast.Builtin Ast.Ttype } ->
- Ttype
- | { Ast.term = Ast.Builtin Ast.Prop } ->
- Ty Expr.Ty.prop
-
- (* Wildcards (only allowed in types *)
- | { Ast.term = Ast.Builtin Ast.Wildcard } ->
- Ty (Expr.Ty.of_id (gen_wildcard ()))
-
- (* 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.f_and (List.map (parse_formula env) l))
-
- | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Or}, l) } ->
- Formula (Expr.Formula.f_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.neg (Expr.Formula.equiv f g))
- | _ -> _bad_op_arity env "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.imply f g)
- | _ -> _bad_op_arity env "=>" 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.equiv f g)
- | _ -> _bad_op_arity env "<=>" 2 t
- end
-
- | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Not}, l) } as t ->
- begin match l with
- | [p] ->
- Formula (Expr.Formula.neg (parse_formula env p))
- | _ -> _bad_op_arity env "not" 1 t
- end
-
- (* Binders *)
- | { Ast.term = Ast.Binder (Ast.All, vars, f) } ->
- let ttype_vars, ty_vars, env' =
- parse_quant_vars (expect env (Typed Expr.Ty.base)) vars in
- Formula (
- mk_quant_ty env' Expr.Formula.allty ttype_vars
- (mk_quant_term env' Expr.Formula.all ty_vars
- (parse_formula env' f)))
-
- | { Ast.term = Ast.Binder (Ast.Ex, vars, f) } ->
- let ttype_vars, ty_vars, env' =
- parse_quant_vars (expect env (Typed Expr.Ty.base)) vars in
- Formula (
- mk_quant_ty env' Expr.Formula.exty ttype_vars
- (mk_quant_term env' Expr.Formula.ex ty_vars
- (parse_formula env' f)))
-
- (* (Dis)Equality *)
- | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Eq}, l) } as t ->
- begin match l with
- | [a; b] ->
- begin match promote env t @@ parse_expr env a,
- promote env t @@ parse_expr env b with
- | Term t1, Term t2 ->
- Formula (make_eq env t t1 t2)
- | Formula f1, Formula f2 ->
- Formula (Expr.Formula.equiv f1 f2)
- | _ ->
- _expected env "either two terms or two formulas" t None
- end
- | _ -> _bad_op_arity env "=" 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'' = CCList.diagonal l' in
- let l''' = List.map (fun (a, b) -> Expr.Formula.neg (make_eq env t a b)) l'' in
- let f = match l''' with
- | [f] -> f
- | _ -> Expr.Formula.f_and l'''
- in
- Formula f
-
- (* 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 ("Unexpected construction", env, ast))
- in
- apply_attr env res t t.Ast.attr
-
-and apply_attr env res ast l =
- let () = List.iter (function
- | Any (tag, v) ->
- apply_tag env ast tag v res;
- ) (parse_attrs env ast [] l) in
- res
-
-and parse_attr_and env ast =
- match ast with
- | { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.And}, l) } ->
- parse_attrs env ast [] l
- | _ -> parse_attrs env ast [] [ast]
-
-and parse_attrs env ast acc = function
- | [] -> acc
- | a :: r ->
- begin match parse_expr (expect env Nothing) a with
- | Tags l ->
- parse_attrs env ast (l @ acc) r
- | res ->
- _expected env "tag" a (Some res)
- | exception (Typing_error (msg, _, t)) ->
- Util.warn ~section "%a while parsing an attribute:@\n%s"
- Dolmen.ParseLocation.fmt (get_loc t) msg;
- parse_attrs env ast acc r
- end
-
-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 (Id.full_name s))
- | Ty ty -> `Term (s, Expr.Id.ty (Id.full_name s) ty)
- | res -> _expected env "type (or Ttype)" e (Some res)
- end
- | { Ast.term = Ast.Symbol s } as t ->
- begin match env.expect with
- | Nothing -> _cannot_infer_quant_var env t
- | Type -> `Ty (s, Expr.Id.ttype (Id.full_name s))
- | Typed ty -> `Term (s, Expr.Id.ty (Id.full_name s) ty)
- end
- | t -> _expected env "(typed) variable" t None
-
-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' (get_loc v) in
- (v'' :: l1, l2, acc')
- | `Term (id, v') ->
- let v'', acc' = add_term_var acc id v' (get_loc 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
- | res -> _expected env "term or formula" e (Some res)
- end
- | t -> _expected env "let-binding" t None
- end
-
-and parse_app env ast s args =
- match find_let env s with
- | `Term t ->
- if args = [] then Term t
- else _fo_let env s ast
- | `Prop p ->
- if args = [] then Formula p
- else _fo_let env s ast
- | `Not_found ->
- begin match find_var env s with
- | `Ty f ->
- if args = [] then Ty (Expr.Ty.of_id f)
- else _fo_let env s ast
- | `Term f ->
- if args = [] then Term (Expr.Term.of_id f)
- else _fo_let env 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 env.builtins env ast s args with
- | Some res -> res
- | None ->
- begin match infer env ast s args (get_loc ast) with
- | Some Ty_fun f -> parse_app_ty env ast f args
- | Some Term_fun f -> parse_app_term env ast f args
- | None ->
- Util.error ~section
- "Looking up '%a' failed, possibilities were:@ @[<hov>%a@]"
- Id.print s (suggest ~limit:1 env) s;
- raise (Typing_error (
- Format.asprintf "Scoping error: '%a' not found" Id.print s, env, ast))
- end
- 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_args = List.length args in
- let n_ty = List.length Expr.(f.id_type.fun_vars) in
- let n_t = List.length Expr.(f.id_type.fun_args) in
- let ty_l, t_l =
- if n_args = n_ty + n_t then
- CCList.take_drop n_ty args
- else if n_args = n_t then
- (CCList.replicate n_ty Dolmen.Term.wildcard, args)
- else
- _bad_term_arity env f (n_ty + n_t) ast
- 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_formula env ast f args =
- if args = [] then Formula f
- else _fo_formula env f ast
-
-and parse_app_subst_ty env ast id args f_args body =
- let l = List.map (parse_ty env) args in
- Ty (ty_subst env 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 = CCList.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 env ast id ty_args t_args f_ty_args f_t_args body)
-
-and parse_ty env ast =
- match parse_expr (expect env Type) ast with
- | Ty ty -> ty
- | res -> _expected env "type" ast (Some res)
-
-and parse_term env ast =
- match parse_expr (expect env (Typed Expr.Ty.base)) ast with
- | Term t -> t
- | res -> _expected env "term" ast (Some res)
-
-and parse_formula env ast =
- match promote env ast @@ parse_expr (expect env (Typed Expr.Ty.prop)) ast with
- | Formula p -> p
- | res -> _expected env "formula" ast (Some res)
-
-let parse_ttype_var env t =
- match parse_var (expect ~force:true env Type) t with
- | `Ty (id, v) -> (id, v, get_loc t)
- | `Term (_, v) ->
- _expected env "type variable" t (Some (Term (Expr.Term.of_id v)))
-
-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", env, h))
- | [] ->
- let aux n = function
- | (_, Ttype) -> n + 1
- | (ast, res) -> raise (Found (ast, res))
- 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,", env, err))
- end
- end
- | Ty ret ->
- let aux acc = function
- | (_, Ty t) -> t :: acc
- | (ast, res) -> raise (Found (ast, res))
- in
- begin
- match List.fold_left aux [] ty_args with
- | exception Found (err, res) -> _expected env "type" err (Some res)
- | l -> `Fun_ty (List.map snd ttype_vars, List.rev l, ret)
- end
- | res -> _expected env "Ttype of type" t (Some res)
- end
-
-and parse_sig_args env l =
- CCList.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
- | (Ty body) as res ->
- if t_args = [] then `Ty (ty_args, body)
- else _expected env "non_dependant type (or a term)" ast (Some res)
- | Term body -> `Term (ty_args, t_args, body)
- | res -> _expected env "term or a type" ast (Some res)
- end
-
-(* High-level parsing functions *)
-(* ************************************************************************ *)
-
-let new_decl env t ?attr id =
- Util.enter_prof section;
- Util.debug ~section "Typing declaration:@ @[<hov>%a :@ %a@]"
- Id.print id Ast.print t;
- let aux acc (Any (tag, v)) = Tag.add acc tag v in
- let tags =
- CCOpt.map (fun a ->
- Util.debug ~section "Typing attribute:@ @[<hov>%a@]" Ast.print a;
- let l = parse_attr_and env a in
- List.fold_left aux Tag.empty l) attr
- in
- let res =
- match parse_sig env t with
- | `Ty_cstr n ->
- let c = Expr.Id.ty_fun ?tags (Id.full_name id) n in
- decl_ty_cstr id c (Declared (get_loc t));
- `Type_decl c
- | `Fun_ty (vars, args, ret) ->
- let f = Expr.Id.term_fun ?tags (Id.full_name id) vars args ret in
- decl_term id f (Declared (get_loc t));
- `Term_decl f
- in
- Util.exit_prof section;
- res
-
-let new_def env t ?attr id =
- Util.enter_prof section;
- Util.debug ~section "Typing definition:@ @[<hov>%a =@ %a@]"
- Id.print id Ast.print t;
- let res =
- match parse_fun [] [] env t with
- | `Ty (ty_args, body) ->
- def_ty id ty_args body;
- `Type_def (id, ty_args, body)
- | `Term (ty_args, t_args, body) ->
- def_term id ty_args t_args body;
- `Term_def (id, ty_args, t_args, body)
- in
- Util.exit_prof section;
- res
-
-let new_formula env t =
- Util.enter_prof section;
- Util.debug ~section "Typing top-level formula:@ %a" Ast.print t;
- let res = parse_formula env t in
- Util.exit_prof section;
- res
-
diff --git a/src/bin/witan.ml b/src/bin/witan.ml
deleted file mode 100644
index f250b7564479bc6cd1418458320aa6f163627d0d..0000000000000000000000000000000000000000
--- a/src/bin/witan.ml
+++ /dev/null
@@ -1,61 +0,0 @@
-(*************************************************************************)
-(* This file is part of Colibrics. *)
-(* *)
-(* Copyright (C) 2017 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(*************************************************************************)
-
-let theories = Witan_theories_bool.[Boolean.th_register; Equality.th_register; Uninterp.th_register ]
-
-
-let () =
- if not Witan_core.(Egraph.check_initialization () &&
- Conflict.check_initialization ()) then
- exit 1
-
-
-let one_file opts file =
- (* Parse input *)
- let statements = Witan_solver.Input.read
- ?language:Options.(opts.input.language)
- ~dir:Options.(opts.input.dir)
- file
- in
- if opts.Options.type_only then exit 0;
- let res =
- Witan_solver.Notypecheck.run
- ?limit:(if opts.Options.step_limit < 0 then None else Some opts.Options.step_limit)
- ~theories statements in
- match res with
- | `Unsat -> Printf.printf "unsat\n"
- | `Sat -> Printf.printf "sat\n"
-
-let () =
- (* Parse command line options *)
- let opts = match Cmdliner.Term.eval (Options.all, Options.info) with
- | `Version | `Help -> exit 0
- | `Error `Parse
- | `Error `Term
- | `Error `Exn -> exit 1
- | `Ok opts -> opts
- in
- List.iter (fun f -> Witan_popop_lib.Debug.set_flag f) opts.Options.debug_flags;
- Witan_popop_lib.Debug.(if test_flag stack_trace then Printexc.record_backtrace true);
- begin match opts.Options.seed_shuffle with
- | None -> Witan_stdlib.Shuffle.set_shuffle None;
- | Some i -> Witan_stdlib.Shuffle.set_shuffle (Some [|i|]);
- end;
- one_file opts Options.(opts.input.file)
diff --git a/src/core/egraph.ml b/src/core/egraph.ml
index a17c16ddf0ee9b890fa271bdfb6f73a40cf8e191..67698331927f24484207b0b7d94ce6f7852ddae6 100644
--- a/src/core/egraph.ml
+++ b/src/core/egraph.ml
@@ -22,7 +22,7 @@ open Witan_popop_lib
open Popop_stdlib
open Nodes
-exception Contradiction of Trail.Pexp.t
+exception Contradiction
let debug = Debug.register_info_flag
~desc:"for the core solver"
@@ -88,7 +88,6 @@ module Def = struct
sem : semtable VSemTable.t;
value : unit VValueTable.t;
envs : Env.VectorH.t;
- trail : Trail.t;
mutable current_delayed : delayed_t; (** For assert-check *)
history : saved Context.history;
}
@@ -98,11 +97,11 @@ module Def = struct
env : t;
todo_immediate_dem : action_immediate_dem Queue.t;
todo_merge_dom : action_merge_dom Queue.t;
- mutable todo_delayed_merge : (Trail.Pexp.t * Node.t * Node.t * bool) option;
+ mutable todo_delayed_merge : (Node.t * Node.t * bool) option;
todo_merge : action_merge Queue.t;
todo_ext_action : action_ext Queue.t;
sched_daemon : Events.Wait.daemon_key -> unit;
- sched_decision : Trail.chogen -> unit;
+ sched_decision : choice -> unit;
}
and action_immediate_dem =
@@ -110,17 +109,36 @@ module Def = struct
and action_merge_dom =
| SetMergeDomNode :
- Trail.Pexp.t * 'a DomKind.t * Node.t * Node.t * bool -> action_merge_dom
+ 'a DomKind.t * Node.t * Node.t * bool -> action_merge_dom
and action_merge =
- | Merge of Trail.Pexp.t * Node.t * Node.t
+ | Merge of Node.t * Node.t
and action_ext =
| ExtDem : Events.Wait.daemon_key -> action_ext
+ and choice_state =
+ | DecNo
+ | DecTodo of (delayed_t -> unit)
+
+ and choice = {
+ choice: delayed_t -> choice_state;
+ prio: int;
+ }
+
end
open Def
+
+
+type choice = Def.choice = {
+ choice: delayed_t -> choice_state;
+ prio: int;
+}
+type choice_state = Def.choice_state =
+ | DecNo
+ | DecTodo of (delayed_t -> unit)
+
(** {2 Define events} *)
module WaitDef = struct
@@ -135,7 +153,7 @@ module Wait : Events.Wait.S with type delayed = delayed_t and type delayed_ro =
Events.Wait.Make(WaitDef)
(** {2 Define domain registration} *)
-module VDom = DomKind.Make(struct type delayed = delayed_t type pexp = Trail.Pexp.t end)
+module VDom = DomKind.Make(struct type delayed = delayed_t end)
include VDom
let mk_dumb_delayed () = { env = Obj.magic 0;
@@ -312,10 +330,6 @@ let output_graph filename t =
ValueKind.pp value (escape_for_dot (print_value value) s);
with Not_found -> ()
in
- let print_ty fmt node =
- if is_repr t node
- then Format.fprintf fmt ": %a" Ty.pp (Node.ty node)
- in
let print_sem fmt node =
match Only_for_solver.thterm node with
| None -> ()
@@ -326,9 +340,8 @@ let output_graph filename t =
Format.fprintf fmt "| {%a | %s}"
ThTermKind.pp sem (escape_for_dot S.pp v)
in
- Format.fprintf fmt "{%a %a %a %a %a}" (* "{%a | %a | %a}" *)
+ Format.fprintf fmt "{%a %a %a %a}" (* "{%a | %a | %a}" *)
Node.pp node
- print_ty node
print_sem node
(if is_repr t node
then VDomTable.pp Format.silent Format.silent
@@ -436,15 +449,14 @@ module Delayed = struct
let events = Node.M.find_opt node t.env.event_value in
Wait.wakeup_events_bag Events.Wait.translate_value t events (node,value)
- let add_pending_merge (t : t) pexp node node' =
+ let add_pending_merge (t : t) node node' =
Debug.dprintf4 debug "[Egraph] @[add_pending_merge for %a and %a@]"
Node.pp node Node.pp node';
assert (is_registered t node);
assert (is_registered t node');
assert (not (Node.equal (find t node) (find t node')));
- assert (Ty.equal (Node.ty node) (Node.ty node'));
(* Add the actual merge for later *)
- Queue.add (Merge (pexp,node,node')) t.todo_merge
+ Queue.add (Merge (node,node')) t.todo_merge
let check_no_dom t node =
let foldi acc _dom (domtable: _ domtable) =
@@ -493,9 +505,8 @@ module Delayed = struct
end
end
- let set_semvalue_pending t pexp node0 node0' =
+ let set_semvalue_pending t node0 node0' =
let node = find t node0 in
- assert (Ty.equal (Node.ty node) (Node.ty node0'));
begin
if not (is_registered t node0') then begin
register t node0';
@@ -505,15 +516,6 @@ module Delayed = struct
termination.
*)
t.env.repr <- Node.M.add node0' node t.env.repr;
- let pexp = pexp () in
- Trail.add_merge_start t.env.trail pexp
- ~node1:node0 ~node2:node0'
- ~node1_repr:node ~node2_repr:node0'
- ~new_repr:node;
- Trail.add_merge_finish t.env.trail pexp
- ~node1:node0 ~node2:node0'
- ~node1_repr:node ~node2_repr:node0'
- ~new_repr:node;
(** wakeup the daemons register_node *)
let event, other_event = Node.M.find_remove node0' t.env.event_repr in
Wait.wakeup_events_bag Events.Wait.translate_change t other_event node0';
@@ -532,23 +534,16 @@ module Delayed = struct
()
else
(** merge node and node0' *)
- let pexp = pexp () in
- add_pending_merge t pexp node0 node0'
+ add_pending_merge t node0 node0'
end
- let set_sem_pending t pexp node0 thterm =
+ let set_sem_pending t node0 thterm =
let node0' = ThTerm.node thterm in
- let pexp () =
- Trail.mk_pexp t.env.trail Trail.exp_same_sem
- (ExpSameSem(pexp,node0,thterm)) in
- set_semvalue_pending t pexp node0 node0'
+ set_semvalue_pending t node0 node0'
- let set_value_pending t pexp node0 nodevalue =
+ let set_value_pending t node0 nodevalue =
let node0' = Value.node nodevalue in
- let pexp () =
- Trail.mk_pexp t.env.trail Trail.exp_same_sem
- (ExpSameValue(pexp,node0,nodevalue)) in
- set_semvalue_pending t pexp node0 node0'
+ set_semvalue_pending t node0 node0'
let set_dom_pending (type a) t (dom : a DomKind.t) node0 new_v =
Debug.incr stats_set_dom;
@@ -597,7 +592,7 @@ module Delayed = struct
else
heuristic ()
- let merge_dom_pending (type a) t pexp (dom : a DomKind.t) node1_0 node2_0 inv =
+ let merge_dom_pending (type a) t (dom : a DomKind.t) node1_0 node2_0 inv =
let node1 = find t node1_0 in
let node2 = find t node2_0 in
let domtable = (get_table_dom t.env dom) in
@@ -613,13 +608,13 @@ module Delayed = struct
match old_other_s, old_repr_s with
| None, None -> ()
| _ ->
- Dom.merge t pexp
+ Dom.merge t
(old_other_s,node1_0)
(old_repr_s,node2_0)
inv
- let merge_dom ?(dry_run=false) t pexp node1_0 node2_0 inv =
+ let merge_dom ?(dry_run=false) t node1_0 node2_0 inv =
let node1 = find t node1_0 in
let node2 = find t node2_0 in
let dom_not_done = ref false in
@@ -632,13 +627,13 @@ module Delayed = struct
dom_not_done := true;
if not dry_run then
Queue.push
- (SetMergeDomNode(pexp,dom,node1_0,node2_0,inv)) t.todo_merge_dom
+ (SetMergeDomNode(dom,node1_0,node2_0,inv)) t.todo_merge_dom
end
in
VDomTable.iter_initializedi {VDomTable.iteri} t.env.dom;
!dom_not_done
- let merge_values t pexp node0 node0' =
+ let merge_values t node0 node0' =
let node = find t node0 in
let node' = find t node0' in
let iteri (type a) (value:a ValueKind.t) (valuetable:a valuetable) =
@@ -664,29 +659,20 @@ module Delayed = struct
(* already same value. Does that really happen? *)
()
else
- let ty = Node.ty node in
- let v = Value.index value v ty in
- let v' = Value.index value v' ty in
- let pexp = Trail.mk_pexp t.env.trail Trail.exp_diff_value (v,node0,node0',v',pexp) in
- raise (Contradiction pexp)
+ raise Contradiction
in
VValueTable.iter_initializedi {VValueTable.iteri} t.env.value
- let finalize_merge t pexp node1_0 node2_0 inv =
+ let finalize_merge t node1_0 node2_0 inv =
let node1 = find t node1_0 in
let node2 = find t node2_0 in
let other_node0,other_node,repr_node0,repr_node =
if inv
then node2_0,node2, node1_0, node1
else node1_0, node1, node2_0, node2 in
- merge_values t pexp node1_0 node2_0;
+ merge_values t node1_0 node2_0;
t.env.repr <- Node.M.add other_node repr_node t.env.repr;
- Trail.add_merge_finish t.env.trail pexp
- ~node1:node1_0 ~node2:node2_0
- ~node1_repr:node1 ~node2_repr:node2
- ~new_repr:repr_node;
- Debug.dprintf10 debug_few "[Egraph.few] [%a] merge %a(%a) -> %a(%a)"
- Trail.print_current_age t.env.trail
+ Debug.dprintf8 debug_few "[Egraph.few] merge %a(%a) -> %a(%a)"
Node.pp other_node Node.pp other_node0
Node.pp repr_node Node.pp repr_node0;
let event, other_event = Node.M.find_remove other_node t.env.event_repr in
@@ -730,30 +716,26 @@ module Delayed = struct
Wait.wakeup_events_bag
Events.Wait.translate_change t other_event other_node
- let do_delayed_merge t pexp node1_0 node2_0 inv =
- let dom_not_done = merge_dom t pexp node1_0 node2_0 inv in
+ let do_delayed_merge t node1_0 node2_0 inv =
+ let dom_not_done = merge_dom t node1_0 node2_0 inv in
if dom_not_done
then begin
Debug.dprintf4 debug "[Egraph] @[merge %a %a dom not done@]"
Node.pp node1_0 Node.pp node2_0;
- t.todo_delayed_merge <- Some (pexp,node1_0,node2_0,inv)
+ t.todo_delayed_merge <- Some (node1_0,node2_0,inv)
end
else
- finalize_merge t pexp node1_0 node2_0 inv
+ finalize_merge t node1_0 node2_0 inv
(** merge two pending actions *)
- let merge_pending t pexp node1_0 node2_0 =
+ let merge_pending t node1_0 node2_0 =
let node1 = find t node1_0 in
let node2 = find t node2_0 in
if not (Node.equal node1 node2) then begin
- let ((other_node0,_),(_,repr_node)) =
+ let ((other_node0,_),(_,_)) =
choose_repr t.env (node1_0,node1) (node2_0,node2) in
let inv = not (Node.equal node1_0 other_node0) in
- Trail.add_merge_start t.env.trail pexp
- ~node1:node1_0 ~node2:node2_0
- ~node1_repr:node1 ~node2_repr:node2
- ~new_repr:repr_node;
- do_delayed_merge t pexp node1_0 node2_0 inv
+ do_delayed_merge t node1_0 node2_0 inv
end
(** {2 Internal scheduler} *)
@@ -790,26 +772,26 @@ module Delayed = struct
do_pending t
else if not (Queue.is_empty t.todo_merge_dom) then
match Queue.pop t.todo_merge_dom with
- | SetMergeDomNode(pexp,dom,node1,node2,inv) ->
+ | SetMergeDomNode(dom,node1,node2,inv) ->
Debug.dprintf6 debug "[Egraph] @[do_pending SetDomNode %a %a %a@]"
DomKind.pp dom Node.pp node1 Node.pp node2;
- merge_dom_pending t pexp dom node1 node2 inv;
+ merge_dom_pending t dom node1 node2 inv;
do_pending t
else match t.todo_delayed_merge with
- | Some(pexp,node1_0,node2_0,inv) ->
+ | Some(node1_0,node2_0,inv) ->
t.todo_delayed_merge <- None;
- assert (not (merge_dom ~dry_run:true t pexp node1_0 node2_0 inv));
+ assert (not (merge_dom ~dry_run:true t node1_0 node2_0 inv));
(** understand why that happend.
Is it really needed to do a fixpoint? *)
- do_delayed_merge t pexp node1_0 node2_0 inv;
+ do_delayed_merge t node1_0 node2_0 inv;
do_pending t
| None ->
if not (Queue.is_empty t.todo_merge) then
match Queue.pop t.todo_merge with
- | Merge (pexp,node1,node2) ->
+ | Merge (node1,node2) ->
Debug.dprintf4 debug "[Egraph] @[do_pending Merge %a %a@]"
Node.pp node1 Node.pp node2;
- merge_pending t pexp node1 node2;
+ merge_pending t node1 node2;
do_pending t
else if not (Queue.is_empty t.todo_ext_action) then
(begin match Queue.pop t.todo_ext_action with
@@ -845,29 +827,29 @@ module Delayed = struct
(** {2 API} *)
- let merge t pexp node1_0 node2_0 =
+ let merge t node1_0 node2_0 =
assert (is_current_env t);
if not (Node.equal
(find t node1_0)
(find t node2_0)) then
- add_pending_merge t pexp node1_0 node2_0
+ add_pending_merge t node1_0 node2_0
let check d node =
assert (Equal.physical d.env.current_delayed d);
assert (is_registered d node)
- let set_thterm d pexp node thterm =
+ let set_thterm d node thterm =
Debug.dprintf4 debug "[Egraph] @[add_pending_set_thterm for %a and %a@]"
Node.pp node ThTerm.pp thterm;
check d node;
- set_sem_pending d pexp node thterm
+ set_sem_pending d node thterm
- let set_value d pexp node nodevalue =
+ let set_value d node nodevalue =
Debug.dprintf4 debug_few
"[Egraph] @[set_value for %a with %a@]"
Node.pp node Value.pp nodevalue;
check d node;
- set_value_pending d pexp node nodevalue
+ set_value_pending d node nodevalue
let set_dom d dom node v =
Debug.dprintf4 debug_few
@@ -882,8 +864,8 @@ module Delayed = struct
Node.pp node (print_dom dom) v;
check d node;
let node' = match d.todo_delayed_merge with
- | Some(_,node1,node2,_) when Node.equal node1 node -> node2
- | Some(_,node1,node2,_) when Node.equal node2 node -> node1
+ | Some(node1,node2,_) when Node.equal node1 node -> node2
+ | Some(node1,node2,_) when Node.equal node2 node -> node1
| _ -> raise (BrokenInvariant(
"set_dom_premerge should be used only on the \
nodeasses currently merged")) in
@@ -899,13 +881,9 @@ module Delayed = struct
let register_decision t chogen =
t.sched_decision chogen
- let mk_pexp t ?age kexp exp = Trail.mk_pexp ?age t.env.trail kexp exp
- let current_age t = Trail.current_age t.env.trail
- let add_pexp t pexp = Trail.add_pexp t.env.trail pexp
-
- let contradiction d pexp =
+ let contradiction d =
d.env.current_delayed <- unsat_delayed;
- raise (Contradiction pexp)
+ raise Contradiction
(** {2 API for attaching event} *)
@@ -1007,7 +985,6 @@ module Backtrackable = struct
sem = VSemTable.create 5;
value = VValueTable.create 5;
envs = Env.VectorH.create 5;
- trail = Trail.create context;
current_delayed = dumb_delayed;
history = Hidden.create context;
}
@@ -1107,27 +1084,10 @@ module Backtrackable = struct
assert (check_disabled_delayed t);
T.find_def t node
- let get_trail t =
- let t = Hidden.ro t in
- (* assert (check_disabled_delayed t); *)
- t.trail
-
let get_getter t =
(* assert (check_disabled_delayed t); *)
t
- let new_dec t =
- let t = Hidden.ro t in
- assert (check_disabled_delayed t);
- Trail.new_dec t.trail
-
- let current_age (t:t) =
- let t = Hidden.ro t in
- Trail.current_age t.trail
- let current_nbdec (t:t) =
- let t = Hidden.ro t in
- Trail.nbdec t.trail
-
let get_direct_dom t dom node =
assert (check_disabled_delayed t);
get_direct_dom t dom node
@@ -1184,3 +1144,5 @@ let () = Exn_printer.register (fun fmt exn ->
Format.fprintf fmt "The environnement of %s is not initialized." env
| exn -> raise exn
)
+
+let print_decision = Witan_popop_lib.Debug.register_flag ~desc:"Print@ information@ about@ the@ decisions@ made" "decision"
diff --git a/src/core/egraph.mli b/src/core/egraph.mli
index afadd49b668921eaf4a7a3a5b65a4d4e565008f1..b140de46f1c69bbc83e9eccdd4ad62623344eaa5 100644
--- a/src/core/egraph.mli
+++ b/src/core/egraph.mli
@@ -24,14 +24,13 @@
equivalence classes, values. It take care to schedule event that
happened. *)
-open Trail
open Nodes
exception NotRegistered
exception UninitializedEnv of string
-exception Contradiction of Trail.Pexp.t
+exception Contradiction
module type Getter = sig
type t
@@ -82,13 +81,13 @@ val unset_dom : t -> 'a DomKind.t -> Node.t -> unit
(** {3 Delayed modifications} *)
-val set_thterm : t -> Trail.Pexp.t -> Node.t -> ThTerm.t -> unit
+val set_thterm : t -> Node.t -> ThTerm.t -> unit
(** attach a theory term to an equivalence class *)
-val set_value: t -> Trail.Pexp.t -> Node.t -> Value.t -> unit
+val set_value: t -> Node.t -> Value.t -> unit
(** attach value to an equivalence class *)
-val merge : t -> Trail.Pexp.t -> Node.t -> Node.t -> unit
+val merge : t -> Node.t -> Node.t -> unit
(** {3 Attach Event} *)
@@ -107,16 +106,21 @@ val attach_reg_value: t -> 'a ValueKind.t -> ('event,'r) Events.Dem.t -> 'event
val attach_node: t -> Node.t -> ('event,'r) Events.Dem.t -> 'event -> unit
(** wakeup when it is not anymore the representative class *)
-val register_decision: t -> Trail.chogen -> unit
+type choice_state =
+ | DecNo
+ | DecTodo of (t -> unit)
+
+type choice = {
+ choice: t -> choice_state;
+ prio: int;
+}
+
+val register_decision: t -> choice -> unit
(** register a decision that would be scheduled later. The
[choose_decision] of the [Cho] will be called at that time to know
if the decision is still needed. *)
-(** {3 Trails} *)
-val mk_pexp: t -> ?age:age -> 'a Exp.t -> 'a -> Trail.Pexp.t
-val current_age: t -> age
-val add_pexp: t -> Trail.Pexp.t -> unit
-val contradiction: t -> Trail.Pexp.t -> 'b
+val contradiction: t -> 'b
(** {3 Low level} *)
val flush_internal: t -> unit
@@ -129,7 +133,7 @@ module Wait : Events.Wait.S with type delayed = t and type delayed_ro = Ro.t
(** {2 Domains and Semantic Values key creation} *)
-module type Dom = DomKind.Dom_partial with type delayed := t and type pexp := Trail.Pexp.t
+module type Dom = DomKind.Dom_partial with type delayed := t
val register_dom : (module Dom with type t = 'a) -> unit
@@ -150,7 +154,7 @@ module Backtrackable: sig
val new_delayed :
sched_daemon:(Events.Wait.daemon_key -> unit) ->
- sched_decision:(chogen -> unit) ->
+ sched_decision:(choice -> unit) ->
t -> delayed
(** The solver shouldn't be used anymore before
calling flush. (flushd doesn't count)
@@ -171,13 +175,11 @@ module Backtrackable: sig
(* val make_decisions : delayed -> attached_daemons -> unit *)
- val get_trail : t -> Trail.t
val get_getter : t -> Getter.t
- val new_dec : t -> Trail.dec
- val current_age : t -> Trail.Age.t
- val current_nbdec : t -> int
(** Debug *)
val draw_graph: ?force:bool -> t -> unit
val output_graph : string -> t -> unit
end
+
+val print_decision: Witan_popop_lib.Debug.flag
diff --git a/src/core/interp.ml b/src/core/interp.ml
index ebc5b6da1e2005f135c300b1076dfbd195d6991e..e2733450db5c75283ee889fb1bd1cf1ebadce5ba 100644
--- a/src/core/interp.ml
+++ b/src/core/interp.ml
@@ -20,10 +20,10 @@
open Witan_popop_lib
open Std
-
-module Register = struct
- let ids : (Term.id -> Nodes.Value.t list -> Nodes.Value.t option) list ref = ref []
+module Register = struct
+ type interp_term = Dolmen_std.Expr.Term.t -> Nodes.Value.t
+ let ids : (interp_term -> Dolmen_std.Expr.Term.t -> Nodes.Value.t option) list ref = ref []
let id f = ids := f::!ids
module ThInterp = Nodes.ThTermKind.MkVector(struct
@@ -42,42 +42,25 @@ module Register = struct
end
-exception NoInterpretation of Term.id
-exception CantInterpretTerm of Term.t
+exception CantInterpretTerm of Dolmen_std.Expr.Term.t
exception CantInterpretThTerm of Nodes.ThTerm.t
-type leaf = Term.t -> Nodes.Value.t option
+type leaf = Dolmen_std.Expr.Term.t -> Nodes.Value.t option
(** No cache currently because there is no guaranty
that the variable in the let is unique *)
let term ?(leaf=(fun _ -> None)) t =
- let rec interp leaf t =
- match leaf t with
- | Some v -> v
- | None ->
- let rec aux leaf args = function
- | { Term.term = App (f, arg); _ } ->
- aux leaf ((interp leaf arg) :: args) f
- | { Term.term = Let (v,e,t); _ } ->
- let v' = interp leaf e in
- let leaf t = match t.Term.term with
- | Id id when Term.Id.equal v id -> Some v'
- | _ -> leaf t in
- aux leaf args t
- | { Term.term = Id id; _ } ->
- let rec find = function
- | [] -> raise (NoInterpretation id)
- | f::l ->
- match f id args with
- | None -> find l
- | Some v -> v
- in
- find !Register.ids
- | t -> raise (CantInterpretTerm t)
+ let rec interp regl t =
+ let rec aux t = function
+ | [] -> raise (CantInterpretTerm t)
+ | a::l ->
+ match a (interp regl) t with
+ | Some v -> v
+ | None -> aux t l
in
- aux leaf [] t
+ aux t regl
in
- interp leaf t
+ interp ((fun _ -> leaf)::!Register.ids) t
let rec node ?(leaf=(fun _ -> None)) n =
match Nodes.Only_for_solver.open_node n with
@@ -89,25 +72,22 @@ and thterm ?(leaf=(fun _ -> None)) t =
| Nodes.Only_for_solver.ThTerm (sem,v) ->
(** check if it is not a synterm *)
match Nodes.ThTermKind.Eq.eq_type sem SynTerm.key with
- | Poly.Eq -> term ~leaf (v:Term.t)
+ | Poly.Eq -> term ~leaf (v:Expr.Term.t)
| Poly.Neq ->
if Register.ThInterp.is_uninitialized Register.thterms sem
then raise (CantInterpretThTerm t);
(Register.ThInterp.get Register.thterms sem) ~interp:(node ~leaf) v
-let model d n =
- match Ty.H.find_opt Register.models (Nodes.Node.ty n) with
- | None -> invalid_arg "Uninterpreted type"
- | Some f -> f d n
+(* let model d n =
+ * match Ty.H.find_opt Register.models (Nodes.Node.ty n) with
+ * | None -> invalid_arg "Uninterpreted type"
+ * | Some f -> f d n *)
let () = Exn_printer.register (fun fmt exn ->
match exn with
- | NoInterpretation id ->
- Format.fprintf fmt "Can't interpret the id %a."
- Term.Id.pp id
| CantInterpretTerm t ->
Format.fprintf fmt "Can't interpret the term %a."
- Term.pp t
+ Dolmen_std.Expr.Term.print t
| CantInterpretThTerm th ->
Format.fprintf fmt "Can't interpret the thterm %a."
Nodes.ThTerm.pp th
diff --git a/src/core/interp.mli b/src/core/interp.mli
index a56c00757224dc4a0c2ac5c2c485add6558eff49..76a77f9ef46424eac781c493c312ba4d7b4fa215 100644
--- a/src/core/interp.mli
+++ b/src/core/interp.mli
@@ -20,18 +20,18 @@
module Register: sig
- val id: (Term.id -> Nodes.Value.t list -> Nodes.Value.t option) -> unit
+ val id: ((Dolmen_std.Expr.Term.t -> Nodes.Value.t) -> (Dolmen_std.Expr.Term.t -> Nodes.Value.t option)) -> unit
val thterm: 'a Nodes.ThTermKind.t -> (interp:(Nodes.Node.t -> Nodes.Value.t) -> 'a -> Nodes.Value.t) -> unit
- val model: Ty.t -> (Egraph.t -> Nodes.Node.t -> Nodes.Value.t) -> unit
+ (* val model: Ty.t -> (Egraph.t -> Nodes.Node.t -> Nodes.Value.t) -> unit *)
end
-type leaf = Term.t -> Nodes.Value.t option
+type leaf = Dolmen_std.Expr.Term.t -> Nodes.Value.t option
-val term : ?leaf:leaf -> Term.t -> Nodes.Value.t
+val term : ?leaf:leaf -> Dolmen_std.Expr.Term.t -> Nodes.Value.t
val thterm : ?leaf:leaf -> Nodes.ThTerm.t -> Nodes.Value.t
val node : ?leaf:leaf -> Nodes.Node.t -> Nodes.Value.t
-val model : Egraph.t -> Nodes.Node.t -> Nodes.Value.t
+(* val model : Egraph.t -> Nodes.Node.t -> Nodes.Value.t *)
diff --git a/src/core/structures/domKind.ml b/src/core/structures/domKind.ml
index 92625cce8eee9936c21d758fbf51160a9074ff1e..554a113678a95bede22c5abcd3c3a4f450c69cbb 100644
--- a/src/core/structures/domKind.ml
+++ b/src/core/structures/domKind.ml
@@ -31,21 +31,20 @@ type 'a dom = 'a t
module type Dom_partial = sig
type delayed
- type pexp
type t
val merged: t option -> t option -> bool
val merge: delayed ->
- pexp -> t option * Node.t -> t option * Node.t ->
+ t option * Node.t -> t option * Node.t ->
bool ->
unit
val pp: Format.formatter -> t -> unit
val key: t Dom.t
end
-module Make(S:sig type delayed type pexp end) = struct
+module Make(S:sig type delayed end) = struct
- module type Dom = Dom_partial with type delayed := S.delayed and type pexp := S.pexp
+ module type Dom = Dom_partial with type delayed := S.delayed
include Dom.Make_Registry(struct
type 'a data = (module Dom with type t = 'a)
diff --git a/src/core/structures/domKind.mli b/src/core/structures/domKind.mli
index 165c3f5e17a80457bff321b2e58ba6db00911e56..07abe1cf62749a9bec986110b47b7435bd38c3ed 100644
--- a/src/core/structures/domKind.mli
+++ b/src/core/structures/domKind.mli
@@ -29,21 +29,20 @@ type 'a dom = 'a t
(** delayed and pexp are instanciated in Egraph *)
module type Dom_partial = sig
type delayed
- type pexp
type t
val merged: t option -> t option -> bool
val merge: delayed ->
- pexp -> t option * Node.t -> t option * Node.t ->
+ t option * Node.t -> t option * Node.t ->
bool ->
unit
val pp: Format.formatter -> t -> unit
val key: t dom
end
-module Make (S:sig type delayed type pexp end) : sig
+module Make (S:sig type delayed end) : sig
- module type Dom = Dom_partial with type delayed := S.delayed and type pexp := S.pexp
+ module type Dom = Dom_partial with type delayed := S.delayed
val register_dom: (module Dom with type t = 'a) -> unit
val check_is_registered : 'a dom -> unit
diff --git a/src/core/structures/expr.ml b/src/core/structures/expr.ml
new file mode 100644
index 0000000000000000000000000000000000000000..35ec88fcc9e12b0de3aca3924cc69fc7de589b8d
--- /dev/null
+++ b/src/core/structures/expr.ml
@@ -0,0 +1,36 @@
+include Dolmen_std.Expr
+
+module Ty = struct
+ include Dolmen_std.Expr.Ty
+
+ let pp = print
+ let hash_fold_t state t = Base.Hash.fold_int state (hash t)
+
+ include Witan_popop_lib.Popop_stdlib.MkDatatype(struct
+ type nonrec t = t
+ let equal = equal
+ let compare = compare
+ let hash = hash
+ let pp = pp
+ end)
+
+end
+
+module Term = struct
+ include Dolmen_std.Expr.Term
+ let pp = print
+
+ include Witan_popop_lib.Popop_stdlib.MkDatatype(struct
+ type nonrec t = t
+ let equal = equal
+ let compare = compare
+ let hash = hash
+ let pp = pp
+ end)
+
+ module Const = struct
+ include Dolmen_std.Expr.Term.Const
+ let pp fmt (t:t) = Dolmen_std.Expr.Id.print fmt t
+ let hash_fold_t state t = Base.Hash.fold_int state (hash t)
+ end
+end
diff --git a/src/core/structures/nodes.ml b/src/core/structures/nodes.ml
index 361481a42a76bfaa17ca33dbb5aa0a3880ee1961..34954cb3beb7ddd66b6a0cde728404ca6978b46e 100644
--- a/src/core/structures/nodes.ml
+++ b/src/core/structures/nodes.ml
@@ -67,16 +67,16 @@ let get_value = ValueRegistry.get
module Node = struct
type 'a r =
- | ThTerm : int * Ty.t * 'a ThTermKind.t * 'a -> [`ThTerm] r
- | Value : int * Ty.t * 'a ValueKind.t * 'a -> [`Value] r
+ | ThTerm : int * 'a ThTermKind.t * 'a -> [`ThTerm] r
+ | Value : int * 'a ValueKind.t * 'a -> [`Value] r
type t' = All : _ r -> t' [@@unboxed]
type thterm = [`ThTerm] r
type nodevalue = [`Value] r
let tag: t' -> int = function
- | All(ThTerm(tag,_,_,_)) -> tag
- | All(Value(tag,_,_,_)) -> tag
+ | All(ThTerm(tag,_,_)) -> tag
+ | All(Value(tag,_,_)) -> tag
let names = Simple_vector.create 100
let used_names : (* next id to use *) int DStr.H.t = DStr.H.create 100
@@ -101,33 +101,29 @@ module Node = struct
let s = Strings.find_new_name used_names s in
Simple_vector.set names (tag node) s
- let ty = function
- | All(ThTerm(_,ty,_,_)) -> ty
- | All(Value(_,ty,_,_)) -> ty
-
module ThTermIndex = ThTermKind.MkVector
- (struct type ('a,_) t = 'a -> Ty.t -> thterm end)
+ (struct type ('a,_) t = 'a -> thterm end)
let semindex : unit ThTermIndex.t = ThTermIndex.create 8
- let thterm sem v ty : thterm =
+ let thterm sem v : thterm =
ThTermRegistry.check_is_registered sem;
- ThTermIndex.get semindex sem v ty
+ ThTermIndex.get semindex sem v
module ValueIndex = ValueKind.MkVector
- (struct type ('a,'unedeed) t = 'a -> Ty.t -> nodevalue end)
+ (struct type ('a,'unedeed) t = 'a -> nodevalue end)
let valueindex : unit ValueIndex.t = ValueIndex.create 8
- let nodevalue value v ty : nodevalue =
+ let nodevalue value v : nodevalue =
ValueRegistry.check_is_registered value;
- ValueIndex.get valueindex value v ty
+ ValueIndex.get valueindex value v
let of_thterm : thterm -> t = fun t -> All t
let of_nodevalue : nodevalue -> t = fun t -> All t
- let index_sem sem v ty = of_thterm (thterm sem v ty)
- let index_value sem v ty = of_nodevalue (nodevalue sem v ty)
+ let index_sem sem v = of_thterm (thterm sem v)
+ let index_value sem v = of_nodevalue (nodevalue sem v)
end
@@ -135,16 +131,13 @@ module ThTerm = struct
include Popop_stdlib.MakeMSH(struct
type t = Node.thterm
let tag: t -> int = function
- | Node.ThTerm(tag,_,_,_) -> tag
+ | Node.ThTerm(tag,_,_) -> tag
let pp fmt : t -> unit = function
- | Node.ThTerm(_,_,sem,v) -> print_thterm sem fmt v
+ | Node.ThTerm(_,sem,v) -> print_thterm sem fmt v
end)
let index = Node.thterm
let node = Node.of_thterm
- let ty : t -> Ty.t = function
- | Node.ThTerm(_,ty,_,_) -> ty
-
end
@@ -154,15 +147,12 @@ module type RegisteredThTerm = sig
(** thterm *)
include Datatype
- val index: s -> Ty.t -> t
+ val index: s -> t
(** Return a thterm from a semantical value *)
val node: t -> Node.t
(** Return a node from a thterm *)
- val ty: t -> Ty.t
- (** Return the type from a thterm *)
-
val sem: t -> s
(** Return the sem from a thterm *)
@@ -186,21 +176,21 @@ module RegisterThTerm (D:ThTerm) : RegisteredThTerm with type s = D.t = struct
let equal: t -> t -> bool = fun a b ->
match a, b with
- | ThTerm(_,tya,sema,va), ThTerm(_,tyb,semb,vb) ->
+ | ThTerm(_,sema,va), ThTerm(_,semb,vb) ->
match ThTermKind.Eq.coerce_type sema D.key,
ThTermKind.Eq.coerce_type semb D.key with
- | Poly.Eq, Poly.Eq -> Ty.equal tya tyb && D.equal va vb
+ | Poly.Eq, Poly.Eq -> D.equal va vb
let hash: t -> int = fun a ->
match a with
- | ThTerm(_,tya,sema,va) ->
+ | ThTerm(_,sema,va) ->
let Poly.Eq = ThTermKind.Eq.coerce_type sema D.key in
- Hashcons.combine (Ty.hash tya) (D.hash va)
+ (D.hash va)
let set_tag: int -> t -> t =
- fun tag (ThTerm(_,ty,sem,v)) -> ThTerm(tag,ty,sem,v)
+ fun tag (ThTerm(_,sem,v)) -> ThTerm(tag,sem,v)
- let tag: t -> int = fun (ThTerm(tag,_,_,_)) -> tag
+ let tag: t -> int = fun (ThTerm(tag,_,_)) -> tag
let pp fmt x =
Format.pp_print_char fmt '@';
@@ -213,13 +203,13 @@ module RegisterThTerm (D:ThTerm) : RegisteredThTerm with type s = D.t = struct
let key = D.key
let tag: t -> int = function
- | Node.ThTerm(tag,_,_,_) -> tag
+ | Node.ThTerm(tag,_,_) -> tag
- let index v ty =
+ let index v =
let node =
- HC.hashcons3
- (fun tag sem v ty -> Node.ThTerm(tag,ty,sem,v))
- D.key v ty in
+ HC.hashcons2
+ (fun tag sem v -> Node.ThTerm(tag,sem,v))
+ D.key v in
let i = tag node in
Simple_vector.inc_size (i+1) Node.names;
begin
@@ -235,19 +225,17 @@ module RegisterThTerm (D:ThTerm) : RegisteredThTerm with type s = D.t = struct
let node = Node.of_thterm
let sem : t -> D.t =
- fun (Node.ThTerm(_,_,sem,v)) ->
+ fun (Node.ThTerm(_,sem,v)) ->
let Poly.Eq = ThTermKind.Eq.coerce_type sem D.key in v
- let ty = ThTerm.ty
-
let thterm: t -> ThTerm.t = fun x -> x
let of_thterm: ThTerm.t -> t option = function
- | Node.ThTerm(_,_,sem',_) as v when ThTermKind.equal sem' D.key -> Some v
+ | Node.ThTerm(_,sem',_) as v when ThTermKind.equal sem' D.key -> Some v
| _ -> None
let coerce_thterm: ThTerm.t -> t =
- fun (Node.ThTerm(_,_,sem',_) as v) -> assert (ThTermKind.equal sem' D.key); v
+ fun (Node.ThTerm(_,sem',_) as v) -> assert (ThTermKind.equal sem' D.key); v
let () =
ThTermRegistry.register (module D: ThTerm with type t = D.t);
@@ -259,25 +247,23 @@ module Value = struct
include Popop_stdlib.MakeMSH(struct
type t = Node.nodevalue
let tag: t -> int = function
- | Node.Value(tag,_,_,_) -> tag
+ | Node.Value(tag,_,_) -> tag
let pp fmt : t -> unit = function
- | Node.Value(_,_,value,v) -> print_value value fmt v
+ | Node.Value(_,value,v) -> print_value value fmt v
end)
let index = Node.nodevalue
let node = Node.of_nodevalue
- let ty : t -> Ty.t = function
- | Node.Value(_,ty,_,_) -> ty
let value : type a. a ValueKind.t -> t -> a option =
- fun value (Node.Value(_,_,value',v)) ->
+ fun value (Node.Value(_,value',v)) ->
match ValueKind.Eq.eq_type value value' with
| Poly.Neq -> None
| Poly.Eq -> Some v
let semantic_equal (x:t) (y:t) : [ `Uncomparable | `Equal | `Disequal ] =
match x, y with
- | Node.Value(_,_,xk,_), Node.Value(_,_,yk,_) when not (ValueKind.equal xk yk) ->
+ | Node.Value(_,xk,_), Node.Value(_,yk,_) when not (ValueKind.equal xk yk) ->
`Uncomparable
| _ -> if equal x y then `Equal else `Disequal
@@ -290,15 +276,12 @@ module type RegisteredValue = sig
(** nodevalue *)
include Datatype
- val index: ?basename:string -> s -> Ty.t -> t
+ val index: ?basename:string -> s -> t
(** Return a nodevalue from a valueantical value *)
val node: t -> Node.t
(** Return a class from a nodevalue *)
- val ty: t -> Ty.t
- (** Return the type from a nodevalue *)
-
val value: t -> s
(** Return the value from a nodevalue *)
@@ -337,23 +320,23 @@ module RegisterValue (D:Value) : RegisteredValue with type s = D.t = struct
let equal: t -> t -> bool = fun a b ->
match a, b with
- | Value(_,tya,valuea,va), Value(_,tyb,valueb,vb) ->
+ | Value(_,valuea,va), Value(_,valueb,vb) ->
match ValueKind.Eq.coerce_type valuea D.key,
ValueKind.Eq.coerce_type valueb D.key with
- | Poly.Eq, Poly.Eq -> Ty.equal tya tyb && D.equal va vb
+ | Poly.Eq, Poly.Eq -> D.equal va vb
let hash: t -> int = fun a ->
match a with
- | Value(_,tya,valuea,va) ->
+ | Value(_,valuea,va) ->
let Poly.Eq = ValueKind.Eq.coerce_type valuea D.key in
- Hashcons.combine (Ty.hash tya) (D.hash va)
+ (D.hash va)
let set_tag: int -> t -> t = fun tag x ->
match x with
- | Value(_,ty,value,v) -> Value(tag,ty,value,v)
+ | Value(_,value,v) -> Value(tag,value,v)
let tag: t -> int = function
- | Value(tag,_,_,_) -> tag
+ | Value(tag,_,_) -> tag
let pp fmt x =
Format.pp_print_char fmt '@';
@@ -366,13 +349,13 @@ module RegisterValue (D:Value) : RegisteredValue with type s = D.t = struct
let key = D.key
let tag: t -> int = function
- | Node.Value(tag,_,_,_) -> tag
+ | Node.Value(tag,_,_) -> tag
- let index ?(basename="") v ty =
+ let index ?(basename="") v =
let node =
- HC.hashcons3
- (fun tag value v ty -> Node.Value(tag,ty,value,v))
- D.key v ty in
+ HC.hashcons2
+ (fun tag value v -> Node.Value(tag,value,v))
+ D.key v in
let i = tag node in
Simple_vector.inc_size (i+1) Node.names;
begin
@@ -387,19 +370,17 @@ module RegisterValue (D:Value) : RegisteredValue with type s = D.t = struct
let node = Node.of_nodevalue
let value : t -> D.t = function
- | Node.Value(_,_,value,v) ->
+ | Node.Value(_,value,v) ->
let Poly.Eq = ValueKind.Eq.coerce_type value D.key in v
- let ty = Value.ty
-
let nodevalue: t -> Value.t = fun x -> x
let of_nodevalue: Value.t -> t option = function
- | Node.Value(_,_,value',_) as v when ValueKind.equal value' D.key -> Some v
+ | Node.Value(_,value',_) as v when ValueKind.equal value' D.key -> Some v
| _ -> None
let coerce_nodevalue: Value.t -> t = function
- | Node.Value(_,_,value',_) as v -> assert (ValueKind.equal value' D.key); v
+ | Node.Value(_,value',_) as v -> assert (ValueKind.equal value' D.key); v
end
@@ -407,7 +388,7 @@ module RegisterValue (D:Value) : RegisteredValue with type s = D.t = struct
let () =
ValueRegistry.register (module D: Value with type t = D.t);
RegisteredValueRegistry.register (module All: RegisteredValue with type s = D.t);
- Node.ValueIndex.set Node.valueindex D.key (fun v ty -> index v ty)
+ Node.ValueIndex.set Node.valueindex D.key index
end
@@ -420,7 +401,7 @@ module Only_for_solver = struct
| Node.All (Node.ThTerm _ as x) -> Some x
let sem_of_node: ThTerm.t -> sem_of_node = function
- | Node.ThTerm (_,_,sem,v) -> ThTerm(sem,v)
+ | Node.ThTerm (_,sem,v) -> ThTerm(sem,v)
type value_of_node =
| Value: 'a ValueKind.t * 'a -> value_of_node
@@ -430,7 +411,7 @@ module Only_for_solver = struct
| Node.All (Node.Value _ as x) -> Some x
let value_of_node: Value.t -> value_of_node = function
- | Node.Value (_,_,value,v) -> Value(value,v)
+ | Node.Value (_,value,v) -> Value(value,v)
let node_of_thterm : ThTerm.t -> Node.t = ThTerm.node
let node_of_nodevalue : Value.t -> Node.t = Value.node
diff --git a/src/core/structures/nodes.mli b/src/core/structures/nodes.mli
index f906f88ce7400aa8bd8eb2af7f3a4ed9777b9d2c..149bf12ec291afd5fa0fc948400e04ea34cd3c12 100644
--- a/src/core/structures/nodes.mli
+++ b/src/core/structures/nodes.mli
@@ -44,13 +44,10 @@ module Node : sig
(** Change the pretty printed string for this node, to use with care
preferably at the start *)
- val ty: t -> Ty.t
- (** Return the type of a node *)
-
- val index_sem: 'a ThTermKind.t -> 'a -> Ty.t -> t
+ val index_sem: 'a ThTermKind.t -> 'a -> t
(** Return the corresponding node from a theory term *)
- val index_value: 'a ValueKind.t -> 'a -> Ty.t -> t
+ val index_value: 'a ValueKind.t -> 'a -> t
(** Return the corresponding node from a value *)
end
@@ -73,15 +70,12 @@ val print_thterm : 'a ThTermKind.t -> 'a Format.printer
module ThTerm: sig
include Datatype
- val index: 'a ThTermKind.t -> 'a -> Ty.t -> t
+ val index: 'a ThTermKind.t -> 'a -> t
(** Return the corresponding node from a theory term *)
val node: t -> Node.t
(** Returns the node associated to this theory term *)
- val ty: t -> Ty.t
- (** Returns the type of the theory term *)
-
end
(** {3 Construction of a theory terms } *)
@@ -96,15 +90,12 @@ module type RegisteredThTerm = sig
(** thterm *)
include Datatype
- val index: s -> Ty.t -> t
+ val index: s -> t
(** Return a theory term from the user type *)
val node: t -> Node.t
(** Return a class from a thterm *)
- val ty: t -> Ty.t
- (** Return the type from a thterm *)
-
val sem: t -> s
(** Return the sem from a thterm *)
@@ -142,13 +133,11 @@ val check_value_registered: 'a ValueKind.t -> unit
module Value: sig
include Datatype
- val index: 'a ValueKind.t -> 'a -> Ty.t -> t
+ val index: 'a ValueKind.t -> 'a -> t
(** Return the corresponding node from a value *)
val node: t -> Node.t
- val ty: t -> Ty.t
-
val value: 'a ValueKind.t -> t -> 'a option
val semantic_equal: t -> t -> [ `Uncomparable | `Equal | `Disequal ]
@@ -165,7 +154,7 @@ module type RegisteredValue = sig
(** nodevalue *)
include Datatype
- val index: ?basename:string -> s -> Ty.t -> t
+ val index: ?basename:string -> s -> t
(** Return a nodevalue from a valueantical term.
Basename is used only for debug
*)
@@ -173,9 +162,6 @@ module type RegisteredValue = sig
val node: t -> Node.t
(** Return a class from a nodevalue *)
- val ty: t -> Ty.t
- (** Return the type from a nodevalue *)
-
val value: t -> s
(** Return the value from a nodevalue *)
diff --git a/src/core/synTerm.ml b/src/core/synTerm.ml
new file mode 100644
index 0000000000000000000000000000000000000000..2dacf209c20618ed6f836fdd8419591a121ed685
--- /dev/null
+++ b/src/core/synTerm.ml
@@ -0,0 +1,101 @@
+(*************************************************************************)
+(* This file is part of Witan. *)
+(* *)
+(* Copyright (C) 2017 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* INRIA (Institut National de Recherche en Informatique et en *)
+(* Automatique) *)
+(* CNRS (Centre national de la recherche scientifique) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
+open Witan_popop_lib
+open Nodes
+
+let synsem = ThTermKind.create_key (module struct type t = Expr.Term.t let name = "syntax" end)
+
+module ThTerm = RegisterThTerm(struct
+ let key = synsem
+ include Expr.Term
+ end)
+
+let node_of_term x = ThTerm.node (ThTerm.index x)
+
+
+type env = {
+ converters: (Egraph.t -> Expr.Term.t -> Node.t option) list;
+ decvars: (Expr.Term.t -> Node.t -> Egraph.choice option) list;
+}
+
+let converters = Env.create_key (module struct
+ type t = env
+ let name = "Synsem.converters"
+ end)
+
+let register_converter env r =
+ let e = Egraph.get_env env converters in
+ Egraph.set_env env converters {e with converters = r::e.converters}
+
+let register_decvars env r =
+ let e = Egraph.get_env env converters in
+ Egraph.set_env env converters {e with decvars = r::e.decvars}
+
+let () = Env.register (fun _ _ -> ()) converters
+
+module DaemonConvertTerm = struct
+ let key = Demon.Fast.create "Synsem.DaemonConvertTerm"
+
+ module Data = Popop_stdlib.DUnit
+
+ let immediate = false
+ let throttle = 100
+ let wakeup d = function
+ | Events.Fired.EventRegSem(thterm,()) ->
+ begin try begin
+ let e = Egraph.get_env d converters in
+ let thterm = ThTerm.coerce_thterm thterm in
+ let v = ThTerm.sem thterm in
+ begin match v with
+ | { descr = App({builtin = Dolmen_std.Expr.Base; _ },_,[]); _ } ->
+ let n = ThTerm.node thterm in
+ List.iter (fun f ->
+ Opt.iter
+ (Egraph.register_decision d)
+ (f v n)
+ ) e.decvars
+ | _ -> ()
+ end;
+ let iter conv =
+ match conv d v with
+ | None -> ()
+ | Some node ->
+ Egraph.register d node;
+ Egraph.merge d (ThTerm.node thterm) node
+ in
+ List.iter iter e.converters
+ end with Exit -> () end
+ | _ -> raise UnwaitedEvent
+
+end
+
+module RDaemonConvertTerm = Demon.Fast.Register(DaemonConvertTerm)
+
+let init env =
+ Egraph.set_env env converters {converters=[]; decvars = []};
+ RDaemonConvertTerm.init env;
+ Demon.Fast.attach env
+ DaemonConvertTerm.key [Demon.Create.EventRegSem(ThTerm.key,())];
+
+include ThTerm
diff --git a/src/solver/notypecheck.mli b/src/core/synTerm.mli
similarity index 64%
rename from src/solver/notypecheck.mli
rename to src/core/synTerm.mli
index 6276577418fe6ff4a4261e9cc0ea84086379bf7f..17bf2bce8e10819415064c1ed47c6fe3e167b455 100644
--- a/src/solver/notypecheck.mli
+++ b/src/core/synTerm.mli
@@ -1,9 +1,12 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Witan. *)
(* *)
(* Copyright (C) 2017 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
+(* INRIA (Institut National de Recherche en Informatique et en *)
+(* Automatique) *)
+(* CNRS (Centre national de la recherche scientifique) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
@@ -18,12 +21,25 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-exception Typing_error of string * Dolmen.Term.t
+open Nodes
-val get_loc: Dolmen.Term.t -> Dolmen.ParseLocation.t
+val key: Dolmen_std.Expr.Term.t ThTermKind.t
-val run:
- ?limit:int ->
- theories:(Egraph.t -> unit) list ->
- (unit -> Dolmen.Statement.t option) ->
- [> `Sat | `Unsat ]
+include RegisteredThTerm with type s = Expr.Term.t
+
+val node_of_term : Expr.Term.t -> Node.t
+
+val init: Egraph.t -> unit
+
+val register_converter:
+ Egraph.t ->
+ (Egraph.t -> Expr.Term.t -> Node.t option) ->
+ unit
+(** register converters between syntactic terms *)
+
+
+val register_decvars:
+ Egraph.t ->
+ (Expr.Term.t -> Node.t -> Egraph.choice option) ->
+ unit
+(** register decision adder on variables *)
diff --git a/src/core/trail.ml b/src/core/trail.ml
deleted file mode 100644
index 36fafe02f8f1ba25912b287d5c892d4b3515170d..0000000000000000000000000000000000000000
--- a/src/core/trail.ml
+++ /dev/null
@@ -1,32 +0,0 @@
-(*************************************************************************)
-(* This file is part of Colibrics. *)
-(* *)
-(* Copyright (C) 2017 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(*************************************************************************)
-
-(** explanation are removed from Colibrics *)
-module Pexp = Witan_popop_lib.Popop_stdlib.DUnit
-module Exp = struct
- type 'a t = unit
- include (Witan_popop_lib.Popop_stdlib.DUnit : Witan_popop_lib.Popop_stdlib.Datatype with type t := unit)
-end
-module Chogen = Witan_popop_lib.Popop_stdlib.DUnit
-type chogen = Chogen.t
-module Age = Witan_popop_lib.Popop_stdlib.DUnit
-type age = Age.t
-type t = unit
-type dec = unit
diff --git a/src/core/witan_core.ml b/src/core/witan_core.ml
index 77ead76da405d97c23a117618bd3270855d78be1..0092fca85ce4350ef18ebc0fd535efb6539f9163 100644
--- a/src/core/witan_core.ml
+++ b/src/core/witan_core.ml
@@ -20,8 +20,8 @@
(** Witan core: define basic types and the solver *)
-module Id = Id
-module Term = Term
+module Expr = Expr
+module Term = Expr.Term
module Ty = Ty
module Keys = Keys
@@ -80,16 +80,11 @@ end
module Env = Env
-module Exp = Trail.Exp
-
module Egraph = Egraph
-module Trail = Trail
module Events = Events
module Demon = Demon
-module Conflict = Conflict
-
exception UnwaitedEvent = Nodes.UnwaitedEvent
(** Can be raised by daemon when receiving an event that they don't
waited for. It is the sign of a bug in the core solver *)
diff --git a/src/popop_lib/dune b/src/popop_lib/dune
index 35ba3fe2c6018aa8cb75871b4f20b3fdeb55f352..c3b02b2180542500799c811cf8d1bbb9a4ebc816 100644
--- a/src/popop_lib/dune
+++ b/src/popop_lib/dune
@@ -4,7 +4,7 @@
(name witan_popop_lib)
(public_name witan.popop_lib)
(synopsis "Temporary for witan (intended to be replaced by another library)")
- (libraries str unix zarith)
+ (libraries str unix zarith base)
(flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always)
(ocamlopt_flags :standard -O3 -bin-annot -unbox-closures
-unbox-closures-factor 20))
diff --git a/src/popop_lib/popop_stdlib.ml b/src/popop_lib/popop_stdlib.ml
index fe7be2908b4c20e1782909271e9542d0c30b0a38..09c34e3861b07a626289eaa6b12c21a8f69cdd8f 100644
--- a/src/popop_lib/popop_stdlib.ml
+++ b/src/popop_lib/popop_stdlib.ml
@@ -63,6 +63,7 @@ module MakeMSH (X : TaggedType) =
struct
module T = OrderedHashed(X)
include T
+ let hash_fold_t state t = Base.Hash.fold_int state (X.tag t)
module MGen = Intmap.Make(struct
include X
let equal ts1 ts2 = X.tag ts1 == X.tag ts2
@@ -90,6 +91,7 @@ end
module type Datatype = sig
include OrderedHashedType
+ val hash_fold_t: Base.Hash.state -> t -> Base.Hash.state
module M : Map_intf.PMap with type key = t
module S : Map_intf.Set with type 'a M.t = 'a M.t
and type M.key = M.key
@@ -102,6 +104,7 @@ module type Printable = sig
end
module MkDatatype(T : OrderedHashedType) = struct
+ let hash_fold_t state t = Base.Hash.fold_int state (T.hash t)
module M = Map.Make(T)
module S = Extset.MakeOfMap(M)
module H = XHashtbl.Make(T)
@@ -122,6 +125,7 @@ module Int = struct
module DInt = struct
include Int
let pp fmt x = Format.pp_print_int fmt x
+ let hash_fold_t = Base.Int.hash_fold_t
module GM = Intmap.Make(Int)
module M = GM.NT
module S = Extset.MakeOfMap(M)
@@ -142,6 +146,7 @@ end
module DBool = struct
include Bool
+ let hash_fold_t = Base.Bool.hash_fold_t
module M = Map.Make(Bool)
module S = Extset.MakeOfMap(M)
module H = XHashtbl.Make(Bool)
@@ -156,6 +161,7 @@ module DStr = struct
let pp = Format.pp_print_string
end
include Str
+ let hash_fold_t = Base.String.hash_fold_t
module M = Map.Make(Str)
module S = Extset.MakeOfMap(M)
module H = XHashtbl.Make(Str)
@@ -171,7 +177,7 @@ module Float = struct
let pp = Format.pp_print_float
end
include Float
-
+ let hash_fold_t = Base.Float.hash_fold_t
module M = Map.Make(Float)
module S = Extset.MakeOfMap(M)
module H = XHashtbl.Make(Float)
diff --git a/src/popop_lib/popop_stdlib.mli b/src/popop_lib/popop_stdlib.mli
index 5b8d425b5cc9c3676183c1d0c7f70ea9d97d4328..1df2d7296cd1d762039151da87a0fdbb7aee5508 100644
--- a/src/popop_lib/popop_stdlib.mli
+++ b/src/popop_lib/popop_stdlib.mli
@@ -41,6 +41,7 @@ end
module type Datatype = sig
include OrderedHashedType
+ val hash_fold_t: t Base.Hash.folder
module M : Map_intf.PMap with type key = t
module S : Map_intf.Set with type 'a M.t = 'a M.t
@@ -54,6 +55,7 @@ module type Printable = sig
end
module MkDatatype(T : OrderedHashedType) : sig
+ val hash_fold_t: T.t Base.Hash.folder
module M : Map_intf.PMap with type key = T.t
module S : Map_intf.Set with type 'a M.t = 'a M.t
and type M.key = M.key
diff --git a/src/popop_lib/unit.ml b/src/popop_lib/unit.ml
index 826c994f7974e7e8997daad8d68227d595555197..0d457c6487d461e1ae5698f86af194e5e7fee99c 100644
--- a/src/popop_lib/unit.ml
+++ b/src/popop_lib/unit.ml
@@ -24,6 +24,7 @@ let compare () () = 0
let equal () () = true
let hash _ = 0
let pp fmt () = Format.pp_print_string fmt "()"
+let hash_fold_t = Base.Unit.hash_fold_t
module M = struct
type key = unit
diff --git a/src/popop_lib/unit.mli b/src/popop_lib/unit.mli
index 233a4dadd9d3682a1e51278b8a80fe1ad556455d..43c11eaeb51cfae742aac3baaf62dc094405d962 100644
--- a/src/popop_lib/unit.mli
+++ b/src/popop_lib/unit.mli
@@ -24,6 +24,7 @@ type t = unit
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
+val hash_fold_t: t Base.Hash.folder
val pp: t Pp.pp
module M: Map_intf.Map with type key = unit
diff --git a/src/solver/dune b/src/solver/dune
index ac2167626d439ea6dbda84ba4995ad4743722401..d22b11cfc67ba305f5305c45ab85e76810c28de3 100644
--- a/src/solver/dune
+++ b/src/solver/dune
@@ -3,7 +3,7 @@
(public_name witan.solver)
(synopsis "witan's solver")
(libraries containers zarith ocamlgraph gen dolmen spelll witan.stdlib
- witan.popop_lib str witan.core witan.core.structures)
+ witan.popop_lib str witan.core witan.core.structures dolmen_loop)
(preprocess
(pps ppx_deriving.std))
(flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always -open
diff --git a/src/solver/input.ml b/src/solver/input.ml
index a6bd478b40959065e8cc1d0f5918226ce4850ee0..024c098b59128511f7150519c860b21a7ce72e0d 100644
--- a/src/solver/input.ml
+++ b/src/solver/input.ml
@@ -18,69 +18,310 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-(* The Dolmen library is used to parse input languages *)
-(* ************************************************************************ *)
-
-exception File_not_found of string
-(** Raised when file is not found. *)
-
-(** See documentation at
- {{:http://gbury.github.io/dolmen/dev/Logic.Make.html} Logic.Make} *)
-module P = Dolmen.Logic.Make
- (Dolmen.ParseLocation)
- (Dolmen.Id)
- (Dolmen.Term)
- (Dolmen.Statement)
-
-(* Some re-export of definitions *)
-type language = P.language =
- | Dimacs
- | ICNF
- | Smtlib
- | Tptp
- | Zf
-
-let enum = P.enum
-
-(** Convenience function to expand includes *)
-let read_aux ~language ~dir input =
- let acc = ref [input] in
- let rec aux () =
- match !acc with
- | [] -> None
- | g :: r ->
- begin match g () with
- | None -> acc := r; aux ()
- | Some { Dolmen.Statement.descr = Dolmen.Statement.Include f; _ } ->
- let file = match P.find ~language ~dir f with
- | None -> raise (File_not_found f)
- | Some f -> f
- in
- let _, g', _ = P.parse_input ~language (`File file) in
- acc := g' :: !acc;
- aux ()
- | (Some _) as res -> res
+type ctx = {
+ scheduler : Scheduler.t;
+ mutable state: [`Sat of Egraph.t | `Unknown | `Unsat | `StepLimitReached];
+ mutable pushpop: Scheduler.bp list;
+}
+
+let create_ctx theories =
+ let t = Scheduler.new_solver () in
+ Scheduler.init_theories t ~theories;
+ {
+ scheduler = t;
+ state = `Unknown;
+ pushpop = [];
+ }
+
+module State = struct
+ include Dolmen_loop.State
+ type t = ctx state
+ let is_interactive _ = false
+end
+module Pipeline = Dolmen_loop.Pipeline.Make(State)
+
+module Parser = Dolmen_loop.Parser.Pipe(Dolmen.Std.Expr)(State)
+module Header = Dolmen_loop.Headers.Pipe(State)
+module Typer = struct
+ module T = Dolmen_loop.Typer.Make(State)
+ include T
+ include Dolmen_loop.Typer.Pipe(Dolmen.Std.Expr)(State)(T)
+end
+
+let split_input = function
+ | `Stdin ->
+ Sys.getcwd (), `Stdin
+ | `File f ->
+ Filename.dirname f, `File (Filename.basename f)
+
+let print_exn st = function
+
+ (* Sigint, potentially wrapped by the typechecker *)
+ | Pipeline.Sigint
+ | Dolmen_loop.Typer.T.Typing_error (
+ Dolmen_loop.Typer.T.Error (_, _, Dolmen_loop.Typer.T.Uncaught_exn (
+ Pipeline.Sigint, _))) ->
+ Format.pp_print_flush Format.std_formatter ();
+ State.error st "User Interrupt"
+
+ (* Timeout, potentially wrapped by the typechecker *)
+ | Pipeline.Out_of_time
+ | Dolmen_loop.Typer.T.Typing_error (
+ Dolmen_loop.Typer.T.Error (_, _, Dolmen_loop.Typer.T.Uncaught_exn (
+ Pipeline.Out_of_time, _))) ->
+ Format.pp_print_flush Format.std_formatter ();
+ State.error st "Time limit reached"
+
+ | Pipeline.Out_of_space
+ | Dolmen_loop.Typer.T.Typing_error (
+ Dolmen_loop.Typer.T.Error (_, _, Dolmen_loop.Typer.T.Uncaught_exn (
+ Pipeline.Out_of_space, _))) ->
+ Format.pp_print_flush Format.std_formatter ();
+ State.error st "Memory limit reached"
+
+ (* Parsing errors *)
+ | Dolmen.Std.Loc.Uncaught (loc, exn) ->
+ let file = Dolmen_loop.State.input_file_loc st in
+ State.error ~loc:{ file; loc; } st "%s" (Printexc.to_string exn)
+ | Dolmen.Std.Loc.Lexing_error (loc, lex) ->
+ let file = Dolmen_loop.State.input_file_loc st in
+ State.error ~loc:{ file; loc; } st "Lexing error: invalid character '%s'" lex
+ | Dolmen.Std.Loc.Syntax_error (loc, `Regular msg) ->
+ let file = Dolmen_loop.State.input_file_loc st in
+ State.error ~loc: { file; loc; } st "%t@." msg
+ | Dolmen.Std.Loc.Syntax_error (loc, `Advanced (prod, lexed, expected)) ->
+ let file = Dolmen_loop.State.input_file_loc st in
+ State.error ~loc: { file; loc; } st
+ "@[<v>@[<hv>while parsing %t,@ read %t,@]@ @[<hov>but expected %t.@]@]"
+ prod lexed expected
+
+ (* Typing errors *)
+ | Dolmen_loop.Typer.T.Typing_error (
+ Dolmen_loop.Typer.T.Error (env, fragment, _err) as error) ->
+ let loc = Dolmen_loop.Typer.T.fragment_loc env fragment in
+ if st.context then
+ Format.eprintf "@[<hv 2>While typing:@ @[<hov>%a@]@]@."
+ Typer.print_fragment (env, fragment);
+ State.error ~loc st "%a"
+ Typer.report_error error
+
+ (* State errors *)
+ | Dolmen_loop.State.File_not_found (loc, dir, f) ->
+ if dir = "." then
+ State.error ~loc st "File not found: '%s'" f
+ else
+ State.error ~loc st "File not found: '%s' in directory '%s'" f dir
+ | Dolmen_loop.State.Input_lang_changed (l, l') ->
+ State.error st "Input language changed from %s to %s (probably because of an include statement)"
+ (Dolmen_loop.Logic.string_of_language l)
+ (Dolmen_loop.Logic.string_of_language l')
+
+ (* Internal Dolmen Expr errors *)
+ | Dolmen.Std.Expr.Bad_ty_arity (c, l) ->
+ let pp_sep fmt () = Format.fprintf fmt ";@ " in
+ State.error st "@[<hv>Internal error: Bad arity for type constant '%a',@ which was provided arguments:@ [@[<hv>%a@]]@]"
+ Dolmen.Std.Expr.Print.ty_const c (Format.pp_print_list ~pp_sep Dolmen.Std.Expr.Ty.print) l
+ | Dolmen.Std.Expr.Bad_term_arity (c, tys, ts) ->
+ let pp_sep fmt () = Format.fprintf fmt ";@ " in
+ State.error st "@[<hv>Internal error: Bad arity for type constant '%a',@ which was provided arguments:@ [@[<hv>%a;@ %a@]]@]"
+ Dolmen.Std.Expr.Print.term_const c
+ (Format.pp_print_list ~pp_sep Dolmen.Std.Expr.Ty.print) tys
+ (Format.pp_print_list ~pp_sep Dolmen.Std.Expr.Term.print) ts
+ | Dolmen.Std.Expr.Type_already_defined c ->
+ State.error st "@[<hv>Internal error: Type constant '%a' was already defined earlier,@ cannot re-define it.@]"
+ Dolmen.Std.Expr.Print.id c
+
+ | Dolmen.Std.Expr.Term.Wrong_type (t, ty) ->
+ State.error st "@[<hv>Internal error: A term of type@ %a@ was expected but instead got a term of type@ %a@]"
+ Dolmen.Std.Expr.Ty.print ty Dolmen.Std.Expr.Ty.print (Dolmen.Std.Expr.Term.ty t)
+
+ (* File format auto-detect *)
+ | Dolmen_loop.Logic.Extension_not_found ext ->
+ State.error st "@[<hv>The following extension was not recognized: '%s'.@ %s" ext
+ "Please use a recognised extension or specify an input language on the command line"
+
+ (* Generic catch-all *)
+ | e -> State.error st "@[<hv>Unhandled exception:@ %s@]" (Printexc.to_string e)
+
+
+let handle_exn_with_exit st exn =
+ if st.State.debug then
+ Format.eprintf "%a@\n%s@."
+ State.debug st
+ (Printexc.to_string exn);
+ let () = print_exn st exn in
+ exit 2
+
+let handle_exn_with_error _ exn =
+ raise exn
+
+
+let finally ~handle_exn st e =
+ match st.State.solve_state.state,e with
+ | `StepLimitReached, None ->
+ raise Scheduler.ReachStepLimit
+ | _, None -> st
+ | _, Some exn ->
+ handle_exn st exn;
+ assert false
+
+let debug_pipe st c =
+ if st.State.debug then
+ Format.eprintf "%a@\n%a@."
+ State.debug st
+ Dolmen.Std.Statement.print c;
+ st, c
+
+let def _st _d = invalid_arg "unimplemented"
+
+let set_term_true ~set_true d t =
+ let t = SynTerm.node_of_term t in
+ Egraph.register d t;
+ set_true d t
+
+let hyp ~set_true st t =
+ Scheduler.add_assertion st.scheduler (fun d ->
+ set_term_true ~set_true d t
+ )
+
+let solve ?limit ~set_true st t =
+ let check st =
+ match Scheduler.check_sat ?limit st.scheduler with
+ | res -> st.state <- res
+ | exception Scheduler.ReachStepLimit ->
+ st.state <- `StepLimitReached
+ in
+ match t with
+ | [] -> check st;
+ | l ->
+ let bp = Scheduler.push st.scheduler in
+ Scheduler.add_assertion st.scheduler (fun d ->
+ List.iter (set_term_true ~set_true d) l
+ );
+ check st;
+ Scheduler.pop_to st.scheduler bp
+
+let rec push st i =
+ assert (0 <= i);
+ if 0 < i then begin
+ st.pushpop <- (Scheduler.push st.scheduler)::st.pushpop;
+ push st (i-1)
+ end
+
+let rec pop st i =
+ assert (0 <= i);
+ match i, st.pushpop with
+ | 0, _ -> ()
+ | _, [] -> assert false (* absurd by dolmen invariant *)
+ | 1, bp::l ->
+ st.pushpop <- l;
+ Scheduler.pop_to st.scheduler bp
+ | n, _::l ->
+ st.pushpop <- l;
+ pop st (n-1)
+
+
+let handle_stmt ?(show_checksat_result=true) ?limit ~set_true (st:State.t) (stmt:Typer.typechecked Typer.stmt) =
+ begin match stmt.contents with
+ | `Reset
+ | `Get_unsat_core
+ | `Plain _
+ | `Get_assignment
+ | `Get_unsat_assumptions
+ | `Get_info _
+ | `Get_proof
+ | `Get_assertions
+ | `Get_value _
+ | `Get_option _
+ | `Get_model
+ | `Reset_assertions
+ | `Set_option _ -> invalid_arg "Unimplemented stmt"
+ | `Push i -> push st.State.solve_state i
+ | `Pop i -> pop st.State.solve_state i
+ | `Decls _ -> (* nothing to do handled by dolmen *) ()
+ | `Defs d -> List.iter (def st.State.solve_state) d
+ | `Goal _ -> invalid_arg "unimplemented"
+ | `Clause l -> hyp ~set_true st.State.solve_state (Expr.Term._or l)
+ | `Hyp d -> hyp ~set_true st.State.solve_state d
+ | `Solve s -> begin
+ solve ~set_true ?limit st.State.solve_state s;
+ if show_checksat_result then
+ match st.State.solve_state.state with
+ | `Unsat -> Format.printf "unsat@."
+ | `Sat _ -> Format.printf "sat@."
+ | `Unknown -> Format.printf "unknown@."
+ | `StepLimitReached -> Format.printf "steplimitreached@."
end
+ | `Echo s -> Format.printf "%s@." s
+ | `Set_info _ -> ()
+ | `Set_logic _ -> (* Perhaps something to do here *) ()
+ | `Exit -> ()
+ end;
+ st, ()
+
+let read ?show_checksat_result ?limit ~set_true ~handle_exn st =
+ let st, g =
+ try Parser.parse [] st
+ with exn ->
+ handle_exn st exn;
+ assert false
in
- aux
-
-let read ?language ~dir f =
- (** Formats Dimacs and Tptp are descriptive and lack the emission
- of formal solve/prove instructions, so we need to add them. *)
- let s = Dolmen.Statement.include_ f [] in
- (* Auto-detect input format *)
- let language =
- match language with
- | Some l -> l
- | None -> let res, _, _ = P.of_filename f in res
+ let st =
+ let open Pipeline in
+ run ~finally:(finally ~handle_exn) g st (
+ (fix (op ~name:"expand" Parser.expand) (
+ (op ~name:"debug" debug_pipe)
+ @>>> (op ~name:"headers" Header.inspect)
+ @>>> (op ~name:"typecheck" Typer.typecheck)
+ @>|> (op (handle_stmt ?show_checksat_result ?limit ~set_true)) @>>> _end
+ )
+ )
+ )
in
- let g =
- match language with
- | P.Zf
- | P.ICNF
- | P.Smtlib -> Gen.singleton s
- | P.Dimacs
- | P.Tptp -> Gen.of_list [s; Dolmen.Statement.prove ()]
+ let st = Header.check st in
+ let _st = Dolmen_loop.State.flush st () in
+ ()
+
+let mk_state
+ ?(gc=false) ?(gc_opt=Gc.get ()) ?(bt=true) ?(colors=true)
+ ?(time_limit=1_000_000_000.) ?(size_limit=1_000_000_000.)
+ ?input_lang ?input_mode ~input
+ ?(header_check=false) ?(header_licenses=[])
+ ?(header_lang_version=None)
+ ?(type_strict=true)
+ ?(debug=false) ?(context=true) ?(max_warn=max_int)
+ theories
+ =
+ (* Side-effects *)
+ let () = Gc.set gc_opt in
+ let () =
+ let style = if colors then `Ansi_tty else `None in
+ Fmt.set_style_renderer Format.err_formatter style;
in
- read_aux ~language ~dir g
+ let () = if bt then Printexc.record_backtrace true in
+ let () = if gc then at_exit (fun () -> Gc.print_stat stdout;) in
+ (* State creation *)
+ let input_dir, input_source = split_input input in
+ let st : State.t = {
+ debug;
+
+ context; max_warn;
+ cur_warn = 0;
+
+ time_limit; size_limit;
+
+ input_dir; input_lang;
+ input_mode; input_source;
+ input_file_loc = Dolmen.Std.Loc.mk_file "";
+
+ header_check; header_licenses; header_lang_version;
+ header_state = Dolmen_loop.Headers.empty;
+
+ type_check = true; type_strict;
+ type_state = Dolmen_loop.Typer.new_state ();
+
+ solve_state = create_ctx theories;
+ export_lang = [];
+ } in
+ st
diff --git a/src/solver/input.mli b/src/solver/input.mli
deleted file mode 100644
index ce5bce6a8d32765af34bb1e5eaf16d93ab1e026f..0000000000000000000000000000000000000000
--- a/src/solver/input.mli
+++ /dev/null
@@ -1,38 +0,0 @@
-(*************************************************************************)
-(* This file is part of Colibrics. *)
-(* *)
-(* Copyright (C) 2017 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(*************************************************************************)
-
-(** Problem input for Witan *)
-
-(** {2 Parsing some input} *)
-
-type language =
- | Dimacs (** The dimacs language *)
- | ICNF (** iCNF is ane xtension of dimacs *)
- | Smtlib (** smtlib language *)
- | Tptp (** TPTP problems language *)
- | Zf (** Zipperposition format *)
-(** The type of input language supported. *)
-
-val enum : (string * language) list
-(** Enumeration of pairs of a language and its name, mainly for use by cmdliner. *)
-
-val read : ?language:language -> dir:string -> string -> Dolmen.Statement.t Gen.t
-(** Read a file in a directory. Automatically expands all include statements.
- @language: if set, overrides input language auto-detection performed by dolmen. *)
diff --git a/src/solver/notypecheck.ml b/src/solver/notypecheck.ml
deleted file mode 100644
index 1a4c2ee6fd9ed16fcab463996442de57443c773c..0000000000000000000000000000000000000000
--- a/src/solver/notypecheck.ml
+++ /dev/null
@@ -1,361 +0,0 @@
-(*************************************************************************)
-(* This file is part of Colibrics. *)
-(* *)
-(* Copyright (C) 2017 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(*************************************************************************)
-
-open Witan_popop_lib
-
-(* Exception for typing errors *)
-module R = Exthtbl.Hashtbl.Make(Dolmen.Id)
-module MId = CCMap.Make(struct include Dolmen.Id let pp = print end)
-type env = Term.Id.t R.t
-
-let create_env () =
- R.create 10
-
-exception Typing_error of string * Dolmen.Term.t
-
-let _bad_op_arity _ s n t =
- let msg = Format.asprintf "Bad arity for operator '%s' (expected %d arguments)" s n in
- raise (Typing_error (msg, t))
-
-let regexp_decimal = Str.regexp "^[0-9]+\\(\\.[0-9]*\\)?$"
-
-(** no typing *)
-let rec parse_formula' (env:env) (lets:Term.t MId.t) (t:Dolmen.Term.t) =
- let module Ast = Dolmen.Term in
- let open Term in
- match t with
-
- (* Ttype & builtin types *)
- | { Ast.term = Ast.Builtin Ast.Ttype } ->
- _Type
- | { Ast.term = Ast.Builtin Ast.Prop } ->
- _Prop
-
- | { Ast.term = Ast.Symbol {Dolmen.Id.name = "Real"} } ->
- _Real
-
- (* Basic formulas *)
- | { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.True }, []) }
- | { Ast.term = Ast.Builtin Ast.True } ->
- true_term
-
- | { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.False }, []) }
- | { Ast.term = Ast.Builtin Ast.False } ->
- false_term
-
- | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.And}, l) } ->
- let f = (and_term (List.length l)) in
- let l = (List.map (parse_formula env lets) l) in
- apply f l
-
- | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Or}, l) } ->
- apply (or_term (List.length l)) (List.map (parse_formula env lets) 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 lets p in
- let g = parse_formula env lets q in
- apply not_term [apply equal_term [f.Term.ty;f;g]]
- | _ -> _bad_op_arity env "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 lets p in
- let g = parse_formula env lets q in
- apply imply_term [f;g]
- | _ -> _bad_op_arity env "=>" 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 lets p in
- let g = parse_formula env lets q in
- apply equiv_term [f;g]
- | _ -> _bad_op_arity env "<=>" 2 t
- end
-
- | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Not}, l) } as t ->
- begin match l with
- | [p] ->
- apply not_term [parse_formula env lets p]
- | _ -> _bad_op_arity env "not" 1 t
- end
-
- (* (\* Binders *\)
- * | { Ast.term = Ast.Binder (Ast.All, vars, f) } ->
- * let ttype_vars, ty_vars, env' =
- * parse_quant_vars (expect env (Typed Expr.Ty.base)) vars in
- * Formula (
- * mk_quant_ty env' Expr.Formula.allty ttype_vars
- * (mk_quant_term env' Expr.Formula.all ty_vars
- * (parse_formula env' f)))
- *
- * | { Ast.term = Ast.Binder (Ast.Ex, vars, f) } ->
- * let ttype_vars, ty_vars, env' =
- * parse_quant_vars (expect env (Typed Expr.Ty.base)) vars in
- * Formula (
- * mk_quant_ty env' Expr.Formula.exty ttype_vars
- * (mk_quant_term env' Expr.Formula.ex ty_vars
- * (parse_formula env' f))) *)
-
- (* (Dis)Equality *)
- | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Eq}, l) } as t ->
- begin match l with
- | [a; b] ->
- let a = parse_formula env lets a in
- let b = parse_formula env lets b in
- apply equal_term [a.Term.ty;a;b]
- (* begin match promote env t @@ parse_expr env a,
- * promote env t @@ parse_expr env b with
- * | Term t1, Term t2 ->
- * Formula (make_eq env t t1 t2)
- * | Formula f1, Formula f2 ->
- * Formula (Expr.Formula.equiv f1 f2)
- * | _ ->
- * _expected env "either two terms or two formulas" t None
- * end *)
- | _ -> _bad_op_arity env "=" 2 t
- end
-
- | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Distinct}, a::args) } ->
- let a = parse_formula env lets a in
- apply (distinct_term (List.length args + 1)) (a.Term.ty::a::(List.map (parse_formula env lets) args))
-
- | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Ite}, l) }
- | { Ast.term = Ast.App ({Ast.term = Ast.Symbol {Dolmen.Id.name = "ite"}}, l) } ->
- begin match l with
- | [cond;then_; else_] ->
- let cond = parse_formula env lets cond in
- let then_ = parse_formula env lets then_ in
- let else_ = parse_formula env lets else_ in
- apply ite_term [then_.Term.ty;cond;then_;else_]
- | _ -> _bad_op_arity env "ite" 3 t
- end
-
- | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Add}, l) }
- | { Ast.term = Ast.App ({Ast.term = Ast.Symbol {Dolmen.Id.name = "+"}}, l) } ->
- let f = (add_real_term (List.length l)) in
- let l = (List.map (parse_formula env lets) l) in
- apply f l
-
- | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Sub}, ([_;_] as l)) }
- | { Ast.term = Ast.App ({Ast.term = Ast.Symbol {Dolmen.Id.name = "-"}}, ([_;_] as l)) } ->
- let f = sub_real_term in
- let l = (List.map (parse_formula env lets) l) in
- apply f l
-
- | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Sub}, ([_] as l)) }
- | { Ast.term = Ast.App ({Ast.term = Ast.Symbol {Dolmen.Id.name = "-"}}, ([_] as l)) } ->
- let f = neg_real_term in
- let l = (List.map (parse_formula env lets) l) in
- apply f l
-
- | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Mult}, ([_;_] as l)) }
- | { Ast.term = Ast.App ({Ast.term = Ast.Symbol {Dolmen.Id.name = "*"}}, ([_;_] as l)) } ->
- let f = mul_real_term in
- let l = (List.map (parse_formula env lets) l) in
- apply f l
-
- | {Ast.term = Ast.Symbol {Dolmen.Id.name = cst}}
- | { Ast.term = Ast.App ({Ast.term = Ast.Symbol {Dolmen.Id.name = cst}}, []) } when Str.string_match regexp_decimal cst 0 ->
- const_real_term cst
-
- (* General case: application *)
- | { Ast.term = Ast.Symbol s } as ast ->
- begin match MId.find_opt s lets with
- | Some t -> t
- | None ->
- begin match R.find_opt env s with
- | Some id -> (const id)
- | None -> raise (Typing_error("unbound variable",ast))
- end
- end
-
- | { Ast.term = Ast.App ({ Ast.term = Ast.Symbol s }, l) } as ast ->
- begin match MId.find_opt s lets with
- | Some t -> apply t (List.map (parse_formula env lets) l)
- | None ->
- begin match R.find_opt env s with
- | Some id -> apply (const id) (List.map (parse_formula env lets) l)
- | None -> raise (Typing_error("unbound variable",ast))
- end
- end
-
- | { term = Ast.Binder (_,[],t); _; } ->
- parse_formula env lets t
-
- (* Local bindings *)
- | { Ast.term = Ast.Binder (Ast.Let, vars, f) } ->
- let rec aux lets = function
- | [] -> parse_formula env lets f
- | {Ast.term = Ast.Colon({Ast.term = Ast.Symbol s},t)}::l ->
- let t = parse_formula env lets t in
- if false then
- let s' = Format.asprintf "%a" Dolmen.Id.print s in
- let id = Witan_core.Id.mk s' t.Term.ty in
- R.add env s id;
- let l = aux lets l in
- R.remove env s;
- Term.letin id t l
- else
- let lets = MId.add s t lets in
- aux lets l
- | t::_ ->
- raise (Typing_error ("Unexpected let binding", t))
- in
- aux lets vars
-
- (* Functionnal arrows *)
- | { Ast.term = Ast.Binder (Ast.Arrow, vars, f) } ->
- Term.arrows (List.map (parse_formula env lets) vars) (parse_formula env lets f)
-
- (* Other cases *)
- | { Ast.term = Ast.App ({Ast.term = Ast.Builtin _}, _) } ->
- raise (Typing_error ("Unexpected builtin", t))
- | { term = Ast.Builtin _; _; } ->
- raise (Typing_error ("Unexpected builtin", t))
- | { term = Ast.Colon (_,_); _; } ->
- raise (Typing_error ("Unexpected colon", t))
- | { term = Ast.App (_,_); _; }->
- raise (Typing_error ("Unexpected app", t))
- | { term = Ast.Binder (_,_,_); _; } ->
- raise (Typing_error ("Unexpected binder", t))
- | { term = Ast.Match (_,_); _; } ->
- raise (Typing_error ("Unexpected construction", t))
-
-and parse_formula (env:env) lets (t:Dolmen.Term.t) =
- try
- parse_formula' env lets t
- with
- | (Typing_error _) as exn -> raise exn
- | exn ->
- raise (Typing_error (Printexc.to_string exn, t))
-
-let rec parse_clause_lit (env:env) t =
- let module Ast = Dolmen.Term in
- let open Term in
- match t with
- | { Ast.term = Ast.Symbol s }
- | { Ast.term = Ast.App ({ Ast.term = Ast.Symbol s }, []) } ->
- let id = R.memo (fun id ->
- let s = Format.asprintf "%a" Dolmen.Id.print id in
- (** only in dimacs they are not declared *)
- Witan_core.Id.mk s _Prop) env s in
- const id
- | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Not}, l) } as t ->
- begin match l with
- | [p] ->
- apply not_term [parse_clause_lit env p]
- | _ -> _bad_op_arity env "not" 1 t
- end
- | _ ->
- raise (Typing_error ("Unexpected construction in dimacs", t))
-
-
-let get_loc =
- let default_loc = Dolmen.ParseLocation.mk "<?>" 0 0 0 0 in
- (fun t -> CCOpt.get_or ~default:default_loc t.Dolmen.Term.loc)
-
-(** used to complete partial model *)
-let get_model env d =
- let model : Value.t Term.H.t = Term.H.create 16 in
- R.iter (fun _ id ->
- let t = Term.const id in
- let n = SynTerm.node_of_term t in
- let v = Interp.model d n in
- Term.H.add_new Std.Impossible model t v)
- env;
- model
-
-let interp_model model n =
- let leaf t = Term.H.find_opt model t in
- (Interp.node ~leaf n)
-
-let check_model model expected n =
- Value.equal (interp_model model n) expected
-
-let run ?limit ~theories statements =
- let env = create_env () in
- let clauses = ref [] in
- let open Witan_core in
- let res =
- Scheduler.run
- ~theories
- ?limit
- (fun d ->
- Gen.iter (fun stmt ->
- let open Dolmen.Statement in
- match stmt.descr with
- | Set_logic _ -> ()
- | Set_info _ -> ()
- | Prove -> ()
- | Dolmen.Statement.Exit -> ()
- | Decl (id,t) ->
- let t = Dolmen.Normalize.smtlib t in
- let ty = parse_formula env MId.empty t in
- let t' =
- let s = Format.asprintf "%a" Dolmen.Id.print id in
- Witan_core.Id.mk s ty
- in
- R.add_new Witan_stdlib.Std.Impossible env id t';
- | Clause l ->
- let map t = SynTerm.node_of_term (parse_clause_lit env t), Witan_core.Conflict.Pos in
- let l = Witan_stdlib.Shuffle.shufflel l in
- let l = List.map map l in
- let l = Witan_stdlib.Shuffle.shufflel l in
- let cl = !Witan_core.Conflict._or l in
- clauses := cl::!clauses;
- Egraph.register d cl;
- !Witan_core.Conflict._set_true d Trail.pexp_fact cl
- | Antecedent t ->
- let map t = SynTerm.node_of_term (parse_formula env MId.empty t) in
- let t = Dolmen.Normalize.smtlib t in
- let cl = map t in
- clauses := cl::!clauses;
- Egraph.register d cl;
- !Witan_core.Conflict._set_true d Trail.pexp_fact cl
- | _ -> invalid_arg (Format.asprintf "Unimplemented command: %a" Dolmen.Statement.print stmt))
- statements) in
- match res with
- | `Contradiction -> `Unsat
- | `Done _d ->
- (* let model = get_model env d in
- * Format.printf "(%a)@."
- * Witan_popop_lib.Pp.(iter22 Witan_core.Term.H.iter space
- * (fun fmt t v -> Format.fprintf fmt "(%a %a)"
- * Witan_core.Term.pp t Witan_core.Values.pp v))
- * model *)
- `Sat
-
-
-
-let () = Exn_printer.register (fun fmt exn ->
- match exn with
- | Typing_error (msg, t) ->
- Format.fprintf fmt
- "%a:@\n%s:@ %a"
- Dolmen.ParseLocation.fmt (get_loc t) msg
- Dolmen.Term.print t;
- | exn -> raise exn
- )
diff --git a/src/solver/scheduler.ml b/src/solver/scheduler.ml
index f0e90ab70e5c7e2f32f9a9e114e997a8eb568784..e5a5352f7e16c905751c85f29aaf36191efa3995 100644
--- a/src/solver/scheduler.ml
+++ b/src/solver/scheduler.ml
@@ -21,8 +21,6 @@
open Witan_popop_lib
open Witan_core
-module S = Egraph
-
let debug = Debug.register_info_flag
~desc:"for the scheduler in the simple version"
"sched_queue"
@@ -47,7 +45,7 @@ exception NeedStopDelayed
module Att = struct
type t =
| Daemon of int * Events.Wait.daemon_key
- | Decision of int * Trail.chogen
+ | Decision of int * Egraph.choice
type prio = float
type db = float Node.H.t
@@ -61,29 +59,26 @@ module Att = struct
if xp = yp then x <= y else xp >= yp (** min *)
| Daemon _ , Decision _ -> true
| Decision _, Daemon _ -> false
- let reprio db = function
+ let reprio _ = function
| Daemon _ -> 0.
- | Decision (_,Trail.GCho(n,_,_)) -> get_prio db n
+ | Decision (_,choice) -> float_of_int choice.prio
end
-exception Contradiction
+
+exception Contradiction = Egraph.Contradiction
module Prio = Leftistheap.Make(Att)
-type pre =
+type bp =
{ pre_wakeup_daemons : Prio.t;
- pre_prev_scheduler_state : pre option;
+ pre_prev_scheduler_state : bp option;
pre_backtrack_point : Context.bp;
- pre_age_dec : Trail.Age.t;
- pre_learnt : Conflict.Learnt.t Bag.t;
- pre_last_dec : Trail.chogen;
}
type t =
{ mutable wakeup_daemons : Prio.t;
- mutable prev_scheduler_state : pre option;
- solver_state : S.Backtrackable.t;
- mutable delayed : S.t option;
- mutable learnt : Conflict.Learnt.t Bag.t;
+ mutable prev_scheduler_state : bp option;
+ solver_state : Egraph.Backtrackable.t;
+ mutable delayed : Egraph.t option;
(* global *)
decprio : Att.db;
var_inc : float ref;
@@ -97,9 +92,7 @@ let print_level fmt t =
let nb_dec =
Prio.fold (fun acc x _ -> match x with Att.Decision _ -> acc + 1 | _ -> acc)
0 t.wakeup_daemons in
- Format.fprintf fmt "%a (level:%i, dec waiting:%i)"
- Trail.Age.pp (S.Backtrackable.current_age t.solver_state)
- (S.Backtrackable.current_nbdec t.solver_state) nb_dec
+ Format.fprintf fmt "(dec waiting:%i)" nb_dec
(* let new_handler t =
* if t.delayed <> None then raise NeedStopDelayed;
@@ -116,30 +109,25 @@ let new_solver () =
let context = Context.create () in
{ wakeup_daemons = Prio.empty;
prev_scheduler_state = None;
- solver_state = S.Backtrackable.new_t (Context.creator context);
+ solver_state = Egraph.Backtrackable.new_t (Context.creator context);
context;
- learnt = Bag.empty;
delayed = None;
decprio = Node.H.create 100;
var_inc = ref 1.;
}
-let push t chogen =
+let push t =
if Debug.test_flag debug_dotgui then
- S.Backtrackable.draw_graph ~force:true t.solver_state;
+ Egraph.Backtrackable.draw_graph ~force:true t.solver_state;
Debug.dprintf0 debug_pushpop "[Scheduler] push";
- let age_dec = Trail.last_dec (S.Backtrackable.get_trail t.solver_state) in
let prev =
{ pre_wakeup_daemons = t.wakeup_daemons;
pre_prev_scheduler_state = t.prev_scheduler_state;
pre_backtrack_point = Context.bp t.context;
- pre_learnt = t.learnt;
- pre_last_dec = chogen;
- pre_age_dec = age_dec;
} in
t.prev_scheduler_state <- Some prev;
- t.learnt <- Bag.empty;
- ignore (Context.push t.context)
+ ignore (Context.push t.context);
+ prev
let update_prio t chogen =
Node.H.change (function
@@ -163,7 +151,7 @@ let new_delayed =
!dec_count;
t.wakeup_daemons <- Prio.insert t.decprio (Att.Decision (!dec_count,dec))
t.wakeup_daemons in
- S.Backtrackable.new_delayed ~sched_daemon ~sched_decision t.solver_state
+ Egraph.Backtrackable.new_delayed ~sched_daemon ~sched_decision t.solver_state
(*
let rec apply_learnt llearnt t d =
@@ -183,39 +171,27 @@ let new_delayed =
conflict_analysis t pexp
*)
-let rec apply_learnt learntdec llearnt t d =
- try
- Debug.dprintf0 debug "[Scheduler] Apply previously learnt";
- let iter_learnt n =
- Debug.dprintf2 debug "[Scheduler] @[Apply %a@]"
- Conflict.Learnt.pp n;
- Conflict.apply_learnt d n;
- S.Backtrackable.flush d in
- Bag.iter iter_learnt llearnt;
- if Conflict.learnt_is_already_true d learntdec
- then assert false; (** absurd: If it is already true it should not be this conflict *)
- iter_learnt learntdec;
- run_until_dec t d;
- Debug.dprintf0 debug_pushpop "[Scheduler] Learnt applied";
- (** TODO: decision on the last decision if it is multiple theory *)
- d
- with S.Contradiction pexp ->
- Debug.dprintf0 debug "[Scheduler] Contradiction during apply learnt";
- conflict_analysis t pexp
-
-and pop_to t prev =
+let pop_to t prev =
Debug.dprintf2 debug_pushpop "[Scheduler] pop from %a"
print_level t;
t.wakeup_daemons <- prev.pre_wakeup_daemons;
t.prev_scheduler_state <- prev.pre_prev_scheduler_state;
Context.pop prev.pre_backtrack_point;
- t.learnt <- prev.pre_learnt;
let d = new_delayed t in
Egraph.Backtrackable.draw_graph t.solver_state;
Debug.dprintf2 debug_pushpop "[Scheduler] pop to %a"
print_level t;
d
+
+let rec apply_learnt t d =
+ try
+ run_until_dec t d;
+ d
+ with Egraph.Contradiction ->
+ Debug.dprintf0 debug "[Scheduler] Contradiction during apply learnt";
+ conflict_analysis t
+
(*
and conflict_analysis t pexp =
Debug.incr stats_con;
@@ -228,7 +204,7 @@ and pop_to t prev =
| None -> raise Contradiction
| Some prev when
Trail.current_age
- (S.get_trail prev.pre_solver_state) <= maxage ->
+ (Egraph.get_trail prev.pre_solver_state) <= maxage ->
llearnt,prev
| Some prev ->
let llearnt = List.rev_append llearnt prev.pre_learnt in
@@ -241,72 +217,48 @@ and pop_to t prev =
pop_to llearnt t prev
*)
-and conflict_analysis t pexp =
+and conflict_analysis t =
if Debug.test_flag debug_dotgui then
- S.Backtrackable.draw_graph ~force:true t.solver_state;
+ Egraph.Backtrackable.draw_graph ~force:true t.solver_state;
Debug.incr stats_con;
- if Egraph.Backtrackable.current_nbdec t.solver_state = 0 then begin
- Debug.dprintf0 debug "[Scheduler] contradiction at level 0";
- raise Contradiction
- end
- else
- let backlevel, learnt, useful =
- Conflict.learn
- (Egraph.Backtrackable.get_getter t.solver_state)
- (Egraph.Backtrackable.get_trail t.solver_state)
- pexp
- in
- t.var_inc := !(t.var_inc) *. var_decay;
- Bag.iter (update_prio t) useful;
- (** We look for the level just below the backtrack level *)
- let rec rewind t learnt llearnt prevo =
- match prevo with
- | None ->
- Debug.dprintf0 debug "[Scheduler] learnt clause false at level 0";
- raise Contradiction
- | Some prev ->
- let llearnt_all = Bag.concat llearnt prev.pre_learnt in
- let age_dec = prev.pre_age_dec in
- if Trail.Age.(backlevel < age_dec) then
- rewind t learnt llearnt_all prev.pre_prev_scheduler_state
- else
- let d = pop_to t prev in
- t.learnt <- Bag.append llearnt_all learnt;
- d,learnt,llearnt
- in
- let d,learntdec,llearnt =
- rewind t learnt t.learnt t.prev_scheduler_state in
- t.wakeup_daemons <- Prio.reprio t.decprio t.wakeup_daemons;
- apply_learnt learntdec llearnt t d
+ t.var_inc := !(t.var_inc) *. var_decay;
+ (** We look for the level just below the backtrack level *)
+ let rewind t prevo =
+ match prevo with
+ | None ->
+ Debug.dprintf0 debug "[Scheduler] learnt clause false at level 0";
+ raise Contradiction
+ | Some prev ->
+ let d = pop_to t prev in
+ d
+ in
+ let d =
+ rewind t t.prev_scheduler_state in
+ t.wakeup_daemons <- Prio.reprio t.decprio t.wakeup_daemons;
+ apply_learnt t d
and try_run_dec:
- t -> S.t -> Prio.t -> Trail.chogen -> S.t = fun t d prio chogen ->
+ t -> Egraph.t -> Prio.t -> Egraph.choice -> Egraph.t = fun t d prio choice ->
(** First we verify its the decision is at this point needed *)
try
- match Conflict.choose_decision d chogen with
- | Conflict.DecNo ->
+ match choice.choice d with
+ | Egraph.DecNo ->
t.wakeup_daemons <- prio;
d (** d can be precised by choose_decision *)
- | Conflict.DecTodo todo ->
+ | Egraph.DecTodo todo ->
Debug.incr stats_dec;
- S.Backtrackable.delayed_stop d;
+ Egraph.Backtrackable.delayed_stop d;
(** The registered state keep the old prio *)
- push t chogen;
+ ignore (push t);
(** We use the priority list without the decision only in the
branch where the decision is made *)
t.wakeup_daemons <- prio;
- let declevel = S.Backtrackable.new_dec t.solver_state in
- Debug.dprintf4 debug_pushpop
- "[Scheduler] Make decision: decision %a level %a"
- Trail.print_dec declevel
- print_level t;
- assert (Egraph.Backtrackable.current_nbdec t.solver_state > 0);
let d = new_delayed t in
todo d;
d
- with S.Contradiction pexp ->
+ with Egraph.Contradiction ->
Debug.dprintf0 debug "[Scheduler] Contradiction";
- conflict_analysis t pexp
+ conflict_analysis t
and run_until_dec t d =
let act = Prio.min t.wakeup_daemons in
@@ -315,8 +267,8 @@ and run_until_dec t d =
let _, prio = Prio.extract_min t.wakeup_daemons in
Debug.incr stats_propa;
t.wakeup_daemons <- prio;
- S.Backtrackable.run_daemon d att;
- S.Backtrackable.flush d;
+ Egraph.Backtrackable.run_daemon d att;
+ Egraph.Backtrackable.flush d;
run_until_dec t d
end
| Some (Att.Decision (_,_)) | None -> ()
@@ -329,19 +281,19 @@ let run_one_step t d =
Debug.incr stats_propa;
t.wakeup_daemons <- prio;
try
- S.Backtrackable.run_daemon d att; d
- with S.Contradiction pexp ->
+ Egraph.Backtrackable.run_daemon d att; d
+ with Egraph.Contradiction ->
Debug.dprintf0 debug "[Scheduler] Contradiction";
- conflict_analysis t pexp
+ conflict_analysis t
end
| Att.Decision (_,chogen) -> try_run_dec t d prio chogen
let rec flush t d =
try
- S.Backtrackable.flush d; d
- with S.Contradiction pexp ->
+ Egraph.Backtrackable.flush d; d
+ with Egraph.Contradiction ->
Debug.dprintf0 debug "[Scheduler] Contradiction";
- let d = conflict_analysis t pexp in
+ let d = conflict_analysis t in
flush t d
exception ReachStepLimit
@@ -360,7 +312,7 @@ let rec run_inf_step ?limit ~nodec t d =
let d = run_one_step t d in
run_inf_step ?limit:(Opt.map pred limit) ~nodec t d
else begin
- S.Backtrackable.delayed_stop d
+ Egraph.Backtrackable.delayed_stop d
end
let run_inf_step ?limit ?(nodec=false) t =
@@ -387,26 +339,54 @@ let flush_delayed t =
| Some d ->
t.delayed <- Some (flush t d)
+let stop t d =
+ let d = flush t d in
+ Egraph.Backtrackable.delayed_stop d;
+ t.delayed <- None
+
let stop_delayed t =
match t.delayed with
| None -> ()
| Some d ->
let d = flush t d in
- S.Backtrackable.delayed_stop d;
- t.delayed <- None
+ stop t d
+
+let init_theories ~theories t =
+ try
+ let d = get_delayed t in
+ List.iter (fun f -> f d) (SynTerm.init::theories);
+ Egraph.Backtrackable.flush d;
+ let d = flush t d in
+ stop t d
+ with Egraph.Contradiction ->
+ Debug.dprintf0 debug
+ "[Scheduler] Contradiction during theory initialization";
+ raise Contradiction
+
+
+let add_assertion t f =
+ try
+ let d = get_delayed t in
+ f d;
+ let d = flush t d in
+ stop t d
+ with Egraph.Contradiction ->
+ Debug.dprintf0 debug
+ "[Scheduler] Contradiction during assertion";
+ raise Contradiction
+
+let check_sat ?limit t =
+ try
+ stop_delayed t;
+ run_inf_step ?limit t;
+ `Sat (get_delayed t)
+ with Contradiction ->
+ `Unsat
let run_exn ?nodec ?limit ~theories f =
let t = new_solver () in
- begin try
- let d = get_delayed t in
- List.iter (fun f -> f d) (SynTerm.init::theories);
- Egraph.Backtrackable.flush d;
- f d
- with S.Contradiction _ ->
- Debug.dprintf0 debug
- "[Scheduler] Contradiction during initial assertion";
- raise Contradiction
- end;
+ init_theories ~theories t;
+ add_assertion t f;
stop_delayed t;
run_inf_step ~nodec:(nodec=Some ()) ?limit t;
get_delayed t
@@ -416,3 +396,5 @@ let run ?nodec ?limit ~theories f =
`Done (run_exn ?nodec ?limit ~theories f)
with Contradiction ->
`Contradiction
+
+let pop_to st bp = ignore (pop_to st bp)
diff --git a/src/solver/scheduler.mli b/src/solver/scheduler.mli
index c88706891085d51acf1d52630917ccfd98c453e5..2bf87eabaf9c5d65079cac2a26e6a8a6406b6d1a 100644
--- a/src/solver/scheduler.mli
+++ b/src/solver/scheduler.mli
@@ -34,3 +34,17 @@ val run:
[> `Contradiction
| `Done of Egraph.t
]
+
+type t
+
+val new_solver: unit -> t
+val init_theories: theories:(Egraph.t -> unit) list -> t -> unit
+val add_assertion: t -> (Egraph.t -> unit) -> unit
+val check_sat: ?limit:int -> t -> [> `Unsat | `Sat of Egraph.t ]
+
+type bp
+
+val push: t -> bp
+val pop_to: t -> bp -> unit
+
+exception ReachStepLimit
diff --git a/src/solver/solver.ml b/src/solver/solver.ml
index 9cc3b06470bde0f608b3188aadf70d548debe007..25c5bee75fe9b8e3c78fdeda2a09a7f092210b9b 100644
--- a/src/solver/solver.ml
+++ b/src/solver/solver.ml
@@ -19,4 +19,3 @@
(*************************************************************************)
module Scheduler = Scheduler
-module Input = Input
diff --git a/src/stdlib/dune b/src/stdlib/dune
index 0973647a7dd79b4577e73b09367111673cfabb33..55423e337a0f8cd17f020434a1ac1fabdbcc3458 100644
--- a/src/stdlib/dune
+++ b/src/stdlib/dune
@@ -4,7 +4,7 @@
(synopsis "Stdlib for witan")
(libraries zarith containers witan_popop_lib)
(preprocess
- (pps ppx_optcomp ppx_deriving.std))
+ (pps ppx_optcomp ppx_deriving.std ppx_hash))
(flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always -open
Containers)
(ocamlopt_flags :standard -O3 -bin-annot -unbox-closures
diff --git a/src/stdlib/std.ml b/src/stdlib/std.ml
index ba98859a1a3fd255175202981fc584e35b742acc..2b0a8bc46064447e4ee540f008f119d41875be2a 100644
--- a/src/stdlib/std.ml
+++ b/src/stdlib/std.ml
@@ -22,9 +22,10 @@
(*************************************************************************)
include Std_sig
+module Hash = Base.Hash
let nnil = function [] -> false | _::_ -> true
-
+
module Poly = struct
type (_,_,_) t =
@@ -59,7 +60,7 @@ end
module Q = struct
module Arg = struct
include Q (* Module from Zarith *)
- let hash = Hash.poly
+ let hash = CCHash.poly
let pp fmt q =
Format.(
match Q.classify q with
@@ -79,7 +80,7 @@ module Q = struct
let of_string_decimal =
let decimal = Str.regexp "\\(+\\|-\\)?\\([0-9]+\\)\\([.]\\([0-9]*\\)\\)?" in
fun s ->
- if not (Str.string_match decimal s 0) then None
+ if not (Str.string_match decimal s 0) then assert false
else
let sgn = match Str.matched_group 1 s with
| "-" -> Q.minus_one
@@ -96,6 +97,6 @@ module Q = struct
let ten = Q.of_int 10 in
Witan_popop_lib.Util.foldi (fun acc _ -> Q.(acc * ten)) dec 1 l
in
- Some Q.(sgn * (int_part + dec_part))
+ Q.(sgn * (int_part + dec_part))
end
diff --git a/src/stdlib/std.mli b/src/stdlib/std.mli
index 4f087cbddc299d8afe1e4605577fb36233d4a8bf..2ec37f57c76a37b7b5ac7045efd08d6241672712 100644
--- a/src/stdlib/std.mli
+++ b/src/stdlib/std.mli
@@ -56,5 +56,5 @@ module Q : sig
val two : t
val ge : t -> t -> bool
val le : t -> t -> bool
- val of_string_decimal : string -> t option
+ val of_string_decimal : string -> t
end
diff --git a/src/tests/dune b/src/tests/dune
index 304220bb3b64f214f8a1c2edb4e68b1b8c106612..6d4e4271aae9684ed72837992f1a80d9acd760c2 100644
--- a/src/tests/dune
+++ b/src/tests/dune
@@ -2,7 +2,7 @@
(modes byte exe)
(name tests)
(libraries containers witan.core witan.theories.bool witan.theories.LRA
- oUnit witan.solver witan.stdlib)
+ ounit2 witan.solver witan.stdlib)
(flags :standard -w +a-4-42-44-48-50-58-32-60-9@8 -color always)
(ocamlopt_flags :standard -O3 -unbox-closures -unbox-closures-factor 20))
diff --git a/src/tests/tests.ml b/src/tests/tests.ml
index ba008aa24da0e1d4aef91c87b1e92f0fbc469717..9c0630752249a6db2952b6707066c6a34cfff5c1 100644
--- a/src/tests/tests.ml
+++ b/src/tests/tests.ml
@@ -18,10 +18,10 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open OUnit
-open Witan_stdlib
-open Witan_core
-open Tests_lib
+open OUnit2
+(* open Witan_stdlib
+ * open Witan_core
+ * open Tests_lib *)
let opt_seed = ref 0
@@ -35,8 +35,8 @@ let make_tests acc seed =
let test = ((Witan_popop_lib.Pp.sprintf "seed %a" print_seed seed) >:::
[ Tests_bool.tests; Tests_uf.tests; Tests_LRA.tests ])
in
- let test = test_decorate
- (fun f -> (fun () -> Shuffle.set_shuffle seed; f ())) test in
+ (* let test = test_decorate
+ * (fun f -> (fun () -> Shuffle.set_shuffle seed; f ())) test in *)
test::acc
let tests () =
@@ -45,98 +45,101 @@ let tests () =
make_tests l None
let tests () =
- if Printexc.backtrace_status ()
- then
- (test_decorate
- (fun f ->
- fun () ->
- try f ()
- with exn ->
- Format.fprintf (Witan_popop_lib.Debug.get_debug_formatter ()) "%s"
- (Printexc.get_backtrace ());
- raise exn
- )) (TestList (tests ()))
- else
- (TestList (tests ()))
+ (* if Printexc.backtrace_status ()
+ * then
+ * (test_decorate
+ * (fun f ->
+ * fun () ->
+ * try f ()
+ * with
+ * | exn ->
+ * Format.fprintf (Witan_popop_lib.Debug.get_debug_formatter ()) "%s"
+ * (Printexc.get_backtrace ());
+ * raise exn
+ * )) (test_list (tests ()))
+ * else *)
+ (test_list (tests ()))
(** From oUnit.ml v 1.2.2 *)
(** just need to make the tests lazily computed *)
-(* Returns true if the result list contains successes only *)
-let rec was_successful =
- function
- | [] -> true
- | RSuccess _::t
- | RSkip _::t ->
- was_successful t
-
- | RFailure _::_
- | RError _::_
- | RTodo _::_ ->
- false
-
-
-(* Call this one from you test suites *)
-let run_test_tt_main ?(arg_specs=[]) suite =
- let only_test = ref [] in
- let () =
- Arg.parse
- (Arg.align
- [
- "-only-test",
- Arg.String (fun str -> only_test := str :: !only_test),
- "path Run only the selected test";
-
- "-list-test",
- Arg.Unit
- (fun () ->
- List.iter
- (fun pth ->
- print_endline (string_of_path pth))
- (test_case_paths (suite ()));
- exit 0),
- " List tests";
- ] @ arg_specs
- )
- (fun x -> raise (Arg.Bad ("Bad argument : " ^ x)))
- ("usage: " ^ Sys.argv.(0) ^ " [-verbose] [-only-test path]*")
- in
- let () = Witan_popop_lib.Debug.Args.set_flags_selected () in
- let verbose = Witan_popop_lib.Debug.test_flag debug in
- let nsuite =
- if !only_test = [] then
- suite ()
- else
- begin
- match test_filter ~skip:true !only_test (suite ()) with
- | Some test ->
- test
- | None ->
- failwith ("Filtering test "^
- (String.concat ", " !only_test)^
- " lead to no test")
- end
- in
- let result = run_test_tt ~verbose nsuite in
- if not (was_successful result) then
- exit 1
- else
- result
-
-(*** End *)
-
-let () =
- if not (Egraph.check_initialization () && Conflict.check_initialization ()) then
- exit 1
-
-let _ =
- try
- run_test_tt_main
- ~arg_specs:(["--seed",Arg.Set_int opt_seed,
- " Base seed used for shuffling the arbitrary decision";
- Witan_popop_lib.Debug.Args.desc_debug_all]@
- Witan_popop_lib.Debug.Args.desc_debug)
- tests
- with e when not (Witan_popop_lib.Debug.test_flag Witan_popop_lib.Debug.stack_trace) ->
- Format.eprintf "%a" Witan_popop_lib.Exn_printer.exn_printer e;
- exit 1
+(* (\* Returns true if the result list contains successes only *\)
+ * let rec was_successful =
+ * function
+ * | [] -> true
+ * | RSuccess _::t
+ * | RSkip _::t ->
+ * was_successful t
+ *
+ * | RFailure _::_
+ * | RError _::_
+ * | RTodo _::_ ->
+ * false
+ *
+ *
+ * (\* Call this one from you test suites *\)
+ * let run_test_tt_main ?(arg_specs=[]) suite =
+ * let only_test = ref [] in
+ * let () =
+ * Arg.parse
+ * (Arg.align
+ * [
+ * "-only-test",
+ * Arg.String (fun str -> only_test := str :: !only_test),
+ * "path Run only the selected test";
+ *
+ * "-list-test",
+ * Arg.Unit
+ * (fun () ->
+ * List.iter
+ * (fun pth ->
+ * print_endline (string_of_path pth))
+ * (test_case_paths (suite ()));
+ * exit 0),
+ * " List tests";
+ * ] @ arg_specs
+ * )
+ * (fun x -> raise (Arg.Bad ("Bad argument : " ^ x)))
+ * ("usage: " ^ Sys.argv.(0) ^ " [-verbose] [-only-test path]*")
+ * in
+ * let () = Witan_popop_lib.Debug.Args.set_flags_selected () in
+ * let verbose = Witan_popop_lib.Debug.test_flag debug in
+ * let nsuite =
+ * if !only_test = [] then
+ * suite ()
+ * else
+ * begin
+ * match test_filter ~skip:true !only_test (suite ()) with
+ * | Some test ->
+ * test
+ * | None ->
+ * failwith ("Filtering test "^
+ * (String.concat ", " !only_test)^
+ * " lead to no test")
+ * end
+ * in
+ * let result = run_test_tt ~verbose nsuite in
+ * if not (was_successful result) then
+ * exit 1
+ * else
+ * result
+ *
+ * (\*** End *\)
+ *
+ * let () =
+ * if not (Egraph.check_initialization ()) then
+ * exit 1
+ *
+ * let _ =
+ * try
+ * run_test_tt_main
+ * ~arg_specs:(["--seed",Arg.Set_int opt_seed,
+ * " Base seed used for shuffling the arbitrary decision";
+ * Witan_popop_lib.Debug.Args.desc_debug_all]@
+ * Witan_popop_lib.Debug.Args.desc_debug)
+ * tests
+ * with e when not (Witan_popop_lib.Debug.test_flag Witan_popop_lib.Debug.stack_trace) ->
+ * Format.eprintf "%a" Witan_popop_lib.Exn_printer.exn_printer e;
+ * exit 1 *)
+
+let () = run_test_tt_main (tests ())
diff --git a/src/tests/tests_LRA.ml b/src/tests/tests_LRA.ml
index 5dc64c2d2dbe8525665b4bba219de728115cd755..493318dbb32dcbec6003b6563ed08e9c4e1ff3ec 100644
--- a/src/tests/tests_LRA.ml
+++ b/src/tests/tests_LRA.ml
@@ -18,7 +18,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open OUnit
+open OUnit2
open Tests_lib
open Witan_theories_bool
open Witan_theories_LRA
@@ -38,9 +38,10 @@ let ($$) f x = f x
(* The tests with rundec check only the result on a model satisfying
the hypothesis *)
+open Expr
-let solve0a () =
- let a = fresh Term._Real "ar" in
+let solve0a _ =
+ let a = fresh Ty.real "ar" in
let _1 = LRA.cst Q.one in
let a1 = LRA.add a _1 in
let env = run $$ fun env ->
@@ -49,7 +50,7 @@ let solve0a () =
in
assert_bool "a+1 = 1 => a = 0" (is_equal env a LRA.zero)
-(* let solve0b () =
+(* let solve0b _ =
* let a = fresh Term._Real "ar" in
* let _1 = LRA.cst Q.one in
* let _2 = LRA.cst Q.two in
@@ -62,9 +63,9 @@ let solve0a () =
* in
* assert_bool "a+1 = 2 => 2*a+2 = 4" (is_equal env _2a2 _4) *)
-let solve0c () =
- let a = fresh Term._Real "ar" in
- let b = fresh Term._Real "br" in
+let solve0c _ =
+ let a = fresh Ty.real "ar" in
+ let b = fresh Ty.real "br" in
let _1 = LRA.cst Q.one in
let a1 = LRA.add a _1 in
let b1 = LRA.add b _1 in
@@ -74,8 +75,8 @@ let solve0c () =
in
assert_bool "a+1 = b+1 => a = b" (is_equal env a b)
-let solve1 () =
- let a,b = Shuffle.seq2 (fresh Term._Real) ("ar","br") in
+let solve1 _ =
+ let a,b = Shuffle.seq2 (fresh Ty.real) ("ar","br") in
let _1 = LRA.cst Q.one in
let a1 = LRA.add a _1 in
let b1 = LRA.add b _1 in
@@ -88,8 +89,8 @@ let solve1 () =
in
assert_bool "a+1 = b+1 => a+2 = b+2" (is_equal env a2 b2)
-let solve2 () =
- let a,b = Shuffle.seq2 (fresh Term._Real) ("ar","br") in
+let solve2 _ =
+ let a,b = Shuffle.seq2 (fresh Ty.real) ("ar","br") in
let _1 = LRA.cst Q.one in
let a1 = LRA.add a _1 in
let b1 = LRA.add b _1 in
@@ -102,8 +103,8 @@ let solve2 () =
in
assert_bool "a+2 = b+1 => a+1 = b" (is_equal env a1 b)
-let solve3 () =
- let a,b = Shuffle.seq2 (fresh Term._Real) ("ar","br") in
+let solve3 _ =
+ let a,b = Shuffle.seq2 (fresh Ty.real) ("ar","br") in
let _1 = LRA.cst Q.one in
let b1 = LRA.add b _1 in
let _2 = LRA.cst (Q.of_int 2) in
@@ -128,9 +129,9 @@ let solve3 () =
assert_bool "a+2 = b+1 => a = 2 => b = 3" (is_equal env b _3)
-let solve4 () =
+let solve4 _ =
let a,b,c =
- Shuffle.seq3 (fresh Term._Real) ("ar","br","cr") in
+ Shuffle.seq3 (fresh Ty.real) ("ar","br","cr") in
let t1 = LRA.cst (Q.of_int 2) in
let t1 = LRA.add t1 c in
let t1 = LRA.add a t1 in
@@ -154,10 +155,10 @@ let solve4 () =
assert_bool "a+(2+c) = b+1 => a = 2 + b => c = -3" (is_equal env c t3')
-let solve5 () =
- let a = fresh Term._Real "ar" in
- let b = fresh Term._Real "br" in
- let c = fresh Term._Real "cr" in
+let solve5 _ =
+ let a = fresh Ty.real "ar" in
+ let b = fresh Ty.real "br" in
+ let c = fresh Ty.real "cr" in
let t1 = LRA.sub b c in
let t1 = LRA.add a t1 in
let t1' = (LRA.cst (Q.of_int 2)) in
@@ -191,9 +192,9 @@ let basic = "LRA.Basic" &:
solve5
]
-(* let mult0 () =
- * let a = fresh Term._Real "ar" in
- * let b = fresh Term._Real "br" in
+(* let mult0 _ =
+ * let a = fresh Ty.real "ar" in
+ * let b = fresh Ty.real "br" in
* let t1 = LRA.sub a b in
* let t1' = LRA.mult a b in
* let t2 = a in
@@ -215,10 +216,10 @@ let basic = "LRA.Basic" &:
* assert_bool "a - b = a * b -> a = 1 -> 1 = 2b" (is_equal env t3 t3')
*
* (\** test that mult normalization trigger the needed solve *\)
- * let mult1 () =
- * let a = fresh Term._Real "ar" in
- * let b = fresh Term._Real "br" in
- * let c = fresh Term._Real "cr" in
+ * let mult1 _ =
+ * let a = fresh Ty.real "ar" in
+ * let b = fresh Ty.real "br" in
+ * let c = fresh Ty.real "cr" in
* let t1 = LRA.mult a b in
* let t1 = LRA.add a t1 in
* let t1' = LRA.add b c in
@@ -253,48 +254,4 @@ let basic = "LRA.Basic" &:
* let altergo = TestList (List.map Tests_lib.test_split files)
*)
-
-let check_file filename =
- let statements = Witan_solver.Input.read
- ~language:Witan_solver.Input.Smtlib
- ~dir:(Filename.dirname filename)
- (Filename.basename filename)
- in
- Witan_solver.Notypecheck.run ~theories ~limit:1000 statements
-
-let tests_smt2 expected dir =
- if Sys.file_exists dir then
- let files = Sys.readdir dir in
- Array.sort String.compare files;
- let files = Array.to_list files in
- List.map
- (fun s ->
- s >: TestCase (fun () ->
- begin match check_file (Filename.concat dir s) with
- | `Sat ->
- Witan_popop_lib.Debug.dprintf1 Tests_lib.debug "@[%s: Sat@]" s;
- assert_bool s (`Sat = expected)
- | `Unsat ->
- Witan_popop_lib.Debug.dprintf1 Tests_lib.debug "@[%s: Unsat@]" s;
- assert_bool s (`Unsat = expected)
- | exception Witan_solver.Notypecheck.Typing_error (msg, t) ->
- assert_string
- (Format.asprintf
- "%a:@\n%s:@ %a"
- Dolmen.ParseLocation.fmt (Witan_solver.Notypecheck.get_loc t) msg
- Dolmen.Term.print t
- )
- end;
- )) files
- else
- []
-
-let smtlib2sat =
- "smtlib2-lra-sat" >:::
- tests_smt2 `Sat "solve/smt_lra/sat/"
-
-let smtlib2unsat =
- "smtlib2-lra-unsat" >:::
- tests_smt2 `Unsat "solve/smt_lra/unsat/"
-
-let tests = TestList [basic;(* (\* mult;*\)altergo;*) (* smtlib2sat; smtlib2unsat *)]
+let tests = test_list [basic;(* (\* mult;*\)altergo;*) (* smtlib2sat; smtlib2unsat *)]
diff --git a/src/tests/tests_bool.ml b/src/tests/tests_bool.ml
index ae7b9bf841a051d5261de9c3afd1c8e2f0471814..e2958df8de42f2d2950bbb22cf5a2fec20809f5b 100644
--- a/src/tests/tests_bool.ml
+++ b/src/tests/tests_bool.ml
@@ -18,7 +18,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open OUnit
+open OUnit2
open Witan_stdlib
open Witan_core
open Tests_lib
@@ -30,21 +30,23 @@ let ($$) f x = f x
let run = Tests_lib.run_exn ~theories
-let bool_interp () =
- let ta = Term.const (Id.mk "a" Boolean.ty) in
- let tb = Term.const (Id.mk "b" Boolean.ty) in
- let tc = Term.const (Id.mk "c" Boolean.ty) in
+open Expr
+
+let bool_interp _ =
+ let ta = fresht Ty.bool "a" in
+ let tb = fresht Ty.bool "b" in
+ let tc = fresht Ty.bool "c" in
let to_n x = SynTerm.node_of_term x in
let na = to_n ta in
let nb = to_n tb in
let nc = to_n tc in
let leaf ~a ~b ~c t =
if Term.equal t ta
- then Some (Value.index Boolean.dom a Boolean.ty)
+ then Some (Value.index Boolean.dom a)
else if Term.equal t tb
- then Some (Value.index Boolean.dom b Boolean.ty)
+ then Some (Value.index Boolean.dom b)
else if Term.equal t tc
- then Some (Value.index Boolean.dom c Boolean.ty)
+ then Some (Value.index Boolean.dom c)
else None
in
let l = [
@@ -64,36 +66,36 @@ let bool_interp () =
in
List.iter test l
-let true_is_true () =
+let true_is_true _ =
let env = run (fun _ -> ()) in
assert_bool "" (Boolean.is_true env Boolean._true);
assert_bool "" (not (Boolean.is_false env Boolean._true))
-let not_true_is_false () =
+let not_true_is_false _ =
let not_true = Boolean._not Boolean._true in
let env = run $$ fun env -> Egraph.register env not_true in
assert_bool "" (Boolean.is_false env not_true);
assert_bool "" (not (Boolean.is_true env not_true))
-let and_true_is_true () =
+let and_true_is_true _ =
let _t = Boolean._true in
let _and = Boolean._and [_t;_t;_t] in
let env = run $$ fun env -> Egraph.register env _and in
assert_bool "" (Boolean.is_true env _and);
assert_bool "" (not (Boolean.is_false env _and))
-let or_not_true_is_false () =
+let or_not_true_is_false _ =
let _f = (Boolean._not Boolean._true) in
let _or = Boolean._and [_f;_f;_f] in
let env = run $$ fun env -> Egraph.register env _or in
assert_bool "" (Boolean.is_false env _or);
assert_bool "" (not (Boolean.is_true env _or))
-let merge_true () =
- let a = fresh Boolean.ty "a" in
- let b = fresh Boolean.ty "b" in
- let c = fresh Boolean.ty "c" in
- let d = fresh Boolean.ty "d" in
+let merge_true _ =
+ let a = fresh Ty.bool "a" in
+ let b = fresh Ty.bool "b" in
+ let c = fresh Ty.bool "c" in
+ let d = fresh Ty.bool "d" in
let _and = Boolean._and [a;b;c] in
let env = run $$ fun env ->
Egraph.register env _and;
@@ -103,22 +105,22 @@ let merge_true () =
(fun () -> merge env a c);
];
merge env a d;
- Boolean.set_true env Trail.pexp_fact d;
+ Boolean.set_true env d;
in
assert_bool "" (Boolean.is_true env _and)
-let imply_implies () =
- let a = Term.const (Id.mk "a" Term._Prop) in
- let b = Term.const (Id.mk "b" Term._Prop) in
- let t = Term.apply Term.imply_term [a;b] in
+let imply_implies _ =
+ let a = fresht Ty.bool "a" in
+ let b = fresht Ty.bool "b" in
+ let t = Term.imply a b in
let an = SynTerm.node_of_term a in
let bn = SynTerm.node_of_term b in
let tn = SynTerm.node_of_term t in
let env = run $$ fun env ->
Egraph.register env tn;
- Boolean.set_true env Trail.pexp_fact tn;
+ Boolean.set_true env tn;
Egraph.register env an;
- Boolean.set_true env Trail.pexp_fact an;
+ Boolean.set_true env an;
in
assert_bool "" (Boolean.is_true env bn)
@@ -132,55 +134,4 @@ let basic = "Boolean.Basic" >::: [ "bool_interp" >:: bool_interp;
(* "modus_ponens" >:: modus_ponens; *)
]
-
-let check_file filename =
- let statements = Witan_solver.Input.read
- ~language:Witan_solver.Input.Dimacs
- ~dir:(Filename.dirname filename)
- (Filename.basename filename)
- in
- try
- Witan_solver.Notypecheck.run ~theories ~limit:1000 statements
- with
- | Witan_solver.Notypecheck.Typing_error (msg, t) ->
- assert_failure
- (Format.asprintf
- "%a:@\n%s:@ %a"
- Dolmen.ParseLocation.fmt (Witan_solver.Notypecheck.get_loc t) msg
- Dolmen.Term.print t
- )
-
-let tests_dimacs expected dir =
- let files = Sys.readdir dir in
- Array.sort String.compare files;
- let files = Array.to_list files in
- List.map
- (fun s ->
- s >: TestCase (fun () ->
- let res = check_file (Filename.concat dir s) in
- begin match res with
- | `Sat -> Witan_popop_lib.Debug.dprintf1 Tests_lib.debug "@[%s: Sat@]" s
- | `Unsat -> Witan_popop_lib.Debug.dprintf1 Tests_lib.debug "@[%s: Unsat@]" s
- end;
- assert_bool s (res = expected);
- )) files
-
-let dimacssat =
- "dimacs-sat" >::: tests_dimacs `Sat "solve/dimacs/sat/"
-
-let dimacsunsat =
- "dimacs-unsat" >::: tests_dimacs `Unsat "solve/dimacs/unsat/"
-
-let tests = TestList [basic; dimacssat;dimacsunsat]
-
-
-let () = Witan_popop_lib.Exn_printer.register (fun fmt exn ->
- match exn with
- | Dolmen.ParseLocation.Syntax_error(l,"") ->
- Format.fprintf fmt "%a: syntax error."
- Dolmen.ParseLocation.fmt l
- | Dolmen.ParseLocation.Syntax_error(l,c) ->
- Format.fprintf fmt "%a: syntax error %s."
- Dolmen.ParseLocation.fmt l c
- | exn -> raise exn
- )
+let tests = test_list [basic]
diff --git a/src/tests/tests_lib.ml b/src/tests/tests_lib.ml
index d6a34c68f4f701265c2709d8a6529b0b67884cb9..3ae0cca61108fed5ca589023aedc3f7143c2a669 100644
--- a/src/tests/tests_lib.ml
+++ b/src/tests/tests_lib.ml
@@ -18,23 +18,24 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open OUnit
+open OUnit2
open Witan_popop_lib
open Witan_core
let debug = Debug.register_flag
~desc:" Run the test in verbose mode." "ounit"
-let fresh ty s = SynTerm.node_of_term (Term.const (Id.mk s ty))
+let fresht ty s = Expr.Term.apply (Expr.Term.Const.mk s [] [] ty) [] []
+let fresh ty s = SynTerm.node_of_term (Expr.Term.apply (Expr.Term.Const.mk s [] [] ty) [] [])
-let (&:) s l = s >::: (List.map (fun f -> TestCase f) l)
+let (&:) s l = s >::: (List.map (fun f -> OUnit2.test_case f) l)
let register d cl =
Egraph.register d cl;
Egraph.Backtrackable.flush d
let merge d cl1 cl2 =
- Egraph.merge d Trail.pexp_fact cl1 cl2;
+ Egraph.merge d cl1 cl2;
Egraph.Backtrackable.flush d
let is_equal = Egraph.is_equal
@@ -65,4 +66,54 @@ exception Contradiction
let run_exn = Witan_solver.Scheduler.run_exn
-let fresh ty s = SynTerm.node_of_term (Term.const (Id.mk s ty))
+let check_file ?limit ~theories filename =
+ let st =
+ Witan_solver.Input.mk_state
+ ~input:(`File filename)
+ theories
+ ~bt:false
+ in
+ Witan_solver.Input.read
+ ~show_checksat_result:false
+ ?limit
+ ~set_true:Witan_theories_bool.Boolean.set_true
+ ~handle_exn:Witan_solver.Input.handle_exn_with_error
+ st;
+ let r = st.Witan_solver.Input.State.solve_state.Witan_solver.Input.state in
+ match r with
+ | `Sat _ -> `Sat
+ | `Unsat -> `Unsat
+ | `Unknown -> `Unknown
+ | `StepLimitReached -> `StepLimitReached
+
+
+let tests_file ?limit ~theories expected dir =
+ if Sys.file_exists dir then
+ let files = Sys.readdir dir in
+ Array.sort String.compare files;
+ let files = Array.to_list files in
+ List.map
+ (fun s ->
+ s >: test_case (fun _ ->
+ begin match check_file ?limit ~theories (Filename.concat dir s) with
+ | `Sat ->
+ Witan_popop_lib.Debug.dprintf1 debug "@[%s: Sat@]" s;
+ assert_bool s (`Sat = expected)
+ | `Unsat ->
+ Witan_popop_lib.Debug.dprintf1 debug "@[%s: Unsat@]" s;
+ assert_bool s (`Unsat = expected)
+ | `Unknown ->
+ Witan_popop_lib.Debug.dprintf1 debug "@[%s: Unknown@]" s;
+ assert_bool s (`Unknown = expected)
+ | `StepLimitReached ->
+ Witan_popop_lib.Debug.dprintf0 debug "StepLimit Reached@.";
+ assert_bool s false
+ | exception exn ->
+ Witan_popop_lib.Debug.dprintf2 debug "@.Error: %s@.%s@."
+ (Printexc.to_string exn)
+ (Printexc.get_backtrace ());
+ assert_bool s false;
+ end;
+ )) files
+ else
+ []
diff --git a/src/tests/tests_uf.ml b/src/tests/tests_uf.ml
index 9359afc2de194c2398695f8a70bc8e011a3ebc5d..831c3e37e0d54fdd68fc82dd1dd5dfa4ade48de3 100644
--- a/src/tests/tests_uf.ml
+++ b/src/tests/tests_uf.ml
@@ -19,7 +19,7 @@
(*************************************************************************)
-open OUnit
+open OUnit2
open Witan_core
open Tests_lib
open Witan_theories_bool
@@ -28,17 +28,19 @@ let theories = [Boolean.th_register; Equality.th_register; Uninterp.th_register
let run = Tests_lib.run_exn ~theories ~nodec:()
let ($$) f x = f x
-let a = SynTerm.node_of_term (Term.const (Id.mk "a" Boolean.ty))
-let b = SynTerm.node_of_term (Term.const (Id.mk "b" Boolean.ty))
-let c = SynTerm.node_of_term (Term.const (Id.mk "c" Boolean.ty))
+open Expr
-let empty () =
+let a = fresh Ty.bool "a"
+let b = fresh Ty.bool "b"
+let c = fresh Ty.bool "c"
+
+let empty _ =
let env = run $$ fun env ->
register env a; register env b;
in
assert_bool "⊬ a == b" (not (is_equal env a b))
-let tauto () =
+let tauto _ =
let env = run $$ fun env ->
register env a; register env b;
merge env a b;
@@ -46,7 +48,7 @@ let tauto () =
assert_bool "a = b => a = b"
(is_equal env a b)
-let tauto_equal () =
+let tauto_equal _ =
let env = run $$ fun env ->
register env a; register env b;
merge env a b;
@@ -54,7 +56,7 @@ let tauto_equal () =
assert_bool "a = b => a = b"
(is_equal env a b)
-let trans () =
+let trans _ =
let env = run $$ fun env ->
register env a; register env b; register env c;
merge env a b; merge env b c;
@@ -63,7 +65,7 @@ let trans () =
assert_bool "a = b => b = c => a = b" (is_equal env a b);
assert_bool "a = b => b = c => b = c" (is_equal env b c)
-let noteq () =
+let noteq _ =
let env = run $$ fun env ->
register env a; register env b; register env c;
merge env b c;
@@ -79,19 +81,19 @@ let fb = f b
let ffa = f (f a)
let ffb = f (f b)
-let refl () =
+let refl _ =
let env = run $$ fun env ->
register env fa;
in
assert_bool "f(a) = f(a)" (is_equal env fa fa)
-let empty () =
+let empty _ =
let env = run $$ fun env ->
register env fa; register env fb;
in
assert_bool "f(a) != f(b)" (not (is_equal env fa fb))
-let congru () =
+let congru _ =
let env = run $$ fun env ->
Shuffle.seql [
(fun () -> register env fa);
@@ -104,7 +106,7 @@ let congru () =
assert_bool "a = b => f(a) = f(b)"
(is_equal env fa fb)
-let _2level () =
+let _2level _ =
let env = run $$ fun env ->
Shuffle.seql [
(fun () -> register env ffa);
@@ -117,7 +119,7 @@ let _2level () =
assert_bool "a = b => f(f(a)) = f(f(b))"
(is_equal env ffa ffb)
-let _2level' () =
+let _2level' _ =
let env = run $$ fun env ->
register env a; register env b;
merge env a b;
@@ -126,7 +128,7 @@ let _2level' () =
assert_bool "a = b => f(f(a)) = f(f(b))" (is_equal env ffa ffb)
-let bigger () =
+let bigger _ =
let rec bf n = if n < 1 then a else (f (bf(n-1))) in
let fa = bf 1 in
let fffa = bf 3 in
@@ -158,11 +160,11 @@ let gab = g a b
let gaa = g a a
let ggabb = g gab b
-let refl () =
+let refl _ =
let env = run $$ fun env -> register env gab in
assert_bool "g(a,b) = g(a,b)" (is_equal env gab gab)
-let congru () =
+let congru _ =
let env = run $$ fun env ->
Shuffle.seql [
(fun () -> register env gab);
@@ -175,7 +177,7 @@ let congru () =
assert_bool "a = b => g(a,b) = g(a,a)"
(is_equal env gab gaa)
-let notcongru () =
+let notcongru _ =
let env = run $$ fun env ->
register env a; register env gab; register env gaa;
merge env a gab;
@@ -183,7 +185,7 @@ let notcongru () =
assert_bool "a = g(a,b) => g(a,b) != g(a,a)"
(not (is_equal env gab gaa))
-let _2level () =
+let _2level _ =
let env = run $$ fun env ->
Shuffle.seql [
(fun () -> register env a);
@@ -208,7 +210,7 @@ let merge env x y =
let x = Variable.fresh ty "x"
let y = Variable.fresh ty "y"
-let altergo0 () =
+let altergo0 _ =
let h = Uninterp.fun1 ty "h" in
let g = Uninterp.fun2 ty "g" in
let gax = g a x in
@@ -224,7 +226,7 @@ let altergo0 () =
assert_bool "h(x)=x and g(a,x)=a -> g(g(a,h(x)),x)=a"
(is_equal env ggahxx a)
-let altergo1 () =
+let altergo1 _ =
let h = Uninterp.fun2 ty "h" in
let rec bf n = if n < 1 then a else f (bf (n-1)) in
let fffa = bf 3 in
@@ -247,7 +249,7 @@ let altergo1 () =
h(g(g(x,y),y),a)=h(x,f(a))"
(is_equal env hggxyya hxfa)
-let altergo2 () =
+let altergo2 _ =
let h = Uninterp.fun2 ty "h" in
let gxy = g x y in
let fa = f a in
@@ -275,47 +277,5 @@ let altergo2 = TestList (List.map Tests_lib.test_split files)
*)
-let check_file filename =
- let statements = Witan_solver.Input.read
- ~language:Witan_solver.Input.Smtlib
- ~dir:(Filename.dirname filename)
- (Filename.basename filename)
- in
- try
- Witan_solver.Notypecheck.run ~theories ~limit:1000 statements
- with
- | Witan_solver.Notypecheck.Typing_error (msg, t) ->
- assert_failure
- (Format.asprintf
- "%a:@\n%s:@ %a"
- Dolmen.ParseLocation.fmt (Witan_solver.Notypecheck.get_loc t) msg
- Dolmen.Term.print t
- )
-
-let tests_smt2 expected dir =
- let files = Sys.readdir dir in
- Array.sort String.compare files;
- let files = Array.to_list files in
- List.map
- (fun s ->
- s >: TestCase (fun () ->
- let res = check_file (Filename.concat dir s) in
- begin match res with
- | `Sat -> Witan_popop_lib.Debug.dprintf1 Tests_lib.debug "@[%s: Sat@]" s
- | `Unsat -> Witan_popop_lib.Debug.dprintf1 Tests_lib.debug "@[%s: Unsat@]" s
- end;
- assert_bool s (res = expected);
- )) files
-
-
-let smtlib2sat =
- "smtlib2-uf-sat" >:::
- tests_smt2 `Sat "solve/smt_uf/sat/"
-
-let smtlib2unsat =
- "smtlib2-uf-unsat" >:::
- tests_smt2 `Unsat "solve/smt_uf/unsat/"
-
-
-let tests = TestList [basic;(* congru1;congru2;altergo;altergo2;*)
- smtlib2sat; smtlib2unsat]
+let tests = OUnit2.test_list [basic;(* congru1;congru2;altergo;altergo2;*)
+ ]
diff --git a/src/theories/LRA/LRA.ml b/src/theories/LRA/LRA.ml
index be09e0f9f7db882d77d5e41ad83612c8c506a7c4..976d80a1b52ca552ad414efd7200bc7441c2201b 100644
--- a/src/theories/LRA/LRA.ml
+++ b/src/theories/LRA/LRA.ml
@@ -34,7 +34,7 @@ module RealValue = ValueKind.Register(struct
let key = real
end)
-let cst' c = RealValue.index ~basename:(Format.asprintf "%aR" Q.pp c) c Term._Real
+let cst' c = RealValue.index ~basename:(Format.asprintf "%aR" Q.pp c) c
let cst c = RealValue.node (cst' c)
let debug_todo = debug
@@ -45,7 +45,6 @@ module S = struct
type t =
| Add of Q.t * Node.t * Q.t * Node.t
| GZero of Node.t * bound
- | Conflict of Polynome.t * bound
[@@ deriving eq,ord]
let pp fmt = function
@@ -61,8 +60,6 @@ module S = struct
else Format.fprintf fmt "%a + %a" pp (q1,cl1) pp (q2,cl2)
| GZero (node,b) ->
Format.fprintf fmt "0 %a %a" Interval.pp_bound b Node.pp node
- | Conflict (p,b) ->
- Format.fprintf fmt "0 %a %a" Interval.pp_bound b Polynome.pp p
let hash = function
| Add (q1,cl1,q2,cl2) ->
@@ -70,8 +67,6 @@ module S = struct
+ 5*(Hashtbl.hash q2) + 7*Node.hash cl2) + 1
| GZero (node,Strict) -> 7 * Node.hash node + 2
| GZero (node,Large) -> 7 * Node.hash node + 3
- | Conflict(p,Strict) -> CCHash.combine2 (Polynome.hash p) 4
- | Conflict(p,Large) -> CCHash.combine2 (Polynome.hash p) 5
end
include T
@@ -85,29 +80,11 @@ module D = Interval.Convexe
let dom = DomKind.create_key (module struct type t = D.t let name = "ARITH" end)
-type exp =
- | ExpAdd of SE.t * Node.t (** on what we propagated *)
- | ExpEmptyDomMerge of Trail.Pexp.t * Node.t * Node.t
- | ExpEmptyDomInter of Trail.Pexp.t * Node.t
- | ExpDistIsZero of SE.t
- | ExpGZeroUp of SE.t * bool
- | ExpGZeroDown of SE.t * Node.t * bool
- | ExpIsSingleton of Trail.Pexp.t * Node.t
- * bool (* the domain of node *) * RealValue.t
- | ExpCst of RealValue.t
- | ExpDec of Node.t * Q.t
-[@@ deriving show]
-
-(** The explanation for a dom will always work on conflict which is an inequality *)
-
-let exp = Trail.Exp.create_key (module struct type t = exp let name = "LRA.exp" end)
-
-let set_dom d pexp node v b =
+let set_dom d node v =
match D.is_singleton v with
| Some q ->
let cst = cst' q in
- let pexp = Egraph.mk_pexp d exp (ExpIsSingleton(pexp,node,b,cst)) in
- Egraph.set_value d pexp node (RealValue.nodevalue cst)
+ Egraph.set_value d node (RealValue.nodevalue cst)
| None ->
(** the pexp must be in the dom *)
Egraph.set_dom d dom node v
@@ -126,14 +103,13 @@ let () = DomKind.register(module struct
| Some i1, Some i2 -> D.equal i1 i2
| _ -> false
- let merge d pexp (i1,cl1) (i2,cl2) _ =
+ let merge d (i1,cl1) (i2,cl2) _ =
assert (not (Egraph.is_equal d cl1 cl2));
match i1, cl1, i2, cl2 with
| Some i1,_, Some i2,_ ->
begin match D.inter i1 i2 with
| None ->
- let pexp = Egraph.mk_pexp d exp (ExpEmptyDomMerge(pexp,cl1,cl2)) in
- Egraph.contradiction d pexp
+ Egraph.contradiction d
| Some i ->
if not (D.equal i i1) then
Egraph.set_dom d dom cl1 i;
@@ -164,31 +140,25 @@ module DaemonPropa = struct
| None -> D.reals
| Some d -> D.singleton d
- let upd del node d d' pexp =
+ let upd del node d d' =
match D.inter d d' with
| None ->
- let pexp = Egraph.mk_pexp del exp pexp in
- let pexp = Egraph.mk_pexp del exp (ExpEmptyDomInter(pexp,node)) in
Debug.dprintf6 debug "[LRA] upd node = %a d = %a d' = %a"
Node.pp node D.pp d D.pp d';
- Egraph.contradiction del pexp
+ Egraph.contradiction del
| Some d' ->
if not (D.equal d d')
- then set_dom del (Egraph.mk_pexp del exp pexp) node d'
- (Equal.option Q.equal (D.is_singleton d') None)
+ then set_dom del node d'
- let upd_value del node d d' pexp =
+ let upd_value del node d d' =
match D.inter d d' with
| None ->
- let pexp = Egraph.mk_pexp del exp pexp in
- let pexp = Egraph.mk_pexp del exp (ExpEmptyDomInter(pexp,node)) in
Debug.dprintf6 debug "[LRA] upd node = %a d = %a d' = %a"
Node.pp node D.pp d D.pp d';
- Egraph.contradiction del pexp
+ Egraph.contradiction del
| Some d' ->
if not (D.equal d d')
- then set_dom del (Egraph.mk_pexp del exp pexp) node d'
- (Equal.option Q.equal (D.is_singleton d') None)
+ then set_dom del node d'
let propagate del s =
match SE.sem s with
@@ -197,12 +167,11 @@ module DaemonPropa = struct
let d0 = get_value del cl0 in
if Q.equal q1 Q.one && Q.equal q2 Q.minus_one &&
D.equal d0 D.zero then
- let pexp = Egraph.mk_pexp del exp (ExpDistIsZero(s)) in
- Egraph.merge del pexp cl1 cl2
+ Egraph.merge del cl1 cl2
else
let d1 = get_value del cl1 in
let d2 = get_value del cl2 in
- let upd_value node d d' = upd_value del node d d' (ExpAdd(s,node)) in
+ let upd_value node d d' = upd_value del node d d' in
let qd1 = D.mult_cst q1 d1 in
let qd2 = D.mult_cst q2 d2 in
upd_value cl0 d0 (D.add qd1 qd2);
@@ -215,70 +184,12 @@ module DaemonPropa = struct
let dzero_false = if equal_bound b Strict then le_zero else lt_zero in
if D.is_included d dzero_true
then begin
- let pexp = Egraph.mk_pexp del exp (ExpGZeroUp(s,true)) in
- Boolean.set_true del pexp cl0
+ Boolean.set_true del cl0
end
else if D.is_included d dzero_false
then
- let pexp = Egraph.mk_pexp del exp (ExpGZeroUp(s,false)) in
- Boolean.set_false del pexp cl0
+ Boolean.set_false del cl0
end
- | S.Conflict(p,b) ->
- (** Choose representative of the equivalence class among the
- present classes, not the current representative *)
- let repr = Polynome.fold (fun acc node _ ->
- Node.M.add (Egraph.find del node) node acc)
- Node.M.empty p in
- let p' = Polynome.fold (fun acc node q ->
- let node = Egraph.find del node in
- let node = Node.M.find_exn Impossible node repr in
- Polynome.add acc (Polynome.monome q node)
- )
- (Polynome.cst p.cst)
- p in
- let rec aux d_first = function
- | [] -> begin
- let cl0 = SE.node s in
- if Equal.option Q.equal (D.is_singleton d_first) None then
- let d = d_first in
- let dzero_true = if equal_bound b Strict then gt_zero else ge_zero in
- let dzero_false = if equal_bound b Strict then le_zero else lt_zero in
- if D.is_included d dzero_true
- then begin
- let pexp = Egraph.mk_pexp del exp (ExpGZeroUp(s,true)) in
- Boolean.set_true del pexp cl0;
- raise Exit
- end
- else if D.is_included d dzero_false
- then
- let pexp = Egraph.mk_pexp del exp (ExpGZeroUp(s,false)) in
- Boolean.set_false del pexp cl0;
- raise Exit
- else
- assert false
- else
- match Boolean.is del cl0 with
- | Some nonot ->
- let dzero = if equal_bound b Strict
- then if nonot then gt_zero else le_zero
- else if nonot then ge_zero else lt_zero in
- dzero,nonot
- | None ->
- raise Exit
- end
- | (node,q)::l ->
- let d = get_dom del node in
- let d' = (D.mult_cst q d) in
- let d_last,b = aux (D.add d' d_first) l in
- Debug.dprintf6 debug "node=%a d_first=%a d_last=%a"
- Node.pp node D.pp d_first D.pp d_last;
- let upd node d d' = upd del node d d' (ExpGZeroDown(s,node,b)) in
- upd node d (D.mult_cst (Q.inv q) (D.minus d_last d_first));
- D.minus d_last d', b
- in
- try
- ignore (aux (D.singleton p'.cst) (Node.M.bindings p'.poly))
- with Exit -> ()
let wakeup del = function
| Events.Fired.EventValue(_,_,s)
@@ -303,16 +214,6 @@ module DaemonPropa = struct
Demon.Fast.attach del key
[Demon.Create.EventValue(SE.node s, Boolean.dom, s);
Demon.Create.EventValue(node, real, s)]
- | Conflict(p,_) ->
- Demon.Fast.attach del key
- [Demon.Create.EventValue(SE.node s, Boolean.dom, s)];
- Polynome.iter (fun node _ ->
- Egraph.register del node;
- Demon.Fast.attach del key
- [Demon.Create.EventValue(node, real, s);
- Demon.Create.EventChange(node, s);
- ]
- ) p
end;
propagate del s;
end
@@ -321,7 +222,7 @@ module RDaemonPropa = Demon.Fast.Register(DaemonPropa)
let zero = cst Q.zero
let one = cst Q.one
-let index s = SE.index s Term._Real
+let index s = SE.index s
let add' q1 cl1 q2 cl2 =
let norm q node = if Q.equal q Q.zero then Q.one, zero else q, node in
@@ -356,14 +257,8 @@ let of_poly p =
let to_poly = function
| S.Add(q1,cl1,q2,cl2) -> Polynome.of_list Q.one [cl1,q1;cl2,q2]
- | Conflict (p,_) -> p
| GZero _ -> raise Impossible
-let choarith =
- Trail.Cho.create_key (module struct type t = Node.t let name = "LRA.cho" end)
-
-let make_dec node = Trail.GCho(node,choarith,node)
-
(** Choice *)
(*
(** Conflict *)
@@ -623,359 +518,28 @@ let pp_hyppoly fmt c =
(bound c.bound)
Polynome.pp c.poly
-module HypDom = struct
- type t = hyppoly
-
- let pp = pp_hyppoly
-
- let key =
- Trail.Hyp.create_key (module struct type nonrec t = t let name = "Arith.hyp" end)
-
- let pp_v fmt v =
- let aux fmt (_,v) = pp_hyppoly fmt v in
- SE.M.bindings v |> Format.(list ~sep:(const char ';') aux) fmt
-
- let levels _ = assert false
- let split _ = assert false
- let apply_learnt hyp =
- match hyp.bound with
- | Eq ->
- let n = of_poly hyp.poly in
- (Equality.equality [n;zero], Conflict.Neg)
- | Le | Lt ->
- let b = if equal_hypbound hyp.bound Le then Interval.Large else Interval.Strict in
- let i = SE.index (S.Conflict(hyp.poly, b)) Term._Real in
- let i = SE.node i in
- (i, Conflict.Neg)
- let useful_nodes _ = assert false
-end
-
-let () = Conflict.register_hyp(module HypDom)
-
-module ExpEquality = struct
- (* open Conflict *)
-
- type t = exp
- let pp = pp_exp
- let key = exp
-
- (* let extract_add s node = match SE.sem s with
- * | S.Cst _
- * | S.GZero _
- * | S.Conflict _
- * -> raise Impossible
- * (\* cl1 = 1/q1*(SE.node s) - q2/q1*cl2 *\)
- * | S.Add (q1,cl1,q2,cl2) when Node.equal node cl1 ->
- * cl1, (Q.inv q1), SE.node s, Q.neg (Q.div q2 q1), cl2
- * (\* cl2 = 1/q2*(SE.node s) - q1/q2*cl1 *\)
- * | S.Add (q1,cl1,q2,cl2) when Node.equal node cl2 ->
- * cl2, (Q.inv q2), SE.node s, Q.neg (Q.div q1 q2), cl1
- * (\* SE.node s = q1*cl1 + q2*cl2 *\)
- * | S.Add (q1,cl1,q2,cl2) ->
- * SE.node s,q1,cl1,q2,cl2
- *
- * (\** the result must be physically one or the other *\)
- * let best_bound_inf op1 op2 =
- * match op1,op2 with
- * | None, None -> None
- * | None, (Some _ as p) | (Some _ as p), None -> p
- * | Some p1, Some p2 ->
- * let q1 = get_exp_conpoly p1 in
- * let q2 = get_exp_conpoly p2 in
- * if Interval.compare_bounds_inf (q1,p1.bound) (q2,p2.bound) < 0
- * then op2 else op1
- *
- * (\** the result must be physically one or the other *\)
- * let best_bound_sup op1 op2 =
- * match op1,op2 with
- * | None, None -> None
- * | None, (Some _ as p) | (Some _ as p), None -> p
- * | Some p1, Some p2 ->
- * let q1 = get_exp_conpoly p1 in
- * let q2 = get_exp_conpoly p2 in
- * if Interval.compare_bounds_sup (q1,p1.bound) (q2,p2.bound) < 0
- * then op1 else op2
- *
- * let best_bound p1 p2 =
- * { mi = best_bound_inf p1.mi p2.mi;
- * ma = best_bound_sup p1.ma p2.ma }
- *
- * (\**
- * 0 <= x + P x + Q < 0
- * implies
- * 0 < x - x + P - Q ( -P <= x < -Q )
- * there was an empty domain so that it was not verified. So for the proof
- * we suppose that it is not verified
- * 0 <= Q - P
- * *\)
- * let bound_distance_not_verified p1 =
- * { mi =
- * Opt.map2 (fun mi ma ->
- * let p = x_p_cy_conpoly ma Q.minus_one mi in
- * { p with bound = inv_bound p.bound }
- * ) p1.mi p1.ma;
- * ma = None }
- *
- * let get_pexp_or_add_def t pexp =
- * match Conflict.Helpers.get_pexp_or_add t pexp condom with
- * | None -> assert false
- * | Some p -> p
- *
- * let get_dom t age node =
- * (\* Look at all the modifications of the cls that are part of the
- * equivalence class of this node, and keep the two with the best bounds
- * *\)
- * Debug.dprintf2 ~nobox:() debug "@,@[<v 3>@[[LRA] get_dom for %a@]" Node.pp node;
- * let f t =
- * let mod_doms = get_dom_before_last_dec t age node dom in
- * let mi, ma =
- * List.fold_left
- * (fun (((mi,_) as miacc),((ma,_) as maacc))
- * (mod_dom:Trail.mod_dom) ->
- * (\** dom -> modcl *\)
- * let p' = (get_pexp_or_add_def t mod_dom.modpexp) in
- * let mi'' = best_bound_inf mi p'.mi in
- * let ma'' = best_bound_sup ma p'.ma in
- * (if mi'' == mi then miacc else (p'.mi,mod_dom.modcl)),
- * (if ma'' == ma then maacc else (p'.ma,mod_dom.modcl)))
- * ((None,(\* dumb *\) zero),(None,(\* dumb *\) zero))
- * mod_doms in
- * let f which = function
- * | (None,_) ->
- * Debug.dprintf0 debug "[LRA] Choose None";
- * None
- * | (d,modcl) ->
- * (\** node -> modcl *\)
- * Debug.dprintf4 debug "[LRA] Choose %a from %a" (Opt.pp pp_conpoly) d Node.pp modcl;
- * Opt.map2 add_conpoly d (which (get_rlist_conpair t node modcl))
- * in
- * { mi = f (fun c -> c.mi) mi; ma = f (fun c -> c.ma) ma }
- * in
- * let p,deps = ComputeConflict.wrap_deps t f in
- * let add_deps m = {m with deps = Deps.concat deps m.deps } in
- * Debug.dprintf0 ~nobox:() debug "@]";
- * { mi = Opt.map add_deps p.mi; ma = Opt.map add_deps p.ma }
- *
- *
- * let analyse t age con = function
- * | ExpCst(node,q) ->
- * Conflict.return con condom
- * (mk_conpair (Polynome.of_list (Q.neg q) [node,Q.one]))
- * | ExpAdd (s,cls) -> begin
- * match SE.sem s with
- * | S.Add _->
- * let cl0, q1, cl1, q2, cl2 = extract_add s cls in
- * let d1 = get_dom t age cl1 in
- * (\* Debug.dprintf2 debug "[LRA] d1=%a" pp_conpair d1; *\)
- * let d2 = get_dom t age cl2 in
- * (\* Debug.dprintf2 debug "[LRA] d2=%a" pp_conpair d2; *\)
- * let semv = mk_conpair
- * (Polynome.of_list Q.zero [cl0,Q.one;cl1,Q.neg q1;cl2,Q.neg q2]) in
- * let d0 = add_conpair semv (cx_p_cy_conpair q1 d1 q2 d2) in
- * (\* Debug.dprintf2 debug "[LRA] d0=%a" pp_conpair d0; *\)
- * (\* Debug.dprintf10 debug *\)
- * (\* "[LRA] cl0=%a q1=%a cl1=%a q2=%a cl2=%a" *\)
- * (\* Node.pp cl0 Q.pp q1 Node.pp cl1 Q.pp q2 Node.pp cl2 ; *\)
- * Conflict.return con condom d0
- * | S.Conflict p ->
- * let repr = Polynome.fold (fun acc node _ ->
- * Node.M.add (Conflict.ComputeConflict.get_repr_at t age node) node acc)
- * Node.M.empty p in
- * let cl0 = SE.node s in
- * let semv,p' = Polynome.fold (fun (semv,acc) node q ->
- * let node' = Conflict.ComputeConflict.get_repr_at t age node in
- * let node' = Node.M.find_exn Impossible node' repr in
- * let semv = x_p_cy_conpair semv q (get_rlist_conpair t node' node) in
- * semv,Polynome.add acc (Polynome.monome q node')
- * )
- * (mk_conpair p,Polynome.cst p.cst)
- * p in
- * let pcl0 = Polynome.monome Q.minus_one cl0 in
- * let semv = add_conpair semv (mk_conpair pcl0) in
- * let p' = Polynome.add p' pcl0 in
- * Debug.dprintf2 debug "[LRA] p=%a" Polynome.pp p;
- * Debug.dprintf2 debug "[LRA] semv=%a" pp_conpair semv;
- * Debug.dprintf2 debug "[LRA] p'=%a" Polynome.pp p';
- * let mi = match semv.mi with
- * | None -> assert false
- * | Some mi -> mi in
- * assert (Polynome.equal p' mi.exp);
- * let qcls = Node.M.find_exn Impossible cls (mi.exp).poly in
- * let semv = cst_mult_conpair (Q.inv qcls) semv in
- * let mi = match semv.mi with
- * | None -> assert false
- * | Some mi -> mi in
- * let semv =
- * Polynome.fold (fun semv node q ->
- * if Node.equal node cls then semv
- * else
- * let d = get_dom t age node in
- * x_p_cy_conpair semv (Q.neg q) d
- * ) semv (mi.exp) in
- * Conflict.return con condom semv
- * | _ -> raise Impossible
- * end
- * | ExpGZeroDown (s,nonot) ->
- * let node,b = match SE.sem s with
- * | S.GZero (node,b) -> node,b
- * | _ -> raise Impossible in
- * let cl0 = SE.node s in
- * ComputeConflict.unknown_con t conclause
- * (Boolean.get_dom t age cl0 Node.M.empty);
- * let p =
- * let exp = Polynome.monome Q.one node in
- * if nonot
- * then
- * {mi = Some
- * { imp = exp; exp; bound=b;
- * deps = Deps.empty};
- * ma = None}
- * else
- * {ma = Some
- * { imp = exp; exp;
- * bound=inv_bound b;
- * deps = Deps.empty};
- * mi = None}
- * in
- * Conflict.return con condom p
- * | ExpEmptyDomMerge (pexp,cl1,cl2) ->
- * let d1 = get_dom t age cl1 in
- * let d2 = get_dom t age cl2 in
- * let eq,deps =
- * Conflict.ComputeConflict.Equal.one_pexp t ~from:cl1 ~to_:cl2 condom
- * zero_conpair Deps.empty pexp
- * in
- * Conflict.ComputeConflict.add_deps t deps;
- * assert (conpair_is_an_equality eq);
- * Debug.dprintf6 debug "d1=%a;@ d2=%a;@ eq=%a"
- * pp_conpair d1 pp_conpair d2 pp_conpair eq;
- * let d2 = add_conpair eq d2 in
- * let r = best_bound d1 d2 in
- * Debug.dprintf4 debug "d2=%a@ r=%a"
- * pp_conpair d2 pp_conpair r;
- * let r = bound_distance_not_verified r in
- * assert (None <> r.mi);
- * assert (match Polynome.is_cst (Opt.get r.mi).exp,
- * (Opt.get r.mi).bound with
- * | Some q, Strict -> Q.lt Q.zero q
- * | Some q, Large -> Q.leq Q.zero q
- * | None,_ -> false);
- * return con condom r
- * | ExpEmptyDomInter (pexp,cl1) ->
- * let d1 = get_dom t age cl1 in
- * Debug.dprintf2 debug "d1=%a" pp_conpair d1;
- * let d2 = (get_pexp_or_add_def t pexp) in
- * Debug.dprintf2 debug "d2=%a" pp_conpair d2;
- * let r' = best_bound d1 d2 in
- * let r = bound_distance_not_verified r' in
- * Debug.dprintf4 debug "r'=%a r=%a@"
- * pp_conpair r' pp_conpair r;
- * assert (None <> r.mi);
- * assert (match Polynome.is_cst (Opt.get r.mi).exp,
- * (Opt.get r.mi).bound with
- * | Some q, Strict -> Q.lt Q.zero q
- * | Some q, Large -> Q.leq Q.zero q
- * | None,_ -> false);
- * return con condom r
- * | ExpGZeroUp(s,nonot) ->
- * let node,b = match SE.sem s with
- * | S.GZero (node,b) -> node,b
- * | _ -> raise Impossible in
- * let d = get_dom t age node in
- * Debug.dprintf6 debug "node=%a %a d=%a" Node.pp node pp_bound b pp_conpair d;
- * if nonot then begin
- * assert ( implies d {ma = None; mi = Some { (mk_conpoly (Polynome.monome Q.one node)) with bound = b}} );
- * ComputeConflict.unknown_con t condom
- * { d with ma = None }
- * end else begin
- * assert ( implies d {mi = None; ma = Some { (mk_conpoly (Polynome.monome Q.one node))
- * with bound = inv_bound b}} );
- * ComputeConflict.unknown_con t condom
- * { d with mi = None }
- * end;
- * Conflict.return con conclause Node.M.empty
- * | ExpDistIsZero s ->
- * let cl0, q1, cl1, q2, cl2 = extract_add s (SE.node s) in
- * let d0 = get_dom t age cl0 in
- * let semv = mk_conpair
- * (Polynome.of_list Q.zero [cl0,Q.minus_one;cl1,q1;cl2,q2]) in
- * return con condom (add_conpair semv d0)
- * | ExpIsSingleton(pexp,node,b,cst) ->
- * let q = match SE.sem cst with | Cst q -> q | _ -> raise Impossible in
- * let d1 = if b then get_dom t age node else {mi=None;ma=None} in
- * let d2 = (get_pexp_or_add_def t pexp) in
- * let r = best_bound d1 d2 in
- * Debug.dprintf8
- * debug
- * "r=%a d1=%a d2=%a q=%a"
- * pp_conpair r pp_conpair d1 pp_conpair d2 Q.pp q;
- * Conflict.return con condom r
- *
- * let expdomlimit _t _age dom' node con v _ =
- * let v = Opt.get_exn Impossible v in
- * let v = Dom.Eq.coerce dom' dom v in
- * let mk = function
- * | None -> None
- * | Some (v,bound) ->
- * let p = Polynome.of_list (Q.neg v) [node,Q.one] in
- * Some {imp = p; exp = p; bound; deps = Deps.empty} in
- * let mi,ma = D.get_convexe_hull v in
- * return con condom {mi=mk mi;ma=mk ma}
- *
- *
- * let same_sem (type a) t age (sem':a sem) (v:a) con exp cl1 cl2 =
- * let r1 = analyse t age condom exp in
- * let p = match r1 with
- * | GRequested p1 ->
- * let p2 =
- * match Sem.Eq.eq_type S.key sem' with
- * | None -> raise Impossible (\* understand why that happend *\)
- * | Some Types.Eq ->
- * Polynome.x_p_cy (Polynome.monome Q.one cl2) Q.minus_one
- * (to_poly v)
- * in
- * x_p_cy_conpair p1 Q.minus_one (mk_conpair p2)
- * | GOther _ -> raise Impossible (\* not created by analyse *\)
- * in
- * Debug.dprintf6 debug_todo "@[same_sem cl1:%a cl2:%a = %a@]"
- * Node.pp cl1 Node.pp cl2 pp_conpair p;
- * assert (conpair_is_an_equality p);
- * assert (Polynome.equal (Opt.get p.mi).exp (dist cl1 cl2));
- * Conflict.return con condom p *)
-
- let analyse _ = assert false
- let from_contradiction _ = assert false
-
-end
-
-let () = Conflict.register_exp(module ExpEquality)
-
-
module ChoLRA = struct
- open Conflict
-
- module OnWhat = Node
-
let make_decision node b env =
- Debug.dprintf4 print_decision
+ Debug.dprintf4 Egraph.print_decision
"[LRA] decide %a on %a" Q.pp b Node.pp node;
- let pexp = Egraph.mk_pexp env exp (ExpDec(node,b)) in
- set_dom env pexp node (D.singleton b) false
+ set_dom env node (D.singleton b)
- let choose_decision env node =
+ let choose_decision node env =
let v = Opt.get_def D.reals (Egraph.get_dom env dom node) in
match D.is_singleton v with
- | Some _ -> DecNo
+ | Some _ -> Egraph.DecNo
| None -> DecTodo (make_decision node (D.choose v))
- let key = choarith
-end
+ let choice n = {
+ Egraph.prio = 1;
+ choice = choose_decision n;
+ }
-let () = Conflict.register_cho(module ChoLRA)
+end
(** API *)
-let index x = SE.node (SE.index x Term._Real)
+let index x = SE.node (SE.index x)
let as_node node = index (S.Add (Q.one,node,Q.one,zero))
@@ -997,10 +561,10 @@ let mult_cst cst node =
add' cst node Q.one zero
let gt_zero node =
- SE.node (SE.index (GZero(node,Strict)) Boolean.ty)
+ SE.node (SE.index (GZero(node,Strict)))
let ge_zero node =
- SE.node (SE.index (GZero(node,Large)) Boolean.ty)
+ SE.node (SE.index (GZero(node,Large)))
let lt cl1 cl2 = gt_zero (sub cl2 cl1)
let le cl1 cl2 = ge_zero (sub cl2 cl1)
@@ -1008,42 +572,55 @@ let gt cl1 cl2 = lt cl2 cl1
let ge cl1 cl2 = le cl2 cl1
(** {2 Initialization} *)
-let converter d f l =
+let converter d (f:Expr.Term.t) =
let of_term t =
let n = SynTerm.node_of_term t in
Egraph.register d n;
n
in
- let node = match f, l with
- | f,[] when Term.is_const_real_term f ->
- Some (cst (Term.get_const_real_term f))
- | f,a::args when Term.is_add_real_term f ->
- Some (List.fold_left add (of_term a) (List.map of_term args))
- | f,[arg1;arg2] when Term.equal f Term.sub_real_term ->
- Some (sub (of_term arg1) (of_term arg2))
- | f,[arg] when Term.equal f Term.neg_real_term ->
- Some (neg (of_term arg))
- | f,args when Term.equal f Term.mul_real_term -> begin
- let mult_cst c t =
- Some (mult_cst (Term.get_const_real_term c) (of_term t))
- in
- match args with
- | [arg1;arg2] when Term.is_const_real_term arg1 ->
- mult_cst arg1 arg2
- | [arg1;arg2] when Term.is_const_real_term arg2 ->
- mult_cst arg2 arg1
- | _ -> None
- end
- | f,[arg1;arg2] when Term.is_lt_real_term f ->
- Some (lt (of_term arg1) (of_term arg2))
- | f,[arg1;arg2] when Term.is_le_real_term f ->
- Some (le (of_term arg1) (of_term arg2))
- | _ -> None in
- node
-
-let decvars n =
- if Ty.equal (Node.ty n) Term._Real
- then Some (make_dec n)
+ match f with
+ | { descr = Expr.App({builtin = Expr.Integer s},[],[]); _ } ->
+ Some (cst (Q.of_string s))
+ | { descr = Expr.App({builtin = Expr.Decimal s},[],[]); _ } ->
+ Some (cst (Q.of_string_decimal s))
+ | { descr = Expr.App({builtin = Expr.Rational s},[],[]); _ } ->
+ Some (cst (Q.of_string_decimal s))
+ | { descr = Expr.App({builtin = Expr.Add},[],[a;b]); _ } ->
+ Some (add (of_term a) (of_term b))
+ | { descr = Expr.App({builtin = Expr.Sub},[],[a;b]); _ } ->
+ Some (sub (of_term a) (of_term b))
+ | { descr = Expr.App({builtin = Expr.Neg},[],[a]); _ } ->
+ Some (neg (of_term a))
+ | { descr = Expr.App({builtin = Expr.Mul},[],args); _ } -> begin
+ let mult_cst c t = Some (mult_cst c (of_term t)) in
+ match args with
+ | [{descr = Expr.App({builtin = Expr.Integer s; _},[],[])};arg2] ->
+ mult_cst (Q.of_string s) arg2
+ | [{descr = Expr.App({builtin = Expr.Decimal s; _},[],[])};arg2] ->
+ mult_cst (Q.of_string_decimal s) arg2
+ | [{descr = Expr.App({builtin = Expr.Rational s; _},[],[])};arg2] ->
+ mult_cst (Q.of_string_decimal s) arg2
+ | [arg2;{descr = Expr.App({builtin = Expr.Integer s; _},[],[])}] ->
+ mult_cst (Q.of_string s) arg2
+ | [arg2;{descr = Expr.App({builtin = Expr.Decimal s; _},[],[])}] ->
+ mult_cst (Q.of_string_decimal s) arg2
+ | [arg2;{descr = Expr.App({builtin = Expr.Rational s; _},[],[])}] ->
+ mult_cst (Q.of_string_decimal s) arg2
+ | _ -> None
+ end
+ | { descr = Expr.App({builtin = Expr.Lt},[],[arg1;arg2]); _ } ->
+ Some (lt (of_term arg1) (of_term arg2))
+ | { descr = Expr.App({builtin = Expr.Leq},[],[arg1;arg2]); _ } ->
+ Some (le (of_term arg1) (of_term arg2))
+ | { descr = Expr.App({builtin = Expr.Gt},[],[arg1;arg2]); _ } ->
+ Some (gt (of_term arg1) (of_term arg2))
+ | { descr = Expr.App({builtin = Expr.Geq},[],[arg1;arg2]); _ } ->
+ Some (ge (of_term arg1) (of_term arg2))
+ | _ -> None
+
+let decvars t n =
+ if Expr.Ty.equal (Expr.Term.ty t) Expr.Ty.real
+ then Some (ChoLRA.choice n)
else None
@@ -1063,8 +640,6 @@ let th_register env =
(fun d value ->
let v = RealValue.value value in
let s = D.singleton v in
- let _pexp = Egraph.mk_pexp d exp (ExpCst value) in
- (** something must be done with the pexp *)
Egraph.set_dom d dom (RealValue.node value) s
) env;
()
@@ -1080,44 +655,48 @@ let () =
match t with
| Add(q1,n1,q2,n2) ->
let v = Q.( q1 * (get_v n1) + q2 * (get_v n2)) in
- RealValue.nodevalue (RealValue.index v Term._Real)
+ RealValue.nodevalue (RealValue.index v)
| GZero(n,bound) ->
gzero bound (get_v n)
- | Conflict (p,bound) ->
- let v = Polynome.fold (fun acc n q -> Q.( acc + q * (get_v n))) Q.zero p in
- gzero bound v
in
Interp.Register.thterm S.key interp
let default_value = Q.zero
-let () =
- Interp.Register.model Term._Real (fun d n ->
- let v = Egraph.get_value d real n in
- let v = Witan_popop_lib.Opt.get_def default_value v in
- let v = RealValue.nodevalue (RealValue.index v Term._Real) in
- v)
+(* let () =
+ * Interp.Register.model Term._Real (fun d n ->
+ * let v = Egraph.get_value d real n in
+ * let v = Witan_popop_lib.Opt.get_def default_value v in
+ * let v = RealValue.nodevalue (RealValue.index v Term._Real) in
+ * v) *)
let () =
- Interp.Register.id (fun id args ->
- let is builtin = Term.Id.equal id builtin in
- let (!>) n = RealValue.value (RealValue.coerce_nodevalue n) in
- let (!<) v = Some (RealValue.nodevalue (RealValue.index v Term._Real)) in
+ Interp.Register.id (fun interp t ->
+ let (!>) t = RealValue.value (RealValue.coerce_nodevalue (interp t)) in
+ let (!<) v = Some (RealValue.nodevalue (RealValue.index v)) in
let (!<<) b = Some (if b then Boolean.values_true else Boolean.values_false) in
- match args with
- | [] when Term.is_const_real_id id ->
- !< (Term.get_const_real_id id)
- | args when Term.is_add_real_id id ->
- !< (List.fold_left (fun acc a -> Q.add acc (!> a)) Q.zero args)
- | [arg1;arg2] when is Term.sub_real_id ->
- !< (Q.sub (!> arg1) (!> arg2))
- | [arg] when is Term.neg_real_id ->
- !< (Q.neg (!> arg))
- | [arg1;arg2] when is Term.mul_real_id ->
- !< (Q.mul (!> arg1) (!> arg2))
- | [arg1;arg2] when Term.is_lt_real_id id ->
- !<< (Q.lt (!> arg1) (!> arg2))
- | [arg1;arg2] when Term.is_le_real_id id ->
- !<< (Q.le (!> arg1) (!> arg2))
- | _ -> None
+ match t with
+ | { descr = Expr.App({builtin = Expr.Integer s},[],[]); _ } ->
+ !< (Q.of_string s)
+ | { descr = Expr.App({builtin = Expr.Decimal s},[],[]); _ } ->
+ !< (Q.of_string_decimal s)
+ | { descr = Expr.App({builtin = Expr.Rational s},[],[]); _ } ->
+ !< (Q.of_string_decimal s)
+ | { descr = Expr.App({builtin = Expr.Add},[],[a;b]); _ } ->
+ !< (Q.add !>a !>b)
+ | { descr = Expr.App({builtin = Expr.Sub},[],[a;b]); _ } ->
+ !< (Q.sub !>a !>b)
+ | { descr = Expr.App({builtin = Expr.Neg},[],[a]); _ } ->
+ !< (Q.neg !>a)
+ | { descr = Expr.App({builtin = Expr.Mul},[],[a;b]); _ } ->
+ !< (Q.mul !>a !>b)
+ | { descr = Expr.App({builtin = Expr.Lt},[],[arg1;arg2]); _ } ->
+ !<< (Q.lt !>arg1 !>arg2)
+ | { descr = Expr.App({builtin = Expr.Leq},[],[arg1;arg2]); _ } ->
+ !<< (Q.leq !>arg1 !>arg2)
+ | { descr = Expr.App({builtin = Expr.Gt},[],[arg1;arg2]); _ } ->
+ !<< (Q.gt !>arg1 !>arg2)
+ | { descr = Expr.App({builtin = Expr.Geq},[],[arg1;arg2]); _ } ->
+ !<< (Q.geq !>arg1 !>arg2)
+ | _ -> None
)
diff --git a/src/theories/bool/boolean.ml b/src/theories/bool/boolean.ml
index 9bf7e90d57d5d6022336f3e0fb03814c646f6072..3121fa1d8bb7f228ecbef04da2bded41c4ee80ab 100644
--- a/src/theories/bool/boolean.ml
+++ b/src/theories/bool/boolean.ml
@@ -29,7 +29,6 @@ let debug = Debug.register_info_flag
~desc:"for the boolean theory"
"bool"
-let ty = Term._Prop
let dom = ValueKind.create_key (module struct type t = bool let name = "bool" end)
module BoolValue = ValueKind.Register(struct
@@ -37,11 +36,11 @@ module BoolValue = ValueKind.Register(struct
let key = dom
end)
-let value_true = BoolValue.index ~basename:"⊤" true ty
+let value_true = BoolValue.index ~basename:"⊤" true
let values_true = BoolValue.nodevalue value_true
let node_true = BoolValue.node value_true
-let value_false = BoolValue.index ~basename:"⊥" false ty
+let value_false = BoolValue.index ~basename:"⊥" false
let values_false = BoolValue.nodevalue value_false
let node_false = BoolValue.node value_false
@@ -49,7 +48,7 @@ let node_false = BoolValue.node value_false
(* let union_disjoint m1 m2 =
* Node.M.union (fun _ b1 b2 -> assert (Equal.physical b1 b2); Some b1) m1 m2 *)
-let index sem v = Node.index_sem sem v ty
+let index sem v = Node.index_sem sem v
let is env node = Egraph.get_value env dom node
let is_true env node = Node.equal node node_true
@@ -58,8 +57,8 @@ let is_false env node = Node.equal node node_false
|| Equal.option Equal.bool (is env node) (Some false)
let is_unknown env node = Equal.option Equal.bool (is env node) None
-let set_bool env pexp node b =
- Egraph.merge env pexp node
+let set_bool env node b =
+ Egraph.merge env node
(if b then node_true else node_false)
type t =
@@ -166,22 +165,6 @@ end
module ThE = ThTermKind.Register(Th)
-(** At least all the leaves except one are known and can be discarded *)
-type bcpkind =
- | BCPOwnKnown (** Top is known and true modulo topnot, propagate true modulo sign to propa *)
- | BCPLeavesKnown (** All leaves are known and false modulo sign, propagate false modulo topnot to own *)
- | BCP (** Merge top with the remaining leave *)
-[@@deriving eq]
-
-type expprop =
-| ExpBCP of ThE.t (* own *) * Node.t (* propa *) * bcpkind
-| ExpUp of ThE.t (* own *) * Node.t (* one leaf to own *)
-| ExpDown of ThE.t (* own *) * Node.t (* leaf *)(* own to leaf *)
-| ExpNot of (Th.t * Node.t * Node.t) * bool (* what have been propagated *)
-| ExpDec of Node.t * bool
-
-let expprop = Exp.create_key (module struct type t = expprop let name = "Bool.prop" end)
-
module DaemonPropaNot = struct
module Data = struct
@@ -195,13 +178,12 @@ module DaemonPropaNot = struct
let throttle = 100
let wakeup d =
function
- | Events.Fired.EventValue(_,dom',((_,node,ncl) as x)) ->
+ | Events.Fired.EventValue(_,dom',((_,node,ncl))) ->
assert (ValueKind.equal dom dom');
begin match Egraph.get_value d dom node with
| None -> raise Impossible
| Some b ->
- let pexp = Egraph.mk_pexp d expprop (ExpNot(x,not b)) in
- set_bool d pexp ncl (not b)
+ set_bool d ncl (not b)
end;
| _ -> raise UnwaitedEvent
@@ -210,14 +192,11 @@ module DaemonPropaNot = struct
let own = ThE.node thterm in
match is d own with
| Some b ->
- let pexp = Egraph.mk_pexp d expprop (ExpNot((v,own,node),not b)) in
- set_bool d pexp node (not b)
+ set_bool d node (not b)
| None ->
match is d node with
| Some b ->
- let pexp = Egraph.mk_pexp d expprop
- (ExpNot((v,node,own),not b)) in
- set_bool d pexp own (not b)
+ set_bool d own (not b)
| None ->
let events = [Demon.Create.EventValue(own,dom,(v,own,node));
Demon.Create.EventValue(node,dom,(v,node,own))] in
@@ -252,35 +231,26 @@ module DaemonPropa = struct
let wakeup_lit d thterm watched watcher =
let v = ThE.sem thterm in
let own = ThE.node thterm in
- let pexp exp = Egraph.mk_pexp d expprop exp in
- let set_dom_up_true d own leaf _ =
+ let set_dom_up_true d own _ _ =
let b = (not v.topnot) in
match Egraph.get_value d dom own with
| Some b' when Equal.bool b' b -> ()
- | _ -> set_bool d (pexp (ExpUp(thterm,leaf))) own b in
+ | _ -> set_bool d own b in
let merge_bcp node sign =
Debug.dprintf2 debug "[Bool] @[merge_bcp %a@]" Node.pp node;
match Egraph.get_value d dom own with
| Some b' ->
- let pexp = if (mulbool b' v.topnot)
- then pexp (ExpBCP(thterm,node,BCPOwnKnown))
- else pexp (ExpDown(thterm,node))
- in
let b = mulbool sign (mulbool b' v.topnot) in
- set_bool d pexp node b
+ set_bool d node b
| None -> (** merge *)
match Egraph.get_value d dom node with
| Some b' ->
- let pexp = if (mulbool b' sign)
- then pexp (ExpUp(thterm,node))
- else pexp (ExpBCP(thterm,node,BCPLeavesKnown))
- in
let b = mulbool sign (mulbool b' v.topnot) in
- set_bool d pexp own b
+ set_bool d own b
| None -> (** merge *)
if mulbool v.topnot sign
then DaemonPropaNot.init d thterm node
- else Egraph.merge d (pexp (ExpBCP(thterm,node,BCP))) own node in
+ else Egraph.merge d own node in
let rec find_watch dir pos bound =
assert (dir = 1 || dir = -1);
if pos = bound
@@ -319,7 +289,6 @@ module DaemonPropa = struct
let wakeup_own d thterm =
let v = ThE.sem thterm in
let own = ThE.node thterm in
- let pexp exp = Egraph.mk_pexp d expprop exp in
begin match Egraph.get_value d dom own with
| None -> (* only during init *)
Demon.Fast.attach d key
@@ -327,8 +296,7 @@ module DaemonPropa = struct
true
(** \/ c1 c2 = false ==> c1 = false /\ c2 = false *)
| Some b when not (mulbool v.topnot b) ->
- let set_dom_down_false (node,sign) =
- set_bool d (pexp (ExpDown(thterm,node))) node sign in
+ let set_dom_down_false (node,sign) = set_bool d node sign in
IArray.iter set_dom_down_false v.lits;
false
| Some _ -> true
@@ -440,241 +408,65 @@ let mk_clause m =
let _false = node_false
-let set_true env pexp node = set_bool env pexp node true
-
-let () =
- let gen_or l =
- let l = List.map (function
- | (n,Conflict.Pos) -> (n,false)
- | (n,Conflict.Neg) -> (n,true)) l in
- gen false l in
- Conflict._or := gen_or;
- Conflict._set_true := set_true;
- Conflict._is_true := is_true
-
-let set_false env pexp node = set_bool env pexp node false
+let set_true env node = set_bool env node true
+let set_false env node = set_bool env node false
-let chobool = Trail.Cho.create_key (module struct type t = Node.t let name = "Bool.cho" end)
-let make_dec node = Trail.GCho(node,chobool,node)
-
-let converter d f l =
+let converter d (f:Expr.Term.t) =
let of_term t =
let n = SynTerm.node_of_term t in
Egraph.register d n;
n
in
- let node = match f, l with
- | f,args when Term.is_or_term f ->
- Some (_or (List.map of_term args))
- | f,args when Term.is_and_term f ->
- Some (_and (List.map of_term args))
- | f,[arg1;arg2] when Term.equal f Term.imply_term ->
- Some (gen false [of_term arg1,true;of_term arg2,false])
- | f,[arg] when Term.equal f Term.not_term ->
- Some (_not (of_term arg))
- | f,[] when Term.equal f Term.true_term ->
- Some _true
- | f,[] when Term.equal f Term.false_term ->
- Some _false
- | _ -> None in
- node
-
-let decvars n =
- if Ty.equal (Node.ty n) ty
- then Some (make_dec n)
- else None
-
-let th_register env =
- RDaemonPropaNot.init env;
- RDaemonPropa.init env;
- RDaemonInit.init env;
- Demon.Fast.attach env
- DaemonInit.key [Demon.Create.EventRegSem(sem,())];
- Egraph.register env node_true;
- Egraph.register env node_false;
- SynTerm.register_converter env converter;
- SynTerm.register_decvars env decvars;
- ()
+ match f with
+ | { descr = Expr.App({builtin = Expr.Or},[],args); _ } ->
+ Some (_or (List.map of_term args))
+ | { descr = Expr.App({builtin = Expr.And},[],args); _ } ->
+ Some (_and (List.map of_term args))
+ | { descr = Expr.App({builtin = Expr.Imply},[],[arg1;arg2]); _ } ->
+ Some (gen false [of_term arg1,true;of_term arg2,false])
+ | { descr = Expr.App({builtin = Expr.Neg},[],[arg]); _ } ->
+ Some (_not (of_term arg))
+ | { descr = Expr.App({builtin = Expr.True},[],[]); _ } ->
+ Some _true
+ | { descr = Expr.App({builtin = Expr.False},[],[]); _ } ->
+ Some _false
+ | _ -> None
(** {2 Choice on bool} *)
module ChoBool = struct
- open Conflict
-
- module OnWhat = Node
- module What = DBool
-
let make_decision env node b =
- Debug.dprintf3 print_decision "[Bool] decide %b on %a" b Node.pp node;
- let pexp = Egraph.mk_pexp env expprop (ExpDec(node,b)) in
- set_bool env pexp node b
+ Debug.dprintf3 Egraph.print_decision "[Bool] decide %b on %a" b Node.pp node;
+ set_bool env node b
- let choose_decision env node =
+ let choose_decision node env =
match Egraph.get_value env dom node with
- | Some _ -> DecNo
+ | Some _ -> Egraph.DecNo
| None -> DecTodo (fun env -> make_decision env node true) (** why not true? *)
- let key = chobool
-
-end
-
-let () = Conflict.register_cho (module ChoBool)
-
-(** {2 Conflict} *)
-
-(** We could use instead directly EqHyp, but it gives an example of a
- simple conflict other than EqHyp *)
-module HypProp = struct
- type t = (Node.t * bool)
-
- let pp fmt (n,b) =
- if b
- then Format.fprintf fmt "¬%a" Node.pp n
- else Node.pp fmt n
-
- let key = Trail.Hyp.create_key (module struct type nonrec t = t let name = "hypprop" end)
-
- let apply_learnt (n,b) = (n,if b then Conflict.Neg else Conflict.Pos)
-
- let node_of_sign b = (node_of_bool (mulbool true b))
-
- let levels t (n,b) =
- let levels = Conflict.Levels.empty in
- let age = Conflict.Conflict.age_merge t n (node_of_sign b) in
- Conflict.Levels.add t age levels
-
- let useful_nodes (n,_) = Bag.elt n
-
- let split t (n,b) a' b' =
- let l', r' = Conflict.EqHyp.split t {l=n;r=node_of_sign b} a' b' in
- (match l' with
- | None -> []
- | Some r -> [Trail.Phyp.phyp Conflict.EqHyp.key {l=n; r}])
- @
- (match r' with
- | None -> []
- | Some l -> [Trail.Phyp.phyp key (l,b)])
-
end
-let () = Conflict.register_hyp (module HypProp)
-
-(** {2 Explanation} *)
-
-module ExpProp = struct
- open Conflict
- type t = expprop
-
- let pp fmt = function
- | ExpBCP (thterm,node,kind) ->
- Format.fprintf fmt "Bcp(%a,%a = %a;%t)"
- ThE.pp thterm Node.pp (ThE.node thterm) Node.pp node
- (fun _ -> match kind with
- | BCPOwnKnown -> Format.fprintf fmt "Own"
- | BCPLeavesKnown -> Format.fprintf fmt "Leaves"
- | BCP -> ())
- | ExpUp (thterm,leaf) ->
- Format.fprintf fmt "Up(%a,%a <- %a)"
- ThE.pp thterm Node.pp (ThE.node thterm) Node.pp leaf
- | ExpDown (thterm,node) ->
- Format.fprintf fmt "Down(%a,%a,%a ->)"
- ThE.pp thterm Node.pp (ThE.node thterm) Node.pp node
- | ExpNot ((v,clf,clt),b) ->
- Format.fprintf fmt "Not(%a,%a,%a,%b)"
- Th.pp v Node.pp clf Node.pp clt b
- | ExpDec (n,b) ->
- Format.fprintf fmt "Dec(%a,%b)"
- Node.pp n b
-
- let eq_of_bool ?dec n b =
- Trail.Phyp.phyp ?dec HypProp.key (n,not b)
-
- let analyse_one_to_one ?dec t phyp to_ to_b from_ from_b =
- (** we have
- c: a = b
- we propagated: to_ = to_b
- because : from_ = from_b
- *)
- let to_not = node_of_bool to_b in
- let eqs = Conflict.split t phyp to_ to_not in
- let eq = eq_of_bool ?dec from_ from_b in
- Debug.dprintf10 debug "clfrom:%a from_b:%b clto:%a to_b:%b eqs:%a eq:%a"
- Node.pp from_
- from_b
- Node.pp to_
- to_b
- (Format.(list ~sep:(const char ',') pp_phyp))
- eqs
- pp_phyp eq;
- (eq::eqs)
-
- let analyse :
- Conflict.t ->
- t -> Trail.Phyp.t -> Trail.Phyp.t list =
- fun t exp phyp ->
- match exp with
- | ExpBCP (thterm,_,_) when IArray.length (ThE.sem thterm).lits = 1 ->
- raise Impossible
- | ExpBCP (thterm,propa,kind) ->
- let v = ThE.sem thterm in
- let own = ThE.node thterm in
- let eqs =
- match kind with
- | BCP -> Conflict.split t phyp own propa
- | BCPOwnKnown ->
- let propa_sign = mulbool true (Opt.get (find v propa)) in
- Conflict.split t phyp propa (node_of_bool propa_sign)
- | BCPLeavesKnown ->
- let sign = mulbool false v.topnot in
- Conflict.split t phyp propa (node_of_bool sign)
- in
- let eqs = if equal_bcpkind kind BCPOwnKnown then (eq_of_bool own (mulbool true v.topnot))::eqs else eqs in
- fold (fun eqs (node,sign) ->
- if (not(equal_bcpkind kind BCPLeavesKnown)) && (Node.equal node propa) then eqs
- else (eq_of_bool node (mulbool false sign))::eqs) eqs v
- | ExpUp (thterm,leaf) ->
- let v = ThE.sem thterm in
- let own = ThE.node thterm in
- analyse_one_to_one t phyp
- own (mulbool true v.topnot)
- leaf (mulbool true (Opt.get (find v leaf)))
- | ExpDown (thterm,leaf) ->
- let v = ThE.sem thterm in
- let own = ThE.node thterm in
- analyse_one_to_one t phyp
- leaf (mulbool false (Opt.get (find v leaf)))
- own (mulbool false v.topnot)
- | ExpNot ((_,clfrom,clto),b)->
- analyse_one_to_one t phyp
- clto b
- clfrom (not b)
- | ExpDec (cl,b) ->
- analyse_one_to_one ~dec:() t phyp
- cl b
- cl b
-
- let key = expprop
-
- let from_contradiction _ _ =
- assert false (** absurd: never used for contradiction *)
-end
+let chobool n = {
+ Egraph.prio = 1;
+ choice = ChoBool.choose_decision n;
+}
-let () = Conflict.register_exp(module ExpProp)
+let decvars t n =
+ if Ty.equal (Expr.Term.ty t) Dolmen_std.Expr.Ty.bool
+ then Some (chobool n)
+ else None
-let () =
- let parity_of_bool b = if b then Conflict.Neg else Conflict.Pos in
- Conflict.EqHyp.register_apply_learnt ty
- (fun {Conflict.EqHyp.l;r} ->
- if Node.equal l node_false
- then (r,parity_of_bool true)
- else if Node.equal l node_true
- then (r,parity_of_bool false)
- else if Node.equal r node_false
- then (l,parity_of_bool true)
- else if Node.equal r node_true
- then (l,parity_of_bool false)
- else !Conflict._equality l r, Pos
- )
+let th_register env =
+ RDaemonPropaNot.init env;
+ RDaemonPropa.init env;
+ RDaemonInit.init env;
+ Demon.Fast.attach env
+ DaemonInit.key [Demon.Create.EventRegSem(sem,())];
+ Egraph.register env node_true;
+ Egraph.register env node_false;
+ SynTerm.register_converter env converter;
+ SynTerm.register_decvars env decvars;
+ ()
(** {2 Interpretations} *)
let () =
@@ -693,27 +485,32 @@ let () =
let default_value = true
-let () =
- Interp.Register.model ty (fun d n ->
- let v = Egraph.get_value d dom n in
- let v = Witan_popop_lib.Opt.get_def default_value v in
- let v = if v then values_true else values_false in
- v)
+(* let () =
+ * Interp.Register.model ty (fun d n ->
+ * let v = Egraph.get_value d dom n in
+ * let v = Witan_popop_lib.Opt.get_def default_value v in
+ * let v = if v then values_true else values_false in
+ * v) *)
let () =
- Interp.Register.id (fun id args ->
- let open Term in
- let is builtin = Term.Id.equal id builtin in
- let (!>) n = BoolValue.value (BoolValue.coerce_nodevalue n) in
+ Interp.Register.id (fun interp t ->
+ let (!>) t = BoolValue.value (BoolValue.coerce_nodevalue (interp t)) in
let (!<) b = Some (if b then values_true else values_false) in
- match args with
- | [] when is true_id -> Some values_true
- | [] when is false_id -> Some values_false
- | [a] when is not_id -> !< (not (!> a))
- | l when is_or_id id -> !< (List.fold_left (||) false (List.map (!>) l))
- | l when is_and_id id -> !< (List.fold_left (&&) true (List.map (!>) l))
+ match t with
+ | { descr = Expr.App({builtin = Expr.Or},[],args); _ } ->
+ !< (List.fold_left (||) false (List.map (!>) args))
+ | { descr = Expr.App({builtin = Expr.And},[],args); _ } ->
+ !< (List.fold_left (&&) true (List.map (!>) args))
+ | { descr = Expr.App({builtin = Expr.Imply},[],[arg1;arg2]); _ } ->
+ !< ( not (!> arg1) || !> arg2 )
+ | { descr = Expr.App({builtin = Expr.Neg},[],[arg]); _ } ->
+ !< (not (!> arg))
+ | { descr = Expr.App({builtin = Expr.True},[],[]); _ } ->
+ Some values_true
+ | { descr = Expr.App({builtin = Expr.False},[],[]); _ } ->
+ Some values_false
| _ -> None
)
diff --git a/src/theories/bool/boolean.mli b/src/theories/bool/boolean.mli
index cf84af45a711bffe6b964801437bdd3183b01728..3bd258bfbe0968715515cafe347bdb46defe9cc5 100644
--- a/src/theories/bool/boolean.mli
+++ b/src/theories/bool/boolean.mli
@@ -18,8 +18,6 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Witan_core_structures
-
type t
val sem: t ThTermKind.t
val dom: bool ValueKind.t
@@ -34,8 +32,8 @@ val gen : bool -> (Node.t * bool) list -> Node.t
not_b0 (or (not_b1 cl1,not_b2 cl2)) with not_x f = if x then not f else f
*)
-val set_true : Egraph.t -> Trail.Pexp.t -> Node.t -> unit
-val set_false : Egraph.t -> Trail.Pexp.t -> Node.t -> unit
+val set_true : Egraph.t -> Node.t -> unit
+val set_false : Egraph.t -> Node.t -> unit
val is : Egraph.t -> Node.t -> bool option
val is_true : Egraph.t -> Node.t -> bool
@@ -48,12 +46,10 @@ val is_unknown : Egraph.t -> Node.t -> bool
val th_register: Egraph.t -> unit
-val chobool: Node.t Trail.Cho.t
+val chobool: Node.t -> Egraph.choice
(* val make_dec: Variable.make_dec *)
-val ty: Ty.t
-
module BoolValue : ValueKind.Registered with type s = bool
val value_true : BoolValue.t
diff --git a/src/theories/bool/dune b/src/theories/bool/dune
index 9d88d4ee3ec606d7a188bb8118532f48b16432cf..3829004922a81c207b21da48120cf334f340aa4b 100644
--- a/src/theories/bool/dune
+++ b/src/theories/bool/dune
@@ -4,9 +4,9 @@
(synopsis "theories for witan")
(modules Boolean Equality Uninterp)
(libraries containers ocamlgraph witan.stdlib witan.popop_lib
- witan.core.structures witan.core)
+ witan.core.structures witan.core dolmen.std)
(preprocess
- (pps ppx_deriving.std))
+ (pps ppx_deriving.std ppx_hash))
(flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always -open
Containers -open Witan_stdlib -open Std -open Witan_core)
(ocamlopt_flags :standard -O3 -bin-annot -unbox-closures
diff --git a/src/theories/bool/equality.ml b/src/theories/bool/equality.ml
index b673b83297b61d82d5d77852173b7350c72529e9..9776c7affa0c392d24b3bafab253526095df7306 100644
--- a/src/theories/bool/equality.ml
+++ b/src/theories/bool/equality.ml
@@ -35,11 +35,7 @@ let sem = ThTermKind.create_key (module struct type nonrec t = t let name = "Eq"
module Th = struct
- let get_ty v = Node.ty (fst (Node.M.choose v))
-
- let inv s = not (Node.M.is_empty s || Node.M.is_num_elt 1 s) &&
- let ty = get_ty s in
- (Node.M.for_all (fun e _ -> Ty.equal ty (Node.ty e)) s)
+ let inv s = not (Node.M.is_empty s || Node.M.is_num_elt 1 s)
let only_two s =
assert (inv s);
@@ -86,34 +82,34 @@ module Dis : sig
val empty: t
val of_node: ThE.t -> elt
val to_node: elt -> ThE.t
- val test_disjoint: (elt -> Trail.Age.t -> unit) -> t -> t -> t
+ val test_disjoint: (elt -> unit) -> t -> t -> t
val disjoint : t -> t -> bool
- val singleton : elt -> Trail.Age.t -> t
+ val singleton : elt -> t
val inter : t -> t -> t
val is_empty : t -> bool
- val choose : t -> elt * Trail.Age.t
- val iter : (elt -> Trail.Age.t -> unit) -> t -> unit
+ val choose : t -> elt
+ val iter : (elt -> unit) -> t -> unit
end = struct
- type t = Trail.Age.t ThE.M.t
+ type t = ThE.S.t
type elt = ThE.t
- let empty = ThE.M.empty
+ let empty = ThE.S.empty
let pp fmt s =
let aux fmt m =
ThE.M.bindings m
|> Format.(list ~sep:(const char ';')
- (pair ~sep:(const char ',') ThE.pp Trail.Age.pp)) fmt
+ (pair ~sep:(const char ',') ThE.pp Pp.nothing)) fmt
in
Format.fprintf fmt "{%a}" aux s
let of_node x = x
let to_node x = x
let test_disjoint f m1 m2 =
- ThE.M.union (fun k v1 v2 -> assert (Trail.Age.equal v1 v2); f k v1; Some v1) m1 m2
- let disjoint = ThE.M.set_disjoint
- let singleton = ThE.M.singleton
- let is_empty = ThE.M.is_empty
- let inter m1 m2 = ThE.M.inter (fun _ v1 v2 -> assert (Trail.Age.equal v1 v2); Some v2) m1 m2
- let choose m1 = ThE.M.choose m1
- let iter = ThE.M.iter
+ ThE.M.union (fun k () () -> f k; Some ()) m1 m2
+ let disjoint = ThE.S.disjoint
+ let singleton = ThE.S.singleton
+ let is_empty = ThE.S.is_empty
+ let inter m1 m2 = ThE.S.inter m1 m2
+ let choose m1 = ThE.S.choose m1
+ let iter = ThE.S.iter
end
let dom = DomKind.create_key (module struct type t = Dis.t let name = "dis" end)
@@ -121,16 +117,6 @@ let dom = DomKind.create_key (module struct type t = Dis.t let name = "dis" end)
(** For each value key give the value *)
module MValues = ValueKind.MkMap(struct type ('a, _) t = 'a end)
-type exp =
- | Merge of Trail.Pexp.t * Node.t * Node.t * Dis.elt * Trail.Age.t
- | SubstUpTrue of ThE.t * Node.t (* e1 *) * Node.t (* e2 *) * Node.t
- | SubstUpFalse of ThE.t * (Node.t * (Dis.t option * unit MValues.t)) list
- | SubstDownTrue of ThE.t
- | SubstDownFalse of ThE.t * Dis.elt
- | Dec of Node.t * Node.t
-
-let exp = Trail.Exp.create_key (module struct type t = exp let name = "Equality" end)
-
module D = struct
type t = Dis.t
@@ -141,7 +127,7 @@ module D = struct
| None, None -> true
| _ -> false
- let merge d pexp (s1,cl1) (s2,cl2) _ =
+ let merge d (s1,cl1) (s2,cl2) _ =
match s1, s2 with
| None, None -> raise Impossible
| Some s, None ->
@@ -149,9 +135,7 @@ module D = struct
| None, Some s ->
Egraph.set_dom d dom cl1 s
| Some s1, Some s2 ->
- let s = Dis.test_disjoint (fun i age ->
- let pexp = Egraph.mk_pexp d exp (Merge(pexp,cl1,cl2,i,age)) in
- Egraph.contradiction d pexp) s1 s2 in
+ let s = Dis.test_disjoint (fun _ -> Egraph.contradiction d) s1 s2 in
Egraph.set_dom d dom cl1 s;
Egraph.set_dom d dom cl2 s
@@ -162,7 +146,7 @@ end
let () = DomKind.register(module D)
-let set_dom d _pexp cl s =
+let set_dom d cl s =
let s = match Egraph.get_dom d dom cl with
| Some s' ->
Dis.test_disjoint (fun _ -> assert false) s' s
@@ -170,7 +154,7 @@ let set_dom d _pexp cl s =
Egraph.set_dom d dom cl s
let check_sem v cl =
- let own = ThE.node (ThE.index v Boolean.ty) in
+ let own = ThE.node (ThE.index v) in
Node.equal cl own
(** API *)
@@ -179,7 +163,7 @@ let equality cll =
try
let fold acc e = Node.S.add_new Exit e acc in
let s = List.fold_left fold Node.S.empty cll in
- ThE.node (ThE.index s Boolean.ty)
+ ThE.node (ThE.index s)
with Exit ->
Boolean._true
@@ -194,9 +178,9 @@ let is_disequal t cl1 cl2 =
| Some s1, Some s2 -> not (Dis.disjoint s1 s2)
| _ -> false
-let new_tag n age =
+let new_tag n =
let n = Dis.of_node n in
- n, fun () -> Dis.singleton n age (** each instance of this tag must not be == *)
+ n, fun () -> Dis.singleton n (** each instance of this tag must not be == *)
exception Found of Node.t * Node.t
@@ -258,47 +242,41 @@ let norm_set d the =
e e0 acc)
Node.M.empty v);
false
- with Found (e1,e2) ->
+ with Found (_e1,_e2) ->
(** TODO remove that and choose what to do. ex: int real *)
- let pexp = Egraph.mk_pexp d exp (SubstUpTrue (the,e1,e2,own)) in
- Boolean.set_true d pexp own;
+ Boolean.set_true d own;
true
module ChoEquals = struct
- open Conflict
-
- module OnWhat = ThE
-
- let key = Trail.Cho.create_key (module struct type t = ThE.t let name = "Equals.cho" end)
-
let make_decision the (cl1,cl2) d =
- Debug.dprintf6 print_decision
+ Debug.dprintf6 Egraph.print_decision
"[Equality] @[decide on merge of %a and %a in %a@]"
Node.pp cl1 Node.pp cl2 ThE.pp the;
- let pexp = Egraph.mk_pexp d exp (Dec(cl1,cl2)) in
Egraph.register d cl1;
Egraph.register d cl2;
- Egraph.merge d pexp cl1 cl2
+ Egraph.merge d cl1 cl2
- let choose_decision d the =
+ let choose_decision the d =
let v = ThE.sem the in
let own = ThE.node the in
Debug.dprintf4 debug "[Equality] @[dec on %a for %a@]"
Node.pp own ThE.pp the;
if norm_set d the
- then DecNo
+ then Egraph.DecNo
else
match find_not_disequal d v with
- | `AllDiff al ->
- let pexp = Egraph.mk_pexp d exp (SubstUpFalse(the,al)) in
- Boolean.set_false d pexp own;
+ | `AllDiff _ ->
+ Boolean.set_false d own;
DecNo
| `Found (cl1,cl2) ->
DecTodo (make_decision the (cl1,cl2))
-end
+ let mk_choice the = {
+ Egraph.choice = choose_decision the;
+ prio = 1;
+ }
-let () = Conflict.register_cho(module ChoEquals)
+end
let norm_dom d the =
let v = ThE.sem the in
@@ -310,32 +288,25 @@ let norm_dom d the =
Node.pp own Th.pp v;
match Boolean.is d own with
| Some false ->
- let age = Trail.Age.succ (Egraph.current_age d) in
- let dis, stag = new_tag the age in
- let pexp =
- Egraph.mk_pexp d exp (SubstDownFalse(the,dis)) in
- Egraph.add_pexp d pexp;
- Node.S.iter (fun cl -> set_dom d pexp cl (stag ())) v;
+ let _dis, stag = new_tag the in
+ Node.S.iter (fun cl -> set_dom d cl (stag ())) v;
Demon.AliveStopped
| Some true ->
begin match Th.only_two v with
| Some (cl1,cl2) ->
- let pexp = Egraph.mk_pexp d exp (SubstDownTrue(the)) in
- Egraph.merge d pexp cl1 cl2; Demon.AliveStopped
+ Egraph.merge d cl1 cl2; Demon.AliveStopped
| None ->
match find_not_disequal d v with
- | `AllDiff al ->
- let pexp = Egraph.mk_pexp d exp (SubstUpFalse(the,al)) in
- Boolean.set_false d pexp own; (** contradiction *)
+ | `AllDiff _ ->
+ Boolean.set_false d own; (** contradiction *)
raise Impossible
| `Found _ ->
Demon.AliveStopped
end
| None ->
match find_not_disequal d v with
- | `AllDiff al ->
- let pexp = Egraph.mk_pexp d exp (SubstUpFalse(the,al)) in
- Boolean.set_false d pexp own;
+ | `AllDiff _ ->
+ Boolean.set_false d own;
Demon.AliveStopped
| `Found _ -> (** they are still not proved disequal *)
Demon.AliveReattached
@@ -352,7 +323,7 @@ module DaemonPropa = struct
let immediate = false
let wakeup d v _ev () =
- norm_dom d (ThE.index v Boolean.ty)
+ norm_dom d (ThE.index v)
end
@@ -388,7 +359,7 @@ module DaemonInit = struct
if true (* GenEquality.dodec (Th.get_ty v) *) then begin
Debug.dprintf4 debug "[Equality] @[ask_dec on %a for %a@]"
Node.pp own Th.pp v;
- Egraph.register_decision d (Trail.GCho(own,ChoEquals.key,clsem));
+ Egraph.register_decision d (ChoEquals.mk_choice clsem)
end
| _ -> ()
end
@@ -401,202 +372,6 @@ end
module RDaemonInit = Demon.Key.Register(DaemonInit)
-
-(** conflict *)
-module HypDis = struct
- open Conflict
-
- type t = {
- l1 : Node.t;
- l0 : Node.t;
- r0 : Node.t;
- r1 : Node.t;
- disequality : Node.t;
- age : Trail.Age.t;
- }
-
- let key = Trail.Hyp.create_key (module struct type nonrec t = t let name = "Diff" end)
-
- let pp fmt c =
- Format.fprintf fmt "%a=%a≠%a=%a"
- Node.pp c.l1
- Node.pp c.l0
- Node.pp c.r0
- Node.pp c.r1
-
- let split t c cl1 cl2 =
- if Equal.option Trail.Age.equal (Conflict.age_merge_opt t cl1 c.l1) None then
- let cl1, cl2 = EqHyp.orient_split t {l=c.r0;r=c.r1} cl1 cl2 in
- (Trail.Phyp.phyp key {c with r1 = cl1})::(EqHyp.create_eq cl2 c.r1)
- else
- let cl1, cl2 = EqHyp.orient_split t {l=c.l0;r=c.l1} cl1 cl2 in
- (Trail.Phyp.phyp key {c with l1 = cl1})::(EqHyp.create_eq cl2 c.l1)
-
-
- let useful_nodes c =
- Bag.list [c.l1;c.l0;c.r1;c.r0]
-
- let levels t c =
- let l = Levels.empty in
- let l = Levels.add t (Conflict.age_merge t c.l1 c.l0) l in
- let l = Levels.add t (Conflict.age_merge t c.r1 c.r0) l in
- let l = Levels.add t c.age l in
- l
-
- let apply_learnt c =
- let n, par = EqHyp.apply_learnt {l=c.l1;r=c.r1} in
- n, neg_parity par
-
- let create_diff_far t cl1 cl2 i age =
- let find_origin v cl =
- Node.S.fold_left (fun acc cl0 ->
- match acc with
- | Some _ -> acc
- | None ->
- match Conflict.age_merge_opt t cl cl0 with
- | Some _ -> Some cl0
- | None -> None) None v
- in
- let the = Dis.to_node i in
- let v = ThE.sem the in
- let cl1_0 = Opt.get (find_origin v cl1) in
- let cl2_0 = Opt.get (find_origin v cl2) in
- let diff = Trail.Phyp.phyp key {l1=cl1;l0=cl1_0;r0=cl2_0;r1=cl2;disequality=ThE.node the; age} in
- diff
-
- let create_diff_near t cl1 cl2 i age =
- let find_origin v cl =
- Node.S.fold_left (fun acc cl0 ->
- match acc with
- | Some _ -> acc
- | None ->
- match Conflict.age_merge_opt t cl cl0 with
- | Some _ -> Some cl0
- | None -> None) None v
- in
- let the = Dis.to_node i in
- let v = ThE.sem the in
- let cl1_0 = Opt.get (find_origin v cl1) in
- let cl2_0 = Opt.get (find_origin v cl2) in
- let diff = Trail.Phyp.phyp key {l1=cl1_0;l0=cl1_0;r0=cl2_0;r1=cl2_0;disequality=ThE.node the; age} in
- diff, (Trail.Phyp.phyp EqHyp.key {l=cl1_0;r=cl2_0})
-
-end
-
-let () = Conflict.register_hyp(module HypDis)
-
-module Exp = struct
- open Conflict
-
- type t = exp
-
- let pp fmt = function
- | Merge (pexp,cl1,cl2,i,_) ->
- Format.fprintf fmt "Merge!(%a,%a,%a,%a)"
- pp_pexp pexp Node.pp cl1 Node.pp cl2 ThE.pp (Dis.to_node i)
- | SubstUpTrue (v,e1,e2,cl) -> (** two are equals *)
- Format.fprintf fmt "SubstUpTrue(%a,%a,%a,%a)"
- ThE.pp v Node.pp e1 Node.pp e2 Node.pp cl
- | SubstUpFalse (the,_) ->
- Format.fprintf fmt "SubstUpFalse(%a)" ThE.pp the
- | SubstDownTrue (the) ->
- Format.fprintf fmt "SubstDownTrue(%a)" ThE.pp the
- | SubstDownFalse (v,i) ->
- Format.fprintf fmt "SubstDownFalse(%a,%a)"
- ThE.pp v ThE.pp (Dis.to_node i)
- | Dec (n1,n2) ->
- Format.fprintf fmt "Dec(%a,%a)"
- Node.pp n1 Node.pp n2
-
- let analyse t e phyp =
- match e with
- | SubstUpTrue (v,e1,e2,_) -> (** two are equals *)
- let own = ThE.node v in
- let lhyp = Conflict.split t phyp own Boolean._true in
- let phyp = Trail.Phyp.phyp EqHyp.key {l=e1;r=e2} in
- phyp::lhyp
- | SubstUpFalse (v,al) ->
- let own = ThE.node v in
- let lhyp = Conflict.split t phyp own Boolean._false in
- let al = CCList.diagonal al in
- let fold lhyp ((e1,(dis1,val1)),(e2,(dis2,val2))) =
- let diff_value () = (** different values *)
- let fold2_inter (type a) (k:a ValueKind.t) v1 v2 acc =
- let (module V) = ValueKind.get k in
- if not (V.equal v1 v2) then
- (EqHyp.create_eq e1 (Node.index_value k v1 (Node.ty e1))) @
- (EqHyp.create_eq e2 (Node.index_value k v2 (Node.ty e2))) @
- acc
- else acc
- in
- let lhyp' = MValues.fold2_inter {fold2_inter} val1 val2 lhyp in
- assert (not (Equal.physical lhyp lhyp')); (** One is different *)
- lhyp'
- in
- match dis1, dis2 with
- | Some dis1, Some dis2 ->
- let dis = Dis.inter dis1 dis2 in
- if Dis.is_empty dis
- then diff_value ()
- else
- (** choose the oldest? *)
- let d,age = Dis.choose dis in
- let diff = HypDis.create_diff_far t e1 e2 d age in
- diff::lhyp
- | _ -> diff_value ()
- in
- List.fold_left fold lhyp al
- | SubstDownTrue (the) -> begin
- let v = ThE.sem the in
- match Node.S.elements v with
- | [a;b] ->
- let lhyp = Conflict.split t phyp a b in
- (EqHyp.create_eq (ThE.node the) Boolean._true)@lhyp
- | _ -> raise Impossible
- end
- | SubstDownFalse (the,_) ->
- let Trail.Phyp.Phyp(hyp,c,_) = phyp in
- let c = Hyp.Eq.coerce hyp HypDis.key c in
- let lhyp = [] in
- let lhyp = (EqHyp.create_eq c.l1 c.l0)@lhyp in
- let lhyp = (EqHyp.create_eq c.r1 c.r0)@lhyp in
- let lhyp = (EqHyp.create_eq (ThE.node the) Boolean._false)@lhyp in
- lhyp
- | Dec(n1,n2) ->
- let lhyp = Conflict.split t phyp n1 n2 in
- let eq = EqHyp.create_eq ~dec:() n1 n2 in
- eq@lhyp
- | Merge(pexp,cl1,cl2,i,age) ->
- assert (Equal.physical pexp (Trail.pexp_fact));
- (** only for bool currently *)
- let cl2' = if Node.equal cl2 Boolean._true then Boolean._false else Boolean._true in
- let lhyp = Conflict.split t phyp cl1 cl2' in
- let diff = HypDis.create_diff_far t cl1 cl2 i age in
- diff::lhyp
-
- let key = exp
-
- let far_disequality = Debug.register_flag "far-disequality"
- ~desc:"Instead of explaining conflict with distinct near the disequality, explain it far from it"
-
- let from_contradiction t = function
- | Merge(pexp,cl1,cl2,i,age) ->
- if Debug.test_flag far_disequality then
- let lhyp = Conflict.analyse t pexp (Trail.Phyp.phyp EqHyp.key {l=cl1;r=cl2}) in
- let diff = HypDis.create_diff_far t cl1 cl2 i age in
- diff::lhyp
- else
- let diff, eq = HypDis.create_diff_near t cl1 cl2 i age in
- let lhyp = Conflict.analyse t pexp eq in
- diff::lhyp
- | _ -> raise Impossible
-
-end
-
-
-let () = Conflict.register_exp(module Exp)
-
-
(** ITE *)
type ite = {cond: Node.t; then_: Node.t; else_: Node.t}
@@ -631,13 +406,7 @@ end
module EITE = ThTermKind.Register(ITE)
let ite cond then_ else_ =
- let ty1 = Node.ty then_ in
- let ty2 = Node.ty else_ in
- assert (Ty.equal ty1 ty2);
- Node.index_sem ITE.key { cond; then_; else_} ty1
-
-let expite =
- Trail.Exp.create_key (module struct type nonrec t = EITE.t * bool let name = "Ite.exp" end)
+ Node.index_sem ITE.key { cond; then_; else_}
module DaemonPropaITE = struct
let key = Demon.Fast.create "ITE.propa"
@@ -648,9 +417,8 @@ module DaemonPropaITE = struct
let v = EITE.sem the in
let own = EITE.node the in
let branch = if b then v.then_ else v.else_ in
- let pexp = Egraph.mk_pexp d expite (the,b) in
Egraph.register d branch;
- Egraph.merge d pexp own branch
+ Egraph.merge d own branch
let immediate = false
let throttle = 100
@@ -687,12 +455,12 @@ module DaemonInitITE = struct
| Some b ->
DaemonPropaITE.simplify d clsem b
| None ->
- let clsem = EITE.index v (Node.ty own) in
+ let clsem = EITE.index v in
assert (Node.equal (EITE.node clsem) own);
Egraph.register d v.cond;
Egraph.register d v.then_;
Egraph.register d v.else_;
- Egraph.register_decision d (Trail.GCho(v.cond,Boolean.chobool,v.cond));
+ Egraph.register_decision d (Boolean.chobool v.cond);
let events = [Demon.Create.EventValue(v.cond,Boolean.dom,clsem)] in
Demon.Fast.attach d DaemonPropaITE.key events
end
@@ -702,31 +470,6 @@ end
module RDaemonInitITE = Demon.Fast.Register(DaemonInitITE)
-module ExpITE = struct
- open Conflict
-
- type t = EITE.t * bool
- let key = expite
-
- let pp fmt (ite,b) =
- Format.fprintf fmt "(%a,%b)" EITE.pp ite b
-
- let analyse :
- Conflict.t ->
- (* Trail.age -> *) t -> Trail.Phyp.t -> Trail.Phyp.t list =
- fun t (the,b) hyp ->
- let v = EITE.sem the in
- let own = EITE.node the in
- let lhyp = Conflict.split t hyp own (if b then v.then_ else v.else_) in
- let phyp = EqHyp.create_eq v.cond (if b then Boolean._true else Boolean._false) in
- phyp@lhyp
-
- let from_contradiction _ _ = raise Impossible
-
-end
-
-let () = Conflict.register_exp(module ExpITE)
-
(** {2 Link between diff and values} *)
(** If can't be a value it they share a diff tag, are different *)
@@ -739,15 +482,13 @@ let iter_on_value_different
(d:Egraph.t)
(own:Node.t) =
let dis = Opt.get_def Dis.empty (Egraph.get_dom d dom own) in
- let iter elt age =
+ let iter elt =
let iter n =
if not (Egraph.is_equal d own n) then
match Egraph.get_value d Val.key n with
| None -> ()
| Some v ->
- let pexp =
- Egraph.mk_pexp d exp (Merge(Trail.pexp_fact,own,n,elt,age)) in
- they_are_different pexp n v
+ they_are_different n v
in
Node.S.iter iter (ThE.sem (Dis.to_node elt))
in
@@ -758,17 +499,15 @@ let init_diff_to_value (type a) (type b)
?(already_registered=([]: b list))
d0
((module Val): (module Witan_core.ValueKind.Registered with type s = a and type t = b))
- ~(they_are_different:(Egraph.t -> Trail.Pexp.t -> Node.t -> a -> unit)) =
+ ~(they_are_different:(Egraph.t -> Node.t -> a -> unit)) =
let propagate_diff d v =
let own = Val.node v in
let dis = Opt.get_def Dis.empty (Egraph.get_dom d dom own) in
- let iter elt age =
+ let iter elt =
let iter n =
if not (Egraph.is_equal d own n) then
- let pexp =
- Egraph.mk_pexp d exp (Merge(Trail.pexp_fact,n,Val.node v,elt,age)) in
- they_are_different d pexp n (Val.value v)
+ they_are_different d n (Val.value v)
in
Node.S.iter iter (ThE.sem (Dis.to_node elt))
in
@@ -807,9 +546,9 @@ let init_diff_to_value (type a) (type b)
let bool_init_diff_to_value d =
init_diff_to_value
d (module Boolean.BoolValue)
- ~they_are_different:(fun d pexp n b ->
- if not b then Boolean.set_true d pexp n
- else Boolean.set_false d pexp n
+ ~they_are_different:(fun d n b ->
+ if not b then Boolean.set_true d n
+ else Boolean.set_false d n
)
~already_registered:[Boolean.value_true;Boolean.value_false]
@@ -833,45 +572,46 @@ let () =
Interp.Register.thterm ITE.key interp
let () =
- Interp.Register.id (fun id args ->
- let open Term in
- let is builtin = Term.Id.equal id builtin in
- let (!>) n = Boolean.BoolValue.value (Boolean.BoolValue.coerce_nodevalue n) in
+ Interp.Register.id (fun interp t ->
+ let (!>) n = Boolean.BoolValue.value (Boolean.BoolValue.coerce_nodevalue (interp n)) in
let (!<) b = Some (if b then Boolean.values_true else Boolean.values_false) in
- match args with
- | [a;b] when is equal_id || is equiv_id -> !< (Value.equal a b)
- | [c;a;b] when is ite_id -> Some (if (!> c) then a else b)
- | _ when is_distinct_id id -> begin
+ match t with
+ | { descr = Expr.App({builtin = Expr.Equal},[_],a::l); _ } ->
+ let a = interp a in
+ !< (List.for_all (fun t -> Value.equal a (interp t)) l)
+ | { descr = Expr.App({builtin = Expr.Equiv},[_],[a;b]); _ } ->
+ !< (Value.equal (interp a) (interp b))
+ | { descr = Expr.App({builtin = Expr.Distinct},[_],args); _ } ->
+ begin
try
- let fold acc v = Value.S.add_new Exit v acc in
+ let fold acc v = Value.S.add_new Exit (interp v) acc in
let _ = List.fold_left fold Value.S.empty args in
Some Boolean.values_false
with Exit ->
Some Boolean.values_true
end
+ | { descr = Expr.App({builtin = Expr.Ite},[_],[c;a;b]); _ } ->
+ Some (if (!> c) then interp a else interp b)
| _ -> None
)
-let converter d f l =
+let converter d (t:Expr.Term.t) =
let of_term t =
let n = SynTerm.node_of_term t in
Egraph.register d n;
n
in
- let node = match f, l with
- | f,(_::([_;_] as args)) when Term.equal f Term.equal_term ||
- Term.equal f Term.equiv_term ->
- Some (equality (List.map of_term args))
- | f,(_::args) when Term.is_distinct_term f ->
- Some (disequality (List.map of_term args))
- | f,[_;c;a;b] when Term.equal f Term.ite_term ->
- Some (ite (of_term c) (of_term a) (of_term b))
- | _, _ -> None in
- node
-
-let () = Conflict._equality := (fun a b -> equality [a;b])
-
+ match t with
+ | { descr = Expr.App({builtin = Expr.Equal},[_],l); _ } ->
+ Some (equality (List.map of_term l))
+ | { descr = Expr.App({builtin = Expr.Equiv},[_],[a;b]); _ } ->
+ Some (equality [of_term a;of_term b])
+ | { descr = Expr.App({builtin = Expr.Distinct},[_],args); _ } ->
+ Some (disequality (List.map of_term args))
+ | { descr = Expr.App({builtin = Expr.Ite},[_],[c;a;b]); _ } ->
+ Some (ite (of_term c) (of_term a) (of_term b))
+ | _ -> None
let th_register env =
RDaemonPropa.init env;
diff --git a/src/theories/bool/equality.mli b/src/theories/bool/equality.mli
index 84faf48a9ec89bec0cc3dff743f3bebbf202850b..1352f9a6d6e658735b09747ff1c85bbd4b060f3e 100644
--- a/src/theories/bool/equality.mli
+++ b/src/theories/bool/equality.mli
@@ -28,7 +28,7 @@ val ite : Node.t -> Node.t -> Node.t -> Node.t
val iter_on_value_different:
(module ValueKind.Registered with type s = 'a and type t = 'b) ->
- they_are_different:(Trail.Pexp.t -> Node.t -> 'a -> unit) ->
+ they_are_different:(Node.t -> 'a -> unit) ->
Egraph.t -> Node.t -> unit
diff --git a/src/theories/bool/uninterp.ml b/src/theories/bool/uninterp.ml
index 7b666cee81b652af1eb9625cf084638d23970415..d00c58666ff37fd4435d6f396bc8bed4dff9fd48 100644
--- a/src/theories/bool/uninterp.ml
+++ b/src/theories/bool/uninterp.ml
@@ -20,38 +20,26 @@
open Witan_popop_lib
open Popop_stdlib
-open Std
open Witan_core
let debug = Debug.register_info_flag
~desc:"for the uninterpreted function theory"
"uninterp"
-type t = App of Node.t * Node.t
-
-let sem = ThTermKind.create_key (module struct type nonrec t = t let name = "UF" end)
-
module Th = struct
module T = struct
- type r = t
- type t = r
- let equal n m =
- match n, m with
- | App (g1,f1), App(g2,f2) -> Node.equal g1 g2 && Node.equal f1 f2
-
- let hash n =
- match n with
- | App(g,f) -> 3 * (Node.hash g) + 5 * (Node.hash f)
-
- let compare n m =
- match n, m with
- | App(g1,f1), App(g2,f2) ->
- let c = Node.compare g1 g2 in
- if c <> 0 then c
- else Node.compare f1 f2
+ let hash_fold_list = Base.hash_fold_list
+ type t =
+ | Fun of Expr.Term.Const.t * Expr.Ty.t list
+ | App of Node.t * Node.t
+ [@@ deriving eq, ord, hash]
let pp fmt v =
match v with
+ | Fun (t,tyl) ->
+ Format.fprintf fmt "%a[%a]"
+ Expr.Term.Const.pp t
+ (Pp.list Pp.colon Expr.Ty.pp) tyl
| App (f,g) -> Format.fprintf fmt "(@[%a@],@,@[%a@])"
Node.pp f Node.pp g
@@ -60,24 +48,25 @@ module Th = struct
include T
include MkDatatype(T)
- let key = sem
+ let key = ThTermKind.create_key (module struct type nonrec t = t let name = "UF" end)
end
+let sem = Th.key
+
let pp = Th.pp
module ThE = ThTermKind.Register(Th)
-let app f g ty = Node.index_sem sem (App(f,g)) ty
+let app f g = Node.index_sem sem (App(f,g))
let appl f l =
- let rec aux acc ty = function
+ let rec aux acc = function
| [] -> acc
| a::l ->
- let _,ty = Term.extract_fun_ty ty in
- aux (app acc a ty) ty l
+ aux (app acc a) l
in
- aux f (Node.ty f) l
+ aux f l
(* let result_of_sort = Ty.H.create 20
*
@@ -116,9 +105,6 @@ let appl f l =
* (fun x1 x2 x3 x4 x5 -> app_fun f [x1;x2;x3;x4;x5]) *)
-type expsubst = {from:ThE.t; to_:ThE.t}
-let expsubst = Trail.Exp.create_key (module struct type t = expsubst let name = "Uninterp" end)
-
module DaemonPropa = struct
type k = ThE.t
let key = Demon.Key.create "Uninterp.DaemonPropa"
@@ -142,14 +128,14 @@ module DaemonPropa = struct
let immediate = true (** can be false *)
let wakeup d (nodesem:k) _ev () =
match ThE.sem nodesem with
- | App(f,g) as v ->
+ | Th.Fun _ -> Demon.AliveStopped
+ | Th.App(f,g) as v ->
Debug.dprintf4 debug "[Uninterp] @[wakeup own %a v:%a@]"
Node.pp (ThE.node nodesem) Th.pp v;
- let v' = App(Egraph.find d f, Egraph.find d g) in
+ let v' = Th.App(Egraph.find d f, Egraph.find d g) in
assert (not (Th.equal v v'));
- let nodesem' = ThE.index v' (ThE.ty nodesem) in
- let pexp = Egraph.mk_pexp d expsubst {from=nodesem;to_=nodesem'} in
- Egraph.set_thterm d pexp (ThE.node nodesem) (ThE.thterm nodesem');
+ let nodesem' = ThE.index v' in
+ Egraph.set_thterm d (ThE.node nodesem) (ThE.thterm nodesem');
Demon.AliveRedirected nodesem'
end
@@ -173,18 +159,18 @@ module DaemonInit = struct
let own = ThE.node nodesem in
Debug.dprintf2 debug "[Uninterp] @[init %a@]" Th.pp v;
if DaemonPropa.is_unborn d nodesem then
- match v with
- | App(f,g) ->
- Egraph.register d f; Egraph.register d g;
- let f' = Egraph.find d f in
- let g' = Egraph.find d g in
- if Node.equal f' f && Node.equal g' g then
- DaemonPropa.attach d f g nodesem
- else
- let v' = App(f',g') in
- let nodesem' = ThE.index v' (Node.ty own) in
- let pexp = Egraph.mk_pexp d expsubst {from=nodesem;to_=nodesem'} in
- Egraph.set_thterm d pexp own (ThE.thterm nodesem')
+ match v with
+ | Fun _ -> assert false (** TODO *)
+ | App(f,g) ->
+ Egraph.register d f; Egraph.register d g;
+ let f' = Egraph.find d f in
+ let g' = Egraph.find d g in
+ if Node.equal f' f && Node.equal g' g then
+ DaemonPropa.attach d f g nodesem
+ else
+ let v' = Th.App(f',g') in
+ let nodesem' = ThE.index v' in
+ Egraph.set_thterm d own (ThE.thterm nodesem')
end
| _ -> raise UnwaitedEvent
) ev;
@@ -195,42 +181,15 @@ end
module RDaemonInit = Demon.Key.Register(DaemonInit)
-module ExpSubst = struct
- open Conflict
-
- type t = expsubst
- let key = expsubst
-
- let pp fmt c =
- match ThE.sem c.from, ThE.sem c.to_ with
- | App(f,g), App(f',g') ->
- Format.fprintf fmt "Subst(%a,%a -> %a,%a)"
- Node.pp f Node.pp g Node.pp f' Node.pp g'
-
- let analyse t {from;to_} phyp =
- match ThE.sem from, ThE.sem to_ with
- | App(f,g), App(f',g') ->
- let lhyp = Conflict.split t phyp (ThE.node from) (ThE.node to_) in
- let lhyp' = if Node.equal f f' then [] else EqHyp.create_eq f f' in
- let lhyp'' = if Node.equal g g' then [] else EqHyp.create_eq g g' in
- lhyp'@lhyp''@lhyp
-
- let from_contradiction _ _ = raise Impossible
-
-end
-
-let () = Conflict.register_exp(module ExpSubst)
-
-
-let converter d f l =
+let converter d (t:Term.t) =
let of_term t =
let n = SynTerm.node_of_term t in
Egraph.register d n;
n
in
- let node = match f with
- | {Term.term=Id id} when not (Term.is_defined id) ->
- let f = of_term f in
+ let node = match t with
+ | { descr = App({builtin = Dolmen_std.Expr.Base; _ } as f,tyl,((_::_) as l)); _ } ->
+ let f = ThE.node (ThE.index (Fun (f,tyl))) in
let l = List.map of_term l in
Some (appl f l)
| _ -> None
diff --git a/src/theories/bool/uninterp.mli b/src/theories/bool/uninterp.mli
index ee1bd8152e2b3537d081cadfb1ecf873d3ccd6b7..92a2ddf1df0586f1b0317b1a46df6941b51a0453 100644
--- a/src/theories/bool/uninterp.mli
+++ b/src/theories/bool/uninterp.mli
@@ -20,10 +20,14 @@
open Witan_core
-type t = App of Node.t * Node.t
-val pp: t Format.printer
+module Th: sig
+ type t =
+ | Fun of Expr.Term.Const.t * Expr.Ty.t list
+ | App of Node.t * Node.t
+ val pp: t Format.printer
+end
-val sem: t ThTermKind.t
+val sem: Th.t ThTermKind.t
(* val fun1 :
* Ty.t -> string ->