FOF Member List

This is the complete list of members for FOF, including all inherited members.

add_formula(const FOF &f)	FOF	inline
clear()	FOF	inline
convert_to_clauses(vector< Clause > &) const	FOF
convert_to_cnf_clauses(vector< Clause > &)	FOF
convert_to_nnf()	FOF
definitional_convert_to_cnf_clauses(vector< Clause > &)	FOF
distribute_and()	FOF
distribute_and_once()	FOF	private
distribute_or()	FOF
distribute_or_once()	FOF	private
dnf_invert_and_convert_to_clauses(vector< Clause > &) const	FOF
find_and() const	FOF
find_definitional_tuple(FOF &, vector< FOF > &, bool)	FOF
find_free_variables() const	FOF
find_or() const	FOF
FOF()=delete	FOF
FOF(FOFType t)	FOF	inline
FOF(const Literal &)	FOF
FOF(FOFType, const vector< FOF > &, Variable *)	FOF
fof_type()	FOF	inline
fun_index	FOF	privatestatic
has_free_variable(Variable *)	FOF	private
invert_literal()	FOF
is_clause() const	FOF
is_literal() const	FOF
make_and(const vector< FOF > &fs)	FOF	inlinestatic
make_definitional_predicate() const	FOF	private
make_exists(const FOF &f, Variable *v)	FOF	inlinestatic
make_forall(const FOF &f, Variable *v)	FOF	inlinestatic
make_iff(const FOF &lhs, const FOF &rhs)	FOF	inlinestatic
make_imp(const FOF &lhs, const FOF &rhs)	FOF	inlinestatic
make_literal(const Literal &lit)	FOF	inlinestatic
make_neg(const FOF &f)	FOF	inlinestatic
make_or(const vector< FOF > &fs)	FOF	inlinestatic
make_skolem_function(const vector< Term * > &)	FOF	private
make_unique_bound_variables()	FOF
miniscope()	FOF
miniscope_all()	FOF	private
miniscope_split(Variable *, vector< FOF > &, vector< FOF > &)	FOF	private
negate()	FOF
operator<< (defined in FOF)	FOF	friend
pred	FOF	private
pred_index	FOF	privatestatic
push_negs()	FOF
remove_existential_quantifiers()	FOF
remove_iff()	FOF
remove_imp()	FOF
remove_negation()	FOF
remove_redundant_quantifiers()	FOF
remove_universal_quantifiers()	FOF
replace_variable(Variable *, Variable *)	FOF	private
replace_variable_with_term(Term *, Variable *)	FOF	private
set_indexes(std::tuple< VariableIndex *, FunctionIndex *, PredicateIndex *, TermIndex * > is)	FOF	inlinestatic
show_indexes() const	FOF	inline
simple_negate()	FOF
simplify_cnf(vector< Clause > &)	FOF	static
simplify_cnf(vector< Clause > &, vector< string > &)	FOF	static
skolemize()	FOF
skolemize_main(vector< Term * >)	FOF	private
skolemize_universals()	FOF
skolemize_universals_main(vector< Term * >)	FOF	private
split_sub_formulas(vector< FOF > &, vector< FOF > &)	FOF
sub_formulas	FOF	private
term_index	FOF	privatestatic
to_Literal(Literal &) const	FOF
to_string() const	FOF
type	FOF	private
var	FOF	private
var_index	FOF	privatestatic