Connect++ 0.6.1
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
Clause.cpp
1/*
2
3Copyright © 2023-25 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#include "Clause.hpp"
26
27std::mt19937 Clause::d(params::random_seed);
28
29//----------------------------------------------------------------------
30bool Clause::is_positive() const {
31#ifdef DEBUGMESSAGES
32 if (c.size() == 0)
33 cerr << "Don't check an empty clause for positivity" << endl;
34#endif
35 for (size_t i = 0; i < c.size(); i++) {
36 if (c[i].is_negative())
37 return false;
38 }
39 return true;
40}
41//----------------------------------------------------------------------
42bool Clause::is_negative() const {
43#ifdef DEBUGMESSAGES
44 if (c.size() == 0)
45 cerr << "Don't check an empty clause for negativity" << endl;
46#endif
47 for (size_t i = 0; i < c.size(); i++) {
48 if (c[i].is_positive())
49 return false;
50 }
51 return true;
52}
53//----------------------------------------------------------------------
55 size_t s = c.size();
56 if (s < 2)
57 return;
58 vector<Literal> new_c;
59 for (size_t i = 0; i < s - 1; i++) {
60 bool found = false;
61 for (size_t j = i+1; j < s; j++ ) {
62 if (c[i] == c[j]) {
63 found = true;
64 break;
65 }
66 }
67 if (!found)
68 new_c.push_back(c[i]);
69 }
70 new_c.push_back(c[s - 1]);
71 c = new_c;
72 }
73//----------------------------------------------------------------------
75 size_t s = c.size();
76 if (s < 2)
77 return false;
78 for (size_t i = 0; i < s - 1; i++) {
79 for (size_t j = i+1; j < s; j++) {
80 if (c[i].is_complement_of(c[j]))
81 return true;
82 }
83 }
84 return false;
85}
86//----------------------------------------------------------------------
87bool Clause::is_ground() const {
88 for (const Literal& l : c) {
89 if (!l.is_ground()) {
90 return false;
91 }
92 }
93 return true;
94}
95//----------------------------------------------------------------------
96void Clause::add_lit(const Literal& l) {
97 for (size_t i = 0; i < c.size(); i++)
98 if (c[i] == l) {
99#ifdef DEBUGMESSAGES
100 cerr << "Don't duplicate Literals in a clause!" << endl;
101#endif
102 return;
103 }
104 c.push_back(l);
105}
106//----------------------------------------------------------------------
108#ifdef DEBUGMESSAGES
109 if (c.size() == 0)
110 cerr << "You are making a copy of an empty clause" << endl;
111#endif
112 size_t s = c.size();
113 vector<Literal> new_lits;
114 unordered_map<Variable*,Term*> new_vars;
115 for (size_t i = 0; i < s; i++)
116 new_lits.push_back(c[i].make_copy_with_new_vars_helper(vi, ti, new_vars));
117 return Clause(new_lits);
118}
119//----------------------------------------------------------------------
121#ifdef DEBUGMESSAGES
122 if (c.size() == 0)
123 cerr << "You are making a copy of an empty clause" << endl;
124#endif
125 size_t s = c.size();
126 vector<Literal> new_lits;
127 unordered_map<Variable*,Term*> new_vars;
128 for (size_t i = 0; i < s; i++)
129 new_lits.push_back(c[i].make_copy_with_new_unique_vars_helper(vi, ti, new_vars));
130 return Clause(new_lits);
131}
132//---------------------------------------------------------------------------
134 size_t s = c.size();
135 unordered_map<Variable*,Term*> new_vars;
136 _l.make_copy_with_new_vars_replace_helper(vi, ti, new_vars);
137 // NOTE: make sure _c actually has room in it, unless you want
138 // horror!
139 for (size_t i = 0; i < s; i++)
140 _c.c[i].make_copy_with_new_vars_replace_helper(vi, ti, new_vars);
141}
142//---------------------------------------------------------------------------
143 SimplificationResult Clause::simplify() {
144 // Do this first in case someone has made a clause with
145 // both $true and $false in it.
146 vector<Literal> new_clause;
147 bool clause_is_true = false;
148 for (Literal& lit : c) {
149 if (lit.is_false())
150 continue;
151 if (lit.is_true()) {
152 clause_is_true = true;
153 continue;
154 }
155 new_clause.push_back(lit);
156 }
157 c = new_clause;
158 if (clause_is_true)
159 return SimplificationResult::Tautology;
161 if (c.size() == 0)
162 return SimplificationResult::Contradiction;
164 return SimplificationResult::Tautology;
165 return SimplificationResult::OK;
166}
167//----------------------------------------------------------------------
168void Clause::drop_literal(LitNum l) {
169 if (c.size() == 0) {
170#ifdef DEBUGMESSAGES
171 cerr << "Can't drop_literal from empty clause" << endl;
172#endif
173 return;
174 }
175 if (l > c.size() - 1) {
176#ifdef DEBUGMESSAGES
177 cerr << "drop_literal argument is out of range" << endl;
178#endif
179 return;
180 }
181 if (c.size() == 1) {
182 c.pop_back();
183 return;
184 }
185 c[l] = c.back();
186 c.pop_back();
187}
188//----------------------------------------------------------------------
190 Literal error_lit;
191 if (c.size() == 0) {
192#ifdef DEBUGMESSAGES
193 cerr << "Can't extract_literal from empty clause" << endl;
194#endif
195 return error_lit;
196 }
197 if (l > c.size() - 1) {
198#ifdef DEBUGMESSAGES
199 cerr << "extract_literal argument is out of range" << endl;
200#endif
201 return error_lit;
202 }
203 Literal lit(c[l]);
204 if (c.size() == 1) {
205 c.pop_back();
206 return lit;
207 }
208 c[l] = c.back();
209 c.pop_back();
210 return lit;
211}
212//----------------------------------------------------------------------
214 Literal error_lit;
215 if (c.size() == 0) {
216#ifdef DEBUGMESSAGES
217 cerr << "Can't extract_literal from empty clause" << endl;
218#endif
219 return error_lit;
220 }
221 if (l > c.size() - 1) {
222#ifdef DEBUGMESSAGES
223 cerr << "extract_literal argument is out of range" << endl;
224#endif
225 return error_lit;
226 }
227 Literal lit(c[l]);
228 return lit;
229}
230//----------------------------------------------------------------------
232#ifdef DEBUGMESSAGES
233 if (i > c.size() - 1)
234 cerr << "You're out of range accessing a clause" << endl;
235#endif
236 return c[i];
237}
238//----------------------------------------------------------------------
240 // Make a permutation.
241 vector<size_t> new_order;
242 size_t s = c.size();
243 for (size_t i = 0; i < s; i++)
244 new_order.push_back(i);
245 std::shuffle(new_order.begin(), new_order.end(), d);
246 // Re-order.
247 vector<Literal> new_c = c;
248 for (size_t i = 0; i < s; i++) {
249 c[i] = new_c[new_order[i]];
250 }
251}
252//----------------------------------------------------------------------
254 std::reverse(c.begin(), c.end());
255}
256//----------------------------------------------------------------------
257string Clause::to_string(bool subbed) const {
258 return vector_to_string(c, subbed, "{ ", " }", ", ");
259}
260//----------------------------------------------------------------------
262 commas::comma com(c.size());
263 string result("[ ");
264 for (const Literal& l : c) {
265 result += l.to_prolog_string();
266 result += com();
267 }
268 result += " ]";
269 return result;
270}
271//----------------------------------------------------------------------
273 commas::comma com(c.size());
274 string result("( ");
275 for (const Literal& l : c) {
276 result += l.to_tptp_string();
277 string s = com();
278 if (s == string(", "))
279 s = string(" | ");
280 result += s;
281 }
282 result += " )";
283 return result;
284}
285//----------------------------------------------------------------------
286string Clause::make_LaTeX(bool subbed) const {
287 commas::comma com(c.size());
288 string s ("\\textcolor{blue}{\\{} ");
289 for (const Literal& l : c) {
290 s += l.make_LaTeX(subbed);
291 s += com();
292 }
293 s += "\\textcolor{blue}{\\}}";
294 return s;
295}
296//----------------------------------------------------------------------
297ostream& operator<<(ostream& out, const Clause& cl) {
298 out << "{ ";
299 size_t s = cl.c.size();
300 size_t i = 1;
301 for (const Literal& l : cl.c) {
302 out << l.to_string();
303 if (i < s)
304 out << " " << unicode_symbols::LogSym::or_sym << " ";
305 i++;
306 }
307 out << " }";
308 return out;
309}
Representation of clauses.
Definition Clause.hpp:52
Literal & operator[](size_t)
Direct read of the specified Literal.
Definition Clause.cpp:231
Literal extract_literal(LitNum)
Get rid of and return the specified Literal.
Definition Clause.cpp:189
bool has_complementary_literals() const
Check whether the clause contains complementary literals.
Definition Clause.cpp:74
string to_tptp_string() const
Convert to a string that is compatible with the TPTP.
Definition Clause.cpp:272
void random_reorder()
Randomly re-order the literals.
Definition Clause.cpp:239
void remove_duplicates()
Get rid of identical literals.
Definition Clause.cpp:54
static std::mt19937 d
Randomness for random reordering.
Definition Clause.hpp:61
Literal get_literal(LitNum) const
Get and return the specified Literal.
Definition Clause.cpp:213
string to_prolog_string() const
Convert to a string that can be read by Prolog.
Definition Clause.cpp:261
Clause make_copy_with_new_unique_vars(VariableIndex &, TermIndex &) const
Make a copy of an entire clause, introducing new variables.
Definition Clause.cpp:120
Clause make_copy_with_new_vars(VariableIndex &, TermIndex &) const
Make a copy of an entire clause, introducing new variables.
Definition Clause.cpp:107
vector< Literal > c
A Clause is just a vector of Literals.
Definition Clause.hpp:57
SimplificationResult simplify()
Simplify a clause by dealing with $true, $false, complementary literals, and duplicates.
Definition Clause.cpp:143
bool is_positive() const
A clause is positive if it has no negated literals.
Definition Clause.cpp:30
void add_lit(const Literal &)
Add a literal, making sure you don't duplicate.
Definition Clause.cpp:96
void reverse()
Reverse the order of the literals in the clause.
Definition Clause.cpp:253
bool is_negative() const
A clause is negative if it has only negated literals.
Definition Clause.cpp:42
string to_string(bool=false) const
Convert to a string.
Definition Clause.cpp:257
string make_LaTeX(bool=false) const
Convert the clause to a LaTeX representation.
Definition Clause.cpp:286
bool is_ground() const
Is this a ground clause?
Definition Clause.cpp:87
void drop_literal(LitNum)
Get rid of the specified Literal.
Definition Clause.cpp:168
Basic representation of literals, bundling together (pointers to) a Predicate, a collection of argume...
Definition Literal.hpp:50
string to_string(bool=false) const
Full conversion of Literal to string.
Definition Literal.cpp:176
void make_copy_with_new_vars_replace_helper(VariableIndex &, TermIndex &, unordered_map< Variable *, Term * > &)
Helper function for making copies with new variables.
Definition Literal.cpp:68
Look after terms, using hash consing to avoid storing copies of terms.
Definition TermIndex.hpp:54
Storage of named variables, and management of new, anonymous and unique variables.
Simple function object for putting commas in lists.