simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat(main): with --cdsat, use cdsat solver

Browse source
This commit is contained in:
Simon Cruanes 2022-10-29 22:48:49 -04:00
parent 8f2e2ac6de
commit 903d12c39b
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 34 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/main/dune
View file

@ -8,7 +8,7 @@
(modes native) (modes native)
(libraries containers iter result sidekick.sat sidekick.core sidekick-base (libraries containers iter result sidekick.sat sidekick.core sidekick-base
sidekick.smt-solver sidekick-base.smtlib sidekick.tef sidekick.drup sidekick.smt-solver sidekick-base.smtlib sidekick.tef sidekick.drup
sidekick.memtrace sidekick-bin.lib) sidekick.memtrace sidekick.cdsat sidekick-bin.lib)
(flags :standard -safe-string -color always -open Sidekick_util)) (flags :standard -safe-string -color always -open Sidekick_util))
(executable (executable

34
src/main/main.ml
View file

@ -11,6 +11,7 @@ module Config = Sidekick_base.Config
module Solver = Sidekick_smtlib.Solver module Solver = Sidekick_smtlib.Solver
module Driver = Sidekick_smtlib.Driver module Driver = Sidekick_smtlib.Driver
module Proof = Sidekick_proof module Proof = Sidekick_proof
module Asolver = Sidekick_abstract_solver.Asolver
open E.Infix open E.Infix
type 'a or_error = ('a, string) E.t type 'a or_error = ('a, string) E.t
@ -28,6 +29,7 @@ let mem_limit = ref 1_000_000_000.
let p_stat = ref false let p_stat = ref false
let p_gc_stat = ref false let p_gc_stat = ref false
let p_progress = ref false let p_progress = ref false
let cdsat = ref false
let enable_trace = ref false let enable_trace = ref false
let proof_file = ref "" let proof_file = ref ""
let trace_file = ref "" let trace_file = ref ""
@ -78,6 +80,7 @@ let argspec =
"--no-proof", Arg.Clear p_proof, " do not print proof"; "--no-proof", Arg.Clear p_proof, " do not print proof";
"-o", Arg.Set_string proof_file, " file into which to output a proof"; "-o", Arg.Set_string proof_file, " file into which to output a proof";
"--model", Arg.Set p_model, " print model"; "--model", Arg.Set p_model, " print model";
"--cdsat", Arg.Set cdsat, " use cdsat solver";
"--trace", Arg.Set enable_trace, " enable tracing"; "--trace", Arg.Set enable_trace, " enable tracing";
"--no-trace", Arg.Clear enable_trace, " disable tracing"; "--no-trace", Arg.Clear enable_trace, " disable tracing";
( "--trace-file", ( "--trace-file",
@ -182,7 +185,13 @@ let main_smt ~config () : _ result =
let tracer = mk_smt_tracer ~trace_file () in let tracer = mk_smt_tracer ~trace_file () in
Proof.Tracer.enable tracer enable_proof; Proof.Tracer.enable tracer enable_proof;
let solver = let asolver =
if !cdsat then
let open Sidekick_cdsat in
let vst = TVar.Store.create tst in
Core.create tst vst ~proof_tracer:(tracer :> Proof.Tracer.t) ()
|> Core.as_asolver
else (
(* TODO: probes, to load only required theories *) (* TODO: probes, to load only required theories *)
let theories = let theories =
let th_bool = Driver.th_bool config in let th_bool = Driver.th_bool config in
@ -191,14 +200,25 @@ let main_smt ~config () : _ result =
(Sidekick_smt_solver.Theory.name th_bool)); (Sidekick_smt_solver.Theory.name th_bool));
[ th_bool; Driver.th_ty_unin; Driver.th_data; Driver.th_lra ] [ th_bool; Driver.th_ty_unin; Driver.th_data; Driver.th_lra ]
in in
let solver =
Solver.Smt_solver.Solver.create_default ~tracer ~theories tst () Solver.Smt_solver.Solver.create_default ~tracer ~theories tst ()
in in
let finally () = if !check then
if !p_stat then (* might have to check conflicts *)
Format.printf "%a@." Solver.Smt_solver.Solver.pp_stats solver Solver.Smt_solver.Solver.add_theory solver
Sidekick_smtlib.Check_cc.theory;
Solver.Smt_solver.Solver.as_asolver solver
)
in in
CCFun.protect ~finally @@ fun () ->
let finally () =
if !p_stat then Format.printf "%a@." Asolver.pp_stats asolver
in
let@ () = CCFun.protect ~finally in
(* FIXME: emit an actual proof *) (* FIXME: emit an actual proof *)
let proof_file = let proof_file =
if !proof_file = "" then if !proof_file = "" then
@ -206,9 +226,6 @@ let main_smt ~config () : _ result =
else else
Some !proof_file Some !proof_file
in in
if !check then
(* might have to check conflicts *)
Solver.Smt_solver.Solver.add_theory solver Sidekick_smtlib.Check_cc.theory;
let parse_res = let parse_res =
let@ () = Profile.with_ "parse" ~args:[ "file", !file ] in let@ () = Profile.with_ "parse" ~args:[ "file", !file ] in
@ -217,7 +234,6 @@ let main_smt ~config () : _ result =
parse_res >>= fun input -> parse_res >>= fun input ->
let driver = let driver =
let asolver = Solver.Smt_solver.Solver.as_asolver solver in
Driver.create ~pp_cnf:!p_cnf ~time:!time_limit ~memory:!mem_limit Driver.create ~pp_cnf:!p_cnf ~time:!time_limit ~memory:!mem_limit
~pp_model:!p_model ?proof_file ~check:!check ~progress:!p_progress asolver ~pp_model:!p_model ?proof_file ~check:!check ~progress:!p_progress asolver
in in