SmtSolver.h

Go to the documentation of this file.

#ifndef STORM_SOLVER_SMTSOLVER
#define STORM_SOLVER_SMTSOLVER
 
#include <cstdint>
 
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/storage/expressions/Expressions.h"
#include "storm/storage/expressions/SimpleValuation.h"
 
#include <functional>
#include <initializer_list>
#include <set>
#include <unordered_set>
#include <vector>
 
namespace storm {
namespace solver {
 
class SmtSolver {
   public:
    enum class CheckResult { Sat, Unsat, Unknown };
 
    class ModelReference {
       public:
        ModelReference(storm::expressions::ExpressionManager const& manager);
        virtual ~ModelReference() = default;
 
        virtual bool getBooleanValue(storm::expressions::Variable const& variable) const = 0;
        virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const = 0;
        virtual double getRationalValue(storm::expressions::Variable const& variable) const = 0;
 
        storm::expressions::ExpressionManager const& getManager() const;
 
        virtual std::string toString() const = 0;
 
       private:
        // The expression manager responsible for the variables whose value can be requested via this model
        // reference.
        storm::expressions::ExpressionManager const& manager;
    };
    class ModelReference {…};
 
   public:
    SmtSolver(storm::expressions::ExpressionManager& manager);
 
    virtual ~SmtSolver();
 
    SmtSolver(SmtSolver const& other) = default;
 
    SmtSolver(SmtSolver&& other) = default;
    SmtSolver& operator=(SmtSolver const& other) = delete;
    SmtSolver& operator=(SmtSolver&& other) = delete;
 
    virtual void push() = 0;
 
    virtual void pop() = 0;
 
    virtual void pop(uint_fast64_t n);
 
    virtual void reset() = 0;
 
    virtual void add(storm::expressions::Expression const& assertion) = 0;
 
    void add(std::set<storm::expressions::Expression> const& assertions);
 
    void add(std::initializer_list<storm::expressions::Expression> const& assertions);
 
    virtual CheckResult check() = 0;
 
    virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) = 0;
 
    virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) = 0;
 
    virtual storm::expressions::SimpleValuation getModelAsValuation();
 
    virtual std::shared_ptr<ModelReference> getModel();
 
    virtual std::vector<storm::expressions::SimpleValuation> allSat(std::vector<storm::expressions::Variable> const& important);
 
    virtual uint_fast64_t allSat(std::vector<storm::expressions::Variable> const& important,
                                 std::function<bool(storm::expressions::SimpleValuation&)> const& callback);
 
    virtual uint_fast64_t allSat(std::vector<storm::expressions::Variable> const& important, std::function<bool(ModelReference&)> const& callback);
 
    virtual std::vector<storm::expressions::Expression> getUnsatCore();
 
    virtual std::vector<storm::expressions::Expression> getUnsatAssumptions();
 
    virtual void setInterpolationGroup(uint_fast64_t group);
 
    virtual storm::expressions::Expression getInterpolant(std::vector<uint_fast64_t> const& groupsA);
 
    storm::expressions::ExpressionManager const& getManager() const;
 
    storm::expressions::ExpressionManager& getManager();
 
    virtual bool setTimeout(uint_fast64_t milliseconds);
 
    virtual bool unsetTimeout();
 
    virtual std::string getSmtLibString() const;
 
   private:
    // The manager responsible for the expressions that interact with this solver.
    storm::expressions::ExpressionManager& manager;
};
class SmtSolver {…};
}  // namespace solver
}  // namespace storm
 
#endif  // STORM_SOLVER_SMTSOLVER