Z3Py: Erhalten der Funktion, die jedem Operator entspricht, z. '*', '==', '-'

Question

Ich möchte Gleichungen/Ungleichungen in Z3Py automatisch mit einem Algorithmus erzeugen, den ich entwickle. Um dies zu erreichen, muss ich Operatoren wie ==, +, * als Funktionen verwenden.

Zum Beispiel in Sympy, kann ich zwei Symbole hinzufügen, wie

import sympy as sp 
sp.Add(x, y) 

, die in x + y ergibt folgt.

Kann ich dasselbe in Z3Py tun?

Für Berechnungsgeschwindigkeit glaube ich, dass es keine gute Idee ist, von oder in eine Zeichenfolgendarstellung des Ausdrucks zu konvertieren.

Answer 1

Ich kann keine Dokumentation finden (und ich nehme an, Sie können auch nicht) für die direkte Unterstützung durch z3py jedoch alle impliziten Operationen in Python haben aufrufbaren Funktionen im Modul operator :

import operator 

x,y = Ints("x y") 

a = operator.add(x,y) 

, wenn Sie die Funktionen auf ihre Symbole zuordnen möchten Sie eine dict verwenden können:

ops = {"+":operator.add, "*":operator.mul} #etc. 

Answer 2

Wie wäre:

import z3 

x, y = z3.Ints('x y') 
print z3.ExprRef.__eq__(x, y)