diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index 5e799b7df0..1b5103aa73 100644 --- a/src/bin/common/parse_command.ml +++ b/src/bin/common/parse_command.ml @@ -303,7 +303,7 @@ let mk_context_opt replay replay_all_used_context replay_used_context let mk_execution_opt input_format parse_only () preludes no_locs_in_answers colors_in_output no_headers_in_output no_formatting_in_output no_forced_flush_in_output pretty_output - type_only type_smt2 + type_only type_smt2 imperative_mode = let answers_with_loc = not no_locs_in_answers in let output_with_colors = colors_in_output || pretty_output in @@ -321,6 +321,7 @@ let mk_execution_opt input_format parse_only () set_type_only type_only; set_type_smt2 type_smt2; set_preludes preludes; + set_imperative_mode imperative_mode; `Ok() let mk_internal_opt @@ -744,12 +745,15 @@ let parse_execution_opt = let doc = "Stop after SMT2 typing." in Arg.(value & flag & info ["type-smt2"] ~docs ~doc) in + let imperative_smt = + let doc = "Starts Alt-Ergo in incremental mode" in + Arg.(value & flag & info ["incremental-mode"] ~docs ~doc) in Term.(ret (const mk_execution_opt $ input_format $ parse_only $ parsers $ preludes $ no_locs_in_answers $ colors_in_output $ no_headers_in_output $ no_formatting_in_output $ no_forced_flush_in_output $ - pretty_output $ type_only $ type_smt2 + pretty_output $ type_only $ type_smt2 $ imperative_smt )) let parse_halt_opt = diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index cfd5dea0dc..521ce58ccc 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -104,7 +104,7 @@ let cmd_on_modes st modes cmd = Errors.forbidden_command curr_mode cmd end -(* Dolmen util *) +(* Dolmen helpers *) (** Adds the named terms of the statement [stmt] to the map accumulator [acc] *) let add_if_named @@ -121,16 +121,69 @@ let add_if_named names. *) acc +type stmt = Typer_Pipe.typechecked D_loop.Typer_Pipe.stmt + +(** Translates dolmen locs to Alt-Ergo's locs *) +let dl_to_ael dloc_file (compact_loc: DStd.Loc.t) = + DStd.Loc.(lexing_positions (loc dloc_file compact_loc)) + (* We currently use the full state of the solver as model. *) type model = Model : 'a sat_module * 'a -> model type solve_res = | Sat of model | Unknown of model option - | Unsat + | Unsat of Explanation.t + +let check_sat_status () = + match Options.get_status () with + | Status_Unsat -> + recoverable_error + "This file is known to be Unsat but Alt-Ergo return Sat"; + | _ -> () + +let check_unsat_status () = + match Options.get_status () with + | Status_Unsat -> + recoverable_error + "This file is known to be Sat but Alt-Ergo return Unsat"; + | _ -> () + +let print_solve_res loc goal_name r = + let validity_mode = + match Options.get_output_format () with + | Smtlib2 -> false + | Native | Why3 | Unknown _ -> true + in + let time = O.Time.value () in + let steps = Steps.get_steps () in + match r with + | Sat _ -> + Printer.print_status_sat ~validity_mode + (Some loc) (Some time) (Some steps) (Some goal_name); + check_sat_status (); + | Unsat dep -> + Printer.print_status_unsat ~validity_mode + (Some loc) (Some time) (Some steps) (Some goal_name); + if O.get_unsat_core() && + not (O.get_debug_unsat_core()) && + not (O.get_save_used_context()) + then + Printer.print_fmt (Options.Output.get_fmt_regular ()) + "unsat-core:@,%a@." + (Explanation.print_unsat_core ~tab:true) dep; + check_unsat_status () + | Unknown _ -> + Printer.print_status_unknown ~validity_mode + (Some loc) (Some time) (Some steps) (Some goal_name); exception StopProcessDecl +(** Returns the value bound to the key in the state in argument: if it does not + exist, results default. *) +let state_get ~default key st = + try State.get key st with State.Key_not_found _ -> default + let main () = let () = Dolmen_loop.Code.init [] in @@ -199,7 +252,7 @@ let main () = end; Unknown (Some mdl) end - | `Unsat -> Unsat + | `Unsat -> Unsat ftdn_env.expl with Util.Timeout -> (* It is still necessary to leave this catch here, because we may trigger this exception in between calls of the sat solver. *) @@ -356,6 +409,48 @@ let main () = State.create_key ~pipe:"" "is_incremental" in + (* Set to true when a query is performed, states for the following SMT + instructions that they are working on an environment in which some formulae + have been decided and must be reverted back to the one before the check-sat + before starting to assert again. *) + let is_decision_env : bool State.key = + State.create_key ~pipe:"" "is_decision_env" + in + + (* Key used only in handle_stmt_pop_reinit, registers the commands executed + to save them them if a push command is executed. *) + let current_path_key : stmt list State.key = + State.create_key ~pipe:"" "current_path" + in + + (* Key used only in handle_stmt_pop_reinit, saves the commands executed + when a push is executed and replays them when a pop is met. *) + let pushed_paths_key : stmt list Vec.t State.key = + State.create_key ~pipe:"" "pushed_paths" + in + + (* Before each query, we push the current environment. This allows to keep a + fresh one for the next assertions. *) + let push_before_query st = + assert (not (State.get is_decision_env st)); + let module Api = (val (DO.SatSolverModule.get st)) in + Api.FE.push 1 Api.env; + State.set is_decision_env true st + in + + (* The pop corresponding to the previous push. It is applied everytime the + mode goes from Sat/Unsat to Assert. *) + let pop_if_post_query st = + if State.get is_decision_env st then + begin + let module Api = (val (DO.SatSolverModule.get st)) in + Api.FE.pop 1 Api.env; + State.set is_decision_env false st + end + else + st + in + let set_steps_bound i st = try DO.Steps.set i st with Invalid_argument _ -> (* Raised by Steps.set_steps_bound *) @@ -393,7 +488,10 @@ let main () = recoverable_error "%t" msg; st | Util.Timeout -> Printer.print_status_timeout None None None None; - exit_as_timeout () + if (not(Options.get_timelimit_per_goal ())) then + exit_as_timeout () + else + st | Errors.Error e -> recoverable_error "%a" Errors.report e; st @@ -425,7 +523,7 @@ let main () = in let set_partial_model_and_mode solve_res st = match solve_res with - | Unsat -> + | Unsat _ -> set_mode Unsat st | Unknown None -> set_mode Sat st @@ -520,6 +618,7 @@ let main () = |> State.set partial_model_key None |> State.set named_terms Util.MS.empty |> State.set incremental_depth 0 + |> State.set is_decision_env false |> DO.init |> State.init ~debug ~report_style ~reports ~max_warn ~time_limit ~size_limit ~response_file @@ -530,6 +629,20 @@ let main () = |> Typer_Pipe.init ~type_check in + (* Initializing hooks in the mode handler. + When we perform a check-sat, the environment we are working on is specific + to the Sat or Unsat mode we end up in. If we start asserting again, we must + do it in the previous environment. + *) + let init_full_incremental_hooks () = + DO.Mode.reset_hooks (); + DO.Mode.add_hook + (fun _ ~old:_ ~new_ st -> + match new_ with + | Assert -> pop_if_post_query st + | _ -> st + ) + in let print_wrn_opt ~name loc ty value = warning "%a The option %s expects a %s, got %a" @@ -688,61 +801,79 @@ let main () = unsupported_opt name; st in - let handle_optimize_stmt ~is_max loc id (term : DStd.Expr.Term.t) st = - let contents = `Optimize (term, is_max) in - let stmt = { Typer_Pipe.id; contents; loc; attrs = []; implicit = false } in - let cnf = - D_cnf.make (State.get State.logic_file st).loc - (State.get solver_ctx_key st).ctx stmt - in - (* Using both optimization and incremental mode may be wrong if - some optimization constraints aren't at the toplevel. - See issue: https://github.com/OCamlPro/alt-ergo/issues/993. *) + let handle_optimize_stmt ~is_max loc expr st = + let st = DO.Mode.set Assert st in + let module Api = (val (DO.SatSolverModule.get st)) in if State.get incremental_depth st > 0 then warning "Optimization constraints in presence of push \ and pop statements are not correctly processed."; - State.set solver_ctx_key ( - let solver_ctx = State.get solver_ctx_key st in - { solver_ctx with ctx = cnf } - ) st + let () = + if not @@ D_cnf.is_pure_term expr then + begin + recoverable_error + "the expression %a is not a valid objective function. \ + Only terms without let bindings or ite subterms can be optimized." + Expr.print expr + end + else + Api.FE.optimize ~loc (expr, is_max) Api.env + in st in let handle_get_objectives (_args : DStd.Expr.Term.t list) st = - let () = - if Options.get_interpretation () then - match State.get partial_model_key st with - | Some Model ((module SAT), partial_model) -> - let objectives = SAT.get_objectives partial_model in - begin - match objectives with - | Some o -> - if not @@ Objective.Model.has_no_limit o then - warning "Some objectives cannot be fulfilled"; - Objective.Model.pp (Options.Output.get_fmt_regular ()) o - | None -> - recoverable_error "No objective generated" - end - | None -> - recoverable_error - "Model generation is disabled (try --produce-models)" - in - st + if Options.get_interpretation () then + match State.get partial_model_key st with + | Some Model ((module SAT), partial_model) -> + let objectives = SAT.get_objectives partial_model in + begin + match objectives with + | Some o -> + if not @@ Objective.Model.has_no_limit o then + warning "Some objectives cannot be fulfilled"; + Objective.Model.pp (Options.Output.get_fmt_regular ()) o + | None -> + recoverable_error "No objective generated" + end + | None -> + recoverable_error + "Model generation is disabled (try --produce-models)" in let handle_custom_statement loc id args st = let args = List.map Dolmen_type.Core.Smtlib2.sexpr_as_term args in let logic_file = State.get State.logic_file st in let st, terms = Typer.terms st ~input:(`Logic logic_file) ~loc args in + let loc = + let dloc_file = (State.get State.logic_file st).loc in + dl_to_ael dloc_file loc + in match id, terms.ret with - | Dolmen.Std.Id.{name = Simple "minimize"; _}, [term] -> + | Dolmen.Std.Id.{name = Simple ("minimize" as name_base); _}, [term] -> cmd_on_modes st [Assert] "minimize"; - handle_optimize_stmt ~is_max:false loc id term st - | Dolmen.Std.Id.{name = Simple "maximize"; _}, [term] -> + let expr = + D_cnf.mk_expr + ~loc + ~name_base + ~toplevel:true + ~decl_kind:Expr.Dobjective + term + in + handle_optimize_stmt ~is_max:false loc expr st + | Dolmen.Std.Id.{name = Simple ("maximize" as name_base); _}, [term] -> cmd_on_modes st [Assert] "maximize"; - handle_optimize_stmt ~is_max:true loc id term st + let expr = + D_cnf.mk_expr + ~loc + ~name_base + ~toplevel:true + ~decl_kind:Expr.Dobjective + term + in + handle_optimize_stmt ~is_max:true loc expr st | Dolmen.Std.Id.{name = Simple "get-objectives"; _}, terms -> cmd_on_modes st [Sat] "get-objectives"; - handle_get_objectives terms st + handle_get_objectives terms st; + st | Dolmen.Std.Id.{name = Simple (("minimize" | "maximize") as ext); _}, _ -> recoverable_error "Statement %s only expects 1 argument (%i given)" @@ -840,79 +971,297 @@ let main () = assignments in - let handle_stmt : - Frontend.used_context -> State.t -> - 'a D_loop.Typer_Pipe.stmt -> State.t = + (* Copied from D_cnf, this treats the `Hyp case. *) + let assume_axiom st name t loc attrs : unit = + let module Api = (val (DO.SatSolverModule.get st)) in + let dloc_file = (State.get State.logic_file st).loc in + let dloc = DStd.Loc.loc dloc_file loc in + let aloc = DStd.Loc.lexing_positions dloc in + (* Dolmen adds information about theory extensions and case splits in the + [attrs] field of the parsed statements. [attrs] can be arbitrary terms, + where the information we care about is encoded as a [Colon]-list of + symbols. + + The few helper functions below are used to extract the information from + the [attrs]. More specifically: + + - "case split" statements have the [DStd.Id.case_split] symbol as an + attribute + + - Theory elements have a 3-length list of symbols as an attribute, of + the form [theory_decl; name; extends], where [theory_decl] is the + symbol [DStd.Id.theory_decl] and [name] and [extends] are the theory + extension name and the base theory name, respectively. + *) + let rec symbols = function + | DStd.Term. { term = Colon ({ term = Symbol sy; _ }, xs); _ } -> + Option.bind (symbols xs) @@ fun sys -> + Some (sy :: sys) + | { term = Symbol sy; _ } -> Some [sy] + | _ -> None + in + let sy_attrs = List.filter_map symbols attrs in + let is_case_split = + let is_case_split = function + | [ sy ] when DStd.Id.(equal sy case_split) -> true + | _ -> false + in + List.exists is_case_split sy_attrs + in + let theory = + let theory = + let open DStd.Id in + function + | [ td; name; extends] when DStd.Id.(equal td theory_decl) -> + let name = match name.name with + | Simple name -> name + | _ -> + Fmt.failwith + "Internal error: invalid theory extension: %a" + print name + in + let extends = match extends.name with + | Simple name -> + begin match Util.th_ext_of_string name with + | Some extends -> extends + | None -> + Errors.typing_error (ThExtError name) aloc + end + | _ -> + Fmt.failwith + "Internal error: invalid base theory name: %a" + print extends + in + Some (name, extends) + | _ -> None + in + match List.filter_map theory sy_attrs with + | [] -> None + | [name, extends] -> Some (name, extends) + | _ -> + Fmt.failwith + "%a: Internal error: multiple theories." + DStd.Loc.fmt dloc + in + let st_loc = dl_to_ael dloc_file loc in + match theory with + | Some (th_name, extends) -> + let axiom_kind = + if is_case_split then Util.Default else Util.Propagator + in + let e = D_cnf.make_form name t st_loc ~decl_kind:Expr.Dtheory in + let th_elt = { + Expr.th_name; + axiom_kind; + extends; + ax_form = e; + ax_name = name; + } in + Api.FE.th_assume ~loc:st_loc th_elt Api.env + | None -> + let e = D_cnf.make_form name t st_loc ~decl_kind:Expr.Daxiom in + Api.FE.assume ~loc:st_loc (name, e, true) Api.env + in + + (* Push the current environment and performs the query. + If an assertion is performed, we have to pop it back. This is handled by + the hook on D_state_option.Mode. *) + let handle_query st id loc attrs contents = + let module Api = (val (DO.SatSolverModule.get st)) in + let st_loc = + let file_loc = (State.get State.logic_file st).loc in + dl_to_ael file_loc loc + in + let name = + match id.DStd.Id.name with + | Simple name -> name + | Indexed _ | Qualified _ -> assert false + in + (* First, we check the environment if it already concluded. *) + let solve_res = + match Api.env.res with + | `Unsat -> Unsat Api.env.expl + | `Sat + | `Unknown -> + (* The environment did not conclude yet, or concluded with SAT. We + add additional constraints which may change this result. *) + begin + (* Preprocessing query. *) + let goal_sort = + match contents with + | `Goal _ -> Ty.Thm + | `Check _ -> Ty.Sat + in + let hyps, t = + match contents with + | `Goal t -> + D_cnf.pp_query t + | `Check hyps -> + D_cnf.pp_query ~hyps (DStd.Expr.Term.(of_cst Const._false)) + in + let () = + List.iter ( + fun t -> + let name = Ty.fresh_hypothesis_name goal_sort in + assume_axiom st name t loc attrs + ) hyps + in + let e = D_cnf.make_form "" t st_loc ~decl_kind:Expr.Dgoal in + (* Performing the query. *) + Api.FE.query ~loc:st_loc (name, e, goal_sort) Api.env; + (* Treatment of the result. *) + let partial_model = Api.env.sat_env in + (* If the status of the SAT environment is inconsistent, + we have to drop the partial model in order to prevent + printing wrong model. *) + match Api.env.res with + | `Sat -> + begin + let mdl = Model ((module Api.SAT), partial_model) in + let () = + if Options.(get_interpretation () && get_dump_models ()) then + Api.FE.print_model + (Options.Output.get_fmt_models ()) + partial_model + in + Sat mdl + end + | `Unknown -> + begin + let mdl = Model ((module Api.SAT), partial_model) in + if Options.(get_interpretation () && get_dump_models ()) then + begin + let ur = Api.SAT.get_unknown_reason partial_model in + Printer.print_fmt (Options.Output.get_fmt_diagnostic ()) + "@[Returned unknown reason = %a@]" + Sat_solver_sig.pp_ae_unknown_reason_opt ur; + Api.FE.print_model + (Options.Output.get_fmt_models ()) + partial_model + end; + Unknown (Some mdl) + end + | `Unsat -> Unsat Api.env.expl + end + in + (* Prints the result. *) + print_solve_res st_loc name solve_res; + (* Updates the dolmen state. *) + set_partial_model_and_mode solve_res st + in + + let handle_solve = let goal_cnt = ref 0 in - fun all_context st td -> + fun st id contents loc attrs -> + let module Api = (val DO.SatSolverModule.get st) in + let file_loc = (State.get State.logic_file st).loc in + let id = + match (State.get State.logic_file st).lang with + | Some (Smtlib2 _) -> + DStd.Id.mk DStd.Namespace.term @@ + "g_" ^ string_of_int (incr goal_cnt; !goal_cnt) + | _ -> id + in + let contents = + match contents with + | `Solve (hyps, []) -> `Check hyps + | `Solve ([], [t]) -> `Goal t + | _ -> + let loc = DStd.Loc.loc file_loc loc in + fatal_error "%a: internal error: unknown statement" + DStd.Loc.fmt loc + in + (* Performing the query *) + handle_query st id loc attrs contents + in + + (* TODO: reset options to their initial value. *) + let reset_state st = + st + |> State.set partial_model_key None + |> State.set solver_ctx_key empty_solver_ctx + |> State.set is_decision_env false + |> DO.Mode.clear + |> DO.Optimize.clear + |> DO.ProduceAssignment.clear + |> DO.init + |> State.set named_terms Util.MS.empty + in + + let handle_stmt_full_incremental : + Frontend.used_context -> + State.t -> + [< Typer_Pipe.typechecked | `Check of 'a ] D_loop.Typer_Pipe.stmt -> + State.t = + fun _all_context st td -> let file_loc = (State.get State.logic_file st).loc in - let solver_ctx = State.get solver_ctx_key st in match td with + (* Set logic *) | { contents = `Set_logic _; _} -> cmd_on_modes st [Start] "set-logic"; DO.Mode.set Util.Assert st + (* Goal definition *) + | { + id; loc; attrs; + contents = (`Goal _) as contents; + implicit = _; + } -> + (* In the non imperative mode, the Solve instruction is handled + differently (i.e. no pop/push). *) + assert (not (Options.get_imperative_mode ())); + cmd_on_modes st [Assert; Sat; Unsat] "goal"; + let st = pop_if_post_query st in + (* Pushing the environment once. This allows to keep a trace of the old + environment in case we want to assert afterwards. + The `pop` instruction is handled by the hook on the mode: when we + assert anything, we must make sure to go back to `Assert` mode. *) + let st = push_before_query st in + handle_query st id loc attrs contents + + (* Axiom definitions *) + | { id = DStd.Id.{name = Simple name; _}; contents = `Hyp t; loc; attrs; + implicit=_ } -> + let st = DO.Mode.set Util.Assert st in + assume_axiom st name t loc attrs; + st + + | { contents = `Defs defs; loc; _ } -> + let module Api = (val (DO.SatSolverModule.get st)) in + let st = DO.Mode.set Util.Assert st in + let loc = dl_to_ael file_loc loc in + let defs = D_cnf.make_defs defs loc in + let () = + List.iter + (function + | `Assume (name, e) -> Api.FE.assume ~loc (name, e, true) Api.env + | `PredDef (e, name) -> Api.FE.pred_def ~loc (name, e) Api.env + ) + defs + in + st + + | {contents = `Decls l; loc; _} -> + let st = DO.Mode.set Util.Assert st in + let decls = D_cnf.make_decls l in + let module Api = (val DO.SatSolverModule.get st) in + let loc = dl_to_ael file_loc loc in + List.iter (fun decl -> Api.FE.declare ~loc decl Api.env) decls; + st + (* When the next statement is a goal, the solver is called and provided the goal and the current context *) - | { id; contents = (`Solve _ as contents); loc ; attrs; implicit } -> - cmd_on_modes st [Assert; Sat; Unsat] "solve"; - let l = - solver_ctx.local @ - solver_ctx.global @ - solver_ctx.ctx - in - let id = - match (State.get State.logic_file st).lang with - | Some (Smtlib2 _) -> - DStd.Id.mk DStd.Namespace.term @@ - "g_" ^ string_of_int (incr goal_cnt; !goal_cnt) - | _ -> id - in - let name = - match id.name with - | Simple name -> name - | _ -> - let loc = DStd.Loc.loc file_loc loc in - Fmt.failwith "%a: internal error: goal name should be simple" - DStd.Loc.fmt loc - in - let contents = - match contents with - | `Solve (hyps, []) -> `Check hyps - | `Solve ([], [t]) -> `Goal t - | _ -> - let loc = DStd.Loc.loc file_loc loc in - Fmt.failwith "%a: internal error: unknown statement" - DStd.Loc.fmt loc - in - let stmt = { Typer_Pipe.id; contents; loc ; attrs; implicit } in - let cnf, is_thm = - match D_cnf.make (State.get State.logic_file st).loc l stmt with - | { Commands.st_decl = Query (_, _, kind); _ } as cnf :: hyps -> - let is_thm = - match kind with Ty.Thm | Sat -> true | _ -> false - in - List.rev (cnf :: hyps), is_thm - | _ -> assert false - in - let solve_res = - solve - (DO.SatSolverModule.get st) - 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 - |> set_partial_model_and_mode solve_res - else - State.set solver_ctx_key ( - let solver_ctx = State.get solver_ctx_key st in - { solver_ctx with local = [] } - ) st - |> set_partial_model_and_mode solve_res + | { id; contents = (`Solve _ as contents); loc ; attrs; implicit=_ } -> + (* In the non imperative mode, the Solve instruction is handled + differently (i.e. no pop/push). *) + assert (not (Options.get_imperative_mode ())); + cmd_on_modes st [Assert; Unsat; Sat] "check-sat"; + let st = pop_if_post_query st in + (* Pushing the environment once. This allows to keep a trace of the old + environment in case we want to assert afterwards. + The `pop` instruction is handled by the hook on the mode: when we + assert anything, we must make sure to go back to `Assert` mode. *) + let st = push_before_query st in + handle_solve st id contents loc attrs | {contents = `Set_option { DStd.Term.term = @@ -949,14 +1298,8 @@ let main () = end | {contents = `Reset; _} -> - st - |> State.set partial_model_key None - |> State.set solver_ctx_key empty_solver_ctx - |> DO.Mode.clear - |> DO.Optimize.clear - |> DO.ProduceAssignment.clear - |> DO.init - |> State.set named_terms Util.MS.empty + let () = Steps.reset_steps () in + reset_state st | {contents = `Exit; _} -> raise Exit @@ -996,43 +1339,221 @@ let main () = | {contents = `Other (custom, args); loc; _} -> handle_custom_statement loc custom args st + | {contents = `Pop n; loc; _} -> + let module Api = (val DO.SatSolverModule.get st) in + let dloc_file = (State.get State.logic_file st).loc in + Api.FE.pop ~loc:(dl_to_ael dloc_file loc) n Api.env; + st + |> State.set incremental_depth (State.get incremental_depth st - n) + |> set_mode Assert + + | {contents = `Push n; loc; _} -> + let module Api = (val DO.SatSolverModule.get st) in + let dloc_file = (State.get State.logic_file st).loc in + Api.FE.push ~loc:(dl_to_ael dloc_file loc) n Api.env; + st + |> State.set incremental_depth (State.get incremental_depth st + n) + |> set_mode Assert + | td -> - let st = - match td.contents with - | `Pop n -> - st - |> State.set incremental_depth (State.get incremental_depth st - n) - |> set_mode Assert - | `Push n -> - st - |> State.set incremental_depth (State.get incremental_depth st + n) - |> set_mode Assert - | _ -> st - in - (* TODO: - - Separate statements that should be ignored from unsupported - statements and throw exception or print a warning when an - unsupported statement is encountered. - *) - let cnf = - D_cnf.make (State.get State.logic_file st).loc - (State.get solver_ctx_key st).ctx td - in - State.set solver_ctx_key ( - let solver_ctx = State.get solver_ctx_key st in - { solver_ctx with ctx = cnf } - ) st + Printer.print_dbg ~header:true + "Ignoring statement: %a" Typer_Pipe.print td; + st in - let handle_stmts all_context st l = + + (* Handle each statement one after the other. + Still experimental due to push & pop issues. *) + let handle_stmts_full_incremental all_context st l = let rec aux named_map st = function | [] -> State.set named_terms named_map st | stmt :: tl -> - let st = handle_stmt all_context st stmt in + let st = handle_stmt_full_incremental all_context st stmt in let named_map = add_if_named ~acc:named_map stmt in aux named_map st tl in aux (State.get named_terms st) st l in + + let get_current_path = state_get ~default:[] current_path_key in + + let get_pushed_paths = + state_get ~default:(Vec.create ~dummy:[]) pushed_paths_key + in + + (* Same as handle_stmts_full_incremental, but removes pops and pushes. + Instead, every command that perform an effect on the environment + (definitions, assertion, resets, set option, ...) are stored in a list of + commands. When a (push n) is performed, this list is stored n times in a + Vec. When a pop m occurs, we reset the analysis, the Vec is popped m times + and the list of commands is replayed before continuing the analysis. + /!\ Pop do not reset options, so there may be inconstencies between a first + execution and a reinitialized one. The handle_reset function should handle + this, but it is not the case yet. *) + let handle_stmt_pop_reinit all_context st l = + + let has_timeout st = + let module Api = (val DO.SatSolverModule.get st) in + match Api.SAT.get_unknown_reason Api.env.sat_env with + | Some (Timeout _) -> true + | _ -> false + in + + (* Pushes n times the current path. *) + let push n st = + let current_path = get_current_path st in + let pushed_paths = get_pushed_paths st in + for _ = 0 to n - 1 do + Vec.push pushed_paths current_path + done + in + + (* Pops n times the current path and calls [replay] on the + list of instruction returned. *) + let pop n st replay = + let pushed_paths = get_pushed_paths st in + let rec pop_until until res = + if until = 0 then + res + else + pop_until (until - 1) (Vec.pop pushed_paths) + in + let rev_prefix = pop_until (n - 1) (Vec.pop pushed_paths) in + let st = reset_state st in + (* Part of the reset, the current path must be reinitialized as well. *) + let st = State.set current_path_key [] st in + replay st (List.rev rev_prefix) + in + + (* Before each query, we push the current environment. This allows to keep a + fresh one for the next assertions. *) + let push_before_query st = + assert (not (State.get is_decision_env st)); + push 1 st; + State.set is_decision_env true st + in + (* The pop corresponding to the previous push. It must be applied everytime + the mode goes from Sat/Unsat to Assert. *) + let rec pop_if_post_query st = + if State.get is_decision_env st + then pop 1 st (aux Util.MS.empty) + else st + and aux named_map st = function + | [] -> State.set named_terms named_map st + | (stmt: stmt) :: tl -> + begin + let current_path = get_current_path st in + match stmt with + | {contents = `Push n; _} -> + push n st; + let st = set_mode Assert st in + aux named_map st tl + | {contents = `Pop n; _} -> + let st = set_mode Assert st in + pop n st begin fun st prefix -> + let st = aux Util.MS.empty st prefix in + aux (State.get named_terms st) st tl + end + | { + id; loc; attrs; + contents = (`Goal _) as contents; + implicit = _; + } -> + cmd_on_modes st [Assert; Sat; Unsat] "goal"; + let st = pop_if_post_query st in + let st = push_before_query st in + let st = handle_query st id loc attrs contents in + let () = + if has_timeout st then + if Options.get_timelimit_per_goal () + then begin + Options.Time.start (); + Options.Time.set_timeout (Options.get_timelimit ()); + end + else exit_as_timeout () + in + st + | { + id; contents = (`Solve _ as contents); loc ; attrs; implicit=_ + } -> + cmd_on_modes st [Assert; Unsat; Sat] "check-sat"; + let st = pop_if_post_query st in + let st = push_before_query st in + let st = handle_solve st id contents loc attrs in + let () = + if has_timeout st then + if Options.get_timelimit_per_goal () + then begin + Options.Time.start (); + Options.Time.set_timeout (Options.get_timelimit ()); + end + else exit_as_timeout () + in + st + | {contents; _ } -> + let st = + let new_current_path = + match contents with + (* Treated above *) + | `Goal _ + | `Push _ + | `Pop _ + | `Solve (_, _) -> assert false + (* Statemets to keep *) + | `Clause _ + | `Decls _ + | `Defs _ + | `Exit (* This case should not happen.*) + | `Hyp _ + | `Reset + | `Reset_assertions + | `Set_info _ + | `Set_logic _ + | `Set_option _ -> stmt :: current_path + (* Statements to remove *) + | `Echo _ + | `Get_assertions + | `Get_info _ + | `Get_model + | `Get_option _ + | `Get_proof + | `Get_unsat_core + | `Get_value _ + | `Get_assignment + | `Get_unsat_assumptions -> current_path + (* Custom statement *) + | `Other (custom, _) -> + begin + match custom with + | {name = Simple ("minimize" | "maximize"); _} -> + stmt :: current_path + | _ -> current_path + end + in + State.set current_path_key new_current_path st + in + let st = handle_stmt_full_incremental all_context st stmt in + let named_map = add_if_named ~acc:named_map stmt in + aux named_map st tl + end + in + DO.Mode.reset_hooks (); + DO.Mode.add_hook + (fun _ ~old:_ ~new_ st -> + match new_ with + | Assert -> pop_if_post_query st + | _ -> st + ); + aux (State.get named_terms st) st l + in + let handle_stmts all_context st l = + begin + if Options.get_imperative_mode () + then + let () = init_full_incremental_hooks () in + handle_stmts_full_incremental + else handle_stmt_pop_reinit + end all_context st l + in let d_fe filename = let logic_file, st = mk_state filename in let () = diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index 2d45eb98c6..50e1e8eb47 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -176,6 +176,8 @@ type _ DStd.Builtin.t += | Integer_round | Abs_real | Sqrt_real + | Int2BV of int + | BV2Nat of int | Sqrt_real_default | Sqrt_real_excess | Ceiling_to_int of [ `Real ] @@ -211,7 +213,8 @@ let builtin_enum = function let add_cstrs map = List.fold_left (fun map ((c : DE.term_cst), _) -> let name = get_basename c.path in - DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } + DStd.Id.Map.add + { name = DStd.Name.simple name; ns = Term } (fun env _ -> builtin_term @@ Dolmen_type.Base.term_app_cst @@ -233,19 +236,63 @@ let fpa_rounding_mode, rounding_modes, add_rounding_modes = module Const = struct open DE + let bv2nat = + with_cache (fun n -> + let name = "bv2nat" in + Id.mk ~name ~builtin:(BV2Nat n) + (DStd.Path.global name) Ty.(arrow [bitv n] int)) + + let int2bv = + with_cache (fun n -> + let name = "int2bv" in + Id.mk ~name ~builtin:(Int2BV n) + (DStd.Path.global name) Ty.(arrow [int] (bitv n))) + let smt_round = with_cache (fun (n, m) -> let name = "ae.round" in - DE.Id.mk + Id.mk ~name ~builtin:(AERound (n, m)) (DStd.Path.global name) Ty.(arrow [fpa_rounding_mode; real] real)) end +let bv2nat t = + let n = + match DT.view (DE.Term.ty t) with + | `Bitv n -> n + | _ -> raise (DE.Term.Wrong_type (t, DT.bitv 0)) + in + DE.Term.apply_cst (Const.bv2nat n) [] [t] + +let int2bv n t = + DE.Term.apply_cst (Const.int2bv n) [] [t] + let smt_round n m rm t = DE.Term.apply_cst (Const.smt_round (n, m)) [] [rm; t] +let bv_builtins env s = + let term_app1 f = + Dl.Typer.T.builtin_term @@ + Dolmen_type.Base.term_app1 (module Dl.Typer.T) env s f + in + match s with + | Dl.Typer.T.Id { + ns = Term ; + name = Simple "bv2nat" } -> + term_app1 bv2nat + | Id { + ns = Term ; + name = Indexed { + basename = "int2bv" ; + indexes = [ n ] } } -> + begin match int_of_string n with + | n -> term_app1 (int2bv n) + | exception Failure _ -> `Not_found + end + | _ -> `Not_found + (** Takes a dolmen identifier [id] and injects it in Alt-Ergo's registered identifiers. It transforms "fpa_rounding_mode", the Alt-Ergo builtin type into the SMT2 @@ -447,17 +494,20 @@ let smt_fpa_builtins = end | _ -> `Not_found +(** Concatenation of builtins handlers. *) +let (++) bt1 bt2 = + fun a b -> + match bt1 a b with + | `Not_found -> bt2 a b + | res -> res + let builtins = fun _st (lang : Typer.lang) -> match lang with | `Logic Alt_ergo -> ae_fpa_builtins - | `Logic (Smtlib2 _) -> smt_fpa_builtins + | `Logic (Smtlib2 _) -> bv_builtins ++ smt_fpa_builtins | _ -> fun _ _ -> `Not_found -(** Translates dolmen locs to Alt-Ergo's locs *) -let dl_to_ael dloc_file (compact_loc: DStd.Loc.t) = - DStd.Loc.(lexing_positions (loc dloc_file compact_loc)) - (** clears the cache in the [Cache] module. *) let clear_cache () = Cache.clear () @@ -1407,8 +1457,8 @@ let rec mk_expr | Integer_round, _ -> op Integer_round | Abs_real, _ -> op Abs_real | Sqrt_real, _ -> op Sqrt_real - | B.Bitv_of_int { n }, _ -> op (Int2BV n) - | B.Bitv_to_nat { n = _ }, _ -> op BV2Nat + | Int2BV n, _ -> op (Int2BV n) + | BV2Nat _, _ -> op BV2Nat | Sqrt_real_default, _ -> op Sqrt_real_default | Sqrt_real_excess, _ -> op Sqrt_real_excess | B.Abs, _ -> op Abs_int @@ -1748,6 +1798,98 @@ let pp_query ?(hyps =[]) t = let axioms, goal = intro_hypothesis t in List.rev_append (List.rev_map (elim_toplevel_forall false) hyps) axioms, goal +let make_defs defs loc = + (* For a mutually recursive definition, we have to add all the function + names in a row. *) + List.iter (fun (def : Typer_Pipe.def) -> + match def with + | `Term_def (_, ({ path; _ } as tcst), _, _, _) -> + let name_base = get_basename path in + let sy = Sy.name ~defined:true name_base in + Cache.store_sy tcst sy + | `Type_alias _ -> () + | `Instanceof _ -> + (* These statements are only used in models when completing a + polymorphic partially-defined bulitin and should not end up + here. *) + assert false + ) defs; + List.filter_map (fun (def : Typer_Pipe.def) -> + match def with + | `Term_def ( _, ({ path; tags; _ } as tcst), tyvars, terml, body) -> + Cache.store_tyvl tyvars; + let name_base = get_basename path in + let binders_set, defn = + let rty = dty_to_ty body.term_ty in + let binders_set, rev_args = + List.fold_left ( + fun (binders_set, acc) (DE.{ path; id_ty; _ } as tv) -> + let ty = dty_to_ty id_ty in + let sy = Sy.var (Var.of_string (get_basename path)) in + Cache.store_sy tv sy; + let e = E.mk_term sy [] ty in + SE.add e binders_set, e :: acc + ) (SE.empty, []) terml + in + let sy = Cache.find_sy tcst in + let e = E.mk_term sy (List.rev rev_args) rty in + binders_set, e + in + begin match DStd.Tag.get tags DE.Tags.predicate with + | Some () -> + let decl_kind = E.Dpredicate defn in + let ff = + mk_expr ~loc ~name_base + ~toplevel:false ~decl_kind body + in + let qb = E.mk_eq ~iff:true defn ff in + let binders = E.mk_binders binders_set in + let ff = + E.mk_forall name_base Loc.dummy binders [] qb ~toplevel:true + ~decl_kind + in + assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty)); + let ff = E.purify_form ff in + let e = + if Ty.Svty.is_empty (E.free_type_vars ff) then ff + else + E.mk_forall name_base loc + Var.Map.empty [] ff ~toplevel:true ~decl_kind + in + Some (`PredDef (e, name_base)) + | None -> + let decl_kind = E.Dfunction defn in + let ff = + mk_expr ~loc ~name_base + ~toplevel:false ~decl_kind body + in + let iff = Ty.equal (Expr.type_info defn) (Ty.Tbool) in + let qb = E.mk_eq ~iff defn ff in + let binders = E.mk_binders binders_set in + let ff = + E.mk_forall name_base Loc.dummy binders [] qb ~toplevel:true + ~decl_kind + in + assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty)); + let ff = E.purify_form ff in + let e = + if Ty.Svty.is_empty (E.free_type_vars ff) then ff + else + E.mk_forall name_base loc + Var.Map.empty [] ff ~toplevel:true ~decl_kind + in + if Options.get_verbose () then + Format.eprintf "defining term of %a@." DE.Term.print body; + Some (`Assume (name_base, e)) + end + | `Type_alias _ -> None + | `Instanceof _ -> + (* These statements are only used in models when completing a + polymorphic partially-defined bulitin and should not end up + here. *) + assert false + ) defs + let make_form name_base f loc ~decl_kind = let ff = mk_expr ~loc ~name_base ~toplevel:true ~decl_kind f @@ -1758,6 +1900,43 @@ let make_form name_base f loc ~decl_kind = else E.mk_forall name_base loc Var.Map.empty [] ff ~toplevel:true ~decl_kind +let make_decls = function + | [] -> assert false (* We could probably just return (). *) + | [td] -> + begin + match td with + | `Type_decl (td, _def) -> mk_ty_decl td; [] + | `Term_decl td -> [mk_term_decl td]; + end + | dcl -> + let rec aux term_acc acc tdl = + (* for now, when acc has more than one element it is assumed that the + types are mutually recursive. Which is not necessarily the case. + But it doesn't affect the execution. + *) + match tdl with + | `Term_decl td :: tl -> + begin match acc with + | [] -> () + | [otd] -> mk_ty_decl otd + | _ -> mk_mr_ty_decls (List.rev acc) + end; + let t = mk_term_decl td in + aux (t :: term_acc) [] tl + + | `Type_decl (td, _def) :: tl -> + aux term_acc (td :: acc) tl + + | [] -> + begin match acc with + | [] -> () + | [otd] -> mk_ty_decl otd + | _ -> mk_mr_ty_decls (List.rev acc) + end; + term_acc + in + aux [] [] dcl + (* Helper function used to check if the expression defining an objective function is a pure term. *) let rec is_pure_term t = @@ -1766,333 +1945,3 @@ let rec is_pure_term t = | (Sy.Let | Lit _ | Form _) -> false | Sy.Op Tite -> false | _ -> List.for_all is_pure_term xs - -let make dloc_file acc stmt = - let rec aux acc (stmt: _ Typer_Pipe.stmt) = - match stmt with - (* Optimize terms *) - | { contents = `Optimize (t, is_max); loc; _ } -> - let st_loc = dl_to_ael dloc_file loc in - let e = - mk_expr ~loc:st_loc ~toplevel:true ~decl_kind:Dobjective t - in - if not @@ is_pure_term e then - begin - Printer.print_wrn - "the expression %a is not a valid objective function. \ - Only terms without let bindings or ite subterms can be optimized." - E.print e; - acc - end - else - let st_decl = C.Optimize (e, is_max) in - C.{ st_decl; st_loc } :: acc - - (* Push and Pop commands *) - | { contents = `Pop n; loc; _ } -> - let st_loc = dl_to_ael dloc_file loc in - let st_decl = C.Pop n in - C.{ st_decl; st_loc } :: acc - - | { contents = `Push n; loc; _ } -> - let st_loc = dl_to_ael dloc_file loc in - let st_decl = C.Push n in - C.{ st_decl; st_loc } :: acc - - (* Goal and check-sat definitions *) - | { - id; loc; attrs; - contents = (`Goal _ | `Check _) as contents; - implicit; - } -> - let name = - match id.name with - | Simple name -> name - | Indexed _ | Qualified _ -> assert false - in - let goal_sort = - match contents with - | `Goal _ -> Ty.Thm - | `Check _ -> Ty.Sat - in - let st_loc = dl_to_ael dloc_file loc in - let _hyps, t = - match contents with - | `Goal t -> - pp_query t - | `Check hyps -> - pp_query ~hyps (DStd.Expr.Term.(of_cst Const._false)) - in - let rev_hyps_c = - List.fold_left ( - fun acc t -> - let ns = DStd.Namespace.Decl in - let name = Ty.fresh_hypothesis_name goal_sort in - let decl: _ Typer_Pipe.stmt = { - id = DStd.Id.mk ns name; - contents = `Hyp t; loc; attrs; implicit - } - in - aux acc decl - ) [] _hyps - in - let e = make_form "" t st_loc ~decl_kind:E.Dgoal in - let st_decl = C.Query (name, e, goal_sort) in - C.{st_decl; st_loc} :: List.rev_append (List.rev rev_hyps_c) acc - - | { contents = `Solve _; _ } -> - (* Filtered out by the solving_loop *) - (* TODO: Remove them from the types *) - assert false - - (* Axiom definitions *) - | { id = DStd.Id.{name = Simple name; _}; contents = `Hyp t; loc; attrs; - implicit=_ } -> - let dloc = DStd.Loc.(loc dloc_file stmt.loc) in - let aloc = DStd.Loc.lexing_positions dloc in - (* Dolmen adds information about theory extensions and case splits in the - [attrs] field of the parsed statements. [attrs] can be arbitrary terms, - where the information we care about is encoded as a [Colon]-list of - symbols. - - The few helper functions below are used to extract the information from - the [attrs]. More specifically: - - - "case split" statements have the [DStd.Id.case_split] symbol as an - attribute - - - Theory elements have a 3-length list of symbols as an attribute, of - the form [theory_decl; name; extends], where [theory_decl] is the - symbol [DStd.Id.theory_decl] and [name] and [extends] are the theory - extension name and the base theory name, respectively. - *) - let rec symbols = function - | DStd.Term. { term = Colon ({ term = Symbol sy; _ }, xs); _ } -> - Option.bind (symbols xs) @@ fun sys -> - Some (sy :: sys) - | { term = Symbol sy; _ } -> Some [sy] - | _ -> None - in - let sy_attrs = List.filter_map symbols attrs in - let is_case_split = - let is_case_split = function - | [ sy ] when DStd.Id.(equal sy case_split) -> true - | _ -> false - in - List.exists is_case_split sy_attrs - in - let theory = - let theory = - let open DStd.Id in - function - | [ td; name; extends] when DStd.Id.(equal td theory_decl) -> - let name = match name.name with - | Simple name -> name - | _ -> - Fmt.failwith - "Internal error: invalid theory extension: %a" - print name - in - let extends = match extends.name with - | Simple name -> - begin match Util.th_ext_of_string name with - | Some extends -> extends - | None -> - Errors.typing_error (ThExtError name) aloc - end - | _ -> - Fmt.failwith - "Internal error: invalid base theory name: %a" - print extends - in - Some (name, extends) - | _ -> None - in - match List.filter_map theory sy_attrs with - | [] -> None - | [name, extends] -> Some (name, extends) - | _ -> - Fmt.failwith - "%a: Internal error: multiple theories." - DStd.Loc.fmt dloc - in - let decl_kind, assume = - match theory with - | Some (th_name, extends) -> - let axiom_kind = - if is_case_split then Util.Default else Util.Propagator - in - let th_assume name e = - let th_elt = { - Expr.th_name; - axiom_kind; - extends; - ax_form = e; - ax_name = name; - } in - C.ThAssume th_elt - in - E.Dtheory, th_assume - | None -> E.Daxiom, fun name e -> C.Assume (name, e, true) - in - let st_loc = dl_to_ael dloc_file loc in - let e = make_form name t st_loc ~decl_kind in - let st_decl = assume name e in - C.{ st_decl; st_loc } :: acc - - (* Function and predicate definitions *) - | { contents = `Defs defs; loc; _ } -> - (* For a mutually recursive definition, we have to add all the function - names in a row. *) - List.iter (fun (def : Typer_Pipe.def) -> - match def with - | `Term_def (_, ({ path; _ } as tcst), _, _, _) -> - let name_base = get_basename path in - let sy = Sy.name ~defined:true name_base in - Cache.store_sy tcst sy - | `Type_alias _ -> () - | `Instanceof _ -> - (* These statements are only used in models when completing a - polymorphic partially-defined bulitin and should not end up - here. *) - assert false - ) defs; - let append xs = List.append xs acc in - append @@ - List.filter_map (fun (def : Typer_Pipe.def) -> - match def with - | `Term_def ( _, ({ path; tags; _ } as tcst), tyvars, terml, body) -> - Cache.store_tyvl tyvars; - let st_loc = dl_to_ael dloc_file loc in - let name_base = get_basename path in - - let binders_set, defn = - let rty = dty_to_ty body.term_ty in - let binders_set, rev_args = - List.fold_left ( - fun (binders_set, acc) (DE.{ path; id_ty; _ } as tv) -> - let ty = dty_to_ty id_ty in - let sy = Sy.var (Var.of_string (get_basename path)) in - Cache.store_sy tv sy; - let e = E.mk_term sy [] ty in - SE.add e binders_set, e :: acc - ) (SE.empty, []) terml - in - let sy = Cache.find_sy tcst in - let e = E.mk_term sy (List.rev rev_args) rty in - binders_set, e - in - - let loc = st_loc in - - begin match DStd.Tag.get tags DE.Tags.predicate with - | Some () -> - let decl_kind = E.Dpredicate defn in - let ff = - mk_expr ~loc ~name_base - ~toplevel:false ~decl_kind body - in - let qb = E.mk_eq ~iff:true defn ff in - let binders = E.mk_binders binders_set in - let ff = - E.mk_forall name_base Loc.dummy binders [] qb ~toplevel:true - ~decl_kind - in - assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty)); - let ff = E.purify_form ff in - let e = - if Ty.Svty.is_empty (E.free_type_vars ff) then ff - else - E.mk_forall name_base loc - Var.Map.empty [] ff ~toplevel:true ~decl_kind - in - Some C.{ st_decl = C.PredDef (e, name_base); st_loc } - | None -> - let decl_kind = E.Dfunction defn in - let ff = - mk_expr ~loc ~name_base - ~toplevel:false ~decl_kind body - in - let iff = Ty.equal (Expr.type_info defn) (Ty.Tbool) in - let qb = E.mk_eq ~iff defn ff in - let binders = E.mk_binders binders_set in - let ff = - E.mk_forall name_base Loc.dummy binders [] qb ~toplevel:true - ~decl_kind - in - assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty)); - let ff = E.purify_form ff in - let e = - if Ty.Svty.is_empty (E.free_type_vars ff) then ff - else - E.mk_forall name_base loc - Var.Map.empty [] ff ~toplevel:true ~decl_kind - in - if Options.get_verbose () then - Format.eprintf "defining term of %a@." DE.Term.print body; - Some C.{ st_decl = C.Assume (name_base, e, true); st_loc } - end - | `Type_alias _ -> None - | `Instanceof _ -> - (* These statements are only used in models when completing a - polymorphic partially-defined bulitin and should not end up - here. *) - assert false - ) defs - - | {contents = `Decls [td]; loc; _ } -> - begin match td with - | `Type_decl (td, _def) -> - mk_ty_decl td; - acc - - | `Term_decl td -> - let st_loc = dl_to_ael dloc_file loc in - C.{ st_decl = Decl (mk_term_decl td); st_loc } :: acc - end - - | {contents = `Decls dcl; loc; _ } -> - let rec aux ty_decls tdl acc = - (* for now, when acc has more than one element it is assumed that the - types are mutually recursive. Which is not necessarily the case. - But it doesn't affect the execution. - *) - match tdl with - | `Term_decl td :: tl -> - begin match ty_decls with - | [] -> () - | [otd] -> mk_ty_decl otd - | _ -> mk_mr_ty_decls (List.rev ty_decls) - end; - let st_loc = dl_to_ael dloc_file loc in - C.{ st_decl = Decl (mk_term_decl td); st_loc } :: aux [] tl acc - - | `Type_decl (td, _def) :: tl -> - aux (td :: ty_decls) tl acc - - | [] -> - begin - let () = - match ty_decls with - | [] -> () - | [otd] -> mk_ty_decl otd - | _ -> mk_mr_ty_decls (List.rev ty_decls) - in - acc - end - in - aux [] dcl acc - - | { contents = `Set_logic _ | `Set_info _ | `Get_info _ ; _ } -> acc - - | { contents = #Typer_Pipe.typechecked; _ } as stmt -> - (* TODO: - - Separate statements that should be ignored from unsupported - statements and throw exception or print a warning when an unsupported - statement is encountered. - *) - Printer.print_dbg ~header:true - "Ignoring statement: %a" Typer_Pipe.print stmt; - acc - in - aux acc stmt diff --git a/src/lib/frontend/d_cnf.mli b/src/lib/frontend/d_cnf.mli index cdb65f51f5..21989426e0 100644 --- a/src/lib/frontend/d_cnf.mli +++ b/src/lib/frontend/d_cnf.mli @@ -44,6 +44,32 @@ val dty_to_ty : ?update:bool -> ?is_var:bool -> D_loop.DStd.Expr.ty -> Ty.t individually. *) +(** [make_defs dlist loc] + Transforms the dolmen definition list [dlist] into an Alt-Ergo definition. + Dolmen definitions can be: + - Definitions, that either are predicates (transformed in `PredDef) or + simple definitions (transformed in `Assume); + - Type aliases (filtered out); + - Statements used in models (they must not be in the input list, otherwise + this function fails). *) +val make_defs : + D_loop.Typer_Pipe.def list -> + Loc.t -> + [> `Assume of string * Expr.t | `PredDef of Expr.t * string ] list + +(** [make_expr ~loc ~name_base ~toplevel ~decl_kind term] + + Builds an Alt-Ergo hashconsed expression from a dolmen term +*) +val mk_expr : + ?loc:Loc.t -> + ?name_base:string -> + ?toplevel:bool -> + decl_kind:Expr.decl_kind -> D_loop.DStd.Expr.term -> Expr.t + +(** [make_form name term loc decl_kind] + Same as `make_expr`, but for formulas. It applies a purification step and + processes free variables by adding a forall quantifier. *) val make_form : string -> D_loop.DStd.Expr.term -> @@ -51,20 +77,34 @@ val make_form : decl_kind:Expr.decl_kind -> Expr.t -val make : - D_loop.DStd.Loc.file -> - Commands.sat_tdecl list -> - [< D_loop.Typer_Pipe.typechecked - | `Optimize of Dolmen.Std.Expr.term * bool - | `Goal of Dolmen.Std.Expr.term - | `Check of Dolmen.Std.Expr.term list - > `Hyp ] D_loop.Typer_Pipe.stmt -> - Commands.sat_tdecl list -(** [make acc stmt] Makes one or more [Commands.sat_tdecl] from the - type-checked statement [stmt] and appends them to [acc]. +(** Preprocesses the body of a goal by: + - removing the top-level universal quantifiers and considering their + quantified variables as uninsterpreted symbols. + - transforming a given formula: [a[1] -> a[2] -> ... -> a[n]] in which + the [a[i]]s are subformulas and [->] is a logical implication, to a set of + hypotheses [{a[1]; ...; a[n-1]}], and a goal [a[n]] whose validity is + verified by the solver. + If additional hypotheses are provided in [hyps], they are preprocessed and + added to the set of hypotheses in the same way as the left-hand side of + implications. In other words, [pp_query ~hyps:[h1; ...; hn] t] is the same + as [pp_query (h1 -> ... -> hn t)], but more convenient if the some + hypotheses are already separated from the goal. + Returns a list of hypotheses and the new goal body *) +val pp_query : + ?hyps:D_loop.DStd.Expr.term list -> + D_loop.DStd.Expr.term -> + D_loop.DStd.Expr.term list * D_loop.DStd.Expr.term + +(** Registers the declarations in the cache. If there are more than one element + in the list, it is assumed they are mutually recursive (but if it is not the + case, it still work). *) +val make_decls : + D_loop.Typer_Pipe.decl list -> (Hstring.t * Ty.t list * Ty.t) list val builtins : Dolmen_loop.State.t -> D_loop.Typer.lang -> Dolmen_loop.Typer.T.builtin_symbols + +val is_pure_term : Expr.t -> bool diff --git a/src/lib/frontend/d_state_option.ml b/src/lib/frontend/d_state_option.ml index 3c5d807c7d..7f1c4e6ec8 100644 --- a/src/lib/frontend/d_state_option.ml +++ b/src/lib/frontend/d_state_option.ml @@ -32,6 +32,13 @@ module O = Options module State = D_loop.State module Typer = D_loop.Typer +type 'a hook = + 'a D_loop.State.key -> + old:'a -> + new_:'a -> + D_loop.Typer.state -> + D_loop.Typer.state + module type Accessor = sig (** The data saved in the state. *) type t @@ -45,34 +52,66 @@ module type S = sig include Accessor (** Sets the option on the dolmen state. *) - val set : t -> D_loop.Typer.state -> D_loop.Typer.state + val set : t -> Typer.state -> Typer.state (** Clears the option from the state. *) - val clear : D_loop.Typer.state -> D_loop.Typer.state + val clear : Typer.state -> Typer.state +end + +module type S_with_hooks = sig + include S + + val reset_hooks : unit -> unit + + val add_hook : t hook -> unit end let create_opt (type t) - ?(on_update=(fun _ _ -> Fun.id)) + ?on_update (key : string) - (get : unit -> t) : (module S with type t = t) = + (default_get : unit -> t) : (module S_with_hooks with type t = t) = (module struct type nonrec t = t + let on_update_base = + match on_update with + | None -> [] + | Some f -> [f] + + let on_update_list = ref on_update_base + let key = State.create_key ~pipe:"" key - let set opt st = - st - |> on_update key opt - |> State.set key opt + let apply_hooks ~old ~new_ st = + List.fold_left + (fun acc f -> f key ~old ~new_ acc) + st + !on_update_list let unsafe_get st = State.get key st - let clear st = State.update_opt key (fun _ -> None) st - let get st = try unsafe_get st with - | State.Key_not_found _ -> get () + | State.Key_not_found _ -> default_get () + + let set new_ st = + let old = get st in + let st = apply_hooks ~old ~new_ st in + State.set key new_ st + + let clear st = + let old = get st in + let new_ = default_get () in + st + |> apply_hooks ~old ~new_ + |> State.update_opt key (fun _ -> None) + (* S: [clear] rebuilds a new default value for the hooks, but does not put + it back on the state. *) + + let reset_hooks () = on_update_list := on_update_base + + let add_hook h = on_update_list := h :: !on_update_list end) (* The current mode of the sat solver. Serves as a flag for some options that @@ -83,12 +122,12 @@ module Mode = (val (create_opt "start_mode") (fun _ -> Util.Start)) in start mode. *) let create_opt_only_start_mode (type t) - ?(on_update=(fun _ _ -> Fun.id)) + ?(on_update=(fun _ ~old:_ ~new_:_ -> Fun.id)) (key : string) - (get : unit -> t) : (module S with type t = t) = - let on_update k opt st = + (get : unit -> t) : (module S_with_hooks with type t = t) = + let on_update k ~old ~new_ st = match Mode.get st with - | Util.Start -> on_update k opt st + | Util.Start -> on_update k ~old ~new_ st | curr_mode -> Errors.invalid_set_option curr_mode key in create_opt ~on_update key get @@ -103,14 +142,28 @@ module Optimize = module ProduceAssignment = (val (create_opt_only_start_mode "produce_assignment" (fun _ -> false))) +module type Sat_solver_api = sig + module SAT : Sat_solver_sig.S + module FE : Frontend.S with type sat_env = SAT.t + + val env : FE.env +end + let get_sat_solver ?(sat = O.get_sat_solver ()) ?(no_th = O.get_no_theory ()) - () = + () : (module Sat_solver_api) = let module SatCont = (val (Sat_solver.get sat) : Sat_solver_sig.SatContainer) in let module TH = (val Sat_solver.get_theory ~no_th) in - (module SatCont.Make(TH) : Sat_solver_sig.S) + let module SAT : Sat_solver_sig.S = SatCont.Make(TH) in + let module FE : Frontend.S with type sat_env = SAT.t = Frontend.Make (SAT) in + (module struct + module SAT = SAT + module FE = FE + + let env = FE.init_env (Frontend.init_all_used_context ()) + end) module SatSolverModule = (val ( @@ -119,15 +172,15 @@ module SatSolverModule = (fun _ -> get_sat_solver ()))) let msatsolver = - let on_update _ sat st = - SatSolverModule.set (get_sat_solver ~sat ()) st + let on_update _ ~old:_ ~new_ st = + SatSolverModule.set (get_sat_solver ~sat:new_ ()) st in (create_opt_only_start_mode ~on_update "sat_solver" O.get_sat_solver) module SatSolver = (val msatsolver) let msteps = - let on_update _ sat st = Steps.set_steps_bound sat; st in + let on_update _ ~old:_ ~new_ st = Steps.set_steps_bound new_; st in (create_opt_only_start_mode ~on_update "steps_bound" O.get_steps_bound) module Steps = (val msteps) diff --git a/src/lib/frontend/d_state_option.mli b/src/lib/frontend/d_state_option.mli index 0d373c3c09..d0db1bd3de 100644 --- a/src/lib/frontend/d_state_option.mli +++ b/src/lib/frontend/d_state_option.mli @@ -32,6 +32,14 @@ an option that can be set, fetched et reset independently from the Options module, which is used as a static reference. *) +(** A hook which is called when an option is updated. *) +type 'a hook = + 'a D_loop.State.key -> + old:'a -> + new_:'a -> + D_loop.Typer.state -> + D_loop.Typer.state + module type Accessor = sig (** The data saved in the state. *) type t @@ -51,8 +59,18 @@ module type S = sig val clear : D_loop.Typer.state -> D_loop.Typer.state end +module type S_with_hooks = sig + include S + + (** Resets all hooks, except the one registered at initialization. *) + val reset_hooks : unit -> unit + + (** Adds a hook which is called during the update of the value. *) + val add_hook : t hook -> unit +end + (** The current mode of the solver. *) -module Mode : S with type t = Util.mode +module Mode : S_with_hooks with type t = Util.mode (** Options are divided in two categories: 1. options that can be updated anytime; @@ -71,9 +89,17 @@ module ProduceAssignment : S with type t = bool (** The Sat solver used. When set, updates the SatSolverModule defined below. *) module SatSolver : S with type t = Util.sat_solver +module type Sat_solver_api = sig + module SAT : Sat_solver_sig.S + + module FE : Frontend.S with type sat_env = SAT.t + + val env : FE.env +end + (** The Sat solver module used for the calculation. This option's value depends on SatSolver: when SatSolver is updated, this one also is. *) -module SatSolverModule : Accessor with type t = (module Sat_solver_sig.S) +module SatSolverModule : Accessor with type t = (module Sat_solver_api) (** Option for setting the max number of steps. Interfaces with the toplevel Steps module. diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index bf57385493..9bbc252d36 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -146,6 +146,8 @@ module type S = sig val init_env : ?sat_env:sat_env -> used_context -> env + val declare : Id.typed process + val push : int process val pop : int process @@ -239,6 +241,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct expl = Explanation.empty } + let set_result env res = env.res <- res + let output_used_context g_name dep = if not (Options.get_js_mode ()) then begin let f = Options.get_used_context_file () in @@ -322,7 +326,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct ~max:n ~elt:() ~init:(env.res, env.expl) in SAT.pop env.sat_env n; - env.res <- res; + set_result env res; env.expl <- expl let internal_assume @@ -389,7 +393,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct in if get_debug_unsat_core () then check_produced_unsat_core expl; if get_save_used_context () then output_used_context n expl; - env.res <- `Unsat; + set_result env `Unsat; env.expl <- expl let internal_th_assume @@ -420,12 +424,13 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct let handle_sat_exn f ?loc x env = try f ?loc x env with - | SAT.Sat -> env.res <- `Sat + | SAT.Sat -> set_result env `Sat | SAT.Unsat expl -> - env.res <- `Unsat; + set_result env `Unsat; env.expl <- Ex.union expl env.expl - | SAT.I_dont_know -> - env.res <- `Unknown + | SAT.I_dont_know -> set_result env `Unknown + | Util.Step_limit_reached _ -> set_result env `Unknown + (* The SAT.Timeout exception is not catched. *) (* Wraps the function f to check if the step limit is reached (in which case, don't do anything), and then calls the function & catches the @@ -433,6 +438,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct let wrap_f f ?loc x env = check_if_over (handle_sat_exn f ?loc x) env + let declare = wrap_f internal_decl + let push = wrap_f internal_push let pop = wrap_f internal_pop @@ -485,7 +492,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct (* This case should mainly occur when a query has a non-unsat result, so we want to print the status in this case. *) hook_on_status (Sat (d, env.sat_env)) (Steps.get_steps ()); - env.res <- `Sat + set_result env `Sat | SAT.Unsat expl' -> (* This case should mainly occur when a new assumption results in an unsat @@ -494,7 +501,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct let expl = Ex.union env.expl expl' in if get_debug_unsat_core () then check_produced_unsat_core expl; (* print_status (Inconsistent d) (Steps.get_steps ()); *) - env.res <- `Unsat; + set_result env `Unsat; env.expl <- expl | SAT.I_dont_know -> @@ -508,7 +515,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct hook_on_status status (Steps.get_steps ()); (* TODO: Is it an appropriate behaviour? *) (* if timeout != NoTimeout then raise Util.Timeout; *) - env.res <- `Unknown + set_result env `Unknown | Util.Timeout as e -> (* In this case, we obviously want to print the status, diff --git a/src/lib/frontend/frontend.mli b/src/lib/frontend/frontend.mli index a5606b1550..c0ad02e10c 100644 --- a/src/lib/frontend/frontend.mli +++ b/src/lib/frontend/frontend.mli @@ -70,6 +70,8 @@ module type S = sig the user. *) type 'a process = ?loc:Loc.t -> 'a -> env -> unit + val declare : Id.typed process + val push : int process val pop : int process diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 7ac10f3deb..22bd813d63 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -168,6 +168,7 @@ module Make (Th : Theory.S) = struct plevel : int; ilevel : int; tbox : Th.t; + tbox_stack: Th.t Stack.t; (* Pushed theory envs (TODO: pure version) *) unit_tbox : Th.t; (* theory env of facts at level 0 *) inst : Inst.t; heuristics : Heuristics.t ref; @@ -1625,13 +1626,15 @@ module Make (Th : Theory.S) = struct env let push env to_push = - if Options.get_tableaux_cdcl () then - Errors.run_error - (Errors.Unsupported_feature - "Incremental commands are not implemented in \ - Tableaux(CDCL) solver ! \ - Please use the Tableaux or CDLC SAT solvers instead" - ); + (* It does not work with Tableaux(CDCL); right now it is (unsoundly) + handled by fun_sat_frontend but we should fix it. *) + (* if Options.get_tableaux_cdcl () then + * Errors.run_error + * (Errors.Unsupported_feature + * "Incremental commands are not implemented in \ + * Tableaux(CDCL) solver ! \ + * Please use the Tableaux or CDLC SAT solvers instead" + * ); *) Util.loop ~f:(fun _n () acc -> let new_guard = E.fresh_name Ty.Tbool in @@ -1639,6 +1642,7 @@ module Make (Th : Theory.S) = struct let guards = ME.add new_guard (mk_gf new_guard "" true true,Ex.empty) acc.guards.guards in + Stack.push env.tbox env.tbox_stack; Stack.push !(env.declare_top) env.declare_tail; {acc with guards = { acc.guards with @@ -1651,13 +1655,15 @@ module Make (Th : Theory.S) = struct ~init:env let pop env to_pop = - if Options.get_tableaux_cdcl () then - Errors.run_error - (Errors.Unsupported_feature - "Incremental commands are not implemented in \ - Tableaux(CDCL) solver ! \ - Please use the Tableaux or CDLC SAT solvers instead" - ); + (* It does not work with Tableaux(CDCL); right now it is (unsoundly) + handled by fun_sat_frontend but we should fix it. *) + (* if Options.get_tableaux_cdcl () then + * Errors.run_error + * (Errors.Unsupported_feature + * "Incremental commands are not implemented in \ + * Tableaux(CDCL) solver ! \ + * Please use the Tableaux or CDLC SAT solvers instead" + * ); *) Util.loop ~f:(fun _n () acc -> let acc,guard_to_neg = restore_guards_and_refs acc in @@ -1668,6 +1674,18 @@ module Make (Th : Theory.S) = struct (mk_gf (E.neg guard_to_neg) "" true true,Ex.empty) acc.guards.guards in + let gamma = + (* If we made a check-sat and we want to work again on the + environment, we have to remove the guard from gamma. *) + match ME.find_opt guard_to_neg acc.gamma with + | None -> acc.gamma + | Some (_, _, dlvl, plvl) -> + ME.filter + (fun _ (_, _, dlvl', plvl') -> + not (dlvl = dlvl' && plvl' >= plvl)) + acc.gamma + in + let tbox = Stack.pop env.tbox_stack in acc.model_gen_phase := false; env.last_saved_model := None; let () = @@ -1680,7 +1698,10 @@ module Make (Th : Theory.S) = struct { acc.guards with current_guard = new_current_guard; guards = guards; - }}) + }; + gamma; + tbox; + }) ~max:to_pop ~elt:() ~init:env @@ -1832,6 +1853,7 @@ module Make (Th : Theory.S) = struct ilevel = 0; tbox = tbox; unit_tbox = tbox; + tbox_stack = Stack.create (); inst = inst; heuristics = ref (Heuristics.empty ()); model_gen_phase = ref false; diff --git a/src/lib/reasoners/fun_sat_frontend.ml b/src/lib/reasoners/fun_sat_frontend.ml index ef5c7e9217..9a22fa8a88 100644 --- a/src/lib/reasoners/fun_sat_frontend.ml +++ b/src/lib/reasoners/fun_sat_frontend.ml @@ -35,33 +35,70 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct module FS = Fun_sat.Make(Th) - type t = FS.t ref + type t = { + mutable fs_env: FS.t; + fs_env_stack: FS.t Stack.t + } - let empty ?selector () = ref (FS.empty ?selector ()) + let internal_empty fs_env = { + fs_env; + fs_env_stack = Stack.create () + } + + let empty ?selector () = internal_empty (FS.empty ?selector ()) let exn_handler f env = - try f !env with - | FS.Sat e -> env := e; raise Sat + try f env with + | FS.Sat e -> env.fs_env <- e; raise Sat | FS.Unsat expl -> raise (Unsat expl) - | FS.I_dont_know e -> env := e; raise I_dont_know - - let declare t id = - t := FS.declare !t id + | FS.I_dont_know e -> env.fs_env <- e; raise I_dont_know - let push t i = exn_handler (fun env -> t := FS.push env i) t - let pop t i = exn_handler (fun env -> t := FS.pop env i) t - - let assume t g expl = exn_handler (fun env -> t := FS.assume env g expl) t + let declare t id = + t.fs_env <- FS.declare t.fs_env id + + (* Push and pop are not implemented with get_tableaux_cdcl, so we have to + manually save and restore environments. *) + + let push_cdcl_tableaux t i = + assert (i > 0); + for _ = 1 to i do + Stack.push t.fs_env t.fs_env_stack + done + + let pop_cdcl_tableaux t i = + assert (i > 0); + let rec aux fs_env = function + | 1 -> t.fs_env <- fs_env + | i -> aux (Stack.pop t.fs_env_stack) (i - 1) + in + aux (Stack.pop t.fs_env_stack) i + + let push t i = exn_handler (fun t -> + if Options.get_tableaux_cdcl () then + push_cdcl_tableaux t i + else + t.fs_env <- FS.push t.fs_env i + ) t + + let pop t i = exn_handler (fun env -> + if Options.get_tableaux_cdcl () then + pop_cdcl_tableaux env i + else + t.fs_env <- FS.pop t.fs_env i + ) t + + let assume t g expl = + exn_handler (fun t -> t.fs_env <- FS.assume t.fs_env g expl) t let assume_th_elt t th expl = - exn_handler (fun env -> t := FS.assume_th_elt env th expl) t + exn_handler (fun t -> t.fs_env <- FS.assume_th_elt t.fs_env th expl) t let pred_def t expr n expl loc = - exn_handler (fun env -> t := FS.pred_def env expr n expl loc) t + exn_handler (fun t -> t.fs_env <- FS.pred_def t.fs_env expr n expl loc) t let unsat t g = - exn_handler (fun env -> FS.unsat env g) t + exn_handler (fun t -> FS.unsat t.fs_env g) t let optimize _env ~is_max:_ _obj = raise (Util.Not_implemented "optimization is not supported by FunSAT.") @@ -70,11 +107,11 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let reinit_ctx = FS.reinit_ctx - let get_model t = FS.get_model !t + let get_model t = FS.get_model t.fs_env - let get_unknown_reason t = FS.get_unknown_reason !t + let get_unknown_reason t = FS.get_unknown_reason t.fs_env - let get_value t expr = FS.get_value !t expr + let get_value t expr = FS.get_value t.fs_env expr let get_objectives _env = raise (Util.Not_implemented "optimization is not supported by FunSAT.") diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index 9b89753e08..042fd1c0aa 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -120,6 +120,7 @@ module type SAT_ML = sig val create : Atom.hcons_env -> t val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> unit + val push_level : t -> int val decision_level : t -> int val cancel_until : t -> int -> unit @@ -175,6 +176,9 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct (* si vrai, les contraintes sont deja fausses *) mutable is_unsat : bool; + (* le nombre de fois que l'on a poussé un environnement unsat *) + mutable is_unsat_cpt : int; + mutable unsat_core : Atom.clause list option; (* clauses du probleme *) @@ -425,6 +429,8 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct is_unsat = false; + is_unsat_cpt = 0; + unsat_core = None; clauses = Vec.make 0 ~dummy:Atom.dummy_clause; @@ -562,6 +568,8 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct env.clause_inc <- env.clause_inc *. 1e-20 end + let push_level env = Vec.size env.increm_guards + let decision_level env = Vec.size env.trail_lim let nb_choices env = env.nchoices @@ -1031,6 +1039,26 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct (ta.lit, Th_util.Other, Ex.empty, 0, env.cpt_current_propagations) :: acc end + (* This was first added by PR 1000, but it triggers a bug in + tests/cc/testfile-ac_cc002.ae with option + --no-tableaux-cdcl-in-instantiation *) + (* if ta.var.level <= Vec.size env.increm_guards then begin + * incr nb_f; + * let ex = + * if ta.var.level = 0 then Ex.empty else + * let d = + * Vec.get + * env.trail + * (Vec.get env.trail_lim (ta.var.level - 1)) + * in + * Ex.singleton (Ex.Literal d) + * in + * (ta.lit, + * Th_util.Other, + * ex, + * ta.var.level, + * env.cpt_current_propagations) :: acc + * end *) else acc )[] lazy_q in @@ -1214,9 +1242,11 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct let print_aux fmt hc = Format.fprintf fmt "%a@," Atom.pr_clause hc + let set_unsat env : unit = env.is_unsat <- true + let report_b_unsat env linit = if not (Options.get_unsat_core ()) then begin - env.is_unsat <- true; + set_unsat env; env.unsat_core <- None; raise (Unsat None) end @@ -1256,7 +1286,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct let unsat_core = HUC.fold (fun c _ l -> c :: l) uc [] in Printer.print_dbg ~header:false "@[UNSAT_CORE:@ %a@]" (Printer.pp_list_no_space print_aux) unsat_core; - env.is_unsat <- true; + set_unsat env; let unsat_core = Some unsat_core in env.unsat_core <- unsat_core; raise (Unsat unsat_core) @@ -1264,7 +1294,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct let report_t_unsat env dep = if not (Options.get_unsat_core ()) then begin - env.is_unsat <- true; + set_unsat env; env.unsat_core <- None; raise (Unsat None) end @@ -1305,7 +1335,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct Printer.print_dbg ~header:false "@[T-UNSAT_CORE:@ %a@]" (Printer.pp_list_no_space print_aux) unsat_core; - env.is_unsat <- true; + set_unsat env; let unsat_core = Some unsat_core in env.unsat_core <- unsat_core; raise (Unsat unsat_core) @@ -2172,11 +2202,14 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct guard.is_guard <- true; guard.neg.is_guard <- false; cancel_until env env.next_dec_guard; - Vec.push env.increm_guards guard + Vec.push env.increm_guards guard; + env.is_unsat_cpt <- if env.is_unsat then env.is_unsat_cpt + 1 else 0 let pop env = (assert (not (Vec.is_empty env.increm_guards))); let g = Vec.pop env.increm_guards in + env.is_unsat <- env.is_unsat_cpt <> 0; + env.is_unsat_cpt <- max 0 (env.is_unsat_cpt - 1); g.is_guard <- false; g.neg.is_guard <- false; assert (not g.var.na.is_true); (* atom not false *) diff --git a/src/lib/reasoners/satml.mli b/src/lib/reasoners/satml.mli index 9dac0344ce..19c9eb9dd5 100644 --- a/src/lib/reasoners/satml.mli +++ b/src/lib/reasoners/satml.mli @@ -77,6 +77,9 @@ module type SAT_ML = sig val create : Atom.hcons_env -> t val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> unit + (** Returns the push/pop depth of the current analysis + (i.e., #push - #pop) *) + val push_level : t -> int val decision_level : t -> int val cancel_until : t -> int -> unit diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 2749d7ce13..94412a2798 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -459,6 +459,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let pred_def env f name dep _loc = (* dep currently not used. No unsat-cores in satML yet *) Debug.pred_def f; + assert (SAT.decision_level env.satml <= SAT.push_level env.satml); let guard = env.guards.current_guard in env.inst <- Inst.add_predicate env.inst ~guard ~name (mk_gf f) dep @@ -1309,8 +1310,12 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct Inst.add_terms env.inst (E.max_ground_terms_rec_of_form gf.E.ff) gf; try - assert (SAT.decision_level env.satml == 0); - let _updated = assume_aux ~dec_lvl:0 env [gf] in + let _updated = + assume_aux + ~dec_lvl:(SAT.decision_level env.satml) + env + [gf] + in let max_t = max_term_depth_in_sat env in env.inst <- Inst.register_max_term_depth env.inst max_t; unsat_rec_prem env ~first_call:true; @@ -1329,8 +1334,14 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let assume env gf _dep = (* dep currently not used. No unsat-cores in satML yet *) - assert (SAT.decision_level env.satml == 0); - try ignore (assume_aux ~dec_lvl:0 env [add_guard env gf]) + assert (SAT.decision_level env.satml <= SAT.push_level env.satml); + try + let _ : bool = + assume_aux + ~dec_lvl:(SAT.decision_level env.satml) + env + [add_guard env gf] + in () with | IUnsat (_env, dep) -> raise (Unsat dep) | Util.Timeout -> (* don't attempt to compute a model if timeout before diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index 9bb1764e9e..16cbc2a975 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -272,6 +272,7 @@ let preludes = ref [] let theory_preludes = ref Theories.default_preludes let type_only = ref false let type_smt2 = ref false +let imperative_mode = ref false let set_answers_with_loc b = answers_with_loc := b let set_output_with_colors b = output_with_colors := b @@ -286,6 +287,7 @@ let set_preludes p = preludes := p let set_theory_preludes t = theory_preludes := t let set_type_only b = type_only := b let set_type_smt2 b = type_smt2 := b +let set_imperative_mode i = imperative_mode := i let get_answers_with_locs () = !answers_with_loc let get_output_with_colors () = !output_with_colors @@ -299,6 +301,7 @@ let get_preludes () = !preludes let get_theory_preludes () = !theory_preludes let get_type_only () = !type_only let get_type_smt2 () = !type_smt2 +let get_imperative_mode () = !imperative_mode (** Internal options *) diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index 9bbbf965c2..02998e7d66 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -298,6 +298,9 @@ val set_triggers_var : bool -> unit (** Set [type_smt2] accessible with {!val:get_type_smt2} *) val set_type_smt2 : bool -> unit +(** Set [imperative_mode] accessible with {!val:get_imperative_mode} *) +val set_imperative_mode : bool -> unit + (** Set [unsat_core] accessible with {!val:get_unsat_core} *) val set_unsat_core : bool -> unit @@ -660,6 +663,10 @@ val get_type_only : unit -> bool val get_type_smt2 : unit -> bool (** Default to [false] *) +(** [true] if the solving loop should work in a pure imperative mode. *) +val get_imperative_mode : unit -> bool +(** Default to [false] *) + (** {4 Internal options} *) (** [true] if the GC is prevented from collecting hashconsed data structrures diff --git a/tests/adts/simple_1.ae b/tests/adts/simple_1.ae index cc82d2f240..416c8f617c 100644 --- a/tests/adts/simple_1.ae +++ b/tests/adts/simple_1.ae @@ -49,7 +49,7 @@ goal g_valid_4_2: e ? B -> false -(**) +(* Isse 1008: this goal fail when encapsulated by a push/pop. *) goal g_valid_5_1: forall n : int. n >= 0 -> (* just here for E-matching *) @@ -57,6 +57,7 @@ goal g_valid_5_1: not (e ? B) -> exists x : int[x]. e = C(x) + goal g_valid_5_2: forall n : int. not (e ? A) -> diff --git a/tests/cram.t/postlude.smt2 b/tests/cram.t/postlude.smt2 index b709d1db6e..e5e0009218 100644 --- a/tests/cram.t/postlude.smt2 +++ b/tests/cram.t/postlude.smt2 @@ -22,8 +22,8 @@ (assert (not (my_leq (f x) x))) (check-sat) - ; Now that x > 10 is known, the trigger should apply - (assert (> x 10)) + ; Now that f x > 10 is known, the trigger should apply + (assert (> (f x) 10)) (check-sat) (pop 1) diff --git a/tests/cram.t/prelude.ae b/tests/cram.t/prelude.ae index 25143cfb95..af49416e00 100644 --- a/tests/cram.t/prelude.ae +++ b/tests/cram.t/prelude.ae @@ -10,5 +10,5 @@ logic f : real -> real theory F_theory extends FPA = axiom f_triggers : - forall x : real [ int_floor(x), x in ]0., ?] ]. my_leq(f(x), x) + forall x: real [ f(x), f(x) in ]0., ?] ]. my_leq(f(x), x) end diff --git a/tests/issues/926.models.smt2 b/tests/issues/926.models.smt2 index 2c9860dae8..ead54d8246 100644 --- a/tests/issues/926.models.smt2 +++ b/tests/issues/926.models.smt2 @@ -1,5 +1,5 @@ -(set-logic ALL) (set-option :produce-models true) +(set-logic ALL) (declare-const x1 Int) (declare-const x2 Int) (declare-const y1 Real) diff --git a/tests/models/arith/arith12.optimize.expected b/tests/models/arith/arith12.optimize.expected index 3f79c668e2..6baad1e2e5 100644 --- a/tests/models/arith/arith12.optimize.expected +++ b/tests/models/arith/arith12.optimize.expected @@ -7,9 +7,8 @@ unknown (x 10)) unknown ( - (define-fun x () Int 10) + (define-fun x () Int 0) ) (objectives - (x 10) - (x 10) + (x 0) ) \ No newline at end of file diff --git a/tests/smtlib/testfile-get-info1.dolmen.expected b/tests/smtlib/testfile-get-info1.dolmen.expected index f3993ae214..bd538a3a51 100644 --- a/tests/smtlib/testfile-get-info1.dolmen.expected +++ b/tests/smtlib/testfile-get-info1.dolmen.expected @@ -1,7 +1,7 @@ unknown ( - :steps 7) + :steps 9) unsupported diff --git a/tests/smtlib/testfile-steps-bound2.dolmen.expected b/tests/smtlib/testfile-steps-bound2.dolmen.expected index 2c1783497a..9c2a2a16f7 100644 --- a/tests/smtlib/testfile-steps-bound2.dolmen.expected +++ b/tests/smtlib/testfile-steps-bound2.dolmen.expected @@ -1,5 +1,5 @@ unknown -(:reason-unknown (:step-limit 3)) +(:reason-unknown (:step-limit 5)) unsat diff --git a/tests/smtlib/testfile-steps-bound2.dolmen.smt2 b/tests/smtlib/testfile-steps-bound2.dolmen.smt2 index 3d578cf450..171dbafe76 100644 --- a/tests/smtlib/testfile-steps-bound2.dolmen.smt2 +++ b/tests/smtlib/testfile-steps-bound2.dolmen.smt2 @@ -1,4 +1,4 @@ -(set-option :steps-bound 2) +(set-option :steps-bound 4) (set-logic ALL) (declare-const x Int)