summaryrefslogtreecommitdiff
path: root/test/unit
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2021-02-08 09:55:38 -0800
committerGitHub <noreply@github.com>2021-02-08 09:55:38 -0800
commit2ee190b7b4ead29ef34e3eb115457ff3e21afbab (patch)
tree7a6ae311a97160a3f8bd8a5aef5f1b42f28a832c /test/unit
parentab271818bb73efaedb5ac2d861d782308025dab5 (diff)
Use consistent names for fixtures in unit tests. (#5863)
Diffstat (limited to 'test/unit')
-rw-r--r--test/unit/api/datatype_api_black.cpp16
-rw-r--r--test/unit/api/grammar_black.cpp10
-rw-r--r--test/unit/api/op_black.cpp16
-rw-r--r--test/unit/api/result_black.cpp16
-rw-r--r--test/unit/api/solver_black.cpp262
-rw-r--r--test/unit/api/sort_black.cpp54
-rw-r--r--test/unit/api/term_black.cpp46
-rw-r--r--test/unit/expr/node_black.cpp2
-rw-r--r--test/unit/expr/node_builder_black.cpp30
9 files changed, 226 insertions, 226 deletions
diff --git a/test/unit/api/datatype_api_black.cpp b/test/unit/api/datatype_api_black.cpp
index 858316971..f72bcd1c3 100644
--- a/test/unit/api/datatype_api_black.cpp
+++ b/test/unit/api/datatype_api_black.cpp
@@ -22,11 +22,11 @@ using namespace api;
namespace test {
-class TestApiDatatypeBlack : public TestApi
+class TestApiBlackDatatype : public TestApi
{
};
-TEST_F(TestApiDatatypeBlack, mkDatatypeSort)
+TEST_F(TestApiBlackDatatype, mkDatatypeSort)
{
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
@@ -43,7 +43,7 @@ TEST_F(TestApiDatatypeBlack, mkDatatypeSort)
ASSERT_NO_THROW(nilConstr.getConstructorTerm());
}
-TEST_F(TestApiDatatypeBlack, mkDatatypeSorts)
+TEST_F(TestApiBlackDatatype, mkDatatypeSorts)
{
/* Create two mutual datatypes corresponding to this definition
* block:
@@ -108,7 +108,7 @@ TEST_F(TestApiDatatypeBlack, mkDatatypeSorts)
ASSERT_THROW(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException);
}
-TEST_F(TestApiDatatypeBlack, datatypeStructs)
+TEST_F(TestApiBlackDatatype, datatypeStructs)
{
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
@@ -182,7 +182,7 @@ TEST_F(TestApiDatatypeBlack, datatypeStructs)
ASSERT_TRUE(dtRecord.isWellFounded());
}
-TEST_F(TestApiDatatypeBlack, datatypeNames)
+TEST_F(TestApiBlackDatatype, datatypeNames)
{
Sort intSort = d_solver.getIntegerSort();
@@ -219,7 +219,7 @@ TEST_F(TestApiDatatypeBlack, datatypeNames)
ASSERT_THROW(DatatypeDecl().getName(), CVC4ApiException);
}
-TEST_F(TestApiDatatypeBlack, parametricDatatype)
+TEST_F(TestApiBlackDatatype, parametricDatatype)
{
std::vector<Sort> v;
Sort t1 = d_solver.mkParamSort("T1");
@@ -297,7 +297,7 @@ TEST_F(TestApiDatatypeBlack, parametricDatatype)
ASSERT_TRUE(pairIntInt.isSubsortOf(pairIntInt));
}
-TEST_F(TestApiDatatypeBlack, datatypeSimplyRec)
+TEST_F(TestApiBlackDatatype, datatypeSimplyRec)
{
/* Create mutual datatypes corresponding to this definition block:
*
@@ -496,7 +496,7 @@ TEST_F(TestApiDatatypeBlack, datatypeSimplyRec)
ASSERT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
}
-TEST_F(TestApiDatatypeBlack, datatypeSpecializedCons)
+TEST_F(TestApiBlackDatatype, datatypeSpecializedCons)
{
/* Create mutual datatypes corresponding to this definition block:
* DATATYPE
diff --git a/test/unit/api/grammar_black.cpp b/test/unit/api/grammar_black.cpp
index c87406a87..406d145ab 100644
--- a/test/unit/api/grammar_black.cpp
+++ b/test/unit/api/grammar_black.cpp
@@ -22,11 +22,11 @@ using namespace api;
namespace test {
-class TestApiGrammarBlack : public TestApi
+class TestApiBlackGrammar : public TestApi
{
};
-TEST_F(TestApiGrammarBlack, addRule)
+TEST_F(TestApiBlackGrammar, addRule)
{
Sort boolean = d_solver.getBooleanSort();
Sort integer = d_solver.getIntegerSort();
@@ -50,7 +50,7 @@ TEST_F(TestApiGrammarBlack, addRule)
ASSERT_THROW(g.addRule(start, d_solver.mkBoolean(false)), CVC4ApiException);
}
-TEST_F(TestApiGrammarBlack, addRules)
+TEST_F(TestApiBlackGrammar, addRules)
{
Sort boolean = d_solver.getBooleanSort();
Sort integer = d_solver.getIntegerSort();
@@ -75,7 +75,7 @@ TEST_F(TestApiGrammarBlack, addRules)
CVC4ApiException);
}
-TEST_F(TestApiGrammarBlack, addAnyConstant)
+TEST_F(TestApiBlackGrammar, addAnyConstant)
{
Sort boolean = d_solver.getBooleanSort();
@@ -96,7 +96,7 @@ TEST_F(TestApiGrammarBlack, addAnyConstant)
ASSERT_THROW(g.addAnyConstant(start), CVC4ApiException);
}
-TEST_F(TestApiGrammarBlack, addAnyVariable)
+TEST_F(TestApiBlackGrammar, addAnyVariable)
{
Sort boolean = d_solver.getBooleanSort();
diff --git a/test/unit/api/op_black.cpp b/test/unit/api/op_black.cpp
index 817662d67..19bd4bb03 100644
--- a/test/unit/api/op_black.cpp
+++ b/test/unit/api/op_black.cpp
@@ -20,18 +20,18 @@ using namespace api;
namespace test {
-class TestApiOpBlack : public TestApi
+class TestApiBlackOp : public TestApi
{
};
-TEST_F(TestApiOpBlack, getKind)
+TEST_F(TestApiBlackOp, getKind)
{
Op x;
x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1);
ASSERT_NO_THROW(x.getKind());
}
-TEST_F(TestApiOpBlack, isNull)
+TEST_F(TestApiBlackOp, isNull)
{
Op x;
ASSERT_TRUE(x.isNull());
@@ -39,7 +39,7 @@ TEST_F(TestApiOpBlack, isNull)
ASSERT_FALSE(x.isNull());
}
-TEST_F(TestApiOpBlack, opFromKind)
+TEST_F(TestApiBlackOp, opFromKind)
{
Op plus(&d_solver, PLUS);
ASSERT_FALSE(plus.isIndexed());
@@ -50,7 +50,7 @@ TEST_F(TestApiOpBlack, opFromKind)
ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT), CVC4ApiException);
}
-TEST_F(TestApiOpBlack, getIndicesString)
+TEST_F(TestApiBlackOp, getIndicesString)
{
Op x;
ASSERT_THROW(x.getIndices<std::string>(), CVC4ApiException);
@@ -66,7 +66,7 @@ TEST_F(TestApiOpBlack, getIndicesString)
ASSERT_THROW(record_update_ot.getIndices<uint32_t>(), CVC4ApiException);
}
-TEST_F(TestApiOpBlack, getIndicesUint)
+TEST_F(TestApiBlackOp, getIndicesUint)
{
Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5);
ASSERT_TRUE(bitvector_repeat_ot.isIndexed());
@@ -116,7 +116,7 @@ TEST_F(TestApiOpBlack, getIndicesUint)
ASSERT_THROW(tuple_update_ot.getIndices<std::string>(), CVC4ApiException);
}
-TEST_F(TestApiOpBlack, getIndicesPairUint)
+TEST_F(TestApiBlackOp, getIndicesPairUint)
{
Op bitvector_extract_ot = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0);
ASSERT_TRUE(bitvector_extract_ot.isIndexed());
@@ -175,7 +175,7 @@ TEST_F(TestApiOpBlack, getIndicesPairUint)
CVC4ApiException);
}
-TEST_F(TestApiOpBlack, opScopingToString)
+TEST_F(TestApiBlackOp, opScopingToString)
{
Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5);
std::string op_repr = bitvector_repeat_ot.toString();
diff --git a/test/unit/api/result_black.cpp b/test/unit/api/result_black.cpp
index 52cb68b25..887be8fe0 100644
--- a/test/unit/api/result_black.cpp
+++ b/test/unit/api/result_black.cpp
@@ -20,11 +20,11 @@ using namespace api;
namespace test {
-class TestApiResultBlack : public TestApi
+class TestApiBlackResult : public TestApi
{
};
-TEST_F(TestApiResultBlack, isNull)
+TEST_F(TestApiBlackResult, isNull)
{
CVC4::api::Result res_null;
ASSERT_TRUE(res_null.isNull());
@@ -41,7 +41,7 @@ TEST_F(TestApiResultBlack, isNull)
ASSERT_FALSE(res.isNull());
}
-TEST_F(TestApiResultBlack, eq)
+TEST_F(TestApiBlackResult, eq)
{
Sort u_sort = d_solver.mkUninterpretedSort("u");
Term x = d_solver.mkVar(u_sort, "x");
@@ -54,7 +54,7 @@ TEST_F(TestApiResultBlack, eq)
ASSERT_EQ(res3, res2);
}
-TEST_F(TestApiResultBlack, isSat)
+TEST_F(TestApiBlackResult, isSat)
{
Sort u_sort = d_solver.mkUninterpretedSort("u");
Term x = d_solver.mkVar(u_sort, "x");
@@ -64,7 +64,7 @@ TEST_F(TestApiResultBlack, isSat)
ASSERT_FALSE(res.isSatUnknown());
}
-TEST_F(TestApiResultBlack, isUnsat)
+TEST_F(TestApiBlackResult, isUnsat)
{
Sort u_sort = d_solver.mkUninterpretedSort("u");
Term x = d_solver.mkVar(u_sort, "x");
@@ -74,7 +74,7 @@ TEST_F(TestApiResultBlack, isUnsat)
ASSERT_FALSE(res.isSatUnknown());
}
-TEST_F(TestApiResultBlack, isSatUnknown)
+TEST_F(TestApiBlackResult, isSatUnknown)
{
d_solver.setLogic("QF_NIA");
d_solver.setOption("incremental", "false");
@@ -87,7 +87,7 @@ TEST_F(TestApiResultBlack, isSatUnknown)
ASSERT_TRUE(res.isSatUnknown());
}
-TEST_F(TestApiResultBlack, isEntailed)
+TEST_F(TestApiBlackResult, isEntailed)
{
d_solver.setOption("incremental", "true");
Sort u_sort = d_solver.mkUninterpretedSort("u");
@@ -104,7 +104,7 @@ TEST_F(TestApiResultBlack, isEntailed)
ASSERT_FALSE(not_entailed.isEntailmentUnknown());
}
-TEST_F(TestApiResultBlack, isEntailmentUnknown)
+TEST_F(TestApiBlackResult, isEntailmentUnknown)
{
d_solver.setLogic("QF_NIA");
d_solver.setOption("incremental", "false");
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 82a176498..2e285fcc7 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -23,11 +23,11 @@ using namespace api;
namespace test {
-class TestApiSolverBlack : public TestApi
+class TestApiBlackSolver : public TestApi
{
};
-TEST_F(TestApiSolverBlack, recoverableException)
+TEST_F(TestApiBlackSolver, recoverableException)
{
d_solver.setOption("produce-models", "true");
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
@@ -35,7 +35,7 @@ TEST_F(TestApiSolverBlack, recoverableException)
ASSERT_THROW(d_solver.getValue(x), CVC4ApiRecoverableException);
}
-TEST_F(TestApiSolverBlack, supportsFloatingPoint)
+TEST_F(TestApiBlackSolver, supportsFloatingPoint)
{
if (d_solver.supportsFloatingPoint())
{
@@ -48,37 +48,37 @@ TEST_F(TestApiSolverBlack, supportsFloatingPoint)
}
}
-TEST_F(TestApiSolverBlack, getBooleanSort)
+TEST_F(TestApiBlackSolver, getBooleanSort)
{
ASSERT_NO_THROW(d_solver.getBooleanSort());
}
-TEST_F(TestApiSolverBlack, getIntegerSort)
+TEST_F(TestApiBlackSolver, getIntegerSort)
{
ASSERT_NO_THROW(d_solver.getIntegerSort());
}
-TEST_F(TestApiSolverBlack, getNullSort)
+TEST_F(TestApiBlackSolver, getNullSort)
{
ASSERT_NO_THROW(d_solver.getNullSort());
}
-TEST_F(TestApiSolverBlack, getRealSort)
+TEST_F(TestApiBlackSolver, getRealSort)
{
ASSERT_NO_THROW(d_solver.getRealSort());
}
-TEST_F(TestApiSolverBlack, getRegExpSort)
+TEST_F(TestApiBlackSolver, getRegExpSort)
{
ASSERT_NO_THROW(d_solver.getRegExpSort());
}
-TEST_F(TestApiSolverBlack, getStringSort)
+TEST_F(TestApiBlackSolver, getStringSort)
{
ASSERT_NO_THROW(d_solver.getStringSort());
}
-TEST_F(TestApiSolverBlack, getRoundingModeSort)
+TEST_F(TestApiBlackSolver, getRoundingModeSort)
{
if (d_solver.supportsFloatingPoint())
{
@@ -90,7 +90,7 @@ TEST_F(TestApiSolverBlack, getRoundingModeSort)
}
}
-TEST_F(TestApiSolverBlack, mkArraySort)
+TEST_F(TestApiBlackSolver, mkArraySort)
{
Sort boolSort = d_solver.getBooleanSort();
Sort intSort = d_solver.getIntegerSort();
@@ -114,13 +114,13 @@ TEST_F(TestApiSolverBlack, mkArraySort)
ASSERT_THROW(slv.mkArraySort(boolSort, boolSort), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkBitVectorSort)
+TEST_F(TestApiBlackSolver, mkBitVectorSort)
{
ASSERT_NO_THROW(d_solver.mkBitVectorSort(32));
ASSERT_THROW(d_solver.mkBitVectorSort(0), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkFloatingPointSort)
+TEST_F(TestApiBlackSolver, mkFloatingPointSort)
{
if (d_solver.supportsFloatingPoint())
{
@@ -134,7 +134,7 @@ TEST_F(TestApiSolverBlack, mkFloatingPointSort)
}
}
-TEST_F(TestApiSolverBlack, mkDatatypeSort)
+TEST_F(TestApiBlackSolver, mkDatatypeSort)
{
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
@@ -151,7 +151,7 @@ TEST_F(TestApiSolverBlack, mkDatatypeSort)
ASSERT_THROW(d_solver.mkDatatypeSort(throwsDtypeSpec), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkDatatypeSorts)
+TEST_F(TestApiBlackSolver, mkDatatypeSorts)
{
Solver slv;
@@ -194,7 +194,7 @@ TEST_F(TestApiSolverBlack, mkDatatypeSorts)
/* Note: More tests are in datatype_api_black. */
}
-TEST_F(TestApiSolverBlack, mkFunctionSort)
+TEST_F(TestApiBlackSolver, mkFunctionSort)
{
ASSERT_NO_THROW(d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
d_solver.getIntegerSort()));
@@ -236,13 +236,13 @@ TEST_F(TestApiSolverBlack, mkFunctionSort)
CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkParamSort)
+TEST_F(TestApiBlackSolver, mkParamSort)
{
ASSERT_NO_THROW(d_solver.mkParamSort("T"));
ASSERT_NO_THROW(d_solver.mkParamSort(""));
}
-TEST_F(TestApiSolverBlack, mkPredicateSort)
+TEST_F(TestApiBlackSolver, mkPredicateSort)
{
ASSERT_NO_THROW(d_solver.mkPredicateSort({d_solver.getIntegerSort()}));
ASSERT_THROW(d_solver.mkPredicateSort({}), CVC4ApiException);
@@ -256,7 +256,7 @@ TEST_F(TestApiSolverBlack, mkPredicateSort)
CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkRecordSort)
+TEST_F(TestApiBlackSolver, mkRecordSort)
{
std::vector<std::pair<std::string, Sort>> fields = {
std::make_pair("b", d_solver.getBooleanSort()),
@@ -272,7 +272,7 @@ TEST_F(TestApiSolverBlack, mkRecordSort)
ASSERT_THROW(slv.mkRecordSort(fields), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkSetSort)
+TEST_F(TestApiBlackSolver, mkSetSort)
{
ASSERT_NO_THROW(d_solver.mkSetSort(d_solver.getBooleanSort()));
ASSERT_NO_THROW(d_solver.mkSetSort(d_solver.getIntegerSort()));
@@ -281,7 +281,7 @@ TEST_F(TestApiSolverBlack, mkSetSort)
ASSERT_THROW(slv.mkSetSort(d_solver.mkBitVectorSort(4)), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkBagSort)
+TEST_F(TestApiBlackSolver, mkBagSort)
{
ASSERT_NO_THROW(d_solver.mkBagSort(d_solver.getBooleanSort()));
ASSERT_NO_THROW(d_solver.mkBagSort(d_solver.getIntegerSort()));
@@ -290,7 +290,7 @@ TEST_F(TestApiSolverBlack, mkBagSort)
ASSERT_THROW(slv.mkBagSort(d_solver.mkBitVectorSort(4)), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkSequenceSort)
+TEST_F(TestApiBlackSolver, mkSequenceSort)
{
ASSERT_NO_THROW(d_solver.mkSequenceSort(d_solver.getBooleanSort()));
ASSERT_NO_THROW(d_solver.mkSequenceSort(
@@ -299,20 +299,20 @@ TEST_F(TestApiSolverBlack, mkSequenceSort)
ASSERT_THROW(slv.mkSequenceSort(d_solver.getIntegerSort()), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkUninterpretedSort)
+TEST_F(TestApiBlackSolver, mkUninterpretedSort)
{
ASSERT_NO_THROW(d_solver.mkUninterpretedSort("u"));
ASSERT_NO_THROW(d_solver.mkUninterpretedSort(""));
}
-TEST_F(TestApiSolverBlack, mkSortConstructorSort)
+TEST_F(TestApiBlackSolver, mkSortConstructorSort)
{
ASSERT_NO_THROW(d_solver.mkSortConstructorSort("s", 2));
ASSERT_NO_THROW(d_solver.mkSortConstructorSort("", 2));
ASSERT_THROW(d_solver.mkSortConstructorSort("", 0), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkTupleSort)
+TEST_F(TestApiBlackSolver, mkTupleSort)
{
ASSERT_NO_THROW(d_solver.mkTupleSort({d_solver.getIntegerSort()}));
Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
@@ -324,7 +324,7 @@ TEST_F(TestApiSolverBlack, mkTupleSort)
ASSERT_THROW(slv.mkTupleSort({d_solver.getIntegerSort()}), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkBitVector)
+TEST_F(TestApiBlackSolver, mkBitVector)
{
uint32_t size0 = 0, size1 = 8, size2 = 32, val1 = 2;
uint64_t val2 = 2;
@@ -351,7 +351,7 @@ TEST_F(TestApiSolverBlack, mkBitVector)
d_solver.mkBitVector(8, "FF", 16));
}
-TEST_F(TestApiSolverBlack, mkVar)
+TEST_F(TestApiBlackSolver, mkVar)
{
Sort boolSort = d_solver.getBooleanSort();
Sort intSort = d_solver.getIntegerSort();
@@ -366,13 +366,13 @@ TEST_F(TestApiSolverBlack, mkVar)
ASSERT_THROW(slv.mkVar(boolSort, "x"), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkBoolean)
+TEST_F(TestApiBlackSolver, mkBoolean)
{
ASSERT_NO_THROW(d_solver.mkBoolean(true));
ASSERT_NO_THROW(d_solver.mkBoolean(false));
}
-TEST_F(TestApiSolverBlack, mkRoundingMode)
+TEST_F(TestApiBlackSolver, mkRoundingMode)
{
if (CVC4::Configuration::isBuiltWithSymFPU())
{
@@ -385,7 +385,7 @@ TEST_F(TestApiSolverBlack, mkRoundingMode)
}
}
-TEST_F(TestApiSolverBlack, mkUninterpretedConst)
+TEST_F(TestApiBlackSolver, mkUninterpretedConst)
{
ASSERT_NO_THROW(d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1));
ASSERT_THROW(d_solver.mkUninterpretedConst(Sort(), 1), CVC4ApiException);
@@ -394,7 +394,7 @@ TEST_F(TestApiSolverBlack, mkUninterpretedConst)
CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkAbstractValue)
+TEST_F(TestApiBlackSolver, mkAbstractValue)
{
ASSERT_NO_THROW(d_solver.mkAbstractValue(std::string("1")));
ASSERT_THROW(d_solver.mkAbstractValue(std::string("0")), CVC4ApiException);
@@ -412,7 +412,7 @@ TEST_F(TestApiSolverBlack, mkAbstractValue)
ASSERT_THROW(d_solver.mkAbstractValue(0), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkFloatingPoint)
+TEST_F(TestApiBlackSolver, mkFloatingPoint)
{
Term t1 = d_solver.mkBitVector(8);
Term t2 = d_solver.mkBitVector(4);
@@ -438,7 +438,7 @@ TEST_F(TestApiSolverBlack, mkFloatingPoint)
}
}
-TEST_F(TestApiSolverBlack, mkEmptySet)
+TEST_F(TestApiBlackSolver, mkEmptySet)
{
Solver slv;
Sort s = d_solver.mkSetSort(d_solver.getBooleanSort());
@@ -449,7 +449,7 @@ TEST_F(TestApiSolverBlack, mkEmptySet)
ASSERT_THROW(slv.mkEmptySet(s), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkEmptyBag)
+TEST_F(TestApiBlackSolver, mkEmptyBag)
{
Solver slv;
Sort s = d_solver.mkBagSort(d_solver.getBooleanSort());
@@ -460,7 +460,7 @@ TEST_F(TestApiSolverBlack, mkEmptyBag)
ASSERT_THROW(slv.mkEmptyBag(s), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkEmptySequence)
+TEST_F(TestApiBlackSolver, mkEmptySequence)
{
Solver slv;
Sort s = d_solver.mkSequenceSort(d_solver.getBooleanSort());
@@ -469,13 +469,13 @@ TEST_F(TestApiSolverBlack, mkEmptySequence)
ASSERT_THROW(slv.mkEmptySequence(s), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkFalse)
+TEST_F(TestApiBlackSolver, mkFalse)
{
ASSERT_NO_THROW(d_solver.mkFalse());
ASSERT_NO_THROW(d_solver.mkFalse());
}
-TEST_F(TestApiSolverBlack, mkNaN)
+TEST_F(TestApiBlackSolver, mkNaN)
{
if (CVC4::Configuration::isBuiltWithSymFPU())
{
@@ -487,7 +487,7 @@ TEST_F(TestApiSolverBlack, mkNaN)
}
}
-TEST_F(TestApiSolverBlack, mkNegZero)
+TEST_F(TestApiBlackSolver, mkNegZero)
{
if (CVC4::Configuration::isBuiltWithSymFPU())
{
@@ -499,7 +499,7 @@ TEST_F(TestApiSolverBlack, mkNegZero)
}
}
-TEST_F(TestApiSolverBlack, mkNegInf)
+TEST_F(TestApiBlackSolver, mkNegInf)
{
if (CVC4::Configuration::isBuiltWithSymFPU())
{
@@ -511,7 +511,7 @@ TEST_F(TestApiSolverBlack, mkNegInf)
}
}
-TEST_F(TestApiSolverBlack, mkPosInf)
+TEST_F(TestApiBlackSolver, mkPosInf)
{
if (CVC4::Configuration::isBuiltWithSymFPU())
{
@@ -523,7 +523,7 @@ TEST_F(TestApiSolverBlack, mkPosInf)
}
}
-TEST_F(TestApiSolverBlack, mkPosZero)
+TEST_F(TestApiBlackSolver, mkPosZero)
{
if (CVC4::Configuration::isBuiltWithSymFPU())
{
@@ -535,7 +535,7 @@ TEST_F(TestApiSolverBlack, mkPosZero)
}
}
-TEST_F(TestApiSolverBlack, mkOp)
+TEST_F(TestApiBlackSolver, mkOp)
{
// mkOp(Kind kind, Kind k)
ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, EQUAL), CVC4ApiException);
@@ -556,9 +556,9 @@ TEST_F(TestApiSolverBlack, mkOp)
ASSERT_THROW(d_solver.mkOp(DIVISIBLE, 1, 2), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkPi) { ASSERT_NO_THROW(d_solver.mkPi()); }
+TEST_F(TestApiBlackSolver, mkPi) { ASSERT_NO_THROW(d_solver.mkPi()); }
-TEST_F(TestApiSolverBlack, mkInteger)
+TEST_F(TestApiBlackSolver, mkInteger)
{
ASSERT_NO_THROW(d_solver.mkInteger("123"));
ASSERT_THROW(d_solver.mkInteger("1.23"), CVC4ApiException);
@@ -599,7 +599,7 @@ TEST_F(TestApiSolverBlack, mkInteger)
ASSERT_NO_THROW(d_solver.mkInteger(val4));
}
-TEST_F(TestApiSolverBlack, mkReal)
+TEST_F(TestApiBlackSolver, mkReal)
{
ASSERT_NO_THROW(d_solver.mkReal("123"));
ASSERT_NO_THROW(d_solver.mkReal("1.23"));
@@ -644,7 +644,7 @@ TEST_F(TestApiSolverBlack, mkReal)
ASSERT_NO_THROW(d_solver.mkReal(val4, val4));
}
-TEST_F(TestApiSolverBlack, mkRegexpEmpty)
+TEST_F(TestApiBlackSolver, mkRegexpEmpty)
{
Sort strSort = d_solver.getStringSort();
Term s = d_solver.mkConst(strSort, "s");
@@ -652,7 +652,7 @@ TEST_F(TestApiSolverBlack, mkRegexpEmpty)
d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpEmpty()));
}
-TEST_F(TestApiSolverBlack, mkRegexpSigma)
+TEST_F(TestApiBlackSolver, mkRegexpSigma)
{
Sort strSort = d_solver.getStringSort();
Term s = d_solver.mkConst(strSort, "s");
@@ -660,7 +660,7 @@ TEST_F(TestApiSolverBlack, mkRegexpSigma)
d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma()));
}
-TEST_F(TestApiSolverBlack, mkSepNil)
+TEST_F(TestApiBlackSolver, mkSepNil)
{
ASSERT_NO_THROW(d_solver.mkSepNil(d_solver.getBooleanSort()));
ASSERT_THROW(d_solver.mkSepNil(Sort()), CVC4ApiException);
@@ -668,7 +668,7 @@ TEST_F(TestApiSolverBlack, mkSepNil)
ASSERT_THROW(slv.mkSepNil(d_solver.getIntegerSort()), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkString)
+TEST_F(TestApiBlackSolver, mkString)
{
ASSERT_NO_THROW(d_solver.mkString(""));
ASSERT_NO_THROW(d_solver.mkString("asdfasdf"));
@@ -678,7 +678,7 @@ TEST_F(TestApiSolverBlack, mkString)
"\"asdf\\u{5c}nasdf\"");
}
-TEST_F(TestApiSolverBlack, mkChar)
+TEST_F(TestApiBlackSolver, mkChar)
{
ASSERT_NO_THROW(d_solver.mkChar(std::string("0123")));
ASSERT_NO_THROW(d_solver.mkChar("aA"));
@@ -688,7 +688,7 @@ TEST_F(TestApiSolverBlack, mkChar)
ASSERT_EQ(d_solver.mkChar("abc"), d_solver.mkChar("ABC"));
}
-TEST_F(TestApiSolverBlack, mkTerm)
+TEST_F(TestApiBlackSolver, mkTerm)
{
Sort bv32 = d_solver.mkBitVectorSort(32);
Term a = d_solver.mkConst(bv32, "a");
@@ -745,7 +745,7 @@ TEST_F(TestApiSolverBlack, mkTerm)
ASSERT_THROW(d_solver.mkTerm(DISTINCT, v6), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkTermFromOp)
+TEST_F(TestApiBlackSolver, mkTermFromOp)
{
Sort bv32 = d_solver.mkBitVectorSort(32);
Term a = d_solver.mkConst(bv32, "a");
@@ -843,13 +843,13 @@ TEST_F(TestApiSolverBlack, mkTermFromOp)
ASSERT_THROW(slv.mkTerm(opterm2, v4), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkTrue)
+TEST_F(TestApiBlackSolver, mkTrue)
{
ASSERT_NO_THROW(d_solver.mkTrue());
ASSERT_NO_THROW(d_solver.mkTrue());
}
-TEST_F(TestApiSolverBlack, mkTuple)
+TEST_F(TestApiBlackSolver, mkTuple)
{
ASSERT_NO_THROW(d_solver.mkTuple({d_solver.mkBitVectorSort(3)},
{d_solver.mkBitVector("101", 2)}));
@@ -873,7 +873,7 @@ TEST_F(TestApiSolverBlack, mkTuple)
CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkUniverseSet)
+TEST_F(TestApiBlackSolver, mkUniverseSet)
{
ASSERT_NO_THROW(d_solver.mkUniverseSet(d_solver.getBooleanSort()));
ASSERT_THROW(d_solver.mkUniverseSet(Sort()), CVC4ApiException);
@@ -881,7 +881,7 @@ TEST_F(TestApiSolverBlack, mkUniverseSet)
ASSERT_THROW(slv.mkUniverseSet(d_solver.getBooleanSort()), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkConst)
+TEST_F(TestApiBlackSolver, mkConst)
{
Sort boolSort = d_solver.getBooleanSort();
Sort intSort = d_solver.getIntegerSort();
@@ -899,7 +899,7 @@ TEST_F(TestApiSolverBlack, mkConst)
ASSERT_THROW(slv.mkConst(boolSort), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkConstArray)
+TEST_F(TestApiBlackSolver, mkConstArray)
{
Sort intSort = d_solver.getIntegerSort();
Sort arrSort = d_solver.mkArraySort(intSort, intSort);
@@ -919,7 +919,7 @@ TEST_F(TestApiSolverBlack, mkConstArray)
ASSERT_THROW(slv.mkConstArray(arrSort, zero2), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, declareDatatype)
+TEST_F(TestApiBlackSolver, declareDatatype)
{
DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
std::vector<DatatypeConstructorDecl> ctors1 = {nil};
@@ -941,7 +941,7 @@ TEST_F(TestApiSolverBlack, declareDatatype)
ASSERT_THROW(slv.declareDatatype(std::string("a"), ctors1), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, declareFun)
+TEST_F(TestApiBlackSolver, declareFun)
{
Sort bvSort = d_solver.mkBitVectorSort(32);
Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
@@ -958,14 +958,14 @@ TEST_F(TestApiSolverBlack, declareFun)
ASSERT_THROW(slv.declareFun("f1", {}, bvSort), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, declareSort)
+TEST_F(TestApiBlackSolver, declareSort)
{
ASSERT_NO_THROW(d_solver.declareSort("s", 0));
ASSERT_NO_THROW(d_solver.declareSort("s", 2));
ASSERT_NO_THROW(d_solver.declareSort("", 2));
}
-TEST_F(TestApiSolverBlack, defineSort)
+TEST_F(TestApiBlackSolver, defineSort)
{
Sort sortVar0 = d_solver.mkParamSort("T0");
Sort sortVar1 = d_solver.mkParamSort("T1");
@@ -978,7 +978,7 @@ TEST_F(TestApiSolverBlack, defineSort)
ASSERT_NO_THROW(arraySort1.substitute({sortVar0, sortVar1}, {intSort, realSort}));
}
-TEST_F(TestApiSolverBlack, defineFun)
+TEST_F(TestApiBlackSolver, defineFun)
{
Sort bvSort = d_solver.mkBitVectorSort(32);
Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
@@ -1024,7 +1024,7 @@ TEST_F(TestApiSolverBlack, defineFun)
ASSERT_THROW(slv.defineFun("ff", {b12, b22}, bvSort2, v1), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, defineFunGlobal)
+TEST_F(TestApiBlackSolver, defineFunGlobal)
{
Sort bSort = d_solver.getBooleanSort();
Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
@@ -1048,7 +1048,7 @@ TEST_F(TestApiSolverBlack, defineFunGlobal)
ASSERT_TRUE(d_solver.checkSat().isUnsat());
}
-TEST_F(TestApiSolverBlack, defineFunRec)
+TEST_F(TestApiBlackSolver, defineFunRec)
{
Sort bvSort = d_solver.mkBitVectorSort(32);
Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
@@ -1100,7 +1100,7 @@ TEST_F(TestApiSolverBlack, defineFunRec)
CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, defineFunRecWrongLogic)
+TEST_F(TestApiBlackSolver, defineFunRecWrongLogic)
{
d_solver.setLogic("QF_BV");
Sort bvSort = d_solver.mkBitVectorSort(32);
@@ -1112,7 +1112,7 @@ TEST_F(TestApiSolverBlack, defineFunRecWrongLogic)
ASSERT_THROW(d_solver.defineFunRec(f, {b, b}, v), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, defineFunRecGlobal)
+TEST_F(TestApiBlackSolver, defineFunRecGlobal)
{
Sort bSort = d_solver.getBooleanSort();
Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
@@ -1137,7 +1137,7 @@ TEST_F(TestApiSolverBlack, defineFunRecGlobal)
ASSERT_TRUE(d_solver.checkSat().isUnsat());
}
-TEST_F(TestApiSolverBlack, defineFunsRec)
+TEST_F(TestApiBlackSolver, defineFunsRec)
{
Sort uSort = d_solver.mkUninterpretedSort("u");
Sort bvSort = d_solver.mkBitVectorSort(32);
@@ -1198,7 +1198,7 @@ TEST_F(TestApiSolverBlack, defineFunsRec)
CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, defineFunsRecWrongLogic)
+TEST_F(TestApiBlackSolver, defineFunsRecWrongLogic)
{
d_solver.setLogic("QF_BV");
Sort uSort = d_solver.mkUninterpretedSort("u");
@@ -1215,7 +1215,7 @@ TEST_F(TestApiSolverBlack, defineFunsRecWrongLogic)
CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, defineFunsRecGlobal)
+TEST_F(TestApiBlackSolver, defineFunsRecGlobal)
{
Sort bSort = d_solver.getBooleanSort();
Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
@@ -1236,7 +1236,7 @@ TEST_F(TestApiSolverBlack, defineFunsRecGlobal)
ASSERT_TRUE(d_solver.checkSat().isUnsat());
}
-TEST_F(TestApiSolverBlack, uFIteration)
+TEST_F(TestApiBlackSolver, uFIteration)
{
Sort intSort = d_solver.getIntegerSort();
Sort funSort = d_solver.mkFunctionSort({intSort, intSort}, intSort);
@@ -1256,13 +1256,13 @@ TEST_F(TestApiSolverBlack, uFIteration)
}
}
-TEST_F(TestApiSolverBlack, getInfo)
+TEST_F(TestApiBlackSolver, getInfo)
{
ASSERT_NO_THROW(d_solver.getInfo("name"));
ASSERT_THROW(d_solver.getInfo("asdf"), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, getInterpolant)
+TEST_F(TestApiBlackSolver, getInterpolant)
{
d_solver.setOption("produce-interpols", "default");
d_solver.setOption("incremental", "false");
@@ -1290,7 +1290,7 @@ TEST_F(TestApiSolverBlack, getInterpolant)
ASSERT_TRUE(output.getSort().isBoolean());
}
-TEST_F(TestApiSolverBlack, getOp)
+TEST_F(TestApiBlackSolver, getOp)
{
Sort bv32 = d_solver.mkBitVectorSort(32);
Term a = d_solver.mkConst(bv32, "a");
@@ -1332,13 +1332,13 @@ TEST_F(TestApiSolverBlack, getOp)
ASSERT_EQ(listhead.getOp(), Op(&d_solver, APPLY_SELECTOR));
}
-TEST_F(TestApiSolverBlack, getOption)
+TEST_F(TestApiBlackSolver, getOption)
{
ASSERT_NO_THROW(d_solver.getOption("incremental"));
ASSERT_THROW(d_solver.getOption("asdf"), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, getUnsatAssumptions1)
+TEST_F(TestApiBlackSolver, getUnsatAssumptions1)
{
#if IS_PROOFS_BUILD
d_solver.setOption("incremental", "false");
@@ -1347,7 +1347,7 @@ TEST_F(TestApiSolverBlack, getUnsatAssumptions1)
#endif
}
-TEST_F(TestApiSolverBlack, getUnsatAssumptions2)
+TEST_F(TestApiBlackSolver, getUnsatAssumptions2)
{
#if IS_PROOFS_BUILD
d_solver.setOption("incremental", "true");
@@ -1357,7 +1357,7 @@ TEST_F(TestApiSolverBlack, getUnsatAssumptions2)
#endif
}
-TEST_F(TestApiSolverBlack, getUnsatAssumptions3)
+TEST_F(TestApiBlackSolver, getUnsatAssumptions3)
{
#if IS_PROOFS_BUILD
d_solver.setOption("incremental", "true");
@@ -1369,7 +1369,7 @@ TEST_F(TestApiSolverBlack, getUnsatAssumptions3)
#endif
}
-TEST_F(TestApiSolverBlack, getUnsatCore1)
+TEST_F(TestApiBlackSolver, getUnsatCore1)
{
#if IS_PROOFS_BUILD
d_solver.setOption("incremental", "false");
@@ -1379,7 +1379,7 @@ TEST_F(TestApiSolverBlack, getUnsatCore1)
#endif
}
-TEST_F(TestApiSolverBlack, getUnsatCore2)
+TEST_F(TestApiBlackSolver, getUnsatCore2)
{
#if IS_PROOFS_BUILD
d_solver.setOption("incremental", "false");
@@ -1390,7 +1390,7 @@ TEST_F(TestApiSolverBlack, getUnsatCore2)
#endif
}
-TEST_F(TestApiSolverBlack, getUnsatCore3)
+TEST_F(TestApiBlackSolver, getUnsatCore3)
{
#if IS_PROOFS_BUILD
d_solver.setOption("incremental", "true");
@@ -1433,7 +1433,7 @@ TEST_F(TestApiSolverBlack, getUnsatCore3)
#endif
}
-TEST_F(TestApiSolverBlack, getValue1)
+TEST_F(TestApiBlackSolver, getValue1)
{
d_solver.setOption("produce-models", "false");
Term t = d_solver.mkTrue();
@@ -1442,7 +1442,7 @@ TEST_F(TestApiSolverBlack, getValue1)
ASSERT_THROW(d_solver.getValue(t), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, getValue2)
+TEST_F(TestApiBlackSolver, getValue2)
{
d_solver.setOption("produce-models", "true");
Term t = d_solver.mkFalse();
@@ -1451,7 +1451,7 @@ TEST_F(TestApiSolverBlack, getValue2)
ASSERT_THROW(d_solver.getValue(t), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, getValue3)
+TEST_F(TestApiBlackSolver, getValue3)
{
d_solver.setOption("produce-models", "true");
Sort uSort = d_solver.mkUninterpretedSort("u");
@@ -1490,7 +1490,7 @@ TEST_F(TestApiSolverBlack, getValue3)
ASSERT_THROW(slv.getValue(x), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, getQuantifierElimination)
+TEST_F(TestApiBlackSolver, getQuantifierElimination)
{
Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
Term forall =
@@ -1503,7 +1503,7 @@ TEST_F(TestApiSolverBlack, getQuantifierElimination)
ASSERT_NO_THROW(d_solver.getQuantifierElimination(forall));
}
-TEST_F(TestApiSolverBlack, getQuantifierEliminationDisjunct)
+TEST_F(TestApiBlackSolver, getQuantifierEliminationDisjunct)
{
Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
Term forall =
@@ -1518,7 +1518,7 @@ TEST_F(TestApiSolverBlack, getQuantifierEliminationDisjunct)
ASSERT_NO_THROW(d_solver.getQuantifierEliminationDisjunct(forall));
}
-TEST_F(TestApiSolverBlack, declareSeparationHeap)
+TEST_F(TestApiBlackSolver, declareSeparationHeap)
{
d_solver.setLogic("ALL_SUPPORTED");
Sort integer = d_solver.getIntegerSort();
@@ -1548,7 +1548,7 @@ void checkSimpleSeparationConstraints(Solver* solver)
}
} // namespace
-TEST_F(TestApiSolverBlack, getSeparationHeapTerm1)
+TEST_F(TestApiBlackSolver, getSeparationHeapTerm1)
{
d_solver.setLogic("QF_BV");
d_solver.setOption("incremental", "false");
@@ -1558,7 +1558,7 @@ TEST_F(TestApiSolverBlack, getSeparationHeapTerm1)
ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, getSeparationHeapTerm2)
+TEST_F(TestApiBlackSolver, getSeparationHeapTerm2)
{
d_solver.setLogic("ALL_SUPPORTED");
d_solver.setOption("incremental", "false");
@@ -1567,7 +1567,7 @@ TEST_F(TestApiSolverBlack, getSeparationHeapTerm2)
ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, getSeparationHeapTerm3)
+TEST_F(TestApiBlackSolver, getSeparationHeapTerm3)
{
d_solver.setLogic("ALL_SUPPORTED");
d_solver.setOption("incremental", "false");
@@ -1578,7 +1578,7 @@ TEST_F(TestApiSolverBlack, getSeparationHeapTerm3)
ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, getSeparationHeapTerm4)
+TEST_F(TestApiBlackSolver, getSeparationHeapTerm4)
{
d_solver.setLogic("ALL_SUPPORTED");
d_solver.setOption("incremental", "false");
@@ -1589,7 +1589,7 @@ TEST_F(TestApiSolverBlack, getSeparationHeapTerm4)
ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, getSeparationHeapTerm5)
+TEST_F(TestApiBlackSolver, getSeparationHeapTerm5)
{
d_solver.setLogic("ALL_SUPPORTED");
d_solver.setOption("incremental", "false");
@@ -1598,7 +1598,7 @@ TEST_F(TestApiSolverBlack, getSeparationHeapTerm5)
ASSERT_NO_THROW(d_solver.getSeparationHeap());
}
-TEST_F(TestApiSolverBlack, getSeparationNilTerm1)
+TEST_F(TestApiBlackSolver, getSeparationNilTerm1)
{
d_solver.setLogic("QF_BV");
d_solver.setOption("incremental", "false");
@@ -1608,7 +1608,7 @@ TEST_F(TestApiSolverBlack, getSeparationNilTerm1)
ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, getSeparationNilTerm2)
+TEST_F(TestApiBlackSolver, getSeparationNilTerm2)
{
d_solver.setLogic("ALL_SUPPORTED");
d_solver.setOption("incremental", "false");
@@ -1617,7 +1617,7 @@ TEST_F(TestApiSolverBlack, getSeparationNilTerm2)
ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, getSeparationNilTerm3)
+TEST_F(TestApiBlackSolver, getSeparationNilTerm3)
{
d_solver.setLogic("ALL_SUPPORTED");
d_solver.setOption("incremental", "false");
@@ -1628,7 +1628,7 @@ TEST_F(TestApiSolverBlack, getSeparationNilTerm3)
ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, getSeparationNilTerm4)
+TEST_F(TestApiBlackSolver, getSeparationNilTerm4)
{
d_solver.setLogic("ALL_SUPPORTED");
d_solver.setOption("incremental", "false");
@@ -1639,7 +1639,7 @@ TEST_F(TestApiSolverBlack, getSeparationNilTerm4)
ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, getSeparationNilTerm5)
+TEST_F(TestApiBlackSolver, getSeparationNilTerm5)
{
d_solver.setLogic("ALL_SUPPORTED");
d_solver.setOption("incremental", "false");
@@ -1648,7 +1648,7 @@ TEST_F(TestApiSolverBlack, getSeparationNilTerm5)
ASSERT_NO_THROW(d_solver.getSeparationNilTerm());
}
-TEST_F(TestApiSolverBlack, push1)
+TEST_F(TestApiBlackSolver, push1)
{
d_solver.setOption("incremental", "true");
ASSERT_NO_THROW(d_solver.push(1));
@@ -1656,25 +1656,25 @@ TEST_F(TestApiSolverBlack, push1)
ASSERT_THROW(d_solver.setOption("incremental", "true"), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, push2)
+TEST_F(TestApiBlackSolver, push2)
{
d_solver.setOption("incremental", "false");
ASSERT_THROW(d_solver.push(1), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, pop1)
+TEST_F(TestApiBlackSolver, pop1)
{
d_solver.setOption("incremental", "false");
ASSERT_THROW(d_solver.pop(1), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, pop2)
+TEST_F(TestApiBlackSolver, pop2)
{
d_solver.setOption("incremental", "true");
ASSERT_THROW(d_solver.pop(1), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, pop3)
+TEST_F(TestApiBlackSolver, pop3)
{
d_solver.setOption("incremental", "true");
ASSERT_NO_THROW(d_solver.push(1));
@@ -1682,7 +1682,7 @@ TEST_F(TestApiSolverBlack, pop3)
ASSERT_THROW(d_solver.pop(1), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, blockModel1)
+TEST_F(TestApiBlackSolver, blockModel1)
{
d_solver.setOption("produce-models", "true");
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
@@ -1691,7 +1691,7 @@ TEST_F(TestApiSolverBlack, blockModel1)
ASSERT_THROW(d_solver.blockModel(), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, blockModel2)
+TEST_F(TestApiBlackSolver, blockModel2)
{
d_solver.setOption("block-models", "literals");
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
@@ -1700,7 +1700,7 @@ TEST_F(TestApiSolverBlack, blockModel2)
ASSERT_THROW(d_solver.blockModel(), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, blockModel3)
+TEST_F(TestApiBlackSolver, blockModel3)
{
d_solver.setOption("produce-models", "true");
d_solver.setOption("block-models", "literals");
@@ -1709,7 +1709,7 @@ TEST_F(TestApiSolverBlack, blockModel3)
ASSERT_THROW(d_solver.blockModel(), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, blockModel4)
+TEST_F(TestApiBlackSolver, blockModel4)
{
d_solver.setOption("produce-models", "true");
d_solver.setOption("block-models", "literals");
@@ -1719,7 +1719,7 @@ TEST_F(TestApiSolverBlack, blockModel4)
ASSERT_NO_THROW(d_solver.blockModel());
}
-TEST_F(TestApiSolverBlack, blockModelValues1)
+TEST_F(TestApiBlackSolver, blockModelValues1)
{
d_solver.setOption("produce-models", "true");
d_solver.setOption("block-models", "literals");
@@ -1732,7 +1732,7 @@ TEST_F(TestApiSolverBlack, blockModelValues1)
CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, blockModelValues2)
+TEST_F(TestApiBlackSolver, blockModelValues2)
{
d_solver.setOption("produce-models", "true");
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
@@ -1741,7 +1741,7 @@ TEST_F(TestApiSolverBlack, blockModelValues2)
ASSERT_THROW(d_solver.blockModelValues({x}), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, blockModelValues3)
+TEST_F(TestApiBlackSolver, blockModelValues3)
{
d_solver.setOption("block-models", "literals");
Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
@@ -1750,7 +1750,7 @@ TEST_F(TestApiSolverBlack, blockModelValues3)
ASSERT_THROW(d_solver.blockModelValues({x}), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, blockModelValues4)
+TEST_F(TestApiBlackSolver, blockModelValues4)
{
d_solver.setOption("produce-models", "true");
d_solver.setOption("block-models", "literals");
@@ -1759,7 +1759,7 @@ TEST_F(TestApiSolverBlack, blockModelValues4)
ASSERT_THROW(d_solver.blockModelValues({x}), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, blockModelValues5)
+TEST_F(TestApiBlackSolver, blockModelValues5)
{
d_solver.setOption("produce-models", "true");
d_solver.setOption("block-models", "literals");
@@ -1769,7 +1769,7 @@ TEST_F(TestApiSolverBlack, blockModelValues5)
ASSERT_NO_THROW(d_solver.blockModelValues({x}));
}
-TEST_F(TestApiSolverBlack, setInfo)
+TEST_F(TestApiBlackSolver, setInfo)
{
ASSERT_THROW(d_solver.setInfo("cvc4-lagic", "QF_BV"), CVC4ApiException);
ASSERT_THROW(d_solver.setInfo("cvc2-logic", "QF_BV"), CVC4ApiException);
@@ -1795,7 +1795,7 @@ TEST_F(TestApiSolverBlack, setInfo)
ASSERT_THROW(d_solver.setInfo("status", "asdf"), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, simplify)
+TEST_F(TestApiBlackSolver, simplify)
{
ASSERT_THROW(d_solver.simplify(Term()), CVC4ApiException);
@@ -1870,7 +1870,7 @@ TEST_F(TestApiSolverBlack, simplify)
ASSERT_NO_THROW(d_solver.simplify(f2));
}
-TEST_F(TestApiSolverBlack, assertFormula)
+TEST_F(TestApiBlackSolver, assertFormula)
{
ASSERT_NO_THROW(d_solver.assertFormula(d_solver.mkTrue()));
ASSERT_THROW(d_solver.assertFormula(Term()), CVC4ApiException);
@@ -1878,7 +1878,7 @@ TEST_F(TestApiSolverBlack, assertFormula)
ASSERT_THROW(slv.assertFormula(d_solver.mkTrue()), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, checkEntailed)
+TEST_F(TestApiBlackSolver, checkEntailed)
{
d_solver.setOption("incremental", "false");
ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTrue()));
@@ -1887,7 +1887,7 @@ TEST_F(TestApiSolverBlack, checkEntailed)
ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, checkEntailed1)
+TEST_F(TestApiBlackSolver, checkEntailed1)
{
Sort boolSort = d_solver.getBooleanSort();
Term x = d_solver.mkConst(boolSort, "x");
@@ -1902,7 +1902,7 @@ TEST_F(TestApiSolverBlack, checkEntailed1)
ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, checkEntailed2)
+TEST_F(TestApiBlackSolver, checkEntailed2)
{
d_solver.setOption("incremental", "true");
@@ -1951,14 +1951,14 @@ TEST_F(TestApiSolverBlack, checkEntailed2)
ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, checkSat)
+TEST_F(TestApiBlackSolver, checkSat)
{
d_solver.setOption("incremental", "false");
ASSERT_NO_THROW(d_solver.checkSat());
ASSERT_THROW(d_solver.checkSat(), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, checkSatAssuming)
+TEST_F(TestApiBlackSolver, checkSatAssuming)
{
d_solver.setOption("incremental", "false");
ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()));
@@ -1967,7 +1967,7 @@ TEST_F(TestApiSolverBlack, checkSatAssuming)
ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, checkSatAssuming1)
+TEST_F(TestApiBlackSolver, checkSatAssuming1)
{
Sort boolSort = d_solver.getBooleanSort();
Term x = d_solver.mkConst(boolSort, "x");
@@ -1982,7 +1982,7 @@ TEST_F(TestApiSolverBlack, checkSatAssuming1)
ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, checkSatAssuming2)
+TEST_F(TestApiBlackSolver, checkSatAssuming2)
{
d_solver.setOption("incremental", "true");
@@ -2031,7 +2031,7 @@ TEST_F(TestApiSolverBlack, checkSatAssuming2)
ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, setLogic)
+TEST_F(TestApiBlackSolver, setLogic)
{
ASSERT_NO_THROW(d_solver.setLogic("AUFLIRA"));
ASSERT_THROW(d_solver.setLogic("AF_BV"), CVC4ApiException);
@@ -2039,7 +2039,7 @@ TEST_F(TestApiSolverBlack, setLogic)
ASSERT_THROW(d_solver.setLogic("AUFLIRA"), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, setOption)
+TEST_F(TestApiBlackSolver, setOption)
{
ASSERT_NO_THROW(d_solver.setOption("bv-sat-solver", "minisat"));
ASSERT_THROW(d_solver.setOption("bv-sat-solver", "1"), CVC4ApiException);
@@ -2048,7 +2048,7 @@ TEST_F(TestApiSolverBlack, setOption)
CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, resetAssertions)
+TEST_F(TestApiBlackSolver, resetAssertions)
{
d_solver.setOption("incremental", "true");
@@ -2063,7 +2063,7 @@ TEST_F(TestApiSolverBlack, resetAssertions)
d_solver.checkSatAssuming({slt, ule});
}
-TEST_F(TestApiSolverBlack, mkSygusVar)
+TEST_F(TestApiBlackSolver, mkSygusVar)
{
Sort boolSort = d_solver.getBooleanSort();
Sort intSort = d_solver.getIntegerSort();
@@ -2080,7 +2080,7 @@ TEST_F(TestApiSolverBlack, mkSygusVar)
ASSERT_THROW(slv.mkSygusVar(boolSort), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, mkSygusGrammar)
+TEST_F(TestApiBlackSolver, mkSygusGrammar)
{
Term nullTerm;
Term boolTerm = d_solver.mkBoolean(true);
@@ -2101,7 +2101,7 @@ TEST_F(TestApiSolverBlack, mkSygusGrammar)
ASSERT_THROW(slv.mkSygusGrammar({boolVar2}, {intVar}), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, synthFun)
+TEST_F(TestApiBlackSolver, synthFun)
{
Sort null = d_solver.getNullSort();
Sort boolean = d_solver.getBooleanSort();
@@ -2135,7 +2135,7 @@ TEST_F(TestApiSolverBlack, synthFun)
CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, synthInv)
+TEST_F(TestApiBlackSolver, synthInv)
{
Sort boolean = d_solver.getBooleanSort();
Sort integer = d_solver.getIntegerSort();
@@ -2160,7 +2160,7 @@ TEST_F(TestApiSolverBlack, synthInv)
ASSERT_THROW(d_solver.synthInv("i4", {x}, g2), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, addSygusConstraint)
+TEST_F(TestApiBlackSolver, addSygusConstraint)
{
Term nullTerm;
Term boolTerm = d_solver.mkBoolean(true);
@@ -2174,7 +2174,7 @@ TEST_F(TestApiSolverBlack, addSygusConstraint)
ASSERT_THROW(slv.addSygusConstraint(boolTerm), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, addSygusInvConstraint)
+TEST_F(TestApiBlackSolver, addSygusInvConstraint)
{
Sort boolean = d_solver.getBooleanSort();
Sort real = d_solver.getRealSort();
@@ -2244,7 +2244,7 @@ TEST_F(TestApiSolverBlack, addSygusInvConstraint)
CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, getSynthSolution)
+TEST_F(TestApiBlackSolver, getSynthSolution)
{
d_solver.setOption("lang", "sygus2");
d_solver.setOption("incremental", "false");
@@ -2267,7 +2267,7 @@ TEST_F(TestApiSolverBlack, getSynthSolution)
ASSERT_THROW(slv.getSynthSolution(f), CVC4ApiException);
}
-TEST_F(TestApiSolverBlack, getSynthSolutions)
+TEST_F(TestApiBlackSolver, getSynthSolutions)
{
d_solver.setOption("lang", "sygus2");
d_solver.setOption("incremental", "false");
diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp
index 16190b76d..747ddb92d 100644
--- a/test/unit/api/sort_black.cpp
+++ b/test/unit/api/sort_black.cpp
@@ -23,11 +23,11 @@ using namespace api;
namespace test {
-class TestApiSortBlack : public TestApi
+class TestApiBlackSort : public TestApi
{
};
-TEST_F(TestApiSortBlack, getDatatype)
+TEST_F(TestApiBlackSort, getDatatype)
{
// create datatype sort, check should not fail
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
@@ -43,7 +43,7 @@ TEST_F(TestApiSortBlack, getDatatype)
ASSERT_THROW(bvSort.getDatatype(), CVC4ApiException);
}
-TEST_F(TestApiSortBlack, datatypeSorts)
+TEST_F(TestApiBlackSort, datatypeSorts)
{
Sort intSort = d_solver.getIntegerSort();
// create datatype sort to test
@@ -93,7 +93,7 @@ TEST_F(TestApiSortBlack, datatypeSorts)
ASSERT_THROW(booleanSort.getSelectorCodomainSort(), CVC4ApiException);
}
-TEST_F(TestApiSortBlack, instantiate)
+TEST_F(TestApiBlackSort, instantiate)
{
// instantiate parametric datatype, check should not fail
Sort sort = d_solver.mkParamSort("T");
@@ -120,7 +120,7 @@ TEST_F(TestApiSortBlack, instantiate)
CVC4ApiException);
}
-TEST_F(TestApiSortBlack, getFunctionArity)
+TEST_F(TestApiBlackSort, getFunctionArity)
{
Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
d_solver.getIntegerSort());
@@ -129,7 +129,7 @@ TEST_F(TestApiSortBlack, getFunctionArity)
ASSERT_THROW(bvSort.getFunctionArity(), CVC4ApiException);
}
-TEST_F(TestApiSortBlack, getFunctionDomainSorts)
+TEST_F(TestApiBlackSort, getFunctionDomainSorts)
{
Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
d_solver.getIntegerSort());
@@ -138,7 +138,7 @@ TEST_F(TestApiSortBlack, getFunctionDomainSorts)
ASSERT_THROW(bvSort.getFunctionDomainSorts(), CVC4ApiException);
}
-TEST_F(TestApiSortBlack, getFunctionCodomainSort)
+TEST_F(TestApiBlackSort, getFunctionCodomainSort)
{
Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
d_solver.getIntegerSort());
@@ -147,7 +147,7 @@ TEST_F(TestApiSortBlack, getFunctionCodomainSort)
ASSERT_THROW(bvSort.getFunctionCodomainSort(), CVC4ApiException);
}
-TEST_F(TestApiSortBlack, getArrayIndexSort)
+TEST_F(TestApiBlackSort, getArrayIndexSort)
{
Sort elementSort = d_solver.mkBitVectorSort(32);
Sort indexSort = d_solver.mkBitVectorSort(32);
@@ -156,7 +156,7 @@ TEST_F(TestApiSortBlack, getArrayIndexSort)
ASSERT_THROW(indexSort.getArrayIndexSort(), CVC4ApiException);
}
-TEST_F(TestApiSortBlack, getArrayElementSort)
+TEST_F(TestApiBlackSort, getArrayElementSort)
{
Sort elementSort = d_solver.mkBitVectorSort(32);
Sort indexSort = d_solver.mkBitVectorSort(32);
@@ -165,7 +165,7 @@ TEST_F(TestApiSortBlack, getArrayElementSort)
ASSERT_THROW(indexSort.getArrayElementSort(), CVC4ApiException);
}
-TEST_F(TestApiSortBlack, getSetElementSort)
+TEST_F(TestApiBlackSort, getSetElementSort)
{
Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
ASSERT_NO_THROW(setSort.getSetElementSort());
@@ -175,7 +175,7 @@ TEST_F(TestApiSortBlack, getSetElementSort)
ASSERT_THROW(bvSort.getSetElementSort(), CVC4ApiException);
}
-TEST_F(TestApiSortBlack, getBagElementSort)
+TEST_F(TestApiBlackSort, getBagElementSort)
{
Sort bagSort = d_solver.mkBagSort(d_solver.getIntegerSort());
ASSERT_NO_THROW(bagSort.getBagElementSort());
@@ -185,7 +185,7 @@ TEST_F(TestApiSortBlack, getBagElementSort)
ASSERT_THROW(bvSort.getBagElementSort(), CVC4ApiException);
}
-TEST_F(TestApiSortBlack, getSequenceElementSort)
+TEST_F(TestApiBlackSort, getSequenceElementSort)
{
Sort seqSort = d_solver.mkSequenceSort(d_solver.getIntegerSort());
ASSERT_TRUE(seqSort.isSequence());
@@ -195,7 +195,7 @@ TEST_F(TestApiSortBlack, getSequenceElementSort)
ASSERT_THROW(bvSort.getSequenceElementSort(), CVC4ApiException);
}
-TEST_F(TestApiSortBlack, getUninterpretedSortName)
+TEST_F(TestApiBlackSort, getUninterpretedSortName)
{
Sort uSort = d_solver.mkUninterpretedSort("u");
ASSERT_NO_THROW(uSort.getUninterpretedSortName());
@@ -203,7 +203,7 @@ TEST_F(TestApiSortBlack, getUninterpretedSortName)
ASSERT_THROW(bvSort.getUninterpretedSortName(), CVC4ApiException);
}
-TEST_F(TestApiSortBlack, isUninterpretedSortParameterized)
+TEST_F(TestApiBlackSort, isUninterpretedSortParameterized)
{
Sort uSort = d_solver.mkUninterpretedSort("u");
ASSERT_FALSE(uSort.isUninterpretedSortParameterized());
@@ -214,7 +214,7 @@ TEST_F(TestApiSortBlack, isUninterpretedSortParameterized)
ASSERT_THROW(bvSort.isUninterpretedSortParameterized(), CVC4ApiException);
}
-TEST_F(TestApiSortBlack, getUninterpretedSortParamSorts)
+TEST_F(TestApiBlackSort, getUninterpretedSortParamSorts)
{
Sort uSort = d_solver.mkUninterpretedSort("u");
ASSERT_NO_THROW(uSort.getUninterpretedSortParamSorts());
@@ -225,7 +225,7 @@ TEST_F(TestApiSortBlack, getUninterpretedSortParamSorts)
ASSERT_THROW(bvSort.getUninterpretedSortParamSorts(), CVC4ApiException);
}
-TEST_F(TestApiSortBlack, getUninterpretedSortConstructorName)
+TEST_F(TestApiBlackSort, getUninterpretedSortConstructorName)
{
Sort sSort = d_solver.mkSortConstructorSort("s", 2);
ASSERT_NO_THROW(sSort.getSortConstructorName());
@@ -233,7 +233,7 @@ TEST_F(TestApiSortBlack, getUninterpretedSortConstructorName)
ASSERT_THROW(bvSort.getSortConstructorName(), CVC4ApiException);
}
-TEST_F(TestApiSortBlack, getUninterpretedSortConstructorArity)
+TEST_F(TestApiBlackSort, getUninterpretedSortConstructorArity)
{
Sort sSort = d_solver.mkSortConstructorSort("s", 2);
ASSERT_NO_THROW(sSort.getSortConstructorArity());
@@ -241,7 +241,7 @@ TEST_F(TestApiSortBlack, getUninterpretedSortConstructorArity)
ASSERT_THROW(bvSort.getSortConstructorArity(), CVC4ApiException);
}
-TEST_F(TestApiSortBlack, getBVSize)
+TEST_F(TestApiBlackSort, getBVSize)
{
Sort bvSort = d_solver.mkBitVectorSort(32);
ASSERT_NO_THROW(bvSort.getBVSize());
@@ -249,7 +249,7 @@ TEST_F(TestApiSortBlack, getBVSize)
ASSERT_THROW(setSort.getBVSize(), CVC4ApiException);
}
-TEST_F(TestApiSortBlack, getFPExponentSize)
+TEST_F(TestApiBlackSort, getFPExponentSize)
{
if (CVC4::Configuration::isBuiltWithSymFPU())
{
@@ -260,7 +260,7 @@ TEST_F(TestApiSortBlack, getFPExponentSize)
}
}
-TEST_F(TestApiSortBlack, getFPSignificandSize)
+TEST_F(TestApiBlackSort, getFPSignificandSize)
{
if (CVC4::Configuration::isBuiltWithSymFPU())
{
@@ -271,7 +271,7 @@ TEST_F(TestApiSortBlack, getFPSignificandSize)
}
}
-TEST_F(TestApiSortBlack, getDatatypeParamSorts)
+TEST_F(TestApiBlackSort, getDatatypeParamSorts)
{
// create parametric datatype, check should not fail
Sort sort = d_solver.mkParamSort("T");
@@ -295,7 +295,7 @@ TEST_F(TestApiSortBlack, getDatatypeParamSorts)
ASSERT_THROW(dtypeSort.getDatatypeParamSorts(), CVC4ApiException);
}
-TEST_F(TestApiSortBlack, getDatatypeArity)
+TEST_F(TestApiBlackSort, getDatatypeArity)
{
// create datatype sort, check should not fail
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
@@ -311,7 +311,7 @@ TEST_F(TestApiSortBlack, getDatatypeArity)
ASSERT_THROW(bvSort.getDatatypeArity(), CVC4ApiException);
}
-TEST_F(TestApiSortBlack, getTupleLength)
+TEST_F(TestApiBlackSort, getTupleLength)
{
Sort tupleSort = d_solver.mkTupleSort(
{d_solver.getIntegerSort(), d_solver.getIntegerSort()});
@@ -320,7 +320,7 @@ TEST_F(TestApiSortBlack, getTupleLength)
ASSERT_THROW(bvSort.getTupleLength(), CVC4ApiException);
}
-TEST_F(TestApiSortBlack, getTupleSorts)
+TEST_F(TestApiBlackSort, getTupleSorts)
{
Sort tupleSort = d_solver.mkTupleSort(
{d_solver.getIntegerSort(), d_solver.getIntegerSort()});
@@ -329,7 +329,7 @@ TEST_F(TestApiSortBlack, getTupleSorts)
ASSERT_THROW(bvSort.getTupleSorts(), CVC4ApiException);
}
-TEST_F(TestApiSortBlack, sortCompare)
+TEST_F(TestApiBlackSort, sortCompare)
{
Sort boolSort = d_solver.getBooleanSort();
Sort intSort = d_solver.getIntegerSort();
@@ -341,7 +341,7 @@ TEST_F(TestApiSortBlack, sortCompare)
ASSERT_TRUE((intSort > bvSort || intSort == bvSort) == (intSort >= bvSort));
}
-TEST_F(TestApiSortBlack, sortSubtyping)
+TEST_F(TestApiBlackSort, sortSubtyping)
{
Sort intSort = d_solver.getIntegerSort();
Sort realSort = d_solver.getRealSort();
@@ -365,7 +365,7 @@ TEST_F(TestApiSortBlack, sortSubtyping)
ASSERT_FALSE(setSortR.isSubsortOf(setSortI));
}
-TEST_F(TestApiSortBlack, sortScopedToString)
+TEST_F(TestApiBlackSort, sortScopedToString)
{
std::string name = "uninterp-sort";
Sort bvsort8 = d_solver.mkBitVectorSort(8);
diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp
index b6f8fc4ed..d43734295 100644
--- a/test/unit/api/term_black.cpp
+++ b/test/unit/api/term_black.cpp
@@ -20,11 +20,11 @@ using namespace api;
namespace test {
-class TestApiTermBlack : public TestApi
+class TestApiBlackTerm : public TestApi
{
};
-TEST_F(TestApiTermBlack, eq)
+TEST_F(TestApiBlackTerm, eq)
{
Sort uSort = d_solver.mkUninterpretedSort("u");
Term x = d_solver.mkVar(uSort, "x");
@@ -39,7 +39,7 @@ TEST_F(TestApiTermBlack, eq)
ASSERT_TRUE(x != z);
}
-TEST_F(TestApiTermBlack, getId)
+TEST_F(TestApiBlackTerm, getId)
{
Term n;
ASSERT_THROW(n.getId(), CVC4ApiException);
@@ -52,7 +52,7 @@ TEST_F(TestApiTermBlack, getId)
ASSERT_NE(x.getId(), z.getId());
}
-TEST_F(TestApiTermBlack, getKind)
+TEST_F(TestApiBlackTerm, getKind)
{
Sort uSort = d_solver.mkUninterpretedSort("u");
Sort intSort = d_solver.getIntegerSort();
@@ -94,7 +94,7 @@ TEST_F(TestApiTermBlack, getKind)
ASSERT_EQ(ss.getKind(), SEQ_CONCAT);
}
-TEST_F(TestApiTermBlack, getSort)
+TEST_F(TestApiBlackTerm, getSort)
{
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
@@ -139,7 +139,7 @@ TEST_F(TestApiTermBlack, getSort)
ASSERT_EQ(p_f_y.getSort(), boolSort);
}
-TEST_F(TestApiTermBlack, getOp)
+TEST_F(TestApiBlackTerm, getOp)
{
Sort intsort = d_solver.getIntegerSort();
Sort bvsort = d_solver.mkBitVectorSort(8);
@@ -219,7 +219,7 @@ TEST_F(TestApiTermBlack, getOp)
ASSERT_EQ(headTerm, d_solver.mkTerm(headTerm.getOp(), children));
}
-TEST_F(TestApiTermBlack, isNull)
+TEST_F(TestApiBlackTerm, isNull)
{
Term x;
ASSERT_TRUE(x.isNull());
@@ -227,7 +227,7 @@ TEST_F(TestApiTermBlack, isNull)
ASSERT_FALSE(x.isNull());
}
-TEST_F(TestApiTermBlack, notTerm)
+TEST_F(TestApiBlackTerm, notTerm)
{
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
@@ -256,7 +256,7 @@ TEST_F(TestApiTermBlack, notTerm)
ASSERT_NO_THROW(p_f_x.notTerm());
}
-TEST_F(TestApiTermBlack, andTerm)
+TEST_F(TestApiBlackTerm, andTerm)
{
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
@@ -322,7 +322,7 @@ TEST_F(TestApiTermBlack, andTerm)
ASSERT_NO_THROW(p_f_x.andTerm(p_f_x));
}
-TEST_F(TestApiTermBlack, orTerm)
+TEST_F(TestApiBlackTerm, orTerm)
{
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
@@ -388,7 +388,7 @@ TEST_F(TestApiTermBlack, orTerm)
ASSERT_NO_THROW(p_f_x.orTerm(p_f_x));
}
-TEST_F(TestApiTermBlack, xorTerm)
+TEST_F(TestApiBlackTerm, xorTerm)
{
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
@@ -454,7 +454,7 @@ TEST_F(TestApiTermBlack, xorTerm)
ASSERT_NO_THROW(p_f_x.xorTerm(p_f_x));
}
-TEST_F(TestApiTermBlack, eqTerm)
+TEST_F(TestApiBlackTerm, eqTerm)
{
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
@@ -520,7 +520,7 @@ TEST_F(TestApiTermBlack, eqTerm)
ASSERT_NO_THROW(p_f_x.eqTerm(p_f_x));
}
-TEST_F(TestApiTermBlack, impTerm)
+TEST_F(TestApiBlackTerm, impTerm)
{
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
@@ -586,7 +586,7 @@ TEST_F(TestApiTermBlack, impTerm)
ASSERT_NO_THROW(p_f_x.impTerm(p_f_x));
}
-TEST_F(TestApiTermBlack, iteTerm)
+TEST_F(TestApiBlackTerm, iteTerm)
{
Sort bvSort = d_solver.mkBitVectorSort(8);
Sort intSort = d_solver.getIntegerSort();
@@ -630,7 +630,7 @@ TEST_F(TestApiTermBlack, iteTerm)
ASSERT_THROW(p_f_x.iteTerm(x, b), CVC4ApiException);
}
-TEST_F(TestApiTermBlack, termAssignment)
+TEST_F(TestApiBlackTerm, termAssignment)
{
Term t1 = d_solver.mkInteger(1);
Term t2 = t1;
@@ -638,7 +638,7 @@ TEST_F(TestApiTermBlack, termAssignment)
ASSERT_EQ(t1, d_solver.mkInteger(1));
}
-TEST_F(TestApiTermBlack, termCompare)
+TEST_F(TestApiBlackTerm, termCompare)
{
Term t1 = d_solver.mkInteger(1);
Term t2 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
@@ -649,7 +649,7 @@ TEST_F(TestApiTermBlack, termCompare)
ASSERT_TRUE((t1 > t2 || t1 == t2) == (t1 >= t2));
}
-TEST_F(TestApiTermBlack, termChildren)
+TEST_F(TestApiBlackTerm, termChildren)
{
// simple term 2+3
Term two = d_solver.mkInteger(2);
@@ -671,7 +671,7 @@ TEST_F(TestApiTermBlack, termChildren)
ASSERT_THROW(tnull[0], CVC4ApiException);
}
-TEST_F(TestApiTermBlack, getInteger)
+TEST_F(TestApiBlackTerm, getInteger)
{
Term int1 = d_solver.mkInteger("-18446744073709551616");
Term int2 = d_solver.mkInteger("-18446744073709551615");
@@ -749,14 +749,14 @@ TEST_F(TestApiTermBlack, getInteger)
ASSERT_EQ(int11.getInteger(), "18446744073709551616");
}
-TEST_F(TestApiTermBlack, getString)
+TEST_F(TestApiBlackTerm, getString)
{
Term s1 = d_solver.mkString("abcde");
ASSERT_TRUE(s1.isString());
ASSERT_EQ(s1.getString(), L"abcde");
}
-TEST_F(TestApiTermBlack, substitute)
+TEST_F(TestApiBlackTerm, substitute)
{
Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
Term one = d_solver.mkInteger(1);
@@ -807,7 +807,7 @@ TEST_F(TestApiTermBlack, substitute)
ASSERT_THROW(xpx.substitute(es, rs), CVC4ApiException);
}
-TEST_F(TestApiTermBlack, constArray)
+TEST_F(TestApiBlackTerm, constArray)
{
Sort intsort = d_solver.getIntegerSort();
Sort arrsort = d_solver.mkArraySort(intsort, intsort);
@@ -830,7 +830,7 @@ TEST_F(TestApiTermBlack, constArray)
d_solver.mkTerm(STORE, stores, d_solver.mkReal(4), d_solver.mkReal(5));
}
-TEST_F(TestApiTermBlack, constSequenceElements)
+TEST_F(TestApiBlackTerm, constSequenceElements)
{
Sort realsort = d_solver.getRealSort();
Sort seqsort = d_solver.mkSequenceSort(realsort);
@@ -847,7 +847,7 @@ TEST_F(TestApiTermBlack, constSequenceElements)
ASSERT_THROW(su.getConstSequenceElements(), CVC4ApiException);
}
-TEST_F(TestApiTermBlack, termScopedToString)
+TEST_F(TestApiBlackTerm, termScopedToString)
{
Sort intsort = d_solver.getIntegerSort();
Term x = d_solver.mkConst(intsort, "x");
diff --git a/test/unit/expr/node_black.cpp b/test/unit/expr/node_black.cpp
index 88406f6bc..33576b2cc 100644
--- a/test/unit/expr/node_black.cpp
+++ b/test/unit/expr/node_black.cpp
@@ -32,7 +32,7 @@
namespace CVC4 {
-using namespace CVC4::kind;
+using namespace kind;
namespace test {
diff --git a/test/unit/expr/node_builder_black.cpp b/test/unit/expr/node_builder_black.cpp
index 3ba78950b..20f907e18 100644
--- a/test/unit/expr/node_builder_black.cpp
+++ b/test/unit/expr/node_builder_black.cpp
@@ -32,11 +32,11 @@
namespace CVC4 {
-using namespace CVC4::kind;
+using namespace kind;
namespace test {
-class TestNodeBuilderBlackNode : public TestNodeBlack
+class TestNodeBlackNodeBuilder : public TestNodeBlack
{
protected:
template <unsigned N>
@@ -51,7 +51,7 @@ class TestNodeBuilderBlackNode : public TestNodeBlack
};
/** Tests just constructors. No modification is done to the node. */
-TEST_F(TestNodeBuilderBlackNode, ctors)
+TEST_F(TestNodeBlackNodeBuilder, ctors)
{
/* Default size tests. */
NodeBuilder<> def;
@@ -153,13 +153,13 @@ TEST_F(TestNodeBuilderBlackNode, ctors)
#endif
}
-TEST_F(TestNodeBuilderBlackNode, dtor)
+TEST_F(TestNodeBlackNodeBuilder, dtor)
{
NodeBuilder<K>* nb = new NodeBuilder<K>();
delete nb;
}
-TEST_F(TestNodeBuilderBlackNode, begin_end)
+TEST_F(TestNodeBlackNodeBuilder, begin_end)
{
/* Test begin() and end() without resizing. */
NodeBuilder<K> ws(d_specKind);
@@ -208,7 +208,7 @@ TEST_F(TestNodeBuilderBlackNode, begin_end)
ASSERT_EQ(smaller_citer, smaller.end());
}
-TEST_F(TestNodeBuilderBlackNode, iterator)
+TEST_F(TestNodeBlackNodeBuilder, iterator)
{
NodeBuilder<> b;
Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode);
@@ -234,7 +234,7 @@ TEST_F(TestNodeBuilderBlackNode, iterator)
}
}
-TEST_F(TestNodeBuilderBlackNode, getKind)
+TEST_F(TestNodeBlackNodeBuilder, getKind)
{
NodeBuilder<> noKind;
ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND);
@@ -259,7 +259,7 @@ TEST_F(TestNodeBuilderBlackNode, getKind)
ASSERT_EQ(spec.getKind(), PLUS);
}
-TEST_F(TestNodeBuilderBlackNode, getNumChildren)
+TEST_F(TestNodeBlackNodeBuilder, getNumChildren)
{
Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode));
@@ -294,7 +294,7 @@ TEST_F(TestNodeBuilderBlackNode, getNumChildren)
#endif
}
-TEST_F(TestNodeBuilderBlackNode, operator_square)
+TEST_F(TestNodeBlackNodeBuilder, operator_square)
{
NodeBuilder<> arr(d_specKind);
@@ -343,7 +343,7 @@ TEST_F(TestNodeBuilderBlackNode, operator_square)
#endif
}
-TEST_F(TestNodeBuilderBlackNode, clear)
+TEST_F(TestNodeBlackNodeBuilder, clear)
{
NodeBuilder<> nb;
@@ -394,7 +394,7 @@ TEST_F(TestNodeBuilderBlackNode, clear)
#endif
}
-TEST_F(TestNodeBuilderBlackNode, operator_stream_insertion_kind)
+TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind)
{
#ifdef CVC4_ASSERTIONS
NodeBuilder<> spec(d_specKind);
@@ -443,7 +443,7 @@ TEST_F(TestNodeBuilderBlackNode, operator_stream_insertion_kind)
d_specKind);
}
-TEST_F(TestNodeBuilderBlackNode, operator_stream_insertion_node)
+TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_node)
{
NodeBuilder<K> nb(d_specKind);
ASSERT_EQ(nb.getKind(), d_specKind);
@@ -471,7 +471,7 @@ TEST_F(TestNodeBuilderBlackNode, operator_stream_insertion_node)
ASSERT_NE(overflow.begin(), overflow.end());
}
-TEST_F(TestNodeBuilderBlackNode, append)
+TEST_F(TestNodeBlackNodeBuilder, append)
{
Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode);
Node y = d_nodeManager->mkSkolem("y", *d_boolTypeNode);
@@ -536,7 +536,7 @@ TEST_F(TestNodeBuilderBlackNode, append)
ASSERT_EQ(b[8], m);
}
-TEST_F(TestNodeBuilderBlackNode, operator_node_cast)
+TEST_F(TestNodeBlackNodeBuilder, operator_node_cast)
{
NodeBuilder<K> implicit(d_specKind);
NodeBuilder<K> explic(d_specKind);
@@ -558,7 +558,7 @@ TEST_F(TestNodeBuilderBlackNode, operator_node_cast)
#endif
}
-TEST_F(TestNodeBuilderBlackNode, leftist_building)
+TEST_F(TestNodeBlackNodeBuilder, leftist_building)
{
NodeBuilder<> nb;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback