From a1b73df93e5a2fac4a7ac87fb1753c4eb518c8c0 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Wed, 27 Mar 2019 11:33:07 +0000 Subject: Separate constraint set and constraint manager --- unittests/Solver/SolverTest.cpp | 7 ++++--- unittests/Solver/Z3SolverTest.cpp | 4 +++- 2 files changed, 7 insertions(+), 4 deletions(-) (limited to 'unittests') diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp index 9c1089e0..d5d207a0 100644 --- a/unittests/Solver/SolverTest.cpp +++ b/unittests/Solver/SolverTest.cpp @@ -80,9 +80,10 @@ void testOperation(Solver &solver, ref queryExpr = EqExpr::create(fullySymbolicExpr, partiallyConstantExpr); - - ConstraintManager constraints; - constraints.addConstraint(expr); + + ConstraintSet constraints; + ConstraintManager cm(constraints); + cm.addConstraint(expr); bool res; bool success = solver.mustBeTrue(Query(constraints, queryExpr), res); EXPECT_EQ(true, success) << "Constraint solving failed"; diff --git a/unittests/Solver/Z3SolverTest.cpp b/unittests/Solver/Z3SolverTest.cpp index a3aa52f6..eab43d79 100644 --- a/unittests/Solver/Z3SolverTest.cpp +++ b/unittests/Solver/Z3SolverTest.cpp @@ -36,7 +36,9 @@ protected: }; TEST_F(Z3SolverTest, GetConstraintLog) { - ConstraintManager Constraints; + ConstraintSet Constraints; + ConstraintManager cm(Constraints); + const std::vector ConstantValues{1, 2, 3, 4}; std::vector> ConstantExpressions; -- cgit 1.4.1