Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Sync with cvc5 main. #144

Merged
merged 2 commits into from
Nov 17, 2024
Merged

Sync with cvc5 main. #144

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
56ed72d
Sync with cvc5 main.
abdoo8080 Nov 17, 2024
6b6b0ab
Add missing rule for Reals.
abdoo8080 Nov 17, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Smt/Reconstruct.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -219,7 +219,7 @@ def solve (query : String) (timeout : Option Nat) : MetaM (Except Error cvc5.Pro
if h : 0 < ps.size then
trace[smt.solve] "proof:\n{← Solver.proofToString ps[0]}"
return ps[0]
throw (self := instMonadExceptOfMonadExceptOf _ _) (Error.user_error "something went wrong")
throw (self := instMonadExceptOfMonadExceptOf _ _) (Error.error s!"Expected unsat, got {r}")

syntax (name := reconstruct) "reconstruct" str : tactic

Expand Down
2 changes: 1 addition & 1 deletion Smt/Reconstruct/Arith/Rewrites.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ theorem arith_div_by_const_elim_real_pos {t c₁ c₂ : Real} : t / (c₁ / c₂
theorem arith_div_by_const_elim_real_neg {t c₁ c₂ : Real} : t / (-c₁ / c₂) = t * (-c₂ / c₁) :=
div_eq_mul_one_div t (-c₁ / c₂) ▸ one_div_div (-c₁) c₂ ▸ div_neg c₂ ▸ neg_div c₁ c₂ ▸ rfl

-- https://github.com/cvc5/cvc5/blob/proof-new/src/theory/arith/rewrites
-- https://github.com/cvc5/cvc5/blob/main/src/theory/arith/rewrites

variable {α : Type} [h : LinearOrderedRing α]

Expand Down
110 changes: 55 additions & 55 deletions Smt/Reconstruct/BitVec.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,12 +22,12 @@ open Lean Qq

@[smt_sort_reconstruct] def reconstructBitVecSort : SortReconstructor := fun s => do match s.getKind with
| .BITVECTOR_SORT =>
let w : Nat := s.getBitVectorSize.val
let w : Nat := s.getBitVectorSize!.val
return q(BitVec $w)
| _ => return none

partial def synthDecidableInst (t : cvc5.Term) : ReconstructM Expr := do match t.getKind with
| .CONST_BOOLEAN => return if t.getBooleanValue then q(instDecidableTrue) else q(instDecidableFalse)
| .CONST_BOOLEAN => return if t.getBooleanValue! then q(instDecidableTrue) else q(instDecidableFalse)
| .NOT =>
let p : Q(Prop) ← reconstructTerm t[0]!
let hp : Q(Decidable $p) ← synthDecidableInst t[0]!
Expand All @@ -43,14 +43,14 @@ partial def synthDecidableInst (t : cvc5.Term) : ReconstructM Expr := do match t
let hq : Q(Decidable $q) ← synthDecidableInst t[1]!
return q(@instDecidableEqOfIff $p $q (@instDecidableIff $p $q $hp $hq))
if t[0]!.getSort.getKind == .BITVECTOR_SORT then
let w : Nat := t[0]!.getSort.getBitVectorSize.val
let w : Nat := t[0]!.getSort.getBitVectorSize!.val
return q(@instDecidableEqBitVec $w)
let p : Q(Prop) ← reconstructTerm t
Meta.synthInstance q(Decidable $p)
| .BITVECTOR_BIT =>
let w : Nat := t[0]!.getSort.getBitVectorSize.val
let w : Nat := t[0]!.getSort.getBitVectorSize!.val
let x : Q(BitVec $w) ← reconstructTerm t[0]!
let i : Nat := t.getOp[0]!.getIntegerValue.toNat
let i : Nat := t.getOp![0]!.getIntegerValue!.toNat
return q(instDecidableEqBool («$x».getLsbD $i) true)
| _ =>
let p : Q(Prop) ← reconstructTerm t
Expand All @@ -67,152 +67,152 @@ where

@[smt_term_reconstruct] def reconstructBitVec : TermReconstructor := fun t => do match t.getKind with
| .CONST_BITVECTOR =>
let w : Nat := t.getSort.getBitVectorSize.val
let v : Nat := (t.getBitVectorValue 10).toNat!
let w : Nat := t.getSort.getBitVectorSize!.val
let v : Nat := (t.getBitVectorValue! 10).toNat!
return q(BitVec.ofNat $w $v)
| .BITVECTOR_CONCAT =>
let n : Nat := t.getNumChildren
let w₁ : Nat := t[0]!.getSort.getBitVectorSize.val
let w₁ : Nat := t[0]!.getSort.getBitVectorSize!.val
let a : Q(BitVec $w₁) ← reconstructTerm t[0]!
let f := fun ⟨w₁, a⟩ i => do
let w₂ : Nat := t[i]!.getSort.getBitVectorSize.val
let w₂ : Nat := t[i]!.getSort.getBitVectorSize!.val
let x : Q(BitVec $w₂) ← reconstructTerm t[i]!
return ⟨q($w₁ + $w₂), q($a ++ $x)⟩
let ⟨_, a⟩ ← [1:n].foldlM f (⟨q($w₁), a⟩ : Σ w : Q(Nat), Q(BitVec $w))
return a
| .BITVECTOR_AND =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
leftAssocOp q(@AndOp.and (BitVec $w) _) t
| .BITVECTOR_OR =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
leftAssocOp q(@OrOp.or (BitVec $w) _) t
| .BITVECTOR_XOR =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
leftAssocOp q(@Xor.xor (BitVec $w) _) t
| .BITVECTOR_NOT =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
let x : Q(BitVec $w) ← reconstructTerm t[0]!
return q(~~~$x)
| .BITVECTOR_MULT =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
leftAssocOp q(@HMul.hMul (BitVec $w) (BitVec $w) (BitVec $w) _) t
| .BITVECTOR_ADD =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
leftAssocOp q(@HAdd.hAdd (BitVec $w) (BitVec $w) (BitVec $w) _) t
| .BITVECTOR_SUB =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
leftAssocOp q(@HSub.hSub (BitVec $w) (BitVec $w) (BitVec $w) _) t
| .BITVECTOR_NEG =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
let x : Q(BitVec $w) ← reconstructTerm t[0]!
return q(-$x)
| .BITVECTOR_UDIV =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
let x : Q(BitVec $w) ← reconstructTerm t[0]!
let y : Q(BitVec $w) ← reconstructTerm t[1]!
return q(BitVec.smtUDiv $x $y)
| .BITVECTOR_UREM =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
let x : Q(BitVec $w) ← reconstructTerm t[0]!
let y : Q(BitVec $w) ← reconstructTerm t[1]!
return q($x % $y)
| .BITVECTOR_SDIV =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
let x : Q(BitVec $w) ← reconstructTerm t[0]!
let y : Q(BitVec $w) ← reconstructTerm t[1]!
return q(BitVec.smtSDiv $x $y)
| .BITVECTOR_SREM =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
let x : Q(BitVec $w) ← reconstructTerm t[0]!
let y : Q(BitVec $w) ← reconstructTerm t[1]!
return q(BitVec.srem $x $y)
| .BITVECTOR_SMOD =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
let x : Q(BitVec $w) ← reconstructTerm t[0]!
let y : Q(BitVec $w) ← reconstructTerm t[1]!
return q(BitVec.smod $x $y)
| .BITVECTOR_SHL =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
let x : Q(BitVec $w) ← reconstructTerm t[0]!
let i : Nat := t.getOp[0]!.getIntegerValue.toNat
let i : Nat := t.getOp![0]!.getIntegerValue!.toNat
return q($x <<< $i)
| .BITVECTOR_LSHR =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
let x : Q(BitVec $w) ← reconstructTerm t[0]!
let i : Nat := t.getOp[0]!.getIntegerValue.toNat
let i : Nat := t.getOp![0]!.getIntegerValue!.toNat
return q($x >>> $i)
| .BITVECTOR_ASHR =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
let x : Q(BitVec $w) ← reconstructTerm t[0]!
let i : Nat := t.getOp[0]!.getIntegerValue.toNat
let i : Nat := t.getOp![0]!.getIntegerValue!.toNat
return q(BitVec.sshiftRight $x $i)
| .BITVECTOR_ULT =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
let x : Q(BitVec $w) ← reconstructTerm t[0]!
let y : Q(BitVec $w) ← reconstructTerm t[1]!
return q($x < $y)
| .BITVECTOR_ULE =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
let x : Q(BitVec $w) ← reconstructTerm t[0]!
let y : Q(BitVec $w) ← reconstructTerm t[1]!
return q($x ≤ $y)
| .BITVECTOR_UGT =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
let x : Q(BitVec $w) ← reconstructTerm t[0]!
let y : Q(BitVec $w) ← reconstructTerm t[1]!
return q($x > $y)
| .BITVECTOR_UGE =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
let x : Q(BitVec $w) ← reconstructTerm t[0]!
let y : Q(BitVec $w) ← reconstructTerm t[1]!
return q($x ≥ $y)
| .BITVECTOR_SLT =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
let x : Q(BitVec $w) ← reconstructTerm t[0]!
let y : Q(BitVec $w) ← reconstructTerm t[1]!
return q(BitVec.slt $x $y)
| .BITVECTOR_SLE =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
let x : Q(BitVec $w) ← reconstructTerm t[0]!
let y : Q(BitVec $w) ← reconstructTerm t[1]!
return q(BitVec.sle $x $y)
| .BITVECTOR_EXTRACT =>
let w : Nat := t.getSort.getBitVectorSize.val
let i : Nat := t.getOp[0]!.getIntegerValue.toNat
let j : Nat := t.getOp[1]!.getIntegerValue.toNat
let w : Nat := t.getSort.getBitVectorSize!.val
let i : Nat := t.getOp![0]!.getIntegerValue!.toNat
let j : Nat := t.getOp![1]!.getIntegerValue!.toNat
let x : Q(BitVec $w) ← reconstructTerm t[0]!
return q(«$x».extractLsb $i $j)
| .BITVECTOR_REPEAT =>
let w : Nat := t.getSort.getBitVectorSize.val
let n : Nat := t.getOp[0]!.getIntegerValue.toNat
let w : Nat := t.getSort.getBitVectorSize!.val
let n : Nat := t.getOp![0]!.getIntegerValue!.toNat
let x : Q(BitVec $w) ← reconstructTerm t[0]!
return q(«$x».replicate $n)
| .BITVECTOR_ZERO_EXTEND =>
let w : Nat := t.getSort.getBitVectorSize.val
let n : Nat := t.getOp[0]!.getIntegerValue.toNat
let w : Nat := t.getSort.getBitVectorSize!.val
let n : Nat := t.getOp![0]!.getIntegerValue!.toNat
let x : Q(BitVec $w) ← reconstructTerm t[0]!
return q(«$x».zeroExtend $n)
| .BITVECTOR_SIGN_EXTEND =>
let w : Nat := t.getSort.getBitVectorSize.val
let n : Nat := t.getOp[0]!.getIntegerValue.toNat
let w : Nat := t.getSort.getBitVectorSize!.val
let n : Nat := t.getOp![0]!.getIntegerValue!.toNat
let x : Q(BitVec $w) ← reconstructTerm t[0]!
return q(«$x».signExtend $n)
| .BITVECTOR_ROTATE_LEFT =>
let w : Nat := t.getSort.getBitVectorSize.val
let n : Nat := t.getOp[0]!.getIntegerValue.toNat
let w : Nat := t.getSort.getBitVectorSize!.val
let n : Nat := t.getOp![0]!.getIntegerValue!.toNat
let x : Q(BitVec $w) ← reconstructTerm t[0]!
return q(«$x».rotateLeft $n)
| .BITVECTOR_ROTATE_RIGHT =>
let w : Nat := t.getSort.getBitVectorSize.val
let n : Nat := t.getOp[0]!.getIntegerValue.toNat
let w : Nat := t.getSort.getBitVectorSize!.val
let n : Nat := t.getOp![0]!.getIntegerValue!.toNat
let x : Q(BitVec $w) ← reconstructTerm t[0]!
return q(«$x».rotateRight $n)
| .INT_TO_BITVECTOR =>
let w : Nat := t.getSort.getBitVectorSize.val
let w : Nat := t.getSort.getBitVectorSize!.val
let x : Q(Int) ← reconstructTerm t[0]!
return q(BitVec.ofNat $w «$x».toNat)
| .BITVECTOR_TO_NAT =>
let w : Nat := t[0]!.getSort.getBitVectorSize.val
let w : Nat := t[0]!.getSort.getBitVectorSize!.val
let x : Q(BitVec $w) ← reconstructTerm t[0]!
return q(«$x».toNat)
| .BITVECTOR_FROM_BOOLS =>
Expand All @@ -226,9 +226,9 @@ where
let bs : Q(BitVec $w) ← (List.range w).foldlM f bs
return q($bs)
| .BITVECTOR_BIT =>
let w : Nat := t[0]!.getSort.getBitVectorSize.val
let w : Nat := t[0]!.getSort.getBitVectorSize!.val
let x : Q(BitVec $w) ← reconstructTerm t[0]!
let i : Nat := t.getOp[0]!.getIntegerValue.toNat
let i : Nat := t.getOp![0]!.getIntegerValue!.toNat
return q(«$x».getLsbD $i = true)
| _ => return none
where
Expand All @@ -248,12 +248,12 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
let t := pf.getArguments[0]![0]!
match t.getKind with
| .CONST_BITVECTOR =>
let w : Nat := t.getSort.getBitVectorSize.toNat
let w : Nat := t.getSort.getBitVectorSize!.toNat
let t : Q(BitVec $w) ← reconstructTerm pf.getResult[0]!
let t' : Q(BitVec $w) ← reconstructTerm pf.getResult[1]!
addThm q($t = $t') q(Eq.refl $t)
| .CONSTANT =>
let w : Nat := t.getSort.getBitVectorSize.toNat
let w : Nat := t.getSort.getBitVectorSize!.toNat
let x : Q(BitVec $w) ← reconstructTerm pf.getResult[0]!
let x' : Q(BitVec $w) ← reconstructTerm pf.getResult[1]!
let h : Q(«$x».bb = $x') ← Meta.mkFreshExprMVar q(«$x».bb = $x')
Expand All @@ -266,7 +266,7 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
mv.refl
addThm q($x = $x') q(Eq.trans (BitVec.self_eq_bb $x) $h)
| .EQUAL =>
let w : Nat := t[0]!.getSort.getBitVectorSize.toNat
let w : Nat := t[0]!.getSort.getBitVectorSize!.toNat
let x : Q(BitVec $w) ← reconstructTerm pf.getResult[0]![0]!
let y : Q(BitVec $w) ← reconstructTerm pf.getResult[0]![1]!
let p : Q(Prop) ← reconstructTerm pf.getResult[1]!
Expand All @@ -283,7 +283,7 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
mv.refl
addThm q(($x = $y) = $p) q(Eq.trans (BitVec.eq_eq_beq $x $y) (Bool.eq_of_decide_eq $h))
| .BITVECTOR_ADD =>
let w : Nat := t[0]!.getSort.getBitVectorSize.toNat
let w : Nat := t[0]!.getSort.getBitVectorSize!.toNat
let x : Q(BitVec $w) ← reconstructTerm pf.getResult[0]![0]!
let y : Q(BitVec $w) ← reconstructTerm pf.getResult[0]![1]!
let z : Q(BitVec $w) ← reconstructTerm pf.getResult[1]!
Expand Down
16 changes: 8 additions & 8 deletions Smt/Reconstruct/Builtin.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,11 +16,11 @@ open Lean Qq

@[smt_sort_reconstruct] def reconstructBuiltinSort : SortReconstructor := fun s => do match s.getKind with
| .FUNCTION_SORT =>
let mut ct : Q(Type) ← reconstructSort s.getFunctionCodomainSort
let mut ct : Q(Type) ← reconstructSort s.getFunctionCodomainSort!
let f s (a : Q(Type)) := do
let t : Q(Type) ← reconstructSort s
return q($t → $a)
let t ← s.getFunctionDomainSorts.foldrM f ct
let t ← s.getFunctionDomainSorts!.foldrM f ct
return t
| _ => return none

Expand All @@ -40,7 +40,7 @@ def getFVarOrConstExpr! (n : String) : ReconstructM Expr := do

@[smt_term_reconstruct] def reconstructBuiltin : TermReconstructor := fun t => do match t.getKind with
| .VARIABLE => getFVarExpr! (getVariableName t)
| .CONSTANT => getFVarOrConstExpr! t.getSymbol
| .CONSTANT => getFVarOrConstExpr! t.getSymbol!
| .EQUAL =>
let α : Q(Type) ← reconstructSort t[0]!.getSort
let x : Q($α) ← reconstructTerm t[0]!
Expand All @@ -61,17 +61,17 @@ def getFVarOrConstExpr! (n : String) : ReconstructM Expr := do
let x : Q($α) ← reconstructTerm t[1]!
let y : Q($α) ← reconstructTerm t[2]!
return q(@ite $α $c $h $x $y)
| .SKOLEM => match t.getSkolemId with
| .PURIFY => reconstructTerm t.getSkolemIndices[0]!
| .SKOLEM => match t.getSkolemId! with
| .PURIFY => reconstructTerm t.getSkolemIndices![0]!
| _ => return none
| _ => return none
where
getVariableName (t : cvc5.Term) : Name :=
if t.hasSymbol then
if t.getSymbol.toName == .anonymous then
Name.mkSimple t.getSymbol
if t.getSymbol!.toName == .anonymous then
Name.mkSimple t.getSymbol!
else
t.getSymbol.toName
t.getSymbol!.toName
else Name.num `x t.getId

def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
Expand Down
2 changes: 1 addition & 1 deletion Smt/Reconstruct/Builtin/Rewrites.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ Authors: Abdalrhman Mohamed

namespace Smt.Reconstruct.Builtin

-- https://github.com/cvc5/cvc5/blob/proof-new/src/theory/builtin/rewrites
-- https://github.com/cvc5/cvc5/blob/main/src/theory/builtin/rewrites

-- ITE

Expand Down
Loading