mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3 into new_ocaml_install
This commit is contained in:
commit
c33a8794a4
|
@ -285,6 +285,9 @@ class AstRef(Z3PPObject):
|
|||
def __repr__(self):
|
||||
return obj_to_string(self)
|
||||
|
||||
def __eq__(self, other):
|
||||
return self.eq(other)
|
||||
|
||||
def __hash__(self):
|
||||
return self.hash()
|
||||
|
||||
|
@ -531,6 +534,10 @@ class SortRef(AstRef):
|
|||
"""
|
||||
return not Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)
|
||||
|
||||
def __hash__(self):
|
||||
""" Hash code. """
|
||||
AstRef.__hash__(self)
|
||||
|
||||
def is_sort(s):
|
||||
"""Return `True` if `s` is a Z3 sort.
|
||||
|
||||
|
@ -793,6 +800,10 @@ class ExprRef(AstRef):
|
|||
a, b = _coerce_exprs(self, other)
|
||||
return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
|
||||
|
||||
def __hash__(self):
|
||||
""" Hash code. """
|
||||
AstRef.__hash__(self)
|
||||
|
||||
def __ne__(self, other):
|
||||
"""Return a Z3 expression that represents the constraint `self != other`.
|
||||
|
||||
|
|
Loading…
Reference in a new issue