PolyBase extends AbstractPoly { @Override public PolyBase add(AbstractPoly x) { BiFunction<BigFraction, BigFraction, BigFraction> add = (lhs,rhs) -> lhs.add(rhs); return binaryOpGen(add,x); } PolyBase();  PolyBase(VariableID x);  PolyBase(BigFraction constant);  PolyBase(BigFraction coeff, VariableID x);  PolyBase(Map<VariableID,BigFraction> coefficientsIn);  PolyBase(Map<VariableID,BigFraction> coefficientsIn, BigFraction constant); @Override Iterator<VariableID> iterator(); @Override PolyBase solveFor(VariableID x); @Override BigFraction getCoefficient(VariableID x); @Override PolyBase negate(); @Override PolyBase add(AbstractPoly x); @Override PolyBase add(BigFraction val); @Override PolyBase subtract(AbstractPoly x); @Override PolyBase subtract(BigFraction val); @Override PolyBase multiply(BigFraction c); @Override PolyBase divide(BigFraction v); @Override boolean isConstant(); @Override BigFraction getConstant(); @Override VariableID leadingVariable(); @Override VariableID trailingVariable(); @Override String toString(); @Override String cexString(); @Override boolean equals(Object obj); @Override BigFraction evaluateCEX(); @Override RegionBounds polyBounds(Map<VariableID, RegionBounds> bounds); @Override BigFraction evaluate(Map<VariableID, BigFraction> bounds); @Override AbstractPoly div(BigInteger d); @Override boolean divisible(BigInteger d); static PolyBase qpoly(BigInteger Q, VariableID k, VariableID m); @Override AbstractPoly rewrite(Map<VariableID, AbstractPoly> rw); @Override String toACL2(); @Override Set<VariableID> updateVariableSet(Set<VariableID> in); @Override BigInteger leastCommonDenominator(); @Override BigInteger constantLCDContribution(); @Override AbstractPoly remove(VariableID x); @Override BigFraction dot(AbstractPoly arg); @Override int compareTo(AbstractPoly arg); @Override AbstractPoly remove(AbstractPoly x); @Override Set<VariableID> getVariables();  }
@Test public void testAdd() { VariableID y = VariableID.principleAlloc("Y", NamedType.REAL,BigFraction.ONE); VariableID x = VariableID.principleAlloc("X",NamedType.REAL,BigFraction.ZERO); Map<VariableID,BigFraction> coefs = new HashMap<VariableID,BigFraction>(); coefs.put(x, BigFraction.valueOf(BigDecimal.valueOf(2))); PolyBase poly1 = new PolyBase(coefs,BigFraction.ONE); System.out.println("poly1: " + poly1); Map<VariableID,BigFraction> coefs2 = new HashMap<VariableID,BigFraction>(); coefs2.put(x, BigFraction.valueOf(BigDecimal.valueOf(5))); coefs2.put(y, BigFraction.valueOf(BigDecimal.valueOf(4))); PolyBase poly2 = new PolyBase(coefs2,BigFraction.valueOf(BigDecimal.valueOf(40))); System.out.println("poly2: " + poly2); AbstractPoly polyadd = poly1.add(poly2); System.out.println("poly1 + poly2: " + polyadd); AbstractPoly polyaddsub = polyadd.subtract(poly2); System.out.println("poly1 + poly2 - poly2: " + polyaddsub); AbstractPoly polysub = poly1.subtract(poly1); System.out.println("poly1 - poly1: " + polysub); AbstractPoly polyaddneg = poly1.add(poly1.negate()); System.out.println("poly1 + (-poly1): " + polyaddneg); System.out.println("poly2 * 3: " + poly2.multiply(BigFraction.valueOf(BigDecimal.valueOf(3)))); PolyBase emptyPoly = new PolyBase(); Map<VariableID,BigFraction> zerocoefs = new HashMap<VariableID,BigFraction>(); PolyBase constZeroPoly = new PolyBase(zerocoefs,BigFraction.ZERO); Map<VariableID,BigFraction> constFourCoef = new HashMap<VariableID,BigFraction>(); PolyBase constFourPoly = new PolyBase(constFourCoef,BigFraction.valueOf(BigDecimal.valueOf(4))); Map<VariableID,BigFraction> negHalfCoef = new HashMap<VariableID,BigFraction>(); BigFraction negHalf = new BigFraction(BigInteger.valueOf(-1),BigInteger.valueOf(2)); PolyBase constNegHalfPoly = new PolyBase(negHalfCoef,negHalf); System.out.println("poly1 - constFour: " + poly1.subtract(constFourPoly)); System.out.println("poly1 solved for x: " + poly1.solveFor(x)); System.out.println("poly2 solved for x: " + poly2.solveFor(x)); System.out.println("poly2 solved for y: " + poly2.solveFor(y)); System.out.println("(poly1 - constFour) solved for x: " + poly1.subtract(constFourPoly).solveFor(x)); System.out.println("evaluate poly1(x is ZERO by default): " + poly1.evaluateCEX()); Map<VariableID,BigFraction> coefsCex1 = new HashMap<VariableID,BigFraction>(); coefsCex1.put(y, BigFraction.valueOf(BigDecimal.valueOf(2))); PolyBase poly1Cex1 = new PolyBase(coefsCex1,BigFraction.ONE); System.out.println("evaluate poly1Cex1: " + poly1Cex1.evaluateCEX()); x.setCex(new BigFraction(BigInteger.valueOf(2))); System.out.println("evaluate poly2: " + poly2.evaluateCEX()); assertEquals(poly1,polyaddsub); assertEquals(emptyPoly,polysub); assertEquals(emptyPoly,polyaddneg); assertEquals(emptyPoly,constZeroPoly); assertEquals(constNegHalfPoly, poly1.solveFor(x)); }