mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
remove trc from C++ and python
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
86b98e3477
commit
aafb16e8ed
|
@ -637,10 +637,6 @@ namespace z3 {
|
|||
Z3_func_decl tc = Z3_mk_transitive_closure(ctx(), *this); check_error(); return func_decl(ctx(), tc);
|
||||
}
|
||||
|
||||
func_decl transitive_reflexive_closure(func_decl const& f) {
|
||||
Z3_func_decl tc = Z3_mk_transitive_reflexive_closure(ctx(), *this); check_error(); return func_decl(ctx(), tc);
|
||||
}
|
||||
|
||||
bool is_const() const { return arity() == 0; }
|
||||
|
||||
expr operator()() const;
|
||||
|
|
|
@ -10403,9 +10403,3 @@ def TransitiveClosure(f):
|
|||
"""
|
||||
return FuncDeclRef(Z3_mk_transitive_closure(f.ctx_ref(), f.ast), f.ctx)
|
||||
|
||||
def TransitiveReflexiveClosure(f):
|
||||
"""Given a binary relation R, such that the two arguments have the same sort
|
||||
create the transitive reflexive closure relation R*.
|
||||
The transitive reflexive closure R* is a new relation.
|
||||
"""
|
||||
return FuncDeclRef(Z3_mk_transitive_reflexive_closure(f.ctx_ref(), f.ast), f.ctx)
|
||||
|
|
Loading…
Reference in a new issue