Architectural elements

The classes documented in this page build the processing pipeline infrastructure.

class consumer

Abstract base class for objects capable of receiving streams of elements from modules and pipeline stages.

Consumers are the objects that can be passed to the module::replay() function and receive a stream of elements (declarations, statements, etc.) from a module or from a preceding pass of a processing pipeline.

Modules are consumer themselves.

Subclassed by black::logic::module, black::pipes::internal::map_t::impl_t, black::solvers::const_t< V >, black::solvers::cvc5_t::impl_t

Public Functions

virtual void import(logic::module) = 0

Streams the import of a module.

virtual void adopt(std::shared_ptr<logic::root const> r) = 0

Streams the adoption of a root object managing a set of declared/defined entity objects. In calls to adopt(), r cannot be null.

virtual void state(logic::term, logic::statement s) = 0

Streams the statement of a requirement or an automaton constraint.

virtual void push() = 0

Streams the push of a frame on the assertion stack.

virtual void pop(size_t n) = 0

Streams the pop of n frames from the assertion stack. Note that n might be greater than the number of previous push() calls.

class transform

Class handling instances of tranform pipelines.

A transform can be created from any transform::pipeline and actually instantiates the pipeline components and sets them up to stream the transform.

One can actually apply the transform by calling the transform object on a given module, obtaining the transformed one. The transformation is incremental: at the next call only the differences with the previous one will be streamed.

Example:

module mod = ...;
pipes::transform nothing = pipes::id() | pipes::id();

module mod2 = nothing(mod);
assert(mod == mod2);

mod.require(x > 0);
mod2 = nothing(mod); // only the last requirement is streamed here

assert(mod == mod2);

Note

Since transforms will generally carry complex state with them, transform objects are move-only.

Constructor

inline transform(pipeline p)

Constructs the transform from a transform::pipeline object.

Public Types

using instance = std::unique_ptr<base>

Type reprsenting an instantiated pipeline stage.

using pipeline = std::function<instance(consumer *next)>

Type representing transform pipeline stages before instantiation.

Public Functions

inline base *get()

Gets a pointer to the underlying instance of transform::base.

inline logic::module operator()(logic::module mod)

Applies the transform to the given module.

class base

Abstract base class for transform pipeline stages.

A pipeline stage has to provide three elements:

1. a pointer to a consumer objects ready to stream (the consumer() function);

2. a way to translate object instances from the world before the transform to the world after the transform (the translate() function);

3. a way to map back values from models obtained by solvers after the transform to terms that make sense before the transform.

Subclassed by black::pipes::internal::composed_t, black::pipes::internal::id_t, black::pipes::internal::map_t

Public Functions

virtual class consumer *consumer() = 0

The consumer implementing the transform.

virtual std::optional<logic::object> translate(logic::object) = 0

The translation function for object instances.

virtual logic::term undo(logic::term) = 0

The back-mapping function for model terms.

template<typename P>
constexpr auto black::pipes::make_transform = make_pipe<P, transform, consumer*>

Utility type to declare pipeline factory objects.

Given a type deriving from transform::base, the result is an object usable as a factory for the corresponding transform::pipeline.

For example, this is the implementation of the pipes::id() transform:

class id_t : public transform::base
{
public:
  id_t(class consumer *next) : _next{next} { }
    
  virtual class consumer *consumer() override { return _next; }

  virtual std::optional<logic::object> translate(logic::object) override 
  { 
    return {};
  }

  virtual logic::term undo(logic::term t) override { return t; }

private:
  class consumer *_next;
};

inline constexpr auto id = make_transform<id_t>{};