Z3py에서 함수에 값을 할당 (어설트) 할 수 있습니까?

Question

다음 Z3 제약 조건을 Z3py (Python API)로 변환하려면 어떻게해야합니까?

 (declare-datatypes() ((S a b c d e f g))) 

     (declare-fun fun1 (S) Bool) 
     (declare-fun fun2 (S S) Bool) 


     (assert (forall ((x S)) (= (fun1 x) 
     (or 
     (= x a) 
     (= x b) 
     (= x c) 
     (= x d) 
     (= x e) 
     (= x f) 
     (= x g) 
     )))) 

     (assert (forall ((y1 S) (y2 S)) (= (fun2 y1 y2) 
     (or 
     (and (= y1 a) (= y2 b)) 
     (and (= y1 c) (= y2 d)) 
     (and (= y2 e) (= y2 f)) 
     )))) 

Answer 1

다음과 같은 방법으로 인코딩 할 수 있습니다

from z3 import * 

S, (a, b, c, d, e, f, g) = EnumSort('S', ['a', 'b', 'c', 'd', 'e', 'f', 'g']) 

fun1 = Function('fun1', S, BoolSort()) 
fun2 = Function('fun2', S, S, BoolSort()) 

s = Solver() 

x = Const('x', S) 
s.add(ForAll([x], fun1(x) == Or(x == a, x == b, x == c, x == d, x == e, x == f, x == g, x == e))) 

y1, y2 = Consts('y1 y2', S) 
s.add(ForAll([y1, y2], fun2(y1, y2) == Or(And(y1 == a, y2 == b), And(y1 == c, y2 == d), And(y1 == e, y2 == f)))) 

print(s.check()) 
print(s.model()) 

참고 fun1 및 fun2은 기본적으로 매크로 것을. 따라서 한정 기호는 사용하지 말고 다음과 같이 정의 할 수 있습니다.

def fun1(x): 
    return Or(x == a, x == b, x == c, x == d, x == e, x == f, x == g, x == e) 

def fun2(y1, y2): 
    return Or(And(y1 == a, y2 == b), And(y1 == c, y2 == d), And(y1 == e, y2 == f))