I'm attempting to implement the quick-explain algorithm with the 'nlsat' solver. As the algorithm requires to solve a subset of the original constraint set many times, I decide to use the push/pop function in z3 c++ interface.(check(assumptions) does not work in nlsat solver). A selector variable is used to imply adding/removing a constraint.
But I experienced a problem when solving a constraint set. z3 is able to tell me the whole constraint set is unsat in less than 1 minute. But when checking a subset of the original constraint set, it didn't give a result for more than 1 hour.
The whole constraint set can be solved in less than 1 minute
a subset of the original constraint set can't get a result for more than 1 hour
What changes the performance dramatically? In general, what affects the performance of nlsat solver?
Any suggestion is appreciated.
