test/unit/api/term_black.h

   1 /*********************                                                        */
   2 /*! \file term_black.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Aina Niemetz, Andres Noetzli
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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.\endverbatim
  11  **
  12  ** \brief Black box testing of the Term class
  13  **/
  14
  15 #include <cxxtest/TestSuite.h>
  16
  17 #include "api/cvc4cpp.h"
  18
  19 using namespace CVC4::api;
  20
  21 class TermBlack : public CxxTest::TestSuite
  22 {
  23  public:
  24   void setUp() override {}
  25   void tearDown() override {}
  26
  27   void testEq();
  28   void testGetId();
  29   void testGetKind();
  30   void testGetSort();
  31   void testGetOp();
  32   void testIsNull();
  33   void testNotTerm();
  34   void testAndTerm();
  35   void testOrTerm();
  36   void testXorTerm();
  37   void testEqTerm();
  38   void testImpTerm();
  39   void testIteTerm();
  40
  41   void testTermAssignment();
  42   void testTermCompare();
  43   void testTermChildren();
  44   void testSubstitute();
  45   void testIsConst();
  46
  47  private:
  48   Solver d_solver;
  49 };
  50
  51 void TermBlack::testEq()
  52 {
  53   Sort uSort = d_solver.mkUninterpretedSort("u");
  54   Term x = d_solver.mkVar(uSort, "x");
  55   Term y = d_solver.mkVar(uSort, "y");
  56   Term z;
  57
  58   TS_ASSERT(x == x);
  59   TS_ASSERT(!(x != x));
  60   TS_ASSERT(!(x == y));
  61   TS_ASSERT(x != y);
  62   TS_ASSERT(!(x == z));
  63   TS_ASSERT(x != z);
  64 }
  65
  66 void TermBlack::testGetId()
  67 {
  68   Term n;
  69   TS_ASSERT_THROWS(n.getId(), CVC4ApiException&);
  70   Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x");
  71   TS_ASSERT_THROWS_NOTHING(x.getId());
  72   Term y = x;
  73   TS_ASSERT_EQUALS(x.getId(), y.getId());
  74
  75   Term z = d_solver.mkVar(d_solver.getIntegerSort(), "z");
  76   TS_ASSERT_DIFFERS(x.getId(), z.getId());
  77 }
  78
  79 void TermBlack::testGetKind()
  80 {
  81   Sort uSort = d_solver.mkUninterpretedSort("u");
  82   Sort intSort = d_solver.getIntegerSort();
  83   Sort boolSort = d_solver.getBooleanSort();
  84   Sort funSort1 = d_solver.mkFunctionSort(uSort, intSort);
  85   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
  86
  87   Term n;
  88   TS_ASSERT_THROWS(n.getKind(), CVC4ApiException&);
  89   Term x = d_solver.mkVar(uSort, "x");
  90   TS_ASSERT_THROWS_NOTHING(x.getKind());
  91   Term y = d_solver.mkVar(uSort, "y");
  92   TS_ASSERT_THROWS_NOTHING(y.getKind());
  93
  94   Term f = d_solver.mkVar(funSort1, "f");
  95   TS_ASSERT_THROWS_NOTHING(f.getKind());
  96   Term p = d_solver.mkVar(funSort2, "p");
  97   TS_ASSERT_THROWS_NOTHING(p.getKind());
  98
  99   Term zero = d_solver.mkReal(0);
 100   TS_ASSERT_THROWS_NOTHING(zero.getKind());
 101
 102   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
 103   TS_ASSERT_THROWS_NOTHING(f_x.getKind());
 104   Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
 105   TS_ASSERT_THROWS_NOTHING(f_y.getKind());
 106   Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
 107   TS_ASSERT_THROWS_NOTHING(sum.getKind());
 108   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
 109   TS_ASSERT_THROWS_NOTHING(p_0.getKind());
 110   Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
 111   TS_ASSERT_THROWS_NOTHING(p_f_y.getKind());
 112 }
 113
 114 void TermBlack::testGetSort()
 115 {
 116   Sort bvSort = d_solver.mkBitVectorSort(8);
 117   Sort intSort = d_solver.getIntegerSort();
 118   Sort boolSort = d_solver.getBooleanSort();
 119   Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
 120   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 121
 122   Term n;
 123   TS_ASSERT_THROWS(n.getSort(), CVC4ApiException&);
 124   Term x = d_solver.mkVar(bvSort, "x");
 125   TS_ASSERT_THROWS_NOTHING(x.getSort());
 126   TS_ASSERT(x.getSort() == bvSort);
 127   Term y = d_solver.mkVar(bvSort, "y");
 128   TS_ASSERT_THROWS_NOTHING(y.getSort());
 129   TS_ASSERT(y.getSort() == bvSort);
 130
 131   Term f = d_solver.mkVar(funSort1, "f");
 132   TS_ASSERT_THROWS_NOTHING(f.getSort());
 133   TS_ASSERT(f.getSort() == funSort1);
 134   Term p = d_solver.mkVar(funSort2, "p");
 135   TS_ASSERT_THROWS_NOTHING(p.getSort());
 136   TS_ASSERT(p.getSort() == funSort2);
 137
 138   Term zero = d_solver.mkReal(0);
 139   TS_ASSERT_THROWS_NOTHING(zero.getSort());
 140   TS_ASSERT(zero.getSort() == intSort);
 141
 142   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
 143   TS_ASSERT_THROWS_NOTHING(f_x.getSort());
 144   TS_ASSERT(f_x.getSort() == intSort);
 145   Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
 146   TS_ASSERT_THROWS_NOTHING(f_y.getSort());
 147   TS_ASSERT(f_y.getSort() == intSort);
 148   Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
 149   TS_ASSERT_THROWS_NOTHING(sum.getSort());
 150   TS_ASSERT(sum.getSort() == intSort);
 151   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
 152   TS_ASSERT_THROWS_NOTHING(p_0.getSort());
 153   TS_ASSERT(p_0.getSort() == boolSort);
 154   Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
 155   TS_ASSERT_THROWS_NOTHING(p_f_y.getSort());
 156   TS_ASSERT(p_f_y.getSort() == boolSort);
 157 }
 158
 159 void TermBlack::testGetOp()
 160 {
 161   Sort intsort = d_solver.getIntegerSort();
 162   Sort bvsort = d_solver.mkBitVectorSort(8);
 163   Sort arrsort = d_solver.mkArraySort(bvsort, intsort);
 164   Sort funsort = d_solver.mkFunctionSort(intsort, bvsort);
 165
 166   Term x = d_solver.mkConst(intsort, "x");
 167   Term a = d_solver.mkConst(arrsort, "a");
 168   Term b = d_solver.mkConst(bvsort, "b");
 169
 170   TS_ASSERT(!x.hasOp());
 171   TS_ASSERT_THROWS(x.getOp(), CVC4ApiException&);
 172
 173   Term ab = d_solver.mkTerm(SELECT, a, b);
 174   Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0);
 175   Term extb = d_solver.mkTerm(ext, b);
 176
 177   TS_ASSERT(ab.hasOp());
 178   TS_ASSERT_EQUALS(ab.getOp(), Op(&d_solver, SELECT));
 179   TS_ASSERT(!ab.getOp().isIndexed());
 180   // can compare directly to a Kind (will invoke Op constructor)
 181   TS_ASSERT_EQUALS(ab.getOp(), Op(&d_solver, SELECT));
 182   TS_ASSERT(extb.hasOp());
 183   TS_ASSERT(extb.getOp().isIndexed());
 184   TS_ASSERT_EQUALS(extb.getOp(), ext);
 185
 186   Term f = d_solver.mkConst(funsort, "f");
 187   Term fx = d_solver.mkTerm(APPLY_UF, f, x);
 188
 189   TS_ASSERT(!f.hasOp());
 190   TS_ASSERT_THROWS(f.getOp(), CVC4ApiException&);
 191   TS_ASSERT(fx.hasOp());
 192   TS_ASSERT_EQUALS(fx.getOp(), Op(&d_solver, APPLY_UF));
 193   std::vector<Term> children(fx.begin(), fx.end());
 194   // testing rebuild from op and children
 195   TS_ASSERT_EQUALS(fx, d_solver.mkTerm(fx.getOp(), children));
 196
 197   // Test Datatypes Ops
 198   Sort sort = d_solver.mkParamSort("T");
 199   DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort);
 200   DatatypeConstructorDecl cons("cons");
 201   DatatypeConstructorDecl nil("nil");
 202   cons.addSelector("head", sort);
 203   cons.addSelectorSelf("tail");
 204   listDecl.addConstructor(cons);
 205   listDecl.addConstructor(nil);
 206   Sort listSort = d_solver.mkDatatypeSort(listDecl);
 207   Sort intListSort =
 208       listSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()});
 209   Term c = d_solver.mkConst(intListSort, "c");
 210   Datatype list = listSort.getDatatype();
 211   // list datatype constructor and selector operator terms
 212   Term consOpTerm = list.getConstructorTerm("cons");
 213   Term nilOpTerm = list.getConstructorTerm("nil");
 214   Term headOpTerm = list["cons"].getSelectorTerm("head");
 215   Term tailOpTerm = list["cons"].getSelectorTerm("tail");
 216
 217   Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilOpTerm);
 218   Term consTerm = d_solver.mkTerm(
 219       APPLY_CONSTRUCTOR, consOpTerm, d_solver.mkReal(0), nilTerm);
 220   Term headTerm = d_solver.mkTerm(APPLY_SELECTOR, headOpTerm, consTerm);
 221   Term tailTerm = d_solver.mkTerm(APPLY_SELECTOR, tailOpTerm, consTerm);
 222
 223   TS_ASSERT(nilTerm.hasOp());
 224   TS_ASSERT(consTerm.hasOp());
 225   TS_ASSERT(headTerm.hasOp());
 226   TS_ASSERT(tailTerm.hasOp());
 227
 228   TS_ASSERT_EQUALS(nilTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
 229   TS_ASSERT_EQUALS(consTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
 230   TS_ASSERT_EQUALS(headTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
 231   TS_ASSERT_EQUALS(tailTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
 232
 233   // Test rebuilding
 234   children.clear();
 235   children.insert(children.begin(), headTerm.begin(), headTerm.end());
 236   TS_ASSERT_EQUALS(headTerm, d_solver.mkTerm(headTerm.getOp(), children));
 237 }
 238
 239 void TermBlack::testIsNull()
 240 {
 241   Term x;
 242   TS_ASSERT(x.isNull());
 243   x = d_solver.mkVar(d_solver.mkBitVectorSort(4), "x");
 244   TS_ASSERT(!x.isNull());
 245 }
 246
 247 void TermBlack::testNotTerm()
 248 {
 249   Sort bvSort = d_solver.mkBitVectorSort(8);
 250   Sort intSort = d_solver.getIntegerSort();
 251   Sort boolSort = d_solver.getBooleanSort();
 252   Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
 253   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 254
 255   TS_ASSERT_THROWS(Term().notTerm(), CVC4ApiException&);
 256   Term b = d_solver.mkTrue();
 257   TS_ASSERT_THROWS_NOTHING(b.notTerm());
 258   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
 259   TS_ASSERT_THROWS(x.notTerm(), CVC4ApiException&);
 260   Term f = d_solver.mkVar(funSort1, "f");
 261   TS_ASSERT_THROWS(f.notTerm(), CVC4ApiException&);
 262   Term p = d_solver.mkVar(funSort2, "p");
 263   TS_ASSERT_THROWS(p.notTerm(), CVC4ApiException&);
 264   Term zero = d_solver.mkReal(0);
 265   TS_ASSERT_THROWS(zero.notTerm(), CVC4ApiException&);
 266   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
 267   TS_ASSERT_THROWS(f_x.notTerm(), CVC4ApiException&);
 268   Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
 269   TS_ASSERT_THROWS(sum.notTerm(), CVC4ApiException&);
 270   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
 271   TS_ASSERT_THROWS_NOTHING(p_0.notTerm());
 272   Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
 273   TS_ASSERT_THROWS_NOTHING(p_f_x.notTerm());
 274 }
 275
 276 void TermBlack::testAndTerm()
 277 {
 278   Sort bvSort = d_solver.mkBitVectorSort(8);
 279   Sort intSort = d_solver.getIntegerSort();
 280   Sort boolSort = d_solver.getBooleanSort();
 281   Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
 282   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 283
 284   Term b = d_solver.mkTrue();
 285   TS_ASSERT_THROWS(Term().andTerm(b), CVC4ApiException&);
 286   TS_ASSERT_THROWS(b.andTerm(Term()), CVC4ApiException&);
 287   TS_ASSERT_THROWS_NOTHING(b.andTerm(b));
 288   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
 289   TS_ASSERT_THROWS(x.andTerm(b), CVC4ApiException&);
 290   TS_ASSERT_THROWS(x.andTerm(x), CVC4ApiException&);
 291   Term f = d_solver.mkVar(funSort1, "f");
 292   TS_ASSERT_THROWS(f.andTerm(b), CVC4ApiException&);
 293   TS_ASSERT_THROWS(f.andTerm(x), CVC4ApiException&);
 294   TS_ASSERT_THROWS(f.andTerm(f), CVC4ApiException&);
 295   Term p = d_solver.mkVar(funSort2, "p");
 296   TS_ASSERT_THROWS(p.andTerm(b), CVC4ApiException&);
 297   TS_ASSERT_THROWS(p.andTerm(x), CVC4ApiException&);
 298   TS_ASSERT_THROWS(p.andTerm(f), CVC4ApiException&);
 299   TS_ASSERT_THROWS(p.andTerm(p), CVC4ApiException&);
 300   Term zero = d_solver.mkReal(0);
 301   TS_ASSERT_THROWS(zero.andTerm(b), CVC4ApiException&);
 302   TS_ASSERT_THROWS(zero.andTerm(x), CVC4ApiException&);
 303   TS_ASSERT_THROWS(zero.andTerm(f), CVC4ApiException&);
 304   TS_ASSERT_THROWS(zero.andTerm(p), CVC4ApiException&);
 305   TS_ASSERT_THROWS(zero.andTerm(zero), CVC4ApiException&);
 306   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
 307   TS_ASSERT_THROWS(f_x.andTerm(b), CVC4ApiException&);
 308   TS_ASSERT_THROWS(f_x.andTerm(x), CVC4ApiException&);
 309   TS_ASSERT_THROWS(f_x.andTerm(f), CVC4ApiException&);
 310   TS_ASSERT_THROWS(f_x.andTerm(p), CVC4ApiException&);
 311   TS_ASSERT_THROWS(f_x.andTerm(zero), CVC4ApiException&);
 312   TS_ASSERT_THROWS(f_x.andTerm(f_x), CVC4ApiException&);
 313   Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
 314   TS_ASSERT_THROWS(sum.andTerm(b), CVC4ApiException&);
 315   TS_ASSERT_THROWS(sum.andTerm(x), CVC4ApiException&);
 316   TS_ASSERT_THROWS(sum.andTerm(f), CVC4ApiException&);
 317   TS_ASSERT_THROWS(sum.andTerm(p), CVC4ApiException&);
 318   TS_ASSERT_THROWS(sum.andTerm(zero), CVC4ApiException&);
 319   TS_ASSERT_THROWS(sum.andTerm(f_x), CVC4ApiException&);
 320   TS_ASSERT_THROWS(sum.andTerm(sum), CVC4ApiException&);
 321   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
 322   TS_ASSERT_THROWS_NOTHING(p_0.andTerm(b));
 323   TS_ASSERT_THROWS(p_0.andTerm(x), CVC4ApiException&);
 324   TS_ASSERT_THROWS(p_0.andTerm(f), CVC4ApiException&);
 325   TS_ASSERT_THROWS(p_0.andTerm(p), CVC4ApiException&);
 326   TS_ASSERT_THROWS(p_0.andTerm(zero), CVC4ApiException&);
 327   TS_ASSERT_THROWS(p_0.andTerm(f_x), CVC4ApiException&);
 328   TS_ASSERT_THROWS(p_0.andTerm(sum), CVC4ApiException&);
 329   TS_ASSERT_THROWS_NOTHING(p_0.andTerm(p_0));
 330   Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
 331   TS_ASSERT_THROWS_NOTHING(p_f_x.andTerm(b));
 332   TS_ASSERT_THROWS(p_f_x.andTerm(x), CVC4ApiException&);
 333   TS_ASSERT_THROWS(p_f_x.andTerm(f), CVC4ApiException&);
 334   TS_ASSERT_THROWS(p_f_x.andTerm(p), CVC4ApiException&);
 335   TS_ASSERT_THROWS(p_f_x.andTerm(zero), CVC4ApiException&);
 336   TS_ASSERT_THROWS(p_f_x.andTerm(f_x), CVC4ApiException&);
 337   TS_ASSERT_THROWS(p_f_x.andTerm(sum), CVC4ApiException&);
 338   TS_ASSERT_THROWS_NOTHING(p_f_x.andTerm(p_0));
 339   TS_ASSERT_THROWS_NOTHING(p_f_x.andTerm(p_f_x));
 340 }
 341
 342 void TermBlack::testOrTerm()
 343 {
 344   Sort bvSort = d_solver.mkBitVectorSort(8);
 345   Sort intSort = d_solver.getIntegerSort();
 346   Sort boolSort = d_solver.getBooleanSort();
 347   Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
 348   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 349
 350   Term b = d_solver.mkTrue();
 351   TS_ASSERT_THROWS(Term().orTerm(b), CVC4ApiException&);
 352   TS_ASSERT_THROWS(b.orTerm(Term()), CVC4ApiException&);
 353   TS_ASSERT_THROWS_NOTHING(b.orTerm(b));
 354   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
 355   TS_ASSERT_THROWS(x.orTerm(b), CVC4ApiException&);
 356   TS_ASSERT_THROWS(x.orTerm(x), CVC4ApiException&);
 357   Term f = d_solver.mkVar(funSort1, "f");
 358   TS_ASSERT_THROWS(f.orTerm(b), CVC4ApiException&);
 359   TS_ASSERT_THROWS(f.orTerm(x), CVC4ApiException&);
 360   TS_ASSERT_THROWS(f.orTerm(f), CVC4ApiException&);
 361   Term p = d_solver.mkVar(funSort2, "p");
 362   TS_ASSERT_THROWS(p.orTerm(b), CVC4ApiException&);
 363   TS_ASSERT_THROWS(p.orTerm(x), CVC4ApiException&);
 364   TS_ASSERT_THROWS(p.orTerm(f), CVC4ApiException&);
 365   TS_ASSERT_THROWS(p.orTerm(p), CVC4ApiException&);
 366   Term zero = d_solver.mkReal(0);
 367   TS_ASSERT_THROWS(zero.orTerm(b), CVC4ApiException&);
 368   TS_ASSERT_THROWS(zero.orTerm(x), CVC4ApiException&);
 369   TS_ASSERT_THROWS(zero.orTerm(f), CVC4ApiException&);
 370   TS_ASSERT_THROWS(zero.orTerm(p), CVC4ApiException&);
 371   TS_ASSERT_THROWS(zero.orTerm(zero), CVC4ApiException&);
 372   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
 373   TS_ASSERT_THROWS(f_x.orTerm(b), CVC4ApiException&);
 374   TS_ASSERT_THROWS(f_x.orTerm(x), CVC4ApiException&);
 375   TS_ASSERT_THROWS(f_x.orTerm(f), CVC4ApiException&);
 376   TS_ASSERT_THROWS(f_x.orTerm(p), CVC4ApiException&);
 377   TS_ASSERT_THROWS(f_x.orTerm(zero), CVC4ApiException&);
 378   TS_ASSERT_THROWS(f_x.orTerm(f_x), CVC4ApiException&);
 379   Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
 380   TS_ASSERT_THROWS(sum.orTerm(b), CVC4ApiException&);
 381   TS_ASSERT_THROWS(sum.orTerm(x), CVC4ApiException&);
 382   TS_ASSERT_THROWS(sum.orTerm(f), CVC4ApiException&);
 383   TS_ASSERT_THROWS(sum.orTerm(p), CVC4ApiException&);
 384   TS_ASSERT_THROWS(sum.orTerm(zero), CVC4ApiException&);
 385   TS_ASSERT_THROWS(sum.orTerm(f_x), CVC4ApiException&);
 386   TS_ASSERT_THROWS(sum.orTerm(sum), CVC4ApiException&);
 387   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
 388   TS_ASSERT_THROWS_NOTHING(p_0.orTerm(b));
 389   TS_ASSERT_THROWS(p_0.orTerm(x), CVC4ApiException&);
 390   TS_ASSERT_THROWS(p_0.orTerm(f), CVC4ApiException&);
 391   TS_ASSERT_THROWS(p_0.orTerm(p), CVC4ApiException&);
 392   TS_ASSERT_THROWS(p_0.orTerm(zero), CVC4ApiException&);
 393   TS_ASSERT_THROWS(p_0.orTerm(f_x), CVC4ApiException&);
 394   TS_ASSERT_THROWS(p_0.orTerm(sum), CVC4ApiException&);
 395   TS_ASSERT_THROWS_NOTHING(p_0.orTerm(p_0));
 396   Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
 397   TS_ASSERT_THROWS_NOTHING(p_f_x.orTerm(b));
 398   TS_ASSERT_THROWS(p_f_x.orTerm(x), CVC4ApiException&);
 399   TS_ASSERT_THROWS(p_f_x.orTerm(f), CVC4ApiException&);
 400   TS_ASSERT_THROWS(p_f_x.orTerm(p), CVC4ApiException&);
 401   TS_ASSERT_THROWS(p_f_x.orTerm(zero), CVC4ApiException&);
 402   TS_ASSERT_THROWS(p_f_x.orTerm(f_x), CVC4ApiException&);
 403   TS_ASSERT_THROWS(p_f_x.orTerm(sum), CVC4ApiException&);
 404   TS_ASSERT_THROWS_NOTHING(p_f_x.orTerm(p_0));
 405   TS_ASSERT_THROWS_NOTHING(p_f_x.orTerm(p_f_x));
 406 }
 407
 408 void TermBlack::testXorTerm()
 409 {
 410   Sort bvSort = d_solver.mkBitVectorSort(8);
 411   Sort intSort = d_solver.getIntegerSort();
 412   Sort boolSort = d_solver.getBooleanSort();
 413   Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
 414   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 415
 416   Term b = d_solver.mkTrue();
 417   TS_ASSERT_THROWS(Term().xorTerm(b), CVC4ApiException&);
 418   TS_ASSERT_THROWS(b.xorTerm(Term()), CVC4ApiException&);
 419   TS_ASSERT_THROWS_NOTHING(b.xorTerm(b));
 420   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
 421   TS_ASSERT_THROWS(x.xorTerm(b), CVC4ApiException&);
 422   TS_ASSERT_THROWS(x.xorTerm(x), CVC4ApiException&);
 423   Term f = d_solver.mkVar(funSort1, "f");
 424   TS_ASSERT_THROWS(f.xorTerm(b), CVC4ApiException&);
 425   TS_ASSERT_THROWS(f.xorTerm(x), CVC4ApiException&);
 426   TS_ASSERT_THROWS(f.xorTerm(f), CVC4ApiException&);
 427   Term p = d_solver.mkVar(funSort2, "p");
 428   TS_ASSERT_THROWS(p.xorTerm(b), CVC4ApiException&);
 429   TS_ASSERT_THROWS(p.xorTerm(x), CVC4ApiException&);
 430   TS_ASSERT_THROWS(p.xorTerm(f), CVC4ApiException&);
 431   TS_ASSERT_THROWS(p.xorTerm(p), CVC4ApiException&);
 432   Term zero = d_solver.mkReal(0);
 433   TS_ASSERT_THROWS(zero.xorTerm(b), CVC4ApiException&);
 434   TS_ASSERT_THROWS(zero.xorTerm(x), CVC4ApiException&);
 435   TS_ASSERT_THROWS(zero.xorTerm(f), CVC4ApiException&);
 436   TS_ASSERT_THROWS(zero.xorTerm(p), CVC4ApiException&);
 437   TS_ASSERT_THROWS(zero.xorTerm(zero), CVC4ApiException&);
 438   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
 439   TS_ASSERT_THROWS(f_x.xorTerm(b), CVC4ApiException&);
 440   TS_ASSERT_THROWS(f_x.xorTerm(x), CVC4ApiException&);
 441   TS_ASSERT_THROWS(f_x.xorTerm(f), CVC4ApiException&);
 442   TS_ASSERT_THROWS(f_x.xorTerm(p), CVC4ApiException&);
 443   TS_ASSERT_THROWS(f_x.xorTerm(zero), CVC4ApiException&);
 444   TS_ASSERT_THROWS(f_x.xorTerm(f_x), CVC4ApiException&);
 445   Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
 446   TS_ASSERT_THROWS(sum.xorTerm(b), CVC4ApiException&);
 447   TS_ASSERT_THROWS(sum.xorTerm(x), CVC4ApiException&);
 448   TS_ASSERT_THROWS(sum.xorTerm(f), CVC4ApiException&);
 449   TS_ASSERT_THROWS(sum.xorTerm(p), CVC4ApiException&);
 450   TS_ASSERT_THROWS(sum.xorTerm(zero), CVC4ApiException&);
 451   TS_ASSERT_THROWS(sum.xorTerm(f_x), CVC4ApiException&);
 452   TS_ASSERT_THROWS(sum.xorTerm(sum), CVC4ApiException&);
 453   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
 454   TS_ASSERT_THROWS_NOTHING(p_0.xorTerm(b));
 455   TS_ASSERT_THROWS(p_0.xorTerm(x), CVC4ApiException&);
 456   TS_ASSERT_THROWS(p_0.xorTerm(f), CVC4ApiException&);
 457   TS_ASSERT_THROWS(p_0.xorTerm(p), CVC4ApiException&);
 458   TS_ASSERT_THROWS(p_0.xorTerm(zero), CVC4ApiException&);
 459   TS_ASSERT_THROWS(p_0.xorTerm(f_x), CVC4ApiException&);
 460   TS_ASSERT_THROWS(p_0.xorTerm(sum), CVC4ApiException&);
 461   TS_ASSERT_THROWS_NOTHING(p_0.xorTerm(p_0));
 462   Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
 463   TS_ASSERT_THROWS_NOTHING(p_f_x.xorTerm(b));
 464   TS_ASSERT_THROWS(p_f_x.xorTerm(x), CVC4ApiException&);
 465   TS_ASSERT_THROWS(p_f_x.xorTerm(f), CVC4ApiException&);
 466   TS_ASSERT_THROWS(p_f_x.xorTerm(p), CVC4ApiException&);
 467   TS_ASSERT_THROWS(p_f_x.xorTerm(zero), CVC4ApiException&);
 468   TS_ASSERT_THROWS(p_f_x.xorTerm(f_x), CVC4ApiException&);
 469   TS_ASSERT_THROWS(p_f_x.xorTerm(sum), CVC4ApiException&);
 470   TS_ASSERT_THROWS_NOTHING(p_f_x.xorTerm(p_0));
 471   TS_ASSERT_THROWS_NOTHING(p_f_x.xorTerm(p_f_x));
 472 }
 473
 474 void TermBlack::testEqTerm()
 475 {
 476   Sort bvSort = d_solver.mkBitVectorSort(8);
 477   Sort intSort = d_solver.getIntegerSort();
 478   Sort boolSort = d_solver.getBooleanSort();
 479   Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
 480   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 481
 482   Term b = d_solver.mkTrue();
 483   TS_ASSERT_THROWS(Term().eqTerm(b), CVC4ApiException&);
 484   TS_ASSERT_THROWS(b.eqTerm(Term()), CVC4ApiException&);
 485   TS_ASSERT_THROWS_NOTHING(b.eqTerm(b));
 486   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
 487   TS_ASSERT_THROWS(x.eqTerm(b), CVC4ApiException&);
 488   TS_ASSERT_THROWS_NOTHING(x.eqTerm(x));
 489   Term f = d_solver.mkVar(funSort1, "f");
 490   TS_ASSERT_THROWS(f.eqTerm(b), CVC4ApiException&);
 491   TS_ASSERT_THROWS(f.eqTerm(x), CVC4ApiException&);
 492   TS_ASSERT_THROWS_NOTHING(f.eqTerm(f));
 493   Term p = d_solver.mkVar(funSort2, "p");
 494   TS_ASSERT_THROWS(p.eqTerm(b), CVC4ApiException&);
 495   TS_ASSERT_THROWS(p.eqTerm(x), CVC4ApiException&);
 496   TS_ASSERT_THROWS(p.eqTerm(f), CVC4ApiException&);
 497   TS_ASSERT_THROWS_NOTHING(p.eqTerm(p));
 498   Term zero = d_solver.mkReal(0);
 499   TS_ASSERT_THROWS(zero.eqTerm(b), CVC4ApiException&);
 500   TS_ASSERT_THROWS(zero.eqTerm(x), CVC4ApiException&);
 501   TS_ASSERT_THROWS(zero.eqTerm(f), CVC4ApiException&);
 502   TS_ASSERT_THROWS(zero.eqTerm(p), CVC4ApiException&);
 503   TS_ASSERT_THROWS_NOTHING(zero.eqTerm(zero));
 504   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
 505   TS_ASSERT_THROWS(f_x.eqTerm(b), CVC4ApiException&);
 506   TS_ASSERT_THROWS(f_x.eqTerm(x), CVC4ApiException&);
 507   TS_ASSERT_THROWS(f_x.eqTerm(f), CVC4ApiException&);
 508   TS_ASSERT_THROWS(f_x.eqTerm(p), CVC4ApiException&);
 509   TS_ASSERT_THROWS_NOTHING(f_x.eqTerm(zero));
 510   TS_ASSERT_THROWS_NOTHING(f_x.eqTerm(f_x));
 511   Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
 512   TS_ASSERT_THROWS(sum.eqTerm(b), CVC4ApiException&);
 513   TS_ASSERT_THROWS(sum.eqTerm(x), CVC4ApiException&);
 514   TS_ASSERT_THROWS(sum.eqTerm(f), CVC4ApiException&);
 515   TS_ASSERT_THROWS(sum.eqTerm(p), CVC4ApiException&);
 516   TS_ASSERT_THROWS_NOTHING(sum.eqTerm(zero));
 517   TS_ASSERT_THROWS_NOTHING(sum.eqTerm(f_x));
 518   TS_ASSERT_THROWS_NOTHING(sum.eqTerm(sum));
 519   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
 520   TS_ASSERT_THROWS_NOTHING(p_0.eqTerm(b));
 521   TS_ASSERT_THROWS(p_0.eqTerm(x), CVC4ApiException&);
 522   TS_ASSERT_THROWS(p_0.eqTerm(f), CVC4ApiException&);
 523   TS_ASSERT_THROWS(p_0.eqTerm(p), CVC4ApiException&);
 524   TS_ASSERT_THROWS(p_0.eqTerm(zero), CVC4ApiException&);
 525   TS_ASSERT_THROWS(p_0.eqTerm(f_x), CVC4ApiException&);
 526   TS_ASSERT_THROWS(p_0.eqTerm(sum), CVC4ApiException&);
 527   TS_ASSERT_THROWS_NOTHING(p_0.eqTerm(p_0));
 528   Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
 529   TS_ASSERT_THROWS_NOTHING(p_f_x.eqTerm(b));
 530   TS_ASSERT_THROWS(p_f_x.eqTerm(x), CVC4ApiException&);
 531   TS_ASSERT_THROWS(p_f_x.eqTerm(f), CVC4ApiException&);
 532   TS_ASSERT_THROWS(p_f_x.eqTerm(p), CVC4ApiException&);
 533   TS_ASSERT_THROWS(p_f_x.eqTerm(zero), CVC4ApiException&);
 534   TS_ASSERT_THROWS(p_f_x.eqTerm(f_x), CVC4ApiException&);
 535   TS_ASSERT_THROWS(p_f_x.eqTerm(sum), CVC4ApiException&);
 536   TS_ASSERT_THROWS_NOTHING(p_f_x.eqTerm(p_0));
 537   TS_ASSERT_THROWS_NOTHING(p_f_x.eqTerm(p_f_x));
 538 }
 539
 540 void TermBlack::testImpTerm()
 541 {
 542   Sort bvSort = d_solver.mkBitVectorSort(8);
 543   Sort intSort = d_solver.getIntegerSort();
 544   Sort boolSort = d_solver.getBooleanSort();
 545   Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
 546   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 547
 548   Term b = d_solver.mkTrue();
 549   TS_ASSERT_THROWS(Term().impTerm(b), CVC4ApiException&);
 550   TS_ASSERT_THROWS(b.impTerm(Term()), CVC4ApiException&);
 551   TS_ASSERT_THROWS_NOTHING(b.impTerm(b));
 552   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
 553   TS_ASSERT_THROWS(x.impTerm(b), CVC4ApiException&);
 554   TS_ASSERT_THROWS(x.impTerm(x), CVC4ApiException&);
 555   Term f = d_solver.mkVar(funSort1, "f");
 556   TS_ASSERT_THROWS(f.impTerm(b), CVC4ApiException&);
 557   TS_ASSERT_THROWS(f.impTerm(x), CVC4ApiException&);
 558   TS_ASSERT_THROWS(f.impTerm(f), CVC4ApiException&);
 559   Term p = d_solver.mkVar(funSort2, "p");
 560   TS_ASSERT_THROWS(p.impTerm(b), CVC4ApiException&);
 561   TS_ASSERT_THROWS(p.impTerm(x), CVC4ApiException&);
 562   TS_ASSERT_THROWS(p.impTerm(f), CVC4ApiException&);
 563   TS_ASSERT_THROWS(p.impTerm(p), CVC4ApiException&);
 564   Term zero = d_solver.mkReal(0);
 565   TS_ASSERT_THROWS(zero.impTerm(b), CVC4ApiException&);
 566   TS_ASSERT_THROWS(zero.impTerm(x), CVC4ApiException&);
 567   TS_ASSERT_THROWS(zero.impTerm(f), CVC4ApiException&);
 568   TS_ASSERT_THROWS(zero.impTerm(p), CVC4ApiException&);
 569   TS_ASSERT_THROWS(zero.impTerm(zero), CVC4ApiException&);
 570   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
 571   TS_ASSERT_THROWS(f_x.impTerm(b), CVC4ApiException&);
 572   TS_ASSERT_THROWS(f_x.impTerm(x), CVC4ApiException&);
 573   TS_ASSERT_THROWS(f_x.impTerm(f), CVC4ApiException&);
 574   TS_ASSERT_THROWS(f_x.impTerm(p), CVC4ApiException&);
 575   TS_ASSERT_THROWS(f_x.impTerm(zero), CVC4ApiException&);
 576   TS_ASSERT_THROWS(f_x.impTerm(f_x), CVC4ApiException&);
 577   Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
 578   TS_ASSERT_THROWS(sum.impTerm(b), CVC4ApiException&);
 579   TS_ASSERT_THROWS(sum.impTerm(x), CVC4ApiException&);
 580   TS_ASSERT_THROWS(sum.impTerm(f), CVC4ApiException&);
 581   TS_ASSERT_THROWS(sum.impTerm(p), CVC4ApiException&);
 582   TS_ASSERT_THROWS(sum.impTerm(zero), CVC4ApiException&);
 583   TS_ASSERT_THROWS(sum.impTerm(f_x), CVC4ApiException&);
 584   TS_ASSERT_THROWS(sum.impTerm(sum), CVC4ApiException&);
 585   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
 586   TS_ASSERT_THROWS_NOTHING(p_0.impTerm(b));
 587   TS_ASSERT_THROWS(p_0.impTerm(x), CVC4ApiException&);
 588   TS_ASSERT_THROWS(p_0.impTerm(f), CVC4ApiException&);
 589   TS_ASSERT_THROWS(p_0.impTerm(p), CVC4ApiException&);
 590   TS_ASSERT_THROWS(p_0.impTerm(zero), CVC4ApiException&);
 591   TS_ASSERT_THROWS(p_0.impTerm(f_x), CVC4ApiException&);
 592   TS_ASSERT_THROWS(p_0.impTerm(sum), CVC4ApiException&);
 593   TS_ASSERT_THROWS_NOTHING(p_0.impTerm(p_0));
 594   Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
 595   TS_ASSERT_THROWS_NOTHING(p_f_x.impTerm(b));
 596   TS_ASSERT_THROWS(p_f_x.impTerm(x), CVC4ApiException&);
 597   TS_ASSERT_THROWS(p_f_x.impTerm(f), CVC4ApiException&);
 598   TS_ASSERT_THROWS(p_f_x.impTerm(p), CVC4ApiException&);
 599   TS_ASSERT_THROWS(p_f_x.impTerm(zero), CVC4ApiException&);
 600   TS_ASSERT_THROWS(p_f_x.impTerm(f_x), CVC4ApiException&);
 601   TS_ASSERT_THROWS(p_f_x.impTerm(sum), CVC4ApiException&);
 602   TS_ASSERT_THROWS_NOTHING(p_f_x.impTerm(p_0));
 603   TS_ASSERT_THROWS_NOTHING(p_f_x.impTerm(p_f_x));
 604 }
 605
 606 void TermBlack::testIteTerm()
 607 {
 608   Sort bvSort = d_solver.mkBitVectorSort(8);
 609   Sort intSort = d_solver.getIntegerSort();
 610   Sort boolSort = d_solver.getBooleanSort();
 611   Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
 612   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 613
 614   Term b = d_solver.mkTrue();
 615   TS_ASSERT_THROWS(Term().iteTerm(b, b), CVC4ApiException&);
 616   TS_ASSERT_THROWS(b.iteTerm(Term(), b), CVC4ApiException&);
 617   TS_ASSERT_THROWS(b.iteTerm(b, Term()), CVC4ApiException&);
 618   TS_ASSERT_THROWS_NOTHING(b.iteTerm(b, b));
 619   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
 620   TS_ASSERT_THROWS_NOTHING(b.iteTerm(x, x));
 621   TS_ASSERT_THROWS_NOTHING(b.iteTerm(b, b));
 622   TS_ASSERT_THROWS(b.iteTerm(x, b), CVC4ApiException&);
 623   TS_ASSERT_THROWS(x.iteTerm(x, x), CVC4ApiException&);
 624   TS_ASSERT_THROWS(x.iteTerm(x, b), CVC4ApiException&);
 625   Term f = d_solver.mkVar(funSort1, "f");
 626   TS_ASSERT_THROWS(f.iteTerm(b, b), CVC4ApiException&);
 627   TS_ASSERT_THROWS(x.iteTerm(b, x), CVC4ApiException&);
 628   Term p = d_solver.mkVar(funSort2, "p");
 629   TS_ASSERT_THROWS(p.iteTerm(b, b), CVC4ApiException&);
 630   TS_ASSERT_THROWS(p.iteTerm(x, b), CVC4ApiException&);
 631   Term zero = d_solver.mkReal(0);
 632   TS_ASSERT_THROWS(zero.iteTerm(x, x), CVC4ApiException&);
 633   TS_ASSERT_THROWS(zero.iteTerm(x, b), CVC4ApiException&);
 634   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
 635   TS_ASSERT_THROWS(f_x.iteTerm(b, b), CVC4ApiException&);
 636   TS_ASSERT_THROWS(f_x.iteTerm(b, x), CVC4ApiException&);
 637   Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
 638   TS_ASSERT_THROWS(sum.iteTerm(x, x), CVC4ApiException&);
 639   TS_ASSERT_THROWS(sum.iteTerm(b, x), CVC4ApiException&);
 640   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
 641   TS_ASSERT_THROWS_NOTHING(p_0.iteTerm(b, b));
 642   TS_ASSERT_THROWS_NOTHING(p_0.iteTerm(x, x));
 643   TS_ASSERT_THROWS(p_0.iteTerm(x, b), CVC4ApiException&);
 644   Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
 645   TS_ASSERT_THROWS_NOTHING(p_f_x.iteTerm(b, b));
 646   TS_ASSERT_THROWS_NOTHING(p_f_x.iteTerm(x, x));
 647   TS_ASSERT_THROWS(p_f_x.iteTerm(x, b), CVC4ApiException&);
 648 }
 649
 650 void TermBlack::testTermAssignment()
 651 {
 652   Term t1 = d_solver.mkReal(1);
 653   Term t2 = t1;
 654   t2 = d_solver.mkReal(2);
 655   TS_ASSERT_EQUALS(t1, d_solver.mkReal(1));
 656 }
 657
 658 void TermBlack::testTermCompare()
 659 {
 660   Term t1 = d_solver.mkReal(1);
 661   Term t2 = d_solver.mkTerm(PLUS, d_solver.mkReal(2), d_solver.mkReal(2));
 662   Term t3 = d_solver.mkTerm(PLUS, d_solver.mkReal(2), d_solver.mkReal(2));
 663   TS_ASSERT(t2 >= t3);
 664   TS_ASSERT(t2 <= t3);
 665   TS_ASSERT((t1 > t2) != (t1 < t2));
 666   TS_ASSERT((t1 > t2 || t1 == t2) == (t1 >= t2));
 667 }
 668
 669 void TermBlack::testTermChildren()
 670 {
 671   // simple term 2+3
 672   Term two = d_solver.mkReal(2);
 673   Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkReal(3));
 674   TS_ASSERT(t1[0] == two);
 675   TS_ASSERT(t1.getNumChildren() == 2);
 676   Term tnull;
 677   TS_ASSERT_THROWS(tnull.getNumChildren(), CVC4ApiException&);
 678
 679   // apply term f(2)
 680   Sort intSort = d_solver.getIntegerSort();
 681   Sort fsort = d_solver.mkFunctionSort(intSort, intSort);
 682   Term f = d_solver.mkConst(fsort, "f");
 683   Term t2 = d_solver.mkTerm(APPLY_UF, f, two);
 684   // due to our higher-order view of terms, we treat f as a child of APPLY_UF
 685   TS_ASSERT(t2.getNumChildren() == 2);
 686   TS_ASSERT_EQUALS(t2[0], f);
 687   TS_ASSERT_EQUALS(t2[1], two);
 688   TS_ASSERT_THROWS(tnull[0], CVC4ApiException&);
 689 }
 690
 691 void TermBlack::testSubstitute()
 692 {
 693   Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
 694   Term one = d_solver.mkReal(1);
 695   Term ttrue = d_solver.mkTrue();
 696   Term xpx = d_solver.mkTerm(PLUS, x, x);
 697   Term onepone = d_solver.mkTerm(PLUS, one, one);
 698
 699   TS_ASSERT_EQUALS(xpx.substitute(x, one), onepone);
 700   TS_ASSERT_EQUALS(onepone.substitute(one, x), xpx);
 701   // incorrect due to type
 702   TS_ASSERT_THROWS(xpx.substitute(one, ttrue), CVC4ApiException&);
 703
 704   // simultaneous substitution
 705   Term y = d_solver.mkConst(d_solver.getIntegerSort(), "y");
 706   Term xpy = d_solver.mkTerm(PLUS, x, y);
 707   Term xpone = d_solver.mkTerm(PLUS, y, one);
 708   std::vector<Term> es;
 709   std::vector<Term> rs;
 710   es.push_back(x);
 711   rs.push_back(y);
 712   es.push_back(y);
 713   rs.push_back(one);
 714   TS_ASSERT_EQUALS(xpy.substitute(es, rs), xpone);
 715
 716   // incorrect substitution due to arity
 717   rs.pop_back();
 718   TS_ASSERT_THROWS(xpy.substitute(es, rs), CVC4ApiException&);
 719
 720   // incorrect substitution due to types
 721   rs.push_back(ttrue);
 722   TS_ASSERT_THROWS(xpy.substitute(es, rs), CVC4ApiException&);
 723
 724   // null cannot substitute
 725   Term tnull;
 726   TS_ASSERT_THROWS(tnull.substitute(one, x), CVC4ApiException&);
 727   TS_ASSERT_THROWS(xpx.substitute(tnull, x), CVC4ApiException&);
 728   TS_ASSERT_THROWS(xpx.substitute(x, tnull), CVC4ApiException&);
 729   rs.pop_back();
 730   rs.push_back(tnull);
 731   TS_ASSERT_THROWS(xpy.substitute(es, rs), CVC4ApiException&);
 732   es.clear();
 733   rs.clear();
 734   es.push_back(x);
 735   rs.push_back(y);
 736   TS_ASSERT_THROWS(tnull.substitute(es, rs), CVC4ApiException&);
 737   es.push_back(tnull);
 738   rs.push_back(one);
 739   TS_ASSERT_THROWS(xpx.substitute(es, rs), CVC4ApiException&);
 740 }
 741
 742 void TermBlack::testIsConst()
 743 {
 744   Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
 745   Term one = d_solver.mkReal(1);
 746   Term xpone = d_solver.mkTerm(PLUS, x, one);
 747   Term onepone = d_solver.mkTerm(PLUS, one, one);
 748   TS_ASSERT(!x.isConst());
 749   TS_ASSERT(one.isConst());
 750   TS_ASSERT(!xpone.isConst());
 751   TS_ASSERT(!onepone.isConst());
 752   Term tnull;
 753   TS_ASSERT_THROWS(tnull.isConst(), CVC4ApiException&);
 754 }