Skip to content
Snippets Groups Projects
Commit 28f1ab26 authored by François Bobot's avatar François Bobot
Browse files

Add option --show-steps

parent f9b9e28f
No related branches found
No related tags found
1 merge request!7One delayed by environment
Pipeline #34973 failed
Stage: build
Hide whitespace changes
Inline Side-by-side
Showing
with 177 additions and 161 deletions
src_colibri2/bin/main.ml
+ 2
− 1
View file @ 28f1ab26
......@@ -33,13 +33,14 @@ let () =
] in
let info = Cmdliner.Term.info ~man ~version:"0.1" "dolmen" in
let theories = Colibri2_core.Egraph.default_theories () in
let st,step_limit = match Cmdliner.Term.eval (Options.state theories, info) with
let st,step_limit,show_steps = match Cmdliner.Term.eval (Options.state theories, info) with
| `Version | `Help -> exit 0
| `Error `Parse | `Error `Term | `Error `Exn -> exit 2
| `Ok opt -> opt
in
Colibri2_solver.Input.read
?limit:step_limit
~show_steps:show_steps
~set_true:Colibri2_theories_bool.Boolean.set_true
~handle_exn:Colibri2_solver.Input.handle_exn_with_exit
st
src_colibri2/bin/options.ml
+ 9
− 4
View file @ 28f1ab26
......@@ -51,7 +51,7 @@ let mk_state theories
header_lang_version
type_check type_strict
debug context max_warn step_limit
debug_flags
debug_flags show_steps
=
List.iter Colibri2_popop_lib.Debug.(fun s -> set_flag (lookup_flag s)) debug_flags;
if debug then
......@@ -62,7 +62,7 @@ let mk_state theories
~size_limit ?input_lang ?input_mode ~input
~header_check ~header_licenses ~header_lang_version
~type_check ~type_strict
~debug ~context ~max_warn theories, step_limit
~debug ~context ~max_warn theories, step_limit, show_steps
(* Input source converter *)
(* ************************************************************************* *)
......@@ -311,7 +311,12 @@ let state theories =
let step_limit =
let doc = Format.asprintf
"Maximum number of steps." in
Arg.(value & opt (some int) None & info ["max-step"] ~docs ~doc)
Arg.(value & opt (some int) None & info ["max-steps"] ~docs ~doc)
in
let show_steps =
let doc = Format.asprintf
"Show the number of steps after solving." in
Arg.(value & flag & info ["show-steps"] ~docs ~doc)
in
let debug_flags =
let doc = Format.asprintf "Debug flags." in
......@@ -320,4 +325,4 @@ let state theories =
Term.(const (mk_state theories) $ gc $ gc_t $ bt $ colors $
time $ size $ in_lang $ in_mode $ input $
header_check $ header_licenses $ header_lang_version $
typing $ strict $ debug $ context $ max_warn $ step_limit $ debug_flags)
typing $ strict $ debug $ context $ max_warn $ step_limit $ debug_flags $ show_steps)
src_colibri2/solver/input.ml
+ 8
− 4
View file @ 28f1ab26
......@@ -227,7 +227,7 @@ let rec pop st i =
pop st (n-1)
let handle_stmt ?(show_checksat_result=true) ?limit ~set_true (st:State.t) (stmt:Typer.typechecked Typer.stmt) =
let handle_stmt ?(show_checksat_result=true) ?(show_steps=false) ?limit ~set_true (st:State.t) (stmt:Typer.typechecked Typer.stmt) =
begin match stmt.contents with
| `Reset
| `Get_unsat_core
......@@ -251,12 +251,16 @@ let handle_stmt ?(show_checksat_result=true) ?limit ~set_true (st:State.t) (stmt
| `Hyp d -> hyp ~set_true st.State.solve_state d
| `Solve s -> begin
solve ~set_true ?limit st.State.solve_state s;
if show_checksat_result then
if show_checksat_result then begin
match st.State.solve_state.state with
| `Unsat -> Format.printf "unsat@."
| `Sat _ -> Format.printf "sat@."
| `Unknown -> Format.printf "unknown@."
| `StepLimitReached -> Format.printf "steplimitreached@."
end;
if show_steps then begin
Format.printf "(steps %i)@." (Scheduler.get_steps st.State.solve_state.scheduler)
end
end
| `Echo s -> Format.printf "%s@." s
| `Set_info _ -> ()
......@@ -265,7 +269,7 @@ let handle_stmt ?(show_checksat_result=true) ?limit ~set_true (st:State.t) (stmt
end;
st, ()
let read ?show_checksat_result ?limit ~set_true ~handle_exn st =
let read ?show_checksat_result ?show_steps ?limit ~set_true ~handle_exn st =
let st, g =
try Parser.parse [] st
with exn ->
......@@ -279,7 +283,7 @@ let read ?show_checksat_result ?limit ~set_true ~handle_exn st =
(op ~name:"debug" debug_pipe)
@>>> (op ~name:"headers" Header.inspect)
@>>> (op ~name:"typecheck" Typer.typecheck)
@>|> (op (handle_stmt ?show_checksat_result ?limit ~set_true)) @>>> _end
@>|> (op (handle_stmt ?show_checksat_result ?show_steps ?limit ~set_true)) @>>> _end
)
)
)
......
src_colibri2/solver/scheduler.ml
+ 12
− 7
View file @ 28f1ab26
......@@ -90,6 +90,7 @@ type t =
context : Context.context;
mutable level: int;
solve_step: solve_step Context.Ref.t;
mutable steps: int;
}
(** To treat in the reverse order *)
......@@ -99,6 +100,8 @@ let print_level fmt t =
0 t.choices in
Format.fprintf fmt "%i (dec waiting:%i)" t.level nb_dec
let get_steps t = t.steps
(* let new_handler t =
* if t.delayed <> None then raise NeedStopDelayed;
* {wakeup_daemons = t.wakeup_daemons;
......@@ -126,6 +129,7 @@ let new_solver () =
var_inc = ref 1.;
level = 0;
solve_step = Context.Ref.create (Context.creator context) (Propagate);
steps = 0;
}
in
let sched_daemon att =
......@@ -353,6 +357,7 @@ let run_one_step_fix_model t =
)
let run_one_step ~nodec t =
t.steps <- t.steps + 1;
match Context.Ref.get t.solve_step with
| Propagate -> begin
match run_one_step_propagation ~nodec t with
......@@ -375,21 +380,21 @@ let rec flush t =
exception ReachStepLimit
let rec run_inf_step ?limit ~nodec t =
(match limit with | Some n when n <= 0 -> raise ReachStepLimit | _ -> ());
let rec run_inf_step ~limit ~nodec t =
if t.steps = limit then raise ReachStepLimit;
flush t;
match run_one_step ~nodec t with
| true ->
run_inf_step ?limit:(Opt.map pred limit) ~nodec t
run_inf_step ~limit ~nodec t
| false ->
Egraph.Backtrackable.delayed_stop t.solver_state
let run_inf_step ?limit ?(nodec=false) t =
let run_inf_step ?(limit=(-1)) ?(nodec=false) t =
try
run_inf_step ?limit ~nodec t;
Debug.dprintf0 debug_pushpop "[Scheduler] sat";
run_inf_step ~limit ~nodec t;
Debug.dprintf1 debug_pushpop "[Scheduler] sat(%i)" t.steps
with (Contradiction as e) ->
Debug.dprintf0 debug_pushpop "[Scheduler] unsat";
Debug.dprintf1 debug_pushpop "[Scheduler] unsat(%i)" t.steps;
raise e
let init_theories ~theories t =
......
src_colibri2/solver/scheduler.mli
+ 1
− 0
View file @ 28f1ab26
......@@ -41,6 +41,7 @@ val new_solver: unit -> t
val init_theories: theories:(Egraph.t -> unit) list -> t -> unit
val add_assertion: t -> (Egraph.t -> unit) -> unit
val check_sat: ?limit:int -> t -> [> `Unsat | `Sat of Egraph.t ]
val get_steps: t -> int
type bp
......
src_colibri2/tests/generate_tests/generate_dune_tests.ml
+ 1
− 1
View file @ 28f1ab26
......@@ -23,7 +23,7 @@ let result = Sys.argv.(2)
let print_test cout file =
Printf.fprintf cout
"(rule (action (with-stdout-to %s.res (run %%{bin:colibri2} --max-step 3000 %%{dep:%s}))))\n"
"(rule (action (with-stdout-to %s.res (run %%{bin:colibri2} --max-steps 3000 %%{dep:%s}))))\n"
file file;
Printf.fprintf cout
"(rule (alias runtest) (action (diff oracle %s.res)))\n"
......
src_colibri2/tests/solve/all/steplimitreached/dune.inc
+ 1
− 1
View file @ 28f1ab26
(rule (action (with-stdout-to oracle (echo "steplimitreached\n"))))
(rule (action (with-stdout-to bag-BagImpl-addqtvc.psmt2.res (run %{bin:colibri2} --max-step 3000 %{dep:bag-BagImpl-addqtvc.psmt2}))))
(rule (action (with-stdout-to bag-BagImpl-addqtvc.psmt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:bag-BagImpl-addqtvc.psmt2}))))
(rule (alias runtest) (action (diff oracle bag-BagImpl-addqtvc.psmt2.res)))
src_colibri2/tests/solve/all/unsat/dune.inc
+ 2
− 2
View file @ 28f1ab26
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
(rule (action (with-stdout-to bag-BagImpl-createqtvc.psmt2.res (run %{bin:colibri2} --max-step 3000 %{dep:bag-BagImpl-createqtvc.psmt2}))))
(rule (action (with-stdout-to bag-BagImpl-createqtvc.psmt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:bag-BagImpl-createqtvc.psmt2}))))
(rule (alias runtest) (action (diff oracle bag-BagImpl-createqtvc.psmt2.res)))
(rule (action (with-stdout-to fact-FactRecursive-fact_recqtvc.psmt2.res (run %{bin:colibri2} --max-step 3000 %{dep:fact-FactRecursive-fact_recqtvc.psmt2}))))
(rule (action (with-stdout-to fact-FactRecursive-fact_recqtvc.psmt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:fact-FactRecursive-fact_recqtvc.psmt2}))))
(rule (alias runtest) (action (diff oracle fact-FactRecursive-fact_recqtvc.psmt2.res)))
src_colibri2/tests/solve/dimacs/sat/dune.inc
+ 11
− 11
View file @ 28f1ab26
(rule (action (with-stdout-to oracle (echo "sat\n"))))
(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:anomaly_agetooold.cnf}))))
(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:anomaly_agetooold.cnf}))))
(rule (alias runtest) (action (diff oracle anomaly_agetooold.cnf.res)))
(rule (action (with-stdout-to anomaly_agetooold2.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:anomaly_agetooold2.cnf}))))
(rule (action (with-stdout-to anomaly_agetooold2.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:anomaly_agetooold2.cnf}))))
(rule (alias runtest) (action (diff oracle anomaly_agetooold2.cnf.res)))
(rule (action (with-stdout-to assertion_fail.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:assertion_fail.cnf}))))
(rule (action (with-stdout-to assertion_fail.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:assertion_fail.cnf}))))
(rule (alias runtest) (action (diff oracle assertion_fail.cnf.res)))
(rule (action (with-stdout-to fuzzing1.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:fuzzing1.cnf}))))
(rule (action (with-stdout-to fuzzing1.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:fuzzing1.cnf}))))
(rule (alias runtest) (action (diff oracle fuzzing1.cnf.res)))
(rule (action (with-stdout-to fuzzing2.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:fuzzing2.cnf}))))
(rule (action (with-stdout-to fuzzing2.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:fuzzing2.cnf}))))
(rule (alias runtest) (action (diff oracle fuzzing2.cnf.res)))
(rule (action (with-stdout-to par8-1-c.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:par8-1-c.cnf}))))
(rule (action (with-stdout-to par8-1-c.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:par8-1-c.cnf}))))
(rule (alias runtest) (action (diff oracle par8-1-c.cnf.res)))
(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-2.cnf}))))
(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:pigeon-2.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-2.cnf.res)))
(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-3.cnf}))))
(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:pigeon-3.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-3.cnf.res)))
(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-4.cnf}))))
(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:pigeon-4.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-4.cnf.res)))
(rule (action (with-stdout-to quinn.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:quinn.cnf}))))
(rule (action (with-stdout-to quinn.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:quinn.cnf}))))
(rule (alias runtest) (action (diff oracle quinn.cnf.res)))
(rule (action (with-stdout-to simple_v3_c2.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:simple_v3_c2.cnf}))))
(rule (action (with-stdout-to simple_v3_c2.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:simple_v3_c2.cnf}))))
(rule (alias runtest) (action (diff oracle simple_v3_c2.cnf.res)))
src_colibri2/tests/solve/dimacs/unsat/dune.inc
+ 6
− 6
View file @ 28f1ab26
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:anomaly_agetooold.cnf}))))
(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:anomaly_agetooold.cnf}))))
(rule (alias runtest) (action (diff oracle anomaly_agetooold.cnf.res)))
(rule (action (with-stdout-to modus_ponens.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:modus_ponens.cnf}))))
(rule (action (with-stdout-to modus_ponens.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:modus_ponens.cnf}))))
(rule (alias runtest) (action (diff oracle modus_ponens.cnf.res)))
(rule (action (with-stdout-to pigeon-1.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-1.cnf}))))
(rule (action (with-stdout-to pigeon-1.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:pigeon-1.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-1.cnf.res)))
(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-2.cnf}))))
(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:pigeon-2.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-2.cnf.res)))
(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-3.cnf}))))
(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:pigeon-3.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-3.cnf.res)))
(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-step 3000 %{dep:pigeon-4.cnf}))))
(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-steps 3000 %{dep:pigeon-4.cnf}))))
(rule (alias runtest) (action (diff oracle pigeon-4.cnf.res)))
src_colibri2/tests/solve/smt_adt/sat/dune.inc
+ 6
− 6
View file @ 28f1ab26
(rule (action (with-stdout-to oracle (echo "sat\n"))))
(rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:enum.smt2}))))
(rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:enum.smt2}))))
(rule (alias runtest) (action (diff oracle enum.smt2.res)))
(rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list0.smt2}))))
(rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:list0.smt2}))))
(rule (alias runtest) (action (diff oracle list0.smt2.res)))
(rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list1.smt2}))))
(rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:list1.smt2}))))
(rule (alias runtest) (action (diff oracle list1.smt2.res)))
(rule (action (with-stdout-to tree1.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:tree1.smt2}))))
(rule (action (with-stdout-to tree1.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:tree1.smt2}))))
(rule (alias runtest) (action (diff oracle tree1.smt2.res)))
(rule (action (with-stdout-to tree2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:tree2.smt2}))))
(rule (action (with-stdout-to tree2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:tree2.smt2}))))
(rule (alias runtest) (action (diff oracle tree2.smt2.res)))
(rule (action (with-stdout-to tree3.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:tree3.smt2}))))
(rule (action (with-stdout-to tree3.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:tree3.smt2}))))
(rule (alias runtest) (action (diff oracle tree3.smt2.res)))
src_colibri2/tests/solve/smt_adt/unsat/dune.inc
+ 8
− 8
View file @ 28f1ab26
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
(rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:enum.smt2}))))
(rule (action (with-stdout-to enum.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:enum.smt2}))))
(rule (alias runtest) (action (diff oracle enum.smt2.res)))
(rule (action (with-stdout-to enum2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:enum2.smt2}))))
(rule (action (with-stdout-to enum2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:enum2.smt2}))))
(rule (alias runtest) (action (diff oracle enum2.smt2.res)))
(rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list0.smt2}))))
(rule (action (with-stdout-to list0.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:list0.smt2}))))
(rule (alias runtest) (action (diff oracle list0.smt2.res)))
(rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list1.smt2}))))
(rule (action (with-stdout-to list1.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:list1.smt2}))))
(rule (alias runtest) (action (diff oracle list1.smt2.res)))
(rule (action (with-stdout-to list2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list2.smt2}))))
(rule (action (with-stdout-to list2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:list2.smt2}))))
(rule (alias runtest) (action (diff oracle list2.smt2.res)))
(rule (action (with-stdout-to list3.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list3.smt2}))))
(rule (action (with-stdout-to list3.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:list3.smt2}))))
(rule (alias runtest) (action (diff oracle list3.smt2.res)))
(rule (action (with-stdout-to list4.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list4.smt2}))))
(rule (action (with-stdout-to list4.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:list4.smt2}))))
(rule (alias runtest) (action (diff oracle list4.smt2.res)))
(rule (action (with-stdout-to parlist0.psmt2.res (run %{bin:colibri2} --max-step 3000 %{dep:parlist0.psmt2}))))
(rule (action (with-stdout-to parlist0.psmt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:parlist0.psmt2}))))
(rule (alias runtest) (action (diff oracle parlist0.psmt2.res)))
src_colibri2/tests/solve/smt_lra/sat/dune.inc
+ 33
− 33
View file @ 28f1ab26
(rule (action (with-stdout-to oracle (echo "sat\n"))))
(rule (action (with-stdout-to arith_CombiRepr_normalize.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_CombiRepr_normalize.smt2}))))
(rule (action (with-stdout-to arith_CombiRepr_normalize.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_CombiRepr_normalize.smt2}))))
(rule (alias runtest) (action (diff oracle arith_CombiRepr_normalize.smt2.res)))
(rule (action (with-stdout-to arith_conflict_add_disequality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_conflict_add_disequality.smt2}))))
(rule (action (with-stdout-to arith_conflict_add_disequality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_conflict_add_disequality.smt2}))))
(rule (alias runtest) (action (diff oracle arith_conflict_add_disequality.smt2.res)))
(rule (action (with-stdout-to arith_conpoly.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_conpoly.smt2}))))
(rule (action (with-stdout-to arith_conpoly.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_conpoly.smt2}))))
(rule (alias runtest) (action (diff oracle arith_conpoly.smt2.res)))
(rule (action (with-stdout-to arith_decide_must_test_is_dis_equal.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_decide_must_test_is_dis_equal.smt2}))))
(rule (action (with-stdout-to arith_decide_must_test_is_dis_equal.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_decide_must_test_is_dis_equal.smt2}))))
(rule (alias runtest) (action (diff oracle arith_decide_must_test_is_dis_equal.smt2.res)))
(rule (action (with-stdout-to arith_init_always_merge_itself.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_init_always_merge_itself.smt2}))))
(rule (action (with-stdout-to arith_init_always_merge_itself.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_init_always_merge_itself.smt2}))))
(rule (alias runtest) (action (diff oracle arith_init_always_merge_itself.smt2.res)))
(rule (action (with-stdout-to arith_init_and_propa_must_be_ordered.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_init_and_propa_must_be_ordered.smt2}))))
(rule (action (with-stdout-to arith_init_and_propa_must_be_ordered.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_init_and_propa_must_be_ordered.smt2}))))
(rule (alias runtest) (action (diff oracle arith_init_and_propa_must_be_ordered.smt2.res)))
(rule (action (with-stdout-to arith_merge_case1.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_case1.smt2}))))
(rule (action (with-stdout-to arith_merge_case1.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_case1.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_case1.smt2.res)))
(rule (action (with-stdout-to arith_merge_case_4.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_case_4.smt2}))))
(rule (action (with-stdout-to arith_merge_case_4.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_case_4.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_case_4.smt2.res)))
(rule (action (with-stdout-to arith_merge_case_4_bis.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_case_4_bis.smt2}))))
(rule (action (with-stdout-to arith_merge_case_4_bis.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_case_4_bis.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_case_4_bis.smt2.res)))
(rule (action (with-stdout-to arith_merge_itself_coef_of_repr_is_one.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_itself_coef_of_repr_is_one.smt2}))))
(rule (action (with-stdout-to arith_merge_itself_coef_of_repr_is_one.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_itself_coef_of_repr_is_one.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_itself_coef_of_repr_is_one.smt2.res)))
(rule (action (with-stdout-to arith_merge_itself_last_case.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_itself_last_case.smt2}))))
(rule (action (with-stdout-to arith_merge_itself_last_case.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_itself_last_case.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_itself_last_case.smt2.res)))
(rule (action (with-stdout-to arith_merge_itself_pivot_not_in_p12.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_itself_pivot_not_in_p12.smt2}))))
(rule (action (with-stdout-to arith_merge_itself_pivot_not_in_p12.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_itself_pivot_not_in_p12.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_itself_pivot_not_in_p12.smt2.res)))
(rule (action (with-stdout-to arith_merge_must_use_find.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_must_use_find.smt2}))))
(rule (action (with-stdout-to arith_merge_must_use_find.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_must_use_find.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_must_use_find.smt2.res)))
(rule (action (with-stdout-to arith_mult_explication.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_mult_explication.smt2}))))
(rule (action (with-stdout-to arith_mult_explication.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_mult_explication.smt2}))))
(rule (alias runtest) (action (diff oracle arith_mult_explication.smt2.res)))
(rule (action (with-stdout-to arith_mult_not_linear_in_conflict.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_mult_not_linear_in_conflict.smt2}))))
(rule (action (with-stdout-to arith_mult_not_linear_in_conflict.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_mult_not_linear_in_conflict.smt2}))))
(rule (alias runtest) (action (diff oracle arith_mult_not_linear_in_conflict.smt2.res)))
(rule (action (with-stdout-to arith_normalize_use_find_def.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_normalize_use_find_def.smt2}))))
(rule (action (with-stdout-to arith_normalize_use_find_def.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_normalize_use_find_def.smt2}))))
(rule (alias runtest) (action (diff oracle arith_normalize_use_find_def.smt2.res)))
(rule (action (with-stdout-to arith_own_repr.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_own_repr.smt2}))))
(rule (action (with-stdout-to arith_own_repr.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_own_repr.smt2}))))
(rule (alias runtest) (action (diff oracle arith_own_repr.smt2.res)))
(rule (action (with-stdout-to arith_propacl.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_propacl.smt2}))))
(rule (action (with-stdout-to arith_propacl.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_propacl.smt2}))))
(rule (alias runtest) (action (diff oracle arith_propacl.smt2.res)))
(rule (action (with-stdout-to arith_subst_and_conflict_add.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_subst_and_conflict_add.smt2}))))
(rule (action (with-stdout-to arith_subst_and_conflict_add.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_subst_and_conflict_add.smt2}))))
(rule (alias runtest) (action (diff oracle arith_subst_and_conflict_add.smt2.res)))
(rule (action (with-stdout-to arith_zero_dom.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_zero_dom.smt2}))))
(rule (action (with-stdout-to arith_zero_dom.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_zero_dom.smt2}))))
(rule (alias runtest) (action (diff oracle arith_zero_dom.smt2.res)))
(rule (action (with-stdout-to attach_only_when_dom_present.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:attach_only_when_dom_present.smt2}))))
(rule (action (with-stdout-to attach_only_when_dom_present.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:attach_only_when_dom_present.smt2}))))
(rule (alias runtest) (action (diff oracle attach_only_when_dom_present.smt2.res)))
(rule (action (with-stdout-to init_not_repr.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:init_not_repr.smt2}))))
(rule (action (with-stdout-to init_not_repr.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:init_not_repr.smt2}))))
(rule (alias runtest) (action (diff oracle init_not_repr.smt2.res)))
(rule (action (with-stdout-to le.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:le.smt2}))))
(rule (action (with-stdout-to le.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:le.smt2}))))
(rule (alias runtest) (action (diff oracle le.smt2.res)))
(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:le2.smt2}))))
(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:le2.smt2}))))
(rule (alias runtest) (action (diff oracle le2.smt2.res)))
(rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul.smt2}))))
(rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul.smt2}))))
(rule (alias runtest) (action (diff oracle mul.smt2.res)))
(rule (action (with-stdout-to sem_invariant_in_learnt_dec.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:sem_invariant_in_learnt_dec.smt2}))))
(rule (action (with-stdout-to sem_invariant_in_learnt_dec.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:sem_invariant_in_learnt_dec.smt2}))))
(rule (alias runtest) (action (diff oracle sem_invariant_in_learnt_dec.smt2.res)))
(rule (action (with-stdout-to solver_add_pexp_cl.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_add_pexp_cl.smt2}))))
(rule (action (with-stdout-to solver_add_pexp_cl.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:solver_add_pexp_cl.smt2}))))
(rule (alias runtest) (action (diff oracle solver_add_pexp_cl.smt2.res)))
(rule (action (with-stdout-to solver_arith_homogeneous_dist_sign.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_arith_homogeneous_dist_sign.smt2}))))
(rule (action (with-stdout-to solver_arith_homogeneous_dist_sign.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:solver_arith_homogeneous_dist_sign.smt2}))))
(rule (alias runtest) (action (diff oracle solver_arith_homogeneous_dist_sign.smt2.res)))
(rule (action (with-stdout-to solver_merge_itself_repr_inside.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_merge_itself_repr_inside.smt2}))))
(rule (action (with-stdout-to solver_merge_itself_repr_inside.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:solver_merge_itself_repr_inside.smt2}))))
(rule (alias runtest) (action (diff oracle solver_merge_itself_repr_inside.smt2.res)))
(rule (action (with-stdout-to solver_set_pending_merge_expsameexp.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_set_pending_merge_expsameexp.smt2}))))
(rule (action (with-stdout-to solver_set_pending_merge_expsameexp.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:solver_set_pending_merge_expsameexp.smt2}))))
(rule (alias runtest) (action (diff oracle solver_set_pending_merge_expsameexp.smt2.res)))
(rule (action (with-stdout-to solver_subst_eventdom_find.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_subst_eventdom_find.smt2}))))
(rule (action (with-stdout-to solver_subst_eventdom_find.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:solver_subst_eventdom_find.smt2}))))
(rule (alias runtest) (action (diff oracle solver_subst_eventdom_find.smt2.res)))
(rule (action (with-stdout-to to_real.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:to_real.smt2}))))
(rule (action (with-stdout-to to_real.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:to_real.smt2}))))
(rule (alias runtest) (action (diff oracle to_real.smt2.res)))
(rule (action (with-stdout-to to_real2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:to_real2.smt2}))))
(rule (action (with-stdout-to to_real2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:to_real2.smt2}))))
(rule (alias runtest) (action (diff oracle to_real2.smt2.res)))
src_colibri2/tests/solve/smt_lra/unsat/dune.inc
+ 11
− 11
View file @ 28f1ab26
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
(rule (action (with-stdout-to arith_ExpMult_by_zero.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_ExpMult_by_zero.smt2}))))
(rule (action (with-stdout-to arith_ExpMult_by_zero.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_ExpMult_by_zero.smt2}))))
(rule (alias runtest) (action (diff oracle arith_ExpMult_by_zero.smt2.res)))
(rule (action (with-stdout-to arith_merge_case2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:arith_merge_case2.smt2}))))
(rule (action (with-stdout-to arith_merge_case2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:arith_merge_case2.smt2}))))
(rule (alias runtest) (action (diff oracle arith_merge_case2.smt2.res)))
(rule (action (with-stdout-to le.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:le.smt2}))))
(rule (action (with-stdout-to le.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:le.smt2}))))
(rule (alias runtest) (action (diff oracle le.smt2.res)))
(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:le2.smt2}))))
(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:le2.smt2}))))
(rule (alias runtest) (action (diff oracle le2.smt2.res)))
(rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul.smt2}))))
(rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul.smt2}))))
(rule (alias runtest) (action (diff oracle mul.smt2.res)))
(rule (action (with-stdout-to repr_and_poly.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:repr_and_poly.smt2}))))
(rule (action (with-stdout-to repr_and_poly.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:repr_and_poly.smt2}))))
(rule (alias runtest) (action (diff oracle repr_and_poly.smt2.res)))
(rule (action (with-stdout-to repr_fourier.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:repr_fourier.smt2}))))
(rule (action (with-stdout-to repr_fourier.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:repr_fourier.smt2}))))
(rule (alias runtest) (action (diff oracle repr_fourier.smt2.res)))
(rule (action (with-stdout-to solver_merge_itself_repr_empty.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_merge_itself_repr_empty.smt2}))))
(rule (action (with-stdout-to solver_merge_itself_repr_empty.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:solver_merge_itself_repr_empty.smt2}))))
(rule (alias runtest) (action (diff oracle solver_merge_itself_repr_empty.smt2.res)))
(rule (action (with-stdout-to solver_set_sem_merge_sign.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:solver_set_sem_merge_sign.smt2}))))
(rule (action (with-stdout-to solver_set_sem_merge_sign.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:solver_set_sem_merge_sign.smt2}))))
(rule (alias runtest) (action (diff oracle solver_set_sem_merge_sign.smt2.res)))
(rule (action (with-stdout-to to_real.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:to_real.smt2}))))
(rule (action (with-stdout-to to_real.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:to_real.smt2}))))
(rule (alias runtest) (action (diff oracle to_real.smt2.res)))
(rule (action (with-stdout-to to_real2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:to_real2.smt2}))))
(rule (action (with-stdout-to to_real2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:to_real2.smt2}))))
(rule (alias runtest) (action (diff oracle to_real2.smt2.res)))
src_colibri2/tests/solve/smt_nra/sat/dune.inc
+ 7
− 7
View file @ 28f1ab26
(rule (action (with-stdout-to oracle (echo "sat\n"))))
(rule (action (with-stdout-to ceil.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:ceil.smt2}))))
(rule (action (with-stdout-to ceil.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:ceil.smt2}))))
(rule (alias runtest) (action (diff oracle ceil.smt2.res)))
(rule (action (with-stdout-to div_pos.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:div_pos.smt2}))))
(rule (action (with-stdout-to div_pos.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:div_pos.smt2}))))
(rule (alias runtest) (action (diff oracle div_pos.smt2.res)))
(rule (action (with-stdout-to div_pos_lt.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:div_pos_lt.smt2}))))
(rule (action (with-stdout-to div_pos_lt.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:div_pos_lt.smt2}))))
(rule (alias runtest) (action (diff oracle div_pos_lt.smt2.res)))
(rule (action (with-stdout-to mul_commut.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_commut.smt2}))))
(rule (action (with-stdout-to mul_commut.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_commut.smt2}))))
(rule (alias runtest) (action (diff oracle mul_commut.smt2.res)))
(rule (action (with-stdout-to mul_commut2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_commut2.smt2}))))
(rule (action (with-stdout-to mul_commut2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_commut2.smt2}))))
(rule (alias runtest) (action (diff oracle mul_commut2.smt2.res)))
(rule (action (with-stdout-to mul_pos.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_pos.smt2}))))
(rule (action (with-stdout-to mul_pos.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_pos.smt2}))))
(rule (alias runtest) (action (diff oracle mul_pos.smt2.res)))
(rule (action (with-stdout-to mul_pos_lt.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_pos_lt.smt2}))))
(rule (action (with-stdout-to mul_pos_lt.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_pos_lt.smt2}))))
(rule (alias runtest) (action (diff oracle mul_pos_lt.smt2.res)))
src_colibri2/tests/solve/smt_nra/unsat/dune.inc
+ 10
− 10
View file @ 28f1ab26
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
(rule (action (with-stdout-to ceil.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:ceil.smt2}))))
(rule (action (with-stdout-to ceil.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:ceil.smt2}))))
(rule (alias runtest) (action (diff oracle ceil.smt2.res)))
(rule (action (with-stdout-to div_pos.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:div_pos.smt2}))))
(rule (action (with-stdout-to div_pos.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:div_pos.smt2}))))
(rule (alias runtest) (action (diff oracle div_pos.smt2.res)))
(rule (action (with-stdout-to div_pos_lt.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:div_pos_lt.smt2}))))
(rule (action (with-stdout-to div_pos_lt.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:div_pos_lt.smt2}))))
(rule (alias runtest) (action (diff oracle div_pos_lt.smt2.res)))
(rule (action (with-stdout-to div_pos_lt_to_real.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:div_pos_lt_to_real.smt2}))))
(rule (action (with-stdout-to div_pos_lt_to_real.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:div_pos_lt_to_real.smt2}))))
(rule (alias runtest) (action (diff oracle div_pos_lt_to_real.smt2.res)))
(rule (action (with-stdout-to floor.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:floor.smt2}))))
(rule (action (with-stdout-to floor.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:floor.smt2}))))
(rule (alias runtest) (action (diff oracle floor.smt2.res)))
(rule (action (with-stdout-to mul_commut.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_commut.smt2}))))
(rule (action (with-stdout-to mul_commut.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_commut.smt2}))))
(rule (alias runtest) (action (diff oracle mul_commut.smt2.res)))
(rule (action (with-stdout-to mul_commut2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_commut2.smt2}))))
(rule (action (with-stdout-to mul_commut2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_commut2.smt2}))))
(rule (alias runtest) (action (diff oracle mul_commut2.smt2.res)))
(rule (action (with-stdout-to mul_pos.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_pos.smt2}))))
(rule (action (with-stdout-to mul_pos.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_pos.smt2}))))
(rule (alias runtest) (action (diff oracle mul_pos.smt2.res)))
(rule (action (with-stdout-to mul_pos_lt.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_pos_lt.smt2}))))
(rule (action (with-stdout-to mul_pos_lt.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_pos_lt.smt2}))))
(rule (alias runtest) (action (diff oracle mul_pos_lt.smt2.res)))
(rule (action (with-stdout-to mul_pos_zero_le.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:mul_pos_zero_le.smt2}))))
(rule (action (with-stdout-to mul_pos_zero_le.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:mul_pos_zero_le.smt2}))))
(rule (alias runtest) (action (diff oracle mul_pos_zero_le.smt2.res)))
src_colibri2/tests/solve/smt_quant/sat/dune.inc
+ 4
− 4
View file @ 28f1ab26
(rule (action (with-stdout-to oracle (echo "sat\n"))))
(rule (action (with-stdout-to exists.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:exists.smt2}))))
(rule (action (with-stdout-to exists.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:exists.smt2}))))
(rule (alias runtest) (action (diff oracle exists.smt2.res)))
(rule (action (with-stdout-to forall0.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall0.smt2}))))
(rule (action (with-stdout-to forall0.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall0.smt2}))))
(rule (alias runtest) (action (diff oracle forall0.smt2.res)))
(rule (action (with-stdout-to forall3.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall3.smt2}))))
(rule (action (with-stdout-to forall3.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall3.smt2}))))
(rule (alias runtest) (action (diff oracle forall3.smt2.res)))
(rule (action (with-stdout-to forall4.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall4.smt2}))))
(rule (action (with-stdout-to forall4.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall4.smt2}))))
(rule (alias runtest) (action (diff oracle forall4.smt2.res)))
src_colibri2/tests/solve/smt_quant/unsat/dune.inc
+ 11
− 11
View file @ 28f1ab26
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
(rule (action (with-stdout-to exists.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:exists.smt2}))))
(rule (action (with-stdout-to exists.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:exists.smt2}))))
(rule (alias runtest) (action (diff oracle exists.smt2.res)))
(rule (action (with-stdout-to exists2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:exists2.smt2}))))
(rule (action (with-stdout-to exists2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:exists2.smt2}))))
(rule (alias runtest) (action (diff oracle exists2.smt2.res)))
(rule (action (with-stdout-to forall0.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall0.smt2}))))
(rule (action (with-stdout-to forall0.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall0.smt2}))))
(rule (alias runtest) (action (diff oracle forall0.smt2.res)))
(rule (action (with-stdout-to forall1.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall1.smt2}))))
(rule (action (with-stdout-to forall1.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall1.smt2}))))
(rule (alias runtest) (action (diff oracle forall1.smt2.res)))
(rule (action (with-stdout-to forall2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall2.smt2}))))
(rule (action (with-stdout-to forall2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall2.smt2}))))
(rule (alias runtest) (action (diff oracle forall2.smt2.res)))
(rule (action (with-stdout-to forall3.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall3.smt2}))))
(rule (action (with-stdout-to forall3.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall3.smt2}))))
(rule (alias runtest) (action (diff oracle forall3.smt2.res)))
(rule (action (with-stdout-to forall4.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall4.smt2}))))
(rule (action (with-stdout-to forall4.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall4.smt2}))))
(rule (alias runtest) (action (diff oracle forall4.smt2.res)))
(rule (action (with-stdout-to forall5.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall5.smt2}))))
(rule (action (with-stdout-to forall5.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall5.smt2}))))
(rule (alias runtest) (action (diff oracle forall5.smt2.res)))
(rule (action (with-stdout-to forall6.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall6.smt2}))))
(rule (action (with-stdout-to forall6.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall6.smt2}))))
(rule (alias runtest) (action (diff oracle forall6.smt2.res)))
(rule (action (with-stdout-to forall7.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall7.smt2}))))
(rule (action (with-stdout-to forall7.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall7.smt2}))))
(rule (alias runtest) (action (diff oracle forall7.smt2.res)))
(rule (action (with-stdout-to forall8.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:forall8.smt2}))))
(rule (action (with-stdout-to forall8.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:forall8.smt2}))))
(rule (alias runtest) (action (diff oracle forall8.smt2.res)))
src_colibri2/tests/solve/smt_uf/sat/dune.inc
+ 21
− 21
View file @ 28f1ab26
(rule (action (with-stdout-to oracle (echo "sat\n"))))
(rule (action (with-stdout-to bad_conflict.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:bad_conflict.smt2}))))
(rule (action (with-stdout-to bad_conflict.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:bad_conflict.smt2}))))
(rule (alias runtest) (action (diff oracle bad_conflict.smt2.res)))
(rule (action (with-stdout-to bcp_dont_like_duplicate.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:bcp_dont_like_duplicate.smt2}))))
(rule (action (with-stdout-to bcp_dont_like_duplicate.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:bcp_dont_like_duplicate.smt2}))))
(rule (alias runtest) (action (diff oracle bcp_dont_like_duplicate.smt2.res)))
(rule (action (with-stdout-to bool_not_propa.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:bool_not_propa.smt2}))))
(rule (action (with-stdout-to bool_not_propa.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:bool_not_propa.smt2}))))
(rule (alias runtest) (action (diff oracle bool_not_propa.smt2.res)))
(rule (action (with-stdout-to boolexpup.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:boolexpup.smt2}))))
(rule (action (with-stdout-to boolexpup.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:boolexpup.smt2}))))
(rule (alias runtest) (action (diff oracle boolexpup.smt2.res)))
(rule (action (with-stdout-to clause_normalization.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:clause_normalization.smt2}))))
(rule (action (with-stdout-to clause_normalization.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:clause_normalization.smt2}))))
(rule (alias runtest) (action (diff oracle clause_normalization.smt2.res)))
(rule (action (with-stdout-to clmerge.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:clmerge.smt2}))))
(rule (action (with-stdout-to clmerge.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:clmerge.smt2}))))
(rule (alias runtest) (action (diff oracle clmerge.smt2.res)))
(rule (action (with-stdout-to conflict_complete_needed_cl.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:conflict_complete_needed_cl.smt2}))))
(rule (action (with-stdout-to conflict_complete_needed_cl.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:conflict_complete_needed_cl.smt2}))))
(rule (alias runtest) (action (diff oracle conflict_complete_needed_cl.smt2.res)))
(rule (action (with-stdout-to directdom_not.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:directdom_not.smt2}))))
(rule (action (with-stdout-to directdom_not.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:directdom_not.smt2}))))
(rule (alias runtest) (action (diff oracle directdom_not.smt2.res)))
(rule (action (with-stdout-to dis_dom_before_first_age.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:dis_dom_before_first_age.smt2}))))
(rule (action (with-stdout-to dis_dom_before_first_age.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:dis_dom_before_first_age.smt2}))))
(rule (alias runtest) (action (diff oracle dis_dom_before_first_age.smt2.res)))
(rule (action (with-stdout-to dom_merge_equality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:dom_merge_equality.smt2}))))
(rule (action (with-stdout-to dom_merge_equality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:dom_merge_equality.smt2}))))
(rule (alias runtest) (action (diff oracle dom_merge_equality.smt2.res)))
(rule (action (with-stdout-to equality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:equality.smt2}))))
(rule (action (with-stdout-to equality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:equality.smt2}))))
(rule (alias runtest) (action (diff oracle equality.smt2.res)))
(rule (action (with-stdout-to equality_condis.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:equality_condis.smt2}))))
(rule (action (with-stdout-to equality_condis.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:equality_condis.smt2}))))
(rule (alias runtest) (action (diff oracle equality_condis.smt2.res)))
(rule (action (with-stdout-to equality_get_sem.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:equality_get_sem.smt2}))))
(rule (action (with-stdout-to equality_get_sem.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:equality_get_sem.smt2}))))
(rule (alias runtest) (action (diff oracle equality_get_sem.smt2.res)))
(rule (action (with-stdout-to exp_sem_equality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:exp_sem_equality.smt2}))))
(rule (action (with-stdout-to exp_sem_equality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:exp_sem_equality.smt2}))))
(rule (alias runtest) (action (diff oracle exp_sem_equality.smt2.res)))
(rule (action (with-stdout-to explimit_cl_equality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:explimit_cl_equality.smt2}))))
(rule (action (with-stdout-to explimit_cl_equality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:explimit_cl_equality.smt2}))))
(rule (alias runtest) (action (diff oracle explimit_cl_equality.smt2.res)))
(rule (action (with-stdout-to implication.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:implication.smt2}))))
(rule (action (with-stdout-to implication.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:implication.smt2}))))
(rule (alias runtest) (action (diff oracle implication.smt2.res)))
(rule (action (with-stdout-to intmap_set_disjoint.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:intmap_set_disjoint.smt2}))))
(rule (action (with-stdout-to intmap_set_disjoint.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:intmap_set_disjoint.smt2}))))
(rule (alias runtest) (action (diff oracle intmap_set_disjoint.smt2.res)))
(rule (action (with-stdout-to is_equal_not_propagated.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:is_equal_not_propagated.smt2}))))
(rule (action (with-stdout-to is_equal_not_propagated.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:is_equal_not_propagated.smt2}))))
(rule (alias runtest) (action (diff oracle is_equal_not_propagated.smt2.res)))
(rule (action (with-stdout-to ite_sem_bool.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:ite_sem_bool.smt2}))))
(rule (action (with-stdout-to ite_sem_bool.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:ite_sem_bool.smt2}))))
(rule (alias runtest) (action (diff oracle ite_sem_bool.smt2.res)))
(rule (action (with-stdout-to polyeq_genequality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:polyeq_genequality.smt2}))))
(rule (action (with-stdout-to polyeq_genequality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:polyeq_genequality.smt2}))))
(rule (alias runtest) (action (diff oracle polyeq_genequality.smt2.res)))
(rule (action (with-stdout-to substupfalse_equality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:substupfalse_equality.smt2}))))
(rule (action (with-stdout-to substupfalse_equality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:substupfalse_equality.smt2}))))
(rule (alias runtest) (action (diff oracle substupfalse_equality.smt2.res)))
src_colibri2/tests/solve/smt_uf/unsat/dune.inc
+ 13
− 13
View file @ 28f1ab26
(rule (action (with-stdout-to oracle (echo "unsat\n"))))
(rule (action (with-stdout-to NEQ004_size4__decide_eq_us.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:NEQ004_size4__decide_eq_us.smt2}))))
(rule (action (with-stdout-to NEQ004_size4__decide_eq_us.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:NEQ004_size4__decide_eq_us.smt2}))))
(rule (alias runtest) (action (diff oracle NEQ004_size4__decide_eq_us.smt2.res)))
(rule (action (with-stdout-to deltaed0.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:deltaed0.smt2}))))
(rule (action (with-stdout-to deltaed0.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:deltaed0.smt2}))))
(rule (alias runtest) (action (diff oracle deltaed0.smt2.res)))
(rule (action (with-stdout-to diff_to_value_for_bool.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:diff_to_value_for_bool.smt2}))))
(rule (action (with-stdout-to diff_to_value_for_bool.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:diff_to_value_for_bool.smt2}))))
(rule (alias runtest) (action (diff oracle diff_to_value_for_bool.smt2.res)))
(rule (action (with-stdout-to diff_value_substupfalse.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:diff_value_substupfalse.smt2}))))
(rule (action (with-stdout-to diff_value_substupfalse.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:diff_value_substupfalse.smt2}))))
(rule (alias runtest) (action (diff oracle diff_value_substupfalse.smt2.res)))
(rule (action (with-stdout-to distinct.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:distinct.smt2}))))
(rule (action (with-stdout-to distinct.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:distinct.smt2}))))
(rule (alias runtest) (action (diff oracle distinct.smt2.res)))
(rule (action (with-stdout-to eq_diamond2.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:eq_diamond2.smt2}))))
(rule (action (with-stdout-to eq_diamond2.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:eq_diamond2.smt2}))))
(rule (alias runtest) (action (diff oracle eq_diamond2.smt2.res)))
(rule (action (with-stdout-to equality_norm_set.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:equality_norm_set.smt2}))))
(rule (action (with-stdout-to equality_norm_set.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:equality_norm_set.smt2}))))
(rule (alias runtest) (action (diff oracle equality_norm_set.smt2.res)))
(rule (action (with-stdout-to fundef.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:fundef.smt2}))))
(rule (action (with-stdout-to fundef.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:fundef.smt2}))))
(rule (alias runtest) (action (diff oracle fundef.smt2.res)))
(rule (action (with-stdout-to get_repr_at__instead_of__equal_CRepr.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:get_repr_at__instead_of__equal_CRepr.smt2}))))
(rule (action (with-stdout-to get_repr_at__instead_of__equal_CRepr.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:get_repr_at__instead_of__equal_CRepr.smt2}))))
(rule (alias runtest) (action (diff oracle get_repr_at__instead_of__equal_CRepr.smt2.res)))
(rule (action (with-stdout-to many_distinct.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:many_distinct.smt2}))))
(rule (action (with-stdout-to many_distinct.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:many_distinct.smt2}))))
(rule (alias runtest) (action (diff oracle many_distinct.smt2.res)))
(rule (action (with-stdout-to polyeq_genequality.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:polyeq_genequality.smt2}))))
(rule (action (with-stdout-to polyeq_genequality.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:polyeq_genequality.smt2}))))
(rule (alias runtest) (action (diff oracle polyeq_genequality.smt2.res)))
(rule (action (with-stdout-to polyeq_genequality_deltaed.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:polyeq_genequality_deltaed.smt2}))))
(rule (action (with-stdout-to polyeq_genequality_deltaed.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:polyeq_genequality_deltaed.smt2}))))
(rule (alias runtest) (action (diff oracle polyeq_genequality_deltaed.smt2.res)))
(rule (action (with-stdout-to xor.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:xor.smt2}))))
(rule (action (with-stdout-to xor.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:xor.smt2}))))
(rule (alias runtest) (action (diff oracle xor.smt2.res)))
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment