Skip to content

Commit

Permalink
Refactor smt_rw tactic.
Browse files Browse the repository at this point in the history
  • Loading branch information
@abdoo8080
abdoo8080 committed Oct 6, 2024
1 parent 68ba819 commit 5b66c53
Show file tree
Hide file tree
Showing 9 changed files with 94 additions and 96 deletions.
23 changes: 13 additions & 10 deletions Smt/Reconstruct/Int.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -95,15 +95,15 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
| .ARITH_PLUS_ZERO =>
if !pf.getArguments[1]![0]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.add_assoc) q(Int.add_zero) q(@Rewrite.plus_zero) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Int Int Int _) q(0 : Int) q(@Rewrite.plus_zero) args)
| .ARITH_MUL_ONE =>
if !pf.getArguments[1]![0]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.mul_assoc) q(Int.mul_one) q(@Rewrite.mul_one) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Int Int Int _) q(1 : Int) q(@Rewrite.mul_one) args)
| .ARITH_MUL_ZERO =>
if !pf.getArguments[1]![0]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.mul_assoc) q(Int.mul_one) q(@Rewrite.mul_zero) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Int Int Int _) q(1 : Int) q(@Rewrite.mul_zero) args)
| .ARITH_INT_DIV_TOTAL =>
let t : Q(Int) ← reconstructTerm pf.getArguments[1]!
let s : Q(Int) ← reconstructTerm pf.getArguments[2]!
Expand Down Expand Up @@ -199,23 +199,23 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
| .ARITH_PLUS_FLATTEN =>
if !pf.getArguments[2]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.add_assoc) q(Int.add_zero) q(@Rewrite.plus_flatten) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Int Int Int _) q(0 : Int) q(@Rewrite.plus_flatten) args)
| .ARITH_MULT_FLATTEN =>
if !pf.getArguments[2]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.mul_assoc) q(Int.mul_one) q(@Rewrite.mult_flatten) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Int Int Int _) q(1 : Int) q(@Rewrite.mult_flatten) args)
| .ARITH_MULT_DIST =>
if !pf.getArguments[2]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.mul_assoc) q(Int.mul_one) q(@Rewrite.mult_dist) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Int Int Int _) q(1 : Int) q(@Rewrite.mult_dist) args)
| .ARITH_PLUS_CANCEL1 =>
if !pf.getArguments[2]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.mul_assoc) q(Int.mul_one) q(@Rewrite.plus_cancel1) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Int Int Int _) q(0 : Int) q(@Rewrite.plus_cancel1) args)
| .ARITH_PLUS_CANCEL2 =>
if !pf.getArguments[2]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Int.add_assoc) q(Int.add_zero) q(@Rewrite.plus_cancel2) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Int Int Int _) q(0 : Int) q(@Rewrite.plus_cancel2) args)
| .ARITH_ABS_ELIM =>
if !pf.getArguments[1]!.getSort.isInteger then return none
let t : Q(Int) ← reconstructTerm pf.getArguments[1]!
Expand All @@ -226,8 +226,11 @@ where
let mut args' := #[]
for arg in args do
let mut arg' := #[]
for subarg in arg do
arg' := arg'.push (← reconstructTerm subarg)
if arg.getKind == .SEXPR then
for subarg in arg do
arg' := arg'.push (← reconstructTerm subarg)
else
arg' := arg'.push (← reconstructTerm arg)
args' := args'.push arg'
return args'

Expand Down
47 changes: 25 additions & 22 deletions Smt/Reconstruct/Prop.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -80,46 +80,46 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
let q : Q(Prop) ← reconstructTerm pf.getArguments[2]!
addThm q(($p → $q) = (¬$p ∨ $q)) q(@Prop.bool_impl_elim $p $q)
-- | .BOOL_OR_TRUE =>
-- let args ← reconstructArgs pf.getArguments
-- addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.or_assoc_eq) q(or_false) q(@Prop.bool_or_true) args)
| .BOOL_OR_TRUE =>
let args ← reconstructArgs pf.getArguments
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Or) q(False) q(@Prop.bool_or_true) args)
| .BOOL_OR_FALSE =>
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.or_assoc_eq) q(or_false) q(@Prop.bool_or_false) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Or) q(False) q(@Prop.bool_or_false) args)
| .BOOL_OR_FLATTEN =>
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.or_assoc_eq) q(or_false) q(@Prop.bool_or_flatten) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Or) q(False) q(@Prop.bool_or_flatten) args)
| .BOOL_OR_DUP =>
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.or_assoc_eq) q(or_false) q(@Prop.bool_or_dup) args)
-- | .BOOL_AND_TRUE =>
-- let args ← reconstructArgs pf.getArguments[1:]
-- addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.and_assoc_eq) q(and_true) q(@Prop.bool_and_true) args)
-- | .BOOL_AND_FALSE =>
-- let args ← reconstructArgs pf.getArguments[1:]
-- addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.and_assoc_eq) q(and_true) q(@Prop.bool_and_false) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Or) q(False) q(@Prop.bool_or_dup) args)
| .BOOL_AND_TRUE =>
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(And) q(True) q(@Prop.bool_and_true) args)
| .BOOL_AND_FALSE =>
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(And) q(True) q(@Prop.bool_and_false) args)
| .BOOL_AND_FLATTEN =>
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.and_assoc_eq) q(and_true) q(@Prop.bool_and_flatten) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(And) q(True) q(@Prop.bool_and_flatten) args)
| .BOOL_AND_DUP =>
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.and_assoc_eq) q(and_true) q(@Prop.bool_and_dup) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(And) q(True) q(@Prop.bool_and_dup) args)
| .BOOL_AND_CONF =>
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.and_assoc_eq) q(and_true) q(@Prop.bool_and_conf) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(And) q(True) q(@Prop.bool_and_conf) args)
| .BOOL_OR_TAUT =>
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.or_assoc_eq) q(or_false) q(@Prop.bool_or_taut) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Or) q(False) q(@Prop.bool_or_taut) args)
| .BOOL_OR_DE_MORGAN =>
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.or_assoc_eq) q(or_false) q(@Prop.bool_or_de_morgan) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Or) q(False) q(@Prop.bool_or_de_morgan) args)
| .BOOL_IMPLIES_DE_MORGAN =>
let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
let q : Q(Prop) ← reconstructTerm pf.getArguments[2]!
addThm q((¬($p → $q)) = ($p ∧ ¬$q)) q(@Prop.bool_implies_de_morgan $p $q)
-- | .BOOL_AND_DE_MORGAN =>
-- let args ← reconstructArgs pf.getArguments[1:]
-- addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.and_assoc_eq) q(and_true) q(@Prop.bool_and_de_morgan) args)
| .BOOL_AND_DE_MORGAN =>
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(And) q(True) q(@Prop.bool_and_de_morgan) args)
| .BOOL_XOR_REFL =>
let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
addThm q(XOr $p $p = False) q(@Prop.bool_xor_refl $p)
Expand Down Expand Up @@ -191,8 +191,11 @@ where
let mut args' := #[]
for arg in args do
let mut arg' := #[]
for subarg in arg do
arg' := arg'.push (← reconstructTerm subarg)
if arg.getKind == .SEXPR then
for subarg in arg do
arg' := arg'.push (← reconstructTerm subarg)
else
arg' := arg'.push (← reconstructTerm arg)
args' := args'.push arg'
return args'

Expand Down
23 changes: 13 additions & 10 deletions Smt/Reconstruct/Rat.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -110,15 +110,15 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
| .ARITH_PLUS_ZERO =>
if pf.getArguments[1]![0]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.add_assoc) q(Rat.add_zero) q(@Rewrite.plus_zero) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Rat Rat Rat _) q(0 : Rat) q(@Rewrite.plus_zero) args)
| .ARITH_MUL_ONE =>
if pf.getArguments[1]![0]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.mul_assoc) q(Rat.mul_one) q(@Rewrite.mul_one) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Rat Rat Rat _) q(1 : Rat) q(@Rewrite.mul_one) args)
| .ARITH_MUL_ZERO =>
if pf.getArguments[1]![0]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.mul_assoc) q(Rat.mul_one) q(@Rewrite.mul_zero) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Rat Rat Rat _) q(1 : Rat) q(@Rewrite.mul_zero) args)
| .ARITH_DIV_TOTAL =>
let t : Q(Rat) ← reconstructTerm pf.getArguments[1]!
let s : Q(Rat) ← reconstructTerm pf.getArguments[2]!
Expand Down Expand Up @@ -181,23 +181,23 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
| .ARITH_PLUS_FLATTEN =>
if pf.getArguments[2]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.add_assoc) q(Rat.add_zero) q(@Rewrite.plus_flatten) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Rat Rat Rat _) q(0 : Rat) q(@Rewrite.plus_flatten) args)
| .ARITH_MULT_FLATTEN =>
if pf.getArguments[2]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.mul_assoc) q(Rat.mul_one) q(@Rewrite.mult_flatten) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Rat Rat Rat _) q(1 : Rat) q(@Rewrite.mult_flatten) args)
| .ARITH_MULT_DIST =>
if pf.getArguments[2]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.mul_assoc) q(Rat.mul_one) q(@Rewrite.mult_dist) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Rat Rat Rat _) q(1 : Rat) q(@Rewrite.mult_dist) args)
| .ARITH_PLUS_CANCEL1 =>
if pf.getArguments[2]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.mul_assoc) q(Rat.mul_one) q(@Rewrite.plus_cancel1) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Rat Rat Rat _) q(0 : Rat) q(@Rewrite.plus_cancel1) args)
| .ARITH_PLUS_CANCEL2 =>
if pf.getArguments[2]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Rat.add_assoc) q(Rat.add_zero) q(@Rewrite.plus_cancel2) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Rat Rat Rat _) q(0 : Rat) q(@Rewrite.plus_cancel2) args)
| .ARITH_ABS_ELIM =>
if pf.getArguments[1]!.getSort.isInteger then return none
let t : Q(Rat) ← reconstructTerm pf.getArguments[1]!
Expand All @@ -208,8 +208,11 @@ where
let mut args' := #[]
for arg in args do
let mut arg' := #[]
for subarg in arg do
arg' := arg'.push (← reconstructTerm subarg)
if arg.getKind == .SEXPR then
for subarg in arg do
arg' := arg'.push (← reconstructTerm subarg)
else
arg' := arg'.push (← reconstructTerm arg)
args' := args'.push arg'
return args'

Expand Down
23 changes: 13 additions & 10 deletions Smt/Reconstruct/Real.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -130,15 +130,15 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
| .ARITH_PLUS_ZERO =>
if pf.getArguments[1]![0]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@add_assoc Real _) q(@add_zero Real _) q(@Rewrite.plus_zero) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Real Real Real _) q(0 : Real) q(@Rewrite.plus_zero) args)
| .ARITH_MUL_ONE =>
if pf.getArguments[1]![0]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@mul_assoc Real _) q(@mul_one Real _) q(@Rewrite.mul_one) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Real Real Real _) q(1 : Real) q(@Rewrite.mul_one) args)
| .ARITH_MUL_ZERO =>
if pf.getArguments[1]![0]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@mul_assoc Real _) q(@mul_one Real _) q(@Rewrite.mul_zero) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Real Real Real _) q(1 : Real) q(@Rewrite.mul_zero) args)
| .ARITH_DIV_TOTAL =>
let t : Q(Real) ← reconstructTerm pf.getArguments[1]!
let s : Q(Real) ← reconstructTerm pf.getArguments[2]!
Expand Down Expand Up @@ -201,23 +201,23 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
| .ARITH_PLUS_FLATTEN =>
if pf.getArguments[2]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@add_assoc Real _) q(@add_zero Real _) q(@Rewrite.plus_flatten) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Real Real Real _) q(0 : Real) q(@Rewrite.plus_flatten) args)
| .ARITH_MULT_FLATTEN =>
if pf.getArguments[2]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@mul_assoc Real _) q(@mul_one Real _) q(@Rewrite.mult_flatten) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Real Real Real _) q(1 : Real) q(@Rewrite.mult_flatten) args)
| .ARITH_MULT_DIST =>
if pf.getArguments[2]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@mul_assoc Real _) q(@mul_one Real _) q(@Rewrite.mult_dist) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Real Real Real _) q(1 : Real) q(@Rewrite.mult_dist) args)
| .ARITH_PLUS_CANCEL1 =>
if pf.getArguments[2]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@mul_assoc Real _) q(@mul_one Real _) q(@Rewrite.plus_cancel1) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Real Real Real _) q(0 : Real) q(@Rewrite.plus_cancel1) args)
| .ARITH_PLUS_CANCEL2 =>
if pf.getArguments[2]!.getSort.isInteger then return none
let args ← reconstructArgs pf.getArguments[1:]
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@add_assoc Real _) q(@add_zero Real _) q(@Rewrite.plus_cancel2) args)
addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Real Real Real _) q(0 : Real) q(@Rewrite.plus_cancel2) args)
| .ARITH_ABS_ELIM =>
if pf.getArguments[1]!.getSort.isInteger then return none
let t : Q(Real) ← reconstructTerm pf.getArguments[1]!
Expand All @@ -228,8 +228,11 @@ where
let mut args' := #[]
for arg in args do
let mut arg' := #[]
for subarg in arg do
arg' := arg'.push (← reconstructTerm subarg)
if arg.getKind == .SEXPR then
for subarg in arg do
arg' := arg'.push (← reconstructTerm subarg)
else
arg' := arg'.push (← reconstructTerm arg)
args' := args'.push arg'
return args'

Expand Down
Loading

0 comments on commit 5b66c53

Please sign in to comment.