From 2db2383b09fb4036c14ca72c8f56ab196a06129b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 18 Jul 2013 17:41:21 -0700 Subject: [PATCH] Add goodies for extended numerals Signed-off-by: Leonardo de Moura --- src/numerics/xnumeral.h | 264 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 264 insertions(+) create mode 100644 src/numerics/xnumeral.h diff --git a/src/numerics/xnumeral.h b/src/numerics/xnumeral.h new file mode 100644 index 000000000..598443f23 --- /dev/null +++ b/src/numerics/xnumeral.h @@ -0,0 +1,264 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once + +#include +#include "numeric_traits.h" +#include "debug.h" + +namespace lean { + +// Goodies (templates) for computing with extended numeral. +// Given a numeric set S, the extended set S+ is S union {-oo, +oo}, +// where -oo is a new number smaller than any number in S, and +oo is a number bigger than +// any number in S. +// +// We do not provide a class extended numeral, since we do not want to commit +// with any particular representation. +// We just provide functions for computing with them. + +enum xnumeral_kind { XN_MINUS_INFINITY, XN_NUMERAL, XN_PLUS_INFINITY }; + +template +bool is_zero(T const & a, xnumeral_kind ak) { + return ak == XN_NUMERAL && numeric_traits::is_zero(a); +} + +template +bool is_pos(T const & a, xnumeral_kind ak) { + return ak == XN_PLUS_INFINITY || (ak == XN_NUMERAL && numeric_traits::is_pos(a)); +} + +template +bool is_neg(T const & a, xnumeral_kind ak) { + return ak == XN_MINUS_INFINITY || (ak == XN_NUMERAL && numeric_traits::is_neg(a)); +} + +inline bool is_infinite(xnumeral_kind ak) { + return ak != XN_NUMERAL; +} + +template +void set(T & a, xnumeral_kind & ak, T const & b, xnumeral_kind bk) { + a = b; + ak = bk; +} + +template +void reset(T & a, xnumeral_kind & ak) { + numeric_traits::reset(a); + ak = XN_NUMERAL; +} + +template +void neg(T & a, xnumeral_kind & ak) { + switch (ak) { + case XN_MINUS_INFINITY: + ak = XN_PLUS_INFINITY; + break; + case XN_NUMERAL: + numeric_traits::neg(a); + break; + case XN_PLUS_INFINITY: + ak = XN_MINUS_INFINITY; + break; + } +} + +template +void inv(T & a, xnumeral_kind & ak) { + lean_assert(numeral_manager::field()); + switch (ak) { + case XN_MINUS_INFINITY: + ak = XN_NUMERAL; + numeric_traits::reset(a); + break; + case XN_NUMERAL: + lean_assert(!numeric_traits::is_zero(a)); + numeric_traits::inv(a); + break; + case XN_PLUS_INFINITY: + ak = XN_NUMERAL; + numeric_traits::reset(a); + break; + } +} + +template +void add(T & r, xnumeral_kind & rk, T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) { + lean_assert(!(ak == XN_MINUS_INFINITY && bk == XN_PLUS_INFINITY)); // result is undefined + lean_assert(!(ak == XN_PLUS_INFINITY && bk == XN_MINUS_INFINITY)); // result is undefined + if (ak != XN_NUMERAL) { + numeric_traits::reset(r); + rk = ak; + } + else if (bk != XN_NUMERAL) { + numeric_traits::reset(r); + rk = bk; + } + else { + r = a + b; + rk = XN_NUMERAL; + } +} + +template +void sub(T & r, xnumeral_kind & rk, T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) { + lean_assert(!(ak == XN_MINUS_INFINITY && bk == XN_MINUS_INFINITY)); // result is undefined + lean_assert(!(ak == XN_PLUS_INFINITY && bk == XN_PLUS_INFINITY)); // result is undefined + if (ak != XN_NUMERAL) { + lean_assert(bk != ak); + numeric_traits::reset(r); + rk = ak; + } + else { + switch (bk) { + case XN_MINUS_INFINITY: + numeric_traits::reset(r); + rk = XN_PLUS_INFINITY; + break; + case XN_NUMERAL: + r = a - b; + rk = XN_NUMERAL; + break; + case XN_PLUS_INFINITY: + numeric_traits::reset(r); + rk = XN_MINUS_INFINITY; + break; + } + } +} + +template +void mul(T & r, xnumeral_kind & rk, T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) { + if (is_zero(a, ak) || is_zero(b, bk)) { + numeric_traits::reset(r); + rk = XN_NUMERAL; + } + else if (is_infinite(ak) || is_infinite(bk)) { + if (is_pos(a, ak) == is_pos(b, bk)) + rk = XN_PLUS_INFINITY; + else + rk = XN_MINUS_INFINITY; + numeric_traits::reset(r); + } + else { + rk = XN_NUMERAL; + r = a * b; + } +} + +template +void div(T & r, xnumeral_kind & rk, T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) { + lean_assert(!is_zero(b, bk)); + if (is_zero(a, ak)) { + lean_assert(!is_zero(b, bk)); + numeric_traits::reset(r); + rk = XN_NUMERAL; + } + else if (is_infinite(ak)) { + lean_assert(!is_infinite(bk)); + if (is_pos(a, ak) == is_pos(b, bk)) + rk = XN_PLUS_INFINITY; + else + rk = XN_MINUS_INFINITY; + numeric_traits::reset(r); + } + else if (is_infinite(bk)) { + lean_assert(!is_infinite(ak)); + numeric_traits::reset(r); + rk = XN_NUMERAL; + } + else { + rk = XN_NUMERAL; + c = a / b; + } +} + +template +void power(T & a, xnumeral_kind & ak, unsigned n) { + switch (ak) { + case XN_MINUS_INFINITY: + if (n % 2 == 0) + ak = XN_PLUS_INFINITY; + break; + case XN_NUMERAL: + numeric_traits::power(a, n); + break; + case XN_PLUS_INFINITY: + break; // do nothing + } +} + +/** + \brief Return true if (a,ak) == (b,bk). +*/ +template +bool eq(T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) { + if (ak == XN_NUMERAL) { + return bk == XN_NUMERAL && a == b; + } + else { + return ak == bk; + } +} + +template +bool neq(T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) { + return !eq(m, a, ak, b, bk); +} + +template +bool lt(T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) { + switch (ak) { + case XN_MINUS_INFINITY: + return bk != XN_MINUS_INFINITY; + case XN_NUMERAL: + switch (bk) { + case XN_MINUS_INFINITY: + return false; + case XN_NUMERAL: + return a < b; + case XN_PLUS_INFINITY: + return true; + default: + UNREACHABLE(); + return false; + } + case XN_PLUS_INFINITY: + return false; + default: + lean_unreachable(); + return false; + } +} + +template +bool gt(T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) { + return lt(m, b, bk, a, ak); +} + +template +bool le(T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) { + return !gt(m, a, ak, b, bk); +} + +template +bool ge(T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) { + return !lt(m, a, ak, b, bk); +} + +template +void display(std::ostream & out, T const & a, xnumeral_kind ak) { + switch (ak) { + case XN_MINUS_INFINITY: out << "-oo"; break; + case XN_NUMERAL: out << a; break; + case XN_PLUS_INFINITY: out << "+oo"; break; + } +} + +}