Solvers

class solver

Opaque handle type representing solvers.

Solvers can be instantiated in various ways (see e.g., backends::cvc5). Independently from their origin, this class wraps solver instances and provides a unified interface.

Constructor

inline solver(std::shared_ptr<base> p)

Constructs a solver from a shared pointer to solver::base.

Public Functions

inline std::shared_ptr<base> ptr() const

Returns the solver’s underlying pointer to solver::base.

inline void set(std::string option, std::string value)

Sets solver-specific options.

inline void set(option opt, std::string value)

Sets solver-agnostic options.

inline support::tribool check(logic::module mod)

Check the satisfiability of the given module.

inline std::optional<class model> model() const

Ask the value of an object in the solver’s current model. This works only after a call to check() that returned true.

class base

Virtual base class to be implemented by solvers.

Subclassed by black::solvers::const_t< V >, black::solvers::cvc5_t, black::solvers::preprocessed_t

Public Functions

virtual void set(std::string option, std::string value) = 0

Sets solver-specific options.

virtual void set(option opt, std::string value) = 0

Sets solver-agnostic options.

virtual pipes::consumer *consumer() = 0

Returns the solver’s underlying pipes::consumer.

virtual support::tribool check() = 0

Check the satisfiability of the current solver’s assertions stack.

virtual std::optional<class model> model() const = 0

Ask the value of an object in the solver’s current model. This works only after a call to check() that returned true.

class model

Class representing models.

Models can come from different sources: solvers, files, runtime traces of monitored systems, etc. This class is a thin wrapper over a shared pointer to model::base, which is the abstract base class for all these kinds of models.

Independently from the source, all models can return a term when given an object and, for non-rigid entities, a time step.

Models can represent temporal state sequences, or single a-temporal structures, depending on their source. Temporal models know their size(), which can be finite or infinite.

Constructors

inline model()

Default constructor for an empty model.

inline model(ptr p)

Constructor from a shared pointer to model::base

Public Functions

inline std::optional<logic::term> value(logic::object x) const

Returns a term associated to an object.

Returns the term associated with x in the model, or an empty optional if this model does not know anything about x or if x does not refer to a rigid entity (in that case, one can use the other overload).

Parameters:

x – the object we want to extract the term of.

inline std::optional<logic::term> value(logic::object x, size_t t) const

Returns a term associated to an object at a given time stamp.

Returns the term associated with x in the model, or an empty optional if this model does not know anything about x.

Parameters:

• x – the object we want to extract the term of.

• t – the timestamp.

inline size_t size() const

Returns the size of the model.

The returned value is:

• zero, if the model is not temporal

• a positive number if the model is temporal and finite

• the model::infinite constant if the model is temporal and infinite

Public Static Attributes

static constexpr size_t infinite = std::numeric_limits<size_t>::max()

A constant to represent the size of an infinite temporal model.

class base

Subclassed by black::solvers::cvc5_t::impl_t, black::solvers::empty_t, black::solvers::preprocessed_t

enum class black::solvers::option : uint8_t

Enum of known solver-agnostic options that can be passed to solvers.

Values:

enumerator logic

Set the SMT logic.