Implementation of NNF (Negation Normal Form) conversion. More...

#include <Nnfizer.h>

Inheritance diagram for dlinear::Nnfizer:

Public Member Functions
Formula	Process (const Formula &f, bool push_negation_into_relationals=false) const
	Convert a `f` into an equivalent formula `f'` in NNF.

Public Member Functions inherited from dlinear::GenericFormulaVisitor< Formula, Args... >
const IterationStats &	stats () const
	Get read-only access to the statistics of the FormulaVisitor.

const Config &	config () const
	Get read-only access to the configuration of the FormulaVisitor.

Private Member Functions
Formula	VisitFalse (const Formula &f, bool polarity, bool push_negation_into_relationals) const override
	Convert `f` into an equivalent formula `f'` in NNF.

Additional Inherited Members
Protected Member Functions inherited from dlinear::FormulaVisitor< bool, bool >
	FormulaVisitor (const Config &config, const std::string &class_name="FormulaVisitor")
	Construct a new FormulaVisitor object with the given `config`.

Protected Member Functions inherited from dlinear::GenericFormulaVisitor< Formula, Args... >
	GenericFormulaVisitor (const Config &config, const std::string &class_name="GenericFormulaVisitor")
	Construct a new FormulaVisitor object with the given `config`.

Protected Attributes inherited from dlinear::GenericFormulaVisitor< Formula, Args... >
const Config &	config_
	Configuration.

IterationStats	stats_
	Statistics.

Detailed Description

Implementation of NNF (Negation Normal Form) conversion.

When push_negation_into_relationals is true, it pushes negations into relational formulas by flipping relational

Definition at line 24 of file Nnfizer.h.

Member Function Documentation

Formula dlinear::Nnfizer::Process	(	const Formula &	f,
		bool	push_negation_into_relationals = false ) const

nodiscard

Convert a f into an equivalent formula f' in NNF.

Parameters

f	formula to be converted
push_negation_into_relationals	whether to push negation into relational formulas

Definition at line 17 of file Nnfizer.cpp.

Formula dlinear::Nnfizer::VisitFalse	(	const Formula &	f,
		bool	polarity,
		bool	push_negation_into_relationals ) const

nodiscardoverrideprivate

Convert f into an equivalent formula f' in NNF.

The parameter polarity is to indicate whether it processes f (if polarity is true) or ¬f (if polarity is false).

Parameters

f	formula to be converted
polarity	whether to process `f` or `¬f`
push_negation_into_relationals	whether to push negation into relational formulas

Definition at line 27 of file Nnfizer.cpp.

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