m::cnf Namespace Reference

Data Structures
struct	Clause
	A cnf::Clause represents a disjunction of Predicates. More...
struct	CNF
	A CNF represents a conjunction of cnf::Clauses. More...
struct	Predicate
	A Predicate contains a Expr of Boolean type in either positive or negative form. More...

Functions
Clause M_EXPORT	operator|| (const Clause &lhs, const Clause &rhs)
	Returns the logical or of two cnf::Clauses, i.e. the disjunction of the Predicates of lhs and rhs.
CNF M_EXPORT	operator&& (const Clause &lhs, const Clause &rhs)
	Returns the logical and of two cnf::Clauses, i.e. a CNF with the two cnf::Clauses lhs and rhs.
CNF M_EXPORT	operator&& (const CNF &lhs, const CNF &rhs)
	Returns the logical and of two CNFs, i.e. the conjunction of the cnf::Clauses of lhs and rhs.
CNF M_EXPORT	operator|| (const CNF &lhs, const CNF &rhs)
	Returns the logical or of two CNFs.
CNF M_EXPORT	operator! (const Clause &clause)
	Returns the logical negation of a cnf::Clause.
CNF M_EXPORT	operator! (const CNF &cnf)
	Returns the logical negation of a CNF.
CNF M_EXPORT	to_CNF (const ast::Expr &e)
	Converts the Boolean Expr e to a CNF.
CNF M_EXPORT	get_CNF (const ast::Clause &c)
	Converts the Boolean Expr of c to a CNF.

Function Documentation

get_CNF()

CNF M_EXPORT m::cnf::get_CNF

(

const ast::Clause &

c

)

Converts the Boolean Expr of c to a CNF.

operator!() [1/2]

CNF m::cnf::operator!

(

const Clause &

clause

)

Returns the logical negation of a cnf::Clause.

It is computed using [De Morgan's laws] (https://en.wikipedia.org/wiki/De_Morgan%27s_laws): ¬(P ∨ Q) ↔ ¬P ∧ ¬Q.

Definition at line 78 of file CNF.cpp.

operator!() [2/2]

CNF m::cnf::operator!

(

const CNF &

cnf

)

Returns the logical negation of a CNF.

It is computed using [De Morgan's laws] (https://en.wikipedia.org/wiki/De_Morgan%27s_laws): ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.

Definition at line 86 of file CNF.cpp.

operator&&() [1/2]

CNF m::cnf::operator&&	(	const Clause &	lhs,
		const Clause &	rhs
	)

Returns the logical and of two cnf::Clauses, i.e. a CNF with the two cnf::Clauses lhs and rhs.

Definition at line 45 of file CNF.cpp.

operator&&() [2/2]

CNF m::cnf::operator&&	(	const CNF &	lhs,
		const CNF &	rhs
	)

Returns the logical and of two CNFs, i.e. the conjunction of the cnf::Clauses of lhs and rhs.

Definition at line 53 of file CNF.cpp.

operator||() [1/2]

cnf::Clause m::cnf::operator||	(	const Clause &	lhs,
		const Clause &	rhs
	)

Returns the logical or of two cnf::Clauses, i.e. the disjunction of the Predicates of lhs and rhs.

Definition at line 36 of file CNF.cpp.

operator||() [2/2]

CNF m::cnf::operator||	(	const CNF &	lhs,
		const CNF &	rhs
	)

Returns the logical or of two CNFs.

It is computed using the distributive law from Boolean algebra: P ∨ (Q ∧ R) ↔ ((P ∨ Q) ∧ (P ∨ R))

Definition at line 62 of file CNF.cpp.

to_CNF()

CNF m::cnf::to_CNF

(

const ast::Expr &

e

)

Converts the Boolean Expr e to a CNF.

Definition at line 298 of file CNF.cpp.

References CNFGenerator::get().