feat(tools/super): use congruence closure

library/tools/super/cdcl.lean

@@ -6,27 +6,11 @@ Authors: Gabriel Ebner
 import .clause .clausifier .cdcl_solver
 open tactic expr monad super
 
-private meta def theory_solver_of_tactic (th_solver : tactic unit) : cdcl.solver (option cdcl.proof_term) :=
-do s ← state_t.read, ↑do
-hyps ← return $ s^.trail^.for (λe, e^.hyp),
-subgoal ← mk_meta_var s^.local_false,
-goals ← get_goals,
-set_goals [subgoal],
-hvs ← for hyps (λhyp, assertv hyp^.local_pp_name hyp^.local_type hyp),
-solved ← (do th_solver, now, return tt) <|> return ff,
-set_goals goals,
-if solved then do
-  proof ← instantiate_mvars subgoal,
-  proof' ← whnf proof, -- gets rid of the unnecessary asserts
-  return $ some proof'
-else
-  return none
-
 meta def cdcl_t (th_solver : tactic unit) : tactic unit := do
 as_refutation, local_false ← target,
 clauses ← clauses_of_context, clauses ← get_clauses_classical clauses,
 for clauses (λc, do c_pp ← pp c, clause.validate c <|> fail c_pp),
-res ← cdcl.solve (theory_solver_of_tactic th_solver) local_false clauses,
+res ← cdcl.solve (cdcl.theory_solver_of_tactic th_solver) local_false clauses,
 match res with
 | (cdcl.result.unsat proof) := exact proof
 | (cdcl.result.sat interp) :=

library/tools/super/cdcl_solver.lean

@@ -412,4 +412,20 @@ meta def solve (local_false : expr) (clauses : list clause) : tactic result := d
 res ← (do for clauses mk_clause, run theory_solver) (state.initial local_false),
 return res.1
 
+meta def theory_solver_of_tactic (th_solver : tactic unit) : cdcl.solver (option cdcl.proof_term) :=
+do s ← state_t.read, ↑do
+hyps ← return $ s^.trail^.for (λe, e^.hyp),
+subgoal ← mk_meta_var s^.local_false,
+goals ← get_goals,
+set_goals [subgoal],
+hvs ← for hyps (λhyp, assertv hyp^.local_pp_name hyp^.local_type hyp),
+solved ← (do th_solver, now, return tt) <|> return ff,
+set_goals goals,
+if solved then do
+proof ← instantiate_mvars subgoal,
+proof' ← whnf proof, -- gets rid of the unnecessary asserts
+return $ some proof'
+else
+return none
+
 end cdcl

library/tools/super/prover_state.lean

@@ -329,8 +329,11 @@ do passive ← flip monad.lift state_t.read $ λst, st^.passive, for' passive^.t
   else
     return ()
 
+def super_cc_config : cc_config :=
+{ default_cc_config with em := ff }
+
 meta def do_sat_run : prover (option expr) :=
-do sat_result ← in_sat_solver $ cdcl.run (return none),
+do sat_result ← in_sat_solver $ cdcl.run (cdcl.theory_solver_of_tactic $ using_smt $ return ()),
 state_t.modify $ λst, { st with needs_sat_run := ff },
 old_model ← lift prover_state.current_model state_t.read,
 match sat_result with