diff --git a/src/Lean/Elab/Tactic/BVDecide/External.lean b/src/Lean/Elab/Tactic/BVDecide/External.lean index 75485afe3c..299d49e054 100644 --- a/src/Lean/Elab/Tactic/BVDecide/External.lean +++ b/src/Lean/Elab/Tactic/BVDecide/External.lean @@ -8,6 +8,7 @@ module prelude public import Std.Tactic.BVDecide.LRAT.Parser public import Lean.CoreM +public import Std.Tactic.BVDecide.Syntax public section @@ -146,7 +147,7 @@ solvers the solver is run with `timeout` in seconds as a maximum time limit to s Note: This function currently assume that the solver has the same CLI as CaDiCal. -/ def satQuery (solverPath : System.FilePath) (problemPath : System.FilePath) (proofOutput : System.FilePath) - (timeout : Nat) (binaryProofs : Bool) : + (timeout : Nat) (binaryProofs : Bool) (mode : Frontend.SolverMode) : CoreM SolverResult := do let cmd := solverPath.toString let mut args := #[ @@ -156,17 +157,12 @@ def satQuery (solverPath : System.FilePath) (problemPath : System.FilePath) (pro s!"--binary={binaryProofs}", "--quiet", /- - This sets the magic parameters of cadical to optimize for UNSAT search. - Given the fact that we are mostly interested in proving things and expect user goals to be - provable this is a fine value to set - -/ - "--unsat", - /- Bitwuzla sets this option and it does improve performance practically: https://github.com/bitwuzla/bitwuzla/blob/0e81e616af4d4421729884f01928b194c3536c76/src/sat/cadical.cpp#L34 -/ "--shrink=0" ] + args := args ++ solverModeFlags mode -- We implement timeouting ourselves because cadicals -t option is not available on Windows. let out? ← runInterruptible timeout { cmd, args, stdin := .piped, stdout := .piped, stderr := .null } @@ -190,6 +186,12 @@ def satQuery (solverPath : System.FilePath) (problemPath : System.FilePath) (pro throwError s!"Error {err} while parsing:\n{stdout}" else throwError s!"The external prover produced unexpected output, stdout:\n{stdout}stderr:\n{stderr}" +where + solverModeFlags (mode : Frontend.SolverMode) : Array String := + match mode with + | .proof => #["--unsat"] + | .counterexample => #["--sat"] + | .default => #["--default"] end External diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean index e80328ded0..6eb5a36889 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean @@ -344,7 +344,14 @@ def lratBitblaster (goal : MVarId) (ctx : TacticContext) (reflectionResult : Ref let res ← withTraceNode `Meta.Tactic.sat (fun _ => return "Obtaining external proof certificate") do - runExternal cnf ctx.solver ctx.lratPath ctx.config.trimProofs ctx.config.timeout ctx.config.binaryProofs + runExternal + cnf + ctx.solver + ctx.lratPath + ctx.config.trimProofs + ctx.config.timeout + ctx.config.binaryProofs + ctx.config.solverMode match res with | .ok cert => diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean index fd871a869b..9568ecbc88 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean @@ -131,7 +131,7 @@ Run an external SAT solver on the `CNF` to obtain an LRAT proof. This will obtain an `LratCert` if the formula is UNSAT and throw errors otherwise. -/ def runExternal (cnf : CNF Nat) (solver : System.FilePath) (lratPath : System.FilePath) - (trimProofs : Bool) (timeout : Nat) (binaryProofs : Bool) : + (trimProofs : Bool) (timeout : Nat) (binaryProofs : Bool) (solverMode : Frontend.SolverMode) : CoreM (Except (Array (Bool × Nat)) LratCert) := do IO.FS.withTempFile fun cnfHandle cnfPath => do withTraceNode `Meta.Tactic.sat (fun _ => return "Serializing SAT problem to DIMACS file") do @@ -141,7 +141,7 @@ def runExternal (cnf : CNF Nat) (solver : System.FilePath) (lratPath : System.Fi let res ← withTraceNode `Meta.Tactic.sat (fun _ => return "Running SAT solver") do - External.satQuery solver cnfPath lratPath timeout binaryProofs + External.satQuery solver cnfPath lratPath timeout binaryProofs solverMode if let .sat assignment := res then return .error assignment diff --git a/src/Std/Tactic/BVDecide/Syntax.lean b/src/Std/Tactic/BVDecide/Syntax.lean index 7c74821860..1a71c78b92 100644 --- a/src/Std/Tactic/BVDecide/Syntax.lean +++ b/src/Std/Tactic/BVDecide/Syntax.lean @@ -14,6 +14,23 @@ set_option linter.missingDocs true -- keep it documented namespace Lean.Elab.Tactic.BVDecide.Frontend +/-- +The various kinds of configurations offered for the SAT solver. +-/ +inductive SolverMode where + /-- + Set SAT solver options to improve proof search. + -/ + | proof + /-- + Set SAT solver options to improve counterexample search. + -/ + | counterexample + /-- + Don't set additional SAT solver flags. + -/ + | default + /-- The configuration options for `bv_decide`. -/ @@ -70,6 +87,11 @@ structure BVDecideConfig where if matching multiplications are not needed to proof a goal. -/ shortCircuit : Bool := false + /-- + The SAT solver configuration to use. Defaults to `.proof` as that is the most relevant use case + for `bv_decide`. + -/ + solverMode : SolverMode := .proof end Lean.Elab.Tactic.BVDecide.Frontend diff --git a/tests/lean/run/bv_decide_solver_modes.lean b/tests/lean/run/bv_decide_solver_modes.lean new file mode 100644 index 0000000000..00967fbc4a --- /dev/null +++ b/tests/lean/run/bv_decide_solver_modes.lean @@ -0,0 +1,38 @@ +import Std.Tactic.BVDecide + + +/-- +error: The prover found a counterexample, consider the following assignment: +x = 4294967295#32 +y = 4294967295#32 +-/ +#guard_msgs in +example (x y : BitVec 32) : x * y = y + x := by + bv_decide + +/-- +error: The prover found a counterexample, consider the following assignment: +x = 4294967295#32 +y = 4294967295#32 +-/ +#guard_msgs in +example (x y : BitVec 32) : x * y = y + x := by + bv_decide (config := { solverMode := .counterexample }) + +/-- +error: The prover found a counterexample, consider the following assignment: +x = 4294967295#32 +y = 4294967295#32 +-/ +#guard_msgs in +example (x y : BitVec 32) : x * y = y + x := by + bv_decide (config := { solverMode := .default }) + +/-- +error: The prover found a counterexample, consider the following assignment: +x = 4294967295#32 +y = 4294967295#32 +-/ +#guard_msgs in +example (x y : BitVec 32) : x * y = y + x := by + bv_decide (config := { solverMode := .proof })