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.

size_t	get_index_entry_size (size_t _i) const
	The ExtensionEnumerator needs to know this.

MatrixPairType	get_index_entry (size_t _i, size_t _j) const
	The ExtensionEnumerator needs to know this.

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

const Literal &	inspect_literal (size_t i, size_t j)
	Straightforward get method.

const Literal &	inspect_index_literal (size_t i, size_t j)
	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_ground (size_t i) const
	Is a particular Clause ground?

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	deterministic_reorder (size_t)
	Deterministic reorder of the clauses.

void	random_reorder ()
	Randomly reorder the matrix.

void	random_reorder_literals ()
	Randomly reorder the literals in each clause in 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.

void	sort_clauses_by_increasing_size ()
	Self-explanatory.

void	get_literal_clause_pair (LitNum, size_t, Literal &, Clause &) const
	Get a literal and clause from the index.

Private Member Functions
void	make_clauses_copy ()
	Store a copy of the clauses.

void	rebuild_index (vector< Clause > &, vector< string > &)
	Rebuild the index after, for example, reordering.

template<class Comparison >
void	sort_clauses (Comparison comparison)
	Template method for general sorting of clauses, which sorts roles at the same time.

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< bool >	ground_clauses
	We need to know this to control backtracking.

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.

vector< vector< LiteralClausePairType > >	literal_clause_index
	This corresponds closely to index, but has the actual Literal, and the Clause after the Literal's removal.

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 a pair of indexes to help with that.

Definition at line 74 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 194 of file Matrix.hpp.

    : clauses()
    , index()
    , literal_clause_index()
    , positive_clauses()
    , negative_clauses()
    , ground_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>())
, literal_clause_index((num_predicates * 2), vector<LiteralClausePairType>())
, positive_clauses()
, negative_clauses()
, ground_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 97 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));
        Clause new_clause = clause;
        new_clause.drop_literal(literal_number);
        literal_clause_index[i].push_back(LiteralClausePairType(clause[j], new_clause));
        literal_number++;
    }
    clauses.push_back(clause);
    positive_clauses.push_back(clause.is_positive());
    negative_clauses.push_back(clause.is_negative());
    ground_clauses.push_back(clause.is_ground());
    clause_roles.push_back(role);
}

◆ begin()

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

inline

Definition at line 351 of file Matrix.hpp.

351{ return clauses.begin(); }

◆ cbegin()

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

inline

Definition at line 349 of file Matrix.hpp.

349{ return clauses.cbegin(); }

◆ cend()

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

inline

Definition at line 350 of file Matrix.hpp.

350{ 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 133 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);
  /*
  * Do the reordering.
  */
  vector<Clause> cs;
  vector<string> ss;
  for (size_t i = 0; i < s; i++) {
    cs.push_back(clauses_copy[new_order[i]]);
    ss.push_back(roles_copy[new_order[i]]);
  }
  /*
  * Clear and rebuild as necessary.
  */
  rebuild_index(cs, ss);
}

◆ end()

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

inline

Definition at line 352 of file Matrix.hpp.

352{ return clauses.end(); }

◆ 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 54 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_index_entry()

MatrixPairType Matrix::get_index_entry	(	size_t	_i,
		size_t	_j ) const

inline

The ExtensionEnumerator needs to know this.

Definition at line 235 of file Matrix.hpp.

                                                                      {
      return (index[_i])[_j];
    }

◆ get_index_entry_size()

size_t Matrix::get_index_entry_size ( size_t _i ) const

inline

The ExtensionEnumerator needs to know this.

Definition at line 229 of file Matrix.hpp.

                                                        {
      return index[_i].size();
    }

◆ get_literal_clause_pair()

void Matrix::get_literal_clause_pair	(	LitNum	_l,
		size_t	_i,
		Literal &	_lit,
		Clause &	_clause ) const

Get a literal and clause from the index.

Parameters

_l	Index for the literal of interest.
_i	Index for where the pair is in _lit's vector.
_lit	Result literal.
_clause	Result clause.

Definition at line 301 of file Matrix.cpp.

                                                                                               {
  LiteralClausePairType result = (literal_clause_index[_l])[_i];
  _lit = result.first;
  _clause = result.second;
}

◆ get_num_clauses()

ClauseNum Matrix::get_num_clauses ( ) const

inline

Straightforward get method.

Definition at line 225 of file Matrix.hpp.

225{ return clauses.size(); }

◆ inspect_index_literal()

const Literal & Matrix::inspect_index_literal	(	size_t	i,
		size_t	j )

inline

Straightforward get method.

Beware - the parameters are not checked, so behave!

Parameters

i	Index in literal_clause_index;
j	Index of required entry.

Definition at line 265 of file Matrix.hpp.

                                                                    { 
      return (literal_clause_index[i])[j].first; 
    }

◆ inspect_literal()

const Literal & Matrix::inspect_literal	(	size_t	i,
		size_t	j )

inline

Straightforward get method.

Beware - the parameters are not checked, so behave!

Parameters

i	Index of clause to get.
j	Index of literal in clause.

Definition at line 254 of file Matrix.hpp.

                                                              { 
      return (clauses[i])[j]; 
    }

◆ 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 49 of file Matrix.cpp.

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

◆ is_ground()

bool Matrix::is_ground ( size_t i ) const

inline

Is a particular Clause ground?

Parameters

i	Index of Clause to check.

Definition at line 285 of file Matrix.hpp.

285{ return ground_clauses[i]; }

◆ 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 279 of file Matrix.hpp.

279{ 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 273 of file Matrix.hpp.

273{ return positive_clauses[i]; }

◆ make_clauses_copy()

void Matrix::make_clauses_copy ( )

inlineprivate

Store a copy of the clauses.

Definition at line 141 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 259 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 208 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();
  ground_clauses.clear();
  clause_roles.clear();
  size_t s2 = index.size();
  size_t s3 = literal_clause_index.size();
  index.clear();
  literal_clause_index.clear();
  index = vector<vector<MatrixPairType> >(s2, vector<MatrixPairType>());
  literal_clause_index = vector<vector<LiteralClausePairType> >(s3, vector<LiteralClausePairType>());
  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 245 of file Matrix.hpp.

245{ return clauses[i]; }

◆ random_reorder()

void Matrix::random_reorder ( )

Randomly reorder the matrix.

Definition at line 164 of file Matrix.cpp.

                            {
  vector<Clause> saved_clauses(clauses);
  vector<string> saved_clause_roles(clause_roles);
  /*
  * 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);
  /*
  * Do the reordering.
  */
  vector<Clause> cs;
  vector<string> ss;
  for (size_t i = 0; i < s; i++) {
    cs.push_back(saved_clauses[new_order[i]]);
    ss.push_back(saved_clause_roles[new_order[i]]);
  }
  /*
  * Clear and rebuild as necessary.
  */
  rebuild_index(cs, ss);
}

◆ random_reorder_literals()

void Matrix::random_reorder_literals ( )

Randomly reorder the literals in each clause in the matrix.

Definition at line 190 of file Matrix.cpp.

                                     {
  vector<Clause> saved_clauses(clauses);
  vector<string> saved_clause_roles(clause_roles);
  size_t s = clauses.size();
  /*
  * Reorder.
  */
  for (size_t i = 0; i < s; i++) {
    Clause c(saved_clauses[i]);
    c.random_reorder();
    saved_clauses[i] = c;
  }
  /*
  * Clear and rebuild as necessary.
  */
  rebuild_index(saved_clauses, saved_clause_roles);
}

◆ rebuild_index()

void Matrix::rebuild_index	(	vector< Clause > &	cs,
		vector< string > &	ss )

private

Rebuild the index after, for example, reordering.

Parameters

cs	Vector of clauses.
ss	Vector of strings.

Definition at line 115 of file Matrix.cpp.

                                                                 {
  size_t s = clauses.size();
  clauses.clear();
  positive_clauses.clear();
  negative_clauses.clear();
  ground_clauses.clear();
  clause_roles.clear();
  size_t s2 = index.size();
  size_t s3 = literal_clause_index.size();
  index.clear();
  literal_clause_index.clear();
  index = vector<vector<MatrixPairType> >(s2, vector<MatrixPairType>());
  literal_clause_index = vector<vector<LiteralClausePairType> >(s3, vector<LiteralClausePairType>());
  for (size_t i = 0; i < s; i++) {
    add_clause(cs[i], ss[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 297 of file Matrix.hpp.

297{ num_equals = n; }

◆ set_num_preds()

void Matrix::set_num_preds ( size_t num_predicates )

Make an empty index.

Definition at line 44 of file Matrix.cpp.

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

◆ show_tptp()

void Matrix::show_tptp ( ) const

Output in TPTP compatible format.

Definition at line 289 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;
  }
}

◆ sort_clauses()

template<class Comparison >

void Matrix::sort_clauses ( Comparison comparison )

inlineprivate

Template method for general sorting of clauses, which sorts roles at the same time.

ClauseComparisons.hpp contains function objects that can be used with this to implement different orderings.

Definition at line 162 of file Matrix.hpp.

                                             {
      /*
      * Combine the clauses with their roles.
      */
      vector<ClauseAndRole> cr;
      size_t s = clauses.size();
      for (size_t i = 0; i < s; i++) {
        cr.push_back(ClauseAndRole(clauses[i], clause_roles[i]));
      }
      /*
      * Sort them according to the relevant ordering.
      */
      std::sort(cr.begin(), cr.end(), comparison);
      /*
      * Split them again and re-build the index.
      */
      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(cr[i].first, cr[i].second);
      }
    }

◆ sort_clauses_by_increasing_size()

void Matrix::sort_clauses_by_increasing_size ( )

inline

Self-explanatory.

Inspired by "Machine Learning Guidance for Connection Tableaux," Farber et al. 2020 although with a different measure of size and happening at a different place.

Makes use of the sort_clauses template.

Definition at line 385 of file Matrix.hpp.

                                           {
      ClauseLengthCompare comparison;
      sort_clauses<ClauseLengthCompare>(comparison);
    }

◆ to_string()

string Matrix::to_string ( ) const

Make a string representation.

Definition at line 236 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 272 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 307 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;
        if (m.ground_clauses[i++]) {
          out << " (ground)";
        }
        out << 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;
    }
    out << endl << "Index: (Literal, Clause without Literal):" << endl;
    out <<         "-----------------------------------------" << endl;
    i = 0;
    for (vector<LiteralClausePairType> v : m.literal_clause_index) {
        out << setw(params::output_width + 20) << index_lits[i++] << ": "  << endl;;
        for (LiteralClausePairType p : v) {
            out << p.first.to_string() << " --- " << p.second.to_string() << endl;
        }
        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 101 of file Matrix.hpp.

◆ clauses

vector<Clause> Matrix::clauses

private

The Matrix itself is just a set of Clauses.

Definition at line 79 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 111 of file Matrix.hpp.

◆ copy_saved

bool Matrix::copy_saved

private

Remember whether you've saved a copy.

Definition at line 120 of file Matrix.hpp.

◆ d

std::mt19937 Matrix::d

staticprivate

Randomness for random reordering.

Definition at line 137 of file Matrix.hpp.

◆ ground_clauses

vector<bool> Matrix::ground_clauses

private

We need to know this to control backtracking.

Definition at line 95 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 128 of file Matrix.hpp.

◆ literal_clause_index

vector<vector<LiteralClausePairType> > Matrix::literal_clause_index

private

This corresponds closely to index, but has the actual Literal, and the Clause after the Literal's removal.

Definition at line 133 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 91 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 106 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 85 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 116 of file Matrix.hpp.

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

/Users/sbh11/Desktop/connection-prover/c++/connect++/source/Matrix.hpp
/Users/sbh11/Desktop/connection-prover/c++/connect++/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_start()

◆ get_index_entry()

◆ get_index_entry_size()

◆ get_literal_clause_pair()

◆ get_num_clauses()

◆ inspect_index_literal()

◆ inspect_literal()

◆ is_conjecture()

◆ is_ground()

◆ is_negative()

◆ is_positive()

◆ make_clauses_copy()

◆ make_LaTeX()

◆ move_equals_to_start()

◆ operator[]()

◆ random_reorder()

◆ random_reorder_literals()

◆ rebuild_index()

◆ set_num_equals()

◆ set_num_preds()

◆ show_tptp()

◆ sort_clauses()

◆ sort_clauses_by_increasing_size()

◆ to_string()

◆ write_to_prolog_file()

Friends And Related Symbol Documentation

◆ operator<<

Member Data Documentation

◆ clause_roles

◆ clauses

◆ clauses_copy

◆ copy_saved

◆ d

◆ ground_clauses

◆ index

◆ literal_clause_index

◆ negative_clauses

◆ num_equals

◆ positive_clauses

◆ roles_copy