как передать выражение в качестве аргумента функции без ее оценки - PullRequest
Новая
       33

как передать выражение в качестве аргумента функции без ее оценки

0 голосов
/ 11 апреля 2020

Сначала посмотрите соответствующий код пользователя для запуска z3-solver. Это работает нормально, и решатель возвращает некоторые значения после вычисления выражения: 

# see source at https://github.com/Z3Prover/z3
# the relevant code is at: z3-master/src/api/python/z3/z3.py
# pip install z3-solver
from z3 import *
x = Int('x')
#print(type(x)) # <class 'z3.z3.ArithRef'>
y = Int('y')
s = Solver()
# print(type(s)) # <class 'z3.z3.Solver'>
s.add(x > 10)  # this works
s.add(y == x + 2)
print(s)
print(s.check())
print(s.model())

Теперь моя короткая попытка написать оценщик, такой как z3: 

class Int():
    def __init__(self,name):
        self.name = name
        self.value = None
    def do_print(self):
        print('Rand({})'.format(self.name))
    def __str__(self):
        return(str(self.value))

class Solver():
    def add(self, *argv):
        self.args = []
        for arg in argv:
            self.args.append(arg)
    def do_print(self):
        print('Constr(',end='')
        for arg in self.args:
            print(arg)
        print(')')

x = Int('x')
s=Solver()
s.add(x > 10) # this does not work - but why is same kind of code in z3 working?
# err: TypeError: '<' not supported between instances of 'Int' and 'int'
x.do_print()
s.do_print()

Я получаю ошибку в строке s.add (). Я понимаю ошибку, что объект «х» нельзя сравнить с целым числом. Это происходит потому, что выражение в этой строке вычисляется перед вызовом s.add ().

Но мой вопрос - как z3-solver обходит эту ошибку? Как он может передать аргументы add () без его предварительной оценки?

Как исправить проблему в моем коде и передать выражение в s.add () без его предварительной оценки?

...