mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

expose numerator/denominators for Martin and Giles

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-02-11 16:02:51 -05:00
parent b42973152f
commit 4c6efbbc8b
1 changed files with 14 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/api/c++/z3++.h
View file

@ -758,6 +758,20 @@ namespace z3 {
return result; return result;
} }
expr numerator() const {
assert(is_numeral());
Z3_ast r = Z3_get_numerator(ctx(), m_ast);
check_error();
return expr(ctx(),r);
}
expr denominator() const {
assert(is_numeral());
Z3_ast r = Z3_get_denominator(ctx(), m_ast);
check_error();
return expr(ctx(),r);
}
operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); } operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }