1
2 /*
3 * File FOOLParamodulation.cpp.
4 *
5 * This file is part of the source code of the software program
6 * Vampire. It is protected by applicable
7 * copyright laws.
8 *
9 * This source code is distributed under the licence found here
10 * https://vprover.github.io/license.html
11 * and in the source directory
12 *
13 * In summary, you are allowed to use Vampire for non-commercial
14 * purposes but not allowed to distribute, modify, copy, create derivatives,
15 * or use in competitions.
16 * For other uses of Vampire please contact developers for a different
17 * licence, which we will make an effort to provide.
18 */
19 /**
20 * @file FOOLParamodulation.cpp
21 * Implements the inference rule, that is needed for efficient treatment of
22 * boolean terms. The details of why it is needed are in the paper
23 * "A First Class Boolean Sort in First-Order Theorem Proving and TPTP"
24 * by Kotelnikov, Kovacs and Voronkov [1].
25 *
26 * [1] http://arxiv.org/abs/1505.01682
27 */
28
29 #include "Lib/Environment.hpp"
30
31 #include "Kernel/Clause.hpp"
32 #include "Kernel/EqHelper.hpp"
33 #include "Kernel/Inference.hpp"
34 #include "Kernel/Term.hpp"
35 #include "Kernel/TermIterators.hpp"
36 #include "Kernel/Signature.hpp"
37 #include "Kernel/Sorts.hpp"
38
39 #include "FOOLParamodulation.hpp"
40
41 namespace Inferences {
42
generateClauses(Clause * premise)43 ClauseIterator FOOLParamodulation::generateClauses(Clause* premise) {
44 CALL("FOOLParamodulation::generateClauses");
45
46 /**
47 * We are going to implement the following inference rule, taken from the paper:
48 *
49 * C[s]
50 * --------------------, where
51 * C[true] \/ s = false
52 *
53 * (a) s is a boolean term other than true or false;
54 * (b) s is not a variable;
55 * (c) C[s] is different from s = false.
56 *
57 * C[s] is a clause with an occurrence of s, and C[true] is the C clause
58 * with s substituted by true.
59 *
60 * C[s] is deleted after the inference is applied.
61 */
62
63 static TermList troo(Term::foolTrue());
64 static TermList fols(Term::foolFalse());
65
66 /**
67 * We will be looking for a literal, standing in a `literalPosition` in
68 * the clause, that has an occurrence of a `booleanTerm`, that is not a
69 * variable, true or false.
70 *
71 * We will only be looking for one boolean term and only replace one
72 * occurrence of it in one literal. An alternative implementation can:
73 * 1) Replace all occurrences of a boolean term in all literals.
74 * 2) Find occurrences of multiple boolean terms and replace their
75 * occurrences simultaneously, adding multiple literals of the form
76 * s_n = false to the conclusion.
77 */
78 TermList booleanTerm;
79 unsigned literalPosition = 0;
80
81 ArrayishObjectIterator<Clause> literals = premise->getSelectedLiteralIterator();
82 while (literals.hasNext()) {
83 Literal* literal = literals.next();
84
85 // we shouldn't touch literals of the form s = false
86 if (literal->isEquality() && literal->polarity()) {
87 TermList* lhs = literal->nthArgument(0);
88 TermList* rhs = literal->nthArgument(1);
89 if ((lhs->isTerm() && env.signature->isFoolConstantSymbol(false,lhs->term()->functor())) ||
90 (rhs->isTerm() && env.signature->isFoolConstantSymbol(false,rhs->term()->functor()))) {
91 literalPosition++;
92 continue;
93 }
94 }
95
96 // we shouldn't replace variables, hence NonVariableIterator
97 NonVariableIterator nvi(literal);
98 while (nvi.hasNext()) {
99 TermList subterm = nvi.next();
100 unsigned functor = subterm.term()->functor();
101
102 // we shouldn't replace boolean constants
103 if (env.signature->isFoolConstantSymbol(false,functor) || env.signature->isFoolConstantSymbol(true,functor)) {
104 continue;
105 }
106
107 unsigned resultType = env.signature->getFunction(functor)->fnType()->result();
108 if (resultType == Sorts::SRT_BOOL) {
109 booleanTerm = subterm;
110 goto substitution;
111 }
112 }
113 literalPosition++;
114 }
115
116 // If we reached this point, it means that there was no boolean terms we are
117 // interested in, so we don't infer anything
118 return ClauseIterator::getEmpty();
119
120 substitution:
121
122 // Found a boolean term! Create the C[true] \/ s = false clause
123 unsigned conclusionLength = premise->length() + 1;
124 Clause* conclusion = new(conclusionLength) Clause(conclusionLength,
125 GeneratingInference1(InferenceRule::FOOL_PARAMODULATION, premise));
126
127 // Copy the literals from the premise except for the one at `literalPosition`,
128 // that has the occurrence of `booleanTerm` replaced with false
129 for (unsigned i = 0; i < conclusion->length() - 1; i++) {
130 (*conclusion)[i] = i == literalPosition ? EqHelper::replace((*premise)[i], booleanTerm, troo) : (*premise)[i];
131 }
132
133 // Add s = false to the clause
134 (*conclusion)[conclusion->length() - 1] = Literal::createEquality(true, booleanTerm, fols, Sorts::SRT_BOOL);
135
136 return pvi(getSingletonIterator(conclusion));
137 }
138
139 }
140