(Z3Py) función

Question

declarando me gustaría encontrar C y T coeficientes en fórmula simple "número = x * c t +" para algunas de Resultados/x pares de dados:

from z3 import * 

x=Int('x') 
c=Int('c') 
t=Int('t') 

s=Solver() 

f = Function('f', IntSort(), IntSort()) 

# x*t+c = result 
# x, result = [(1,55), (12,34), (13,300)] 

s.add (f(x)==(x*t+c)) 
s.add (f(1)==55, f(12)==34, f(13)==300) 

t=s.check() 
if t==sat: 
    print s.model() 
else: 
    print t 

... pero el resultado es obviamente incorrecto Probablemente necesito averiguar cómo mapear los argumentos de la función.

¿Cómo debo definir la función correctamente?

Answer 1

La afirmación es f(x) == x*t + cno definir la función f para todos x. Solo dice que el valor de f para dadox es x*t + c. Z3 admite cuantificadores universales. Sin embargo, son muy caros, y Z3 no está completo cuando un conjunto de restricciones contiene cuantificadores universales ya que el problema se vuelve indecidible. Es decir, Z3 puede devolver unknown para este tipo de problema.

Tenga en cuenta que f es esencialmente un "macro" en su secuencia de comandos. En lugar de usar una función Z3 para codificar esta "macro", podemos crear una función de Python que haga el truco. Es decir, una función de Python que, dada una expresión Z3, devuelve una nueva expresión Z3. Aquí hay una nueva secuencia de comandos. El guión también está disponible en línea en: http://rise4fun.com/Z3Py/Yoi Aquí es otra versión del guión donde c y t son Real en lugar de Int: http://rise4fun.com/Z3Py/uZl

from z3 import * 

c=Int('c') 
t=Int('t') 

def f(x): 
    return x*t + c 

# data is a list of pairs (x, r) 
def find(data): 
    s=Solver() 
    s.add([ f(x) == r for (x, r) in data ]) 
    t = s.check() 
    if s.check() == sat: 
     print s.model() 
    else: 
     print t 

find([(1, 55)]) 
find([(1, 55), (12, 34)]) 
find([(1, 55), (12, 34), (13, 300)]) 

Observación: En el SMT 2.0 front-end, las macros se pueden definir utilizando el comando define-fun.