Codificar la siguiente ecuación sobre enteros en Z3 para encontrar una solución:
Considerar el rompecabezas siguiente:
Además, alguien toma agua, alguien posee una zebra, y cada una de las cinco casas está pintada de un color distinto, y sus habitantes son de nacionalidades distintas, poseen mascotas distintas, toman bebidas distintas y fuman distintas marcas de cigarillos.
(= Ingles Rojo)
.(or (= Noruego (- Azul 1)) (= Noruego (+ Azul 1)))
. (Ayuda: en este caso como los otros dados en el enunciado, no hay overflow, o sea esta restricción sirve tal cual sin fijarse que no superemos el valor 5.)(distinct t1 t2 ... tn)
para especificar que todas las entidades de mismo tipo (color, casa, etc.) tienen un valor distinto.Considerá la operación siguiente: (x + y - ((x & y) << 1))
donde << n
es la operación "shift left n veces".
Demostrá que esta operación es equivalente a la operación x xor y
sobre cualquier par (x, y) de vectores de bits de tamaño 64.
Ayuda: el vector de 64 bits que contiene solo el valor 1 se puede escribir directamente (_ bv1 64))
.
El generador pseudoaleatorio por defecto de la librería estándar de C es basado sobre un LCG (Linear Congruential Generator). Sus debilidades son conocidas, veamos si podemos encontrar sus valores de estados interno solo viendo la salida de un programa y conociendo la implementación del LCG. Vamos a definir las relaciones entre los estados internos del LCG usando Z3. Este es un programa de prueba:
#include <stdlib.h>
#include <stdio.h>
#include <time.h>
main(){
int i;
srand(time(NULL));
for (i=0; i<10; i++)
printf ("%d\n", rand()%100);
}
Imprime 10 números entre 0 y 99:
37
29
74
95
98
40
23
58
61
17
Definamos obs2 = 29, obs3 = 74, obs9 = 61.
Veamos si observando solo 8 valores (de 29 a 61) podemos predecir el siguiente (17).
Este programa está compilado con MSVC 2013 (su LCG es más simple que el de GLib). Usemos un desensemblador para conocer las operaciones y constantes que usa:
.text:0040112E rand proc near
.text:0040112E call __getptd
.text:00401133 imul ecx, [eax+0x14], 214013
.text:0040113A add ecx, 2531011
.text:00401140 mov [eax+14h], ecx
.text:00401143 shr ecx, 16
.text:00401146 and ecx, 7FFFh
.text:0040114C mov eax, ecx
.text:0040114E retn
.text:0040114E rand endp
Estamos listos para usar Z3.
state1
a state10
, output_prev
y output_next
.bvurem
es el equivalente en SMTLIB de la operacion módulo sobre vectores de bits). En el script SMTLIB, no declarar los obsi sino usar directamente sus valores numéricos como constantes.sat
[state3 = 2276903645,
state4 = 1467740716,
state5 = 3163191359,
state7 = 4108542129,
state8 = 2839445680,
state2 = 998088354,
state6 = 4214551046,
state1 = 1791599627,
state9 = 548002995,
output_next = 17,
output_prev = 37,
state10 = 1390515370]
Por defecto, Z3 muestra los vectores de bits sin convertirlos a enteros.
Para que Z3 muestre los vectores de bits como enteros, agregar
lo siguiente a la fórmula: `(set-option :pp.bv-literals false)`.