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

11 files changed, 123 insertions, 109 deletions

diff --git a/test/api/reset_assertions.cpp b/test/api/reset_assertions.cpp
index 73629a0d0..2168d053e 100644
--- a/test/api/reset_assertions.cpp
+++ b/test/api/reset_assertions.cpp
@@ -31,7 +31,7 @@ int main()
 
   Sort real = slv.getRealSort();
   Term x = slv.mkConst(real, "x");
-  Term four = slv.mkReal(4);
+  Term four = slv.mkInteger(4);
   Term xEqFour = slv.mkTerm(Kind::EQUAL, x, four);
   slv.assertFormula(xEqFour);
   std::cout << slv.checkSat() << std::endl;
@@ -43,7 +43,7 @@ int main()
   Sort arrayType = slv.mkArraySort(indexType, elementType);
   Term array = slv.mkConst(arrayType, "array");
   Term arrayAtFour = slv.mkTerm(Kind::SELECT, array, four);
-  Term ten = slv.mkReal(10);
+  Term ten = slv.mkInteger(10);
   Term arrayAtFour_eq_ten = slv.mkTerm(Kind::EQUAL, arrayAtFour, ten);
   slv.assertFormula(arrayAtFour_eq_ten);
   std::cout << slv.checkSat() << std::endl;
diff --git a/test/api/sep_log_api.cpp b/test/api/sep_log_api.cpp
index f0a55cf79..1b1efb07e 100644
--- a/test/api/sep_log_api.cpp
+++ b/test/api/sep_log_api.cpp
@@ -135,10 +135,10 @@ int validate_getters(void)
   Sort integer = slv.getIntegerSort();
 
   /* A "random" constant */
-  Term random_constant = slv.mkReal(0xDEADBEEF);
+  Term random_constant = slv.mkInteger(0xDEADBEEF);
 
   /* Another random constant */
-  Term expr_nil_val = slv.mkReal(0xFBADBEEF);
+  Term expr_nil_val = slv.mkInteger(0xFBADBEEF);
 
   /* Our nil term */
   Term nil = slv.mkSepNil(integer);
diff --git a/test/regress/regress0/get-value-reals-ints.smt2 b/test/regress/regress0/get-value-reals-ints.smt2
index b75f535d5..c8d3bb348 100644
--- a/test/regress/regress0/get-value-reals-ints.smt2
+++ b/test/regress/regress0/get-value-reals-ints.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-; EXPECT: ((pos_int 5) (pos_real_int_value (/ 3 1)) (pos_rat (/ 1 3)) (zero (/ 0 1)) (neg_rat (/ (- 2) 3)) (neg_real_int_value (/ (- 2) 1)) (neg_int (- 6)))
+; EXPECT: ((pos_int 5) (pos_real_int_value (/ 3.0 1.0)) (pos_rat (/ 1 3)) (zero (/ 0.0 1.0)) (neg_rat (/ (- 2) 3)) (neg_real_int_value (/ (- 2.0) 1.0)) (neg_int (- 6)))
 (set-info :smt-lib-version 2.0)
 (set-option :produce-models true)
 (set-logic QF_LIRA)
diff --git a/test/regress/regress0/get-value-reals.smt2 b/test/regress/regress0/get-value-reals.smt2
index 09ec0917f..d27581114 100644
--- a/test/regress/regress0/get-value-reals.smt2
+++ b/test/regress/regress0/get-value-reals.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-; EXPECT: ((pos_int (/ 3 1)) (pos_rat (/ 1 3)) (zero (/ 0 1)) (neg_rat (/ (- 2) 3)) (neg_int (/ (- 2) 1)))
+; EXPECT: ((pos_int (/ 3.0 1.0)) (pos_rat (/ 1 3)) (zero (/ 0.0 1.0)) (neg_rat (/ (- 2) 3)) (neg_int (/ (- 2.0) 1.0)))
 (set-info :smt-lib-version 2.0)
 (set-option :produce-models true)
 (set-logic QF_LRA)
diff --git a/test/unit/api/grammar_black.h b/test/unit/api/grammar_black.h
index bf0d97e9d..afbd09d0f 100644
--- a/test/unit/api/grammar_black.h
+++ b/test/unit/api/grammar_black.h
@@ -57,7 +57,7 @@ void GrammarBlack::testAddRule()
   TS_ASSERT_THROWS(g.addRule(start, nullTerm), CVC4ApiException&);
   TS_ASSERT_THROWS(g.addRule(nts, d_solver->mkBoolean(false)),
                    CVC4ApiException&);
-  TS_ASSERT_THROWS(g.addRule(start, d_solver->mkReal(0)), CVC4ApiException&);
+  TS_ASSERT_THROWS(g.addRule(start, d_solver->mkInteger(0)), CVC4ApiException&);
 
   d_solver->synthFun("f", {}, boolean, g);
 
@@ -83,7 +83,7 @@ void GrammarBlack::testAddRules()
   TS_ASSERT_THROWS(g.addRules(start, {nullTerm}), CVC4ApiException&);
   TS_ASSERT_THROWS(g.addRules(nts, {d_solver->mkBoolean(false)}),
                    CVC4ApiException&);
-  TS_ASSERT_THROWS(g.addRules(start, {d_solver->mkReal(0)}), CVC4ApiException&);
+  TS_ASSERT_THROWS(g.addRules(start, {d_solver->mkInteger(0)}), CVC4ApiException&);
 
   d_solver->synthFun("f", {}, boolean, g);
 
diff --git a/test/unit/api/python/test_grammar.py b/test/unit/api/python/test_grammar.py
index 0321f03d0..5a0d5101f 100644
--- a/test/unit/api/python/test_grammar.py
+++ b/test/unit/api/python/test_grammar.py
@@ -38,7 +38,7 @@ def test_add_rule():
   with pytest.raises(Exception):
     g.addRule(nts, solver.mkBoolean(false))
   with pytest.raises(Exception):
-    g.addRule(start, solver.mkReal(0))
+    g.addRule(start, solver.mkInteger(0))
 
   # expecting no errors
   solver.synthFun("f", {}, boolean, g)
@@ -68,7 +68,7 @@ def test_add_rules():
   with pytest.raises(Exception):
     g.addRules(nts, {solver.mkBoolean(False)})
   with pytest.raises(Exception):
-    g.addRules(start, {solver.mkReal(0)})
+    g.addRules(start, {solver.mkInteger(0)})
   #Expecting no errors
   solver.synthFun("f", {}, boolean, g)
 
diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py
index 9c25b584f..a0c1b4681 100644
--- a/test/unit/api/python/test_term.py
+++ b/test/unit/api/python/test_term.py
@@ -103,26 +103,12 @@ def test_get_op():
     assert fx.getOp() == solver.mkOp(kinds.ApplyUf)
 
 
-def test_is_const():
-    solver = pycvc4.Solver()
-    intsort = solver.getIntegerSort()
-    one = solver.mkReal(1)
-    x = solver.mkConst(intsort, 'x')
-    xpone = solver.mkTerm(kinds.Plus, x, one)
-    onepone = solver.mkTerm(kinds.Plus, one, one)
-    assert not x.isValue()
-    assert one.isValue()
-    assert not xpone.isValue()
-    assert not onepone.isValue()
-
 def test_const_sequence_elements():
     solver = pycvc4.Solver()
     realsort = solver.getRealSort()
     seqsort = solver.mkSequenceSort(realsort)
     s = solver.mkEmptySequence(seqsort)
 
-    assert s.isValue()
-
     assert s.getKind() == kinds.ConstSequence
     # empty sequence has zero elements
     cs = s.getConstSequenceElements()
diff --git a/test/unit/api/python/test_to_python_obj.py b/test/unit/api/python/test_to_python_obj.py
index 3ce08f6b8..eb15e7469 100644
--- a/test/unit/api/python/test_to_python_obj.py
+++ b/test/unit/api/python/test_to_python_obj.py
@@ -15,7 +15,7 @@ def testGetBool():
 
 def testGetInt():
     solver = pycvc4.Solver()
-    two = solver.mkReal(2)
+    two = solver.mkInteger(2)
     assert two.toPythonObj() == 2
 
 
@@ -27,7 +27,7 @@ def testGetReal():
     neg34 = solver.mkReal("-3/4")
     assert neg34.toPythonObj() == Fraction(-3, 4)
 
-    neg1 = solver.mkReal("-1")
+    neg1 = solver.mkInteger("-1")
     assert neg1.toPythonObj() == -1
 
 
@@ -40,12 +40,10 @@ def testGetBV():
 def testGetArray():
     solver = pycvc4.Solver()
     arrsort = solver.mkArraySort(solver.getRealSort(), solver.getRealSort())
-    zero_array = solver.mkConstArray(arrsort, solver.mkReal(0))
-    stores = solver.mkTerm(kinds.Store, zero_array, solver.mkReal(1), solver.mkReal(2))
-    stores = solver.mkTerm(kinds.Store, stores, solver.mkReal(2), solver.mkReal(3))
-    stores = solver.mkTerm(kinds.Store, stores, solver.mkReal(4), solver.mkReal(5))
-
-    assert stores.isValue()
+    zero_array = solver.mkConstArray(arrsort, solver.mkInteger(0))
+    stores = solver.mkTerm(kinds.Store, zero_array, solver.mkInteger(1), solver.mkInteger(2))
+    stores = solver.mkTerm(kinds.Store, stores, solver.mkInteger(2), solver.mkInteger(3))
+    stores = solver.mkTerm(kinds.Store, stores, solver.mkInteger(4), solver.mkInteger(5))
 
     array_dict = stores.toPythonObj()
 
@@ -58,10 +56,7 @@ def testGetArray():
 
 def testGetSymbol():
     solver = pycvc4.Solver()
-    x = solver.mkConst(solver.getBooleanSort(), "x")
-
-    with pytest.raises(RuntimeError):
-        x.toPythonObj()
+    solver.mkConst(solver.getBooleanSort(), "x")
 
 
 def testGetString():
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 8b8c6dd58..1324e3890 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -72,6 +72,7 @@ class SolverBlack : public CxxTest::TestSuite
   void testMkPi();
   void testMkPosInf();
   void testMkPosZero();
+  void testMkInteger();
   void testMkReal();
   void testMkRegexpEmpty();
   void testMkRegexpSigma();
@@ -598,7 +599,7 @@ void SolverBlack::testMkFloatingPoint()
 {
   Term t1 = d_solver->mkBitVector(8);
   Term t2 = d_solver->mkBitVector(4);
-  Term t3 = d_solver->mkReal(2);
+  Term t3 = d_solver->mkInteger(2);
   if (CVC4::Configuration::isBuiltWithSymFPU())
   {
     TS_ASSERT_THROWS_NOTHING(d_solver->mkFloatingPoint(3, 5, t1));
@@ -742,6 +743,47 @@ void SolverBlack::testMkOp()
 
 void SolverBlack::testMkPi() { TS_ASSERT_THROWS_NOTHING(d_solver->mkPi()); }
 
+void SolverBlack::testMkInteger()
+{
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger("123"));
+  TS_ASSERT_THROWS(d_solver->mkInteger("1.23"), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger("1/23"), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger("12/3"), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(".2"), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger("2."), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(""), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger("asdf"), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger("1.2/3"), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger("."), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger("/"), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger("2/"), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger("/2"), CVC4ApiException&);
+
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(std::string("123")));
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("1.23")), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("1/23")), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("12/3")), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string(".2")), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("2.")), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("")), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("asdf")), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("1.2/3")), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string(".")), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("/")), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("2/")), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("/2")), CVC4ApiException&);
+
+  int32_t val1 = 1;
+  int64_t val2 = -1;
+  uint32_t val3 = 1;
+  uint64_t val4 = -1;
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val1));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val2));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val3));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val4));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val4));
+}
+
 void SolverBlack::testMkReal()
 {
   TS_ASSERT_THROWS_NOTHING(d_solver->mkReal("123"));
@@ -839,8 +881,8 @@ void SolverBlack::testMkTerm()
   std::vector<Term> v1 = {a, b};
   std::vector<Term> v2 = {a, Term()};
   std::vector<Term> v3 = {a, d_solver->mkTrue()};
-  std::vector<Term> v4 = {d_solver->mkReal(1), d_solver->mkReal(2)};
-  std::vector<Term> v5 = {d_solver->mkReal(1), Term()};
+  std::vector<Term> v4 = {d_solver->mkInteger(1), d_solver->mkInteger(2)};
+  std::vector<Term> v5 = {d_solver->mkInteger(1), Term()};
   std::vector<Term> v6 = {};
   Solver slv;
 
@@ -896,10 +938,10 @@ void SolverBlack::testMkTermFromOp()
   Sort bv32 = d_solver->mkBitVectorSort(32);
   Term a = d_solver->mkConst(bv32, "a");
   Term b = d_solver->mkConst(bv32, "b");
-  std::vector<Term> v1 = {d_solver->mkReal(1), d_solver->mkReal(2)};
-  std::vector<Term> v2 = {d_solver->mkReal(1), Term()};
+  std::vector<Term> v1 = {d_solver->mkInteger(1), d_solver->mkInteger(2)};
+  std::vector<Term> v2 = {d_solver->mkInteger(1), Term()};
   std::vector<Term> v3 = {};
-  std::vector<Term> v4 = {d_solver->mkReal(5)};
+  std::vector<Term> v4 = {d_solver->mkInteger(5)};
   Solver slv;
 
   // simple operator terms
@@ -948,13 +990,13 @@ void SolverBlack::testMkTermFromOp()
 
   // mkTerm(Op op, Term child) const
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm1, a));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm2, d_solver->mkReal(1)));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm2, d_solver->mkInteger(1)));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, headTerm1, c));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, tailTerm2, c));
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, a), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, Term()), CVC4ApiException&);
   TS_ASSERT_THROWS(
-      d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkReal(0)),
+      d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkInteger(0)),
       CVC4ApiException&);
   TS_ASSERT_THROWS(slv.mkTerm(opterm1, a), CVC4ApiException&);
 
@@ -962,19 +1004,19 @@ void SolverBlack::testMkTermFromOp()
   TS_ASSERT_THROWS_NOTHING(
       d_solver->mkTerm(APPLY_CONSTRUCTOR,
                        consTerm1,
-                       d_solver->mkReal(0),
+                       d_solver->mkInteger(0),
                        d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)));
   TS_ASSERT_THROWS(
-      d_solver->mkTerm(opterm2, d_solver->mkReal(1), d_solver->mkReal(2)),
+      d_solver->mkTerm(opterm2, d_solver->mkInteger(1), d_solver->mkInteger(2)),
       CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, d_solver->mkReal(1), Term()),
+  TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, d_solver->mkInteger(1), Term()),
                    CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, Term(), d_solver->mkReal(1)),
+  TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, Term(), d_solver->mkInteger(1)),
                    CVC4ApiException&);
   TS_ASSERT_THROWS(slv.mkTerm(APPLY_CONSTRUCTOR,
                               consTerm1,
-                              d_solver->mkReal(0),
+                              d_solver->mkInteger(0),
                               d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)),
                    CVC4ApiException&);
 
@@ -982,7 +1024,7 @@ void SolverBlack::testMkTermFromOp()
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b, a), CVC4ApiException&);
   TS_ASSERT_THROWS(
       d_solver->mkTerm(
-          opterm2, d_solver->mkReal(1), d_solver->mkReal(1), Term()),
+          opterm2, d_solver->mkInteger(1), d_solver->mkInteger(1), Term()),
       CVC4ApiException&);
 
   // mkTerm(Op op, const std::vector<Term>& children) const
@@ -1004,7 +1046,7 @@ void SolverBlack::testMkTuple()
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTuple(
       {d_solver->mkBitVectorSort(3)}, {d_solver->mkBitVector("101", 2)}));
   TS_ASSERT_THROWS_NOTHING(
-      d_solver->mkTuple({d_solver->getRealSort()}, {d_solver->mkReal("5")}));
+      d_solver->mkTuple({d_solver->getRealSort()}, {d_solver->mkInteger("5")}));
 
   TS_ASSERT_THROWS(d_solver->mkTuple({}, {d_solver->mkBitVector("101", 2)}),
                    CVC4ApiException&);
@@ -1054,7 +1096,7 @@ void SolverBlack::testMkConstArray()
 {
   Sort intSort = d_solver->getIntegerSort();
   Sort arrSort = d_solver->mkArraySort(intSort, intSort);
-  Term zero = d_solver->mkReal(0);
+  Term zero = d_solver->mkInteger(0);
   Term constArr = d_solver->mkConstArray(arrSort, zero);
 
   TS_ASSERT_THROWS_NOTHING(d_solver->mkConstArray(arrSort, zero));
@@ -1064,7 +1106,7 @@ void SolverBlack::testMkConstArray()
                    CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkConstArray(intSort, zero), CVC4ApiException&);
   Solver slv;
-  Term zero2 = slv.mkReal(0);
+  Term zero2 = slv.mkInteger(0);
   Sort arrSort2 = slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort());
   TS_ASSERT_THROWS(slv.mkConstArray(arrSort2, zero), CVC4ApiException&);
   TS_ASSERT_THROWS(slv.mkConstArray(arrSort, zero2), CVC4ApiException&);
@@ -1454,7 +1496,7 @@ void SolverBlack::testGetOp()
 
   Term listnil = d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm);
   Term listcons1 = d_solver->mkTerm(
-      APPLY_CONSTRUCTOR, consTerm, d_solver->mkReal(1), listnil);
+      APPLY_CONSTRUCTOR, consTerm, d_solver->mkInteger(1), listnil);
   Term listhead = d_solver->mkTerm(APPLY_SELECTOR, headTerm, listcons1);
 
   TS_ASSERT(listnil.hasOp());
@@ -1542,8 +1584,8 @@ void SolverBlack::testGetUnsatCore3()
   Term y = d_solver->mkConst(uSort, "y");
   Term f = d_solver->mkConst(uToIntSort, "f");
   Term p = d_solver->mkConst(intPredSort, "p");
-  Term zero = d_solver->mkReal(0);
-  Term one = d_solver->mkReal(1);
+  Term zero = d_solver->mkInteger(0);
+  Term one = d_solver->mkInteger(1);
   Term f_x = d_solver->mkTerm(APPLY_UF, f, x);
   Term f_y = d_solver->mkTerm(APPLY_UF, f, y);
   Term sum = d_solver->mkTerm(PLUS, f_x, f_y);
@@ -1601,8 +1643,8 @@ void SolverBlack::testGetValue3()
   Term z = d_solver->mkConst(uSort, "z");
   Term f = d_solver->mkConst(uToIntSort, "f");
   Term p = d_solver->mkConst(intPredSort, "p");
-  Term zero = d_solver->mkReal(0);
-  Term one = d_solver->mkReal(1);
+  Term zero = d_solver->mkInteger(0);
+  Term one = d_solver->mkInteger(1);
   Term f_x = d_solver->mkTerm(APPLY_UF, f, x);
   Term f_y = d_solver->mkTerm(APPLY_UF, f, y);
   Term sum = d_solver->mkTerm(PLUS, f_x, f_y);
@@ -1985,11 +2027,11 @@ void SolverBlack::testSimplify()
 
   Term i1 = d_solver->mkConst(d_solver->getIntegerSort(), "i1");
   TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i1));
-  Term i2 = d_solver->mkTerm(MULT, i1, d_solver->mkReal("23"));
+  Term i2 = d_solver->mkTerm(MULT, i1, d_solver->mkInteger("23"));
   TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i2));
   TS_ASSERT(i1 != i2);
   TS_ASSERT(i1 != d_solver->simplify(i2));
-  Term i3 = d_solver->mkTerm(PLUS, i1, d_solver->mkReal(0));
+  Term i3 = d_solver->mkTerm(PLUS, i1, d_solver->mkInteger(0));
   TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i3));
   TS_ASSERT(i1 != i3);
   TS_ASSERT(i1 == d_solver->simplify(i3));
@@ -1998,7 +2040,7 @@ void SolverBlack::testSimplify()
   Term dt1 = d_solver->mkTerm(
       APPLY_CONSTRUCTOR,
       consList.getConstructorTerm("cons"),
-      d_solver->mkReal(0),
+      d_solver->mkInteger(0),
       d_solver->mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
   TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt1));
   Term dt2 = d_solver->mkTerm(
@@ -2075,8 +2117,8 @@ void SolverBlack::testCheckEntailed2()
   Term f = d_solver->mkConst(uToIntSort, "f");
   Term p = d_solver->mkConst(intPredSort, "p");
   // Values
-  Term zero = d_solver->mkReal(0);
-  Term one = d_solver->mkReal(1);
+  Term zero = d_solver->mkInteger(0);
+  Term one = d_solver->mkInteger(1);
   // Terms
   Term f_x = d_solver->mkTerm(APPLY_UF, f, x);
   Term f_y = d_solver->mkTerm(APPLY_UF, f, y);
@@ -2158,8 +2200,8 @@ void SolverBlack::testCheckSatAssuming2()
   Term f = d_solver->mkConst(uToIntSort, "f");
   Term p = d_solver->mkConst(intPredSort, "p");
   // Values
-  Term zero = d_solver->mkReal(0);
-  Term one = d_solver->mkReal(1);
+  Term zero = d_solver->mkInteger(0);
+  Term one = d_solver->mkInteger(1);
   // Terms
   Term f_x = d_solver->mkTerm(APPLY_UF, f, x);
   Term f_y = d_solver->mkTerm(APPLY_UF, f, y);
@@ -2279,7 +2321,7 @@ void SolverBlack::testSynthFun()
   g1.addRule(start1, d_solver->mkBoolean(false));
 
   Grammar g2 = d_solver->mkSygusGrammar({x}, {start2});
-  g2.addRule(start2, d_solver->mkReal(0));
+  g2.addRule(start2, d_solver->mkInteger(0));
 
   TS_ASSERT_THROWS_NOTHING(d_solver->synthFun("", {}, boolean));
   TS_ASSERT_THROWS_NOTHING(d_solver->synthFun("f1", {x}, boolean));
@@ -2314,7 +2356,7 @@ void SolverBlack::testSynthInv()
   g1.addRule(start1, d_solver->mkBoolean(false));
 
   Grammar g2 = d_solver->mkSygusGrammar({x}, {start2});
-  g2.addRule(start2, d_solver->mkReal(0));
+  g2.addRule(start2, d_solver->mkInteger(0));
 
   TS_ASSERT_THROWS_NOTHING(d_solver->synthInv("", {}));
   TS_ASSERT_THROWS_NOTHING(d_solver->synthInv("i1", {x}));
@@ -2328,7 +2370,7 @@ void SolverBlack::testAddSygusConstraint()
 {
   Term nullTerm;
   Term boolTerm = d_solver->mkBoolean(true);
-  Term intTerm = d_solver->mkReal(1);
+  Term intTerm = d_solver->mkInteger(1);
 
   TS_ASSERT_THROWS_NOTHING(d_solver->addSygusConstraint(boolTerm));
   TS_ASSERT_THROWS(d_solver->addSygusConstraint(nullTerm), CVC4ApiException&);
@@ -2344,7 +2386,7 @@ void SolverBlack::testAddSygusInvConstraint()
   Sort real = d_solver->getRealSort();
 
   Term nullTerm;
-  Term intTerm = d_solver->mkReal(1);
+  Term intTerm = d_solver->mkInteger(1);
 
   Term inv = d_solver->declareFun("inv", {real}, boolean);
   Term pre = d_solver->declareFun("pre", {real}, boolean);
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index 786b60bb3..bebfc6e1f 100644
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -42,7 +42,6 @@ class TermBlack : public CxxTest::TestSuite
   void testTermCompare();
   void testTermChildren();
   void testSubstitute();
-  void testIsValue();
   void testConstArray();
   void testConstSequenceElements();
 
@@ -100,7 +99,7 @@ void TermBlack::testGetKind()
   Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS_NOTHING(p.getKind());
 
-  Term zero = d_solver.mkReal(0);
+  Term zero = d_solver.mkInteger(0);
   TS_ASSERT_THROWS_NOTHING(zero.getKind());
 
   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
@@ -146,7 +145,7 @@ void TermBlack::testGetSort()
   TS_ASSERT_THROWS_NOTHING(p.getSort());
   TS_ASSERT(p.getSort() == funSort2);
 
-  Term zero = d_solver.mkReal(0);
+  Term zero = d_solver.mkInteger(0);
   TS_ASSERT_THROWS_NOTHING(zero.getSort());
   TS_ASSERT(zero.getSort() == intSort);
 
@@ -227,7 +226,7 @@ void TermBlack::testGetOp()
 
   Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilOpTerm);
   Term consTerm = d_solver.mkTerm(
-      APPLY_CONSTRUCTOR, consOpTerm, d_solver.mkReal(0), nilTerm);
+      APPLY_CONSTRUCTOR, consOpTerm, d_solver.mkInteger(0), nilTerm);
   Term headTerm = d_solver.mkTerm(APPLY_SELECTOR, headOpTerm, consTerm);
   Term tailTerm = d_solver.mkTerm(APPLY_SELECTOR, tailOpTerm, consTerm);
 
@@ -272,7 +271,7 @@ void TermBlack::testNotTerm()
   TS_ASSERT_THROWS(f.notTerm(), CVC4ApiException&);
   Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS(p.notTerm(), CVC4ApiException&);
-  Term zero = d_solver.mkReal(0);
+  Term zero = d_solver.mkInteger(0);
   TS_ASSERT_THROWS(zero.notTerm(), CVC4ApiException&);
   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
   TS_ASSERT_THROWS(f_x.notTerm(), CVC4ApiException&);
@@ -308,7 +307,7 @@ void TermBlack::testAndTerm()
   TS_ASSERT_THROWS(p.andTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(p.andTerm(f), CVC4ApiException&);
   TS_ASSERT_THROWS(p.andTerm(p), CVC4ApiException&);
-  Term zero = d_solver.mkReal(0);
+  Term zero = d_solver.mkInteger(0);
   TS_ASSERT_THROWS(zero.andTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(zero.andTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(zero.andTerm(f), CVC4ApiException&);
@@ -374,7 +373,7 @@ void TermBlack::testOrTerm()
   TS_ASSERT_THROWS(p.orTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(p.orTerm(f), CVC4ApiException&);
   TS_ASSERT_THROWS(p.orTerm(p), CVC4ApiException&);
-  Term zero = d_solver.mkReal(0);
+  Term zero = d_solver.mkInteger(0);
   TS_ASSERT_THROWS(zero.orTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(zero.orTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(zero.orTerm(f), CVC4ApiException&);
@@ -440,7 +439,7 @@ void TermBlack::testXorTerm()
   TS_ASSERT_THROWS(p.xorTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(p.xorTerm(f), CVC4ApiException&);
   TS_ASSERT_THROWS(p.xorTerm(p), CVC4ApiException&);
-  Term zero = d_solver.mkReal(0);
+  Term zero = d_solver.mkInteger(0);
   TS_ASSERT_THROWS(zero.xorTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(zero.xorTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(zero.xorTerm(f), CVC4ApiException&);
@@ -506,7 +505,7 @@ void TermBlack::testEqTerm()
   TS_ASSERT_THROWS(p.eqTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(p.eqTerm(f), CVC4ApiException&);
   TS_ASSERT_THROWS_NOTHING(p.eqTerm(p));
-  Term zero = d_solver.mkReal(0);
+  Term zero = d_solver.mkInteger(0);
   TS_ASSERT_THROWS(zero.eqTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(zero.eqTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(zero.eqTerm(f), CVC4ApiException&);
@@ -572,7 +571,7 @@ void TermBlack::testImpTerm()
   TS_ASSERT_THROWS(p.impTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(p.impTerm(f), CVC4ApiException&);
   TS_ASSERT_THROWS(p.impTerm(p), CVC4ApiException&);
-  Term zero = d_solver.mkReal(0);
+  Term zero = d_solver.mkInteger(0);
   TS_ASSERT_THROWS(zero.impTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(zero.impTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(zero.impTerm(f), CVC4ApiException&);
@@ -639,7 +638,7 @@ void TermBlack::testIteTerm()
   Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS(p.iteTerm(b, b), CVC4ApiException&);
   TS_ASSERT_THROWS(p.iteTerm(x, b), CVC4ApiException&);
-  Term zero = d_solver.mkReal(0);
+  Term zero = d_solver.mkInteger(0);
   TS_ASSERT_THROWS(zero.iteTerm(x, x), CVC4ApiException&);
   TS_ASSERT_THROWS(zero.iteTerm(x, b), CVC4ApiException&);
   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
@@ -660,17 +659,17 @@ void TermBlack::testIteTerm()
 
 void TermBlack::testTermAssignment()
 {
-  Term t1 = d_solver.mkReal(1);
+  Term t1 = d_solver.mkInteger(1);
   Term t2 = t1;
-  t2 = d_solver.mkReal(2);
-  TS_ASSERT_EQUALS(t1, d_solver.mkReal(1));
+  t2 = d_solver.mkInteger(2);
+  TS_ASSERT_EQUALS(t1, d_solver.mkInteger(1));
 }
 
 void TermBlack::testTermCompare()
 {
-  Term t1 = d_solver.mkReal(1);
-  Term t2 = d_solver.mkTerm(PLUS, d_solver.mkReal(2), d_solver.mkReal(2));
-  Term t3 = d_solver.mkTerm(PLUS, d_solver.mkReal(2), d_solver.mkReal(2));
+  Term t1 = d_solver.mkInteger(1);
+  Term t2 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
+  Term t3 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
   TS_ASSERT(t2 >= t3);
   TS_ASSERT(t2 <= t3);
   TS_ASSERT((t1 > t2) != (t1 < t2));
@@ -680,8 +679,8 @@ void TermBlack::testTermCompare()
 void TermBlack::testTermChildren()
 {
   // simple term 2+3
-  Term two = d_solver.mkReal(2);
-  Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkReal(3));
+  Term two = d_solver.mkInteger(2);
+  Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkInteger(3));
   TS_ASSERT(t1[0] == two);
   TS_ASSERT(t1.getNumChildren() == 2);
   Term tnull;
@@ -702,7 +701,7 @@ void TermBlack::testTermChildren()
 void TermBlack::testSubstitute()
 {
   Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
-  Term one = d_solver.mkReal(1);
+  Term one = d_solver.mkInteger(1);
   Term ttrue = d_solver.mkTrue();
   Term xpx = d_solver.mkTerm(PLUS, x, x);
   Term onepone = d_solver.mkTerm(PLUS, one, one);
@@ -750,34 +749,27 @@ void TermBlack::testSubstitute()
   TS_ASSERT_THROWS(xpx.substitute(es, rs), CVC4ApiException&);
 }
 
-void TermBlack::testIsValue()
-{
-  Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
-  Term one = d_solver.mkReal(1);
-  Term xpone = d_solver.mkTerm(PLUS, x, one);
-  Term onepone = d_solver.mkTerm(PLUS, one, one);
-  TS_ASSERT(!x.isValue());
-  TS_ASSERT(one.isValue());
-  TS_ASSERT(!xpone.isValue());
-  TS_ASSERT(!onepone.isValue());
-  Term tnull;
-  TS_ASSERT_THROWS(tnull.isValue(), CVC4ApiException&);
-}
-
 void TermBlack::testConstArray()
 {
   Sort intsort = d_solver.getIntegerSort();
   Sort arrsort = d_solver.mkArraySort(intsort, intsort);
   Term a = d_solver.mkConst(arrsort, "a");
-  Term one = d_solver.mkReal(1);
+  Term one = d_solver.mkInteger(1);
   Term constarr = d_solver.mkConstArray(arrsort, one);
 
-  TS_ASSERT(!a.isValue());
-  TS_ASSERT(constarr.isValue());
-
   TS_ASSERT_EQUALS(constarr.getKind(), CONST_ARRAY);
   TS_ASSERT_EQUALS(constarr.getConstArrayBase(), one);
   TS_ASSERT_THROWS(a.getConstArrayBase(), CVC4ApiException&);
+
+  arrsort =
+      d_solver.mkArraySort(d_solver.getRealSort(), d_solver.getRealSort());
+  Term zero_array = d_solver.mkConstArray(arrsort, d_solver.mkReal(0));
+  Term stores = d_solver.mkTerm(
+      STORE, zero_array, d_solver.mkReal(1), d_solver.mkReal(2));
+  stores =
+      d_solver.mkTerm(STORE, stores, d_solver.mkReal(2), d_solver.mkReal(3));
+  stores =
+      d_solver.mkTerm(STORE, stores, d_solver.mkReal(4), d_solver.mkReal(5));
 }
 
 void TermBlack::testConstSequenceElements()
@@ -786,7 +778,6 @@ void TermBlack::testConstSequenceElements()
   Sort seqsort = d_solver.mkSequenceSort(realsort);
   Term s = d_solver.mkEmptySequence(seqsort);
 
-  TS_ASSERT(s.isValue());
 
   TS_ASSERT_EQUALS(s.getKind(), CONST_SEQUENCE);
   // empty sequence has zero elements
diff --git a/test/unit/theory/theory_sets_type_rules_white.h b/test/unit/theory/theory_sets_type_rules_white.h
index c098ca9b8..f06c1f77d 100644
--- a/test/unit/theory/theory_sets_type_rules_white.h
+++ b/test/unit/theory/theory_sets_type_rules_white.h
@@ -56,7 +56,7 @@ class SetsTypeRuleWhite : public CxxTest::TestSuite
     Sort realSort = d_slv->getRealSort();
     Sort intSort = d_slv->getIntegerSort();
     Term emptyReal = d_slv->mkEmptySet(d_slv->mkSetSort(realSort));
-    Term one = d_slv->mkReal(1);
+    Term one = d_slv->mkInteger(1);
     Term singletonInt = d_slv->mkSingleton(intSort, one);
     Term singletonReal = d_slv->mkSingleton(realSort, one);
     // (union