pulsatrix::datalog::Rule Class Reference

A rule: a head atom entailed whenever every body atom is simultaneously satisfiable under one consistent variable substitution. More...

#include <datalog_rule.hpp>

Public Member Functions
	Rule (Atom head, std::vector< Atom > body)
	Constructs a rule.
const Atom &	head () const
const std::vector< Atom > &	body () const

Detailed Description

A rule: a head atom entailed whenever every body atom is simultaneously satisfiable under one consistent variable substitution.

Note

Enforces Datalog "range restriction"/safety at construction: every variable that appears in the head must also appear in at least one body atom. Without this, a rule like p(X) :- q(a). would be free to bind X to an unbounded/arbitrary constant, breaking the decidable-fragment termination guarantee this whole phase depends on (campaign doc Decision Point 1: "Datalog's decidable fragment always terminates via bottom-up fixpoint"). A rule with an empty body is never safe unless its head is also empty-arity (there is no such head shape here), so an empty body with a non-empty head always throws.

Constructor & Destructor Documentation

Rule()

pulsatrix::datalog::Rule::Rule	(	Atom	head,
		std::vector< Atom >	body
	)

Constructs a rule.

Exceptions

std::invalid_argument

if any variable in head does not appear in body (unsafe/unrestricted rule).

Member Function Documentation

body()

const std::vector< Atom > & pulsatrix::datalog::Rule::body ( ) const

inline

head()

const Atom & pulsatrix::datalog::Rule::head ( ) const

inline

---

The documentation for this class was generated from the following file:

• include/pulsatrix/datalog_rule.hpp