From fc5ce9bf87dd4524ed6c47ec514ae877c1dd1427 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 8 Aug 2022 21:52:47 -0400 Subject: [PATCH] wip: make it compile --- src/smt/solver.ml | 3 -- src/smt/solver.mli | 2 + src/smtlib/Process.ml | 45 ++++++++++--------- src/smtlib/Process.mli | 9 +--- src/smtlib/dune | 2 +- {src/tests => unittest/old}/basic.cnf | 0 .../old}/basic.drup.expected | 0 {src/tests => unittest/old}/dune | 2 +- {src/tests => unittest/old}/regression/dune | 0 .../regression/reg_model_lra1.out.expected | 0 .../old}/regression/reg_model_lra1.smt2 | 0 {src/tests => unittest/old}/run_tests.ml | 7 +-- 12 files changed, 29 insertions(+), 41 deletions(-) rename {src/tests => unittest/old}/basic.cnf (100%) rename {src/tests => unittest/old}/basic.drup.expected (100%) rename {src/tests => unittest/old}/dune (93%) rename {src/tests => unittest/old}/regression/dune (100%) rename {src/tests => unittest/old}/regression/reg_model_lra1.out.expected (100%) rename {src/tests => unittest/old}/regression/reg_model_lra1.smt2 (100%) rename {src/tests => unittest/old}/run_tests.ml (79%) diff --git a/src/smt/solver.ml b/src/smt/solver.ml index 6f92f526..4b2aa8ab 100644 --- a/src/smt/solver.ml +++ b/src/smt/solver.ml @@ -69,8 +69,6 @@ type t = { count_solve: int Stat.counter; (* config: Config.t *) } -type solver = t - (** {2 Main} *) type theory = Theory.t @@ -117,7 +115,6 @@ let create arg ?(stat = Stat.global) ?size ~proof ~theories tst () : t = self let[@inline] solver self = self.solver -let[@inline] cc self = Solver_internal.cc self.si let[@inline] stats self = self.stat let[@inline] tst self = Solver_internal.tst self.si let[@inline] proof self = self.proof diff --git a/src/smt/solver.mli b/src/smt/solver.mli index 97628abd..d297cc6a 100644 --- a/src/smt/solver.mli +++ b/src/smt/solver.mli @@ -14,6 +14,8 @@ type t val registry : t -> Registry.t (** A solver contains a registry so that theories can share data *) +type theory = Theory.t + val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 17f685ed..8ff0297b 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -1,8 +1,8 @@ (** {2 Conversion into {!Term.t}} *) +open Sidekick_core module Profile = Sidekick_util.Profile open! Sidekick_base -module SBS = Sidekick_base_solver [@@@ocaml.warning "-32"] @@ -10,12 +10,11 @@ type 'a or_error = ('a, string) CCResult.t module E = CCResult module Fmt = CCFormat -module Solver = SBS.Solver +module Solver = Sidekick_smt_solver.Solver module Check_cc = struct - module Lit = Solver.Solver_internal.Lit - module SI = Solver.Solver_internal - module MCC = Sidekick_mini_cc.Make (SBS.Solver_arg) + module SI = Sidekick_smt_solver.Solver_internal + module MCC = Sidekick_mini_cc let pp_c out c = Fmt.fprintf out "(@[%a@])" (Util.pp_list ~sep:" ∨ " Lit.pp) c @@ -30,7 +29,7 @@ module Check_cc = struct let check_conflict si _cc (confl : Lit.t list) : unit = Log.debugf 15 (fun k -> k "(@[check-cc-conflict@ %a@])" pp_c confl); let tst = SI.tst si in - let cc = MCC.create tst in + let cc = MCC.create_default tst in (* add [¬confl] and check it's unsat *) List.iter (fun lit -> add_cc_lit cc @@ Lit.neg lit) confl; if MCC.check_sat cc then @@ -46,7 +45,7 @@ module Check_cc = struct Log.debugf 15 (fun k -> k "(@[check-cc-prop@ %a@ :reason %a@])" Lit.pp p pp_and reason); let tst = SI.tst si in - let cc = MCC.create tst in + let cc = MCC.create_default tst in (* add [reason & ¬lit] and check it's unsat *) List.iter (add_cc_lit cc) reason; add_cc_lit cc (Lit.neg p); @@ -62,10 +61,8 @@ module Check_cc = struct let theory = Solver.mk_theory ~name:"cc-check" ~create_and_setup:(fun si -> - let n_calls = - Stat.mk_int (Solver.Solver_internal.stats si) "check-cc.call" - in - Solver.Solver_internal.on_cc_conflict si (fun { cc; th; c } -> + let n_calls = Stat.mk_int (SI.stats si) "check-cc.call" in + SI.on_cc_conflict si (fun { cc; th; c } -> if not th then ( Stat.incr n_calls; check_conflict si cc c @@ -184,7 +181,7 @@ let solve ?gc:_ ?restarts:_ ?proof_file ?(pp_model = false) ?(check = false) | Solver.Sat m -> if pp_model then (* TODO: use actual {!Model} in the solver? or build it afterwards *) - Format.printf "(@[model@ %a@])@." Solver.Model.pp m; + Format.printf "(@[model@ %a@])@." Sidekick_smt_solver.Model.pp m; (* TODO if check then ( Solver.check_model s; @@ -210,12 +207,16 @@ let solve ?gc:_ ?restarts:_ ?proof_file ?(pp_model = false) ?(check = false) | Some step_id -> let proof = Solver.proof s in let proof_quip = - Profile.with_ "proof.to-quip" @@ fun () -> - Proof_quip.of_proof proof ~unsat:step_id + Profile.with_ "proof.to-quip" @@ fun () -> assert false + (* TODO + Proof_quip.of_proof proof ~unsat:step_id + *) in Profile.with_ "proof.write-file" @@ fun () -> with_file_out file @@ fun oc -> - Proof_quip.output oc proof_quip; + (* TODO + Proof_quip.output oc proof_quip; + *) flush oc) | _ -> ()); @@ -248,7 +249,7 @@ let process_stmt ?gc ?restarts ?(pp_cnf = false) ?proof_file ?pp_model (* TODO: more? *) in - let add_step r = Solver.Proof_trace.add_step (Solver.proof solver) r in + let add_step r = Proof_trace.add_step (Solver.proof solver) r in match stmt with | Statement.Stmt_set_logic logic -> @@ -283,7 +284,7 @@ let process_stmt ?gc ?restarts ?(pp_cnf = false) ?proof_file ?pp_model if pp_cnf then Format.printf "(@[assert@ %a@])@." Term.pp t; let lit = Solver.mk_lit_t solver t in Solver.add_clause solver [| lit |] - (add_step @@ Proof.Rule_sat.sat_input_clause (Iter.singleton lit)); + (add_step @@ fun () -> Proof_sat.sat_input_clause [ lit ]); E.return () | Statement.Stmt_assert_clause c_ts -> if pp_cnf then @@ -293,16 +294,16 @@ let process_stmt ?gc ?restarts ?(pp_cnf = false) ?proof_file ?pp_model (* proof of assert-input + preprocessing *) let pr = - let tst = Solver.tst solver in - let lits = Iter.of_list c_ts |> Iter.map (Lit.atom tst) in - add_step @@ Proof.Rule_sat.sat_input_clause lits + add_step @@ fun () -> + let lits = List.map Lit.atom c_ts in + Proof_sat.sat_input_clause lits in Solver.add_clause solver (CCArray.of_list c) pr; E.return () | Statement.Stmt_get_model -> (match Solver.last_res solver with - | Some (Solver.Sat m) -> Fmt.printf "%a@." Solver.Model.pp m + | Some (Solver.Sat m) -> Fmt.printf "%a@." Sidekick_smt_solver.Model.pp m | _ -> Error.errorf "cannot access model"); E.return () | Statement.Stmt_get_value l -> @@ -311,7 +312,7 @@ let process_stmt ?gc ?restarts ?(pp_cnf = false) ?proof_file ?pp_model let l = List.map (fun t -> - match Solver.Model.eval m t with + match Sidekick_smt_solver.Model.eval m t with | None -> Error.errorf "cannot evaluate %a" Term.pp t | Some u -> t, u) l diff --git a/src/smtlib/Process.mli b/src/smtlib/Process.mli index 1d67b33c..99785ff3 100644 --- a/src/smtlib/Process.mli +++ b/src/smtlib/Process.mli @@ -1,14 +1,7 @@ (** {1 Process Statements} *) open Sidekick_base - -module Solver : - Sidekick_smt_solver.S - with type T.Term.t = Term.t - and type T.Term.store = Term.store - and type T.Ty.t = Ty.t - and type T.Ty.store = Ty.store - and type Proof_trace.t = Proof.t +module Solver = Sidekick_smt_solver.Solver val th_bool : Solver.theory val th_data : Solver.theory diff --git a/src/smtlib/dune b/src/smtlib/dune index 2083bacf..e32fd5b9 100644 --- a/src/smtlib/dune +++ b/src/smtlib/dune @@ -2,5 +2,5 @@ (name sidekick_smtlib) (public_name sidekick-bin.smtlib) (libraries containers zarith sidekick.core sidekick.util sidekick-base - smtlib-utils sidekick.tef) + sidekick.mini-cc smtlib-utils sidekick.tef) (flags :standard -warn-error -a+8 -open Sidekick_util)) diff --git a/src/tests/basic.cnf b/unittest/old/basic.cnf similarity index 100% rename from src/tests/basic.cnf rename to unittest/old/basic.cnf diff --git a/src/tests/basic.drup.expected b/unittest/old/basic.drup.expected similarity index 100% rename from src/tests/basic.drup.expected rename to unittest/old/basic.drup.expected diff --git a/src/tests/dune b/unittest/old/dune similarity index 93% rename from src/tests/dune rename to unittest/old/dune index 7cab1b89..da6b7015 100644 --- a/src/tests/dune +++ b/unittest/old/dune @@ -3,7 +3,7 @@ (modules run_tests) (modes native) (libraries containers alcotest qcheck sidekick.util sidekick_test_simplex - sidekick_test_util sidekick_test_minicc) + sidekick_test_util) (flags :standard -warn-error -a+8 -color always)) (rule diff --git a/src/tests/regression/dune b/unittest/old/regression/dune similarity index 100% rename from src/tests/regression/dune rename to unittest/old/regression/dune diff --git a/src/tests/regression/reg_model_lra1.out.expected b/unittest/old/regression/reg_model_lra1.out.expected similarity index 100% rename from src/tests/regression/reg_model_lra1.out.expected rename to unittest/old/regression/reg_model_lra1.out.expected diff --git a/src/tests/regression/reg_model_lra1.smt2 b/unittest/old/regression/reg_model_lra1.smt2 similarity index 100% rename from src/tests/regression/reg_model_lra1.smt2 rename to unittest/old/regression/reg_model_lra1.smt2 diff --git a/src/tests/run_tests.ml b/unittest/old/run_tests.ml similarity index 79% rename from src/tests/run_tests.ml rename to unittest/old/run_tests.ml index d3b48e08..0f2f1334 100644 --- a/src/tests/run_tests.ml +++ b/unittest/old/run_tests.ml @@ -1,10 +1,5 @@ let tests : unit Alcotest.test list = - List.flatten - @@ [ - [ Sidekick_test_simplex.tests ]; - [ Sidekick_test_minicc.tests ]; - Sidekick_test_util.tests; - ] + List.flatten @@ [ [ Sidekick_test_simplex.tests ]; Sidekick_test_util.tests ] let props = List.flatten [ Sidekick_test_simplex.props; Sidekick_test_util.props ]