smtrat::covering_ng::formula::formula_ds Namespace Reference

Data Structures
struct	overloaded
struct	FormulaClassification
struct	TRUE
struct	FALSE
struct	NOT
struct	AND
struct	OR
struct	IFF
struct	XOR
struct	BOOL
struct	CONSTRAINT
struct	Formula
struct	FormulaGraph

Typedefs
using	FormulaID = unsigned
using	FormulaDB = std::vector< Formula >
using	VariableToFormula = boost::container::flat_map< carl::Variable, std::vector< FormulaID > >

Enumerations
enum	CompareResult { SUBSET , SUPSET , EQ , NONE }

Functions
template<class... Ts>
	overloaded (Ts...) -> overloaded< Ts... >
void	print (std::ostream &stream, const FormulaDB &db, const FormulaID id, const std::size_t level)
void	log (const FormulaDB &db, const FormulaID id)
FormulaID	to_formula_db (cadcells::datastructures::Projections &c, const FormulaT &f, FormulaDB &db, VariableToFormula &vartof, std::map< std::size_t, FormulaID > &cache)
CompareResult	compare (const Formula::Reason &a, const Formula::Reason &b)
bool	merge_reason (Formula::Reasons &set, const Formula::Reason &add)
bool	merge_reasons (Formula::Reasons &set, const Formula::Reasons &adds)
Formula::Reason	merge (const Formula::Reason &a, const Formula::Reason &b)
Formula::Reasons	combine_reasons (const Formula::Reasons &a, const Formula::Reasons &b)
FormulaClassification	classify_formulas (const FormulaDB &db, const std::vector< FormulaID > &formulas)

Typedef Documentation

FormulaDB

using smtrat::covering_ng::formula::formula_ds::FormulaDB = typedef std::vector<Formula>

Definition at line 56 of file FormulaEvaluationGraph.h.

FormulaID

using smtrat::covering_ng::formula::formula_ds::FormulaID = typedef unsigned

Definition at line 10 of file FormulaEvaluationGraph.h.

VariableToFormula

using smtrat::covering_ng::formula::formula_ds::VariableToFormula = typedef boost::container::flat_map<carl::Variable, std::vector<FormulaID> >

Definition at line 57 of file FormulaEvaluationGraph.h.

Enumeration Type Documentation

CompareResult

enum smtrat::covering_ng::formula::formula_ds::CompareResult

Enumerator
SUBSET
SUPSET
EQ
NONE

Definition at line 203 of file FormulaEvaluationGraph.cpp.

Function Documentation

classify_formulas()

FormulaClassification smtrat::covering_ng::formula::formula_ds::classify_formulas	(	const FormulaDB &	db,
		const std::vector< FormulaID > &	formulas
	)

Definition at line 315 of file FormulaEvaluationGraph.cpp.

Here is the caller graph for this function:

combine_reasons()

Formula::Reasons smtrat::covering_ng::formula::formula_ds::combine_reasons	(	const Formula::Reasons &	a,
		const Formula::Reasons &	b
	)

Definition at line 298 of file FormulaEvaluationGraph.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

compare()

CompareResult smtrat::covering_ng::formula::formula_ds::compare	(	const Formula::Reason &	a,
		const Formula::Reason &	b
	)

Definition at line 205 of file FormulaEvaluationGraph.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

log()

void smtrat::covering_ng::formula::formula_ds::log	(	const FormulaDB &	db,
		const FormulaID	id
	)

Definition at line 79 of file FormulaEvaluationGraph.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

merge()

Formula::Reason smtrat::covering_ng::formula::formula_ds::merge	(	const Formula::Reason &	a,
		const Formula::Reason &	b
	)

Definition at line 268 of file FormulaEvaluationGraph.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

merge_reason()

bool smtrat::covering_ng::formula::formula_ds::merge_reason	(	Formula::Reasons &	set,
		const Formula::Reason &	add
	)

Definition at line 222 of file FormulaEvaluationGraph.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

merge_reasons()

bool smtrat::covering_ng::formula::formula_ds::merge_reasons	(	Formula::Reasons &	set,
		const Formula::Reasons &	adds
	)

Definition at line 240 of file FormulaEvaluationGraph.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

overloaded()

template<class... Ts>

smtrat::covering_ng::formula::formula_ds::overloaded

(

Ts...

)

-> overloaded< Ts... >

print()

void smtrat::covering_ng::formula::formula_ds::print	(	std::ostream &	stream,
		const FormulaDB &	db,
		const FormulaID	id,
		const std::size_t	level
	)

Definition at line 20 of file FormulaEvaluationGraph.cpp.

Here is the caller graph for this function:

to_formula_db()

FormulaID smtrat::covering_ng::formula::formula_ds::to_formula_db	(	cadcells::datastructures::Projections &	c,
		const FormulaT &	f,
		FormulaDB &	db,
		VariableToFormula &	vartof,
		std::map< std::size_t, FormulaID > &	cache
	)

Definition at line 88 of file FormulaEvaluationGraph.cpp.

Here is the call graph for this function:

Here is the caller graph for this function: