Extensiones a la comprobación de satisfacibilidad de restricciones

Trabajo fin de m´ aster M´ aster en Ingenier´ ıa del Software, M´ etodos Formales y Sistemas de Informaci´ on Extensiones a la comprobaci´on de satisfacibilidad de restricciones Autor: Pablo Viciano Negre Director de tesina: Santiago Escobar 17 de septiembre de 2012 Resumen En esta tesina de m´aster se estudia la satisfacibilidad de f´ormulas en la aritm´etica Presburger para el lenguaje de programaci´on de alto rendimiento Maude y c´omo se pueden extender estos algoritmos a modelos que extiendan la aritm´etica Presburger con propiedades ecuacionales tales como asociatividad, conmutatividad e identidad, as´ı como el caso m´as complejo (con un algoritmo de semi-decisi´on en vez de un algoritmo de decisi´on) para teor´ıas ecuacionales con propiedades ecuacionales orientadas como reglas. Palabras Clave satisfacibilidad de f´ormulas ; unificaci´on ecuacional ; estrechamiento ecuacional ´ Indice general ´ Indice de figuras VII 1. Introducci´on 1 2. Conceptos b´asicos 5 2.1. Sistemas de reescritura de t´erminos . . . . . . . . . . . . . . . 5 2.2. Maude............................... 9 2.2.1. Un programa en Maude . . . . . . . . . . . . . . . . . 10 2.2.2. Tipos de datos predefinidos . . . . . . . . . . . . . . . 11 2.2.3. Declaraci´on obligatoria de variables . . . . . . . . . . . 11 2.2.4. Declaraciones de Tipos (Sorts), S´ımbolos ConstructoresyVariables ...................... 12 2.2.5. Tipos de datos ordenados y sobrecarga de operadores . 13 2.2.6. Propiedades avanzadas (o algebr´aicas) de los s´ımbolos . 14 2.2.7. Declaraci´on de Funciones . . . . . . . . . . . . . . . . . 16 2.2.8. B´usqueda eficiente de elementos en listas y conjuntos . 18 v vi ´ INDICE GENERAL 2.2.9. Ejecuci´on de programas en Maude ............ 19 2.2.10. Metanivel en Maude .................... 21 2.2.11. Unificaci´on y Estrechamiento en Maude . . . . . . . . . 27 2.3. CVC3 ............................... 31 2.3.1. Ejecutando CVC3 desde l´ınea de comandos . . . . . . . 32 2.3.2. Sistema de tipos de CVC3 . . . . . . . . . . . . . . . . 33 2.3.3. Comprobaci´on de tipos . . . . . . . . . . . . . . . . . . 39 2.3.4. T´erminos y f´ormulas . . . . . . . . . . . . . . . . . . . 39 2.4. Interfaz CVC3 en Maude . . . . . . . . . . . . . . . . . . . . . 42 2.4.1. Tipos de datos . . . . . . . . . . . . . . . . . . . . . . 42 2.4.2. Modo de uso de la interfaz . . . . . . . . . . . . . . . . 44 2.4.3. Ejemplos de expresiones . . . . . . . . . . . . . . . . . 46 3. Prototipo - Primera parte 49 3.1. Satisfacibilidad de igualdades sobre los n´umeros naturales en Maude............................... 49 3.2. Tiposdedatos .......................... 53 3.3. Transformaci´on de SATProblem a expresiones iBool ...... 54 3.4. Ejemplos de transformaci´on . . . . . . . . . . . . . . . . . . . 59 4. Prototipo - Segunda parte 63 4.1. Satisfacibilidad de igualdades para t´erminos cualesquiera . . . 63 ´ INDICE GENERAL vii 4.2. Tiposdedatos .......................... 65 4.3. Proceso de conversi´on . . . . . . . . . . . . . . . . . . . . . . . 67 4.3.1. Abstracci´on de variables . . . . . . . . . . . . . . . . . 67 4.3.2. Combinaci´on de variables . . . . . . . . . . . . . . . . 72 4.3.3. Conversi´on de PairSet aSATProblem .......... 75 4.3.4. Flujo de ejecuci´on del prototipo . . . . . . . . . . . . . 79 5. Prototipo - Tercera parte 83 5.1. Satisfacibilidad de igualdades con reglas extra . . . . . . . . . 83 5.2. Tiposdedatos .......................... 86 5.3. Ejecuci´on del algoritmo . . . . . . . . . . . . . . . . . . . . . . 87 5.3.1. Expansi´on de ecuaciones . . . . . . . . . . . . . . . . . 87 5.3.2. Obtenci´on de sustituciones mediante Narrowing . . . . 96 5.3.3. Generaci´on de estados . . . . . . . . . . . . . . . . . . 98 5.3.4. Control del flujo del programa . . . . . . . . . . . . . . 104 6. Conclusiones 115 Bibliograf´ıa 116 1 Introducci´on La satisfacibilidad de f´ormulas (Satisfiability -SAT) ha atra´ıdo [1] a muchos investigadores de diferentes disciplinas tales como la inteligencia artificial o la verificaci´on formal durante los ´ultimos a˜nos debido a la incre´ıble mejora en rendimiento de los SAT solvers. Se ha convertido en la pieza de tecnolog´ıa m´as decisiva en muchas ´areas de verificaci´on hardware y software. Por ejemplo, la verificaci´on de modelos con l´ımites (Bounded Model Checking -BMC ) es una de las ´areas que m´as extensamente utiliza SAT solvers. Donde un modelo (generado hasta cierto l´ımite) se traduce en cantidades enormes de f´ormulas booleanas tal que la verificaci´on de una propiedad concreta sobre ese modelo consiste en a˜nadir un conjunto extra de f´ormulas booleanas y utilizar un SAT solver para comprobar la satisfacibilidad del conjunto extendido de f´ormulas booleanas. Sin embargo, aunque la satisfacibilidad de f´ormulas ha ayudado a muchas ´areas, ocurre cada vez con m´as frecuencia que estas aplicaciones requieren la satisfacibilidad de f´ormulas en l´ogicas m´as ricas o con propiedades sem´anticas extra (correspondientes a la denominada teor´ıa de fondo). Para muchas teor´ıas de fondo, los m´etodos especializados han permitido disponer de procedimientos de decisi´on para la satisfacibilidad de f´ormulas libres de cuantificadores o para algunas subclases; ver [2]. De hecho, muchos procedimientos han sido descubierto o inventados para teor´ıas de fondo tales como varias teor´ıas aritm´eticas, ciertas teor´ıas de vectores, teor´ıas de listas, tuplas, registros y vectores de bits (muy comunes y necesarias en lenguajes de programaci´on como C). La satisfacibilidad de f´ormulas bajo una teor´ıa de fondo se denomina satisfacibilidad modulo teor´ıas (Satisfiability Modulo Theories - 1 8 2.1. Sistemas de reescritura de t´erminos →R/E es confluente si cuando t→∗ R/E t0yt→∗ R/E t00, existe un t´ermino t000 tal que t0→∗ R/E t000 yt00 →∗ R/E t000. Una teor´ıa de reescritura de tipos ordenados (Σ, E, R) es confluente (resp. terminante) si la relaci´on →R/E es confluente (resp. terminante). En una teor´ıa de reescritura de tipos ordenados que sea confluente, terminante y decreciente en tipo, para cada t´ermino t∈ TΣ(X), existe una ´unica forma R/E-irreducible t0(modulo E-equivalencia) obtenida de tpor reescritura hasta la forma canonica, la cual se denota como t→! R/E t0, ot↓R/E cuando t0es irrelevante. La relaci´on →R,E sobre TΣ(X) se define de la siguiente forma: t→p,R,E t0 (o simplemente t→R,E t0) si y s´olo si existe una posici´on p∈PosΣ(t), una regla l→ren Ry una sustituci´on σtal que t|p=Elσ yt0=t[rσ]p. N´otese que si la relaci´on de E-emparejamiento es decidible, la relaci´on →R,E es decidible. Las nociones de confluencia, terminaci´on y t´erminos y sustituciones irreducibles se adaptan trivialmente para la relaci´on →R,E. Si el conjunto de reglas Res confluente, terminante y decreciente en tipo, la relaci´on →! R,E es decidible, ya que →R,E⊆→R/E. La relaci´on →R/E es indecidible en general ya que las clases de E-congruencia pueden ser arbitrariamente extensas. Por lo tanto, la relaci´on de reescritura →R/E se implementa normalmente a trav´es de la relaci´on →R,E (ver [6]). Se asumen las siguientes propiedades sobre RyE: 1. Ees regular y decreciente en tipo; adem´as, para cada ecuaci´on t=t0 en E, todas las variables de Var(t) tienen un tipo m´aximo. 2. Etiene un algoritmo finitario y completo de unificaci´on. 3. Las reglas Rson confluentes, terminantes y decrecientes en tipo modulo E. 4. →R,E es localmente E-coherente (ver [6]), es decir, para todos los t´erminos t1, t2, t3tenemos que t1→R,E t2yt1=Et3implica existe t4, t5tal que t2→∗ R,E t4,t3→+ R,E t5, y t4=Et5. Dada una teor´ıa ecuacional para tipos ordenados (Σ, G), decimos que (Σ, E, R) es una descomposici´on de (Σ, G) si G=R∪Ey (Σ, E, R) es una teor´ıa de reescritura para tipos ordenados que satisfaga las propiedades (1)–(4) indicadas m´as arriba. 2. Conceptos b´asicos 9 Dada una teor´ıa de reescritura para tipos ordenados (Σ, E, R), un t´ermino ty un conjunto Wde variables tales que Var(t)⊆W, la relaci´on de R, Eestrechamiento (R, E-narrowing) sobre TΣ(X) se define como t p,σ,R,E t0 (´o σ,R,E si pse sobreentiende, σsi R, E se sobreentiende, y si σse sobreentiende) si existe una posici´on no variable p∈PosΣ(t), una regla l→r∈Rapropiadamente renombrada tal que (Var(l)∪Var(r)) ∩W=∅, y un unificador σ∈CSU W0 E(t|p=l) para el conjunto de variables W0=W∪ Var(l), tal que t0= (t[r]p)σ. Por conveniencia, en cada paso de estrechamiento t σt0s´olo se espeficica la parte de la sustituci´on σque liga variables del t´ermino t. El cierre transitivo (resp. transitive y reflexivo) de la relaci´on se denota como +(resp. ∗). Escribiremos t k σt0si existen t´erminos u1, . . . , uk−1y sustituciones ρ1, . . . , ρktales que t ρ1u1· · · uk−1 ρkt0,k≥0 yσ=ρ1· · · ρk. 2.2. Maude El lenguaje de programaci´on Maude utiliza reglas de reescritura, como los lenguajes denominados funcionales tales como Haskell,ML,Scheme, o Lisp. En concreto, el lenguaje Maude est´a basado en la l´ogica de reescritura que permite definir multitud de modelos computacionales complejos tales como programaci´on concurrente o programaci´on orientada a objetos. Por ejemplo, Maude permite especificar objetos directamente en el lenguaje, siguiendo una aproximaci´on declarativa a la programaci´on orientada a objetos que no est´a disponible ni en lenguajes imperativos como C++oJava ni en lenguajes declarativos como Haskell. El desarrollo del lenguaje Maude parte de una iniciativa internacional cuyo objetivo consiste en dise˜nar una plataforma com´un para la investigaci´on, docencia y aplicaci´on de los lenguajes declarativos. Se puede encontrar m´as informaci´on en: http://maude.cs.uiuc.edu A continuaci´on se resumen las principales car´acter´ısticas del lenguaje Maude. Sin embargo, hay un extenso manual y un ”primer”(libro de introducci´on muy sencillo y basado en ejemplos) en la direcci´on web indicada antes. Existe tambi´en un libro sobre Maude, con ejemplares adquiridos por la Biblioteca General y la ETSInf, y accesible online en : 10 2.2. Maude http://www.springerlink.com/content/p6h32301712p 2.2.1. Un programa en Maude Un programa Maude esta compuesto por diferentes m´odulos. Cada m´odulo se define entre las palabras reservadas mod yendm, si es un m´odulo de sistema, o entre fmod yendfm, si es un m´odulo funcional. Cada m´odulo incluye declaraciones de tipos y s´ımbolos, junto con las reglas, encabezadas por rl, que describen la l´ogica de algunos de los s´ımbolos, llamadas funciones. B´asicamente, los s´ımbolos y reglas definidos en un m´odulo de sistema tienen un comportamiento indeterminista y ejecuciones posiblemente infinitas en el tiempo (es decir, que no terminen nunca); mientras que los s´ımbolos y reglas definidos en un m´odulo funcional, encabezadas por eq ya que se denominan ecuaciones en este caso, tienen un comportamiento determinista y siempre terminan su ejecuci´on. Es decir, un m´odulo de sistema permite reglas indeterministas y no terminantes, ya que modela un sistema de estados (o aut´omata) y, claramente, pueden haber ciclos y varias posibles acciones a tomar para cada estado del sistema. Sin embargo, un m´odulo funcional s´olo permite ecuaciones (es decir, reglas deterministas y terminantes), ya que representa un programa funcional y todo programa termina y debe devolver siempre el mismo valor. Por ejemplo, el siguiente m´odulo de sistema simula una m´aquina de caf´e y galletas: mod VENDING - MACHINE is sorts Coin Coffee Cookie Item State . subsorts Coffee Cookie < Item . subsorts Coin Item < State . op null : -> State . op __ : State State -> State [ assoc comm id: null ] . op $ : -> Coin . op q : -> Coin . op a : -> Cookie . op c : -> Coffee . var St : State . rl St => St q . --- Modela que se ha anyadido un cuarto de dolar rl St => St $ . --- Modela que se ha anyadido un dolar rl $ => c . --- Modela que se ha trabado el dolar --- y ha devuelto un cafe rl $ => aq . --- Devuelve una galleta y un cuarto de dolar eq q q q q = $. --- Cambia cuatro cuartos de dolar por un dolar endm 2. Conceptos b´asicos 11 Este sistema es indeterminista (p.ej. para un d´olar ”$”hay dos posibles acciones) y no terminante (siempre se puede a˜nadir m´as dinero a la m´aquina). Adem´as el m´odulo incluye una ecuaci´on para el cambio de cuatro cuartos de d´olar por un d´olar de manera transparente, es decir sin que haya una transici´on entre dos estados. Sin embargo, podemos especificar el siguiente m´odulo que simula la funci´on factorial: fmod FACT is protecting INT . op _! : Int -> Int . var N : Int . eq 0 ! = 1 . --- factorial de N=0 es 1 eq N ! = (N - 1)! * N [ owise ] . --- factorial de N >0 es N* factorial de N -1 endfm Este sistema es determinista y termina para cada posible ejecuci´on. N´otese que cada l´ınea de texto se termina con un espacio y un punto. En un m´odulo de sistema podremos incluir reglas y ecuaciones, pero en un m´odulo funcional s´olo pueden aparecer ecuaciones. 2.2.2. Tipos de datos predefinidos Maude dispone de varios tipos de datos predefinidos incluidos en el fichero prelude.maude de la instalaci´on. En concreto, se dispone del tipo Bool definido en el m´odulo BOOL, el tipo Nat definido en el m´odulo NAT, el tipo Int en el m´odulo INT, el tipo Float en el m´odulo FLOAT, y los tipo Char y Stirng en el m´odulo STRING. Para hacer uso de alguno de esos tipos, sus operadores, deberemos importar el m´odulo donde se encuentran con una de las palabras reservadas including,protecting oextending. Por ejemplo, el m´odulo FACT para factorial mostrado anteriormente importa el m´odulo INT de los n´umeros enteros. 2.2.3. Declaraci´on obligatoria de variables Es obligatorio declarar el tipo de las variables antes de ser usadas en el programa, p.ej. la siguiente declaraci´on de variables 12 2.2. Maude var N : Nat . var NL : NatList . var NS : NatSet . o a˜nadirles el tipo directamente a las variables cuando vamos a usarlas, p.ej. ”X:Nat + Y:Nat”. 2.2.4. Declaraciones de Tipos (Sorts), S´ımbolos Constructores y Variables Una declaraci´on de tipo tiene la forma sort T . e introduce un nuevo tipo de datos T. Si se desea introducir varios tipos a la vez, se escribe sorts T1... Tn->T . Despu´es se define los constructores que formar´an los datos asociados a ese tipo de la forma op C : T1T2... Tn->T . donde T1,T2, ..., Tnson los tipos de los par´ametros de ese s´ımbolo. Tambi´en se puede escribir ops C1... Cn:T1T2... Tn->T . y denota que todos los s´ımbolos C1, ..., Cntienen el mismo tipo. Por ejemplo, las declaraciones de tipo: sort Bool . ops true false : -> Bool . sort NatList . op nil : -> NatList . op _:_ : Nat NatList -> NatList .. introducen el tipo Bool con dos constantes true yfalse, y el tipo Natlist 2. Conceptos b´asicos 13 (listas cuyos elementos son naturales, es decir, de tipo Nat). Hay que tener en cuenta que Maude no soporta tipos de datos param´etricos, como Haskell, por lo tanto no se puden definir listas param´etricas sino espec´ıficas para cada tipo, como en el caso de NatList. Sin embargo, es interesante fijarse en la forma de definir el operador binario infijo de construcci´on de una lista, ”:”, donde se indica que el primer argumento debe aparecer antes de los dos puntos mientras que el segundo detr´as de los dos puntos. Una lista de enteros se podr´a definir por lo tanto en notaci´on infija como 0 : (1 : (2 : nil)) en vez de la notaci´on prefija :(0,:(1,:(2,nil))) simplemente indicando que el s´ımbolo a utilizar es ” :”. Esto es muy pr´actico y vers´atil ya que simplemente se debe indicar con un ” ”d´onde va a aparecer el argumento, p.ej., se pueden definir s´ımbolos tan vers´atiles como op if_then_else_fi : Bool Exp Exp -> Exp op for(_;_;_) {_} : Nat Bool Bool Exp -> Exp En concreto en el ejemplo VENDING MACHINE tenemos un s´ımbolo op : State State ->State que denota que el car´acter ”vac´ıo” es un s´ımbolo v´alido para concatenar estados. Y en el ejemplo FACT tenemos op ! : Int ->Int . que denota el s´ımbolo factorial en notaci´on postfija. 2.2.5. Tipos de datos ordenados y sobrecarga de operadores En Maude se pueden crear tipos de datos ordenados o divididos en jerarqu´ıas. Por ejemplo, podemos indicar que los n´umeros naturales se dividen en n´umeros naturales positivos y el cero usando la palabra reservada subsort de la siguiente forma sorts Nat Zero NzNat . subsort Zero < Nat . subsort NzNat < Nat . op 0 : -> Zero . op s : Nat -> NzNat . 14 2.2. Maude De esta forma, la expresi´on s(0) es de tipo NzNat y a la vez es de tipo Nat, mientras que no es de tipo Zero. E igualmente, la expresi´on 0es de tipo Zero yNat, pero no es de tipo NzNat. Otra caracter´ıstica interesante del sistema de tipos de Maude es la sobrecarga de operadores. Por ejemplo, se puede reutilizar el s´ımbolo 0en el tipo de datos Binary sin ning´un problema sorts Nat Zero NzNat . subsort Zero < Nat . subsort NzNat < Nat . op 0 : -> Zero . op s : Nat -> NzNat . sort Binary . op 0 : -> Binary . op 1 : -> Binary . En este caso, pueden surgir ambig¨uedades sobre alg´un t´ermino que se resuelven especificando el tipo detr´as del t´ermino, por ejemplo (0).Zero ´o (0).Binary. El sistema informar´a s´olo de ambig¨uedades que no pueda resolver por su cuenta. La uni´on de la sobrecarga de s´ımbolos y los tipos ordenados le confiere una gran flexibilidad al lenguaje. Por ejemplo, se puede redefinir el anterior tipo de datos de lista de n´umeros naturales de la siguiente forma, donde ENatList denota lista vac´ıa (es decir nil) y NeNatList denota lista no vac´ıa de elementos sorts NatList ENatList NeNatList . subsort ENatList < NatList . op nil : -> ENatList . subsort NeNatList < NatList . op _:_ : Nat NeNatList -> NeNatList . op _:_ : Nat ENatList -> NeNatList . 2.2.6. Propiedades avanzadas (o algebr´aicas) de los s´ımbolos El lenguaje Maude incorpora la posibilidad de especificar s´ımbolos con propiedades algebraicas extra como asociatividad, conmutatividad, elemento neutro, etc. que facilitan mucho la creaci´on de programas. Por ejemplo, se 2. Conceptos b´asicos 15 puede redefinir el tipo de datos lista de n´umeros naturales de la siguiente forma sorts NatList ENatList NeNatList . subsort ENatList < NatList . op nil : -> ENatList . subsort Nat < NeNatList < NatList . op _: _ : NatList NatList -> NeNatList [ assoc ] . donde :es un s´ımbolo asociativo, es decir, no son necesarios los par´entesis para separar los t´erminos. N´otese que los dos argumentos del s´ımbolo : tienen que ser del mismo tipo para poder indicar que el s´ımbolo es asociativo. Ahora Maude entiende que las siguiente expresiones significan exactamente lo mismo s(0) : s(s (0) ) : nil s(0) : (s(s (0)) : nil ) (s (0) : s(s(0) )) : nil Otra posibilidad es a˜nadir un elemento neutro al operador asociativo: sorts NatList . subsort Nat < NatList . op nil : -> NatList . op _: _ : NatList NatList -> NatList [ assoc id : nil ] . donde en este momento :es un s´ımbolo asociativo y el t´ermino nil es el elemento neutro del tipo de datos, que por lo tanto se puede eliminar salvo cuando aparece s´olo. Ahora Maude entiende que las siguiente expresiones significan exactamente lo mismo s(0) : s(s (0) ) : nil s(0) : s(s (0) ) nil : s (0) : nil : s(s (0) ) : nil Tambi´en se puede a˜nadir la propiedad de conmutatividad a la lista, creando el tipo de datos multiconjunto sorts NatMultiSet . subsort Nat < NatMultiSet . op nil : -> NatMultiSet . op _:_ : NatMultiSet NatMultiSet -> NatMultiSet [assoc comm id: nil ] . 16 2.2. Maude donde la propiedad de conmutatividad indica que se puede intercambiar el orden de los elementos. Ahora Maude entiende que las siguientes expresiones significan exactamente lo mismo 0 : s(0) : s(s (0) ) : s(0) 0 : s(0) : s(0) : s(s (0) ) : nil s(0) : 0 : s(s (0) ) : s(0) : nil nil : s (0) : nil : s(s (0) ) : nil : s (0) : nil : 0 : nil Finalmente, se puede a˜nadir la propiedad que no pueden haber elementos repetidos, convirtiendo el multiconjunto en un conjunto sorts NatSet . subsort Nat < NatSet . op nil : -> NatSet . op _:_ : NatSet NatSet -> NatSet [ assoc comm id : nil ] . eq X: Nat : X: Nat = X:Nat . donde la ecuaci´on, encabezada por la palabra eq, elimina aquellas ocurrencias repetidas de un t´ermino. Ahora Maude entiende que las siguiente expresiones significan exactamente lo mismo 0 : s(0) : s(s (0) ) 0 : s(0) : s(0) : s (0) : s (0) : s(s (0) ) : nil s(0) : 0 : s(s (0) ) : s(0) : nil nil : s (0) : nil : s(s (0) ) : nil : s (0) : nil : 0 : nil 2.2.7. Declaraci´on de Funciones Aquellos operadores o s´ımbolos que dispongan de reglas o ecuaciones que los definan son denominados funciones mientras que los que no dispongan de reglas o ecuaciones son denominados constructores. Las reglas de una funci´on se definen con el operador reservado ”rl => .” y las ecuaciones con el operador reservado ”eq = .”. N´otese que es obligatorio en Maude declarar el tipo de todas las funciones, tipo de todas las variables, etc. En otros lenguajes funcionales, como Haskell, esto no es necesario aunque se recomienda. En particular, esto puede ayudar a detectar f´acilmente errores en el programa, cuando se definen funciones que no se ajustan al tipo declarado. Respecto a las reglas/ecuaciones que definen las funciones, ´estas pueden ser de la forma 2. Conceptos b´asicos 17 rl f(t1, ..., tn=>e . eq f(t1, ..., tn= e . donde t1, ..., tnyeson t´erminos. Las ecuaciones pueden etiquetarse con la palabra reservada owise (otherwise) y en ese caso se indica que s´olo se aplicar´a si ninguna otra ecuaci´on para s´ımbolo es aplicable. La palabra owise s´olo se puede aplicar a una ecuaci´on, nunca a una regla ya que tienen un significado indeterminista. Por ejemplo, se puede dar el siguiente m´odulo funcional fmod FACT is protecting INT . op _! : Int -> Int . var N : Int . eq 0 ! = 1 . eq N ! = (N - 1)! * N [ owise ] . endfm Las funciones se pueden definir tambi´en mediante reglas/ecuaciones condicionales crl f(t1, ..., tn=>e if c . ceq f(t1, ..., tn= e if c . donde la condici´on ces un conjunto de emparejamientos de la forma t := t’ separados por el operador /\. Un emparejamiento t := t’ indica que el t´ermino t’ debe tener la forma del t´ermino t, instanciando las variables de tsi es necesario, ya que las variables de tpueden ser usadas en la expresi´on ede la regla para extraer informaci´on de t’. Las ecuaciones condicionales s´olo pueden aplicarse, si la condici´on tiene ´exito. Tambi´en es posible definir una ecuaci´on condicional en la que las guardas sean expresiones de tipo Bool en vez de t := t’; en ese caso se interpretan como true := t. Por ejemplo, podemos escribir la anterior funci´on factorial de la siguiente forma ceq N ! = 1 if N == 0 . ceq N ! = (N - 1)! * N if N =/= 0 . donde la igualdad ’==’ se eval´ua a true si ambas expresiones son iguales y ’=/=’ se eval´ua a true si ambas expresiones son distintas. N´otese que en este caso, se puede usar tambi´en el operador condicional if then else fi. eq N ! = if N == 0 then 1 else (N - 1)! * N fi . 24 2.2. Maude fmod VENDING - MACHINE - SIGNATURE is sorts Coin Item State . subsorts Coin Item < State . op __ : State State -> State [ assoc comm ] . op $ : -> Coin [ format (r! o)] . op q : -> Coin [ format (r! o)] . op a : -> Item [ format (b! o)] . op c : -> Item [ format (b! o)] . endfm Por contra la meta-representaci´on del mismo m´odulo ser´ıa fmod ’VENDING - MACHINE - SIGNATURE is nil sorts ’Coin ; ’Item ; ’State . subsort ’Coin < ’State . subsort ’Item < ’State . op ’__ : ’State ’State -> ’ State [assoc comm ] . op ’a : nil -> ’Item [ format ( ’b ! ’o)] . op ’c : nil -> ’Item [ format ( ’b ! ’o)] . op ’$ : nil -> ’Coin [ format ( ’r ! ’o)] . op ’q : nil -> ’Coin [ format ( ’r ! ’o)] . none none endfm El siguiente ejemplo define las reglas del m´odulo anterior y, adem´as asociada etiquetas a las reglas. La representaci´on com´un ser´ıa mod VENDING - MACHINE is including VENDING - MACHINE - SIGNATURE . var M : State . rl [add -q] : M => M q . rl [add -$] : M => M $ . rl [buy -c] : $ => c . rl [buy -a] : $ => a q . rl [ change ] : q q q q => $ . endm La meta-representaci´on ser´ıa mod ’VENDING - MACHINE is including ’ VENDING - MACHINE - SIGNATURE . sorts none . none none none none rl ’M: State => ’__ [’M: State , ’q .Coin ] [ label ( ’add -q )] . rl ’M: State => ’__ [’M: State , ’$ .Coin ] [ label ( ’add -$ )] . rl ’$. Coin => ’c. Item [ label ( ’buy -c )] . rl ’$.Coin => ’__[’a.Item , ’q. Coin ] [label (’buy -a)] . rl ’__[’q.Coin ,’q.Coin ,’q. Coin , ’q. Coin ] 2. Conceptos b´asicos 25 => ’$. Coin [ label ( ’ change )] . endm Ejemplos de cambios de nivel representaci´on Como se ha comentado con anterioridad, existen distintas funciones auxiliares que permiten mover t´erminos, m´odulos, tipos, ´etc. entre los distintos niveles de representaci´on. Su especificaci´on es op upModule : Qid Bool ~> Module [ special (...) ] . op upSorts : Qid Bool ~> SortSet [ special (...) ] . op upSubsortDecls : Qid Bool ~> SubsortDeclSet [ special (...) ] . op upOpDecls : Qid Bool ~> OpDeclSet [ special (...) ] . op upMbs : Qid Bool ~> MembAxSet [ special (...) ] . op upEqs : Qid Bool ~> EquationSet [ special (...) ] . op upRls : Qid Bool ~> RuleSet [ special (...) ] . Como se habr´a podido comprobar, estas funciones son parciales (pueden dar un error) donde: El primer argumento se espera que sea un nombre de un m´odulo. El segundo argumento es Bool, indicando si se est´a interesado en importar adem´as el m´odulo o no. En el siguiente ejemplo se obtiene la meta-representaci´on de las ecuaciones del m´odulo VENDING-MACHINE y se indica en el segundo argumento true para importar el m´odulo. Maude > reduce in META - LEVEL : upEqs ( ’VENDING - MACHINE , true ) . result EquationSet : eq ’_and_ [’true. Bool , ’A: Bool ] = ’A: Bool [ none] . eq ’_and_ [ ’A :Bool , ’A: Bool ] = ’A: Bool [ none ] . eq ’_and_ [ ’A :Bool , ’ _xor_ [ ’B: Bool , ’C: Bool ]] = ’ _xor_ [ ’_and_ [ ’A: Bool , ’B: Bool ], ’ _and_ [ ’A: Bool , ’C: Bool ]] [none ] . eq ’_and_ [ ’false . Bool , ’A: Bool ] = ’ false . Bool [none ] . eq ’_or_ [ ’A:Bool ,’B: Bool ] = ’ _xor_ [ ’_and_ [ ’A: Bool , ’B: Bool ],’ _xor_ [ ’A:Bool , ’B: Bool ]] [none ] . eq ’_xor_ [ ’A :Bool , ’A: Bool ] = ’ false . Bool [ none ] . eq ’_xor_ [ ’false . Bool , ’A: Bool ] = ’A: Bool [ none ] . eq ’not_ [ ’A: Bool ] = ’_xor_ [’true . Bool , ’A:Bool ] [none ] . eq ’_implies_ [ ’A:Bool , ’B: Bool ] = ’not_ [’ _xor_ [’A:Bool , ’_and_ [’A:Bool , ’B: Bool ]]] [ none ] . 26 2.2. Maude A continuaci´on se realiza la misma llamada pero sin importar el m´odulo Maude > reduce in META - LEVEL : upEqs (’VENDING - MACHINE , false ) . result EquationSet : ( none ). EquationSet En el siguiente ejemplo se muestra c´omo meta-representaci´on de las reglas del mismo m´odulo Maude > reduce in META - LEVEL : upRls ( ’VENDING - MACHINE , true ) . result RuleSet : rl ’$. Coin => ’c. Item [ label ( ’buy -c )] . rl ’$.Coin => ’__[ ’q.Coin , ’a. Item ] [ label( ’buy -a)] . rl ’M: State => ’__[ ’$. Coin , ’M: State ] [ label ( ’add -$ )] . rl ’M: State => ’__[ ’q. Coin , ’M: State ] [ label ( ’add -q )] . rl ’__[’q.Coin ,’q.Coin ,’q. Coin , ’q. Coin ] => ’$. Coin [ label ( ’ change ) ] . Finalmente se muestra un ejemplo de navegaci´on de niveles en t´erminos. Si se dispone de la definici´on del m´odulo fmod UP -DOWN - TEST is protecting META - LEVEL . sort Foo . ops a b c d : -> Foo . op f : Foo Foo -> Foo . op error : -> [Foo ] . eq c = d . endfm Si se llama a la funci´on upTerm para mostrar la meta-representaci´on de un t´ermino f(a, f(b,c)). Maude > reduce in UP -DOWN - TEST : upTerm (f(a , f(b, c))) . result GroundTerm : ’f[ ’a.Foo ,’f[’b.Foo , ’d. Foo ]] Si se ejecuta la funci´on downTerm permite navegar de meta-representaci´on a representaci´on Maude > reduce downTerm (’f[’a.Foo , ’f[’b.Foo ,’c.Foo ]] , error ) . result Foo : f(a, f(b, c)) Si se intenta mostrar un met´a-t´ermino que no est´a definido en el m´odulo se genera un error Maude > reduce downTerm (’f[’a.Foo , ’f[’b.Foo ,’e.Foo ]] , error ) . 2. Conceptos b´asicos 27 Advisory : could not find a constant e of sort Foo in meta - module UP - DOWN - TEST . result [ Foo ]: error 2.2.11. Unificaci´on y Estrechamiento en Maude El prototipo que se detallar´a en posteriores secciones utiliza ´ıntegramente meta-representaciones de t´erminos y m´odulos y para realizar ciertas acciones necesita, adem´as de las comentadas anteriormente dos muy importantes son metaNarrowSearch ymetaUnify. La funci´on metaNarrowSearch1es la meta-representaci´on que se usa para realizar an´alisis de alcanzabilidad basados en narrowing. Esta funci´on est´a definido (junto con su infraestructura necesaria) en el m´odulo META-NARROWING-SEARCH y se define de la siguiente forma. op metaNarrowSearch : Module Term Term Substitution Qid Bound Bound -> ResultTripleSet . donde Module es la meta-representaci´on del m´odulo donde est´a definida la teor´ıa. Term es la meta-representaci´on del t´ermino inicial. Term es la meta-representaci´on del t´ermino final. Substitution (si est´a dado, normalmente es none) cualquier sustituci´on computada debe ser una instancia de la pasada por argumentos. Qid meta-representa la b´usqueda adecuada, en n´umero de pasos (normalmente *, es decir, indeterminado). Bound indica el n´umero m´aximo de soluciones que se desean (profundidad del ´arbol de narrowing). Bound indica el n´umero de soluciones computadas (normalmente unbounded). 1http://maude.cs.uiuc.edu/maude2-manual/html/maude-manualch16.html 28 2.2. Maude El tipo de datos ResultTripleSet representa un conjunto formado por El t´ermino resultante calculado. El tipo (sort) del t´ermino. Una lista de sustituciones para cada variable. Por ejemplo result ResultTripleSet : {’s_ ^1[ ’0. Zero ], ’Nat , ’#1: Nat <- ’0. Zero ; ’#2: Nat <- ’0. Zero } | {’s_ ^2[ ’0. Zero ], ’Nat , ’#3: Nat <- ’0. Zero } Para la ejecuci´on de los ejemplos se usar´a el m´odulo del listado 2.2.11. (N´otese que la definici´on del m´odulo est´a envuelva por par´entesis, esto es necesario) 1( mod NARROWING - VENDING - MACHINE is 2sorts Coin Item Marking Money State . 3subsort Coin < Money . 4op __ : Money Money -> Money [ assoc comm ] . 5subsort Money Item < Marking . 6op __ : Marking Marking -> Marking [ assoc comm] . 7op <_> : Marking -> State . 8op $ : -> Coin [ format (r! o)] . 9op q : -> Coin [ format (r! o)] . 10 op a : -> Item [ format (b! o)] . 11 op c : -> Item [ format (b! o)] . 12 13 var M : Marking . 14 rl [buy -c] : < $ > => < c > . 15 rl [buy -c] : < M $ > => < M c > . 16 rl [buy -a] : < $ > => < a q > . 17 rl [buy -a] : < M $ > => < M a q > . 18 rl [ change ]: < q q q q > => < $ > . 19 rl [ change ]: < M q q q q > => < M $ > . 20 endm) Si se quisiera ejecutar la funci´on metaNarrowSearch, un posible comando sobre el anterior m´odulo ser´ıa Maude > ( red in META - NARROWING - SEARCH : metaNarrowSearch ( upModule ( NARROWING - VENDING - MACHINE ) , ’<_ >[ ’M: Money ], 2. Conceptos b´asicos 29 ’<_ >[ ’__ [’a. Item , ’c .Item ]] , none , ’*, 4, unbounded ) .) result ResultTripleSet : { ’<_ >[ ’__ [’a .Item , ’c .Item ]] , ’ State , ’#1: Marking <- ’__[’q.Coin , ’q.Coin , ’q. Coin ]; ’#3: Money <- ’__[’q.Coin , ’q.Coin , ’q.Coin ]; ’#4: Marking <- ’a. Item ; ’#6: Marking <- ’a. Item ; ’M: Money <- ’__[ ’$.Coin , ’__[’q.Coin , ’q. Coin , ’q. Coin ]]} | { ’<_ >[ ’ __ [’a. Item , ’c. Item ]] , ’ State , ’#1: Marking <- ’__[’q.Coin , ’q.Coin , ’q. Coin ]; ’#3: Money <- ’__[’q.Coin , ’q.Coin , ’q.Coin ]; ’#4: Marking <- ’__[’q.Coin , ’q.Coin , ’q. Coin ]; ’#6: Money <- ’__[’q.Coin , ’q.Coin , ’q.Coin ]; ’#7: Marking <- ’a. Item ; ’#9: Marking <- ’a. Item ; ’M: Money <- ’__[ ’q.Coin , ’q.Coin , ’q.Coin , ’q. Coin , ’__[’q.Coin , ’q.Coin , ’q. Coin ]]} La funci´on metaUnify2es la meta-representaci´on de la unificaci´on. Esto es importante por dos razones: Muchas de las aplicaciones de razonamiento formal de unificaci´on requieren acceso a funciones de unificaci´on al metanivel. Por ejemplo, la computaci´on de pares cr´ıticos para determinar si un m´odulo funcional es localmente confluente. Esto se realizar´a correctamente mediante una funci´on que coja la meta-representaci´on de dicho m´odulo funcional como datos, y entonces llame a las funciones de unificaci´on como parte de sus computaciones de pares cr´ıticos. El algoritmo de unificaci´on es dependiente de la teor´ıa, as´ı que a partir de la combinaci´on de cada signatura con unos axiomas generan algoritmos de unificaci´on order-sorted diferentes. Gracias a la funci´on metaUnify, que recibe la meta-representaci´on del m´odulo que se desee, se puede realizar la unificaci´on de forma correcta. La definici´on de la funci´on metaUnify es op metaUnify : Module UnificationProblem Nat Nat ~> UnificationPair ? special (...) ] . donde 2http://maude.cs.uiuc.edu/maude2-manual/html/maude-manualch12.html 30 2.2. Maude Module es la meta-representaci´on del m´odulo donde est´a definida la teor´ıa. UnificationProblem Es una lista de pares de la forma T:Term =? T:Term. Nat Indica el identificador en el que se deben empezar a crear variables fescas (en caso que se necesiten). Nat Se usa para seleccionar el resultado que quiere (empezando desde el 0) El tipo de datos UnificationProblem se define de la siguiente manera donde cada componente es un UnificationPair formado por T:Term =? T:Term. En cuanto al resultado de dicha funci´on (UnificationPair?) est´a formado por una lista de Sustitution, Nat. sorts UnificandPair UnificationProblem . subsort UnificandPair < UnificationProblem . op _=? _ : Term Term -> UnificandPair [ctor prec 71] . op _/\ _ : UnificationProblem UnificationProblem -> UnificationProblem [ctor assoc comm prec 73] . subsort UnificationPair < UnificationPair ? . subsort UnificationTriple < UnificationTriple ? . op {_,_} : Substitution Nat -> UnificationPair [ctor] . op {_,_,_} : Substitution Substitution Nat -> UnificationTriple [ctor ] . op noUnifier : -> UnificationPair ? [ ctor ] . Un ejemplo de uso de metaUnify Maude > reduce in META - LEVEL : metaUnify ( upModule ( ’UNIFICATION -EX1 , false ), ’f[’X:Nat , ’Y: NzNat ] =? ’f[’Z:NzNat , ’U:Nat ] /\ ’V: NzNat =? ’f[’X:Nat , ’U:Nat ], 0, 0) . result UnificationPair : {’U: Nat <- ’#1: NzNat ; ’V: NzNat <- ’f [’ #2: NzNat , ’#1: NzNat ] ; ’X: Nat <- ’#2: NzNat ; ’Y: NzNat <- ’ #1: NzNat ; ’Z: NzNat <- ’ #2: NzNat , 2} 2. Conceptos b´asicos 31 2.3. CVC3 CVC33es un solver (testeador/provador) autom´atico de Teor´ıas M´odulo Satisfacibilidad (SMT Solver). Puede usarse para comprobar la validez (o, dualmente, la satisfacibilidad) de f´ormulas de primer orden en un n´umero grande de teor´ıas l´ogicas y combinaciones de ´estas. CVC3 es el ´ultimo descendiente de una serie de testers SMT originados en la Universidad de Stanford con el sistema SVC. En particular se ha generado a partir del c´odigo base de CVC Lite4(su m´as reciente predecesor, discontinuado en la actualidad). CVC3 trata con una versi´on de l´ogica de primer orden con tipos polim´orficos y tiene una gran variedad de caracter´ısticas como: Algunas teor´ıas base incluidas como aritm´etica lineal racional y entera, arrays, tuplas, tipos de datos inductivos, etc. Soporte para cuantificadores. Interfaz interactiva basada en texto. Una API creada en C y C++ para ser incluida en otros sistemas. Generaci´on de pruebas y modelos. Subtipado de predicados. No tiene l´ımites de uso ya sea para investigaci´on o fines comerciales. A continuaci´on se detallan algunas caracter´ısticas y tipos de CVC3, se puede encontrar m´as informaci´on en la documentaci´on en la web http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html 3http://www.cs.nyu.edu/acsys/cvc3/ 4http://www.cs.nyu.edu/acsys/cvcl/ 32 2.3. CVC3 2.3.1. Ejecutando CVC3 desde l´ınea de comandos Asumiendo que se ha instalado correctamente CVC3 (apartado instalaci´on5del manual) existe un ejecutable denominado cvc3. Este ejecutable lee la entrada (una secuencia de comandos) desde la entrada est´andar y escribe los resultados en la salida est´andar. Los errores y otros mensajes (salidas de depuraci´on) se redirigen a la salida de error est´andar. T´ıpicamente, la entrada de cvc3 se guarda en una archivo y se redirige al ejecutable por ejemplo # Reading from standard input : cvc3 < input - file .cvc # Reading directly from file: cvc3 input -file .cvc N´otese que por razones de eficiencia CVC3 usa b´uffers de entrada, y la entrada no siempre se procesa inmediatamente despu´es de recibir cada comando. De este modo, si se desea escribir los comandos de forma interactiva y recibir los resultados de forma r´apida se debe usar la opci´on +interactiva o tambi´en acortado mediante +int cvc3 +int Si se desea obtener la ayuda de cvc3 se puede usar el comando -h. El front-end de l´ınea de comandos de CVC3 soporta dos lenguajes de entrada: El propio lenguaje de presentaci´on CVC3 cuya sint´axis estaba inicialmente inspirada por los sistemas PVS6(Prototype Verification System) ySAL y es casi id´entico al lenguaje de entrada de CVC yCVC Lite, los predecesores de CVC3. El lenguaje est´andar promovido por la iniciativa SMT-LIB7para benchmarks SMT-LIB. 5http://www.cs.nyu.edu/acsys/cvc3/doc/INSTALL.html 6http://en.wikipedia.org/wiki/Prototype_Verification_System 7http://www.smt-lib.org/ 2. Conceptos b´asicos 33 A continuaci´on se describen otras car´acter´ısticas de CVC3 enfoc´andose en el primero de los lenguajes. 2.3.2. Sistema de tipos de CVC3 El sistema de tipos de CVC3 incluye una serie de tipos incluidos que pueden ser expandidos por otros definidos por el usuario. Este sistema de tipos consiste en tipos valuados, tipos no valuados ysubtipos, todos ellos interpretados como conjuntos. Por conveniencia, algunas veces se identificar´a la interpretaci´on de un tipo con el propio tipo. Los tipos valuados pueden ser tipos at´omicos y tipos estructurados. Los tipos at´omicos son REAL,BITVECTOR(n) para todo n >0, as´ı como los tipos definidos por el usuario (llamados tambi´en tipos no interpretados). Los tipos estructurados, son array,tuple, y record, as´ı como los tipos estilo ML definidos por el usuario (tipos inductivos). Los tipos no valuados consisten en el tipo BOOLEAN y los tipos function. Los subtipos incluyen el subtipo incluido INT oREAL y se detallan seguidamente. Tipo REAL El tipo REAL est´a interpretado como el conjunto de n´umeros racionales. El nombre REAL est´a justificado por el hecho que una f´ormula CVC3 es v´alida en la teor´ıa de n´umeros racionales s´ı y solo s´ı es v´alida en la teor´ıa de n´umeros reales. Tipos Bit Vector Para cada numeral positivo n, el tipo BITVECTOR(n) esta interpretado como el conjunto de todos los vectores de bits de tama˜no n. 40 2.3. CVC3 abstracciones lambda, y declaraciones locales de s´ımbolos. N´otese que estas extensiones se mantienen en el lenguaje de primer orden de CVC3. En particular, las abstracciones lambda est´an restringidas para coger y devolver s´olo t´erminos de tipos valuados. De la misma forma, los cuantificadores pueden s´olo cuantificar variables de tipos valuados. Los s´ımbolos de funciones libres incluyen s´ımbolos constantes y s´ımbolos predicado, respectivamente los s´ımbolos de funci´on nularios y s´ımbolos de funci´on con un tipo de retorno BOOLEAN. Los s´ımbolos libres est´an introducidos con declaraciones globales de la forma f1,...,fm: T; donde m >0, fi son los nombres de los s´ımbolos y Tes su tipo: % integer constants a, b, c: INT ; % real constants x,y,z: REAL; % unary function f1: REAL -> REAL ; % binary function f2: ( REAL , INT ) -> REAL ; % unary function with a tuple argument f3: [INT , REAL] -> BOOLEAN ; % binary predicate p: ( INT , REAL ) -> BOOLEAN ; % Propositional " variables " P,Q; BOOLEAN ; Igual que la declaraci´on de tipos, las declaraciones de s´ımbolos libres tienen un ´ambito global y deben ser ´unicos. En otras palabras, no es posible globalmente declarar un s´ımbolo m´as de una vez. Esto implica otras cosas como que los s´ımbolos no pueden ser sobrecargados con tipos diferentes. Al igual que los tipos, un nuevo s´ımbolo libre puede ser definido como el nombre de un t´ermino del correspondiente tipo. Con s´ımbolos de constante esto es correcto con una declaraci´on de la forma f : T = t; 2. Conceptos b´asicos 41 c: INT ; i: INT = 5 + 3* c; j: REAL = 3/4; t: [ REAL , INT ] = (2/3 , -4); r: [# key: INT , value : REAL #] = (# key := 4, value := (c + 1) /2 #) ; f: BOOLEAN = FORALL (x: INT ): x <= 0 OR x > c ; Una restricci´on sobre constantes del tipo BOOLEAN es que su valor s´olo puede ser una f´ormula cerrada, esto es, sin variables libres. Un t´ermino y su nombre puede ser usados indistintamente en expresiones posteriores. Los t´erminos con nombre son a menudo ´utiles para compartir subt´erminos (t´erminos usados varias veces en diferente lugares) desde su uso pueden hacer la entrada exponencialmente m´as concisa. Los t´erminos con nombre son procesados muy eficientemente por CVC3. Es mucho m´as eficiente asociar un t´ermino complejo con un nombre directamente en lugar de declarar una constante y despu´es comprobar si es igual al mismo t´ermino. En CVC3 uno puede asociar un t´ermino a un s´ımbolo de funci´on de cualquier aridad. Para s´ımbolos de funci´on no constantes se declara de la forma f : (T1,...,Tn) ->T = LAMBDA (x1:T1,...,xn:Tn) : t ; donde tes cualquier t´ermino de tipo Tcon variables libres x1,...,xn. El conector lambda tiene la sem´antica normal y se ajusta a las reglas l´exicas de ´ambito normales: con el t´ermino tla declaraci´on de los s´ımbolos x1,...,xn como variables locales de l tipo respectivo T1,...,Tnocultando cualquier declaraci´on global previa sobre estos s´ımbolos. Cuando hay k tipos consecutivos Ti,...,Ti+k−1en la expresi´on lambda LAMBDA(x1:T1,...,x : Tn) : t son id´enticos, la sintaxis LAMBDA(x1: T1,...,xi,...,xi+k−1:Ti,...,x : Tn) : t tambi´en se permite. % Global declaration of x as a unary function symbol x: REAL -> REAL; % Local declarations of x as a constant symbol 42 2.4. Interfaz CVC3 en Maude f: REAL -> REAL = LAMBDA (x: REAL): 2* x + 3; p: (INT , INT ) -> BOOLEAN = LAMBDA (x,i: INT ): i*x - 1 > 0; g: ( REAL , INT ) -> [REAL , INT ] = LAMBDA (x: REAL , i:INT ): (x + 1, i - 3); Los s´ımbolos de constante y de funci´on pueden tambi´en ser declarados localmente en cualquier lugar con un t´ermino por medio del enlazador let. Una posible definici´on usando let ser´ıa t: REAL = LET g = LAMBDA (x:INT ): x + 1, x1 = 42 , x2 = 2* x1 + 7/2 IN (LET x3 = g(x1) IN x3 + x2) / x1 ; 2.4. Interfaz CVC3 en Maude Para la realizaci´on de esta tesina se ha utilizado una versi´on modificada de Maude (creada por un estudiante de Grigore Rosu) que lleva incluido el SAT-Solver CVC3 en el propio ejecutable (disponible p´ublicamente en 8). Para poder interactuar entre Maude yCVC3 se ha utilizado una interfaz desarrollada por Camilo Rocha9(estudiante de doctorado de la University of Illinois) en la cual se realiza ’deep-embedding’10 de la sintaxis de PLEXIL11 en Maude. Esta interfaz define un peque˜no lenguaje que posteriormente se transforma a lenguaje SMT-LIB y, ´este ´ultimo, se env´ıa al solver. A continuaci´on se detallan los aspectos m´as importantes de esta interfaz. 2.4.1. Tipos de datos Las expresiones de la interfaz pueden ser constantes, variables o t´erminos recursivamente formados a partir de los dos anteriores. Cada constante o 8http://code.google.com/p/sraplx/downloads/list 9http://www.camilorocha.info/ 10http://en.wiktionary.org/wiki/deep_embedding 11http://en.wikipedia.org/wiki/PLEXIL 2. Conceptos b´asicos 43 variable puede ser de tipo booleano o entero. Algunas definiciones de datos se muestran en la siguiente lista: sorts iBool iBoolAtom iBoolCns iBoolVar . sorts iInt iIntAtom iIntCns iIntVar . subsort iBoolCns iBoolVar < iBoolAtom < iBool . subsort iIntCns iIntVar < iIntAtom < iInt . subsorts iBool iInt < iExpr . subsorts iBoolAtom iIntAtom < iExprAtom . subsorts iExprAtom < iExpr . donde se puede observar que el tipo m´as general se denomina iExpr. Adem´as se definen dos tipos generales, ’iBool’ para booleanos e ’iInt’ para enteros. A su vez, hay dos subtipos para cada uno, uno para las constantes booleanas ’iBoolCns’ y para las variables booleanas ’iBoolVar’. Del mismo modo se han definido para el tipo entero, para constantes ’iIntCns’ y para variables ’iIntVar’. Las constantes se definen mediante el operador ’c’ y un Bool (en el caso de ser booleano) y un Int (en caso de ser entero): --- Boolean and integer constants op c : Bool -> iBoolCns [ctor ] . op c : Int -> iIntCns [ctor ] . Por su parte, para representar variables existen dos operadores distintos ’b’ para variables booleanas e ’i’ para enteras. Ambos necesitan un Nat para poder identificar la variable concreta. --- Boolean and integer variables op b : Nat -> iBoolVar [ctor ] . op i : Nat -> iIntVar [ctor ] . Al mismo tiempo se han definido las t´ıpicas operaciones entre tipos de datos booleanos (tanto variables como constantes) tales como la negaci´on ( ), igualdad (===), desigualdad (= // =), disyunci´on (^) y conjunci´on (v) . --- Boolean expressions op ~_ : iBool -> iBool [ prec 41] . ops _^_ _v_ : iBool iBool -> iBool [ assoc comm prec 45] . op _->_ : iBool iBool -> iBool [prec 47] . ops _ ===_ _=//=_ : iBool iBool -> iBool [ comm prec 60] . 44 2.4. Interfaz CVC3 en Maude Del mismo modo, tambi´en se han definido las operaciones comunes para los datos de tipo entero --- Integer expressions op -_ : iInt -> iInt [ prec 31] . ops _+_ _*_ : iInt iInt -> iInt [ assoc comm prec 35] . op _-_ : iInt iInt -> iInt . --- Relational expressions on integers ops _ <=_ _<_ _ >=_ _>_ : iInt iInt -> iBool [ prec 37] . ops _ ===_ _=//=_ : iInt iInt -> iBool [ comm prec 60] . 2.4.2. Modo de uso de la interfaz La funci´on para realizar comprobaciones de satisfacibilidad sobre una expresi´on definida en la interfaz (iBool) es check-sat, del mismo modo existe una funci´on para comprobar si una expresi´on no es satisfacible llamada check-unsat. Ambas funci´on est´an definidas en el m´odulo SMT-INTERFACE. 1--- SMT interface for checking ( un ) satisfiability of PLEXIL ’s Boolean expressions 2fmod SMT - INTERFACE is 3pr SMT - HOOK . 4pr SMT - TRANSLATE . 5 6var iB : iBool . 7--- checks if the given Boolean expression is satisfiable 8op check -sat : iBool -> Bool [ memo ] . 9eq check -sat(iB) 10 = if iB == c(true ) 11 then true 12 else 13 if iB == c( false ) 14 then false 15 else 16 if check - sat ( translate ( iB)) == " sat" 17 then true 18 else false 19 fi 20 fi 21 fi . 22 --- checks if the given Boolean expression is unsatisfiable 23 op check - unsat : iBool -> Bool [ memo ] . 24 eq check - unsat ( iB ) 25 = if iB == c(false ) 26 then true 27 else 28 if iB == c( true) 29 then false 30 else 31 if check - sat ( translate ( iB)) == " unsat" 32 then true 2. Conceptos b´asicos 45 33 else false 34 fi 35 fi 36 fi . 37 endfm La funci´on translate (definida en el m´odulo SMT-TRANSLATE) es la que se encarga de de transformar un t´ermino de tipo iBool en una cadena (String) que sigue la sintaxis SMT-LIB est´andar (en la lista indican las primeras l´ıneas del m´odulo) 1fmod SMT - TRANSLATE is 2pr 3 TUPLE { String , NatSet , NatSet } 3* (sort Tuple {String ,NatSet , NatSet } to Translation ) . 4pr EXPR . 5pr SMT - CONSTANTS . 6pr CONVERSION . 7 8var B : Bool . 9vars iB iB ’ : iBool . 10 vars iE iE ’ : iExpr . 11 vars iI iI ’ : iInt . 12 vars I I’ : Int . 13 vars N N’ : Nat . 14 vars NS NS ’ : NatSet . 15 vars NS2 NS3 : NatSet . 16 vars Str Str ’ : String . 17 vars Str2 Str3 : String . 18 19 --- translates a given Boolean expression into the 20 --- SMTLIB syntax 21 op translate : iBool -> String [memo ] . 22 --- translates a given expression into the SMTLIB syntax 23 --- accumulating the Boolean and integer symbolic variables in it 24 op $trans : iExpr -> Translation [memo ] . 25 ceq translate (iE ) 26 = add -smt - metadata ( Str ’ + Str2 ) 27 if (Str ,NS ,NS ’) := $trans (iE) 28 /\ Str ’ := declare - bool - vars (NS ) + declare -int - vars ( NS ’) 29 /\ Str2 := "( assert " + Str + ") " . Este String resultante se le env´ıa por par´ametros a la funci´on check-sat definida el m´odulo SMT-HOOK que act´ua a modo de enlace (hook) entre la interfaz y el solver. Es decir, es la funci´on que le env´ıa los datos al solver integrado en Maude. Esta funci´on devuelve un String que ´unicamente puede tener dos valores: ’sat’ si la expresi´on es satisfacible. ’unsat’ si la expresi´on no es satisfacibe. 46 2.4. Interfaz CVC3 en Maude 1fmod SMT - HOOK is 2including STRING . 3op check -sat : String -> String 4[ special (id - hook StringOpSymbol ( callSolvers ) 5op -hook stringSymbol (< Strings > : ~> String ))] . 6endfm 2.4.3. Ejemplos de expresiones A continuaci´on se definen algunos ejemplos de expresiones con la sintaxis definida en la interfaz. En el primer ejemplo se comprueba si la expresion 1 + 2 es igual a la expresi´on 4 - 1 red check -sat ( (c (1) + c (2) ) === (c (4) - c(1)) ) . El resultado obtenido es el esperado (true) reduce in METASAT : check -sat (c (1) + c (2) === c (4) - c (1) ) . rewrites : 37 in 1 ms cpu (1 ms real ) (28179 rewrites / second ) result Bool: true Tambi´en se pueden mezclar tipos de datos iBool eiInt, en este caso se verifica si true (del ejemplo anterior) ^ c(false) es false. red check -sat ( (c (1) + c (2) === c(4) - c (1) ) ^ c( false ) ) . El resultado es reduce in METASAT : check -sat (c( false ) ^ (c (1) + c(2) === c(4) - c(1))) . rewrites : 27 in 1 ms cpu (1 ms real ) (23663 rewrites / second ) result Bool: false En el siguiente ejemplo se comprueba si existe una variable x que haga que la siguiente ecuaci´on sea cierta (x * 1 = x * 2) red check -sat ( (i (0) * c (1) ) === (i(0) * c(2)) ) . 2. Conceptos b´asicos 47 El resultado es true ya que existe un ´unico caso cuando x = 0. reduce in METASAT : check -sat (c (1) * i (0) === c (2) * i (0)) . rewrites : 1 in 0ms cpu (0 ms real ) (~ rewrites / second ) result Bool: true Como ´ultimo ejemplo se muestra una expresi´on muy parecida a las que se generar´an usando el prototipo. En este caso se comprueba si existen alg´un valor para las variables X, Y, W, Z y K tal que X= 1 ∧W= 2 ∧X= Y∧Y=W+Z∧Z=K, donde las variables se codifican de la siguiente forma x == i(1), y == i(2), w == i(3), z == i(4) y k == i(5). red check -sat (c( true ) ^ (c (1) === i (1) ) ^ (c (2) === i (3)) ^ (i (1) === i(2)) ^ (i (2) === i (3) + i (4)) ^ (i (4) === i (5)) ) . El resultado obtenido es reduce in METASAT : check -sat (c( true ) ^ ((((i (2) === i (3) + i (4) ) ^ (i (4) === i(5) )) ^ (i (1) === i (2))) ^ (c(2) === i(3))) ^ (c(1) === i (1) )) . rewrites : 150 in 4 ms cpu (4 ms real ) (32930 rewrites /second ) result Bool: true ya que puede darse el caso si X= 1 ∧Y= 1 ∧W= 2 ∧Z=−1∧k=−1. 3 Prototipo - Primera parte Tomando como base la implementaci´on de la interfaz desarrollada por Camilo Rocha (Secci´on 2.4) se ha definido un prototipo en el que, dado un problema de satisfacibilidad como una secuencia de t´erminos (en metanivel) se convierte dicho problema en una expresi´on (iBool, Secci´on 2.4.1) que pueda ser evaluada por el SAT CVC3. El presente prototipo se ha definido en el m´odulo METASAT-INT. Primero procedemos a detallar formalmente la resoluci´on de problemas de satisfacibilidad en Maude. 3.1. Satisfacibilidad de igualdades sobre los n´umeros naturales en Maude En esta tesina, partimos del model est´andar de la teor´ıa de primer orden para los n´umeros naturales, denominada aritm´etica Presburger en honor a Moj˙zesz Presburger, quien la introdujo. La aritm´etica Presburger incluye solamente los n´umeros naturales, la operaci´on de suma (+) y la operaci´on de igualdad entre t´erminos (=). Dicha teor´ıa de primer orden omite la operaci´on de multiplicaci´on, donde la aritm´etica de Peano corresponde a la aritm´etica Presburger junto con la multiplicaci´on y no se disponen de procedimientos de decisi´on para la aritm´etica de Peano mientras que s´ı existen para la aritm´etica Presburger. Normalmente, los procedimientos de decisi´on para la aritm´etica Presburger asumen tambi´en una operaci´on binaria de mayor-que entre dos n´umeros naturales (>), as´ı como los operadores l´ogicos t´ıpicos (conjunci´on 49 56 3.3. Transformaci´on de SATProblem a expresiones iBool 9 10 ceq transT (M: Module , ’s_ [T: Term ], S : Substitution , N:Nat , i: iExpr ) 11 = {S1: Substitution , (B1: iExpr + c(1) ), N1:Nat , i1: iExpr } 12 if { S1 : Substitution , B1 : iExpr , N1 :Nat , i1 : iExpr } 13 := transT (M: Module , T:Term , S: Substitution , N:Nat , i: iExpr ) . 14 15 eq transT (M: Module , F: Qid [ empty ] , S: Substitution , N: Nat , i : iExpr ) 16 = {S: Substitution , c (0) , N:Nat , i: iExpr } . 17 18 ceq transT (M: Module , ’ sd [T1 :Term , T2 : TermList ], S: Substitution , N:Nat , i: iExpr ) 19 = { S2 : Substitution , ( B1 : iExpr - B2 : iExpr ) , N2 :Nat , i2 : iExpr } 20 if { S1 : Substitution , B1 : iExpr , N1 :Nat , i1 : iExpr } 21 := transT (M :Module , T1 :Term , S: Substitution , N:Nat , i: iExpr ) 22 /\ { S2 : Substitution , B2 : iExpr , N2 :Nat , i2 : iExpr } 23 := transT (M: Module , ’sd[ T2: TermList ], S1 : Substitution , N1 :Nat , i1: iExpr ) . 24 25 ceq transT (M: Module , ’_*_[T1:Term , T2: TermList ], S: Substitution , N:Nat , i: iExpr ) 26 = { S2 : Substitution , ( B1 : iExpr * B2 : iExpr ) , N2 :Nat , i2 : iExpr } 27 if { S1 : Substitution , B1 : iExpr , N1 :Nat , i1 : iExpr } 28 := transT (M :Module , T1 :Term , S: Substitution , N:Nat , i: iExpr ) 29 /\ { S2 : Substitution , B2 : iExpr , N2 :Nat , i2 : iExpr } 30 := transT (M: Module , ’_*_[T2 : TermList ], S1: Substitution , N1:Nat , i1: iExpr ) . 31 32 ceq transT (M: Module , ’_= // =_[T1: Term , T2: Term ], S: Substitution , N:Nat , i: iExpr ) 33 = { S2 : Substitution , B1 : iExpr =// = B2 : iExpr , N2 :Nat , i2 : iExpr } 34 if { S1 : Substitution , B1 : iExpr , N1 :Nat , i1 : iExpr } 35 := transT (M :Module , T1 :Term , S: Substitution , N:Nat , i: iExpr ) 36 /\ { S2 : Substitution , B2 : iExpr , N2 :Nat , i2 : iExpr } 37 := transT (M: Module , T2:Term , S1: Substitution , N1:Nat , i1: iExpr ) . 38 39 ceq transT ( M: Module , ’_ == _[ T1 :Term , T2 : Term ] , S: Substitution , N: Nat , i: iExpr ) 40 = { S2 : Substitution , B1 : iExpr === B2 :iExpr , N2 :Nat , i2 : iExpr } 41 if { S1 : Substitution , B1 : iExpr , N1 :Nat , i1 : iExpr } 42 := transT (M :Module , T1 :Term , S: Substitution , N:Nat , i: iExpr ) 43 /\ { S2 : Substitution , B2 : iExpr , N2 :Nat , i2 : iExpr } 44 := transT (M: Module , T2:Term , S1: Substitution , N1:Nat , i1: iExpr ) . 45 46 ceq transT (M: Module , ’_<_[T1:Term , T2: Term ], S: Substitution , N:Nat , i: iExpr ) 47 = { S2 : Substitution , B1 : iExpr < B2 : iExpr , N2 :Nat , i2 : iExpr } 48 if { S1 : Substitution , B1 : iExpr , N1 :Nat , i1 : iExpr } 49 := transT (M :Module , T1 :Term , S: Substitution , N:Nat , i: iExpr ) 50 /\ { S2 : Substitution , B2 : iExpr , N2 :Nat , i2 : iExpr } 51 := transT (M: Module , T2:Term , S1: Substitution , N1:Nat , i1: iExpr ) . 52 53 ceq transT (M: Module , ’_>_[T1:Term , T2: Term ], S: Substitution , N:Nat , i: iExpr ) 54 = { S2 : Substitution , B1 : iExpr > B2 : iExpr , N2 :Nat , i2 : iExpr } 55 if { S1 : Substitution , B1 : iExpr , N1 :Nat , i1 : iExpr } 56 := transT (M :Module , T1 :Term , S: Substitution , N:Nat , i: iExpr ) 57 /\ { S2 : Substitution , B2 : iExpr , N2 :Nat , i2 : iExpr } 58 := transT (M: Module , T2:Term , S1: Substitution , N1:Nat , i1: iExpr ) . 59 60 ceq transT ( M: Module , ’_ <= _[ T1 :Term , T2 : Term ] , S: Substitution , N: Nat , i: iExpr ) 61 = { S2 : Substitution , B1 : iExpr <= B2 : iExpr , N2 :Nat , i2 : iExpr } 62 if { S1 : Substitution , B1 : iExpr , N1 :Nat , i1 : iExpr } 63 := transT (M :Module , T1 :Term , S: Substitution , N:Nat , i: iExpr ) 3. Prototipo - Primera parte 57 64 /\ { S2 : Substitution , B2 : iExpr , N2 :Nat , i2 : iExpr } 65 := transT (M: Module , T2:Term , S1: Substitution , N1:Nat , i1: iExpr ) . 66 67 ceq transT ( M: Module , ’_ >= _[ T1 :Term , T2 : Term ] , S: Substitution , N: Nat , i: iExpr ) 68 = { S2 : Substitution , B1 : iExpr >= B2 : iExpr , N2 :Nat , i2 : iExpr } 69 if { S1 : Substitution , B1 : iExpr , N1 :Nat , i1 : iExpr } 70 := transT (M :Module , T1 :Term , S: Substitution , N:Nat , i: iExpr ) 71 /\ { S2 : Substitution , B2 : iExpr , N2 :Nat , i2 : iExpr } 72 := transT (M: Module , T2:Term , S1: Substitution , N1:Nat , i1: iExpr ) . Cuando el t´ermino que se recibe en la funci´on transT es un booleano o un 0 se sustituye dicho t´ermino por el correspondiente: ’true.Bool por c(true),’false.Bool por c(false) y’0.Zero por c(0) (los otros datos pasados por par´ametros no se alteran). Si el t´ermino no es ninguno de estos se env´ıa a la funci´on transT2. 1eq transT (M: Module , ’true. Bool , S: Substitution , N:Nat , i: iExpr ) 2= {S: Substitution , c( true ), N:Nat , i: iExpr} . 3 4eq transT (M: Module , ’ false . Bool , S : Substitution , N:Nat , i: iExpr ) 5= {S: Substitution , c( false ), N:Nat , i: iExpr } . 6 7eq transT (M: Module , ’ 0. Zero , S: Substitution , N:Nat , i: iExpr ) 8= {S: Substitution , c (0) , N:Nat , i: iExpr } . 9 10 eq transT (M: Module , T:Term , S: Substitution , N:Nat , i: iExpr ) 11 = transT2 (M: Module , T:Term , S: Substitution , N:Nat , i:iExpr ) [ owise ] . La funci´on transT2 se encarga de transformar los t´erminos en caso que sean de tipo variable y exista una substituci´on (en el conjunto de substituciones) para ´esta. En primer lugar se comprueba el tipo de variable: Si es de tipo Bool entonces se a˜nade el t´ermino b(downTerm(T:Term, 0)) donde T:Term es la substituci´on de la variable. Si es de tipo Nat entonces se a˜nade el t´ermino i(downTerm(T:Term, 0)) y, adem´as se comprueba que exista dicha variable en el conjunto de restricciones de variables (para obligar que sean variables positivas, como se ha comentado con anterioridad). 1op transT2 : Module Term Substitution Nat iExpr -> SubstiExprTetra . 2 3ceq transT2 (M:Module , V: Variable , V: Variable <- T: Term ; S: Substitution , N: Nat , i: iExpr ) 4= {V: Variable <- T: Term ; S: Substitution , b( downTerm (T: Term , 0) ), N: Nat , i: iExpr } 58 3.3. Transformaci´on de SATProblem a expresiones iBool 5if sortLeq (M: Module , ’Bool , getType (V: Variable )) == true . 6 7ceq transT2 (M:Module , V: Variable , V: Variable <- T: Term ; S: Substitution , N: Nat , i: iExpr ) 8= {V: Variable <- T: Term ; S: Substitution , i( downTerm (T: Term , 0) ), N: Nat , 9if existVar (i: iExpr , i( downTerm (T: Term , 0) )) == true 10 then i: iExpr 11 else i:iExpr ^ (i(N:Nat) >= c(0) ) fi } 12 if sortLeq (M: Module , ’Nat , getType (V: Variable )) == true . 13 14 eq transT2 (M:Module , T: Term , S: Substitution , N:Nat , i: iExpr ) 15 = transT3 (M: Module , T:Term , S: Substitution , N:Nat , i:iExpr ) [ owise ] . En el caso que no exista una substituci´on sobre la variable entonces se llama a la funci´on transT3 para que siga con la traducci´on. Si no existe una substituci´on sobre una variable significa que dicha variable se est´a convirtiendo por primera vez y, por tanto, a parte de realizar la conversi´on que se produce en la funci´on transT2 se ha de a˜nadir la substituci´on al conjunto de substituciones. En caso que el t´ermino no unifique con ninguna cabecera, se delega su transformaci´on a la funci´on transT4. 1op transT3 : Module Term Substitution Nat iExpr -> SubstiExprTetra . 2 3eq transT3 (M:Module , V: Variable , S: Substitution , N:Nat , i: iExpr ) 4= { V: Variable <- upTerm ( N: Nat ) ; S: Substitution , 5if sortLeq (M: Module , ’Bool , getType (V: Variable )) == true 6then b(N:Nat) 7else i(N:Nat) 8fi , 9N: Nat + 1, 10 if existVar (i: iExpr , i(N: Nat )) == true 11 then i: iExpr 12 else i:iExpr ^ (i(N:Nat ) >= c (0)) fi } . 13 14 eq transT3 (M:Module , T: Term , S: Substitution , N:Nat , i: iExpr ) 15 = transT4 (M: Module , T:Term , S: Substitution , N:Nat , i:iExpr ) [ owise ] . La funci´on transT4 se ejecuta en caso que no se pueda convertir por ninguna funci´on anterior y ´unicamente comprueba que el t´ermino sea de tipo Nat y pone ese n´umero dentro de un constructor de variables (c(X:Nat)). 1eq transT3 (M:Module , T:Term , S: Substitution , N:Nat , i: iExpr ) = transT4 (M: Module , T :Term , S : Substitution , N: Nat , i: iExpr ) [ owise ] . 2 3op transT4 : Module Term Substitution Nat iExpr -> SubstiExprTetra . 4 5ceq transT4 (M:Module , T:Term , S: Substitution , N:Nat , i: iExpr) = {S: Substitution , c (X: Nat ) , N:Nat , i: iExpr } 6if X:Nat := downTerm (T: Term , 0) . 3. Prototipo - Primera parte 59 El motivo de utilizar distintas funciones para transformar (transT,transT2, transT3,transT4) radica en que se desea llevar un orden de transformaci´on ya que si todo el proceso se realizase dentro de una ´unica funci´on podr´ıan darse casos en el que las transformaciones no se realizasen de forma correcta. Finalmente, est´a la funci´on iExprUnion que ´unicamente une la expresi´on generada con el conjunto de restricciones sobre las variables. op iExprUnion : SubstiExprTetra -> iExpr . eq iExprUnion (S: SubstiExprTetra ) = getiExpr (S: SubstiExprTetra ) ^ getVars (S: SubstiExprTetra ) . 3.4. Ejemplos de transformaci´on Todos los ejemplos de esta secci´on utilizan la meta-representaci´on del m´odulo NAT incluido en Maude. A continuaci´on se muestra un ejemplo de conversi´on, supongamos que tenemos el problema ’#6: Nat === ’#0: Nat ^ ’#6: Nat === ’0. Zero ^ ’#7: Nat === ’#0: Nat ^ ’#7: Nat === ’s_ ^1[ ’0. Zero ] Donde cada #Entero:Nat representa una variable entera y las constantes enteras se representan en notaci´on de sucesor. La transformaci´on que realiza la funci´on trans genera la tupla SubstiExprTetra: { ’#0: Nat <- ’s_ ^2[ ’0. Zero ] ; ’#6: Nat <- ’s_[ ’0. Zero ] ; ’#7: Nat <- ’s_ ^3[ ’0. Zero ], c( true ) ^ (c(0) === i(1)) ^ (c (1) === i (3)) ^ (i(1) === i(2)) ^ (i(2) === i (3)) , 4, c( true ) ^ i (1) >= c (0) ^ i (2) >= c (0) ^ i (3) >= c (0) } 60 3.4. Ejemplos de transformaci´on De la cual el conjunto de substituciones es ’#0: Nat <- ’s_ ^2[ ’0. Zero ] ; ’#6: Nat <- ’s_ [’0. Zero ] ; ’#7: Nat <- ’s_ ^3[ ’0. Zero] La expresi´on generada es c( true ) ^ (c(0) === i(1)) ^ (c (1) === i (3)) ^ (i(1) === i(2)) ^ (i(2) === i (3)) El identificador de la pr´oxima variable es 4 Y el conjunto de restricciones sobre variables es c( true ) ^ i (1) >= c (0) ^ i (2) >= c (0) ^ i (3) >= c (0) Para poder ejecutar el anterior ejemplo en el prototipo se deber´ıa realizar de la siguiente forma. red metasat - interface (upModule (’MULT , false ), ’#6: Nat === ’#0: Nat ^ ’#6: Nat === ’0. Zero ^ ’#7: Nat === ’#0: Nat ^ ’#7: Nat === ’s_ ^1[ ’0. Zero ]) . Internamente se convertir´ıa en la siguiente llamada sobre la interfaz de Camilo Rocha check -sat (c( true ) ^ (c(0) === i(1)) ^ (c (1) === i (3) ) ^ (i (1) === i (2)) ^ (i (2) === i (3)) ^ c( true ) ^ i(1) >= c(0) ^ i(2) >= c (0) ^ i (3) >= c (0) ) . El resultado proporcionado por Maude ser´ıa: reduce in METASAT : metasat - interface ( upModule ( ’MULT , false ), ’#6: Nat === ’#0: Nat ^ ’#6: Nat === ’0. Zero ^ ’#7: Nat === ’#0: Nat ^ ’#7: Nat === ’s_ ^1[ ’0. Zero ]) . rewrites : 223 in 3 ms cpu (3 ms real ) (60221 rewrites /second ) result Bool: false Otro ejemplo de una posible conversi´on ser´ıa el siguiente 3. Prototipo - Primera parte 61 ’#5: Nat === ’M:Nat ^ ’#5: Nat === ’s_ ^1[ ’0. Zero] ^ ’#6: Nat === ’0. Zero ^ ’#6: Nat === ’s_ ^2[ ’0. Zero ] Donde la funci´on trans devolver´ıa la tupla { ’#5: Nat <- ’s_[ ’0. Zero ] ; ’#6: Nat <- ’s_ ^3[ ’0. Zero ] ; ’M: Nat <- ’s_ ^2[ ’0. Zero ], c( true ) ^ (c(0) === i(3)) ^ (c (1) === i (1)) ^ (c(2) === i(3)) ^ (i(1) === i (2)) , 4, c( true ) ^ i (1) >= c (0) ^ i (2) >= c (0) ^ i (3) >= c (0) } Y el resultado obtenido por Maude ser´ıa: reduce in METASAT : metasat - interface ( upModule ( ’MULT , false ), ’ #5: Nat === ’M: Nat ^ ’#5: Nat === ’s_ ^1[ ’0. Zero ] ^ ’#6: Nat === ’0. Zero ^ ’#6: Nat === ’s_ ^2[ ’0. Zero ]) . rewrites : 219 in 3 ms cpu (3 ms real ) (59125 rewrites /second ) result Bool: false 4 Prototipo - Segunda parte En esta segunda parte se extiende el procedimiento de decisi´on de la satisfacibilidad de una conjunci´on de igualdades para la aritm´etica Presburger para que admita t´erminos cualesquiera en una teor´ıa ecuacional extendida con m´as propiedades algebraicas pero sin ninguna regla. Para ello se realizar´a un proceso de abstracci´on de variables (sustituyendo las variables contenidas en los pares por nuevas variables frescas) y combinaci´on de variables (utilizando unificaci´on ecuacional) para encontrar unificadores entre las variables. Este prototipo se ha definido en el m´odulo METASAT-TRANS. 4.1. Satisfacibilidad de igualdades para t´erminos cualesquiera En esta secci´on, partimos de la teor´ıa de primer orden para la aritm´etica Presburger N= (N,+N,0N,1N, >N) definida en la Secci´on 3.1 y asumimos una teor´ıa ecuacional (ΣN, EN, RN) para tipos ordenados basada en un tipo especial Nat que es una descomposici´on de la aritm´etica Presburger Ncomo se indica tambi´en en la Secci´on 3.1. Dada una teor´ıa ecuacional para tipos ordenados (Σ, E, R), decimos que es una extensi´on v´alida de la aritm´etica Presburger si cumple las siguientes condiciones: 63 64 4.1. Satisfacibilidad de igualdades para t´erminos cualesquiera 1. se a˜naden m´as s´ımbolos y tipos de datos, es decir, Σ = ΣN]Σ0donde el conjunto de tipos Sasociado a Σ contiene el ´unico tipo Nat permitido en ΣN, 2. se a˜naden m´as propiedades ecuacionales, es decir, E=EN]E0, 3. no existen m´as ecuaciones que las de la aritm´etica Presburger, es decir, R=RN, 4. la teor´ıa ecuacional protege el algebra inicial de los naturales, es decir, para cada Σ-t´ermino tsin variables del tipo Nat, existe un Σ-t´ermino t0sin variables del tipo Nat tal que t↓R,E =ENt0. Dada una teor´ıa ecuacional (Σ, E, R) que sea una extensi´on v´alida de la aritm´etica Presburger (ΣN, EN, RN) y una conjunci´on de igualdades C= {u1=v1∧ · · · ∧ uk=vk}donde los t´erminos u1, v1, . . . , uk, vkson t´erminos con variables de TΣ(X), la conjunci´on Ces satisfacible si y s´olo si existe una sustituci´on σ:XC→ TΣ,XC=Vars(Viui=vi), tal que para cada i, (uiσ)↓R,E =E(viσ)↓R,E. Dada una teor´ıa ecuacional (Σ, E, R) que sea una extensi´on v´alida de la aritm´etica Presburger (ΣN, EN, RN) y un algoritmo de unificaci´on finitario y completo para la teor´ıa ecuacional E0de E=EN]E0, es decidible si una conjunci´on de igualdades C={u1=v1∧ · · · ∧ uk=vk}donde los t´erminos u1, v1, . . . , uk, vkson t´erminos con variables de cualquier tipo de datos es satisfacible. El algoritmo asociado al proceso de satisfacibilidad es muy sencillo gracias a que la teor´ıa extendida protege el algebra inicial de los n´umeros naturales. Es decir, dada una conjunci´on de igualdades C={u1=v1∧ · · · ∧ uk=vk} donde los t´erminos u1, v1, . . . , uk, vkson t´erminos con variables de TΣ(X), se realiza un proceso de abstracci´on con variables, generando dos conjuntos b C={bu1=bv1∧ · · · ∧ buk=bvk}yCN={X1=t1∧ · · · ∧ Xn=tn}donde X1, . . . , Xn∈ XNat son variables frescas que no aparezcan en Cyt1, . . . , tn∈ TΣ(X)Nat, tal que para todo 1 ≤i≤n, existe un ´ındice 1 ≤j≤ky una posici´on pi,j tal que ui|pi,j =tiybui|pi,j =Xi´o vi|pi,j =tiybvi|pi,j =Xi. Una vez generados las conjunciones b CyCN, el proceso de decisi´on es simple gracias a que la teor´ıa protege los naturales, ya que primero resolvemos el conjunto b Cpor unificacion ecuacional y, para cada unificador, invocamos el proceso de decisi´on para los naturales. 4. Prototipo - Segunda parte 65 4.2. Tipos de datos El principal tipo de datos definido en este prototipo es Pair (construido mediante el operador =?= entre dos t´erminos) y representa una pregunta, ¿es el t´ermino 1 igual al t´ermino 2?. Pair es a su vez subtipo de PairSet que define un conjunto de Pair que permite concatenarlos utilizando el operador ^. sort Pair . op _=?=_ : Term Term -> Pair [prec 71] . sort PairSet . subsort Pair < PairSet . op emptyPairSet : -> PairSet . op _^ _ : PairSet PairSet -> PairSet [ assoc comm id : emptyPairSet prec 73] . Para mantener el estado entre llamadas sobre funciones se ha definido el tipo de datos Term&PairSet&Counter, formado por una lista de t´erminos, un conjunto PairSet y el Nat que identifica la pr´oxima variable que se puede generar. Adem´as se han definido distintas operaciones para acceder a cada uno de sus miembros. *** Variable de estado sort Term & PairSet & Counter . op (_ ,_ ,_) : TermList PairSet Nat -> Term & PairSet & Counter . op getTermList : Term & PairSet & Counter -> TermList . op getPairSet : Term & PairSet & Counter -> PairSet . op getCounter : Term & PairSet & Counter -> Nat . eq getTermList (T: TermList , P:PairSet , N:Nat) = T: TermList . eq getPairSet (T:TermList , P: PairSet , N: Nat ) = P: PairSet . eq getCounter (T:TermList , P: PairSet , N: Nat ) = N: Nat . Se ha definido otro tipo denominado PairSet&PairSet&Counter usado para (al igual que el tipo de datos Term&PairSet&Counter) mantener el estado cuando se generan secuencias de PairSet. Los datos que forman cada t´ermino PairSet&PairSet&Counter son, un t´ermino PairSet con la transformaci´on del t´ermino, otro t´ermino PairSet que contiene la lista de restricciones de las variables y, por ´ultimo, un Nat que identifica la pr´oxima variable a generar. Otro tipo generado es el denominado PairSet&PairSet&Counter&Substitution 72 4.3. Proceso de conversi´on rewrites : 46 in 0 ms cpu (0 ms real ) (235897 rewrites / second ) result PairSet & PairSet & Counter : ( ’#0: Nat =?= ’#1: Nat ^ ’ #2: Nat =?= ’#3: Nat , ’#0: Nat =?= ’_+_[ ’Z:Nat , ’W:Nat ] ^ ’#1: Nat =?= ’_+_[ ’s_ ^3[ ’0. Zero ], ’s_ ^2[ ’0. Zero ]] ^ ’#2: Nat =?= ’_+_[ ’s_[ ’0. Zero ], ’X: Nat] ^ ’#3: Nat =?= ’Y:Nat ,4) Donde el resultado reescrito ser´ıa ’#0: Nat =?= ’#1: Nat ^ ’#2: Nat =?= ’#3: Nat Y el conjunto de restricciones ’#0: Nat =?= ’_+_[’Z:Nat ,’W:Nat] ^ ’#1: Nat =?= ’_+_[ ’s_ ^3[ ’0. Zero ],’s_ ^2[ ’0. Zero ]] ^ ’#2: Nat =?= ’_+_[’s_ [’0. Zero ], ’X:Nat ] ^ ’#3: Nat =?= ’Y:Nat 4.3.2. Combinaci´on de variables El proceso de combinaci´on de variables intenta encontrar una lista sustituciones entre las variables tal que al aplicar dichas sustituciones el PairSet sea cierto y se cumplan todas las restricciones (al enviarlo como SATProblem a la primera parte del prototipo, Secci´on 3). Estas sustituciones se calculan utilizando la funci´on metaUnify (Secci´on 2.2.11). Este proceso se divide en dos partes: Transformar los PairSet en UnificationProblem para que metaUnify pueda tratarlos. Llamar a la funci´on metaUnify y realizar las sustituciones resultantes sobre las restricciones. Para realizar la transformaci´on de PairSet aUnificationProblem se utiliza la funci´on transformU (listado 4.5) en la que se sustituye en cada Pair el operador =?= por =?. Listing 4.5: Funci´on transformU 4. Prototipo - Segunda parte 73 1op transformU : Module PairSet -> UnificationProblem . 2eq transformU (M: Module , T1: Term =?= T2: Term ^ PS: PairSet ) = 3if PS : PairSet == emptyPairSet 4then T1: Term =? T2: Term 5else T1 :Term =? T2: Term /\ transformU (M:Module , PS: PairSet ) 6fi . Posteriormente se realiza la llamada a metaUnify mediante la funci´on callUnification (listado 4.6) Listing 4.6: Funci´on callUnification 1***( Llamada a meta unificacion 2Nat -> Indice de variables 3Nat -> Unificacion 4) 5op callUnification : Module UnificationProblem Nat Nat -> UnificationPair . 6eq callUnification (M:Module , U: UnificationProblem , N:Nat , N2: Nat ) 7= metaUnify (M: Module , U: UnificationProblem , N:Nat , N2 :Nat ) . La llamada que se realiza internamente en el prototipo es la siguiente callUnification (M: Module , transformU (M: Module , getFirstPair (P: PairSet & PairSet & Counter )) , getCounter (P: PairSet & PairSet & Counter ) , N: Nat ) . Donde en primer lugar se obtiene el primer PairSet de un t´ermino de tipo PairSet&PairSet&Counter y, sobre ´este se realiza la conversi´on a UnificationProblem. El contador getCounter sirve para indicarle a la funci´on metaUnify a partir de qu´e identificador debe crear variables frescas. El ´ultimo dato N:Nat sirve para indicar que sustituci´on se desea obtener (la 0, la 1, etc.). La funci´on callUnification devuelve un conjunto de UnificationPair en caso que haya encontrado sustituciones o noUnifier en caso que no haya encontrado ninguna substituci´on. Seguidamente se presentar´an algunos ejemplos. Ejemplos En esta secci´on se partir´a de los ejemplos vistos en la Secci´on 4.3.1 y se observar´a c´omo se convierten y qu´e resultados se obtienen. Se ha definido un m´odulo para la realizaci´on de los ejemplos denominada ACNAT (listado 4.7). 74 4.3. Proceso de conversi´on Listing 4.7: M´odulo ACNAT 1mod ACNAT is 2pr NAT . 3sorts S Nat2 . 4subsort Nat < Nat2 < S . 5op _;_ : S S -> S [assoc comm prec 75] . 6endm El primer ejemplo es ’s_[’0. Zero ] =?= ’s_ ^2[ ’0. Zero ] En el que el resultado al aplicar la abstracci´on de variables es ’#0: Nat =?= ’#1: Nat Al llamar a la funci´on callUnification mediante el comando red callUnification ( upModule (’ACNAT , false ) , transformU ( upModule ( ’ACNAT , false ), ’#0: Nat =?= ’#1: Nat ), 2, 0) . Devuelve el UnificationPair resultante reduce in METASAT : callUnification ( upModule (’ACNAT , false ) , transformU ( upModule (’ACNAT , false ), ’#0: Nat =?= ’#1: Nat) , 2, 0) . rewrites : 6 in 1 ms cpu (3 ms real ) (4373 rewrites / second ) result UnificationPair : { ’#0: Nat <- ’#3: Nat ; ’#1: Nat <- ’#3: Nat ,3} Si repetimos el comando con el mismo ejemplo para obtener la siguiente sustituci´on red callUnification ( upModule (’ACNAT , false ) , transformU ( upModule ( ’ACNAT , false ), ’#0: Nat =?= ’#1: Nat ), 2, 1) . Obtenemos que no existen m´as unificadores reduce in METASAT : callUnification ( upModule (’ACNAT , false ) , transformU ( upModule (’ACNAT , false ), ’#0: Nat =?= ’#1: Nat) , 2, 1) . rewrites : 6 in 0ms cpu (0 ms real ) (~ rewrites / second ) result UnificationPair ?: ( noUnifier ). UnificationPair ? 4. Prototipo - Segunda parte 75 Si utilizamos como ejemplo ’_+_[ ’s_[ ’0. Zero ], ’X:Nat ] =?= ’Y: Nat ^ ’_+_[ ’Z:Nat , ’W:Nat ] =?= ’_+_[ ’s_ ^3[ ’0. Zero ], ’s_ ^2[ ’0. Zero ]] En el que el resultado era ’#0: Nat =?= ’#1: Nat ^ ’#2: Nat =?= ’#3: Nat Si utilizamos el comando anterior red callUnification ( upModule (’ACNAT , false ) , transformU ( upModule (’ACNAT , false ) , ’#0: Nat =?= ’#1: Nat ^ ’#2: Nat =?= ’#3: Nat), 4, 0) . Obtenemos la sustituci´on reduce in METASAT : callUnification ( upModule (’ACNAT , false ) , transformU ( upModule (’ACNAT , false ), ’#0: Nat =?= ’#1: Nat ^ ’#2: Nat =?= ’#3: Nat) , 4, 0) . rewrites : 9 in 0 ms cpu (0 ms real ) (47872 rewrites / second ) result UnificationPair : { ’#0: Nat <- ’#5: Nat ; ’#1: Nat <- ’#5: Nat ; ’#2: Nat <- ’#6: Nat ; ’#3: Nat <- ’#6: Nat ,6} 4.3.3. Conversi´on de PairSet aSATProblem La finalidad de este proceso es, a partir del resultado de la Secci´on 4.3.2, sustituir cada UnificationPair sobre el t´ermino que corresponda del conjunto de restricciones y crear una petici´on SATProblem para enviar a la primera parte del prototipo (Secci´on 3). La sustituci´on de t´erminos se realiza mediante las funciones substitutePairs (listado 4.8) y substitutePair (listado 4.9) cuya ejecuci´on es muy simple pues ´unicamente sustituye cada t´ermino de cada Pair por la sustituci´on indicada. Listing 4.8: Funci´on substitutePairs 76 4.3. Proceso de conversi´on 1*** Substitution PairSet 2op substitutePairs : PairSet Substitution -> PairSet . 3eq substitutePairs (P: PairSet , none ) = P: PairSet . 4eq substitutePairs (P: PairSet , S: Substitution ; S2: Substitution ) 5= substitutePairs ( substitutePair (P: PairSet , S: Substitution ) , S2: Substitution) . Listing 4.9: Funci´on substitutePair 1op substitutePair : PairSet Substitution -> PairSet . 2eq substitutePair ( emptyPairSet , S: Substitution ) = emptyPairSet . 3ceq substitutePair (T1 :Term =?= T2 :Term ^ P: PairSet , S: Substitution ) = T1 ’: Term =?= T2 ’: Term ^ P ’: PairSet 4if T1 ’: Term := T1 :Term << S: Substitution 5/\ T2 ’: Term := T2 :Term << S: Substitution 6/\ P’: PairSet := substitutePair (P: PairSet , S: Substitution ) . La conversi´on de PairSet aSATProblem tambi´en es muy sencilla pues ´unicamente se sustituye el operador de construcci´on de Pair (=?=) por el operador de construcci´on de SATPair (===). Esta conversi´on la realiza la funci´on createSATRequest que se puede observar en el listado 4.10. Listing 4.10: Funci´on createSATRequest 1*** createSATRequest 2*** PairSet -> Pares variable =?= valor 3op createSATRequest : PairSet -> SATProblem . 4eq createSATRequest ( emptyPairSet ) = empty . 5eq createSATRequest (T1 : Term =?= T2: Term ^ P: PairSet ) = T1 : Term === T2 : Term ^ createSATRequest (P: PairSet ) . Finalmente la llamada concreta para crear una petici´on SATProblem ser´ıa red createSATRequest ( substitutePairs (P: PairSet , getSubst (U: UnificationPair )) . Donde P:PairSet es el conjunto de restricci´on y getSubst(U:UnificationPair) es la lista de sustituciones obtenida mediante la funci´on callUnification. Al igual que las secciones anteriores, a continuaci´on se presentan unos ejemplos. 4. Prototipo - Segunda parte 77 Ejemplos En esta secci´on se usan los resultados de los ejemplos de la Secci´on 4.3.2. Para el ejemplo ’s_[’0. Zero ] =?= ’s_ ^2[ ’0. Zero ] Se hab´ıa obtenido el UnificationPair reduce in METASAT : callUnification ( upModule (’ACNAT , false ) , transformU ( upModule (’ACNAT , false ), ’#0: Nat =?= ’#1: Nat) , 2, 0) . rewrites : 6 in 1 ms cpu (3 ms real ) (4373 rewrites / second ) result UnificationPair : { ’#0: Nat <- ’#3: Nat ; ’#1: Nat <- ’#3: Nat ,3} Si se llama a la funci´on substitutePairs sobre las restricciones obtenidas en el proceso de abstracci´on (Secci´on 4.3.1) con estas sustituciones red substitutePairs ( ’#0: Nat =?= ’s_ [’0. Zero ] ^ ’ #1: Nat =?= ’s_ ^2[ ’0. Zero ], ’#0: Nat <- ’#3: Nat ; ’#1: Nat <- ’#3: Nat) . Se obtiene el PairSet resultante reduce in METASAT : substitutePairs (’#0: Nat =?= ’s_[ ’0. Zero ] ^ ’#1: Nat =?= ’s_ ^2[ ’0. Zero ], ’#0: Nat <- ’#3: Nat ; ’#1: Nat <- ’#3: Nat ) . rewrites : 21 in 0 ms cpu (0 ms real ) (~ rewrites / second ) result PairSet : ’#3: Nat =?= ’s_ [’0. Zero ] ^ ’#3: Nat =?= ’s_ ^2[ ’0. Zero ] Si se le pasa este PairSet a la funci´on createSATRequest red createSATRequest (’#3: Nat =?= ’s_ [’0. Zero ] ^ ’#3: Nat =?= ’s_ ^2[ ’0. Zero ]) . Se obtiene el siguiente SATProblem listo para ser enviado a la interfaz reduce in METASAT : createSATRequest (’#3: Nat =?= ’s_[’0. Zero ] ^ ’#3: Nat =?= ’s_ ^2[ ’0. Zero ]) . rewrites : 3 in 0ms cpu (0 ms real ) (~ rewrites / second ) result SATProblem : ’#3: Nat === ’s_ [’0. Zero ] ^ ’#3: Nat === ’s_ ^2[ ’0. Zero ] 78 4.3. Proceso de conversi´on Para el caso del ejemplo ’_+_[ ’s_[ ’0. Zero ], ’X:Nat ] =?= ’Y: Nat ^ ’_+_[ ’Z:Nat , ’W:Nat ] =?= ’_+_[ ’s_ ^3[ ’0. Zero ], ’s_ ^2[ ’0. Zero ]] El UnificationPair obtenido era reduce in METASAT : callUnification ( upModule (’ACNAT , false ) , transformU ( upModule (’ACNAT , false ), ’#0: Nat =?= ’#1: Nat ^ ’#2: Nat =?= ’#3: Nat) , 4, 0) . rewrites : 9 in 0 ms cpu (0 ms real ) (47872 rewrites / second ) result UnificationPair : { ’#0: Nat <- ’#5: Nat ; ’#1: Nat <- ’#5: Nat ; ’#2: Nat <- ’#6: Nat ; ’#3: Nat <- ’#6: Nat ,6} Al llamar a la funci´on substitutePairs sobre las restricciones obtenidas en el proceso de abstracci´on (Secci´on 4.3.1) con el anterior resultado se obtiene el PairSet red substitutePairs ( ’#0: Nat =?= ’_+_[ ’Z:Nat , ’W:Nat ] ^ ’#1: Nat =?= ’_+_[ ’s_ ^3[ ’0. Zero ],’s_ ^2[ ’0. Zero ]] ^ ’#2: Nat =?= ’_+_[’s_ [’0. Zero ], ’X:Nat ] ^ ’#3: Nat =?= ’Y:Nat , ’#0: Nat <- ’#5: Nat ; ’#1: Nat <- ’#5: Nat ; ’#2: Nat <- ’#6: Nat ; ’#3: Nat <- ’#6: Nat ) . Al llamar a la funci´on substitutePairs sobre las restricciones obtenidas en el proceso de abstracci´on (Secci´on 4.3.1) con el anterior resultado reduce in METASAT : substitutePairs (’#0: Nat =?= ’_+_[ ’Z:Nat , ’W:Nat ] ^ ’#1: Nat =?= ’_+_[ ’s_ ^3[ ’0. Zero ], ’s_ ^2[ ’0. Zero ]] ^ ’#2: Nat =?= ’_+_[’s_[’0. Zero ], ’X: Nat ] ^ ’#3: Nat =?= ’Y:Nat , ’#0: Nat <- ’#5: Nat ; ’#1: Nat <- ’#5: Nat ; ’#2: Nat <- ’#6: Nat ; ’#3: Nat <- ’#6: Nat ) . rewrites : 105 in 0 ms cpu (0 ms real ) (889830 rewrites / second ) result PairSet : ’#5: Nat =?= ’_+_[’Z:Nat ,’W:Nat] ^ ’#5: Nat =?= ’_+_[’s_ ^3[ ’0. Zero ],’s_ ^2[ ’0. Zero ]] ^ ’#6: Nat =?= ’Y: Nat ^ ’#6: Nat =?= ’_+_[ ’s_[ ’0. Zero ],’X:Nat ] Finalmente, al llamar a la funci´on createSATRequest mediante red createSATRequest ( ’#5: Nat =?= ’_+_[ ’Z: Nat , ’W:Nat ] ^ 4. Prototipo - Segunda parte 79 ’#5: Nat =?= ’_+_[ ’s_ ^3[ ’0. Zero ],’s_ ^2[ ’0. Zero ]] ^ ’#6: Nat =?= ’Y:Nat ^ ’#6: Nat =?= ’_+_[ ’s_ [’0. Zero ], ’X:Nat ]) . Se obtiene el SATProblem reduce in METASAT : createSATRequest ( ’#5: Nat =?= ’_+_[’Z:Nat ,’W: Nat ] ^ ’#5: Nat =?= ’_+_[ ’s_ ^3[ ’0. Zero ], ’s_ ^2[ ’0. Zero ]] ^ ’#6: Nat =?= ’Y: Nat ^ ’#6: Nat =?= ’_+_[ ’s_ [’0. Zero ], ’X: Nat ]) . rewrites : 5 in 0ms cpu (0 ms real ) (~ rewrites / second ) result SATProblem : ’#5: Nat === ’_+_[’Z:Nat ,’W:Nat ] ^ ’#5: Nat === ’_+_[’s_ ^3[ ’0. Zero ],’s_ ^2[ ’0. Zero ]] ^ ’#6: Nat === ’Y: Nat ^ ’#6: Nat === ’_+_[ ’s_[ ’0. Zero ],’X:Nat ] 4.3.4. Flujo de ejecuci´on del prototipo El punto de entrada del prototipo es la funci´on metasat-trans (listado 4.11) y ´unicamente realiza una llamada a la funci´on parseInput (explicada en la Secci´on 4.3.1) y env´ıa el resultado a la funci´on m´as importante del prototipo, executesat. Listing 4.11: Funci´on metasat-trans 1op metasat - trans : Module PairSet Nat -> Bool . 2ceq metasat - trans(M:Module , P:PairSet , N: Nat ) 3= executesat (M: Module ,( PS: PairSet , PS1 : PairSet , N1: Nat ), 0) 4if (PS :PairSet , PS1: PairSet , N1 :Nat , S1: Substitution ) 5:= parseInput (M: Module , N:Nat , P:PairSet , none ) . La funci´on executesat (listado 4.12) act´ua a modo de bucle (cada iteraci´on se ha modelado mediante la funci´on SATIteration, listado 4.13). Cada SATIteration ejecuta el proceso que se ha realizado en la Secci´on 4.3.3, es decir, realiza las sustituciones obtenidas de la funci´on callUnification sobre el conjunto de restricciones, crea la petici´on SATProblem y realiza la llamada sobre la funci´on del prototipo metasat-interface (Secci´on 3.3). Una vez se ha ejecutado la funci´on SATIteration, se devuelve un Bool que se mapea a Boole (Secci´on 4.2). Los posibles casos son los siguientes: SATIteration devuelve true: Finaliza la ejecuci´on del algoritmo y devuelve true. 80 4.3. Proceso de conversi´on SATIteration devuelve false: Se realiza recursivamente una nueva llamada a la funci´on executesat incremententando el N:Nat final en una unidad. Esto significa que se llamar´a a la funci´on callUnification para que obtenga el siguiente UnificationPair, en caso que exista. SATIteration devuelve error: No ha podido ejecutarse la funci´on SATIteration porque la funci´on callUnification no ha encontrado m´as UnificationPair y el resultado de metasat-interface devuelve false, se aborta la ejecuci´on del algoritmo y se devuelve false. Listing 4.12: Funci´on executesat 1*** Execute SAT 2*** Nat -> Numero de unificacion 3op executesat : Module PairSet & PairSet & Counter Nat -> Bool . 4ceq executesat (M: Module , P: PairSet & PairSet & Counter , N: Nat ) 5= if B: Boole == true 6then true 7else if B: Boole == error 8then false 9else executesat (M :Module , P: PairSet & PairSet & Counter , N: Nat + 1) 10 fi 11 fi 12 if B: Boole := SATIteration (M: Module , getSecondPair (P: PairSet &PairSet&Counter), 13 callUnification (M: Module , transformU (M: Module , 14 getFirstPair (P: PairSet & PairSet & Counter)), 15 getCounter (P : PairSet & PairSet & Counter ), N:Nat )) . d Listing 4.13: Funci´on SATIteration 1op SATIteration : Module PairSet UnificationPair -> Boole . 2ceq SATIteration (M: Module , P: PairSet , noUnifier ) 3= if B:Bool == true then true 4else error 5fi 6if B: Bool := metasat - interface (M: Module , createSATRequest (P: PairSet ) ) . 7eq SATIteration (M:Module , P: PairSet , U: UnificationPair ) 8= metasat - interface (M: Module , 9createSATRequest ( substitutePairs (P: PairSet , getSubst (U: UnificationPair )))) . A continuaci´on se detallan algunos ejemplos. 4. Prototipo - Segunda parte 81 Ejemplos Si se toma el ejemplo de la Secci´on 4.3.3 ’_+_[ ’s_[ ’0. Zero ], ’X:Nat ] =?= ’Y: Nat ^ ’_+_[ ’Z:Nat , ’W:Nat ] =?= ’_+_[ ’s_ ^3[ ’0. Zero ], ’s_ ^2[ ’0. Zero ]] Del que se hab´ıa obtenido el siguiente SATProblem ’#5: Nat === ’_+_[’Z:Nat ,’W:Nat] ^ ’#5: Nat === ’_+_[ ’s_ ^3[ ’0. Zero ],’s_ ^2[ ’0. Zero ]] ^ ’#6: Nat === ’Y:Nat ^ ’#6: Nat === ’_+_[’s_ [’0. Zero ], ’X:Nat ] Y se ejecuta la funci´on metasat-trans red metasat - trans ( upModule (’ACNAT , false ) , ’_+_[ ’s_[ ’0. Zero ], ’X:Nat ] =?= ’Y: Nat ^ ’_+_[ ’Z:Nat , ’W:Nat ] =?= ’_+_[ ’s_ ^3[ ’0. Zero ], ’s_ ^2[ ’0. Zero ]] , 0 ) . Se obtiene el siguiente resultado reduce in METASAT : metasat - trans ( upModule (’ACNAT , false ) , ’_+_ [’Z:Nat , ’W: Nat] =?= ’_+_[ ’s_ ^3[ ’0. Zero ], ’s_ ^2[ ’0. Zero ]] ^ ’_+_[’s_[ ’0. Zero ],’X: Nat ] =?= ’Y:Nat , 0) . rewrites : 681 in 13 ms cpu (49 ms real ) (50662 rewrites / second ) result Bool: true Otro ejemplo ser´ıa el siguiente ’s_[’0. Zero ] =?= ’s_ ^2[ ’0. Zero ] Donde el SATProblem resultante era reduce in METASAT : createSATRequest (’#3: Nat =?= ’s_[’0. Zero ] ^ ’#3: Nat =?= ’s_ ^2[ ’0. Zero ]) . rewrites : 3 in 0ms cpu (0 ms real ) (~ rewrites / second ) result SATProblem : ’#3: Nat === ’s_ [’0. Zero ] ^ ’#3: Nat === ’s_ ^2[ ’0. Zero ] Al ejecutar la funci´on metasat-trans 88 5.3. Ejecuci´on del algoritmo Listing 5.2: Funci´on expand 1***( 2Expand 3TemList -. Lista de cabeceras de funcion 4) 5op expand : Module EquationSet RuleSet Nat PairSet -> PairSet & PairSet & Counter . 6eq expand (M:Module , O: EquationSet , R:RuleSet , N:Nat , emptyPairSet ) 7= (emptyPairSet , emptyPairSet , N:Nat) . 8ceq expand (M: Module , O: EquationSet , R:RuleSet , N:Nat , T1: Term =?= T2: Term ^ PS : PairSet ) 9= ( T1 ’: Term =?= T2 ’: Term ^ PS3 : PairSet , PS1 : PairSet ^ PS2 : PairSet ^ PS4: PairSet , N3:Nat) 10 if ( T1 ’: Term , PS1 : PairSet , N1 : Nat ) 11 := convert (M: Module , (T1 :Term , emptyPairSet , N: Nat ) , O: EquationSet , R: RuleSet ) 12 /\ ( T2 ’: Term , PS2 : PairSet , N2 : Nat ) 13 := convert (M: Module , (T2 :Term , emptyPairSet , N1 :Nat ), O: EquationSet , R: RuleSet ) 14 /\ (PS3: PairSet , PS4: PairSet , N3: Nat ) 15 := expand (M: Module , O: EquationSet , R: RuleSet , N2:Nat , PS: PairSet) . Del mismo modo se ha definido una funci´on denominada canExpand (listado 5.3) que comprueba si un determinado conjunto PairSet puede expandirse (devolviendo true ofalse segun el caso). Los argumentos son los mismos que la funci´on expand. Listing 5.3: Funci´on canExpand 1op canExpand : Module EquationSet RuleSet Nat PairSet -> Bool . 2eq canExpand (M: Module , O:EquationSet , R: RuleSet , N:Nat , emptyPairSet ) = false . 3ceq canExpand (M: Module , O: EquationSet , R: RuleSet , N:Nat , T1: Term =?= T2: Term ^ PS : PairSet ) 4= B: Bool or B1: Bool or B2: Bool 5if B: Bool := containSymbol ( T1 :Term , O: EquationSet , R: RuleSet ) 6/\ B1 : Bool := containSymbol ( T2 :Term , O: EquationSet , R: RuleSet ) 7/\ B2: Bool := canExpand (M: Module , O: EquationSet , R: RuleSet , N:Nat , PS : PairSet ) . La anterior funci´on canExpand trabaja conjuntamente con la funci´on reduceTrivialProblem (listado 5.4) que comprueba que, en el caso que haya una ´unica variable a uno de los lados de un operador Pair (=?=), si existe una ocurrencia de dicha variable en alguna otra ecuaci´on. Sino existe ninguna ocurrencia de dicha variable se reemplaza la ecuaci´on en la que aparece por una igualdad siempre cierta (’0.Zero =?= ’0.Zero). Si dicha variable aparece en otra ecuaci´on, no se modifica el conjunto PairSet. Listing 5.4: Funci´on reduceTrivialProblem 5. Prototipo - Tercera parte 89 1op reduceTrivialProblem : PairSet -> PairSet . 2eq reduceTrivialProblem ( emptyPairSet ) = emptyPairSet . 3ceq reduceTrivialProblem (T1 : Term =?= V: Variable ^ P: PairSet ) = 4’0. Zero =?= ’0. Zero ^ reduceTrivialProblem (P: PairSet ) 5if not VariableIn (V: Variable , P : PairSet ) . 6 7ceq reduceTrivialProblem (V: Variable =?= T1 :Term ^ P: PairSet ) = 8’0. Zero =?= ’0. Zero ^ reduceTrivialProblem (P: PairSet ) 9if not VariableIn (V: Variable , P : PairSet ) . 10 11 eq reduceTrivialProblem (P: PairSet ) = P: PairSet [ owise ] . La funci´on reduceTrivialProblem se apoya sobre la funci´on VariableIn (listado 5.5) que comprueba si una variable esta contenida en un PairSet. Listing 5.5: Funci´on VariableIn 1op VariableIn : Variable PairSet -> Bool . 2eq VariableIn (V: Variable , emptyPairSet ) = false . 3eq VariableIn (V: Variable , V: Variable =?= T2 :Term ^ P: PairSet ) = true . 4eq VariableIn (V: Variable , T: Term =?= T2 :Term ^ P: PairSet ) 5= VariableInTerm (V: Variable , T: Term ) 6or - else VariableInTerm ( V: Variable , T2 : Term ) 7or - else VariableIn (V: Variable , P: PairSet ) [ owise ] . Finalmente, la funci´on VariableInTerm (listado 5.6) es la que realmente comprueba si una variable existe en un t´ermino o lista de t´erminos. Listing 5.6: Funci´on VariableInTerm 1op VariableInTerm : Variable Term -> Bool . 2eq VariableInTerm (V: Variable , V’: Variable ) = if V: Variable == V ’: Variable then true else false fi . 3eq VariableInTerm (V:Variable , empty) = false . 4eq VariableInTerm (V:Variable , C: Constant ) = false . 5eq VariableInTerm (V: Variable , F: Qid[ TL ’: TermList ]) = VariableInTerm (V: Variable , TL ’: TermList ) . 6eq VariableInTerm (V: Variable , (T: Term , TL: TermList )) 7= VariableInTerm (V: Variable , T: Term ) or - else VariableInTerm (V: Variable , TL : TermList ) . 8 9eq VariableInTerm (V:Variable , T: Term) = false [owise ] . La funci´on convert (listado 5.7) recibe un Term&PairSet&Counter (visto en la Secci´on 4.2) junto con el m´odulo y el conjunto de ecuaciones y reglas y, si el t´ermino (T:Term) contiene alguna regla (funci´on containRls) entonces se llama a la funci´on replaceTermRls que los sustituye. Aunque la funci´on convert puede tambi´en reemplazar ecuaciones se ha eliminado (comentado) dicha opci´on pues queda fuera del ´ambito de la presente teor´ıa. En un futuro 90 5.3. Ejecuci´on del algoritmo podr´ıa realizarse tambi´en una sustituci´on de ecuaciones, por este motivo en la presente memoria no se detallar´an las funciones de sustituci´on de ecuaciones sino ´unicamente las que sustituyen reglas. Listing 5.7: Funci´on convert 1***( 2Convert 3TemList -. Lista de cabeceras de funcion 4) 5op convert : Module Term & PairSet & Counter EquationSet RuleSet -> Term & PairSet&Counter . 6eq convert (M: Module , ( empty , PS :PairSet , N: Nat ) , E: EquationSet , R: RuleSet ) = (empty , PS :PairSet , N: Nat) . 7eq convert (M: Module , (T: Term , PS: PairSet , N: Nat ), E: EquationSet , R: RuleSet ) 8= if containRls (T: Term , R: RuleSet ) == true 9then replaceTermRls (M: Module , (T: Term , PS: PairSet , N: Nat ), R :RuleSet) 10 else 11 (T:Term , PS: PairSet , N:Nat ) 12 ***( Codigo para reemplazar ecuaciones 13 if containEqs (T: Term , E: EquationSet ) == true 14 then replaceTermEqs (M: Module , (T: Term , PS: PairSet , N: Nat ), E :EquationSet) 15 else 16 (T:Term , PS: PairSet , N:Nat ) 17 fi) --- fin comentario 18 fi . La funci´on containRls (listado 5.8) se ejecuta junto a la funci´on containRl (listado 5.9) y se encargan de comprobar si en un t´ermino hay alguna ocurrencia de alguna regla definida en un conjunto RuleSet. Su ejecuci´on es el siguiente, para cada regla containRls delega en containRl para que ´esta ´ultima compruebe si existe dicha regla en el t´ermino dado. Si el resultado es true entonces containRls devuelve true pero si el resultado es false entonces containRls sigue iterando sobre el conjunto restante de reglas. Listing 5.8: Funci´on containRls 1***( 2Comprueba si el termino contiene algun QID de alguna regla 3) 4op containRls : Term RuleSet -> Bool . 5eq containRls ( T: Term , none ) = false . 6ceq containRls (T:Term , ( rl F’: Qid[ TL: TermList ] => T’: Term [Ats : AttrSet ] .) R :RuleSet) 7= B: Bool or B1 :Bool 8if B: Bool := containRl (T:Term , (rl F ’:Qid [TL : TermList ] => T ’:Term [ Ats : AttrSet ] .) ) 9/\ B1 : Bool := containRls (T:Term , R: RuleSet ) . Listing 5.9: Funci´on containRl 5. Prototipo - Tercera parte 91 1***( 2Comprueba si los terminos y subterminos tienen el mismo qid que una regla dada 3) 4op containRl : Term Rule -> Bool . 5eq containRl (empty , E: Rule ) = false . 6eq containRl (F: Qid [TL ’: TermList ], rl F ’: Qid [TL : TermList ] => T ’: Term [ Ats : AttrSet] . ) 7=if F:Qid == F’: Qid 8then true 9else containRl ( TL ’: TermList , rl F ’: Qid [TL: TermList ] => T ’: Term [ Ats : AttrSet ] . ) fi . 10 eq containRl (( F: Qid [TL ’: TermList ] , TL : TermList ) , E: Rule ) 11 = containRl (F: Qid [TL ’: TermList ], E: Rule ) or containRl ( TL : TermList , E :Rule ) . 12 eq containRl (( T: Term , TL : TermList ) , E: Rule ) 13 = containRl (TL: TermList , E: Rule ) . 14 eq containRl (T:Term , E: Rule ) = false [owise ] . Para reemplazar las ocurrencias de las reglas sobre un t´ermino se ha definido la funci´on replaceTermRls (listado 5.10), en ella se comprueba en primer lugar (utilizando la funci´on containRls) si existe alguna ocurrencia de la regla actual. Si el resultado es true entonces se llama a la funci´on replaceTermRl para que reemplace dicha regla. Si el resultado es false entonces recursivamente se vuelve a llamar a la funci´on replaceTermRls con el resto de reglas hasta que no haya ninguna (none). Listing 5.10: Funci´on replaceTermRls 1***( 2Reemplaza un termino por una variable si coincide con alguna regla (sobre un conjunto ) 3) 4op replaceTermRls : Module Term & PairSet & Counter RuleSet -> Term & PairSet & Counter . 5eq replaceTermRls (M:Module , (T:Term , PS: PairSet , N: Nat ), none ) = (T:Term , PS :PairSet , N:Nat) . 6eq replaceTermRls (M:Module , (T:Term , PS: PairSet , N: Nat ), (rl F ’:Qid [TL: TermList ] => T’: Term [ Ats : AttrSet ] .) R: RuleSet ) 7= if containRl (T:Term , rl F’: Qid [TL : TermList ] => T ’:Term [ Ats : AttrSet ] .) == true 8then replaceTermRl (M:Module , (T:Term , PS: PairSet , N:Nat ), rl F ’: Qid [ TL : TermList ] = > T’: Term [Ats : AttrSet ] .) 9else replaceTermRls (M:Module , (T:Term , PS: PairSet , N: Nat) , R: RuleSet ) fi . La funci´on replaceTermRl (listado 5.11) recibe un Term&PairSet&Counter con el t´ermino a expandir y una regla (Rule) y seg´un la composici´on del t´ermino pueden darse varios casos de expansi´on. El primero de ellos se da en el caso que el t´ermino sea una operaci´on con un Qid (en concreto 92 5.3. Ejecuci´on del algoritmo F:Qid[TL’:TermList]) entonces, en primer lugar se comprueba si ese Qid es el mismo que el Qid de la regla (F’:Qid) (al mismo tiempo se intenta convertir la lista de t´erminos TL’:TermList dando como resultado la lista de t´erminos T1:TermList). Si son el mismo, entonces se crea una variable nueva (m´etodo similar al visto en la Secci´on 4.3.1), se sustituye todo el t´ermino por dicha variable y se a˜nade una nueva restricci´on al conjunto de restricciones ((createVariableT(M:Module, F:Qid[T1:TermList], N1:Nat) =?= F:Qid[T1:TermList])). Si los Qid no son iguales se devuelve el mismo Qid con la lista de t´erminos (posiblemente) convertida (T1:TermList). Listing 5.11: Funci´on replaceTermRl 1***( 2Reemplaza un termino por una variable si coincide con una regla 3) 4op replaceTermRl : Module Term & PairSet & Counter Rule -> Term & PairSet & Counter . 5ceq replaceTermRl (M: Module , (F:Qid [TL ’: TermList ], PS: PairSet , N:Nat ), 6rl F ’: Qid [TL: TermList ] => T ’: Term [Ats : AttrSet ] .) 7= if F:Qid == F’: Qid 8then ( createVariableT (M: Module , F: Qid [T1 : TermList ], N1: Nat ), 9PS1 :PairSet ^ ( createVariableT (M: Module , F: Qid [T1: TermList ], N1: Nat ) 10 =?= F: Qid [T1 : TermList ]) , N1 : Nat + 1) 11 else (F: Qid [T1: TermList ], PS1: PairSet , N1: Nat ) fi 12 if (T1 : TermList , PS1 : PairSet , N1: Nat) 13 := replaceTermRl (M: Module , ( TL ’:TermList , PS: PairSet , N: Nat ) , 14 rl F ’: Qid [TL: TermList ] => T ’: Term [Ats : AttrSet ] .) . Otro de los posibles casos de la funci´on replaceTermRl es que el t´ermino sea una un operador junto a una lista de t´erminos ((F:Qid[TL’:TermList], TL:TermList)), en ese caso, primero se intenta convertir cada lista de t´erminos por separado y, finalmente se unen los resultados que proporcionan las llamadas replaceTermRl(M:Module, (F:Qid[TL’:TermList], PS:PairSet, N:Nat), R:Rule) yreplaceTermRl(M:Module, (TL:TermList, PS:PairSet, N1:Nat), R:Rule) (conjuntos de pares y restricciones). 1ceq replaceTermRl (M: Module , ((F: Qid [TL ’: TermList ], TL: TermList ) , PS : PairSet , N: Nat ), R: Rule) 2= (( T1: TermList , T2: TermList ) , PS1 : PairSet ^ PS2 :PairSet , N2: Nat) 3if (T1 : TermList , PS1 : PairSet , N1: Nat) 4:= replaceTermRl (M: Module , (F: Qid [TL ’: TermList ] , PS : PairSet , N: Nat ), R: Rule) 5/\ (T2 : TermList , PS2 : PairSet , N2: Nat) 6:= replaceTermRl (M: Module , (TL: TermList , PS: PairSet , N1: Nat) , R: Rule ) . Tambi´en puede darse el caso que en la lista de t´erminos el primero sea un 5. Prototipo - Tercera parte 93 t´ermino com´un, en ese caso ´unicamente hay que convertir la lista de t´erminos (TL:TermList). 1ceq replaceTermRl (M: Module , ((T: Term , TL : TermList ), PS : PairSet , N: Nat ), R: Rule) 2= (( T:Term , T1: TermList ) , PS1 :PairSet , N1 :Nat ) 3if (T1 : TermList , PS1 : PairSet , N1: Nat) 4:= replaceTermRl (M: Module , (TL :TermList , 5PS: PairSet , N: Nat ), R: Rule ) . El ´ultimo caso es en el que no pueda entrar por ning´un caso anterior y, por tanto, el t´ermino se devuelve sin modificar. 1eq replaceTermRl (M: Module , (T:Term , PS:PairSet , N: Nat) , R: Rule ) 2= (T:Term , PS: PairSet , N: Nat ) [ owise ] . A continuaci´on se describen algunos ejemplos. Ejemplos Por ejemplo, definimos el siguiente m´odulo MULT (listado 5.12) en Maude que es una teor´ıa extendida de la aritm´etica Presburger con la multiplicaci´on. Listing 5.12: M´odulo MULT 1mod MULT is 2pr NAT . 3sorts S Nat2 . 4subsort Nat < Nat2 < S . 5op _;_ : S S -> S [assoc comm prec 75] . 6op _**_ : Nat2 Nat2 -> Nat2 [ prec 73] . 7rl 0 ** S1: Nat2 => 0 . 8rl s( S1: Nat2 ) ** S2 :Nat2 => S2: Nat2 + (S1: Nat2 ** S2 :Nat2) . 9endm Si se da el siguiente ejemplo 1’_** _[’s_ ^1[ ’0. Zero ], ’s_ ^4[ ’0. Zero ]] =?= ’s_ ^4[ ’0. Zero ] Como se puede observar en el ejemplo no existe ninguna variable, por tanto la funci´on reduceTrivialProblem no puede eliminar ninguna ecuaci´on. 94 5.3. Ejecuci´on del algoritmo Al aplicar el comando de Maude 1red expand ( upModule ( ’MULT , false ), getEqs ( upModule ( ’MULT , false )), 2getRls ( upModule ( ’MULT , false )) , 0, 3’_** _[’s_ ^1[ ’0. Zero ], ’s_ ^4[ ’0. Zero ]] =?= ’s_ ^4[ ’0. Zero ]) . Se obtiene el siguiente PairSet&PairSet&Counter 1red expand ( upModule ( ’MULT , false ), getEqs ( upModule ( ’MULT , false )), 2getRls ( upModule ( ’MULT , false )) , 0, 3’_** _[’s_ ^1[ ’0. Zero], ’s_ ^4[ ’0. Zero ]] =?= ’s_ ^4[ ’0. Zero ]) . 4reduce in METASAT : expand ( upModule ( ’MULT , false ) , 5getEqs ( upModule ( ’MULT , false )) , getRls ( upModule ( ’MULT , false )) , 0, 6’_** _[’s_ ^1[ ’0. Zero ], ’s_ ^4[ ’0. Zero ]] =?= ’s_ ^4[ ’0. Zero ]) . 7rewrites : 77 in 0 ms cpu (0 ms real ) (~ rewrites / second ) 8result PairSet&PairSet&Counter: 9(’#0: Nat2 =?= ’s_ ^4[ ’0. Zero ], ’#0: Nat2 =?= ’_** _[’s_ ^1[ ’0. Zero ], ’s_ ^4[ ’0. Zero ]] ,1) Donde el conjunto convertido es 1’#0: Nat2 =?= ’s_ ^4[ ’0. Zero ] Y el conjunto de restricciones es 1’#0: Nat2 =?= ’_ ** _[’s_ ^1[ ’0. Zero ],’s_ ^4[ ’0. Zero ]] Si se toma el siguiente ejemplo 1’_+_[ ’Y: Nat2 , ’_ ** _[ ’Z:Nat2 , ’s_ ^1[ ’0. Zero ]]] =?= ’s_ ^1[ ’0. Zero ] Al lanzar el comando Maude 1red expand ( upModule ( ’MULT , false ), getEqs ( upModule ( ’MULT , false )), 2getRls ( upModule ( ’MULT , false )) , 0, 3’_+_[ ’Y: Nat2 , ’_ ** _[ ’Z:Nat2 , ’s_ ^1[ ’0. Zero ]]] =?= ’s_ ^1[ ’0. Zero ]) . Se obtiene el siguiente resultado 1reduce in METASAT : expand ( upModule ( ’MULT , false ) , getEqs ( upModule (’MULT , false ) ), 2getRls ( upModule ( ’MULT , false )) , 0, 3’_+_[ ’Y: Nat2 , ’_ ** _[ ’Z:Nat2 , ’s_ ^1[ ’0. Zero ]]] =?= ’s_ ^1[ ’0. Zero ]) 5. Prototipo - Tercera parte 95 4. 5rewrites : 89 in 0 ms cpu (0 ms real ) (89000000 rewrites / second ) 6result PairSet&PairSet&Counter: 7(’_+_[’Y: Nat2 , ’#0: Nat2 ] =?= ’s_ ^1[ ’0. Zero ], 8’#0: Nat2 =?= ’_ ** _[’Z: Nat2 , ’s_ ^1[ ’0. Zero ]] ,1) Donde el conjunto convertido es 1’_+_[ ’Y:Nat2 ,’#0: Nat2 ] =?= ’s_ ^1[ ’0. Zero ] Y el conjunto de restricciones 1’#0: Nat2 =?= ’_ ** _[’Z: Nat2 , ’s_ ^1[ ’0. Zero ]] A continuaci´on se muestra un ejemplo un poco m´as complejo 1’_**_[’Y:Nat2 ,’_** _[ ’Z:Nat2 ,’s_ ^1[ ’0. Zero ]]] =?= 2’_** _[’s_ ^3[ ’0. Zero ], ’_ ** _[ ’W: Nat2 , ’X: Nat2 ]] El comando de Maude es 1red expand ( upModule ( ’MULT , false ) , getEqs ( upModule (’MULT , false )) , 2getRls ( upModule ( ’MULT , false )) , 0, 3’_** _[’Y:Nat2 , ’_ ** _[ ’Z:Nat2 , ’s_ ^1[ ’0. Zero ]]] =?= 4’_** _[’s_ ^3[ ’0. Zero ], ’_ ** _[ ’W: Nat2 , ’X: Nat2 ]]) . Y el correspondiente resultado es 1reduce in METASAT : expand ( upModule ( ’MULT , false ) , getEqs ( upModule (’MULT , false ) ), 2getRls ( upModule ( ’MULT , false )) , 0, 3’_** _[’Y:Nat2 , ’_ ** _[ ’Z:Nat2 , ’s_ ^1[ ’0. Zero ]]] =?= 4’_** _[’s_ ^3[ ’0. Zero ], ’_ ** _[ ’W: Nat2 , ’X: Nat2 ]]) . 5rewrites : 122 in 0 ms cpu (0 ms real ) (~ rewrites / second ) 6result PairSet&PairSet&Counter: 7(’#1: Nat2 =?= ’#3: Nat2 ,’#0: Nat2 =?= ’_ **_[’Z: Nat2 , 8’s_ ^1[ ’0. Zero ]] ^ ’ #1: Nat2 =?= ’_** _[’Y:Nat2 , ’#0: Nat2 ] ^ 9’#2: Nat2 =?= ’_**_[’W:Nat2 , ’X: Nat2 ] ^ 10 ’#3: Nat2 =?= ’_ ** _[’s_ ^3[ ’0. Zero ],’#2: Nat2 ] 11 ,4) Donde el conjunto convertido es 1’#1: Nat2 =?= ’#3: Nat2 96 5.3. Ejecuci´on del algoritmo Y el conjunto de restricciones 1’#0: Nat2 =?= ’_ ** _[’Z: Nat2 , ’s_ ^1[ ’0. Zero ]] ^ 2’#1: Nat2 =?= ’_**_[’Y:Nat2 ,’#0: Nat2 ] ^ 3’#2: Nat2 =?= ’_**_[’W:Nat2 ,’X: Nat2 ] ^ 4’#3: Nat2 =?= ’_ ** _[’s_ ^3[ ’0. Zero ],’#2: Nat2 ] 5.3.2. Obtenci´on de sustituciones mediante Narrowing Una vez se ha obtenido el conjunto PairSet convertido y el conjunto PairSet de restricciones, visto en la Secci´on 5.3.1, se intentan encontrar substituciones sobre las partes derechas de las restricciones utilizando la funci´on de Maude llamada metaNarrowSearch (vista en la Secci´on 2.2.11). La funci´on que realiza esa llamada se denomina callMetaNarrow (listado 5.13). Esta funci´on recibe el m´odulo con la teor´ıa ecuacional, un PairSet de la forma Var =?= Term (contenido en el conjunto de restricciones) y una variable que es la meta-representaci´on del punto de llegada de la funci´on metaNarrowSearch. Como se puede observar en la llamada, se le indica a la funci´on metaNarrowSearch que busque el resultado en varios pasos ’* y que ´unicamente devuelva una soluci´on (con el par´ametro 1). La funci´on callMetaNarrow devuelve la tripleta ResultTripleSet obtenida (en caso afirmativo) a partir de la llamada a metaNarrowSearch oempty en caso que el PairSet est´e vac´ıo (emptyPairSet). Listing 5.13: Funci´on callMetaNarrow 1***( 2Lanza la funcion metaNarrowSearch 3) 4op callMetaNarrow : Module PairSet Variable -> ResultTripleSet . 5eq callMetaNarrow (M:Module , emptyPairSet , V: Variable ) = empty . 6eq callMetaNarrow ( M: Module , T: Term =?= T2 :Term , V: Variable ) 7= metaNarrowSearch (M: Module , T2 :Term , V: Variable , none , ’*, 1, unbounded ) . Ejemplos Si se toman las restricciones obtenidas de un ejmplo anterior ’#0: Nat2 =?= ’_ ** _[’Z: Nat2 , ’s_ ^1[ ’0. Zero ]] ^ ’#1: Nat2 =?= ’_**_[’Y:Nat2 ,’#0: Nat2 ] ^ 5. Prototipo - Tercera parte 97 ’#2: Nat2 =?= ’_**_[’W:Nat2 , ’X: Nat2 ] ^ ’#3: Nat2 =?= ’_ ** _[’s_ ^3[ ’0. Zero ],’#2: Nat2 ] Y se realiza la llamada callMetaNarrow red callMetaNarrow ( upModule ( ’MULT , false ) , ’#0: Nat2 =?= ’_ ** _[’Z: Nat2 , ’s_ ^1[ ’0. Zero ]] , ’#4: Nat2 ) . Se obtienen las substituciones del listado 5.3.2, de las cuales tan s´olo interesan la primera y tercera, pues la segunda (’ ** [’Z:Nat2,’s ^1[’0.Zero]]) es exactamente el mismo t´ermino que se han lanzado en la llamada, por tanto, si se utilizase en la ejecuci´on se crear´ıan ejecuciones infinitas. reduce in METASAT : callMetaNarrow ( upModule ( ’MULT , false ) , ’#0: Nat2 =?= ’_ ** _[’Z: Nat2 , ’s_ ^1[ ’0. Zero ]] , ’#4: Nat2 ) . rewrites : 2207 in 2 ms cpu (2 ms real ) (821667 rewrites / second ) result Result TripleSet : { ’0. Zero , ’Zero , ’#4: Nat2 <- ’0. Zero ; ’#5: Nat2 <- ’s_[’0. Zero] ; ’Z: Nat2 <- ’0. Zero } | {’_** _[ ’Z:Nat2 , ’s_ ^1[ ’0. Zero ]] ,’Nat2 , ’#4: Nat2 <- ’_** _[’Z:Nat2 , ’s_[ ’0. Zero ]] ; ’#6: Nat2 <- ’Z: Nat2 } | {’_+_[’s_[’0. Zero],’_**_[ ’#8: Nat ,’s_ [’0. Zero ]]] ,’Nat2 , ’#10: Nat <- ’#8: Nat ; ’#4: Nat2 <- ’_+_[’s_[’0. Zero],’_**_[ ’#8: Nat ,’s_ [’0. Zero ]]] ; ’#5: Nat2 <- ’#8: Nat ; ’#6: Nat2 <- ’s_[’0. Zero] ; ’Z: Nat2 <- ’s_ [’#8: Nat ]} Si se ejecuta la segunda restricci´on con la llamada red callMetaNarrow ( upModule ( ’MULT , false ) , ’#1: Nat2 =?= ’_**_[’Y:Nat2 , ’#0: Nat2 ], ’#4: Nat2 ) . Se produce el resultado del listado 5.3.2,y, de estas sustituciones las ´unicas validas son la primera y la tercera por los mismos motivos que se han definido anteriormente. reduce in METASAT : callMetaNarrow ( upModule (’MULT , false ), ’#1: Nat2 =?= ’_** _[ ’Y:Nat2 ,’#0: Nat2 ], ’#4: Nat2 ) . rewrites : 1856 in 1 ms cpu (2 ms real ) (1022026 rewrites / second ) result Result TripleSet : { ’0. Zero , ’Zero , ’#4: Nat2 <- ’0. Zero ; ’#5: Nat2 <- ’#0: Nat2 ; ’#7: Nat2 <- ’#0: Nat2 ; ’Y: Nat2 <- ’0. Zero } | 104 5.3. Ejecuci´on del algoritmo Estos dos estados ser´ıan el resultado de la llamada a la funci´on nextLevel creando, a partir de un estado, un nuevo nivel en el ´arbol que contiene dos estados. En este ejemplo, por cada llamada nextLevel sucesiva sobre cada estado se generar´ıan estados dependiendo del n´umero de sustituciones que generase la funci´on callMetaNarrow, es decir, si hay 2 restricciones cada una con 2 sustituciones v´alidas para cada una se generar´ıan 4 estados. En el caso en que hubiesen 3 restricciones con 3 sustituciones v´alidas para cada una se generar´ıan 9 estados, y as´ı sucesivamente. 5.3.4. Control del flujo del programa Esta parte del prototipo refleja c´omo se comporta la ejecuci´on y generaci´on de estados para no entrar en ciclos infinitos de recurrencia ya que podr´ıa existir un problema de terminaci´on con la explosi´on combinatoria de estados que se ha comentado con anterioridad (Secci´on 5.3.3). Toda la gesti´on del prototipo la maneja la funci´on globalControl (listado 5.18) en la que se sigue un procedimiento para evitar en lo posible, la creaci´on de bucles infinitos. Esta funci´on en primer lugar comprueba si el conjunto de f´ormulas ”expandido” se satisface llamando a la funci´on de la segunda parte del prototipo metasat-trans (Secci´on 4). Si esta funci´on devuelve false entonces se elimina dicho estado ya que ninguna sustituci´on sobre las variables har´a que la f´ormula resulte cierta. Si por el contrario, la funci´on devuelve true entonces significa que podr´ıa ser cierta y, por este motivo, se genera un nuevo estado temporal uniendo el conjunto de f´ormulas ”expandidas” con el conjunto de reglas. Si este estado se puede seguir expandiendo (funci´on canExpand comentada con anterioridad), entonces contin´ua la ejecuci´on de la funci´on globalControl expandiendo todos los posibles estados al aplicar un nuevo nivel (nextLevel) sobre dicho estado temporal. Si dicho estado temporal no se puede expandir y la llamada a la funci´on metasat-trans con dicho estado devuelve false entonces se elimina el estado principal y contin´ua la ejecuci´on del algoritmo. Si la funci´on metasat-trans devuelve true sabemos que las f´ormulas y restricciones de ese estado se satisfacen y, por tanto, no hace falta seguir con la ejecuci´on del algoritmo (devolviendo el valor true). Este proceso se explica en pseudocodigo (listado 5.19). Listing 5.18: Funci´on globalControl 5. Prototipo - Tercera parte 105 1***( 2Funcion global de control 3) 4op globalControl : Module StateSet -> Bool . 5eq globalControl (M: Module , emptyState ) = false . 6eq globalControl (M: Module , P&P&C ; S: StateSet ) 7= if metasat - trans ( M: Module , getFirstPair ( P&P &C) , getCounter (P& P&C )) == false 8then globalControl (M: Module , S: StateSet ) 9else 10 if canExpand (M: Module , getEqs ( M: Module ) , getRls (M: Module ) , getCounter (P&P& C) , getFirstPair (P&P&C) ^ getSecondPair (P&P&C)) == false 11 then if metasat - trans (M:Module , getFirstPair (P&P&C) ^ getSecondPair (P&P& C) , getCounter (P&P&C)) == true 12 then true 13 else 14 globalControl (M: Module , S: StateSet ) 15 fi 16 else 17 globalControl (M: Module , S: StateSet ; 18 expandAll ( M: Module , getEqs (M: Module ), 19 getRls (M : Module ) , nextLevel (M: Module , P&P& C))) 20 fi 21 fi . Listing 5.19: Pseudocodigo globalControl 1globalControl ( conjuntoestados ): 2si conjuntoestados == [] 3return false ; 4 5si metasat - trans ( conjuntoestados [1] - > formulas ) == false 6eliminar ( conjuntoestados [1]) ; 7globalControl ( conjuntoestados ); 8si no // metasat - trans == true 9si posibleExpandir ( conjuntoestados [1] -> formulas + conjuntoestados [1]- > restricciones ) == false 10 si metasat -trans (conjuntoestados [1] -> formulas + conjuntoestados [1] -> restricciones ) == true 11 return true ; 12 si no // metasat - trans == false 13 eliminar ( conjuntoestados [1]) ; 14 globalControl ( conjuntoestados ); 15 si no // posibleExpandir == true 16 eliminar ( conjuntoestados [1]) ; 17 nuevoconjunto = nuevonivel ( conjuntoestados [1] - > formulas + conjuntoestados [1] -> restricciones ); 18 conjuntoexpandido = expandir ( nuevoconjunto ); 19 conjuntoestados . append ( conjuntoexpandido ) ; 20 globalControl ( conjuntoestados ); Finalmente, el punto de entrada al prototipo es la funci´on metasat (listado 5.20) que delega todo el control a la funci´on globalControl. Listing 5.20: Funci´on metasat 106 5.3. Ejecuci´on del algoritmo 1op metasat : Module PairSet -> Bool . 2eq metasat (M: Module , P: PairSet ) = globalControl (M: Module , expand (M: Module , getEqs (M : Module ) , getRls ( M: Module ), 0, reduceTrivialProblem ( P: PairSet ))) . Ejemplos A continuaci´on se muestran algunos ejemplos de ejecuci´on donde entran los tres prototipos proporcionando resultados completos. Ejemplo false El primer ejemplo es ’_** _[’s_ ^1[ ’0. Zero ], ’s_ ^4[ ’0. Zero ]] =?= ’s_ ^5[ ’0. Zero ] Cuya expansi´on genera el estado result PairSet&PairSet&Counter: (’#0: Nat2 =?= ’s_ ^5[ ’0. Zero ], ’#0: Nat2 =?= ’_** _[’s_ ^1[ ’0. Zero ], ’s_ ^4[ ’0. Zero ]] ,1) El primer estado que recibir´ıa la funci´on metasat-trans ser´ıa ’#0: Nat2 =?= ’s_ ^5[ ’0. Zero ] Cuya transformaci´on en SATProblem ser´ıa ’#4: Nat === ’#0: Nat2 ^ ’#4: Nat === ’s_ ^5[ ’0. Zero ] A su vez, el iBool resultante ser´ıa c( true ) ^ c( true ) ^ (c (5) === i (1) ) ^ (i (1) === i (2)) ^ i (1) >= c (0) ^ i (2) >= c (0) 5. Prototipo - Tercera parte 107 Dando como resultado el valor true, entonces se comprueba si se puede expandir, al ser cierto (por tener la restricci´on ’#0:Nat2 =?= ’ ** [’s ^1[’0.Zero],’s ^4[’0.Zero]]) se llama a la funci´on nextLevel generando el estado ’#0: Nat2 =?= ’_+_[’s_ ^4[ ’0. Zero ],’#1: Nat2 ] ^ ’ #0: Nat2 =?= ’s_ ^5[ ’0. Zero ] ^ ’ #1: Nat2 =?= ’0. Zero Cuyo SATProblem generado ser´ıa ’#10: Nat === ’s_ ^4[ ’0. Zero ] ^ ’#8: Nat === ’#0: Nat2 ^ ’#8: Nat === ’s_ ^5[ ’0. Zero ] ^ ’#9: Nat === ’#1: Nat2 ^ ’_+_[ ’#9: Nat , ’#10: Nat ] === ’ #0: Nat2 Y el correspondiente iBool ser´ıa c( true ) ^ c( true ) ^ (c (4) === i (1) ) ^ (c (5) === i (2)) ^ (i (2) === i (3) ) ^ (i (3) === i (1) + i (4)) ^ (i(4) === i(5)) ^ i(1) >= c(0) ^ i(2) >= c (0) ^ i (3) >= c (0) ^ i (4) >= c (0) ^ i(5) >= c(0) Este estado resulta false y, por tanto, se elimina dicho estado del conjunto de estados y como no existen m´as estados en el conjunto se sale de la ejecuci´on devolviendo el valor false. Ejemplo true Dado el ejemplo ’_** _[’Y: Nat2 , ’s_ ^1[ ’0. Zero ]] =?= ’0. Zero Al igual que en los ejemplos anteriores la funci´on reduceTrivialProblem no puede realizar ninguna acci´on ya que no hay ninguna variable sola en ning´un lado de la igualdad. Cuya expansi´on genera el estado result PairSet&PairSet&Counter: (’#0: Nat2 =?= ’0. Zero ,’#0: Nat2 =?= ’_** _[’Y: Nat2 , ’s_ ^1[ ’0. Zero ]] ,1) 108 5.3. Ejecuci´on del algoritmo El estado env´ıado a metasat-trans ser´ıa ’#0: Nat2 =?= ’0. Zero Convirti´endose en el SATProblem ’#4: Nat === ’#0: Nat2 ^ ’#4: Nat === ’0. Zero Y el correspondiente iBool c( true ) ^ c( true ) ^ (c (0) === i (1) ) ^ (i (1) === i (2)) ^ i(1) >= c(0) ^ i (2) >= c (0) La funci´on devuelve true, por tanto se comprueba si el estado se puede expandir. Como tiene la restricci´on (’#0:Nat2 =?= ’ ** [’Y:Nat2, ’s ^1[’0.Zero]]) se devuelve cierto y, por tanto, se debe llamar a la generaci´on de un nuevo nivel de estados. result StateSet : ( ’#0: Nat2 =?= ’ 0. Zero , ’#0: Nat2 =?= ’ 0. Zero ,1) ; (’#0: Nat2 =?= ’0. Zero , ’#0: Nat2 =?= ’_+_[ ’s_ [’0. Zero],’_ **_[’#5: Nat ,’s_ [’0. Zero ]]] ,6) El siguiente estado en ser ejecutado es ’#0: Nat2 =?= ’0. Zero ^ ’#0: Nat2 =?= ’0. Zero Que genera el SATProblem ’#6: Nat === ’#0: Nat2 ^ ’#6: Nat === ’0. Zero ^ ’#7: Nat === ’#0: Nat2 ^ ’#7: Nat === ’0. Zero Y el iBool c( true ) ^ c( true ) ^ (c (0) === i (1) ) ^ (c (0) === i (3)) ^ (i(1) === i(2)) ^ (i (2) === i (3) ) ^ i(1) >= c(0) ^ i(2) >= c (0) ^ i (3) >= c (0) Dando como resultado true y c´omo este estado no es puede expandir m´as (no hay operaciones ** en las restricciones) el prototipo finaliza su ejecuci´on y devuelve el valor true. 5. Prototipo - Tercera parte 109 Otro posible ejemplo vendr´ıa dado por la siguiente ecuaci´on ’_**_[’Y:Nat2 , ’s_ ^1[ ’0. Zero ]] =?= ’X: Nat2 Donde la funci´on reduceTrivialProblem resolver´ıa el problema ya que la ’X:Nat no aparece en otra ecuaci´on. La f´ormula se reducir´ıa a ’0. Zero =?= ’0. Zero Dando como resultado final true ya que no hay m´as estados disponibles. Otro ejemplo m´as complejo ser´ıa el siguiente ’_** _[’Y:Nat2 , ’s_ ^1[ ’0. Zero ]] =?= ’_ ** _[’s_ ^2[ ’0. Zero ], ’X: Nat2 ] Donde el primer estado generado ser´ıa result PairSet&PairSet&Counter: (’#0: Nat2 =?= ’#1: Nat2 , ’#0: Nat2 =?= ’_ ** _[’Y: Nat2 , ’s_ ^1[ ’0. Zero ]] ^ ’#1: Nat2 =?= ’_ ** _[ ’s_ ^2[ ’0. Zero ], ’X: Nat2 ] ,2) El t´ermino que se enviar´ıa a la funci´on metasat-trans ser´ıa ’#0: Nat2 =?= ’#1: Nat2 , Que devolver´ıa el valor true (se han omitido los pasos intermedios). Por tanto se generar´ıa el siguiente conjunto de estados al llamar a la funci´on nextLevel result StateSet : (’#0: Nat2 =?= ’#1: Nat2 ,’#0: Nat2 =?= ’0. Zero ^ ’#1: Nat2 =?= ’_+_[ ’X:Nat2 , ’_** _[’s_[ ’0. Zero ],’X: Nat2 ]] ,2) ; (’#0: Nat2 =?= ’#1: Nat2 ,’#0: Nat2 =?= ’_+_[’s_[ ’0. Zero ], ’_** _[ ’#6: Nat , ’s_ [’ 0. Zero ]]] ^ ’#1: Nat2 =?= ’_+_[’X:Nat2 , ’_ ** _[ ’s_[ ’0. Zero ],’X: Nat2 ]] ,7) Y expandidos (funci´on expand sobre cada uno de ellos) quedar´ıan 110 5.3. Ejecuci´on del algoritmo result StateSet : (’#0: Nat2 =?= ’#1: Nat2 ^ ’#0: Nat2 =?= ’0. Zero ^ ’#1: Nat2 =?= ’_+_[ ’X:Nat2 ,’#2: Nat2 ], ’#2: Nat2 =?= ’_ ** _[ ’s_ [’ 0. Zero ], ’X: Nat2 ] ,3) (’#0: Nat2 =?= ’#1: Nat2 ^ ’#0: Nat2 =?= ’_+_[’s_[’0. Zero ], ’#7: Nat2 ] ^ ’#1: Nat2 =?= ’_+_[ ’X:Nat2 ,’#8: Nat2 ], ’#7: Nat2 =?= ’_** _[’#6: Nat ,’s_[ ’0. Zero ]] ^ ’#8: Nat2 =?= ’_ ** _[ ’s_ [’ 0. Zero ], ’X: Nat2 ] ,9) El estado que se enviar´ıa a la funci´on metasat-trans ser´ıa ’#0: Nat2 =?= ’#1: Nat2 ^ ’#0: Nat2 =?= ’0. Zero ^ ’#1: Nat2 =?= ’_+_[ ’X:Nat2 ,’#2: Nat2 ] Transform´andose en el SATProblem ’#11: Nat === ’#0: Nat2 ^ ’#11: Nat === ’#1: Nat2 ^ ’#12: Nat === ’#0: Nat2 ^ ’#12: Nat === ’0. Zero ^ ’#13: Nat === ’X: Nat2 ^ ’#14: Nat === ’#2: Nat2 ^ ’_+_[ ’#13: Nat ,’#14: Nat] === ’#1: Nat2 Y a su vez en el iBool c( true ) ^ c( true ) ^ (c (0) === i (4) ) ^ (i (1) === i (2)) ^ (i (1) === i (3) ) ^ (i (2) === i (4)) ^ (i (3) === i (5) + i (7) ) ^ (i (5) === i (6)) ^ (i (7) === i (8) ) ^ i(1) >= c(0) ^ i(2) >= c (0) ^ i(3) >= c(0) ^ i(4) >= c(0) ^ i (5) >= c (0) ^ i(6) >= c(0) ^ i(7) >= c(0) ^ i (8) >= c (0) Que da como resultado true, por tanto, ´este estado puede ser satisfacible. A continuaci´on se comprueba si puede ser expandido y como s´ı que puede ser (restricci´on ’#2:Nat2 =?= ’ ** [’s [’0.Zero],’X:Nat2]) se debe crear un nuevo nivel sobre ´este y expandirlo. En este caso ´unicamente se genera un nuevo estado que ser´a a˜nadido al conjunto de estados. PairSet&PairSet&Counter: (’#0: Nat2 =?= ’#1: Nat2 ^ ’#0: Nat2 =?= ’0. Zero ^ ’#1: Nat2 =?= ’_+_[ ’X:Nat2 ,’#2: Nat2 ], ’#2: Nat2 =?= ’_+_[’X:Nat2 ,’_** _[ ’0. Zero ,’X: Nat2 ]] ,3) A continuaci´on se prosigue la ejecuci´on con el siguiente estado del conjunto envi´andose a la funci´on metasat-trans 5. Prototipo - Tercera parte 111 ’#0: Nat2 =?= ’#1: Nat2 ^ ’#0: Nat2 =?= ’_+_[’s_[’0. Zero ], ’#7: Nat2 ] ^ ’#1: Nat2 =?= ’_+_[ ’X:Nat2 ,’#8: Nat2 ] Generando el SATProblem ’#10: Nat =?= ’#1: Nat2 ^ ’#10: Nat =?= ’_+_[’#13: Nat , ’#14: Nat ] ^ ’#11: Nat =?= ’s_ [’0. Zero ] ^ ’#12: Nat =?= ’#7: Nat2 ^ ’#13: Nat =?= ’X: Nat2 ^ ’#14: Nat =?= ’#8: Nat2 ^ ’#9: Nat =?= ’#0: Nat2 ^ ’#9: Nat =?= ’#10: Nat ^ ’#9: Nat =?= ’_+_[ ’#11: Nat , ’#12: Nat ] Y el iBool final c( true ) ^ c( true ) ^ (i (4) === c (0) + i (1) + i (3)) ^ (i (6) === c (0) + i (2) + i (5) ) ^ (i (7) === c (0) + i (3) + i (5)) ^ (i (8) === c (0) + i (1) + i (2) + i (3) + i (5) ) ^ (i (9) === c (0) + i (1) + i (2) + i (3) + i (5) ) ^ (c (0) + c (1) === c (0) + i (1) + i (2) ) ^ (c (0) + i(1) + i(2) + i(3) + i(5) === c (0) + i(1) + i (2) + i(3) + i(5)) ^ (c (0) + i(1) + i(2) + i(3) + i(5) === c (0) + c(0) + c (0) + i(1) + i(2) + i (3) + i (5)) ^ (c (0) + i(1) + i(2) + i(3) + i(5) === c (0) + c(0) + c (0) + i(1) + i(2) + i (3) + i (5)) ^ i(1) >= c(0) ^ i(2) >= c (0) ^ i (3) >= c (0) ^ i (4) >= c (0) ^ i (5) >= c (0) ^ i(6) >= c(0) ^ i(7) >= c (0) ^ i (8) >= c (0) ^ i (9) >= c (0) La funci´on metasat-interface con este iBool devuelve true, por tanto hay que hacer el mismo proceso anterior. Como el estado se puede expandir, hay que llamar a la funci´on nextLevel y expandir los estados resultantes que son a˜nadidos al conjunto de estados global. (’#0: Nat2 =?= ’#1: Nat2 ^ ’#0: Nat2 =?= ’_+_[’s_[ ’0. Zero ],’#7: Nat2 ] ^ ’#1: Nat2 =?= ’_+_[ ’X:Nat2 ,’#8: Nat2 ],’#7: Nat2 =?= ’0. Zero ^ 8: Nat2 =?= ’_+_[’X:Nat2 ,’_** _[’0. Zero ,’X: Nat2 ]] ,9) ; (’#0: Nat2 =?= ’#1: Nat2 ^ ’#0: Nat2 =?= ’_+_[’s_[ ’0. Zero ],’#7: Nat2 ] ^ ’#1: Nat2 =?= ’_+_[ ’X:Nat2 ,’#8: Nat2 ],’#7: Nat2 =?= ’_+_[’s_ [’0. Zero], ’_** _[’ #13: Nat , ’s_[ ’0. Zero ]]] ^ ’#8: Nat2 =?= ’_+_[ ’X:Nat2 ,’_ **_[’0. Zero , ’X: Nat2 ]] ,14) Este proceso se realiza recursivamente hasta que se genera el siguiente estado no expansible (’#0: Nat2 =?= ’#1: Nat2 ^ ’#0: Nat2 =?= ’0. Zero ^ ’#1: Nat2 =?= ’_+_[ ’X:Nat2 ,’#2: Nat2 ] ^ ’#2: Nat2 =?= ’_+_[ ’X:Nat2 ,’#3: Nat2 ] ^ ’#3: Nat2 =?= ’0. Zero , emptyPairSet ,4) 112 5.3. Ejecuci´on del algoritmo Cuyo resultado final (depu´es de transformarse a SATProblem yiBool) es true y, como no se puede expandir, el algoritmo acaba y devuelve el valor true. A continuaci´on se puede observar c´omo se ejecutar´ıa el presente ejemplo de una forma gr´afica (Figura 5.1). 5. Prototipo - Tercera parte 113 Figura 5.1: Diagrama de ejecuci´on