Scenario
In the world of mathematical optimization, the need to model inequality g_k(...) constraints arises. g_k(...) can sometimes be a function call to an external program that is, for all intents and purposes, a blackbox. Simply finding satisfactory answers can be beneficial for certain engineering analysis.
Example
An example application of the above scenario for Reals, but could also be Ints or Booleans:
min f(x,y)
g1(x,y) <= 25
g2(x,y) >= 7.7
x,y ε Real
x >= 0
x <= 50.0
y >= 0
y <= 5.0
g1 and g2 are Python functions that call an external program. The functions return a real number. Following this Z3 format to find a model that simply satisfies the constraints would be represented as:
from z3 import *
from ExternalCodes import Code1, Code2 #For example, these could be Python wrappers to C++ codes
def g_1(x, y):
return Code1(x, y) #isinstance(Code1(x,y), float) == True
def g_2(x, y):
return Code2(x, y) #isinstance(Code2(x,y), float) == True
s = Solver()
x, y = Reals('x y')
s.add(g_1(x, y) <= 25.0)
s.add(g_2(x, y) >= 7.7)
s.add(x <= 0)
s.add(50.0 <= x)
s.add(y <= 0)
s.add(5.0 <= y)
m = s.model()
print(m)
Questions
- I understand that the type returned by Code1 and Code2 need to be Z3 datatypes. How do I convert Python types to Z3 types like mentioned in the 1st comment
- How is Z3 used to find a sat model when constraints may need to be evaluated in external code, i.e. declare functions? I understand it may be inefficient, I would loose heuristics, etc., because it is undecidable, but for certain engineering applications, enumerating a sat solution, if it exists, is more advantageous than employing an optimizer from the get-go.
Relevant answers
-
-Not quite the same application. I'm curious if, 4 years later, is this answer still the case, but this is not my question.
Can Z3 call an externally defined function?
-In essence, the same question. No Z3Py answer, and unfortunately, the Rise4fun link is broken. I also cannot find the mentioned F#/.NET example in the Github repo
