mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

use template<> syntax

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-07-15 11:11:37 -07:00
parent ff104c4b13
commit 5f4ca8c6fc
1 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/sls/sls_arith_base.cpp
View file

@ -371,6 +371,7 @@ namespace sls {
ineq.m_args.push_back({ c, v });
}
template<>
bool arith_base<checked_int64<true>>::is_num(expr* e, checked_int64<true>& i) {
rational r;
if (a.is_numeral(e, r)) {
@ -382,6 +383,7 @@ namespace sls {
return false;
}
template<>
bool arith_base<rational>::is_num(expr* e, rational& i) {
return a.is_numeral(e, i);
}
@ -392,10 +394,12 @@ namespace sls {
return false;
}
template<>
expr_ref arith_base<rational>::from_num(sort* s, rational const& n) {
return expr_ref(a.mk_numeral(n, s), m);
}
template<>
expr_ref arith_base<checked_int64<true>>::from_num(sort* s, checked_int64<true> const& n) {
return expr_ref(a.mk_numeral(rational(n.get_int64(), rational::i64()), s), m);
}