SmtlibSmtSolver.h

Go to the documentation of this file.

#pragma once
 
#include <fstream>
#include <iostream>
 
#include "storm-config.h"
#include "storm/adapters/RationalFunctionForward.h"
#include "storm/adapters/Smt2ExpressionAdapter.h"
#include "storm/solver/SmtSolver.h"
 
namespace storm {
namespace solver {
class SmtlibSmtSolver : public SmtSolver {
   public:
    class SmtlibModelReference : public SmtSolver::ModelReference {
       public:
        SmtlibModelReference(storm::expressions::ExpressionManager const& manager);
        virtual bool getBooleanValue(storm::expressions::Variable const& variable) const override;
        virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const override;
        virtual double getRationalValue(storm::expressions::Variable const& variable) const override;
        virtual std::string toString() const override;
    };
 
   public:
    SmtlibSmtSolver(storm::expressions::ExpressionManager& manager, bool useCarlExpressions = false);
    virtual ~SmtlibSmtSolver();
 
    virtual void push() override;
 
    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;
 
    // adds the constraint "leftHandSide relation rightHandSide"
    virtual void add(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation,
                     storm::RationalFunction const& rightHandSide = storm::RationalFunction(0));
 
    // asserts that the given variable has the given value. The variable should have type 'bool'
    void add(storm::RationalFunctionVariable const& variable, bool value);
 
    virtual CheckResult check() override;
 
    virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) override;
 
    virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) override;
 
    bool isNeedsRestart() const;
 
    // Todo: some of these might be added in the future
    // virtual storm::expressions::SimpleValuation getModelAsValuation() override;
 
    // virtual std::shared_ptr<SmtSolver::ModelReference> getModel() override;
 
    //  virtual std::vector<storm::expressions::SimpleValuation> allSat(std::vector<storm::expressions::Variable> const& important) override;
 
    //  virtual uint_fast64_t allSat(std::vector<storm::expressions::Variable> const& important, std::function<bool(storm::expressions::SimpleValuation&)>
    // const& callback) override;
 
    //  virtual uint_fast64_t allSat(std::vector<storm::expressions::Variable> const& important, std::function<bool(ModelReference&)> const& callback) override;
 
    //  virtual std::vector<storm::expressions::Expression> getUnsatAssumptions() override;
 
   private:
    void init();
 
    void writeCommand(std::string smt2Command, bool expectSuccess);
 
    std::vector<std::string> readSolverOutput(bool waitForOutput = true);
 
    void checkForErrorMessage(const std::string message);
 
    // descriptors for the pipe from and to the solver
    int toSolver;
    int fromSolver;
    // A flag storing the Process ID of the solver. If this is zero, then the solver is not running
    pid_t processIdOfSolver;
 
    // a filestream where the commands that we send to the solver will be stored (can be used for debugging purposes)
    std::ofstream commandFile;
 
    bool isCommandFileOpen;
 
    // An expression adapter that is used for translating the expression into Smt2's format.
    std::unique_ptr<storm::adapters::Smt2ExpressionAdapter> expressionAdapter;
 
    // A flag storing whether the last call to a check method provided aussumptions.
    // bool lastCheckAssumptions;
 
    // The last result that was returned by any of the check methods.
    // CheckResult lastResult;
 
    // A flag that states whether we want to use carl expressions.
    bool useCarlExpressions;
 
    // A flag that states whether to use readable variable names
    bool useReadableVarNames = true;
 
    // A flag that states whether some error has occured
    bool needsRestart = false;
};
}  // namespace solver
}  // namespace storm