CODEWITHSUNDEEP
c#z3
JeffZhe
JeffZhe

Reputation: 11

What can z3' check() do?

I recently met a C# project that uses z3. I found that when the program runs to check(), it will last for a long long time so that the solution can't get the result. More specifically, this project has at least 40 constraints and at least 8 variables. The number of constraints and variables are multiples related to the input. It can be solved only when the input is one, but as long as the input is greater than one, it will be stuck in check(). However, in reality, my input must be greater than one.

I would like to ask what is the use of check(). If there are other methods to replace it, or even if it can be deleted. (I tried to delete it, and the surprising thing is that when the input is greater than one, the result can be obtained quickly.)

Upvotes: 0

Views: 158

Answers (1)

alias
alias

Reputation: 30428

The call to check makes sure the constraints given are satisfiable. If you don't call check, then obviously z3 will not check anything for you, so it isn't surprising that it goes faster.

Regarding if you can delete the call to check; well, you haven't told us what this project is, nor what it uses z3 for. But in general, no; you cannot remove the call to check. It'll return sat or unsat as a result (of course, it can also fail to terminate or return unknown depending on what constraints are asserted.) And you'd proceed according to the result of the call.

I'd advise looking at how your code uses the result of the call to check. Or contact the developer in the first place.

Upvotes: 2

Related Questions