diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-28 17:29:01 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-28 17:29:01 +0000 |
commit | 65f720aac2d497c6e829d9c76638073a10060e7d (patch) | |
tree | 357035797e31f96a37dce30cb97ddb0aaf8f3bb7 /test | |
parent | c0c351a89871e0a6881668fa1a8d87349ab8af8e (diff) |
Public interface review items:
* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument()
* Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only
* CheckArgument() throws non-AssertionException
* things outside the core library (parsers, driver) use regular C-style assert,
or a public exception type.
* auto-generated documentation for Smt options and internal options
Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.
Diffstat (limited to 'test')
-rw-r--r-- | test/system/ouroborous.cpp | 10 | ||||
-rw-r--r-- | test/unit/expr/expr_manager_public.h | 5 | ||||
-rw-r--r-- | test/unit/expr/expr_public.h | 1 | ||||
-rw-r--r-- | test/unit/expr/kind_map_black.h | 2 | ||||
-rw-r--r-- | test/unit/expr/node_black.h | 4 | ||||
-rw-r--r-- | test/unit/expr/type_cardinality_public.h | 1 | ||||
-rw-r--r-- | test/unit/theory/logic_info_white.h | 68 | ||||
-rw-r--r-- | test/unit/util/assert_white.h | 4 | ||||
-rw-r--r-- | test/unit/util/boolean_simplification_black.h | 8 |
9 files changed, 48 insertions, 55 deletions
diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp index ac864d16b..daa7a9aae 100644 --- a/test/system/ouroborous.cpp +++ b/test/system/ouroborous.cpp @@ -72,8 +72,8 @@ string translate(string in, InputLanguage inlang, OutputLanguage outlang) { Expr e = psr->nextExpression(); stringstream ss; ss << Expr::setlanguage(outlang) << Expr::setdepth(-1) << e; - AlwaysAssert(psr->nextExpression().isNull(), "next expr should be null"); - AlwaysAssert(psr->done(), "parser should be done"); + assert(psr->nextExpression().isNull());// next expr should be null + assert(psr->done());// parser should be done string s = ss.str(); cout << "got this:" << endl << s << endl @@ -81,7 +81,7 @@ string translate(string in, InputLanguage inlang, OutputLanguage outlang) { psr->setInput(Input::newStringInput(toInputLanguage(outlang), s, "internal-buffer")); Expr f = psr->nextExpression(); - AlwaysAssert(e == f); + assert(e == f); cout << "got same expressions " << e.getId() << " and " << f.getId() << endl << "==============================================" << endl; @@ -103,7 +103,7 @@ void runTestString(std::string instr, InputLanguage instrlang = input::LANG_SMTL string out = translate(cvc, input::LANG_CVC4, output::LANG_SMTLIB_V2); cout << "back to SMT2 : " << out << endl << endl; - AlwaysAssert(out == smt2, "differences in output"); + assert(out == smt2);// differences in output } @@ -121,7 +121,7 @@ int runTest() { delete c; } - AlwaysAssert(psr->done(), "parser should be done"); + assert(psr->done());// parser should be done cout << Expr::setdepth(-1); diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h index e709648c9..e0ebe9640 100644 --- a/test/unit/expr/expr_manager_public.h +++ b/test/unit/expr/expr_manager_public.h @@ -23,7 +23,6 @@ #include "expr/expr_manager.h" #include "expr/expr.h" -#include "util/Assert.h" #include "util/exception.h" using namespace CVC4; @@ -120,12 +119,12 @@ public: void testMkAssociativeTooFew() { std::vector<Expr> vars = mkVars(d_exprManager->booleanType(), 1); - TS_ASSERT_THROWS( d_exprManager->mkAssociative(AND,vars), AssertionException); + TS_ASSERT_THROWS( d_exprManager->mkAssociative(AND,vars), IllegalArgumentException); } void testMkAssociativeBadKind() { std::vector<Expr> vars = mkVars(d_exprManager->integerType(), 10); - TS_ASSERT_THROWS( d_exprManager->mkAssociative(TUPLE,vars), AssertionException); + TS_ASSERT_THROWS( d_exprManager->mkAssociative(TUPLE,vars), IllegalArgumentException); } }; diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h index 279d4bebe..0d7608cac 100644 --- a/test/unit/expr/expr_public.h +++ b/test/unit/expr/expr_public.h @@ -23,7 +23,6 @@ #include "expr/expr_manager.h" #include "expr/expr.h" -#include "util/Assert.h" #include "util/exception.h" using namespace CVC4; diff --git a/test/unit/expr/kind_map_black.h b/test/unit/expr/kind_map_black.h index e5bcdd298..b994bd3af 100644 --- a/test/unit/expr/kind_map_black.h +++ b/test/unit/expr/kind_map_black.h @@ -102,7 +102,7 @@ public: TS_ASSERT(!(AND ^ AND ^ AND).isEmpty()); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(~LAST_KIND, IllegalArgumentException); + TS_ASSERT_THROWS(~LAST_KIND, AssertArgumentException); #endif /* CVC4_ASSERTIONS */ } diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 1518efadf..1a5f5ecfa 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -427,8 +427,8 @@ public: TS_ASSERT( f == fa.getOperator() ); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS( f.getOperator(), AssertionException ); - TS_ASSERT_THROWS( a.getOperator(), AssertionException ); + TS_ASSERT_THROWS( f.getOperator(), IllegalArgumentException ); + TS_ASSERT_THROWS( a.getOperator(), IllegalArgumentException ); #endif /* CVC4_ASSERTIONS */ } diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h index 7ba212dd5..78a872aea 100644 --- a/test/unit/expr/type_cardinality_public.h +++ b/test/unit/expr/type_cardinality_public.h @@ -26,7 +26,6 @@ #include "expr/type.h" #include "expr/expr_manager.h" #include "util/cardinality.h" -#include "util/Assert.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h index a2f61f5d2..c091eab71 100644 --- a/test/unit/theory/logic_info_white.h +++ b/test/unit/theory/logic_info_white.h @@ -450,31 +450,29 @@ public: LogicInfo info; TS_ASSERT( !info.isLocked() ); -#ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS( info.getLogicString(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BUILTIN ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BOOL ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_UF ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARITH ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARRAY ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BV ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_DATATYPES ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_QUANTIFIERS ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_REWRITERULES ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_BUILTIN ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_BOOL ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_UF ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_ARITH ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_ARRAY ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_BV ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_DATATYPES ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_QUANTIFIERS ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_REWRITERULES ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isQuantified(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.areIntegersUsed(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.areRealsUsed(), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isLinear(), CVC4::AssertionException ); -#endif /* CVC4_ASSERTIONS */ + TS_ASSERT_THROWS( info.getLogicString(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BUILTIN ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BOOL ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_UF ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARITH ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARRAY ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BV ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_DATATYPES ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_QUANTIFIERS ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_REWRITERULES ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_BUILTIN ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_BOOL ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_UF ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_ARITH ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_ARRAY ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_BV ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_DATATYPES ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_QUANTIFIERS ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_REWRITERULES ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isQuantified(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.areIntegersUsed(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.areRealsUsed(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( ! info.isLinear(), CVC4::IllegalArgumentException ); info.lock(); TS_ASSERT( info.isLocked() ); @@ -503,17 +501,15 @@ public: TS_ASSERT( info.areRealsUsed() ); TS_ASSERT( ! info.isLinear() ); -#ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS( info.arithOnlyLinear(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.disableIntegers(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.disableQuantifiers(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.disableTheory(THEORY_BV), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.disableTheory(THEORY_DATATYPES), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.enableIntegers(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.disableReals(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.disableTheory(THEORY_ARITH), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.disableTheory(THEORY_UF), CVC4::AssertionException ); -#endif /* CVC4_ASSERTIONS */ + TS_ASSERT_THROWS( info.arithOnlyLinear(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.disableIntegers(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.disableQuantifiers(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.disableTheory(THEORY_BV), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.disableTheory(THEORY_DATATYPES), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.enableIntegers(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.disableReals(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.disableTheory(THEORY_ARITH), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.disableTheory(THEORY_UF), CVC4::IllegalArgumentException ); info = info.getUnlockedCopy(); TS_ASSERT( !info.isLocked() ); diff --git a/test/unit/util/assert_white.h b/test/unit/util/assert_white.h index 6d88f89bd..54c77b165 100644 --- a/test/unit/util/assert_white.h +++ b/test/unit/util/assert_white.h @@ -32,7 +32,7 @@ public: void testAssert() { #ifdef CVC4_ASSERTIONS TS_ASSERT_THROWS( Assert(false), AssertionException ); - TS_ASSERT_THROWS( AssertArgument(false, "x"), IllegalArgumentException ); + TS_ASSERT_THROWS( AssertArgument(false, "x"), AssertArgumentException ); #else /* CVC4_ASSERTIONS */ TS_ASSERT_THROWS_NOTHING( Assert(false) ); TS_ASSERT_THROWS_NOTHING( AssertArgument(false, "x") ); @@ -46,7 +46,7 @@ public: TS_ASSERT_THROWS( IllegalArgument("x"), IllegalArgumentException ); TS_ASSERT_THROWS( CheckArgument(false, "x"), IllegalArgumentException ); TS_ASSERT_THROWS( AlwaysAssertArgument(false, "x"), - IllegalArgumentException ); + AssertArgumentException ); TS_ASSERT_THROWS_NOTHING( AssertArgument(true, "x") ); TS_ASSERT_THROWS_NOTHING( AssertArgument(true, "x") ); } diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h index 8f2d0d97f..e333e7205 100644 --- a/test/unit/util/boolean_simplification_black.h +++ b/test/unit/util/boolean_simplification_black.h @@ -135,7 +135,7 @@ public: #ifdef CVC4_ASSERTIONS in = Node(); - TS_ASSERT_THROWS( BooleanSimplification::negate(in), IllegalArgumentException ); + TS_ASSERT_THROWS( BooleanSimplification::negate(in), AssertArgumentException ); #endif /* CVC4_ASSERTIONS */ } @@ -170,7 +170,7 @@ public: #ifdef CVC4_ASSERTIONS in = d_nm->mkNode(kind::AND, a, b); - TS_ASSERT_THROWS( BooleanSimplification::simplifyClause(in), IllegalArgumentException ); + TS_ASSERT_THROWS( BooleanSimplification::simplifyClause(in), AssertArgumentException ); #endif /* CVC4_ASSERTIONS */ } @@ -195,7 +195,7 @@ public: #ifdef CVC4_ASSERTIONS in = d_nm->mkNode(kind::OR, a, b); - TS_ASSERT_THROWS( BooleanSimplification::simplifyHornClause(in), IllegalArgumentException ); + TS_ASSERT_THROWS( BooleanSimplification::simplifyHornClause(in), AssertArgumentException ); #endif /* CVC4_ASSERTIONS */ } @@ -216,7 +216,7 @@ public: #ifdef CVC4_ASSERTIONS in = d_nm->mkNode(kind::OR, a, b); - TS_ASSERT_THROWS( BooleanSimplification::simplifyConflict(in), IllegalArgumentException ); + TS_ASSERT_THROWS( BooleanSimplification::simplifyConflict(in), AssertArgumentException ); #endif /* CVC4_ASSERTIONS */ } |