[<<][rtl][>>][..]
Sun Sep 16 10:11:53 EDT 2018

SAT/SMT: stick to z3 for now

( Getting more into how other people make monad wrappers.  This one
sure looks ugly, but is straightforward, to the point. )


Notes:

mkFreshIntVar: create a variable
mkInteger:     create an integer constant

assert: add assertion to Z3 monad

connectives:
  mkLe
  mkAnd
  mkIte
  mkEq
  mkSub
  mkUnaryMinux

withModel: provides context such that evalInt works
evalInt:   evaluate variable






[Reply][About]
[<<][rtl][>>][..]