Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha103/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha103/ Alpha release site authentication: User Name: maudeabuser Password: bughunter This is an alpha quality release, to allow users to experiment with a single new feature: a very tentative integration with the CVC4 SMT solver. Bug fixes -------- (1) Tokens of the form 0/n for positive integer n (e.g. 0/1) are now recognized as valid rational numbers. (2) Maude now prints an advisory when reflecting down a meta-term yields a term of the wrong kind; for example: red in META-LEVEL : downTerm(''foo.Qid, 9) . Previous it would return 9 without alerting the user. (3) A bug where metaPrettyPrint() would fail to generation disambiguation syntax for non-algebraic constants or terms made from built-in operators; For example: fmod FOO is pr META-LEVEL . sort Foo . op 1 : -> Foo . endfm red metaPrettyPrint(['FOO], 's_['0.Zero]) . Here the 1 symbol belonging to Foo has the same concrete syntax as the number syntax for the term s 0, but metaPrettyPrint() fails to generate the disambiguation syntax. New feature ----------- There is an interface to allow CVC4 to be called from Maude, both from the command line and (more usefully) from the meta-level. The design is a first draft to allow experimentation and will likely change in the near future. Currently only direct queries to CVC4 are supported - built-in support for rewriting modulo SMT is not yet implemented. The theoretical framework for rewriting modulo SMT [1,2] and the de facto standard for presenting SMT problems, SMT-LIB [3] (which btw is actually a language, not a library API), both assume a many-sorted algebra for SMT types. Thus the representation of SMT types in Maude is orthogonal to Maude's normal built-in data types and is many-sorted and non-algebraic. This may change in the future if the theory for mapping from an order-sorted algebra to many-sorted algebra plus SMT constraints is developed, however the current design sticks closely to SMT-LIB. The SMT interface is accessed by loading the file smt.maude The SMT-LIB "Core theory" is represented by the following signature: fmod BOOLEAN is sort Boolean . op tt : -> Boolean [special (id-hook SMT_Symbol (true))] . op ff : -> Boolean [special (id-hook SMT_Symbol (false))] . op not_ : Boolean -> Boolean [prec 53 special (id-hook SMT_Symbol (not))] . op _and_ : Boolean Boolean -> Boolean [gather (E e) prec 55 special (id-hook SMT_Symbol (and))] . op _xor_ : Boolean Boolean -> Boolean [gather (E e) prec 57 special (id-hook SMT_Symbol (xor))] . op _or_ : Boolean Boolean -> Boolean [gather (E e) prec 59 special (id-hook SMT_Symbol (or))] . op _implies_ : Boolean Boolean -> Boolean [gather (e E) prec 61 special (id-hook SMT_Symbol (implies))] . 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 _?_:_ : Boolean Boolean Boolean -> Boolean [gather (e e e) prec 71 special (id-hook SMT_Symbol (ite))] . endfm Here tt and ff are used for true and false to avoid immediately ambiguity with Maude's Bool sort. All of the operators are inert - they have no built-in semantics at the Maude level - they are simply a way to represent SMT expressions in Maude. The _?_:_ operator is the if-the-else operation and _=_ and _!=_ are used to represent equality and inequality, again to minimize syntactic ambiguity. The SMT-LIB "Ints theory" is represented by the following signature: fmod INTEGER is protecting BOOLEAN . sort Integer . op : -> Integer [special (id-hook SMT_NumberSymbol (integers))] . op -_ : Integer -> Integer [special (id-hook SMT_Symbol (-))] . op _+_ : Integer Integer -> Integer [gather (E e) prec 33 special (id-hook SMT_Symbol (+))] . op _*_ : Integer Integer -> Integer [gather (E e) prec 31 special (id-hook SMT_Symbol (*))] . op _-_ : Integer Integer -> Integer [gather (E e) prec 33 special (id-hook SMT_Symbol (-))] . op _div_ : Integer Integer -> Integer [gather (E e) prec 31 special (id-hook SMT_Symbol (div))] . op _mod_ : Integer Integer -> Integer [gather (E e) prec 31 special (id-hook SMT_Symbol (mod))] . op _<_ : Integer Integer -> Boolean [prec 37 special (id-hook SMT_Symbol (<))] . op _<=_ : Integer Integer -> Boolean [prec 37 special (id-hook SMT_Symbol (<=))] . op _>_ : Integer Integer -> Boolean [prec 37 special (id-hook SMT_Symbol (>))] . op _>=_ : Integer Integer -> Boolean [prec 37 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 _?_:_ : Boolean Integer Integer -> Integer [gather (e e e) prec 71 special (id-hook SMT_Symbol (ite))] . op _divisible_ : Integer Integer -> Boolean [prec 51 special (id-hook SMT_Symbol (divisible))] . endfm Here the integer constants are a non-algebraic defined set, , whose concrete representation is the usual one: ..., -2, -1, 0, 1, 2, ... Again all of the operators are inert. Note that _divisible_ has the opposite argument order to Maude's _divides_ operator on Ints. It follows the SMT-LIB convention. The SMT-LIB "Reals theory" is represented by the following signature: fmod REAL is protecting BOOLEAN . sort Real . op : -> Real [special (id-hook SMT_NumberSymbol (reals))] . op -_ : Real -> Real [special (id-hook SMT_Symbol (-))] . op _+_ : Real Real -> Real [gather (E e) prec 33 special (id-hook SMT_Symbol (+))] . op _*_ : Real Real -> Real [gather (E e) prec 31 special (id-hook SMT_Symbol (*))] . op _-_ : Real Real -> Real [gather (E e) prec 33 special (id-hook SMT_Symbol (-))] . op _/_ : Real Real -> Real [gather (E e) prec 31 special (id-hook SMT_Symbol (/))] . op _<_ : Real Real -> Boolean [prec 37 special (id-hook SMT_Symbol (<))] . op _<=_ : Real Real -> Boolean [prec 37 special (id-hook SMT_Symbol (<=))] . op _>_ : Real Real -> Boolean [prec 37 special (id-hook SMT_Symbol (>))] . op _>=_ : Real Real -> Boolean [prec 37 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 (!=))] . op _?_:_ : Boolean Real Real -> Real [gather (e e e) prec 71 special (id-hook SMT_Symbol (ite))] . endfm Here the real constants are a non-algebraically defined set, , of which only the rational subset have concrete representations, that look like -1/1, -3/100, 0/1, 7/3 etc. The / symbol is mandatory and servers to distinguish the Reals from the Integers (which are completely different types in SMT-LIB). Again all of the operators are inert, although currently, rational constants are canonicalized (this may change). Finally the SMT-Lib "Reals-Ints theory" is represented by the following signature: fmod REAL-INTEGER is protecting INTEGER . protecting REAL . op toReal : Integer -> Real [special (id-hook SMT_Symbol (toReal))] . op toInteger : Real -> Integer [special (id-hook SMT_Symbol (toInteger))] . op isInteger : Real -> Boolean [special (id-hook SMT_Symbol (isInteger))] . endfm Again it should be emphasized that this is just inert syntax with no built-in semantics from Maude's point of view. The interpretation of the syntax is completely up to CVC4. CVC4 can be called using the check command: fmod TEST-RI is pr REAL-INTEGER . vars W X Y Z : Boolean . vars I J K L : Integer . vars P Q R S : Real . endfm check toInteger(R) + toInteger(P) = toInteger(R + P) . check not(toInteger(R) + toInteger(P) = toInteger(R + P)) . check -2 < I and -2 * I > -1 and I != -1 . check -2 < I and -2 * I > -1 and I != -1 and I - I != I . The syntax of this command is: check [in :] . where must only contain the constants and operators from the appropriate signatures above, together with variables from the 3 sorts, Boolean, Integer and Real when these are available. Adding any super or subsorts to these 3 sorts (or subsort relations between them) will cause issues, as will adding any additional operators. Maude responds with whatever CVC4 returns, typically sat or unsat. Note that the current implementation is quite brittle. There is only a cursory attempt to check that the query to CVC4 makes sense and no attempt to catch CVC4's exceptions - attempting to check a non-linear arithmetic assertion, for example, will cause a crash. There is no ^C interrupt while in CVC4. The reflection of the SMT signatures follows the normal Maude metalevel conventions with for example 1/3 becoming '1/3.Real The check command is reflected by the descent function: op metaCheck : Module Term ~> Bool [special (...)] . For example: fmod META-CHECK is pr META-LEVEL . pr REAL-INTEGER . vars W X Y Z : Boolean . vars I J K L : Integer . vars P Q R S : Real . endfm red metaCheck(['META-CHECK], upTerm( (I > J ? I : J) = I or (I > J ? I : J) = J )) . red metaCheck(['META-CHECK], upTerm( not((I > J ? I : J) = I or (I > J ? I : J) = J ) )) . red metaCheck(['META-CHECK], upTerm( (I > J ? I : J) != I and (I > J ? I : J) != J )) . red metaCheck(['META-CHECK], upTerm( (I > J ? I : J) != I or (I > J ? I : J) != J )) . Here metaCheck() returns true if CVC4 responds with sat and false otherwise (CVC4 can occasionally produce results other than sat and unsat, for example if it can't decide satisfiability). As stated above, this is a tentative first attempt to integrating Maude and SMT and I'm very interested in getting feedback. Steven [1] Camilo Rocha, Symbolic Reachability Analysis for Rewrite Theories, Ph.D. Dissertation. Urbana, October, 2012. [2] Camilo Rocha, Jose Meseguer and Cesar Munoz. Rewriting Modulo SMT and Open System Analysis, Procs. WRLA 2014. [3] David R. Cok, The SMT-LIBv2 Language and Tools: A Tutorial, www.grammatech.com/resource/smt/SMTLIBTutorial.pdf