Z3 ast_to_string() API with Subtraction

0
votes

The problem is pretty simple. I assert following statement in Z3 using the C API interface. 

(assert(>= (xA 1) (- (yB 0) period))))

Now Sometimes, I need to check what kind of assertions have been fed and the result in the SatSolver. I do this, by generating a text file by using ast_to_string() API. This API returns me above statement as - 

(assert(>= (xA 1) (+ (yB 0) (* -1 period))))

When I feed this file to the Sat Solver it complains me with the error -

(error "ERROR: line 150 column 56: could not locate id -1.")

So then, I have to manually fix all -1 in the code and run the sat solver. Is there any other way where I can avoid this?

1
z3
What do you mean by the SatSolver? Why do need to go through a text file? Can't just invoke it from the API as well? – Philippe

1 Answers

1
votes

Remember to set:

Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB2_COMPLIANT);

before using ast_to_string() in order that that output formulas comply with SMTLIB 2.0 format.