| author | wenzelm |
| Wed, 04 Oct 2017 12:00:53 +0200 | |
| changeset 66787 | 64b47495676d |
| parent 63992 | 3aa9837d05c7 |
| permissions | -rw-r--r-- |
| 63992 | 1 |
(* Title: HOL/Tools/Argo/argo_sat_solver.ML |
|
63962
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
2 |
Author: Sascha Boehme |
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
3 |
|
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
4 |
A SAT solver based on the Argo solver. |
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
5 |
This SAT solver produces models. For proofs use Argo_Tactic.prove instead. |
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
6 |
*) |
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
7 |
|
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
8 |
structure Argo_SAT_Solver: sig end = |
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
9 |
struct |
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
10 |
|
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
11 |
fun con_of i = (string_of_int i, Argo_Expr.Bool) |
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
12 |
|
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
13 |
fun expr_of Prop_Logic.True = Argo_Expr.true_expr |
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
14 |
| expr_of Prop_Logic.False = Argo_Expr.false_expr |
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
15 |
| expr_of (Prop_Logic.Not p) = Argo_Expr.mk_not (expr_of p) |
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
16 |
| expr_of (Prop_Logic.Or (p1, p2)) = Argo_Expr.mk_or2 (expr_of p1) (expr_of p2) |
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
17 |
| expr_of (Prop_Logic.And (p1, p2)) = Argo_Expr.mk_and2 (expr_of p1) (expr_of p2) |
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
18 |
| expr_of (Prop_Logic.BoolVar i) = Argo_Expr.mk_con (con_of i) |
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
19 |
|
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
20 |
fun argo_solver p = |
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
21 |
let val argo = Argo_Solver.assert [expr_of p] Argo_Solver.context |
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
22 |
in SAT_Solver.SATISFIABLE (Argo_Solver.model_of argo o con_of) end |
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
23 |
handle Argo_Proof.UNSAT _ => SAT_Solver.UNSATISFIABLE NONE |
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
24 |
|
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
25 |
val () = SAT_Solver.add_solver ("argo", argo_solver)
|
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
26 |
|
|
83a625d06e91
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
boehmes
parents:
diff
changeset
|
27 |
end |