CODEWITHSUNDEEP
z3
Radu Stoenescu
Radu Stoenescu

Reputation: 3205

Duplicate a Z3Context

I need to be able to duplicate a Z3Context instance in order to be able to add new definitions to one instance without affecting the other.

Is this possible ?

What part of the API should I look at ?

I mention that I'm using the Java API.

Thanks

Upvotes: 0

Views: 200

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

There Is no method for cloning contexts. It would also be somewhat hard to use: after cloning a context, what would be the pointers corresponding to terms and formulas in the new context? Instead there are various translation methods that let you import terms, formulas, solvers and goals between contexts. For example, use

       Z3_ast Z3_API Z3_translate(Z3_context source, Z3_ast a, Z3_context target);

to copy a term/formula between two contexts. The 

     Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target);

method lets you clone a solver. You can clone the solver between two different contexts or the same context, especially if you are just using cloning for exploring different variants of assertions.

Upvotes: 1

Related Questions