diff options
Diffstat (limited to 'src/extraction/test.ml')
| -rw-r--r-- | src/extraction/test.ml | 89 |
1 files changed, 47 insertions, 42 deletions
diff --git a/src/extraction/test.ml b/src/extraction/test.ml index 2444a23..459ca8f 100644 --- a/src/extraction/test.ml +++ b/src/extraction/test.ml @@ -10,45 +10,50 @@ (**************************************************************************) -let _ = Printf.printf "Zchaff_checker.checker \"tests/sat1.cnf\" \"tests/sat1.zlog\" = %b\n" (Zchaff_checker.checker "tests/sat1.cnf" "tests/sat1.zlog") -let _ = Printf.printf "Zchaff_checker.checker \"tests/sat2.cnf\" \"tests/sat2.zlog\" = %b\n" (Zchaff_checker.checker "tests/sat2.cnf" "tests/sat2.zlog") -let _ = Printf.printf "Zchaff_checker.checker \"tests/sat3.cnf\" \"tests/sat3.zlog\" = %b\n" (Zchaff_checker.checker "tests/sat3.cnf" "tests/sat3.zlog") -let _ = Printf.printf "Zchaff_checker.checker \"tests/sat5.cnf\" \"tests/sat5.zlog\" = %b\n" (Zchaff_checker.checker "tests/sat5.cnf" "tests/sat5.zlog") -let _ = Printf.printf "Zchaff_checker.checker \"tests/sat6.cnf\" \"tests/sat6.zlog\" = %b\n" (Zchaff_checker.checker "tests/sat6.cnf" "tests/sat6.zlog") -let _ = Printf.printf "Zchaff_checker.checker \"tests/sat7.cnf\" \"tests/sat7.zlog\" = %b\n" (Zchaff_checker.checker "tests/sat7.cnf" "tests/sat7.zlog") -let _ = Printf.printf "Zchaff_checker.checker \"tests/hole4.cnf\" \"tests/hole4.zlog\" = %b\n" (Zchaff_checker.checker "tests/hole4.cnf" "tests/hole4.zlog") -let _ = Printf.printf "Zchaff_checker.checker \"tests/cmu-bmc-barrel6.cnf\" \"tests/cmu-bmc-barrel6.zlog\" = %b\n" (Zchaff_checker.checker "tests/cmu-bmc-barrel6.cnf" "tests/cmu-bmc-barrel6.zlog") -let _ = Printf.printf "Zchaff_checker.checker \"tests/velev-sss-1.0-05.cnf\" \"tests/velev-sss-1.0-05.zlog\" = %b\n" (Zchaff_checker.checker "tests/velev-sss-1.0-05.cnf" "tests/velev-sss-1.0-05.zlog") - - - - -let _ = Printf.printf "Verit_checker.checker \"tests/sat1.smt2\" \"tests/sat1.vtlog\" = %b\n" (Verit_checker.checker "tests/sat1.smt2" "tests/sat1.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/sat2.smt2\" \"tests/sat2.vtlog\" = %b\n" (Verit_checker.checker "tests/sat2.smt2" "tests/sat2.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/sat3.smt2\" \"tests/sat3.vtlog\" = %b\n" (Verit_checker.checker "tests/sat3.smt2" "tests/sat3.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/sat4.smt2\" \"tests/sat4.vtlog\" = %b\n" (Verit_checker.checker "tests/sat4.smt2" "tests/sat4.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/sat5.smt2\" \"tests/sat5.vtlog\" = %b\n" (Verit_checker.checker "tests/sat5.smt2" "tests/sat5.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/sat6.smt2\" \"tests/sat6.vtlog\" = %b\n" (Verit_checker.checker "tests/sat6.smt2" "tests/sat6.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/sat7.smt2\" \"tests/sat7.vtlog\" = %b\n" (Verit_checker.checker "tests/sat7.smt2" "tests/sat7.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/sat8.smt2\" \"tests/sat8.vtlog\" = %b\n" (Verit_checker.checker "tests/sat8.smt2" "tests/sat8.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/sat9.smt2\" \"tests/sat9.vtlog\" = %b\n" (Verit_checker.checker "tests/sat9.smt2" "tests/sat9.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/sat11.smt2\" \"tests/sat11.vtlog\" = %b\n" (Verit_checker.checker "tests/sat11.smt2" "tests/sat11.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/sat12.smt2\" \"tests/sat12.vtlog\" = %b\n" (Verit_checker.checker "tests/sat12.smt2" "tests/sat12.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/sat13.smt2\" \"tests/sat13.vtlog\" = %b\n" (Verit_checker.checker "tests/sat13.smt2" "tests/sat13.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/hole4.smt2\" \"tests/hole4.vtlog\" = %b\n" (Verit_checker.checker "tests/hole4.smt2" "tests/hole4.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/uf1.smt2\" \"tests/uf1.vtlog\" = %b\n" (Verit_checker.checker "tests/uf1.smt2" "tests/uf1.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/uf2.smt2\" \"tests/uf2.vtlog\" = %b\n" (Verit_checker.checker "tests/uf2.smt2" "tests/uf2.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/uf3.smt2\" \"tests/uf3.vtlog\" = %b\n" (Verit_checker.checker "tests/uf3.smt2" "tests/uf3.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/uf4.smt2\" \"tests/uf4.vtlog\" = %b\n" (Verit_checker.checker "tests/uf4.smt2" "tests/uf4.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/uf5.smt2\" \"tests/uf5.vtlog\" = %b\n" (Verit_checker.checker "tests/uf5.smt2" "tests/uf5.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/uf6.smt2\" \"tests/uf6.vtlog\" = %b\n" (Verit_checker.checker "tests/uf6.smt2" "tests/uf6.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/uf7.smt2\" \"tests/uf7.vtlog\" = %b\n" (Verit_checker.checker "tests/uf7.smt2" "tests/uf7.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/lia1.smt2\" \"tests/lia1.vtlog\" = %b\n" (Verit_checker.checker "tests/lia1.smt2" "tests/lia1.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/lia2.smt2\" \"tests/lia2.vtlog\" = %b\n" (Verit_checker.checker "tests/lia2.smt2" "tests/lia2.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/lia3.smt2\" \"tests/lia3.vtlog\" = %b\n" (Verit_checker.checker "tests/lia3.smt2" "tests/lia3.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/lia4.smt2\" \"tests/lia4.vtlog\" = %b\n" (Verit_checker.checker "tests/lia4.smt2" "tests/lia4.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/lia5.smt2\" \"tests/lia5.vtlog\" = %b\n" (Verit_checker.checker "tests/lia5.smt2" "tests/lia5.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/lia6.smt2\" \"tests/lia6.vtlog\" = %b\n" (Verit_checker.checker "tests/lia6.smt2" "tests/lia6.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/lia7.smt2\" \"tests/lia7.vtlog\" = %b\n" (Verit_checker.checker "tests/lia7.smt2" "tests/lia7.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/let1.smt2\" \"tests/let1.vtlog\" = %b\n" (Verit_checker.checker "tests/let1.smt2" "tests/let1.vtlog") -let _ = Printf.printf "Verit_checker.checker \"tests/let2.smt2\" \"tests/let2.vtlog\" = %b\n" (Verit_checker.checker "tests/let2.smt2" "tests/let2.vtlog") +open Smtcoq_extr + + +let _ = Printf.printf "Zchaff_checker.checker \"../../unit-tests/sat1.cnf\" \"../../unit-tests/sat1.zlog\" = %b\n" (Zchaff_checker.checker "../../unit-tests/sat1.cnf" "../../unit-tests/sat1.zlog") +let _ = Printf.printf "Zchaff_checker.checker \"../../unit-tests/sat2.cnf\" \"../../unit-tests/sat2.zlog\" = %b\n" (Zchaff_checker.checker "../../unit-tests/sat2.cnf" "../../unit-tests/sat2.zlog") +let _ = Printf.printf "Zchaff_checker.checker \"../../unit-tests/sat3.cnf\" \"../../unit-tests/sat3.zlog\" = %b\n" (Zchaff_checker.checker "../../unit-tests/sat3.cnf" "../../unit-tests/sat3.zlog") +let _ = Printf.printf "Zchaff_checker.checker \"../../unit-tests/sat5.cnf\" \"../../unit-tests/sat5.zlog\" = %b\n" (Zchaff_checker.checker "../../unit-tests/sat5.cnf" "../../unit-tests/sat5.zlog") +let _ = Printf.printf "Zchaff_checker.checker \"../../unit-tests/sat6.cnf\" \"../../unit-tests/sat6.zlog\" = %b\n" (Zchaff_checker.checker "../../unit-tests/sat6.cnf" "../../unit-tests/sat6.zlog") +let _ = Printf.printf "Zchaff_checker.checker \"../../unit-tests/sat7.cnf\" \"../../unit-tests/sat7.zlog\" = %b\n" (Zchaff_checker.checker "../../unit-tests/sat7.cnf" "../../unit-tests/sat7.zlog") +let _ = Printf.printf "Zchaff_checker.checker \"../../unit-tests/hole4.cnf\" \"../../unit-tests/hole4.zlog\" = %b\n" (Zchaff_checker.checker "../../unit-tests/hole4.cnf" "../../unit-tests/hole4.zlog") +let _ = Printf.printf "Zchaff_checker.checker \"../../unit-tests/cmu-bmc-barrel6.cnf\" \"../../unit-tests/cmu-bmc-barrel6.zlog\" = %b\n" (Zchaff_checker.checker "../../unit-tests/cmu-bmc-barrel6.cnf" "../../unit-tests/cmu-bmc-barrel6.zlog") +let _ = Printf.printf "Zchaff_checker.checker \"../../unit-tests/velev-sss-1.0-05.cnf\" \"../../unit-tests/velev-sss-1.0-05.zlog\" = %b\n" (Zchaff_checker.checker "../../unit-tests/velev-sss-1.0-05.cnf" "../../unit-tests/velev-sss-1.0-05.zlog") + + + + +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat0.smt2\" \"../../unit-tests/sat0.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat0.smt2" "../../unit-tests/sat0.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat1.smt2\" \"../../unit-tests/sat1.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat1.smt2" "../../unit-tests/sat1.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat2.smt2\" \"../../unit-tests/sat2.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat2.smt2" "../../unit-tests/sat2.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat3.smt2\" \"../../unit-tests/sat3.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat3.smt2" "../../unit-tests/sat3.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat4.smt2\" \"../../unit-tests/sat4.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat4.smt2" "../../unit-tests/sat4.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat5.smt2\" \"../../unit-tests/sat5.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat5.smt2" "../../unit-tests/sat5.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat6.smt2\" \"../../unit-tests/sat6.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat6.smt2" "../../unit-tests/sat6.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat7.smt2\" \"../../unit-tests/sat7.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat7.smt2" "../../unit-tests/sat7.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat8.smt2\" \"../../unit-tests/sat8.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat8.smt2" "../../unit-tests/sat8.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat9.smt2\" \"../../unit-tests/sat9.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat9.smt2" "../../unit-tests/sat9.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat11.smt2\" \"../../unit-tests/sat11.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat11.smt2" "../../unit-tests/sat11.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat12.smt2\" \"../../unit-tests/sat12.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat12.smt2" "../../unit-tests/sat12.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat13.smt2\" \"../../unit-tests/sat13.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat13.smt2" "../../unit-tests/sat13.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat14.smt2\" \"../../unit-tests/sat14.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat14.smt2" "../../unit-tests/sat14.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/hole4.smt2\" \"../../unit-tests/hole4.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/hole4.smt2" "../../unit-tests/hole4.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/uf1.smt2\" \"../../unit-tests/uf1.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/uf1.smt2" "../../unit-tests/uf1.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/uf2.smt2\" \"../../unit-tests/uf2.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/uf2.smt2" "../../unit-tests/uf2.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/uf3.smt2\" \"../../unit-tests/uf3.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/uf3.smt2" "../../unit-tests/uf3.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/uf4.smt2\" \"../../unit-tests/uf4.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/uf4.smt2" "../../unit-tests/uf4.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/uf5.smt2\" \"../../unit-tests/uf5.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/uf5.smt2" "../../unit-tests/uf5.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/uf6.smt2\" \"../../unit-tests/uf6.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/uf6.smt2" "../../unit-tests/uf6.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/uf7.smt2\" \"../../unit-tests/uf7.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/uf7.smt2" "../../unit-tests/uf7.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/lia1.smt2\" \"../../unit-tests/lia1.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/lia1.smt2" "../../unit-tests/lia1.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/lia2.smt2\" \"../../unit-tests/lia2.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/lia2.smt2" "../../unit-tests/lia2.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/lia3.smt2\" \"../../unit-tests/lia3.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/lia3.smt2" "../../unit-tests/lia3.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/lia4.smt2\" \"../../unit-tests/lia4.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/lia4.smt2" "../../unit-tests/lia4.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/lia5.smt2\" \"../../unit-tests/lia5.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/lia5.smt2" "../../unit-tests/lia5.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/lia6.smt2\" \"../../unit-tests/lia6.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/lia6.smt2" "../../unit-tests/lia6.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/lia7.smt2\" \"../../unit-tests/lia7.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/lia7.smt2" "../../unit-tests/lia7.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/let1.smt2\" \"../../unit-tests/let1.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/let1.smt2" "../../unit-tests/let1.vtlog") +let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/let2.smt2\" \"../../unit-tests/let2.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/let2.smt2" "../../unit-tests/let2.vtlog") |