Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha104/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha104/ 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 1-step rewriting modulo SMT. Bug fixes ======= (1) A longstanding bug where commands with 2 optional numeric arguments would not echo the first numeric argument if the second was not given. For example: mod FOO is sort Foo . ops a b : -> Foo . rl a => b . endm search [1] a =>! X:Foo . Here the [1] is missing from the echoed command. (2) A longstanding bug in the descent function cacheing where asking for solution #n twice in succession rather than solution #n followed by solution #n+1 missed the cache and did the computation twice. For some descent functions this bug only manifests itself for n = 0, while for metaSearch() the bug is triggered for all values of n, as the following example demonstrates: mod TWO is sort Foo . ops a b c : -> Foo . rl a => b . rl a => c . endm set trace on . red in META-LEVEL : metaSearch(['TWO], 'a.Foo, 'X:Foo, nil, '+, 1, 0) . red in META-LEVEL : metaSearch(['TWO], 'a.Foo, 'X:Foo, nil, '+, 1, 0) . red in META-LEVEL : metaSearch(['TWO], 'a.Foo, 'X:Foo, nil, '+, 1, 1) . red in META-LEVEL : metaSearch(['TWO], 'a.Foo, 'X:Foo, nil, '+, 1, 1) . Changes ====== First off, the concrete syntax for the SMT signature has changed slightly. The SMT tt and ff constants are renamed to match their BOOL counterparts: op true : -> Boolean [special (id-hook SMT_Symbol (true))] . op false : -> Boolean [special (id-hook SMT_Symbol (false))] . Since ad hoc overloading of constants is always allowed this does not cause problems, although in rare cases it may require explicit disambiguation. Note that at the metalevel, meta-constants are always tagged with their sort. Also the various SMT equality/inequality operators that used to be called _=_ and _!=_ are renamed to use the syntax from the long purged IDENTICAL module: op _===_ : Boolean Boolean -> Boolean [gather (e E) prec 51 special (id-hook SMT_Symbol (===))] . op _=/==_ : Boolean Boolean -> Boolean [gather (e E) prec 51 special (id-hook SMT_Symbol (=/==))] . op _===_ : Integer Integer -> Boolean [gather (e E) prec 51 special (id-hook SMT_Symbol (===))] . op _=/==_ : Integer Integer -> Boolean [gather (e E) prec 51 special (id-hook SMT_Symbol (=/==))] . op _===_ : Real Real -> Boolean [gather (e E) prec 51 special (id-hook SMT_Symbol (===))] . op _=/==_ : Real Real -> Boolean [gather (e E) prec 51 special (id-hook SMT_Symbol (=/==))] . This is to avoid ambiguity issues with condition fragments. Originally I thought to use the same syntax as the polymorphic BOOL equality/inequality operators since it doesn't make sense to do rewriting modulo SMT in a module that imports BOOL because rewriting modulo SMT as currently defined has no concept of equations. However it turns out that having a module that imports BOOL (indirectly via META-LEVEL) and SMT modules is desirable when working at the metalevel even though no rewriting modulo SMT can be done in it. A module used for rewriting modulo SMT must not contain equations or membership axioms (this is checked for). Only comm and assoc axioms are allowed on user operators; collapse axioms (id:, idem) are not allowed (this is not currently checked). User operators are not allowed to return SMT sorts. Instead a super-sort should be created. Again this is not currently checked for. Rules have a very restricted form: rl lhs => rhs . crl lhs => rhs if c1 = c1' /\ ... /\ cn = cn' . Here lhs must not contain any SMT operators - non-variable SMT subterms must be abstracted by SMT variables and moved in to the condition since Maude's matcher does not grok them. This abstraction is not currently checked, and failure to do it correctly will lead to missed matches. There is no such restriction on rhs, so abstracting SMT subterms here is optional. The terms in the condition, c1,..., cn and c1',..., cn', must only contain SMT operators and variables. Any violation of this will cause failure of the condition, since the SMT solver can only deal with pure SMT expressions. The normal way of using conditions is a single fragment of the form = true where is an pure SMT term of sort Boolean denoting a quantifier-free formula. But the more general form is understood and converted to a SMT expression consisting of an SMT conjunction of SMT equalities. For rewriting module SMT, there is no requirement that SMT variables occurring in the condition or rhs appear in the lhs. However if this is done, the rule should be given the nonexec attribute to prevent other parts of Maude from complaining. During rewriting modulo SMT, unbound SMT variables are bound to fresh SMT variables. Having unbound non-SMT variables is prohibited, but this is not checked for. In principle all rules should have a lhs and rhs that parse to the same sort. In practice Maude only insists (as usual) that the lhs and rhs of a given rule parse to sorts in the same kind. Since rewriting module SMT only happens at the top of a term, having rules in different kinds simply partitions the rule set, with only the partition corresponding to the kind of the current term active. Rewriting modulo SMT takes place at the top of a term representing the state, while the accumulated constraint is stored in a term of sort Boolean. These terms are paired to represent a constrained state. Currently there is no state sort, pair sort or pairing operator defined. These should be declared by the user. The names of the state sort and pair sort are unimportant. The syntax of the pairing constructor is unimportant, but it must be a free ctor of two arguments, the first one of the state sort, the second one of sort Boolean and the return sort must be the pair sort. I use: sorts State Pair . op <_|_> : State Boolean -> Pair [ctor] . Here is an example that defined a multiset of SMT Integers with a rule to extract pairs of integers that meet certain criteria. load smt mod INTEGER-SOUP is pr INTEGER . sorts State Pair . op <_|_> : State Boolean -> Pair [ctor] . sort Soup . subsort Integer < Soup . op __ : Soup Soup -> Soup [assoc comm] . op f : Soup -> State . op g : Integer Integer -> State . vars I J K : Integer . var S : Soup . crl f(I J S) => g(I, J) if I === 3 * J = true . endm 1-step rewriting modulo SMT is invoked with the smt-search command. The syntax is smt-search [] in : . For example: smt-search [3] in INTEGER-SOUP : < f(1 2 3 4 5 6 7 8 9 10 11 12) | true > . The solutions are constructed using the same pairing operation used to form the constrained state. As usual the [] and in parts are optional. It is possible to pass SMT variables in the query to get symbolic solutions: smt-search < f(K 1 2 3 4 5 6 7 8 9 10 11 12) | true > . smt-search < f(K 1 2 3 4 5 6 7 8 9 10 11 12) | K <= 24 > . smt-search < f(K 1 2 3 4 5 6 7 8 9 10 11 12) | K divisible 5 > . Notice that Maude does not grok the semantics of the SMT data types and does not attempt to simplify the accumulated constraint. If a rule contains SMT variables in the rhs or condition that are not bound in the lhs, they are bound to fresh variables. Note that such rules should have the nonexec attribute. For example: mod INTEGER-SOUP2 is pr INTEGER . sorts State Pair . op <_|_> : State Boolean -> Pair [ctor] . sort Soup . subsort Integer < Soup . op __ : Soup Soup -> Soup [assoc comm] . op f : Soup -> State . op g : Integer Integer -> State . vars I J K : Integer . var S : Soup . crl f(I S) => g(I, K) if I === 3 * K = true [nonexec] . endm smt-search < f(1 2 3 4 5 6 7 8 9 10 11 12) | true > . Currently the fresh variable names look like #1-K:Integer i.e. #- but this may change. The smt-search command is reflected by the descent function: op metaSmtSearch : Module Term Qid Nat Bound Nat ~> SmtResult? [special (...)] . Return values are constructed from the signature: sort SmtResult SmtResult? . subsort SmtResult < SmtResult? . op {_,_} : Term Nat -> SmtResult [ctor] . op failure : -> SmtResult? [ctor] . Here the Qid must be '+ and the Bound must 1 since only 1-step rewriting modulo SMT is currently supported. The first Nat argument specifies a number that is at least as larget as the the number in the largest numbered free variable occurring in the Term argument - this is not currently checked. The Nat value in the result is the largest number of a free variable in the Term part. This follows the convention used to ensure freshness of variables in metaUnify(), and allows the user to pass the result of one metaSmtSearch() to another metaSmtSearch without renaming any fresh variables to avoid clashes. As usually the final Nat argument specifies which solution is wanted; if such a solution does not exist, failure is returned. It is convenient to have a module that includes both the module to be used for SMT rewriting the META-LEVEL. This module will thus have both Bool and Boolean sorts. For example: mod TEST is pr INTEGER-SOUP2 . pr META-LEVEL . endm red metaSmtSearch(['INTEGER-SOUP2], upTerm(< f(1 2 3 4 5 6 7 8 9 10 11 12) | true >), '+, 0, 1, 0) . red metaSmtSearch(['INTEGER-SOUP2], upTerm(< f(1 2 3 4 5 6 7 8 9 10 11 12) | true >), '+, 0, 1, 1) . red metaSmtSearch(['INTEGER-SOUP2], upTerm(< f(1 2 3 4 5 6 7 8 9 10 11 12) | true >), '+, 0, 1, 2) . red metaSmtSearch(['INTEGER-SOUP2], upTerm(< f(1 2 3 4 5 6 7 8 9 10 11 12) | true >), '+, 0, 1, 3) . red metaSmtSearch(['INTEGER-SOUP2], upTerm(< f(1 2 3 4 5 6 7 8 9 10 11 12) | true >), '+, 0, 1, 5) . red metaSmtSearch(['INTEGER-SOUP2], upTerm(< f(1 2 3 4 5 6 7 8 9 10 11 12) | true >), '+, 42, 1, 0) . Steven