SI242 SMT-solver tool (interface to Z3)

Enter a formula with the same syntax as the propositional logic tool, except that in addition to propositional variables, you have predicates, functions, theory constants, quantified variables and infix equality (=) and disequality (!=) operators.

Warning! There is a bug in this system because of how Z3 is packaged. Certain kinds of formula trigger it, but they should not arise in the limited use we will make of the tool in this course.

Important: The current version of this tool assumes the theory of linear integer arithmetic, which means you can add but not multiply. Here's an example input:

lt(v,x) & E:y[lt(x,y) & lt(y,u)] & 
(s => lt(0,u) & lt(0,v) & lt(0,x)) &
(~s => lt(u,0) & lt(v,0) & lt(x,0)) &
sum = plus(plus(u,v),x) & sum = 42