SMT.Examples

module SMT.Examples where

open import Agda.Builtin.String using (String)

open import Cubical.Foundations.Prelude
open import Cubical.Data.Bool.Base using (true; false)
open import Cubical.Data.Int.Base using (ℤ; negsuc; pos)
open import Cubical.Data.List.Base using ([]; _∷_)
open import Cubical.Data.Unit.Base using (tt)
open import Cubical.Relation.Nullary.Base using (¬_)

open import SMT.Core
open import SMT.Semantics

zeroInt : ℤ
zeroInt = pos 0

oneInt : ℤ
oneInt = pos 1

twoInt : ℤ
twoInt = pos 2

minusOne : ℤ
minusOne = negsuc 0

minusTwo : ℤ
minusTwo = negsuc 1

Γ₁ : Ctx
Γ₁ = decl "x" sInt ∷ []

x : Expr Γ₁ sInt
x = var vz

claim₁ : Expr Γ₁ sBool
claim₁ = iLe (int (pos 0)) (iAdd x (int oneInt))

problem₁ : Problem Γ₁
problem₁ = problem [] claim₁

statement₁ : Type₀
statement₁ = Statement problem₁

counterexample₁ : Counterexample problem₁
counterexample₁ = counterexample (minusTwo , tt) all[] refl

not-statement₁ : ¬ Statement problem₁
not-statement₁ = refute counterexample₁

smtlib₁ : String
smtlib₁ = counterexampleQuerySMT problem₁

Γ₂ : Ctx
Γ₂ = decl "b" sBool ∷ []

b₂ : Expr Γ₂ sBool
b₂ = var vz

problem₂ : Problem Γ₂
problem₂ = problem (b₂ ∷ []) (bNot b₂)

counterexample₂ : Counterexample problem₂
counterexample₂ =
  counterexample
    (true , tt)
    (refl all∷ all[])
    refl

semantic-counterexample₂ : SemanticCounterexample problem₂
semantic-counterexample₂ =
  semanticCounterexample
    (true , tt)
    (tt holds∷ allHolds[])
    tt

not-statement₂ : ¬ Statement problem₂
not-statement₂ = refute counterexample₂

not-statement₂-semantic : ¬ Statement problem₂
not-statement₂-semantic = refuteSemantic semantic-counterexample₂

smtlib₂ : String
smtlib₂ = counterexampleQuerySMT problem₂

Γ₃ : Ctx
Γ₃ = decl "x" sInt ∷ decl "y" sInt ∷ []

x₃ : Expr Γ₃ sInt
x₃ = var vz

y₃ : Expr Γ₃ sInt
y₃ = var (vs vz)

problem₃ : Problem Γ₃
problem₃ = problem (iLe x₃ y₃ ∷ []) (iEq x₃ y₃)

counterexample₃ : Counterexample problem₃
counterexample₃ =
  counterexample
    (zeroInt , (oneInt , tt))
    (refl all∷ all[])
    refl

not-statement₃ : ¬ Statement problem₃
not-statement₃ = refute counterexample₃

smtlib₃ : String
smtlib₃ = counterexampleQuerySMT problem₃

Γ₄ : Ctx
Γ₄ = decl "x" sInt ∷ []

x₄ : Expr Γ₄ sInt
x₄ = var vz

linear₄ : Expr Γ₄ sInt
linear₄ = iAdd (iScale twoInt x₄) (int oneInt)

problem₄ : Problem Γ₄
problem₄ = problem [] (iLe linear₄ (int zeroInt))

counterexample₄ : Counterexample problem₄
counterexample₄ =
  counterexample
    (zeroInt , tt)
    all[]
    refl

not-statement₄ : ¬ Statement problem₄
not-statement₄ = refute counterexample₄

smtlib₄ : String
smtlib₄ = counterexampleQuerySMT problem₄

Γ₅ : Ctx
Γ₅ = decl "b" sBool ∷ decl "x" sInt ∷ []

b₅ : Expr Γ₅ sBool
b₅ = var vz

x₅ : Expr Γ₅ sInt
x₅ = var (vs vz)

problem₅ : Problem Γ₅
problem₅ = problem [] (iLe (ite b₅ x₅ (int zeroInt)) x₅)

counterexample₅ : Counterexample problem₅
counterexample₅ =
  counterexample
    (false , (minusOne , tt))
    all[]
    refl

not-statement₅ : ¬ Statement problem₅
not-statement₅ = refute counterexample₅

smtlib₅ : String
smtlib₅ = counterexampleQuerySMT problem₅

problem₆ : Problem Γ₂
problem₆ = problem (bAnd b₂ (bool true) ∷ []) b₂

semantic-statement₆ : SemanticStatement problem₆
semantic-statement₆ ρ (hand holds∷ allHolds[]) with and-sound {ρ = ρ} {p = b₂} {q = bool true} hand
... | hb , _ = hb

statement₆ : Statement problem₆
statement₆ = semantic→statement {p = problem₆} semantic-statement₆

smtlib₆ : String
smtlib₆ = counterexampleQuerySMT problem₆

problem₇ : Problem Γ₁
problem₇ = problem (iGe x (int zeroInt) ∷ []) (iGt x (int zeroInt))

problem₇-assumptions-satisfiable : SatisfiableProblem problem₇
problem₇-assumptions-satisfiable =
  (zeroInt , tt) , (tt holds∷ allHolds[])

counterexample₇ : Counterexample problem₇
counterexample₇ =
  counterexample
    (zeroInt , tt)
    (refl all∷ all[])
    refl

not-statement₇ : ¬ Statement problem₇
not-statement₇ = refute counterexample₇

smtlib₇ : String
smtlib₇ = counterexampleQuerySMT problem₇

problem₈ : Problem Γ₁
problem₈ = problem (iNe x (int zeroInt) ∷ []) (iLt x (int zeroInt))

counterexample₈ : Counterexample problem₈
counterexample₈ =
  counterexample
    (oneInt , tt)
    (refl all∷ all[])
    refl

not-statement₈ : ¬ Statement problem₈
not-statement₈ = refute counterexample₈

smtlib₈ : String
smtlib₈ = counterexampleQuerySMT problem₈

problem₉ : Problem Γ₂
problem₉ = problem [] (bNot (bXor b₂ b₂))

semantic-statement₉ : SemanticStatement problem₉
semantic-statement₉ ρ allHolds[] = xor-self-refuted {ρ = ρ} {p = b₂}

statement₉ : Statement problem₉
statement₉ = semantic→statement {p = problem₉} semantic-statement₉

no-counterexample₉ : NoCounterexample problem₉
no-counterexample₉ = semantic→noCounterexample {p = problem₉} semantic-statement₉

semantic-statement₉-again : SemanticStatement problem₉
semantic-statement₉-again = noCounterexample→semantic {p = problem₉} no-counterexample₉

smtlib₉ : String
smtlib₉ = counterexampleQuerySMT problem₉