reduce visibility of several methods in solver-specific numeral formula managers.

kfriedberger · kfriedberger · commit b8587768b4e1 · 2019-11-14T19:33:42.000+01:00
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NumeralFormulaManager.java
@@ -71,7 +71,7 @@ abstract class CVC4NumeralFormulaManager<
   protected abstract Type getNumeralType();
 
   @Override
-  public boolean isNumeral(Expr pVal) {
+  protected boolean isNumeral(Expr pVal) {
     return (pVal.getType().isInteger() || pVal.getType().isReal()) && pVal.isConst();
   }
 
@@ -134,7 +134,7 @@ protected Expr makeVariableImpl(String varName) {
   }
 
   @Override
-  public Expr multiply(Expr pParam1, Expr pParam2) {
+  protected Expr multiply(Expr pParam1, Expr pParam2) {
     if (consistsOfNumerals(pParam1) || consistsOfNumerals(pParam2)) {
       return exprManager.mkExpr(Kind.MULT, pParam1, pParam2);
     } else {
@@ -143,47 +143,47 @@ public Expr multiply(Expr pParam1, Expr pParam2) {
   }
 
   @Override
-  public Expr modulo(Expr pParam1, Expr pParam2) {
+  protected Expr modulo(Expr pParam1, Expr pParam2) {
     return exprManager.mkExpr(Kind.INTS_MODULUS, pParam1, pParam2);
   }
 
   @Override
-  public Expr negate(Expr pParam1) {
+  protected Expr negate(Expr pParam1) {
     return exprManager.mkExpr(Kind.UMINUS, pParam1);
   }
 
   @Override
-  public Expr add(Expr pParam1, Expr pParam2) {
+  protected Expr add(Expr pParam1, Expr pParam2) {
     return exprManager.mkExpr(Kind.PLUS, pParam1, pParam2);
   }
 
   @Override
-  public Expr subtract(Expr pParam1, Expr pParam2) {
+  protected Expr subtract(Expr pParam1, Expr pParam2) {
     return exprManager.mkExpr(Kind.MINUS, pParam1, pParam2);
   }
 
   @Override
-  public Expr equal(Expr pParam1, Expr pParam2) {
+  protected Expr equal(Expr pParam1, Expr pParam2) {
     return exprManager.mkExpr(Kind.EQUAL, pParam1, pParam2);
   }
 
   @Override
-  public Expr greaterThan(Expr pParam1, Expr pParam2) {
+  protected Expr greaterThan(Expr pParam1, Expr pParam2) {
     return exprManager.mkExpr(Kind.GT, pParam1, pParam2);
   }
 
   @Override
-  public Expr greaterOrEquals(Expr pParam1, Expr pParam2) {
+  protected Expr greaterOrEquals(Expr pParam1, Expr pParam2) {
     return exprManager.mkExpr(Kind.GEQ, pParam1, pParam2);
   }
 
   @Override
-  public Expr lessThan(Expr pParam1, Expr pParam2) {
+  protected Expr lessThan(Expr pParam1, Expr pParam2) {
     return exprManager.mkExpr(Kind.LT, pParam1, pParam2);
   }
 
   @Override
-  public Expr lessOrEquals(Expr pParam1, Expr pParam2) {
+  protected Expr lessOrEquals(Expr pParam1, Expr pParam2) {
     return exprManager.mkExpr(Kind.LEQ, pParam1, pParam2);
   }
 
diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NumeralFormulaManager.java
@@ -55,7 +55,7 @@ protected boolean isNumeral(Long val) {
   }
 
   @Override
-  public Long makeNumberImpl(long pNumber) {
+  protected Long makeNumberImpl(long pNumber) {
     int i = (int) pNumber;
     if (i == pNumber) { // fits in an int
       return msat_make_int_number(mathsatEnv, i);
@@ -64,49 +64,49 @@ public Long makeNumberImpl(long pNumber) {
   }
 
   @Override
-  public Long makeNumberImpl(BigInteger pI) {
+  protected Long makeNumberImpl(BigInteger pI) {
     return msat_make_number(mathsatEnv, pI.toString());
   }
 
   @Override
-  public Long makeNumberImpl(String pI) {
+  protected Long makeNumberImpl(String pI) {
     return msat_make_number(mathsatEnv, pI);
   }
 
   protected abstract long getNumeralType();
 
   @Override
-  public Long makeVariableImpl(String var) {
+  protected Long makeVariableImpl(String var) {
     return getFormulaCreator().makeVariable(getNumeralType(), var);
   }
 
   @Override
-  public Long negate(Long pNumber) {
+  protected Long negate(Long pNumber) {
     return msat_make_times(mathsatEnv, pNumber, msat_make_number(mathsatEnv, "-1"));
   }
 
   @Override
-  public Long add(Long pNumber1, Long pNumber2) {
+  protected Long add(Long pNumber1, Long pNumber2) {
     return msat_make_plus(mathsatEnv, pNumber1, pNumber2);
   }
 
   @Override
-  public Long subtract(Long pNumber1, Long pNumber2) {
+  protected Long subtract(Long pNumber1, Long pNumber2) {
     return msat_make_plus(mathsatEnv, pNumber1, negate(pNumber2));
   }
 
   @Override
-  public Long multiply(Long pNumber1, Long pNumber2) {
+  protected Long multiply(Long pNumber1, Long pNumber2) {
     return msat_make_times(mathsatEnv, pNumber1, pNumber2);
   }
 
   @Override
-  public Long equal(Long pNumber1, Long pNumber2) {
+  protected Long equal(Long pNumber1, Long pNumber2) {
     return msat_make_equal(mathsatEnv, pNumber1, pNumber2);
   }
 
   @Override
-  public Long distinctImpl(List<Long> pNumbers) {
+  protected Long distinctImpl(List<Long> pNumbers) {
     // MathSat does not directly support this method, we need to build the whole term.
     long r = msat_make_true(mathsatEnv);
     for (int i = 0; i < pNumbers.size(); i++) {
@@ -118,12 +118,12 @@ public Long distinctImpl(List<Long> pNumbers) {
   }
 
   @Override
-  public Long greaterThan(Long pNumber1, Long pNumber2) {
+  protected Long greaterThan(Long pNumber1, Long pNumber2) {
     return makeNot(lessOrEquals(pNumber1, pNumber2));
   }
 
   @Override
-  public Long greaterOrEquals(Long pNumber1, Long pNumber2) {
+  protected Long greaterOrEquals(Long pNumber1, Long pNumber2) {
     return lessOrEquals(pNumber2, pNumber1);
   }
 
@@ -132,12 +132,12 @@ private long makeNot(long n) {
   }
 
   @Override
-  public Long lessThan(Long pNumber1, Long pNumber2) {
+  protected Long lessThan(Long pNumber1, Long pNumber2) {
     return makeNot(lessOrEquals(pNumber2, pNumber1));
   }
 
   @Override
-  public Long lessOrEquals(Long pNumber1, Long pNumber2) {
+  protected Long lessOrEquals(Long pNumber1, Long pNumber2) {
     return msat_make_leq(mathsatEnv, pNumber1, pNumber2);
   }
 
diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessNumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessNumeralFormulaManager.java
@@ -46,22 +46,22 @@ abstract class PrincessNumeralFormulaManager<
   }
 
   @Override
-  public ITerm negate(IExpression pNumber) {
+  protected ITerm negate(IExpression pNumber) {
     return ((ITerm) pNumber).unary_$minus();
   }
 
   @Override
-  public ITerm add(IExpression pNumber1, IExpression pNumber2) {
+  protected ITerm add(IExpression pNumber1, IExpression pNumber2) {
     return ((ITerm) pNumber1).$plus((ITerm) pNumber2);
   }
 
   @Override
-  public ITerm subtract(IExpression pNumber1, IExpression pNumber2) {
+  protected ITerm subtract(IExpression pNumber1, IExpression pNumber2) {
     return ((ITerm) pNumber1).$minus((ITerm) pNumber2);
   }
 
   @Override
-  public IFormula equal(IExpression pNumber1, IExpression pNumber2) {
+  protected IFormula equal(IExpression pNumber1, IExpression pNumber2) {
     return ((ITerm) pNumber1).$eq$eq$eq((ITerm) pNumber2);
   }
 
@@ -71,22 +71,22 @@ protected IExpression distinctImpl(List<IExpression> pNumbers) {
   }
 
   @Override
-  public IFormula greaterThan(IExpression pNumber1, IExpression pNumber2) {
+  protected IFormula greaterThan(IExpression pNumber1, IExpression pNumber2) {
     return ((ITerm) pNumber1).$greater((ITerm) pNumber2);
   }
 
   @Override
-  public IFormula greaterOrEquals(IExpression pNumber1, IExpression pNumber2) {
+  protected IFormula greaterOrEquals(IExpression pNumber1, IExpression pNumber2) {
     return ((ITerm) pNumber1).$greater$eq((ITerm) pNumber2);
   }
 
   @Override
-  public IFormula lessThan(IExpression pNumber1, IExpression pNumber2) {
+  protected IFormula lessThan(IExpression pNumber1, IExpression pNumber2) {
     return ((ITerm) pNumber1).$less((ITerm) pNumber2);
   }
 
   @Override
-  public IFormula lessOrEquals(IExpression pNumber1, IExpression pNumber2) {
+  protected IFormula lessOrEquals(IExpression pNumber1, IExpression pNumber2) {
     return ((ITerm) pNumber1).$less$eq((ITerm) pNumber2);
   }
 }
diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3NumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3NumeralFormulaManager.java
@@ -69,64 +69,64 @@ protected Long makeVariableImpl(String varName) {
   }
 
   @Override
-  public Long negate(Long pNumber) {
+  protected Long negate(Long pNumber) {
     long sort = Native.getSort(z3context, pNumber);
     long minusOne = Native.mkInt(z3context, -1, sort);
     return Native.mkMul(z3context, 2, new long[] {minusOne, pNumber});
   }
 
   @Override
-  public Long add(Long pNumber1, Long pNumber2) {
+  protected Long add(Long pNumber1, Long pNumber2) {
     return Native.mkAdd(z3context, 2, new long[] {pNumber1, pNumber2});
   }
 
   @Override
-  public Long sumImpl(List<Long> operands) {
+  protected Long sumImpl(List<Long> operands) {
     return Native.mkAdd(z3context, operands.size(), Longs.toArray(operands));
   }
 
   @Override
-  public Long subtract(Long pNumber1, Long pNumber2) {
+  protected Long subtract(Long pNumber1, Long pNumber2) {
     return Native.mkSub(z3context, 2, new long[] {pNumber1, pNumber2});
   }
 
   @Override
-  public Long divide(Long pNumber1, Long pNumber2) {
+  protected Long divide(Long pNumber1, Long pNumber2) {
     return Native.mkDiv(z3context, pNumber1, pNumber2);
   }
 
   @Override
-  public Long multiply(Long pNumber1, Long pNumber2) {
+  protected Long multiply(Long pNumber1, Long pNumber2) {
     return Native.mkMul(z3context, 2, new long[] {pNumber1, pNumber2});
   }
 
   @Override
-  public Long equal(Long pNumber1, Long pNumber2) {
+  protected Long equal(Long pNumber1, Long pNumber2) {
     return Native.mkEq(z3context, pNumber1, pNumber2);
   }
 
   @Override
-  public Long distinctImpl(List<Long> pNumbers) {
+  protected Long distinctImpl(List<Long> pNumbers) {
     return Native.mkDistinct(z3context, pNumbers.size(), Longs.toArray(pNumbers));
   }
 
   @Override
-  public Long greaterThan(Long pNumber1, Long pNumber2) {
+  protected Long greaterThan(Long pNumber1, Long pNumber2) {
     return Native.mkGt(z3context, pNumber1, pNumber2);
   }
 
   @Override
-  public Long greaterOrEquals(Long pNumber1, Long pNumber2) {
+  protected Long greaterOrEquals(Long pNumber1, Long pNumber2) {
     return Native.mkGe(z3context, pNumber1, pNumber2);
   }
 
   @Override
-  public Long lessThan(Long pNumber1, Long pNumber2) {
+  protected Long lessThan(Long pNumber1, Long pNumber2) {
     return Native.mkLt(z3context, pNumber1, pNumber2);
   }
 
   @Override
-  public Long lessOrEquals(Long pNumber1, Long pNumber2) {
+  protected Long lessOrEquals(Long pNumber1, Long pNumber2) {
     return Native.mkLe(z3context, pNumber1, pNumber2);
   }
 }

Original file line number	Diff line number	Diff line change
`@@ -71,7 +71,7 @@ abstract class CVC4NumeralFormulaManager<`
`71`	`71`	`protected abstract Type getNumeralType();`
`72`	`72`
`73`	`73`	`@Override`
`74`		`- public boolean isNumeral(Expr pVal) {`
	`74`	`+ protected boolean isNumeral(Expr pVal) {`
`75`	`75`	`return (pVal.getType().isInteger() \|\| pVal.getType().isReal()) && pVal.isConst();`
`76`	`76`	`}`
`77`	`77`
`@@ -134,7 +134,7 @@ protected Expr makeVariableImpl(String varName) {`
`134`	`134`	`}`
`135`	`135`
`136`	`136`	`@Override`
`137`		`- public Expr multiply(Expr pParam1, Expr pParam2) {`
	`137`	`+ protected Expr multiply(Expr pParam1, Expr pParam2) {`
`138`	`138`	`if (consistsOfNumerals(pParam1) \|\| consistsOfNumerals(pParam2)) {`
`139`	`139`	`return exprManager.mkExpr(Kind.MULT, pParam1, pParam2);`
`140`	`140`	`} else {`
`@@ -143,47 +143,47 @@ public Expr multiply(Expr pParam1, Expr pParam2) {`
`143`	`143`	`}`
`144`	`144`
`145`	`145`	`@Override`
`146`		`- public Expr modulo(Expr pParam1, Expr pParam2) {`
	`146`	`+ protected Expr modulo(Expr pParam1, Expr pParam2) {`
`147`	`147`	`return exprManager.mkExpr(Kind.INTS_MODULUS, pParam1, pParam2);`
`148`	`148`	`}`
`149`	`149`
`150`	`150`	`@Override`
`151`		`- public Expr negate(Expr pParam1) {`
	`151`	`+ protected Expr negate(Expr pParam1) {`
`152`	`152`	`return exprManager.mkExpr(Kind.UMINUS, pParam1);`
`153`	`153`	`}`
`154`	`154`
`155`	`155`	`@Override`
`156`		`- public Expr add(Expr pParam1, Expr pParam2) {`
	`156`	`+ protected Expr add(Expr pParam1, Expr pParam2) {`
`157`	`157`	`return exprManager.mkExpr(Kind.PLUS, pParam1, pParam2);`
`158`	`158`	`}`
`159`	`159`
`160`	`160`	`@Override`
`161`		`- public Expr subtract(Expr pParam1, Expr pParam2) {`
	`161`	`+ protected Expr subtract(Expr pParam1, Expr pParam2) {`
`162`	`162`	`return exprManager.mkExpr(Kind.MINUS, pParam1, pParam2);`
`163`	`163`	`}`
`164`	`164`
`165`	`165`	`@Override`
`166`		`- public Expr equal(Expr pParam1, Expr pParam2) {`
	`166`	`+ protected Expr equal(Expr pParam1, Expr pParam2) {`
`167`	`167`	`return exprManager.mkExpr(Kind.EQUAL, pParam1, pParam2);`
`168`	`168`	`}`
`169`	`169`
`170`	`170`	`@Override`
`171`		`- public Expr greaterThan(Expr pParam1, Expr pParam2) {`
	`171`	`+ protected Expr greaterThan(Expr pParam1, Expr pParam2) {`
`172`	`172`	`return exprManager.mkExpr(Kind.GT, pParam1, pParam2);`
`173`	`173`	`}`
`174`	`174`
`175`	`175`	`@Override`
`176`		`- public Expr greaterOrEquals(Expr pParam1, Expr pParam2) {`
	`176`	`+ protected Expr greaterOrEquals(Expr pParam1, Expr pParam2) {`
`177`	`177`	`return exprManager.mkExpr(Kind.GEQ, pParam1, pParam2);`
`178`	`178`	`}`
`179`	`179`
`180`	`180`	`@Override`
`181`		`- public Expr lessThan(Expr pParam1, Expr pParam2) {`
	`181`	`+ protected Expr lessThan(Expr pParam1, Expr pParam2) {`
`182`	`182`	`return exprManager.mkExpr(Kind.LT, pParam1, pParam2);`
`183`	`183`	`}`
`184`	`184`
`185`	`185`	`@Override`
`186`		`- public Expr lessOrEquals(Expr pParam1, Expr pParam2) {`
	`186`	`+ protected Expr lessOrEquals(Expr pParam1, Expr pParam2) {`
`187`	`187`	`return exprManager.mkExpr(Kind.LEQ, pParam1, pParam2);`
`188`	`188`	`}`
`189`	`189`
Original file line number	Diff line number	Diff line change
`@@ -55,7 +55,7 @@ protected boolean isNumeral(Long val) {`
`55`	`55`	`}`
`56`	`56`
`57`	`57`	`@Override`
`58`		`- public Long makeNumberImpl(long pNumber) {`
	`58`	`+ protected Long makeNumberImpl(long pNumber) {`
`59`	`59`	`int i = (int) pNumber;`
`60`	`60`	`if (i == pNumber) { // fits in an int`
`61`	`61`	`return msat_make_int_number(mathsatEnv, i);`
`@@ -64,49 +64,49 @@ public Long makeNumberImpl(long pNumber) {`
`64`	`64`	`}`
`65`	`65`
`66`	`66`	`@Override`
`67`		`- public Long makeNumberImpl(BigInteger pI) {`
	`67`	`+ protected Long makeNumberImpl(BigInteger pI) {`
`68`	`68`	`return msat_make_number(mathsatEnv, pI.toString());`
`69`	`69`	`}`
`70`	`70`
`71`	`71`	`@Override`
`72`		`- public Long makeNumberImpl(String pI) {`
	`72`	`+ protected Long makeNumberImpl(String pI) {`
`73`	`73`	`return msat_make_number(mathsatEnv, pI);`
`74`	`74`	`}`
`75`	`75`
`76`	`76`	`protected abstract long getNumeralType();`
`77`	`77`
`78`	`78`	`@Override`
`79`		`- public Long makeVariableImpl(String var) {`
	`79`	`+ protected Long makeVariableImpl(String var) {`
`80`	`80`	`return getFormulaCreator().makeVariable(getNumeralType(), var);`
`81`	`81`	`}`
`82`	`82`
`83`	`83`	`@Override`
`84`		`- public Long negate(Long pNumber) {`
	`84`	`+ protected Long negate(Long pNumber) {`
`85`	`85`	`return msat_make_times(mathsatEnv, pNumber, msat_make_number(mathsatEnv, "-1"));`
`86`	`86`	`}`
`87`	`87`
`88`	`88`	`@Override`
`89`		`- public Long add(Long pNumber1, Long pNumber2) {`
	`89`	`+ protected Long add(Long pNumber1, Long pNumber2) {`
`90`	`90`	`return msat_make_plus(mathsatEnv, pNumber1, pNumber2);`
`91`	`91`	`}`
`92`	`92`
`93`	`93`	`@Override`
`94`		`- public Long subtract(Long pNumber1, Long pNumber2) {`
	`94`	`+ protected Long subtract(Long pNumber1, Long pNumber2) {`
`95`	`95`	`return msat_make_plus(mathsatEnv, pNumber1, negate(pNumber2));`
`96`	`96`	`}`
`97`	`97`
`98`	`98`	`@Override`
`99`		`- public Long multiply(Long pNumber1, Long pNumber2) {`
	`99`	`+ protected Long multiply(Long pNumber1, Long pNumber2) {`
`100`	`100`	`return msat_make_times(mathsatEnv, pNumber1, pNumber2);`
`101`	`101`	`}`
`102`	`102`
`103`	`103`	`@Override`
`104`		`- public Long equal(Long pNumber1, Long pNumber2) {`
	`104`	`+ protected Long equal(Long pNumber1, Long pNumber2) {`
`105`	`105`	`return msat_make_equal(mathsatEnv, pNumber1, pNumber2);`
`106`	`106`	`}`
`107`	`107`
`108`	`108`	`@Override`
`109`		`- public Long distinctImpl(List<Long> pNumbers) {`
	`109`	`+ protected Long distinctImpl(List<Long> pNumbers) {`
`110`	`110`	`// MathSat does not directly support this method, we need to build the whole term.`
`111`	`111`	`long r = msat_make_true(mathsatEnv);`
`112`	`112`	`for (int i = 0; i < pNumbers.size(); i++) {`
`@@ -118,12 +118,12 @@ public Long distinctImpl(List<Long> pNumbers) {`
`118`	`118`	`}`
`119`	`119`
`120`	`120`	`@Override`
`121`		`- public Long greaterThan(Long pNumber1, Long pNumber2) {`
	`121`	`+ protected Long greaterThan(Long pNumber1, Long pNumber2) {`
`122`	`122`	`return makeNot(lessOrEquals(pNumber1, pNumber2));`
`123`	`123`	`}`
`124`	`124`
`125`	`125`	`@Override`
`126`		`- public Long greaterOrEquals(Long pNumber1, Long pNumber2) {`
	`126`	`+ protected Long greaterOrEquals(Long pNumber1, Long pNumber2) {`
`127`	`127`	`return lessOrEquals(pNumber2, pNumber1);`
`128`	`128`	`}`
`129`	`129`
`@@ -132,12 +132,12 @@ private long makeNot(long n) {`
`132`	`132`	`}`
`133`	`133`
`134`	`134`	`@Override`
`135`		`- public Long lessThan(Long pNumber1, Long pNumber2) {`
	`135`	`+ protected Long lessThan(Long pNumber1, Long pNumber2) {`
`136`	`136`	`return makeNot(lessOrEquals(pNumber2, pNumber1));`
`137`	`137`	`}`
`138`	`138`
`139`	`139`	`@Override`
`140`		`- public Long lessOrEquals(Long pNumber1, Long pNumber2) {`
	`140`	`+ protected Long lessOrEquals(Long pNumber1, Long pNumber2) {`
`141`	`141`	`return msat_make_leq(mathsatEnv, pNumber1, pNumber2);`
`142`	`142`	`}`
`143`	`143`
Original file line number	Diff line number	Diff line change
`@@ -46,22 +46,22 @@ abstract class PrincessNumeralFormulaManager<`
`46`	`46`	`}`
`47`	`47`
`48`	`48`	`@Override`
`49`		`- public ITerm negate(IExpression pNumber) {`
	`49`	`+ protected ITerm negate(IExpression pNumber) {`
`50`	`50`	`return ((ITerm) pNumber).unary_$minus();`
`51`	`51`	`}`
`52`	`52`
`53`	`53`	`@Override`
`54`		`- public ITerm add(IExpression pNumber1, IExpression pNumber2) {`
	`54`	`+ protected ITerm add(IExpression pNumber1, IExpression pNumber2) {`
`55`	`55`	`return ((ITerm) pNumber1).$plus((ITerm) pNumber2);`
`56`	`56`	`}`
`57`	`57`
`58`	`58`	`@Override`
`59`		`- public ITerm subtract(IExpression pNumber1, IExpression pNumber2) {`
	`59`	`+ protected ITerm subtract(IExpression pNumber1, IExpression pNumber2) {`
`60`	`60`	`return ((ITerm) pNumber1).$minus((ITerm) pNumber2);`
`61`	`61`	`}`
`62`	`62`
`63`	`63`	`@Override`
`64`		`- public IFormula equal(IExpression pNumber1, IExpression pNumber2) {`
	`64`	`+ protected IFormula equal(IExpression pNumber1, IExpression pNumber2) {`
`65`	`65`	`return ((ITerm) pNumber1).$eq$eq$eq((ITerm) pNumber2);`
`66`	`66`	`}`
`67`	`67`
`@@ -71,22 +71,22 @@ protected IExpression distinctImpl(List<IExpression> pNumbers) {`
`71`	`71`	`}`
`72`	`72`
`73`	`73`	`@Override`
`74`		`- public IFormula greaterThan(IExpression pNumber1, IExpression pNumber2) {`
	`74`	`+ protected IFormula greaterThan(IExpression pNumber1, IExpression pNumber2) {`
`75`	`75`	`return ((ITerm) pNumber1).$greater((ITerm) pNumber2);`
`76`	`76`	`}`
`77`	`77`
`78`	`78`	`@Override`
`79`		`- public IFormula greaterOrEquals(IExpression pNumber1, IExpression pNumber2) {`
	`79`	`+ protected IFormula greaterOrEquals(IExpression pNumber1, IExpression pNumber2) {`
`80`	`80`	`return ((ITerm) pNumber1).$greater$eq((ITerm) pNumber2);`
`81`	`81`	`}`
`82`	`82`
`83`	`83`	`@Override`
`84`		`- public IFormula lessThan(IExpression pNumber1, IExpression pNumber2) {`
	`84`	`+ protected IFormula lessThan(IExpression pNumber1, IExpression pNumber2) {`
`85`	`85`	`return ((ITerm) pNumber1).$less((ITerm) pNumber2);`
`86`	`86`	`}`
`87`	`87`
`88`	`88`	`@Override`
`89`		`- public IFormula lessOrEquals(IExpression pNumber1, IExpression pNumber2) {`
	`89`	`+ protected IFormula lessOrEquals(IExpression pNumber1, IExpression pNumber2) {`
`90`	`90`	`return ((ITerm) pNumber1).$less$eq((ITerm) pNumber2);`
`91`	`91`	`}`
`92`	`92`	`}`
Original file line number	Diff line number	Diff line change
`@@ -69,64 +69,64 @@ protected Long makeVariableImpl(String varName) {`
`69`	`69`	`}`
`70`	`70`
`71`	`71`	`@Override`
`72`		`- public Long negate(Long pNumber) {`
	`72`	`+ protected Long negate(Long pNumber) {`
`73`	`73`	`long sort = Native.getSort(z3context, pNumber);`
`74`	`74`	`long minusOne = Native.mkInt(z3context, -1, sort);`
`75`	`75`	`return Native.mkMul(z3context, 2, new long[] {minusOne, pNumber});`
`76`	`76`	`}`
`77`	`77`
`78`	`78`	`@Override`
`79`		`- public Long add(Long pNumber1, Long pNumber2) {`
	`79`	`+ protected Long add(Long pNumber1, Long pNumber2) {`
`80`	`80`	`return Native.mkAdd(z3context, 2, new long[] {pNumber1, pNumber2});`
`81`	`81`	`}`
`82`	`82`
`83`	`83`	`@Override`
`84`		`- public Long sumImpl(List<Long> operands) {`
	`84`	`+ protected Long sumImpl(List<Long> operands) {`
`85`	`85`	`return Native.mkAdd(z3context, operands.size(), Longs.toArray(operands));`
`86`	`86`	`}`
`87`	`87`
`88`	`88`	`@Override`
`89`		`- public Long subtract(Long pNumber1, Long pNumber2) {`
	`89`	`+ protected Long subtract(Long pNumber1, Long pNumber2) {`
`90`	`90`	`return Native.mkSub(z3context, 2, new long[] {pNumber1, pNumber2});`
`91`	`91`	`}`
`92`	`92`
`93`	`93`	`@Override`
`94`		`- public Long divide(Long pNumber1, Long pNumber2) {`
	`94`	`+ protected Long divide(Long pNumber1, Long pNumber2) {`
`95`	`95`	`return Native.mkDiv(z3context, pNumber1, pNumber2);`
`96`	`96`	`}`
`97`	`97`
`98`	`98`	`@Override`
`99`		`- public Long multiply(Long pNumber1, Long pNumber2) {`
	`99`	`+ protected Long multiply(Long pNumber1, Long pNumber2) {`
`100`	`100`	`return Native.mkMul(z3context, 2, new long[] {pNumber1, pNumber2});`
`101`	`101`	`}`
`102`	`102`
`103`	`103`	`@Override`
`104`		`- public Long equal(Long pNumber1, Long pNumber2) {`
	`104`	`+ protected Long equal(Long pNumber1, Long pNumber2) {`
`105`	`105`	`return Native.mkEq(z3context, pNumber1, pNumber2);`
`106`	`106`	`}`
`107`	`107`
`108`	`108`	`@Override`
`109`		`- public Long distinctImpl(List<Long> pNumbers) {`
	`109`	`+ protected Long distinctImpl(List<Long> pNumbers) {`
`110`	`110`	`return Native.mkDistinct(z3context, pNumbers.size(), Longs.toArray(pNumbers));`
`111`	`111`	`}`
`112`	`112`
`113`	`113`	`@Override`
`114`		`- public Long greaterThan(Long pNumber1, Long pNumber2) {`
	`114`	`+ protected Long greaterThan(Long pNumber1, Long pNumber2) {`
`115`	`115`	`return Native.mkGt(z3context, pNumber1, pNumber2);`
`116`	`116`	`}`
`117`	`117`
`118`	`118`	`@Override`
`119`		`- public Long greaterOrEquals(Long pNumber1, Long pNumber2) {`
	`119`	`+ protected Long greaterOrEquals(Long pNumber1, Long pNumber2) {`
`120`	`120`	`return Native.mkGe(z3context, pNumber1, pNumber2);`
`121`	`121`	`}`
`122`	`122`
`123`	`123`	`@Override`
`124`		`- public Long lessThan(Long pNumber1, Long pNumber2) {`
	`124`	`+ protected Long lessThan(Long pNumber1, Long pNumber2) {`
`125`	`125`	`return Native.mkLt(z3context, pNumber1, pNumber2);`
`126`	`126`	`}`
`127`	`127`
`128`	`128`	`@Override`
`129`		`- public Long lessOrEquals(Long pNumber1, Long pNumber2) {`
	`129`	`+ protected Long lessOrEquals(Long pNumber1, Long pNumber2) {`
`130`	`130`	`return Native.mkLe(z3context, pNumber1, pNumber2);`
`131`	`131`	`}`
`132`	`132`	`}`