feat: change bv_decide to an elaborated config (#6010)
This PR changes `bv_decide`'s configuration from lots of `set_option` to an elaborated config like `simp` or `omega`. The notable exception is `sat.solver` which is still a `set_option` such that users can configure a custom SAT solver globally for an entire project or file. Additionally it introduces the ability to set `maxSteps` for the simp preprocessing run through the new config. The latter feature was requested by people using `bv_decide` on SMTLIB which has ginormous terms that exceed the default.
This commit is contained in:
Henrik Böving
GitHub
parent
85f2213d5a
commit
837a67bedb
15 changed files with 106 additions and 113 deletions
|
|
@ -170,8 +170,8 @@ def satQuery (solverPath : System.FilePath) (problemPath : System.FilePath) (pro
|
|||
match out? with
|
||||
| .timeout =>
|
||||
let mut err := "The SAT solver timed out while solving the problem.\n"
|
||||
err := err ++ "Consider increasing the timeout with `set_option sat.timeout <sec>`.\n"
|
||||
err := err ++ "If solving your problem relies inherently on using associativity or commutativity, consider enabling the `bv.ac_nf` option."
|
||||
err := err ++ "Consider increasing the timeout with the `timeout` config option.\n"
|
||||
err := err ++ "If solving your problem relies inherently on using associativity or commutativity, consider enabling the `acNf` config option."
|
||||
throwError err
|
||||
| .success { exitCode := exitCode, stdout := stdout, stderr := stderr} =>
|
||||
if exitCode == 255 then
|
||||
|
|
|
|||
|
|
@ -6,6 +6,7 @@ Authors: Kim Morrison, Henrik Böving
|
|||
prelude
|
||||
import Lean.Util.Trace
|
||||
import Lean.Elab.Tactic.Simp
|
||||
import Std.Tactic.BVDecide.Syntax
|
||||
|
||||
/-!
|
||||
Provides environment extensions around the `bv_decide` tactic frontends.
|
||||
|
|
@ -32,30 +33,7 @@ register_builtin_option sat.solver : String := {
|
|||
to use the one that ships with Lean."
|
||||
}
|
||||
|
||||
register_builtin_option sat.timeout : Nat := {
|
||||
defValue := 10
|
||||
descr := "the number of seconds that the sat solver is run before aborting"
|
||||
}
|
||||
|
||||
register_builtin_option sat.trimProofs : Bool := {
|
||||
defValue := true
|
||||
descr := "Whether to run the trimming algorithm on LRAT proofs"
|
||||
}
|
||||
|
||||
register_builtin_option sat.binaryProofs : Bool := {
|
||||
defValue := true
|
||||
descr := "Whether to use the binary LRAT proof format. Currently set to false and ignored on Windows due to a bug in CaDiCal."
|
||||
}
|
||||
|
||||
register_builtin_option debug.bv.graphviz : Bool := {
|
||||
defValue := false
|
||||
descr := "Output the AIG of bv_decide as graphviz into a file called aig.gv in the working directory of the Lean process."
|
||||
}
|
||||
|
||||
register_builtin_option bv.ac_nf : Bool := {
|
||||
defValue := false
|
||||
descr := "Canonicalize with respect to associativity and commutativitiy."
|
||||
}
|
||||
declare_config_elab elabBVDecideConfig Lean.Elab.Tactic.BVDecide.Frontend.BVDecideConfig
|
||||
|
||||
builtin_initialize bvNormalizeExt : Meta.SimpExtension ←
|
||||
Meta.registerSimpAttr `bv_normalize "simp theorems used by bv_normalize"
|
||||
|
|
|
|||
|
|
@ -28,22 +28,22 @@ def getSrcDir : TermElabM System.FilePath := do
|
|||
| throwError "cannot compute parent directory of '{srcPath}'"
|
||||
return srcDir
|
||||
|
||||
def mkContext (lratPath : System.FilePath) : TermElabM TacticContext := do
|
||||
def mkContext (lratPath : System.FilePath) (cfg : BVDecideConfig) : TermElabM TacticContext := do
|
||||
let lratPath := (← getSrcDir) / lratPath
|
||||
TacticContext.new lratPath
|
||||
TacticContext.new lratPath cfg
|
||||
|
||||
/--
|
||||
Prepare an `Expr` that proves `bvExpr.unsat` using `ofReduceBool`.
|
||||
-/
|
||||
def lratChecker (cfg : TacticContext) (bvExpr : BVLogicalExpr) : MetaM Expr := do
|
||||
let cert ← LratCert.ofFile cfg.lratPath cfg.trimProofs
|
||||
cert.toReflectionProof cfg bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
|
||||
def lratChecker (ctx : TacticContext) (bvExpr : BVLogicalExpr) : MetaM Expr := do
|
||||
let cert ← LratCert.ofFile ctx.lratPath ctx.config.trimProofs
|
||||
cert.toReflectionProof ctx bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
|
||||
|
||||
@[inherit_doc Lean.Parser.Tactic.bvCheck]
|
||||
def bvCheck (g : MVarId) (cfg : TacticContext) : MetaM Unit := do
|
||||
def bvCheck (g : MVarId) (ctx : TacticContext) : MetaM Unit := do
|
||||
let unsatProver : UnsatProver := fun _ reflectionResult _ => do
|
||||
withTraceNode `sat (fun _ => return "Preparing LRAT reflection term") do
|
||||
let proof ← lratChecker cfg reflectionResult.bvExpr
|
||||
let proof ← lratChecker ctx reflectionResult.bvExpr
|
||||
return .ok ⟨proof, ""⟩
|
||||
let _ ← closeWithBVReflection g unsatProver
|
||||
return ()
|
||||
|
|
@ -52,14 +52,15 @@ def bvCheck (g : MVarId) (cfg : TacticContext) : MetaM Unit := do
|
|||
open Lean.Meta.Tactic in
|
||||
@[builtin_tactic Lean.Parser.Tactic.bvCheck]
|
||||
def evalBvCheck : Tactic := fun
|
||||
| `(tactic| bv_check%$tk $path:str) => do
|
||||
let cfg ← BVDecide.Frontend.BVCheck.mkContext path.getString
|
||||
| `(tactic| bv_check%$tk $cfgStx:optConfig $path:str) => do
|
||||
let cfg ← elabBVDecideConfig cfgStx
|
||||
let ctx ← BVDecide.Frontend.BVCheck.mkContext path.getString cfg
|
||||
liftMetaFinishingTactic fun g => do
|
||||
let g'? ← Normalize.bvNormalize g
|
||||
let g'? ← Normalize.bvNormalize g cfg
|
||||
match g'? with
|
||||
| some g' => bvCheck g' cfg
|
||||
| some g' => bvCheck g' ctx
|
||||
| none =>
|
||||
let bvNormalizeStx ← `(tactic| bv_normalize)
|
||||
let bvNormalizeStx ← `(tactic| bv_normalize $cfgStx)
|
||||
logWarning m!"This goal can be closed by only applying bv_normalize, no need to keep the LRAT proof around."
|
||||
TryThis.addSuggestion tk bvNormalizeStx (origSpan? := ← getRef)
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
|
|
|||
|
|
@ -186,7 +186,7 @@ def explainCounterExampleQuality (counterExample : CounterExample) : MetaM Messa
|
|||
err := err ++ m!"Consider the following assignment:\n"
|
||||
return err
|
||||
|
||||
def lratBitblaster (goal : MVarId) (cfg : TacticContext) (reflectionResult : ReflectionResult)
|
||||
def lratBitblaster (goal : MVarId) (ctx : TacticContext) (reflectionResult : ReflectionResult)
|
||||
(atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) :
|
||||
MetaM (Except CounterExample UnsatProver.Result) := do
|
||||
let bvExpr := reflectionResult.bvExpr
|
||||
|
|
@ -197,7 +197,7 @@ def lratBitblaster (goal : MVarId) (cfg : TacticContext) (reflectionResult : Ref
|
|||
let aigSize := entry.aig.decls.size
|
||||
trace[Meta.Tactic.bv] s!"AIG has {aigSize} nodes."
|
||||
|
||||
if cfg.graphviz then
|
||||
if ctx.config.graphviz then
|
||||
IO.FS.writeFile ("." / "aig.gv") <| AIG.toGraphviz entry
|
||||
|
||||
let (cnf, map) ←
|
||||
|
|
@ -211,12 +211,12 @@ def lratBitblaster (goal : MVarId) (cfg : TacticContext) (reflectionResult : Ref
|
|||
|
||||
let res ←
|
||||
withTraceNode `sat (fun _ => return "Obtaining external proof certificate") do
|
||||
runExternal cnf cfg.solver cfg.lratPath cfg.trimProofs cfg.timeout cfg.binaryProofs
|
||||
runExternal cnf ctx.solver ctx.lratPath ctx.config.trimProofs ctx.config.timeout ctx.config.binaryProofs
|
||||
|
||||
match res with
|
||||
| .ok cert =>
|
||||
trace[Meta.Tactic.sat] "SAT solver found a proof."
|
||||
let proof ← cert.toReflectionProof cfg bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
|
||||
let proof ← cert.toReflectionProof ctx bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
|
||||
return .ok ⟨proof, cert⟩
|
||||
| .error assignment =>
|
||||
trace[Meta.Tactic.sat] "SAT solver found a counter example."
|
||||
|
|
@ -267,10 +267,10 @@ def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
|
|||
return .ok cert
|
||||
| .error counterExample => return .error counterExample
|
||||
|
||||
def bvUnsat (g : MVarId) (cfg : TacticContext) : MetaM (Except CounterExample LratCert) := M.run do
|
||||
def bvUnsat (g : MVarId) (ctx : TacticContext) : MetaM (Except CounterExample LratCert) := M.run do
|
||||
let unsatProver : UnsatProver := fun g reflectionResult atomsAssignment => do
|
||||
withTraceNode `bv (fun _ => return "Preparing LRAT reflection term") do
|
||||
lratBitblaster g cfg reflectionResult atomsAssignment
|
||||
lratBitblaster g ctx reflectionResult atomsAssignment
|
||||
closeWithBVReflection g unsatProver
|
||||
|
||||
/--
|
||||
|
|
@ -287,18 +287,18 @@ structure Result where
|
|||
Try to close `g` using a bitblaster. Return either a `CounterExample` if one is found or a `Result`
|
||||
if `g` is proven.
|
||||
-/
|
||||
def bvDecide' (g : MVarId) (cfg : TacticContext) : MetaM (Except CounterExample Result) := do
|
||||
let g? ← Normalize.bvNormalize g
|
||||
def bvDecide' (g : MVarId) (ctx : TacticContext) : MetaM (Except CounterExample Result) := do
|
||||
let g? ← Normalize.bvNormalize g ctx.config
|
||||
let some g := g? | return .ok ⟨none⟩
|
||||
match ← bvUnsat g cfg with
|
||||
match ← bvUnsat g ctx with
|
||||
| .ok lratCert => return .ok ⟨some lratCert⟩
|
||||
| .error counterExample => return .error counterExample
|
||||
|
||||
/--
|
||||
Call `bvDecide'` and throw a pretty error if a counter example ends up being produced.
|
||||
-/
|
||||
def bvDecide (g : MVarId) (cfg : TacticContext) : MetaM Result := do
|
||||
match ← bvDecide' g cfg with
|
||||
def bvDecide (g : MVarId) (ctx : TacticContext) : MetaM Result := do
|
||||
match ← bvDecide' g ctx with
|
||||
| .ok result => return result
|
||||
| .error counterExample =>
|
||||
counterExample.goal.withContext do
|
||||
|
|
@ -309,9 +309,10 @@ def bvDecide (g : MVarId) (cfg : TacticContext) : MetaM Result := do
|
|||
|
||||
@[builtin_tactic Lean.Parser.Tactic.bvDecide]
|
||||
def evalBvTrace : Tactic := fun
|
||||
| `(tactic| bv_decide) => do
|
||||
| `(tactic| bv_decide $cfg:optConfig) => do
|
||||
let cfg ← elabBVDecideConfig cfg
|
||||
IO.FS.withTempFile fun _ lratFile => do
|
||||
let cfg ← BVDecide.Frontend.TacticContext.new lratFile
|
||||
let cfg ← BVDecide.Frontend.TacticContext.new lratFile cfg
|
||||
liftMetaFinishingTactic fun g => do
|
||||
discard <| bvDecide g cfg
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
|
|
|||
|
|
@ -34,12 +34,13 @@ open Lean.Meta.Tactic in
|
|||
open Lean.Elab.Tactic.BVDecide.LRAT in
|
||||
@[builtin_tactic Lean.Parser.Tactic.bvTrace]
|
||||
def evalBvTrace : Tactic := fun
|
||||
| `(tactic| bv_decide?%$tk) => do
|
||||
| `(tactic| bv_decide?%$tk $cfgStx:optConfig) => do
|
||||
let cfg := { (← elabBVDecideConfig cfgStx) with trimProofs := false }
|
||||
let lratFile : System.FilePath ← BVTrace.getLratFileName
|
||||
let cfg := { (← BVCheck.mkContext lratFile) with trimProofs := false }
|
||||
let ctx ← BVCheck.mkContext lratFile cfg
|
||||
let g ← getMainGoal
|
||||
let trace ← g.withContext do
|
||||
bvDecide g cfg
|
||||
bvDecide g ctx
|
||||
/-
|
||||
Ideally trace.lratCert would be the `ByteArray` version of the proof already and we just write
|
||||
it. This isn't yet possible so instead we do the following:
|
||||
|
|
@ -57,12 +58,12 @@ def evalBvTrace : Tactic := fun
|
|||
let normalizeStx ← `(tactic| bv_normalize)
|
||||
TryThis.addSuggestion tk normalizeStx (origSpan? := ← getRef)
|
||||
| some .. =>
|
||||
if sat.trimProofs.get (← getOptions) then
|
||||
if ctx.config.trimProofs then
|
||||
let lratPath := (← BVCheck.getSrcDir) / lratFile
|
||||
let proof ← loadLRATProof lratPath
|
||||
let trimmed ← IO.ofExcept <| trim proof
|
||||
dumpLRATProof lratPath trimmed cfg.binaryProofs
|
||||
let bvCheckStx ← `(tactic| bv_check $(quote lratFile.toString))
|
||||
let bvCheckStx ← `(tactic| bv_check $cfgStx:optConfig $(quote lratFile.toString))
|
||||
TryThis.addSuggestion tk bvCheckStx (origSpan? := ← getRef)
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
|
|
|
|||
|
|
@ -30,37 +30,28 @@ structure TacticContext where
|
|||
reflectionDef : Name
|
||||
solver : System.FilePath
|
||||
lratPath : System.FilePath
|
||||
graphviz : Bool
|
||||
timeout : Nat
|
||||
trimProofs : Bool
|
||||
binaryProofs : Bool
|
||||
config : BVDecideConfig
|
||||
|
||||
def TacticContext.new (lratPath : System.FilePath) : Lean.Elab.TermElabM TacticContext := do
|
||||
def TacticContext.new (lratPath : System.FilePath) (config : BVDecideConfig) :
|
||||
Lean.Elab.TermElabM TacticContext := do
|
||||
-- Account for: https://github.com/arminbiere/cadical/issues/112
|
||||
let config :=
|
||||
if System.Platform.isWindows then
|
||||
{ config with binaryProofs := false }
|
||||
else
|
||||
config
|
||||
let exprDef ← Lean.Elab.Term.mkAuxName `_expr_def
|
||||
let certDef ← Lean.Elab.Term.mkAuxName `_cert_def
|
||||
let reflectionDef ← Lean.Elab.Term.mkAuxName `_reflection_def
|
||||
let opts ← getOptions
|
||||
let solver ← determineSolver
|
||||
trace[Meta.Tactic.sat] m!"Using SAT solver at '{solver}'"
|
||||
let timeout := sat.timeout.get opts
|
||||
let graphviz := debug.bv.graphviz.get opts
|
||||
let trimProofs := sat.trimProofs.get opts
|
||||
let binaryProofs :=
|
||||
-- Account for: https://github.com/arminbiere/cadical/issues/112
|
||||
if System.Platform.isWindows then
|
||||
false
|
||||
else
|
||||
sat.binaryProofs.get opts
|
||||
return {
|
||||
exprDef,
|
||||
certDef,
|
||||
reflectionDef,
|
||||
solver,
|
||||
lratPath,
|
||||
graphviz,
|
||||
timeout,
|
||||
trimProofs,
|
||||
binaryProofs
|
||||
config
|
||||
}
|
||||
where
|
||||
determineSolver : Lean.Elab.TermElabM System.FilePath := do
|
||||
|
|
|
|||
|
|
@ -157,14 +157,14 @@ partial def fixpointPipeline (passes : List Pass) (goal : MVarId) : MetaM (Optio
|
|||
/--
|
||||
Responsible for applying the Bitwuzla style rewrite rules.
|
||||
-/
|
||||
def rewriteRulesPass : Pass := fun goal => do
|
||||
def rewriteRulesPass (maxSteps : Nat) : Pass := fun goal => do
|
||||
let bvThms ← bvNormalizeExt.getTheorems
|
||||
let bvSimprocs ← bvNormalizeSimprocExt.getSimprocs
|
||||
let sevalThms ← getSEvalTheorems
|
||||
let sevalSimprocs ← Simp.getSEvalSimprocs
|
||||
|
||||
let simpCtx : Simp.Context := {
|
||||
config := { failIfUnchanged := false, zetaDelta := true }
|
||||
config := { failIfUnchanged := false, zetaDelta := true, maxSteps }
|
||||
simpTheorems := #[bvThms, sevalThms]
|
||||
congrTheorems := (← getSimpCongrTheorems)
|
||||
}
|
||||
|
|
@ -181,7 +181,7 @@ def rewriteRulesPass : Pass := fun goal => do
|
|||
Substitute embedded constraints. That is look for hypotheses of the form `h : x = true` and use
|
||||
them to substitute occurences of `x` within other hypotheses
|
||||
-/
|
||||
def embeddedConstraintPass : Pass := fun goal =>
|
||||
def embeddedConstraintPass (maxSteps : Nat) : Pass := fun goal =>
|
||||
goal.withContext do
|
||||
let hyps ← goal.getNondepPropHyps
|
||||
let relevanceFilter acc hyp := do
|
||||
|
|
@ -195,7 +195,7 @@ def embeddedConstraintPass : Pass := fun goal =>
|
|||
let relevantHyps : SimpTheoremsArray ← hyps.foldlM (init := #[]) relevanceFilter
|
||||
|
||||
let simpCtx : Simp.Context := {
|
||||
config := { failIfUnchanged := false }
|
||||
config := { failIfUnchanged := false, maxSteps }
|
||||
simpTheorems := relevantHyps
|
||||
congrTheorems := (← getSimpCongrTheorems)
|
||||
}
|
||||
|
|
@ -222,32 +222,35 @@ def acNormalizePass : Pass := fun goal => do
|
|||
/--
|
||||
The normalization passes used by `bv_normalize` and thus `bv_decide`.
|
||||
-/
|
||||
def defaultPipeline : List Pass := [rewriteRulesPass, embeddedConstraintPass]
|
||||
def defaultPipeline (cfg : BVDecideConfig ): List Pass :=
|
||||
[
|
||||
rewriteRulesPass cfg.maxSteps,
|
||||
embeddedConstraintPass cfg.maxSteps
|
||||
]
|
||||
|
||||
def passPipeline : MetaM (List Pass) := do
|
||||
let opts ← getOptions
|
||||
def passPipeline (cfg : BVDecideConfig) : List Pass := Id.run do
|
||||
let mut passPipeline := defaultPipeline cfg
|
||||
|
||||
let mut passPipeline := defaultPipeline
|
||||
|
||||
if bv.ac_nf.get opts then
|
||||
if cfg.acNf then
|
||||
passPipeline := passPipeline ++ [acNormalizePass]
|
||||
|
||||
return passPipeline
|
||||
|
||||
end Pass
|
||||
|
||||
def bvNormalize (g : MVarId) : MetaM (Option MVarId) := do
|
||||
def bvNormalize (g : MVarId) (cfg : BVDecideConfig) : MetaM (Option MVarId) := do
|
||||
withTraceNode `bv (fun _ => return "Normalizing goal") do
|
||||
-- Contradiction proof
|
||||
let some g ← g.falseOrByContra | return none
|
||||
trace[Meta.Tactic.bv] m!"Running preprocessing pipeline on:\n{g}"
|
||||
Pass.fixpointPipeline (← Pass.passPipeline) g
|
||||
Pass.fixpointPipeline (Pass.passPipeline cfg) g
|
||||
|
||||
@[builtin_tactic Lean.Parser.Tactic.bvNormalize]
|
||||
def evalBVNormalize : Tactic := fun
|
||||
| `(tactic| bv_normalize) => do
|
||||
| `(tactic| bv_normalize $cfg:optConfig) => do
|
||||
let cfg ← elabBVDecideConfig cfg
|
||||
let g ← getMainGoal
|
||||
match ← bvNormalize g with
|
||||
match ← bvNormalize g cfg with
|
||||
| some newGoal => replaceMainGoal [newGoal]
|
||||
| none => replaceMainGoal []
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
|
|
|||
|
|
@ -9,6 +9,38 @@ import Init.Simproc
|
|||
|
||||
set_option linter.missingDocs true -- keep it documented
|
||||
|
||||
namespace Lean.Elab.Tactic.BVDecide.Frontend
|
||||
|
||||
/--
|
||||
The configuration options for `bv_decide`.
|
||||
-/
|
||||
structure BVDecideConfig where
|
||||
/-- The number of seconds that the SAT solver is run before aborting. -/
|
||||
timeout : Nat := 10
|
||||
/-- Whether to run the trimming algorithm on LRAT proofs. -/
|
||||
trimProofs : Bool := true
|
||||
/--
|
||||
Whether to use the binary LRAT proof format.
|
||||
Currently set to false and ignored on Windows due to a bug in CaDiCal.
|
||||
-/
|
||||
binaryProofs : Bool := true
|
||||
/--
|
||||
Canonicalize with respect to associativity and commutativitiy.
|
||||
-/
|
||||
acNf : Bool := false
|
||||
/--
|
||||
Output the AIG of bv_decide as graphviz into a file called aig.gv in the working directory of the
|
||||
Lean process.
|
||||
-/
|
||||
graphviz : Bool := false
|
||||
/--
|
||||
The maximum number of subexpressions to visit when performing simplification.
|
||||
-/
|
||||
maxSteps : Nat := Lean.Meta.Simp.defaultMaxSteps
|
||||
|
||||
end Lean.Elab.Tactic.BVDecide.Frontend
|
||||
|
||||
|
||||
namespace Lean.Parser
|
||||
|
||||
namespace Tactic
|
||||
|
|
@ -21,7 +53,7 @@ current Lean file:
|
|||
bv_check "proof.lrat"
|
||||
```
|
||||
-/
|
||||
syntax (name := bvCheck) "bv_check " str : tactic
|
||||
syntax (name := bvCheck) "bv_check " optConfig str : tactic
|
||||
|
||||
/--
|
||||
Close fixed-width `BitVec` and `Bool` goals by obtaining a proof from an external SAT solver and
|
||||
|
|
@ -48,19 +80,19 @@ the `bv.ac_nf` option.
|
|||
|
||||
Note: `bv_decide` uses `ofReduceBool` and thus trusts the correctness of the code generator.
|
||||
-/
|
||||
syntax (name := bvDecide) "bv_decide" : tactic
|
||||
syntax (name := bvDecide) "bv_decide" optConfig : tactic
|
||||
|
||||
|
||||
/--
|
||||
Suggest a proof script for a `bv_decide` tactic call. Useful for caching LRAT proofs.
|
||||
-/
|
||||
syntax (name := bvTrace) "bv_decide?" : tactic
|
||||
syntax (name := bvTrace) "bv_decide?" optConfig : tactic
|
||||
|
||||
/--
|
||||
Run the normalization procedure of `bv_decide` only. Sometimes this is enough to solve basic
|
||||
`BitVec` goals already.
|
||||
-/
|
||||
syntax (name := bvNormalize) "bv_normalize" : tactic
|
||||
syntax (name := bvNormalize) "bv_normalize" optConfig : tactic
|
||||
|
||||
end Tactic
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,5 @@
|
|||
import Std.Tactic.BVDecide
|
||||
|
||||
set_option bv.ac_nf false in
|
||||
example
|
||||
(a k n : BitVec 32) :
|
||||
n < -1 - k →
|
||||
|
|
|
|||
|
|
@ -2,8 +2,6 @@ import Std.Tactic.BVDecide
|
|||
|
||||
open BitVec
|
||||
|
||||
set_option bv.ac_nf false
|
||||
|
||||
theorem arith_unit_1 (x y : BitVec 64) : x + y = y + x := by
|
||||
bv_decide
|
||||
|
||||
|
|
|
|||
|
|
@ -2,8 +2,6 @@ import Std.Tactic.BVDecide
|
|||
|
||||
open BitVec
|
||||
|
||||
set_option bv.ac_nf false
|
||||
|
||||
theorem bv_axiomCheck (x y : BitVec 1) : x + y = y + x := by
|
||||
bv_decide
|
||||
|
||||
|
|
|
|||
|
|
@ -2,8 +2,6 @@ import Std.Tactic.BVDecide
|
|||
|
||||
open BitVec
|
||||
|
||||
set_option bv.ac_nf false
|
||||
|
||||
theorem bitwise_unit_1 {x y : BitVec 64} : ~~~(x &&& y) = (~~~x ||| ~~~y) := by
|
||||
bv_decide
|
||||
|
||||
|
|
|
|||
|
|
@ -85,12 +85,10 @@ example {x : BitVec 16} : (BitVec.twoPow 16 2) = 4#16 := by bv_normalize
|
|||
|
||||
section
|
||||
|
||||
set_option bv.ac_nf true
|
||||
|
||||
example (x y : BitVec 256) : x * y = y * x := by
|
||||
bv_decide
|
||||
bv_decide (config := { acNf := true })
|
||||
|
||||
example {x y z : BitVec 64} : ~~~(x &&& (y * z)) = (~~~x ||| ~~~(z * y)) := by
|
||||
bv_decide
|
||||
bv_decide (config := { acNf := true })
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -2,17 +2,14 @@ import Std.Tactic.BVDecide
|
|||
|
||||
open BitVec
|
||||
|
||||
set_option bv.ac_nf false
|
||||
|
||||
/--
|
||||
error: The SAT solver timed out while solving the problem.
|
||||
Consider increasing the timeout with `set_option sat.timeout <sec>`.
|
||||
If solving your problem relies inherently on using associativity or commutativity, consider enabling the `bv.ac_nf` option.
|
||||
Consider increasing the timeout with the `timeout` config option.
|
||||
If solving your problem relies inherently on using associativity or commutativity, consider enabling the `acNf` config option.
|
||||
-/
|
||||
#guard_msgs in
|
||||
set_option sat.timeout 1 in
|
||||
theorem timeout (x y z : BitVec 1024) : x - (y + z) = x - y - z := by
|
||||
bv_decide
|
||||
bv_decide (config := { timeout := 1 })
|
||||
|
||||
/--
|
||||
error: None of the hypotheses are in the supported BitVec fragment.
|
||||
|
|
|
|||
|
|
@ -2,8 +2,6 @@ import Std.Tactic.BVDecide
|
|||
|
||||
open BitVec
|
||||
|
||||
set_option bv.ac_nf false
|
||||
|
||||
theorem substructure_unit_1 (x y z : BitVec 8) : ((x = y) ∧ (y = z)) ↔ ¬(¬(x =y) ∨ (¬(y = z))) := by
|
||||
bv_decide
|
||||
|
||||
|
|
@ -33,7 +31,7 @@ theorem substructure_unit_6 (a b c: Bool) : (if a then b else c) = (if !a then c
|
|||
|
||||
theorem substructure_unit_7 (a b c: Bool) : (bif a then b else c) = (bif !a then c else b) := by
|
||||
bv_decide
|
||||
|
||||
|
||||
theorem substructure_unit_8 (x : BitVec 32) : (if x.getLsbD 0 then !x.getLsbD 0 else x.getLsbD 0) = false := by
|
||||
bv_decide
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue