From 4c6efbbc8bce874cedbf8ffb14a3b883df62e767 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Feb 2017 16:02:51 -0500 Subject: [PATCH] expose numerator/denominators for Martin and Giles Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index e5d0acaab..e60809646 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -758,6 +758,20 @@ namespace z3 { 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(m_ast); }