equal
deleted
inserted
replaced
49 in |
49 in |
50 |
50 |
51 val cvc3: SMT2_Solver.solver_config = { |
51 val cvc3: SMT2_Solver.solver_config = { |
52 name = "cvc3", |
52 name = "cvc3", |
53 class = K SMTLIB2_Interface.smtlib2C, |
53 class = K SMTLIB2_Interface.smtlib2C, |
54 avail = make_avail "CVC3_NEW", |
54 avail = make_avail "CVC3", |
55 command = make_command "CVC3_NEW", |
55 command = make_command "CVC3", |
56 options = cvc3_options, |
56 options = cvc3_options, |
57 default_max_relevant = 400 (* FUDGE *), |
57 default_max_relevant = 400 (* FUDGE *), |
58 outcome = on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."), |
58 outcome = on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."), |
59 parse_proof = NONE, |
59 parse_proof = NONE, |
60 replay = NONE } |
60 replay = NONE } |
65 (* Yices *) |
65 (* Yices *) |
66 |
66 |
67 val yices: SMT2_Solver.solver_config = { |
67 val yices: SMT2_Solver.solver_config = { |
68 name = "yices", |
68 name = "yices", |
69 class = K SMTLIB2_Interface.smtlib2C, |
69 class = K SMTLIB2_Interface.smtlib2C, |
70 avail = make_avail "YICES_NEW", |
70 avail = make_avail "YICES", |
71 command = make_command "YICES_NEW", |
71 command = make_command "YICES", |
72 options = (fn ctxt => [ |
72 options = (fn ctxt => [ |
73 "--rand-seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed), |
73 "--rand-seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed), |
74 "--timeout=" ^ |
74 "--timeout=" ^ |
75 string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)), |
75 string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)), |
76 "--smtlib"]), |
76 "--smtlib"]), |