smtrat::covering_ng::formula::GraphEvaluation Class Reference

#include <FormulaEvaluationGraph.h>

Collaboration diagram for smtrat::covering_ng::formula::GraphEvaluation:

Public Types
enum	BooleanExploration { OFF , PROPAGATION , EXPLORATION , EXPLORATION_ONLY_BOOL }

Public Member Functions
	GraphEvaluation (cadcells::datastructures::Projections proj, ImplicantOrdering implicant_complexity_ordering, std::size_t results, ConstraintOrdering constraint_complexity_ordering, bool stop_evaluation_on_conflict, bool preprocess, bool postprocess, BooleanExploration boolean_exploration)
void	set_formula (const FormulaT &f)
void	extend_valuation (const cadcells::Assignment &ass)
void	revert_valuation (const cadcells::Assignment &ass)
std::vector< boost::container::flat_set< cadcells::datastructures::PolyConstraint > >	compute_implicants ()
Valuation	root_valuation () const

Private Member Functions
formula_ds::Formula::Reasons	explore (formula_ds::FormulaGraph &graph)

Private Attributes
cadcells::datastructures::Projections	m_proj
formula_ds::FormulaGraph	true_graph
formula_ds::FormulaGraph	false_graph
formula_ds::VariableToFormula	vartof
cadcells::Assignment	assignment
boost::container::flat_map< formula_ds::FormulaID, bool >	m_decisions
formula_ds::Formula::Reasons	m_true_conflict_reasons
formula_ds::Formula::Reasons	m_false_conflict_reasons
ImplicantOrdering	m_implicant_complexity_ordering
std::size_t	m_results
ConstraintOrdering	m_constraint_complexity_ordering
bool	m_stop_evaluation_on_conflict
bool	m_preprocess
bool	m_postprocess
BooleanExploration	m_boolean_exploration

Detailed Description

Definition at line 76 of file FormulaEvaluationGraph.h.

Member Enumeration Documentation

BooleanExploration

enum smtrat::covering_ng::formula::GraphEvaluation::BooleanExploration

Enumerator
OFF
PROPAGATION
EXPLORATION
EXPLORATION_ONLY_BOOL

Definition at line 79 of file FormulaEvaluationGraph.h.

Constructor & Destructor Documentation

GraphEvaluation()

smtrat::covering_ng::formula::GraphEvaluation::GraphEvaluation ( cadcells::datastructures::Projections  proj, ImplicantOrdering  implicant_complexity_ordering, std::size_t  results, ConstraintOrdering  constraint_complexity_ordering, bool  stop_evaluation_on_conflict, bool  preprocess, bool  postprocess, BooleanExploration  boolean_exploration  )

inline

Definition at line 103 of file FormulaEvaluationGraph.h.

Member Function Documentation

compute_implicants()

std::vector< boost::container::flat_set< cadcells::datastructures::PolyConstraint > > smtrat::covering_ng::formula::GraphEvaluation::compute_implicants

(

)

Definition at line 916 of file FormulaEvaluationGraph.cpp.

Here is the call graph for this function:

explore()

formula_ds::Formula::Reasons smtrat::covering_ng::formula::GraphEvaluation::explore ( formula_ds::FormulaGraph &  graph )

private

Definition at line 759 of file FormulaEvaluationGraph.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

extend_valuation()

void smtrat::covering_ng::formula::GraphEvaluation::extend_valuation

(

const cadcells::Assignment &

ass

)

Definition at line 803 of file FormulaEvaluationGraph.cpp.

Here is the call graph for this function:

revert_valuation()

void smtrat::covering_ng::formula::GraphEvaluation::revert_valuation

(

const cadcells::Assignment &

ass

)

Definition at line 852 of file FormulaEvaluationGraph.cpp.

Here is the call graph for this function:

root_valuation()

Valuation smtrat::covering_ng::formula::GraphEvaluation::root_valuation

(

)

const

Definition at line 952 of file FormulaEvaluationGraph.cpp.

Here is the caller graph for this function:

set_formula()

void smtrat::covering_ng::formula::GraphEvaluation::set_formula

(

const FormulaT &

f

)

Definition at line 711 of file FormulaEvaluationGraph.cpp.

Here is the call graph for this function:

Field Documentation

assignment

cadcells::Assignment smtrat::covering_ng::formula::GraphEvaluation::assignment

private

Definition at line 87 of file FormulaEvaluationGraph.h.

false_graph

formula_ds::FormulaGraph smtrat::covering_ng::formula::GraphEvaluation::false_graph

private

Definition at line 85 of file FormulaEvaluationGraph.h.

m_boolean_exploration

BooleanExploration smtrat::covering_ng::formula::GraphEvaluation::m_boolean_exploration

private

Definition at line 98 of file FormulaEvaluationGraph.h.

m_constraint_complexity_ordering

ConstraintOrdering smtrat::covering_ng::formula::GraphEvaluation::m_constraint_complexity_ordering

private

Definition at line 94 of file FormulaEvaluationGraph.h.

m_decisions

boost::container::flat_map<formula_ds::FormulaID, bool> smtrat::covering_ng::formula::GraphEvaluation::m_decisions

private

Definition at line 88 of file FormulaEvaluationGraph.h.

m_false_conflict_reasons

formula_ds::Formula::Reasons smtrat::covering_ng::formula::GraphEvaluation::m_false_conflict_reasons

private

Definition at line 90 of file FormulaEvaluationGraph.h.

m_implicant_complexity_ordering

ImplicantOrdering smtrat::covering_ng::formula::GraphEvaluation::m_implicant_complexity_ordering

private

Definition at line 92 of file FormulaEvaluationGraph.h.

m_postprocess

bool smtrat::covering_ng::formula::GraphEvaluation::m_postprocess

private

Definition at line 97 of file FormulaEvaluationGraph.h.

m_preprocess

bool smtrat::covering_ng::formula::GraphEvaluation::m_preprocess

private

Definition at line 96 of file FormulaEvaluationGraph.h.

m_proj

cadcells::datastructures::Projections smtrat::covering_ng::formula::GraphEvaluation::m_proj

private

Definition at line 82 of file FormulaEvaluationGraph.h.

m_results

std::size_t smtrat::covering_ng::formula::GraphEvaluation::m_results

private

Definition at line 93 of file FormulaEvaluationGraph.h.

m_stop_evaluation_on_conflict

bool smtrat::covering_ng::formula::GraphEvaluation::m_stop_evaluation_on_conflict

private

Definition at line 95 of file FormulaEvaluationGraph.h.

m_true_conflict_reasons

formula_ds::Formula::Reasons smtrat::covering_ng::formula::GraphEvaluation::m_true_conflict_reasons

private

Definition at line 89 of file FormulaEvaluationGraph.h.

true_graph

formula_ds::FormulaGraph smtrat::covering_ng::formula::GraphEvaluation::true_graph

private

Definition at line 84 of file FormulaEvaluationGraph.h.

vartof

formula_ds::VariableToFormula smtrat::covering_ng::formula::GraphEvaluation::vartof

private

Definition at line 86 of file FormulaEvaluationGraph.h.

---

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

• smtrat-coveringng/FormulaEvaluationGraph.h
• smtrat-coveringng/FormulaEvaluationGraph.cpp