mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
adding orphaned function declaration #1574
This commit is contained in:
parent
28fbcd7687
commit
6078d24016
|
@ -2680,6 +2680,9 @@ namespace z3 {
|
|||
inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range) {
|
||||
return range.ctx().function(name, d1, d2, d3, d4, d5, range);
|
||||
}
|
||||
inline func_decl function(char const& name, sort_vector const& domain, sort const& range) {
|
||||
return range.ctx().function(name, domain, range);
|
||||
}
|
||||
|
||||
inline expr select(expr const & a, expr const & i) {
|
||||
check_context(a, i);
|
||||
|
|
Loading…
Reference in a new issue