chore: merge with main

ufmg-smite · Jul 8, 2024 · 013047f · 013047f
2 parents 86acef5 + 91ac7f4
commit 013047f
Show file tree

Hide file tree

Showing 60 changed files with 1,462 additions and 218 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -25,5 +25,6 @@ jobs:
         lake update
         lake build
         lake build +Smt:dynlib
+        lake build +Smt.Real:dynlib
     - name: Test lean-smt
       run: lake run test
diff --git a/Smt.lean b/Smt.lean
@@ -5,10 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Abdalrhman Mohamed
 -/
 
-import Smt.Arith
 import Smt.BitVec
 import Smt.Bool
 import Smt.Builtin
+import Smt.Int
 import Smt.Nat
 import Smt.Options
 import Smt.Prop

diff --git a/Smt/Data/Sexp.lean b/Smt/Data/Sexp.lean
@@ -83,9 +83,9 @@ partial def parseOneAux : List Substring → Except ParseError (Sexp × List Sub
       return (atom tk.toString, tks)
   | [] => throw <| .incomplete "expected a token, got none"
 
-partial def parseManyAux :=
+partial def parseManyAux : List Substring → Except ParseError (Array Sexp × List Substring) :=
   go #[]
-where go (stk : Array Sexp) : List Substring → Except ParseError (Array Sexp × List Substring)
+where go (stk : Array Sexp)
   | tk :: tks => do
     if tk.front == ')' then .ok (stk, tk :: tks)
     else

diff --git a/Smt/Real.lean b/Smt/Real.lean
@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2021-2023 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Abdalrhman Mohamed
+-/
+
+import Smt.Reconstruct.Real
+import Smt.Translate.Real
diff --git a/Smt/Reconstruct.lean b/Smt/Reconstruct.lean
@@ -203,6 +203,7 @@ def solve (query : String) (timeout : Option Nat) : MetaM (Except Error cvc5.Pro
     if r.isUnsat then
       let ps ← Solver.getProof
       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")
 

diff --git a/Smt/Reconstruct/BitVec.lean b/Smt/Reconstruct/BitVec.lean
@@ -47,7 +47,7 @@ partial def synthDecidableInst (t : cvc5.Term) : ReconstructM Expr := do match t
         return q(@instDecidableEqBitVec $w)
       let p : Q(Prop) ← reconstructTerm t
       Meta.synthInstance q(Decidable $p)
-    | .BITVECTOR_BITOF =>
+    | .BITVECTOR_BIT =>
       let w : Nat := t[0]!.getSort.getBitVectorSize.val
       let x : Q(BitVec $w) ← reconstructTerm t[0]!
       let i : Nat := t.getOp[0]!.getIntegerValue.toNat
@@ -70,16 +70,6 @@ where
     let w : Nat := t.getSort.getBitVectorSize.val
     let v : Nat := (t.getBitVectorValue 10).toNat!
     return q(BitVec.ofNat $w $v)
-  | .BITVECTOR_BB_TERM =>
-    let w : Nat := t.getNumChildren
-    let bs : Q(BitVec 0) := q(.nil)
-    let f (bs : Expr) (i : Nat) : ReconstructM Expr := do
-      let p : Q(Prop) ← reconstructTerm t[i]!
-      let bs : Q(BitVec $i) := bs
-      let hp : Q(Decidable $p) ← synthDecidableInst t[i]!
-      return q(@BitVec.cons $i (@decide $p $hp) $bs)
-    let bs : Q(BitVec $w) ← (List.range w).foldlM f bs
-    return q($bs)
   | .BITVECTOR_CONCAT =>
     let n : Nat := t.getNumChildren
     let w₁ : Nat := t[0]!.getSort.getBitVectorSize.val
@@ -192,11 +182,6 @@ where
     let j : Nat := t.getOp[1]!.getIntegerValue.toNat
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
     return q(«$x».extractLsb $i $j)
-  | .BITVECTOR_BITOF =>
-    let w : Nat := t[0]!.getSort.getBitVectorSize.val
-    let x : Q(BitVec $w) ← reconstructTerm t[0]!
-    let i : Nat := t.getOp[0]!.getIntegerValue.toNat
-    return q(«$x».getLsb $i = true)
   | .BITVECTOR_REPEAT =>
     let w : Nat := t.getSort.getBitVectorSize.val
     let n : Nat := t.getOp[0]!.getIntegerValue.toNat
@@ -230,6 +215,21 @@ where
     let w : Nat := t[0]!.getSort.getBitVectorSize.val
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
     return q(«$x».toNat)
+  | .BITVECTOR_FROM_BOOLS =>
+    let w : Nat := t.getNumChildren
+    let bs : Q(BitVec 0) := q(.nil)
+    let f (bs : Expr) (i : Nat) : ReconstructM Expr := do
+      let p : Q(Prop) ← reconstructTerm t[i]!
+      let bs : Q(BitVec $i) := bs
+      let hp : Q(Decidable $p) ← synthDecidableInst t[i]!
+      return q(@BitVec.cons $i (@decide $p $hp) $bs)
+    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 x : Q(BitVec $w) ← reconstructTerm t[0]!
+    let i : Nat := t.getOp[0]!.getIntegerValue.toNat
+    return q(«$x».getLsb $i = true)
   | _ => return none
 where
   leftAssocOp (op : Expr) (t : cvc5.Term) : ReconstructM Expr := do

diff --git a/Smt/Reconstruct/Int.lean b/Smt/Reconstruct/Int.lean
@@ -7,7 +7,6 @@ Authors: Abdalrhman Mohamed
 
 import Smt.Reconstruct
 import Smt.Reconstruct.Builtin.Lemmas
-import Smt.Reconstruct.Int.Core
 import Smt.Reconstruct.Int.Lemmas
 import Smt.Reconstruct.Int.Polynorm
 import Smt.Reconstruct.Int.Rewrites
@@ -150,14 +149,14 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
     let t : Q(Int) ← reconstructTerm pf.getArguments[1]!
     let s : Q(Int) ← reconstructTerm pf.getArguments[2]!
     addThm q(($t < $s) = ¬($t ≥ $s)) q(@Rewrite.elim_lt $t $s)
-  -- | .ARITH_ELIM_INT_GT =>
-  --   let t : Q(Int) ← reconstructTerm pf.getArguments[1]!
-  --   let s : Q(Int) ← reconstructTerm pf.getArguments[2]!
-  --   addThm q(($t > $s) = ($t ≥ $s + 1)) q(@Rewrite.elim_int_gt $t $s)
-  -- | .ARITH_ELIM_INT_LT =>
-  --   let t : Q(Int) ← reconstructTerm pf.getArguments[1]!
-  --   let s : Q(Int) ← reconstructTerm pf.getArguments[2]!
-  --   addThm q(($t < $s) = ($s ≥ $t + 1)) q(@Rewrite.elim_int_lt $t $s)
+  | .ARITH_ELIM_INT_GT =>
+    let t : Q(Int) ← reconstructTerm pf.getArguments[1]!
+    let s : Q(Int) ← reconstructTerm pf.getArguments[2]!
+    addThm q(($t > $s) = ($t ≥ $s + 1)) q(@Rewrite.elim_int_gt $t $s)
+  | .ARITH_ELIM_INT_LT =>
+    let t : Q(Int) ← reconstructTerm pf.getArguments[1]!
+    let s : Q(Int) ← reconstructTerm pf.getArguments[2]!
+    addThm q(($t < $s) = ($s ≥ $t + 1)) q(@Rewrite.elim_int_lt $t $s)
   | .ARITH_ELIM_LEQ =>
     if !pf.getArguments[1]!.getSort.isInteger then return none
     let t : Q(Int) ← reconstructTerm pf.getArguments[1]!
@@ -350,43 +349,84 @@ where
   | .ARITH_SUM_UB =>
     if !pf.getResult[0]!.getSort.isInteger then return none
     reconstructSumUB pf
+  | .INT_TIGHT_UB =>
+    if !pf.getResult[0]!.getSort.isInteger then return none
+    let i : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[0]!
+    let c : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[1]!
+    let h : Q($i < $c) ← reconstructProof pf.getChildren[0]!
+    addThm q($i ≤ $c - 1) q(@Int.int_tight_ub $c $i $h)
+  | .INT_TIGHT_LB =>
+    if !pf.getResult[0]!.getSort.isInteger then return none
+    let i : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[0]!
+    let c : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[1]!
+    let h : Q($i > $c) ← reconstructProof pf.getChildren[0]!
+    addThm q($i ≥ $c + 1) q(@Int.int_tight_lb $c $i $h)
   | .ARITH_TRICHOTOMY =>
     if !pf.getResult[0]!.getSort.isInteger then return none
     let x : Q(Int) ← reconstructTerm pf.getResult[0]!
     let c : Q(Int) ← reconstructTerm pf.getResult[1]!
     let k₁ := pf.getChildren[0]!.getResult.getKind
     let k₂ := pf.getChildren[1]!.getResult.getKind
-    if k₁ == .GEQ && k₂ == .NOT then
-      let h₁ : Q($x ≥ $c) ← reconstructProof pf.getChildren[0]!
+    if k₁ == .LEQ && k₂ == .NOT then
+      let h₁ : Q($x ≤ $c) ← reconstructProof pf.getChildren[0]!
       let h₂ : Q($x ≠ $c) ← reconstructProof pf.getChildren[1]!
-      addThm q($x > $c) q(Int.trichotomy₁ $h₁ $h₂)
+      addThm q($x < $c) q(Int.trichotomy₁ $h₁ $h₂)
+    else if k₁ == .LEQ && k₂ == .GEQ then
+      let h₁ : Q($x ≤ $c) ← reconstructProof pf.getChildren[0]!
+      let h₂ : Q($x ≥ $c) ← reconstructProof pf.getChildren[1]!
+      addThm q($x = $c) q(Int.trichotomy₂ $h₁ $h₂)
+    else if k₁ == .NOT && k₂ == .LEQ then
+      let h₁ : Q($x ≠ $c) ← reconstructProof pf.getChildren[0]!
+      let h₂ : Q($x ≤ $c) ← reconstructProof pf.getChildren[1]!
+      addThm q($x < $c) q(Int.trichotomy₃ $h₁ $h₂)
     else if k₁ == .NOT && k₂ == .GEQ then
       let h₁ : Q($x ≠ $c) ← reconstructProof pf.getChildren[0]!
       let h₂ : Q($x ≥ $c) ← reconstructProof pf.getChildren[1]!
-      addThm q($x > $c) q(Int.trichotomy₂ $h₁ $h₂)
+      addThm q($x > $c) q(Int.trichotomy₄ $h₁ $h₂)
     else if k₁ == .GEQ && k₂ == .LEQ then
       let h₁ : Q($x ≥ $c) ← reconstructProof pf.getChildren[0]!
       let h₂ : Q($x ≤ $c) ← reconstructProof pf.getChildren[1]!
-      addThm q($x = $c) q(Int.trichotomy₃ $h₁ $h₂)
-    else if k₁ == .LEQ && k₂ == .GEQ then
-      let h₁ : Q($x ≤ $c) ← reconstructProof pf.getChildren[0]!
-      let h₂ : Q($x ≥ $c) ← reconstructProof pf.getChildren[1]!
-      addThm q($x = $c) q(Int.trichotomy₄ $h₁ $h₂)
-    else if k₁ == .NOT && k₂ == .LT then
-      let h₁ : Q($x ≠ $c) ← reconstructProof pf.getChildren[0]!
-      let h₂ : Q($x ≤ $c) ← reconstructProof pf.getChildren[1]!
-      addThm q($x < $c) q(Int.trichotomy₅ $h₁ $h₂)
-    else if k₁ == .LT && k₂ == .NOT then
-      let h₁ : Q($x ≤ $c) ← reconstructProof pf.getChildren[0]!
+      addThm q($x = $c) q(Int.trichotomy₅ $h₁ $h₂)
+    else if k₁ == .GEQ && k₂ == .NOT then
+      let h₁ : Q($x ≥ $c) ← reconstructProof pf.getChildren[0]!
       let h₂ : Q($x ≠ $c) ← reconstructProof pf.getChildren[1]!
-      addThm q($x < $c) q(Int.trichotomy₆ $h₁ $h₂)
+      addThm q($x > $c) q(Int.trichotomy₆ $h₁ $h₂)
     else
       return none
   | .ARITH_POLY_NORM =>
-    if !pf.getResult[0]!.getSort.isInteger then return none
-    let a : Q(Int) ← reconstructTerm pf.getResult[0]!
-    let b : Q(Int) ← reconstructTerm pf.getResult[1]!
-    addTac q($a = $b) Int.polyNorm
+    if pf.getResult[0]!.getSort.getKind == .BOOLEAN_SORT then
+      if !pf.getResult[0]![0]!.getSort.isInteger then return none
+      let a₁ : Q(Int) ← reconstructTerm pf.getResult[0]![0]!
+      let a₂ : Q(Int) ← reconstructTerm pf.getResult[0]![1]!
+      let b₁ : Q(Int) ← reconstructTerm pf.getResult[1]![0]!
+      let b₂ : Q(Int) ← reconstructTerm pf.getResult[1]![1]!
+      let (l, es) ← (toPolyNormExpr q($a₁ - $a₂)).run #[]
+      let (r, _) ← (toPolyNormExpr q($b₁ - $b₂)).run es
+      let c₁ : Q(Int) :=
+        if h : 0 < r.toPolynomial.length then let n : Nat := r.toPolynomial[0].coeff.natAbs; q(OfNat.ofNat $n) else q(1)
+      let c₂ : Q(Int) :=
+        if h : 0 < l.toPolynomial.length then let n : Nat := l.toPolynomial[0].coeff.natAbs; q(OfNat.ofNat $n) else q(1)
+      let hc₁ : Q($c₁ > 0) := .app q(@of_decide_eq_true ($c₁ > 0) _) q(Eq.refl true)
+      let hc₂ : Q($c₂ > 0) := .app q(@of_decide_eq_true ($c₂ > 0) _) q(Eq.refl true)
+      let h : Q($c₁ * ($a₁ - $a₂) = $c₂ * ($b₁ - $b₂)) ← Meta.mkFreshExprMVar q($c₁ * ($a₁ - $a₂) = $c₂ * ($b₁ - $b₂))
+      Int.polyNorm h.mvarId!
+      match pf.getResult[0]!.getKind with
+      | .LT =>
+        addThm q(($a₁ < $a₂) = ($b₁ < $b₂)) q(Int.lt_of_sub_eq $hc₁ $hc₂ $h)
+      | .LEQ =>
+        addThm q(($a₁ ≤ $a₂) = ($b₁ ≤ $b₂)) q(Int.le_of_sub_eq $hc₁ $hc₂ $h)
+      | .EQUAL =>
+        addThm q(($a₁ = $a₂) = ($b₁ = $b₂)) q(Int.eq_of_sub_eq $hc₁ $hc₂ $h)
+      | .GEQ =>
+        addThm q(($a₁ ≥ $a₂) = ($b₁ ≥ $b₂)) q(Int.ge_of_sub_eq $hc₁ $hc₂ $h)
+      | .GT =>
+        addThm q(($a₁ > $a₂) = ($b₁ > $b₂)) q(Int.gt_of_sub_eq $hc₁ $hc₂ $h)
+      | _   => return none
+    else
+      if !pf.getResult[0]!.getSort.isInteger then return none
+      let a : Q(Int) ← reconstructTerm pf.getResult[0]!
+      let b : Q(Int) ← reconstructTerm pf.getResult[1]!
+      addTac q($a = $b) Int.polyNorm
   | .ARITH_MULT_SIGN =>
     if !pf.getResult[1]![0]!.getSort.isInteger then return none
     reconstructMulSign pf

diff --git a/Smt/Reconstruct/Int/Lemmas.lean b/Smt/Reconstruct/Int/Lemmas.lean
@@ -31,13 +31,13 @@ namespace Smt.Reconstruct.Int
 variable {a b c d : Int}
 
 theorem sum_ub₁ (h₁ : a < b) (h₂ : c < d) : a + c < b + d := by
-  have r₁: a + c < a + d := Int.add_lt_add_left h₂ a
-  have r₂: a + d < b + d := Int.add_lt_add_right h₁ d
+  have r₁ : a + c < a + d := Int.add_lt_add_left h₂ a
+  have r₂ : a + d < b + d := Int.add_lt_add_right h₁ d
   exact Int.lt_trans r₁ r₂
 
 theorem sum_ub₂ (h₁ : a < b) (h₂ : c ≤ d) : a + c < b + d := by
-  have r₁: a + c ≤ a + d := Int.add_le_add_left h₂ a
-  have r₂: a + d < b + d := Int.add_lt_add_right h₁ d
+  have r₁ : a + c ≤ a + d := Int.add_le_add_left h₂ a
+  have r₂ : a + d < b + d := Int.add_lt_add_right h₁ d
   exact Int.lt_of_le_of_lt r₁ r₂
 
 theorem sum_ub₃ (h₁ : a < b) (h₂ : c = d) : a + c < b + d := by
@@ -70,29 +70,35 @@ theorem sum_ub₉ (h₁ : a = b) (h₂ : c = d) : a + c ≤ b + d := by
   rewrite [h₁, h₂]
   exact Int.le_refl (b + d)
 
-theorem trichotomy₁ (h₁ : a ≥ b) (h₂ : a ≠ b) : a > b := by
-  have tr := Int.lt_trichotomy a b
-  exact Or.resolve_left (Or.resolve_left tr (Int.not_lt.mpr h₁)) h₂
+theorem int_tight_ub {i : Int} (h : i < c) : i ≤ c - 1 :=
+  Int.le_sub_one_of_lt h
 
-theorem trichotomy₂ (h₁ : a ≠ b) (h₂ : a ≥ b) : a > b := by
-  have tr := Int.lt_trichotomy a b
-  exact Or.resolve_left (Or.resolve_left tr (Int.not_lt.mpr h₂)) h₁
+theorem int_tight_lb {i : Int} (h : i > c) : i ≥ c + 1 :=
+  h
 
-theorem trichotomy₃ (h₁ : a ≥ b) (h₂ : a ≤ b) : a = b := by
+theorem trichotomy₁ (h₁ : a ≤ b) (h₂ : a ≠ b) : a < b := by
   have tr := Int.lt_trichotomy a b
-  exact Or.resolve_right (Or.resolve_left tr (Int.not_lt.mpr h₁)) (Int.not_lt.mpr h₂)
+  exact Or.resolve_right (Or.resolve_right (or_assoc.mpr tr) (Int.not_lt.mpr h₁)) h₂
 
-theorem trichotomy₄ (h₁ : a ≤ b) (h₂ : a ≥ b) : a = b := by
+theorem trichotomy₂ (h₁ : a ≤ b) (h₂ : a ≥ b) : a = b := by
   have tr := Int.lt_trichotomy a b
   exact Or.resolve_right (Or.resolve_left tr (Int.not_lt.mpr h₂)) (Int.not_lt.mpr h₁)
 
-theorem trichotomy₅ (h₁ : a ≠ b) (h₂ : a ≤ b) : a < b := by
+theorem trichotomy₃ (h₁ : a ≠ b) (h₂ : a ≤ b) : a < b := by
   have tr := Int.lt_trichotomy a b
   exact Or.resolve_right (Or.resolve_right (or_assoc.mpr tr) (Int.not_lt.mpr h₂)) h₁
 
-theorem trichotomy₆ (h₁ : a ≤ b) (h₂ : a ≠ b) : a < b := by
+theorem trichotomy₄ (h₁ : a ≠ b) (h₂ : a ≥ b) : a > b := by
   have tr := Int.lt_trichotomy a b
-  exact Or.resolve_right (Or.resolve_right (or_assoc.mpr tr) (Int.not_lt.mpr h₁)) h₂
+  exact Or.resolve_left (Or.resolve_left tr (Int.not_lt.mpr h₂)) h₁
+
+theorem trichotomy₅ (h₁ : a ≥ b) (h₂ : a ≤ b) : a = b := by
+  have tr := Int.lt_trichotomy a b
+  exact Or.resolve_right (Or.resolve_left tr (Int.not_lt.mpr h₁)) (Int.not_lt.mpr h₂)
+
+theorem trichotomy₆ (h₁ : a ≥ b) (h₂ : a ≠ b) : a > b := by
+  have tr := Int.lt_trichotomy a b
+  exact Or.resolve_left (Or.resolve_left tr (Int.not_lt.mpr h₁)) h₂
 
 theorem lt_eq_sub_lt_zero : (a < b) = (a - b < 0) := by
   apply propext

diff --git a/Smt/Reconstruct/Int/Polynorm.lean b/Smt/Reconstruct/Int/Polynorm.lean
@@ -191,20 +191,29 @@ def getIndex (e : Q(Int)) : PolyM Nat := do
     set (es.push e)
     return size
 
-partial def toArithExpr (e : Q(Int)) : PolyM Q(PolyNorm.Expr) := do
+partial def toPolyNormExpr (e : Q(Int)) : PolyM PolyNorm.Expr := do
+  match e with
+  | ~q(OfNat.ofNat $x) => pure (.val x.rawNatLit?.get!)
+  | ~q(-$x) => pure (.neg (← toPolyNormExpr x))
+  | ~q($x + $y) => pure (.add (← toPolyNormExpr x) (← toPolyNormExpr y))
+  | ~q($x - $y) => pure (.sub (← toPolyNormExpr x) (← toPolyNormExpr y))
+  | ~q($x * $y) => pure (.mul (← toPolyNormExpr x) (← toPolyNormExpr y))
+  | e => let v : Nat ← getIndex e; pure (.var v)
+
+partial def toQPolyNormExpr (e : Q(Int)) : PolyM Q(PolyNorm.Expr) := do
   match e with
   | ~q(OfNat.ofNat $x) => pure q(.val (@OfNat.ofNat Int $x _))
-  | ~q(-$x) => pure q(.neg $(← toArithExpr x))
-  | ~q($x + $y) => pure q(.add $(← toArithExpr x) $(← toArithExpr y))
-  | ~q($x - $y) => pure q(.sub $(← toArithExpr x) $(← toArithExpr y))
-  | ~q($x * $y) => pure q(.mul $(← toArithExpr x) $(← toArithExpr y))
+  | ~q(-$x) => pure q(.neg $(← toQPolyNormExpr x))
+  | ~q($x + $y) => pure q(.add $(← toQPolyNormExpr x) $(← toQPolyNormExpr y))
+  | ~q($x - $y) => pure q(.sub $(← toQPolyNormExpr x) $(← toQPolyNormExpr y))
+  | ~q($x * $y) => pure q(.mul $(← toQPolyNormExpr x) $(← toQPolyNormExpr y))
   | e => let v : Nat ← getIndex e; pure q(.var $v)
 
 def polyNorm (mv : MVarId) : MetaM Unit := do
   let some (_, l, r) := (← mv.getType).eq?
     | throwError "[poly_norm] expected an equality, got {← mv.getType}"
-  let (l, es) ← (toArithExpr l).run #[]
-  let (r, es) ← (toArithExpr r).run es
+  let (l, es) ← (toQPolyNormExpr l).run #[]
+  let (r, es) ← (toQPolyNormExpr r).run es
   let is : Q(Array Int) := es.foldl (fun acc e => q(«$acc».push $e)) q(#[])
   let ctx : Q(PolyNorm.Context) := q(fun v => if h : v < «$is».size then $is[v] else 0)
   let h : Q(«$l».toPolynomial = «$r».toPolynomial) := .app q(@Eq.refl.{1} PolyNorm.Polynomial) q(«$l».toPolynomial)