1
2 /*
3 * File TheoryAxioms.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 TheoryAxioms.cpp
21 * Implements class TheoryAxioms.
22 */
23
24 #include "Lib/Environment.hpp"
25 #include "Lib/Stack.hpp"
26
27 #include "Kernel/Clause.hpp"
28 #include "Kernel/EqHelper.hpp"
29 #include "Kernel/Formula.hpp"
30 #include "Kernel/FormulaUnit.hpp"
31 #include "Kernel/Inference.hpp"
32 #include "Kernel/Problem.hpp"
33 #include "Kernel/Signature.hpp"
34 #include "Kernel/Sorts.hpp"
35 #include "Kernel/Term.hpp"
36 #include "Kernel/TermIterators.hpp"
37 #include "Kernel/Theory.hpp"
38
39 #include "Property.hpp"
40 #include "SymCounter.hpp"
41 #include "TheoryAxioms.hpp"
42 #include "Options.hpp"
43
44 using namespace Lib;
45 using namespace Kernel;
46 using namespace Shell;
47
48
49 /**
50 * Add the unit @c to @c problem and output it, if the option show_theory_axioms is on.
51 * @since 11/11/2013 Manchester
52 * @author Andrei Voronkov
53 */
addAndOutputTheoryUnit(Unit * unit,unsigned level)54 void TheoryAxioms::addAndOutputTheoryUnit(Unit* unit, unsigned level)
55 {
56 CALL("TheoryAxioms::addAndOutputTheoryUnit");
57
58 static Options::TheoryAxiomLevel opt_level = env.options->theoryAxioms();
59 // if the theory axioms are some or off (want this case for some things like fool) and the axiom is not
60 // a cheap one then don't add it
61 if(opt_level != Options::TheoryAxiomLevel::ON && level != CHEAP){ return; }
62
63 if (env.options->showTheoryAxioms()) {
64 Unit* qunit = unit;
65 Formula* f = 0;
66 if(unit->isClause()){
67 f = Formula::fromClause(static_cast<Clause*>(unit));
68 qunit = new FormulaUnit(f,unit->inference());
69 }
70 cout << "% Theory " << (unit->isClause() ? "clause" : "formula" ) << ": " << qunit->toString() << "\n";
71 if(f){ f->destroy(); }
72 }
73 if(!unit->isClause()){
74 _prb.reportFormulasAdded();
75 }
76 UnitList::push(unit, _prb.units());
77 } // addAndOutputTheoryUnit
78
79 /**
80 * Add the theory clause with literals @c lits to @c problem.
81 * @since 11/11/2013, Manchester: output of the clause added
82 * @author Andrei Voronkov
83 */
addTheoryClauseFromLits(std::initializer_list<Literal * > lits,InferenceRule rule,unsigned level)84 void TheoryAxioms::addTheoryClauseFromLits(std::initializer_list<Literal*> lits, InferenceRule rule, unsigned level)
85 {
86 CALL("TheoryAxioms::addTheoryClauseFromLits");
87 LiteralStack lit_stack;
88 for (Literal* lit : lits) {
89 ASS(lit);
90 lit_stack.push(lit);
91 }
92 Clause* cl = Clause::fromStack(lit_stack, TheoryAxiom(rule));
93 addAndOutputTheoryUnit(cl, level);
94 } // addTheoryClauseFromLits
95
96 /**
97 * Add the axiom f(X,Y)=f(Y,X).
98 * @since 11/11/2013, Manchester: modified
99 * @author Andrei Voronkov
100 */
addCommutativity(Interpretation op)101 void TheoryAxioms::addCommutativity(Interpretation op)
102 {
103 CALL("TheoryAxioms::addCommutativity");
104 ASS(theory->isFunction(op));
105 ASS_EQ(theory->getArity(op),2);
106
107 unsigned f = env.signature->getInterpretingSymbol(op);
108 unsigned srt = theory->getOperationSort(op);
109 TermList x(0,false);
110 TermList y(1,false);
111 TermList fxy(Term::create2(f,x,y));
112 TermList fyx(Term::create2(f,y,x));
113 Literal* eq = Literal::createEquality(true,fxy,fyx,srt);
114 addTheoryClauseFromLits({eq}, InferenceRule::THA_COMMUTATIVITY, EXPENSIVE);
115 } // addCommutativity
116
117 /**
118 * Add axiom f(X,f(Y,Z))=f(f(X,Y),Z).
119 * @since 11/11/2013, Manchester: modified
120 * @author Andrei Voronkov
121 */
addAssociativity(Interpretation op)122 void TheoryAxioms::addAssociativity(Interpretation op)
123 {
124 CALL("TheoryAxioms::addCommutativity");
125 ASS(theory->isFunction(op));
126 ASS_EQ(theory->getArity(op),2);
127
128 unsigned f = env.signature->getInterpretingSymbol(op);
129 unsigned srt = theory->getOperationSort(op);
130 TermList x(0,false);
131 TermList y(1,false);
132 TermList z(2,false);
133 TermList fxy(Term::create2(f,x,y));
134 TermList fyz(Term::create2(f,y,z));
135 TermList fx_fyz(Term::create2(f,x,fyz));
136 TermList f_fxy_z(Term::create2(f,fxy,z));
137 Literal* eq = Literal::createEquality(true, fx_fyz,f_fxy_z, srt);
138 addTheoryClauseFromLits({eq}, InferenceRule::THA_ASSOCIATIVITY, EXPENSIVE);
139 } // addAsssociativity
140
141
142 /**
143 * Add axiom f(X,e)=X.
144 * @since 11/11/2013, Manchester: modified
145 * @author Andrei Voronkov
146 */
addRightIdentity(Interpretation op,TermList e)147 void TheoryAxioms::addRightIdentity(Interpretation op, TermList e)
148 {
149 CALL("TheoryAxioms::addRightIdentity");
150 ASS(theory->isFunction(op));
151 ASS_EQ(theory->getArity(op),2);
152
153 unsigned f = env.signature->getInterpretingSymbol(op);
154 unsigned srt = theory->getOperationSort(op);
155 TermList x(0,false);
156 TermList fxe(Term::create2(f,x,e));
157 Literal* eq = Literal::createEquality(true,fxe,x,srt);
158 addTheoryClauseFromLits({eq}, InferenceRule::THA_RIGHT_IDENTINTY, EXPENSIVE);
159 } // addRightIdentity
160
161 /**
162 * Add axiom f(e,X)=X.
163 */
addLeftIdentity(Interpretation op,TermList e)164 void TheoryAxioms::addLeftIdentity(Interpretation op, TermList e)
165 {
166 CALL("TheoryAxioms::addLeftIdentity");
167 ASS(theory->isFunction(op));
168 ASS_EQ(theory->getArity(op),2);
169
170 unsigned f = env.signature->getInterpretingSymbol(op);
171 unsigned srt = theory->getOperationSort(op);
172 TermList x(0,false);
173 TermList fex(Term::create2(f,e,x));
174 Literal* eq = Literal::createEquality(true,fex,x,srt);
175 addTheoryClauseFromLits({eq}, InferenceRule::THA_LEFT_IDENTINTY, EXPENSIVE);
176 } // addLeftIdentity
177
178 /**
179 * Add axioms for commutative group with addition @c op, inverse @c inverse and unit @c e:
180 * <ol>
181 * <li>f(X,Y)=f(Y,X) (commutativity)</li>
182 * <li>f(X,f(Y,Z))=f(f(X,Y),Z) (associativity)</li>
183 * <li>f(X,e)=X (right identity)</li>
184 * <li>i(f(x,y)) = f(i(y),i(x))</li>
185 * <li>f(x,i(x))=e (right inverse)</li>
186 * </ol>
187 * @since 11/11/2013, Manchester: modified
188 * @author Andrei Voronkov
189 */
addCommutativeGroupAxioms(Interpretation op,Interpretation inverse,TermList e)190 void TheoryAxioms::addCommutativeGroupAxioms(Interpretation op, Interpretation inverse, TermList e)
191 {
192 CALL("TheoryAxioms::addCommutativeGroupAxioms");
193
194 ASS(theory->isFunction(op));
195 ASS_EQ(theory->getArity(op),2);
196 ASS(theory->isFunction(inverse));
197 ASS_EQ(theory->getArity(inverse),1);
198
199 addCommutativity(op);
200 addAssociativity(op);
201 addRightIdentity(op,e);
202
203 // i(f(x,y)) = f(i(y),i(x))
204 unsigned f = env.signature->getInterpretingSymbol(op);
205 unsigned i = env.signature->getInterpretingSymbol(inverse);
206 unsigned srt = theory->getOperationSort(op);
207 ASS_EQ(srt, theory->getOperationSort(inverse));
208
209 TermList x(0,false);
210 TermList y(1,false);
211 TermList fxy(Term::create2(f,x,y));
212 TermList ix(Term::create1(i,x));
213 TermList iy(Term::create1(i,y));
214 TermList i_fxy(Term::create1(i,fxy));
215 TermList f_iy_ix(Term::create2(f,iy,ix));
216 Literal* eq1 = Literal::createEquality(true,i_fxy,f_iy_ix,srt);
217 addTheoryClauseFromLits({eq1}, InferenceRule::THA_INVERSE_OP_OP_INVERSES, EXPENSIVE);
218
219 // f(x,i(x))=e
220 TermList fx_ix(Term::create2(f,x,ix));
221 Literal* eq2 = Literal::createEquality(true,fx_ix,e,srt);
222 addTheoryClauseFromLits({eq2}, InferenceRule::THA_INVERSE_OP_UNIT, EXPENSIVE);
223 } // TheoryAxioms::addCommutativeGroupAxioms
224
225 /**
226 * Add axiom op(op(x,i(y)),y) = x
227 * e.g. (x+(-y))+y = x
228 */
addRightInverse(Interpretation op,Interpretation inverse)229 void TheoryAxioms::addRightInverse(Interpretation op, Interpretation inverse)
230 {
231 TermList x(0,false);
232 TermList y(0,false);
233 unsigned f = env.signature->getInterpretingSymbol(op);
234 unsigned i = env.signature->getInterpretingSymbol(inverse);
235 unsigned srt = theory->getOperationSort(op);
236 ASS_EQ(srt, theory->getOperationSort(inverse));
237
238 TermList iy(Term::create1(i,y));
239 TermList xiy(Term::create2(f,x,iy));
240 TermList xiyy(Term::create2(f,xiy,y));
241 Literal* eq = Literal::createEquality(true,xiyy,x,srt);
242 addTheoryClauseFromLits({eq}, InferenceRule::THA_INVERSE_ASSOC, EXPENSIVE);
243 }
244
245 /**
246 * Add axiom ~op(X,X)
247 */
addNonReflexivity(Interpretation op)248 void TheoryAxioms::addNonReflexivity(Interpretation op)
249 {
250 CALL("TheoryAxioms::addNonReflexivity");
251
252 ASS(!theory->isFunction(op));
253 ASS_EQ(theory->getArity(op),2);
254
255 unsigned opPred = env.signature->getInterpretingSymbol(op);
256 TermList x(0,false);
257 Literal* l11 = Literal::create2(opPred, false, x, x);
258 addTheoryClauseFromLits({l11}, InferenceRule::THA_NONREFLEX, CHEAP);
259 } // addNonReflexivity
260
261 /**
262 * Add axiom ~op(X,Y) | ~op(Y,Z) | op(X,Z)
263 */
addTransitivity(Interpretation op)264 void TheoryAxioms::addTransitivity(Interpretation op)
265 {
266 CALL("TheoryAxioms::addTransitivity");
267 ASS(!theory->isFunction(op));
268 ASS_EQ(theory->getArity(op),2);
269
270 unsigned opPred = env.signature->getInterpretingSymbol(op);
271 TermList x(0,false);
272 TermList y(1,false);
273 TermList v3(2,false);
274
275 Literal* nonL12 = Literal::create2(opPred, false, x, y);
276 Literal* nonL23 = Literal::create2(opPred, false, y, v3);
277 Literal* l13 = Literal::create2(opPred, true, x, v3);
278
279 addTheoryClauseFromLits({nonL12,nonL23,l13}, InferenceRule::THA_TRANSITIVITY, CHEAP);
280 }
281
282 /**
283 * Add axiom less(X,Y) | less(Y,X) | X=Y
284 */
addOrderingTotality(Interpretation less)285 void TheoryAxioms::addOrderingTotality(Interpretation less)
286 {
287 CALL("TheoryAxioms::addOrderingTotality");
288 ASS(!theory->isFunction(less));
289 ASS_EQ(theory->getArity(less),2);
290
291 unsigned opPred = env.signature->getInterpretingSymbol(less);
292 TermList x(0,false);
293 TermList y(1,false);
294
295 Literal* l12 = Literal::create2(opPred, true, x, y);
296 Literal* l21 = Literal::create2(opPred, true, y, x);
297
298 unsigned srt = theory->getOperationSort(less);
299 Literal* eq = Literal::createEquality(true,x,y,srt);
300
301 addTheoryClauseFromLits({l12,l21,eq}, InferenceRule::THA_ORDER_TOTALALITY, CHEAP);
302 }
303
304 /**
305 * Add axioms of reflexivity, transitivity and total ordering for predicate @c less
306 */
addTotalOrderAxioms(Interpretation less)307 void TheoryAxioms::addTotalOrderAxioms(Interpretation less)
308 {
309 CALL("TheoryAxioms::addTotalOrderAxioms");
310
311 addNonReflexivity(less);
312 addTransitivity(less);
313 addOrderingTotality(less);
314 }
315
316 /**
317 * Add axiom ~less(X,Y) | less(X+Z,Y+Z)
318 */
addMonotonicity(Interpretation less,Interpretation addition)319 void TheoryAxioms::addMonotonicity(Interpretation less, Interpretation addition)
320 {
321 CALL("TheoryAxioms::addMonotonicity");
322 ASS(!theory->isFunction(less));
323 ASS_EQ(theory->getArity(less),2);
324 ASS(theory->isFunction(addition));
325 ASS_EQ(theory->getArity(addition),2);
326
327 unsigned lessPred = env.signature->getInterpretingSymbol(less);
328 unsigned addFun = env.signature->getInterpretingSymbol(addition);
329 TermList x(0,false);
330 TermList y(1,false);
331 TermList v3(2,false);
332 TermList xPv3(Term::create2(addFun, x,v3));
333 TermList yPv3(Term::create2(addFun, y,v3));
334 Literal* nonLe = Literal::create2(lessPred, false, x, y);
335 Literal* leAdded = Literal::create2(lessPred, true, xPv3, yPv3);
336
337 addTheoryClauseFromLits({nonLe,leAdded}, InferenceRule::THA_ORDER_MONOTONICITY, EXPENSIVE);
338 }
339
340 /**
341 * Add the axiom $less(X,$sum(X,1))
342 *
343 * Taken from SPASS+T work
344 */
addPlusOneGreater(Interpretation plus,TermList oneElement,Interpretation less)345 void TheoryAxioms::addPlusOneGreater(Interpretation plus, TermList oneElement,
346 Interpretation less)
347 {
348 CALL("TheoryAxioms::addPlusOneGreater");
349 ASS(!theory->isFunction(less));
350 ASS_EQ(theory->getArity(less),2);
351 ASS(theory->isFunction(plus));
352 ASS_EQ(theory->getArity(plus),2);
353
354 unsigned lessPred = env.signature->getInterpretingSymbol(less);
355 unsigned addFun = env.signature->getInterpretingSymbol(plus);
356 TermList x(0,false);
357
358 TermList xPo(Term::create2(addFun,x,oneElement));
359 Literal* xPo_g_x = Literal::create2(lessPred,true,x,xPo);
360 addTheoryClauseFromLits({xPo_g_x}, InferenceRule::THA_PLUS_ONE_GREATER, CHEAP);
361 }
362
363 /**
364 * Add axioms for addition, unary minus and ordering
365 */
addAdditionAndOrderingAxioms(Interpretation plus,Interpretation unaryMinus,TermList zeroElement,TermList oneElement,Interpretation less)366 void TheoryAxioms::addAdditionAndOrderingAxioms(Interpretation plus, Interpretation unaryMinus,
367 TermList zeroElement, TermList oneElement, Interpretation less)
368 {
369 CALL("TheoryAxioms::addAdditionAndOrderingAxioms");
370
371 addCommutativeGroupAxioms(plus, unaryMinus, zeroElement);
372 addTotalOrderAxioms(less);
373 addMonotonicity(less, plus);
374
375 // y < x+one | x<y
376 unsigned plusFun = env.signature->getInterpretingSymbol(plus);
377 unsigned lessPred = env.signature->getInterpretingSymbol(less);
378 TermList x(0,false);
379 TermList y(1,false);
380 Literal* xLy = Literal::create2(lessPred,true,x,y);
381 TermList xP(Term::create2(plusFun,x,oneElement));
382 Literal* yLxP = Literal::create2(lessPred,true,y,xP);
383
384 addTheoryClauseFromLits({xLy,yLxP}, InferenceRule::THA_ORDER_PLUS_ONE_DICHOTOMY, EXPENSIVE);
385
386 // add that --x = x
387 unsigned varSort = theory->getOperationSort(unaryMinus);
388 unsigned unaryMinusFun = env.signature->getInterpretingSymbol(unaryMinus);
389 TermList mx(Term::create1(unaryMinusFun,x));
390 TermList mmx(Term::create1(unaryMinusFun,mx));
391 Literal* mmxEqx = Literal::createEquality(true,mmx,x,varSort);
392 addTheoryClauseFromLits({mmxEqx}, InferenceRule::THA_MINUS_MINUS_X, EXPENSIVE);
393 }
394
395 /**
396 * Add axioms for addition, multiplication, unary minus and ordering
397 */
addAdditionOrderingAndMultiplicationAxioms(Interpretation plus,Interpretation unaryMinus,TermList zeroElement,TermList oneElement,Interpretation less,Interpretation multiply)398 void TheoryAxioms::addAdditionOrderingAndMultiplicationAxioms(Interpretation plus, Interpretation unaryMinus,
399 TermList zeroElement, TermList oneElement, Interpretation less, Interpretation multiply)
400 {
401 CALL("TheoryAxioms::addAdditionOrderingAndMultiplicationAxioms");
402
403 unsigned srt = theory->getOperationSort(plus);
404 ASS_EQ(srt, theory->getOperationSort(unaryMinus));
405 ASS_EQ(srt, theory->getOperationSort(less));
406 ASS_EQ(srt, theory->getOperationSort(multiply));
407
408 addAdditionAndOrderingAxioms(plus, unaryMinus, zeroElement, oneElement, less);
409
410 addCommutativity(multiply);
411 addAssociativity(multiply);
412 addRightIdentity(multiply, oneElement);
413
414 //axiom( X0*zero==zero );
415 unsigned mulFun = env.signature->getInterpretingSymbol(multiply);
416 TermList x(0,false);
417 TermList xMulZero(Term::create2(mulFun, x, zeroElement));
418 Literal* xEqXMulZero = Literal::createEquality(true, xMulZero, zeroElement, srt);
419 addTheoryClauseFromLits({xEqXMulZero}, InferenceRule::THA_TIMES_ZERO, EXPENSIVE);
420
421 // Distributivity
422 //axiom x*(y+z) = (x*y)+(x*z)
423
424 unsigned plusFun = env.signature->getInterpretingSymbol(plus);
425 TermList y(1,false);
426 TermList z(2,false);
427
428 TermList yPz(Term::create2(plusFun,y,z));
429 TermList xTyPz(Term::create2(mulFun,x,yPz));
430
431 TermList xTy(Term::create2(mulFun,x,y));
432 TermList xTz(Term::create2(mulFun,x,z));
433 TermList xTyPxTz(Term::create2(plusFun,xTy,xTz));
434
435 Literal* distrib = Literal::createEquality(true, xTyPz, xTyPxTz,srt);
436 addTheoryClauseFromLits({distrib}, InferenceRule::THA_DISTRIBUTIVITY, EXPENSIVE);
437
438 // Divisibility
439 // (x != 0 & x times z = y & x times w = y) -> z = w
440 // x=0 | x*z != y | x*w != y | z=w
441 TermList w(3,false);
442 Literal* xEz = Literal::createEquality(true,x,zeroElement,srt);
443 TermList xTw(Term::create2(mulFun,x,w));
444 Literal* xTznEy = Literal::createEquality(false,xTz,y,srt);
445 Literal* xTwnEy = Literal::createEquality(false,xTw,y,srt);
446 Literal* zEw = Literal::createEquality(true,z,w,srt);
447
448 addTheoryClauseFromLits({xEz,xTznEy,xTwnEy,zEw}, InferenceRule::THA_DIVISIBILITY, EXPENSIVE);
449 }
450
451 /**
452 * Add axioms for integer division
453 * Also modulo and abs functions
454 */
addIntegerDivisionWithModuloAxioms(Interpretation plus,Interpretation unaryMinus,Interpretation less,Interpretation multiply,Interpretation divide,Interpretation divides,Interpretation modulo,Interpretation abs,TermList zeroElement,TermList oneElement)455 void TheoryAxioms::addIntegerDivisionWithModuloAxioms(Interpretation plus, Interpretation unaryMinus, Interpretation less,
456 Interpretation multiply, Interpretation divide, Interpretation divides,
457 Interpretation modulo, Interpretation abs, TermList zeroElement,
458 TermList oneElement)
459 {
460 CALL("TheoryAxioms::addIntegerDivisionWithModuloAxioms");
461
462
463 unsigned srt = theory->getOperationSort(plus);
464 ASS_EQ(srt, theory->getOperationSort(unaryMinus));
465 ASS_EQ(srt, theory->getOperationSort(less));
466 ASS_EQ(srt, theory->getOperationSort(multiply));
467 ASS_EQ(srt, theory->getOperationSort(divide));
468 ASS_EQ(srt, theory->getOperationSort(divides));
469 ASS_EQ(srt, theory->getOperationSort(modulo));
470 ASS_EQ(srt, theory->getOperationSort(abs));
471
472 unsigned lessPred = env.signature->getInterpretingSymbol(less);
473 unsigned umFun = env.signature->getInterpretingSymbol(unaryMinus);
474 unsigned mulFun = env.signature->getInterpretingSymbol(multiply);
475 unsigned divFun = env.signature->getInterpretingSymbol(divide);
476 unsigned modFun = env.signature->getInterpretingSymbol(modulo);
477 unsigned absFun = env.signature->getInterpretingSymbol(abs);
478 unsigned plusFun = env.signature->getInterpretingSymbol(plus);
479
480 addIntegerAbsAxioms(abs,less,unaryMinus,zeroElement);
481
482 TermList x(1,false);
483 TermList y(2,false);
484
485 // divides
486 //TODO
487
488 Literal* yis0 = Literal::createEquality(true,y,zeroElement,srt);
489 TermList modxy(Term::create2(modFun,x,y));
490
491 //y!=0 => x = modulo(x,y) + multiply(y,div(x,y))
492
493 TermList divxy(Term::create2(divFun,x,y));
494 TermList mulydivxy(Term::create2(mulFun,y,divxy));
495 TermList sum(Term::create2(plusFun,modxy,mulydivxy));
496 Literal* xeqsum = Literal::createEquality(true,x,sum,srt);
497 addTheoryClauseFromLits({yis0,xeqsum}, InferenceRule::THA_MODULO_MULTIPLY, EXPENSIVE);
498
499 // y!=0 => (0 <= mod(x,y))
500 // y=0 | ~(mod(x,y) < 0)
501 Literal* modxyge0 = Literal::create2(lessPred,false,modxy,zeroElement);
502 addTheoryClauseFromLits({yis0,modxyge0}, InferenceRule::THA_MODULO_POSITIVE, EXPENSIVE);
503
504 // y!=0 => (mod(x,y) <= abs(y)-1)
505 // y=0 | ~( abs(y)-1 < mod(x,y) )
506 TermList absy(Term::create1(absFun,y));
507 TermList m1(Term::create1(umFun,oneElement));
508 TermList absym1(Term::create2(plusFun,absy,m1));
509 Literal* modxyleabsym1 = Literal::create2(lessPred,false,absym1,modxy);
510 addTheoryClauseFromLits({yis0,modxyleabsym1}, InferenceRule::THA_MODULO_SMALL, EXPENSIVE);
511 }
512
addIntegerDividesAxioms(Interpretation divides,Interpretation multiply,TermList zero,TermList n)513 void TheoryAxioms::addIntegerDividesAxioms(Interpretation divides, Interpretation multiply, TermList zero, TermList n)
514 {
515 CALL("TheoryAxioms::addIntegerDividesAxioms");
516
517 #if VDEBUG
518 // ASSERT n>0
519 ASS(theory->isInterpretedConstant(n));
520 IntegerConstantType nc;
521 ALWAYS(theory->tryInterpretConstant(n,nc));
522 ASS(nc.toInner()>0);
523 #endif
524
525 // ![Y] : (divides(n,Y) <=> ?[Z] : multiply(Z,n) = Y)
526
527 unsigned srt = theory->getOperationSort(divides);
528 ASS_EQ(srt, theory->getOperationSort(multiply));
529
530 unsigned divsPred = env.signature->getInterpretingSymbol(divides);
531 unsigned mulFun = env.signature->getInterpretingSymbol(multiply);
532
533 TermList y(1,false);
534 TermList z(2,false);
535
536 // divides(n,Y) | multiply(Z,n) != Y
537 Literal* divsXY = Literal::create2(divsPred,true,n,y);
538 TermList mZX(Term::create2(mulFun,z,n));
539 Literal* mZXneY = Literal::createEquality(false,mZX,y,srt);
540 addTheoryClauseFromLits({divsXY,mZXneY}, InferenceRule::THA_DIVIDES_MULTIPLY, EXPENSIVE);
541
542 // ~divides(n,Y) | multiply(skolem(n,Y),n)=Y
543 Literal* ndivsXY = Literal::create2(divsPred,false,n,y);
544
545 // create a skolem function with signature srt*srt>srt
546 unsigned skolem = env.signature->addSkolemFunction(2);
547 Signature::Symbol* sym = env.signature->getFunction(skolem);
548 sym->setType(OperatorType::getFunctionType({srt,srt},srt));
549 TermList skXY(Term::create2(skolem,n,y));
550 TermList msxX(Term::create2(mulFun,skXY,n));
551 Literal* msxXeqY = Literal::createEquality(true,msxX,y,srt);
552
553 addTheoryClauseFromLits({ndivsXY,msxXeqY}, InferenceRule::THA_NONDIVIDES_SKOLEM, EXPENSIVE);
554 }
555
addIntegerAbsAxioms(Interpretation abs,Interpretation less,Interpretation unaryMinus,TermList zeroElement)556 void TheoryAxioms::addIntegerAbsAxioms(Interpretation abs, Interpretation less,
557 Interpretation unaryMinus, TermList zeroElement)
558 {
559 CALL("TheoryAxioms::addIntegerAbsAxioms");
560
561 unsigned srt = theory->getOperationSort(abs);
562 ASS_EQ(srt, theory->getOperationSort(less));
563 ASS_EQ(srt, theory->getOperationSort(unaryMinus));
564
565 unsigned lessPred = env.signature->getInterpretingSymbol(less);
566 unsigned absFun = env.signature->getInterpretingSymbol(abs);
567 unsigned umFun = env.signature->getInterpretingSymbol(unaryMinus);
568
569 TermList x(1,false);
570 TermList absX(Term::create1(absFun,x));
571 TermList mx(Term::create1(umFun,x));
572 TermList absmX(Term::create1(absFun,mx));
573
574 // If x is positive then abs(x)=x
575 // If x is negative then abs(x)=-x
576
577 Literal* xNeg = Literal::create2(lessPred,false,zeroElement,x); // not 0<x
578 Literal* xPos = Literal::create2(lessPred,false,x,zeroElement); // not x<0
579
580 Literal* absXeqX = Literal::createEquality(true,absX,x,srt);
581 Literal* absXeqmX = Literal::createEquality(true,absX,mx,srt);
582
583 addTheoryClauseFromLits({xNeg,absXeqX}, InferenceRule::THA_ABS_EQUALS, EXPENSIVE);
584 addTheoryClauseFromLits({xPos,absXeqmX}, InferenceRule::THA_ABS_MINUS_EQUALS, EXPENSIVE);
585 }
586
587
588 /**
589 * Add axioms for quotient i.e. rat or real division
590 */
addQuotientAxioms(Interpretation quotient,Interpretation multiply,TermList zeroElement,TermList oneElement,Interpretation less)591 void TheoryAxioms::addQuotientAxioms(Interpretation quotient, Interpretation multiply,
592 TermList zeroElement, TermList oneElement, Interpretation less)
593 {
594 CALL("TheoryAxioms::addQuotientAxioms");
595
596 unsigned srt = theory->getOperationSort(quotient);
597 ASS_EQ(srt, theory->getOperationSort(multiply));
598 ASS_EQ(srt, theory->getOperationSort(less));
599
600 TermList x(1,false);
601 TermList y(2,false);
602
603 unsigned mulFun = env.signature->getInterpretingSymbol(multiply);
604 unsigned divFun = env.signature->getInterpretingSymbol(quotient);
605
606 Literal* guardx = Literal::createEquality(true,x,zeroElement,srt);
607
608 // x=0 | quotient(x,x)=1, easily derivable!
609 //TermList qXX(Term::create2(quotient,x,x));
610 //Literal* xQxis1 = Literal::createEquality(true,qXX,oneElement,srt);
611 //addTheoryNonUnitClause(guardx,xQxis1);
612
613 // x=0 | quotient(1,x)!=0
614 TermList q1X(Term::create2(divFun,oneElement,x));
615 Literal* oQxnot0 = Literal::createEquality(false,q1X,zeroElement,srt);
616 addTheoryClauseFromLits({guardx,oQxnot0}, InferenceRule::THA_QUOTIENT_NON_ZERO, EXPENSIVE);
617
618 // quotient(x,1)=x, easily derivable!
619 //TermList qX1(Term::create2(quotient,x,oneElement));
620 //Literal* qx1isx = Literal::createEquality(true,qX1,x,srt);
621 //addTheoryUnitClause(qx1isx);
622
623 // x=0 | quotient(multiply(y,x),x)=y
624 TermList myx(Term::create2(mulFun,y,x));
625 TermList qmx(Term::create2(divFun,myx,x));
626 Literal* qmxisy = Literal::createEquality(true,qmx,y,srt);
627
628 addTheoryClauseFromLits({guardx,qmxisy}, InferenceRule::THA_QUOTIENT_MULTIPLY, EXPENSIVE);
629 }
630
631 /**
632 * Add axiom valid only for integer ordering: Y>X -> Y => X+1
633 *
634 * ~(x<y) | ~(y,x+1)
635 */
addExtraIntegerOrderingAxiom(Interpretation plus,TermList oneElement,Interpretation less)636 void TheoryAxioms::addExtraIntegerOrderingAxiom(Interpretation plus, TermList oneElement,
637 Interpretation less)
638 {
639 CALL("TheoryAxioms::addExtraIntegerOrderingAxiom");
640
641 unsigned lessPred = env.signature->getInterpretingSymbol(less);
642 unsigned plusFun = env.signature->getInterpretingSymbol(plus);
643 TermList x(0,false);
644 TermList y(1,false);
645 Literal* nxLy = Literal::create2(lessPred, false, x, y);
646 TermList xPOne(Term::create2(plusFun, x, oneElement));
647 Literal* nyLxPOne = Literal::create2(lessPred, false, y,xPOne);
648
649 addTheoryClauseFromLits({nxLy,nyLxPOne}, InferenceRule::THA_EXTRA_INTEGER_ORDERING, EXPENSIVE);
650 }
651
652 /**
653 * Add axioms defining floor function
654 * @author Giles
655 */
addFloorAxioms(Interpretation floor,Interpretation less,Interpretation unaryMinus,Interpretation plus,TermList oneElement)656 void TheoryAxioms::addFloorAxioms(Interpretation floor, Interpretation less, Interpretation unaryMinus,
657 Interpretation plus, TermList oneElement)
658 {
659 CALL("TheoryAxioms::addFloorAxioms");
660
661 unsigned lessPred = env.signature->getInterpretingSymbol(less);
662 unsigned plusFun = env.signature->getInterpretingSymbol(plus);
663 unsigned umFun = env.signature->getInterpretingSymbol(unaryMinus);
664 unsigned floorFun = env.signature->getInterpretingSymbol(floor);
665 TermList x(0,false);
666 TermList floorX(Term::create1(floorFun,x));
667
668 //axiom( floor(X) <= X )
669 // is ~(X < floor(X))
670 Literal* a1 = Literal::create2(lessPred, false, x, floorX);
671 addTheoryClauseFromLits({a1}, InferenceRule::THA_FLOOR_SMALL, EXPENSIVE);
672
673 //axiom( X-1 < floor(X) )
674 TermList m1(Term::create1(umFun,oneElement));
675 TermList xm1(Term::create2(plusFun, x, m1));
676 Literal* a2 = Literal::create2(lessPred,true, xm1, floorX);
677
678 addTheoryClauseFromLits({a2}, InferenceRule::THA_FLOOR_BIG, EXPENSIVE);
679 } //addFloorAxioms
680
681 /**
682 * Add axioms defining ceiling function
683 * @author Giles
684 */
addCeilingAxioms(Interpretation ceiling,Interpretation less,Interpretation plus,TermList oneElement)685 void TheoryAxioms::addCeilingAxioms(Interpretation ceiling, Interpretation less,
686 Interpretation plus, TermList oneElement)
687 {
688 CALL("TheoryAxioms::addCeilingAxioms");
689
690 unsigned lessPred = env.signature->getInterpretingSymbol(less);
691 unsigned plusFun = env.signature->getInterpretingSymbol(plus);
692 unsigned ceilingFun = env.signature->getInterpretingSymbol(ceiling);
693 TermList x(0,false);
694 TermList ceilingX(Term::create1(ceilingFun,x));
695
696 //axiom( ceiling(X) >= X )
697 // is ~( ceiling(X) < X )
698 Literal* a1 = Literal::create2(lessPred, false, ceilingX, x);
699 addTheoryClauseFromLits({a1}, InferenceRule::THA_CEILING_BIG, EXPENSIVE);
700
701 //axiom( ceiling(X) < X+1 )
702 TermList xp1(Term::create2(plusFun, x, oneElement));
703 Literal* a2 = Literal::create2(lessPred,true, ceilingX, xp1);
704 addTheoryClauseFromLits({a2}, InferenceRule::THA_CEILING_SMALL, EXPENSIVE);
705 } //addCeilingAxioms
706
707 /**
708 * Add axioms defining round function
709 * @author Giles
710 */
addRoundAxioms(Interpretation round,Interpretation floor,Interpretation ceiling)711 void TheoryAxioms::addRoundAxioms(Interpretation round, Interpretation floor, Interpretation ceiling)
712 {
713 CALL("TheoryAxioms::addRoundAxioms");
714
715 //TODO... not that interesting as $round not in TPTP or translations
716 // Suggested axioms:
717 // round(x) = floor(x) | round(x) = ceiling(x)
718 // x-0.5 > floor(x) => round(x) = ceiling(x)
719 // x+0.5 < ceiling(x) => round(x) = floor(x)
720 // x-0.5 = floor(x) => ?y : is_int(y) & 2*y = round(x)
721 // x+0.5 = ceiling(x) => ?y : is_int(y) & 2*y = round(x)
722 //NOT_IMPLEMENTED;
723
724 } //addRoundAxioms
725
726 /**
727 * Add axioms defining truncate function
728 * truncate is 'towards zero'
729 *
730 * >> x positive
731 * x<0 | ~( x < tr(x) ) // x-1 < tr(x) <= x
732 * x<0 | x-1 < tr(x)
733 *
734 * >> x negative
735 * ~(x<0) | ~( tr(x) < x ) // x <= tr(x) < x+1
736 * ~(x<0) | tr(x) < x+1
737 *
738 * @author Giles
739 */
addTruncateAxioms(Interpretation truncate,Interpretation less,Interpretation unaryMinus,Interpretation plus,TermList zeroElement,TermList oneElement)740 void TheoryAxioms::addTruncateAxioms(Interpretation truncate, Interpretation less, Interpretation unaryMinus,
741 Interpretation plus, TermList zeroElement, TermList oneElement)
742 {
743 CALL("TheoryAxioms::addTruncateAxioms");
744
745 unsigned lessPred = env.signature->getInterpretingSymbol(less);
746 unsigned plusFun = env.signature->getInterpretingSymbol(plus);
747 unsigned umFun = env.signature->getInterpretingSymbol(unaryMinus);
748 unsigned truncateFun = env.signature->getInterpretingSymbol(truncate);
749 TermList x(0,false);
750 TermList truncateX(Term::create1(truncateFun,x));
751
752 TermList m1(Term::create1(umFun,oneElement));
753 TermList xm1(Term::create2(plusFun,x,m1));
754 TermList xp1(Term::create2(plusFun,x,oneElement));
755
756 Literal* xLz = Literal::create2(lessPred,true,x,zeroElement);
757 Literal* nxLz= Literal::create2(lessPred,false,x,zeroElement);
758
759 //x<0 | ~( x < tr(x) )
760 Literal* a1 = Literal::create2(lessPred,false,x,truncateX);
761 addTheoryClauseFromLits({xLz,a1}, InferenceRule::THA_TRUNC1, EXPENSIVE);
762
763 //x<0 | x-1 < tr(x)
764 Literal* a2 = Literal::create2(lessPred,true,xm1,truncateX);
765 addTheoryClauseFromLits({xLz,a2}, InferenceRule::THA_TRUNC2, EXPENSIVE);
766
767 // ~(x<0) | ~( tr(x) < x )
768 Literal* a3 = Literal::create2(lessPred,false,truncateX,x);
769 addTheoryClauseFromLits({nxLz,a3}, InferenceRule::THA_TRUNC3, EXPENSIVE);
770
771 // ~(x<0) | tr(x) < x+1
772 Literal* a4 = Literal::create2(lessPred,true,truncateX,xp1);
773 addTheoryClauseFromLits({nxLz,a4}, InferenceRule::THA_TRUNC4, EXPENSIVE);
774 } //addTruncateAxioms
775
776 /**
777 * Adds the extensionality axiom of arrays (of type array1 or array2):
778 * select(X,sk(X,Y)) != select(Y,sk(X,Y)) | X = Y
779 *
780 * @author Laura Kovacs
781 * @since 31/08/2012, Vienna
782 * @since 11/11/2013 Manchester, updates
783 * @author Andrei Voronkov
784 * @since 05/01/2014 Vienna, add axiom in clause form (we need skolem function in other places)
785 * @author Bernhard Kragl
786 */
addArrayExtensionalityAxioms(unsigned arraySort,unsigned skolemFn)787 void TheoryAxioms::addArrayExtensionalityAxioms(unsigned arraySort, unsigned skolemFn)
788 {
789 CALL("TheoryAxioms::addArrayExtenstionalityAxioms");
790
791 unsigned sel = env.signature->getInterpretingSymbol(Theory::ARRAY_SELECT,Theory::getArrayOperatorType(arraySort,Theory::ARRAY_SELECT));
792
793 Sorts::ArraySort* si = env.sorts->getArraySort(arraySort);
794 unsigned rangeSort = si->getInnerSort();
795
796 TermList x(0,false);
797 TermList y(1,false);
798
799 TermList sk(Term::create2(skolemFn, x, y)); //sk(x,y)
800 TermList sel_x_sk(Term::create2(sel,x,sk)); //select(x,sk(x,y))
801 TermList sel_y_sk(Term::create2(sel,y,sk)); //select(y,sk(x,y))
802 Literal* eq = Literal::createEquality(true,x,y,arraySort); //x = y
803 Literal* ineq = Literal::createEquality(false,sel_x_sk,sel_y_sk,rangeSort); //select(x,sk(x,y) != select(y,z)
804
805 addTheoryClauseFromLits({eq,ineq}, InferenceRule::THA_ARRAY_EXTENSIONALITY, CHEAP);
806 } // addArrayExtensionalityAxiom
807
808 /**
809 * Adds the extensionality axiom of boolean arrays:
810 * select(X, sk(X, Y)) <~> select(Y, sk(X, Y)) | X = Y
811 *
812 * @since 25/08/2015 Gothenburg
813 * @author Evgeny Kotelnikov
814 */
addBooleanArrayExtensionalityAxioms(unsigned arraySort,unsigned skolemFn)815 void TheoryAxioms::addBooleanArrayExtensionalityAxioms(unsigned arraySort, unsigned skolemFn)
816 {
817 CALL("TheoryAxioms::addBooleanArrayExtenstionalityAxioms");
818
819 OperatorType* selectType = Theory::getArrayOperatorType(arraySort,Theory::ARRAY_BOOL_SELECT);
820
821 unsigned sel = env.signature->getInterpretingSymbol(Theory::ARRAY_BOOL_SELECT,selectType);
822
823 TermList x(0,false);
824 TermList y(1,false);
825
826 TermList sk(Term::create2(skolemFn, x, y)); //sk(x,y)
827 Formula* x_neq_y = new AtomicFormula(Literal::createEquality(false,x,y,arraySort)); //x != y
828
829 Formula* sel_x_sk = new AtomicFormula(Literal::create2(sel, true, x, sk)); //select(x,sk(x,y))
830 Formula* sel_y_sk = new AtomicFormula(Literal::create2(sel, true, y, sk)); //select(y,sk(x,y))
831 Formula* sx_neq_sy = new BinaryFormula(XOR, sel_x_sk, sel_y_sk); //select(x,sk(x,y)) <~> select(y,sk(x,y))
832
833 Formula* axiom = new QuantifiedFormula(FORALL, new Formula::VarList(0, new Formula::VarList(1, 0)),
834 new Formula::SortList(arraySort, new Formula::SortList(arraySort,0)),
835 new BinaryFormula(IMP, x_neq_y, sx_neq_sy));
836
837 addAndOutputTheoryUnit(new FormulaUnit(axiom, TheoryAxiom(InferenceRule::THA_BOOLEAN_ARRAY_EXTENSIONALITY)),CHEAP);
838 } // addBooleanArrayExtensionalityAxiom
839
840 /**
841 * Adds the write/select axiom of arrays (of type array1 or array2),
842 * @author Laura Kovacs
843 * @since 31/08/2012, Vienna
844 */
addArrayWriteAxioms(unsigned arraySort)845 void TheoryAxioms::addArrayWriteAxioms(unsigned arraySort)
846 {
847 CALL("TheoryAxioms::addArrayWriteAxioms");
848
849 unsigned func_select = env.signature->getInterpretingSymbol(Theory::ARRAY_SELECT,Theory::getArrayOperatorType(arraySort,Theory::ARRAY_SELECT));
850 unsigned func_store = env.signature->getInterpretingSymbol(Theory::ARRAY_STORE,Theory::getArrayOperatorType(arraySort,Theory::ARRAY_STORE));
851
852 Sorts::ArraySort* si = env.sorts->getArraySort(arraySort);
853 unsigned rangeSort = si->getInnerSort();
854 unsigned domainSort = si->getIndexSort();
855
856 TermList i(0,false);
857 TermList j(1,false);
858 TermList v(2,false);
859 TermList a(3,false);
860 TermList args[] = {a, i, v};
861
862 //axiom (!A: arraySort, !I:domainSort, !V:rangeSort: (select(store(A,I,V), I) = V
863 TermList wAIV(Term::create(func_store, 3, args)); //store(A,I,V)
864 TermList sWI(Term::create2(func_select, wAIV,i)); //select(wAIV,I)
865 Literal* ax = Literal::createEquality(true, sWI, v, rangeSort);
866 addTheoryClauseFromLits({ax}, InferenceRule::THA_ARRAY_WRITE1, CHEAP);
867
868 //axiom (!A: arraySort, !I,J:domainSort, !V:rangeSort: (I!=J)->(select(store(A,I,V), J) = select(A,J)
869 TermList sWJ(Term::create2(func_select, wAIV,j)); //select(wAIV,J)
870 TermList sAJ(Term::create2(func_select, a, j)); //select(A,J)
871
872 Literal* indexEq = Literal::createEquality(true, i, j, domainSort);//!(!(I=J)) === I=J
873 Literal* writeEq = Literal::createEquality(true, sWJ, sAJ, rangeSort);//(select(store(A,I,V), J) = select(A,J)
874 addTheoryClauseFromLits({indexEq,writeEq}, InferenceRule::THA_ARRAY_WRITE2, CHEAP);
875 } //
876
877 /**
878 * Adds the write/select axiom of arrays (of type array1 or array2),
879 * @author Laura Kovacs
880 * @since 31/08/2012, Vienna
881 */
addBooleanArrayWriteAxioms(unsigned arraySort)882 void TheoryAxioms::addBooleanArrayWriteAxioms(unsigned arraySort)
883 {
884 CALL("TheoryAxioms::addArrayWriteAxioms");
885
886 unsigned pred_select = env.signature->getInterpretingSymbol(Theory::ARRAY_BOOL_SELECT,Theory::getArrayOperatorType(arraySort,Theory::ARRAY_BOOL_SELECT));
887 unsigned func_store = env.signature->getInterpretingSymbol(Theory::ARRAY_STORE,Theory::getArrayOperatorType(arraySort,Theory::ARRAY_STORE));
888
889 Sorts::ArraySort* si = env.sorts->getArraySort(arraySort);
890 unsigned domainSort = si->getIndexSort();
891
892 TermList a(0,false);
893 TermList i(1,false);
894
895 TermList false_(Term::foolFalse());
896 TermList true_(Term::foolTrue());
897
898 // select(store(A,I,$$true), I)
899 //~select(store(A,I,$$false), I)
900
901 for (TermList bval : {false_,true_}) {
902 TermList args[] = {a, i, bval};
903 TermList wAIV(Term::create(func_store, 3, args)); //store(A,I,bval)
904 Literal* lit = Literal::create2(pred_select, true, wAIV,i);
905 if (bval == false_) {
906 lit = Literal::complementaryLiteral(lit);
907 }
908 Formula* ax = new AtomicFormula(lit);
909 addAndOutputTheoryUnit(new FormulaUnit(ax, TheoryAxiom(InferenceRule::THA_BOOLEAN_ARRAY_WRITE1)),CHEAP);
910 }
911
912 TermList v(2,false);
913 TermList j(3,false);
914
915 TermList args[] = {a, i, v};
916
917 //axiom (!A: arraySort, !I,J:domainSort, !V:rangeSort: (I!=J)->(select(store(A,I,V), J) <=> select(A,J)
918 TermList wAIV(Term::create(func_store, 3, args)); //store(A,I,V)
919 Formula* sWJ = new AtomicFormula(Literal::create2(pred_select, true, wAIV,j)); //select(wAIV,J)
920 Formula* sAJ = new AtomicFormula(Literal::create2(pred_select, true, a, j)); //select(A,J)
921
922 Formula* indexEq = new AtomicFormula(Literal::createEquality(false, i, j, domainSort));//I!=J
923 Formula* writeEq = new BinaryFormula(IFF, sWJ, sAJ);//(select(store(A,I,V), J) <=> select(A,J)
924 Formula* ax2 = new BinaryFormula(IMP, indexEq, writeEq);
925 addAndOutputTheoryUnit(new FormulaUnit(ax2, TheoryAxiom(InferenceRule::THA_BOOLEAN_ARRAY_WRITE2)),CHEAP);
926 } //
927
928 //Axioms for integer division that hven't been implemented yet
929 //
930 //axiom( (ige(X0,zero) & igt(X1,zero)) --> ( ilt(X0-X1, idiv(X0,X1)*X1) & ile(idiv(X0,X1)*X1, X0) ) );
931 //axiom( (ilt(X0,zero) & ilt(X1,zero)) --> ( igt(X0-X1, idiv(X0,X1)*X1) & ige(idiv(X0,X1)*X1, X0) ) );
932 //axiom( (ige(X0,zero) & ilt(X1,zero)) --> ( ilt(X0+X1, idiv(X0,X1)*X1) & ile(idiv(X0,X1)*X1, X0) ) );
933 //axiom( (ilt(X0,zero) & igt(X1,zero)) --> ( igt(X0+X1, idiv(X0,X1)*X1) & ige(idiv(X0,X1)*X1, X0) ) );
934 //axiom( (ilt(X0,zero) & igt(X1,zero)) --> ( igt(X0+X1, idiv(X0,X1)*X1) & ige(idiv(X0,X1)*X1, X0) ) );
935 //axiom( (X1!=zero) --> (idiv(X0,X1)+X2==idiv(X0+(X1*X2),X1)) );
936
937
938 /**
939 * Add theory axioms to the @b problem that are relevant to
940 * units present in the problem. The problem must have been processed
941 * by the InterpretedNormalizer before using this rule
942 *
943 * @since 11/11/2013, Manchester: bug fixes
944 * @author Andrei Voronkov
945 */
apply()946 void TheoryAxioms::apply()
947 {
948 CALL("TheoryAxioms::applyProperty");
949 Property* prop = _prb.getProperty();
950 bool modified = false;
951 bool haveIntPlus =
952 prop->hasInterpretedOperation(Theory::INT_PLUS) ||
953 prop->hasInterpretedOperation(Theory::INT_UNARY_MINUS) ||
954 prop->hasInterpretedOperation(Theory::INT_LESS) ||
955 prop->hasInterpretedOperation(Theory::INT_MULTIPLY);
956 bool haveIntMultiply =
957 prop->hasInterpretedOperation(Theory::INT_MULTIPLY);
958
959 bool haveIntDivision =
960 prop->hasInterpretedOperation(Theory::INT_QUOTIENT_E) || // let's ignore the weird _F and _T for now!
961 prop->hasInterpretedOperation(Theory::INT_REMAINDER_E) ||
962 prop->hasInterpretedOperation(Theory::INT_ABS);
963
964 bool haveIntDivides = prop->hasInterpretedOperation(Theory::INT_DIVIDES);
965
966 bool haveIntFloor = prop->hasInterpretedOperation(Theory::INT_FLOOR);
967 bool haveIntCeiling = prop->hasInterpretedOperation(Theory::INT_CEILING);
968 bool haveIntRound = prop->hasInterpretedOperation(Theory::INT_ROUND);
969 bool haveIntTruncate = prop->hasInterpretedOperation(Theory::INT_TRUNCATE);
970 bool haveIntUnaryRoundingFunction = haveIntFloor || haveIntCeiling || haveIntRound || haveIntTruncate;
971
972 if (haveIntPlus || haveIntUnaryRoundingFunction || haveIntDivision || haveIntDivides) {
973 TermList zero(theory->representConstant(IntegerConstantType(0)));
974 TermList one(theory->representConstant(IntegerConstantType(1)));
975 if(haveIntMultiply || haveIntDivision || haveIntDivides) {
976 addAdditionOrderingAndMultiplicationAxioms(Theory::INT_PLUS, Theory::INT_UNARY_MINUS, zero, one,
977 Theory::INT_LESS, Theory::INT_MULTIPLY);
978 if(haveIntDivision){
979 addIntegerDivisionWithModuloAxioms(Theory::INT_PLUS, Theory::INT_UNARY_MINUS, Theory::INT_LESS,
980 Theory::INT_MULTIPLY, Theory::INT_QUOTIENT_E, Theory::INT_DIVIDES,
981 Theory::INT_REMAINDER_E, Theory::INT_ABS, zero,one);
982 }
983 else if(haveIntDivides){
984 Stack<TermList>& ns = env.signature->getDividesNvalues();
985 Stack<TermList>::Iterator nsit(ns);
986 while(nsit.hasNext()){
987 TermList n = nsit.next();
988 addIntegerDividesAxioms(Theory::INT_DIVIDES,Theory::INT_MULTIPLY,zero,n);
989 }
990 }
991 }
992 else {
993 addAdditionAndOrderingAxioms(Theory::INT_PLUS, Theory::INT_UNARY_MINUS, zero, one,
994 Theory::INT_LESS);
995 }
996 addExtraIntegerOrderingAxiom(Theory::INT_PLUS, one, Theory::INT_LESS);
997 modified = true;
998 }
999 bool haveRatPlus =
1000 prop->hasInterpretedOperation(Theory::RAT_PLUS) ||
1001 prop->hasInterpretedOperation(Theory::RAT_UNARY_MINUS) ||
1002 prop->hasInterpretedOperation(Theory::RAT_LESS) ||
1003 prop->hasInterpretedOperation(Theory::RAT_QUOTIENT) ||
1004 prop->hasInterpretedOperation(Theory::RAT_MULTIPLY);
1005 bool haveRatMultiply =
1006 prop->hasInterpretedOperation(Theory::RAT_MULTIPLY);
1007 bool haveRatQuotient =
1008 prop->hasInterpretedOperation(Theory::RAT_QUOTIENT);
1009
1010 bool haveRatFloor = prop->hasInterpretedOperation(Theory::RAT_FLOOR);
1011 bool haveRatCeiling = prop->hasInterpretedOperation(Theory::RAT_CEILING);
1012 bool haveRatRound = prop->hasInterpretedOperation(Theory::RAT_ROUND);
1013 bool haveRatTruncate = prop->hasInterpretedOperation(Theory::RAT_TRUNCATE);
1014 bool haveRatUnaryRoundingFunction = haveRatFloor || haveRatCeiling || haveRatRound || haveRatTruncate;
1015
1016 if (haveRatPlus || haveRatUnaryRoundingFunction) {
1017 TermList zero(theory->representConstant(RationalConstantType(0, 1)));
1018 TermList one(theory->representConstant(RationalConstantType(1, 1)));
1019 if(haveRatMultiply || haveRatRound || haveRatQuotient) {
1020 addAdditionOrderingAndMultiplicationAxioms(Theory::RAT_PLUS, Theory::RAT_UNARY_MINUS, zero, one,
1021 Theory::RAT_LESS, Theory::RAT_MULTIPLY);
1022
1023 if(haveRatQuotient){
1024 addQuotientAxioms(Theory::RAT_QUOTIENT,Theory::RAT_MULTIPLY,zero,one,Theory::RAT_LESS);
1025 }
1026 }
1027 else {
1028 addAdditionAndOrderingAxioms(Theory::RAT_PLUS, Theory::RAT_UNARY_MINUS, zero, one,
1029 Theory::RAT_LESS);
1030 }
1031 if(haveRatFloor || haveRatRound){
1032 addFloorAxioms(Theory::RAT_FLOOR,Theory::RAT_LESS,Theory::RAT_UNARY_MINUS,Theory::RAT_PLUS,one);
1033 }
1034 if(haveRatCeiling || haveRatRound){
1035 addCeilingAxioms(Theory::RAT_CEILING,Theory::RAT_LESS,Theory::RAT_PLUS,one);
1036 }
1037 if(haveRatRound){
1038 //addRoundAxioms(Theory::INT_TRUNCATE,Theory::INT_FLOOR,Theory::INT_CEILING);
1039 }
1040 if(haveRatTruncate){
1041 addTruncateAxioms(Theory::RAT_TRUNCATE,Theory::RAT_LESS,Theory::RAT_UNARY_MINUS,
1042 Theory::RAT_PLUS,zero,one);
1043 }
1044 modified = true;
1045 }
1046 bool haveRealPlus =
1047 prop->hasInterpretedOperation(Theory::REAL_PLUS) ||
1048 prop->hasInterpretedOperation(Theory::REAL_UNARY_MINUS) ||
1049 prop->hasInterpretedOperation(Theory::REAL_LESS) ||
1050 prop->hasInterpretedOperation(Theory::REAL_QUOTIENT) ||
1051 prop->hasInterpretedOperation(Theory::REAL_MULTIPLY);
1052 bool haveRealMultiply =
1053 prop->hasInterpretedOperation(Theory::REAL_MULTIPLY);
1054 bool haveRealQuotient =
1055 prop->hasInterpretedOperation(Theory::REAL_QUOTIENT);
1056
1057 bool haveRealFloor = prop->hasInterpretedOperation(Theory::REAL_FLOOR);
1058 bool haveRealCeiling = prop->hasInterpretedOperation(Theory::REAL_CEILING);
1059 bool haveRealRound = prop->hasInterpretedOperation(Theory::REAL_ROUND);
1060 bool haveRealTruncate = prop->hasInterpretedOperation(Theory::REAL_TRUNCATE);
1061 bool haveRealUnaryRoundingFunction = haveRealFloor || haveRealCeiling || haveRealRound || haveRealTruncate;
1062
1063 if (haveRealPlus || haveRealUnaryRoundingFunction) {
1064 TermList zero(theory->representConstant(RealConstantType(RationalConstantType(0, 1))));
1065 TermList one(theory->representConstant(RealConstantType(RationalConstantType(1, 1))));
1066 if(haveRealMultiply || haveRealQuotient) {
1067 addAdditionOrderingAndMultiplicationAxioms(Theory::REAL_PLUS, Theory::REAL_UNARY_MINUS, zero, one,
1068 Theory::REAL_LESS, Theory::REAL_MULTIPLY);
1069
1070 if(haveRealQuotient){
1071 addQuotientAxioms(Theory::REAL_QUOTIENT,Theory::REAL_MULTIPLY,zero,one,Theory::REAL_LESS);
1072 }
1073 }
1074 else {
1075 addAdditionAndOrderingAxioms(Theory::REAL_PLUS, Theory::REAL_UNARY_MINUS, zero, one,
1076 Theory::REAL_LESS);
1077 }
1078 if(haveRealFloor || haveRealRound){
1079 addFloorAxioms(Theory::REAL_FLOOR,Theory::REAL_LESS,Theory::REAL_UNARY_MINUS,Theory::REAL_PLUS,one);
1080 }
1081 if(haveRealCeiling || haveRealRound){
1082 addCeilingAxioms(Theory::REAL_CEILING,Theory::REAL_LESS,Theory::REAL_PLUS,one);
1083 }
1084 if(haveRealRound){
1085 //addRoundAxioms(Theory::INT_TRUNCATE,Theory::INT_FLOOR,Theory::INT_CEILING);
1086 }
1087 if(haveRealTruncate){
1088 addTruncateAxioms(Theory::REAL_TRUNCATE,Theory::REAL_LESS,Theory::REAL_UNARY_MINUS,
1089 Theory::REAL_PLUS,zero,one);
1090 }
1091
1092 modified = true;
1093 }
1094
1095 VirtualIterator<unsigned> arraySorts = env.sorts->getStructuredSorts(Sorts::StructuredSort::ARRAY);
1096 while(arraySorts.hasNext()){
1097 unsigned arraySort = arraySorts.next();
1098
1099 bool isBool = (env.sorts->getArraySort(arraySort)->getInnerSort() == Sorts::SRT_BOOL);
1100
1101 // Check if they are used
1102 Interpretation arraySelect = isBool ? Theory::ARRAY_BOOL_SELECT : Theory::ARRAY_SELECT;
1103 bool haveSelect = prop->hasInterpretedOperation(arraySelect,Theory::getArrayOperatorType(arraySort,arraySelect));
1104 bool haveStore = prop->hasInterpretedOperation(Theory::ARRAY_STORE,Theory::getArrayOperatorType(arraySort,Theory::ARRAY_STORE));
1105
1106 if (haveSelect || haveStore) {
1107 unsigned sk = theory->getArrayExtSkolemFunction(arraySort);
1108 if (isBool) {
1109 addBooleanArrayExtensionalityAxioms(arraySort, sk);
1110 } else {
1111 addArrayExtensionalityAxioms(arraySort, sk);
1112 }
1113 if (haveStore) {
1114 if (isBool) {
1115 addBooleanArrayWriteAxioms(arraySort);
1116 } else {
1117 addArrayWriteAxioms(arraySort);
1118 }
1119 }
1120 modified = true;
1121 }
1122 }
1123
1124 VirtualIterator<TermAlgebra*> tas = env.signature->termAlgebrasIterator();
1125 while (tas.hasNext()) {
1126 TermAlgebra* ta = tas.next();
1127
1128 addExhaustivenessAxiom(ta);
1129 addDistinctnessAxiom(ta);
1130 addInjectivityAxiom(ta);
1131 addDiscriminationAxiom(ta);
1132
1133 if (env.options->termAlgebraCyclicityCheck() == Options::TACyclicityCheck::AXIOM) {
1134 addAcyclicityAxiom(ta);
1135 }
1136
1137 modified = true;
1138 }
1139
1140 if(modified) {
1141 _prb.reportEqualityAdded(false);
1142 }
1143 } // TheoryAxioms::apply
1144
applyFOOL()1145 void TheoryAxioms::applyFOOL() {
1146 CALL("TheoryAxioms::applyFOOL");
1147
1148 TermList t(Term::foolTrue());
1149 TermList f(Term::foolFalse());
1150
1151 // Add "$$true != $$false"
1152 Literal* tneqf = Literal::createEquality(false, t, f, Sorts::SRT_BOOL);
1153 addTheoryClauseFromLits({tneqf},InferenceRule::FOOL_AXIOM_TRUE_NEQ_FALSE,CHEAP);
1154
1155 // Do not add the finite domain axiom if --fool_paradomulation on
1156 if (env.options->FOOLParamodulation()) {
1157 return;
1158 }
1159
1160 // Add "![X : $bool]: ((X = $$true) | (X = $$false))"
1161 Literal* boolVar1 = Literal::createEquality(true, TermList(0, false), t, Sorts::SRT_BOOL);
1162 Literal* boolVar2 = Literal::createEquality(true, TermList(0, false), f, Sorts::SRT_BOOL);
1163 addTheoryClauseFromLits({boolVar1,boolVar2},InferenceRule::FOOL_AXIOM_ALL_IS_TRUE_OR_FALSE,CHEAP);
1164 } // TheoryAxioms::addBooleanDomainAxiom
1165
1166 /*
1167 * Note: In contrast to all other internally added theory axioms, the exhaustiveness axiom is
1168 * added in some cases as Formula and not as a clause. We would like to enforce the invariant that all internally
1169 * added theory axioms are added as clauses, in order to allow for an easy check whether a clause is
1170 * a theory axiom or not (without going up the preprocessing derivation until we derive at the axiom formula).
1171 * We currently already use this easy check, and miss the exhaustiveness axiom in some cases.
1172 *
1173 * Adding the exhaustiveness axiom as clause is difficult in the case where some destructor
1174 * has boolean sort: The currently implemented clausification-algorithms (default and newcnf) differ
1175 * in how they clausify the axiom formula, and newcnf as far as I know generates different clausifications
1176 * of the exhaustiveness axiom formula depending on the value of some magic constants.
1177 */
addExhaustivenessAxiom(TermAlgebra * ta)1178 void TheoryAxioms::addExhaustivenessAxiom(TermAlgebra* ta) {
1179 CALL("TheoryAxioms::addExhaustivenessAxiom");
1180
1181 TermList x(0, false);
1182
1183 // Part 1: compute list of literals and set flag if a FOOL-destructor occurs
1184 Stack<Literal*> lits;
1185 bool addsFOOL = false;
1186
1187 Stack<TermList> argTerms;
1188 for (unsigned i = 0; i < ta->nConstructors(); i++) {
1189 TermAlgebraConstructor *c = ta->constructor(i);
1190 argTerms.reset();
1191
1192 for (unsigned j = 0; j < c->arity(); j++) {
1193 if (c->argSort(j) == Sorts::SRT_BOOL) {
1194 addsFOOL = true;
1195 Literal* lit = Literal::create1(c->destructorFunctor(j), true, x);
1196 Term* t = Term::createFormula(new AtomicFormula(lit));
1197 argTerms.push(TermList(t));
1198 } else {
1199 Term* t = Term::create1(c->destructorFunctor(j), x);
1200 argTerms.push(TermList(t));
1201 }
1202 }
1203
1204 TermList rhs(Term::create(c->functor(), argTerms.size(), argTerms.begin()));
1205 lits.push(Literal::createEquality(true, x, rhs, ta->sort()));
1206 }
1207 ASS(!lits.isEmpty());
1208
1209 // Part 2: add axiom
1210 // - if no FOOL-destructors occur, add the axiom as clause
1211 // - otherwise, add the axiom as formula (cf. comments at the beginning of this method)
1212 Unit* axiom;
1213 if (!addsFOOL) {
1214 axiom = Clause::fromStack(lits, TheoryAxiom(InferenceRule::TERM_ALGEBRA_EXHAUSTIVENESS_AXIOM));
1215 } else {
1216 Formula* disjunction;
1217 if(lits.size() == 1) {
1218 disjunction = new AtomicFormula(lits[0]);
1219 } else {
1220 FormulaList* fl = FormulaList::empty();
1221 for (unsigned i = 0; i < lits.size(); i++)
1222 {
1223 FormulaList::push(new AtomicFormula(lits[i]), fl);
1224 }
1225 disjunction = new JunctionFormula(Connective::OR, fl);
1226 }
1227 Formula::VarList* vars = Formula::VarList::cons(x.var(), Formula::VarList::empty());
1228 Formula::SortList* sorts = Formula::SortList::cons(ta->sort(), Formula::SortList::empty());
1229 auto universal = new QuantifiedFormula(Connective::FORALL, vars, sorts, disjunction);
1230
1231 axiom = new FormulaUnit(universal, TheoryAxiom(InferenceRule::TERM_ALGEBRA_EXHAUSTIVENESS_AXIOM));
1232
1233 _prb.reportFOOLAdded();
1234 }
1235
1236 addAndOutputTheoryUnit(axiom, CHEAP);
1237 }
1238
addDistinctnessAxiom(TermAlgebra * ta)1239 void TheoryAxioms::addDistinctnessAxiom(TermAlgebra* ta) {
1240 CALL("TermAlgebra::addDistinctnessAxiom");
1241
1242 Array<TermList> terms(ta->nConstructors());
1243
1244 unsigned var = 0;
1245 for (unsigned i = 0; i < ta->nConstructors(); i++) {
1246 TermAlgebraConstructor* c = ta->constructor(i);
1247
1248 Stack<TermList> args;
1249 for (unsigned j = 0; j < c->arity(); j++) {
1250 args.push(TermList(var++, false));
1251 }
1252 TermList term(Term::create(c->functor(), (unsigned)args.size(), args.begin()));
1253 terms[i] = term;
1254 }
1255
1256 for (unsigned i = 0; i < ta->nConstructors(); i++) {
1257 for (unsigned j = i + 1; j < ta->nConstructors(); j++) {
1258 Literal* ineq = Literal::createEquality(false, terms[i], terms[j], ta->sort());
1259 addTheoryClauseFromLits({ineq}, InferenceRule::TERM_ALGEBRA_DISTINCTNESS_AXIOM,CHEAP);
1260 }
1261 }
1262 }
1263
addInjectivityAxiom(TermAlgebra * ta)1264 void TheoryAxioms::addInjectivityAxiom(TermAlgebra* ta)
1265 {
1266 CALL("TheoryAxioms::addInjectivityAxiom");
1267
1268 for (unsigned i = 0; i < ta->nConstructors(); i++) {
1269 TermAlgebraConstructor* c = ta->constructor(i);
1270
1271 Stack<TermList> lhsArgs(c->arity());
1272 Stack<TermList> rhsArgs(c->arity());
1273
1274 for (unsigned j = 0; j < c->arity(); j++) {
1275 lhsArgs.push(TermList(j * 2, false));
1276 rhsArgs.push(TermList(j * 2 + 1, false));
1277 }
1278
1279 TermList lhs(Term::create(c->functor(), (unsigned)lhsArgs.size(), lhsArgs.begin()));
1280 TermList rhs(Term::create(c->functor(), (unsigned)rhsArgs.size(), rhsArgs.begin()));
1281 Literal* eql = Literal::createEquality(false, lhs, rhs, ta->sort());
1282
1283 for (unsigned j = 0; j < c->arity(); j++) {
1284 Literal* eqr = Literal::createEquality(true, TermList(j * 2, false), TermList(j * 2 + 1, false), c->argSort(j));
1285
1286 addTheoryClauseFromLits({eql,eqr},InferenceRule::TERM_ALGEBRA_INJECTIVITY_AXIOM,CHEAP);
1287 }
1288 }
1289 }
1290
addDiscriminationAxiom(TermAlgebra * ta)1291 void TheoryAxioms::addDiscriminationAxiom(TermAlgebra* ta) {
1292 CALL("addDiscriminationAxiom");
1293
1294 Array<TermList> cases(ta->nConstructors());
1295 for (unsigned i = 0; i < ta->nConstructors(); i++) {
1296 TermAlgebraConstructor* c = ta->constructor(i);
1297
1298 Stack<TermList> variables;
1299 for (unsigned var = 0; var < c->arity(); var++) {
1300 variables.push(TermList(var, false));
1301 }
1302
1303 TermList term(Term::create(c->functor(), (unsigned)variables.size(), variables.begin()));
1304 cases[i] = term;
1305 }
1306
1307 for (unsigned i = 0; i < ta->nConstructors(); i++) {
1308 TermAlgebraConstructor* constructor = ta->constructor(i);
1309
1310 if (!constructor->hasDiscriminator()) continue;
1311
1312 for (unsigned c = 0; c < cases.size(); c++) {
1313 Literal* lit = Literal::create1(constructor->discriminator(), c == i, cases[c]);
1314 addTheoryClauseFromLits({lit}, InferenceRule::TERM_ALGEBRA_DISCRIMINATION_AXIOM,CHEAP);
1315 }
1316 }
1317 }
1318
addAcyclicityAxiom(TermAlgebra * ta)1319 void TheoryAxioms::addAcyclicityAxiom(TermAlgebra* ta)
1320 {
1321 CALL("TheoryAxioms::addAcyclicityAxiom");
1322
1323 unsigned pred = ta->getSubtermPredicate();
1324
1325 if (ta->allowsCyclicTerms()) {
1326 return;
1327 }
1328
1329 bool rec = false;
1330
1331 for (unsigned i = 0; i < ta->nConstructors(); i++) {
1332 if (addSubtermDefinitions(pred, ta->constructor(i))) {
1333 rec = true;
1334 }
1335 }
1336
1337 // rec <=> the subterm relation is non-empty
1338 if (!rec) {
1339 return;
1340 }
1341
1342 static TermList x(0, false);
1343
1344 Literal* sub = Literal::create2(pred, false, x, x);
1345 addTheoryClauseFromLits({sub}, InferenceRule::TERM_ALGEBRA_ACYCLICITY_AXIOM,CHEAP);
1346 }
1347
addSubtermDefinitions(unsigned subtermPredicate,TermAlgebraConstructor * c)1348 bool TheoryAxioms::addSubtermDefinitions(unsigned subtermPredicate, TermAlgebraConstructor* c)
1349 {
1350 CALL("TheoryAxioms::addSubtermDefinitions");
1351
1352 TermList z(c->arity(), false);
1353
1354 Stack<TermList> args;
1355 for (unsigned i = 0; i < c->arity(); i++) {
1356 args.push(TermList(i, false));
1357 }
1358 TermList right(Term::create(c->functor(), (unsigned)args.size(), args.begin()));
1359
1360 bool added = false;
1361 for (unsigned i = 0; i < c->arity(); i++) {
1362 if (c->argSort(i) != c->rangeSort()) continue;
1363
1364 TermList y(i, false);
1365
1366 // Direct subterms are subterms: Sub(y, c(x1, ... y ..., xn))
1367 Literal* sub = Literal::create2(subtermPredicate, true, y, right);
1368 addTheoryClauseFromLits({sub}, InferenceRule::TERM_ALGEBRA_DIRECT_SUBTERMS_AXIOM,CHEAP);
1369
1370 // Transitivity of the subterm relation: Sub(z, y) -> Sub(z, c(x1, ... y , xn))
1371 Literal* trans1 = Literal::create2(subtermPredicate, false, z, y);
1372 Literal* trans2 = Literal::create2(subtermPredicate, true, z, right);
1373 addTheoryClauseFromLits({trans1,trans2}, InferenceRule::TERM_ALGEBRA_SUBTERMS_TRANSITIVE_AXIOM,CHEAP);
1374
1375 added = true;
1376 }
1377 return added;
1378 }
1379