z3

    6El calor

    1Respuesta

    necesita ayuda para entender la ecuación

    Tener la ecuación de Pell x*x - 193 * y*y = 1 en z3py: x = BitVec('x',64) y = BitVec('y',64) solve(x*x - 193 * y*y == 1, x > 0, y > 0) Resultado: [y = 2744248620923429728, x = 8169167793018974721]
    z3 z3py 2012-09-07

    9El calor

    1Respuesta

    Recorrido del árbol Z3_ast en C/C++

    En resumen, necesito poder atravesar el árbol Z3_ast y acceder a los datos asociados a sus nodos. Parece que no puede encontrar ninguna documentación/ejemplos sobre cómo hacer eso. Cualquier indicador
    z3 2012-09-19

    5El calor

    1Respuesta

    Rendimiento Z3 con aritmética no lineal

    Estamos teniendo problemas de rendimiento con lo que creo que es la parte de Z3 que trata la aritmética no lineal. Aquí hay un ejemplo concreto de Boogie, que cuando se verifica con Z3 (versión 4.1) t
    z3 2012-09-20

    6El calor

    1Respuesta

    ini-option CASE_SPLIT produce el modelo extraño

    Mientras trabajaba en mi tesis de maestría con z3, encontré algo extraño que no puedo entender. Espero que me puedas ayudar. :) El SMT-archivo que he escrito tiene este aspecto: (set-logic QF_UF) (se
    z3 2012-09-20

    6El calor

    1Respuesta

    z3python: conversión de cadena a expresión

    Dado que x,y,z = Ints('x y z') y una cadena como s='x + y + 2*z = 5', ¿hay una forma rápida de convertir s en una expresión z3? Si no es posible, entonces parece que tengo que hacer muchas operaciones
    python z3 2012-09-22

    5El calor

    1Respuesta

    Comprender la indexación de las variables enlazadas en Z3

    Estoy tratando de comprender cómo las variables vinculadas están indexadas en z3. Aquí en un fragmento en z3py y la salida correspondiente. (http://rise4fun.com/Z3Py/plVw1) x, y = Ints('x y') f1 = Fo
    z3 2012-08-05

    10El calor

    1Respuesta

    Z3/Python obteniendo valores de python del modelo

    ¿Cómo puedo obtener valores de python reales de un modelo Z3? E.g. p = Bool('p') x = Real('x') s = Solver() s.add(Or(x < 5, x > 10), Or(p, x**2 == 2), Not(p)) s.check() print s.model()[x] print
    python z3 z3py 2012-09-26

    12El calor

    1Respuesta

    (Z3Py) comprobando todas las soluciones para la ecuación

    En Z3Py, ¿cómo puedo verificar si la ecuación para las restricciones dadas tiene una sola solución? Si hay más de una solución, ¿cómo puedo enumerarlas?
    python z3 z3py 2012-08-08

    5El calor

    1Respuesta

    (Z3Py) función

    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
    python z3 2012-08-09

    5El calor

    1Respuesta

    TryFor en Z3 no deja de verificar después del límite de tiempo dado

    Estoy usando la API .NET de Z3. Cuando una instancia de un solucionador llamando: Solver s = ctx.MkSolver(ctx.TryFor(ctx.MkTactic("qflia"), TimeLimit)); y darle un TimeLimit de 60 segundos (60000 mi
    .net z3 2012-08-12
Última pregunta