Skip to content

Commit

Permalink
🍎: added has_single_sol API in solver plugin
Browse files Browse the repository at this point in the history
Signed-off-by: degrigis <degrigis@ucsb.edu>
  • Loading branch information
degrigis committed Aug 5, 2024
1 parent 5e3b64f commit 01b80bc
Showing 1 changed file with 9 additions and 0 deletions.
9 changes: 9 additions & 0 deletions greed/state_plugins/solver.py
Original file line number Diff line number Diff line change
Expand Up @@ -279,6 +279,15 @@ def is_formula_false(self, formula: BoolTerm) -> bool:
"""
return self._solver.is_formula_false(formula)

def has_single_sol(self, term: BVTerm) -> bool:
"""
Check if a term has a single solution.
Args:
term: The term to check.
"""
raw_sol = self.eval(term, raw=True)
return not self.is_formula_sat(NotEqual(term, raw_sol))

def eval(self, term, raw=False):
"""
Evaluate a term.
Expand Down

0 comments on commit 01b80bc

Please sign in to comment.