test/unit/api/cpp/term_black.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Aina Niemetz, Makai Mann, Andrew Reynolds
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * Black box testing of the Term class.
  14  */
  15
  16 #include "test_api.h"
  17
  18 namespace cvc5::internal {
  19
  20 namespace test {
  21
  22 class TestApiBlackTerm : public TestApi
  23 {
  24 };
  25
  26 TEST_F(TestApiBlackTerm, eq)
  27 {
  28   Sort uSort = d_solver.mkUninterpretedSort("u");
  29   Term x = d_solver.mkVar(uSort, "x");
  30   Term y = d_solver.mkVar(uSort, "y");
  31   Term z;
  32
  33   ASSERT_TRUE(x == x);
  34   ASSERT_FALSE(x != x);
  35   ASSERT_FALSE(x == y);
  36   ASSERT_TRUE(x != y);
  37   ASSERT_FALSE((x == z));
  38   ASSERT_TRUE(x != z);
  39 }
  40
  41 TEST_F(TestApiBlackTerm, getId)
  42 {
  43   Term n;
  44   ASSERT_THROW(n.getId(), CVC5ApiException);
  45   Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x");
  46   ASSERT_NO_THROW(x.getId());
  47   Term y = x;
  48   ASSERT_EQ(x.getId(), y.getId());
  49
  50   Term z = d_solver.mkVar(d_solver.getIntegerSort(), "z");
  51   ASSERT_NE(x.getId(), z.getId());
  52 }
  53
  54 TEST_F(TestApiBlackTerm, getKind)
  55 {
  56   Sort uSort = d_solver.mkUninterpretedSort("u");
  57   Sort intSort = d_solver.getIntegerSort();
  58   Sort boolSort = d_solver.getBooleanSort();
  59   Sort funSort1 = d_solver.mkFunctionSort({uSort}, intSort);
  60   Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
  61
  62   Term n;
  63   ASSERT_THROW(n.getKind(), CVC5ApiException);
  64   Term x = d_solver.mkVar(uSort, "x");
  65   ASSERT_NO_THROW(x.getKind());
  66   Term y = d_solver.mkVar(uSort, "y");
  67   ASSERT_NO_THROW(y.getKind());
  68
  69   Term f = d_solver.mkVar(funSort1, "f");
  70   ASSERT_NO_THROW(f.getKind());
  71   Term p = d_solver.mkVar(funSort2, "p");
  72   ASSERT_NO_THROW(p.getKind());
  73
  74   Term zero = d_solver.mkInteger(0);
  75   ASSERT_NO_THROW(zero.getKind());
  76
  77   Term f_x = d_solver.mkTerm(APPLY_UF, {f, x});
  78   ASSERT_NO_THROW(f_x.getKind());
  79   Term f_y = d_solver.mkTerm(APPLY_UF, {f, y});
  80   ASSERT_NO_THROW(f_y.getKind());
  81   Term sum = d_solver.mkTerm(ADD, {f_x, f_y});
  82   ASSERT_NO_THROW(sum.getKind());
  83   Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero});
  84   ASSERT_NO_THROW(p_0.getKind());
  85   Term p_f_y = d_solver.mkTerm(APPLY_UF, {p, f_y});
  86   ASSERT_NO_THROW(p_f_y.getKind());
  87
  88   // Sequence kinds do not exist internally, test that the API properly
  89   // converts them back.
  90   Sort seqSort = d_solver.mkSequenceSort(intSort);
  91   Term s = d_solver.mkConst(seqSort, "s");
  92   Term ss = d_solver.mkTerm(SEQ_CONCAT, {s, s});
  93   ASSERT_EQ(ss.getKind(), SEQ_CONCAT);
  94 }
  95
  96 TEST_F(TestApiBlackTerm, getSort)
  97 {
  98   Sort bvSort = d_solver.mkBitVectorSort(8);
  99   Sort intSort = d_solver.getIntegerSort();
 100   Sort boolSort = d_solver.getBooleanSort();
 101   Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
 102   Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
 103
 104   Term n;
 105   ASSERT_THROW(n.getSort(), CVC5ApiException);
 106   Term x = d_solver.mkVar(bvSort, "x");
 107   ASSERT_NO_THROW(x.getSort());
 108   ASSERT_EQ(x.getSort(), bvSort);
 109   Term y = d_solver.mkVar(bvSort, "y");
 110   ASSERT_NO_THROW(y.getSort());
 111   ASSERT_EQ(y.getSort(), bvSort);
 112
 113   Term f = d_solver.mkVar(funSort1, "f");
 114   ASSERT_NO_THROW(f.getSort());
 115   ASSERT_EQ(f.getSort(), funSort1);
 116   Term p = d_solver.mkVar(funSort2, "p");
 117   ASSERT_NO_THROW(p.getSort());
 118   ASSERT_EQ(p.getSort(), funSort2);
 119
 120   Term zero = d_solver.mkInteger(0);
 121   ASSERT_NO_THROW(zero.getSort());
 122   ASSERT_EQ(zero.getSort(), intSort);
 123
 124   Term f_x = d_solver.mkTerm(APPLY_UF, {f, x});
 125   ASSERT_NO_THROW(f_x.getSort());
 126   ASSERT_EQ(f_x.getSort(), intSort);
 127   Term f_y = d_solver.mkTerm(APPLY_UF, {f, y});
 128   ASSERT_NO_THROW(f_y.getSort());
 129   ASSERT_EQ(f_y.getSort(), intSort);
 130   Term sum = d_solver.mkTerm(ADD, {f_x, f_y});
 131   ASSERT_NO_THROW(sum.getSort());
 132   ASSERT_EQ(sum.getSort(), intSort);
 133   Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero});
 134   ASSERT_NO_THROW(p_0.getSort());
 135   ASSERT_EQ(p_0.getSort(), boolSort);
 136   Term p_f_y = d_solver.mkTerm(APPLY_UF, {p, f_y});
 137   ASSERT_NO_THROW(p_f_y.getSort());
 138   ASSERT_EQ(p_f_y.getSort(), boolSort);
 139 }
 140
 141 TEST_F(TestApiBlackTerm, getOp)
 142 {
 143   Sort intsort = d_solver.getIntegerSort();
 144   Sort bvsort = d_solver.mkBitVectorSort(8);
 145   Sort arrsort = d_solver.mkArraySort(bvsort, intsort);
 146   Sort funsort = d_solver.mkFunctionSort({intsort}, bvsort);
 147
 148   Term x = d_solver.mkConst(intsort, "x");
 149   Term a = d_solver.mkConst(arrsort, "a");
 150   Term b = d_solver.mkConst(bvsort, "b");
 151
 152   ASSERT_FALSE(x.hasOp());
 153   ASSERT_THROW(x.getOp(), CVC5ApiException);
 154
 155   Term ab = d_solver.mkTerm(SELECT, {a, b});
 156   Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, {4, 0});
 157   Term extb = d_solver.mkTerm(ext, {b});
 158
 159   ASSERT_TRUE(ab.hasOp());
 160   ASSERT_FALSE(ab.getOp().isIndexed());
 161   // can compare directly to a Kind (will invoke Op constructor)
 162   ASSERT_TRUE(extb.hasOp());
 163   ASSERT_TRUE(extb.getOp().isIndexed());
 164   ASSERT_EQ(extb.getOp(), ext);
 165
 166   Term f = d_solver.mkConst(funsort, "f");
 167   Term fx = d_solver.mkTerm(APPLY_UF, {f, x});
 168
 169   ASSERT_FALSE(f.hasOp());
 170   ASSERT_THROW(f.getOp(), CVC5ApiException);
 171   ASSERT_TRUE(fx.hasOp());
 172   std::vector<Term> children(fx.begin(), fx.end());
 173   // testing rebuild from op and children
 174   ASSERT_EQ(fx, d_solver.mkTerm(fx.getOp(), children));
 175
 176   // Test Datatypes Ops
 177   Sort sort = d_solver.mkParamSort("T");
 178   DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort);
 179   DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
 180   DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
 181   cons.addSelector("head", sort);
 182   cons.addSelectorSelf("tail");
 183   listDecl.addConstructor(cons);
 184   listDecl.addConstructor(nil);
 185   Sort listSort = d_solver.mkDatatypeSort(listDecl);
 186   Sort intListSort =
 187       listSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()});
 188   Term c = d_solver.mkConst(intListSort, "c");
 189   Datatype list = listSort.getDatatype();
 190   // list datatype constructor and selector operator terms
 191   Term consOpTerm = list.getConstructor("cons").getTerm();
 192   Term nilOpTerm = list.getConstructor("nil").getTerm();
 193   Term headOpTerm = list["cons"].getSelector("head").getTerm();
 194   Term tailOpTerm = list["cons"].getSelector("tail").getTerm();
 195
 196   Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilOpTerm});
 197   Term consTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR,
 198                                   {consOpTerm, d_solver.mkInteger(0), nilTerm});
 199   Term headTerm = d_solver.mkTerm(APPLY_SELECTOR, {headOpTerm, consTerm});
 200   Term tailTerm = d_solver.mkTerm(APPLY_SELECTOR, {tailOpTerm, consTerm});
 201
 202   ASSERT_TRUE(nilTerm.hasOp());
 203   ASSERT_TRUE(consTerm.hasOp());
 204   ASSERT_TRUE(headTerm.hasOp());
 205   ASSERT_TRUE(tailTerm.hasOp());
 206
 207   // Test rebuilding
 208   children.clear();
 209   children.insert(children.begin(), headTerm.begin(), headTerm.end());
 210   ASSERT_EQ(headTerm, d_solver.mkTerm(headTerm.getOp(), children));
 211 }
 212
 213 TEST_F(TestApiBlackTerm, hasGetSymbol)
 214 {
 215   Term n;
 216   Term t = d_solver.mkBoolean(true);
 217   Term c = d_solver.mkConst(d_solver.getBooleanSort(), "|\\|");
 218
 219   ASSERT_THROW(n.hasSymbol(), CVC5ApiException);
 220   ASSERT_FALSE(t.hasSymbol());
 221   ASSERT_TRUE(c.hasSymbol());
 222
 223   ASSERT_THROW(n.getSymbol(), CVC5ApiException);
 224   ASSERT_THROW(t.getSymbol(), CVC5ApiException);
 225   ASSERT_EQ(c.getSymbol(), "|\\|");
 226 }
 227
 228 TEST_F(TestApiBlackTerm, isNull)
 229 {
 230   Term x;
 231   ASSERT_TRUE(x.isNull());
 232   x = d_solver.mkVar(d_solver.mkBitVectorSort(4), "x");
 233   ASSERT_FALSE(x.isNull());
 234 }
 235
 236 TEST_F(TestApiBlackTerm, notTerm)
 237 {
 238   Sort bvSort = d_solver.mkBitVectorSort(8);
 239   Sort intSort = d_solver.getIntegerSort();
 240   Sort boolSort = d_solver.getBooleanSort();
 241   Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
 242   Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
 243
 244   ASSERT_THROW(Term().notTerm(), CVC5ApiException);
 245   Term b = d_solver.mkTrue();
 246   ASSERT_NO_THROW(b.notTerm());
 247   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
 248   ASSERT_THROW(x.notTerm(), CVC5ApiException);
 249   Term f = d_solver.mkVar(funSort1, "f");
 250   ASSERT_THROW(f.notTerm(), CVC5ApiException);
 251   Term p = d_solver.mkVar(funSort2, "p");
 252   ASSERT_THROW(p.notTerm(), CVC5ApiException);
 253   Term zero = d_solver.mkInteger(0);
 254   ASSERT_THROW(zero.notTerm(), CVC5ApiException);
 255   Term f_x = d_solver.mkTerm(APPLY_UF, {f, x});
 256   ASSERT_THROW(f_x.notTerm(), CVC5ApiException);
 257   Term sum = d_solver.mkTerm(ADD, {f_x, f_x});
 258   ASSERT_THROW(sum.notTerm(), CVC5ApiException);
 259   Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero});
 260   ASSERT_NO_THROW(p_0.notTerm());
 261   Term p_f_x = d_solver.mkTerm(APPLY_UF, {p, f_x});
 262   ASSERT_NO_THROW(p_f_x.notTerm());
 263 }
 264
 265 TEST_F(TestApiBlackTerm, andTerm)
 266 {
 267   Sort bvSort = d_solver.mkBitVectorSort(8);
 268   Sort intSort = d_solver.getIntegerSort();
 269   Sort boolSort = d_solver.getBooleanSort();
 270   Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
 271   Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
 272
 273   Term b = d_solver.mkTrue();
 274   ASSERT_THROW(Term().andTerm(b), CVC5ApiException);
 275   ASSERT_THROW(b.andTerm(Term()), CVC5ApiException);
 276   ASSERT_NO_THROW(b.andTerm(b));
 277   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
 278   ASSERT_THROW(x.andTerm(b), CVC5ApiException);
 279   ASSERT_THROW(x.andTerm(x), CVC5ApiException);
 280   Term f = d_solver.mkVar(funSort1, "f");
 281   ASSERT_THROW(f.andTerm(b), CVC5ApiException);
 282   ASSERT_THROW(f.andTerm(x), CVC5ApiException);
 283   ASSERT_THROW(f.andTerm(f), CVC5ApiException);
 284   Term p = d_solver.mkVar(funSort2, "p");
 285   ASSERT_THROW(p.andTerm(b), CVC5ApiException);
 286   ASSERT_THROW(p.andTerm(x), CVC5ApiException);
 287   ASSERT_THROW(p.andTerm(f), CVC5ApiException);
 288   ASSERT_THROW(p.andTerm(p), CVC5ApiException);
 289   Term zero = d_solver.mkInteger(0);
 290   ASSERT_THROW(zero.andTerm(b), CVC5ApiException);
 291   ASSERT_THROW(zero.andTerm(x), CVC5ApiException);
 292   ASSERT_THROW(zero.andTerm(f), CVC5ApiException);
 293   ASSERT_THROW(zero.andTerm(p), CVC5ApiException);
 294   ASSERT_THROW(zero.andTerm(zero), CVC5ApiException);
 295   Term f_x = d_solver.mkTerm(APPLY_UF, {f, x});
 296   ASSERT_THROW(f_x.andTerm(b), CVC5ApiException);
 297   ASSERT_THROW(f_x.andTerm(x), CVC5ApiException);
 298   ASSERT_THROW(f_x.andTerm(f), CVC5ApiException);
 299   ASSERT_THROW(f_x.andTerm(p), CVC5ApiException);
 300   ASSERT_THROW(f_x.andTerm(zero), CVC5ApiException);
 301   ASSERT_THROW(f_x.andTerm(f_x), CVC5ApiException);
 302   Term sum = d_solver.mkTerm(ADD, {f_x, f_x});
 303   ASSERT_THROW(sum.andTerm(b), CVC5ApiException);
 304   ASSERT_THROW(sum.andTerm(x), CVC5ApiException);
 305   ASSERT_THROW(sum.andTerm(f), CVC5ApiException);
 306   ASSERT_THROW(sum.andTerm(p), CVC5ApiException);
 307   ASSERT_THROW(sum.andTerm(zero), CVC5ApiException);
 308   ASSERT_THROW(sum.andTerm(f_x), CVC5ApiException);
 309   ASSERT_THROW(sum.andTerm(sum), CVC5ApiException);
 310   Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero});
 311   ASSERT_NO_THROW(p_0.andTerm(b));
 312   ASSERT_THROW(p_0.andTerm(x), CVC5ApiException);
 313   ASSERT_THROW(p_0.andTerm(f), CVC5ApiException);
 314   ASSERT_THROW(p_0.andTerm(p), CVC5ApiException);
 315   ASSERT_THROW(p_0.andTerm(zero), CVC5ApiException);
 316   ASSERT_THROW(p_0.andTerm(f_x), CVC5ApiException);
 317   ASSERT_THROW(p_0.andTerm(sum), CVC5ApiException);
 318   ASSERT_NO_THROW(p_0.andTerm(p_0));
 319   Term p_f_x = d_solver.mkTerm(APPLY_UF, {p, f_x});
 320   ASSERT_NO_THROW(p_f_x.andTerm(b));
 321   ASSERT_THROW(p_f_x.andTerm(x), CVC5ApiException);
 322   ASSERT_THROW(p_f_x.andTerm(f), CVC5ApiException);
 323   ASSERT_THROW(p_f_x.andTerm(p), CVC5ApiException);
 324   ASSERT_THROW(p_f_x.andTerm(zero), CVC5ApiException);
 325   ASSERT_THROW(p_f_x.andTerm(f_x), CVC5ApiException);
 326   ASSERT_THROW(p_f_x.andTerm(sum), CVC5ApiException);
 327   ASSERT_NO_THROW(p_f_x.andTerm(p_0));
 328   ASSERT_NO_THROW(p_f_x.andTerm(p_f_x));
 329 }
 330
 331 TEST_F(TestApiBlackTerm, orTerm)
 332 {
 333   Sort bvSort = d_solver.mkBitVectorSort(8);
 334   Sort intSort = d_solver.getIntegerSort();
 335   Sort boolSort = d_solver.getBooleanSort();
 336   Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
 337   Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
 338
 339   Term b = d_solver.mkTrue();
 340   ASSERT_THROW(Term().orTerm(b), CVC5ApiException);
 341   ASSERT_THROW(b.orTerm(Term()), CVC5ApiException);
 342   ASSERT_NO_THROW(b.orTerm(b));
 343   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
 344   ASSERT_THROW(x.orTerm(b), CVC5ApiException);
 345   ASSERT_THROW(x.orTerm(x), CVC5ApiException);
 346   Term f = d_solver.mkVar(funSort1, "f");
 347   ASSERT_THROW(f.orTerm(b), CVC5ApiException);
 348   ASSERT_THROW(f.orTerm(x), CVC5ApiException);
 349   ASSERT_THROW(f.orTerm(f), CVC5ApiException);
 350   Term p = d_solver.mkVar(funSort2, "p");
 351   ASSERT_THROW(p.orTerm(b), CVC5ApiException);
 352   ASSERT_THROW(p.orTerm(x), CVC5ApiException);
 353   ASSERT_THROW(p.orTerm(f), CVC5ApiException);
 354   ASSERT_THROW(p.orTerm(p), CVC5ApiException);
 355   Term zero = d_solver.mkInteger(0);
 356   ASSERT_THROW(zero.orTerm(b), CVC5ApiException);
 357   ASSERT_THROW(zero.orTerm(x), CVC5ApiException);
 358   ASSERT_THROW(zero.orTerm(f), CVC5ApiException);
 359   ASSERT_THROW(zero.orTerm(p), CVC5ApiException);
 360   ASSERT_THROW(zero.orTerm(zero), CVC5ApiException);
 361   Term f_x = d_solver.mkTerm(APPLY_UF, {f, x});
 362   ASSERT_THROW(f_x.orTerm(b), CVC5ApiException);
 363   ASSERT_THROW(f_x.orTerm(x), CVC5ApiException);
 364   ASSERT_THROW(f_x.orTerm(f), CVC5ApiException);
 365   ASSERT_THROW(f_x.orTerm(p), CVC5ApiException);
 366   ASSERT_THROW(f_x.orTerm(zero), CVC5ApiException);
 367   ASSERT_THROW(f_x.orTerm(f_x), CVC5ApiException);
 368   Term sum = d_solver.mkTerm(ADD, {f_x, f_x});
 369   ASSERT_THROW(sum.orTerm(b), CVC5ApiException);
 370   ASSERT_THROW(sum.orTerm(x), CVC5ApiException);
 371   ASSERT_THROW(sum.orTerm(f), CVC5ApiException);
 372   ASSERT_THROW(sum.orTerm(p), CVC5ApiException);
 373   ASSERT_THROW(sum.orTerm(zero), CVC5ApiException);
 374   ASSERT_THROW(sum.orTerm(f_x), CVC5ApiException);
 375   ASSERT_THROW(sum.orTerm(sum), CVC5ApiException);
 376   Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero});
 377   ASSERT_NO_THROW(p_0.orTerm(b));
 378   ASSERT_THROW(p_0.orTerm(x), CVC5ApiException);
 379   ASSERT_THROW(p_0.orTerm(f), CVC5ApiException);
 380   ASSERT_THROW(p_0.orTerm(p), CVC5ApiException);
 381   ASSERT_THROW(p_0.orTerm(zero), CVC5ApiException);
 382   ASSERT_THROW(p_0.orTerm(f_x), CVC5ApiException);
 383   ASSERT_THROW(p_0.orTerm(sum), CVC5ApiException);
 384   ASSERT_NO_THROW(p_0.orTerm(p_0));
 385   Term p_f_x = d_solver.mkTerm(APPLY_UF, {p, f_x});
 386   ASSERT_NO_THROW(p_f_x.orTerm(b));
 387   ASSERT_THROW(p_f_x.orTerm(x), CVC5ApiException);
 388   ASSERT_THROW(p_f_x.orTerm(f), CVC5ApiException);
 389   ASSERT_THROW(p_f_x.orTerm(p), CVC5ApiException);
 390   ASSERT_THROW(p_f_x.orTerm(zero), CVC5ApiException);
 391   ASSERT_THROW(p_f_x.orTerm(f_x), CVC5ApiException);
 392   ASSERT_THROW(p_f_x.orTerm(sum), CVC5ApiException);
 393   ASSERT_NO_THROW(p_f_x.orTerm(p_0));
 394   ASSERT_NO_THROW(p_f_x.orTerm(p_f_x));
 395 }
 396
 397 TEST_F(TestApiBlackTerm, xorTerm)
 398 {
 399   Sort bvSort = d_solver.mkBitVectorSort(8);
 400   Sort intSort = d_solver.getIntegerSort();
 401   Sort boolSort = d_solver.getBooleanSort();
 402   Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
 403   Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
 404
 405   Term b = d_solver.mkTrue();
 406   ASSERT_THROW(Term().xorTerm(b), CVC5ApiException);
 407   ASSERT_THROW(b.xorTerm(Term()), CVC5ApiException);
 408   ASSERT_NO_THROW(b.xorTerm(b));
 409   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
 410   ASSERT_THROW(x.xorTerm(b), CVC5ApiException);
 411   ASSERT_THROW(x.xorTerm(x), CVC5ApiException);
 412   Term f = d_solver.mkVar(funSort1, "f");
 413   ASSERT_THROW(f.xorTerm(b), CVC5ApiException);
 414   ASSERT_THROW(f.xorTerm(x), CVC5ApiException);
 415   ASSERT_THROW(f.xorTerm(f), CVC5ApiException);
 416   Term p = d_solver.mkVar(funSort2, "p");
 417   ASSERT_THROW(p.xorTerm(b), CVC5ApiException);
 418   ASSERT_THROW(p.xorTerm(x), CVC5ApiException);
 419   ASSERT_THROW(p.xorTerm(f), CVC5ApiException);
 420   ASSERT_THROW(p.xorTerm(p), CVC5ApiException);
 421   Term zero = d_solver.mkInteger(0);
 422   ASSERT_THROW(zero.xorTerm(b), CVC5ApiException);
 423   ASSERT_THROW(zero.xorTerm(x), CVC5ApiException);
 424   ASSERT_THROW(zero.xorTerm(f), CVC5ApiException);
 425   ASSERT_THROW(zero.xorTerm(p), CVC5ApiException);
 426   ASSERT_THROW(zero.xorTerm(zero), CVC5ApiException);
 427   Term f_x = d_solver.mkTerm(APPLY_UF, {f, x});
 428   ASSERT_THROW(f_x.xorTerm(b), CVC5ApiException);
 429   ASSERT_THROW(f_x.xorTerm(x), CVC5ApiException);
 430   ASSERT_THROW(f_x.xorTerm(f), CVC5ApiException);
 431   ASSERT_THROW(f_x.xorTerm(p), CVC5ApiException);
 432   ASSERT_THROW(f_x.xorTerm(zero), CVC5ApiException);
 433   ASSERT_THROW(f_x.xorTerm(f_x), CVC5ApiException);
 434   Term sum = d_solver.mkTerm(ADD, {f_x, f_x});
 435   ASSERT_THROW(sum.xorTerm(b), CVC5ApiException);
 436   ASSERT_THROW(sum.xorTerm(x), CVC5ApiException);
 437   ASSERT_THROW(sum.xorTerm(f), CVC5ApiException);
 438   ASSERT_THROW(sum.xorTerm(p), CVC5ApiException);
 439   ASSERT_THROW(sum.xorTerm(zero), CVC5ApiException);
 440   ASSERT_THROW(sum.xorTerm(f_x), CVC5ApiException);
 441   ASSERT_THROW(sum.xorTerm(sum), CVC5ApiException);
 442   Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero});
 443   ASSERT_NO_THROW(p_0.xorTerm(b));
 444   ASSERT_THROW(p_0.xorTerm(x), CVC5ApiException);
 445   ASSERT_THROW(p_0.xorTerm(f), CVC5ApiException);
 446   ASSERT_THROW(p_0.xorTerm(p), CVC5ApiException);
 447   ASSERT_THROW(p_0.xorTerm(zero), CVC5ApiException);
 448   ASSERT_THROW(p_0.xorTerm(f_x), CVC5ApiException);
 449   ASSERT_THROW(p_0.xorTerm(sum), CVC5ApiException);
 450   ASSERT_NO_THROW(p_0.xorTerm(p_0));
 451   Term p_f_x = d_solver.mkTerm(APPLY_UF, {p, f_x});
 452   ASSERT_NO_THROW(p_f_x.xorTerm(b));
 453   ASSERT_THROW(p_f_x.xorTerm(x), CVC5ApiException);
 454   ASSERT_THROW(p_f_x.xorTerm(f), CVC5ApiException);
 455   ASSERT_THROW(p_f_x.xorTerm(p), CVC5ApiException);
 456   ASSERT_THROW(p_f_x.xorTerm(zero), CVC5ApiException);
 457   ASSERT_THROW(p_f_x.xorTerm(f_x), CVC5ApiException);
 458   ASSERT_THROW(p_f_x.xorTerm(sum), CVC5ApiException);
 459   ASSERT_NO_THROW(p_f_x.xorTerm(p_0));
 460   ASSERT_NO_THROW(p_f_x.xorTerm(p_f_x));
 461 }
 462
 463 TEST_F(TestApiBlackTerm, eqTerm)
 464 {
 465   Sort bvSort = d_solver.mkBitVectorSort(8);
 466   Sort intSort = d_solver.getIntegerSort();
 467   Sort boolSort = d_solver.getBooleanSort();
 468   Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
 469   Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
 470
 471   Term b = d_solver.mkTrue();
 472   ASSERT_THROW(Term().eqTerm(b), CVC5ApiException);
 473   ASSERT_THROW(b.eqTerm(Term()), CVC5ApiException);
 474   ASSERT_NO_THROW(b.eqTerm(b));
 475   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
 476   ASSERT_THROW(x.eqTerm(b), CVC5ApiException);
 477   ASSERT_NO_THROW(x.eqTerm(x));
 478   Term f = d_solver.mkVar(funSort1, "f");
 479   ASSERT_THROW(f.eqTerm(b), CVC5ApiException);
 480   ASSERT_THROW(f.eqTerm(x), CVC5ApiException);
 481   ASSERT_NO_THROW(f.eqTerm(f));
 482   Term p = d_solver.mkVar(funSort2, "p");
 483   ASSERT_THROW(p.eqTerm(b), CVC5ApiException);
 484   ASSERT_THROW(p.eqTerm(x), CVC5ApiException);
 485   ASSERT_THROW(p.eqTerm(f), CVC5ApiException);
 486   ASSERT_NO_THROW(p.eqTerm(p));
 487   Term zero = d_solver.mkInteger(0);
 488   ASSERT_THROW(zero.eqTerm(b), CVC5ApiException);
 489   ASSERT_THROW(zero.eqTerm(x), CVC5ApiException);
 490   ASSERT_THROW(zero.eqTerm(f), CVC5ApiException);
 491   ASSERT_THROW(zero.eqTerm(p), CVC5ApiException);
 492   ASSERT_NO_THROW(zero.eqTerm(zero));
 493   Term f_x = d_solver.mkTerm(APPLY_UF, {f, x});
 494   ASSERT_THROW(f_x.eqTerm(b), CVC5ApiException);
 495   ASSERT_THROW(f_x.eqTerm(x), CVC5ApiException);
 496   ASSERT_THROW(f_x.eqTerm(f), CVC5ApiException);
 497   ASSERT_THROW(f_x.eqTerm(p), CVC5ApiException);
 498   ASSERT_NO_THROW(f_x.eqTerm(zero));
 499   ASSERT_NO_THROW(f_x.eqTerm(f_x));
 500   Term sum = d_solver.mkTerm(ADD, {f_x, f_x});
 501   ASSERT_THROW(sum.eqTerm(b), CVC5ApiException);
 502   ASSERT_THROW(sum.eqTerm(x), CVC5ApiException);
 503   ASSERT_THROW(sum.eqTerm(f), CVC5ApiException);
 504   ASSERT_THROW(sum.eqTerm(p), CVC5ApiException);
 505   ASSERT_NO_THROW(sum.eqTerm(zero));
 506   ASSERT_NO_THROW(sum.eqTerm(f_x));
 507   ASSERT_NO_THROW(sum.eqTerm(sum));
 508   Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero});
 509   ASSERT_NO_THROW(p_0.eqTerm(b));
 510   ASSERT_THROW(p_0.eqTerm(x), CVC5ApiException);
 511   ASSERT_THROW(p_0.eqTerm(f), CVC5ApiException);
 512   ASSERT_THROW(p_0.eqTerm(p), CVC5ApiException);
 513   ASSERT_THROW(p_0.eqTerm(zero), CVC5ApiException);
 514   ASSERT_THROW(p_0.eqTerm(f_x), CVC5ApiException);
 515   ASSERT_THROW(p_0.eqTerm(sum), CVC5ApiException);
 516   ASSERT_NO_THROW(p_0.eqTerm(p_0));
 517   Term p_f_x = d_solver.mkTerm(APPLY_UF, {p, f_x});
 518   ASSERT_NO_THROW(p_f_x.eqTerm(b));
 519   ASSERT_THROW(p_f_x.eqTerm(x), CVC5ApiException);
 520   ASSERT_THROW(p_f_x.eqTerm(f), CVC5ApiException);
 521   ASSERT_THROW(p_f_x.eqTerm(p), CVC5ApiException);
 522   ASSERT_THROW(p_f_x.eqTerm(zero), CVC5ApiException);
 523   ASSERT_THROW(p_f_x.eqTerm(f_x), CVC5ApiException);
 524   ASSERT_THROW(p_f_x.eqTerm(sum), CVC5ApiException);
 525   ASSERT_NO_THROW(p_f_x.eqTerm(p_0));
 526   ASSERT_NO_THROW(p_f_x.eqTerm(p_f_x));
 527 }
 528
 529 TEST_F(TestApiBlackTerm, impTerm)
 530 {
 531   Sort bvSort = d_solver.mkBitVectorSort(8);
 532   Sort intSort = d_solver.getIntegerSort();
 533   Sort boolSort = d_solver.getBooleanSort();
 534   Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
 535   Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
 536
 537   Term b = d_solver.mkTrue();
 538   ASSERT_THROW(Term().impTerm(b), CVC5ApiException);
 539   ASSERT_THROW(b.impTerm(Term()), CVC5ApiException);
 540   ASSERT_NO_THROW(b.impTerm(b));
 541   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
 542   ASSERT_THROW(x.impTerm(b), CVC5ApiException);
 543   ASSERT_THROW(x.impTerm(x), CVC5ApiException);
 544   Term f = d_solver.mkVar(funSort1, "f");
 545   ASSERT_THROW(f.impTerm(b), CVC5ApiException);
 546   ASSERT_THROW(f.impTerm(x), CVC5ApiException);
 547   ASSERT_THROW(f.impTerm(f), CVC5ApiException);
 548   Term p = d_solver.mkVar(funSort2, "p");
 549   ASSERT_THROW(p.impTerm(b), CVC5ApiException);
 550   ASSERT_THROW(p.impTerm(x), CVC5ApiException);
 551   ASSERT_THROW(p.impTerm(f), CVC5ApiException);
 552   ASSERT_THROW(p.impTerm(p), CVC5ApiException);
 553   Term zero = d_solver.mkInteger(0);
 554   ASSERT_THROW(zero.impTerm(b), CVC5ApiException);
 555   ASSERT_THROW(zero.impTerm(x), CVC5ApiException);
 556   ASSERT_THROW(zero.impTerm(f), CVC5ApiException);
 557   ASSERT_THROW(zero.impTerm(p), CVC5ApiException);
 558   ASSERT_THROW(zero.impTerm(zero), CVC5ApiException);
 559   Term f_x = d_solver.mkTerm(APPLY_UF, {f, x});
 560   ASSERT_THROW(f_x.impTerm(b), CVC5ApiException);
 561   ASSERT_THROW(f_x.impTerm(x), CVC5ApiException);
 562   ASSERT_THROW(f_x.impTerm(f), CVC5ApiException);
 563   ASSERT_THROW(f_x.impTerm(p), CVC5ApiException);
 564   ASSERT_THROW(f_x.impTerm(zero), CVC5ApiException);
 565   ASSERT_THROW(f_x.impTerm(f_x), CVC5ApiException);
 566   Term sum = d_solver.mkTerm(ADD, {f_x, f_x});
 567   ASSERT_THROW(sum.impTerm(b), CVC5ApiException);
 568   ASSERT_THROW(sum.impTerm(x), CVC5ApiException);
 569   ASSERT_THROW(sum.impTerm(f), CVC5ApiException);
 570   ASSERT_THROW(sum.impTerm(p), CVC5ApiException);
 571   ASSERT_THROW(sum.impTerm(zero), CVC5ApiException);
 572   ASSERT_THROW(sum.impTerm(f_x), CVC5ApiException);
 573   ASSERT_THROW(sum.impTerm(sum), CVC5ApiException);
 574   Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero});
 575   ASSERT_NO_THROW(p_0.impTerm(b));
 576   ASSERT_THROW(p_0.impTerm(x), CVC5ApiException);
 577   ASSERT_THROW(p_0.impTerm(f), CVC5ApiException);
 578   ASSERT_THROW(p_0.impTerm(p), CVC5ApiException);
 579   ASSERT_THROW(p_0.impTerm(zero), CVC5ApiException);
 580   ASSERT_THROW(p_0.impTerm(f_x), CVC5ApiException);
 581   ASSERT_THROW(p_0.impTerm(sum), CVC5ApiException);
 582   ASSERT_NO_THROW(p_0.impTerm(p_0));
 583   Term p_f_x = d_solver.mkTerm(APPLY_UF, {p, f_x});
 584   ASSERT_NO_THROW(p_f_x.impTerm(b));
 585   ASSERT_THROW(p_f_x.impTerm(x), CVC5ApiException);
 586   ASSERT_THROW(p_f_x.impTerm(f), CVC5ApiException);
 587   ASSERT_THROW(p_f_x.impTerm(p), CVC5ApiException);
 588   ASSERT_THROW(p_f_x.impTerm(zero), CVC5ApiException);
 589   ASSERT_THROW(p_f_x.impTerm(f_x), CVC5ApiException);
 590   ASSERT_THROW(p_f_x.impTerm(sum), CVC5ApiException);
 591   ASSERT_NO_THROW(p_f_x.impTerm(p_0));
 592   ASSERT_NO_THROW(p_f_x.impTerm(p_f_x));
 593 }
 594
 595 TEST_F(TestApiBlackTerm, iteTerm)
 596 {
 597   Sort bvSort = d_solver.mkBitVectorSort(8);
 598   Sort intSort = d_solver.getIntegerSort();
 599   Sort boolSort = d_solver.getBooleanSort();
 600   Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
 601   Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
 602
 603   Term b = d_solver.mkTrue();
 604   ASSERT_THROW(Term().iteTerm(b, b), CVC5ApiException);
 605   ASSERT_THROW(b.iteTerm(Term(), b), CVC5ApiException);
 606   ASSERT_THROW(b.iteTerm(b, Term()), CVC5ApiException);
 607   ASSERT_NO_THROW(b.iteTerm(b, b));
 608   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
 609   ASSERT_NO_THROW(b.iteTerm(x, x));
 610   ASSERT_NO_THROW(b.iteTerm(b, b));
 611   ASSERT_THROW(b.iteTerm(x, b), CVC5ApiException);
 612   ASSERT_THROW(x.iteTerm(x, x), CVC5ApiException);
 613   ASSERT_THROW(x.iteTerm(x, b), CVC5ApiException);
 614   Term f = d_solver.mkVar(funSort1, "f");
 615   ASSERT_THROW(f.iteTerm(b, b), CVC5ApiException);
 616   ASSERT_THROW(x.iteTerm(b, x), CVC5ApiException);
 617   Term p = d_solver.mkVar(funSort2, "p");
 618   ASSERT_THROW(p.iteTerm(b, b), CVC5ApiException);
 619   ASSERT_THROW(p.iteTerm(x, b), CVC5ApiException);
 620   Term zero = d_solver.mkInteger(0);
 621   ASSERT_THROW(zero.iteTerm(x, x), CVC5ApiException);
 622   ASSERT_THROW(zero.iteTerm(x, b), CVC5ApiException);
 623   Term f_x = d_solver.mkTerm(APPLY_UF, {f, x});
 624   ASSERT_THROW(f_x.iteTerm(b, b), CVC5ApiException);
 625   ASSERT_THROW(f_x.iteTerm(b, x), CVC5ApiException);
 626   Term sum = d_solver.mkTerm(ADD, {f_x, f_x});
 627   ASSERT_THROW(sum.iteTerm(x, x), CVC5ApiException);
 628   ASSERT_THROW(sum.iteTerm(b, x), CVC5ApiException);
 629   Term p_0 = d_solver.mkTerm(APPLY_UF, {p, zero});
 630   ASSERT_NO_THROW(p_0.iteTerm(b, b));
 631   ASSERT_NO_THROW(p_0.iteTerm(x, x));
 632   ASSERT_THROW(p_0.iteTerm(x, b), CVC5ApiException);
 633   Term p_f_x = d_solver.mkTerm(APPLY_UF, {p, f_x});
 634   ASSERT_NO_THROW(p_f_x.iteTerm(b, b));
 635   ASSERT_NO_THROW(p_f_x.iteTerm(x, x));
 636   ASSERT_THROW(p_f_x.iteTerm(x, b), CVC5ApiException);
 637 }
 638
 639 TEST_F(TestApiBlackTerm, termAssignment)
 640 {
 641   Term t1 = d_solver.mkInteger(1);
 642   Term t2 = t1;
 643   t2 = d_solver.mkInteger(2);
 644   ASSERT_EQ(t1, d_solver.mkInteger(1));
 645 }
 646
 647 TEST_F(TestApiBlackTerm, termCompare)
 648 {
 649   Term t1 = d_solver.mkInteger(1);
 650   Term t2 =
 651       d_solver.mkTerm(ADD, {d_solver.mkInteger(2), d_solver.mkInteger(2)});
 652   Term t3 =
 653       d_solver.mkTerm(ADD, {d_solver.mkInteger(2), d_solver.mkInteger(2)});
 654   ASSERT_TRUE(t2 >= t3);
 655   ASSERT_TRUE(t2 <= t3);
 656   ASSERT_TRUE((t1 > t2) != (t1 < t2));
 657   ASSERT_TRUE((t1 > t2 || t1 == t2) == (t1 >= t2));
 658 }
 659
 660 TEST_F(TestApiBlackTerm, termChildren)
 661 {
 662   // simple term 2+3
 663   Term two = d_solver.mkInteger(2);
 664   Term t1 = d_solver.mkTerm(ADD, {two, d_solver.mkInteger(3)});
 665   ASSERT_EQ(t1[0], two);
 666   ASSERT_EQ(t1.getNumChildren(), 2);
 667   Term tnull;
 668   ASSERT_THROW(tnull.getNumChildren(), CVC5ApiException);
 669
 670   // apply term f(2)
 671   Sort intSort = d_solver.getIntegerSort();
 672   Sort fsort = d_solver.mkFunctionSort({intSort}, intSort);
 673   Term f = d_solver.mkConst(fsort, "f");
 674   Term t2 = d_solver.mkTerm(APPLY_UF, {f, two});
 675   // due to our higher-order view of terms, we treat f as a child of APPLY_UF
 676   ASSERT_EQ(t2.getNumChildren(), 2);
 677   ASSERT_EQ(t2[0], f);
 678   ASSERT_EQ(t2[1], two);
 679   ASSERT_THROW(tnull[0], CVC5ApiException);
 680 }
 681
 682 TEST_F(TestApiBlackTerm, getInteger)
 683 {
 684   Term int1 = d_solver.mkInteger("-18446744073709551616");
 685   Term int2 = d_solver.mkInteger("-18446744073709551615");
 686   Term int3 = d_solver.mkInteger("-4294967296");
 687   Term int4 = d_solver.mkInteger("-4294967295");
 688   Term int5 = d_solver.mkInteger("-10");
 689   Term int6 = d_solver.mkInteger("0");
 690   Term int7 = d_solver.mkInteger("10");
 691   Term int8 = d_solver.mkInteger("4294967295");
 692   Term int9 = d_solver.mkInteger("4294967296");
 693   Term int10 = d_solver.mkInteger("18446744073709551615");
 694   Term int11 = d_solver.mkInteger("18446744073709551616");
 695   Term int12 = d_solver.mkInteger("-0");
 696
 697   ASSERT_THROW(d_solver.mkInteger(""), CVC5ApiException);
 698   ASSERT_THROW(d_solver.mkInteger("-"), CVC5ApiException);
 699   ASSERT_THROW(d_solver.mkInteger("-1-"), CVC5ApiException);
 700   ASSERT_THROW(d_solver.mkInteger("0.0"), CVC5ApiException);
 701   ASSERT_THROW(d_solver.mkInteger("-0.1"), CVC5ApiException);
 702   ASSERT_THROW(d_solver.mkInteger("012"), CVC5ApiException);
 703   ASSERT_THROW(d_solver.mkInteger("0000"), CVC5ApiException);
 704   ASSERT_THROW(d_solver.mkInteger("-01"), CVC5ApiException);
 705   ASSERT_THROW(d_solver.mkInteger("-00"), CVC5ApiException);
 706
 707   ASSERT_TRUE(!int1.isInt32Value() && !int1.isUInt32Value()
 708               && !int1.isInt64Value() && !int1.isUInt64Value()
 709               && int1.isIntegerValue());
 710   ASSERT_EQ(int1.getIntegerValue(), "-18446744073709551616");
 711   ASSERT_TRUE(int1.getRealOrIntegerValueSign() == -1);
 712   ASSERT_TRUE(!int2.isInt32Value() && !int2.isUInt32Value()
 713               && !int2.isInt64Value() && !int2.isUInt64Value()
 714               && int2.isIntegerValue());
 715   ASSERT_EQ(int2.getIntegerValue(), "-18446744073709551615");
 716   ASSERT_TRUE(!int3.isInt32Value() && !int3.isUInt32Value()
 717               && int3.isInt64Value() && !int3.isUInt64Value()
 718               && int3.isIntegerValue());
 719   ASSERT_EQ(int3.getInt64Value(), -4294967296);
 720   ASSERT_EQ(int3.getIntegerValue(), "-4294967296");
 721   ASSERT_TRUE(!int4.isInt32Value() && !int4.isUInt32Value()
 722               && int4.isInt64Value() && !int4.isUInt64Value()
 723               && int4.isIntegerValue());
 724   ASSERT_EQ(int4.getInt64Value(), -4294967295);
 725   ASSERT_EQ(int4.getIntegerValue(), "-4294967295");
 726   ASSERT_TRUE(int5.isInt32Value() && !int5.isUInt32Value()
 727               && int5.isInt64Value() && !int5.isUInt64Value()
 728               && int5.isIntegerValue());
 729   ASSERT_EQ(int5.getInt32Value(), -10);
 730   ASSERT_EQ(int5.getInt64Value(), -10);
 731   ASSERT_EQ(int5.getIntegerValue(), "-10");
 732   ASSERT_TRUE(int6.isInt32Value() && int6.isUInt32Value() && int6.isInt64Value()
 733               && int6.isUInt64Value() && int6.isIntegerValue());
 734   ASSERT_EQ(int6.getInt32Value(), 0);
 735   ASSERT_EQ(int6.getUInt32Value(), 0);
 736   ASSERT_EQ(int6.getInt64Value(), 0);
 737   ASSERT_EQ(int6.getUInt64Value(), 0);
 738   ASSERT_EQ(int6.getIntegerValue(), "0");
 739   ASSERT_TRUE(int6.getRealOrIntegerValueSign() == 0);
 740   ASSERT_TRUE(int7.isInt32Value() && int7.isUInt32Value() && int7.isInt64Value()
 741               && int7.isUInt64Value() && int7.isIntegerValue());
 742   ASSERT_EQ(int7.getInt32Value(), 10);
 743   ASSERT_EQ(int7.getUInt32Value(), 10);
 744   ASSERT_EQ(int7.getInt64Value(), 10);
 745   ASSERT_EQ(int7.getUInt64Value(), 10);
 746   ASSERT_EQ(int7.getIntegerValue(), "10");
 747   ASSERT_TRUE(int7.getRealOrIntegerValueSign() == 1);
 748   ASSERT_TRUE(!int8.isInt32Value() && int8.isUInt32Value()
 749               && int8.isInt64Value() && int8.isUInt64Value()
 750               && int8.isIntegerValue());
 751   ASSERT_EQ(int8.getUInt32Value(), 4294967295);
 752   ASSERT_EQ(int8.getInt64Value(), 4294967295);
 753   ASSERT_EQ(int8.getUInt64Value(), 4294967295);
 754   ASSERT_EQ(int8.getIntegerValue(), "4294967295");
 755   ASSERT_TRUE(!int9.isInt32Value() && !int9.isUInt32Value()
 756               && int9.isInt64Value() && int9.isUInt64Value()
 757               && int9.isIntegerValue());
 758   ASSERT_EQ(int9.getInt64Value(), 4294967296);
 759   ASSERT_EQ(int9.getUInt64Value(), 4294967296);
 760   ASSERT_EQ(int9.getIntegerValue(), "4294967296");
 761   ASSERT_TRUE(!int10.isInt32Value() && !int10.isUInt32Value()
 762               && !int10.isInt64Value() && int10.isUInt64Value()
 763               && int10.isIntegerValue());
 764   ASSERT_EQ(int10.getUInt64Value(), 18446744073709551615ull);
 765   ASSERT_EQ(int10.getIntegerValue(), "18446744073709551615");
 766   ASSERT_TRUE(!int11.isInt32Value() && !int11.isUInt32Value()
 767               && !int11.isInt64Value() && !int11.isUInt64Value()
 768               && int11.isIntegerValue());
 769   ASSERT_EQ(int11.getIntegerValue(), "18446744073709551616");
 770 }
 771
 772 TEST_F(TestApiBlackTerm, getString)
 773 {
 774   Term s1 = d_solver.mkString("abcde");
 775   ASSERT_TRUE(s1.isStringValue());
 776   ASSERT_EQ(s1.getStringValue(), L"abcde");
 777 }
 778
 779 TEST_F(TestApiBlackTerm, getReal)
 780 {
 781   Term real1 = d_solver.mkReal("0");
 782   Term real2 = d_solver.mkReal(".0");
 783   Term real3 = d_solver.mkReal("-17");
 784   Term real4 = d_solver.mkReal("-3/5");
 785   Term real5 = d_solver.mkReal("12.7");
 786   Term real6 = d_solver.mkReal("1/4294967297");
 787   Term real7 = d_solver.mkReal("4294967297");
 788   Term real8 = d_solver.mkReal("1/18446744073709551617");
 789   Term real9 = d_solver.mkReal("18446744073709551617");
 790   Term real10 = d_solver.mkReal("2343.2343");
 791
 792   ASSERT_TRUE(real1.isRealValue() && real1.isReal64Value()
 793               && real1.isReal32Value());
 794   ASSERT_TRUE(real2.isRealValue() && real2.isReal64Value()
 795               && real2.isReal32Value());
 796   ASSERT_TRUE(real3.isRealValue() && real3.isReal64Value()
 797               && real3.isReal32Value());
 798   ASSERT_TRUE(real4.isRealValue() && real4.isReal64Value()
 799               && real4.isReal32Value());
 800   ASSERT_TRUE(real5.isRealValue() && real5.isReal64Value()
 801               && real5.isReal32Value());
 802   ASSERT_TRUE(real6.isRealValue() && real6.isReal64Value());
 803   ASSERT_TRUE(real7.isRealValue() && real7.isReal64Value());
 804   ASSERT_TRUE(real8.isRealValue());
 805   ASSERT_TRUE(real9.isRealValue());
 806   ASSERT_TRUE(real10.isRealValue());
 807
 808   ASSERT_EQ((std::pair<int32_t, uint32_t>(0, 1)), real1.getReal32Value());
 809   ASSERT_EQ((std::pair<int64_t, uint64_t>(0, 1)), real1.getReal64Value());
 810   ASSERT_EQ("0/1", real1.getRealValue());
 811
 812   ASSERT_EQ((std::pair<int32_t, uint32_t>(0, 1)), real2.getReal32Value());
 813   ASSERT_EQ((std::pair<int64_t, uint64_t>(0, 1)), real2.getReal64Value());
 814   ASSERT_EQ("0/1", real2.getRealValue());
 815
 816   ASSERT_EQ((std::pair<int32_t, uint32_t>(-17, 1)), real3.getReal32Value());
 817   ASSERT_EQ((std::pair<int64_t, uint64_t>(-17, 1)), real3.getReal64Value());
 818   ASSERT_EQ("-17/1", real3.getRealValue());
 819
 820   ASSERT_EQ((std::pair<int32_t, uint32_t>(-3, 5)), real4.getReal32Value());
 821   ASSERT_EQ((std::pair<int64_t, uint64_t>(-3, 5)), real4.getReal64Value());
 822   ASSERT_EQ("-3/5", real4.getRealValue());
 823
 824   ASSERT_EQ((std::pair<int32_t, uint32_t>(127, 10)), real5.getReal32Value());
 825   ASSERT_EQ((std::pair<int64_t, uint64_t>(127, 10)), real5.getReal64Value());
 826   ASSERT_EQ("127/10", real5.getRealValue());
 827
 828   ASSERT_EQ((std::pair<int64_t, uint64_t>(1, 4294967297)),
 829             real6.getReal64Value());
 830   ASSERT_EQ("1/4294967297", real6.getRealValue());
 831
 832   ASSERT_EQ((std::pair<int64_t, uint64_t>(4294967297, 1)),
 833             real7.getReal64Value());
 834   ASSERT_EQ("4294967297/1", real7.getRealValue());
 835
 836   ASSERT_EQ("1/18446744073709551617", real8.getRealValue());
 837
 838   ASSERT_EQ("18446744073709551617/1", real9.getRealValue());
 839
 840   ASSERT_EQ("23432343/10000", real10.getRealValue());
 841 }
 842
 843 TEST_F(TestApiBlackTerm, getConstArrayBase)
 844 {
 845   Sort intsort = d_solver.getIntegerSort();
 846   Sort arrsort = d_solver.mkArraySort(intsort, intsort);
 847   Term one = d_solver.mkInteger(1);
 848   Term constarr = d_solver.mkConstArray(arrsort, one);
 849
 850   ASSERT_TRUE(constarr.isConstArray());
 851   ASSERT_EQ(one, constarr.getConstArrayBase());
 852 }
 853
 854 TEST_F(TestApiBlackTerm, getBoolean)
 855 {
 856   Term b1 = d_solver.mkBoolean(true);
 857   Term b2 = d_solver.mkBoolean(false);
 858
 859   ASSERT_TRUE(b1.isBooleanValue());
 860   ASSERT_TRUE(b2.isBooleanValue());
 861   ASSERT_TRUE(b1.getBooleanValue());
 862   ASSERT_FALSE(b2.getBooleanValue());
 863 }
 864
 865 TEST_F(TestApiBlackTerm, getBitVector)
 866 {
 867   Term b1 = d_solver.mkBitVector(8, 15);
 868   Term b2 = d_solver.mkBitVector(8, "00001111", 2);
 869   Term b3 = d_solver.mkBitVector(8, "15", 10);
 870   Term b4 = d_solver.mkBitVector(8, "0f", 16);
 871   Term b5 = d_solver.mkBitVector(9, "00001111", 2);
 872   Term b6 = d_solver.mkBitVector(9, "15", 10);
 873   Term b7 = d_solver.mkBitVector(9, "0f", 16);
 874
 875   ASSERT_TRUE(b1.isBitVectorValue());
 876   ASSERT_TRUE(b2.isBitVectorValue());
 877   ASSERT_TRUE(b3.isBitVectorValue());
 878   ASSERT_TRUE(b4.isBitVectorValue());
 879   ASSERT_TRUE(b5.isBitVectorValue());
 880   ASSERT_TRUE(b6.isBitVectorValue());
 881   ASSERT_TRUE(b7.isBitVectorValue());
 882
 883   ASSERT_EQ("00001111", b1.getBitVectorValue(2));
 884   ASSERT_EQ("15", b1.getBitVectorValue(10));
 885   ASSERT_EQ("f", b1.getBitVectorValue(16));
 886   ASSERT_EQ("00001111", b2.getBitVectorValue(2));
 887   ASSERT_EQ("15", b2.getBitVectorValue(10));
 888   ASSERT_EQ("f", b2.getBitVectorValue(16));
 889   ASSERT_EQ("00001111", b3.getBitVectorValue(2));
 890   ASSERT_EQ("15", b3.getBitVectorValue(10));
 891   ASSERT_EQ("f", b3.getBitVectorValue(16));
 892   ASSERT_EQ("00001111", b4.getBitVectorValue(2));
 893   ASSERT_EQ("15", b4.getBitVectorValue(10));
 894   ASSERT_EQ("f", b4.getBitVectorValue(16));
 895   ASSERT_EQ("000001111", b5.getBitVectorValue(2));
 896   ASSERT_EQ("15", b5.getBitVectorValue(10));
 897   ASSERT_EQ("f", b5.getBitVectorValue(16));
 898   ASSERT_EQ("000001111", b6.getBitVectorValue(2));
 899   ASSERT_EQ("15", b6.getBitVectorValue(10));
 900   ASSERT_EQ("f", b6.getBitVectorValue(16));
 901   ASSERT_EQ("000001111", b7.getBitVectorValue(2));
 902   ASSERT_EQ("15", b7.getBitVectorValue(10));
 903   ASSERT_EQ("f", b7.getBitVectorValue(16));
 904 }
 905
 906 TEST_F(TestApiBlackTerm, getUninterpretedSortValue)
 907 {
 908   d_solver.setOption("produce-models", "true");
 909   Sort uSort = d_solver.mkUninterpretedSort("u");
 910   Term x = d_solver.mkConst(uSort, "x");
 911   Term y = d_solver.mkConst(uSort, "y");
 912   d_solver.assertFormula(d_solver.mkTerm(EQUAL, {x, y}));
 913   ASSERT_TRUE(d_solver.checkSat().isSat());
 914   Term vx = d_solver.getValue(x);
 915   Term vy = d_solver.getValue(y);
 916   ASSERT_TRUE(vx.isUninterpretedSortValue());
 917   ASSERT_TRUE(vy.isUninterpretedSortValue());
 918   ASSERT_EQ(vx.getUninterpretedSortValue(), vy.getUninterpretedSortValue());
 919 }
 920
 921 TEST_F(TestApiBlackTerm, isRoundingModeValue)
 922 {
 923   ASSERT_FALSE(d_solver.mkInteger(15).isRoundingModeValue());
 924   ASSERT_TRUE(d_solver.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN)
 925                   .isRoundingModeValue());
 926   ASSERT_FALSE(
 927       d_solver.mkConst(d_solver.getRoundingModeSort()).isRoundingModeValue());
 928 }
 929
 930 TEST_F(TestApiBlackTerm, getRoundingModeValue)
 931 {
 932   ASSERT_THROW(d_solver.mkInteger(15).getRoundingModeValue(), CVC5ApiException);
 933   ASSERT_EQ(d_solver.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN)
 934                 .getRoundingModeValue(),
 935             RoundingMode::ROUND_NEAREST_TIES_TO_EVEN);
 936   ASSERT_EQ(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_POSITIVE)
 937                 .getRoundingModeValue(),
 938             RoundingMode::ROUND_TOWARD_POSITIVE);
 939   ASSERT_EQ(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_NEGATIVE)
 940                 .getRoundingModeValue(),
 941             RoundingMode::ROUND_TOWARD_NEGATIVE);
 942   ASSERT_EQ(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO)
 943                 .getRoundingModeValue(),
 944             RoundingMode::ROUND_TOWARD_ZERO);
 945   ASSERT_EQ(d_solver.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_AWAY)
 946                 .getRoundingModeValue(),
 947             RoundingMode::ROUND_NEAREST_TIES_TO_AWAY);
 948 }
 949
 950 TEST_F(TestApiBlackTerm, getTuple)
 951 {
 952   Sort s1 = d_solver.getIntegerSort();
 953   Sort s2 = d_solver.getRealSort();
 954   Sort s3 = d_solver.getStringSort();
 955
 956   Term t1 = d_solver.mkInteger(15);
 957   Term t2 = d_solver.mkReal(17, 25);
 958   Term t3 = d_solver.mkString("abc");
 959
 960   Term tup = d_solver.mkTuple({s1, s2, s3}, {t1, t2, t3});
 961
 962   ASSERT_TRUE(tup.isTupleValue());
 963   ASSERT_EQ(std::vector<Term>({t1, t2, t3}), tup.getTupleValue());
 964 }
 965
 966 TEST_F(TestApiBlackTerm, getFloatingPoint)
 967 {
 968   Term bvval = d_solver.mkBitVector(16, "0000110000000011", 2);
 969   Term fp = d_solver.mkFloatingPoint(5, 11, bvval);
 970
 971   ASSERT_TRUE(fp.isFloatingPointValue());
 972   ASSERT_FALSE(fp.isFloatingPointPosZero());
 973   ASSERT_FALSE(fp.isFloatingPointNegZero());
 974   ASSERT_FALSE(fp.isFloatingPointPosInf());
 975   ASSERT_FALSE(fp.isFloatingPointNegInf());
 976   ASSERT_FALSE(fp.isFloatingPointNaN());
 977   ASSERT_EQ(std::make_tuple(5u, 11u, bvval), fp.getFloatingPointValue());
 978
 979   ASSERT_TRUE(d_solver.mkFloatingPointPosZero(5, 11).isFloatingPointPosZero());
 980   ASSERT_TRUE(d_solver.mkFloatingPointNegZero(5, 11).isFloatingPointNegZero());
 981   ASSERT_TRUE(d_solver.mkFloatingPointPosInf(5, 11).isFloatingPointPosInf());
 982   ASSERT_TRUE(d_solver.mkFloatingPointNegInf(5, 11).isFloatingPointNegInf());
 983   ASSERT_TRUE(d_solver.mkFloatingPointNaN(5, 11).isFloatingPointNaN());
 984 }
 985
 986 TEST_F(TestApiBlackTerm, getSet)
 987 {
 988   Sort s = d_solver.mkSetSort(d_solver.getIntegerSort());
 989
 990   Term i1 = d_solver.mkInteger(5);
 991   Term i2 = d_solver.mkInteger(7);
 992
 993   Term s1 = d_solver.mkEmptySet(s);
 994   Term s2 = d_solver.mkTerm(Kind::SET_SINGLETON, {i1});
 995   Term s3 = d_solver.mkTerm(Kind::SET_SINGLETON, {i1});
 996   Term s4 = d_solver.mkTerm(Kind::SET_SINGLETON, {i2});
 997   Term s5 = d_solver.mkTerm(Kind::SET_UNION,
 998                             {s2, d_solver.mkTerm(Kind::SET_UNION, {s3, s4})});
 999
1000   ASSERT_TRUE(s1.isSetValue());
1001   ASSERT_TRUE(s2.isSetValue());
1002   ASSERT_TRUE(s3.isSetValue());
1003   ASSERT_TRUE(s4.isSetValue());
1004   ASSERT_FALSE(s5.isSetValue());
1005   s5 = d_solver.simplify(s5);
1006   ASSERT_TRUE(s5.isSetValue());
1007
1008   ASSERT_EQ(std::set<Term>({}), s1.getSetValue());
1009   ASSERT_EQ(std::set<Term>({i1}), s2.getSetValue());
1010   ASSERT_EQ(std::set<Term>({i1}), s3.getSetValue());
1011   ASSERT_EQ(std::set<Term>({i2}), s4.getSetValue());
1012   ASSERT_EQ(std::set<Term>({i1, i2}), s5.getSetValue());
1013 }
1014
1015 TEST_F(TestApiBlackTerm, getSequence)
1016 {
1017   Sort s = d_solver.mkSequenceSort(d_solver.getIntegerSort());
1018
1019   Term i1 = d_solver.mkInteger(5);
1020   Term i2 = d_solver.mkInteger(7);
1021
1022   Term s1 = d_solver.mkEmptySequence(s);
1023   Term s2 = d_solver.mkTerm(Kind::SEQ_UNIT, {i1});
1024   Term s3 = d_solver.mkTerm(Kind::SEQ_UNIT, {i1});
1025   Term s4 = d_solver.mkTerm(Kind::SEQ_UNIT, {i2});
1026   Term s5 = d_solver.mkTerm(Kind::SEQ_CONCAT,
1027                             {s2, d_solver.mkTerm(Kind::SEQ_CONCAT, {s3, s4})});
1028
1029   ASSERT_TRUE(s1.isSequenceValue());
1030   ASSERT_TRUE(!s2.isSequenceValue());
1031   ASSERT_TRUE(!s3.isSequenceValue());
1032   ASSERT_TRUE(!s4.isSequenceValue());
1033   ASSERT_TRUE(!s5.isSequenceValue());
1034
1035   s2 = d_solver.simplify(s2);
1036   s3 = d_solver.simplify(s3);
1037   s4 = d_solver.simplify(s4);
1038   s5 = d_solver.simplify(s5);
1039
1040   ASSERT_EQ(std::vector<Term>({}), s1.getSequenceValue());
1041   ASSERT_EQ(std::vector<Term>({i1}), s2.getSequenceValue());
1042   ASSERT_EQ(std::vector<Term>({i1}), s3.getSequenceValue());
1043   ASSERT_EQ(std::vector<Term>({i2}), s4.getSequenceValue());
1044   ASSERT_EQ(std::vector<Term>({i1, i1, i2}), s5.getSequenceValue());
1045 }
1046
1047 TEST_F(TestApiBlackTerm, substitute)
1048 {
1049   Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
1050   Term one = d_solver.mkInteger(1);
1051   Term ttrue = d_solver.mkTrue();
1052   Term xpx = d_solver.mkTerm(ADD, {x, x});
1053   Term onepone = d_solver.mkTerm(ADD, {one, one});
1054
1055   ASSERT_EQ(xpx.substitute(x, one), onepone);
1056   ASSERT_EQ(onepone.substitute(one, x), xpx);
1057   // incorrect due to type
1058   ASSERT_THROW(xpx.substitute(one, ttrue), CVC5ApiException);
1059
1060   // simultaneous substitution
1061   Term y = d_solver.mkConst(d_solver.getIntegerSort(), "y");
1062   Term xpy = d_solver.mkTerm(ADD, {x, y});
1063   Term xpone = d_solver.mkTerm(ADD, {y, one});
1064   std::vector<Term> es;
1065   std::vector<Term> rs;
1066   es.push_back(x);
1067   rs.push_back(y);
1068   es.push_back(y);
1069   rs.push_back(one);
1070   ASSERT_EQ(xpy.substitute(es, rs), xpone);
1071
1072   // incorrect substitution due to arity
1073   rs.pop_back();
1074   ASSERT_THROW(xpy.substitute(es, rs), CVC5ApiException);
1075
1076   // incorrect substitution due to types
1077   rs.push_back(ttrue);
1078   ASSERT_THROW(xpy.substitute(es, rs), CVC5ApiException);
1079
1080   // null cannot substitute
1081   Term tnull;
1082   ASSERT_THROW(tnull.substitute(one, x), CVC5ApiException);
1083   ASSERT_THROW(xpx.substitute(tnull, x), CVC5ApiException);
1084   ASSERT_THROW(xpx.substitute(x, tnull), CVC5ApiException);
1085   rs.pop_back();
1086   rs.push_back(tnull);
1087   ASSERT_THROW(xpy.substitute(es, rs), CVC5ApiException);
1088   es.clear();
1089   rs.clear();
1090   es.push_back(x);
1091   rs.push_back(y);
1092   ASSERT_THROW(tnull.substitute(es, rs), CVC5ApiException);
1093   es.push_back(tnull);
1094   rs.push_back(one);
1095   ASSERT_THROW(xpx.substitute(es, rs), CVC5ApiException);
1096 }
1097
1098 TEST_F(TestApiBlackTerm, constArray)
1099 {
1100   Sort intsort = d_solver.getIntegerSort();
1101   Sort arrsort = d_solver.mkArraySort(intsort, intsort);
1102   Term a = d_solver.mkConst(arrsort, "a");
1103   Term one = d_solver.mkInteger(1);
1104   Term constarr = d_solver.mkConstArray(arrsort, one);
1105
1106   ASSERT_EQ(constarr.getKind(), CONST_ARRAY);
1107   ASSERT_EQ(constarr.getConstArrayBase(), one);
1108   ASSERT_THROW(a.getConstArrayBase(), CVC5ApiException);
1109
1110   arrsort =
1111       d_solver.mkArraySort(d_solver.getRealSort(), d_solver.getRealSort());
1112   Term zero_array = d_solver.mkConstArray(arrsort, d_solver.mkReal(0));
1113   Term stores = d_solver.mkTerm(
1114       STORE, {zero_array, d_solver.mkReal(1), d_solver.mkReal(2)});
1115   stores =
1116       d_solver.mkTerm(STORE, {stores, d_solver.mkReal(2), d_solver.mkReal(3)});
1117   stores =
1118       d_solver.mkTerm(STORE, {stores, d_solver.mkReal(4), d_solver.mkReal(5)});
1119 }
1120
1121 TEST_F(TestApiBlackTerm, getSequenceValue)
1122 {
1123   Sort realsort = d_solver.getRealSort();
1124   Sort seqsort = d_solver.mkSequenceSort(realsort);
1125   Term s = d_solver.mkEmptySequence(seqsort);
1126
1127   ASSERT_EQ(s.getKind(), CONST_SEQUENCE);
1128   // empty sequence has zero elements
1129   std::vector<Term> cs = s.getSequenceValue();
1130   ASSERT_TRUE(cs.empty());
1131
1132   // A seq.unit app is not a constant sequence (regardless of whether it is
1133   // applied to a constant).
1134   Term su = d_solver.mkTerm(SEQ_UNIT, {d_solver.mkReal(1)});
1135   ASSERT_THROW(su.getSequenceValue(), CVC5ApiException);
1136 }
1137
1138 TEST_F(TestApiBlackTerm, getCardinalityConstraint)
1139 {
1140   Sort su = d_solver.mkUninterpretedSort("u");
1141   Term t = d_solver.mkCardinalityConstraint(su, 3);
1142   ASSERT_TRUE(t.isCardinalityConstraint());
1143   std::pair<Sort, uint32_t> cc = t.getCardinalityConstraint();
1144   ASSERT_EQ(cc.first, su);
1145   ASSERT_EQ(cc.second, 3);
1146   Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
1147   ASSERT_FALSE(x.isCardinalityConstraint());
1148   ASSERT_THROW(x.getCardinalityConstraint(), CVC5ApiException);
1149   Term nullt;
1150   ASSERT_THROW(nullt.isCardinalityConstraint(), CVC5ApiException);
1151 }
1152
1153 TEST_F(TestApiBlackTerm, termScopedToString)
1154 {
1155   Sort intsort = d_solver.getIntegerSort();
1156   Term x = d_solver.mkConst(intsort, "x");
1157   ASSERT_EQ(x.toString(), "x");
1158   Solver solver2;
1159   ASSERT_EQ(x.toString(), "x");
1160 }
1161
1162 TEST_F(TestApiBlackTerm, toString) { ASSERT_NO_THROW(Term().toString()); }
1163 }  // namespace test
1164 }  // namespace cvc5::internal