Skip to content
Snippets Groups Projects
Commit d62656ca authored by Jan Gruteser's avatar Jan Gruteser
Browse files

add Infinity definition from Reals module

parent 6a13701e
Branches
Tags
No related merge requests found
Pipeline #148667 passed
...@@ -18,6 +18,7 @@ public interface BBuildIns extends ToolGlobals { ...@@ -18,6 +18,7 @@ public interface BBuildIns extends ToolGlobals {
UniqueString OP_nat = UniqueString.uniqueStringOf("Nat"); UniqueString OP_nat = UniqueString.uniqueStringOf("Nat");
UniqueString OP_int = UniqueString.uniqueStringOf("Int"); UniqueString OP_int = UniqueString.uniqueStringOf("Int");
UniqueString OP_real = UniqueString.uniqueStringOf("Real"); UniqueString OP_real = UniqueString.uniqueStringOf("Real");
UniqueString OP_infinity = UniqueString.uniqueStringOf("Infinity");
UniqueString OP_bool = UniqueString.uniqueStringOf("BOOLEAN"); UniqueString OP_bool = UniqueString.uniqueStringOf("BOOLEAN");
UniqueString OP_true = UniqueString.uniqueStringOf("TRUE"); UniqueString OP_true = UniqueString.uniqueStringOf("TRUE");
UniqueString OP_false = UniqueString.uniqueStringOf("FALSE"); UniqueString OP_false = UniqueString.uniqueStringOf("FALSE");
...@@ -98,4 +99,5 @@ public interface BBuildIns extends ToolGlobals { ...@@ -98,4 +99,5 @@ public interface BBuildIns extends ToolGlobals {
int B_OPCODE_real = B_OPCODE_assert + 1; int B_OPCODE_real = B_OPCODE_assert + 1;
int B_OPCODE_realdiv = B_OPCODE_assert + 2; int B_OPCODE_realdiv = B_OPCODE_assert + 2;
int B_OPCODE_infinity = B_OPCODE_assert + 3;
} }
...@@ -29,6 +29,7 @@ public class BBuiltInOPs implements BBuildIns { ...@@ -29,6 +29,7 @@ public class BBuiltInOPs implements BBuildIns {
B_Opcodes.put(OP_nat, B_OPCODE_nat); B_Opcodes.put(OP_nat, B_OPCODE_nat);
B_Opcodes.put(OP_int, B_OPCODE_int); B_Opcodes.put(OP_int, B_OPCODE_int);
B_Opcodes.put(OP_real, B_OPCODE_real); B_Opcodes.put(OP_real, B_OPCODE_real);
B_Opcodes.put(OP_infinity, B_OPCODE_infinity);
B_Opcodes.put(OP_string, B_OPCODE_string); B_Opcodes.put(OP_string, B_OPCODE_string);
B_Opcodes.put(OP_finite, B_OPCODE_finite); B_Opcodes.put(OP_finite, B_OPCODE_finite);
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment