summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/system/ouroborous.cpp10
-rw-r--r--test/unit/expr/expr_manager_public.h5
-rw-r--r--test/unit/expr/expr_public.h1
-rw-r--r--test/unit/expr/kind_map_black.h2
-rw-r--r--test/unit/expr/node_black.h4
-rw-r--r--test/unit/expr/type_cardinality_public.h1
-rw-r--r--test/unit/theory/logic_info_white.h68
-rw-r--r--test/unit/util/assert_white.h4
-rw-r--r--test/unit/util/boolean_simplification_black.h8
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 */
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback