Examples

Examples for Metalevel Functions
1. smt-check-ex.maude
2. smt-search-ex.maude
Module restrictions

Examples for Metalevel Functions

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

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

smt-check-ex.maude

This file demonstrates 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

1. SIMPLE Module: This module simply imports INTEGER module.

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

2. EUF Module: This module defines a new sort A and an uninterpreted symbol f.

fmod EUF is
  pr BOOLEAN .

  sort A .

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

3. EUF-ARRAY Module: This module connects interpreted symbols from the Array 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. EUF-XOR Module: This module contains another example for uninterpreted symbol.

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. For example, you can run the example with the CVC5 solver using the following command.

$ maude-se ./smt-check-ex.maude -s cvc5 -no-meta

Here’s some results:

==========================================
reduce in SIMPLE : metaSmtCheck(upModule('INTEGER, false), upTerm(X:Integer > (4).Integer), 'QF_LRA, true) .
result SmtCheckResult: {'X:Integer |-> '5.Integer}
==========================================
reduce in EUF-XOR-CHECK : metaSmtCheck(upModule('EUF-XOR, false), upTerm((0).Integer <= (N xor (255).Integer)), 'QF_UFLIA, true) .
result SmtCheckResult: 
  {'N:Integer |-> '1.Integer}
==========================================
...

smt-search-ex.maude

This file provides examples for metaSmtSearch 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 metaSmtSearch, we need to import META-SMT-SEARCH 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 metaSmtSearch(upModule('GCD, false), upTerm(gcd(10, I)), upTerm(return(J)), 
                  upTerm(I < 9 and I > 0) = upTerm((true).Boolean), '*, unbounded, 0, 'QF_LRA) .

red metaSmtSearch(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).Boolean), '*, unbounded, 0, 'QF_NRA) .

The first command searches for the first 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.

We can run the both commands with Z3 using the following command:

$ maude-se smt-search-ex.maude -no-meta

The search results are as follows.

==========================================
reduce in GCD-ANALYSIS : metaSmtSearch(upModule('GCD, false), upTerm(gcd((10).Integer, I)), upTerm(return(J)), upTerm(I < (9).Integer and I > (0).Integer) = upTerm((true).Boolean), '*, unbounded, (0).Zero, 'QF_LRA) .
rewrites: 310 in 5ms cpu (9ms real) (52837 rewrites/second)
result SmtResult2: {'return['%%ubVar$5:Integer],...,
  ...
  '%%ubVar$1:Integer <- '5.Integer ;
  '%%ubVar$2:Integer <- '5.Integer ;
  '%%ubVar$3:Integer <- '10.Integer ;
  '%%ubVar$4:Integer <- '5.Integer ;
  '%%ubVar$5:Integer <- '5.Integer ;
  '%%ubVar$6:Integer <- '5.Integer ;
  'I:Integer <- '5.Integer ;
  'J:Integer <- '5.Integer ;
  'V0:Integer <- '10.Integer ;
  'V1:Integer <- '5.Integer ;
  'V2:Integer <- '5.Integer, (6).NzNat, (3).NzNat}
==========================================
reduce in ROBOT-ANALYSIS : metaSmtSearch(upModule('ROBOT-DYNAMICS, false), upTerm(< r : Robot | pos : [IPX, IPY], vel : [IVX, IVY], acc : [IAX, IAY], time : CLK >), upTerm(< r : Robot | ATTRSET, pos : [NPX, NPY] >), upTerm(NPX === (10/1).Real and NPY === (10/1).Real and IPX === (0/1).Real and IPY === (0/1).Real and IVX === (0/1).Real and IVY === (0/1).Real and IAX === (0/1).Real and IAY === (0/1).Real and CLK === (0/1).Real) = upTerm((true).Boolean), '*, unbounded, (0).Zero, 'QF_NRA) .
rewrites: 1181 in 386ms cpu (391ms real) (3055 rewrites/second)
result SmtResult2: {'<_:_|_>['r.Oid, 'Robot.Robot ...
  ...
  '%%ubVar$9:Real <- '20/3.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 ;
  'V0:Real <- '0/1.Real ;
  'V1:Real <- '0/1.Real ;
  'V2:Real <- '0/1.Real ;
  'V3:Real <- '0/1.Real ;
  'V4:Real <- '0/1.Real ;
  'V5:Real <- '0/1.Real ;
  'V6:Real <- '0/1.Real ;
  'V7:Real <- '10/1.Real ;
  'V8:Real <- '10/1.Real, (53).NzNat, (180).NzNat}

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.

reduce in ROBOT-ANALYSIS : metaSmtSearch(upModule('ROBOT-DYNAMICS, false), upTerm(< r : Robot | pos : [IPX, IPY], vel : [IVX, IVY], acc : [IAX, IAY], time : CLK >), upTerm(< r : Robot | ATTRSET, pos : [NPX, NPY] >), upTerm(NPX === (10/1).Real and NPY === (10/1).Real and IPX === (0/1).Real and IPY === (0/1).Real and IVX === (0/1).Real and IVY === (0/1).Real and IAX === (0/1).Real and IAY === (0/1).Real and CLK === (0/1).Real) = upTerm((true).Boolean), '*, unbounded, 0, 'QF_NRA, true) .
rewrites: 1145 in 11073ms cpu (11138ms real) (103 rewrites/second)
result SmtResult2: {'<_:_|_>[...] ;
  ...
  '%%ubVar$11:Real <- '20/3.Real ;
  '%%ubVar$7:Real <- '10/3.Real ;
  '%%ubVar$8:Real <- '0/1.Real ;
  '%%ubVar$9:Real <- '20/3.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 ;
  ...
  'V8:Real <- '10/1.Real, (53).NzNat, (128).NzNat}

The result shows that we could find the same solution by exploring 128 states.

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.

Examples

Table of contents

Examples for Metalevel Functions

smt-check-ex.maude

smt-search-ex.maude

Module restrictions