Loge: SMT-LIB smoke test

root = Path.expand("..", __DIR__)

Mix.install([
  {:loge, path: Path.join(root, "loge"), override: true},
  {:loge_smtlib, path: Path.join(root, "loge_smtlib")},
  {:kino_loge, path: Path.join(root, "kino_loge")}
])

Solving

Expected: Satisfiable, a model with x and y summing to 10.

Loge.run!(
  Loge.Smtlib.Engines.Z3,
  "(set-logic QF_LIA)\n(declare-const x Int)\n(declare-const y Int)\n(assert (> x 2))\n(assert (= (+ x y) 10))\n(check-sat)\n(get-model)\n",
  time_limit: 10
)

The same script with cvc5. Expected: Satisfiable, possibly another model.

Loge.run!(
  Loge.Smtlib.Engines.Cvc5,
  "(set-logic QF_LIA)\n(declare-const x Int)\n(declare-const y Int)\n(assert (> x 2))\n(assert (= (+ x y) 10))\n(check-sat)\n(get-model)\n",
  time_limit: 10
)

Several check-sat commands give a table of results and no single verdict. Expected: sat, unsat, sat.

Loge.run!(
  Loge.Smtlib.Engines.Z3,
  "(declare-const p Bool)\n(check-sat)\n(push 1)\n(assert (and p (not p)))\n(check-sat)\n(pop 1)\n(check-sat)\n",
  time_limit: 10
)

Expected: Timeout after two seconds.

Loge.run!(
  Loge.Smtlib.Engines.Z3,
  "(set-logic NIA)\n(declare-const x Int)\n(declare-const y Int)\n(declare-const z Int)\n(assert (and (> x 0) (> y 0) (> z 0)))\n(assert (= (+ (* x x x) (* y y y)) (* z z z)))\n(check-sat)\n",
  time_limit: 2
)

Linting

Expected: under the editor, declare-const lacks its sort and simplify is not an SMT-LIB 2.6 command (warning); evaluating raises Loge.Error.

Loge.run!(Loge.Smtlib.Engines.Z3, "(declare-const x)\n(simplify (+ 1 2))\n(check-sat)\n",
  time_limit: 10
)

A solver error appears in the Result tab. Expected: unknown constant y on line 2.

Loge.run!(Loge.Smtlib.Engines.Z3, "(declare-const x Int)\n(assert (> y 1))\n(check-sat)\n",
  time_limit: 10
)