/// should be able to do these: https://smt-lib.org/examples.shtml
//
//
// Examples:
// ; Basic Boolean example
// (set-option :print-success false)
// (set-logic QF_UF)
// (declare-const p Bool)
// (assert (and p (not p)))
// (check-sat) ; returns 'unsat'
// (exit)
// This should be in egglog:
// (let p (smt-bool-const "p"))
// (check (is-unsat "QF_UF" (and p (not p))))
// ; Integer arithmetic
// (set-logic QF_LIA)
// (declare-const x Int)
// (declare-const y Int)
// (assert (= (- x y) (+ x (- y) 1)))
// (check-sat)
// ; unsat
// (exit)
// This should be in egglog:
// (let x (smt-int-const "x"))
// (let y (smt-int-const "y"))
// (check (is-unsat "QF_LIA" (= (- x y) (+ x (- y) (smt-int 1)))))
// ; Getting values or models
// (set-option :print-success false)
// (set-option :produce-models true)
// (set-logic QF_LIA)
// (declare-const x Int)
// (declare-const y Int)
// (assert (= (+ x (* 2 y)) 20))
// (assert (= (- x y) 2))
// (check-sat)
// ; sat
// (get-value (x y))
// ; ((x 8) (y 6))
// (get-model)
// ; ((define-fun x () Int 8)
// ; (define-fun y () Int 6)
// ; )
// (exit)
// This should be in egglog:
// (let x (smt-int-const "x"))
// (let y (smt-int-const "y"))
// (let model (smt-model "QF_LIA" (smt-= (+ x (* (smt-int 2) y)) (smt-int 20))) (smt-= (- x y) (smt-int 2)))))
// (check (= (get-value model x) (smt-int 8)))
// (check (= (get-value model y) (smt-int 6)))
