diff --git a/src/solver/MathsatSmtSolver.cpp b/src/solver/MathsatSmtSolver.cpp index 2fc22103a..6be855dae 100644 --- a/src/solver/MathsatSmtSolver.cpp +++ b/src/solver/MathsatSmtSolver.cpp @@ -1,7 +1,6 @@ #include "src/solver/MathsatSmtSolver.h" -#include - +#include "src/exceptions/NotSupportedException.h" #include "src/exceptions/UnexpectedException.h" #include "src/exceptions/InvalidStateException.h" @@ -44,7 +43,7 @@ namespace storm { #ifdef STORM_HAVE_MSAT msat_push_backtrack_point(env); #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); #endif } @@ -52,16 +51,20 @@ namespace storm { #ifdef STORM_HAVE_MSAT msat_pop_backtrack_point(env); #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); #endif } + void MathsatSmtSolver::pop(uint_fast64_t n) { + SmtSolver::pop(n); + } + void MathsatSmtSolver::reset() { #ifdef STORM_HAVE_MSAT msat_reset_env(env); #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); #endif } @@ -70,7 +73,7 @@ namespace storm { #ifdef STORM_HAVE_MSAT msat_assert_formula(env, expressionAdapter->translateExpression(e, true)); #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); #endif } @@ -91,7 +94,7 @@ namespace storm { } return this->lastResult; #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); #endif } @@ -119,7 +122,7 @@ namespace storm { } return this->lastResult; #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); #endif } @@ -147,18 +150,17 @@ namespace storm { } return this->lastResult; #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); #endif } storm::expressions::SimpleValuation MathsatSmtSolver::getModel() { #ifdef STORM_HAVE_MSAT - - STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Requested Model but last check result was not SAT."); + STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable."); return this->convertMathsatModelToValuation(); #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); #endif } @@ -166,27 +168,25 @@ namespace storm { storm::expressions::SimpleValuation MathsatSmtSolver::convertMathsatModelToValuation() { storm::expressions::SimpleValuation stormModel; - msat_model_iterator model = msat_create_model_iterator(env); - - STORM_LOG_THROW(!MSAT_ERROR_MODEL_ITERATOR(model), storm::exceptions::UnexpectedException, "MathSat returned an illegal model iterator."); + msat_model_iterator modelIterator = msat_create_model_iterator(env); + STORM_LOG_THROW(!MSAT_ERROR_MODEL_ITERATOR(modelIterator), storm::exceptions::UnexpectedException, "MathSat returned an illegal model iterator."); - while (msat_model_iterator_has_next(model)) { + while (msat_model_iterator_has_next(modelIterator)) { msat_term t, v; - msat_model_iterator_next(model, &t, &v); + msat_model_iterator_next(modelIterator, &t, &v); - storm::expressions::Expression var_i_interp = this->expressionAdapter->translateTerm(v); + storm::expressions::Expression variableIInterpretation = this->expressionAdapter->translateTerm(v); char* name = msat_decl_get_name(msat_term_get_decl(t)); - switch (var_i_interp.getReturnType()) { + switch (variableIInterpretation.getReturnType()) { case storm::expressions::ExpressionReturnType::Bool: - - stormModel.addBooleanIdentifier(std::string(name), var_i_interp.evaluateAsBool()); + stormModel.addBooleanIdentifier(std::string(name), variableIInterpretation.evaluateAsBool()); break; case storm::expressions::ExpressionReturnType::Int: - stormModel.addIntegerIdentifier(std::string(name), var_i_interp.evaluateAsInt()); + stormModel.addIntegerIdentifier(std::string(name), variableIInterpretation.evaluateAsInt()); break; case storm::expressions::ExpressionReturnType::Double: - stormModel.addDoubleIdentifier(std::string(name), var_i_interp.evaluateAsDouble()); + stormModel.addDoubleIdentifier(std::string(name), variableIInterpretation.evaluateAsDouble()); break; default: STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Variable interpretation in model is not of type bool, int or double.") @@ -204,99 +204,140 @@ namespace storm { std::vector MathsatSmtSolver::allSat(std::vector const& important) { #ifdef STORM_HAVE_MSAT - std::vector valuations; - - this->allSat(important, [&valuations](storm::expressions::SimpleValuation& valuation) -> bool {valuations.push_back(valuation); return true; }); - + this->allSat(important, [&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; }); return valuations; - #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); #endif } #ifdef STORM_HAVE_MSAT - class AllsatValuationsCallbackUserData { + class AllsatValuationCallbackUserData { public: - AllsatValuationsCallbackUserData(msat_env &env, - storm::adapters::MathsatExpressionAdapter &adapter, - std::function const& callback) - : env(env), adapter(adapter), callback(callback) { + AllsatValuationCallbackUserData(msat_env& env, std::function const& callback) : env(env), callback(callback) { + // Intentionally left empty. } - msat_env &env; - storm::adapters::MathsatExpressionAdapter &adapter; + + static int allsatValuationsCallback(msat_term* model, int size, void* user_data) { + AllsatValuationCallbackUserData* user = reinterpret_cast(user_data); + + storm::expressions::SimpleValuation valuation; + for (int i = 0; i < size; ++i) { + bool currentTermValue = true; + msat_term currentTerm = model[i]; + if (msat_term_is_not(user->env, currentTerm)) { + currentTerm = msat_term_get_arg(currentTerm, 0); + currentTermValue = false; + } + char* name = msat_decl_get_name(msat_term_get_decl(currentTerm)); + std::string nameAsString(name); + msat_free(name); + valuation.addBooleanIdentifier(nameAsString, currentTermValue); + } + + if (user->callback(valuation)) { + return 1; + } else { + return 0; + } + } + + protected: + // The MathSAT environment. It is used to retrieve the values of the atoms in a model. + msat_env& env; + + // The function that is to be called when the MathSAT model has been translated to a valuation. std::function const& callback; }; - - int allsatValuationsCallback(msat_term *model, int size, void *user_data) { - AllsatValuationsCallbackUserData* user = reinterpret_cast(user_data); - - storm::expressions::SimpleValuation valuation; - - for (int i = 0; i < size; ++i) { - bool currentTermValue = true; - msat_term currentTerm = model[i]; - if (msat_term_is_not(user->env, currentTerm)) { - currentTerm = msat_term_get_arg(currentTerm, 0); - currentTermValue = false; - } - char* name = msat_decl_get_name(msat_term_get_decl(currentTerm)); - std::string name_str(name); - valuation.addBooleanIdentifier(name_str, currentTermValue); - msat_free(name); - } - - if (user->callback(valuation)) { - return 1; - } else { - return 0; - } - } + + class AllsatModelReferenceCallbackUserData { + public: + AllsatModelReferenceCallbackUserData(msat_env& env, std::unordered_map const& atomNameToSlotMapping, std::function const& callback) : env(env), atomNameToSlotMapping(atomNameToSlotMapping), callback(callback) { + // Intentionally left empty. + } + + static int allsatModelReferenceCallback(msat_term* model, int size, void* user_data) { + AllsatModelReferenceCallbackUserData* user = reinterpret_cast(user_data); + MathsatSmtSolver::MathSatModelReference modelReference(user->env, model, user->atomNameToSlotMapping); + if (user->callback(modelReference)) { + return 1; + } else { + return 0; + } + } + + protected: + // The MathSAT environment. It is used to retrieve the values of the atoms in a model. + msat_env& env; + + // Store a mapping from the names of atoms to their slots in the model. + std::unordered_map const& atomNameToSlotMapping; + + // The function that is to be called when the MathSAT model has been translated to a valuation. + std::function const& callback; + }; #endif uint_fast64_t MathsatSmtSolver::allSat(std::vector const& important, std::function const& callback) { #ifdef STORM_HAVE_MSAT + // Create a backtracking point, because MathSAT will modify the assertions stack during its AllSat procedure. + this->push(); + std::vector msatImportant; msatImportant.reserve(important.size()); - for (storm::expressions::Expression e : important) { - if (!e.isVariable()) { - throw storm::exceptions::InvalidArgumentException() << "The important expressions for AllSat must be atoms, i.e. variable expressions."; - } - msatImportant.push_back(expressionAdapter->translateExpression(e)); + for (storm::expressions::Expression const& atom : important) { + STORM_LOG_THROW(atom.isVariable() && atom.hasBooleanReturnType(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be boolean variables."); + msatImportant.push_back(expressionAdapter->translateExpression(atom)); } - AllsatValuationsCallbackUserData allSatUserData(env, *expressionAdapter, callback); - int numModels = msat_all_sat(env, msatImportant.data(), msatImportant.size(), &allsatValuationsCallback, &allSatUserData); + AllsatValuationCallbackUserData allSatUserData(env, callback); + int numberOfModels = msat_all_sat(env, msatImportant.data(), msatImportant.size(), &AllsatValuationCallbackUserData::allsatValuationsCallback, &allSatUserData); - return numModels; + // Restore original assertion stack and return. + this->pop(); + return static_cast(numberOfModels); #else - LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); #endif } uint_fast64_t MathsatSmtSolver::allSat(std::vector const& important, std::function const& callback) { #ifdef STORM_HAVE_MSAT - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not Implemented."); + // Create a backtracking point, because MathSAT will modify the assertions stack during its AllSat procedure. + this->push(); + + std::vector msatImportant; + msatImportant.reserve(important.size()); + std::unordered_map atomNameToSlotMapping; + + for (storm::expressions::Expression const& atom : important) { + STORM_LOG_THROW(atom.isVariable() && atom.hasBooleanReturnType(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be boolean variables."); + msatImportant.push_back(expressionAdapter->translateExpression(atom)); + atomNameToSlotMapping[atom.getIdentifier()] = msatImportant.size() - 1; + } + + AllsatModelReferenceCallbackUserData allSatUserData(env, atomNameToSlotMapping, callback); + int numberOfModels = msat_all_sat(env, msatImportant.data(), msatImportant.size(), &AllsatModelReferenceCallbackUserData::allsatModelReferenceCallback, &allSatUserData); + + // Restore original assertion stack and return. + this->pop(); + return static_cast(numberOfModels); #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); #endif } std::vector MathsatSmtSolver::getUnsatAssumptions() { #ifdef STORM_HAVE_MSAT - if (lastResult != SmtSolver::CheckResult::Unsat) { - throw storm::exceptions::InvalidStateException() << "Unsat Assumptions was called but last state is not unsat."; - } - if (!lastCheckAssumptions) { - throw storm::exceptions::InvalidStateException() << "Unsat Assumptions was called but last check had no assumptions."; - } - + STORM_LOG_THROW(lastResult == SmtSolver::CheckResult::Unsat, storm::exceptions::InvalidStateException, "Unable to generate unsatisfiable core of assumptions, because the last check did not determine the formulas to be unsatisfiable.") + STORM_LOG_THROW(lastCheckAssumptions, storm::exceptions::InvalidStateException, "Unable to generate unsatisfiable core of assumptions, because the last check did not involve assumptions."); + size_t numUnsatAssumpations; msat_term* msatUnsatAssumptions = msat_get_unsat_assumptions(env, &numUnsatAssumpations); @@ -309,43 +350,34 @@ namespace storm { return unsatAssumptions; #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); #endif } void MathsatSmtSolver::setInterpolationGroup(uint_fast64_t group) { #ifdef STORM_HAVE_MSAT auto groupIter = this->interpolationGroups.find(group); - if( groupIter == this->interpolationGroups.end() ) { + if (groupIter == this->interpolationGroups.end() ) { int newGroup = msat_create_itp_group(env); auto insertResult = this->interpolationGroups.insert(std::make_pair(group, newGroup)); - if (!insertResult.second) { - throw storm::exceptions::InvalidStateException() << "Internal error in MathSAT wrapper: Unable to insert newly created interpolation group."; - } groupIter = insertResult.first; } msat_set_itp_group(env, groupIter->second); #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); #endif } storm::expressions::Expression MathsatSmtSolver::getInterpolant(std::vector const& groupsA) { #ifdef STORM_HAVE_MSAT - if (lastResult != SmtSolver::CheckResult::Unsat) { - throw storm::exceptions::InvalidStateException() << "getInterpolant was called but last state is not unsat."; - } - if (lastCheckAssumptions) { - throw storm::exceptions::InvalidStateException() << "getInterpolant was called but last check had assumptions."; - } + STORM_LOG_THROW(lastResult == SmtSolver::CheckResult::Unsat, storm::exceptions::InvalidStateException, "Unable to generate interpolant, because the last check did not determine the formulas to be unsatisfiable."); + STORM_LOG_THROW(!lastCheckAssumptions, storm::exceptions::InvalidStateException, "Unable to generate interpolant, because the last check for satisfiability involved assumptions."); std::vector msatInterpolationGroupsA; msatInterpolationGroupsA.reserve(groupsA.size()); for (auto groupOfA : groupsA) { auto groupIter = this->interpolationGroups.find(groupOfA); - if (groupIter == this->interpolationGroups.end()) { - throw storm::exceptions::InvalidArgumentException() << "Requested interpolant for non existing interpolation group " << groupOfA; - } + STORM_LOG_THROW(groupIter != this->interpolationGroups.end(), storm::exceptions::InvalidArgumentException, "Unable to generate interpolant, because an unknown interpolation group was referenced."); msatInterpolationGroupsA.push_back(groupIter->second); } msat_term interpolant = msat_get_interpolant(env, msatInterpolationGroupsA.data(), msatInterpolationGroupsA.size()); @@ -354,7 +386,7 @@ namespace storm { return this->expressionAdapter->translateTerm(interpolant); #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); #endif } } diff --git a/src/solver/MathsatSmtSolver.h b/src/solver/MathsatSmtSolver.h index 4cff5f4f1..efd488450 100644 --- a/src/solver/MathsatSmtSolver.h +++ b/src/solver/MathsatSmtSolver.h @@ -41,7 +41,7 @@ namespace storm { class MathSatModelReference : public SmtSolver::ModelReference { public: #ifdef STORM_HAVE_MSAT - MathSatModelReference(msat_env const& env, storm::adapters::MathsatExpressionAdapter& adapter); + MathSatModelReference(msat_env const& env, msat_term* model, std::unordered_map const& atomNameToSlotMapping); #endif virtual bool getBooleanValue(std::string const& name) const override; virtual int_fast64_t getIntegerValue(std::string const& name) const override; @@ -50,11 +50,11 @@ namespace storm { private: #ifdef STORM_HAVE_MSAT msat_env const& env; - storm::adapters::MathsatExpressionAdapter& expressionAdapter; + msat_term* model; + std::unordered_map const& atomNameToSlotMapping; #endif }; - public: MathsatSmtSolver(Options const& options = Options()); virtual ~MathsatSmtSolver(); @@ -63,6 +63,8 @@ namespace storm { virtual void pop() override; + virtual void pop(uint_fast64_t n) override; + virtual void reset() override; virtual void add(storm::expressions::Expression const& assertion) override; diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index 17360d2a5..638972027 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/src/solver/Z3SmtSolver.cpp @@ -146,7 +146,7 @@ namespace storm { #endif } - SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list assumptions) + SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list const& assumptions) { #ifdef STORM_HAVE_Z3 lastCheckAssumptions = true; @@ -216,7 +216,7 @@ namespace storm { { #ifdef STORM_HAVE_Z3 std::vector valuations; - this->allSat(important, [&valuations](storm::expressions::SimpleValuation& valuation) -> bool { valuations.push_back(valuation); return true; }); + this->allSat(important, [&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; }); return valuations; #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); @@ -227,7 +227,7 @@ namespace storm { { #ifdef STORM_HAVE_Z3 for (storm::expressions::Expression const& atom : important) { - STORM_LOG_THROW(atom.isVariable(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be atoms, i.e. variables."); + STORM_LOG_THROW(atom.isVariable() && atom.hasBooleanReturnType(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be boolean variables."); } uint_fast64_t numberOfModels = 0; @@ -278,7 +278,7 @@ namespace storm { { #ifdef STORM_HAVE_Z3 for (storm::expressions::Expression const& atom : important) { - STORM_LOG_THROW(atom.isVariable(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be atoms, i.e. variables."); + STORM_LOG_THROW(atom.isVariable() && atom.hasBooleanReturnType(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be boolean variables."); } uint_fast64_t numberOfModels = 0; diff --git a/test/functional/solver/MathSatSmtSolverTest.cpp b/test/functional/solver/MathSatSmtSolverTest.cpp index e495c4be8..2ca48d935 100644 --- a/test/functional/solver/MathSatSmtSolverTest.cpp +++ b/test/functional/solver/MathSatSmtSolverTest.cpp @@ -2,17 +2,17 @@ #include "storm-config.h" #ifdef STORM_HAVE_MSAT -#include "src/solver/MathSatSmtSolver.h" +#include "src/solver/MathsatSmtSolver.h" -TEST(MathSatSmtSolver, CheckSat) { - storm::solver::MathSatSmtSolver s; - storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN; +TEST(MathsatSmtSolver, CheckSat) { + storm::solver::MathsatSmtSolver s; + storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff((!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y"))); - ASSERT_NO_THROW(s.assertExpression(exprDeMorgan)); + ASSERT_NO_THROW(s.add(exprDeMorgan)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); ASSERT_NO_THROW(s.reset()); storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); @@ -24,21 +24,21 @@ TEST(MathSatSmtSolver, CheckSat) { && c == (a * b) && b + a > c; - ASSERT_NO_THROW(s.assertExpression(exprFormula)); + ASSERT_NO_THROW(s.add(exprFormula)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); ASSERT_NO_THROW(s.reset()); } -TEST(MathSatSmtSolver, CheckUnsat) { - storm::solver::MathSatSmtSolver s; - storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN; +TEST(MathsatSmtSolver, CheckUnsat) { + storm::solver::MathsatSmtSolver s; + storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff( (!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y"))); - ASSERT_NO_THROW(s.assertExpression(!exprDeMorgan)); + ASSERT_NO_THROW(s.add(!exprDeMorgan)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); ASSERT_NO_THROW(s.reset()); storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); @@ -50,40 +50,40 @@ TEST(MathSatSmtSolver, CheckUnsat) { && c == (a + b + storm::expressions::Expression::createIntegerLiteral(1)) && b + a > c; - ASSERT_NO_THROW(s.assertExpression(exprFormula)); + ASSERT_NO_THROW(s.add(exprFormula)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); } -TEST(MathSatSmtSolver, Backtracking) { - storm::solver::MathSatSmtSolver s; - storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN; +TEST(MathsatSmtSolver, Backtracking) { + storm::solver::MathsatSmtSolver s; + storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; storm::expressions::Expression expr1 = storm::expressions::Expression::createTrue(); storm::expressions::Expression expr2 = storm::expressions::Expression::createFalse(); storm::expressions::Expression expr3 = storm::expressions::Expression::createFalse(); - ASSERT_NO_THROW(s.assertExpression(expr1)); + ASSERT_NO_THROW(s.add(expr1)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); ASSERT_NO_THROW(s.push()); - ASSERT_NO_THROW(s.assertExpression(expr2)); + ASSERT_NO_THROW(s.add(expr2)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); ASSERT_NO_THROW(s.pop()); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); ASSERT_NO_THROW(s.push()); - ASSERT_NO_THROW(s.assertExpression(expr2)); + ASSERT_NO_THROW(s.add(expr2)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); ASSERT_NO_THROW(s.push()); - ASSERT_NO_THROW(s.assertExpression(expr3)); + ASSERT_NO_THROW(s.add(expr3)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); ASSERT_NO_THROW(s.pop(2)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); ASSERT_NO_THROW(s.reset()); storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); @@ -96,21 +96,21 @@ TEST(MathSatSmtSolver, Backtracking) { && b + a > c; storm::expressions::Expression exprFormula2 = c > a + b + storm::expressions::Expression::createIntegerLiteral(1); - ASSERT_NO_THROW(s.assertExpression(exprFormula)); + ASSERT_NO_THROW(s.add(exprFormula)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); ASSERT_NO_THROW(s.push()); - ASSERT_NO_THROW(s.assertExpression(exprFormula2)); + ASSERT_NO_THROW(s.add(exprFormula2)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); ASSERT_NO_THROW(s.pop()); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); } -TEST(MathSatSmtSolver, Assumptions) { - storm::solver::MathSatSmtSolver s; - storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN; +TEST(MathsatSmtSolver, Assumptions) { + storm::solver::MathsatSmtSolver s; + storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); @@ -123,22 +123,22 @@ TEST(MathSatSmtSolver, Assumptions) { storm::expressions::Expression f2 = storm::expressions::Expression::createBooleanVariable("f2"); storm::expressions::Expression exprFormula2 = f2.implies(c > a + b + storm::expressions::Expression::createIntegerLiteral(1)); - ASSERT_NO_THROW(s.assertExpression(exprFormula)); + ASSERT_NO_THROW(s.add(exprFormula)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); - ASSERT_NO_THROW(s.assertExpression(exprFormula2)); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); + ASSERT_NO_THROW(s.add(exprFormula2)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); ASSERT_NO_THROW(result = s.checkWithAssumptions({f2})); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); ASSERT_NO_THROW(result = s.checkWithAssumptions({ !f2 })); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); } -TEST(MathSatSmtSolver, GenerateModel) { - storm::solver::MathSatSmtSolver s; +TEST(MathsatSmtSolver, GenerateModel) { + storm::solver::MathsatSmtSolver s; storm::solver::SmtSolver::CheckResult result; storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); @@ -150,9 +150,9 @@ TEST(MathSatSmtSolver, GenerateModel) { && c == (a + b - storm::expressions::Expression::createIntegerLiteral(1)) && b + a > c; - (s.assertExpression(exprFormula)); + (s.add(exprFormula)); (result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); storm::expressions::SimpleValuation model; (model = s.getModel()); int_fast64_t a_eval = model.getIntegerValue("a"); @@ -161,9 +161,9 @@ TEST(MathSatSmtSolver, GenerateModel) { ASSERT_TRUE(c_eval == a_eval + b_eval - 1); } -TEST(MathSatSmtSolver, AllSat) { - storm::solver::MathSatSmtSolver s; - storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN; +TEST(MathsatSmtSolver, AllSat) { + storm::solver::MathsatSmtSolver s; + storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); @@ -174,9 +174,9 @@ TEST(MathSatSmtSolver, AllSat) { storm::expressions::Expression exprFormula2 = y.implies(a < storm::expressions::Expression::createIntegerLiteral(5)); storm::expressions::Expression exprFormula3 = z.implies(b < storm::expressions::Expression::createIntegerLiteral(5)); - (s.assertExpression(exprFormula1)); - (s.assertExpression(exprFormula2)); - (s.assertExpression(exprFormula3)); + (s.add(exprFormula1)); + (s.add(exprFormula2)); + (s.add(exprFormula3)); std::vector valuations = s.allSat({x,y}); @@ -195,9 +195,9 @@ TEST(MathSatSmtSolver, AllSat) { } } -TEST(MathSatSmtSolver, UnsatAssumptions) { - storm::solver::MathSatSmtSolver s; - storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN; +TEST(MathsatSmtSolver, UnsatAssumptions) { + storm::solver::MathsatSmtSolver s; + storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); @@ -210,19 +210,19 @@ TEST(MathSatSmtSolver, UnsatAssumptions) { storm::expressions::Expression f2 = storm::expressions::Expression::createBooleanVariable("f2"); storm::expressions::Expression exprFormula2 = f2.implies(c > a + b + storm::expressions::Expression::createIntegerLiteral(1)); - (s.assertExpression(exprFormula)); - (s.assertExpression(exprFormula2)); + (s.add(exprFormula)); + (s.add(exprFormula2)); (result = s.checkWithAssumptions({ f2 })); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); std::vector unsatCore = s.getUnsatAssumptions(); ASSERT_EQ(unsatCore.size(), 1); ASSERT_TRUE(unsatCore[0].isVariable()); ASSERT_STREQ("f2", unsatCore[0].getIdentifier().c_str()); } -TEST(MathSatSmtSolver, InterpolationTest) { - storm::solver::MathSatSmtSolver s(storm::solver::SmtSolver::Options::InterpolantComputation); - storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN; +TEST(MathsatSmtSolver, InterpolationTest) { + storm::solver::MathsatSmtSolver s(storm::solver::MathsatSmtSolver::Options(false, false, true)); + storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); @@ -232,28 +232,28 @@ TEST(MathSatSmtSolver, InterpolationTest) { storm::expressions::Expression exprFormula3 = c > a; s.setInterpolationGroup(0); - s.assertExpression(exprFormula); + s.add(exprFormula); s.setInterpolationGroup(1); - s.assertExpression(exprFormula2); + s.add(exprFormula2); s.setInterpolationGroup(2); - s.assertExpression(exprFormula3); + s.add(exprFormula3); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); storm::expressions::Expression interpol; ASSERT_NO_THROW(interpol = s.getInterpolant({0, 1})); - storm::solver::MathSatSmtSolver s2; + storm::solver::MathsatSmtSolver s2; - ASSERT_NO_THROW(s2.assertExpression(!(exprFormula && exprFormula2).implies(interpol))); + ASSERT_NO_THROW(s2.add(!(exprFormula && exprFormula2).implies(interpol))); ASSERT_NO_THROW(result = s2.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); ASSERT_NO_THROW(s2.reset()); - ASSERT_NO_THROW(s2.assertExpression(interpol && exprFormula3)); + ASSERT_NO_THROW(s2.add(interpol && exprFormula3)); ASSERT_NO_THROW(result = s2.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); } #endif \ No newline at end of file diff --git a/test/functional/solver/Z3SmtSolverTest.cpp b/test/functional/solver/Z3SmtSolverTest.cpp index 30d023f0d..93f2876bb 100644 --- a/test/functional/solver/Z3SmtSolverTest.cpp +++ b/test/functional/solver/Z3SmtSolverTest.cpp @@ -7,13 +7,13 @@ TEST(Z3SmtSolver, CheckSat) { storm::solver::Z3SmtSolver s; - storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN; + storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff((!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y"))); - ASSERT_NO_THROW(s.assertExpression(exprDeMorgan)); + ASSERT_NO_THROW(s.add(exprDeMorgan)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); ASSERT_NO_THROW(s.reset()); storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); @@ -25,21 +25,21 @@ TEST(Z3SmtSolver, CheckSat) { && c == (a * b) && b + a > c; - ASSERT_NO_THROW(s.assertExpression(exprFormula)); + ASSERT_NO_THROW(s.add(exprFormula)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); ASSERT_NO_THROW(s.reset()); } TEST(Z3SmtSolver, CheckUnsat) { storm::solver::Z3SmtSolver s; - storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN; + storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff( (!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y"))); - ASSERT_NO_THROW(s.assertExpression(!exprDeMorgan)); + ASSERT_NO_THROW(s.add(!exprDeMorgan)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); ASSERT_NO_THROW(s.reset()); @@ -52,41 +52,41 @@ TEST(Z3SmtSolver, CheckUnsat) { && c == (a * b) && b + a > c; - ASSERT_NO_THROW(s.assertExpression(exprFormula)); + ASSERT_NO_THROW(s.add(exprFormula)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); } TEST(Z3SmtSolver, Backtracking) { storm::solver::Z3SmtSolver s; - storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN; + storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; storm::expressions::Expression expr1 = storm::expressions::Expression::createTrue(); storm::expressions::Expression expr2 = storm::expressions::Expression::createFalse(); storm::expressions::Expression expr3 = storm::expressions::Expression::createFalse(); - ASSERT_NO_THROW(s.assertExpression(expr1)); + ASSERT_NO_THROW(s.add(expr1)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); ASSERT_NO_THROW(s.push()); - ASSERT_NO_THROW(s.assertExpression(expr2)); + ASSERT_NO_THROW(s.add(expr2)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); ASSERT_NO_THROW(s.pop()); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); ASSERT_NO_THROW(s.push()); - ASSERT_NO_THROW(s.assertExpression(expr2)); + ASSERT_NO_THROW(s.add(expr2)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); ASSERT_NO_THROW(s.push()); - ASSERT_NO_THROW(s.assertExpression(expr3)); + ASSERT_NO_THROW(s.add(expr3)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); ASSERT_NO_THROW(s.pop(2)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); ASSERT_NO_THROW(s.reset()); @@ -100,21 +100,21 @@ TEST(Z3SmtSolver, Backtracking) { && b + a > c; storm::expressions::Expression exprFormula2 = a >= storm::expressions::Expression::createIntegerLiteral(2); - ASSERT_NO_THROW(s.assertExpression(exprFormula)); + ASSERT_NO_THROW(s.add(exprFormula)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); ASSERT_NO_THROW(s.push()); - ASSERT_NO_THROW(s.assertExpression(exprFormula2)); + ASSERT_NO_THROW(s.add(exprFormula2)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); ASSERT_NO_THROW(s.pop()); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); } TEST(Z3SmtSolver, Assumptions) { storm::solver::Z3SmtSolver s; - storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN; + storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown; storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); @@ -127,18 +127,18 @@ TEST(Z3SmtSolver, Assumptions) { storm::expressions::Expression f2 = storm::expressions::Expression::createBooleanVariable("f2"); storm::expressions::Expression exprFormula2 = f2.implies(a >= storm::expressions::Expression::createIntegerLiteral(2)); - ASSERT_NO_THROW(s.assertExpression(exprFormula)); + ASSERT_NO_THROW(s.add(exprFormula)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); - ASSERT_NO_THROW(s.assertExpression(exprFormula2)); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); + ASSERT_NO_THROW(s.add(exprFormula2)); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); ASSERT_NO_THROW(result = s.checkWithAssumptions({f2})); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); ASSERT_NO_THROW(result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); ASSERT_NO_THROW(result = s.checkWithAssumptions({ !f2 })); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); } TEST(Z3SmtSolver, GenerateModel) { @@ -154,9 +154,9 @@ TEST(Z3SmtSolver, GenerateModel) { && c == (a * b) && b + a > c; - (s.assertExpression(exprFormula)); + (s.add(exprFormula)); (result = s.check()); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat); storm::expressions::SimpleValuation model; (model = s.getModel()); int_fast64_t a_eval; @@ -178,9 +178,9 @@ TEST(Z3SmtSolver, AllSat) { storm::expressions::Expression exprFormula2 = y.implies(a < storm::expressions::Expression::createIntegerLiteral(5)); storm::expressions::Expression exprFormula3 = z.implies(b < storm::expressions::Expression::createIntegerLiteral(5)); - (s.assertExpression(exprFormula1)); - (s.assertExpression(exprFormula2)); - (s.assertExpression(exprFormula3)); + (s.add(exprFormula1)); + (s.add(exprFormula2)); + (s.add(exprFormula3)); std::vector valuations = s.allSat({x,y}); @@ -214,10 +214,10 @@ TEST(Z3SmtSolver, UnsatAssumptions) { storm::expressions::Expression f2 = storm::expressions::Expression::createBooleanVariable("f2"); storm::expressions::Expression exprFormula2 = f2.implies(a >= storm::expressions::Expression::createIntegerLiteral(2)); - s.assertExpression(exprFormula); - s.assertExpression(exprFormula2); + s.add(exprFormula); + s.add(exprFormula2); result = s.checkWithAssumptions({ f2 }); - ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); + ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); std::vector unsatCore = s.getUnsatAssumptions(); ASSERT_EQ(unsatCore.size(), 1); ASSERT_TRUE(unsatCore[0].isVariable());