1

Can I create a new solver from an old one in Z3? In Z3, the standard process to create a solver is like the following

context ctx; solver sv(ctx);

After a process of inserting assertions and checking, I want to create a new solver, say sv2, that is equivalent to sv. But I cannot find the supporting function or API. Solving is expensive, that is way I do not want to create sv2 from scratch.

Ting Chen

Ting Chen
  • 79
  • 2
  • What exactly do you mean by `equivalent`? You can create as many solvers as you like, but they will not contain the assertions of the first one. You can of course copy those over to the new solver, but I can't see how that could make anything cheaper. – Christoph Wintersteiger Oct 05 '15 at 11:53
  • Yes, as you say, copy all assertions from old solver to new one does not make anything cheaper. I believe in this way, I have to solve the assertions what I have already solved in old solver. So is there a cheap way. I mean creating a new solver from an old one, while maintaining the status, so as to solve incrementally. – Ting Chen Oct 05 '15 at 12:21

1 Answers1

2

The usual ways of doing that is either by using push/pull or to solve under assumptions (all on the same solver and context), see Soft/Hard constraints in Z3, Z3/SMT: When should I prefer push/pop to reset?. Also, search for those keywords, there are many questions and answers regarding this issue.

Community
  • 1
  • 1
Christoph Wintersteiger
  • 8,234
  • 1
  • 16
  • 30