Terms and formulas

The error term

using namespace black::logic;

struct error

A logically erroneous term.

Constructor:

error(logic::term source, std::string error)

Parameters:

• source – The erroneous term.

• error – The error.

Members:

logic::term source() const

Returns:

The erroneous term.

std::string error() const

Returns:

The error.

Constant terms

using namespace black::logic;

struct integer

A constant integer value (e.g., 42).

Constructor:

integer(int64_t value)

Parameters:

value – The constant value.

Members:

int64_t value() const

Returns:

The constant value.

struct real

A constant real value (e.g., 3.14).

Constructor:

real(double value)

Parameters:

value – The constant value.

Members:

double value() const

Returns:

The constant value.

struct boolean

A constant boolean value (i.e., true or false).

Constructor:

boolean(bool value)

Parameters:

value – The boolean value.

Members:

bool value() const

Returns:

The boolean value.

Boolean and first-order predicates

using namespace black::logic;

struct variable

An unbound variable.

Constructor:

variable(ast::core::label name)

Parameters:

name – The variable’s name.

Members:

ast::core::label name() const

Returns:

The variable’s name.

struct object

A resolved object.

Constructor:

object(logic::entity const *entity)

Parameters:

entity – The object’s underlying entity.

Members:

logic::entity const *entity() const

Returns:

The object’s underlying entity.

struct prime

A reference to an state variable’s value at the next step in a transition relation.

Constructor:

prime(logic::object object)

Parameters:

object – The object refering to the state variable.

Members:

logic::object object() const

Returns:

The object refering to the state variable.

struct equal

An equality constraint between terms.

Constructor:

equal(std::vector<logic::term> arguments)

Parameters:

arguments – The operands.

Members:

std::vector<logic::term> arguments() const

Returns:

The operands.

struct distinct

An inequality constraint between terms.

Constructor:

distinct(std::vector<logic::term> arguments)

Parameters:

arguments – The operands.

Members:

std::vector<logic::term> arguments() const

Returns:

The operands.

struct atom

An atomic first-order term (e.g. f(x, y)).

Constructor:

atom(logic::term head, std::vector<logic::term> arguments)

Parameters:

• head – The applied term.

• arguments – The arguments.

Members:

logic::term head() const

Returns:

The applied term.

std::vector<logic::term> arguments() const

Returns:

The arguments.

struct exists

An existentially quantified term.

Constructor:

exists(std::vector<logic::decl> decls, logic::term body)

Parameters:

• decls – The quantified variables.

• body – The quantified term.

Members:

std::vector<logic::decl> decls() const

Returns:

The quantified variables.

logic::term body() const

Returns:

The quantified term.

struct forall

An universally quantified term.

Constructor:

forall(std::vector<logic::decl> decls, logic::term body)

Parameters:

• decls – The quantified variables.

• body – The quantified term.

Members:

std::vector<logic::decl> decls() const

Returns:

The quantified variables.

logic::term body() const

Returns:

The quantified term.

Boolean connectives

using namespace black::logic;

struct negation

A logical negation.

Constructor:

negation(logic::term argument)

Parameters:

argument – The term to negate.

Members:

logic::term argument() const

Returns:

The term to negate.

struct conjunction

A logical conjunction.

Constructor:

conjunction(std::vector<logic::term> arguments)

Parameters:

arguments – The conjuncts.

Members:

std::vector<logic::term> arguments() const

Returns:

The conjuncts.

struct disjunction

A logical disjunction.

Constructor:

disjunction(std::vector<logic::term> arguments)

Parameters:

arguments – The disjuncts.

Members:

std::vector<logic::term> arguments() const

Returns:

The disjuncts.

struct implication

A logical implication.

Constructor:

implication(logic::term left, logic::term right)

Parameters:

• left – The antecedent.

• right – The consequent.

Members:

logic::term left() const

Returns:

The antecedent.

logic::term right() const

Returns:

The consequent.

Functional constructs

using namespace black::logic;

struct ite

An if/then/else selection construct.

Constructor:

ite(logic::term guard, logic::term iftrue, logic::term iffalse)

Parameters:

• guard – The test guard.

• iftrue – The result if the guard is true.

• iffalse – The result if the guard is false.

Members:

logic::term guard() const

Returns:

The test guard.

logic::term iftrue() const

Returns:

The result if the guard is true.

logic::term iffalse() const

Returns:

The result if the guard is false.

struct lambda

A lambda abstraction (i.e., an anonymous function).

Constructor:

lambda(std::vector<logic::decl> vars, logic::term body)

Parameters:

• vars – The lambda’s parameters.

• body – The lambda’s body.

Members:

std::vector<logic::decl> vars() const

Returns:

The lambda’s parameters.

logic::term body() const

Returns:

The lambda’s body.

Linear Temporal Logic (future) temporal operators

using namespace black::logic;

struct tomorrow

An tomorrow LTL formula.

Constructor:

tomorrow(logic::term argument)

Parameters:

argument – The operator’s argument.

Members:

logic::term argument() const

Returns:

The operator’s argument.

struct w_tomorrow

A weak tomorrow LTL formula.

Constructor:

w_tomorrow(logic::term argument)

Parameters:

argument – The operator’s argument.

Members:

logic::term argument() const

Returns:

The operator’s argument.

struct eventually

An eventually LTL formula.

Constructor:

eventually(logic::term argument)

Parameters:

argument – The operator’s argument.

Members:

logic::term argument() const

Returns:

The operator’s argument.

struct always

An always LTL formula.

Constructor:

always(logic::term argument)

Parameters:

argument – The operator’s argument.

Members:

logic::term argument() const

Returns:

The operator’s argument.

struct until

An until LTL formula.

Constructor:

until(logic::term left, logic::term right)

Parameters:

• left – The universal argument.

• right – The existential argument.

Members:

logic::term left() const

Returns:

The universal argument.

logic::term right() const

Returns:

The existential argument.

struct release

A release LTL formula.

Constructor:

release(logic::term left, logic::term right)

Parameters:

• left – The existential argument.

• right – The universal argument.

Members:

logic::term left() const

Returns:

The existential argument.

logic::term right() const

Returns:

The universal argument.

Linear Temporal Logic (past) temporal operators

using namespace black::logic;

struct yesterday

An yesterday LTL formula.

Constructor:

yesterday(logic::term argument)

Parameters:

argument – The operator’s argument.

Members:

logic::term argument() const

Returns:

The operator’s argument.

struct w_yesterday

A weak yesterday LTL formula.

Constructor:

w_yesterday(logic::term argument)

Parameters:

argument – The operator’s argument.

Members:

logic::term argument() const

Returns:

The operator’s argument.

struct once

A once LTL formula.

Constructor:

once(logic::term argument)

Parameters:

argument – The operator’s argument.

Members:

logic::term argument() const

Returns:

The operator’s argument.

struct historically

An historically LTL formula.

Constructor:

historically(logic::term argument)

Parameters:

argument – The operator’s argument.

Members:

logic::term argument() const

Returns:

The operator’s argument.

struct since

A since LTL formula.

Constructor:

since(logic::term left, logic::term right)

Parameters:

• left – The universal argument.

• right – The existential argument.

Members:

logic::term left() const

Returns:

The universal argument.

logic::term right() const

Returns:

The existential argument.

struct triggered

A triggered LTL formula.

Constructor:

triggered(logic::term left, logic::term right)

Parameters:

• left – The existential argument.

• right – The universal argument.

Members:

logic::term left() const

Returns:

The existential argument.

logic::term right() const

Returns:

The universal argument.

Arithmetic operators

using namespace black::logic;

struct minus

The unary minus.

Constructor:

minus(logic::term argument)

Parameters:

argument – The operand.

Members:

logic::term argument() const

Returns:

The operand.

struct sum

An arithmetic sum.

Constructor:

sum(logic::term left, logic::term right)

Parameters:

• left – The first summand.

• right – The second summand.

Members:

logic::term left() const

Returns:

The first summand.

logic::term right() const

Returns:

The second summand.

struct product

An arithmetic product.

Constructor:

product(logic::term left, logic::term right)

Parameters:

• left – The first factor.

• right – The second factor.

Members:

logic::term left() const

Returns:

The first factor.

logic::term right() const

Returns:

The second factor.

struct difference

An arithmetic difference.

Constructor:

difference(logic::term left, logic::term right)

Parameters:

• left – The minuend.

• right – The subtrahend.

Members:

logic::term left() const

Returns:

The minuend.

logic::term right() const

Returns:

The subtrahend.

struct division

An arithmetic division.

Constructor:

division(logic::term left, logic::term right)

Parameters:

• left – The numerator.

• right – The denominator.

Members:

logic::term left() const

Returns:

The numerator.

logic::term right() const

Returns:

The denominator.

Relational comparisons

using namespace black::logic;

struct less_than

A less-than comparison.

Constructor:

less_than(logic::term left, logic::term right)

Parameters:

• left – The lower argument.

• right – The greater argument.

Members:

logic::term left() const

Returns:

The lower argument.

logic::term right() const

Returns:

The greater argument.

struct less_than_eq

A less-than-or-equal comparison.

Constructor:

less_than_eq(logic::term left, logic::term right)

Parameters:

• left – The lower argument.

• right – The greater argument.

Members:

logic::term left() const

Returns:

The lower argument.

logic::term right() const

Returns:

The greater argument.

struct greater_than

A greater-than comparison.

Constructor:

greater_than(logic::term left, logic::term right)

Parameters:

• left – The greater argument.

• right – The lower argument.

Members:

logic::term left() const

Returns:

The greater argument.

logic::term right() const

Returns:

The lower argument.

struct greater_than_eq

A greater-than-or-equal comparison.

Constructor:

greater_than_eq(logic::term left, logic::term right)

Parameters:

• left – The greater argument.

• right – The lower argument.

Members:

logic::term left() const

Returns:

The greater argument.

logic::term right() const

Returns:

The lower argument.

Basic types

using namespace black::logic::types;

struct integer

The type of integer numbers.

Constructor:

integer()

struct real

The type of real numbers.

Constructor:

real()

struct boolean

The type of boolean values.

Constructor:

boolean()

struct function

The type of functions.

Constructor:

function(std::vector<logic::types::type> parameters, logic::types::type range)

Parameters:

• parameters – The parameters types.

• range – The function’s range.

Members:

std::vector<logic::types::type> parameters() const

Returns:

The parameters types.

logic::types::type range() const

Returns:

The function’s range.

Inferred types placeholder

using namespace black::logic::types;

struct inferred

Placeholder for type inference.

Constructor:

inferred()

The error type

using namespace black::logic::types;

struct error

A logically erroneous term.

Constructor:

error(logic::term source, std::string error)

Parameters:

• source – The erroneous term.

• error – The error.

Members:

logic::term source() const

Returns:

The erroneous term.

std::string error() const

Returns:

The error.