Add mkInteger to the API (#5274)

This PR adds mkInteger to the API and update mkReal to ensure that the returned term has real sort.
The parsers are modified to parse numbers like "0" "5" as integers and "0.0" and "15.0" as reals.
This means subtyping is effectively eliminated from all theories except arithmetic.
Other changes:

Term::isValue is removed which was introduced to support parsing for constant arrays. It is no longer needed after this PR.
Benchmarks are updated to match the changes in the parsers
Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu

20 files changed, 40 insertions, 40 deletions

diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp
index 191bb83bd..307c30709 100644
--- a/examples/api/combination.cpp
+++ b/examples/api/combination.cpp
@@ -58,8 +58,8 @@ int main()
   Term p = slv.mkConst(intPred, "p");
 
   // Constants
-  Term zero = slv.mkReal(0);
-  Term one = slv.mkReal(1);
+  Term zero = slv.mkInteger(0);
+  Term one = slv.mkInteger(1);
 
   // Terms
   Term f_x = slv.mkTerm(APPLY_UF, f, x);
diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp
index 00c0b9810..d9d3c9e9c 100644
--- a/examples/api/datatypes.cpp
+++ b/examples/api/datatypes.cpp
@@ -39,7 +39,7 @@ void test(Solver& slv, Sort& consListSort)
   Term t = slv.mkTerm(
       APPLY_CONSTRUCTOR,
       consList.getConstructorTerm("cons"),
-      slv.mkReal(0),
+      slv.mkInteger(0),
       slv.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
 
   std::cout << "t is " << t << std::endl
@@ -124,7 +124,7 @@ void test(Solver& slv, Sort& consListSort)
             << "sort of cons is "
             << paramConsList.getConstructorTerm("cons").getSort() << std::endl
             << std::endl;
-  Term assertion = slv.mkTerm(GT, head_a, slv.mkReal(50));
+  Term assertion = slv.mkTerm(GT, head_a, slv.mkInteger(50));
   std::cout << "Assert " << assertion << std::endl;
   slv.assertFormula(assertion);
   std::cout << "Expect sat." << std::endl;
diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp
index 2d6636d0f..2e70460af 100644
--- a/examples/api/linear_arith.cpp
+++ b/examples/api/linear_arith.cpp
@@ -39,8 +39,8 @@ int main()
   Term y = slv.mkConst(real, "y");
 
   // Constants
-  Term three = slv.mkReal(3);
-  Term neg2 = slv.mkReal(-2);
+  Term three = slv.mkInteger(3);
+  Term neg2 = slv.mkInteger(-2);
   Term two_thirds = slv.mkReal(2, 3);
 
   // Terms
diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py
index 253365c9d..ed3fe0be5 100644
--- a/examples/api/python/combination.py
+++ b/examples/api/python/combination.py
@@ -46,8 +46,8 @@ if __name__ == "__main__":
     p = slv.mkConst(intPred, "p")
 
     # Constants
-    zero = slv.mkReal(0)
-    one = slv.mkReal(1)
+    zero = slv.mkInteger(0)
+    one = slv.mkInteger(1)
 
     # Terms
     f_x = slv.mkTerm(kinds.ApplyUf, f, x)
diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py
index 8ae2c29fd..6eef4478d 100644
--- a/examples/api/python/datatypes.py
+++ b/examples/api/python/datatypes.py
@@ -33,7 +33,7 @@ def test(slv, consListSort):
     # "nil" is a constructor too
 
     t = slv.mkTerm(kinds.ApplyConstructor, consList.getConstructorTerm("cons"),
-                   slv.mkReal(0),
+                   slv.mkInteger(0),
                    slv.mkTerm(kinds.ApplyConstructor, consList.getConstructorTerm("nil")))
 
     print("t is {}\nsort of cons is {}\n sort of nil is {}".format(
@@ -82,7 +82,7 @@ def test(slv, consListSort):
     print("head_a is {} of sort {}".format(head_a, head_a.getSort()))
     print("sort of cons is", paramConsList.getConstructorTerm("cons").getSort())
 
-    assertion = slv.mkTerm(kinds.Gt, head_a, slv.mkReal(50))
+    assertion = slv.mkTerm(kinds.Gt, head_a, slv.mkInteger(50))
     print("Assert", assertion)
     slv.assertFormula(assertion)
     print("Expect sat.")
diff --git a/examples/api/python/linear_arith.py b/examples/api/python/linear_arith.py
index f85171150..94ce730a3 100644
--- a/examples/api/python/linear_arith.py
+++ b/examples/api/python/linear_arith.py
@@ -33,8 +33,8 @@ if __name__ == "__main__":
     y = slv.mkConst(real, "y")
 
     # Constants
-    three = slv.mkReal(3)
-    neg2 = slv.mkReal(-2)
+    three = slv.mkInteger(3)
+    neg2 = slv.mkInteger(-2)
     two_thirds = slv.mkReal(2, 3)
 
     # Terms
diff --git a/examples/api/python/sequences.py b/examples/api/python/sequences.py
index 1b0c34f44..7ed5448cd 100644
--- a/examples/api/python/sequences.py
+++ b/examples/api/python/sequences.py
@@ -42,9 +42,9 @@ if __name__ == "__main__":
     # Sequence length: |x.y.empty|
     concat_len = slv.mkTerm(kinds.SeqLength, concat)
     # |x.y.empty| > 1
-    formula1 = slv.mkTerm(kinds.Gt, concat_len, slv.mkReal(1))
+    formula1 = slv.mkTerm(kinds.Gt, concat_len, slv.mkInteger(1))
     # Sequence unit: seq(1)
-    unit = slv.mkTerm(kinds.SeqUnit, slv.mkReal(1))
+    unit = slv.mkTerm(kinds.SeqUnit, slv.mkInteger(1))
     # x = seq(1)
     formula2 = slv.mkTerm(kinds.Equal, x, unit)
 
diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py
index 67d9808e7..77de3e5b3 100644
--- a/examples/api/python/sets.py
+++ b/examples/api/python/sets.py
@@ -62,9 +62,9 @@ if __name__ == "__main__":
 
     # Find me an element in 1, 2 intersection 2, 3, if there is one.
 
-    one = slv.mkReal(1)
-    two = slv.mkReal(2)
-    three = slv.mkReal(3)
+    one = slv.mkInteger(1)
+    two = slv.mkInteger(2)
+    three = slv.mkInteger(3)
 
     singleton_one = slv.mkSingleton(integer, one)
     singleton_two = slv.mkSingleton(integer, two)
diff --git a/examples/api/python/strings.py b/examples/api/python/strings.py
index c007b4bb5..1e85c56bb 100644
--- a/examples/api/python/strings.py
+++ b/examples/api/python/strings.py
@@ -51,7 +51,7 @@ if __name__ == "__main__":
     # Length of y: |y|
     leny = slv.mkTerm(kinds.StringLength, y)
     # |y| >= 0
-    formula2 = slv.mkTerm(kinds.Geq, leny, slv.mkReal(0))
+    formula2 = slv.mkTerm(kinds.Geq, leny, slv.mkInteger(0))
 
     # Regular expression: (ab[c-e]*f)|g|h
     r = slv.mkTerm(kinds.RegexpUnion,
diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py
index d331c9f9e..a85902961 100644
--- a/examples/api/python/sygus-fun.py
+++ b/examples/api/python/sygus-fun.py
@@ -41,8 +41,8 @@ if __name__ == "__main__":
   start_bool = slv.mkVar(boolean, "StartBool")
 
   # define the rules
-  zero = slv.mkReal(0)
-  one = slv.mkReal(1)
+  zero = slv.mkInteger(0)
+  one = slv.mkInteger(1)
 
   plus = slv.mkTerm(kinds.Plus, start, start)
   minus = slv.mkTerm(kinds.Minus, start, start)
diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py
index 7a8f89c68..cfa342f35 100644
--- a/examples/api/python/sygus-grammar.py
+++ b/examples/api/python/sygus-grammar.py
@@ -38,7 +38,7 @@ if __name__ == "__main__":
   start = slv.mkVar(integer, "Start")
 
   # define the rules
-  zero = slv.mkReal(0)
+  zero = slv.mkInteger(0)
   neg_x = slv.mkTerm(kinds.Uminus, x)
   plus = slv.mkTerm(kinds.Plus, x, start)
 
diff --git a/examples/api/python/sygus-inv.py b/examples/api/python/sygus-inv.py
index f71091371..4e7465382 100644
--- a/examples/api/python/sygus-inv.py
+++ b/examples/api/python/sygus-inv.py
@@ -30,9 +30,9 @@ if __name__ == "__main__":
   integer = slv.getIntegerSort()
   boolean = slv.getBooleanSort()
 
-  zero = slv.mkReal(0)
-  one = slv.mkReal(1)
-  ten = slv.mkReal(10)
+  zero = slv.mkInteger(0)
+  one = slv.mkInteger(1)
+  ten = slv.mkInteger(10)
 
   # declare input variables for functions
   x = slv.mkVar(integer, "x")
diff --git a/examples/api/sequences.cpp b/examples/api/sequences.cpp
index 3783d35c4..63d5aac96 100644
--- a/examples/api/sequences.cpp
+++ b/examples/api/sequences.cpp
@@ -47,9 +47,9 @@ int main()
   // Sequence length: |x.y.empty|
   Term concat_len = slv.mkTerm(SEQ_LENGTH, concat);
   // |x.y.empty| > 1
-  Term formula1 = slv.mkTerm(GT, concat_len, slv.mkReal(1));
+  Term formula1 = slv.mkTerm(GT, concat_len, slv.mkInteger(1));
   // Sequence unit: seq(1)
-  Term unit = slv.mkTerm(SEQ_UNIT, slv.mkReal(1));
+  Term unit = slv.mkTerm(SEQ_UNIT, slv.mkInteger(1));
   // x = seq(1)
   Term formula2 = slv.mkTerm(EQUAL, x, unit);
 
diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp
index fd85858a2..549b68e0d 100644
--- a/examples/api/sets.cpp
+++ b/examples/api/sets.cpp
@@ -69,9 +69,9 @@ int main()
 
   // Find me an element in {1, 2} intersection {2, 3}, if there is one.
   {
-    Term one = slv.mkReal(1);
-    Term two = slv.mkReal(2);
-    Term three = slv.mkReal(3);
+    Term one = slv.mkInteger(1);
+    Term two = slv.mkInteger(2);
+    Term three = slv.mkInteger(3);
 
     Term singleton_one = slv.mkSingleton(integer, one);
     Term singleton_two = slv.mkSingleton(integer, two);
diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp
index ad8df9ffa..556c49c8e 100644
--- a/examples/api/strings.cpp
+++ b/examples/api/strings.cpp
@@ -56,7 +56,7 @@ int main()
   // Length of y: |y|
   Term leny = slv.mkTerm(STRING_LENGTH, y);
   // |y| >= 0
-  Term formula2 = slv.mkTerm(GEQ, leny, slv.mkReal(0));
+  Term formula2 = slv.mkTerm(GEQ, leny, slv.mkInteger(0));
 
   // Regular expression: (ab[c-e]*f)|g|h
   Term r = slv.mkTerm(REGEXP_UNION,
diff --git a/examples/api/sygus-fun.cpp b/examples/api/sygus-fun.cpp
index b85529554..b2d6e9215 100644
--- a/examples/api/sygus-fun.cpp
+++ b/examples/api/sygus-fun.cpp
@@ -74,8 +74,8 @@ int main()
   Term start_bool = slv.mkVar(boolean, "StartBool");
 
   // define the rules
-  Term zero = slv.mkReal(0);
-  Term one = slv.mkReal(1);
+  Term zero = slv.mkInteger(0);
+  Term one = slv.mkInteger(1);
 
   Term plus = slv.mkTerm(PLUS, start, start);
   Term minus = slv.mkTerm(MINUS, start, start);
diff --git a/examples/api/sygus-grammar.cpp b/examples/api/sygus-grammar.cpp
index 4cfbe84fa..ea8256c70 100644
--- a/examples/api/sygus-grammar.cpp
+++ b/examples/api/sygus-grammar.cpp
@@ -69,7 +69,7 @@ int main()
   Term start = slv.mkVar(integer, "Start");
 
   // define the rules
-  Term zero = slv.mkReal(0);
+  Term zero = slv.mkInteger(0);
   Term neg_x = slv.mkTerm(UMINUS, x);
   Term plus = slv.mkTerm(PLUS, x, start);
 
diff --git a/examples/api/sygus-inv.cpp b/examples/api/sygus-inv.cpp
index 710265113..d57d9be4e 100644
--- a/examples/api/sygus-inv.cpp
+++ b/examples/api/sygus-inv.cpp
@@ -53,9 +53,9 @@ int main()
   Sort integer = slv.getIntegerSort();
   Sort boolean = slv.getBooleanSort();
 
-  Term zero = slv.mkReal(0);
-  Term one = slv.mkReal(1);
-  Term ten = slv.mkReal(10);
+  Term zero = slv.mkInteger(0);
+  Term one = slv.mkInteger(1);
+  Term ten = slv.mkInteger(10);
 
   // declare input variables for functions
   Term x = slv.mkVar(integer, "x");
diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp
index 49a4f576e..e648b9994 100644
--- a/examples/simple_vc_cxx.cpp
+++ b/examples/simple_vc_cxx.cpp
@@ -32,16 +32,16 @@ int main() {
 
   Term x = slv.mkConst(integer, "x");
   Term y = slv.mkConst(integer, "y");
-  Term zero = slv.mkReal(0);
+  Term zero = slv.mkInteger(0);
 
   Term x_positive = slv.mkTerm(Kind::GT, x, zero);
   Term y_positive = slv.mkTerm(Kind::GT, y, zero);
 
-  Term two = slv.mkReal(2);
+  Term two = slv.mkInteger(2);
   Term twox = slv.mkTerm(Kind::MULT, two, x);
   Term twox_plus_y = slv.mkTerm(Kind::PLUS, twox, y);
 
-  Term three = slv.mkReal(3);
+  Term three = slv.mkInteger(3);
   Term twox_plus_y_geq_3 = slv.mkTerm(Kind::GEQ, twox_plus_y, three);
 
   Term formula =
diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp
index 7596b4771..538cb359f 100644
--- a/examples/simple_vc_quant_cxx.cpp
+++ b/examples/simple_vc_quant_cxx.cpp
@@ -40,7 +40,7 @@ int main() {
   std::cout << "Made expression : " << quantpospx << std::endl;
 
   //make ~P( 5 )
-  Term five = slv.mkReal(5);
+  Term five = slv.mkInteger(5);
   Term pfive = slv.mkTerm(Kind::APPLY_UF, p, five);
   Term negpfive = slv.mkTerm(Kind::NOT, pfive);
   std::cout << "Made expression : " << negpfive << std::endl;