Examples
Table of contents
Examples
We provide two example files, smt-check-ex.maude and smt-search-ex.maude, to show the usage of the two functions.
smt-check-ex.maude
In this file, we show the usage of metaSmtCheck using various theories and formulas including interpreted and uninterpreted symbols. The file contains four functional module: SIMPLE, EUF, EUF-ARRAY, EUF-XOR. The SIMPLE module simply imports INTEGER module. The EUF module defines a new sort A and an uninterpreted symbol f. The EUF-ARRAY module connects interpreted symbols from the Array theory to Maude operators. The EUF-XOR is another example for uninterpreted symbol.
fmod SIMPLE is
pr INTEGER .
pr META-SMT-CHECK .
endfm
fmod EUF is
pr BOOLEAN .
sort A .
op _===_ : A A -> Boolean .
op f : A -> A [ctor metadata "smt euf"] .
endfm
fmod ARRAY is
pr REAL-INTEGER .
sort Array{Integer,Integer} .
op _===_ : Array{Integer,Integer} Array{Integer,Integer} -> Boolean .
op select : Array{Integer,Integer} Integer -> Integer [metadata "smt array:select"] .
op _[_] : Array{Integer,Integer} Integer -> Integer [metadata "smt array:select"] .
op store : Array{Integer,Integer} Integer Integer -> Array{Integer,Integer} [metadata "smt array:store"] .
endfm
fmod EUF-XOR is
pr INTEGER .
op _xor_ : Integer Integer -> Integer [metadata "smt euf"] .
endfm
As the modules EUF and EUF-XOR show, we can declare uninterpreted symbols by declaring operators and annotating them as uninterpreted symbols using the metadata attribute. For example, the uninterpreted symbol f of EUF is annotated with metadata smt euf, meaning that the operator is an SMT symbol (smt) and an uninterpreted symbol (euf).
Another module ARRAY show how to connect interpreted symbol to Maude. We also use the metadata attribute. For example, we use the metadata smt array:select to denote the interpreted symbol select of the array theory. In addition, we can connect a single interpreted symbol to different Maude operators. For example, we connect the select to select and _[_] in the ARRAY module.
To use metaSmtCheck, we need to import META-SMT-CHECK module. Then, we can check the satisfiability of various formulas under EUF and Array theories as follows.
red metaSmtCheck(upModule('INTEGER, false), upTerm(X:Integer > 4), 'QF_LRA, true) .
red metaSmtCheck(upModule('REAL, false), upTerm(X:Real > 4/3), 'QF_LRA, true) .
red metaSmtCheck(upModule('BOOLEAN, false), upTerm(B:Boolean), 'QF_LRA, true) .
red metaSmtCheck(upModule('EUF, false), upTerm(f(f(X)) === X and f(X) === Y and not (X === Y)), 'QF_UF) .
red metaSmtCheck(upModule('ARRAY, false), upTerm(select(A1, X) === X and store(A1, X, Y) === A1), 'QF_AUFLIA) .
red metaSmtCheck(upModule('ARRAY, false), upTerm(A1[X] === X and store(A1, X, Y) === A1), 'QF_AUFLIA) .
red metaSmtCheck(upModule('EUF-XOR, false), upTerm(not(N === 0) and 0 <= N and 0 <= (N xor 255) and N < 256 and not (0 <= (N xor 255))), 'QF_UFLIA) .
red metaSmtCheck(upModule('EUF-XOR, false), upTerm(0 <= (N xor 255)), 'QF_UFLIA) .
red metaSmtCheck(upModule('EUF-XOR, false), upTerm(0 <= (N xor 255)), 'QF_UFLIA, true) . --- generating a satisfying assignment
The usage of metaSmtCheck is similar to metaCheck except that it takes an SMT logic and a boolean flag as its arguments, where the flag decides whether to generate a satisfying assignment for the satisfiable case.
op metaSmtCheck : Module Term Qid -> SmtCheckResult .
eq metaSmtCheck(M:Module, TERM:Term, LOGIC:Qid) = metaSmtCheck(M:Module, TERM:Term, LOGIC:Qid, false) .
op metaSmtCheck : Module Term Qid Bool -> SmtCheckResult
[special (id-hook SpecialHubSymbol (SmtCheckerSymbol)
op-hook unknownResultSymbol (unknown : ~> SmtCheckResult)
op-hook smtAssignmentResultSymbol ({_} : SatAssignmentSet ~> SmtCheckResult)
op-hook emptySatAssignmentSetSymbol (empty : ~> SatAssignmentSet)
op-hook concatSatAssignmentSetSymbol (_,_ : SatAssignmentSet SatAssignmentSet ~> SatAssignmentSet)
op-hook assnPairSymbol (_|->_ : Term Term ~> SatAssignment)
term-hook builtinTrueTerm ((true).Bool)
term-hook builtinFalseTerm ((false).Bool)
)] .
The check result is given as a term of sort SmtCheckResult, which can be one of unknown, true, false, or {_}. The symbol {_} consists of a set of assignments, where each assignment is denoted as a term _|->_.
sort SmtCheckResult .
subsort Bool < SmtCheckResult .
op unknown : -> SmtCheckResult [ctor] .
op {_} : SatAssignmentSet -> SmtCheckResult [ctor] .
sort SatAssignment .
op _|->_ : Term Term -> SatAssignment [ctor] .
sort SatAssignmentSet .
subsort SatAssignment < SatAssignmentSet .
op empty : -> SatAssignmentSet [ctor] .
op _,_ : SatAssignmentSet SatAssignmentSet -> SatAssignmentSet [ctor comm assoc id: empty] .
We can run the smt-check-ex.maude file with CVC5 using the following command:
~/maude-se-linux$ maude-se smt-check-ex.maude -s cvc5
The results are as follows.
==========================================
reduce in SIMPLE : metaSmtCheck(upModule('INTEGER, false), upTerm(X:Integer > (4).Integer), 'QF_LRA, true) .
rewrites: 1
result SmtCheckResult: {'X:Integer |-> '5.Integer}
==========================================
reduce in SIMPLE : metaSmtCheck(upModule('REAL, false), upTerm(X:Real > 4/3), 'QF_LRA, true) .
rewrites: 1
result SmtCheckResult: {'X:Real |-> '7/3.Real}
==========================================
reduce in SIMPLE : metaSmtCheck(upModule('BOOLEAN, false), upTerm(B:Boolean), 'QF_LRA, true) .
rewrites: 1
result SmtCheckResult: {'B:Boolean |-> 'true.Boolean}
==========================================
reduce in EUF-CHECK : metaSmtCheck(upModule('EUF, false), upTerm(f(f(X)) === X and f(X) === Y and not X === Y), 'QF_UF) .
rewrites: 4
result Bool: (true).Bool
==========================================
reduce in ARRAY-CHECK : metaSmtCheck(upModule('ARRAY, false), upTerm(select(A1, X) === X and store(A1, X, Y) === A1), 'QF_AUFLIA) .
rewrites: 4 in 1ms cpu (1ms real) (2619 rewrites/second)
result Bool: (true).Bool
==========================================
reduce in ARRAY-CHECK : metaSmtCheck(upModule('ARRAY, false), upTerm(A1[X] === X and store(A1, X, Y) === A1), 'QF_AUFLIA) .
rewrites: 4
result Bool: (true).Bool
==========================================
reduce in EUF-XOR-CHECK : metaSmtCheck(upModule('EUF-XOR, false), upTerm(not N === (0).Integer and (0).Integer <= N and (0).Integer <= (N xor (255).Integer) and N < (256).Integer and not (0).Integer <= (N xor (255).Integer)), 'QF_UFLIA) .
rewrites: 4
result Bool: (false).Bool
==========================================
reduce in EUF-XOR-CHECK : metaSmtCheck(upModule('EUF-XOR, false), upTerm((0).Integer <= (N xor (255).Integer)), 'QF_UFLIA) .
rewrites: 4
result Bool: (true).Bool
==========================================
reduce in EUF-XOR-CHECK : metaSmtCheck(upModule('EUF-XOR, false), upTerm((0).Integer <= (N xor (255).Integer)), 'QF_UFLIA, true) .
rewrites: 1
result SmtCheckResult: {('N:Integer |-> '1.Integer),{"_xor_" |-> "(lambda ((_arg_1 Int) (_arg_2 Int)) 0)"}}
==========================================
smt-search-ex.maude
This file provides examples of metaSmtSearch2 using gcd and robot examples.
mod GCD is
pr INTEGER .
sorts GcdResult .
op gcd : Integer Integer -> GcdResult [ctor] .
op return : Integer -> GcdResult [ctor] .
vars X Y : Integer .
crl [r1] : gcd(X, Y) => gcd(X - Y, Y) if X > Y = true [nonexec] .
crl [r2] : gcd(X, Y) => gcd(X, Y - X) if X < Y = true [nonexec] .
crl [r3] : gcd(X, Y) => return (X) if X === Y = true [nonexec] .
endm
omod ROBOT is
pr REAL .
class Robot | pos : Vector, vel : Vector, acc : Vector, time : Real .
sort Vector .
op [_,_] : Real Real -> Vector [ctor] .
endom
omod ROBOT-DYNAMICS is
pr ROBOT .
vars O : Oid .
vars CONST CONST' : Boolean .
vars PX VX AX PY VY AY PX' VX' AX' PY' VY' AY' T T' TAU : Real .
crl [move]:
< O : Robot | pos : [PX, PY], vel : [VX, VY],
acc : [AX, AY], time : T >
=> < O : Robot | pos : [PX', PY'], vel : [VX', VY'],
time : T + TAU >
if TAU >= 0/1 and VX' === VX + AX * TAU and VY' === VY + AY * TAU
and PX' === 1/2 * AX * TAU * TAU + VX * TAU + PX
and PY' === 1/2 * AY * TAU * TAU + VY * TAU + PY = true [nonexec] .
crl [accX]:
< O : Robot | acc : [AX, AY] >
=> < O : Robot | acc : [AX', AY] >
if AY === 0/1 = true [nonexec] .
crl [accY]:
< O : Robot | acc : [AX, AY] >
=> < O : Robot | acc : [AX, AY'] >
if AX === 0/1 = true [nonexec] .
op r : -> Oid [ctor] .
endom
To use metaSmtSearch2, we need to import META-SMT-SEARCH2 module. The following commands show how to perform rewriting modulo SMT.
--- gcd(10, I) =>* return(J) such that I < 9 and I > 0 = true .
red metaSmtSearch2(upModule('GCD, false), upTerm(gcd(10, I)), upTerm(return(J)),
upTerm(I < 9 and I > 0) = upTerm((true).Bool), '=>*, unbounded, 8, 'QF_LRA) .
red metaSmtSearch2(upModule('ROBOT-DYNAMICS, false),
upTerm(< r : Robot | pos : [IPX, IPY], vel : [IVX, IVY], acc : [IAX, IAY], time : CLK >),
upTerm(< r : Robot | pos : [NPX, NPY], ATTRSET >),
upTerm(NPX === 10/1 and NPY === 10/1 and IPX === 0/1 and IPY === 0/1
and IVX === 0/1 and IVY === 0/1 and IAX === 0/1
and IAY === 0/1 and CLK === 0/1) = upTerm((true).Bool), '=>*, unbounded, 1, 'QF_NRA) .
The first command searches for the 8-th solution term that matches return(J) and satisfies the consition I < 9 and I > 0, starting from an initial term gcd(10, I) without folding under the QF_LRA logic.
The second command searches for the first solution, with the QF_NRA logic, that matches the goal pattern < r : Robot | pos : [NPX, NPY], ATTRSET > and satisfies the consition NPX === 10/1 and NPY === 10/1, starting from an initial term, where all its attributes are zeros.
The metaSmtSearch2 is similar to metaSmtSearch except that it takes a logic and a folding flag as its arguments.
op metaSmtSearch2 : Module Term Term Condition Qid Bound Nat Qid Bool Bool -> SmtResult? .
eq metaSmtSearch2(M, T, T', COND, STEP, B, N, LOGIC, FOLD, MERGE)
= metaSmtSearchInternal(transform(M), makeConstTerm(T), makeConstTerm(T'), COND, STEP, B, N, LOGIC, FOLD, MERGE) .
op metaSmtSearch2 : Module Term Term Condition Qid Bound Nat Qid -> SmtResult? .
eq metaSmtSearch2(M, T, T', COND, STEP, B, N, LOGIC)
= metaSmtSearch2(M, T, T', COND, STEP, B, N, LOGIC, false, false) .
op metaSmtSearch2 : Module Term Term Condition Qid Bound Nat Qid Bool -> SmtResult? .
eq metaSmtSearch2(M, T, T', COND, STEP, B, N, LOGIC, FOLD)
= metaSmtSearch2(M, T, T', COND, STEP, B, N, LOGIC, FOLD, false) .
op metaSmtSearchInternal : Module Term Term Condition Qid Bound Nat Qid Bool Bool -> SmtResult?
[special (id-hook SpecialHubSymbol (SmtSearchSymbol)
op-hook failureSymbol (failure : ~> SmtResult?)
op-hook resultSymbol ({_,_,_,_} : Term Substitution Term Nat ~> SmtResult))].
We can run the smt-search-ex.maude file with Yices using the following command:
~/maude-se-linux$ maude-se smt-search-ex.maude -s yices
The search results are as follows.
==========================================
reduce metaSmtSearch2(upModule('GCD, false), upTerm(gcd((10).Integer, I)), upTerm(return(J)),
upTerm(I < (9).Integer and I > (0).Integer) = upTerm((true).Bool),
'=>*, unbounded, 8, 'QF_LRA) .
result SmtResult2: {'return['%%ubVar$9:Integer],
'%%ubVar$1:Integer <- '9.Integer ;
'%%ubVar$2:Integer <- '8.Integer ;
'%%ubVar$3:Integer <- '7.Integer ;
'%%ubVar$4:Integer <- '6.Integer ;
'%%ubVar$5:Integer <- '5.Integer ;
'%%ubVar$6:Integer <- '4.Integer ;
'%%ubVar$7:Integer <- '3.Integer ;
'%%ubVar$8:Integer <- '2.Integer ;
'%%ubVar$9:Integer <- '1.Integer ;
'I:Integer <- '1.Integer ;
'J:Integer <- '1.Integer,
'return['1.Integer],
'_or_[...], 26}
==========================================
red metaSmtSearch2(upModule('ROBOT-DYNAMICS, false),
upTerm(< r : Robot | pos : [IPX, IPY], vel : [IVX, IVY], acc : [IAX, IAY], time : CLK >),
upTerm(< r : Robot | pos : [NPX, NPY], ATTRSET >),
upTerm(NPX === 10/1 and NPY === 10/1 and IPX === 0/1 and IPY === 0/1
and IVX === 0/1 and IVY === 0/1 and IAX === 0/1
and IAY === 0/1 and CLK === 0/1) = upTerm((true).Bool),
'=>*, unbounded, 1, 'QF_NRA) .
result SmtResult2: {'<_:_|_>[...],
'%%ubVar$10:Real <- '10/1.Real ;
'%%ubVar$11:Real <- '10/1.Real ;
'%%ubVar$12:Real <- '20/3.Real ;
'%%ubVar$13:Real <- '20/1.Real ;
'%%ubVar$14:Real <- '2/1.Real ;
'%%ubVar$15:Real <- '1/1.Real ;
'%%ubVar$1:Real <- '20/3.Real ;
'%%ubVar$2:Real <- '10/3.Real ;
'%%ubVar$3:Real <- '0/1.Real ;
'%%ubVar$4:Real <- '20/3.Real ;
'%%ubVar$5:Real <- '0/1.Real ;
'%%ubVar$6:Real <- '1/1.Real ;
'%%ubVar$7:Real <- '1/1.Real ;
'%%ubVar$8:Real <- '0/1.Real ;
'%%ubVar$9:Real <- '20/1.Real ;
'CLK:Real <- '0/1.Real ;
'IAX:Real <- '0/1.Real ;
'IAY:Real <- '0/1.Real ;
'IPX:Real <- '0/1.Real ;
'IPY:Real <- '0/1.Real ;
'IVX:Real <- '0/1.Real ;
'IVY:Real <- '0/1.Real ;
'NPX:Real <- '10/1.Real ;
'NPY:Real <- '10/1.Real,
'<_:_|_>[...], 180}
In the current alpha version, the number of rewrites reported by metaSmtSearch2 is incorrect.
As we need to explore 180 states to find reachable state for robot example, we can reduce the search space by enabling folding as follows.
red metaSmtSearch2(upModule('ROBOT-DYNAMICS, false),
upTerm(< r : Robot | pos : [IPX, IPY], vel : [IVX, IVY], acc : [IAX, IAY], time : CLK >),
upTerm(< r : Robot | pos : [NPX, NPY], ATTRSET >),
upTerm(NPX === 10/1 and NPY === 10/1 and IPX === 0/1 and IPY === 0/1
and IVX === 0/1 and IVY === 0/1 and IAX === 0/1
and IAY === 0/1 and CLK === 0/1) = upTerm((true).Bool),
'=>*, unbounded, 1, 'QF_NRA, true) .
==========================================
result SmtResult2: {'<_:_|_>[...],
'%%ubVar$10:Real <- '10/1.Real ;
'%%ubVar$11:Real <- '10/1.Real ;
'%%ubVar$12:Real <- '20/3.Real ;
'%%ubVar$13:Real <- '20/1.Real ;
'%%ubVar$14:Real <- '2/1.Real ;
'%%ubVar$15:Real <- '1/1.Real ;
'%%ubVar$1:Real <- '20/3.Real ;
'%%ubVar$2:Real <- '10/3.Real ;
'%%ubVar$3:Real <- '0/1.Real ;
'%%ubVar$4:Real <- '20/3.Real ;
'%%ubVar$5:Real <- '0/1.Real ;
'%%ubVar$6:Real <- '1/1.Real ;
'%%ubVar$7:Real <- '1/1.Real ;
'%%ubVar$8:Real <- '0/1.Real ;
'%%ubVar$9:Real <- '20/1.Real ;
'CLK:Real <- '0/1.Real ;
'IAX:Real <- '0/1.Real ;
'IAY:Real <- '0/1.Real ;
'IPX:Real <- '0/1.Real ;
'IPY:Real <- '0/1.Real ;
'IVX:Real <- '0/1.Real ;
'IVY:Real <- '0/1.Real ;
'NPX:Real <- '10/1.Real ;
'NPY:Real <- '10/1.Real,
'<_:_|_>[...], 37}
The result shows that we could find the solution by exploring only 37 states.
Python API
Since we use Maude-as-a-library to implement Maude-SE, we also provide the Python API for Maude-SE by using the Python implementation. For example, the api-test.py file shows how to perform SMT search for the gcd and robot examples using the Python API. See our api-test.py for more details.
import maude
...
from maudeSE.api import * # import our Python API
maude.init(advise=False)
maude.load(os.path.join(os.path.dirname(__file__), '.', 'api-test.maude'))
gcd = maude.getModule('GCD')
init = gcd.parseTerm('gcd(10, I:Integer)')
goal = gcd.parseTerm('return(J:Integer)')
c = maude.EqualityCondition(gcd.parseTerm('I:Integer < 9 and I:Integer > 0'),
gcd.parseTerm('(true).Bool'))
gcd_result = smtSearch2(gcd, init, goal, c, "=>*", "unbounded", 8, False)
print(gcd_result)
The arguments of the smtSearch2 function are not meta-level terms.
We can run the test file api-test.py using the following command:
python3 api-test.py
The result are as follows.
{'return['#ubVar$9:Integer],
'#newVar$0:Integer <- '1.Integer ;
'#ubVar$1:Integer <- '9.Integer ;
'#ubVar$2:Integer <- '8.Integer ;
'#ubVar$3:Integer <- '7.Integer ;
'#ubVar$4:Integer <- '6.Integer ;
'#ubVar$5:Integer <- '5.Integer ;
'#ubVar$6:Integer <- '4.Integer ;
'#ubVar$7:Integer <- '3.Integer ;
'#ubVar$8:Integer <- '2.Integer ;
'#ubVar$9:Integer <- '1.Integer ;
'I:Integer <- '1.Integer ;
'J:Integer <- '1.Integer,'return['1.Integer],
..., 26}
==========================================
{'<_:_|_>[...],
'%%ubVar$10:Real <- '10/1.Real ;
'%%ubVar$11:Real <- '10/1.Real ;
'%%ubVar$12:Real <- '20/3.Real ;
'%%ubVar$13:Real <- '20/1.Real ;
'%%ubVar$14:Real <- '2/1.Real ;
'%%ubVar$15:Real <- '1/1.Real ;
'%%ubVar$1:Real <- '20/3.Real ;
'%%ubVar$2:Real <- '10/3.Real ;
'%%ubVar$3:Real <- '0/1.Real ;
'%%ubVar$4:Real <- '20/3.Real ;
'%%ubVar$5:Real <- '0/1.Real ;
'%%ubVar$6:Real <- '1/1.Real ;
'%%ubVar$7:Real <- '1/1.Real ;
'%%ubVar$8:Real <- '0/1.Real ;
'%%ubVar$9:Real <- '20/1.Real ;
'CLK:Real <- '0/1.Real ;
'IAX:Real <- '0/1.Real ;
'IAY:Real <- '0/1.Real ;
'IPX:Real <- '0/1.Real ;
'IPY:Real <- '0/1.Real ;
'IVX:Real <- '0/1.Real ;
'IVY:Real <- '0/1.Real ;
'NPX:Real <- '10/1.Real ;
'NPY:Real <- '10/1.Real,'<_:_|_>[...],180}
==========================================
{'<_:_|_>[...],
'%%ubVar$10:Real <- '10/1.Real ;
'%%ubVar$11:Real <- '10/1.Real ;
'%%ubVar$12:Real <- '20/3.Real ;
'%%ubVar$13:Real <- '20/1.Real ;
'%%ubVar$14:Real <- '2/1.Real ;
'%%ubVar$15:Real <- '1/1.Real ;
'%%ubVar$1:Real <- '20/3.Real ;
'%%ubVar$2:Real <- '10/3.Real ;
'%%ubVar$3:Real <- '0/1.Real ;
'%%ubVar$4:Real <- '20/3.Real ;
'%%ubVar$5:Real <- '0/1.Real ;
'%%ubVar$6:Real <- '1/1.Real ;
'%%ubVar$7:Real <- '1/1.Real ;
'%%ubVar$8:Real <- '0/1.Real ;
'%%ubVar$9:Real <- '20/1.Real ;
'CLK:Real <- '0/1.Real ;
'IAX:Real <- '0/1.Real ;
'IAY:Real <- '0/1.Real ;
'IPX:Real <- '0/1.Real ;
'IPY:Real <- '0/1.Real ;
'IVX:Real <- '0/1.Real ;
'IVY:Real <- '0/1.Real ;
'NPX:Real <- '10/1.Real ;
'NPY:Real <- '10/1.Real,'<_:_|_>[...],37}
Module restrictions
Currently, we make several restrictions to rewrite rules and equations:
- Rewrite rules should not have non-SMT constraints in their conditions.
- Equations should not contradict or conflict with SMT theories.
- When defining and connecting SMT symbols using metadata, one should not use equational axiom attritues (e.g., assoc, comm, id) and the metadata attributes together.