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

diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp
index 191bb83bd02f193d70cbfb97ab768af6d54ee33d..307c307096eb430efb41015e54869978ae7c62b0 100644 (file)
--- 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 00c0b9810566c07838931670b659bd910475d680..d9d3c9e9cefc8ef34a70cadd2de28f5d94267d43 100644 (file)
--- 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 2d6636d0f89a85043ad51e04039c7d5c75159aba..2e70460af59fb03fe1ae0c556473cd604cef4090 100644 (file)
--- 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 253365c9dcef8c9369da99512107eeac0107bd1f..ed3fe0be59e3ec2c13de53e41c1f359a0203c2b4 100644 (file)
--- 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 8ae2c29fd39300c1c4467a2b300e12851874aee5..6eef4478d7d6f4956f34d9e73f7d72da905ec655 100644 (file)
--- 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 f85171150f9ccfe4b7d8d9194ac445488c3da646..94ce730a3fc978a89e8938e3c28d8b19591a1343 100644 (file)
--- 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 1b0c34f44f57c574ffbfa7a464fbbe964bd689fe..7ed5448cdb88c86888bc31b37e793e7c27c7e66c 100644 (file)
--- 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 67d9808e72400938610bb1eafc4a7c6c6960e6ca..77de3e5b31340b44a2f6500eec42bf924465ab60 100644 (file)
--- 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 c007b4bb59c163f570347ef0ea7adf234b5731b1..1e85c56bb9eec1d569cd096442e7306c610e7638 100644 (file)
--- 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 d331c9f9ea49f16471ecbf533401439945ab0d9e..a85902961db0bc2467d631788b99e3cc2996483a 100644 (file)
--- 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 7a8f89c6841627a9e9b198b0c73c051c784ae35c..cfa342f35cbefac643b4f2000c907befbfa62db1 100644 (file)
--- 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 f710913719ec62160d552b25d06fa3ce917ad11b..4e7465382e5aa6b5b792ae4f17506b79784ded48 100644 (file)
--- 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 3783d35c4347bfd7c8e56283ab0765f20bc04769..63d5aac964df74a81e0a7d560d7a49bba0a09212 100644 (file)
--- 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 fd85858a26a39ea50de3ad259958a43748fb0759..549b68e0dbbbc08f60247ab97012796eefdc71ba 100644 (file)
--- 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 ad8df9ffa9eb2d78793d8174300a081f2e2da610..556c49c8e37a787c3497b145651c9389ae1ac9f6 100644 (file)
--- 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 b855295547cbdb4c120fa9e302b802a5e03f2f54..b2d6e92152b428d5aeb9ef878beb433f767cb2fa 100644 (file)
--- 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 4cfbe84faceab941aa8d83b37e7304b79e5a1c0c..ea8256c70cba5ceecfc0ca03b5b36fa6a42152d6 100644 (file)
--- 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 710265113cc3adcf33173e95330c847e57cf61fd..d57d9be4e1baf316025209be76d34c3a88131ee7 100644 (file)
--- 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 49a4f576eb474ef55adb1c67163c7cc5b57bfc5e..e648b99949eda89e9aedb9b0a57898370df1c6d0 100644 (file)
--- 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 7596b4771bbfb6b1f76404bef02748885391423b..538cb359f3e313eb7b3f5c7697f484dbbb786987 100644 (file)
--- 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;

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index be82a517ffde0f147616510b90e096c46c937c8e..507e270bb49b7f37be6aa4b6ac43f773cc358df3 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -34,6 +34,7 @@
 #include "api/cvc4cpp.h"
 
 #include <cstring>
+#include <regex>
 #include <sstream>
 
 #include "base/check.h"
@@ -1603,7 +1604,7 @@ Kind Term::getKindHelper() const
   // (string) versions back to sequence. All operators where this is
   // necessary are such that their first child is of sequence type, which
   // we check here.
-  if (getNumChildren() > 0 && (*this)[0].getSort().isSequence())
+  if (d_node->getNumChildren() > 0 && (*d_node)[0].getType().isSequence())
   {
     switch (d_node->getKind())
     {
@@ -1626,9 +1627,22 @@ Kind Term::getKindHelper() const
   }
   // Notice that kinds like APPLY_TYPE_ASCRIPTION will be converted to
   // INTERNAL_KIND.
+  if(isCastedReal())
+  {
+    return CONST_RATIONAL;
+  }
   return intToExtKind(d_node->getKind());
 }
 
+bool Term::isCastedReal() const
+{
+  if(d_node->getKind() == kind::CAST_TO_REAL)
+  {
+    return (*d_node)[0].isConst() && (*d_node)[0].getType().isInteger();
+  }
+  return false;
+}
+
 bool Term::operator==(const Term& t) const { return *d_node == *t.d_node; }
 
 bool Term::operator!=(const Term& t) const { return *d_node != *t.d_node; }
@@ -1649,12 +1663,20 @@ size_t Term::getNumChildren() const
   {
     return d_node->getNumChildren() + 1;
   }
+  if(isCastedReal())
+  {
+    return 0;
+  }
   return d_node->getNumChildren();
 }
 
 Term Term::operator[](size_t index) const
 {
   CVC4_API_CHECK_NOT_NULL;
+
+  // check the index within the number of children
+  CVC4_API_CHECK(index < getNumChildren()) << "index out of bound";
+
   // special cases for apply kinds
   if (isApplyKind(d_node->getKind()))
   {
@@ -1763,12 +1785,6 @@ Op Term::getOp() const
 
 bool Term::isNull() const { return isNullHelper(); }
 
-bool Term::isValue() const
-{
-  CVC4_API_CHECK_NOT_NULL;
-  return d_node->isConst();
-}
-
 Term Term::getConstArrayBase() const
 {
   CVC4::ExprManagerScope exmgrs(*(d_solver->getExprManager()));
@@ -3109,16 +3125,20 @@ Term Solver::mkValHelper(T t) const
 
 Term Solver::mkRealFromStrHelper(const std::string& s) const
 {
-  /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
-   * throws an std::invalid_argument exception. For consistency, we treat it
-   * as invalid. */
-  CVC4_API_ARG_CHECK_EXPECTED(s != ".", s)
-      << "a string representing an integer, real or rational value.";
-
-  CVC4::Rational r = s.find('/') != std::string::npos
-                         ? CVC4::Rational(s)
-                         : CVC4::Rational::fromDecimal(s);
-  return mkValHelper<CVC4::Rational>(r);
+  try
+  {
+    CVC4::Rational r = s.find('/') != std::string::npos
+                           ? CVC4::Rational(s)
+                           : CVC4::Rational::fromDecimal(s);
+    return mkValHelper<CVC4::Rational>(r);
+  }
+  catch (const std::invalid_argument& e)
+  {
+    std::stringstream message;
+    message << "Cannot construct Real or Int from string argument '" << s << "'"
+            << std::endl;
+    throw std::invalid_argument(message.str());
+  }
 }
 
 Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const
@@ -3725,24 +3745,66 @@ Term Solver::mkPi() const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
+Term Solver::mkInteger(const std::string& s) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_ARG_CHECK_EXPECTED(std::regex_match(s, std::regex("-?\\d+")), s)
+      << " an integer ";
+  Term integer = mkRealFromStrHelper(s);
+  CVC4_API_ARG_CHECK_EXPECTED(integer.getSort() == getIntegerSort(), s)
+      << " an integer";
+  return integer;
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
+Term Solver::mkInteger(int64_t val) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  Term integer = mkValHelper<CVC4::Rational>(CVC4::Rational(val));
+  Assert(integer.getSort() == getIntegerSort());
+  return integer;
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
 Term Solver::mkReal(const std::string& s) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return mkRealFromStrHelper(s);
+  /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
+   * throws an std::invalid_argument exception. For consistency, we treat it
+   * as invalid. */
+  CVC4_API_ARG_CHECK_EXPECTED(s != ".", s)
+      << "a string representing a real or rational value.";
+  Term rational = mkRealFromStrHelper(s);
+  return ensureRealSort(rational);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
+Term Solver::ensureRealSort(const Term t) const
+{
+  CVC4_API_ARG_CHECK_EXPECTED(
+      t.getSort() == getIntegerSort() || t.getSort() == getRealSort(),
+      " an integer or real term");
+  if (t.getSort() == getIntegerSort())
+  {
+    Node n = getNodeManager()->mkNode(kind::CAST_TO_REAL, *t.d_node);
+    return Term(this, n);
+  }
+  return t;
+}
+
 Term Solver::mkReal(int64_t val) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return mkValHelper<CVC4::Rational>(CVC4::Rational(val));
+  Term rational = mkValHelper<CVC4::Rational>(CVC4::Rational(val));
+  return ensureRealSort(rational);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Term Solver::mkReal(int64_t num, int64_t den) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
+  Term rational = mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
+  return ensureRealSort(rational);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -3918,10 +3980,17 @@ Term Solver::mkConstArray(Sort sort, Term val) const
   CVC4_API_SOLVER_CHECK_SORT(sort);
   CVC4_API_SOLVER_CHECK_TERM(val);
   CVC4_API_CHECK(sort.isArray()) << "Not an array sort.";
-  CVC4_API_CHECK(sort.getArrayElementSort().isComparableTo(val.getSort()))
+  CVC4_API_CHECK(val.getSort().isSubsortOf(sort.getArrayElementSort()))
       << "Value does not match element sort.";
-  Term res = mkValHelper<CVC4::ArrayStoreAll>(CVC4::ArrayStoreAll(
-      TypeNode::fromType(*sort.d_type), Node::fromExpr(val.d_node->toExpr())));
+  // handle the special case of (CAST_TO_REAL n) where n is an integer
+  Node n = *val.d_node;
+  if (val.isCastedReal())
+  {
+    // this is safe because the constant array stores its type
+    n = n[0];
+  }
+  Term res = mkValHelper<CVC4::ArrayStoreAll>(
+      CVC4::ArrayStoreAll(TypeNode::fromType(*sort.d_type), n));
   return res;
   CVC4_API_SOLVER_TRY_CATCH_END;
 }

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 646695c648bc71c3a78ae32398def0ef44041fec..c05390e42fed6a0d20ceedfcfee9294a1f41eb6c 100644 (file)
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -981,13 +981,6 @@ class CVC4_PUBLIC Term
    */
   bool isNull() const;
 
-  /**
-   * Check if this is a Term representing a value.
-   *
-   * @return true if this is a Term representing a value
-   */
-  bool isValue() const;
-
   /**
    *  Return the base (element stored at all indices) of a constant array
    *  throws an exception if the kind is not CONST_ARRAY
@@ -1175,6 +1168,11 @@ class CVC4_PUBLIC Term
    */
   Kind getKindHelper() const;
 
+  /**
+   * returns true if the current term is a constant integer that is casted into
+   * real using the operator CAST_TO_REAL, and returns false otherwise
+   */
+  bool isCastedReal() const;
   /**
    * The internal expression wrapped by this term.
    * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
@@ -2580,12 +2578,26 @@ class CVC4_PUBLIC Solver
    * @return a constant representing Pi
    */
   Term mkPi() const;
+  /**
+   * Create an integer constant from a string.
+   * @param s the string representation of the constant, may represent an
+   *          integer (e.g., "123").
+   * @return a constant of sort Integer assuming 's' represents an integer)
+   */
+  Term mkInteger(const std::string& s) const;
+
+  /**
+   * Create an integer constant from a c++ int.
+   * @param val the value of the constant
+   * @return a constant of sort Integer
+   */
+  Term mkInteger(int64_t val) const;
 
   /**
    * Create a real constant from a string.
    * @param s the string representation of the constant, may represent an
    *          integer (e.g., "123") or real constant (e.g., "12.34" or "12/34").
-   * @return a constant of sort Real or Integer (if 's' represents an integer)
+   * @return a constant of sort Real
    */
   Term mkReal(const std::string& s) const;
 
@@ -2600,7 +2612,7 @@ class CVC4_PUBLIC Solver
    * Create a real constant from a rational.
    * @param num the value of the numerator
    * @param den the value of the denominator
-   * @return a constant of sort Real or Integer (if 'num' is divisible by 'den')
+   * @return a constant of sort Real
    */
   Term mkReal(int64_t num, int64_t den) const;
 
@@ -3461,10 +3473,10 @@ class CVC4_PUBLIC Solver
   /**
    * Helper function that ensures that a given term is of sort real (as opposed
    * to being of sort integer).
-   * @param term a term of sort integer or real
+   * @param t a term of sort integer or real
    * @return a term of sort real
    */
-  Term ensureRealSort(Term expr) const;
+  Term ensureRealSort(Term t) const;
 
   /**
    * Create n-ary term of given kind. This handles the cases of left/right

diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index 73ccde14a313dcb89b5313b71116c0db435a6c88..113895ad7abcc35a079354721cb03aacf99a8975 100644 (file)
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -173,6 +173,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         Term mkFalse() except +
         Term mkBoolean(bint val) except +
         Term mkPi() except +
+        Term mkInteger(const string& s) except +
         Term mkReal(const string& s) except +
         Term mkRegexpEmpty() except +
         Term mkRegexpSigma() except +
@@ -329,7 +330,6 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         bint hasOp() except +
         Op getOp() except +
         bint isNull() except +
-        bint isValue() except +
         Term getConstArrayBase() except +
         vector[Term] getConstSequenceElements() except +
         Term notTerm() except +

diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index 188b678d1398e7c600438c53ef2786c0b8a261f3..4cdd60893ed7ba4f684ebd8e0d72f090d258dbb1 100644 (file)
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -664,6 +664,12 @@ cdef class Solver:
         term.cterm = self.csolver.mkPi()
         return term
 
+    def mkInteger(self, val):
+        cdef Term term = Term(self)
+        integer = int(val)
+        term.cterm = self.csolver.mkInteger("{}".format(integer).encode())
+        return term
+
     def mkReal(self, val, den=None):
         cdef Term term = Term(self)
         if den is None:
@@ -1448,9 +1454,6 @@ cdef class Term:
     def isNull(self):
         return self.cterm.isNull()
 
-    def isValue(self):
-        return self.cterm.isValue()
-
     def getConstArrayBase(self):
         cdef Term term = Term(self.solver)
         term.cterm = self.cterm.getConstArrayBase()
@@ -1502,7 +1505,6 @@ cdef class Term:
     def toPythonObj(self):
         '''
         Converts a constant value Term to a Python object.
-        Requires isValue to hold.
 
         Currently supports:
           Boolean -- returns a Python bool
@@ -1514,9 +1516,6 @@ cdef class Term:
           String  -- returns a Python Unicode string
         '''
 
-        if not self.isValue():
-            raise RuntimeError("Cannot call toPythonObj on a non-const Term")
-
         string_repr = self.cterm.toString().decode()
         assert string_repr
         sort = self.getSort()

diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp
index 92383dcd189325a1429a8e87f00ac5d5173d7085..ed21f8f9c07a44095852f8182fdd9f4f914321ac 100644 (file)
--- a/src/expr/array_store_all.cpp
+++ b/src/expr/array_store_all.cpp
@@ -45,7 +45,8 @@ ArrayStoreAll::ArrayStoreAll(const TypeNode& type, const Node& value)
       "expr type `%s' does not match constituent type of array type `%s'",
       value.getType().toString().c_str(),
       type.toString().c_str());
-
+  Trace("arrays") << "constructing constant array of type: '" << type
+                  << "' and value: '" << value << "'" << std::endl;
   PrettyCheckArgument(
       value.isConst(), value, "ArrayStoreAll requires a constant expression");
 

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 292871d2a92ce23af880a8ccf010fbd018fc3c46..0bb41b4833521422e0a05aeb14a43f8563a0f282 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -2177,13 +2177,6 @@ simpleTerm[CVC4::api::Term& f]
        * literals, we can use the push/pop scope. */
       /* PARSER_STATE->popScope(); */
       t = SOLVER->mkArraySort(t, t2);
-      if(!f.isValue()) {
-        std::stringstream ss;
-        ss << "expected constant term inside array constant, but found "
-           << "nonconstant term" << std::endl
-           << "the term: " << f;
-        PARSER_STATE->parseError(ss.str());
-      }
       if(!t2.isComparableTo(f.getSort())) {
         std::stringstream ss;
         ss << "type mismatch inside array constant term:" << std::endl
@@ -2207,18 +2200,12 @@ simpleTerm[CVC4::api::Term& f]
       std::stringstream strRat;
       strRat << r;
       f = SOLVER->mkReal(strRat.str());
-      if(f.getSort().isInteger()) {
-        // Must cast to Real to ensure correct type is passed to parametric type constructors.
-        // We do this cast using division with 1.
-        // This has the advantage wrt using TO_REAL since (constant) division is always included in the theory.
-        f = MK_TERM(api::DIVISION, f, SOLVER->mkReal(1));
-      }
     }
   | INTEGER_LITERAL {
       Rational r = AntlrInput::tokenToRational($INTEGER_LITERAL);
       std::stringstream strRat;
       strRat << r;
-      f = SOLVER->mkReal(strRat.str());
+      f = SOLVER->mkInteger(strRat.str());
     }
     /* bitvector literals */
   | HEX_LITERAL

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 7c1c5dc3e909d8e75a1cea303cce14bfaf8c1abd..7647f8e5313ae80ac01d50e4b2b16ff7aade477b 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1710,7 +1710,7 @@ identifier[CVC4::ParseOp& p]
         // we adopt a special syntax (_ tupSel n)
         p.d_kind = api::APPLY_SELECTOR;
         // put m in expr so that the caller can deal with this case
-        p.d_expr = SOLVER->mkReal(AntlrInput::tokenToUnsigned($m));
+        p.d_expr = SOLVER->mkInteger(AntlrInput::tokenToUnsigned($m));
       }
     | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
       {
@@ -1735,7 +1735,7 @@ termAtomic[CVC4::api::Term& atomTerm]
   : INTEGER_LITERAL
     {
       std::string intStr = AntlrInput::tokenText($INTEGER_LITERAL);
-      atomTerm = SOLVER->mkReal(intStr);
+      atomTerm = SOLVER->mkInteger(intStr);
     }
   | DECIMAL_LITERAL
     {
@@ -1830,7 +1830,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
     {
       std::stringstream sIntLit;
       sIntLit << $INTEGER_LITERAL;
-      api::Term n = SOLVER->mkReal(sIntLit.str());
+      api::Term n = SOLVER->mkInteger(sIntLit.str());
       std::vector<api::Term> values;
       values.push_back( n );
       std::string attr_name(AntlrInput::tokenText($tok));

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 629164593d2ee042104bca2e5c5ec020ace87b08..edeb47f06d5f25e92a07c13a8fc9f539de04e4c6 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1055,33 +1055,22 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       parseError("Too many arguments to array constant.");
     }
     api::Term constVal = args[0];
-    if (!constVal.isValue())
+
+    // To parse array constants taking reals whose values are specified by
+    // rationals, e.g. ((as const (Array Int Real)) (/ 1 3)), we must handle
+    // the fact that (/ 1 3) is the division of constants 1 and 3, and not
+    // the resulting constant rational value. Thus, we must construct the
+    // resulting rational here. This also is applied for integral real values
+    // like 5.0 which are converted to (/ 5 1) to distinguish them from
+    // integer constants. We must ensure numerator and denominator are
+    // constant and the denominator is non-zero.
+    if (constVal.getKind() == api::DIVISION)
     {
-      // To parse array constants taking reals whose values are specified by
-      // rationals, e.g. ((as const (Array Int Real)) (/ 1 3)), we must handle
-      // the fact that (/ 1 3) is the division of constants 1 and 3, and not
-      // the resulting constant rational value. Thus, we must construct the
-      // resulting rational here. This also is applied for integral real values
-      // like 5.0 which are converted to (/ 5 1) to distinguish them from
-      // integer constants. We must ensure numerator and denominator are
-      // constant and the denominator is non-zero.
-      if (constVal.getKind() == api::DIVISION && constVal[0].isValue()
-          && constVal[1].isValue()
-          && !constVal[1].getExpr().getConst<Rational>().isZero())
-      {
-        std::stringstream sdiv;
-        sdiv << constVal[0] << "/" << constVal[1];
-        constVal = d_solver->mkReal(sdiv.str());
-      }
-      if (!constVal.isValue())
-      {
-        std::stringstream ss;
-        ss << "expected constant term inside array constant, but found "
-           << "nonconstant term:" << std::endl
-           << "the term: " << constVal;
-        parseError(ss.str());
-      }
+      std::stringstream sdiv;
+      sdiv << constVal[0] << "/" << constVal[1];
+      constVal = d_solver->mkReal(sdiv.str());
     }
+
     if (!p.d_type.getArrayElementSort().isComparableTo(constVal.getSort()))
     {
       std::stringstream ss;

diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index b99376685aa8ddb30cdc9adcd2f7924897e49e76..8e29c25f1a503b74452d3c5803587f823c987635 100644 (file)
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -477,7 +477,7 @@ definedPred[CVC4::ParseOp& p]
       api::Term body =
           MK_TERM(api::AND,
                   MK_TERM(api::NOT,
-                          MK_TERM(api::EQUAL, r, SOLVER->mkReal(0))),
+                          MK_TERM(api::EQUAL, r, SOLVER->mkInteger(0))),
                   MK_TERM(api::EQUAL, qr, MK_TERM(api::MULT, n, rr)));
       api::Term bvl = MK_TERM(api::BOUND_VAR_LIST, q, r);
       body = MK_TERM(api::EXISTS, bvl, body);
@@ -537,7 +537,7 @@ thfDefinedPred[CVC4::ParseOp& p]
       api::Term body = MK_TERM(
           api::AND,
           MK_TERM(api::NOT,
-                  MK_TERM(api::EQUAL, r, SOLVER->mkReal(0))),
+                  MK_TERM(api::EQUAL, r, SOLVER->mkInteger(0))),
           MK_TERM(api::EQUAL, qr, MK_TERM(api::MULT, n, rr)));
       api::Term bvl = MK_TERM(api::BOUND_VAR_LIST, q, r);
       body = MK_TERM(api::EXISTS, bvl, body);
@@ -708,7 +708,7 @@ definedFun[CVC4::ParseOp& p]
                                                   n,
                                                   SOLVER->mkReal(2)),
                                           SOLVER->mkReal(1, 2))),
-                          SOLVER->mkReal(2))));
+                          SOLVER->mkInteger(2))));
       p.d_kind = api::LAMBDA;
       p.d_expr = MK_TERM(api::LAMBDA, formals, expr);
       }
@@ -1747,7 +1747,15 @@ NUMBER
   : ( SIGN[pos]? num=DECIMAL
       { std::stringstream ss;
         ss << ( pos ? "" : "-" ) << AntlrInput::tokenText($num);
-        PARSER_STATE->d_tmp_expr = SOLVER->mkReal(ss.str());
+        std::string str = ss.str();
+        if (str.find(".") == std::string::npos)
+        {
+          PARSER_STATE->d_tmp_expr = SOLVER->mkInteger(str);
+        }
+        else
+        {
+          PARSER_STATE->d_tmp_expr = SOLVER->mkReal(str);
+        }
       }
     | SIGN[pos]? num=DECIMAL DOT den=DECIMAL (EXPONENT SIGN[posE]? e=DECIMAL)?
       {

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index bab619dcead0708d2212c6e7ce26bed7200f78e1..9ccf023017437075a888fb3290360241e510fb90 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -644,6 +644,8 @@ void CvcPrinter::toStream(
       opType = PREFIX;
       break;
     case kind::TO_REAL:
+    case kind::CAST_TO_REAL:
+    {
       if (n[0].getKind() == kind::CONST_RATIONAL)
       {
         // print the constant as a rational
@@ -655,6 +657,7 @@ void CvcPrinter::toStream(
         toStream(out, n[0], depth, types, false);
       }
       return;
+    }
     case kind::DIVISIBLE:
       out << "DIVISIBLE(";
       toStream(out, n[0], depth, types, false);

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 8815f96322bb11a38d0f5cc73fc7ae8a85e13620..a0cd8cf9ca9baded7be7cf71001e497dbc79181f 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -477,10 +477,10 @@ void Smt2Printer::toStream(std::ostream& out,
   bool typeChildren = false;  // operators (op t1...tn) where at least one of t1...tn may require a type cast e.g. Int -> Real
   // operator
   Kind k = n.getKind();
-  if(n.getNumChildren() != 0 &&
-     k != kind::INST_PATTERN_LIST &&
-     k != kind::APPLY_TYPE_ASCRIPTION &&
-     k != kind::CONSTRUCTOR_TYPE) {
+  if (n.getNumChildren() != 0 && k != kind::INST_PATTERN_LIST
+      && k != kind::APPLY_TYPE_ASCRIPTION && k != kind::CONSTRUCTOR_TYPE
+      && k != kind::CAST_TO_REAL)
+  {
     out << '(';
   }
   switch(k) {
@@ -603,11 +603,17 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::ABS:
   case kind::IS_INTEGER:
   case kind::TO_INTEGER:
-  case kind::TO_REAL:
   case kind::POW: 
     parametricTypeChildren = true;
     out << smtKindString(k, d_variant) << " ";
     break;
+  case kind::TO_REAL:
+  case kind::CAST_TO_REAL:
+  {
+    // (to_real 5) is printed as 5.0
+    out << n[0] << ".0";
+    return;
+  }
   case kind::IAND:
     out << "(_ iand " << n.getOperator().getConst<IntAnd>().d_size << ") ";
     stillNeedToPrintParams = false;
@@ -1029,7 +1035,8 @@ void Smt2Printer::toStream(std::ostream& out,
       }
     }
   }
-  if(n.getNumChildren() != 0) {
+  if (n.getNumChildren() != 0)
+  {
     out << parens.str() << ')';
   }
 }/* Smt2Printer::toStream(TNode) */

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index dc91d678e14bc7d46601ff6ef61ab8e068289af1..a65fbd961f1b9b3fa21a3fb7bc6e54377d612028 100644 (file)
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -138,7 +138,7 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
     case kind::TO_INTEGER:
       return RewriteResponse(REWRITE_DONE, t);
     case kind::TO_REAL:
-      return RewriteResponse(REWRITE_DONE, t[0]);
+    case kind::CAST_TO_REAL: return RewriteResponse(REWRITE_DONE, t[0]);
     case kind::POW:
       return RewriteResponse(REWRITE_DONE, t);
     case kind::PI:
@@ -198,7 +198,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
       }
       return RewriteResponse(REWRITE_DONE, t);
     case kind::TO_REAL:
-      return RewriteResponse(REWRITE_DONE, t[0]);
+    case kind::CAST_TO_REAL: return RewriteResponse(REWRITE_DONE, t[0]);
     case kind::TO_INTEGER:
       if(t[0].isConst()) {
         return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(Rational(t[0].getConst<Rational>().floor())));

diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index e563d8f6669410dfb38947486f05f7c872e6d008..fc8f76ee413f248e5fd85ab15eb9dcf6d99146bf 100644 (file)
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -80,9 +80,16 @@ operator LEQ 2 "less than or equal, x <= y"
 operator GT 2 "greater than, x > y"
 operator GEQ 2 "greater than or equal, x >= y"
 
-operator IS_INTEGER 1 "term-is-integer predicate (parameter is a real-sorted term)"
-operator TO_INTEGER 1 "convert term to integer by the floor function (parameter is a real-sorted term)"
-operator TO_REAL 1 "cast term to real (parameter is an integer-sorted term; this is a no-op in CVC4, as integer is a subtype of real)"
+operator IS_INTEGER   1 "term-is-integer predicate (parameter is a real-sorted term)"
+operator TO_INTEGER   1 "convert term to integer by the floor function (parameter is a real-sorted term)"
+operator TO_REAL      1 "cast term to real (parameter is an integer-sorted term; this is a no-op in CVC4, as integer is a subtype of real)"
+
+# CAST_TO_REAL is added to distinguish between integers casted to reals internally, and
+# integers casted to reals or using the API \
+# Solver::mkReal(int val) would return an internal node (CAST_TO_REAL val), but in the api it appears as term (val) \
+# Solver::mkTerm(TO_REAL, Solver::mkInteger(int val)) would return both term and node (TO_REAL val) \
+# This way, we avoid having 2 nested TO_REAL nodess as a result of Solver::mkTerm(TO_REAL, Solver::mkReal(int val))
+operator CAST_TO_REAL 1 "cast term to real same as TO_REAL, but it is used internally, whereas TO_REAL is accessible in the API"
 
 typerule PLUS ::CVC4::theory::arith::ArithOperatorTypeRule
 typerule MULT ::CVC4::theory::arith::ArithOperatorTypeRule
@@ -99,9 +106,10 @@ typerule LEQ "SimpleTypeRule<RBool, AReal, AReal>"
 typerule GT "SimpleTypeRule<RBool, AReal, AReal>"
 typerule GEQ "SimpleTypeRule<RBool, AReal, AReal>"
 
-typerule TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule
-typerule TO_INTEGER ::CVC4::theory::arith::ArithOperatorTypeRule
-typerule IS_INTEGER "SimpleTypeRule<RBool, AReal>"
+typerule TO_REAL      ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule CAST_TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule TO_INTEGER   ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule IS_INTEGER   "SimpleTypeRule<RBool, AReal>"
 
 typerule ABS "SimpleTypeRule<RInteger, AInteger>"
 typerule INTS_DIVISION "SimpleTypeRule<RInteger, AInteger, AInteger>"

diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 9dd18d84b7e809fa5d4fd94db315a34ef92f292b..0aa9cd4b387ef768f15a64486812ddc74d655012 100644 (file)
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -60,12 +60,13 @@ public:
         }
       }
     }
-    switch(Kind k = n.getKind()) {
+    switch (Kind k = n.getKind())
+    {
       case kind::TO_REAL:
-        return realType;
-      case kind::TO_INTEGER:
-        return integerType;
-      default: {
+      case kind::CAST_TO_REAL: return realType;
+      case kind::TO_INTEGER: return integerType;
+      default:
+      {
         bool isDivision = k == kind::DIVISION || k == kind::DIVISION_TOTAL;
         return (isInteger && !isDivision ? integerType : realType);
       }

diff --git a/test/api/reset_assertions.cpp b/test/api/reset_assertions.cpp
index 73629a0d05a800c5e82250c8cf057cbfe5f55152..2168d053e8e7f1f89731fce139c5a032bd4638e9 100644 (file)
--- 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 f0a55cf79757d66eacf30692e913a32b65f4d41d..1b1efb07ed1f8b90f33f6aa981504f8d9217d799 100644 (file)
--- 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 b75f535d5d92855ad8900256b9473b3c49dbb928..c8d3bb348f49de2dc0743a07264a8a5a1135dd49 100644 (file)
--- 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 09ec0917f746514706d230ca28d65b602c5b3af9..d27581114338b68cb941c436cf81bf00140c1fed 100644 (file)
--- 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 bf0d97e9ddd7b3a3b22b04e8c3c31e37e0aceb20..afbd09d0f0fd4aa06747daae7bd700713bcf1da7 100644 (file)
--- 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 0321f03d09cc28eeafa1fbd7092aafbb80fd13fb..5a0d5101f2c6e578d1f40e3ea7a5f2eb8d26382a 100644 (file)
--- 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 9c25b584fbc6c86c9067f86bac7edede6343a921..a0c1b46813060a011859e11e826159f72abdfcdf 100644 (file)
--- 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 3ce08f6b8d1c116b07ba2c18c4d5f167cd748b40..eb15e74696a0e6740085a384110d2bace754b95c 100644 (file)
--- 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 8b8c6dd58f113d57bd033958210bdd96b6042b94..1324e3890af04070052bf7f74ec2768e71be354c 100644 (file)
--- 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 786b60bb375310d3124289cb450a3b802c471c56..bebfc6e1f7744a661b6efb3edf13fa9451e71394 100644 (file)
--- 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 c098ca9b8a4241a82f95d8427a1e32ffe3fb473b..f06c1f77d67bbecfb55c23a6b12b5492f0b6f8a6 100644 (file)
--- 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