Cvc5SmtSolver.h

Go to the documentation of this file.

#pragma once
 
#include "storm-config.h"
#include "storm/adapters/Cvc5ExpressionAdapter.h"
#include "storm/solver/SmtSolver.h"
 
#ifdef STORM_HAVE_CVC5
#include <cvc5/cvc5.h>
#endif
 
namespace storm::solver {
class Cvc5SmtSolver : public SmtSolver {
   public:
    class Cvc5ModelReference : public SmtSolver::ModelReference {
       public:
        Cvc5ModelReference(storm::expressions::ExpressionManager const& manager, storm::expressions::SimpleValuation variableValues);
 
        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;
 
       private:
        void checkVariable(storm::expressions::Variable const& variable) const;
 
        // The values that the model assigns to the variables.
        storm::expressions::SimpleValuation variableValues;
    };
 
   public:
    Cvc5SmtSolver(storm::expressions::ExpressionManager& manager);
    virtual ~Cvc5SmtSolver();
 
    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;
 
    virtual void addNotCurrentModel(bool performSolverReset = true) override;
 
    virtual CheckResult check() override;
 
    virtual CheckResult checkWithAssumptions(storm::expressions::ExpressionSet const& assumptions) override;
 
    virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) override;
 
    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;
 
    virtual bool setTimeout(uint_fast64_t milliseconds) override;
 
    virtual bool unsetTimeout() override;
 
   private:
#ifdef STORM_HAVE_CVC5
    SmtSolver::CheckResult translateResult(cvc5::Result const& result) const;

    std::unordered_map<storm::expressions::Variable, cvc5::Term> collectVariableValues() const;

    storm::expressions::SimpleValuation collectModelAsValuation() const;

    cvc5::Term createModelExpression(std::vector<storm::expressions::Variable> const& variables) const;
 
    // The manager that terms and sorts are built with, which is also passed to the cvc5::Solver constructor. It
    // is declared before the solver so that it outlives it, as the terms of the solver refer to it.
    std::unique_ptr<cvc5::TermManager> termManager;
 
    // The actual solver object.
    std::unique_ptr<cvc5::Solver> solver;
 
    // An expression adapter that is used for translating the expression into cvc5's format.
    std::unique_ptr<storm::adapters::Cvc5ExpressionAdapter> expressionAdapter;
 
    // A flag storing whether the last call to a check method provided assumptions.
    bool lastCheckAssumptions;
 
    // The last result that was returned by any of the check methods.
    CheckResult lastResult;
#endif
};
}  // namespace storm::solver