27std::mt19937
Clause::d(params::random_seed);
33 cerr <<
"Don't check an empty clause for positivity" << endl;
35 for (
size_t i = 0; i <
c.size(); i++) {
45 cerr <<
"Don't check an empty clause for negativity" << endl;
47 for (
size_t i = 0; i <
c.size(); i++) {
58 vector<Literal> new_c;
59 for (
size_t i = 0; i < s - 1; i++) {
61 for (
size_t j = i+1; j < s; j++ ) {
68 new_c.push_back(
c[i]);
70 new_c.push_back(
c[s - 1]);
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]))
97 for (
size_t i = 0; i <
c.size(); i++)
100 cerr <<
"Don't duplicate Literals in a clause!" << endl;
110 cerr <<
"You are making a copy of an empty clause" << endl;
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));
123 cerr <<
"You are making a copy of an empty clause" << endl;
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));
135 unordered_map<Variable*,Term*> new_vars;
139 for (
size_t i = 0; i < s; i++)
140 _c.
c[i].make_copy_with_new_vars_replace_helper(vi, ti, new_vars);
146 vector<Literal> new_clause;
147 bool clause_is_true =
false;
152 clause_is_true =
true;
155 new_clause.push_back(lit);
159 return SimplificationResult::Tautology;
162 return SimplificationResult::Contradiction;
164 return SimplificationResult::Tautology;
165 return SimplificationResult::OK;
171 cerr <<
"Can't drop_literal from empty clause" << endl;
175 if (l >
c.size() - 1) {
177 cerr <<
"drop_literal argument is out of range" << endl;
193 cerr <<
"Can't extract_literal from empty clause" << endl;
197 if (l >
c.size() - 1) {
199 cerr <<
"extract_literal argument is out of range" << endl;
217 cerr <<
"Can't extract_literal from empty clause" << endl;
221 if (l >
c.size() - 1) {
223 cerr <<
"extract_literal argument is out of range" << endl;
233 if (i >
c.size() - 1)
234 cerr <<
"You're out of range accessing a clause" << endl;
241 vector<size_t> new_order;
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);
247 vector<Literal> new_c =
c;
248 for (
size_t i = 0; i < s; i++) {
249 c[i] = new_c[new_order[i]];
254 std::reverse(
c.begin(),
c.end());
258 return vector_to_string(
c, subbed,
"{ ",
" }",
", ");
265 result += l.to_prolog_string();
276 result += l.to_tptp_string();
278 if (s ==
string(
", "))
288 string s (
"\\textcolor{blue}{\\{} ");
290 s += l.make_LaTeX(subbed);
293 s +=
"\\textcolor{blue}{\\}}";
297ostream& operator<<(ostream& out,
const Clause& cl) {
299 size_t s = cl.
c.size();
304 out <<
" " << unicode_symbols::LogSym::or_sym <<
" ";
Representation of clauses.
Literal & operator[](size_t)
Direct read of the specified Literal.
Literal extract_literal(LitNum)
Get rid of and return the specified Literal.
bool has_complementary_literals() const
Check whether the clause contains complementary literals.
string to_tptp_string() const
Convert to a string that is compatible with the TPTP.
void random_reorder()
Randomly re-order the literals.
void remove_duplicates()
Get rid of identical literals.
static std::mt19937 d
Randomness for random reordering.
Literal get_literal(LitNum) const
Get and return the specified Literal.
string to_prolog_string() const
Convert to a string that can be read by Prolog.
Clause make_copy_with_new_unique_vars(VariableIndex &, TermIndex &) const
Make a copy of an entire clause, introducing new variables.
Clause make_copy_with_new_vars(VariableIndex &, TermIndex &) const
Make a copy of an entire clause, introducing new variables.
vector< Literal > c
A Clause is just a vector of Literals.
SimplificationResult simplify()
Simplify a clause by dealing with $true, $false, complementary literals, and duplicates.
bool is_positive() const
A clause is positive if it has no negated literals.
void add_lit(const Literal &)
Add a literal, making sure you don't duplicate.
void reverse()
Reverse the order of the literals in the clause.
bool is_negative() const
A clause is negative if it has only negated literals.
string to_string(bool=false) const
Convert to a string.
string make_LaTeX(bool=false) const
Convert the clause to a LaTeX representation.
bool is_ground() const
Is this a ground clause?
void drop_literal(LitNum)
Get rid of the specified Literal.
Basic representation of literals, bundling together (pointers to) a Predicate, a collection of argume...
string to_string(bool=false) const
Full conversion of Literal to string.
void make_copy_with_new_vars_replace_helper(VariableIndex &, TermIndex &, unordered_map< Variable *, Term * > &)
Helper function for making copies with new variables.
Look after terms, using hash consing to avoid storing copies of terms.
Storage of named variables, and management of new, anonymous and unique variables.
Simple function object for putting commas in lists.