diff --git a/src/main/isabelle/.gitignore b/src/main/isabelle/.gitignore
deleted file mode 100644
index c0810538385bb019c4ca5566f2e0a4b28d52b3c5..0000000000000000000000000000000000000000
--- a/src/main/isabelle/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-Scratch.thy
diff --git a/src/main/isabelle/Leon.thy b/src/main/isabelle/Leon.thy
deleted file mode 100644
index 60ffbc20801be58656c2f01f339bd65fdb7f991e..0000000000000000000000000000000000000000
--- a/src/main/isabelle/Leon.thy
+++ /dev/null
@@ -1,5 +0,0 @@
-theory Leon
-imports Leon_Ops Leon_Library
-begin
-
-end
\ No newline at end of file
diff --git a/src/main/isabelle/Leon_Library.thy b/src/main/isabelle/Leon_Library.thy
deleted file mode 100644
index 4327381f8b44ca5855f23aa86e9e9af689409a60..0000000000000000000000000000000000000000
--- a/src/main/isabelle/Leon_Library.thy
+++ /dev/null
@@ -1,31 +0,0 @@
-theory Leon_Library
-imports Leon_Ops
-begin
-
-axiomatization
- error :: "nat \<Rightarrow> 'a"
-
-typedecl string
-
-declare [[code abort: error]]
-
-declare null_rec[simp]
-declare List.null_def[simp]
-declare List.bind_def[simp]
-declare Let_def[leon_unfold]
-declare Product_Type.split[leon_unfold]
-declare comp_apply[simp del]
-declare comp_def[simp]
-declare member_rec[simp]
-
-lemma [simp]: "list_ex P xs = (\<not> list_all (Not \<circ> P) xs)"
-by (induct xs) auto
-
-syntax "_leon_var" :: "idt \<Rightarrow> 'a" ("<var _>")
-syntax "_leon_const" :: "idt \<Rightarrow> 'a" ("<const _>")
-
-ML_file "leon_syntax.ML"
-
-setup \<open>Leon_Syntax.setup\<close>
-
-end
\ No newline at end of file
diff --git a/src/main/isabelle/Leon_Ops.thy b/src/main/isabelle/Leon_Ops.thy
deleted file mode 100644
index 8ed524cc66c6dd60bf5284f686f36f7097453423..0000000000000000000000000000000000000000
--- a/src/main/isabelle/Leon_Ops.thy
+++ /dev/null
@@ -1,47 +0,0 @@
-theory Leon_Ops
-imports
- Protocol
- Codec_Class
- "~~/src/HOL/Word/Word"
- "~~/src/HOL/Library/Simps_Case_Conv"
- Complex_Main
-begin
-
-named_theorems leon_unfold
-
-ML_file "~~/src/HOL/TPTP/sledgehammer_tactics.ML"
-
-sledgehammer_params [timeout = 5, provers = cvc4 z3 spass e]
-
-lemma if_to_cond_simps:
- assumes "f = (if p then x else y)"
- shows "p \<Longrightarrow> f = x" "\<not> p \<Longrightarrow> f = y"
-using assms by auto
-
-ML_file "tactics.ML"
-ML_file "util.ML"
-ML_file "stateless_ops.ML"
-ML_file "stateful_ops.ML"
-
-operation_setup (auto) numeral_literal = \<open>Stateless_Ops.numeral\<close>
-operation_setup (auto) word_literal = \<open>Stateless_Ops.word\<close>
-operation_setup (auto) map_literal = \<open>Stateless_Ops.map\<close>
-operation_setup (auto) serial_nat = \<open>Stateless_Ops.serial_nat\<close>
-operation_setup (auto) load = \<open>Stateful_Ops.load\<close>
-operation_setup (auto) "oracle" = \<open>Stateful_Ops.oracle\<close>
-operation_setup (auto) fresh = \<open>Stateful_Ops.fresh\<close>
-operation_setup (auto) prove = \<open>Stateful_Ops.prove\<close>
-operation_setup (auto) equivalences = \<open>Stateful_Ops.equivalences\<close>
-operation_setup (auto) assume_equivalences = \<open>Stateful_Ops.assume_equivalences\<close>
-operation_setup (auto) "lemmas" = \<open>Stateful_Ops.lemmas\<close>
-operation_setup (auto) assume_lemmas = \<open>Stateful_Ops.assume_lemmas\<close>
-operation_setup (auto) "declare" = \<open>Stateful_Ops.declare\<close>
-operation_setup (auto) pretty = \<open>Stateful_Ops.pretty\<close>
-operation_setup (auto) report = \<open>Stateful_Ops.report\<close>
-operation_setup (auto) dump = \<open>Stateful_Ops.dump\<close>
-operation_setup (auto) lookup_datatype = \<open>Stateful_Ops.lookup_datatype\<close>
-operation_setup (auto) "datatypes" = \<open>Stateful_Ops.datatypes\<close>
-operation_setup (auto) "functions" = \<open>Stateful_Ops.functions\<close>
-operation_setup (auto) cases = \<open>Stateful_Ops.cases\<close>
-
-end
\ No newline at end of file
diff --git a/src/main/isabelle/ROOT b/src/main/isabelle/ROOT
deleted file mode 100644
index d95bef0c4a3bcacb7ab56a1767280e54a749e285..0000000000000000000000000000000000000000
--- a/src/main/isabelle/ROOT
+++ /dev/null
@@ -1,8 +0,0 @@
-session Leon_Deps = "HOL-Protocol" +
- theories
- "~~/src/HOL/Word/Word"
- "~~/src/HOL/Library/Simps_Case_Conv"
-
-session Leon = Leon_Deps +
- theories
- Leon
diff --git a/src/main/isabelle/leon_syntax.ML b/src/main/isabelle/leon_syntax.ML
deleted file mode 100644
index cc0c704a08cdbe12de2c6c061f4228e4098afaaa..0000000000000000000000000000000000000000
--- a/src/main/isabelle/leon_syntax.ML
+++ /dev/null
@@ -1,82 +0,0 @@
-signature LEON_SYNTAX = sig
- val setup: theory -> theory
-end
-
-structure Leon_Syntax: LEON_SYNTAX = struct
-
-fun is_digit #"0" = true
- | is_digit #"1" = true
- | is_digit #"2" = true
- | is_digit #"3" = true
- | is_digit #"4" = true
- | is_digit #"5" = true
- | is_digit #"6" = true
- | is_digit #"7" = true
- | is_digit #"8" = true
- | is_digit #"9" = true
- | is_digit _ = false
-
-fun is_leon_name base id name =
- let
- val prefix = Long_Name.append base (id ^ "'")
- val exploded = String.explode name
- in
- String.isPrefix prefix name andalso List.all is_digit (drop (String.size prefix) exploded)
- end
-
-fun find_leon_name base id names =
- case filter (is_leon_name base id) names of
- [name] => SOME name
- | _ => NONE
-
-fun translation const ctxt args =
- let
- val thy = Proof_Context.theory_of ctxt
- val thy_name = Context.theory_name thy
- val fixes = Variable.dest_fixes ctxt
- val {constants = consts, ...} = Consts.dest (Sign.consts_of thy)
- fun guess id =
- if const then
- case find_leon_name thy_name id (map fst consts) of
- SOME name => Const (name, dummyT)
- | NONE => raise TERM ("unknown or ambiguous Leon constant " ^ id, args)
- else
- case find_leon_name "" id (map fst fixes) of
- SOME name => Free (name, dummyT)
- | NONE => raise TERM ("unknown or ambiguous Leon variable " ^ id, args)
- in
- case args of
- [(Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ _] => guess s
- | _ => impossible "Leon_Syntax.translation" @{here}
- end
-
-val const_translation = translation true
-val var_translation = translation false
-
-val translation_setup = Sign.parse_translation
- [(@{syntax_const "_leon_var"}, var_translation),
- (@{syntax_const "_leon_const"}, const_translation)]
-
-
-fun get_induct id thy =
- let
- val functions = Stateful_Ops.get_functions thy
- val names = Symtab.keys functions
- in
- case find_leon_name "" id names of
- SOME name =>
- (case the (Symtab.lookup functions name) of
- (NONE, _) => error ("no induction rule for " ^ id)
- | (SOME thm, _) => thm)
- | NONE => error ("unknown or ambiguous Leon function " ^ id)
- end
-
-val attrib_setup =
- Attrib.setup @{binding leon_induct}
- (Scan.lift Args.name >>
- (fn name => Thm.mixed_attribute (fn (context, _) => (context, get_induct name (Context.theory_of context)))))
- "induction rule for Leon function"
-
-val setup = translation_setup #> attrib_setup
-
-end
\ No newline at end of file
diff --git a/src/main/isabelle/stateful_ops.ML b/src/main/isabelle/stateful_ops.ML
deleted file mode 100644
index 88ee8478f2653d69619fa15ff6dfb04a712aa6d1..0000000000000000000000000000000000000000
--- a/src/main/isabelle/stateful_ops.ML
+++ /dev/null
@@ -1,580 +0,0 @@
-signature STATEFUL_OPS = sig
- val load: string * string * (string * string) list -> string list
- val oracle: unit -> unit
- val fresh: string -> string
- val prove: term list * string option -> string option
- val declare: string list -> unit
- val cases: (term * (string * typ) list) * (typ * (term * term) list) -> term
- val equivalences: (string * string) list -> string list
- val assume_equivalences: (string * string) list -> unit
- val lemmas: (string * term) list -> string list
- val assume_lemmas: (string * term) list -> unit
- val functions: (string * (string * typ) list * (term * typ)) list -> string option
- val datatypes: (string * string list * (string * (string * typ) list) list) list -> string option
- val lookup_datatype: string * (string * string) list -> (string, (string * (term * term * term list)) list) Codec.either
- val pretty: term -> string
- val report: unit -> (string * string) list
- val dump: unit -> (string * string) list
-
- (* internal *)
- val reset: theory option -> unit
- val peek: unit -> local_theory option
- val get_functions: theory -> (thm option * thm list) Symtab.table
-end
-
-structure Stateful_Ops: STATEFUL_OPS = struct
-
-fun try_timeout' f = try_timeout 5 f (* global timeout for auxiliary operations *)
-
-fun err_timeout msg f x =
- case try_timeout 5 f x of
- Exn.Res r => r
- | Exn.Exn TimeLimit.TimeOut => raise Timeout msg
- | Exn.Exn exn => reraise exn
-
-datatype report =
- Function of {heads: (string * string) list, raws: string list, specs: string list, inducts: (string * string) list} |
- Datatype of string |
- Theory of {import: string, scripts: (string * string) list} |
- Equivalence of string |
- Lemma of {name: string, prop: string} |
- Oracle |
- End
-
-structure Reports = Theory_Data
-(
- type T = report list
- val empty = []
- fun merge _ = impossible "Reports.merge" @{here}
- val extend = I
-)
-
-structure Functions = Theory_Data
-(
- type T = (thm option * thm list) Symtab.table
- val empty = Symtab.empty
- fun merge _ = impossible "Functions.merge" @{here}
- val extend = I
-)
-
-structure Oracle = Theory_Data
-(
- type T = (cterm -> thm) option
- val empty = NONE
- fun merge _ = impossible "Oracle.merge" @{here}
- val extend = I
-)
-
-fun add_report report = Reports.map (fn list => report :: list)
-val add_fun = Functions.map o Symtab.update_new
-val add_funs = fold add_fun
-fun set_oracle thy =
- let
- val ((_, oracle), thy') = Thm.add_oracle (@{binding leon_oracle}, I) thy
- in
- Oracle.map (K (SOME oracle)) thy'
- |> add_report Oracle
- end
-val get_oracle =
- Proof_Context.theory_of
- #> Oracle.get
- #> the_error "expected oracle" @{here}
-
-val get_functions = Functions.get
-
-type state = local_theory option
-val empty_state = NONE: state
-
-val state = Synchronized.var "libisabelle.leon_state" empty_state
-
-fun unset_parallel_proofs () =
- Goal.parallel_proofs := 0
-
-fun reset thy =
- (unset_parallel_proofs (); Synchronized.change state (K (Option.map (Named_Target.theory_init) thy)))
-
-fun peek () =
- Synchronized.value state
-
-local
- fun not_loaded pos =
- invalid_state "no theory loaded" pos
- fun already_loaded lthy =
- invalid_state ("theory " ^ Context.theory_name (Proof_Context.theory_of lthy) ^ "already loaded")
-in
-
-fun access_loaded f =
- case Synchronized.value state of
- SOME thy => f thy
- | NONE => not_loaded @{here}
-
-fun update_loaded f =
- let
- fun upd NONE = not_loaded @{here}
- | upd (SOME thy) = let val (a, thy') = f thy in (a, SOME thy') end
- in
- Synchronized.change_result state upd
- end
-
-fun load (root_name, thy_name, scripts) =
- let
- val _ = unset_parallel_proofs ()
- val _ =
- if Execution.is_running_exec Document_ID.none then ()
- else invalid_state "Must not be running in interactive mode" @{here}
- val root = Thy_Info.get_theory root_name
-
- fun load_script (name, txt) =
- let
- val thy = Theory.begin_theory (name, Position.none) [root]
- in (name, Exn.interruptible_capture (script_thy Position.none txt) thy) end
-
- fun classify (_, Exn.Res thy) = ([thy], [])
- | classify (name, Exn.Exn _) = ([], [name])
-
- fun upd (SOME lthy) = already_loaded lthy @{here}
- | upd NONE =
- let
- val (good, bad) = map classify (Par_List.map load_script scripts)
- |> split_list ||> flat |>> flat
-
- fun thy () =
- Theory.begin_theory (thy_name, Position.none) (root :: good)
- |> add_report (Theory {import = root_name, scripts = scripts})
-
- val res =
- if null bad then
- SOME (Named_Target.theory_init (thy ()))
- else
- NONE
- in (bad, res) end
- in Synchronized.change_result state upd end
-
-end
-
-fun oracle () =
- update_loaded (Local_Theory.background_theory set_oracle #> pair ())
-
-fun fresh n =
- update_loaded (Variable.variant_fixes [n] #>> hd)
-
-fun prove (ts, method) =
- access_loaded (fn lthy =>
- let
- val (ts', lthy) = register_terms ts lthy
- val prop = Balanced_Tree.make HOLogic.mk_disj ts'
- fun tac ctxt =
- case method of
- NONE => prove_tac ctxt
- | SOME src => HEADGOAL (method_tac @{here} src ctxt)
- in
- (* Assumption: all proofs are sequential *)
- try (Goal.prove lthy [] [] prop) (fn {context, ...} => tac context)
- |> Option.map (print_thm lthy)
- end)
-
-fun gen_lemmas prove props =
- update_loaded (fn lthy =>
- let
- fun process (name, prop) lthy =
- let
- val ([prop'], lthy') = register_terms [prop] lthy
- val binding = Binding.qualified true "lemma" (Binding.make (name, @{here}))
- in
- case prove lthy' prop' of
- NONE => ([name], lthy)
- | SOME thm =>
- lthy (* sic *)
- |> Local_Theory.note ((binding, @{attributes [simp]}), [thm]) |> snd
- |> Local_Theory.background_theory (add_report (Lemma {name = name, prop = print_thm lthy thm}))
- |> pair []
- end
- in
- fold_map process props lthy
- |>> flat
- end)
-
-val lemmas =
- gen_lemmas (fn ctxt => fn goal =>
- try_timeout' (Goal.prove ctxt [] [] goal) (fn {context, ...} => prove_tac context) |> Exn.get_res)
-
-val assume_lemmas =
- gen_lemmas (fn ctxt => fn goal =>
- SOME (get_oracle ctxt (Thm.cterm_of ctxt goal)))
- #> K ()
-
-fun declare names =
- update_loaded (fold Variable.declare_names (map (Free o rpair dummyT) names) #> pair ())
-
-fun cases ((raw_scr, bounds), (expected_typ, clauses)) =
- access_loaded (fn ctxt =>
- let
- fun dest_abs (name, typ) t = Term.dest_abs (name, typ, t)
- val unbound = fold_map dest_abs bounds #> snd
-
- val scr = Syntax.check_term ctxt (unbound raw_scr)
- val scr_typ = fastype_of scr
- val names = Variable.names_of ctxt
-
- fun process_clause (raw_pat, raw_rhs) =
- let
- val pat = Syntax.check_term ctxt (Type.constraint scr_typ raw_pat)
- val frees = all_undeclared_frees ctxt pat
- val (free_names', ctxt') = Variable.add_fixes (map fst frees) ctxt
- val frees' = map Free (free_names' ~~ map snd frees)
- val frees = map Free frees
- val (pat', raw_rhs') = apply2 (subst_free (frees ~~ frees')) (pat, unbound raw_rhs)
-
- val rhs' =
- Type.constraint expected_typ raw_rhs'
- |> Syntax.check_term (Variable.declare_term pat' ctxt')
- in
- (pat', rhs')
- end
-
- val term =
- map process_clause clauses
- |> Case_Translation.make_case ctxt Case_Translation.Quiet names scr
- |> Syntax.check_term ctxt
-
- fun find_type (t $ u) name = merge_options (find_type t name, find_type u name)
- | find_type (Abs (_, _, t)) name = find_type t name
- | find_type (Free (name', typ)) name = if name = name' then SOME typ else NONE
- | find_type _ _ = NONE
-
- fun get_type (name, typ) =
- if typ = dummyT then
- the_default dummyT (find_type term name)
- else
- typ
-
- val new_bounds = map fst bounds ~~ map get_type bounds
- in
- fold (Term.lambda o Free) new_bounds term |> strip_abs_body
- end)
-
-fun gen_equivalences prove eqs =
- update_loaded (fn lthy =>
- let
- fun prepare (lhs, rhs) =
- let
- val lhs' = qualify lthy lhs
-
- val (rule, specs) =
- Symtab.lookup (Functions.get (Proof_Context.theory_of lthy)) lhs
- |> the_error "equivalences" @{here}
-
- val goal = mk_untyped_eq (Const (lhs', dummyT), Syntax.parse_term lthy rhs)
- |> HOLogic.mk_Trueprop
- |> Syntax.check_term lthy
- in
- (lhs, specs, goal, rule)
- end
-
- val prepared = map prepare eqs
-
- fun process (name, specs, goal, rule) lthy =
- let
- val binding = Binding.qualified true "equiv" (Binding.make (name, @{here}))
- in
- case prove lthy goal rule of
- NONE => (([name], []), lthy)
- | SOME thm =>
- lthy
- |> Local_Theory.note ((Binding.empty, @{attributes [simp del]}), specs) |> snd
- |> Local_Theory.note ((binding, @{attributes [simp]}), [thm]) |> snd
- |> pair ([], [thm])
- end
-
- val ((bad, good), lthy') =
- fold_map process prepared lthy
- |>> split_list |>> apfst flat |>> apsnd flat
-
- val lthy'' =
- Local_Theory.background_theory (fold (add_report o Equivalence o print_thm lthy') good) lthy'
- in
- (bad, lthy'')
- end)
-
-val assume_equivalences =
- gen_equivalences (fn lthy => fn goal => fn _ =>
- SOME (get_oracle lthy (Thm.cterm_of lthy goal)))
- #> K ()
-
-val equivalences =
- gen_equivalences (fn lthy => fn goal => fn rule =>
- try_timeout' (Goal.prove lthy [] [] goal) (fn {context, ...} => equiv_tac rule context) |> Exn.get_res)
-
-fun functions raw_funs =
- update_loaded (fn lthy =>
- let
- fun transform (name, raw_args, (raw_rhs, expected_typ)) =
- let
- val lhs = list_comb (Free (name, dummyT), map Free raw_args)
- val rhs = Type.constraint expected_typ raw_rhs
- in
- ((Binding.make (name, @{here}), NONE, NoSyn),
- HOLogic.mk_Trueprop (Const (@{const_name HOL.eq}, dummyT) $ lhs $ rhs))
- end
-
- val no_args = exists (equal 0 o length o #2) raw_funs
-
- val specs =
- map transform raw_funs
- |> split_list
- ||> map (Syntax.check_term lthy)
- ||> length raw_funs > 1 ? homogenize_raw_types lthy
- ||> map (pair (Binding.empty, []))
- |> op ~~
-
- val recursive =
- case specs of
- [(_, (_, prop))] =>
- let
- val ((f, _), rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop prop) |>> strip_comb
- in
- exists (equal f o Free) (all_frees rhs)
- end
- | _ => true
-
- fun fun_construction lthy =
- let
- val (heads, props) = split_list specs
- val construction = Function.add_function heads props Function_Fun.fun_config pat_completeness_auto_tac
- val (_, lthy) = err_timeout "function construction" construction lthy
- val (info, lthy) = err_timeout "termination proof" (Function.prove_termination NONE (termination_tac lthy)) lthy
- in
- #simps info
- |> the_error "simps of function definition" @{here}
- |> rpair lthy
- end
- fun def_construction lthy =
- let val [(head, prop)] = specs in
- Specification.definition (SOME head, prop) lthy
- |>> snd |>> snd |>> single
- end
-
- fun construction lthy = lthy |>
- (case (recursive, no_args) of
- (true, true) => raise Unsupported ("Mutual definition without arguments: " ^ commas (map #1 raw_funs))
- | (true, false) => fun_construction
- | (false, _) => def_construction)
- in
- case Exn.interruptible_capture construction lthy of
- Exn.Res (thms, lthy) =>
- let
- val names = map #1 raw_funs
- val get_typ =
- Thm.prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst
- #> strip_comb #> fst
- #> fastype_of
- #> print_typ lthy
- val typs = map get_typ thms
- val lthy' = Local_Theory.restore lthy
- val thms = Proof_Context.export lthy lthy' thms
- val simpss = thms
- |> map (try_case_to_simps lthy' o restore_eq o full_simplify (mk_simp_ctxt lthy'))
- |> map (homogenize_spec_types lthy')
- val simps = maps if_to_cond_simps (flat simpss)
- val specs = names ~~ map (`(try_timeout' (mk_induction_schema lthy') #> Exn.get_res)) simpss
- fun print_induct (_, (NONE, _)) = NONE
- | print_induct (name, (SOME rule, _)) = SOME (name, print_thm lthy' rule)
- val binding = Binding.qualified true "spec" (Binding.make (hd names, @{here}))
- val report =
- Function
- {heads = names ~~ typs,
- inducts = map_filter print_induct specs,
- specs = map (print_thm lthy') simps,
- raws = map (print_thm lthy') thms}
- val lthy'' = lthy'
- |> Local_Theory.note ((Binding.empty, @{attributes [simp del]}), thms) |> snd
- |> Local_Theory.note ((binding, @{attributes [simp]}), simps) |> snd
- |> Local_Theory.background_theory (add_funs specs #> add_report report)
- in
- (NONE, lthy'')
- end
- | Exn.Exn (exn as Impossible _) =>
- reraise exn
- | Exn.Exn exn =>
- (SOME (print_exn exn), lthy)
- end)
-
-fun datatypes raw_dts =
- update_loaded (fn lthy =>
- let
- val raw_dts = map (apfst (qualify lthy o #1) o dupl) raw_dts
-
- fun mk_edges (qname, (_, _, constrs)) =
- let
- fun collect_types (Type (name, typs)) = name :: maps collect_types typs
- | collect_types _ = []
- val deps = constrs |> maps snd |> maps (collect_types o snd)
- in map (pair qname) deps end
-
- fun free tp = TFree ("'" ^ tp, @{sort type})
-
- fun homogenize ((dt as (_, tps, _)) :: dts) =
- let
- fun subst tps' = typ_subst_atomic (map free tps' ~~ map free tps)
- fun replace (name, tps', constrs) = (name, tps, map (apsnd (map (apsnd (subst tps')))) constrs)
- in
- dt :: map replace dts
- end
-
- val sccs = compute_sccs raw_dts (maps mk_edges raw_dts)
-
- fun check_arity_dts dts = length (distinct op = (map (length o #2) dts)) = 1
- val check_arity = not (exists (equal false) (map check_arity_dts sccs))
-
- fun transform_tp raw_tp =
- (SOME (Binding.name raw_tp), (free raw_tp, @{sort type}))
- fun transform_field (name, typ) =
- (Binding.name ("s" ^ name), typ)
- fun transform_constr (name, raw_fields) =
- (((Binding.name ("d" ^ name), Binding.name ("c" ^ name)), map transform_field raw_fields), NoSyn)
- fun transform (name, raw_tps, raw_constrs) =
- let
- val dt = ((map transform_tp raw_tps, Binding.make (name, @{here})), NoSyn)
- val constrs = map transform_constr raw_constrs
- in
- (((dt, constrs), (@{binding map}, @{binding rel})), [])
- end
-
- fun print lthy dts =
- let
- fun print_tp tp = "'" ^ tp
- fun print_tps [] = ""
- | print_tps tps = enclose "(" ")" (commas (map print_tp tps))
- fun print_field (name, typ) =
- "(s" ^ name ^ ": " ^ quote (print_typ lthy typ) ^ ")"
- fun print_constr (name, fields) =
- "d" ^ name ^ ": c" ^ name ^ " " ^ space_implode " " (map print_field fields)
- fun print_one (name, tps, constrs) =
- print_tps tps ^ " " ^ name ^ " = " ^ space_implode " | " (map print_constr constrs)
- in
- "datatype " ^ space_implode " and " (map print_one dts)
- end
-
- fun setup_dts scc lthy =
- let
- val input = (Ctr_Sugar.default_ctr_options, map transform scc)
- val lthy =
- BNF_FP_Def_Sugar.co_datatypes BNF_Util.Least_FP BNF_LFP.construct_lfp input lthy
- |> Local_Theory.restore
-
- fun get_sugar (name, _, _) =
- qualify lthy name |> Ctr_Sugar.ctr_sugar_of lthy
- |> the_error ("ctr_sugar of " ^ name) @{here}
-
- val sugars = map get_sugar scc
-
- fun get_splits {split, split_asm, ...} = [split, split_asm]
- fun get_cases {case_thms, ...} = case_thms
- in
- lthy
- |> Local_Theory.note ((Binding.empty, @{attributes [split]}), maps get_splits sugars) |> snd
- |> Local_Theory.note ((Binding.empty, @{attributes [leon_unfold]}), maps get_cases sugars) |> snd
- end
- in
- if check_arity then
- let
- val sccs = map homogenize sccs
- val lthy' = fold setup_dts sccs lthy
- val lthy'' = Local_Theory.background_theory (fold (add_report o Datatype o print lthy') sccs) lthy'
- in (NONE, lthy'') end
- else
- (SOME "Unsupported feature: mismatched datatype arity", lthy)
- end)
-
-fun lookup_datatype (name, raw_constructors) =
- update_loaded (fn lthy =>
- case Ctr_Sugar.ctr_sugar_of lthy name of
- NONE =>
- (Codec.Left ("unknown datatype " ^ name), lthy)
- | SOME {ctrs, discs, selss, split, split_asm, case_thms, ...} =>
- let
- val raw_constructors = sort_by snd (raw_constructors)
- val (names, terms) =
- map (fst o dest_Const) ctrs ~~ (discs ~~ selss)
- |> sort_by fst
- |> split_list
- fun process (internal_name, name) (disc, sels) =
- (internal_name, (Const (name, dummyT), dummify_types disc, map dummify_types sels))
-
- val lthy' =
- lthy
- |> Local_Theory.note ((Binding.empty, @{attributes [split]}), [split, split_asm]) |> snd
- |> Local_Theory.note ((Binding.empty, @{attributes [leon_unfold]}), case_thms) |> snd
- in
- if map snd raw_constructors <> names then
- (Codec.Left ("constructor name mismatch: declared constructors are " ^ commas names), lthy)
- else
- (Codec.Right (map2 process raw_constructors terms), lthy')
- end)
-
-fun pretty t =
- access_loaded (fn lthy => print_term lthy t)
-
-fun report () =
- access_loaded (fn lthy =>
- let
- fun print_report (Theory {scripts, ...}) = map (pair "Script" o fst) scripts
- | print_report (Equivalence prop) = [("Equivalence", prop)]
- | print_report (Datatype spec) = [("Datatype", spec)]
- | print_report (Lemma {name, prop}) = [("Lemma", name ^ ": " ^ prop)]
- | print_report (Function {raws, inducts, specs, ...}) =
- map (pair "Function (raw)") raws @
- map (pair "Function (spec)") specs @
- map (fn (name, induct) => ("Function (induct)", name ^ ": " ^ induct)) inducts
- | print_report Oracle = [("Oracle", "enabled")]
- in
- Proof_Context.theory_of lthy
- |> Reports.get
- |> rev
- |> maps print_report
- end)
-
-fun dump () =
- access_loaded (fn lthy =>
- let
- fun print_thy_header name imports =
- "theory " ^ name ^ "\n" ^
- "imports " ^ space_implode " " imports ^ "\n" ^
- "begin\n"
-
- fun print_thy name import text =
- print_thy_header name [import] ^ text ^ "\nend\n"
-
- val name = Context.theory_name (Proof_Context.theory_of lthy)
-
- fun print_report (Theory {scripts, import}) =
- (map (fn (script_name, text) => (script_name, print_thy script_name import text)) scripts,
- print_thy_header name (import :: map fst scripts))
- | print_report (Equivalence prop) = ([], "lemma [simp]: " ^ quote prop ^ "\nsorry")
- | print_report (Lemma {prop, ...}) = ([], "lemma [simp]: " ^ quote prop ^ "\nsorry")
- | print_report (Datatype spec) = ([], spec)
- | print_report Oracle = ([], "")
- | print_report End = ([], "\nend\n")
- | print_report (Function {heads, specs, ...}) =
- let
- fun mk_head (name, typ) = quote name ^ " :: " ^ quote typ
- val head = "fun " ^ space_implode " and " (map mk_head heads) ^ " where\n"
- val body = space_implode "|\n" (map quote specs)
- in
- ([], head ^ body)
- end
- in
- Proof_Context.theory_of lthy
- |> Reports.get
- |> cons End
- |> rev
- |> map print_report
- |> split_list
- |>> flat
- ||> space_implode "\n\n"
- ||> pair name
- |> swap
- |> op ::
- end)
-
-end
\ No newline at end of file
diff --git a/src/main/isabelle/stateless_ops.ML b/src/main/isabelle/stateless_ops.ML
deleted file mode 100644
index 31fc63999570922f63dac1972289bd43b1044a5b..0000000000000000000000000000000000000000
--- a/src/main/isabelle/stateless_ops.ML
+++ /dev/null
@@ -1,40 +0,0 @@
-signature STATELESS_OPS = sig
- val numeral: (int * typ) -> term
- val serial_nat: unit -> term
- val word: int -> typ
- val map: ((term * term) list * (typ * typ)) -> term
-end
-
-structure Stateless_Ops: STATELESS_OPS = struct
-
-fun numeral (n, typ) =
- let
- fun wrap numeral = HOLogic.numeral_const typ $ numeral
- in
- if n = 0 then
- Const (@{const_name "zero_class.zero"}, typ)
- else if n > 0 then
- wrap (HOLogic.mk_numeral n)
- else
- Const (@{const_name "uminus"}, dummyT) $ wrap (HOLogic.mk_numeral (~n))
- end
-
-val serial_nat =
- numeral o rpair @{typ nat} o serial
-
-fun word n =
- Type (@{type_name word}, [Syntax.read_typ @{context} (Markup.print_int n)])
-
-fun map (xs, (fty, tty)) =
- let
- val opt_tty = Type (@{type_name option}, [tty])
- val fun_ty = fty --> opt_tty
- val init = Abs ("x", fty, Const (@{const_name None}, opt_tty))
- fun aux (f, t) acc =
- Const (@{const_name fun_upd}, fun_ty --> fty --> opt_tty --> fun_ty) $ acc $ f $
- (Const (@{const_name Some}, tty --> opt_tty) $ t)
- in
- fold aux xs init
- end
-
-end
\ No newline at end of file
diff --git a/src/main/isabelle/tactics.ML b/src/main/isabelle/tactics.ML
deleted file mode 100644
index d2a5ce83b8499bcc45bd0037a992e56f9f7d30c7..0000000000000000000000000000000000000000
--- a/src/main/isabelle/tactics.ML
+++ /dev/null
@@ -1,66 +0,0 @@
-fun mk_simp_ctxt ctxt =
- (put_simpset HOL_ss ctxt) addsimps Named_Theorems.get ctxt @{named_theorems leon_unfold}
-
-fun prove_tac ctxt =
- HEADGOAL
- (SELECT_GOAL (TRY (auto_tac ctxt)) THEN_ALL_NEW
- (FIRST'
- [Cooper.tac false [] [] ctxt,
- Sledgehammer_Tactics.sledgehammer_with_metis_tac ctxt [] Sledgehammer_Fact.no_fact_override []]))
-
-fun equiv_tac rule ctxt =
- let
- val solve_tac =
- TRY (ALLGOALS (REPEAT_ALL_NEW (resolve_tac ctxt @{thms ext}))) THEN
- Local_Defs.unfold_tac ctxt (Named_Theorems.get ctxt @{named_theorems leon_unfold}) THEN
- auto_tac ctxt
-
- fun ext_tac 0 _ = all_tac
- | ext_tac n k = resolve_tac ctxt @{thms ext} k THEN ext_tac (n - 1) k
-
- fun induct rule = CSUBGOAL (fn (concl, n) =>
- let
- val (p, args) = strip_comb (HOLogic.dest_Trueprop (Thm.concl_of rule))
-
- val p_inst = Thm.term_of concl
- |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
- |> apply2 (rpair (map Bound (length args - 1 downto 0)))
- |> apply2 list_comb
- |> HOLogic.mk_eq
- |> fold (fn _ => fn t => Abs ("x", dummyT, t)) (1 upto length args)
- |> Syntax.check_term ctxt
- |> Thm.cterm_of ctxt
-
- val insts = [(fst (dest_Var p), p_inst)]
- val rule = Drule.infer_instantiate ctxt insts rule
- in ext_tac (length args) n THEN resolve_tac ctxt [rule] n end)
-
- val maybe_induct =
- case rule of
- NONE => K all_tac
- | SOME rule => induct rule
- in
- HEADGOAL maybe_induct THEN solve_tac
- end
-
-fun method_tac pos src = Subgoal.FOCUS (fn {context = ctxt, concl, ...} =>
- let
- val scan = Scan.finite Token.stopper Method.parse;
- val ((m, _), []) =
- src
- |> Token.explode (Thy_Header.get_keywords (Proof_Context.theory_of ctxt)) pos
- |> filter_out Token.is_space
- |> Scan.catch scan
- val state =
- Proof.theorem NONE (K I) [[(Thm.term_of concl, [])]] ctxt
- |> Proof.refine_singleton m
- val {goal, ...} = Proof.simple_goal state
- in
- HEADGOAL (resolve_tac ctxt [Goal.conclude goal])
- end)
-
-fun pat_completeness_auto_tac ctxt =
- Pat_Completeness.pat_completeness_tac ctxt 1 THEN auto_tac ctxt
-
-fun termination_tac ctxt =
- Function_Common.termination_prover_tac true ctxt
\ No newline at end of file
diff --git a/src/main/isabelle/util.ML b/src/main/isabelle/util.ML
deleted file mode 100644
index 55be31d116b0e3be15c4ffb19b30b38946213996..0000000000000000000000000000000000000000
--- a/src/main/isabelle/util.ML
+++ /dev/null
@@ -1,281 +0,0 @@
-fun map_result_exn _ (Exn.Res r) = Exn.Res r
- | map_result_exn f (Exn.Exn exn) = Exn.Exn (f exn)
-
-fun print_position pos =
- let
- val print_file = Path.implode o Path.base o Path.explode
- in
- case (Position.file_of pos, Position.line_of pos) of
- (SOME file, SOME line) => print_file file ^ ":" ^ Markup.print_int line
- | (SOME file, NONE) => print_file file
- | _ => "<unknown>"
- end
-
-exception Unsupported of string
-exception Construction of string * exn
-exception Impossible of string
-exception Invalid_State of string
-exception Timeout of string
-
-local
- fun format_message msg pos = msg ^ " (at " ^ print_position pos ^ ")"
-in
-
-fun impossible msg pos =
- raise Impossible (format_message msg pos)
-
-fun invalid_state msg pos =
- raise Invalid_State (format_message msg pos)
-
-fun the_error msg pos NONE = impossible ("expected SOME: " ^ msg) pos
- | the_error _ _ (SOME x) = x
-
-fun single_error _ _ [t] = t
- | single_error msg pos _ = impossible ("expected singleton list: " ^ msg) pos
-
-end
-
-fun print_exn (exn: exn) =
- YXML.content_of (@{make_string} exn)
-
-fun check true _ = ()
- | check false f = error (f ())
-
-fun dupl x = (x, x)
-
-val unvarify_typ =
- let
- fun aux (TVar ((name, idx), sort)) = TFree (name ^ Markup.print_int idx, sort)
- | aux t = t
- in map_atyps aux end
-
-val unvarify =
- let
- fun aux (Var ((name, idx), typ)) = Free (name ^ Markup.print_int idx, typ)
- | aux t = t
- in map_aterms aux o map_types unvarify_typ end
-
-fun print_term ctxt =
- let
- val ctxt' = Config.put show_markup false ctxt
- in YXML.content_of o Syntax.string_of_term ctxt' o unvarify end
-
-fun print_typ ctxt =
- let
- val ctxt' = Config.put show_markup false ctxt
- in YXML.content_of o Syntax.string_of_typ ctxt' o unvarify_typ end
-
-fun print_thm ctxt thm =
- let
- val t = Thm.prop_of thm
- val {oracle, ...} = Thm.peek_status thm
- val suffix = if oracle then " [!]" else ""
- in
- print_term ctxt t ^ suffix
- end
-
-fun all_consts (Const (name, typ)) = [(name, typ)]
- | all_consts (t $ u) = all_consts t @ all_consts u
- | all_consts (Abs (_, _, t)) = all_consts t
- | all_consts _ = []
-
-fun all_frees (Free (name, typ)) = [(name, typ)]
- | all_frees (t $ u) = all_frees t @ all_frees u
- | all_frees (Abs (_, _, t)) = all_frees t
- | all_frees _ = []
-
-fun all_undeclared_frees ctxt =
- all_frees
- #> distinct op =
- #> filter (not o Variable.is_declared ctxt o fst)
-
-fun register_terms ts lthy =
- let
- val ts' = Syntax.check_terms lthy ts |> map HOLogic.mk_Trueprop
- val frees = distinct op = (maps (all_undeclared_frees lthy) ts')
- val (free_names', lthy) = Variable.add_fixes (map fst frees) lthy
- val frees' = map Free (free_names' ~~ map snd frees)
- val frees = map Free frees
- val ts'' = map (subst_free (frees ~~ frees')) ts'
- in
- (ts'', fold Variable.declare_term ts'' lthy)
- end
-
-fun qualify ctxt name =
- Context.theory_name (Proof_Context.theory_of ctxt) ^ "." ^ name
-
-fun compute_sccs nodes edges =
- Graph.empty
- |> fold Graph.new_node nodes
- |> fold (fn edge => perhaps (try (Graph.add_edge edge))) edges
- |> (fn graph => map (map (Graph.get_node graph)) (Graph.strong_conn graph))
- |> rev
-
-val dummify_types = map_types (K dummyT)
-
-fun fold_opt _ [] y = SOME y
- | fold_opt f (x :: xs) y = Option.mapPartial (fold_opt f xs) (f x y)
-
-fun fold_res _ [] y = Exn.Res y
- | fold_res f (x :: xs) y = Exn.maps_res (fold_res f xs) (f x y)
-
-fun map_generalized f t =
- case t of
- Const (@{const_name Pure.all}, typ) $ Abs (name, typ', t) =>
- (Const (@{const_name Pure.all}, typ) $ Abs (name, typ', map_generalized f t))
- | _ =>
- f t
-
-fun mk_untyped_eq (x, y) =
- HOLogic.eq_const dummyT $ x $ y
-
-fun strip_first_prem t =
- let
- val prems = tl (Logic.strip_imp_prems t)
- val concl = Logic.strip_imp_concl t
- in Logic.list_implies (prems, concl) end
-
-fun map_prems f t =
- let
- val prems = Logic.strip_imp_prems t
- val concl = Logic.strip_imp_concl t
- in Logic.list_implies (map f prems, concl) end
-
-fun mk_induction_schema lthy thms =
- let
- val props = map (unvarify o Thm.prop_of) thms
-
- val ((heads, argss), rhss) =
- props
- |> map (HOLogic.dest_eq o HOLogic.dest_Trueprop)
- |> split_list
- |>> map strip_comb |>> split_list
-
- val names =
- map (fst o dest_Const) heads
- |> distinct op =
- |> Name.invent_names (Variable.names_of (fold Variable.declare_names (flat argss) lthy)) "temp"
- |> map swap
-
- fun subst (t as Const (name, _)) =
- (case AList.lookup op = names name of SOME new => Free (new, dummyT) | NONE => t)
- | subst t = t
-
- fun mk_prop head args rhs =
- map_aterms subst rhs
- |> pair (list_comb (subst head, args))
- |> mk_untyped_eq
- |> HOLogic.mk_Trueprop
-
- fun mk_head name = (Binding.name name, NONE, NoSyn)
- val props = map (pair (Binding.empty, [])) (Syntax.check_terms lthy (@{map 3} mk_prop heads argss rhss))
- val heads = map (mk_head o snd) names
-
- val (info, _) =
- (* FIXME funny warning *)
- Function.add_function heads props Function_Common.default_config pat_completeness_auto_tac lthy
-
- val raw_prop = unvarify (Thm.prop_of (hd (#pinducts info)))
- val prop = map_prems (map_generalized strip_first_prem) (strip_first_prem raw_prop)
- val frees = distinct op = (map fst (all_frees prop))
-
- fun tac ctxt =
- Induction_Schema.induction_schema_tac ctxt [] THEN
- HEADGOAL (Pat_Completeness.pat_completeness_tac ctxt) THEN
- Lexicographic_Order.lexicographic_order_tac false ctxt
-
- val thm = Goal.prove lthy frees [] prop (fn {context, ...} => tac context)
- val lthy' = Local_Theory.restore lthy
- in
- Morphism.thm (Proof_Context.export_morphism lthy lthy') thm
- end
-
-(* based on Thy_Info.script_thy *)
-fun script_thy pos txt thy =
- let
- val trs = flat
- [[Toplevel.init_theory (K thy) Toplevel.empty],
- Outer_Syntax.parse thy pos txt,
- [Toplevel.exit Toplevel.empty]]
- val end_state = fold (Toplevel.command_exception true) trs Toplevel.toplevel;
- in
- Toplevel.end_theory pos end_state
- end
-
-fun try_timeout secs f x =
- let
- val time = Time.fromSeconds secs
- in
- Exn.capture (TimeLimit.timeLimit time f) x
- end
-
-fun try_case_to_simps ctxt thm =
- the_default [thm] (try (Simps_Case_Conv.to_simps ctxt) thm)
-
-fun restore_eq thm =
- case Thm.prop_of thm of
- @{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => thm
- | _ => @{lemma "P \<Longrightarrow> P = True" by simp} OF [thm]
-
-fun homogenize_spec_types ctxt thms =
- let
- val get_head = dest_Const o fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of
- val paired = map (`get_head) thms
-
- val head = map (fst o fst) paired
- |> distinct op =
- |> single_error "heads" @{here}
-
- val typ = Sign.the_const_type (Proof_Context.theory_of ctxt) head
-
- fun mk_subst (iname, (sort, inst)) =
- ((iname, sort), Thm.ctyp_of ctxt inst)
-
- fun instantiate ((_, ttyp), thm) =
- let
- val subst = Type.raw_match (ttyp, typ) Vartab.empty |> Vartab.dest |> map mk_subst
- in
- Thm.instantiate (subst, []) thm
- end
- in
- map instantiate paired
- end
-
-fun unify_all_types ctxt ts =
- let
- val unif = Pattern.unify_types (Context.Proof ctxt)
- fun aux (t1 :: t2 :: ts) env = aux (t2 :: ts) (unif (t1, t2) env)
- | aux _ env = env
- in
- aux ts
- end
-
-fun homogenize_raw_types ctxt terms =
- let
- val terms = map Logic.varify_types_global terms
-
- val get_head = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop
- val heads = map get_head terms
-
- fun typ_occurences head =
- maps all_frees terms
- |> filter (equal head o fst)
- |> map snd
-
- val problem = map typ_occurences heads
- val env = Envir.empty (maxidx_of_typs (flat problem))
-
- val env' = fold (unify_all_types ctxt) problem env
-
- val solution = map_types (unvarify_typ o Envir.norm_type (Envir.type_env env'))
- in
- map solution terms
- |> Syntax.check_terms ctxt (* fail early if something's wrong *)
- end
-
-fun if_to_cond_simps thm =
- case Thm.concl_of thm of
- @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ (Const (@{const_name If}, _) $ _ $ _ $ _)) =>
- maps (fn s => if_to_cond_simps (s OF [thm])) @{thms if_to_cond_simps}
- | _ =>
- [thm]
\ No newline at end of file
diff --git a/src/main/scala/inox/InoxContext.scala b/src/main/scala/inox/InoxContext.scala
index fa49102840a559fbb0f3d30b827ac64547d902b4..1c3554235ab2dc9a8e721a7c4010850b9f822a8a 100644
--- a/src/main/scala/inox/InoxContext.scala
+++ b/src/main/scala/inox/InoxContext.scala
@@ -16,8 +16,10 @@ case class InoxContext(
def build(opts: Seq[InoxOption[Any]]) = InoxContext(reporter, interruptManager, opts, timers)
- def toSolver: solvers.SolverOptions = ???
- def toEvaluator: evaluators.EvaluatorOptions = ???
+ def toSolver: solvers.SolverOptions = solvers.SolverOptions(
+ options.filter(opt => solvers.SolverOptions.options.exists(_ == opt.optionDef)))
+ def toEvaluator: evaluators.EvaluatorOptions = evaluators.EvaluatorOptions(
+ options.filter(opt => evaluators.EvaluatorOptions.options.exists(_ == opt.optionDef)))
}
object InoxContext {
diff --git a/src/main/scala/inox/ast/Constructors.scala b/src/main/scala/inox/ast/Constructors.scala
index 2ba2c15118fd6d4d7ef5b61b318a228b3acf0d1a..e9bf6c88568941cde347ea2f98810b6392ef121a 100644
--- a/src/main/scala/inox/ast/Constructors.scala
+++ b/src/main/scala/inox/ast/Constructors.scala
@@ -280,8 +280,4 @@ trait Constructors {
IsInstanceOf(expr, tpe)
}
}
-
- def finiteLambda(cases: Seq[(Expr, Expr)], default: Expr, ft: FunctionType): Expr = {
- ???
- }
}
diff --git a/src/main/scala/inox/evaluators/Evaluator.scala b/src/main/scala/inox/evaluators/Evaluator.scala
index c7f271d2769467e7b9d05852ee57adcfdb734ca2..af3fc771fcfd6e516ea4177fec393e2cad57e4cb 100644
--- a/src/main/scala/inox/evaluators/Evaluator.scala
+++ b/src/main/scala/inox/evaluators/Evaluator.scala
@@ -9,8 +9,14 @@ case class EvaluatorOptions(options: Seq[InoxOption[Any]]) extends InoxOptions[E
object EvaluatorOptions {
def empty = EvaluatorOptions(Seq())
+
+ val options = Seq(
+ optIgnoreContracts
+ )
}
+object optIgnoreContracts extends InoxFlagOptionDef("ignorecontracts", "Don't fail on invalid contracts during evaluation", false)
+
trait Evaluator {
val program: Program
val options: EvaluatorOptions
diff --git a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
index 983bc3a49c9583c96595a225f234767fa3e7129c..745b7e1e7a0a949979add45d19b88bc972282527 100644
--- a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
@@ -17,6 +17,8 @@ trait RecursiveEvaluator
val name = "Recursive Evaluator"
+ lazy val ignoreContracts = options.findOptionOrDefault(optIgnoreContracts)
+
private def shift(b: BitSet, size: Int, i: Int): BitSet =
b.map(_ + i).filter(bit => bit >= 1 && bit <= size)
@@ -50,7 +52,7 @@ trait RecursiveEvaluator
e(b)(rctx.withNewVar(i, first), gctx)
case Assume(cond, body) =>
- if (e(cond) != BooleanLiteral(true))
+ if (!ignoreContracts && e(cond) != BooleanLiteral(true))
throw RuntimeError("Assumption did not hold @" + expr.getPos)
e(body)
diff --git a/src/main/scala/inox/evaluators/SolvingEvaluator.scala b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
index 554f6a44a4bfd55580d32d9b888bc2b4519e5900..cbe03bda120b01fbf3ec4d0d6d5641c19c2f7cf8 100644
--- a/src/main/scala/inox/evaluators/SolvingEvaluator.scala
+++ b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
@@ -12,7 +12,7 @@ trait SolvingEvaluator extends Evaluator {
import program.trees._
import program.symbols._
- object optForallCache extends InoxOptionDef[MutableMap[program.trees.Forall, Boolean]] {
+ private object optForallCache extends InoxOptionDef[MutableMap[program.trees.Forall, Boolean]] {
val parser = { (_: String) => throw FatalError("Unparsable option \"bankOption\"") }
val name = "bank-option"
val description = "Evaluation bank shared between solver and evaluator"
diff --git a/src/main/scala/inox/solvers/Solver.scala b/src/main/scala/inox/solvers/Solver.scala
index c85ed8688d578e091a1cc040f7f5897f766f8449..b6874bea60ef94735202f6963474757b8ee2b6b5 100644
--- a/src/main/scala/inox/solvers/Solver.scala
+++ b/src/main/scala/inox/solvers/Solver.scala
@@ -11,6 +11,15 @@ case class SolverOptions(options: Seq[InoxOption[Any]]) extends InoxOptions[Solv
object SolverOptions {
def empty = SolverOptions(Seq())
+
+ val options = Seq(
+ optCheckModels,
+ optSilentErrors,
+ unrolling.optUnrollFactor,
+ unrolling.optFeelingLucky,
+ unrolling.optUnrollCores,
+ smtlib.optCVC4Options
+ )
}
case object DebugSectionSolver extends DebugSection("solver")
diff --git a/src/main/scala/inox/solvers/smtlib/CVC4Target.scala b/src/main/scala/inox/solvers/smtlib/CVC4Target.scala
index e9961b45169429b8a625e11b4b3b677952a3a0d4..b4a788bfe305f63a8019cf41d33f62acb87ad3c3 100644
--- a/src/main/scala/inox/solvers/smtlib/CVC4Target.scala
+++ b/src/main/scala/inox/solvers/smtlib/CVC4Target.scala
@@ -54,44 +54,18 @@ trait CVC4Target extends SMTLIBTarget {
case (QualifiedIdentifier(SMTIdentifier(SSymbol("emptyset"), Seq()), _), Some(SetType(base))) =>
FiniteSet(Seq(), base)
- case (FunctionApplication(QualifiedIdentifier(SMTIdentifier(SSymbol("const"), _), _), Seq(elem)), Some(tpe)) =>
- tpe match {
- case ft @ FunctionType(from, to) =>
- finiteLambda(Seq.empty, fromSMT(elem, to), ft)
-
- case MapType(k, v) =>
- FiniteMap(Seq(), fromSMT(elem, v), k)
- }
-
- case (FunctionApplication(SimpleSymbol(SSymbol("__array_store_all__")), Seq(_, elem)), Some(tpe)) =>
- tpe match {
- case ft @ FunctionType(from, to) =>
- finiteLambda(Seq.empty, fromSMT(elem, to), ft)
-
- case MapType(k, v) =>
- FiniteMap(Seq(), fromSMT(elem, v), k)
- }
-
- case (FunctionApplication(SimpleSymbol(SSymbol("store")), Seq(arr, key, elem)), Some(tpe)) =>
- tpe match {
- case FunctionType(from, v) =>
- val Lambda(args, bd) = fromSMT(arr, otpe)
- Lambda(args, IfExpr(
- Equals(
- tupleWrap(args.map(_.toVariable)),
- fromSMT(key, tupleTypeWrap(from))
- ),
- fromSMT(elem, v),
- bd
- ))
-
- case MapType(kT, vT) =>
- val FiniteMap(elems, default, _) = fromSMT(arr, otpe)
- val newKey = fromSMT(key, kT)
- val newV = fromSMT(elem, vT)
- val newElems = elems.filterNot(_._1 == newKey) :+ (newKey -> newV)
- FiniteMap(newElems, default, kT)
- }
+ case (FunctionApplication(QualifiedIdentifier(SMTIdentifier(SSymbol("const"), _), _), Seq(elem)), Some(MapType(k, v))) =>
+ FiniteMap(Seq(), fromSMT(elem, v), k)
+
+ case (FunctionApplication(SimpleSymbol(SSymbol("__array_store_all__")), Seq(_, elem)), Some(MapType(k, v))) =>
+ FiniteMap(Seq(), fromSMT(elem, v), k)
+
+ case (FunctionApplication(SimpleSymbol(SSymbol("store")), Seq(arr, key, elem)), Some(MapType(kT, vT))) =>
+ val FiniteMap(elems, default, _) = fromSMT(arr, otpe)
+ val newKey = fromSMT(key, kT)
+ val newV = fromSMT(elem, vT)
+ val newElems = elems.filterNot(_._1 == newKey) :+ (newKey -> newV)
+ FiniteMap(newElems, default, kT)
case (FunctionApplication(SimpleSymbol(SSymbol("singleton")), elems), Some(SetType(base))) =>
FiniteSet(elems.map(fromSMT(_, base)), base)
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index 887e008442e78b99421f3e0470910f94c6e42992..9650c3903bcace2ad71b15955d1374cce682bbd9 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -12,7 +12,6 @@ import evaluators._
object optUnrollFactor extends InoxLongOptionDef("unrollfactor", "Number of unfoldings to perform in each unfold step", default = 1, "<PosInt>")
object optFeelingLucky extends InoxFlagOptionDef("feelinglucky", "Use evaluator to find counter-examples early", false)
object optUnrollCores extends InoxFlagOptionDef("unrollcores", "Use unsat-cores to drive unfolding while remaining fair", false)
-object optAssumePre extends InoxFlagOptionDef("assumepre", "Assume precondition holds (pre && f(x) = body) when unfolding", false)
trait AbstractUnrollingSolver
extends Solver {
@@ -42,12 +41,11 @@ trait AbstractUnrollingSolver
type Cores = Set[Encoded]
}
- val unfoldFactor = options.findOptionOrDefault(optUnrollFactor)
- val feelingLucky = options.findOptionOrDefault(optFeelingLucky)
- val checkModels = options.findOptionOrDefault(optCheckModels)
- val unrollUnsatCores = options.findOptionOrDefault(optUnrollCores)
- val assumePreHolds = options.findOptionOrDefault(optAssumePre)
- val silentErrors = options.findOptionOrDefault(optSilentErrors)
+ lazy val unfoldFactor = options.findOptionOrDefault(optUnrollFactor)
+ lazy val feelingLucky = options.findOptionOrDefault(optFeelingLucky)
+ lazy val checkModels = options.findOptionOrDefault(optCheckModels)
+ lazy val unrollUnsatCores = options.findOptionOrDefault(optUnrollCores)
+ lazy val silentErrors = options.findOptionOrDefault(optSilentErrors)
def check(config: Configuration): config.Response[Model, Cores] =
checkAssumptions(config)(Set.empty)