38#include "InferenceItem.hpp"
50using std::filesystem::path;
58using MatrixPairType = pair<ClauseNum, LitNum>;
122 vector<vector<MatrixPairType>>
index;
126 static std::mt19937
d;
302 vector<Clause>::const_iterator cbegin()
const {
return clauses.cbegin(); }
303 vector<Clause>::const_iterator cend()
const {
return clauses.cend(); }
304 vector<Clause>::iterator begin() {
return clauses.begin(); }
305 vector<Clause>::iterator end() {
return clauses.end(); }
329 friend ostream& operator<<(ostream&,
const Matrix&);
Representation of clauses.
Basic representation of literals, bundling together (pointers to) a Predicate, a collection of argume...
Representation of the Matrix within a proof.
string to_string() const
Make a string representation.
vector< Clause > clauses
The Matrix itself is just a set of Clauses.
void deterministic_reorder(size_t)
Deterministic reorder of the clauses.
void move_equals_to_start()
Self-explanatory.
ClauseNum get_num_clauses() const
Straightforward get method.
string make_LaTeX(bool=false) const
Make a usable LaTeX representation.
vector< string > clause_roles
Keep track of which clauses are conjectures etc.
void make_clauses_copy()
Store a copy of the clauses.
void find_extensions(Unifier &, vector< InferenceItem > &, const Literal &, LitNum, VariableIndex &, TermIndex &)
Find all possible extensions, given a Literal.
Matrix()
Use this constructor if you really want an empty Matrix.
uint32_t num_equals
You need to know how many equality axioms there are in case you want to move them around.
vector< vector< MatrixPairType > > index
We want to be able to quickly identify where in each clause a particular literal lives.
void add_clause(Clause &, string="")
Add a Clause to the Matrix and update the index accordingly.
bool is_negative(size_t i) const
Is a particular Clause negative?.
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.
bool copy_saved
Remember whether you've saved a copy.
static std::mt19937 d
Randomness for random reordering.
void find_all_extensions(Unifier &, vector< InferenceItem > &, Clause &, VariableIndex &, TermIndex &)
Find all possible extensions given a Clause, considering all Literals in the Clause.
bool is_conjecture(size_t i) const
Is a particular Clause a conjecture?
vector< string > roles_copy
It makes sense to keep a copy of the roles if your schedule reorders multiple times.
void write_to_prolog_file(const path &) const
Write to a file that can be read by Prolog.
void set_num_equals(uint32_t n)
Straightforward set method.
const Clause & operator[](size_t i) const
Straightforward get method.
Matrix(const Matrix &)=delete
You're never going to need to copy a Matrix.
bool is_positive(size_t i) const
Is a particular Clause positive?.
void show_tptp() const
Output in TPTP compatible format.
vector< Clause > clauses_copy
It makes sense to keep a copy of the clauses if your schedule reorders multiple times.
void set_num_preds(size_t)
Make an empty index.
pair< bool, size_t > find_start() const
Use a simple heuristic to find a good start clause.
void random_reorder()
Randomly reorder the matrix.
vector< bool > negative_clauses
Keep track of which clauses are negative.
vector< bool > positive_clauses
Keep track of which clauses are positive.
Look after terms, (ideally) using hash consing to avoid storing copies of terms.
Wrap up various applications of unificiation into a single class: all the unification you need to do ...
Storage of named variables, and management of new, anonymous variables.