test/system/cvc3_main.cpp

   1 /*********************                                                        */
   2 /*! \file cvc3_main.cpp
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009-2012  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Test of CVC3 compatibility interface
  13  **
  14  ** This is part of a test of the CVC3 compatibility interface present in
  15  ** CVC4.  It is a test copied from CVC3's "test" directory.  Only #includes
  16  ** were changed to support this test in CVC4.
  17  **
  18  ** The original file comment is preserved in the source.
  19  **/
  20
  21 ///////////////////////////////////////////////////////////////////////////////
  22 //                                                                           //
  23 // File: main.cpp                                                            //
  24 // Author: Clark Barrett                                                     //
  25 // Created: Sat Apr 19 01:47:47 2003                                         //
  26 //                                                                           //
  27 ///////////////////////////////////////////////////////////////////////////////
  28
  29
  30 #include "compat/cvc3_compat.h"
  31 //#include "vc.h"
  32 //#include "theory_arith.h" // for arith kinds and expressions
  33 //#include "theory_array.h"
  34 #include <fstream>
  35 #include <iostream>
  36 #include <string>
  37 #include <deque>
  38 //#include "exception.h"
  39 //#include "typecheck_exception.h"
  40 //#include "command_line_flags.h"
  41 //#include "debug.h"
  42 #include "cvc3_george.h"
  43
  44
  45 using namespace std;
  46 using namespace CVC3;
  47
  48 int exitStatus;
  49
  50 inline void __expect__(const std::string& file,
  51                        int line,
  52                        bool cond,
  53                        const std::string& cond_s,
  54                        const std::string& msg) {
  55   if(!cond) {
  56     std::cerr << file << ":" << line
  57               << ": Expected: (" << cond_s << "). "
  58               << msg << std::endl;
  59     exitStatus = 1;
  60   }
  61 }
  62
  63 #define EXPECT(cond, msg) __expect__(__FILE__, __LINE__, (cond), #cond, (msg))
  64
  65 // Check whether e is valid
  66 bool check(ValidityChecker* vc, Expr e, bool verbose=true)
  67 {
  68   if(verbose) {
  69     cout << "Query: ";
  70     vc->printExpr(e);
  71   }
  72   bool res = vc->query(e);
  73   switch (res) {
  74     case false:
  75       if(verbose) cout << "Invalid" << endl << endl;
  76       break;
  77     case true:
  78       if(verbose) cout << "Valid" << endl << endl;
  79       break;
  80   }
  81   return res;
  82 }
  83
  84
  85 // Make a new assertion
  86 void newAssertion(ValidityChecker* vc, Expr e)
  87 {
  88   cout << "Assert: ";
  89   vc->printExpr(e);
  90   vc->assertFormula(e);
  91 }
  92
  93 int eqExprVecs(const vector<Expr>& v1,
  94                 const vector<Expr>& v2) {
  95     if( v1.size() != v2.size() ) {
  96         return 0;
  97     }
  98
  99     for( unsigned int i=0; i < v1.size(); ++i ) {
 100         if( v1[i] != v2[i] ) {
 101             return 0;
 102         }
 103     }
 104
 105     return 1;
 106 }
 107
 108 int eqExprVecVecs(const vector<vector<Expr> > vv1,
 109                    const vector<vector<Expr> > vv2) {
 110     if( vv1.size() != vv2.size() ) {
 111         return 0;
 112     }
 113
 114     for( unsigned int i=0; i < vv1.size(); ++i ) {
 115         if( !eqExprVecs(vv1[i],vv2[i]) ) {
 116             return 0;
 117         }
 118     }
 119
 120     return 1;
 121 }
 122
 123
 124 void test ()
 125 {
 126    CLFlags flags = ValidityChecker::createFlags();
 127    ValidityChecker* vc = ValidityChecker::create(flags);
 128
 129    try {
 130      Type it (vc->intType ());                //int
 131      Op f = vc->createOp("f",vc->funType(it,it));
 132      Expr z = vc->varExpr("z",it);
 133      Expr e = vc->funExpr(f, vc->funExpr(f, z));
 134      e = e[0];
 135      Expr f2 = vc->funExpr(f, e);
 136      Expr f3 = vc->funExpr(f, f2);
 137
 138      EXPECT(e != f2 && e != f3, "Refcount problems");
 139
 140      Expr x (vc->boundVarExpr ("x", "0", it));//x0:int
 141      vector<Expr> xs;
 142      xs.push_back (x);                        //<x0:int>
 143      Op lxsx (vc->lambdaExpr (xs,x));       //\<x0:int>. x0:int
 144      Expr y (vc->ratExpr (1,1));              //1
 145      vector<Expr> ys;
 146      ys.push_back (y);                        //<1>
 147      Expr lxsxy = vc->funExpr (lxsx, y);      //(\<x0:int>. x0:int)1
 148      Expr lxsxys = vc->funExpr (lxsx, ys);  //(\<x0:int>. x0:int)<1>
 149      cout << "Lambda application: " << lxsxy << endl;
 150      cout << "Simplified: " << vc->simplify(lxsxy) << endl;
 151    } catch(const Exception& e) {
 152      exitStatus = 1;
 153      cout << "*** Exception caught in test (): \n" << e << endl;
 154    }
 155    delete vc;
 156 }
 157
 158 void test1()
 159 {
 160   CLFlags flags = ValidityChecker::createFlags();
 161   flags.setFlag("dagify-exprs",false);
 162   flags.setFlag("dump-log", ".test1.cvc");
 163   ValidityChecker* vc = ValidityChecker::create(flags);
 164
 165   // It is important that all Expr objects are deleted before vc is
 166   // deleted.  Therefore, we enclose them in a scope of try{ }catch
 167   // block.
 168   //
 169   // Also, vc methods may throw an Exception, and we want to delete vc
 170   // even in those exceptional cases.
 171   try {
 172
 173     bool b = check(vc, vc->trueExpr());
 174     EXPECT(b, "Should be valid");
 175
 176     vc->push();
 177     b = check(vc, vc->falseExpr());
 178     EXPECT(!b, "Should be invalid");
 179     vc->pop();
 180
 181     // Check p OR ~p
 182
 183     Expr p = vc->varExpr("p", vc->boolType());
 184     Expr e = vc->orExpr(p, vc->notExpr(p));
 185
 186     b = check(vc, e);
 187     EXPECT(b, "Should be valid");
 188
 189     // Check x = y -> f(x) = f(y)
 190
 191     Expr x = vc->varExpr("x", vc->realType());
 192     Expr y = vc->varExpr("y", vc->realType());
 193
 194     Type real2real = vc->funType(vc->realType(), vc->realType());
 195     Op f = vc->createOp("f", real2real);
 196     Expr fx = vc->funExpr(f, x);
 197     Expr fy = vc->funExpr(f, y);
 198
 199     e = vc->impliesExpr(vc->eqExpr(x,y),vc->eqExpr(fx, fy));
 200     b = check(vc, e);
 201     EXPECT(b, "Should be valid");
 202
 203     // Check f(x) = f(y) -> x = y
 204
 205     e = vc->impliesExpr(vc->eqExpr(fx,fy),vc->eqExpr(x, y));
 206     int scopeLevel = vc->scopeLevel();
 207     vc->push();
 208     b = check(vc, e);
 209     EXPECT(!b, "Should be invalid");
 210
 211     // Get counter-example
 212
 213     vector<Expr> assertions;
 214     cout << "Scope level: " << vc->scopeLevel() << endl;
 215     cout << "Counter-example:" << endl;
 216     //vc->getCounterExample(assertions);
 217     for (unsigned i = 0; i < assertions.size(); ++i) {
 218       vc->printExpr(assertions[i]);
 219     }
 220     cout << "End of counter-example" << endl << endl;
 221
 222     // Reset to initial scope
 223     cout << "Resetting" << endl;
 224     vc->pop();
 225     EXPECT(scopeLevel == vc->scopeLevel(), "scope error");
 226     cout << "Scope level: " << vc->scopeLevel() << endl << endl;
 227
 228     // Check w = x & x = y & y = z & f(x) = f(y) & x = 1 & z = 2
 229
 230     Expr w = vc->varExpr("w", vc->realType());
 231     Expr z = vc->varExpr("z", vc->realType());
 232
 233     cout << "Push Scope" << endl << endl;
 234     vc->push();
 235
 236     newAssertion(vc, vc->eqExpr(w, x));
 237     newAssertion(vc, vc->eqExpr(x, y));
 238     newAssertion(vc, vc->eqExpr(y, z));
 239     newAssertion(vc, vc->eqExpr(fx, fy));
 240     newAssertion(vc, vc->eqExpr(x, vc->ratExpr(1)));
 241
 242     cout << endl << "simplify(w) = ";
 243     vc->printExpr(vc->simplify(w));
 244     cout << endl;
 245     EXPECT(vc->simplify(w)==vc->ratExpr(1), "Expected simplify(w) = 1");
 246
 247     newAssertion(vc, vc->eqExpr(z, vc->ratExpr(2)));
 248     assertions.clear();
 249     cout << "Inconsistent?: " << vc->inconsistent(assertions) << endl;
 250
 251     cout << "Assumptions Used:" << endl;
 252     for (unsigned i = 0; i < assertions.size(); ++i) {
 253       vc->printExpr(assertions[i]);
 254     }
 255
 256     cout << endl << "Pop Scope" << endl << endl;
 257     vc->pop();
 258
 259     cout << "simplify(w) = ";
 260     vc->printExpr(vc->simplify(w));
 261     EXPECT(vc->simplify(w)==w, "Expected simplify(w) = w");
 262     cout << endl;
 263
 264     assertions.clear();
 265     cout << "Inconsistent?: " << vc->inconsistent(assertions) << endl;
 266   } catch(const Exception& e) {
 267     exitStatus = 1;
 268     cout << "*** Exception caught in test1(): \n" << e << endl;
 269   }
 270   delete vc;
 271 }
 272
 273
 274 void test2()
 275 {
 276   CLFlags flags = ValidityChecker::createFlags();
 277   flags.setFlag("dagify-exprs",false);
 278   ValidityChecker* vc = ValidityChecker::create(flags);
 279
 280   try {
 281
 282     Expr bexpr = vc->varExpr("b", vc->intType());
 283     vc->assertFormula(vc->ltExpr(bexpr, vc->ratExpr(10)));
 284
 285     Expr c = vc->varExpr("c", vc->intType());
 286     vc->assertFormula(c.eqExpr(vc->ratExpr(0)) || c.eqExpr(vc->ratExpr(1)));
 287
 288     bool b = check(vc, vc->leExpr(bexpr, vc->ratExpr(10)));
 289     EXPECT(b, "Should be valid");
 290
 291     b = check(vc, vc->falseExpr());
 292     EXPECT(!b, "Should be invalid");
 293     vc->returnFromCheck();
 294
 295     // Check x = y -> g(x,y) = g(y,x)
 296
 297     Expr x = vc->varExpr("x", vc->realType());
 298     Expr y = vc->varExpr("y", vc->realType());
 299
 300     Type real = vc->realType();
 301     vector<Type> RxR;
 302     RxR.push_back(real);
 303     RxR.push_back(real);
 304
 305     Type realxreal2real = vc->funType(RxR, real);
 306     Op g = vc->createOp("g", realxreal2real);
 307
 308     Expr gxy = vc->funExpr(g, x, y);
 309     Expr gyx = vc->funExpr(g, y, x);
 310
 311     Expr e = vc->impliesExpr(vc->eqExpr(x,y),vc->eqExpr(gxy, gyx));
 312     b = check(vc, e);
 313     EXPECT(b, "Should be valid");
 314
 315     Op h = vc->createOp("h", realxreal2real);
 316
 317     Expr hxy = vc->funExpr(h, x, y);
 318     Expr hyx = vc->funExpr(h, y, x);
 319
 320     e = vc->impliesExpr(vc->eqExpr(x,y),vc->eqExpr(hxy, hyx));
 321     b = check(vc, e);
 322     EXPECT(b, "Should be valid");
 323
 324   } catch(const Exception& e) {
 325     exitStatus = 1;
 326     cout << "*** Exception caught in test2(): \n" << e << endl;
 327   }
 328
 329   delete vc;
 330 }
 331
 332
 333 Expr ltLex(ValidityChecker* vc, Expr i1, Expr i2, Expr j1, Expr j2)
 334 {
 335   Expr res = vc->ltExpr(i1, j1);
 336   return vc->orExpr(res, vc->andExpr(vc->eqExpr(i1, j1), vc->ltExpr(i2, j2)));
 337 }
 338
 339
 340 Expr createTestFormula(ValidityChecker* vc, Expr i1, Expr i2, Expr r1, Expr r2)
 341 {
 342   Expr lt1 = ltLex(vc, r1, r2, i1, i2);
 343   Expr lt2 = ltLex(vc, i2, i1, r2, r1);
 344   return vc->andExpr(lt1, lt2);
 345 }
 346
 347
 348 void test3()
 349 {
 350   CLFlags flags = ValidityChecker::createFlags();
 351   flags.setFlag("dagify-exprs",false);
 352   ValidityChecker* vc = ValidityChecker::create(flags);
 353
 354   try {
 355     Expr i = vc->varExpr("i", vc->realType());
 356     Expr j = vc->varExpr("j", vc->realType());
 357     Expr k = vc->varExpr("k", vc->realType());
 358
 359     Expr one = vc->ratExpr(1);
 360
 361     cout << "i: " << i.getIndex() << endl;
 362
 363     Expr test = createTestFormula(vc, i, j,
 364                                   vc->minusExpr(i, one), vc->minusExpr(j, k));
 365
 366     cout << "Trying test: ";
 367     vc->printExpr(test);
 368     cout << endl;
 369
 370     vc->push();
 371     bool result = vc->query(test);
 372     if (result) {
 373       cout << "Test Valid" << endl;
 374       vc->pop();
 375     }
 376     else {
 377       Expr condition;
 378       vector<Expr> assertions;
 379       unsigned index;
 380
 381       //vc->getCounterExample(assertions);
 382
 383       cout << "Test Invalid Under Conditions:" << endl;
 384       for (index = 0; index < assertions.size(); ++index) {
 385         vc->printExpr(assertions[index]);
 386       }
 387
 388       // Try assertions one by one
 389       for (index = 0; index < assertions.size(); ++index) {
 390         condition = vc->notExpr(assertions[index]);
 391         cout << "Trying test under condition: ";
 392         vc->printExpr(condition);
 393         cout << endl;
 394         vc->pop();
 395         vc->push();
 396         result = vc->query(vc->impliesExpr(condition, test));
 397         if (result) {
 398           cout << "Result Valid" << endl;
 399           break;
 400         }
 401         else {
 402           cout << "Result Invalid" << endl;
 403         }
 404       }
 405     }
 406   } catch(const Exception& e) {
 407     exitStatus = 1;
 408     cout << "*** Exception caught in test3(): \n" << e << endl;
 409   }
 410   delete vc;
 411 }
 412
 413
 414 void test4()
 415 {
 416   CLFlags flags = ValidityChecker::createFlags();
 417   flags.setFlag("dagify-exprs",false);
 418   ValidityChecker* vc = ValidityChecker::create(flags);
 419
 420   try {
 421   Expr i = vc->varExpr("i", vc->realType());
 422   Expr j = vc->varExpr("j", vc->realType());
 423   Expr k = vc->varExpr("k", vc->realType());
 424
 425   Expr one = vc->ratExpr(1);
 426
 427   cout << "i: " << i.getIndex() << endl;
 428
 429   Expr test = createTestFormula(vc, i, j,
 430                                 vc->minusExpr(i, one), vc->minusExpr(j, k));
 431
 432   cout << "Trying test: ";
 433   vc->printExpr(test);
 434   cout << endl;
 435
 436   vc->push();
 437   bool result = vc->query(test);
 438   if (result) {
 439     cout << "Test Valid" << endl;
 440   }
 441   else {
 442     Expr condition;
 443     vector<Expr> assertions;
 444     unsigned index;
 445
 446     //vc->getCounterExample(assertions);
 447
 448     cout << "Test Invalid Under Conditions:" << endl;
 449     for (index = 0; index < assertions.size(); ++index) {
 450       vc->printExpr(assertions[index]);
 451     }
 452
 453     // Try assertions one by one
 454     for (index = 0; index < assertions.size(); ++index) {
 455       condition = vc->notExpr(assertions[index]);
 456       cout << "Trying test under condition: ";
 457       vc->printExpr(condition);
 458       cout << endl;
 459       vc->pop();
 460       vc->push();
 461       result = vc->query(vc->impliesExpr(condition, test));
 462       if (result) {
 463         cout << "Result Valid" << endl;
 464         break;
 465       }
 466       else {
 467         cout << "Result Invalid" << endl;
 468       }
 469     }
 470   }
 471   } catch(const Exception& e) {
 472     exitStatus = 1;
 473     cout << "*** Exception caught in test4(): \n" << e << endl;
 474   }
 475   delete vc;
 476 }
 477
 478
 479 void findLeaves(Expr e, vector<Expr>& l)
 480 {
 481   int ar = e.arity();
 482   if (ar > 0) {
 483     for (int i = 0; i < ar; ++i)
 484       findLeaves(e[i], l);
 485     return;
 486   }
 487   l.push_back(e);
 488 }
 489
 490
 491 bool hasij(Expr e, Expr i, Expr j)
 492 {
 493   int ar = e.arity();
 494   if (ar > 0) {
 495     for (int k = 0; k < ar; ++k)
 496       if (hasij(e[k], i, j)) return true;
 497     return false;
 498   }
 499   if (e == i || e == j) return true;
 500   return false;
 501 }
 502
 503
 504 Expr plusExpr(ValidityChecker* vc, vector<Expr>& kids)
 505 {
 506   if (kids.size() == 0) return vc->ratExpr(0);
 507   else if (kids.size() == 1) return kids[0];
 508   else if (kids.size() == 2) return vc->plusExpr(kids[0], kids[1]);
 509   else {
 510     Expr r = kids.back();
 511     kids.pop_back();
 512     return vc->plusExpr(plusExpr(vc, kids), r);
 513   }
 514 }
 515
 516
 517 void test5()
 518 {
 519   CLFlags flags = ValidityChecker::createFlags();
 520   flags.setFlag("dagify-exprs",false);
 521   flags.setFlag("dump-log", ".test5.cvc");
 522   ValidityChecker* vc = ValidityChecker::create(flags);
 523
 524   try {
 525   Expr i = vc->varExpr("i1", vc->realType());
 526   Expr j = vc->varExpr("i2", vc->realType());
 527   Expr p = vc->varExpr("p", vc->realType());
 528   Expr q = vc->varExpr("q", vc->realType());
 529   Expr r = vc->varExpr("r", vc->realType());
 530   Expr a = vc->varExpr("arb_addr", vc->realType());
 531   Expr N = vc->varExpr("N", vc->realType());
 532
 533   Expr M = vc->varExpr("M", vc->arrayType(vc->realType(), vc->realType()));
 534
 535   Expr M2 = vc->writeExpr(M, vc->plusExpr(q, i), vc->readExpr(M, vc->plusExpr(r, i)));
 536
 537   Expr M1 = vc->writeExpr(M, vc->plusExpr(p, j), vc->readExpr(M, vc->plusExpr(r, j)));
 538
 539   Expr e = vc->eqExpr(vc->readExpr(vc->writeExpr(M2, vc->plusExpr(p, j), vc->readExpr(M2, vc->plusExpr(r, j))), a),
 540                       vc->readExpr(vc->writeExpr(M1, vc->plusExpr(q, i), vc->readExpr(M1, vc->plusExpr(r, i))), a));
 541
 542   Expr one = vc->ratExpr(1);
 543   Expr zero = vc->ratExpr(0);
 544
 545   Expr qmp = vc->minusExpr(q, p);
 546   Expr qmr = vc->minusExpr(q, r);
 547
 548   vector<Expr> hyp;
 549   hyp.push_back(vc->ltExpr(i, j));
 550 //   hyp.push_back(vc->orExpr(vc->geExpr(qmp, N), vc->leExpr(qmp, zero)));
 551 //   hyp.push_back(vc->orExpr(vc->geExpr(qmr, N), vc->leExpr(qmr, zero)));
 552
 553   Expr test = vc->impliesExpr(vc->andExpr(hyp), e);
 554   Expr query;
 555
 556   cout << "Checking verification condition:" << endl;
 557   vc->printExpr(test);
 558   cout << endl;
 559
 560   vc->push();
 561   bool result = vc->query(test);
 562   if (result) {
 563     cout << "Valid" << endl;
 564   }
 565   else {
 566     vector<Expr> conditions;
 567     vector<Expr> assertions;
 568     unsigned index, index2;
 569     int req;
 570     vector<Expr> leaves;
 571
 572     //vc->getCounterExample(assertions);
 573
 574     cout << "Invalid Under Conditions:" << endl;
 575     for (index = 0; index < assertions.size(); ++index) {
 576       if (assertions[index] == (!test)) {
 577         for (; index < assertions.size()-1; ++index) {
 578           assertions[index] = assertions[index+1];
 579         }
 580         assertions.pop_back();
 581         break;
 582       }
 583     }
 584     for (index = 0; index < assertions.size(); ++index) {
 585       vc->printExpr(assertions[index]);
 586     }
 587
 588     cout << endl;
 589
 590     // Try assertions one by one
 591     for (index = 0; index < assertions.size(); ++index) {
 592       e = assertions[index];
 593
 594       // Check condition for eligibility
 595       if (e.isNot()) {
 596         cout << "Condition ineligible: negation" << endl;
 597         vc->printExpr(e);
 598         cout << endl;
 599         continue;
 600       }
 601       if (e.isEq()) {
 602         req = 2;
 603       }
 604       else req = 1;
 605
 606       leaves.clear();
 607       findLeaves(e, leaves);
 608       for (index2 = 0; index2 < leaves.size(); ++index2) {
 609         if (!leaves[index2].isVar() ||
 610             leaves[index2] == i ||
 611             leaves[index2] == j ||
 612             leaves[index2] == a)
 613           continue;
 614         req--;
 615       }
 616       if (req > 0) {
 617         cout << "Condition ineligible: not enough non-loop variables" << endl;
 618         vc->printExpr(e);
 619         cout << endl;
 620         continue;
 621       }
 622
 623       cout << "Condition selected:" << endl;
 624       vc->printExpr(e);
 625       cout << endl << endl;
 626
 627       conditions.push_back(vc->notExpr(e));
 628       cout << "Trying verification condition with hypothesis:" << endl;
 629       vc->printExpr(vc->andExpr(conditions));
 630       cout << endl;
 631       vc->pop();
 632       vc->push();
 633       query = vc->impliesExpr(vc->andExpr(conditions), test);
 634       result = vc->query(query);
 635       if (result) {
 636         cout << "Result Valid" << endl;
 637         break;
 638       }
 639       else {
 640         assertions.clear();
 641         vc->getCounterExample(assertions);
 642
 643         cout << "Invalid Under Conditions:" << endl;
 644         for (index2 = 0; index2 < assertions.size(); ++index2) {
 645           if (assertions[index2] == (!query)) {
 646             for (; index2 < assertions.size()-1; ++index2) {
 647               assertions[index2] = assertions[index2+1];
 648             }
 649             assertions.pop_back();
 650             break;
 651           }
 652         }
 653
 654         for (index2 = 0; index2 < assertions.size(); ++index2) {
 655           vc->printExpr(assertions[index2]);
 656         }
 657         cout << endl;
 658         index = (unsigned)-1;
 659       }
 660     }
 661
 662     cout << endl << "Attempting to remove loop variables" << endl;
 663     // replace loop variables in conditions
 664     vector<Expr> newConditions;
 665     vector<Expr> newPlus;
 666     bool foundi, foundj, negi, negj;
 667     Expr minusone = vc->ratExpr(-1);
 668     for (index = 0; index < conditions.size(); ++index) {
 669       if (conditions[index][0].isEq()) {
 670         e = vc->simplify(vc->minusExpr(conditions[index][0][0], conditions[index][0][1]));
 671         if (hasij(e, i, j)) {
 672           if (e.getKind() == CVC3::PLUS) {
 673             newPlus.clear();
 674             newPlus.push_back(e[0]);
 675             foundi = foundj = negi = negj = false;
 676             for (index2 = 1; index2 < (unsigned)e.arity(); index2++) {
 677               Expr term = e[index2];
 678               if (term == i && !foundi) foundi = true;
 679               else if (term == j && !foundj) {
 680                 foundj = true;
 681                 negj = true;
 682               }
 683               else if (term.getKind() == CVC3::MULT && term[0] == minusone && term[1] == i && !foundi) {
 684                 foundi = true;
 685                 negi = true;
 686               }
 687               else if (term.getKind() == CVC3::MULT && term[0] == minusone && term[1] == j && !foundj) foundj = true;
 688               else newPlus.push_back(term);
 689             }
 690             if (foundi && foundj && ((negi && negj) || (!negi && !negj))) {
 691               e = plusExpr(vc, newPlus);
 692               if (negi && negj) e = vc->uminusExpr(e);
 693               e = vc->simplify(e);
 694               if (!hasij(e, i, j)) {
 695                 newConditions.push_back(vc->orExpr(vc->geExpr(e, N), vc->leExpr(e, zero)));
 696                 continue;
 697               }
 698             }
 699           }
 700           cout << "Unable to remove loop variables:" << endl;
 701           vc->printExpr(e);
 702           break;
 703         }
 704       }
 705       newConditions.push_back(conditions[index]);
 706     }
 707     if (index == conditions.size()) {
 708       cout << "Loop variables successfully removed:" << endl;
 709       Expr cond = (newConditions.size()>0)?
 710         vc->andExpr(newConditions) : vc->trueExpr();
 711       vc->printExpr(cond);
 712       cout << endl;
 713
 714       vector<Expr> loopConditions;
 715       loopConditions.push_back(cond);
 716       loopConditions.push_back(vc->geExpr(i, one));
 717       loopConditions.push_back(vc->geExpr(j, one));
 718       loopConditions.push_back(vc->leExpr(i, N));
 719       loopConditions.push_back(vc->leExpr(j, N));
 720       vc->pop();
 721       vc->push();
 722       cout << "Final query" << endl;
 723       result = vc->query(vc->impliesExpr(vc->andExpr(loopConditions), test));
 724       if (result) {
 725         cout << "Result Valid" << endl;
 726       }
 727       else {
 728         cout << "Result Invalid" << endl;
 729       }
 730     }
 731   }
 732   } catch(const Exception& e) {
 733     exitStatus = 1;
 734     cout << "*** Exception caught in test5(): \n" << e << endl;
 735   }
 736   delete vc;
 737 }
 738
 739 //#include "debug.h"
 740
 741 // Test importing of Exprs from a different validity checker
 742 void test6() {
 743   ValidityChecker* vc1 = ValidityChecker::create();
 744   ValidityChecker* vc2 = ValidityChecker::create();
 745
 746   try {
 747     Type real1 = vc1->realType();
 748
 749     Expr x1 = vc1->varExpr("x", real1);
 750     Expr y1 = vc1->boundVarExpr("y", "0", real1);
 751
 752     cout << "vc1 variables: " << x1 << ", " << y1 << endl;
 753
 754     Expr x2 = vc2->varExpr("x", vc2->importType(real1));
 755     Expr y2 = vc2->boundVarExpr("y", "0", vc2->realType());
 756
 757     cout << "vc2 variables: " << x2 << ", " << y2 << endl;
 758     cout << "vars imported to vc2 from vc1: "
 759          << vc2->importExpr(x1) << ", " << vc2->importExpr(y1) << endl;
 760     Expr t1 = vc1->trueExpr();
 761     Expr and1 = vc1->andExpr(t1, vc1->falseExpr());
 762     Op f1 = vc1->createOp("f", vc1->funType(real1, real1));
 763     Expr fx1 = vc1->funExpr(f1, x1);
 764     Expr f5_1 = vc1->funExpr(f1, vc1->ratExpr(5,1));
 765     Type rt1 = vc1->recordType("foo", real1, "bar", real1);
 766     Expr r1 = vc1->recordExpr("foo", fx1, "bar", f5_1);
 767     Expr r1_eq = vc1->eqExpr(r1, vc1->recUpdateExpr(r1, "foo", f5_1));
 768     Type art1 = vc1->arrayType(real1, rt1);
 769     Expr ar1 = vc1->varExpr("ar", art1);
 770     Expr ar_eq1 = vc1->eqExpr(vc1->writeExpr(ar1, x1, r1), ar1);
 771     Expr query1 = vc1->eqExpr(vc1->recSelectExpr(vc1->readExpr(ar1, x1), "foo"),
 772                               vc1->recSelectExpr(r1, "bar"));
 773
 774     cout << "*** VC #1:" << endl;
 775     newAssertion(vc1, r1_eq);
 776     newAssertion(vc1, ar_eq1);
 777     check(vc1, query1);
 778
 779     cout << "*** VC #2:" << endl;
 780     newAssertion(vc2, vc2->importExpr(r1_eq));
 781     newAssertion(vc2, vc2->importExpr(ar_eq1));
 782     check(vc2, vc2->importExpr(query1));
 783   } catch(const Exception& e) {
 784     exitStatus = 1;
 785     cout << "*** Exception caught in test6(): \n" << e << endl;
 786   }
 787   delete vc1;
 788   delete vc2;
 789 }
 790
 791
 792 void test7() {
 793   ValidityChecker* vc1 = ValidityChecker::create();
 794   ValidityChecker* vc2 = ValidityChecker::create();
 795   try {
 796     Expr e1 = vc1->varExpr("e1", vc1->realType());
 797     Expr e2 = vc2->varExpr("e2", vc2->realType());
 798     newAssertion(vc2, vc2->eqExpr(vc2->importExpr(e1), e2));
 799   } catch(const Exception& e) {
 800     exitStatus = 1;
 801     cout << "*** Exception caught in test7(): \n" << e << endl;
 802   }
 803   delete vc1;
 804   delete vc2;
 805 }
 806
 807
 808 void test8() {
 809   ValidityChecker* vc = ValidityChecker::create();
 810   try {
 811     vector<Expr> vec;
 812     vec.push_back(vc->boundVarExpr("x", "x", vc->realType()));
 813     Expr lambda = vc->lambdaExpr(vec, vc->falseExpr()).getExpr();
 814     Expr witness;
 815     try {
 816       Type t = vc->subtypeType(lambda, witness);
 817       EXPECT(false, "Typechecking exception expected");
 818     } catch(const TypecheckException&) {
 819       // fall through
 820     }
 821   } catch(const Exception& e) {
 822     exitStatus = 1;
 823     cout << "*** Exception caught in test8(): \n" << e << endl;
 824   }
 825   delete vc;
 826 }
 827
 828
 829 Expr adder(ValidityChecker* vc, const Expr& a, const Expr& b, const Expr& c)
 830 {
 831   return vc->notExpr(vc->iffExpr(vc->notExpr(vc->iffExpr(a,b)),c));
 832 }
 833
 834
 835 Expr carry(ValidityChecker* vc, const Expr& a, const Expr& b, const Expr& c)
 836 {
 837   return vc->orExpr(vc->andExpr(a,b), vc->orExpr(vc->andExpr(b,c),vc->andExpr(a,c)));
 838 }
 839
 840
 841 void add(ValidityChecker* vc, vector<Expr> a, vector<Expr> b, vector<Expr>& sum)
 842 {
 843   int i,N=a.size();
 844   Expr c = vc->falseExpr();
 845
 846   for (i=0; i < N; i++)
 847   {
 848     sum.push_back(adder(vc,a[i],b[i],c));
 849     c = carry(vc,a[i],b[i],c);
 850   }
 851 }
 852
 853
 854 Expr vectorEq(ValidityChecker* vc, vector<Expr> a, vector<Expr> b)
 855 {
 856   int i, N=a.size();
 857   Expr result = vc->trueExpr();
 858
 859   for (i=0; i < N; i++) {
 860     result = result && a[i].iffExpr(b[i]);
 861   }
 862   return result;
 863 }
 864
 865
 866 void test9(int N) {
 867   CLFlags flags = ValidityChecker::createFlags();
 868   //  flags.setFlag("proofs",true);
 869   ValidityChecker* vc = ValidityChecker::create(flags);
 870
 871   try {
 872   int i;
 873   vector<Expr> a,b,sum1,sum2;
 874
 875   for (i=0; i < N; i++) {
 876     a.push_back(vc->varExpr("a" + int2string(i), vc->boolType()));
 877     b.push_back(vc->varExpr("b" + int2string(i), vc->boolType()));
 878   }
 879
 880   add(vc,a,b,sum1);
 881   add(vc,b,a,sum2);
 882
 883   Expr q = vectorEq(vc,sum1,sum2);
 884
 885   check(vc, q);
 886
 887   //  Proof p = vc->getProof();
 888
 889   } catch(const Exception& e) {
 890     exitStatus = 1;
 891     cout << "*** Exception caught in test9(): \n" << e << endl;
 892   }
 893   delete vc;
 894 }
 895
 896
 897 Expr bvadder(ValidityChecker* vc, const Expr& a, const Expr& b, const Expr& c)
 898 {
 899   return vc->newBVXorExpr(a, vc->newBVXorExpr(b, c));
 900 }
 901
 902
 903 Expr bvcarry(ValidityChecker* vc, const Expr& a, const Expr& b, const Expr& c)
 904 {
 905   return vc->newBVOrExpr(vc->newBVAndExpr(a,b), vc->newBVOrExpr(vc->newBVAndExpr(b,c),vc->newBVAndExpr(a,c)));
 906 }
 907
 908
 909 void bvadd(ValidityChecker* vc, vector<Expr> a, vector<Expr> b, vector<Expr>& sum)
 910 {
 911   int i,N=a.size();
 912   Expr c = vc->newBVConstExpr(Rational(0), 1);
 913
 914   for (i=0; i < N; i++)
 915   {
 916     sum.push_back(bvadder(vc,a[i],b[i],c));
 917     c = bvcarry(vc,a[i],b[i],c);
 918   }
 919 }
 920
 921
 922 Expr bvvectorEq(ValidityChecker* vc, vector<Expr> a, vector<Expr> b)
 923 {
 924   int i, N=a.size();
 925   Expr result = vc->newBVConstExpr(string("1"));
 926
 927   for (i=0; i < N; i++) {
 928     result = vc->newBVAndExpr(result, vc->newBVXnorExpr(a[i], b[i]));
 929   }
 930   return result;
 931 }
 932
 933
 934 void bvtest9(int N) {
 935   CLFlags flags = ValidityChecker::createFlags();
 936   ValidityChecker* vc = ValidityChecker::create(flags);
 937
 938   try {
 939   int i;
 940   vector<Expr> avec,bvec,sum1vec,sum2;
 941
 942   Expr a, b, sum1;
 943   a = vc->varExpr("a", vc->bitvecType(N));
 944   b = vc->varExpr("b", vc->bitvecType(N));
 945   vector<Expr> kids;
 946   kids.push_back(a);
 947   kids.push_back(b);
 948   sum1 = vc->newBVPlusExpr(N, kids);
 949
 950   for (i=0; i < N; i++) {
 951     avec.push_back(vc->newBVExtractExpr(a, i, i));
 952     bvec.push_back(vc->newBVExtractExpr(b, i, i));
 953     sum1vec.push_back(vc->newBVExtractExpr(sum1, i, i));
 954   }
 955
 956   bvadd(vc,avec,bvec,sum2);
 957
 958   Expr q = bvvectorEq(vc,sum1vec,sum2);
 959
 960   check(vc, vc->eqExpr(q,vc->newBVConstExpr(string("1"))));
 961
 962   } catch(const Exception& e) {
 963     exitStatus = 1;
 964     cout << "*** Exception caught in bvtest9(): \n" << e << endl;
 965   }
 966   delete vc;
 967 }
 968
 969
 970 // Test for memory leaks (run silently)
 971 void test10()
 972 {
 973   CLFlags flags = ValidityChecker::createFlags();
 974   ValidityChecker* vc = ValidityChecker::create(flags);
 975
 976   // Create all expressions in a separate scope, so that they are
 977   // destroyed before vc is deleted.
 978
 979   try {
 980     //  Check x = y -> g(x,y) = g(y,x)
 981
 982     Expr x = vc->varExpr("x", vc->realType());
 983     Expr y = vc->varExpr("y", vc->realType());
 984
 985     Type real = vc->realType();
 986     vector<Type> RxR;
 987     RxR.push_back(real);
 988     RxR.push_back(real);
 989
 990     Type realxreal2real = vc->funType(RxR, real);
 991     Op g = vc->createOp("g", realxreal2real);
 992
 993     Expr gxy = vc->funExpr(g, x, y);
 994     Expr gyx = vc->funExpr(g, y, x);
 995
 996     Expr e = vc->impliesExpr(vc->eqExpr(x,y),vc->eqExpr(gxy, gyx));
 997     check(vc, e, false);
 998
 999     Op h = vc->createOp("h", realxreal2real);
1000
1001     Expr hxy = vc->funExpr(h, x, y);
1002     Expr hyx = vc->funExpr(h, y, x);
1003
1004     e = vc->impliesExpr(vc->eqExpr(x,y),vc->eqExpr(hxy, hyx));
1005     check(vc, e, false);
1006
1007   } catch(const Exception& e) {
1008     exitStatus = 1;
1009     cout << "*** Exception caught in test10(): \n" << e << endl;
1010   }
1011   // Make sure all Expr's are deleted first
1012   delete vc;
1013 }
1014
1015 unsigned int printImpliedLiterals(ValidityChecker* vc)
1016 {
1017   unsigned int count = 0;
1018   cout << "Implied Literals:" << endl;
1019   Expr impLit = vc->getImpliedLiteral();
1020   while (!impLit.isNull()) {
1021     ++count;
1022     vc->printExpr(impLit);
1023     impLit = vc->getImpliedLiteral();
1024   }
1025   return count;
1026 }
1027
1028
1029 void test11()
1030 {
1031   CLFlags flags = ValidityChecker::createFlags();
1032   ValidityChecker* vc = ValidityChecker::create(flags);
1033
1034   try {
1035     Expr x = vc->varExpr("x", vc->realType());
1036     Expr y = vc->varExpr("y", vc->realType());
1037     Expr z = vc->varExpr("z", vc->realType());
1038
1039     Type real = vc->realType();
1040     Type real2real = vc->funType(real, real);
1041     Type real2bool = vc->funType(real, vc->boolType());
1042     Op f = vc->createOp("f", real2real);
1043     Op p = vc->createOp("p", real2bool);
1044
1045     Expr fx = vc->funExpr(f, x);
1046     Expr fy = vc->funExpr(f, y);
1047
1048     Expr px = vc->funExpr(p, x);
1049     Expr py = vc->funExpr(p, y);
1050
1051     Expr xeqy = vc->eqExpr(x, y);
1052     Expr yeqx = vc->eqExpr(y, x);
1053     Expr xeqz = vc->eqExpr(x, z);
1054     Expr zeqx = vc->eqExpr(z, x);
1055     Expr yeqz = vc->eqExpr(y, z);
1056     Expr zeqy = vc->eqExpr(z, y);
1057
1058     unsigned int c;
1059
1060     vc->registerAtom(vc->eqExpr(x,vc->ratExpr(0,1)));
1061     vc->registerAtom(xeqy);
1062     vc->registerAtom(yeqx);
1063     vc->registerAtom(xeqz);
1064     vc->registerAtom(zeqx);
1065     vc->registerAtom(yeqz);
1066     vc->registerAtom(zeqy);
1067     vc->registerAtom(px);
1068     vc->registerAtom(py);
1069     vc->registerAtom(vc->eqExpr(fx, fy));
1070
1071     cout << "Push" << endl;
1072     vc->push();
1073
1074     cout << "Assert x = y" << endl;
1075     vc->assertFormula(xeqy);
1076     c = printImpliedLiterals(vc);
1077     EXPECT(c==3,"Implied literal error 0");
1078
1079     cout << "Push" << endl;
1080     vc->push();
1081     cout << "Assert x /= z" << endl;
1082     vc->assertFormula(!xeqz);
1083     c = printImpliedLiterals(vc);
1084     EXPECT(c==4,"Implied literal error 1");
1085     cout << "Pop" << endl;
1086     vc->pop();
1087
1088     cout << "Push" << endl;
1089     vc->push();
1090     cout << "Assert y /= z" << endl;
1091     vc->assertFormula(!yeqz);
1092     c = printImpliedLiterals(vc);
1093     EXPECT(c==4,"Implied literal error 2");
1094     cout << "Pop" << endl;
1095     vc->pop();
1096
1097     cout << "Push" << endl;
1098     vc->push();
1099     cout << "Assert p(x)" << endl;
1100     vc->assertFormula(px);
1101     c = printImpliedLiterals(vc);
1102     EXPECT(c==2,"Implied literal error 3");
1103     cout << "Pop" << endl;
1104     vc->pop();
1105
1106     cout << "Push" << endl;
1107     vc->push();
1108     cout << "Assert p(y)" << endl;
1109     vc->assertFormula(py);
1110     c = printImpliedLiterals(vc);
1111     EXPECT(c==2,"Implied literal error 4");
1112     cout << "Pop" << endl;
1113     vc->pop();
1114
1115     cout << "Pop" << endl;
1116     vc->pop();
1117
1118     cout << "Push" << endl;
1119     vc->push();
1120     cout << "Assert y = x" << endl;
1121     vc->assertFormula(yeqx);
1122     c = printImpliedLiterals(vc);
1123     EXPECT(c==3,"Implied literal error 5");
1124     cout << "Pop" << endl;
1125     vc->pop();
1126
1127     cout << "Push" << endl;
1128     vc->push();
1129     cout << "Assert p(x)" << endl;
1130     vc->assertFormula(px);
1131     c = printImpliedLiterals(vc);
1132     EXPECT(c==1,"Implied literal error 6");
1133     cout << "Assert x = y" << endl;
1134     vc->assertFormula(xeqy);
1135     c = printImpliedLiterals(vc);
1136     EXPECT(c==4,"Implied literal error 7");
1137     cout << "Pop" << endl;
1138     vc->pop();
1139
1140     cout << "Push" << endl;
1141     vc->push();
1142     cout << "Assert NOT p(x)" << endl;
1143     vc->assertFormula(!px);
1144     c = printImpliedLiterals(vc);
1145     EXPECT(c==1,"Implied literal error 8");
1146     cout << "Assert x = y" << endl;
1147     vc->assertFormula(xeqy);
1148     c = printImpliedLiterals(vc);
1149     EXPECT(c==4,"Implied literal error 9");
1150     cout << "Pop" << endl;
1151     vc->pop();
1152
1153   } catch(const Exception& e) {
1154     exitStatus = 1;
1155     cout << "*** Exception caught in test11(): \n" << e << endl;
1156   }
1157   delete vc;
1158 }
1159
1160
1161 void test12()
1162 {
1163   ValidityChecker * vc = ValidityChecker::create( );
1164   try {
1165     Type realType = vc->realType();
1166     Type intType = vc->intType();
1167     Type boolType = vc->boolType();
1168     vc -> push();
1169     int initial_layer = vc->stackLevel();
1170     int initial_scope = vc->scopeLevel();
1171     Expr exprObj_trueID = vc->trueExpr();
1172     Expr exprObj_falseID = vc->notExpr(vc->trueExpr());
1173     vc->popto(initial_layer);
1174     EXPECT(vc->scopeLevel() == initial_scope, "Expected no change");
1175     EXPECT(vc->stackLevel() == initial_layer, "Expected no change");
1176     // TODO: what happens if we push and then popscope?
1177   } catch(const Exception& e) {
1178     exitStatus = 1;
1179     cout << "*** Exception caught in test12(): \n" << e << endl;
1180   }
1181   delete vc;
1182 }
1183
1184
1185 void test13()
1186 {
1187   CLFlags flags = ValidityChecker::createFlags();
1188   flags.setFlag("dagify-exprs", false);
1189   flags.setFlag("dump-log", ".test13.cvc");
1190   ValidityChecker* vc = ValidityChecker::create(flags);
1191   try {
1192     Expr rat_one = vc->ratExpr(1);
1193     Expr rat_two = vc->ratExpr(2);
1194     Expr rat_minus_one = vc->ratExpr(-1);
1195
1196     bool query_result;
1197     query_result = vc->query(vc->eqExpr(rat_two,rat_one));
1198     cout << "2=1 " << query_result << endl;
1199     query_result = vc->query(vc->eqExpr(rat_two,rat_minus_one));
1200     cout << "2=-1 " << query_result << endl;
1201   } catch(const Exception& e) {
1202     exitStatus = 1;
1203     cout << "*** Exception caught in test13(): \n" << e << endl;
1204   }
1205   delete vc;
1206 }
1207
1208
1209 Expr func1(ValidityChecker *vc)  {
1210  // local Expr 'tmp'
1211  Expr tmp = vc->varExpr("tmp", vc->boolType());
1212  return vc->trueExpr();
1213 }
1214
1215
1216 void test14()  {
1217   ValidityChecker *vc = ValidityChecker::create();
1218   try {
1219     // func call: ok
1220     Expr test1 = func1(vc);
1221
1222     // func call: fail
1223     Expr test2 = func1(vc);
1224   } catch(const Exception& e) {
1225     exitStatus = 1;
1226     cout << "*** Exception caught in test14(): \n" << e << endl;
1227   }
1228   delete vc;
1229 }
1230
1231
1232 void test15() {
1233   CLFlags flags = ValidityChecker::createFlags();
1234   flags.setFlag("dagify-exprs", false);
1235   ValidityChecker *vc = ValidityChecker::create(flags);
1236   try {
1237
1238   /*****************************************************
1239    *          array declaration                        *
1240    *****************************************************/
1241
1242   // array: index type
1243   Type index_type = vc->subrangeType(vc->ratExpr(0),
1244                                      vc->ratExpr(3));
1245   // array: data type
1246   Type data_type = vc->subrangeType(vc->ratExpr(0),
1247                                     vc->ratExpr(3));
1248   // array type: [0 .. 3] of 0 .. 3
1249   Type array_type = vc->arrayType(index_type, data_type);
1250   Expr arr = vc->varExpr("array", array_type);
1251
1252   // array: [1,1,0,0]
1253   arr = vc->writeExpr(arr, vc->ratExpr(0), vc->ratExpr(1));
1254   arr = vc->writeExpr(arr, vc->ratExpr(1), vc->ratExpr(1));
1255   arr = vc->writeExpr(arr, vc->ratExpr(2), vc->ratExpr(0));
1256   arr = vc->writeExpr(arr, vc->ratExpr(3), vc->ratExpr(0));
1257
1258
1259
1260   /*****************************************************
1261    *             forall Expr                           *
1262    *****************************************************/
1263
1264   // for loop: index
1265   Expr id = vc->boundVarExpr("id", "0", vc->subrangeType(vc->ratExpr(0),
1266                                                          vc->ratExpr(2)));
1267   vector<Expr> vars;
1268   vars.push_back(id);
1269
1270   // for loop: body
1271   Expr for_body = vc->leExpr(vc->readExpr(arr, id),
1272                              vc->readExpr(arr, vc->plusExpr(id, vc->ratExpr(1))));
1273   // forall expr
1274   Expr forall_expr = vc->forallExpr(vars, for_body);
1275
1276   vc->push();
1277   check(vc, forall_expr);
1278
1279   vector<Expr> assertions;
1280   cout << "Scope level: " << vc->scopeLevel() << endl;
1281   cout << "Counter-example:" << endl;
1282   //vc->getCounterExample(assertions);
1283   for (unsigned i = 0; i < assertions.size(); ++i) {
1284     vc->printExpr(assertions[i]);
1285   }
1286   cout << "End of counter-example" << endl << endl;
1287   vc->pop();
1288
1289   /*****************************************************
1290    *            manual expansion                       *
1291    *****************************************************/
1292
1293   Expr e1 = vc->leExpr(vc->readExpr(arr, vc->ratExpr(0)),
1294                        vc->readExpr(arr, vc->ratExpr(1)));
1295   Expr e2 = vc->leExpr(vc->readExpr(arr, vc->ratExpr(1)),
1296                        vc->readExpr(arr, vc->ratExpr(2)));
1297   Expr e3 = vc->leExpr(vc->readExpr(arr, vc->ratExpr(2)),
1298                        vc->readExpr(arr, vc->ratExpr(3)));
1299   Expr manual_expr = vc->andExpr(e1, vc->andExpr(e2, e3));
1300
1301
1302
1303   /*****************************************************
1304    *            exists Expr                            *
1305    *****************************************************/
1306
1307   // exists: index
1308   Expr id_ex = vc->varExpr("id_ex", vc->subrangeType(vc->ratExpr(0),
1309                                                      vc->ratExpr(2)));
1310   vector<Expr> vars_ex;
1311   vars_ex.push_back(id_ex);
1312
1313   // exists: body
1314   Expr ex_body = vc->gtExpr(vc->readExpr(arr, id_ex),
1315                             vc->readExpr(arr, vc->plusExpr(id_ex, vc->ratExpr(1))));
1316   // exists expr
1317   Expr ex_expr = vc->existsExpr(vars_ex, ex_body);
1318
1319
1320
1321
1322   /*****************************************************
1323    *            ???     forall <==> manual expansion   *
1324    *****************************************************/
1325
1326   cout << endl << "Checking forallExpr <==> manual expansion ..." << endl;
1327   if (vc->query(vc->iffExpr(forall_expr, manual_expr)))
1328     cout << "   -- yes." << endl;
1329   else {
1330     cout << "   -- no, with counter examples as " << endl;
1331
1332     vector<Expr> assert1;
1333     vc->getCounterExample(assert1);
1334     for (unsigned int i = 0; i < assert1.size(); i ++)
1335       vc->printExpr(assert1[i]);
1336
1337   }
1338   cout << endl;
1339
1340
1341
1342   /*****************************************************
1343    *            ???     !forall <==> existsExpr        *
1344    *****************************************************/
1345   cout << endl << "Checking !forallExpr <==> existsExpr ..." << endl;
1346   if (vc->query(vc->iffExpr(vc->notExpr(forall_expr), ex_expr)))
1347     cout << "   -- yes." << endl;
1348   else if (vc->incomplete()) {
1349     cout << "   -- incomplete:" << endl;
1350     vector<string> reasons;
1351     vc->incomplete(reasons);
1352     for (unsigned int i = 0; i < reasons.size(); ++i)
1353       cout << reasons[i] << endl;
1354   }
1355   else {
1356     cout << "   -- no, with counter examples as " << endl;
1357
1358     vector<Expr> assert2;
1359     //vc->getCounterExample(assert2);
1360     for (unsigned int i = 0; i < assert2.size(); i ++)
1361       vc->printExpr(assert2[i]);
1362   }
1363
1364   cout << endl << "End of testcases." << endl << endl;
1365
1366
1367   } catch(const Exception& e) {
1368     exitStatus = 1;
1369     cout << "*** Exception caught in test15(): \n" << e << endl;
1370   }
1371   delete vc;
1372 }
1373
1374
1375 void test16()  {
1376   ValidityChecker *vc = ValidityChecker::create();
1377   try {
1378     Type zto100 = vc->subrangeType(vc->ratExpr(0), vc->ratExpr(100));
1379     Expr mem = vc->varExpr("mem", vc->arrayType(zto100, vc->intType()));
1380     Expr a = vc->varExpr("a", zto100);
1381     Expr b = vc->varExpr("b", zto100);
1382
1383     Expr lhs = vc->readExpr(vc->writeExpr(mem, a, vc->ratExpr(30)), b);
1384     Expr rhs = vc->readExpr(vc->writeExpr(mem, b, vc->ratExpr(40)), a);
1385
1386     Expr q = vc->impliesExpr(vc->notExpr(vc->eqExpr(a, b)), vc->eqExpr(lhs, rhs));
1387
1388     check(vc, q);
1389
1390     vector<Expr> assertions;
1391     cout << "Scope level: " << vc->scopeLevel() << endl;
1392     cout << "Counter-example:" << endl;
1393     vc->getCounterExample(assertions);
1394     EXPECT(assertions.size() > 0, "Expected non-empty counter-example");
1395     for (unsigned i = 0; i < assertions.size(); ++i) {
1396       vc->printExpr(assertions[i]);
1397     }
1398     cout << "End of counter-example" << endl << endl;
1399
1400     ExprMap<Expr> m;
1401     vc->getConcreteModel(m);
1402     ExprMap<Expr>::iterator it = m.begin(), end = m.end();
1403     if(it == end)
1404       cout << " Did not find concrete model for any vars" << endl;
1405     else {
1406       cout << "%Satisfiable  Variable Assignment: % \n";
1407       for(; it!= end; it++) {
1408         Expr eq;
1409         if(it->first.getType().isBool()) {
1410           EXPECT((it->second).isBoolConst(),
1411                       "Bad variable assignement: e = "+(it->first).toString()
1412                       +"\n\n val = "+(it->second).toString());
1413           if((it->second).isTrue())
1414             eq = it->first;
1415           else
1416             eq = !(it->first);
1417         }
1418         else
1419           eq = (it->first).eqExpr(it->second);
1420         //cout << Expr(ASSERT,  eq) << "\n";
1421       }
1422     }
1423
1424   } catch(const Exception& e) {
1425     exitStatus = 1;
1426     cout << "*** Exception caught in test16(): \n" << e << endl;
1427   }
1428   delete vc;
1429 }
1430
1431
1432 void test17()  {
1433   ValidityChecker *vc = ValidityChecker::create();
1434   try {
1435     try {
1436       vector<string> selectors;
1437       vector<Expr> types;
1438
1439       selectors.push_back("car");
1440       types.push_back(vc->intType().getExpr());
1441       selectors.push_back("cdr");
1442       types.push_back(vc->stringExpr("list"));
1443
1444       Type badList = vc->dataType("list", "cons", selectors, types);
1445       EXPECT(false, "Typechecking exception expected");
1446     } catch(const TypecheckException&) {
1447       // fall through
1448     }
1449     delete vc;
1450     vc = ValidityChecker::create();
1451     {
1452       vector<string> constructors;
1453       vector<vector<string> > selectors(2);
1454       vector<vector<Expr> > types(2);
1455
1456       constructors.push_back("cons");
1457       selectors[0].push_back("car");
1458       types[0].push_back(vc->intType().getExpr());
1459       selectors[0].push_back("cdr");
1460       types[0].push_back(vc->stringExpr("list"));
1461       constructors.push_back("null");
1462
1463       Type list = vc->dataType("list", constructors, selectors, types);
1464
1465       Expr x = vc->varExpr("x", vc->intType());
1466       Expr y = vc->varExpr("y", list);
1467
1468       vector<Expr> args;
1469       args.push_back(x);
1470       args.push_back(y);
1471       Expr cons = vc->datatypeConsExpr("cons", args);
1472
1473       Expr sel = vc->datatypeSelExpr("car", cons);
1474       bool b = check(vc, vc->eqExpr(sel, x));
1475       EXPECT(b, "Should be valid");
1476
1477     }
1478     delete vc;
1479     vc = ValidityChecker::create();
1480     try {
1481       vector<string> names;
1482       vector<vector<string> > constructors(2);
1483       vector<vector<vector<string> > > selectors(2);
1484       vector<vector<vector<Expr> > > types(2);
1485       vector<Type> returnTypes;
1486
1487       names.push_back("list1");
1488
1489       selectors[0].resize(1);
1490       types[0].resize(1);
1491       constructors[0].push_back("cons1");
1492       selectors[0][0].push_back("car1");
1493       types[0][0].push_back(vc->intType().getExpr());
1494       selectors[0][0].push_back("cdr1");
1495       types[0][0].push_back(vc->stringExpr("list2"));
1496
1497       names.push_back("list2");
1498
1499       selectors[1].resize(1);
1500       types[1].resize(1);
1501       constructors[1].push_back("cons2");
1502       selectors[0][0].push_back("car2");
1503       types[0][0].push_back(vc->intType().getExpr());
1504       selectors[0][0].push_back("cdr2");
1505       types[0][0].push_back(vc->stringExpr("list1"));
1506
1507       vc->dataType(names, constructors, selectors, types, returnTypes);
1508       EXPECT(false, "Typechecking exception expected");
1509     } catch(const TypecheckException&) {
1510       // fall through
1511     }
1512     delete vc;
1513     vc = ValidityChecker::create();
1514     {
1515       vector<string> names;
1516       vector<vector<string> > constructors(2);
1517       vector<vector<vector<string> > > selectors(2);
1518       vector<vector<vector<Expr> > > types(2);
1519       vector<Type> returnTypes;
1520
1521       names.push_back("list1");
1522
1523       selectors[0].resize(1);
1524       types[0].resize(1);
1525       constructors[0].push_back("cons1");
1526       selectors[0][0].push_back("car1");
1527       types[0][0].push_back(vc->intType().getExpr());
1528       selectors[0][0].push_back("cdr1");
1529       types[0][0].push_back(vc->stringExpr("list2"));
1530
1531       names.push_back("list2");
1532
1533       selectors[1].resize(2);
1534       types[1].resize(2);
1535       constructors[1].push_back("cons2");
1536       selectors[1][0].push_back("car2");
1537       types[1][0].push_back(vc->intType().getExpr());
1538       selectors[1][0].push_back("cdr2");
1539       types[1][0].push_back(vc->stringExpr("list1"));
1540       constructors[1].push_back("null");
1541
1542       vc->dataType(names, constructors, selectors, types, returnTypes);
1543
1544       Type list1 = returnTypes[0];
1545       Type list2 = returnTypes[1];
1546
1547       Expr x = vc->varExpr("x", vc->intType());
1548       Expr y = vc->varExpr("y", list2);
1549       Expr z = vc->varExpr("z", list1);
1550
1551       vector<Expr> args;
1552       args.push_back(x);
1553       args.push_back(y);
1554       Expr cons1 = vc->datatypeConsExpr("cons1", args);
1555
1556       Expr isnull = vc->datatypeTestExpr("null", y);
1557       Expr hyp = vc->andExpr(vc->eqExpr(z, cons1), isnull);
1558
1559       args.clear();
1560       Expr null = vc->datatypeConsExpr("null", args);
1561
1562       args.push_back(x);
1563       args.push_back(null);
1564       Expr cons1_2 = vc->datatypeConsExpr("cons1", args);
1565
1566       bool b = check(vc, vc->impliesExpr(hyp, vc->eqExpr(z, cons1_2)));
1567       EXPECT(b, "Should be valid");
1568
1569     }
1570     delete vc;
1571     vc = ValidityChecker::create();
1572     {
1573       vector<string> constructors;
1574       vector<vector<string> > selectors(2);
1575       vector<vector<Expr> > types(2);
1576
1577       constructors.push_back("A");
1578       constructors.push_back("B");
1579
1580       Type two = vc->dataType("two", constructors, selectors, types);
1581
1582       Expr x = vc->varExpr("x", two);
1583       Expr y = vc->varExpr("y", two);
1584       Expr z = vc->varExpr("z", two);
1585
1586       vector<Expr> args;
1587       args.push_back(!vc->eqExpr(x,y));
1588       args.push_back(!vc->eqExpr(y,z));
1589       args.push_back(!vc->eqExpr(x,z));
1590
1591       bool b = check(vc, !vc->andExpr(args));
1592       EXPECT(b, "Should be valid");
1593
1594     }
1595   } catch(const Exception& e) {
1596     exitStatus = 1;
1597     cout << "*** Exception caught in test17(): \n" << e << endl;
1598   }
1599   delete vc;
1600 }
1601
1602
1603 void test18()
1604 {
1605   CLFlags flags = ValidityChecker::createFlags();
1606   flags.setFlag("tcc", true);
1607   ValidityChecker *vc = ValidityChecker::create(flags);
1608   try {
1609     vector<string> names;
1610     vector<vector<string> > constructors(3);
1611     vector<vector<vector<string> > > selectors(3);
1612     vector<vector<vector<Expr> > > types(3);
1613     vector<Type> returnTypes;
1614
1615     names.push_back("nat");
1616
1617     selectors[0].resize(2);
1618     types[0].resize(2);
1619     constructors[0].push_back("zero");
1620     constructors[0].push_back("succ");
1621     selectors[0][1].push_back("pred");
1622     types[0][1].push_back(vc->stringExpr("nat"));
1623
1624     names.push_back("list");
1625
1626     selectors[1].resize(2);
1627     types[1].resize(2);
1628     constructors[1].push_back("cons");
1629     selectors[1][0].push_back("car");
1630     types[1][0].push_back(vc->stringExpr("tree"));
1631     selectors[1][0].push_back("cdr");
1632     types[1][0].push_back(vc->stringExpr("list"));
1633     constructors[1].push_back("null");
1634
1635     names.push_back("tree");
1636
1637     selectors[2].resize(2);
1638     types[2].resize(2);
1639     constructors[2].push_back("leaf");
1640     constructors[2].push_back("node");
1641     selectors[2][1].push_back("data");
1642     types[2][1].push_back(vc->stringExpr("nat"));
1643     selectors[2][1].push_back("children");
1644     types[2][1].push_back(vc->stringExpr("list"));
1645
1646     vc->dataType(names, constructors, selectors, types, returnTypes);
1647
1648     Type nat = returnTypes[0];
1649     Type listType = returnTypes[1];
1650     Type tree = returnTypes[2];
1651
1652     Expr x = vc->varExpr("x", nat);
1653
1654     vector<Expr> args;
1655     Expr zero = vc->datatypeConsExpr("zero", args);
1656     Expr null = vc->datatypeConsExpr("null", args);
1657     Expr leaf = vc->datatypeConsExpr("leaf", args);
1658
1659     vc->push();
1660     try {
1661       check(vc, vc->notExpr(vc->eqExpr(zero, null)));
1662       // TCCs not supported by CVC4 yet
1663       //EXPECT(false, "Should have caught tcc exception");
1664     } catch(const TypecheckException&) { }
1665
1666     vc->pop();
1667     args.push_back(vc->datatypeSelExpr("pred",x));
1668     Expr spx = vc->datatypeConsExpr("succ", args);
1669     Expr spxeqx = vc->eqExpr(spx, x);
1670     vc->push();
1671     try {
1672       check(vc, spxeqx);
1673       // TCCs not supported by CVC4 yet
1674       //EXPECT(false, "Should have caught tcc exception");
1675     } catch(const TypecheckException&) { }
1676
1677     vc->pop();
1678     bool b = check(vc, vc->impliesExpr(vc->datatypeTestExpr("succ", x), spxeqx));
1679     EXPECT(b, "Should be valid");
1680
1681     b = check(vc, vc->orExpr(vc->datatypeTestExpr("zero", x),
1682                              vc->datatypeTestExpr("succ", x)));
1683     EXPECT(b, "Should be valid");
1684
1685     Expr y = vc->varExpr("y", nat);
1686     Expr xeqy = vc->eqExpr(x, y);
1687     args.clear();
1688     args.push_back(x);
1689     Expr sx = vc->datatypeConsExpr("succ", args);
1690     args.clear();
1691     args.push_back(y);
1692     Expr sy = vc->datatypeConsExpr("succ", args);
1693     Expr sxeqsy = vc->eqExpr(sx,sy);
1694     b = check(vc, vc->impliesExpr(xeqy, sxeqsy));
1695     EXPECT(b, "Should be valid");
1696
1697     b = check(vc, vc->notExpr(vc->eqExpr(sx, zero)));
1698     EXPECT(b, "Should be valid");
1699
1700     b = check(vc, vc->impliesExpr(sxeqsy, xeqy));
1701     EXPECT(b, "Should be valid");
1702
1703     b = check(vc, vc->notExpr(vc->eqExpr(sx, x)));
1704     EXPECT(b, "Should be valid");
1705
1706   } catch(const Exception& e) {
1707     exitStatus = 1;
1708     cout << "*** Exception caught in test18(): \n" << e << endl;
1709   }
1710   delete vc;
1711 }
1712
1713 void test19()
1714 {
1715   CVC3::CLFlags flags = CVC3::ValidityChecker::createFlags();
1716   flags.setFlag("dagify-exprs", false);
1717   CVC3::ValidityChecker* vc = CVC3::ValidityChecker::create(flags);
1718   try {
1719     CVC3::Type RealType=(vc->realType());
1720     CVC3::Type IntType=(vc->intType());
1721     CVC3::Type BoolType=(vc->boolType());
1722     CVC3::Type PtrType=(RealType);
1723     CVC3::Type HeapType=(vc->arrayType(PtrType, RealType));
1724
1725     // -----------------
1726     //ASSERT(FORALL (CVCi: REAL): (Hs[CVCi] = Ht[CVCi]));
1727     //QUERY(Hs[(t6 + (3 * 1))] = Ht[(t6 + (3 * 1))]);
1728     CVC3::Expr Ad = vc->boundVarExpr("CVCi", "CVCi", RealType);
1729     CVC3::Expr Hs = vc->varExpr("Hs", HeapType);
1730     CVC3::Expr Ht = vc->varExpr("Ht", HeapType);
1731     CVC3::Expr t6 = vc->varExpr("t6", RealType);
1732
1733     vector<CVC3::Expr> Vars;
1734     Vars.push_back(Ad);
1735     // Body= (Hs[Ad] = Ht[Ad])
1736     CVC3::Expr Body = vc->eqExpr(vc->readExpr(Hs, Ad), vc->readExpr(Ht, Ad));
1737
1738     //A = forall (~i:REAL): Body
1739     CVC3::Expr A = vc->forallExpr(Vars, Body);
1740
1741     // Q = (Hs[t6] = Ht[t6])
1742     CVC3::Expr Q = vc->eqExpr(vc->readExpr(Hs, t6), vc->readExpr(Ht, t6));
1743
1744     // ----------- CHECK A -> Q
1745     vc->push();
1746
1747     vc->assertFormula(A);
1748
1749     cout<<"Checking formula "<<Q<<"\n in context "<<A<<"\n";
1750
1751     bool Succ = vc->query(Q);
1752
1753     EXPECT(Succ, "Expected valid formula");
1754
1755   } catch(const Exception& e) {
1756     exitStatus = 1;
1757     cout << "*** Exception caught in test19(): \n" << e << endl;
1758   }
1759   delete vc;
1760 }
1761
1762
1763 void test20()  {
1764   ValidityChecker *vc = ValidityChecker::create();
1765   try {
1766     vector<string> names;
1767     vector<vector<string> > constructors(3);
1768     vector<vector<vector<string> > > selectors(3);
1769     vector<vector<vector<Expr> > > types(3);
1770     vector<Type> returnTypes;
1771
1772     names.push_back("pair");
1773
1774     selectors[0].resize(1);
1775     types[0].resize(1);
1776     constructors[0].push_back("p");
1777     selectors[0][0].push_back("p1");
1778     types[0][0].push_back(vc->stringExpr("t1"));
1779     selectors[0][0].push_back("p2");
1780     types[0][0].push_back(vc->stringExpr("t2"));
1781
1782     names.push_back("t1");
1783
1784     selectors[1].resize(5);
1785     types[1].resize(5);
1786     constructors[1].push_back("a");
1787     constructors[1].push_back("b");
1788     constructors[1].push_back("c");
1789     constructors[1].push_back("d");
1790     constructors[1].push_back("e");
1791
1792     names.push_back("t2");
1793
1794     selectors[2].resize(1);
1795     types[2].resize(1);
1796     constructors[2].push_back("cons");
1797     selectors[2][0].push_back("s0");
1798     types[2][0].push_back(vc->bitvecType(2).getExpr());
1799     selectors[2][0].push_back("s1");
1800     types[2][0].push_back(vc->arrayType(vc->intType(), vc->subrangeType(vc->ratExpr(0), vc->ratExpr(0))).getExpr());
1801
1802     vc->dataType(names, constructors, selectors, types, returnTypes);
1803
1804     EXPECT(returnTypes[0].card() == CARD_FINITE, "Expected finite");
1805     Unsigned size = returnTypes[0].sizeFinite();
1806     Unsigned i = 0;
1807     for (; i < size; ++i) {
1808       cout << i << ": ";
1809       vc->printExpr(returnTypes[0].enumerateFinite(i));
1810     }
1811
1812   } catch(const Exception& e) {
1813     exitStatus = 1;
1814     cout << "*** Exception caught in test20(): \n" << e << endl;
1815   }
1816   delete vc;
1817 }
1818
1819 void test21()  {
1820   ValidityChecker *vc = ValidityChecker::create();
1821
1822   try {
1823     Type t = vc->realType();
1824
1825     Expr x1 = vc->varExpr("x",t);
1826
1827     Expr x2 = vc->exprFromString("x");
1828     cout << "x1: " << x1;
1829     cout << "\nx2: " << x2;
1830     EXPECT(x1 == x2, "Expected x1 == x2");
1831
1832     Expr x3 = vc->exprFromString("x", SMTLIB_V2_LANG);
1833     cout << "\nx3: " << x3;
1834     EXPECT(x1 == x3, "Expected x1 == x3");
1835
1836     Expr y1 = vc->varExpr("y",t);
1837     Expr y2 = vc->exprFromString("y");
1838     cout << "\ny1: " << y1;
1839     cout << "\ny2: " << y2;
1840     EXPECT(y1 == y2, "Expected y1 == y2");
1841
1842     Expr y3 = vc->exprFromString("y", SMTLIB_V2_LANG);
1843     cout << "\ny3: " << y3;
1844     EXPECT(y1 == y3, "Expected y1 == y3");
1845
1846     Expr a1 = vc->gtExpr(x1,vc->ratExpr(0,1));
1847     Expr a2 = vc->exprFromString("x > 0");
1848     cout << "\na1: " << a1;
1849     cout << "\na2: " << a2;
1850     EXPECT(a1 == a2, "Expected a1 == a2");
1851
1852     Expr a3 = vc->exprFromString("(> x 0)", SMTLIB_V2_LANG);
1853     cout << "\na3: " << a3;
1854     EXPECT(a1 == a3, "Expected a1 == a3");
1855
1856     Expr b1 = vc->ltExpr(x1,y1);
1857     Expr b2 = vc->exprFromString ("x < y");
1858     cout << "\nb1: " << b1;
1859     cout << "\nb2: " << b2;
1860     EXPECT(b1 == b2, "Expected b1 == b2");
1861
1862     Expr b3 = vc->exprFromString ("(< x y)", SMTLIB_V2_LANG);
1863     cout << "\nb3: " << b3;
1864     EXPECT(b1 == b3, "Expected b1 == b3");
1865
1866     Expr e1 = a1 && b1;
1867     Expr e2 = vc->exprFromString("x > 0 AND x < y");
1868     cout << "\ne1: " << e1;
1869     cout << "\ne2: " << e2;
1870     EXPECT(e1 == e2, "Expected e1 == e2");
1871
1872     Expr e3 = vc->exprFromString("(and (> x 0) (< x y))", SMTLIB_V2_LANG);
1873     cout << "\ne3: " << e3;
1874     EXPECT(e1 == e3, "Expected e1 == e3");
1875   } catch(const Exception& e) {
1876     exitStatus = 1;
1877     cout << "*** Exception caught in test21(): \n" << e << endl;
1878   }
1879   delete vc;
1880 }
1881
1882 void test22() {
1883   CLFlags flags = ValidityChecker::createFlags();
1884   ValidityChecker* vc = ValidityChecker::create(flags);
1885
1886   try {
1887     Type intType(vc->intType());
1888     Type fType(vc->funType(intType,intType));
1889
1890     Op f(vc->createOp("f",fType));
1891     Expr x(vc->varExpr("x",intType));
1892     Expr fx(vc->exprFromString("f(x)"));
1893
1894     Expr p(vc->exprFromString("FORALL (x:INT) : x < f(x)"));
1895
1896     vector<vector<Expr> > patternvv;
1897     vector<Expr> patternv;
1898     patternv.push_back(fx);
1899     patternvv.push_back(patternv);
1900
1901     vc->setTriggers(p,patternv);
1902     EXPECT( eqExprVecVecs(p.getTriggers(), patternvv),
1903                  "Expected p.getTriggers() == patternvv: " + p.toString() );
1904
1905     vc->setTriggers(p,patternvv);
1906
1907     EXPECT( eqExprVecVecs(p.getTriggers(), patternvv),
1908                  "Expected p.getTriggers() == patternvv: " + p.toString() );
1909
1910     // [chris 10/4/2009] Not sure why, but this fails
1911
1912     // Expr q(vc->exprFromString("FORALL (x:INT) : PATTERN (f(x)) : x < f(x)"));
1913
1914     // EXPECT( eqExprVecVecs(q.getTriggers(), patternvv),
1915     //              "Expected q.getTriggers() == patternvv"  + q.toString());
1916
1917     vector<Expr> vars;
1918     vars.push_back(x);
1919     Expr r(vc->forallExpr( vars, vc->ltExpr(x,fx), patternvv ));
1920
1921     EXPECT( eqExprVecVecs(r.getTriggers(), patternvv),
1922                  "Expected r.getTriggers() == patternvv: " + r.toString() );
1923
1924     Expr s(vc->exprFromString("FORALL (x:INT) : x > f(x)"));
1925     vc->setTrigger(s,fx);
1926
1927     std::vector<std::vector<Expr> > trigsvv = s.getTriggers();
1928     EXPECT( trigsvv.size() == 1,
1929                  "Expected s.getTriggers().size() == 1: " + trigsvv.size() );
1930
1931     std::vector<Expr> trigsv = trigsvv[0];
1932     EXPECT( trigsv.size() == 1,
1933                  "Expected s.getTriggers()[0].size() == 1: "
1934                  + trigsv.size() );
1935
1936     EXPECT( trigsv[0] == fx,
1937                  "Expected s.getTriggers()[0][0] == fx: "
1938                  + (trigsv[0].toString()) );
1939
1940     Expr t(vc->exprFromString("FORALL (x:INT) : x > f(x)"));
1941     vc->setMultiTrigger(t,patternv);
1942     trigsvv = t.getTriggers();
1943     EXPECT( trigsvv.size() == 1,
1944                  "Expected t.getTriggers().size() == 1: " + trigsvv.size() );
1945
1946     trigsv = trigsvv[0];
1947     EXPECT( trigsv.size() == 1,
1948                  "Expected t.getTriggers()[0].size() == 1: "
1949                  + trigsv.size() );
1950
1951     EXPECT( trigsv[0] == fx,
1952                  "Expected t.getTriggers()[0][0] == fx: "
1953                  + (trigsv[0].toString()) );
1954   } catch(const Exception& e) {
1955     exitStatus = 1;
1956     cout << "*** Exception caught in test22(): \n" << e << endl;
1957   }
1958   delete vc;
1959 }
1960
1961 void test23() {
1962   CLFlags flags = ValidityChecker::createFlags();
1963   ValidityChecker* vc = ValidityChecker::create(flags);
1964
1965   try {
1966     Type intType(vc->intType());
1967     Type fType(vc->funType(intType,intType));
1968
1969     Expr x(vc->varExpr("x",intType));
1970     Expr y(vc->varExpr("y",intType));
1971     Expr a(vc->varExpr("a",intType));
1972     Expr b(vc->varExpr("b",intType));
1973
1974     Expr s(vc->exprFromString("x < y"));
1975     Expr t(vc->exprFromString("a < b"));
1976
1977     cout << "s=" << s << "\nt=" << t << "\n";
1978
1979     std::vector<Expr> oldExprs, newExprs;
1980     oldExprs.push_back(x);
1981     oldExprs.push_back(y);
1982     newExprs.push_back(a);
1983     newExprs.push_back(b);
1984
1985     Expr u(s.substExpr(oldExprs,newExprs));
1986     cout << "u=" << u << "\n";
1987
1988     EXPECT( t == u, "Expected t==u" );
1989   } catch(const Exception& e) {
1990     exitStatus = 1;
1991     cout << "*** Exception caught in test23(): \n" << e << endl;
1992   }
1993   delete vc;
1994 }
1995
1996 void test24() {
1997   CLFlags flags = ValidityChecker::createFlags();
1998   ValidityChecker* vc = ValidityChecker::create(flags);
1999
2000   try {
2001     Type intType(vc->intType());
2002     Type aType(vc->arrayType(intType,intType));
2003
2004     Expr a(vc->varExpr("a",aType));
2005     Expr x(vc->varExpr("x",intType));
2006     Expr ax(vc->exprFromString("a[x]"));
2007
2008     Expr p(vc->exprFromString("FORALL (x:INT) : PATTERN (a[x]) : x < a[x]"));
2009
2010     cout << p  << "\n";
2011
2012     vector<vector<Expr> > pTriggers(p.getTriggers());
2013     EXPECT( pTriggers.size() == 1,
2014             "Actual: " + int2string(pTriggers.size()));
2015     EXPECT( pTriggers[0].size() == 1,
2016             "Actual: " + int2string( pTriggers[0].size()));
2017     /* We can't check that the trigger == ax, because x will have
2018      * been replaced with a bvar
2019      */
2020     EXPECT( pTriggers[0][0].getKind() == READ,
2021             "Actual: " + int2string(pTriggers[0][0].getKind()));
2022     EXPECT( pTriggers[0][0][0] == a,
2023             "Actual: " + pTriggers[0][0][0].toString() );
2024
2025     Expr aPrime(vc->varExpr("a'",aType));
2026     Expr axPrime(vc->exprFromString("a'[x]"));
2027
2028     ExprHashMap<Expr> substMap;
2029     substMap.insert(a,aPrime);
2030
2031     Expr q(p.substExpr(substMap));
2032
2033     cout << q << "\n";
2034
2035     vector<vector<Expr> > qTriggers(q.getTriggers());
2036     EXPECT( qTriggers.size() == 1,
2037             "Actual: " +
2038             int2string(qTriggers.size()));
2039     EXPECT( qTriggers[0].size() == 1,
2040             "Actual: " +
2041             int2string(qTriggers[0].size()));
2042     EXPECT( qTriggers[0][0].getKind() == READ,
2043             "Actual: " +
2044             int2string(qTriggers[0][0].getKind()));
2045     EXPECT( qTriggers[0][0][0] == aPrime,
2046             "Actual: " + qTriggers[0][0][0].toString() );
2047   } catch(const Exception& e) {
2048     exitStatus = 1;
2049     cout << "*** Exception caught in test24(): \n" << e << endl;
2050   }
2051   delete vc;
2052 }
2053
2054
2055 void test25() {
2056   CLFlags flags = ValidityChecker::createFlags();
2057   ValidityChecker* vc = ValidityChecker::create(flags);
2058
2059   try {
2060     Type realType(vc->realType());
2061
2062     Expr x = vc->ratExpr("-0.1");
2063     cout << "-0.1: " << x << endl;
2064     Expr y = vc->ratExpr("-1/10");
2065     cout << "-1/10: " << y << endl;
2066     Expr z = vc->ratExpr("-1","10",10);
2067     cout << "-1 over 10: " << z << endl;
2068     Expr w = vc->ratExpr(-1,10);
2069     cout << "-1 over 10 (ints): " << w << endl;
2070
2071     EXPECT(x == y && y == z && z == w, "Error in rational constants");
2072
2073   } catch(const Exception& e) {
2074     exitStatus = 1;
2075     cout << "*** Exception caught in test25(): \n" << e << endl;
2076   }
2077   delete vc;
2078 }
2079
2080
2081 void test26() {
2082   CLFlags flags = ValidityChecker::createFlags();
2083   ValidityChecker* vc = ValidityChecker::create(flags);
2084
2085   try {
2086     Type bvType(vc->bitvecType(32));
2087
2088     Expr x = vc->varExpr("x", bvType);
2089     Expr e1 = vc->newFixedConstWidthLeftShiftExpr(x, 16);
2090     Expr e2 = vc->newBVSHL(x, vc->newBVConstExpr(16, 32));
2091
2092     bool b = check(vc, vc->eqExpr(e1, e2));
2093     EXPECT(b, "Should be valid");
2094
2095     e1 = vc->newFixedRightShiftExpr(x, 16);
2096     e2 = vc->newBVLSHR(x, vc->newBVConstExpr(16, 32));
2097
2098     b = check(vc, vc->eqExpr(e1, e2));
2099     EXPECT(b, "Should be valid");
2100
2101     e2 = vc->newBVASHR(x, vc->newBVConstExpr(16, 32));
2102     b = check(vc, vc->eqExpr(e1, e2));
2103     EXPECT(!b, "Should be invalid");
2104
2105   } catch(const Exception& e) {
2106     exitStatus = 1;
2107     cout << "*** Exception caught in test26(): \n" << e << endl;
2108   }
2109   delete vc;
2110 }
2111
2112
2113 int main(int argc, char** argv)
2114 {
2115   int regressLevel = 3;
2116   if (argc > 1) regressLevel = atoi(argv[1]);
2117   cout << "Running API test, regress level = " << regressLevel << endl;
2118   exitStatus = 0;
2119
2120   try {
2121     // [MGD for CVC4] This is a CVC3 test, and many tests had to be commented
2122     // out for CVC4 since the functionality is either unsupported or
2123     // as-yet-unimplemented in CVC4's compatibility layer.  For example,
2124     // subranges, predicate subtyping, quantifiers, and string expressions
2125     // are unavailable.  Also, Exprs and Types are distinct in CVC4 and it's
2126     // not clear how to implement Type::getExpr(), and Exprs and Ops are
2127     // indistinguishable, so getOp() and getOpExpr() have the same result.
2128
2129     cout << "\n}\ntest26(): {" << endl;
2130     test26();
2131     //cout << "\ntest(): {" << endl;
2132     //test();
2133     cout << "\n}\ntest1(): {" << endl;
2134     test1();
2135     cout << "\n}\n\ntest2(): {" << endl;
2136     test2();
2137     cout << "\n}\n\ntest3(): {" << endl;
2138     test3();
2139     cout << "\n}\n\ntest4(): {" << endl;
2140     test4();
2141     if (regressLevel > 0) {
2142       cout << "\n}\n\ntest5(): {" << endl;
2143       test5();
2144     }
2145     //cout << "\n}\n\ntest6(): {" << endl;
2146     //test6();
2147     cout << "\n}\n\ntest7(): {" << endl;
2148     test7();
2149     //cout << "\n}\n\ntest8(): {" << endl;
2150     //test8();
2151     cout << "\n}\n\ntest9(" << 10*regressLevel+10 << "): {" << endl;
2152     test9(10*regressLevel+10);
2153     cout << "\nbvtest9(): {" << endl;
2154     bvtest9(regressLevel*3+2);
2155     cout << "\n}" << endl;
2156
2157     // Test for obvious memory leaks
2158     int limit = 100 * regressLevel+10;
2159     for(int i=0; i<limit; ++i) {
2160       if(i % 100 == 0)  cout << "test10[" << i << "]" << endl;
2161       test10();
2162     }
2163
2164     //cout << "\ntest11(): {" << endl;
2165     //test11();
2166     cout << "\n}\ntest12(): {" << endl;
2167     test12();
2168     cout << "\n}\ntest13(): {" << endl;
2169     test13();
2170     cout << "\n}\ntest14(): {" << endl;
2171     test14();
2172     //cout << "\n}\ntest15(): {" << endl;
2173     //test15();
2174     //cout << "\n}\ntest16(): {" << endl;
2175     //test16();
2176     cout << "\n}\ntest17(): {" << endl;
2177     test17();
2178     cout << "\n}\ntest18(): {" << endl;
2179     test18();
2180     cout << "\n}\ntest19(): {" << endl;
2181     test19();
2182     cout << "\ntest20(): {" << endl;
2183     test20();
2184     cout << "\n}\ntest21(): {" << endl;
2185     test21();
2186     //cout << "\n}\ntest22(): {" << endl;
2187     //test22();
2188     cout << "\n}\ntest23(): {" << endl;
2189     test23();
2190     cout << "\n}\ntest24(): {" << endl;
2191     test24();
2192     cout << "\n}\ntest25(): {" << endl;
2193     test25();
2194
2195     /*
2196     if (regressLevel > 1) {
2197       cout << "\n}\ntestgeorge1(): {" << endl;
2198       testgeorge1();
2199       cout << "\n}\ntestgeorge2(): {" << endl;
2200       testgeorge2();
2201       cout << "\n}\ntestgeorge3(): {" << endl;
2202       testgeorge3();
2203       cout << "\n}\ntestgeorge4(): {" << endl;
2204       testgeorge4();
2205       cout << "\n}\ntestgeorge5(): {" << endl;
2206       testgeorge5();
2207     }
2208     */
2209     cout << "\n}" << endl;
2210
2211   } catch(const Exception& e) {
2212     cout << "*** Exception caught: \n" << e << endl;
2213     exitStatus = 1;
2214   }
2215   if(exitStatus == 0)
2216     cout << "Program exits successfully." << endl;
2217   else
2218     cout << "Program exits with error status = " << exitStatus << "." << endl;
2219   return exitStatus;
2220 }