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