Skip to content

introduce zero_expr() and one_expr() for number types #8441

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Sep 5, 2024
Merged

introduce zero_expr() and one_expr() for number types #8441

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 42 additions & 0 deletions src/util/mathematical_types.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]

#include "mathematical_types.h"

#include "std_expr.h"

/// Returns true if the type is a rational, real, integer, natural, complex,
/// unsignedbv, signedbv, floatbv or fixedbv.
bool is_number(const typet &type)
Expand All @@ -21,3 +23,43 @@ bool is_number(const typet &type)
id == ID_natural || id == ID_complex || id == ID_unsignedbv ||
id == ID_signedbv || id == ID_floatbv || id == ID_fixedbv;
}

constant_exprt integer_typet::zero_expr() const
{
return constant_exprt{ID_0, *this};
}

constant_exprt integer_typet::one_expr() const
{
return constant_exprt{ID_1, *this};
}

constant_exprt natural_typet::zero_expr() const
{
return constant_exprt{ID_0, *this};
}

constant_exprt natural_typet::one_expr() const
{
return constant_exprt{ID_1, *this};
}

constant_exprt rational_typet::zero_expr() const
{
return constant_exprt{ID_0, *this};
}

constant_exprt rational_typet::one_expr() const
{
return constant_exprt{ID_1, *this};
}

constant_exprt real_typet::zero_expr() const
{
return constant_exprt{ID_0, *this};
}

constant_exprt real_typet::one_expr() const
{
return constant_exprt{ID_1, *this};
}
14 changes: 14 additions & 0 deletions src/util/mathematical_types.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,13 +17,18 @@ Author: Daniel Kroening, [email protected]
#include "invariant.h"
#include "type.h"

class constant_exprt;

/// Unbounded, signed integers (mathematical integers, not bitvectors)
class integer_typet : public typet
{
public:
integer_typet() : typet(ID_integer)
{
}

constant_exprt zero_expr() const;
constant_exprt one_expr() const;
};

/// Natural numbers including zero (mathematical integers, not bitvectors)
Expand All @@ -33,6 +38,9 @@ class natural_typet : public typet
natural_typet() : typet(ID_natural)
{
}

constant_exprt zero_expr() const;
constant_exprt one_expr() const;
};

/// Unbounded, signed rational numbers
Expand All @@ -42,6 +50,9 @@ class rational_typet : public typet
rational_typet() : typet(ID_rational)
{
}

constant_exprt zero_expr() const;
constant_exprt one_expr() const;
};

/// Unbounded, signed real numbers
Expand All @@ -51,6 +62,9 @@ class real_typet : public typet
real_typet() : typet(ID_real)
{
}

constant_exprt zero_expr() const;
constant_exprt one_expr() const;
};

/// A type for mathematical functions (do not confuse with functions/methods
Expand Down