From 668bd36311302912a3bb68565299b649cb7ee32e Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 1 Feb 2019 21:01:06 -0600 Subject: [PATCH] test: remove API test, which belongs in msat --- tests/dune | 14 ---- tests/test_api.ml | 190 ---------------------------------------------- 2 files changed, 204 deletions(-) delete mode 100644 tests/dune delete mode 100644 tests/test_api.ml diff --git a/tests/dune b/tests/dune deleted file mode 100644 index b105a8d4..00000000 --- a/tests/dune +++ /dev/null @@ -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))) - - diff --git a/tests/test_api.ml b/tests/test_api.ml deleted file mode 100644 index 4ce25199..00000000 --- a/tests/test_api.ml +++ /dev/null @@ -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), - " 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()