Added assumptions into unsat cores when solving under assumptions is used #680
Conversation
marcogario
left a comment
marcogario
left a comment
There was a problem hiding this comment.
LGTM.
could you update the PR description to clarify whether this is a bug or not?
Is the expectation that we always return assumptions in unsat cores or not?
I have some doubts about returning assumptions in the named unsat core case, but I do not see any harm in keeping this.
| btor_assumptions = [self.converter.convert(a) for a in assumptions] | ||
| self.btor.Assume(*btor_assumptions) | ||
| self._last_assumptions = list(assumptions) |
There was a problem hiding this comment.
If assumption is an iterator, we will consume it in L234, and then L238 will return an empty list.
Shall we do list(assumptions) earlier?
| self.mgr = environment.formula_manager | ||
| self.declarations = {} | ||
| self._named_assertions = {} | ||
| self._last_assumptions = [] |
There was a problem hiding this comment.
Maybe just assumptions? We cannot have multiple assumptions at the same time, right? That's why we are satisfied with storing only one set of assumptions.
| # relies on this assertion stack being ordered | ||
| assert isinstance(self._assertion_stack, list) | ||
| btor_assertions = [self.converter.convert(a) for a in self._assertion_stack] | ||
| lst = self._assertion_stack + self._last_assumptions |
There was a problem hiding this comment.
Maybe:
| lst = self._assertion_stack + self._last_assumptions | |
| assertions = self._assertion_stack + self._last_assumptions |
| if self.options.unsat_cores_mode == "named": | ||
| unsat_core = {} | ||
| # relies on this assertion stack being ordered | ||
| lst = list(self._named_assertions.keys()) + self._last_assumptions |
There was a problem hiding this comment.
As above, let's use a more meaningful name here.
| for a, in_core in zip(lst, in_unsat_core): | ||
| if in_core: | ||
| name = self._named_assertions[a] | ||
| name = self._named_assertions.get(a, '_a_%d' % cnt) |
There was a problem hiding this comment.
We are making up the name for the assumption? If so, how is the caller supposed to link this information back? I wonder if in the named case returning the assumptions makes sense.
No description provided.