FOF Class Reference

Representation of first order formulas. More...

#include <FOF.hpp>

Collaboration diagram for FOF:

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	simple_negate ()
	Negate an FOF without applying any simplifications.
void	invert_literal ()
	Self-explanatory!
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	remove_redundant_quantifiers ()
	Remove quantifiers if they don't bind anything in their scope.
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 > &, vector< string > &, const string &)
	Convert to Conjunctive Normal Form.
void	split_sub_formulas (vector< FOF > &, vector< FOF > &)
	Split subformulas in half.
void	find_definitional_tuple (FOF &, vector< FOF > &, vector< FOF > &, bool)
	Heavy-lifting for conversion to definitional clause form.
void	definitional_convert_to_cnf_clauses (vector< Clause > &, vector< string > &, const string &)
	Convert to Conjunctive Normal Form using a form of definitional conversion.
void	skolemize ()
	Skolemize the given formula.
void	remove_universal_quantifiers ()
	Self-explanatory.
void	skolemize_universals ()
	Skolemize the universal quantifiers in the given formula.
void	remove_existential_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.
void	dnf_invert_and_convert_to_clauses (vector< Clause > &) const
	Assuming you have a DNF, invert it and convert it to a collection of CNF clauses.
size_t	find_and () const
	Does the collection of subformulas contain an AND? If so, find it.
size_t	find_or () const
	Does the collection of subformulas contain an OR? If so, find it.
void	distribute_or ()
	Distribute ORs to the maximum extent possible.
void	distribute_and ()
	Distribute ANDs to the maximum extent possible.
string	to_string () const
	Convert a FOF into a nice-looking string.
string	to_tptp_string (bool=false) const
	Convert a FOF into a nice-looking string in the TPTP format.
string	predicate_to_tptp_string () const
	Assuming this is an Atom, return the predicate name as a string.
set< Term * >	find_free_variables () const
	Find the free variables in the formula.

Static Public Member Functions
static void	set_indexes (std::tuple< VariableIndex *, FunctionIndex *, PredicateIndex *, TermIndex * > is)
	Set up pointer to the variable index etc.
static void	set_recs_p (TPTPRecords *_p)
	Set up the pointer allowing TPTP outputs to be added.
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.
static SimplificationResult	simplify_cnf (vector< Clause > &, vector< string > &, vector< string > &)
	As first version of simplify_cnf, but keep track of corresponding roles as well.

Private Member Functions
bool	has_free_variable (Variable *)
	Does this formula contain the specified variable unbound?
void	replace_variable (Variable *, Variable *)
	Self-explanatory.
Term *	make_skolem_function (const vector< Term * > &)
	Make a new Skolem function.
void	replace_variable_with_term (Term *, Variable *)
	Replace a Variable with a Term.
void	skolemize_main (vector< Term * >, FOF *, bool=false)
	Main helper function called by FOF::skolemize().
void	skolemize_universals_main (vector< Term * >, FOF *, bool=false)
	The dual of skolemize_main.
void	miniscope_split (Variable *, vector< FOF > &, vector< FOF > &)
	Helper for miniscope.
void	miniscope_all ()
	Apply miniscoping to all subformulas.
FOF	make_definitional_predicate () const
	When doing definitional clause conversion you need to be able to make unique new predicates. This will provide one.
bool	distribute_or_once ()
	Find an OR that can be distributed and deal with it. Indicate if there isn't one.
bool	distribute_and_once ()
	Find an AND that can be distributed and deal with it. Indicate if there isn't one.

Private Attributes
FOFType	type
	Used for all FOFs to denote what kind it it.
Literal	pred
	FOFType::Atom can store one of these to represent a Literal.
vector< FOF >	sub_formulas
	Most FOFs will have subformulas.
Variable *	var
	Associate a Variable with a quantifier.

Static Private Attributes
static TPTPRecords *	recs_p = nullptr
	Allow FOF to add TPTP outputs.
static VariableIndex *	var_index = nullptr
	Access to the index: static because all FOFs should share it.
static FunctionIndex *	fun_index = nullptr
	Access to the index: static because all FOFs should share it.
static TermIndex *	term_index = nullptr
	Access to the index: static because all FOFs should share it.
static PredicateIndex *	pred_index = nullptr
	Access to the index: static because all FOFs should share it.

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

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.

Definition at line 58 of file FOF.hpp.

Constructor & Destructor Documentation

FOF() [1/3]

FOF::FOF ( FOFType t )

inline

You probably don't want this constructor.

Definition at line 219 of file FOF.hpp.

  : type(t), pred(), sub_formulas(), var(nullptr) {}

FOF() [2/3]

FOF::FOF

(

const Literal &

lit

)

Construct FOF from Literal.

Parameters

lit	Reference to Literal to use.

Definition at line 347 of file FOF.cpp.

: sub_formulas()
, var(nullptr)
{
  if (lit.is_positive()) {
    type = FOFType::Atom;
    pred = lit;
  }
  else {
    pred.clear();
    type = FOFType::Neg;
    Literal lit_copy = lit;
    lit_copy.make_positive();
    FOF f(lit_copy);
    sub_formulas.push_back(f);
  }
}

FOF() [3/3]

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.

Definition at line 365 of file FOF.cpp.

: type(t)
, pred()
, sub_formulas(sf)
, var(v)
{
  switch (t) {
      case FOFType::Atom:
        cerr << "Stop it! You can't make an atom with this constructor!" << endl;
        break;
      case FOFType::Neg:
      case FOFType::And:
      case FOFType::Or:
      case FOFType::Imp:
      case FOFType::Iff:
        // Easy as the work gets done above.
        if (var != nullptr) {
          cerr << "Are you sure you want to associate a variable with something that's not a quantifier?" << endl;
          var = nullptr;
        }
        break;
      case FOFType::A:
      case FOFType::E:
        if (sf.size() != 1) {
          cerr << "Careful! A quantifier should only have one subformula." << endl;
        }
        if (v == nullptr) {
          cerr << "Careful! A quantifier needs a variable." << endl;
        }
        break;
      default:
        break;
  }
}

Member Function Documentation

add_formula()

void FOF::add_formula ( const FOF & f )

inline

Add a subformula.

Definition at line 272 of file FOF.hpp.

{ sub_formulas.push_back(f); }

clear()

void FOF::clear ( )

inline

Make an FOFType::Empty.

Definition at line 276 of file FOF.hpp.

               { 
    type = FOFType::Empty; 
    pred.clear(); 
    sub_formulas.clear();
     var = nullptr; 
  }

convert_to_clauses()

void FOF::convert_to_clauses

(

vector< Clause > &

cs

)

const

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

Definition at line 1169 of file FOF.cpp.

                                                     {
  cs.clear();
  if (is_literal()) {
    Literal new_lit;
    to_Literal(new_lit);
    Clause new_c;
    new_c.add_lit(new_lit);
    cs.push_back(new_c);
    return;
  } 
  if (type == FOFType::Or) {
    vector<Clause> c;
    Clause new_c;
    cs.push_back(new_c);
    for (size_t i = 0; i < sub_formulas.size(); i++) {
      sub_formulas[i].convert_to_clauses(c);
      for (size_t j = 0; j < c[0].size(); j++) {
        cs[0].add_lit((c[0])[j]);
      }
    }
    return;
  }
  if (type == FOFType::And) {
    vector<Clause> c;
    for (size_t i = 0; i < sub_formulas.size(); i++) {
      sub_formulas[i].convert_to_clauses(c);
      for (size_t j = 0; j < c.size();j++) {
        cs.push_back(c[j]);
      }
    }
  }
}

convert_to_cnf_clauses()

void FOF::convert_to_cnf_clauses	(	vector< Clause > &	cs,
		vector< string > &	_names,
		const string &	_role )

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. Also, this implementation does miniscoping.

Parameters

cs	vector of clauses containing the CNF.

Definition at line 817 of file FOF.cpp.

                                                                                                {
  if (type == FOFType::Empty) {
    cerr << "Don't do this with an Empty FOF!" << endl;
    return;
  }
#ifdef DEBUGOUTPUT
      cout << "Remove iff:" << endl;
#endif
  remove_iff();
#ifdef DEBUGOUTPUT
      cout << *this << endl;
      cout << "Remove imp" << endl;
#endif
  remove_imp();
#ifdef DEBUGOUTPUT
      cout << *this << endl;
      cout << "Push negs:" << endl;
#endif
  push_negs();
  recs_p->add_fof_inference_record("fof_nnf,[status(thm)]", 
                                   this->to_tptp_string());
 
#ifdef DEBUGOUTPUT
      cout << *this << endl;
      cout << "Make unique vars:" << endl;
#endif
  make_unique_bound_variables();
  recs_p->add_fof_inference_record("variable_rename,[status(thm)]",
                                   this->to_tptp_string());
#ifdef DEBUGOUTPUT
      cout << *this << endl;
      cout << "Remove redundant quantifiers:" << endl;
#endif
  remove_redundant_quantifiers();
#ifdef DEBUGOUTPUT
      cout << *this << endl;
      cout << "Miniscope:" << endl;
#endif
  if (params::miniscope) {
    miniscope();
  }
  recs_p->add_fof_inference_record("miniscope,[status(thm)]",
                                   this->to_tptp_string());
#ifdef DEBUGOUTPUT
      cout << *this << endl;
      cout << "Skolemize:" << endl;
#endif
  skolemize();
#ifdef DEBUGOUTPUT
      cout << *this << endl;
      cout << "Remove universal quantifiers:" << endl;
#endif
  remove_universal_quantifiers();
#ifdef DEBUGOUTPUT
      cout << *this << endl;
      cout << "Distribute or:" << endl;
#endif
  distribute_or();
#ifdef DEBUGOUTPUT
      cout << *this << endl;
      cout << "Convert to clauses:" << endl;
#endif
  convert_to_clauses(cs);
  for (const Clause& c : cs) {
    string role = _role;
    if (_role != string("negated_conjecture")) 
      role = "plain";
    string name = recs_p->add_clause_record(c, role);
    _names.push_back(name);
  }
#ifdef DEBUGOUTPUT
      cout << *this << endl;
#endif
}

convert_to_nnf()

void FOF::convert_to_nnf

(

)

Convert to Negation Normal Form.

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

Definition at line 638 of file FOF.cpp.

                         {
  if (type == FOFType::Empty) {
    cerr << "Don't do this with an Empty FOF!" << endl;
    return;
  }
  remove_iff();
  remove_imp();
  push_negs();
}

definitional_convert_to_cnf_clauses()

void FOF::definitional_convert_to_cnf_clauses	(	vector< Clause > &	cs,
		vector< string > &	_names,
		const string &	_role )

Convert to Conjunctive Normal Form using a form of definitional conversion.

There are lots of ways of doing definitional conversion. However as the restricted backtracking paper describing leanCoP v2.1 gives experimental results demonstrating that a particular approach is preferred, this implements the method as described in that paper.

Parameters

cs	vector of clauses containing the CNF.

See also

find_definitional_tuple

Definition at line 984 of file FOF.cpp.

                                                                                                             {
   if (type == FOFType::Empty) {
    cerr << "Don't do this with an Empty FOF!" << endl;
    return;
  }
  /*
  * Note that the description in the restricted backtracking paper produces a 
  * DNF and starts with a Skolemized NNF of the original formula, *not* its 
  * negation. As the difference between this and the current representation, for 
  * connection calculus is just that all the literals get negated, this could 
  * be done more efficiently, but for now I'm going to just do a direct 
  * implementation of the procedure described in the paper. So: negate 
  * first, produce a DNF, then negate again.
  */ 
  simple_negate();
 
  recs_p->add_fof_inference_record("def_negate,[status(cth)]",
                                    this->to_tptp_string());
 
  remove_iff();
  remove_imp();
  push_negs();
 
  recs_p->add_fof_inference_record("fof_nnf,[status(thm)]", 
                                   this->to_tptp_string());
 
  make_unique_bound_variables();
 
  recs_p->add_fof_inference_record("variable_rename,[status(thm)]",
                                   this->to_tptp_string());
 
  remove_redundant_quantifiers();
  /*
  * As we're producing a DNF, we skolemize universals and then remove existentials.
  */
  skolemize_universals();
  remove_existential_quantifiers();
  /*
  * Now we do the definitional magic. 
  */
  FOF f(FOFType::Empty);
  vector<FOF> d;
  vector<FOF> d_preds;
  find_definitional_tuple(f, d, d_preds, false);
  /*
  * f is a DNF so we can invert it and flatten it to 
  * the required CNF. 
  */
  f.dnf_invert_and_convert_to_clauses(cs);
  /*
  * Each element of d now needs to be converted using 
  * a standard conversion, then inverted and transformed 
  * to CNF.
  */
  for (FOF& formula : d) {
    vector<Clause> new_cs;
    formula.distribute_and();
    formula.dnf_invert_and_convert_to_clauses(new_cs);
    for (const Clause& new_c : new_cs) {
      cs.push_back(new_c);
    }
  }
  /*  
  * TPTP has no dnf() way of doing things. D'Oh! So I need a way of 
  * making TPTP format output. Do the negation and make the clauses 
  * for cnf. Then use their conjunction to output the new symbols 
  * introduced but as CTP, which it is with respect to the herbrand step. 
  * Then the individual clauses are THM.
  */
  /*
  * First make a cnf formula but in an fof format with quantifiers.
  */
  string tptp_fof_string("( ");
  int remaining = cs.size();
  for (const Clause& c : cs) {
     tptp_fof_string += c.to_tptp_fof_string();
     if (--remaining > 0) {
      tptp_fof_string += " & ";
     }
  }
  tptp_fof_string += " )";
  /*
  * Now you can construct the necessary TPTP format proof output. This 
  * is where you also report any new symbols.
  */
  string role = _role;
  if (_role != string("negated_conjecture")) 
      role = "plain";
 
  string def_symbols;
  if (d_preds.size() > 0) {
    def_symbols += "[";
    commas::comma com(d_preds.size());
    for (const FOF& f : d_preds) {
      def_symbols += f.predicate_to_tptp_string();
      def_symbols += com();
    }
    def_symbols += "]";
  }
  recs_p->add_definitional_record(tptp_fof_string, def_symbols);
  /*
  * Now make what you actually need in cnf format.
  */ 
  for (const Clause& c : cs) {
    string name = recs_p->add_clause_record(c, role);
    _names.push_back(name);
  }
}

distribute_and()

void FOF::distribute_and

(

)

Distribute ANDs to the maximum extent possible.

Assumes you have nothing but a quantifier-free DNF in NNF. The result will have a tree structure with ORs at the top, then ANDs, then literals.

Definition at line 1263 of file FOF.cpp.

                         {
  while (distribute_and_once()) {};
}

distribute_and_once()

bool FOF::distribute_and_once ( )

private

Find an AND that can be distributed and deal with it. Indicate if there isn't one.

Definition at line 150 of file FOF.cpp.

                              {
  // For literals there is nothing to do.
  if (is_literal()) {
    return false;
  }
  // If we're at an OR, or an AND with no OR immediately under it,
  // then we're just going to deal with the subformulas. 
  size_t or_location = find_or();
  size_t s = sub_formulas.size();
  if (type == FOFType::Or || 
      ((type == FOFType::And) && (or_location == s))) {
    bool result = false;
    // OK, so it's not, strictly speaking, just "once" but 
    // we don't really mind do we?
    for (size_t i = 0; i < s; i++) {
      if (sub_formulas[i].distribute_and_once())
        result = true;
    }
    return result;
  }
  // It must be an AND with an OR immediately under it. That means 
  // we can distribute. First get the OR's subformulas and 
  // remove it.
  vector<FOF> or_fof_subs = sub_formulas[or_location].sub_formulas;
  if (or_location != (s-1)) {
    sub_formulas[or_location] = sub_formulas[s-1];
  }
  sub_formulas.pop_back();
  // Now you've saved the sub-formulas for the OR, and 
  // removed it. The last remaining child of the AND is 
  // now going to be combined using AND with all 
  // the saved subformulas.
  FOF f = sub_formulas[s-2];
  size_t s2 = or_fof_subs.size();
  vector<FOF> new_sub_formulas_2;
  for (int i = 0; i < s2; i++) {
    vector<FOF> new_sub_formulas;
    new_sub_formulas.push_back(f);
    new_sub_formulas.push_back(or_fof_subs[i]);
    new_sub_formulas_2.push_back(FOF::make_and(new_sub_formulas));
  }
  // You may have started with an AND with only two children. If so 
  // then you can now move the OR upwards.
  if (s == 2) {
    type = FOFType::Or;
    sub_formulas = new_sub_formulas_2;
  }
  else {
    sub_formulas[s-2] = FOF::make_or(new_sub_formulas_2);
  }
  return true;
}

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.

Definition at line 1259 of file FOF.cpp.

                        {
  while (distribute_or_once()) {};
}

distribute_or_once()

bool FOF::distribute_or_once ( )

private

Find an OR that can be distributed and deal with it. Indicate if there isn't one.

Definition at line 97 of file FOF.cpp.

                             {
  // For literals there is nothing to do.
  if (is_literal()) {
    return false;
  }
  // If we're at an AND, or an OR with no AND immediately under it,
  // then we're just going to deal with the subformulas. 
  size_t and_location = find_and();
  size_t s = sub_formulas.size();
  if (type == FOFType::And || 
      ((type == FOFType::Or) && (and_location == s))) {
    bool result = false;
    // OK, so it's not, strictly speaking, just "once" but 
    // we don't really mind do we?
    for (size_t i = 0; i < s; i++) {
      if (sub_formulas[i].distribute_or_once())
        result = true;
    }
    return result;
  }
  // It must be an OR with an AND immediately under it. That means 
  // we can distribute. First get the AND's subformulas and 
  // remove it.
  vector<FOF> and_fof_subs = sub_formulas[and_location].sub_formulas;
  if (and_location != (s-1)) {
    sub_formulas[and_location] = sub_formulas[s-1];
  }
  sub_formulas.pop_back();
  // Now you've saved the sub-formulas for the AND, and 
  // removed it. The last remaining child of the OR is 
  // now going to be combined using OR with all 
  // the saved subformulas.
  FOF f = sub_formulas[s-2];
  size_t s2 = and_fof_subs.size();
  vector<FOF> new_sub_formulas_2;
  for (int i = 0; i < s2; i++) {
    vector<FOF> new_sub_formulas;
    new_sub_formulas.push_back(f);
    new_sub_formulas.push_back(and_fof_subs[i]);
    new_sub_formulas_2.push_back(FOF::make_or(new_sub_formulas));
  }
  // You may have started with an OR with only two children. If so 
  // then you can now move the AND upwards.
  if (s == 2) {
    type = FOFType::And;
    sub_formulas = new_sub_formulas_2;
  }
  else {
    sub_formulas[s-2] = FOF::make_and(new_sub_formulas_2);
  }
  return true;
}

dnf_invert_and_convert_to_clauses()

void FOF::dnf_invert_and_convert_to_clauses

(

vector< Clause > &

cs

)

const

Assuming you have a DNF, invert it and convert it to a collection of CNF clauses.

Definition at line 1202 of file FOF.cpp.

                                                                    {
  cs.clear();
  if (is_literal()) {
    Literal new_lit;
    to_Literal(new_lit);
    // This is where the inversion happens.
    new_lit.invert();
    Clause new_c;
    new_c.add_lit(new_lit);
    cs.push_back(new_c);
    return;
  } 
  // Anything under here is essentially ANDed literals.
  if (type == FOFType::And) {
    vector<Clause> c;
    Clause new_c;
    cs.push_back(new_c);
    for (size_t i = 0; i < sub_formulas.size(); i++) {
      sub_formulas[i].dnf_invert_and_convert_to_clauses(c);
      for (size_t j = 0; j < c[0].size(); j++) {
        cs[0].add_lit((c[0])[j]);
      }
    }
    return;
  }
  // Anything below here essentially converts to another DNF.
  if (type == FOFType::Or) {
    vector<Clause> c;
    for (size_t i = 0; i < sub_formulas.size(); i++) {
      sub_formulas[i].dnf_invert_and_convert_to_clauses(c);
      for (size_t j = 0; j < c.size();j++) {
        cs.push_back(c[j]);
      }
    }
  }
}

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.

Definition at line 1239 of file FOF.cpp.

                           {
  size_t s = sub_formulas.size();
  for (size_t i = 0; i < s; i++) {
    if (sub_formulas[i].type == FOFType::And) {
      return i;
    }
  }
  return s;
}

find_definitional_tuple()

void FOF::find_definitional_tuple	(	FOF &	f,
		vector< FOF > &	d,
		vector< FOF > &	d_preds,
		bool	in_conjunction )

Heavy-lifting for conversion to definitional clause form.

Parameters

f	First part of definitional tuple.
d	Second part of definitional tuple.
d_preds	Collects any new predicates introduced.
in_conjunctionm	Indicates whether or not the parent formula was a conjunction.

Definition at line 916 of file FOF.cpp.

                                                                                                   {
  f.clear();
  d.clear();
  // Literals are straightforward.
  if (is_literal()) {
    f = *this;
    vector<FOF> new_d;
    d = new_d;
    return;
  }
  // You must have an And or an Or because we're in NNF.
  // Let's split half and half, just for the sake of symmetry.
  vector<FOF> left;
  vector<FOF> right;
  split_sub_formulas(left, right);
  FOF l = left[0];
  FOF r = right[0];
  if (left.size() > 1) {
    l = FOF(type, left, nullptr);
  }
  if (right.size() > 1) {
    r = FOF(type, right, nullptr);
  }
  // Somewhere to store results.
  FOF new_f_1(FOFType::Empty);
  FOF new_f_2(FOFType::Empty);
  vector<FOF> new_d_1;
  vector<FOF> new_d_2;
  // The tricky case is an Or inside an And.
  if (in_conjunction && type == FOFType::Or) {
    l.find_definitional_tuple(new_f_1, new_d_1, d_preds, false);
    r.find_definitional_tuple(new_f_2, new_d_2, d_preds, false);
    FOF def = make_definitional_predicate();
    f = def;
    d_preds.push_back(def);
 
    def.simple_negate();
    vector<FOF> args1;
    args1.push_back(def);
    args1.push_back(new_f_1);
    d.push_back(FOF::make_and(args1));
    vector<FOF> args2;
    args2.push_back(def);
    args2.push_back(new_f_2);
    d.push_back(FOF::make_and(args2));
    for (const FOF& g : new_d_1) {
      d.push_back(g);
    }
    for (const FOF& g : new_d_2) {
      d.push_back(g);
    }
    return;
  }
  // The final case is straightforward.
  bool is_and(type == FOFType::And);
  l.find_definitional_tuple(new_f_1, new_d_1, d_preds, is_and);
  r.find_definitional_tuple(new_f_2, new_d_2, d_preds, is_and);
  vector<FOF> new_args;
  new_args.push_back(new_f_1);
  new_args.push_back(new_f_2);
  FOF new_f(type, new_args, nullptr);
  f = new_f;
  d = new_d_1;
  for (const FOF& g : new_d_2){
    d.push_back(g);
  }
}

find_free_variables()

set< Term * > FOF::find_free_variables

(

)

const

Find the free variables in the formula.

Note: will consider x to be free in:

( P(x) | Ax. Q(x) ).

Definition at line 1511 of file FOF.cpp.

                                          {
  set<Term*> result;
  set<Term*> free; 
  Term* to_remove; 
  switch (type) {
    case FOFType::Empty:
      cerr << "You shouldn't be doing this with an FOFType::Empty!" << endl;
      break;
    case FOFType::Atom:
      for (const Term* p : pred.get_args()) {
        free = p->all_variables();
        result.insert(free.begin(), free.end());
      }
      break;
    case FOFType::Neg:
    case FOFType::And: 
    case FOFType::Or: 
    case FOFType::Imp:
    case FOFType::Iff: 
      for (const FOF& f : sub_formulas) {
        free = f.find_free_variables();
        result.insert(free.begin(), free.end());
      }
      break;
    case FOFType::A: 
    case FOFType::E:
      result = sub_formulas[0].find_free_variables();
      to_remove = term_index->add_variable_term(var);
      result.erase(to_remove);
      break;
    default:
      break;
  }
  return result;
}

find_or()

size_t FOF::find_or

(

)

const

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

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

Definition at line 1249 of file FOF.cpp.

                          {
  size_t s = sub_formulas.size();
  for (size_t i = 0; i < s; i++) {
    if (sub_formulas[i].type == FOFType::Or) {
      return i;
    }
  }
  return s;
}

fof_type()

FOFType FOF::fof_type ( )

inline

Basic get method.

Definition at line 268 of file FOF.hpp.

{ return type; }

has_free_variable()

bool FOF::has_free_variable ( Variable * v )

private

Does this formula contain the specified variable unbound?

Only use this if bound variables are unique. (If it finds any quantifier binding the variable it will return false.)

Parameters

v	Pointer to Variable of interest.

Definition at line 36 of file FOF.cpp.

                                       {
  switch (type) {
    case FOFType::Empty:
      cerr << "Don't do this with an Empty FOF!" << endl;
      return false;
      break;
    case FOFType::Atom:
      return pred.contains_variable(v);
    case FOFType::Neg:
      return (sub_formulas[0].has_free_variable(v));
      break;
    case FOFType::And:
    case FOFType::Or:
      for (size_t i = 0; i < sub_formulas.size(); i++) {
        if (sub_formulas[i].has_free_variable(v)) {
          return true;
        }
      }
      return false;
      break;
    case FOFType::Imp:
    case FOFType::Iff:
      return (sub_formulas[0].has_free_variable(v) ||
              sub_formulas[1].has_free_variable(v));
      break;
    case FOFType::A:
    case FOFType::E:
      if (var == v) 
        return false;
      return sub_formulas[0].has_free_variable(v);
      break;
    default:
      break;
  }
  return false;
}

invert_literal()

void FOF::invert_literal

(

)

Self-explanatory!

Definition at line 462 of file FOF.cpp.

                         {
  if (type == FOFType::Atom) {
    simple_negate();
    return;
  } 
  if (type == FOFType::Neg && sub_formulas[0].type == FOFType::Atom) {
    remove_negation();
    return;
  }
  cerr << "Don't use this with a non-literal." << endl;
}

is_clause()

bool FOF::is_clause

(

)

const

Check if something is a clause.

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

Returns false if FOFType::Empty.

Definition at line 407 of file FOF.cpp.

                          {
  if (is_literal()) {
    return true;
  }
  if (!(type == FOFType::Or)) {
    return false;
  }
  for (size_t i = 0; i < sub_formulas.size(); i++) {
    if (!sub_formulas[i].is_literal()) {
      return false;
    }
  } 
  return true;
}

is_literal()

bool FOF::is_literal

(

)

const

Check if an FOF is a literal.

Works in general, not just for NNF.

Definition at line 402 of file FOF.cpp.

                           {
  return (type == FOFType::Atom) || 
    (type == FOFType::Neg && sub_formulas[0].type == FOFType::Atom);
}

make_and()

static FOF FOF::make_and ( const vector< FOF > & fs )

inlinestatic

Directly make a conjunction.

Definition at line 306 of file FOF.hpp.

                                             {
    FOF result(FOFType::And, fs, nullptr);
    return result;
  }

make_definitional_predicate()

FOF FOF::make_definitional_predicate ( ) const

private

When doing definitional clause conversion you need to be able to make unique new predicates. This will provide one.

Definition at line 87 of file FOF.cpp.

                                           {
  set<Term*> a = this->find_free_variables();
  vector<Term*> args;
  for (Term* p : a)
    args.push_back(p);
  Predicate* name = pred_index->make_definitional_predicate(args.size());
  Literal lit(name, args, args.size(), true);
  return FOF(lit);
}

make_exists()

static FOF FOF::make_exists ( const FOF & f, Variable * v )

inlinestatic

Directly make an existentially quantified FOF.

Definition at line 349 of file FOF.hpp.

                                                    {
    vector<FOF> fs;
    fs.push_back(f);
    FOF result(FOFType::E, fs, v);
    return result;
  }

make_forall()

static FOF FOF::make_forall ( const FOF & f, Variable * v )

inlinestatic

Directly make a universally quantified FOF.

Definition at line 340 of file FOF.hpp.

                                                    {
    vector<FOF> fs;
    fs.push_back(f);
    FOF result(FOFType::A, fs, v);
    return result;
  }

make_iff()

static FOF FOF::make_iff ( const FOF & lhs, const FOF & rhs )

inlinestatic

Directly make an iff.

Definition at line 330 of file FOF.hpp.

                                                      {
    vector<FOF> fs;
    fs.push_back(lhs);
    fs.push_back(rhs);
    FOF result(FOFType::Iff, fs, nullptr);
    return result;
  }

make_imp()

static FOF FOF::make_imp ( const FOF & lhs, const FOF & rhs )

inlinestatic

Directly make an implication.

Definition at line 320 of file FOF.hpp.

                                                      {
    vector<FOF> fs;
    fs.push_back(lhs);
    fs.push_back(rhs);
    FOF result(FOFType::Imp, fs, nullptr);
    return result;
  }

make_literal()

static FOF FOF::make_literal ( const Literal & lit )

inlinestatic

Directly make a Literal.

Definition at line 288 of file FOF.hpp.

                                              {
    FOF result(lit);
    return result;
  }

make_neg()

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

inlinestatic

Directly negate a FOF.

Careful: no attempt here to make any obvious simplifications.

Definition at line 297 of file FOF.hpp.

                                    {
    vector<FOF> fs;
    fs.push_back(f);
    FOF result(FOFType::Neg, fs, nullptr);
    return result;
  }

make_or()

static FOF FOF::make_or ( const vector< FOF > & fs )

inlinestatic

Directly make a disjunction.

Definition at line 313 of file FOF.hpp.

                                            {
    FOF result(FOFType::Or, fs, nullptr);
    return result;
  }

make_skolem_function()

Term * FOF::make_skolem_function ( const vector< Term * > & args )

private

Make a new Skolem function.

Mainly achieved using methods from other classes.

Parameters

args	Vector of pointers to Term. These are the Skolem function arguments.

Definition at line 205 of file FOF.cpp.

                                                         {
  Function* sk = fun_index->make_skolem_function(args.size());
  Term* sk_t = term_index->add_function_term(sk, args);
  return sk_t;
}

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.

Definition at line 519 of file FOF.cpp.

                                      {
  Variable* new_var;
  switch (type) {
    case FOFType::Atom:
      break;
    case FOFType::Neg:
    case FOFType::And:
    case FOFType::Or:
    case FOFType::Imp:
    case FOFType::Iff:
      for (FOF& sf : sub_formulas)
        sf.make_unique_bound_variables();
      break;
    case FOFType::A:
    case FOFType::E:
      sub_formulas[0].make_unique_bound_variables();
      new_var = var_index->add_unique_var();
      sub_formulas[0].replace_variable(new_var, var);
      var = new_var;
      break;
    default:
      break;
    }
}

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.

Definition at line 648 of file FOF.cpp.

                    {
  vector<FOF> free;
  vector<FOF> absent;
  FOF new_sub(FOFType::Empty);
  vector<FOF> new_subs;
  Variable* new_var;
  switch (type) {
    case FOFType::Empty:
      cerr << "Don't do this with an empty formula" << endl;
      break;
    case FOFType::Atom:
    case FOFType::Neg:
      break;
    case FOFType::And:
    case FOFType::Or:
      miniscope_all();
      break;
    case FOFType::Imp:
    case FOFType::Iff:
      cerr << "Don't do this unless you've removed -> and <->" << endl;
      break;
    // Remember you're only dealing with stuff in NNF. You 
    // do however have to handle nested quantifiers.
    case FOFType::A:
      sub_formulas[0].miniscope();
      if (!(sub_formulas[0].type == FOFType::And ||
          sub_formulas[0].type == FOFType::Or)) {
        return;
      }
      // You have \forall followed by (miniscoped) AND or OR.
      miniscope_split(var, free, absent);
      // If the quantifier is followed by AND you can just 
      // make a \forall for every subformula involving the 
      // variable.
      if (sub_formulas[0].type == FOFType::And) {
        type = FOFType::And;
        // If everything is bound then make a new forall everywhere
        // with a new variable.
        if (free.size() == sub_formulas[0].sub_formulas.size()) {
          for (size_t i = 0; i < free.size(); i++) {
            new_var = var_index->add_unique_var();
            new_sub = free[i];
            new_sub.replace_variable(new_var, var);
            new_sub = FOF::make_forall(new_sub, new_var);
            new_subs.push_back(new_sub);
          }
          sub_formulas = new_subs;
        }
        // If any subformula doesn't have the variable then just
        // move the forall in. Remember you need to consider the 
        // possibility that the quantifier can just be removed.
        else if (free.size() > 0) {
          sub_formulas = absent;
          if (free.size() == 1)
            new_sub = free[0];
          else
            new_sub = FOF::make_and(free);
          new_sub = FOF::make_forall(new_sub, var);
          sub_formulas.push_back(new_sub);
        }
        // You're just going to remove the quantifier.
        else {
          sub_formulas = sub_formulas[0].sub_formulas;
        }
        var = nullptr;
        miniscope_all();
        return;
      }
      if (sub_formulas[0].type == FOFType::Or) {
        // You have a \forall followed by an OR.
        // If eveything is bound there's nothing to do.
        if (absent.size() == 0)
          return;
        else if (free.size() > 0) {
          type = FOFType::Or;
          sub_formulas = absent;
          if (free.size() == 1)
            new_sub = free[0];
          else
            new_sub = FOF::make_or(free);
          new_sub = FOF::make_forall(new_sub, var);
          sub_formulas.push_back(new_sub);
          var = nullptr;
          miniscope_all();
        }
        // You can just drop the quantifier.
        else {
          type = FOFType::Or;
          vector<FOF> sf(sub_formulas);
          sub_formulas = sf[0].sub_formulas;
          var = nullptr;
        }
        return;
      }
      break;
    // You have an \exists.
    case FOFType::E:
      sub_formulas[0].miniscope();
      if (!(sub_formulas[0].type == FOFType::And ||
          sub_formulas[0].type == FOFType::Or)) {
        return;
      }
      // You have an \exists followed by AND or OR.
      miniscope_split(var, free, absent);
      if (sub_formulas[0].type == FOFType::Or) {
        type = FOFType::Or;
        // If everything is bound then make a new exists everywhere
        // with a new variable.
        if (free.size() == sub_formulas[0].sub_formulas.size()) {
          for (size_t i = 0; i < free.size(); i++) {
            new_var = var_index->add_unique_var();
            new_sub = free[i];
            new_sub.replace_variable(new_var, var);
            new_sub = FOF::make_exists(new_sub, new_var);
            new_subs.push_back(new_sub);
          }
          sub_formulas = new_subs;
        }
        // If any subformula doesn't have the variable then just
        // move the \exists in.
        else if (free.size() > 0) {
          sub_formulas = absent;
          if (free.size() == 1)
            new_sub = free[0];
          else
            new_sub = FOF::make_or(free);
          new_sub = FOF::make_exists(new_sub, var);
          sub_formulas.push_back(new_sub);
        }
        // We're just going to drop the quantifier.
        else {
          sub_formulas = sub_formulas[0].sub_formulas;
        }
        var = nullptr;
        miniscope_all();
        return;
      }
      // You have an \exists followed by and AND.
      if (sub_formulas[0].type == FOFType::And) {
        // If eveything is bound there's nothing to do.
        if (absent.size() == 0)
          return;
        else if (free.size() != sub_formulas[0].sub_formulas.size()) {
          type = FOFType::And;
          sub_formulas = absent;
           if (free.size() == 1)
            new_sub = free[0];
          else
            new_sub = FOF::make_and(free);
          new_sub = FOF::make_exists(new_sub, var);
          sub_formulas.push_back(new_sub);
          var = nullptr;
          miniscope_all();
        }
        // We can just drop the quantifier.
        else {
          type = FOFType::And;
          vector<FOF> sf(sub_formulas);
          sub_formulas = sf[0].sub_formulas;
          var = nullptr;
        }
        return;
      }
      break;
    default:
      break;
    }
}

miniscope_all()

void FOF::miniscope_all ( )

private

Apply miniscoping to all subformulas.

Definition at line 339 of file FOF.cpp.

                        {
  for (size_t i = 0; i < sub_formulas.size(); i++ ) {
    sub_formulas[i].miniscope();
  }
}

miniscope_split()

void FOF::miniscope_split ( Variable * v, vector< FOF > & free, vector< FOF > & absent )

private

Helper for miniscope.

Split subformulas into ones that do and don't have the relevant variable.

Parameters

v	Pointer to Variable of interest.
free	Reference to vector of FOF. Collect FOFs with the Variable.
absent	Reference to vector of FOF. Collect FOFs without the Variable.

Definition at line 323 of file FOF.cpp.

                                               {
  // Remember that at this point you have a NNF with 
  // unique variables. So whatever is in the subformula 
  // is AND, OR, Atom or Neg (Literal).
  vector<FOF>& subs = sub_formulas[0].sub_formulas;
  for (size_t i = 0; i < subs.size(); i++) {
    FOF f(subs[i]);
    if (f.has_free_variable(v))
      free.push_back(f);
    else
      absent.push_back(f);
  }
}

negate()

void FOF::negate

(

)

Negate an FOF, applying obvious simplifications if it's already negated or an implication.

Definition at line 431 of file FOF.cpp.

                 {
  if (type == FOFType::Empty) {
    cerr << "Don't do this with an Empty FOF!" << endl;
    return;
  }
  if (type == FOFType::Imp) {
    type = FOFType::And;
    sub_formulas[1].negate();
  }
  else if (type == FOFType::Neg) {
    remove_negation();
  }
  else {
    FOF f = *this;
    type = FOFType::Neg;
    pred.clear();
    var = nullptr;
    sub_formulas.clear();
    sub_formulas.push_back(f);
  }
}

predicate_to_tptp_string()

string FOF::predicate_to_tptp_string

(

)

const

Assuming this is an Atom, return the predicate name as a string.

Definition at line 1438 of file FOF.cpp.

                                           {
  if (type != FOFType::Atom) {
    cerr << "You should only be doing this with an atom!" << endl;
    return string();
  }
  return pred.get_pred()->to_tptp_string();
 
}

push_negs()

void FOF::push_negs

(

)

Push all negations in.

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

Definition at line 573 of file FOF.cpp.

                    {
  switch (type) {
    case FOFType::Neg:
      switch (sub_formulas[0].type) {
          case FOFType::Neg:
            remove_negation();
            remove_negation();
            push_negs();
            break;
          case FOFType::Atom:
            break;
          case FOFType::And:
            remove_negation();
            type = FOFType::Or;
            for (FOF& f : sub_formulas) {
              f.negate();
              f.push_negs();
            }
            break;
          case FOFType::Or:
            remove_negation();
            type = FOFType::And;
            for (FOF& f : sub_formulas) {
              f.negate();
              f.push_negs();
            }
            break;
          case FOFType::A:
            remove_negation();
            type = FOFType::E;
            sub_formulas[0].negate();
            sub_formulas[0].push_negs();
            break;
          case FOFType::E:
            remove_negation();
            type = FOFType::A;
            sub_formulas[0].negate();
            sub_formulas[0].push_negs();
            break;
          case FOFType::Imp:
          case FOFType::Iff:
            cerr << "Stop it!!! You don't push negations through -> or <->." << endl;
            break;
          default:
            break;
      }
      break;
    case FOFType::Atom:
      break;
    case FOFType::And:
    case FOFType::Or:
    case FOFType::A:
    case FOFType::E:
      for (FOF& f : sub_formulas)
        f.push_negs();
      break;
    case FOFType::Imp:
    case FOFType::Iff:
      cerr << "Stop it!!! You don't push negations through -> or <->." << endl;
      break;
    default:
      break;
  }
}

remove_existential_quantifiers()

void FOF::remove_existential_quantifiers

(

)

Self-explanatory.

Definition at line 1131 of file FOF.cpp.

                                         {
  FOF f(FOFType::Atom);
  switch (type) {
    case FOFType::Atom:
      break;
    case FOFType::Neg:
      sub_formulas[0].remove_existential_quantifiers();
      break;
    case FOFType::And:
    case FOFType::Or:
    case FOFType::Imp:
    case FOFType::Iff:
      for (FOF& g : sub_formulas)
        g.remove_existential_quantifiers();
      break;
    case FOFType::E:
      sub_formulas[0].remove_existential_quantifiers();
      f = sub_formulas[0];
      *this = f;
      break;
    case FOFType::A:
      sub_formulas[0].remove_existential_quantifiers();
      break;
    default:
      break;
    }
}

remove_iff()

void FOF::remove_iff

(

)

Replace <-> throughout using ->.

Definition at line 474 of file FOF.cpp.

                     {
  if (type == FOFType::Empty) {
    cerr << "Don't do this with an Empty FOF!" << endl;
    return;
  }
  // End of recursion.
  if (type == FOFType::Atom)
    return;
  // Do the relevant transformation.
  if (type == FOFType::Iff) {
    FOF lhs = *this;
    FOF rhs = *this;
    lhs.type = FOFType::Imp;
    rhs.type = FOFType::Imp;
    FOF store = rhs.sub_formulas[1];
    rhs.sub_formulas[1] = rhs.sub_formulas[0];
    rhs.sub_formulas[0] = store;
    type = FOFType::And;
    sub_formulas.clear();
    sub_formulas.push_back(lhs);
    sub_formulas.push_back(rhs);
  }
  // Finish the job. Also applies the transformation to other FOF types.
  for (FOF& f : sub_formulas)
    f.remove_iff();
}

remove_imp()

void FOF::remove_imp

(

)

Replace A->B throughout with neg A v B.

Definition at line 501 of file FOF.cpp.

                     {
  if (type == FOFType::Empty) {
    cerr << "Don't do this with an Empty FOF!" << endl;
    return;
  }
  // End of recursion.
  if (type == FOFType::Atom)
    return;
  // Do the relevant transformation.
  if (type == FOFType::Imp) {
    type = FOFType::Or;
    sub_formulas[0].negate();
  }
  // Finish the job. Also applies the transformation to other FOF types.
  for (FOF& f : sub_formulas)
    f.remove_imp();
}

remove_negation()

void FOF::remove_negation

(

)

Remove the leading negation from an arbitrary FOF, if it has one.

Definition at line 424 of file FOF.cpp.

                          {
  if (type == FOFType::Neg) {
    FOF f = sub_formulas[0];
    *this = f;
  }
}

remove_redundant_quantifiers()

void FOF::remove_redundant_quantifiers

(

)

Remove quantifiers if they don't bind anything in their scope.

Yes, the TPTP does contain such formulas. Use this only if bound variables are unique.

Definition at line 544 of file FOF.cpp.

                                       {
  Variable* new_var;
  switch (type) {
    case FOFType::Atom:
      break;
    case FOFType::Neg:
    case FOFType::And:
    case FOFType::Or:
    case FOFType::Imp:
    case FOFType::Iff:
      for (FOF& sf : sub_formulas)
        sf.remove_redundant_quantifiers();
      break;
    case FOFType::A:
    case FOFType::E:
      sub_formulas[0].remove_redundant_quantifiers();
      if (!sub_formulas[0].has_free_variable(var)) {
        vector<FOF> sf(sub_formulas);
        type = sub_formulas[0].type;
        pred = sub_formulas[0].pred;
        var = sub_formulas[0].var;
        sub_formulas = sf[0].sub_formulas;
      }
      break;
    default:
      break;
    }
}

remove_universal_quantifiers()

void FOF::remove_universal_quantifiers

(

)

Self-explanatory.

Definition at line 1103 of file FOF.cpp.

                                       {
  FOF f(FOFType::Atom);
  switch (type) {
    case FOFType::Atom:
      break;
    case FOFType::Neg:
      sub_formulas[0].remove_universal_quantifiers();
      break;
    case FOFType::And:
    case FOFType::Or:
    case FOFType::Imp:
    case FOFType::Iff:
      for (FOF& g : sub_formulas)
        g.remove_universal_quantifiers();
      break;
    case FOFType::A:
      sub_formulas[0].remove_universal_quantifiers();
      f = sub_formulas[0];
      *this = f;
      break;
    case FOFType::E:
      sub_formulas[0].remove_universal_quantifiers();
      break;
    default:
      break;
    }
}

replace_variable()

void FOF::replace_variable ( Variable * new_var, Variable * old_var )

private

Self-explanatory.

However note that this works only on Atoms: quantifiers will be unaffected.

Parameters

new_var	Pointer to new Variable.
old_var	Pointer to Variable to replace.

Definition at line 73 of file FOF.cpp.

                                                               {
  if (type == FOFType::Empty) {
    cerr << "Don't do this with an Empty FOF!" << endl;
    return;
  }
  if (type == FOFType::Atom) {
    pred.replace_variable(new_var, old_var, term_index);
  }
  else {
    for (FOF& f : sub_formulas)
      f.replace_variable(new_var, old_var);
  }
}

replace_variable_with_term()

void FOF::replace_variable_with_term ( Term * new_term, Variable * old_var )

private

Replace a Variable with a Term.

Mainly achieved using methods from other classes.

Note that this works only on Atoms: quantifiers will be unaffected.

Parameters

new_term	Pointer to new Term to use.
old_var	Pointer to Variable to replace.

Definition at line 211 of file FOF.cpp.

                                                                      {
  if (type == FOFType::Empty) {
    cerr << "Don't do this with an Empty FOF!" << endl;
    return;
  }
  if (type == FOFType::Atom) {
    pred.replace_variable_with_term(new_term, old_var, term_index);
  }
  else {
    for (FOF& f : sub_formulas)
      f.replace_variable_with_term(new_term, old_var);
  }
}

set_indexes()

static void FOF::set_indexes ( std::tuple< VariableIndex *, FunctionIndex *, PredicateIndex *, TermIndex * > is )

inlinestatic

Set up pointer to the variable index etc.

Definition at line 241 of file FOF.hpp.

                                          {
    var_index = std::get<0>(is);
    fun_index = std::get<1>(is);
    pred_index = std::get<2>(is);
    term_index = std::get<3>(is);
  }

set_recs_p()

static void FOF::set_recs_p ( TPTPRecords * _p )

inlinestatic

Set up the pointer allowing TPTP outputs to be added.

Definition at line 253 of file FOF.hpp.

                                          {
    recs_p = _p;
  }

show_indexes()

void FOF::show_indexes ( ) const

inline

Show the indices.

Definition at line 259 of file FOF.hpp.

                            {
    cout << var_index << " " << fun_index 
                      << " " << pred_index 
                      << " " << term_index 
                      << endl;
  }

simple_negate()

void FOF::simple_negate

(

)

Negate an FOF without applying any simplifications.

Definition at line 453 of file FOF.cpp.

                        {
  FOF f = *this;
  type = FOFType::Neg;
  pred.clear();
  var = nullptr;
  sub_formulas.clear();
  sub_formulas.push_back(f);
}

simplify_cnf() [1/2]

SimplificationResult FOF::simplify_cnf ( vector< Clause > & cnf )

static

Simplify the clauses in a CNF using the method in Clause.

Definition at line 1490 of file FOF.cpp.

                                                          {
  vector<Clause> new_cnf;
  bool cnf_is_contradiction = false;
  for (Clause& c : cnf) {
    SimplificationResult result = c.simplify();
    if (result == SimplificationResult::Tautology)
      continue;
    if (result == SimplificationResult::Contradiction) {
      cnf_is_contradiction = true;
      continue;
    } 
    new_cnf.push_back(c);
  }
  cnf = new_cnf;
  if (cnf_is_contradiction) 
    return SimplificationResult::Contradiction;
  if (cnf.size() == 0)
    return SimplificationResult::Tautology;
  return SimplificationResult::OK;
}

simplify_cnf() [2/2]

SimplificationResult FOF::simplify_cnf ( vector< Clause > & cnf, vector< string > & roles, vector< string > & names )

static

As first version of simplify_cnf, but keep track of corresponding roles as well.

Definition at line 1447 of file FOF.cpp.

                                                              {
  vector<Clause> new_cnf;
  vector<string> new_roles;
  vector<string> new_names;
  bool cnf_is_contradiction = false;
  size_t i = 0;
  for (Clause& c : cnf) {
    Clause c2 = c;
    SimplificationResult result = c.simplify();
    if (result == SimplificationResult::Tautology) {
      recs_p->add_tf_clause_record(names[i], roles[i], "$true");
      i++;
      continue;
    }
    if (result == SimplificationResult::Contradiction) {
      cnf_is_contradiction = true;
      recs_p->add_tf_clause_record(names[i], roles[i], "$false");
      i++;
      continue;
    } 
    new_cnf.push_back(c);
    new_roles.push_back(roles[i]);
    if (c == c2) {
      new_names.push_back(names[i]);
    }
    else {
      string new_name = recs_p->add_clause_record(c, roles[i], names[i]);
      new_names.push_back(new_name);
    }
    i++;
  }
  cnf = new_cnf;
  roles = new_roles;
  names = new_names;
  if (cnf_is_contradiction) 
    return SimplificationResult::Contradiction;
  if (cnf.size() == 0)
    return SimplificationResult::Tautology;
  return SimplificationResult::OK;
}

skolemize()

void FOF::skolemize

(

)

Skolemize the given formula.

All the hard work is done by skolemize_main.

See also

skolemize_main

Definition at line 1093 of file FOF.cpp.

                    {
  vector<Term*> skolem_arguments;
  skolemize_main(skolem_arguments, this, true);
}

skolemize_main()

void FOF::skolemize_main ( vector< Term * > skolem_arguments, FOF * whole_f, bool tptp = false )

private

Main helper function called by FOF::skolemize().

The parameter is used to collect variables for the universal quantifiers inside which you find an existential quantifier. Those then become the parameters for the Skolem function.

Parameters

skolem_arguments

Vector of pointers to Term.

See also

make_skolem_function.

replace_variable_with_term.

Definition at line 225 of file FOF.cpp.

                                    {
  Term* sk_t;
  FOF f(FOFType::Atom);
  string sk_s;
  string sk_t_s;
  string var_s;
  string f_s;
  switch (type) {
    case FOFType::Atom:
      break;
    case FOFType::Neg:
      sub_formulas[0].skolemize_main(skolem_arguments, whole_f, tptp);
      break;
    case FOFType::And:
    case FOFType::Or:
    case FOFType::Imp:
    case FOFType::Iff:
      for (FOF& g : sub_formulas)
        g.skolemize_main(skolem_arguments, whole_f, tptp);
      break;
    case FOFType::A:
      skolem_arguments.push_back(term_index->add_variable_term(var));
      sub_formulas[0].skolemize_main(skolem_arguments, whole_f, tptp);
      break;
    case FOFType::E:
      sk_t = make_skolem_function(skolem_arguments);
      if (tptp) {
        sk_s = sk_t->get_f()->get_name();
        sk_t_s = sk_t->to_prolog_string();
        var_s = var->to_prolog_string();
      }
      sub_formulas[0].replace_variable_with_term(sk_t, var);
      f = sub_formulas[0];
      *this = f;
      if (tptp) {
        FOF f2 = *whole_f;
        f_s = f2.to_tptp_string();
        recs_p->add_skolemization_record(f_s, var_s, sk_t_s, sk_s);
      }
      skolemize_main(skolem_arguments, whole_f, tptp);
      break;
    default:
      break;
    }
}

skolemize_universals()

void FOF::skolemize_universals

(

)

Skolemize the universal quantifiers in the given formula.

All the hard work is done by skolemize_universals_main.

See also

skolemize_universals_main

Definition at line 1098 of file FOF.cpp.

                               {
  vector<Term*> skolem_arguments;
  skolemize_universals_main(skolem_arguments, this, true);
}

skolemize_universals_main()

void FOF::skolemize_universals_main ( vector< Term * > skolem_arguments, FOF * whole_f, bool tptp = false )

private

The dual of skolemize_main.

See also

skolemize_main

Definition at line 273 of file FOF.cpp.

                                               {
  Term* sk_t;
  FOF f(FOFType::Atom);
  string sk_s;
  string sk_t_s;
  string var_s;
  string f_s;
  switch (type) {
    case FOFType::Atom:
      break;
    case FOFType::Neg:
      sub_formulas[0].skolemize_universals_main(skolem_arguments, whole_f, tptp);
      break;
    case FOFType::And:
    case FOFType::Or:
    case FOFType::Imp:
    case FOFType::Iff:
      for (FOF& g : sub_formulas)
        g.skolemize_universals_main(skolem_arguments, whole_f, tptp);
      break;
    case FOFType::E:
      skolem_arguments.push_back(term_index->add_variable_term(var));
      sub_formulas[0].skolemize_universals_main(skolem_arguments, whole_f, tptp);
      break;
    case FOFType::A:
      sk_t = make_skolem_function(skolem_arguments);
      if (tptp) {
        sk_s = sk_t->get_f()->get_name();
        sk_t_s = sk_t->to_prolog_string();
        var_s = var->to_prolog_string();
      }
      sub_formulas[0].replace_variable_with_term(sk_t, var);
      f = sub_formulas[0];
      *this = f;
      if (tptp) {
        FOF f2 = *whole_f;
        f_s = f2.to_tptp_string();
        recs_p->add_herbrandization_record(f_s, var_s, sk_t_s, sk_s);
      }
      skolemize_universals_main(skolem_arguments, whole_f, tptp);
      break;
    default:
      break;
    }
}

split_sub_formulas()

void FOF::split_sub_formulas	(	vector< FOF > &	left_sub,
		vector< FOF > &	right_sub )

Split subformulas in half.

Parameters

left_sub	First half of the subformulas.
right_sub	Second half of subformulas.

Definition at line 892 of file FOF.cpp.

                                                                          {
  left_sub.clear();
  right_sub.clear();
  size_t s = sub_formulas.size();
  if (s == 2) {
    left_sub.push_back(sub_formulas[0]);
    right_sub.push_back(sub_formulas[1]);
    return;
  }
  if (s == 3) {
    right_sub.push_back(sub_formulas[2]);
    left_sub = sub_formulas;
    left_sub.pop_back();
    return;
  }
  size_t left_size = s / 2;
  for (size_t i = 0; i < left_size; i++) {
    left_sub.push_back(sub_formulas[i]);
  }
  for (size_t i = left_size; i < s; i++) {
    right_sub.push_back(sub_formulas[i]);
  }
}

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.

Definition at line 1159 of file FOF.cpp.

                                           {
    if (type == FOFType::Atom) {
      new_lit = pred;
    }
    else {
      new_lit = sub_formulas[0].pred;
      new_lit.make_negative();
    }
}

to_string()

string FOF::to_string

(

)

const

Convert a FOF into a nice-looking string.

Definition at line 1267 of file FOF.cpp.

                            {
  string result;
  size_t s = sub_formulas.size();;
  size_t i = 1;
  switch (type) {
    case FOFType::Atom:
      result = pred.to_string();
      break;
    case FOFType::Neg:
      result = unicode_symbols::LogSym::neg;
      result += "( ";
      result += sub_formulas[0].to_string();
      result += " )";
      break;
    case FOFType::And:
      result = "( ";
      for (const FOF& g : sub_formulas) {
        result += g.to_string();
        if (i < s) {
         result += " ";
          result += unicode_symbols::LogSym::and_sym;
          result += " ";
        }
        i++;
      }
      result += " )";
      break;
    case FOFType::Or:
      result = "( ";
      for (const FOF& g : sub_formulas) {
        result += g.to_string();
        if (i < s) {
            result += " ";
            result += unicode_symbols::LogSym::or_sym;
            result += " ";
        }
        i++;
      }
      result += " )";
      break;
    case FOFType::Imp:
      result = "( ";
      result +=  sub_formulas[0].to_string();
      result += " ";
      result += unicode_symbols::LogSym::ifthen;
      result += " ";
      result += sub_formulas[1].to_string();
      result += " )";
      break;
    case FOFType::Iff:
      result = "( ";
      result += sub_formulas[0].to_string();
      result += " ";
      result += unicode_symbols::LogSym::iff;
      result += " ";
      result += sub_formulas[1].to_string();
      result += " )";
      break;
    case FOFType::A:
      result = unicode_symbols::LogSym::forall;
      result += var->to_string();
      result += " . [ ";
      result += sub_formulas[0].to_string();
      result += " ]";
      break;
    case FOFType::E:
      result = unicode_symbols::LogSym::exists;
      result += var->to_string();
      result += " . [ ";
      result += sub_formulas[0].to_string();
      result += " ]";
      break;
    default:
      break;
  }
  return result;
}

to_tptp_string()

string FOF::to_tptp_string

(

bool

nesting = false

)

const

Convert a FOF into a nice-looking string in the TPTP format.

Argument allows you to collect variables for nested quantifiers.

Definition at line 1345 of file FOF.cpp.

                                             {
  string result;
  size_t s = sub_formulas.size();;
  size_t i = 1;
  bool nested = false;
  switch (type) {
    case FOFType::Atom:
      result = pred.to_tptp_string();
      break;
    case FOFType::Neg:
      result = "~";
      result += "( ";
      result += sub_formulas[0].to_tptp_string();
      result += " )";
      break;
    case FOFType::And:
      result = "( ";
      for (const FOF& g : sub_formulas) {
        result += g.to_tptp_string();
        if (i < s) {
         result += " ";
          result += "&";
          result += " ";
        }
        i++;
      }
      result += " )";
      break;
    case FOFType::Or:
      result = "( ";
      for (const FOF& g : sub_formulas) {
        result += g.to_tptp_string();
        if (i < s) {
            result += " ";
            result += "|";
            result += " ";
        }
        i++;
      }
      result += " )";
      break;
    case FOFType::Imp:
      result = "( ";
      result +=  sub_formulas[0].to_tptp_string();
      result += " ";
      result += "=>";
      result += " ";
      result += sub_formulas[1].to_tptp_string();
      result += " )";
      break;
    case FOFType::Iff:
      result = "( ";
      result += sub_formulas[0].to_tptp_string();
      result += " ";
      result += "<=>";
      result += " ";
      result += sub_formulas[1].to_tptp_string();
      result += " )";
      break;
    case FOFType::A:
      if (nesting) {
        result += ",";
      }
      else {
        result = "! [ ";
      }
      result += var->to_prolog_string();
      nested = sub_formulas[0].type == FOFType::A;
      if (!nested) {
        result += " ] : ";
      } 
      result += sub_formulas[0].to_tptp_string(nested);
      break;
    case FOFType::E:
      if (nesting) {
        result += ",";
      }
      else {
        result = "? [ ";
      }
      result += var->to_prolog_string();
      nested = sub_formulas[0].type == FOFType::E;
      if (!nested) {
        result += " ] : ";
      } 
      result += sub_formulas[0].to_tptp_string(nested);
      break;
    default:
      break;
  }
  return result;
}

Friends And Related Symbol Documentation

operator<<

ostream & operator<< ( ostream & out, const FOF & f )

friend

Definition at line 1547 of file FOF.cpp.

                                                {
  out << f.to_string();
  return out;
}

Member Data Documentation

fun_index

FunctionIndex * FOF::fun_index = nullptr

staticprivate

Access to the index: static because all FOFs should share it.

Definition at line 90 of file FOF.hpp.

pred

Literal FOF::pred

private

FOFType::Atom can store one of these to represent a Literal.

Definition at line 72 of file FOF.hpp.

pred_index

PredicateIndex * FOF::pred_index = nullptr

staticprivate

Access to the index: static because all FOFs should share it.

Definition at line 100 of file FOF.hpp.

recs_p

TPTPRecords * FOF::recs_p = nullptr

staticprivate

Allow FOF to add TPTP outputs.

Definition at line 63 of file FOF.hpp.

sub_formulas

vector<FOF> FOF::sub_formulas

private

Most FOFs will have subformulas.

Definition at line 76 of file FOF.hpp.

term_index

TermIndex * FOF::term_index = nullptr

staticprivate

Access to the index: static because all FOFs should share it.

Definition at line 95 of file FOF.hpp.

type

FOFType FOF::type

private

Used for all FOFs to denote what kind it it.

Definition at line 67 of file FOF.hpp.

var

Variable* FOF::var

private

Associate a Variable with a quantifier.

Definition at line 80 of file FOF.hpp.

var_index

VariableIndex * FOF::var_index = nullptr

staticprivate

Access to the index: static because all FOFs should share it.

Definition at line 85 of file FOF.hpp.

---

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

• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/FOF.hpp
• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/FOF.cpp