More examples

We provide a zip file (maude-se-examples.zip), containing example files.

File	Description
smt-check-ex.maude	A Maude file containing examples for the check command
smt-search-ex.maude	A Maude file containing examples for the smt-search command
smt-check-meta-ex.maude	A Maude file containing examples for the metaSmtCheck function
smt-search-meta-ex.maude	A Maude file containing examples for the metaSmtSearch function

smt-check-ex.maude

This file demonstrates the usage of check with various theories and formulas, including both interpreted and uninterpreted symbols. It contains four functional modules:

• SIMPLE

• EUF

• ARRAY

• EUF-XOR

1. The SIMPLE module: A minimal example that imports the REAL-INTEGER module.

fmod SIMPLE is
  pr REAL-INTEGER .
  pr META-SMT-CHECK .
endfm

2. The EUF module: Defines a new sort A and declares f as an uninterpreted function symbol.

fmod EUF is
  pr BOOLEAN .

  sort A .

  op _===_ : A A -> Boolean .
  op f : A -> A [ctor metadata "smt euf"] .
endfm

3. The ARRAY module: Connects interpreted symbols from the SMT theory to Maude operators.

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

4. The EUF-XOR module: Contains a single uninterpreted symbol.

fmod EUF-XOR is
  pr INTEGER .
  op _xor_ : Integer Integer -> Integer [metadata "smt euf"] .
endfm

As shown in the EUF and EUF-XOR modules, uninterpreted symbols can be declared by defining operators and annotating them with the metadata attribute. For example, the uninterpreted symbol f in EUF is annotated with metadata smt euf, indicating that the operator is both an SMT symbol (smt) and an uninterpreted function (euf).

Another module, ARRAY, shows how to connect interpreted symbols to Maude using the metadata attribute. For example, the metadata smt array:select is used to denote the interpreted symbol select from the array theory. Additionally, a single interpreted symbol can be connected to multiple Maude operators. In the ARRAY module, for instance, select is associated with both select and _[_].

Important

The built-in converters already support the array select and store operators shown above. To connect a new interpreted SMT symbol that is not supported, extend or implement an SMT converter.

The downloadable smt-check-meta-ex.maude file contains satisfiability checks for these EUF and Array terms using metaSmtCheck without requesting a model. When a model is requested, assignments that cannot be represented as Maude terms (such as uninterpreted-function or array values) are retained as solver-text String assignments.

---

smt-check-meta-ex.maude

This file demonstrates the usage of metaSmtCheck with several usage examples. Satisfiability checking can be performed as explained in SMT Interface.

---

smt-search-ex.maude

This file includes examples demonstrating the use of smt-search with the gcd and robot modules. The search commands shown below are commented out in the example file; enter them at the MaudeSE prompt after loading the file.

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] .
   rl [r3] : gcd(X, X) => return (X) .
endm

The following command searches for the first solution term that matches return(J) and satisfies the condition I < 9 and I > 0, starting from the initial term gcd(10, I) under the QF_LIA logic.

MaudeSE> smt-search [1] in GCD : gcd(10, I:Integer) =>* return(J:Integer) 
                such that I:Integer > 0 and I:Integer < 9 using QF_LIA .

Solution 1 (state 3)

Symbolic state:
 return(#5-V5:Integer)

Constraint:
 V0:Integer === 10 and V1:Integer === I:Integer and ...

Substitution:
 V2:Integer <-- #5-V5:Integer

Assignment:
 #1-V12:Integer <-- 5
 #2-V13:Integer <-- 5
 ...
 I:Integer <-- 5
 J:Integer <-- 5
 V0:Integer <-- 10
 V1:Integer <-- 5
 V2:Integer <-- 5

Concrete state:
 return(5)

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

The following command searches for the first solution, using the QF_NRA logic, that matches the goal pattern < r : Robot | pos : [NPX, NPY], ATTRSET > and satisfies the condition NPX === 10/1 and NPY === 10/1. The initial term uses symbolic variables; the such that condition requires all initial attribute values to be zero.

MaudeSE> smt-search [1] in ROBOT-DYNAMICS :
              < r : Robot | pos : [IPX:Real, IPY:Real], vel : [IVX:Real, IVY:Real], 
                            acc : [IAX:Real, IAY:Real], time : CLK:Real >
          =>* < r : Robot | pos : [NPX:Real, NPY:Real], ATTRSET:AttributeSet > 
    such that NPX:Real === 10/1 and NPY:Real === 10/1 
          and IPX:Real === 0/1 and IPY:Real === 0/1 and IVX:Real === 0/1 and IVY:Real === 0/1 
          and IAX:Real === 0/1 and IAY:Real === 0/1 and CLK:Real === 0/1 using QF_NRA .

Solution 1 (state 180)

Symbolic state:
 < r : Robot | pos : [#35-V24:Real, #36-V25:Real], vel : [#37-V26:Real, #38-V27:Real], 
               acc : [#39-V28:Real, #40-V29:Real], time : #41-V30:Real >

Constraint:
 V0:Real === IPX:Real and V1:Real === IPY:Real and ...

Substitution:
 ATTRSET:AttributeSet <-- vel : [#37-V26:Real, #38-V27:Real], ...
 V7:Real <-- #35-V24:Real
 V8:Real <-- #36-V25:Real

Assignment:
 #1-V15:Real <-- 0/1
 #10-V28:Real <-- 0/1
 ...

Concrete state:
 < r : Robot | pos : [10/1, 10/1], vel : [20/1, 20/3], acc : [20/1, 0/1], time : 2/1 >

---

smt-search-meta-ex.maude

This file demonstrates the usage of metaSmtSearch, corresponding to the two commands described in the previous section.

---

Module restrictions

Currently, we impose several restrictions on rewrite rules and equations:

• The condition of a rewrite rule must be decomposed into pure SMT and non-SMT conditions.

• Equations must not contradict or conflict with SMT theories.

• When defining and connecting SMT symbols using metadata, equational axiom attributes (e.g., assoc, comm, id) must not be used together with metadata attributes.