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_clauses (vector< Clause > &)
	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	convert_to_clauses (vector< Clause > &) const
	Assuming you have a CNF, convert it to a collection of Clauses.
size_t	find_and () const
	Does the collection of subformulas contain an AND? If so, find it.
bool	distribute_or_once ()
	Find an OR that can be distributed and deal with it. Indicate if there isn't one.
void	distribute_or ()
string	to_string () const
	Convert a FOF into a nice-looking string.

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.
static SimplificationResult	simplify_cnf (vector< Clause > &)
	Simplify the clauses in a CNF using the method in Clause.

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 vector of FOF for subformulas.
v	Pointer to Variable.

Member Function Documentation

convert_to_cnf_clauses()

void FOF::convert_to_cnf_clauses

(

vector< Clause > &

cs

)

Convert to Conjunctive Normal Form.

Follow the usual recipe (Larry's lecture notes.) BUT there are lots of ways to do this—at present there is nothing sophisticated happening, and the approach is entirely obvious/straightforward.

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.

find_and()

size_t FOF::find_and

(

)

const

Does the collection of subformulas contain an AND? If so, find it.

Note: does not do any recursion – only looks at the top level.

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_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