diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index d09cc1d02..89736c488 100644 --- a/src/bin/common/parse_command.ml +++ b/src/bin/common/parse_command.ml @@ -366,8 +366,8 @@ let mk_limit_opt age_bound fm_cross_limit timelimit_interpretation `Ok() let mk_output_opt - interpretation use_underscore unsat_core output_format model_type - () () () () + interpretation use_underscore all_models show_prop_model unsat_core + output_format model_type () () () () = set_infer_output_format (Option.is_none output_format); let output_format = match output_format with @@ -380,6 +380,8 @@ let mk_output_opt in set_interpretation interpretation; set_interpretation_use_underscore use_underscore; + set_all_models all_models; + set_show_prop_model show_prop_model; set_unsat_core unsat_core; set_output_format output_format; set_model_type model_type; @@ -1032,11 +1034,29 @@ let parse_output_opt = let docv = "VAL" in Arg.(value & flag & info ["interpretation-use-underscore";"use-underscore"] - ~docv ~docs:s_models ~doc ~deprecated) in + ~docv ~docs:s_models ~doc ~deprecated) + in + let all_models = + let doc = "Enable all-models (or all-sat) feature, in which case, \ + all possible boolean models will be explored. If \ + --interpretation is also set, an interpretation for \ + each boolean model will also be displayed. Note that \ + timeouts are set per model/SAT branch in this case." + in + Arg.(value & flag & info ["all-models"; "all-sat"] ~docs:s_models ~doc) + in + let show_prop_model = + let doc = " also show the propositional if a model is requested \ + (with --interpretation or with --all-models options)." + in + Arg.(value & flag & info + ["show-prop-model"; "show-propositional-model"] ~docs:s_models ~doc) + in let unsat_core = let doc = "Experimental support for computing and printing unsat-cores." in - Arg.(value & flag & info ["u"; "unsat-core"] ~doc ~docs) in + Arg.(value & flag & info ["u"; "unsat-core"] ~doc ~docs) + in let output_format = let doc = @@ -1082,8 +1102,9 @@ let parse_output_opt = in Term.(ret (const mk_output_opt $ - interpretation $ use_underscore $ unsat_core $ - output_format $ model_type $ + interpretation $ use_underscore $ + all_models $ show_prop_model $ + unsat_core $ output_format $ model_type $ set_dump_models $ set_dump_models_on $ set_sat_options $ set_frontend )) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 22afb5053..bf85516f7 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -121,7 +121,7 @@ let main () = | Ty.Cut -> { state with solver_ctx = { state.solver_ctx with local = []}} - | Ty.Thm | Ty.Sat -> + | Ty.Thm | Ty.Sat | Ty.AllSat _ -> { state with solver_ctx = { state.solver_ctx with global = []; local = []}} end @@ -223,7 +223,7 @@ let main () = State.create_key ~pipe:"" "solving_state" in - let partial_model_key: SAT.t option State.key = + let partial_model_key: Models.t Lazy.t option State.key = State.create_key ~pipe:"" "sat_state" in @@ -453,20 +453,20 @@ let main () = List.rev (cnf :: hyps), is_thm | _ -> assert false in - let partial_model = solve all_context (cnf, name) in + let sat_env = solve all_context (cnf, name) in if is_thm then State.set solver_ctx_key ( let solver_ctx = State.get solver_ctx_key st in { solver_ctx with global = []; local = [] } ) st - |> State.set partial_model_key partial_model + |> State.set partial_model_key (Option.bind sat_env SAT.get_model) else State.set solver_ctx_key ( let solver_ctx = State.get solver_ctx_key st in { solver_ctx with local = [] } ) st - |> State.set partial_model_key partial_model + |> State.set partial_model_key (Option.bind sat_env SAT.get_model) | {contents = `Set_option { DStd.Term.term = @@ -481,17 +481,10 @@ let main () = | {contents = `Get_model; _ } -> if Options.get_interpretation () then match State.get partial_model_key st with - | Some partial_model -> - begin - match SAT.get_model partial_model with - | Some (lazy model) -> - Models.output_concrete_model - (Options.Output.get_fmt_regular ()) model; - st - | _ -> - (* TODO: is it reachable? *) - st - end + | Some (lazy model) -> + Models.output_concrete_model ~pp_prop_model:false + (Options.Output.get_fmt_regular ()) model; + st | None -> (* TODO: add the location of the statement. *) Printer.print_smtlib_err "No model produced."; diff --git a/src/bin/js/worker_js.ml b/src/bin/js/worker_js.ml index 4442500ec..e289d7512 100644 --- a/src/bin/js/worker_js.ml +++ b/src/bin/js/worker_js.ml @@ -145,7 +145,107 @@ let main worker_id content = begin match kind with | Ty.Check | Ty.Cut -> { state with local = []; } - | Ty.Thm | Ty.Sat -> { state with global = []; local = []; } + | Ty.Thm | Ty.Sat | Ty.AllSat _ -> + { state with global = []; local = []; } + end + | Typed.TAxiom (_, s, _, _) when Ty.is_global_hyp s -> + let cnf = Cnf.make state.global td in + { state with global = cnf; } + | Typed.TAxiom (_, s, _, _) when Ty.is_local_hyp s -> + let cnf = Cnf.make state.local td in + { state with local = cnf; } + | _ -> + let cnf = Cnf.make state.ctx td in + { state with ctx = cnf; } + in + + let (module I : Input.S) = Input.find (Options.get_frontend ()) in + let parsed () = + try + Options.Time.start (); + I.parse_file ~content ~format:None + with + | Parsing.Parse_error -> + Printer.print_err "%a" Errors.report + (Syntax_error ((Lexing.dummy_pos,Lexing.dummy_pos),"")); + raise Exit + | Errors.Error e -> + begin match e with + | Errors.Run_error r -> begin + match r with + | Steps_limit _ -> + returned_status := + Worker_interface.LimitReached "Steps limit" + | _ -> returned_status := Worker_interface.Error "Run error" + end + | _ -> returned_status := Worker_interface.Error "Error" + end; + Printer.print_err "%a" Errors.report e; + raise Exit + in + let all_used_context = FE.init_all_used_context () in + let assertion_stack = Stack.create () in + let typing_loop state p = + try + let l, env = I.type_parsed state.env assertion_stack p in + List.fold_left (typed_loop all_used_context) { state with env; } l + with Errors.Error e -> + Printer.print_err "%a" Errors.report e; + raise Exit + in + + let state = { + env = I.empty_env; + ctx = []; + local = []; + global = []; + } in + + begin + try let _ : _ state = + Seq.fold_left typing_loop state (parsed ()) in () + with Exit -> () end; + + let get_status_and_print status n = + returned_status := + begin match status with + | FE.Unsat _ -> Worker_interface.Unsat n + | FE.Inconsistent _ -> Worker_interface.Inconsistent n + | FE.Sat _ -> Worker_interface.Sat n + | FE.Unknown _ -> Worker_interface.Unknown n + | FE.Timeout _ -> Worker_interface.LimitReached "timeout" + | FE.Preprocess -> Worker_interface.Unknown n + end; + FE.print_status status n + in + + let solve all_context (cnf, goal_name) = + let used_context = FE.choose_used_context all_context ~goal_name in + let consistent_dep_stack = Stack.create () in + SAT.reset_refs (); + let _,_,dep = + let env = SAT.empty_with_inst add_inst in + List.fold_left + (FE.process_decl + get_status_and_print used_context consistent_dep_stack) + (env, `Unknown env, Explanation.empty) cnf + in + if Options.get_unsat_core () then begin + unsat_core := Explanation.get_unsat_core dep; + end; + in + + let typed_loop all_context state td = + match td.Typed.c with + | Typed.TGoal (_, kind, name, _) -> + let l = state.local @ state.global @ state.ctx in + let cnf = List.rev @@ Cnf.make l td in + let () = solve all_context (cnf, name) in + begin match kind with + | Ty.Check + | Ty.Cut -> { state with local = []; } + | Ty.Thm | Ty.Sat | Ty.AllSat _ -> + { state with global = []; local = []; } end | Typed.TAxiom (_, s, _, _) when Ty.is_global_hyp s -> let cnf = Cnf.make state.global td in @@ -224,13 +324,12 @@ let main worker_id content = end | Some r -> let b,e = r.loc in - (r.name,b.Lexing.pos_lnum,e.Lexing.pos_lnum, - !nb,Worker_interface.Used) + (r.name,b.Lexing.pos_lnum,e.Lexing.pos_lnum,!nb, + Worker_interface.Used) :: acc ) tbl [] in - (* returns a records with compatible worker_interface fields *) { Worker_interface.worker_id = worker_id; diff --git a/src/bin/text/main_text.ml b/src/bin/text/main_text.ml index 708c4eef1..2aee75f14 100644 --- a/src/bin/text/main_text.ml +++ b/src/bin/text/main_text.ml @@ -40,6 +40,7 @@ let parse_cmdline () = try Parse_command.parse_cmdline_arguments () with Parse_command.Exit_parse_command i -> exit i + let () = register_input (); parse_cmdline (); diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index 8de0f2c4d..608541ba6 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -161,24 +161,42 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct | Some SAT.ProofSearch -> "ProofSearch" | Some SAT.ModelGen -> "ModelGen" - let print_model env timeout = - if Options.(get_interpretation () && get_dump_models ()) then begin - let s = timeout_reason_to_string timeout in + (* TODO: This function is a temporary fix. Printing Models + should be done in the binary part of AE and will be done after + merging OptimAE. *) + let print_model_aux mdl timeout = + let s = timeout_reason_to_string timeout in + Printer.print_fmt + (Options.Output.get_fmt_diagnostic ()) + "@[; Returned timeout reason = %s@]" s; + Models.output_concrete_model ~pp_prop_model:false + (Options.Output.get_fmt_models ()) mdl + + let print_model ?(all_sat=false) env timeout = + let pp_prop_model = all_sat || Options.get_show_prop_model () in + if Options.(get_interpretation () + && (get_dump_models () || pp_prop_model)) then begin match SAT.get_model env with | None -> + let s = timeout_reason_to_string timeout in Printer.print_fmt (Options.Output.get_fmt_diagnostic ()) "@[It seems that no model has been computed so \ far. You may need to change your model generation strategy \ or to increase your timeouts. Returned timeout reason = %s@]" s - | Some (lazy model) -> - Printer.print_fmt - (Options.Output.get_fmt_diagnostic ()) - "@[; Returned timeout reason = %s@]" s; - Models.output_concrete_model (Options.Output.get_fmt_models ()) model + | Some (lazy mdl) -> + print_model_aux mdl timeout end - let process_decl print_status used_context consistent_dep_stack + let filter_by_all_sat propositional filter = + if filter == E.Set.empty then propositional + else + E.Set.filter + (fun t -> + E.Set.mem t filter || E.Set.mem (E.neg t) filter + )propositional + + let rec process_decl print_status used_context consistent_dep_stack ((env, consistent, dep) as acc) d = try match d.st_decl with @@ -269,9 +287,10 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct | SAT.Sat t -> (* This case should mainly occur when a query has a non-unsat result, so we want to print the status in this case. *) - print_status (Sat (d,t)) (Steps.get_steps ()); - print_model env (Some SAT.NoTimeout); - env, `Sat t, dep + process_unknown + print_status used_context consistent_dep_stack + t t dep d SAT.NoTimeout + | SAT.Unsat dep' -> (* This case should mainly occur when a new assumption results in an unsat env, in which case we do not want to print status, since the correct @@ -280,6 +299,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct if get_debug_unsat_core () then check_produced_unsat_core dep; (* print_status (Inconsistent d) (Steps.get_steps ()); *) env , `Unsat, dep + | SAT.I_dont_know {env = t; timeout} -> (* TODO: always print Unknown for why3 ? *) let status = @@ -287,18 +307,112 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct else (Unknown (d, t)) in print_status status (Steps.get_steps ()); - print_model t (Some timeout); - (* TODO: Is it an appropriate behaviour? *) - (* if timeout != NoTimeout then raise Util.Timeout; *) - env, `Unknown t, dep + process_unknown + print_status used_context consistent_dep_stack + env t dep d timeout | Util.Timeout as e -> (* In this case, we obviously want to print the status, since we exit right after *) print_status (Timeout (Some d)) (Steps.get_steps ()); - print_model env None; + (* dont call 'process_unknown' in this case. Timeout stops + all-models listing *) + (* print_model (SAT.get_model env) None; *) raise e + and process_unknown + print_status used_context consistent_dep_stack env t dep d + timeout_kind = + match d.st_decl with + | Assume _ | PredDef _ | RwtDef _ | Push _ | Pop _ | ThAssume _-> + (* cannot raise Sat or Unknown in this case *) + assert false + + | Query (n, _, sort) -> + (* 1. check if we are in all-sat mode, and build the filter + that'll be applied on the boolean model *) + let all_sat_mode = + match sort with + | AllSat l -> + (* 1.A SMT command check-all-sat *) + Some (List.fold_left + (fun acc s -> + (*transform string to propositional vars (E.t)*) + let t = E.mk_term (Symbols.name s) [] Ty.Tbool in + E.Set.add t acc + )E.Set.empty l) + + | Thm | Sat -> + (* 1.B if user rather set option --all-models: empty + filter. Otherwise, all_sat_mode = None *) + if Options.get_all_models () then Some E.Set.empty + else None + + | Cut | Check -> + (* 1.3 all_sat_mode = None for cut and check *) + None + in + let m = match SAT.get_model env with + | None -> + if all_sat_mode != None then + (* all-sat enabled but interpretation disabled. No timeout + here! Return a model with just the propositional part + *) + Some (lazy { + Models.propositional = SAT.get_propositional_model env; + constants = ModelMap.empty; + functions = ModelMap.empty; + arrays = ModelMap.empty; + }) + else + None + | Some _ as md -> md + in + match m, all_sat_mode with + | Some m, Some filter -> + (* 1. case where all-bool-models wrt. given filter is + requested *) + let m = Lazy.force m in + let propositional = filter_by_all_sat m.propositional filter in + let m = { m with propositional } in + print_model_aux m (Some timeout_kind); + (* we build the conjunction that corresponds to the current + filtered model *) + let f = + Expr.Set.fold + (fun e acc -> E.mk_and e acc false) propositional E.vrai + in + if E.equal f E.vrai then + begin + (* this may happen if current propositional model is empty + (for instance, in case of timeout and no model computed + so far). We should stop to avoid infinite loop *) + if timeout_kind != NoTimeout then raise Util.Timeout; + (* TODO: is it the appropriate status? *) + env , `Unknown t, dep + end + else + (* we negate and propagate the current filtered boolean model + to force the SAT to explore other branches *) + let d = { d with st_decl = Query (n, E.neg f, sort) } in + (* re-set timelimit *) + Options.Time.set_timeout (Options.get_timelimit ()); + let env = SAT.reset_last_saved_model env in + (* TODO: The last call of process_decl will produce a + unexpected `unsat` as we have excludes all the possible + propositional model. We can fix it easily as soon as we + prevent process_decl to print itself results. *) + process_decl + print_status used_context consistent_dep_stack + (env, `Unknown t, dep) d + + | _ -> + (* 2. default case + case where a simple interpretation is + requested *) + print_model t (Some timeout_kind); + (* TODO: is it the appropriate status? *) + env , `Unknown t, dep + let print_status status steps = let check_status_consistency s = let known_status = get_status () in @@ -374,10 +488,6 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct (Some time) (Some steps) - - - - let init_with_replay_used acc f = assert (Sys.file_exists f); let cin = open_in f in diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index 8d5e315fd..1c78b0b5e 100644 --- a/src/lib/frontend/models.ml +++ b/src/lib/frontend/models.ml @@ -490,7 +490,7 @@ let rec pp_value ppk ppf = function let pp_constant ppf (_sy, t) = Fmt.pf ppf "%a" SmtlibCounterExample.pp_abstract_value_of_type t -let output_concrete_model fmt m = +let output_concrete_model ~pp_prop_model:_ fmt m = SmtlibCounterExample.reset_counter (); if ModelMap.(is_suspicious m.functions || is_suspicious m.constants || is_suspicious m.arrays) then @@ -543,4 +543,4 @@ let output_concrete_model fmt m = (* Arrays *) (* SmtlibCounterExample.output_arrays_counterexample fmt m.arrays; *) - Printer.print_fmt fmt "@]@,)"; + Printer.print_fmt fmt "@]@,)" diff --git a/src/lib/frontend/models.mli b/src/lib/frontend/models.mli index 3120efa18..4d1724dbe 100644 --- a/src/lib/frontend/models.mli +++ b/src/lib/frontend/models.mli @@ -37,6 +37,6 @@ type t = { arrays : ModelMap.t; } -val output_concrete_model : t Fmt.t +val output_concrete_model : pp_prop_model:bool -> t Fmt.t (** [output_concrete_model ppf mdl] prints the model [mdl] on the formatter [ppf]. *) diff --git a/src/lib/frontend/parsed_interface.ml b/src/lib/frontend/parsed_interface.ml index 8e831e4b5..2f5f2b199 100644 --- a/src/lib/frontend/parsed_interface.ml +++ b/src/lib/frontend/parsed_interface.ml @@ -92,6 +92,9 @@ let mk_goal loc name expr = let mk_check_sat loc name expr = Check_sat (loc, name, expr) +let mk_check_all_sat loc name llexpr = + Check_all_sat (loc, name, llexpr) + (** Declaration of theories, generic axioms and rewriting rules **) let mk_theory loc name ext expr = diff --git a/src/lib/frontend/parsed_interface.mli b/src/lib/frontend/parsed_interface.mli index 3b1f965a1..dd3239b6d 100644 --- a/src/lib/frontend/parsed_interface.mli +++ b/src/lib/frontend/parsed_interface.mli @@ -79,6 +79,8 @@ val mk_goal : Loc.t -> string -> lexpr -> decl val mk_check_sat : Loc.t -> string -> lexpr -> decl +val mk_check_all_sat : Loc.t -> string -> string list -> decl + (** Declaration of theories, generic axioms and rewriting rules **) val mk_theory : Loc.t -> string -> string -> decl list -> decl diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml index 7caf6d2c4..8f2637f7f 100644 --- a/src/lib/frontend/typechecker.ml +++ b/src/lib/frontend/typechecker.ml @@ -2213,6 +2213,7 @@ let type_one_th_decl env e = | Rewriting(loc, _, _) | Goal(loc, _, _) | Check_sat(loc, _, _) + | Check_all_sat(loc, _, _) | Predicate_def(loc,_,_,_) | Function_def(loc,_,_,_,_) | MutRecDefs ((loc,_,_,_,_) :: _) @@ -2370,12 +2371,10 @@ let type_user_defined_type_body ~is_recursive env acc (loc, ls, s, body) = let declare_fun env loc n ?(defined=false) ?ret_ty l = check_duplicate_params l; let infix, ty = - let l = List.map (fun (_,_,x) -> x) l in + let l = List.map (fun (_ ,_ , x) -> x) l in match ret_ty with - | None | Some PPTbool -> - PPiff, PPredicate l - | Some ty -> - PPeq, PFunction(l,ty) + | None | Some PPTbool -> PPiff, PPredicate l + | Some ty -> PPeq, PFunction(l,ty) in let mk_symb hs = Symbols.name hs ~defined ~kind:Symbols.Other in let tlogic, env = Env.add_logics env mk_symb [n] ty loc in (* TODO *) @@ -2503,6 +2502,14 @@ let rec type_decl (acc, env) d assertion_stack = | Function_def(loc,n,l,ret_ty,e) -> type_fun (acc, env) loc n l ~ret_ty e + | Check_all_sat(loc, n, l) -> + Options.tool_req 1 "TR-Typing-CheckAllSatDecl$_F$"; + let f = { pp_loc = loc; pp_desc = PPconst ConstFalse} in + List.iter (fun s -> + ignore (type_form env {pp_desc = PPapp(s,[]); pp_loc = loc}) + ) l; + type_and_intro_goal acc env (AllSat l) n f, env + | TypeDecl [] -> assert false diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 19ad29cb2..78efd9e30 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -1676,7 +1676,21 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct ~elt:() ~init:env + (* in case of all-models and/or call to solver with old + unbacktracked decisions *) + let check_no_decision_in_env env = + if env.dlevel > 0 then + Errors.run_error + (Errors.Unsupported_feature + "Some of the enabled features are not provided by the \ + Fun_SAT solver. Please consider switching to \ + CDCL(Tableaux) instead." + ) + let unsat env gf = + (* in case of all-models and/or call to solver with old + unbacktracked decisions *) + check_no_decision_in_env env; Debug.is_it_unsat gf; try let guards_to_assume = @@ -1752,6 +1766,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct {gf with E.ff = E.mk_imp current_guard gf.E.ff} let assume env fg dep = + (* in case of all-models and/or call to solver with old + unbacktracked decisions *) + check_no_decision_in_env env; try if Options.get_tableaux_cdcl () then cdcl_assume false env [add_guard env fg,dep]; @@ -1883,4 +1900,10 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct Shostak.Combine.save_cache (); Uf.save_cache () + let get_propositional_model env = + ME.fold (fun f _ acc -> E.Set.add f acc) env.gamma E.Set.empty + + let reset_last_saved_model env = + { env with last_saved_model = ref None} + end diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml index 0c10a0d49..ab2bf3d8e 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/src/lib/reasoners/sat_solver_sig.ml @@ -82,6 +82,12 @@ module type S = sig (** [get_model t] produces the current model. *) val get_model: t -> Models.t Lazy.t option + (** returns the latest solver's boolean assignation for literals + that is validated by the theories *) + val get_propositional_model: t -> Expr.Set.t + + (** reset last saved model, if any *) + val reset_last_saved_model: t -> t end diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli index 611b6034d..f25137ed8 100644 --- a/src/lib/reasoners/sat_solver_sig.mli +++ b/src/lib/reasoners/sat_solver_sig.mli @@ -83,6 +83,12 @@ module type S = sig (** [get_model t] produces the current model. *) val get_model: t -> Models.t Lazy.t option + (** returns the latest solver's boolean assignation for literals + that is validated by the theories *) + val get_propositional_model: t -> Expr.Set.t + + (** reset last saved model, if any *) + val reset_last_saved_model: t -> t end diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 9348554f8..b668eded7 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1182,6 +1182,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct (E.max_ground_terms_rec_of_form gf.E.ff) gf} in try + SAT.cancel_until env.satml 0; assert (SAT.decision_level env.satml == 0); let env, _updated = assume_aux ~dec_lvl:0 env [gf] in let max_t = max_term_depth_in_sat env in @@ -1247,6 +1248,13 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let get_model env = !(env.last_saved_model) + let get_propositional_model env = + let tbox = SAT.current_tbox env.satml in + Th.get_assumed tbox + + let reset_last_saved_model env = + { env with last_saved_model = ref None} + let reinit_ctx () = Steps.reinit_steps (); Th.reinit_cpt (); diff --git a/src/lib/structures/parsed.ml b/src/lib/structures/parsed.ml index 3fe8f12ed..e679393d0 100644 --- a/src/lib/structures/parsed.ml +++ b/src/lib/structures/parsed.ml @@ -263,6 +263,7 @@ type decl = | Rewriting of Loc.t * string * lexpr list | Goal of Loc.t * string * lexpr | Check_sat of Loc.t * string * lexpr + | Check_all_sat of Loc.t * string * string list | Logic of Loc.t * Symbols.name_kind * (string * string) list * plogic_type | Predicate_def of Loc.t * (string * string) * diff --git a/src/lib/structures/parsed.mli b/src/lib/structures/parsed.mli index aa2e14a4d..da0bd0a6d 100644 --- a/src/lib/structures/parsed.mli +++ b/src/lib/structures/parsed.mli @@ -124,6 +124,7 @@ type decl = | Rewriting of Loc.t * string * lexpr list | Goal of Loc.t * string * lexpr | Check_sat of Loc.t * string * lexpr + | Check_all_sat of Loc.t * string * string list | Logic of Loc.t * Symbols.name_kind * (string * string) list * plogic_type | Predicate_def of Loc.t * (string * string) * diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml index d43bef972..c0a6fc9ad 100644 --- a/src/lib/structures/ty.ml +++ b/src/lib/structures/ty.ml @@ -706,13 +706,14 @@ let print_full = (** Goal sort *) -type goal_sort = Cut | Check | Thm | Sat +type goal_sort = Cut | Check | Thm | Sat | AllSat of string list let print_goal_sort fmt = function | Cut -> Format.fprintf fmt "cut" | Check -> Format.fprintf fmt "check" | Thm -> Format.fprintf fmt "thm" | Sat -> Format.fprintf fmt "sat" + | AllSat _ -> Format.fprintf fmt "all-sat" let fresh_hypothesis_name = let cpt = ref 0 in diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli index 895bac4e2..db36dbefd 100644 --- a/src/lib/structures/ty.mli +++ b/src/lib/structures/ty.mli @@ -286,6 +286,9 @@ type goal_sort = (** The goal to be proved valid *) | Sat (** The goal to be proved satisfiable *) + | AllSat of string list + (** Rather generate all models involving the given list of + propositional variables *) (** Goal sort. Used in typed declarations. *) val fresh_hypothesis_name : goal_sort -> string diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index 8895a8809..1964a104a 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -340,6 +340,8 @@ let get_timelimit_per_goal () = !timelimit_per_goal let interpretation = ref INone let dump_models = ref false let interpretation_use_underscore = ref false +let all_models = ref false +let show_prop_model = ref false let output_format = ref Native let model_type = ref Value let infer_output_format = ref true @@ -348,6 +350,8 @@ let unsat_core = ref false let set_interpretation b = interpretation := b let set_dump_models b = dump_models := b let set_interpretation_use_underscore b = interpretation_use_underscore := b +let set_all_models b = all_models := b +let set_show_prop_model b = show_prop_model := b let set_output_format b = output_format := b let set_model_type t = model_type := t let set_infer_output_format b = infer_output_format := b @@ -385,6 +389,8 @@ let get_first_interpretation () = equal_mode !interpretation IFirst let get_every_interpretation () = equal_mode !interpretation IEvery let get_last_interpretation () = equal_mode !interpretation ILast let get_interpretation_use_underscore () = !interpretation_use_underscore +let get_all_models () = !all_models +let get_show_prop_model () = !show_prop_model let get_output_format () = !output_format let get_output_smtlib () = equal_output_format !output_format Smtlib2 let get_model_type () = !model_type diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index f146f33d0..be92c5629 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -222,6 +222,14 @@ val set_dump_models : bool -> unit {!val:get_interpretation_use_underscore} *) val set_interpretation_use_underscore : bool -> unit +(** Set [all_models] accessible with + {!val:get_all_models} *) +val set_all_models : bool -> unit + +(** Set [show_prop_model] accessible with + {!val:get_show_prop_model} *) +val set_show_prop_model : bool -> unit + (** Set [max_split] accessible with {!val:get_max_split} *) val set_max_split : Numbers.Q.t -> unit @@ -734,6 +742,16 @@ val get_last_interpretation : unit -> bool val get_interpretation_use_underscore : unit -> bool (** Default to [false] *) +(** [true] if the all_models flag is set to generate all propositional + models *) +val get_all_models : unit -> bool +(** Default to [false] *) + +(** [true] if the show_prop_model flag is set to also output the + propositional model, when a model is requested *) +val get_show_prop_model : unit -> bool +(** Default to [false] *) + (** Value specifying the default output format. possible values are {ul {- native} {- smtlib2} {- why3}} . *) diff --git a/src/parsers/psmt2_to_alt_ergo.ml b/src/parsers/psmt2_to_alt_ergo.ml index b43390874..e654d7090 100644 --- a/src/parsers/psmt2_to_alt_ergo.ml +++ b/src/parsers/psmt2_to_alt_ergo.ml @@ -390,6 +390,13 @@ module Translate = struct let count_goals = ref 0 + let translate_check_all_sat command l = + let loc = pos command in + incr count_goals; + let gname = "g_" ^ (string_of_int !count_goals) in + let l = List.rev_map (fun symb -> symb.c) (List.rev l) in + mk_check_all_sat loc gname l + let translate_check_sat command l = let loc = pos command in incr count_goals; @@ -413,6 +420,8 @@ module Translate = struct (translate_check_sat command []) :: acc | Cmd_CheckSatAssum l -> (translate_check_sat command l) :: acc + | Cmd_CheckAllSat l -> + (translate_check_all_sat command l) :: acc | Cmd_DeclareConst(symbol,const_dec) -> (translate_decl_fun symbol [] (translate_const_dec const_dec)) :: acc | Cmd_DeclareDataType(symbol,datatype_dec) -> @@ -452,7 +461,6 @@ module Translate = struct | Cmd_SetInfo _ -> not_supported "set-info"; acc | Cmd_Push n -> translate_push_pop mk_push n (pos command) :: acc | Cmd_Pop n -> translate_push_pop mk_pop n (pos command) :: acc - | Cmd_CheckAllSat _ -> not_supported "check-all-sat"; acc | Cmd_Maximize _ -> not_supported "maximize"; acc | Cmd_Minimize _ -> not_supported "minimize"; acc | Cmd_Exit -> acc