# HG changeset patch
# User boehmes
# Date 1475175285 -7200
# Node ID 83a625d06e91ff94d5ea1d259782a709bf3cb71c
# Parent  2fd9656c4c827c33b3839043ebefda4361c14f93
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable

diff -r 2fd9656c4c82 -r 83a625d06e91 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Thu Sep 29 20:54:45 2016 +0200
+++ b/src/HOL/Presburger.thy	Thu Sep 29 20:54:45 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Decision Procedure for Presburger Arithmetic\<close>
 
 theory Presburger
-imports Groebner_Basis Set_Interval Argo
+imports Groebner_Basis Set_Interval
 keywords "try0" :: diag
 begin
 
diff -r 2fd9656c4c82 -r 83a625d06e91 src/HOL/SAT.thy
--- a/src/HOL/SAT.thy	Thu Sep 29 20:54:45 2016 +0200
+++ b/src/HOL/SAT.thy	Thu Sep 29 20:54:45 2016 +0200
@@ -8,12 +8,13 @@
 section \<open>Reconstructing external resolution proofs for propositional logic\<close>
 
 theory SAT
-imports HOL
+imports Argo
 begin
 
 ML_file "Tools/prop_logic.ML"
 ML_file "Tools/sat_solver.ML"
 ML_file "Tools/sat.ML"
+ML_file "Tools/Argo/argo_sat_solver.ML"
 
 method_setup sat = \<open>Scan.succeed (SIMPLE_METHOD' o SAT.sat_tac)\<close>
   "SAT solver"
diff -r 2fd9656c4c82 -r 83a625d06e91 src/HOL/Tools/Argo/argo_sat_solver.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Argo/argo_sat_solver.ML	Thu Sep 29 20:54:45 2016 +0200
@@ -0,0 +1,27 @@
+(*  Title:      HOL/Tools/argo_sat_solver.ML
+    Author:     Sascha Boehme
+
+A SAT solver based on the Argo solver.
+This SAT solver produces models. For proofs use Argo_Tactic.prove instead.
+*)
+
+structure Argo_SAT_Solver: sig end =
+struct
+
+fun con_of i = (string_of_int i, Argo_Expr.Bool)
+
+fun expr_of Prop_Logic.True = Argo_Expr.true_expr
+  | expr_of Prop_Logic.False = Argo_Expr.false_expr
+  | expr_of (Prop_Logic.Not p) = Argo_Expr.mk_not (expr_of p)
+  | expr_of (Prop_Logic.Or (p1, p2)) = Argo_Expr.mk_or2 (expr_of p1) (expr_of p2)
+  | expr_of (Prop_Logic.And (p1, p2)) = Argo_Expr.mk_and2 (expr_of p1) (expr_of p2)
+  | expr_of (Prop_Logic.BoolVar i) = Argo_Expr.mk_con (con_of i)
+
+fun argo_solver p =
+  let val argo = Argo_Solver.assert [expr_of p] Argo_Solver.context
+  in SAT_Solver.SATISFIABLE (Argo_Solver.model_of argo o con_of) end
+  handle Argo_Proof.UNSAT _ => SAT_Solver.UNSATISFIABLE NONE
+
+val () = SAT_Solver.add_solver ("argo", argo_solver)
+
+end