SMT Interface
Table of contents
Analysis Commands
Maude-SE provides various analysis commands, including check, show model, smt-search, and show smt-path, using Maude’s meta-interpreter.
check
The check command determines the satisfiability of boolean formulas. For a given module M, a boolean formula f, and an (optional) SMT theory Th, it determines the satisfiability of f under the theory Th.
check in M : f using Th .
For example, consider a module EUF-EX.
fmod EUF-EX is
protecting INTEGER .
sort A .
op f : A-> A [special (id-hook SMT_Symbol (EUF))] .
op _xor_ : Integer Integer-> A [prec 30 special (id-hook SMT_Symbol (EUF))] .
op _===_ : A A-> Boolean [special (id-hook SMT_Symbol (===))] .
endfm
We can check the satisfiability using the command as follows:
MaudeSE> check in EUF-EX : I:Integer > 2 and I:Integer xor J:Integer > 3 and f(X:A) === X:A .
result: sat
show model
The show model command returns the satisfying assignment, if any, for the last check command. For example, we can get the assigment of the above check example as follows:
MaudeSE> show model .
assignment: I |--> 3; J |--> 2; X |--> A!val!0; _xor_ |--> [else-> 4]; f |--> [else-> A!val!0]
smt-search
This command performs symbolic reachability analysis, along with folding. Given an initial term t, a goal pattern u, and a goal condition c, the following command searches for n solutions that are reachable within m rewrite steps from t, match the goal pattern u, and satisfy the goal condition c under the SMT theory Th:
{fold} smt-search [n,m] in M : t =>* u such that c using Th .
The arguments {fold}, Th, n, and m are optional. If {fold} is given, the command ignores constrained terms that are subsumed by other constrained terms.
As an example, consider the following system module COFFEE-MACHINE that specifies the coffee machine parametric timed automaton (PTA).
mod COFFEE-MACHINE is
protecting REAL .
sorts State Location .
vars T X Y X' Y' P1 P2 P3 : Real .
vars L L' : Location .
var PHI : Boolean .
ops idle addsugar preparingcoffee cdone :-> Location .
op <_;_;_> <_;_;_> : Location Real Real Real Real Real-> State .
op [_;_;_] <_;_;_> : Location Real Real Real Real Real-> State .
sort Tuple{Location,Real,Real,Boolean} .
op {_,_,_,_} : Location Real Real Boolean-> Tuple{Location,Real,Real,Boolean} [ctor] .
crl [tick] : [ L ; X ; Y ] < P1 ; P2 ; P3 >
=> < L ; X + T ; Y + T > < P1 ; P2 ; P3 >
if PHI := tickCond(L, T, X, Y, P2, P3) /\ (T >= 0/1 and PHI) = true [nonexec] .
op tickCond : Location Real Real Real Real Real-> Boolean .
eq tickCond(idle, T, X, Y, P2, P3) = true .
eq tickCond(addsugar, T, X, Y, P2, P3) = Y + T <= P2 .
eq tickCond(preparingcoffee, T, X, Y, P2, P3) = Y + T <= P3 .
eq tickCond(cdone, T, X, Y, P2, P3) = X + T <= 10/1 .
crl [toAddsugar] : < L ; X ; Y > < P1 ; P2 ; P3 >
=> [ L' ; X' ; Y' ] < P1 ; P2 ; P3 >
if {L', X', Y', PHI} := nextAddSugar(L, X, Y, P1, P2) /\ PHI = true .
op nextAddSugar : Location Real Real Real Real-> Tuple{Location,Real,Real,Boolean} .
eq nextAddSugar(idle, X, Y, P1, P2) = {addsugar, 0/1, 0/1, 0/1 <= P2} .
eq nextAddSugar(addsugar, X, Y, P1, P2) = {addsugar, 0/1, Y, Y <= P2 and X >= P1} .
eq nextAddSugar(cdone, X, Y, P1, P2) = {addsugar, 0/1, 0/1, 0/1 <= P2} .
crl [toOther] : < L ; X ; Y > < P1 ; P2 ; P3 >
=> [ L' ; X' ; Y' ] < P1 ; P2 ; P3 >
if {L', X', Y', PHI} := nextOther(L, X, Y, P2, P3) /\ PHI = true .
op nextOther : Location Real Real Real Real-> Tuple{Location,Real,Real,Boolean} .
eq nextOther(addsugar, X, Y, P2, P3) = {preparingcoffee, X, Y, Y <= P3 and Y === P2} .
eq nextOther(preparingcoffee, X, Y, P2, P3) = {cdone, 0/1, Y, 0/1 <= 10/1 and Y === P3} .
eq nextOther(cdone, X, Y, P2, P3) = {idle, X, Y, X === 10/1} .
endm
The following command finds the first solution of the PTA coffee machine that goes to cdone with all the clocks and parameters are greater than or equal to 0.
MaudeSE> {fold} smt-search [1, 10000] :
< idle ; X:Real ; Y:Real > < P1:Real ; P2:Real ; P3:Real > =>*
< cdone ; X’:Real ; Y’:Real > < P1:Real ; P2:Real ; P3:Real >
such that X:Real === Y:Real and X:Real >= 0/1 and Y:Real >= 0/1 and
P1:Real >= 0/1 and P2:Real >= 0/1 and P3:Real >= 0/1 .
Solution 1 (state 12)
Symbolic term: < cdone ; %ubVar$8 ; %ubVar$9 > < PAR1 ; PAR2 ; PAR3 >
Constraint: T1 === T2 and T1 >= 0/1 and T2 >= 0/1 ...
Substitution: %ubVar$1 <-- 1/2 ; ... ; %ubVar$9 <-- 1/2 ; ...
Concrete term: < cdone ; 0/1 ; 1/2 > < 1/2 ; 1/2 ; 1/2 >
show smt-path
This command returns a symbolic/concrete path of the last smt-search result. It takes two arguments: a path type (either symbolic or concrete) and a state number. A symbolic path is given by a sequence of contracted terms and rewrite rules. The corresponding concrete path is an instance of the symbolic path with a satisfying assignment.
For example, the following commands show the symbolic and concrete paths for Solution 3 of the above smt-search command.
MaudeSE> show smt-path symbolic 3 .
{ < idle ; T1 ; T2 > < PAR1 ; PAR2 ; PAR3 > || T1 === T2 ... } ====='[ toAddsugar ']=====>
{ [addsugar ; 0/1 ; 0/1] < PAR1 ; PAR2 ; PAR3 > || T1 === T2 ... } ...
MaudeSE> show smt-path concrete 3 .
< idle ; 10/1 ; 10/1 > < 0/1 ; 0/1 ; 0/1 > ===[ toAddsugar ]===>
[addsugar ; 0/1 ; 0/1] < 0/1 ; 0/1 ; 0/1 > ...
Metalevel Functions
Maude-SE provides three meta-level functions: metaSmtCheck, metaSmtSearch2, and metaSmtSearch2Path.
metaSmtCheck
Given a module M, a boolean formula f, and an SMT theory Th, the function metaSmtCheck(M',f',Th,b) returns the solution of the following command:
check in M : f using Th .
The argument b is a Boolean flag for generating satisfying assignment. M' and f' are the metarepresentations of M and f, respectively, and Th is an optional argument.
metaSmtSearch2
Analogously, given an initial state t, a goal pattern u, and a goal condition c, the function metaSmtSearch2(M',t',u',c',*,m,k,Th,b) returns the (k + 1)-th solution of the smt-search command:
{fold} smt-search [n,m] in M : t =>* u such that c using Th .
The arugment b is a Boolean flag for folding, t', u', and c' denote the metarepresentations of t, u, and c, respectively, and k is less than n.
metaSmtSearch2Path
If a solution exists for metaSmtSearch2, the function metaSmtSearch2Path(M',t',u',c',*,m,k,Th,b) returns a symbolic path and its concrete witness for the solution of the same command.