Representation of the Matrix within a proof. More...

#include <Matrix.hpp>

Collaboration diagram for Matrix:

[legend]

Public Member Functions
	Matrix ()
	Use this constructor if you really want an empty Matrix.

	Matrix (size_t)
	Use this constructor when you know how many predicates there are.

	Matrix (const Matrix &)=delete
	You're never going to need to copy a Matrix.

	Matrix (const Matrix &&)=delete

Matrix &	operator= (const Matrix &)=delete

Matrix &	operator= (const Matrix &&)=delete

ClauseNum	get_num_clauses () const
	Straightforward get method.

const Clause &	operator[] (size_t i) const
	Straightforward get method.

bool	is_positive (size_t i) const
	Is a particular Clause positive?.

bool	is_negative (size_t i) const
	Is a particular Clause negative?.

bool	is_conjecture (size_t i) const
	Is a particular Clause a conjecture?

void	set_num_equals (uint32_t n)
	Straightforward set method.

pair< bool, size_t >	find_start () const
	Use a simple heuristic to find a good start clause.

void	set_num_preds (size_t)
	Make an empty index.

void	add_clause (Clause &, string="")
	Add a Clause to the Matrix and update the index accordingly.

void	find_limited_extensions (Unifier &, vector< InferenceItem > &, Clause &, VariableIndex &, TermIndex &)
	Find all possible extensions given a Clause, but only consider the first Literal in the Clause.

void	find_all_extensions (Unifier &, vector< InferenceItem > &, Clause &, VariableIndex &, TermIndex &)
	Find all possible extensions given a Clause, considering all Literals in the Clause.

void	deterministic_reorder (size_t)
	Deterministic reorder of the clauses.

void	random_reorder ()
	Randomly reorder the matrix.

void	move_equals_to_start ()
	Self-explanatory.

vector< Clause >::const_iterator	cbegin () const

vector< Clause >::const_iterator	cend () const

vector< Clause >::iterator	begin ()

vector< Clause >::iterator	end ()

string	to_string () const
	Make a string representation.

string	make_LaTeX (bool=false) const
	Make a usable LaTeX representation.

void	write_to_prolog_file (const path &) const
	Write to a file that can be read by Prolog.

void	show_tptp () const
	Output in TPTP compatible format.

Private Member Functions
void	find_extensions (Unifier &, vector< InferenceItem > &, const Literal &, LitNum, VariableIndex &, TermIndex &)
	Find all possible extensions, given a Literal.

void	make_clauses_copy ()
	Store a copy of the clauses.

Private Attributes
vector< Clause >	clauses
	The Matrix itself is just a set of Clauses.

vector< bool >	positive_clauses
	Keep track of which clauses are positive.

vector< bool >	negative_clauses
	Keep track of which clauses are negative.

vector< string >	clause_roles
	Keep track of which clauses are conjectures etc.

uint32_t	num_equals
	You need to know how many equality axioms there are in case you want to move them around.

vector< Clause >	clauses_copy
	It makes sense to keep a copy of the clauses if your schedule reorders multiple times.

vector< string >	roles_copy
	It makes sense to keep a copy of the roles if your schedule reorders multiple times.

bool	copy_saved
	Remember whether you've saved a copy.

vector< vector< MatrixPairType > >	index
	We want to be able to quickly identify where in each clause a particular literal lives.

Static Private Attributes
static std::mt19937	d
	Randomness for random reordering.

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

Detailed Description

Representation of the Matrix within a proof.

The Matrix itself never actually changes. However we do want to be able to look things up quickly when finding possible extension steps, so we build an index to help with that.

This class is also the natural place to implement the finding of all extensions, and the start clause heuristics.

Definition at line 72 of file Matrix.hpp.

Constructor & Destructor Documentation

◆ Matrix() [1/3]

Matrix::Matrix ( )

inline

Use this constructor if you really want an empty Matrix.

Definition at line 162 of file Matrix.hpp.

    : clauses()
    , index()
    , positive_clauses()
    , negative_clauses()
    , clause_roles()
    , clauses_copy()
    , roles_copy()
    , copy_saved(false)
    {}

◆ Matrix() [2/3]

Matrix::Matrix ( size_t num_predicates )

Use this constructor when you know how many predicates there are.

Parameters

num_predicates Number of predicates.

Definition at line 30 of file Matrix.cpp.

: clauses()
, index((num_predicates * 2), vector<MatrixPairType>())
, positive_clauses()
, negative_clauses()
, clause_roles()
, num_equals(0)
, clauses_copy()
, roles_copy()
, copy_saved(false)
{}

◆ Matrix() [3/3]

Matrix::Matrix ( const Matrix & )

delete

You're never going to need to copy a Matrix.

Let the compiler be your friend.

Member Function Documentation

◆ add_clause()

void Matrix::add_clause	(	Clause &	clause,
		string	role = `""`
	)

Add a Clause to the Matrix and update the index accordingly.

Optionally add a clause role.

Parameters

clause	Reference to the Clause.
role	A string denoting the role of the clause.

Definition at line 91 of file Matrix.cpp.

                                                   {
    ClauseNum clause_number = clauses.size();
    LitNum literal_number = 0;
    for (size_t j = 0; j < clause.size(); j++) {
        size_t i = clause[j].get_pred_as_index();
        index[i].push_back(MatrixPairType(clause_number, literal_number));
        literal_number++;
    }
    clauses.push_back(clause);
    positive_clauses.push_back(clause.is_positive());
    negative_clauses.push_back(clause.is_negative());
    clause_roles.push_back(role);
}

◆ begin()

vector< Clause >::iterator Matrix::begin ( )

inline

Definition at line 304 of file Matrix.hpp.

304{ return clauses.begin(); }

◆ cbegin()

vector< Clause >::const_iterator Matrix::cbegin ( ) const

inline

Definition at line 302 of file Matrix.hpp.

302{ return clauses.cbegin(); }

◆ cend()

vector< Clause >::const_iterator Matrix::cend ( ) const

inline

Definition at line 303 of file Matrix.hpp.

303{ return clauses.cend(); }

◆ deterministic_reorder()

void Matrix::deterministic_reorder ( size_t n )

Deterministic reorder of the clauses.

Call the reorder algorithm the specified number of times. This assumes you have stored a copy of the original clauses.

Parameters

n	Number of times to call the reorder algorithm

Only store a copy of the clauses the first time you do this.

Definition at line 105 of file Matrix.cpp.

                                           {
  if (!copy_saved) {
    copy_saved = true;
    make_clauses_copy();
  }
  /*
  * Find a suitably reordered set of indices.
  */
  vector<uint32_t> new_order;
  size_t s = clauses.size();
  for (size_t i = 0; i < s; i++)
    new_order.push_back(i);
  new_order = deterministic_reorder_n_times<uint32_t>(new_order, n);
  /*
  * Clear and rebuild as necessary.
  */
  clauses.clear();
  positive_clauses.clear();
  negative_clauses.clear();
  clause_roles.clear();
  size_t s2 = index.size();
  index.clear();
  index = vector<vector<MatrixPairType> >(s2, vector<MatrixPairType>());
  for (size_t i = 0; i < s; i++) {
    add_clause(clauses_copy[new_order[i]], roles_copy[new_order[i]]);
  }
}

◆ end()

vector< Clause >::iterator Matrix::end ( )

inline

Definition at line 305 of file Matrix.hpp.

305{ return clauses.end(); }

◆ find_all_extensions()

void Matrix::find_all_extensions	(	Unifier &	u,
		vector< InferenceItem > &	result,
		Clause &	c,
		VariableIndex &	var_index,
		TermIndex &	term_index
	)

Find all possible extensions given a Clause, considering all Literals in the Clause.

See the documentation for find_extensions, which does all the heavy lifting.

Parameters

u	A reference to a Unifier function object.
result	A reference to a vector of InferenceItems. Start with this empty.
c	The Clause of interest.
var_index	A reference to the VariableIndex.
term_index	A reference to the TermIndex.

Definition at line 222 of file Matrix.cpp.

                                                {
  if (c.size() == 0) {
    cerr << "You shouldn't be looking for extensions with an empty clause" << endl;
    return;
  }
  for (size_t index = 0; index < c.size(); index++) {
      find_extensions(u, result, c[index], index, var_index, term_index);
  }
}

◆ find_extensions()

void Matrix::find_extensions	(	Unifier &	u,
		vector< InferenceItem > &	result,
		const Literal &	lit,
		LitNum	ind,
		VariableIndex &	var_index,
		TermIndex &	term_index
	)

private

Find all possible extensions, given a Literal.

Essentially this involves finding all the Clauses in the Matrix containing a Literal complementary to the one of interest, and selecting each of those Literals that unifies with the one of interest. You can do this by traversing a single row of the index.

It's up to the caller to decide whether to clear the result.

Parameters

u	Reference to a Unifier function object.
result	Reference to a vector of InferenceItems.
lit	Reference to the Literal of interest.
ind	the index (position) of the Literal in its Clause.
var_index	Reference to the VariableIndex.
term_index	Reference to the TermIndex.

Definition at line 191 of file Matrix.cpp.

                                                                              {
    Literal neg_lit(lit);
    neg_lit.invert();
    size_t i = neg_lit.get_pred_as_index();
    for (const MatrixPairType& p : index[i]) {
        ClauseNum c_num = p.first;
        LitNum l_num = p.second;
        var_index.add_backtrack_point();
        Clause new_c = (clauses[c_num]).make_copy_with_new_vars(var_index, term_index);
        UnificationOutcome outcome = u(neg_lit, new_c[l_num]);
        if (outcome == UnificationOutcome::Succeed) {
            result.push_back(InferenceItem(InferenceItemType::Extension, lit, ind,
                            c_num, l_num, u.get_substitution()));
        }
        var_index.backtrack();
        u.backtrack();
    }
}

◆ find_limited_extensions()

void Matrix::find_limited_extensions	(	Unifier &	u,
		vector< InferenceItem > &	result,
		Clause &	c,
		VariableIndex &	var_index,
		TermIndex &	term_index
	)

Find all possible extensions given a Clause, but only consider the first Literal in the Clause.

See the documentation for find_extensions, which does all the heavy lifting.

Parameters

u	A reference to a Unifier function object.
result	A reference to a vector of InferenceItems. Start with this empty.
c	The Clause of interest.
var_index	A reference to the VariableIndex.
term_index	A reference to the TermIndex.

Definition at line 212 of file Matrix.cpp.

                                                {
  if (c.size() == 0) {
    cerr << "You shouldn't be looking for extensions with an empty clause" << endl;
    return;
  }
  find_extensions(u, result, c[0], 0, var_index, term_index);
}

◆ find_start()

pair< bool, size_t > Matrix::find_start ( ) const

Use a simple heuristic to find a good start clause.

Find a start clause that is positive/negative according to the –negative flag, and if possible also a conjecture clause. Also, indicate if there is no positive/negative clause, which means the problem is trivial.

Definition at line 51 of file Matrix.cpp.

                                           {
  bool found_positive = false;
  bool found_negative = false;
  size_t first_positive = 0;
  size_t first_negative = 0;
  bool found_candidate = false;
  size_t candidate = 0;
  size_t i = 0;
  for (bool positive : positive_clauses) {
    if (positive_clauses[i]) {
      if (!found_positive) {
        first_positive = i;
        found_positive = true;
      }
    }
    if (negative_clauses[i]) {
      if (!found_negative) {
        first_negative = i;
        found_negative = true;
      }
    }
    if (is_conjecture(i) && !found_candidate) {
      if ((params::positive_representation && positive_clauses[i]) ||
         (!params::positive_representation && negative_clauses[i])) {
            found_candidate = true;
            candidate = i;
      }
    }
    i++;
  }
  if (!(found_positive && found_negative))
    return pair<bool,size_t>(false, 0);
  if (found_candidate)
    return pair<bool, size_t>(true, candidate);
  else if (params::positive_representation)
    return pair<bool, size_t>(true, first_positive);
  else
    return pair<bool, size_t>(true, first_negative);
}

◆ get_num_clauses()

ClauseNum Matrix::get_num_clauses ( ) const

inline

Straightforward get method.

Definition at line 191 of file Matrix.hpp.

191{ return clauses.size(); }

◆ is_conjecture()

bool Matrix::is_conjecture ( size_t i ) const

Is a particular Clause a conjecture?

Parameters

i	Index of Clause to check.

Definition at line 46 of file Matrix.cpp.

                                         {
  return clause_roles[i] == "negated_conjecture" ||
         clause_roles[i] == "conjecture";
}

◆ is_negative()

bool Matrix::is_negative ( size_t i ) const

inline

Is a particular Clause negative?.

Parameters

i	Index of Clause to check.

Definition at line 211 of file Matrix.hpp.

211{ return negative_clauses[i]; }

◆ is_positive()

bool Matrix::is_positive ( size_t i ) const

inline

Is a particular Clause positive?.

Parameters

i	Index of Clause to check.

Definition at line 205 of file Matrix.hpp.

205{ return positive_clauses[i]; }

◆ make_clauses_copy()

void Matrix::make_clauses_copy ( )

inlineprivate

Store a copy of the clauses.

Definition at line 151 of file Matrix.hpp.

                             {
      clauses_copy.clear();
      clauses_copy = clauses;
      roles_copy.clear();
      roles_copy = clause_roles;
    }

◆ make_LaTeX()

string Matrix::make_LaTeX ( bool subbed = false ) const

Make a usable LaTeX representation.

Parameters

subbed Implement substitutions if true.

Definition at line 257 of file Matrix.cpp.

                                           {
  string s ("\\[\n\\begin{split}\n");
  s += "\\textcolor{magenta}{M} = ";
  for (const Clause& c : clauses) {
    s += "&\\,";
    s += c.make_LaTeX(subbed);
    s += "\\\\";
  }
  s += "\n\\end{split}\n\\]\n";
 
  return s;
}

◆ move_equals_to_start()

void Matrix::move_equals_to_start ( )

Self-explanatory.

BUT only do this to the matrix built at the start of the process, as it assumes the equality axioms are at the end of the matrix.

Definition at line 167 of file Matrix.cpp.

                                  {
  if (num_equals == 0) {
    cerr << "Why are you trying to move equality axioms - there aren't any?" << endl;
    return;
  }
  make_clauses_copy();
  clauses.clear();
  positive_clauses.clear();
  negative_clauses.clear();
  clause_roles.clear();
  size_t s2 = index.size();
  index.clear();
  index = vector<vector<MatrixPairType> >(s2, vector<MatrixPairType>());
  size_t n_clauses = clauses_copy.size();
  for (size_t i = n_clauses - num_equals; i < n_clauses; i++) {
    add_clause(clauses_copy[i], roles_copy[i]);
  }
  for (size_t i = 0; i < n_clauses - num_equals; i++) {
    add_clause(clauses_copy[i], roles_copy[i]);
  }
  clauses_copy.clear();
  roles_copy.clear();
}

◆ operator[]()

const Clause & Matrix::operator[] ( size_t i ) const

inline

Straightforward get method.

Beware - the parameter is not checked, so behave!

Parameters

i	Index of item to get.

Definition at line 199 of file Matrix.hpp.

199{ return clauses[i]; }

◆ random_reorder()

void Matrix::random_reorder ( )

Randomly reorder the matrix.

Only store a copy of the clauses the first time you do this.

Definition at line 136 of file Matrix.cpp.

                            {
  if (!copy_saved) {
    copy_saved = true;
    make_clauses_copy();
  }
  /*
  * Find a suitably reordered set of indices.
  */
  vector<uint32_t> new_order;
  size_t s = clauses.size();
  for (size_t i = 0; i < s; i++)
    new_order.push_back(i);
  std::shuffle(new_order.begin(), new_order.end(), d);
  /*
  * Clear and rebuild as necessary.
  */
  clauses.clear();
  positive_clauses.clear();
  negative_clauses.clear();
  clause_roles.clear();
  size_t s2 = index.size();
  index.clear();
  index = vector<vector<MatrixPairType> >(s2, vector<MatrixPairType>());
  for (size_t i = 0; i < s; i++) {
    add_clause(clauses_copy[new_order[i]], roles_copy[new_order[i]]);
  }
}

◆ set_num_equals()

void Matrix::set_num_equals ( uint32_t n )

inline

Straightforward set method.

Parameters

n	Number of equality axioms.

Definition at line 223 of file Matrix.hpp.

223{ num_equals = n; }

◆ set_num_preds()

void Matrix::set_num_preds ( size_t num_predicates )

Make an empty index.

Definition at line 42 of file Matrix.cpp.

                                                {
    index = vector<vector<MatrixPairType> >((num_predicates * 2), vector<MatrixPairType>());
}

◆ show_tptp()

void Matrix::show_tptp ( ) const

Output in TPTP compatible format.

Definition at line 287 of file Matrix.cpp.

                             {
  size_t matrix_i = 0;
  for (const Clause& c : clauses) {
    cout << "cnf(matrix-";
    cout << std::to_string(matrix_i++);
    cout << ", plain, ";
    cout << c.to_tptp_string();
    cout << ").";
    cout << std::endl;
  }
}

◆ to_string()

string Matrix::to_string ( ) const

Make a string representation.

Definition at line 234 of file Matrix.cpp.

                               {
  string result;
  colour_string::ColourString cs(params::use_colours);
  size_t i = 0;
  for (const Clause& c : clauses) {
    if (is_conjecture(i))
      result += cs("*").orange();
    else
      result += " ";
    if (positive_clauses[i])
      result += cs("+").orange();
    else if (negative_clauses[i])
      result += cs("-").orange();
    else
      result += " ";
    result += " ";
    i++;
    result += c.to_string();
    result += "\n";
  }
  return result;
}

◆ write_to_prolog_file()

void Matrix::write_to_prolog_file ( const path & path_to_file ) const

Write to a file that can be read by Prolog.

This is for proof checking.

Parameters

path_to_file Reference to path object.

Definition at line 270 of file Matrix.cpp.

                                                                {
  std::ofstream file(path_to_file);
  size_t matrix_i = 0;
  // Nasty hack needed to stop the proof checker from printing 
  // a bunch of warnings when reading the matrix.
  file << ":- style_check(-singleton)." << std::endl;
  for (const Clause& c : clauses) {
    file << "matrix(";
    file << std::to_string(matrix_i++);
    file << ", ";
    file << c.to_prolog_string();
    file << ").";
    file << std::endl;
  }
  file.close();
}

Friends And Related Symbol Documentation

◆ operator<<

ostream & operator<<	(	ostream &	out,
		const Matrix &	m
	)

friend

Definition at line 299 of file Matrix.cpp.

                                                   {
    out << "Clauses in matrix:" << endl;
    out << "------------------" << endl;
    size_t i = 0;
    for (const Clause& c : m.clauses)
        out << setw(params::output_width) << i++
        << ": " << c << endl;
    vector<string> index_lits(m.index.size(), string(""));
    for (Clause c : m.clauses)
      for (size_t i = 0; i < c.size(); i++)
        index_lits[c[i].get_pred_as_index()] = c[i].get_small_lit();
    i = 0;
    out << endl << "Index: (Clause, Literal):" << endl;
    out <<         "-------------------------" << endl;
    for (vector<MatrixPairType> v : m.index) {
        out << setw(params::output_width + 20) << index_lits[i++] << ": ";
        for (MatrixPairType p : v) {
            out << "(" << p.first << ", " << p.second << ") ";
        }
        out << endl;
    }
    return out;
}

Member Data Documentation

◆ clause_roles

vector<string> Matrix::clause_roles

private

Keep track of which clauses are conjectures etc.

This allows start clause heuristics to be applied.

Definition at line 95 of file Matrix.hpp.

◆ clauses

vector<Clause> Matrix::clauses

private

The Matrix itself is just a set of Clauses.

Definition at line 77 of file Matrix.hpp.

◆ clauses_copy

vector<Clause> Matrix::clauses_copy

private

It makes sense to keep a copy of the clauses if your schedule reorders multiple times.

Definition at line 105 of file Matrix.hpp.

◆ copy_saved

bool Matrix::copy_saved

private

Remember whether you've saved a copy.

Definition at line 114 of file Matrix.hpp.

◆ d

std::mt19937 Matrix::d

staticprivate

Randomness for random reordering.

Definition at line 126 of file Matrix.hpp.

◆ index

vector<vector<MatrixPairType> > Matrix::index

private

We want to be able to quickly identify where in each clause a particular literal lives.

Store clause and position as pairs in a row corresponding to the literal.

Definition at line 122 of file Matrix.hpp.

◆ negative_clauses

vector<bool> Matrix::negative_clauses

private

Keep track of which clauses are negative.

This allows start clause heuristics to be applied.

Definition at line 89 of file Matrix.hpp.

◆ num_equals

uint32_t Matrix::num_equals

private

You need to know how many equality axioms there are in case you want to move them around.

Definition at line 100 of file Matrix.hpp.

◆ positive_clauses

vector<bool> Matrix::positive_clauses

private

Keep track of which clauses are positive.

This allows start clause heuristics to be applied.

Definition at line 83 of file Matrix.hpp.

◆ roles_copy

vector<string> Matrix::roles_copy

private

It makes sense to keep a copy of the roles if your schedule reorders multiple times.

Definition at line 110 of file Matrix.hpp.

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

source/Matrix.hpp
source/Matrix.cpp

Public Member Functions

Private Member Functions

Private Attributes

Static Private Attributes

Friends

Detailed Description

Constructor & Destructor Documentation

◆ Matrix() [1/3]

◆ Matrix() [2/3]

◆ Matrix() [3/3]

Member Function Documentation

◆ add_clause()

◆ begin()

◆ cbegin()

◆ cend()

◆ deterministic_reorder()

◆ end()

◆ find_all_extensions()

◆ find_extensions()

◆ find_limited_extensions()

◆ find_start()

◆ get_num_clauses()

◆ is_conjecture()

◆ is_negative()

◆ is_positive()

◆ make_clauses_copy()

◆ make_LaTeX()

◆ move_equals_to_start()

◆ operator[]()

◆ random_reorder()

◆ set_num_equals()

◆ set_num_preds()

◆ show_tptp()

◆ to_string()

◆ write_to_prolog_file()

Friends And Related Symbol Documentation

◆ operator<<

Member Data Documentation

◆ clause_roles

◆ clauses

◆ clauses_copy

◆ copy_saved

◆ d

◆ index

◆ negative_clauses

◆ num_equals

◆ positive_clauses

◆ roles_copy