Symbolic formula representing conjunctions (f1 ∧ ... More...

#include </home/soonhokong/work/dreal4/third_party/com_github_robotlocomotion_drake/dreal/symbolic/symbolic_formula_cell.h>

Inheritance diagram for FormulaAnd:

Public Member Functions
	FormulaAnd (std::set< Formula > formulas)
	Constructs from `formulas`. More...

	FormulaAnd (const Formula &f1, const Formula &f2)
	Constructs `f1` ∧ `f2`. More...

bool	Evaluate (const Environment &env) const override
	Evaluates under a given environment. More...

Formula	Substitute (const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override
	Returns a Formula obtained by replacing all occurrences of the variables in `s` in the current formula cell with the corresponding expressions in `s`.

std::ostream &	Display (std::ostream &os) const override
	Outputs string representation of formula into output stream `os`. More...

Public Member Functions inherited from NaryFormulaCell
	NaryFormulaCell ()=delete
	Default constructor (deleted). More...

	~NaryFormulaCell () override=default
	Default destructor (deleted). More...

	NaryFormulaCell (NaryFormulaCell &&f)=delete
	Move-construct a formula from an rvalue (DELETED). More...

	NaryFormulaCell (const NaryFormulaCell &f)=delete
	Copy-construct a formula from an lvalue (DELETED). More...

NaryFormulaCell &	operator= (NaryFormulaCell &&f)=delete
	Move-assign (DELETED). More...

NaryFormulaCell &	operator= (const NaryFormulaCell &f)=delete
	Copy-assign (DELETED). More...

	NaryFormulaCell (FormulaKind k, std::set< Formula > formulas)
	Construct NaryFormulaCell of kind `k` with `formulas`. More...

bool	EqualTo (const FormulaCell &f) const override
	Checks structural equality. More...

bool	Less (const FormulaCell &f) const override
	Checks ordering. More...

const std::set< Formula > &	get_operands () const
	Returns the formulas. More...

std::set< Formula > &	get_mutable_operands ()
	Returns the formulas. More...

Public Member Functions inherited from FormulaCell
	FormulaCell ()=delete
	Default constructor (DELETED). More...

FormulaCell &	operator= (FormulaCell &&f)=delete
	Move-assign (DELETED). More...

	FormulaCell (const FormulaCell &f)=delete
	Copy-construct a formula from an lvalue. More...

	FormulaCell (FormulaCell &&f)=delete
	Move-construct a formula from an rvalue (DELETED). More...

FormulaCell &	operator= (const FormulaCell &f)=delete
	Copy-assign (DELETED). More...

FormulaKind	get_kind () const
	Returns kind of formula. More...

size_t	get_hash () const
	Returns hash of formula. More...

const Variables &	GetFreeVariables () const
	Returns set of free variables in formula. More...

unsigned	use_count () const
	Returns the reference count of this cell. More...

bool	include_ite () const
	Returns true if this symbolic formula includes an ITE (If-Then-Else) expression. More...

Additional Inherited Members
Protected Member Functions inherited from NaryFormulaCell
std::ostream &	DisplayWithOp (std::ostream &os, const std::string &op) const

Protected Member Functions inherited from FormulaCell
	FormulaCell (FormulaKind k, size_t hash, bool include_ite, Variables variables)
	Construct FormulaCell of kind `k` with `hash`. More...

virtual	~FormulaCell ()=default
	Default destructor. More...

Formula	GetFormula ()
	Returns a Formula pointing to this FormulaCell. More...

Detailed Description

Symbolic formula representing conjunctions (f1 ∧ ...

∧ fn).

Constructor & Destructor Documentation

◆ FormulaAnd() [1/2]

FormulaAnd ( std::set< Formula > formulas )

explicit

Constructs from formulas.

◆ FormulaAnd() [2/2]

FormulaAnd	(	const Formula &	f1,
		const Formula &	f2
	)

Constructs f1 ∧ f2.

Member Function Documentation

◆ Display()

ostream & Display ( std::ostream & os ) const

overridevirtual

Outputs string representation of formula into output stream os.

Implements FormulaCell.

◆ Evaluate()

bool Evaluate ( const Environment & env ) const

overridevirtual

Evaluates under a given environment.