FOF Class Reference

Representation of first order formulas. More...

#include <FOF.hpp>

Public Member Functions
	FOF ()=delete
	You don't want this constructor.
	FOF (FOFType t)
	You probably don't want this constructor.
	FOF (const Literal &)
	Construct FOF from Literal.
	FOF (FOFType, const vector< FOF > &, Variable *)
	Construct FOF for a non-literal.
void	show_indexes () const
	Show the indices.
FOFType	fof_type ()
	Basic get method.
void	add_formula (const FOF &f)
	Add a subformula.
void	clear ()
	Make an FOFType::Empty.
bool	is_literal () const
	Check if an FOF is a literal.
bool	is_clause () const
	Check if something is a clause.
void	remove_negation ()
	Remove the leading negation from an arbitrary FOF, if it has one.
void	negate ()
	Negate an FOF, applying obvious simplifications if it's already negated or an implication.
void	remove_iff ()
	Replace <-> throughout using ->.
void	remove_imp ()
	Replace A->B throughout with neg A v B.
void	make_unique_bound_variables ()
	Replace all bound variables with unique new ones.
void	push_negs ()
	Push all negations in.
void	convert_to_nnf ()
	Convert to Negation Normal Form.
void	miniscope ()
	Apply the rules for miniscoping.
void	convert_to_cnf ()
	Convert to Conjunctive Normal Form.
void	skolemize ()
	Skolemize the given formula.
void	remove_universal_quantifiers ()
	Self-explanatory.
void	to_Literal (Literal &) const
	Assuming the FOF is a literal, convert it to something of type Literal.
void	to_clause (Clause &) const
	Assuming you have an FOF that's just a clause, convert it to something of Clause type.
void	to_clauses (vector< Clause > &) const
	Assuming you have a flattened CNF, convert it to a collection of Clauses.
bool	has_and () const
	Does the collection of subformulas contain an AND?
void	collect_ors ()
	Assuming you just have a structure containing ORs, ANDs and literals, re-arrange it to make it easier to do distribution of ORs.
void	distribute_or ()
	Distribute ORs to the maximum extent possible.
void	flatten_ands ()
	Assuming you have a conjunction of CNFs, get rid of the initial AND.
void	flatten ()
	After distributing ORs, flatten into something directly in CNF form.
string	to_string () const

Static Public Member Functions
static void	set_indexes (std::tuple< VariableIndex *, FunctionIndex *, PredicateIndex *, TermIndex * > is)
	Set up pointer to the variable index etc.
static FOF	make_literal (const Literal &lit)
	Directly make a Literal.
static FOF	make_neg (const FOF &f)
	Directly negate a FOF.
static FOF	make_and (const vector< FOF > &fs)
	Directly make a conjunction.
static FOF	make_or (const vector< FOF > &fs)
	Directly make a disjunction.
static FOF	make_imp (const FOF &lhs, const FOF &rhs)
	Directly make an implication.
static FOF	make_iff (const FOF &lhs, const FOF &rhs)
	Directly make an iff.
static FOF	make_forall (const FOF &f, Variable *v)
	Directly make a universally quantified FOF.
static FOF	make_exists (const FOF &f, Variable *v)
	Directly make an existentially quantified FOF.

Friends
ostream &	operator<< (ostream &, const FOF &)

Detailed Description

Representation of first order formulas.

First and foremost: I intensely dislike the use of inheritance. I vastly prefer to make the methods static and do everything the obvioous way. If you want the alternative sort of OO , then feel free to implement this yourself.

This has to play nicely with the parser and with the indexing of terms, variables and so on, so it needs pointers to the relevant indices.

Constructor & Destructor Documentation

FOF() [1/2]

FOF::FOF

(

const Literal &

lit

)

Construct FOF from Literal.

Parameters

lit	Reference to Literal to use.

FOF() [2/2]

FOF::FOF	(	FOFType	t,
		const vector< FOF > &	sf,
		Variable *	v
	)

Construct FOF for a non-literal.

Parameters

t	Specify FOFType for what you're making.
sf	Reference to vecgtor of FOF for subformulas.
v	Pointer to Variable.

Member Function Documentation

convert_to_cnf()

void FOF::convert_to_cnf

(

)

Convert to Conjunctive Normal Form.

Follow the usual recipe (Larry's lecture notes.) BUT there are lots of ways to do this, so I need to expand this comment.

convert_to_nnf()

void FOF::convert_to_nnf

(

)

Convert to Negation Normal Form.

Follows the usual recipe (Larry's lecture notes.)

distribute_or()

void FOF::distribute_or

(

)

Distribute ORs to the maximum extent possible.

Assumes you have nothing but a quantifier-free NNF. The result will have a tree structure with ANDs at the top, then ORs, then literals. Use flatten to get it into a nicer format

flatten()

void FOF::flatten

(

)

After distributing ORs, flatten into something directly in CNF form.

Last step before applying to_clauses.

is_clause()

bool FOF::is_clause

(

)

const

Check if something is a clause.

This check in the strict sense: either it must be a literal or a disjunction of literals, including an empty disjunction.

Returns false if FOFType::Empty.

is_literal()

bool FOF::is_literal

(

)

const

Check if an FOF is a literal.

Works in general, not just for NNF.

make_neg()

static FOF FOF::make_neg ( const FOF &  f )

inlinestatic

Directly negate a FOF.

Careful: no attempt here to make any obvious simplifications.

make_unique_bound_variables()

void FOF::make_unique_bound_variables

(

)

Replace all bound variables with unique new ones.

Has to be done with care to maintain the indexes correctly.

miniscope()

void FOF::miniscope

(

)

Apply the rules for miniscoping.

Push the quantifiers in as much as you can. Don't use this unless your formula is in NNF.

push_negs()

void FOF::push_negs

(

)

Push all negations in.

DON'T call it on anything with a -> or <->.

skolemize()

void FOF::skolemize

(

)

Skolemize the given formula.

All the hard work is done by skolemize_main.

See also

skolemize_main

to_clause()

void FOF::to_clause

(

Clause &

c

)

const

Assuming you have an FOF that's just a clause, convert it to something of Clause type.

DON't use this unless your FOF is either a literal or a disjunction of literals.

to_clauses()

void FOF::to_clauses

(

vector< Clause > &

cs

)

const

Assuming you have a flattened CNF, convert it to a collection of Clauses.

A flattened FOF here means a literal, a single disjunction of literals, or a conjunction of literals and disjunctions of literals.

to_Literal()

void FOF::to_Literal

(

Literal &

new_lit

)

const

Assuming the FOF is a literal, convert it to something of type Literal.

This is straightforward as most of the heavy lifting has already been done. DON'T use it on an FOF that isn't in the form of a literal.

---

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

• FOF.hpp
• FOF.cpp