z3: conversion of expressions with transcendental functions from z3py to smt-lib2

Question

As per my knowledge, since z3 doesn't recognize transcendental functions its throwing me an error while conversion using following code.

def convertor(f, status="unknown", name="benchmark", logic=""):
  v = (Ast * 0)()
  if isinstance(f, Solver):
    a = f.assertions()
    if len(a) == 0:
      f = BoolVal(True)
    else:
      f = And(*a)
  return Z3_benchmark_to_smtlib_string(f.ctx_ref(), name, logic, status, "", 0, v, f.as_ast())


pi, EI, kA , kB, N = Reals('pi EI kA kB N')

s= Solver()
s.add(pi == 3.1415926525)
s.add(EI == 175.2481)
s.add(kA>= 0)
s.add(kA<= 100)
s.add(kB>= 0)
s.add(kB<= 100)
s.add(N>= 100)
s.add(N<= 200)

please change the path of the input file "beamfinv3.bch", which can be found at: link

continue_read=False
input_file = open('/home/mani/downloads/new_z3/beamfinv3.bch', 'r')
for line in input_file:
    if line.strip()=="Constraints":
        continue_read=True
        continue
    if line.strip()=="end":
         continue_read=False
    if continue_read==True:
        parts = line.split(';')
        if (parts[0]!="end"):              
         #print parts[0]
         s.add(eval(parts[0]))

input_file.close()
file=open('cyber.smt2','w')    
result=convertor(s, logic="None")
file.write (result)

error:

File "<string>", line 1, in <module>
NameError: name 'sin' is not defined

Any way out? or help?

Thanks.

score 0 · Answer 1 · edited May 23 '17 at 12:29

0

The core of this problem is that eval tries to execute a Python script, i.e., all functions that occur within parts[0] must have a corresponding Python function of the same name, which is not the case for the trigonometric functions (the are neither in the Python API nor the C API, the former being based on the latter). For now you could try to add those functions yourself, perhaps with an implementation based on parse_smt2_string, or perhaps by replacing the Python strings with SMT2 strings altogether.

Z3 can represent expressions containing trigonometric functions, but it will refuse to do so when the logic is set to something; see arith_decl_plugin. I don't know Python well enough, but it might have to be None instead of "".

While Z3 can represent these expressions, it's probably not very good at solving them. See comments on the limitations in Can Z3 handle sinusoidal and exponential functions, Z3 supports for nonlinear arithmetics, and Z3 Performance with Non-Linear Arithmetic.

edited May 23 '17 at 12:29

Community

1
1

answered Oct 05 '15 at 19:52

Christoph Wintersteiger

8,234
1
16
30

Thanks, but still does not work, throws the same error. – Rauf Oct 05 '15 at 20:08
What else did you try and which expressions are you feeding into it? – Christoph Wintersteiger Oct 05 '15 at 21:48
I tried changing "" to None/none/"None" etc. I dont exactly know how: https://github.com/Z3Prover/z3/blob/master/src/ast/arith_decl_plugin.cpp#L550 works, but If trignometric functions are define then it shouldn't throw me any error and it should recognize "sin". The expressions I am feeding it are pretty huge. – Rauf Oct 05 '15 at 22:03
If you can create a small repro, it would help. – Nikolaj Bjorner Oct 05 '15 at 23:03
I have updated the post and have provided the link to the input file. please have a look at it – Rauf Oct 09 '15 at 20:14

z3: conversion of expressions with transcendental functions from z3py to smt-lib2

1 Answers1