Connect++ 0.3.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
Matrix.hpp
1/*
2
3Copyright © 2023-24 Sean Holden. All rights reserved.
4
5*/
6/*
7
8This file is part of Connect++.
9
10Connect++ is free software: you can redistribute it and/or modify it
11under the terms of the GNU General Public License as published by the
12Free Software Foundation, either version 3 of the License, or (at your
13option) any later version.
14
15Connect++ is distributed in the hope that it will be useful, but WITHOUT
16ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
17FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for
18more details.
19
20You should have received a copy of the GNU General Public License along
21with Connect++. If not, see <https://www.gnu.org/licenses/>.
22
23*/
24
25#ifndef MATRIX_HPP
26#define MATRIX_HPP
27
28#include<iostream>
29#include<fstream>
30#include<filesystem>
31#include<iomanip>
32#include<string>
33#include<vector>
34#include<tuple>
35#include<algorithm>
36#include<random>
37
38#include "InferenceItem.hpp"
39#include "Clause.hpp"
40#include "Unifier.hpp"
41#include "Reorder.hpp"
42
43using std::pair;
44using std::tuple;
45using std::vector;
46using std::ostream;
47using std::endl;
48using std::setw;
49using std::cout;
50using std::filesystem::path;
51
58using MatrixPairType = pair<ClauseNum, LitNum>;
59
72class Matrix {
73private:
77 vector<Clause> clauses;
83 vector<bool> positive_clauses;
89 vector<bool> negative_clauses;
95 vector<string> clause_roles;
100 uint32_t num_equals;
105 vector<Clause> clauses_copy;
110 vector<string> roles_copy;
122 vector<vector<MatrixPairType>> index;
126 static std::mt19937 d;
146 void find_extensions(Unifier&, vector<InferenceItem>&, const Literal&,
147 LitNum, VariableIndex&, TermIndex&);
152 clauses_copy.clear();
154 roles_copy.clear();
156 }
157public:
163 : clauses()
164 , index()
167 , clause_roles()
168 , clauses_copy()
169 , roles_copy()
170 , copy_saved(false)
171 {}
178 Matrix(size_t);
184 Matrix(const Matrix&) = delete;
185 Matrix(const Matrix&&) = delete;
186 Matrix& operator=(const Matrix&) = delete;
187 Matrix& operator=(const Matrix&&) = delete;
191 ClauseNum get_num_clauses() const { return clauses.size(); }
199 const Clause& operator[](size_t i) const { return clauses[i]; }
205 bool is_positive(size_t i) const { return positive_clauses[i]; }
211 bool is_negative(size_t i) const { return negative_clauses[i]; }
217 bool is_conjecture(size_t i) const;
223 inline void set_num_equals(uint32_t n) { num_equals = n; }
232 pair<bool,size_t> find_start() const;
236 void set_num_preds(size_t);
245 void add_clause(Clause&, string = "");
260 void find_limited_extensions(Unifier&, vector<InferenceItem>&, Clause&,
276 void find_all_extensions(Unifier&, vector<InferenceItem>&, Clause&,
286 void deterministic_reorder(size_t);
290 void random_reorder();
299 /*
300 * Iteration on a Matrix is just iteration over the Clauses.
301 */
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(); }
309 string to_string() const;
315 string make_LaTeX(bool = false) const;
323 void write_to_prolog_file(const path&) const;
327 void show_tptp() const;
328
329 friend ostream& operator<<(ostream&, const Matrix&);
330};
331
332
333#endif
Representation of clauses.
Definition Clause.hpp:52
Basic representation of literals, bundling together (pointers to) a Predicate, a collection of argume...
Definition Literal.hpp:50
Representation of the Matrix within a proof.
Definition Matrix.hpp:72
string to_string() const
Make a string representation.
Definition Matrix.cpp:234
vector< Clause > clauses
The Matrix itself is just a set of Clauses.
Definition Matrix.hpp:77
void deterministic_reorder(size_t)
Deterministic reorder of the clauses.
Definition Matrix.cpp:105
void move_equals_to_start()
Self-explanatory.
Definition Matrix.cpp:167
ClauseNum get_num_clauses() const
Straightforward get method.
Definition Matrix.hpp:191
string make_LaTeX(bool=false) const
Make a usable LaTeX representation.
Definition Matrix.cpp:257
vector< string > clause_roles
Keep track of which clauses are conjectures etc.
Definition Matrix.hpp:95
void make_clauses_copy()
Store a copy of the clauses.
Definition Matrix.hpp:151
void find_extensions(Unifier &, vector< InferenceItem > &, const Literal &, LitNum, VariableIndex &, TermIndex &)
Find all possible extensions, given a Literal.
Definition Matrix.cpp:191
Matrix()
Use this constructor if you really want an empty Matrix.
Definition Matrix.hpp:162
uint32_t num_equals
You need to know how many equality axioms there are in case you want to move them around.
Definition Matrix.hpp:100
vector< vector< MatrixPairType > > index
We want to be able to quickly identify where in each clause a particular literal lives.
Definition Matrix.hpp:122
void add_clause(Clause &, string="")
Add a Clause to the Matrix and update the index accordingly.
Definition Matrix.cpp:91
bool is_negative(size_t i) const
Is a particular Clause negative?.
Definition Matrix.hpp:211
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.
Definition Matrix.cpp:212
bool copy_saved
Remember whether you've saved a copy.
Definition Matrix.hpp:114
static std::mt19937 d
Randomness for random reordering.
Definition Matrix.hpp:126
void find_all_extensions(Unifier &, vector< InferenceItem > &, Clause &, VariableIndex &, TermIndex &)
Find all possible extensions given a Clause, considering all Literals in the Clause.
Definition Matrix.cpp:222
bool is_conjecture(size_t i) const
Is a particular Clause a conjecture?
Definition Matrix.cpp:46
vector< string > roles_copy
It makes sense to keep a copy of the roles if your schedule reorders multiple times.
Definition Matrix.hpp:110
void write_to_prolog_file(const path &) const
Write to a file that can be read by Prolog.
Definition Matrix.cpp:270
void set_num_equals(uint32_t n)
Straightforward set method.
Definition Matrix.hpp:223
const Clause & operator[](size_t i) const
Straightforward get method.
Definition Matrix.hpp:199
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?.
Definition Matrix.hpp:205
void show_tptp() const
Output in TPTP compatible format.
Definition Matrix.cpp:287
vector< Clause > clauses_copy
It makes sense to keep a copy of the clauses if your schedule reorders multiple times.
Definition Matrix.hpp:105
void set_num_preds(size_t)
Make an empty index.
Definition Matrix.cpp:42
pair< bool, size_t > find_start() const
Use a simple heuristic to find a good start clause.
Definition Matrix.cpp:51
void random_reorder()
Randomly reorder the matrix.
Definition Matrix.cpp:136
vector< bool > negative_clauses
Keep track of which clauses are negative.
Definition Matrix.hpp:89
vector< bool > positive_clauses
Keep track of which clauses are positive.
Definition Matrix.hpp:83
Look after terms, (ideally) using hash consing to avoid storing copies of terms.
Definition TermIndex.hpp:75
Wrap up various applications of unificiation into a single class: all the unification you need to do ...
Definition Unifier.hpp:83
Storage of named variables, and management of new, anonymous variables.