[clang][dataflow] Make SolverTest a type-parameterized test.
#91455
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This allows the tests to be run against any implementation of `Solver` instead of begin specific to `WatchedLiteralsSolver` as they currently are.
llvmbot
added
clang
|
@llvm/pr-subscribers-clang Author: None (martinboehme) ChangesThis allows the tests to be run against any implementation of Full diff: https://github.com/llvm/llvm-project/pull/91455.diff 5 Files Affected:
diff --git a/clang/docs/tools/clang-formatted-files.txt b/clang/docs/tools/clang-formatted-files.txt
index 2252d0ccde96d..eaeadf2656b0b 100644
--- a/clang/docs/tools/clang-formatted-files.txt
+++ b/clang/docs/tools/clang-formatted-files.txt
@@ -632,11 +632,12 @@ clang/unittests/Analysis/FlowSensitive/MapLatticeTest.cpp
clang/unittests/Analysis/FlowSensitive/MatchSwitchTest.cpp
clang/unittests/Analysis/FlowSensitive/MultiVarConstantPropagationTest.cpp
clang/unittests/Analysis/FlowSensitive/SingleVarConstantPropagationTest.cpp
-clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+clang/unittests/Analysis/FlowSensitive/SolverTest.h
clang/unittests/Analysis/FlowSensitive/TestingSupport.cpp
clang/unittests/Analysis/FlowSensitive/TestingSupport.h
clang/unittests/Analysis/FlowSensitive/TestingSupportTest.cpp
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
+clang/unittests/Analysis/FlowSensitive/WatchedLiteralsSolverTest.cpp
clang/unittests/AST/ASTImporterFixtures.cpp
clang/unittests/AST/ASTImporterFixtures.h
clang/unittests/AST/ASTImporterObjCTest.cpp
diff --git a/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt b/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
index 94160d949637c..cfabb80576bc1 100644
--- a/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
+++ b/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
@@ -19,7 +19,6 @@ add_clang_unittest(ClangAnalysisFlowSensitiveTests
SignAnalysisTest.cpp
SimplifyConstraintsTest.cpp
SingleVarConstantPropagationTest.cpp
- SolverTest.cpp
TestingSupport.cpp
TestingSupportTest.cpp
TransferBranchTest.cpp
@@ -27,6 +26,7 @@ add_clang_unittest(ClangAnalysisFlowSensitiveTests
TypeErasedDataflowAnalysisTest.cpp
UncheckedOptionalAccessModelTest.cpp
ValueTest.cpp
+ WatchedLiteralsSolverTest.cpp
)
clang_target_link_libraries(ClangAnalysisFlowSensitiveTests
diff --git a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/SolverTest.h
similarity index 62%
rename from clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
rename to clang/unittests/Analysis/FlowSensitive/SolverTest.h
index 71f6da93594e3..b375344381213 100644
--- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.h
@@ -1,4 +1,4 @@
-//===- unittests/Analysis/FlowSensitive/SolverTest.cpp --------------------===//
+//===--- SolverTest.h - Type-parameterized test for solvers ---------------===//
//
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
// See https://llvm.org/LICENSE.txt for license information.
@@ -6,43 +6,53 @@
//
//===----------------------------------------------------------------------===//
-#include <utility>
+#ifndef LLVM_CLANG_ANALYSIS_FLOW_SENSITIVE_SOLVER_TEST_H_
+#define LLVM_CLANG_ANALYSIS_FLOW_SENSITIVE_SOLVER_TEST_H_
#include "TestingSupport.h"
-#include "clang/Analysis/FlowSensitive/Arena.h"
-#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/Solver.h"
-#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
-#include "clang/Basic/LLVM.h"
-#include "llvm/ADT/ArrayRef.h"
#include "gmock/gmock.h"
#include "gtest/gtest.h"
-#include <vector>
+
+namespace clang::dataflow::test {
namespace {
-using namespace clang;
-using namespace dataflow;
+constexpr auto AssignedTrue = Solver::Result::Assignment::AssignedTrue;
+constexpr auto AssignedFalse = Solver::Result::Assignment::AssignedFalse;
-using test::ConstraintContext;
-using test::parseFormulas;
using testing::_;
using testing::AnyOf;
using testing::Pair;
using testing::UnorderedElementsAre;
-constexpr auto AssignedTrue = Solver::Result::Assignment::AssignedTrue;
-constexpr auto AssignedFalse = Solver::Result::Assignment::AssignedFalse;
+} // namespace
-// Checks if the conjunction of `Vals` is satisfiable and returns the
-// corresponding result.
-Solver::Result solve(llvm::ArrayRef<const Formula *> Vals) {
- return WatchedLiteralsSolver().solve(Vals);
-}
+/// Type-parameterized test for implementations of the `Solver` interface.
+/// To use:
+/// 1. Implement a specialization of `createSolverWithLowTimeout()` for the
+/// solver you want to test.
+/// 2. Instantiate the test suite for the solver you want to test using
+/// `INSTANTIATE_TYPED_TEST_SUITE_P()`.
+/// See WatchedLiteralsSolverTest.cpp for an example.
+template <typename SolverT> class SolverTest : public ::testing::Test {
+protected:
+ // Checks if the conjunction of `Vals` is satisfiable and returns the
+ // corresponding result.
+ Solver::Result solve(llvm::ArrayRef<const Formula *> Vals) {
+ return SolverT().solve(Vals);
+ }
+
+ // Create a specialization for the solver type to test.
+ SolverT createSolverWithLowTimeout();
+};
+
+TYPED_TEST_SUITE_P(SolverTest);
MATCHER(unsat, "") {
return arg.getStatus() == Solver::Result::Status::Unsatisfiable;
}
+
MATCHER_P(sat, SolutionMatcher,
"is satisfiable, where solution " +
(testing::DescribeMatcher<
@@ -55,57 +65,57 @@ MATCHER_P(sat, SolutionMatcher,
result_listener);
}
-TEST(SolverTest, Var) {
+TYPED_TEST_P(SolverTest, Var) {
ConstraintContext Ctx;
auto X = Ctx.atom();
// X
- EXPECT_THAT(solve({X}),
+ EXPECT_THAT(this->solve({X}),
sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue))));
}
-TEST(SolverTest, NegatedVar) {
+TYPED_TEST_P(SolverTest, NegatedVar) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto NotX = Ctx.neg(X);
// !X
- EXPECT_THAT(solve({NotX}),
+ EXPECT_THAT(this->solve({NotX}),
sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse))));
}
-TEST(SolverTest, UnitConflict) {
+TYPED_TEST_P(SolverTest, UnitConflict) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto NotX = Ctx.neg(X);
// X ^ !X
- EXPECT_THAT(solve({X, NotX}), unsat());
+ EXPECT_THAT(this->solve({X, NotX}), unsat());
}
-TEST(SolverTest, DistinctVars) {
+TYPED_TEST_P(SolverTest, DistinctVars) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto Y = Ctx.atom();
auto NotY = Ctx.neg(Y);
// X ^ !Y
- EXPECT_THAT(solve({X, NotY}),
+ EXPECT_THAT(this->solve({X, NotY}),
sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
Pair(Y->getAtom(), AssignedFalse))));
}
-TEST(SolverTest, DoubleNegation) {
+TYPED_TEST_P(SolverTest, DoubleNegation) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto NotX = Ctx.neg(X);
auto NotNotX = Ctx.neg(NotX);
// !!X ^ !X
- EXPECT_THAT(solve({NotNotX, NotX}), unsat());
+ EXPECT_THAT(this->solve({NotNotX, NotX}), unsat());
}
-TEST(SolverTest, NegatedDisjunction) {
+TYPED_TEST_P(SolverTest, NegatedDisjunction) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto Y = Ctx.atom();
@@ -113,10 +123,10 @@ TEST(SolverTest, NegatedDisjunction) {
auto NotXOrY = Ctx.neg(XOrY);
// !(X v Y) ^ (X v Y)
- EXPECT_THAT(solve({NotXOrY, XOrY}), unsat());
+ EXPECT_THAT(this->solve({NotXOrY, XOrY}), unsat());
}
-TEST(SolverTest, NegatedConjunction) {
+TYPED_TEST_P(SolverTest, NegatedConjunction) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto Y = Ctx.atom();
@@ -124,48 +134,48 @@ TEST(SolverTest, NegatedConjunction) {
auto NotXAndY = Ctx.neg(XAndY);
// !(X ^ Y) ^ (X ^ Y)
- EXPECT_THAT(solve({NotXAndY, XAndY}), unsat());
+ EXPECT_THAT(this->solve({NotXAndY, XAndY}), unsat());
}
-TEST(SolverTest, DisjunctionSameVarWithNegation) {
+TYPED_TEST_P(SolverTest, DisjunctionSameVarWithNegation) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto NotX = Ctx.neg(X);
auto XOrNotX = Ctx.disj(X, NotX);
// X v !X
- EXPECT_THAT(solve({XOrNotX}), sat(_));
+ EXPECT_THAT(this->solve({XOrNotX}), sat(_));
}
-TEST(SolverTest, DisjunctionSameVar) {
+TYPED_TEST_P(SolverTest, DisjunctionSameVar) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto XOrX = Ctx.disj(X, X);
// X v X
- EXPECT_THAT(solve({XOrX}), sat(_));
+ EXPECT_THAT(this->solve({XOrX}), sat(_));
}
-TEST(SolverTest, ConjunctionSameVarsConflict) {
+TYPED_TEST_P(SolverTest, ConjunctionSameVarsConflict) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto NotX = Ctx.neg(X);
auto XAndNotX = Ctx.conj(X, NotX);
// X ^ !X
- EXPECT_THAT(solve({XAndNotX}), unsat());
+ EXPECT_THAT(this->solve({XAndNotX}), unsat());
}
-TEST(SolverTest, ConjunctionSameVar) {
+TYPED_TEST_P(SolverTest, ConjunctionSameVar) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto XAndX = Ctx.conj(X, X);
// X ^ X
- EXPECT_THAT(solve({XAndX}), sat(_));
+ EXPECT_THAT(this->solve({XAndX}), sat(_));
}
-TEST(SolverTest, PureVar) {
+TYPED_TEST_P(SolverTest, PureVar) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto Y = Ctx.atom();
@@ -175,12 +185,12 @@ TEST(SolverTest, PureVar) {
auto NotXOrNotY = Ctx.disj(NotX, NotY);
// (!X v Y) ^ (!X v !Y)
- EXPECT_THAT(solve({NotXOrY, NotXOrNotY}),
+ EXPECT_THAT(this->solve({NotXOrY, NotXOrNotY}),
sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
Pair(Y->getAtom(), _))));
}
-TEST(SolverTest, MustAssumeVarIsFalse) {
+TYPED_TEST_P(SolverTest, MustAssumeVarIsFalse) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto Y = Ctx.atom();
@@ -191,12 +201,12 @@ TEST(SolverTest, MustAssumeVarIsFalse) {
auto NotXOrNotY = Ctx.disj(NotX, NotY);
// (X v Y) ^ (!X v Y) ^ (!X v !Y)
- EXPECT_THAT(solve({XOrY, NotXOrY, NotXOrNotY}),
+ EXPECT_THAT(this->solve({XOrY, NotXOrY, NotXOrNotY}),
sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
Pair(Y->getAtom(), AssignedTrue))));
}
-TEST(SolverTest, DeepConflict) {
+TYPED_TEST_P(SolverTest, DeepConflict) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto Y = Ctx.atom();
@@ -208,10 +218,10 @@ TEST(SolverTest, DeepConflict) {
auto XOrNotY = Ctx.disj(X, NotY);
// (X v Y) ^ (!X v Y) ^ (!X v !Y) ^ (X v !Y)
- EXPECT_THAT(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}), unsat());
+ EXPECT_THAT(this->solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}), unsat());
}
-TEST(SolverTest, IffIsEquivalentToDNF) {
+TYPED_TEST_P(SolverTest, IffIsEquivalentToDNF) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto Y = Ctx.atom();
@@ -222,19 +232,19 @@ TEST(SolverTest, IffIsEquivalentToDNF) {
auto NotEquivalent = Ctx.neg(Ctx.iff(XIffY, XIffYDNF));
// !((X <=> Y) <=> ((X ^ Y) v (!X ^ !Y)))
- EXPECT_THAT(solve({NotEquivalent}), unsat());
+ EXPECT_THAT(this->solve({NotEquivalent}), unsat());
}
-TEST(SolverTest, IffSameVars) {
+TYPED_TEST_P(SolverTest, IffSameVars) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto XEqX = Ctx.iff(X, X);
// X <=> X
- EXPECT_THAT(solve({XEqX}), sat(_));
+ EXPECT_THAT(this->solve({XEqX}), sat(_));
}
-TEST(SolverTest, IffDistinctVars) {
+TYPED_TEST_P(SolverTest, IffDistinctVars) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto Y = Ctx.atom();
@@ -242,36 +252,36 @@ TEST(SolverTest, IffDistinctVars) {
// X <=> Y
EXPECT_THAT(
- solve({XEqY}),
+ this->solve({XEqY}),
sat(AnyOf(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
Pair(Y->getAtom(), AssignedTrue)),
UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
Pair(Y->getAtom(), AssignedFalse)))));
}
-TEST(SolverTest, IffWithUnits) {
+TYPED_TEST_P(SolverTest, IffWithUnits) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto Y = Ctx.atom();
auto XEqY = Ctx.iff(X, Y);
// (X <=> Y) ^ X ^ Y
- EXPECT_THAT(solve({XEqY, X, Y}),
+ EXPECT_THAT(this->solve({XEqY, X, Y}),
sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
Pair(Y->getAtom(), AssignedTrue))));
}
-TEST(SolverTest, IffWithUnitsConflict) {
+TYPED_TEST_P(SolverTest, IffWithUnitsConflict) {
Arena A;
auto Constraints = parseFormulas(A, R"(
(V0 = V1)
V0
!V1
)");
- EXPECT_THAT(solve(Constraints), unsat());
+ EXPECT_THAT(this->solve(Constraints), unsat());
}
-TEST(SolverTest, IffTransitiveConflict) {
+TYPED_TEST_P(SolverTest, IffTransitiveConflict) {
Arena A;
auto Constraints = parseFormulas(A, R"(
(V0 = V1)
@@ -279,63 +289,63 @@ TEST(SolverTest, IffTransitiveConflict) {
V2
!V0
)");
- EXPECT_THAT(solve(Constraints), unsat());
+ EXPECT_THAT(this->solve(Constraints), unsat());
}
-TEST(SolverTest, DeMorgan) {
+TYPED_TEST_P(SolverTest, DeMorgan) {
Arena A;
auto Constraints = parseFormulas(A, R"(
(!(V0 | V1) = (!V0 & !V1))
(!(V2 & V3) = (!V2 | !V3))
)");
- EXPECT_THAT(solve(Constraints), sat(_));
+ EXPECT_THAT(this->solve(Constraints), sat(_));
}
-TEST(SolverTest, RespectsAdditionalConstraints) {
+TYPED_TEST_P(SolverTest, RespectsAdditionalConstraints) {
Arena A;
auto Constraints = parseFormulas(A, R"(
(V0 = V1)
V0
!V1
)");
- EXPECT_THAT(solve(Constraints), unsat());
+ EXPECT_THAT(this->solve(Constraints), unsat());
}
-TEST(SolverTest, ImplicationIsEquivalentToDNF) {
+TYPED_TEST_P(SolverTest, ImplicationIsEquivalentToDNF) {
Arena A;
auto Constraints = parseFormulas(A, R"(
!((V0 => V1) = (!V0 | V1))
)");
- EXPECT_THAT(solve(Constraints), unsat());
+ EXPECT_THAT(this->solve(Constraints), unsat());
}
-TEST(SolverTest, ImplicationConflict) {
+TYPED_TEST_P(SolverTest, ImplicationConflict) {
Arena A;
auto Constraints = parseFormulas(A, R"(
(V0 => V1)
(V0 & !V1)
)");
- EXPECT_THAT(solve(Constraints), unsat());
+ EXPECT_THAT(this->solve(Constraints), unsat());
}
-TEST(SolverTest, ReachedLimitsReflectsTimeouts) {
+TYPED_TEST_P(SolverTest, ReachedLimitsReflectsTimeouts) {
Arena A;
auto Constraints = parseFormulas(A, R"(
(!(V0 | V1) = (!V0 & !V1))
(!(V2 & V3) = (!V2 & !V3))
)");
- WatchedLiteralsSolver solver(10);
+ TypeParam solver = this->createSolverWithLowTimeout();
ASSERT_EQ(solver.solve(Constraints).getStatus(),
Solver::Result::Status::TimedOut);
EXPECT_TRUE(solver.reachedLimit());
}
-TEST(SolverTest, SimpleButLargeContradiction) {
+TYPED_TEST_P(SolverTest, SimpleButLargeContradiction) {
// This test ensures that the solver takes a short-cut on known
// contradictory inputs, without using max_iterations. At the time
// this test is added, formulas that are easily recognized to be
// contradictory at CNF construction time would lead to timeout.
- WatchedLiteralsSolver solver(10);
+ TypeParam solver = this->createSolverWithLowTimeout();
ConstraintContext Ctx;
auto first = Ctx.atom();
auto last = first;
@@ -358,4 +368,16 @@ TEST(SolverTest, SimpleButLargeContradiction) {
EXPECT_FALSE(solver.reachedLimit());
}
-} // namespace
+REGISTER_TYPED_TEST_SUITE_P(
+ SolverTest, Var, NegatedVar, UnitConflict, DistinctVars, DoubleNegation,
+ NegatedDisjunction, NegatedConjunction, DisjunctionSameVarWithNegation,
+ DisjunctionSameVar, ConjunctionSameVarsConflict, ConjunctionSameVar,
+ PureVar, MustAssumeVarIsFalse, DeepConflict, IffIsEquivalentToDNF,
+ IffSameVars, IffDistinctVars, IffWithUnits, IffWithUnitsConflict,
+ IffTransitiveConflict, DeMorgan, RespectsAdditionalConstraints,
+ ImplicationIsEquivalentToDNF, ImplicationConflict,
+ ReachedLimitsReflectsTimeouts, SimpleButLargeContradiction);
+
+} // namespace clang::dataflow::test
+
+#endif // LLVM_CLANG_ANALYSIS_FLOW_SENSITIVE_TESTING_SUPPORT_H_
diff --git a/clang/unittests/Analysis/FlowSensitive/WatchedLiteralsSolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/WatchedLiteralsSolverTest.cpp
new file mode 100644
index 0000000000000..d83ea403511af
--- /dev/null
+++ b/clang/unittests/Analysis/FlowSensitive/WatchedLiteralsSolverTest.cpp
@@ -0,0 +1,26 @@
+//===- unittests/Analysis/FlowSensitive/SolverTest.cpp --------------------===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "SolverTest.h"
+
+namespace clang::dataflow::test {
+
+template <>
+WatchedLiteralsSolver
+SolverTest<WatchedLiteralsSolver>::createSolverWithLowTimeout() {
+ return WatchedLiteralsSolver(10);
+}
+
+namespace {
+
+INSTANTIATE_TYPED_TEST_SUITE_P(WatchedLiteralsSolverTest, SolverTest,
+ WatchedLiteralsSolver);
+
+} // namespace
+} // namespace clang::dataflow::test
diff --git a/llvm/utils/gn/secondary/clang/unittests/Analysis/FlowSensitive/BUILD.gn b/llvm/utils/gn/secondary/clang/unittests/Analysis/FlowSensitive/BUILD.gn
index df5b4587bf1c1..e16ca31b81a8d 100644
--- a/llvm/utils/gn/secondary/clang/unittests/Analysis/FlowSensitive/BUILD.gn
+++ b/llvm/utils/gn/secondary/clang/unittests/Analysis/FlowSensitive/BUILD.gn
@@ -33,7 +33,6 @@ unittest("ClangAnalysisFlowSensitiveTests") {
"SignAnalysisTest.cpp",
"SimplifyConstraintsTest.cpp",
"SingleVarConstantPropagationTest.cpp",
- "SolverTest.cpp",
"TestingSupport.cpp",
"TestingSupportTest.cpp",
"TransferBranchTest.cpp",
@@ -41,5 +40,6 @@ unittest("ClangAnalysisFlowSensitiveTests") {
"TypeErasedDataflowAnalysisTest.cpp",
"UncheckedOptionalAccessModelTest.cpp",
"ValueTest.cpp",
+ "WatchedLiteralsSolverTest.cpp",
]
}
|
ymand
approved these changes
May 8, 2024
|
CI failure looks unrelated. |
chapuni
added a commit
that referenced
this pull request
May 10, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This allows the tests to be run against any implementation of
Solverinsteadof begin specific to
WatchedLiteralsSolveras they currently are.