Skip to content

Commit e83b436

Browse files
abdoo8080abdoo8080
committed
Sync with main branch.
1 parent 295dc86 commit e83b436

4 files changed

Lines changed: 40 additions & 43 deletions

File tree

‎Smt/Reconstruct.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -36,9 +36,9 @@ structure Reconstruct.State where
3636
proofCache : Std.HashMap cvc5.Proof Expr := {}
3737
count : Nat := 0
3838
currAssums : Array Expr := #[]
39-
skippedGoals : Array MVarId := #[]
4039
/-- finite-fields polynomial context for each prime order. -/
4140
ffCtx : Std.HashMap Nat (Array Expr) := {}
41+
skippedGoals : Array MVarId := #[]
4242

4343
abbrev ReconstructM := ReaderT Reconstruct.Context (StateT Reconstruct.State MetaM)
4444

@@ -239,7 +239,7 @@ partial def reconstructProof (pf : cvc5.Proof) (ctx : Reconstruct.Context) :
239239
let (dfns, state) ← (pf.getArguments.toList.mapM Reconstruct.reconstructTerm).run ctx {}
240240
let (ps, state) ← (pf.getChildren[0]!.getArguments.toList.mapM Reconstruct.reconstructTerm).run ctx state
241241
let ((p : Q(Prop)), state) ← (Reconstruct.reconstructTerm (pf.getResult)).run ctx state
242-
let (h, ⟨_, _, _, _, _, mvs, _⟩) ← (Reconstruct.reconstructProof pf).run ctx state
242+
let (h, ⟨_, _, _, _, _, _, mvs⟩) ← (Reconstruct.reconstructProof pf).run ctx state
243243
if dfns.isEmpty then
244244
let h : Q(True → $p) ← pure h
245245
return (dfns, ps, p, q($h trivial), mvs.toList)
@@ -424,7 +424,7 @@ def solveAndReconstructProof (query : String)
424424
return .unsat none [] uc
425425
-- Reconstruct proof.
426426
let some pf := pf | throwError "failed to reconstruct proof for unsat result"
427-
let (h, ⟨_, _, _, _, _, mvs⟩) ← (Reconstruct.reconstructProof pf).run ctx state
427+
let (h, ⟨_, _, _, _, _, _, mvs⟩) ← (Reconstruct.reconstructProof pf).run ctx state
428428
return .unsat h mvs.toList uc
429429
| .ok (.sat model) =>
430430
-- Return potential counter-example.

‎Smt/Reconstruct/UF.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -98,7 +98,7 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
9898
@[smt_proof_reconstruct] def reconstructUFProof : ProofReconstructor := fun pf => do match pf.getRule with
9999
| .DSL_REWRITE => reconstructRewrite pf
100100
| .REFL =>
101-
if pf.getArguments[0]!.getKind == .FINITE_FIELD_IDEAL then return none
101+
if pf.getArguments[0]!.getKind! == .FINITE_FIELD_IDEAL then return none
102102
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort pf.getArguments[0]!.getSort!
103103
let a : Q($α) ← reconstructTerm pf.getArguments[0]!
104104
addThm q($a = $a) q(Eq.refl $a)

‎Smt/Reconstruct/ZMod.lean‎

Lines changed: 35 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -168,6 +168,7 @@ partial def reify (n : Nat) (e : Q(ZMod $n)) : MvPolynomialM n (Q(MvPolynomial N
168168

169169
end MvPolynomialM
170170

171+
noncomputable
171172
def ideal (ps : List (MvPolynomial Nat (ZMod n))) : Ideal (MvPolynomial Nat (ZMod n)) :=
172173
Ideal.span ps.toFinset
173174

@@ -869,55 +870,55 @@ theorem variety_split_zmod_of_mem [Fact n.Prime]
869870

870871
open Lean
871872
open Qq
872-
@[smt_sort_reconstruct] def reconstructZModSort : SortReconstructor := fun s => do match s.getKind with
873+
@[smt_sort_reconstruct] def reconstructZModSort : SortReconstructor := fun s => do match s.getKind! with
873874
| .FINITE_FIELD_SORT =>
874875
let o : Nat := s.getFiniteFieldSize!
875876
return q(ZMod $o)
876877
| _ => return none
877878

878-
@[smt_term_reconstruct] def reconstructZMod : TermReconstructor := fun t => do match t.getKind with
879+
@[smt_term_reconstruct] def reconstructZMod : TermReconstructor := fun t => do match t.getKind! with
879880
| .CONST_FINITE_FIELD =>
880-
let o : Nat := t.getSort.getFiniteFieldSize!
881-
let v : Nat := (t.getFiniteFieldValue!.toInt! % o).toNat
881+
let o : Nat := t.getSort!.getFiniteFieldSize!
882+
let v : Nat := (t.getFiniteFieldValue! % o).toNat
882883
return mkZModLit o v
883884
| .FINITE_FIELD_ADD =>
884-
let w : Nat := t.getSort.getFiniteFieldSize!
885+
let w : Nat := t.getSort!.getFiniteFieldSize!
885886
rightAssocOp q(@HAdd.hAdd (ZMod $w) (ZMod $w) (ZMod $w) _) t
886887
| .FINITE_FIELD_MULT =>
887-
let w : Nat := t.getSort.getFiniteFieldSize!
888+
let w : Nat := t.getSort!.getFiniteFieldSize!
888889
leftAssocOp q(@HMul.hMul (ZMod $w) (ZMod $w) (ZMod $w) _) t
889890
| .FINITE_FIELD_NEG =>
890-
let w : Nat := t.getSort.getFiniteFieldSize!
891+
let w : Nat := t.getSort!.getFiniteFieldSize!
891892
let x : Q(ZMod $w) ← reconstructTerm t[0]!
892893
return q(-$x)
893894
| .FINITE_FIELD_IDEAL =>
894-
let o : Nat := t[0]!.getSort.getFiniteFieldSize!
895+
let o : Nat := t[0]!.getSort!.getFiniteFieldSize!
895896
let mut ps : Q(List (MvPolynomial Nat (ZMod $o))) := q([])
896897
for i in t.getChildren.reverse do
897898
let p : Q(ZMod $o) ← reconstructTerm i
898899
let p ← MvPolynomialM.reify o p
899900
ps := q($p :: $ps)
900901
return q(ideal $ps)
901902
| .FINITE_FIELD_VARIETY =>
902-
let o: Nat := t.getSort.getSetElementSort!.getFiniteFieldSize!
903+
let o: Nat := t.getSort!.getSetElementSort!.getFiniteFieldSize!
903904
let ho : Q(Fact «$o».Prime) ← Meta.synthInstance q(Fact «$o».Prime)
904905
let s : Q(Ideal (MvPolynomial Nat (ZMod $o))) ← reconstructTerm t[0]!
905906
return q(@variety $o $ho $s)
906907
| .SET_MEMBER =>
907-
if t[1]!.getKind != .FINITE_FIELD_IDEAL then return none
908-
let o : Nat := t[0]!.getSort.getFiniteFieldSize!
908+
if t[1]!.getKind! != .FINITE_FIELD_IDEAL then return none
909+
let o : Nat := t[0]!.getSort!.getFiniteFieldSize!
909910
let x : Q(ZMod $o) ← reconstructTerm t[0]!
910911
let x ← MvPolynomialM.reify o x
911912
let s : Q(Ideal (MvPolynomial Nat (ZMod $o))) ← reconstructTerm t[1]!
912913
return q($x ∈ $s)
913914
| .SET_IS_EMPTY =>
914-
if t[0]!.getKind != .FINITE_FIELD_VARIETY then return none
915-
let o : Nat := t[0]!.getSort.getSetElementSort!.getFiniteFieldSize!
915+
if t[0]!.getKind! != .FINITE_FIELD_VARIETY then return none
916+
let o : Nat := t[0]!.getSort!.getSetElementSort!.getFiniteFieldSize!
916917
let s : Q(Set (Nat → ZMod $o)) ← reconstructTerm t[0]!
917918
return q($s = ∅)
918919
| .SKOLEM => match t.getSkolemId! with
919920
| .FF_DISEQ =>
920-
let o : Nat := t.getSort.getFiniteFieldSize!
921+
let o : Nat := t.getSort!.getFiniteFieldSize!
921922
let t := t.getSkolemIndices![0]! -- (not (= a b))
922923
let a : Q(ZMod $o) ← reconstructTerm (t[0]!)[0]!
923924
let b : Q(ZMod $o) ← reconstructTerm (t[0]!)[1]!
@@ -952,14 +953,14 @@ open Qq
952953
| .DSL_REWRITE
953954
| .THEORY_REWRITE => reconstructRewrite pf
954955
| .REFL =>
955-
if pf.getArguments[0]!.getKind != .FINITE_FIELD_IDEAL then return none
956-
let o : Nat := pf.getArguments[0]!.getSort.getSetElementSort!.getFiniteFieldSize!
956+
if pf.getArguments[0]!.getKind! != .FINITE_FIELD_IDEAL then return none
957+
let o : Nat := pf.getArguments[0]!.getSort!.getSetElementSort!.getFiniteFieldSize!
957958
let a : Q(Ideal (MvPolynomial Nat (ZMod $o))) ← reconstructTerm pf.getArguments[0]!
958959
addThm q($a = $a) q(Eq.refl $a)
959960
| .CONG =>
960-
if pf.getResult[0]!.getKind != .SET_MEMBER || (pf.getResult[0]!)[1]!.getKind != .FINITE_FIELD_IDEAL then
961+
if pf.getResult[0]!.getKind! != .SET_MEMBER || (pf.getResult[0]!)[1]!.getKind! != .FINITE_FIELD_IDEAL then
961962
return none
962-
let o : Nat ← pure (pf.getResult[0]!)[0]!.getSort.getFiniteFieldSize!
963+
let o : Nat ← pure (pf.getResult[0]!)[0]!.getSort!.getFiniteFieldSize!
963964
let e₁ : Q(ZMod $o) ← reconstructTerm (pf.getResult[0]!)[0]!
964965
let e₂ : Q(ZMod $o) ← reconstructTerm (pf.getResult[1]!)[0]!
965966
let e₁ ← Expr.reify o e₁
@@ -979,7 +980,7 @@ open Qq
979980
addThm q((«$e₁».toPoly ∈ $s₁) = («$e₂».toPoly ∈ $s₂)) q(Expr.elem_congr $he $hs)
980981
| .FF_POLY_CONVERSION =>
981982
let ps := ((pf.getResult[0]!)[0]!)[0]!.getChildren
982-
let o : Nat ← pure ps[0]!.getSort.getFiniteFieldSize!
983+
let o : Nat ← pure ps[0]!.getSort!.getFiniteFieldSize!
983984
let ho : Q(Fact «$o».Prime) ← Meta.synthInstance q(Fact «$o».Prime)
984985
let reconstructZMEs := fun (t : cvc5.Term) (acc : Q(List (Expr $o))) => do
985986
let p : Q(ZMod $o) ← reconstructTerm t
@@ -993,7 +994,7 @@ open Qq
993994
let h : Q(andN («$ps».map fun p => p.eval $ctx = 0)) ← reconstructProof pf.getChildren[0]!
994995
addThm q(variety (ideal («$ps».map Expr.toPoly)) ≠ ∅) q(@Expr.variety_nonempty_of_eval_eq_zero $o $ctx $ho $ps $h)
995996
| .FF_POLY_NORM =>
996-
let o : Nat := pf.getResult[0]!.getSort.getFiniteFieldSize!
997+
let o : Nat := pf.getResult[0]!.getSort!.getFiniteFieldSize!
997998
let a : Q(ZMod $o) ← reconstructTerm pf.getResult[0]!
998999
let b : Q(ZMod $o) ← reconstructTerm pf.getResult[1]!
9991000
let l : Q(Expr $o) ← Expr.reify o a
@@ -1002,7 +1003,7 @@ open Qq
10021003
let tac := if ← useNative then ZMod.nativePolyNorm o l r is else ZMod.polyNorm o l r is
10031004
addTac q($a = $b) tac
10041005
| .FF_POLY_NORM_EQ =>
1005-
let o : Nat := (pf.getChildren[0]!.getResult[0]!)[0]!.getSort.getFiniteFieldSize!
1006+
let o : Nat := (pf.getChildren[0]!.getResult[0]!)[0]!.getSort!.getFiniteFieldSize!
10061007
let ho : Q(Fact «$o».Prime) ← Meta.synthInstance q(Fact «$o».Prime)
10071008
let cx : Q(ZMod $o) ← reconstructTerm (pf.getChildren[0]!.getResult[0]!)[0]!
10081009
let cy : Q(ZMod $o) ← reconstructTerm (pf.getChildren[0]!.getResult[1]!)[0]!
@@ -1015,7 +1016,7 @@ open Qq
10151016
let h : Q($cx * ($x₁ + -$x₂) = $cy * ($y₁ + -$y₂)) ← reconstructProof pf.getChildren[0]!
10161017
addThm q(($x₁ = $x₂) = ($y₁ = $y₂)) q(@eq_of_add_neg_eq $o $x₁ $x₂ $y₁ $y₂ $ho $cx $cy $hcx $hcy $h)
10171018
| .FF_IDEAL_GENERATOR =>
1018-
let o : Nat := pf.getResult[0]!.getSort.getFiniteFieldSize!
1019+
let o : Nat := pf.getResult[0]!.getSort!.getFiniteFieldSize!
10191020
let y : Q(ZMod $o) ← reconstructTerm pf.getResult[0]!
10201021
let y ← MvPolynomialM.reify o y
10211022
let ps := pf.getResult[1]!.getChildren
@@ -1029,7 +1030,7 @@ open Qq
10291030
let zs ← zs.foldrM reconstructMVPs q([])
10301031
addThm q($y ∈ ideal ($xs ++ $y :: $zs)) q(@ideal_generator $o $xs $y $zs)
10311032
| .FF_ONE_UNSAT =>
1032-
let o : Nat := pf.getChildren[0]!.getResult[0]!.getSort.getFiniteFieldSize!
1033+
let o : Nat := pf.getChildren[0]!.getResult[0]!.getSort!.getFiniteFieldSize!
10331034
let ho : Q(Fact «$o».Prime) ← Meta.synthInstance q(Fact «$o».Prime)
10341035
let ps := pf.getChildren[0]!.getResult[1]!.getChildren
10351036
let reconstructMVPs := fun (t : cvc5.Term) (acc : Q(List (MvPolynomial Nat (ZMod $o)))) => do
@@ -1040,13 +1041,13 @@ open Qq
10401041
let h : Q(1 ∈ ideal $ps) ← reconstructProof pf.getChildren[0]!
10411042
addThm q(variety (ideal $ps) = ∅) q(@one_unsat $o $ho $ps $h)
10421043
| .FF_DISEQ =>
1043-
let o : Nat := pf.getArguments[0]!.getSort.getFiniteFieldSize!
1044+
let o : Nat := pf.getArguments[0]!.getSort!.getFiniteFieldSize!
10441045
let ho : Q(Fact «$o».Prime) ← Meta.synthInstance q(Fact «$o».Prime)
10451046
let l : Q(ZMod $o) ← reconstructTerm pf.getArguments[0]!
10461047
let r : Q(ZMod $o) ← reconstructTerm pf.getArguments[1]!
10471048
addThm q(($l ≠ $r) = (($l + -$r) * Classical.epsilon (fun x => ($l + -$r) * x + -1 = 0) + -1 = 0)) q(@diseq $o $ho $l $r)
10481049
| .FF_POLY_COMBINATION =>
1049-
let o : Nat := pf.getResult[0]!.getSort.getFiniteFieldSize!
1050+
let o : Nat := pf.getResult[0]!.getSort!.getFiniteFieldSize!
10501051
let reconstructMVPs := fun (t : cvc5.Term) (acc : Q(List (MvPolynomial Nat (ZMod $o)))) => do
10511052
let p : Q(ZMod $o) ← reconstructTerm t
10521053
let p ← MvPolynomialM.reify o p
@@ -1068,7 +1069,7 @@ open Qq
10681069
let h : Q(andN (List.map (fun r => r ∈ ideal $ps) $rs)) := hq
10691070
addThm q(addN (List.zipWith (· * ·) $ms $rs) ∈ ideal $ps) q(@poly_combination $o $ps $ms $rs $h)
10701071
| .FF_ROOT_BRANCH =>
1071-
let o : Nat := pf.getArguments[2]!.getSort.getFiniteFieldSize!
1072+
let o : Nat := pf.getArguments[2]!.getSort!.getFiniteFieldSize!
10721073
let ho : Q(Fact «$o».Prime) ← Meta.synthInstance q(Fact «$o».Prime)
10731074
let reconstructMVPs := fun (t : cvc5.Term) (acc : Q(List (MvPolynomial Nat (ZMod $o)))) => do
10741075
let p : Q(ZMod $o) ← reconstructTerm t
@@ -1099,15 +1100,11 @@ where
10991100
return .app q(@of_decide_eq_true $p $hp) q(Eq.refl true)
11001101
nativeDecide (p : Q(Prop)) : MetaM Q($p) := do
11011102
let hp : Q(Decidable $p) ← Meta.synthInstance q(Decidable $p)
1102-
let auxDeclName ← mkNativeAuxDecl `_nativePolynorm q(Bool) q(decide $p)
1103-
let b : Q(Bool) := .const auxDeclName []
1104-
return .app q(@of_decide_eq_true $p $hp) (.app q(Lean.ofReduceBool $b true) q(Eq.refl true))
1105-
mkNativeAuxDecl (baseName : Name) (type value : Lean.Expr) : MetaM Name := do
1106-
let auxName ← Lean.mkAuxDeclName baseName
1107-
let decl := Declaration.defnDecl {
1108-
name := auxName, levelParams := [], type, value
1109-
hints := .abbrev
1110-
safety := .safe
1111-
}
1112-
addAndCompile decl
1113-
pure auxName
1103+
match ← Meta.nativeEqTrue `Smt.rootBranch q(decide $p) with
1104+
| .notTrue =>
1105+
throwError m!"[ff_root_branch] evaluated that the proposition
1106+
{indentExpr q(decide $p)}\n\
1107+
is false"
1108+
| .success hdp =>
1109+
-- get instance from `d`
1110+
return .app q(@of_decide_eq_true $p $hp) hdp

‎lake-manifest.json‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@
1515
"type": "git",
1616
"subDir": null,
1717
"scope": "",
18-
"rev": "6a5991ee9b5f671249fa2b2c2118eab5c5663ae2",
18+
"rev": "e18693d477b9af96221463cf05c417c1ef36caf3",
1919
"name": "cvc5",
2020
"manifestFile": "lake-manifest.json",
2121
"inputRev": "finite-fields-tag",

0 commit comments

Comments
 (0)