From 7f5700465343e1927a07782b35fccc1cb9b5324d Mon Sep 17 00:00:00 2001
From: hra687261 <hichem.ait-el-hara@ocamlpro.com>
Date: Tue, 29 Nov 2022 16:01:24 +0100
Subject: [PATCH] Update Dolmen state creation
---
colibri2/solver/input.ml | 43 +++++++++++++++++++++++-----------------
colibrics/bin/loop.ml | 3 +++
colibrics/bin/options.ml | 35 ++++++++++++++++----------------
3 files changed, 46 insertions(+), 35 deletions(-)
diff --git a/colibri2/solver/input.ml b/colibri2/solver/input.ml
index 8403567b3..9eb402a59 100644
--- a/colibri2/solver/input.ml
+++ b/colibri2/solver/input.ml
@@ -152,6 +152,9 @@ module Typer = struct
include
Dolmen_loop.Typer.Make (Dolmen.Std.Expr) (Dolmen.Std.Expr.Print) (State) (T)
+
+ let init_pipe = init
+ let init = T.init
end
type tag_colibri2 = Goal
@@ -571,8 +574,8 @@ let mk_state ?(gc = false) ?(gc_opt = Gc.get ()) ?(bt = true) ?(colors = true)
let () = if bt then Printexc.record_backtrace true in
let () = if gc then at_exit (fun () -> Gc.print_stat stdout) in
(* State creation *)
+ let dir, source = split_input input in
let logic_file : _ State.file =
- let dir, source = split_input input in
{
lang = input_lang;
mode = input_mode;
@@ -581,26 +584,30 @@ let mk_state ?(gc = false) ?(gc_opt = Gc.get ()) ?(bt = true) ?(colors = true)
loc = Dolmen.Std.Loc.mk_file "";
}
in
+ let response_file : _ State.file =
+ {
+ lang = None;
+ mode = None;
+ dir;
+ source = `Raw ("", "");
+ loc = Dolmen.Std.Loc.mk_file "";
+ }
+ in
let ctx =
create_ctx ?step_limit ?last_effort_limit ?options ?print_success
?negate_goal learning theories
in
(* State creation *)
let set = State.set in
- State.empty |> set solver_state ctx |> set State.debug debug
- |> set State.report_style Contextual
- |> set State.reports
- (Dolmen_loop.Report.Conf.mk
- ~default:Dolmen_loop.Report.Warning.Status.Disabled)
- |> set State.max_warn max_warn
- |> set State.cur_warn 0
- |> set State.time_limit time_limit
- |> set State.size_limit size_limit
- |> set State.logic_file logic_file
- |> set Header.header_check header_check
- |> set Header.header_state Dolmen_loop.Headers.empty
- |> set Header.header_licenses header_licenses
- |> set Header.header_lang_version header_lang_version
- |> set Typer.type_check type_check
- |> set Typer.ty_state (Dolmen_loop.Typer.new_state ())
- |> set Typer.smtlib2_forced_logic None
+ State.empty |> set solver_state ctx
+ |> State.init ~debug ~report_style:Contextual
+ ~reports:
+ (Dolmen_loop.Report.Conf.mk
+ ~default:Dolmen_loop.Report.Warning.Status.Disabled)
+ ~max_warn ~time_limit ~size_limit ~logic_file ~response_file
+ |> Parser.init
+ |> Typer.init
+ ~ty_state:(Dolmen_loop.Typer.new_state ())
+ ~smtlib2_forced_logic:None
+ |> Typer.init_pipe ~type_check
+ |> Header.init ~header_check ~header_licenses ~header_lang_version
diff --git a/colibrics/bin/loop.ml b/colibrics/bin/loop.ml
index 9717918fb..08ee2366c 100644
--- a/colibrics/bin/loop.ml
+++ b/colibrics/bin/loop.ml
@@ -13,6 +13,9 @@ module Typer = struct
module T = Dolmen_loop.Typer.Typer(State)
include T
include Dolmen_loop.Typer.Make(Dolmen.Std.Expr)(Dolmen.Std.Expr.Print)(State)(T)
+
+ let init_pipe = init
+ let init = T.init
end
let solver_state : Dolmen_to_colibrics.t State.key = State.create_key ~pipe:"" "solver_state"
diff --git a/colibrics/bin/options.ml b/colibrics/bin/options.ml
index 65135bd84..05488fdab 100644
--- a/colibrics/bin/options.ml
+++ b/colibrics/bin/options.ml
@@ -46,8 +46,8 @@ let mk_state
let () = if bt then Printexc.record_backtrace true in
let () = if gc then at_exit (fun () -> Gc.print_stat stdout) in
(* State creation *)
- let logic_file : _ State.file =
let dir, source = split_input input in
+ let logic_file : _ State.file =
{
lang = input_lang;
mode = input_mode;
@@ -56,27 +56,28 @@ let mk_state
loc = Dolmen.Std.Loc.mk_file "";
}
in
+ let response_file : _ State.file = {
+ lang = None; mode = None; dir;
+ loc = Dolmen.Std.Loc.mk_file "";
+ source = `Raw ("", "");
+ } in
let ctx = Dolmen_to_colibrics.create ()
in
(* State creation *)
let set = State.set in
- State.empty |> set solver_state ctx |> set State.debug debug
- |> set State.report_style Minimal
- |> set State.reports
- (Dolmen_loop.Report.Conf.mk
- ~default:Dolmen_loop.Report.Warning.Status.Disabled)
- |> set State.max_warn max_warn
- |> set State.cur_warn 0
- |> set State.time_limit time_limit
- |> set State.size_limit size_limit
- |> set State.logic_file logic_file
- |> set Header.header_check header_check
+ State.empty |> set solver_state ctx
|> set Header.header_state Dolmen_loop.Headers.empty
- |> set Header.header_licenses header_licenses
- |> set Header.header_lang_version header_lang_version
- |> set Typer.type_check type_check
- |> set Typer.ty_state (Dolmen_loop.Typer.new_state ())
- |> set Typer.smtlib2_forced_logic None
+ |> State.init ~debug ~report_style:Minimal
+ ~reports:
+ (Dolmen_loop.Report.Conf.mk
+ ~default:Dolmen_loop.Report.Warning.Status.Disabled)
+ ~max_warn ~time_limit ~size_limit ~logic_file ~response_file
+ |> Parser.init
+ |> Typer.init
+ ~ty_state:(Dolmen_loop.Typer.new_state ())
+ ~smtlib2_forced_logic:None
+ |> Typer.init_pipe ~type_check
+ |> Header.init ~header_check ~header_licenses ~header_lang_version
(* Input source converter *)
(* ************************************************************************* *)
--
GitLab