module SMT.Tests.AdvancedRendering where

open import Cubical.Foundations.Prelude using (_≡_; refl)

open import SMT.Core
open import SMT.Examples.Advanced

valid-subtract-back-renders :
  counterexampleCheckSMT valid-subtract-back ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const x Int)\n" ++s
  "(declare-const y Int)\n" ++s
  "(assert (not (= (- (+ x y) y) x)))\n" ++s
  "(check-sat)\n"
valid-subtract-back-renders = refl

valid-negated-subtraction-renders :
  counterexampleCheckSMT valid-negated-subtraction ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const x Int)\n" ++s
  "(declare-const y Int)\n" ++s
  "(assert (not (= (- (- x y)) (- y x))))\n" ++s
  "(check-sat)\n"
valid-negated-subtraction-renders = refl

valid-absolute-value-nonnegative-renders :
  counterexampleCheckSMT valid-absolute-value-nonnegative ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const x Int)\n" ++s
  "(assert (not (>= (ite (>= x 0) x (- x)) 0)))\n" ++s
  "(check-sat)\n"
valid-absolute-value-nonnegative-renders = refl

valid-conditional-upper-bound-renders :
  counterexampleCheckSMT valid-conditional-upper-bound ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const b Bool)\n" ++s
  "(declare-const x Int)\n" ++s
  "(declare-const y Int)\n" ++s
  "(declare-const z Int)\n" ++s
  "(assert (<= x z))\n" ++s
  "(assert (<= y z))\n" ++s
  "(assert (not (<= (ite b x y) z)))\n" ++s
  "(check-sat)\n"
valid-conditional-upper-bound-renders = refl

valid-branch-refinement-renders :
  counterexampleCheckSMT valid-branch-refinement ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const b Bool)\n" ++s
  "(declare-const x Int)\n" ++s
  "(declare-const y Int)\n" ++s
  "(assert (=> b (>= x 2)))\n" ++s
  "(assert (=> (not b) (>= y 3)))\n" ++s
  "(assert (not (>= (ite b (- x 2) (- y 3)) 0)))\n" ++s
  "(check-sat)\n"
valid-branch-refinement-renders = refl

valid-additive-upper-bound-renders :
  counterexampleCheckSMT valid-additive-upper-bound ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const x Int)\n" ++s
  "(declare-const y Int)\n" ++s
  "(declare-const z Int)\n" ++s
  "(assert (<= x y))\n" ++s
  "(assert (<= z 0))\n" ++s
  "(assert (not (<= (+ x z) y)))\n" ++s
  "(check-sat)\n"
valid-additive-upper-bound-renders = refl

valid-boolean-resolution-renders :
  counterexampleCheckSMT valid-boolean-resolution ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const p Bool)\n" ++s
  "(declare-const q Bool)\n" ++s
  "(assert (or p q))\n" ++s
  "(assert (not p))\n" ++s
  "(assert (not q))\n" ++s
  "(check-sat)\n"
valid-boolean-resolution-renders = refl

valid-implication-chain-renders :
  counterexampleCheckSMT valid-implication-chain ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const p Bool)\n" ++s
  "(declare-const q Bool)\n" ++s
  "(declare-const r Bool)\n" ++s
  "(assert (=> p q))\n" ++s
  "(assert (=> q r))\n" ++s
  "(assert p)\n" ++s
  "(assert (not r))\n" ++s
  "(check-sat)\n"
valid-implication-chain-renders = refl

invalid-strict-from-nonstrict-renders :
  counterexampleCheckSMT invalid-strict-from-nonstrict ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const x Int)\n" ++s
  "(declare-const y Int)\n" ++s
  "(assert (<= x y))\n" ++s
  "(assert (not (< x y)))\n" ++s
  "(check-sat)\n"
invalid-strict-from-nonstrict-renders = refl

invalid-drop-branch-guard-renders :
  counterexampleCheckSMT invalid-drop-branch-guard ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const b Bool)\n" ++s
  "(declare-const x Int)\n" ++s
  "(declare-const y Int)\n" ++s
  "(assert (=> b (>= x 0)))\n" ++s
  "(assert (not (>= (ite b x y) 0)))\n" ++s
  "(check-sat)\n"
invalid-drop-branch-guard-renders = refl

invalid-additive-cancel-renders :
  counterexampleCheckSMT invalid-additive-cancel ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const x Int)\n" ++s
  "(declare-const y Int)\n" ++s
  "(declare-const z Int)\n" ++s
  "(assert (<= x (+ y z)))\n" ++s
  "(assert (not (<= x y)))\n" ++s
  "(check-sat)\n"
invalid-additive-cancel-renders = refl

invalid-positive-sum-left-renders :
  counterexampleCheckSMT invalid-positive-sum-left ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const x Int)\n" ++s
  "(declare-const y Int)\n" ++s
  "(assert (> (+ x y) 0))\n" ++s
  "(assert (> y 0))\n" ++s
  "(assert (not (> x 0)))\n" ++s
  "(check-sat)\n"
invalid-positive-sum-left-renders = refl

invalid-branch-equality-renders :
  counterexampleCheckSMT invalid-branch-equality ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const b Bool)\n" ++s
  "(declare-const x Int)\n" ++s
  "(declare-const y Int)\n" ++s
  "(assert (not (= (ite b x y) x)))\n" ++s
  "(check-sat)\n"
invalid-branch-equality-renders = refl