Rm the slow solver code (#859)
This commit is contained in:
parent
0fc4bba9ad
commit
d5a692fc59
@ -358,16 +358,7 @@ class Z3Solver(Solver):
|
||||
value = self._getvalue(var)
|
||||
result.append(value)
|
||||
|
||||
# Reset the solver to avoid the incremental mode
|
||||
# Triggered with two consecutive calls to check-sat
|
||||
# Yet, if the number of solution is large, sending back
|
||||
# the whole formula is more expensive
|
||||
if len(result) < 50:
|
||||
self._reset(temp_cs.related_to(var))
|
||||
for value in result:
|
||||
self._assert(var != value)
|
||||
else:
|
||||
self._assert(var != value)
|
||||
self._assert(var != value)
|
||||
|
||||
if len(result) >= maxcnt:
|
||||
if silent:
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user