94 command = make_command "CVC4", |
94 command = make_command "CVC4", |
95 options = cvc4_options, |
95 options = cvc4_options, |
96 smt_options = [(":produce-unsat-cores", "true")], |
96 smt_options = [(":produce-unsat-cores", "true")], |
97 good_slices = |
97 good_slices = |
98 (* FUDGE *) |
98 (* FUDGE *) |
99 [(512, meshN), |
99 [((512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]), |
100 (64, meshN), |
100 ((64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]), |
101 (1024, meshN), |
101 ((1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]), |
102 (256, mepoN), |
102 ((256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]), |
103 (32, meshN), |
103 ((32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]), |
104 (128, meshN)], |
104 ((128, meshN), ["--no-e-matching", "--full-saturate-quant"]), |
|
105 ((256, meshN), ["--finite-model-find", "--fmf-inst-engine"])], |
105 outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"), |
106 outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"), |
106 parse_proof = SOME (K CVC4_Proof_Parse.parse_proof), |
107 parse_proof = SOME (K CVC4_Proof_Parse.parse_proof), |
107 replay = NONE } |
108 replay = NONE } |
108 |
109 |
109 end |
110 end |
138 command = the o check_tool "ISABELLE_VERIT", |
139 command = the o check_tool "ISABELLE_VERIT", |
139 options = veriT_options, |
140 options = veriT_options, |
140 smt_options = [(":produce-proofs", "true")], |
141 smt_options = [(":produce-proofs", "true")], |
141 good_slices = |
142 good_slices = |
142 (* FUDGE *) |
143 (* FUDGE *) |
143 [(1024, meshN), |
144 [((1024, meshN), []), |
144 (512, mashN), |
145 ((512, mashN), []), |
145 (64, meshN), |
146 ((64, meshN), []), |
146 (128, meshN), |
147 ((128, meshN), []), |
147 (256, mepoN), |
148 ((256, mepoN), []), |
148 (32, meshN)], |
149 ((32, meshN), [])], |
149 outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "Time limit exceeded"), |
150 outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "Time limit exceeded"), |
150 parse_proof = SOME (K VeriT_Proof_Parse.parse_proof), |
151 parse_proof = SOME (K VeriT_Proof_Parse.parse_proof), |
151 replay = SOME Verit_Replay.replay } |
152 replay = SOME Verit_Replay.replay } |
152 |
153 |
153 end |
154 end |
179 command = make_command "Z3", |
180 command = make_command "Z3", |
180 options = z3_options, |
181 options = z3_options, |
181 smt_options = [(":produce-proofs", "true")], |
182 smt_options = [(":produce-proofs", "true")], |
182 good_slices = |
183 good_slices = |
183 (* FUDGE *) |
184 (* FUDGE *) |
184 [(1024, meshN), |
185 [((1024, meshN), []), |
185 (512, mepoN), |
186 ((512, mepoN), []), |
186 (64, meshN), |
187 ((64, meshN), []), |
187 (256, meshN), |
188 ((256, meshN), []), |
188 (128, mashN), |
189 ((128, mashN), []), |
189 (32, meshN)], |
190 ((32, meshN), [])], |
190 outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"), |
191 outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"), |
191 parse_proof = SOME Z3_Replay.parse_proof, |
192 parse_proof = SOME Z3_Replay.parse_proof, |
192 replay = SOME Z3_Replay.replay } |
193 replay = SOME Z3_Replay.replay } |
193 |
194 |
194 end |
195 end |