PNF.h File Reference

#include "../Formula.h"
#include "Substitution.h"
#include "aux.h"

Include dependency graph for PNF.h:

Go to the source code of this file.

Namespaces
	carl
	carl is the main namespace for the library.

Typedefs
using	carl::QuantifierPrefix = std::vector< std::pair< Quantifier, carl::Variable > >

Enumerations
enum class	carl::Quantifier { carl::EXISTS , carl::FORALL , carl::FREE }

Functions
std::ostream &	carl::operator<< (std::ostream &os, const Quantifier &type)
template<typename Poly >
Formula< Poly >	carl::to_pnf (const Formula< Poly > &f, QuantifierPrefix &reverse_prefix, boost::container::flat_set< Variable > &used_vars, bool negated=false)
template<typename Poly >
void	carl::free_variables (const Formula< Poly > &f, boost::container::flat_set< Variable > &current_quantified_vars, boost::container::flat_set< Variable > &free_vars)
template<typename Poly >
auto	carl::free_variables (const Formula< Poly > &f)
template<typename Poly >
std::pair< QuantifierPrefix, Formula< Poly > >	carl::to_pnf (const Formula< Poly > &f)
	Transforms this formula to its equivalent in prenex normal form. More...
template<typename Poly >
Formula< Poly >	carl::to_formula (const QuantifierPrefix &prefix, const Formula< Poly > &matrix)