diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-10-04 14:40:01 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-10-04 14:40:01 +0000 |
commit | 536c95e9cd2e98cf3bc01a808ee1ae90df1b1b10 (patch) | |
tree | 978649c639a9aaa3561d5a3578eac26d0e8f62a1 /test | |
parent | 01d547ba46a88b1ab98778cd267e6458b3e30713 (diff) |
compatibility, bindings
Diffstat (limited to 'test')
-rw-r--r-- | test/system/cvc3_main.cpp | 43 |
1 files changed, 26 insertions, 17 deletions
diff --git a/test/system/cvc3_main.cpp b/test/system/cvc3_main.cpp index d86526da8..76ff9e974 100644 --- a/test/system/cvc3_main.cpp +++ b/test/system/cvc3_main.cpp @@ -202,7 +202,7 @@ void test1() vector<Expr> assertions; cout << "Scope level: " << vc->scopeLevel() << endl; cout << "Counter-example:" << endl; - vc->getCounterExample(assertions); + //vc->getCounterExample(assertions); for (unsigned i = 0; i < assertions.size(); ++i) { vc->printExpr(assertions[i]); } @@ -367,7 +367,7 @@ void test3() vector<Expr> assertions; unsigned index; - vc->getCounterExample(assertions); + //vc->getCounterExample(assertions); cout << "Test Invalid Under Conditions:" << endl; for (index = 0; index < assertions.size(); ++index) { @@ -432,7 +432,7 @@ void test4() vector<Expr> assertions; unsigned index; - vc->getCounterExample(assertions); + //vc->getCounterExample(assertions); cout << "Test Invalid Under Conditions:" << endl; for (index = 0; index < assertions.size(); ++index) { @@ -539,7 +539,8 @@ void test5() // hyp.push_back(vc->orExpr(vc->geExpr(qmp, N), vc->leExpr(qmp, zero))); // hyp.push_back(vc->orExpr(vc->geExpr(qmr, N), vc->leExpr(qmr, zero))); - Expr test = vc->impliesExpr(vc->andExpr(hyp), e); + //Expr test = vc->impliesExpr(vc->andExpr(hyp), e); + Expr test = vc->impliesExpr(hyp[0], e); Expr query; cout << "Checking verification condition:" << endl; @@ -558,7 +559,7 @@ void test5() int req; vector<Expr> leaves; - vc->getCounterExample(assertions); + //vc->getCounterExample(assertions); cout << "Invalid Under Conditions:" << endl; for (index = 0; index < assertions.size(); ++index) { @@ -2090,6 +2091,14 @@ int main(int argc, char** argv) cout << "Running API test, regress level = " << regressLevel << endl; exitStatus = 0; try { + // [MGD for CVC4] This is a CVC3 test, and many tests had to be commented + // out for CVC4 since the functionality is either unsupported or + // as-yet-unimplemented in CVC4's compatibility layer. For example, + // subranges, predicate subtyping, quantifiers, and string expressions + // are unavailable. Also, Exprs and Types are distinct in CVC4 and it's + // not clear how to implement Type::getExpr(), and Exprs and Ops are + // indistinguishable, so getOp() and getOpExpr() have the same result. + //cout << "\n}\ntest26(): {" << endl; //test26(); //cout << "\ntest(): {" << endl; @@ -2110,8 +2119,8 @@ int main(int argc, char** argv) //test6(); cout << "\n}\n\ntest7(): {" << endl; test7(); - cout << "\n}\n\ntest8(): {" << endl; - test8(); + //cout << "\n}\n\ntest8(): {" << endl; + //test8(); cout << "\n}\n\ntest9(" << 10*regressLevel+10 << "): {" << endl; test9(10*regressLevel+10); cout << "\nbvtest9(): {" << endl; @@ -2133,22 +2142,22 @@ int main(int argc, char** argv) test13(); cout << "\n}\ntest14(): {" << endl; test14(); - cout << "\n}\ntest15(): {" << endl; - test15(); - cout << "\n}\ntest16(): {" << endl; - test16(); + //cout << "\n}\ntest15(): {" << endl; + //test15(); + //cout << "\n}\ntest16(): {" << endl; + //test16(); cout << "\n}\ntest17(): {" << endl; test17(); cout << "\n}\ntest18(): {" << endl; test18(); - cout << "\n}\ntest19(): {" << endl; - test19(); - cout << "\ntest20(): {" << endl; - test20(); + //cout << "\n}\ntest19(): {" << endl; + //test19(); + //cout << "\ntest20(): {" << endl; + //test20(); cout << "\n}\ntest21(): {" << endl; test21(); - cout << "\n}\ntest22(): {" << endl; - test22(); + //cout << "\n}\ntest22(): {" << endl; + //test22(); cout << "\n}\ntest23(): {" << endl; test23(); cout << "\n}\ntest24(): {" << endl; |