From f69b79593c6a687dfcd2bb831ffc4412cb960df0 Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Mon, 5 May 2014 22:05:57 +0200 Subject: [PATCH] initial interface for smt solver wrappers Former-commit-id: e43b7afb3c230a6ff7f0330e5bb0864caf0640c0 --- src/solver/SmtSolver.h | 151 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 151 insertions(+) create mode 100644 src/solver/SmtSolver.h diff --git a/src/solver/SmtSolver.h b/src/solver/SmtSolver.h new file mode 100644 index 000000000..9c9dbce80 --- /dev/null +++ b/src/solver/SmtSolver.h @@ -0,0 +1,151 @@ +#ifndef STORM_SOLVER_SMTSOLVER +#define STORM_SOLVER_SMTSOLVER + +#include + +#include "exceptions/IllegalArgumentValueException.h" +#include "exceptions/NotImplementedException.h" +#include "exceptions/IllegalArgumentTypeException.h" +#include "exceptions/IllegalFunctionCallException.h" +#include "exceptions/InvalidStateException.h" +#include "storage/expressions/Expressions.h" +#include "storage/expressions/SimpleValuation.h" + +#include +#include +#include +#include + +namespace storm { + namespace solver { + + /*! + * An interface that captures the functionality of an SMT solver. + */ + class SmtSolver { + public: + //! Option flags for smt solvers. + enum class Options { + ModelGeneration = 0x01, + UnsatCoreComputation = 0x02, + InterpolantComputation = 0x04 + }; + //! possible check results + enum class CheckResult {SAT, UNSAT, UNKNOWN}; + public: + /*! + * Constructs a new smt solver with the given options. + * + * @param options the options for the solver + * @throws storm::exceptions::IllegalArgumentValueException if an option is unsupported for the solver + */ + SmtSolver(Options options = Options::ModelGeneration) {}; + virtual ~SmtSolver() {}; + + //! pushes a backtrackingpoint in the solver + virtual void push() = 0; + //! pops a backtrackingpoint in the solver + virtual void pop() = 0; + //! pops multiple backtrack points + //! @param n number of backtrackingpoint to pop + virtual void pop(uint_fast64_t n) = 0; + //! removes all assertions + virtual void reset() = 0; + + + //! assert an expression in the solver + //! @param e the asserted expression, the return type has to be bool + //! @throws IllegalArgumentTypeException if the return type of the expression is not bool + virtual void assert(storm::expressions::Expression &e) = 0; + //! assert a set of expressions in the solver + //! @param es the asserted expressions + //! @see assert(storm::expressions::Expression &e) + virtual void assert(std::set &es) { + for (storm::expressions::Expression e : es) { + this->assert(e); + } + } + //! assert a set of expressions in the solver + //! @param es the asserted expressions + //! @see assert(storm::expressions::Expression &e) + virtual void assert(std::unordered_set &es) { + for (storm::expressions::Expression e : es) { + this->assert(e); + } + } + //! assert a set of expressions in the solver + //! @param es the asserted expressions + //! @see assert(storm::expressions::Expression &e) + virtual void assert(std::initializer_list &es) { + for (storm::expressions::Expression e : es) { + this->assert(e); + } + } + + /*! + * check satisfiability of the conjunction of the currently asserted expressions + * + * @returns CheckResult::SAT if the conjunction of the asserted expressions is satisfiable, + * CheckResult::UNSAT if it is unsatisfiable and CheckResult::UNKNOWN if the solver + * could not determine satisfiability + */ + virtual CheckResult check() = 0; + //! check satisfiability of the conjunction of the currently asserted expressions and the provided assumptions + //! @param es the asserted expressions + //! @throws IllegalArgumentTypeException if the return type of one of the expressions is not bool + //! @see check() + virtual CheckResult checkWithAssumptions(std::set &assumptions) = 0; + //! check satisfiability of the conjunction of the currently asserted expressions and the provided assumptions + //! @param es the asserted expressions + //! @throws IllegalArgumentTypeException if the return type of one of the expressions is not bool + //! @see check() + virtual CheckResult checkWithAssumptions(std::unordered_set &assumptions) = 0; + //! check satisfiability of the conjunction of the currently asserted expressions and the provided assumptions + //! @param es the asserted expressions + //! @throws IllegalArgumentTypeException if the return type of one of the expressions is not bool + //! @see check() + virtual CheckResult checkWithAssumptions(std::initializer_list &assumptions) = 0; + + /*! + * Gets a model for the assertion stack (and possibly assumtions) for the last call to ::check or ::checkWithAssumptions if that call + * returned CheckResult::SAT. Otherwise an exception is thrown. + * @remark Note that this function may throw an exception if it is not called immediately after a call to::check or ::checkWithAssumptions + * that returned CheckResult::SAT depending on the implementation. + * @throws InvalidStateException if no model is available + * @throws IllegalFunctionCallException if model generation is not configured for this solver + * @throws NotImplementedException if model generation is not implemented with this solver class + */ + virtual storm::expressions::SimpleValuation getModel() { + throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support model generation."); + } + + /*! + * Get get a maximal number of models for the assertion stack such that each model has a distinct valuation of the diversifyers. + * + * @param diversifyers A set of expressions over which to diversify. For each returned model the valuation these terms is distinct. + * + * @throws IllegalFunctionCallException if model generation is not configured for this solver + * @throws NotImplementedException if model generation is not implemented with this solver class + */ + virtual std::set solveAndDiversify(std::set diversifyers) { + throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support model generation."); + } + + /*! + * Get get a maximal number of models for the assertion stack such that each model has a distinct valuation of the diversifyers. + * For each model that is found the provided callback function is called once with the model as parameter. + * + * @param diversifyers A set of expressions over which to diversify. For each returned model the valuation these terms is distinct. + * @param callback A function to call for each found model. + * + * @throws IllegalFunctionCallException if model generation is not configured for this solver + * @throws NotImplementedException if model generation is not implemented with this solver class + */ + virtual uint_fast64_t solveAndDiversify(std::set diversifyers, std::function callback) { + throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support model generation."); + } + }; + } +} + +#endif // STORM_SOLVER_SMTSOLVER