SmtSolver.h

Go to the documentation of this file.

#pragma once
 
#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;
    };
 
   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 void addNotCurrentModel(bool performSolverReset = true);

    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;
};
}  // namespace solver
}  // namespace storm