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 testIsNull();
  32   void testIsParameterized();
  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
  43  private:
  44   Solver d_solver;
  45 };
  46
  47 void TermBlack::testEq()
  48 {
  49   Sort uSort = d_solver.mkUninterpretedSort("u");
  50   Term x = d_solver.mkVar(uSort, "x");
  51   Term y = d_solver.mkVar(uSort, "y");
  52   Term z;
  53
  54   TS_ASSERT(x == x);
  55   TS_ASSERT(!(x != x));
  56   TS_ASSERT(!(x == y));
  57   TS_ASSERT(x != y);
  58   TS_ASSERT(!(x == z));
  59   TS_ASSERT(x != z);
  60 }
  61
  62 void TermBlack::testGetId()
  63 {
  64   Term n;
  65   TS_ASSERT_THROWS(n.getId(), CVC4ApiException&);
  66   Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x");
  67   TS_ASSERT_THROWS_NOTHING(x.getId());
  68   Term y = x;
  69   TS_ASSERT_EQUALS(x.getId(), y.getId());
  70
  71   Term z = d_solver.mkVar(d_solver.getIntegerSort(), "z");
  72   TS_ASSERT_DIFFERS(x.getId(), z.getId());
  73 }
  74
  75 void TermBlack::testGetKind()
  76 {
  77   Sort uSort = d_solver.mkUninterpretedSort("u");
  78   Sort intSort = d_solver.getIntegerSort();
  79   Sort boolSort = d_solver.getBooleanSort();
  80   Sort funSort1 = d_solver.mkFunctionSort(uSort, intSort);
  81   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
  82
  83   Term n;
  84   TS_ASSERT_THROWS(n.getKind(), CVC4ApiException&);
  85   Term x = d_solver.mkVar(uSort, "x");
  86   TS_ASSERT_THROWS_NOTHING(x.getKind());
  87   Term y = d_solver.mkVar(uSort, "y");
  88   TS_ASSERT_THROWS_NOTHING(y.getKind());
  89
  90   Term f = d_solver.mkVar(funSort1, "f");
  91   TS_ASSERT_THROWS_NOTHING(f.getKind());
  92   Term p = d_solver.mkVar(funSort2, "p");
  93   TS_ASSERT_THROWS_NOTHING(p.getKind());
  94
  95   Term zero = d_solver.mkReal(0);
  96   TS_ASSERT_THROWS_NOTHING(zero.getKind());
  97
  98   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
  99   TS_ASSERT_THROWS_NOTHING(f_x.getKind());
 100   Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
 101   TS_ASSERT_THROWS_NOTHING(f_y.getKind());
 102   Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
 103   TS_ASSERT_THROWS_NOTHING(sum.getKind());
 104   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
 105   TS_ASSERT_THROWS_NOTHING(p_0.getKind());
 106   Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
 107   TS_ASSERT_THROWS_NOTHING(p_f_y.getKind());
 108 }
 109
 110 void TermBlack::testGetSort()
 111 {
 112   Sort bvSort = d_solver.mkBitVectorSort(8);
 113   Sort intSort = d_solver.getIntegerSort();
 114   Sort boolSort = d_solver.getBooleanSort();
 115   Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
 116   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 117
 118   Term n;
 119   TS_ASSERT_THROWS(n.getSort(), CVC4ApiException&);
 120   Term x = d_solver.mkVar(bvSort, "x");
 121   TS_ASSERT_THROWS_NOTHING(x.getSort());
 122   TS_ASSERT(x.getSort() == bvSort);
 123   Term y = d_solver.mkVar(bvSort, "y");
 124   TS_ASSERT_THROWS_NOTHING(y.getSort());
 125   TS_ASSERT(y.getSort() == bvSort);
 126
 127   Term f = d_solver.mkVar(funSort1, "f");
 128   TS_ASSERT_THROWS_NOTHING(f.getSort());
 129   TS_ASSERT(f.getSort() == funSort1);
 130   Term p = d_solver.mkVar(funSort2, "p");
 131   TS_ASSERT_THROWS_NOTHING(p.getSort());
 132   TS_ASSERT(p.getSort() == funSort2);
 133
 134   Term zero = d_solver.mkReal(0);
 135   TS_ASSERT_THROWS_NOTHING(zero.getSort());
 136   TS_ASSERT(zero.getSort() == intSort);
 137
 138   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
 139   TS_ASSERT_THROWS_NOTHING(f_x.getSort());
 140   TS_ASSERT(f_x.getSort() == intSort);
 141   Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
 142   TS_ASSERT_THROWS_NOTHING(f_y.getSort());
 143   TS_ASSERT(f_y.getSort() == intSort);
 144   Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
 145   TS_ASSERT_THROWS_NOTHING(sum.getSort());
 146   TS_ASSERT(sum.getSort() == intSort);
 147   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
 148   TS_ASSERT_THROWS_NOTHING(p_0.getSort());
 149   TS_ASSERT(p_0.getSort() == boolSort);
 150   Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
 151   TS_ASSERT_THROWS_NOTHING(p_f_y.getSort());
 152   TS_ASSERT(p_f_y.getSort() == boolSort);
 153 }
 154
 155 void TermBlack::testIsNull()
 156 {
 157   Term x;
 158   TS_ASSERT(x.isNull());
 159   x = d_solver.mkVar(d_solver.mkBitVectorSort(4), "x");
 160   TS_ASSERT(!x.isNull());
 161 }
 162
 163 void TermBlack::testNotTerm()
 164 {
 165   Sort bvSort = d_solver.mkBitVectorSort(8);
 166   Sort intSort = d_solver.getIntegerSort();
 167   Sort boolSort = d_solver.getBooleanSort();
 168   Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
 169   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 170
 171   TS_ASSERT_THROWS(Term().notTerm(), CVC4ApiException&);
 172   Term b = d_solver.mkTrue();
 173   TS_ASSERT_THROWS_NOTHING(b.notTerm());
 174   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
 175   TS_ASSERT_THROWS(x.notTerm(), CVC4ApiException&);
 176   Term f = d_solver.mkVar(funSort1, "f");
 177   TS_ASSERT_THROWS(f.notTerm(), CVC4ApiException&);
 178   Term p = d_solver.mkVar(funSort2, "p");
 179   TS_ASSERT_THROWS(p.notTerm(), CVC4ApiException&);
 180   Term zero = d_solver.mkReal(0);
 181   TS_ASSERT_THROWS(zero.notTerm(), CVC4ApiException&);
 182   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
 183   TS_ASSERT_THROWS(f_x.notTerm(), CVC4ApiException&);
 184   Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
 185   TS_ASSERT_THROWS(sum.notTerm(), CVC4ApiException&);
 186   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
 187   TS_ASSERT_THROWS_NOTHING(p_0.notTerm());
 188   Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
 189   TS_ASSERT_THROWS_NOTHING(p_f_x.notTerm());
 190 }
 191
 192 void TermBlack::testIsParameterized()
 193 {
 194   Term n;
 195   TS_ASSERT_THROWS(n.isParameterized(), CVC4ApiException&);
 196   Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x");
 197   TS_ASSERT_THROWS_NOTHING(x.isParameterized());
 198 }
 199
 200 void TermBlack::testAndTerm()
 201 {
 202   Sort bvSort = d_solver.mkBitVectorSort(8);
 203   Sort intSort = d_solver.getIntegerSort();
 204   Sort boolSort = d_solver.getBooleanSort();
 205   Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
 206   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 207
 208   Term b = d_solver.mkTrue();
 209   TS_ASSERT_THROWS(Term().andTerm(b), CVC4ApiException&);
 210   TS_ASSERT_THROWS(b.andTerm(Term()), CVC4ApiException&);
 211   TS_ASSERT_THROWS_NOTHING(b.andTerm(b));
 212   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
 213   TS_ASSERT_THROWS(x.andTerm(b), CVC4ApiException&);
 214   TS_ASSERT_THROWS(x.andTerm(x), CVC4ApiException&);
 215   Term f = d_solver.mkVar(funSort1, "f");
 216   TS_ASSERT_THROWS(f.andTerm(b), CVC4ApiException&);
 217   TS_ASSERT_THROWS(f.andTerm(x), CVC4ApiException&);
 218   TS_ASSERT_THROWS(f.andTerm(f), CVC4ApiException&);
 219   Term p = d_solver.mkVar(funSort2, "p");
 220   TS_ASSERT_THROWS(p.andTerm(b), CVC4ApiException&);
 221   TS_ASSERT_THROWS(p.andTerm(x), CVC4ApiException&);
 222   TS_ASSERT_THROWS(p.andTerm(f), CVC4ApiException&);
 223   TS_ASSERT_THROWS(p.andTerm(p), CVC4ApiException&);
 224   Term zero = d_solver.mkReal(0);
 225   TS_ASSERT_THROWS(zero.andTerm(b), CVC4ApiException&);
 226   TS_ASSERT_THROWS(zero.andTerm(x), CVC4ApiException&);
 227   TS_ASSERT_THROWS(zero.andTerm(f), CVC4ApiException&);
 228   TS_ASSERT_THROWS(zero.andTerm(p), CVC4ApiException&);
 229   TS_ASSERT_THROWS(zero.andTerm(zero), CVC4ApiException&);
 230   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
 231   TS_ASSERT_THROWS(f_x.andTerm(b), CVC4ApiException&);
 232   TS_ASSERT_THROWS(f_x.andTerm(x), CVC4ApiException&);
 233   TS_ASSERT_THROWS(f_x.andTerm(f), CVC4ApiException&);
 234   TS_ASSERT_THROWS(f_x.andTerm(p), CVC4ApiException&);
 235   TS_ASSERT_THROWS(f_x.andTerm(zero), CVC4ApiException&);
 236   TS_ASSERT_THROWS(f_x.andTerm(f_x), CVC4ApiException&);
 237   Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
 238   TS_ASSERT_THROWS(sum.andTerm(b), CVC4ApiException&);
 239   TS_ASSERT_THROWS(sum.andTerm(x), CVC4ApiException&);
 240   TS_ASSERT_THROWS(sum.andTerm(f), CVC4ApiException&);
 241   TS_ASSERT_THROWS(sum.andTerm(p), CVC4ApiException&);
 242   TS_ASSERT_THROWS(sum.andTerm(zero), CVC4ApiException&);
 243   TS_ASSERT_THROWS(sum.andTerm(f_x), CVC4ApiException&);
 244   TS_ASSERT_THROWS(sum.andTerm(sum), CVC4ApiException&);
 245   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
 246   TS_ASSERT_THROWS_NOTHING(p_0.andTerm(b));
 247   TS_ASSERT_THROWS(p_0.andTerm(x), CVC4ApiException&);
 248   TS_ASSERT_THROWS(p_0.andTerm(f), CVC4ApiException&);
 249   TS_ASSERT_THROWS(p_0.andTerm(p), CVC4ApiException&);
 250   TS_ASSERT_THROWS(p_0.andTerm(zero), CVC4ApiException&);
 251   TS_ASSERT_THROWS(p_0.andTerm(f_x), CVC4ApiException&);
 252   TS_ASSERT_THROWS(p_0.andTerm(sum), CVC4ApiException&);
 253   TS_ASSERT_THROWS_NOTHING(p_0.andTerm(p_0));
 254   Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
 255   TS_ASSERT_THROWS_NOTHING(p_f_x.andTerm(b));
 256   TS_ASSERT_THROWS(p_f_x.andTerm(x), CVC4ApiException&);
 257   TS_ASSERT_THROWS(p_f_x.andTerm(f), CVC4ApiException&);
 258   TS_ASSERT_THROWS(p_f_x.andTerm(p), CVC4ApiException&);
 259   TS_ASSERT_THROWS(p_f_x.andTerm(zero), CVC4ApiException&);
 260   TS_ASSERT_THROWS(p_f_x.andTerm(f_x), CVC4ApiException&);
 261   TS_ASSERT_THROWS(p_f_x.andTerm(sum), CVC4ApiException&);
 262   TS_ASSERT_THROWS_NOTHING(p_f_x.andTerm(p_0));
 263   TS_ASSERT_THROWS_NOTHING(p_f_x.andTerm(p_f_x));
 264 }
 265
 266 void TermBlack::testOrTerm()
 267 {
 268   Sort bvSort = d_solver.mkBitVectorSort(8);
 269   Sort intSort = d_solver.getIntegerSort();
 270   Sort boolSort = d_solver.getBooleanSort();
 271   Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
 272   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 273
 274   Term b = d_solver.mkTrue();
 275   TS_ASSERT_THROWS(Term().orTerm(b), CVC4ApiException&);
 276   TS_ASSERT_THROWS(b.orTerm(Term()), CVC4ApiException&);
 277   TS_ASSERT_THROWS_NOTHING(b.orTerm(b));
 278   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
 279   TS_ASSERT_THROWS(x.orTerm(b), CVC4ApiException&);
 280   TS_ASSERT_THROWS(x.orTerm(x), CVC4ApiException&);
 281   Term f = d_solver.mkVar(funSort1, "f");
 282   TS_ASSERT_THROWS(f.orTerm(b), CVC4ApiException&);
 283   TS_ASSERT_THROWS(f.orTerm(x), CVC4ApiException&);
 284   TS_ASSERT_THROWS(f.orTerm(f), CVC4ApiException&);
 285   Term p = d_solver.mkVar(funSort2, "p");
 286   TS_ASSERT_THROWS(p.orTerm(b), CVC4ApiException&);
 287   TS_ASSERT_THROWS(p.orTerm(x), CVC4ApiException&);
 288   TS_ASSERT_THROWS(p.orTerm(f), CVC4ApiException&);
 289   TS_ASSERT_THROWS(p.orTerm(p), CVC4ApiException&);
 290   Term zero = d_solver.mkReal(0);
 291   TS_ASSERT_THROWS(zero.orTerm(b), CVC4ApiException&);
 292   TS_ASSERT_THROWS(zero.orTerm(x), CVC4ApiException&);
 293   TS_ASSERT_THROWS(zero.orTerm(f), CVC4ApiException&);
 294   TS_ASSERT_THROWS(zero.orTerm(p), CVC4ApiException&);
 295   TS_ASSERT_THROWS(zero.orTerm(zero), CVC4ApiException&);
 296   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
 297   TS_ASSERT_THROWS(f_x.orTerm(b), CVC4ApiException&);
 298   TS_ASSERT_THROWS(f_x.orTerm(x), CVC4ApiException&);
 299   TS_ASSERT_THROWS(f_x.orTerm(f), CVC4ApiException&);
 300   TS_ASSERT_THROWS(f_x.orTerm(p), CVC4ApiException&);
 301   TS_ASSERT_THROWS(f_x.orTerm(zero), CVC4ApiException&);
 302   TS_ASSERT_THROWS(f_x.orTerm(f_x), CVC4ApiException&);
 303   Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
 304   TS_ASSERT_THROWS(sum.orTerm(b), CVC4ApiException&);
 305   TS_ASSERT_THROWS(sum.orTerm(x), CVC4ApiException&);
 306   TS_ASSERT_THROWS(sum.orTerm(f), CVC4ApiException&);
 307   TS_ASSERT_THROWS(sum.orTerm(p), CVC4ApiException&);
 308   TS_ASSERT_THROWS(sum.orTerm(zero), CVC4ApiException&);
 309   TS_ASSERT_THROWS(sum.orTerm(f_x), CVC4ApiException&);
 310   TS_ASSERT_THROWS(sum.orTerm(sum), CVC4ApiException&);
 311   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
 312   TS_ASSERT_THROWS_NOTHING(p_0.orTerm(b));
 313   TS_ASSERT_THROWS(p_0.orTerm(x), CVC4ApiException&);
 314   TS_ASSERT_THROWS(p_0.orTerm(f), CVC4ApiException&);
 315   TS_ASSERT_THROWS(p_0.orTerm(p), CVC4ApiException&);
 316   TS_ASSERT_THROWS(p_0.orTerm(zero), CVC4ApiException&);
 317   TS_ASSERT_THROWS(p_0.orTerm(f_x), CVC4ApiException&);
 318   TS_ASSERT_THROWS(p_0.orTerm(sum), CVC4ApiException&);
 319   TS_ASSERT_THROWS_NOTHING(p_0.orTerm(p_0));
 320   Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
 321   TS_ASSERT_THROWS_NOTHING(p_f_x.orTerm(b));
 322   TS_ASSERT_THROWS(p_f_x.orTerm(x), CVC4ApiException&);
 323   TS_ASSERT_THROWS(p_f_x.orTerm(f), CVC4ApiException&);
 324   TS_ASSERT_THROWS(p_f_x.orTerm(p), CVC4ApiException&);
 325   TS_ASSERT_THROWS(p_f_x.orTerm(zero), CVC4ApiException&);
 326   TS_ASSERT_THROWS(p_f_x.orTerm(f_x), CVC4ApiException&);
 327   TS_ASSERT_THROWS(p_f_x.orTerm(sum), CVC4ApiException&);
 328   TS_ASSERT_THROWS_NOTHING(p_f_x.orTerm(p_0));
 329   TS_ASSERT_THROWS_NOTHING(p_f_x.orTerm(p_f_x));
 330 }
 331
 332 void TermBlack::testXorTerm()
 333 {
 334   Sort bvSort = d_solver.mkBitVectorSort(8);
 335   Sort intSort = d_solver.getIntegerSort();
 336   Sort boolSort = d_solver.getBooleanSort();
 337   Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
 338   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 339
 340   Term b = d_solver.mkTrue();
 341   TS_ASSERT_THROWS(Term().xorTerm(b), CVC4ApiException&);
 342   TS_ASSERT_THROWS(b.xorTerm(Term()), CVC4ApiException&);
 343   TS_ASSERT_THROWS_NOTHING(b.xorTerm(b));
 344   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
 345   TS_ASSERT_THROWS(x.xorTerm(b), CVC4ApiException&);
 346   TS_ASSERT_THROWS(x.xorTerm(x), CVC4ApiException&);
 347   Term f = d_solver.mkVar(funSort1, "f");
 348   TS_ASSERT_THROWS(f.xorTerm(b), CVC4ApiException&);
 349   TS_ASSERT_THROWS(f.xorTerm(x), CVC4ApiException&);
 350   TS_ASSERT_THROWS(f.xorTerm(f), CVC4ApiException&);
 351   Term p = d_solver.mkVar(funSort2, "p");
 352   TS_ASSERT_THROWS(p.xorTerm(b), CVC4ApiException&);
 353   TS_ASSERT_THROWS(p.xorTerm(x), CVC4ApiException&);
 354   TS_ASSERT_THROWS(p.xorTerm(f), CVC4ApiException&);
 355   TS_ASSERT_THROWS(p.xorTerm(p), CVC4ApiException&);
 356   Term zero = d_solver.mkReal(0);
 357   TS_ASSERT_THROWS(zero.xorTerm(b), CVC4ApiException&);
 358   TS_ASSERT_THROWS(zero.xorTerm(x), CVC4ApiException&);
 359   TS_ASSERT_THROWS(zero.xorTerm(f), CVC4ApiException&);
 360   TS_ASSERT_THROWS(zero.xorTerm(p), CVC4ApiException&);
 361   TS_ASSERT_THROWS(zero.xorTerm(zero), CVC4ApiException&);
 362   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
 363   TS_ASSERT_THROWS(f_x.xorTerm(b), CVC4ApiException&);
 364   TS_ASSERT_THROWS(f_x.xorTerm(x), CVC4ApiException&);
 365   TS_ASSERT_THROWS(f_x.xorTerm(f), CVC4ApiException&);
 366   TS_ASSERT_THROWS(f_x.xorTerm(p), CVC4ApiException&);
 367   TS_ASSERT_THROWS(f_x.xorTerm(zero), CVC4ApiException&);
 368   TS_ASSERT_THROWS(f_x.xorTerm(f_x), CVC4ApiException&);
 369   Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
 370   TS_ASSERT_THROWS(sum.xorTerm(b), CVC4ApiException&);
 371   TS_ASSERT_THROWS(sum.xorTerm(x), CVC4ApiException&);
 372   TS_ASSERT_THROWS(sum.xorTerm(f), CVC4ApiException&);
 373   TS_ASSERT_THROWS(sum.xorTerm(p), CVC4ApiException&);
 374   TS_ASSERT_THROWS(sum.xorTerm(zero), CVC4ApiException&);
 375   TS_ASSERT_THROWS(sum.xorTerm(f_x), CVC4ApiException&);
 376   TS_ASSERT_THROWS(sum.xorTerm(sum), CVC4ApiException&);
 377   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
 378   TS_ASSERT_THROWS_NOTHING(p_0.xorTerm(b));
 379   TS_ASSERT_THROWS(p_0.xorTerm(x), CVC4ApiException&);
 380   TS_ASSERT_THROWS(p_0.xorTerm(f), CVC4ApiException&);
 381   TS_ASSERT_THROWS(p_0.xorTerm(p), CVC4ApiException&);
 382   TS_ASSERT_THROWS(p_0.xorTerm(zero), CVC4ApiException&);
 383   TS_ASSERT_THROWS(p_0.xorTerm(f_x), CVC4ApiException&);
 384   TS_ASSERT_THROWS(p_0.xorTerm(sum), CVC4ApiException&);
 385   TS_ASSERT_THROWS_NOTHING(p_0.xorTerm(p_0));
 386   Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
 387   TS_ASSERT_THROWS_NOTHING(p_f_x.xorTerm(b));
 388   TS_ASSERT_THROWS(p_f_x.xorTerm(x), CVC4ApiException&);
 389   TS_ASSERT_THROWS(p_f_x.xorTerm(f), CVC4ApiException&);
 390   TS_ASSERT_THROWS(p_f_x.xorTerm(p), CVC4ApiException&);
 391   TS_ASSERT_THROWS(p_f_x.xorTerm(zero), CVC4ApiException&);
 392   TS_ASSERT_THROWS(p_f_x.xorTerm(f_x), CVC4ApiException&);
 393   TS_ASSERT_THROWS(p_f_x.xorTerm(sum), CVC4ApiException&);
 394   TS_ASSERT_THROWS_NOTHING(p_f_x.xorTerm(p_0));
 395   TS_ASSERT_THROWS_NOTHING(p_f_x.xorTerm(p_f_x));
 396 }
 397
 398 void TermBlack::testEqTerm()
 399 {
 400   Sort bvSort = d_solver.mkBitVectorSort(8);
 401   Sort intSort = d_solver.getIntegerSort();
 402   Sort boolSort = d_solver.getBooleanSort();
 403   Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
 404   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 405
 406   Term b = d_solver.mkTrue();
 407   TS_ASSERT_THROWS(Term().eqTerm(b), CVC4ApiException&);
 408   TS_ASSERT_THROWS(b.eqTerm(Term()), CVC4ApiException&);
 409   TS_ASSERT_THROWS_NOTHING(b.eqTerm(b));
 410   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
 411   TS_ASSERT_THROWS(x.eqTerm(b), CVC4ApiException&);
 412   TS_ASSERT_THROWS_NOTHING(x.eqTerm(x));
 413   Term f = d_solver.mkVar(funSort1, "f");
 414   TS_ASSERT_THROWS(f.eqTerm(b), CVC4ApiException&);
 415   TS_ASSERT_THROWS(f.eqTerm(x), CVC4ApiException&);
 416   TS_ASSERT_THROWS_NOTHING(f.eqTerm(f));
 417   Term p = d_solver.mkVar(funSort2, "p");
 418   TS_ASSERT_THROWS(p.eqTerm(b), CVC4ApiException&);
 419   TS_ASSERT_THROWS(p.eqTerm(x), CVC4ApiException&);
 420   TS_ASSERT_THROWS(p.eqTerm(f), CVC4ApiException&);
 421   TS_ASSERT_THROWS_NOTHING(p.eqTerm(p));
 422   Term zero = d_solver.mkReal(0);
 423   TS_ASSERT_THROWS(zero.eqTerm(b), CVC4ApiException&);
 424   TS_ASSERT_THROWS(zero.eqTerm(x), CVC4ApiException&);
 425   TS_ASSERT_THROWS(zero.eqTerm(f), CVC4ApiException&);
 426   TS_ASSERT_THROWS(zero.eqTerm(p), CVC4ApiException&);
 427   TS_ASSERT_THROWS_NOTHING(zero.eqTerm(zero));
 428   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
 429   TS_ASSERT_THROWS(f_x.eqTerm(b), CVC4ApiException&);
 430   TS_ASSERT_THROWS(f_x.eqTerm(x), CVC4ApiException&);
 431   TS_ASSERT_THROWS(f_x.eqTerm(f), CVC4ApiException&);
 432   TS_ASSERT_THROWS(f_x.eqTerm(p), CVC4ApiException&);
 433   TS_ASSERT_THROWS_NOTHING(f_x.eqTerm(zero));
 434   TS_ASSERT_THROWS_NOTHING(f_x.eqTerm(f_x));
 435   Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
 436   TS_ASSERT_THROWS(sum.eqTerm(b), CVC4ApiException&);
 437   TS_ASSERT_THROWS(sum.eqTerm(x), CVC4ApiException&);
 438   TS_ASSERT_THROWS(sum.eqTerm(f), CVC4ApiException&);
 439   TS_ASSERT_THROWS(sum.eqTerm(p), CVC4ApiException&);
 440   TS_ASSERT_THROWS_NOTHING(sum.eqTerm(zero));
 441   TS_ASSERT_THROWS_NOTHING(sum.eqTerm(f_x));
 442   TS_ASSERT_THROWS_NOTHING(sum.eqTerm(sum));
 443   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
 444   TS_ASSERT_THROWS_NOTHING(p_0.eqTerm(b));
 445   TS_ASSERT_THROWS(p_0.eqTerm(x), CVC4ApiException&);
 446   TS_ASSERT_THROWS(p_0.eqTerm(f), CVC4ApiException&);
 447   TS_ASSERT_THROWS(p_0.eqTerm(p), CVC4ApiException&);
 448   TS_ASSERT_THROWS(p_0.eqTerm(zero), CVC4ApiException&);
 449   TS_ASSERT_THROWS(p_0.eqTerm(f_x), CVC4ApiException&);
 450   TS_ASSERT_THROWS(p_0.eqTerm(sum), CVC4ApiException&);
 451   TS_ASSERT_THROWS_NOTHING(p_0.eqTerm(p_0));
 452   Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
 453   TS_ASSERT_THROWS_NOTHING(p_f_x.eqTerm(b));
 454   TS_ASSERT_THROWS(p_f_x.eqTerm(x), CVC4ApiException&);
 455   TS_ASSERT_THROWS(p_f_x.eqTerm(f), CVC4ApiException&);
 456   TS_ASSERT_THROWS(p_f_x.eqTerm(p), CVC4ApiException&);
 457   TS_ASSERT_THROWS(p_f_x.eqTerm(zero), CVC4ApiException&);
 458   TS_ASSERT_THROWS(p_f_x.eqTerm(f_x), CVC4ApiException&);
 459   TS_ASSERT_THROWS(p_f_x.eqTerm(sum), CVC4ApiException&);
 460   TS_ASSERT_THROWS_NOTHING(p_f_x.eqTerm(p_0));
 461   TS_ASSERT_THROWS_NOTHING(p_f_x.eqTerm(p_f_x));
 462 }
 463
 464 void TermBlack::testImpTerm()
 465 {
 466   Sort bvSort = d_solver.mkBitVectorSort(8);
 467   Sort intSort = d_solver.getIntegerSort();
 468   Sort boolSort = d_solver.getBooleanSort();
 469   Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
 470   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 471
 472   Term b = d_solver.mkTrue();
 473   TS_ASSERT_THROWS(Term().impTerm(b), CVC4ApiException&);
 474   TS_ASSERT_THROWS(b.impTerm(Term()), CVC4ApiException&);
 475   TS_ASSERT_THROWS_NOTHING(b.impTerm(b));
 476   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
 477   TS_ASSERT_THROWS(x.impTerm(b), CVC4ApiException&);
 478   TS_ASSERT_THROWS(x.impTerm(x), CVC4ApiException&);
 479   Term f = d_solver.mkVar(funSort1, "f");
 480   TS_ASSERT_THROWS(f.impTerm(b), CVC4ApiException&);
 481   TS_ASSERT_THROWS(f.impTerm(x), CVC4ApiException&);
 482   TS_ASSERT_THROWS(f.impTerm(f), CVC4ApiException&);
 483   Term p = d_solver.mkVar(funSort2, "p");
 484   TS_ASSERT_THROWS(p.impTerm(b), CVC4ApiException&);
 485   TS_ASSERT_THROWS(p.impTerm(x), CVC4ApiException&);
 486   TS_ASSERT_THROWS(p.impTerm(f), CVC4ApiException&);
 487   TS_ASSERT_THROWS(p.impTerm(p), CVC4ApiException&);
 488   Term zero = d_solver.mkReal(0);
 489   TS_ASSERT_THROWS(zero.impTerm(b), CVC4ApiException&);
 490   TS_ASSERT_THROWS(zero.impTerm(x), CVC4ApiException&);
 491   TS_ASSERT_THROWS(zero.impTerm(f), CVC4ApiException&);
 492   TS_ASSERT_THROWS(zero.impTerm(p), CVC4ApiException&);
 493   TS_ASSERT_THROWS(zero.impTerm(zero), CVC4ApiException&);
 494   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
 495   TS_ASSERT_THROWS(f_x.impTerm(b), CVC4ApiException&);
 496   TS_ASSERT_THROWS(f_x.impTerm(x), CVC4ApiException&);
 497   TS_ASSERT_THROWS(f_x.impTerm(f), CVC4ApiException&);
 498   TS_ASSERT_THROWS(f_x.impTerm(p), CVC4ApiException&);
 499   TS_ASSERT_THROWS(f_x.impTerm(zero), CVC4ApiException&);
 500   TS_ASSERT_THROWS(f_x.impTerm(f_x), CVC4ApiException&);
 501   Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
 502   TS_ASSERT_THROWS(sum.impTerm(b), CVC4ApiException&);
 503   TS_ASSERT_THROWS(sum.impTerm(x), CVC4ApiException&);
 504   TS_ASSERT_THROWS(sum.impTerm(f), CVC4ApiException&);
 505   TS_ASSERT_THROWS(sum.impTerm(p), CVC4ApiException&);
 506   TS_ASSERT_THROWS(sum.impTerm(zero), CVC4ApiException&);
 507   TS_ASSERT_THROWS(sum.impTerm(f_x), CVC4ApiException&);
 508   TS_ASSERT_THROWS(sum.impTerm(sum), CVC4ApiException&);
 509   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
 510   TS_ASSERT_THROWS_NOTHING(p_0.impTerm(b));
 511   TS_ASSERT_THROWS(p_0.impTerm(x), CVC4ApiException&);
 512   TS_ASSERT_THROWS(p_0.impTerm(f), CVC4ApiException&);
 513   TS_ASSERT_THROWS(p_0.impTerm(p), CVC4ApiException&);
 514   TS_ASSERT_THROWS(p_0.impTerm(zero), CVC4ApiException&);
 515   TS_ASSERT_THROWS(p_0.impTerm(f_x), CVC4ApiException&);
 516   TS_ASSERT_THROWS(p_0.impTerm(sum), CVC4ApiException&);
 517   TS_ASSERT_THROWS_NOTHING(p_0.impTerm(p_0));
 518   Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
 519   TS_ASSERT_THROWS_NOTHING(p_f_x.impTerm(b));
 520   TS_ASSERT_THROWS(p_f_x.impTerm(x), CVC4ApiException&);
 521   TS_ASSERT_THROWS(p_f_x.impTerm(f), CVC4ApiException&);
 522   TS_ASSERT_THROWS(p_f_x.impTerm(p), CVC4ApiException&);
 523   TS_ASSERT_THROWS(p_f_x.impTerm(zero), CVC4ApiException&);
 524   TS_ASSERT_THROWS(p_f_x.impTerm(f_x), CVC4ApiException&);
 525   TS_ASSERT_THROWS(p_f_x.impTerm(sum), CVC4ApiException&);
 526   TS_ASSERT_THROWS_NOTHING(p_f_x.impTerm(p_0));
 527   TS_ASSERT_THROWS_NOTHING(p_f_x.impTerm(p_f_x));
 528 }
 529
 530 void TermBlack::testIteTerm()
 531 {
 532   Sort bvSort = d_solver.mkBitVectorSort(8);
 533   Sort intSort = d_solver.getIntegerSort();
 534   Sort boolSort = d_solver.getBooleanSort();
 535   Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
 536   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 537
 538   Term b = d_solver.mkTrue();
 539   TS_ASSERT_THROWS(Term().iteTerm(b, b), CVC4ApiException&);
 540   TS_ASSERT_THROWS(b.iteTerm(Term(), b), CVC4ApiException&);
 541   TS_ASSERT_THROWS(b.iteTerm(b, Term()), CVC4ApiException&);
 542   TS_ASSERT_THROWS_NOTHING(b.iteTerm(b, b));
 543   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
 544   TS_ASSERT_THROWS_NOTHING(b.iteTerm(x, x));
 545   TS_ASSERT_THROWS_NOTHING(b.iteTerm(b, b));
 546   TS_ASSERT_THROWS(b.iteTerm(x, b), CVC4ApiException&);
 547   TS_ASSERT_THROWS(x.iteTerm(x, x), CVC4ApiException&);
 548   TS_ASSERT_THROWS(x.iteTerm(x, b), CVC4ApiException&);
 549   Term f = d_solver.mkVar(funSort1, "f");
 550   TS_ASSERT_THROWS(f.iteTerm(b, b), CVC4ApiException&);
 551   TS_ASSERT_THROWS(x.iteTerm(b, x), CVC4ApiException&);
 552   Term p = d_solver.mkVar(funSort2, "p");
 553   TS_ASSERT_THROWS(p.iteTerm(b, b), CVC4ApiException&);
 554   TS_ASSERT_THROWS(p.iteTerm(x, b), CVC4ApiException&);
 555   Term zero = d_solver.mkReal(0);
 556   TS_ASSERT_THROWS(zero.iteTerm(x, x), CVC4ApiException&);
 557   TS_ASSERT_THROWS(zero.iteTerm(x, b), CVC4ApiException&);
 558   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
 559   TS_ASSERT_THROWS(f_x.iteTerm(b, b), CVC4ApiException&);
 560   TS_ASSERT_THROWS(f_x.iteTerm(b, x), CVC4ApiException&);
 561   Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
 562   TS_ASSERT_THROWS(sum.iteTerm(x, x), CVC4ApiException&);
 563   TS_ASSERT_THROWS(sum.iteTerm(b, x), CVC4ApiException&);
 564   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
 565   TS_ASSERT_THROWS_NOTHING(p_0.iteTerm(b, b));
 566   TS_ASSERT_THROWS_NOTHING(p_0.iteTerm(x, x));
 567   TS_ASSERT_THROWS(p_0.iteTerm(x, b), CVC4ApiException&);
 568   Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
 569   TS_ASSERT_THROWS_NOTHING(p_f_x.iteTerm(b, b));
 570   TS_ASSERT_THROWS_NOTHING(p_f_x.iteTerm(x, x));
 571   TS_ASSERT_THROWS(p_f_x.iteTerm(x, b), CVC4ApiException&);
 572 }
 573
 574 void TermBlack::testTermAssignment()
 575 {
 576   Term t1 = d_solver.mkReal(1);
 577   Term t2 = t1;
 578   t2 = d_solver.mkReal(2);
 579   TS_ASSERT_EQUALS(t1, d_solver.mkReal(1));
 580 }