mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 11:15:43 -05:00
test: remove API test, which belongs in msat
This commit is contained in:
Simon Cruanes
parent
3f24e9cfe3
commit
668bd36311
2 changed files with 0 additions and 204 deletions
14
tests/dune
14
tests/dune
|
|
@ -1,14 +0,0 @@
|
|||
|
||||
(executable
|
||||
(name test_api)
|
||||
(libraries sidekick.backend sidekick.sat sidekick.smt.th-bool)
|
||||
(flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)
|
||||
(ocamlopt_flags :standard -O3 -color always
|
||||
-unbox-closures -unbox-closures-factor 20)
|
||||
)
|
||||
|
||||
(alias
|
||||
(name runtest)
|
||||
(action (run ./test_api.exe)))
|
||||
|
||||
|
||||
|
|
@ -1,190 +0,0 @@
|
|||
(*
|
||||
MSAT is free software, using the Apache license, see file LICENSE
|
||||
Copyright 2014 Guillaume Bury
|
||||
Copyright 2014 Simon Cruanes
|
||||
*)
|
||||
|
||||
(* Tests that require the API *)
|
||||
|
||||
open Sidekick_sat
|
||||
|
||||
module Th = Sidekick_th_sat.Th
|
||||
module F = CDCL_tseitin.Make(Th)
|
||||
|
||||
let (|>) x f = f x
|
||||
|
||||
let time_limit = ref 300.
|
||||
let size_limit = ref 1000_000_000.
|
||||
|
||||
let error_msg opt arg l =
|
||||
Format.fprintf Format.str_formatter "'%s' is not a valid argument for '%s', valid arguments are : %a"
|
||||
arg opt (fun fmt -> List.iter (fun (s, _) -> Format.fprintf fmt "%s, " s)) l;
|
||||
Format.flush_str_formatter ()
|
||||
|
||||
let set_flag opt arg flag l =
|
||||
try
|
||||
flag := List.assoc arg l
|
||||
with Not_found ->
|
||||
invalid_arg (error_msg opt arg l)
|
||||
|
||||
let usage = "Usage : test_api [options]"
|
||||
let argspec = Arg.align [
|
||||
"-v", Arg.Int (fun i -> Log.set_debug i),
|
||||
"<lvl> Sets the debug verbose level";
|
||||
]
|
||||
|
||||
type solver_res =
|
||||
| R_sat
|
||||
| R_unsat
|
||||
|
||||
exception Incorrect_model
|
||||
|
||||
module type BASIC_SOLVER = sig
|
||||
type t
|
||||
val create : unit -> t
|
||||
val solve : t -> ?assumptions:F.atom list -> unit -> solver_res
|
||||
val assume : t -> ?tag:int -> F.atom list list -> unit
|
||||
end
|
||||
|
||||
let mk_solver (): (module BASIC_SOLVER) =
|
||||
let module S = struct
|
||||
include CDCL_sat
|
||||
let create() = create()
|
||||
let solve st ?assumptions () =
|
||||
match solve st ?assumptions() with
|
||||
| Sat _ ->
|
||||
R_sat
|
||||
| Unsat (Unsat_state us) ->
|
||||
let p = us.get_proof () in
|
||||
Proof.check p;
|
||||
R_unsat
|
||||
end
|
||||
in (module S)
|
||||
|
||||
exception Error of string
|
||||
|
||||
let error msg = raise (Error msg)
|
||||
let errorf msg = Format.ksprintf error msg
|
||||
|
||||
module Test = struct
|
||||
type action =
|
||||
| A_assume of F.atom list list
|
||||
| A_solve of F.atom list * [`Expect_sat | `Expect_unsat]
|
||||
|
||||
type t = {
|
||||
name: string;
|
||||
actions: action list;
|
||||
}
|
||||
|
||||
let mk_test name l = {name; actions=l}
|
||||
let assume l = A_assume l
|
||||
let assume1 c = assume [c]
|
||||
let solve ?(assumptions=[]) e = A_solve (assumptions, e)
|
||||
|
||||
type result =
|
||||
| Pass
|
||||
| Fail of string
|
||||
|
||||
let run (t:t): result =
|
||||
(* Interesting stuff happening *)
|
||||
let (module S: BASIC_SOLVER) = mk_solver () in
|
||||
let st = S.create() in
|
||||
try
|
||||
List.iter
|
||||
(function
|
||||
| A_assume cs ->
|
||||
S.assume st cs
|
||||
| A_solve (assumptions, expect) ->
|
||||
match S.solve st ~assumptions (), expect with
|
||||
| R_sat, `Expect_sat
|
||||
| R_unsat, `Expect_unsat -> ()
|
||||
| R_unsat, `Expect_sat ->
|
||||
error "expect sat, got unsat"
|
||||
| R_sat, `Expect_unsat ->
|
||||
error "expect unsat, got sat"
|
||||
)
|
||||
t.actions;
|
||||
Pass
|
||||
with Error msg ->
|
||||
Fail msg
|
||||
|
||||
(* basic test *)
|
||||
let test1 =
|
||||
[ assume [[-1;2]; [-1;3]];
|
||||
solve `Expect_sat;
|
||||
assume [[-2;4]; [-3;-4]];
|
||||
solve `Expect_sat;
|
||||
assume [[1]];
|
||||
solve `Expect_unsat;
|
||||
] |> mk_test "test1"
|
||||
|
||||
(* same as test1 but with assumptions *)
|
||||
let test2 =
|
||||
[ solve `Expect_sat;
|
||||
assume [[-1;2]; [-1;3]];
|
||||
solve `Expect_sat;
|
||||
assume [[-2;4]; [-3;-4]];
|
||||
solve `Expect_sat;
|
||||
solve ~assumptions:[1] `Expect_unsat;
|
||||
solve `Expect_sat;
|
||||
] |> mk_test "test2"
|
||||
|
||||
(* repeat assumptions *)
|
||||
let test3 =
|
||||
[ assume [[-1;2]; [-1;3]];
|
||||
solve `Expect_sat;
|
||||
assume [[-2;4]; [-3;-4]];
|
||||
solve `Expect_sat;
|
||||
solve ~assumptions:[1] `Expect_unsat;
|
||||
solve `Expect_sat;
|
||||
solve ~assumptions:[1] `Expect_unsat;
|
||||
solve `Expect_sat;
|
||||
solve ~assumptions:[1] `Expect_unsat;
|
||||
solve `Expect_sat;
|
||||
solve ~assumptions:[2] `Expect_sat;
|
||||
assume [[1]];
|
||||
solve `Expect_unsat;
|
||||
] |> mk_test "test3"
|
||||
|
||||
(* Conflict at level 0 *)
|
||||
let test4 =
|
||||
[ assume [[-1; -2]];
|
||||
solve `Expect_sat;
|
||||
assume [[1]];
|
||||
solve `Expect_sat;
|
||||
assume [[2]];
|
||||
solve ~assumptions:[3] `Expect_unsat;
|
||||
solve ~assumptions:[] `Expect_unsat;
|
||||
solve ~assumptions:[] `Expect_unsat;
|
||||
] |> mk_test "conflict0"
|
||||
|
||||
(* just check that we do create new solvers *)
|
||||
let test_clean =
|
||||
[ solve `Expect_sat
|
||||
] |> mk_test "test_clean"
|
||||
|
||||
let suite =
|
||||
[ test1;
|
||||
test2;
|
||||
test3;
|
||||
test4;
|
||||
test_clean; (* after test3 *)
|
||||
]
|
||||
end
|
||||
|
||||
let main () =
|
||||
(* Administrative duties *)
|
||||
Arg.parse argspec (fun _ -> ()) usage;
|
||||
let failed = ref false in
|
||||
List.iter
|
||||
(fun test ->
|
||||
Printf.printf "%-10s... %!" test.Test.name;
|
||||
match Test.run test with
|
||||
| Test.Pass -> Printf.printf "ok\n%!"
|
||||
| Test.Fail msg ->
|
||||
failed := true;
|
||||
Printf.printf "fail (%s)\n%!" msg)
|
||||
Test.suite;
|
||||
if !failed then exit 1
|
||||
|
||||
let () = main()
|
||||
Loading…
Add table
Reference in a new issue