Dear Maude Abusers,

A new alpha release can be accessed at SRI-CSL in:

~eker/public_html/Maude/Alpha105/

or downloaded from:

http://www.csl.sri.com/~eker/Maude/Alpha105/

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This is an alpha quality release, to allow users to experiment with a tentative implementation
of multi-step search modulo SMT.

Changes
======
The smt-search no longer works on <state, contraint> pairs and instead has a syntax suggested by Jose.

smt-search [<#solutions>, <depth>] in <module> : <start-term> <arrow> <pattern> such that <condition> .

Here the
  [<#solutions>, <depth>]
  in <module> :
  s.t. <condition>
parts are optional as with the regular search command. Also the ", <depth>" subpart may omitted from the
[<#solutions>, <depth>] part.

<arrow> may be =>* or =>+
At the object level only the arrow =>1 is acceptable as an abreviation for =>+ while setting depth to 1.
The arrow =>! doesn't make sense for symbolic search and is not supported.

<depth> must be >= 1 if included. If no depth is specified it is assumed to unbounded.

<start-term> may only have variables of an SMT sort but otherwise isn't subject to restrictions.

<pattern> must be linear in both SMT and non-SMT variables, and may not contain SMT operators. Note
that non-linear SMT variables and SMT subexpressions can both be eliminated by the user by
abstracting with a fresh SMT variable and adding an equality constraint to <condition>.

<condition> may only have equality fragments and must be purely SMT.

One subtlety is that the constraints in <condition> will be checked as the search proceeds but
further constraints arising from the matching <pattern> may also be checked after the match.
It is reasonable for an SMT variable to appear in <start-term>, <pattern> and <condition> as long as
it is linear in <pattern>.

A solution consists of a substitution binding any non-SMT variables in <pattern> and an SMT constraint.
Note that SMT variables are constrained rather than bound and do not appear in the substitution.
This is because it is reasonable to constrain I === I + J + K but binding I --> I + J + K
is an occurs check failure.

load smt

set show advise off .

mod ITEST is
  pr INTEGER .

  vars A B C D E : Boolean .
  vars I J K L M N : Integer .

  sort State .

  sort Foo .
  ops f : Integer -> State .
  var X : State .


  crl f(I) => f(I + 1) if I >= 10 = true /\ I <= 12  = true .
  crl f(I) => f(I - 1) if I >= 10 = true /\ I <= 12  = true .
endm

smt-search [4] f(11) =>1 X .
smt-search [4] f(11) =>* X .
smt-search [4] f(11) =>+ X .
smt-search [4] f(J) =>* f(K)  such that J = K .

Note that the seach is often infinite. Support for ^C interrupts is incomplete but it works some of the time.

At the metalevel metaSmtSearch now looks like:

  op metaSmtSearch : Module Term Term Condition Qid Nat Bound Nat ~> SmtResult? [....] .

The arguments are:
  Meta-module to use
  Start meta-term
  Pattern meta-term
  Meta-condition
  Search type: '+ or '*
  Last variable number to avoid - all fresh variables will have a larger number in them
  Depth bound
  Solution number

Meta-solutions are now constructed with:

  op {_,_,_,_} : Term Substitution Term Nat -> SmtResult [ctor] .

The arguments are:
  State meta-term
  Matching meta-substitution for non-SMT variables
  Constraint encoded as a meta-term
  Largest variable number used
  
For example:

mod TEST2 is
  pr ITEST .
  pr META-LEVEL .
  vars I J K L M N : Integer .
endm

red metaSmtSearch(['ITEST],
                  upTerm(f(J)),
                  upTerm(f(K)),
                  'J:Integer = 'K:Integer,
                  '*, 42, 2, 0) .

Steven