CODEWITHSUNDEEP
z3
user1487718
user1487718

Reputation:

How to rename a variable using Z3?

given an expression x'=x+1, I wish to rename x' to y. How to do using z3?

Upvotes: 0

Views: 550

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 461

There are a number of API functions that let you modify terms and substitute new subterms for old ones. They are described under the Modifiers section that contain the modifiers Z3_update_term, z3_substitute, and Z3_substitute_vars (there is also Z3_translate to port terms between two contexts). Here is the link:

http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa7497c70a827db2d61ba98889fe657b5

You can also traverse terms directly and write utilities to modify terms. The display_ast example shows the main cases for recursively traversing terms:

http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi__ex.html#ga807b5fe0e26acdec09e52a77318208d0

Upvotes: 2

Related Questions