Implemented Unsat Core/Assumtions & simple test

Former-commit-id: f79ee3a809

src/solver/SmtSolver.h

@@ -157,6 +157,32 @@ namespace storm {
 			virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> important, std::function<bool(storm::expressions::SimpleValuation&)> callback) {
 				throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support model generation.");
 			}
+
+			/*!
+			* Retrieves the unsat core of the last call to check()
+			*
+			* @returns a subset of the asserted formulas s.t. this subset is unsat
+			*
+			* @throws InvalidStateException if no unsat core is available, i.e. the asserted formulas are consistent
+			* @throws IllegalFunctionCallException if unsat core generation is not configured for this solver
+			* @throws NotImplementedException if unsat core generation is not implemented with this solver class
+			*/
+			virtual std::vector<storm::expressions::Expression> getUnsatCore() {
+				throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support unsat core generation.");
+			}
+
+			/*!
+			* Retrieves a subset of the assumptions from the last call to checkWithAssumptions(), s.t. the result is still unsatisfiable
+			*
+			* @returns a subset of the assumptions s.t. this subset of the assumptions results in unsat
+			*
+			* @throws InvalidStateException if no unsat assumptions is available, i.e. the asserted formulas are consistent
+			* @throws IllegalFunctionCallException if unsat assumptions generation is not configured for this solver
+			* @throws NotImplementedException if unsat assumptions generation is not implemented with this solver class
+			*/
+			virtual std::vector<storm::expressions::Expression> getUnsatAssumptions() {
+				throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support unsat core generation.");
+			}
 		};
 	}
 }

src/solver/Z3SmtSolver.cpp

@@ -9,6 +9,7 @@ namespace storm {
 			, m_solver(m_context)
 			, m_adapter(m_context, {})
 			, lastResult(CheckResult::UNKNOWN)
+			, lastCheckAssumptions(false)
 #endif
 		{
 			//intentionally left empty
@@ -63,6 +64,7 @@ namespace storm {
 		SmtSolver::CheckResult Z3SmtSolver::check()
 		{
 #ifdef STORM_HAVE_Z3
+			lastCheckAssumptions = false;
 			switch (this->m_solver.check()) {
 				case z3::sat:
 					this->lastResult = SmtSolver::CheckResult::SAT;
@@ -83,6 +85,7 @@ namespace storm {
 		SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::set<storm::expressions::Expression> &assumptions)
 		{
 #ifdef STORM_HAVE_Z3
+			lastCheckAssumptions = true;
 			z3::expr_vector z3Assumptions(this->m_context);
 
 			for (storm::expressions::Expression assumption : assumptions) {
@@ -109,6 +112,7 @@ namespace storm {
 		SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list<storm::expressions::Expression> assumptions)
 		{
 #ifdef STORM_HAVE_Z3
+			lastCheckAssumptions = true;
 			z3::expr_vector z3Assumptions(this->m_context);
 
 			for (storm::expressions::Expression assumption : assumptions) {
@@ -238,6 +242,27 @@ namespace storm {
 			LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
 #endif
 		}
+		std::vector<storm::expressions::Expression> Z3SmtSolver::getUnsatAssumptions() {
+#ifdef STORM_HAVE_Z3
+			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.";
+			}
 
+			z3::expr_vector z3UnsatAssumptions = this->m_solver.unsat_core();
+
+			std::vector<storm::expressions::Expression> unsatAssumptions;
+			
+			for (unsigned int i = 0; i < z3UnsatAssumptions.size(); ++i) {
+				unsatAssumptions.push_back(this->m_adapter.translateExpression(z3UnsatAssumptions[i]));
+			}
+
+			return unsatAssumptions;
+#else
+			LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+#endif
+		}
 	}
 }

src/solver/Z3SmtSolver.h

@@ -37,6 +37,8 @@ namespace storm {
 
 			virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> important, std::function<bool(storm::expressions::SimpleValuation&)> callback) override;
 
+			virtual std::vector<storm::expressions::Expression> getUnsatAssumptions() override;
+
 		protected:
 			virtual storm::expressions::SimpleValuation z3ModelToStorm(z3::model m);
 		private:
@@ -46,6 +48,7 @@ namespace storm {
 			z3::solver m_solver;
 			storm::adapters::Z3ExpressionAdapter m_adapter;
 
+			bool lastCheckAssumptions;
 			CheckResult lastResult;
 #endif
 		};

test/functional/solver/Z3SmtSolverTest.cpp

@@ -223,6 +223,36 @@ TEST(Z3SmtSolver, AllSat) {
 		}
 	}
 
+#else
+	ASSERT_TRUE(false) << "StoRM built without Z3 support.";
+#endif
+}
+
+TEST(Z3SmtSolver, UnsatAssumptions) {
+#ifdef STORM_HAVE_Z3
+	storm::solver::Z3SmtSolver s;
+	storm::solver::Z3SmtSolver::CheckResult result;
+
+	storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
+	storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b");
+	storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c");
+	storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(0)
+		&& a < storm::expressions::Expression::createIntegerLiteral(5)
+		&& b > storm::expressions::Expression::createIntegerLiteral(7)
+		&& c == (a * b)
+		&& b + a > c;
+	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));
+	(result = s.checkWithAssumptions({ f2 }));
+	ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+	std::vector<storm::expressions::Expression> unsatCore = s.getUnsatAssumptions();
+	ASSERT_EQ(unsatCore.size(), 1);
+	ASSERT_TRUE(unsatCore[0].isVariable());
+	ASSERT_STREQ("f2", unsatCore[0].getIdentifier().c_str());
+
 #else
 	ASSERT_TRUE(false) << "StoRM built without Z3 support.";
 #endif