diff --git a/src/main/java/leon/codegen/runtime/ArrayBox.java b/src/main/java/leon/codegen/runtime/ArrayBox.java deleted file mode 100644 index 0da4e64ca22a3430b6177483ddbd9a1c528d2692..0000000000000000000000000000000000000000 --- a/src/main/java/leon/codegen/runtime/ArrayBox.java +++ /dev/null @@ -1,83 +0,0 @@ -/* Copyright 2009-2016 EPFL, Lausanne */ - -package leon.codegen.runtime; - -import java.util.Arrays; - -public final class ArrayBox { - private final Object[] obj1; - private final int[] obj2; - private final boolean[] obj3; - private final int mode; - - protected final Object[] arrayValue() { - return obj1; - } - - protected final int[] arrayValueI() { - return obj2; - } - - protected final boolean[] arrayValueZ() { - return obj3; - } - - public ArrayBox(Object[] array) { - obj1 = array; - obj2 = null; - obj3 = null; - mode = 1; - } - - public ArrayBox(int[] array) { - obj1 = null; - obj2 = array; - obj3 = null; - mode = 2; - } - - public ArrayBox(boolean[] array) { - obj1 = null; - obj2 = null; - obj3 = array; - mode = 3; - } - - @Override - public boolean equals(Object that) { - if(that == this) return true; - if(!(that instanceof ArrayBox)) return false; - - ArrayBox other = (ArrayBox)that; - - if (mode == 1) { - return (other.mode == 1) && Arrays.equals(this.obj1, other.obj1); - } else if (mode == 2) { - return (other.mode == 2) && Arrays.equals(this.obj2, other.obj2); - } else { - return (other.mode == 3) && Arrays.equals(this.obj3, other.obj3); - } - } - - @Override - public String toString() { - if (mode == 1) { - return Arrays.toString(obj1); - } else if (mode == 2) { - return Arrays.toString(obj2); - } else { - return Arrays.toString(obj3); - } - } - - @Override - public int hashCode() { - if (mode == 1) { - return Arrays.hashCode(obj1); - } else if (mode == 2) { - return Arrays.hashCode(obj2); - } else { - return Arrays.hashCode(obj3); - } - } -} diff --git a/src/main/java/leon/codegen/runtime/Bag.java b/src/main/java/leon/codegen/runtime/Bag.java deleted file mode 100644 index e7404f522b8170523ff70e2a8e94059d05c1317b..0000000000000000000000000000000000000000 --- a/src/main/java/leon/codegen/runtime/Bag.java +++ /dev/null @@ -1,117 +0,0 @@ -/* Copyright 2009-2016 EPFL, Lausanne */ - -package leon.codegen.runtime; - -import java.util.Iterator; -import java.util.HashMap; - -/** If someone wants to make it an efficient implementation of immutable - * sets, go ahead. */ -public final class Bag { - private final HashMap<Object, BigInt> _underlying; - - protected final HashMap<Object, BigInt> underlying() { - return _underlying; - } - - public Bag() { - _underlying = new HashMap<Object, BigInt>(); - } - - private Bag(HashMap<Object, BigInt> u) { - _underlying = u; - } - - // Uses mutation! Useful at building time. - public void add(Object e) { - add(e, BigInt.ONE); - } - - // Uses mutation! Useful at building time. - public void add(Object e, BigInt count) { - _underlying.put(e, get(e).add(count)); - } - - public Iterator<java.util.Map.Entry<Object, BigInt>> getElements() { - return _underlying.entrySet().iterator(); - } - - public BigInt get(Object element) { - BigInt r = _underlying.get(element); - if (r == null) return BigInt.ZERO; - else return r; - } - - public Bag plus(Object e) { - Bag n = new Bag(new HashMap<Object, BigInt>(_underlying)); - n.add(e); - return n; - } - - public Bag union(Bag b) { - Bag n = new Bag(new HashMap<Object, BigInt>(_underlying)); - for (java.util.Map.Entry<Object, BigInt> entry : b.underlying().entrySet()) { - n.add(entry.getKey(), entry.getValue()); - } - return n; - } - - public Bag intersect(Bag b) { - Bag n = new Bag(); - for (java.util.Map.Entry<Object, BigInt> entry : _underlying.entrySet()) { - BigInt b1 = entry.getValue(), b2 = b.get(entry.getKey()); - BigInt m = b1.lessThan(b2) ? b1 : b2; - if (m.greaterThan(BigInt.ZERO)) n.add(entry.getKey(), m); - } - return n; - } - - public Bag difference(Bag b) { - Bag n = new Bag(); - for (java.util.Map.Entry<Object, BigInt> entry : _underlying.entrySet()) { - BigInt m = entry.getValue().sub(b.get(entry.getKey())); - if (m.greaterThan(BigInt.ZERO)) n.add(entry.getKey(), m); - } - return n; - } - - @Override - public boolean equals(Object that) { - if(that == this) return true; - if(!(that instanceof Bag)) return false; - - Bag other = (Bag) that; - for (Object key : _underlying.keySet()) { - if (!get(key).equals(other.get(key))) return false; - } - - for (Object key : other.underlying().keySet()) { - if (!get(key).equals(other.get(key))) return false; - } - - return true; - } - - @Override - public String toString() { - StringBuilder sb = new StringBuilder(); - sb.append("Bag("); - boolean first = true; - for (java.util.Map.Entry<Object, BigInt> entry : _underlying.entrySet()) { - if(!first) { - sb.append(", "); - first = false; - } - sb.append(entry.getKey().toString()); - sb.append(" -> "); - sb.append(entry.getValue().toString()); - } - sb.append(")"); - return sb.toString(); - } - - @Override - public int hashCode() { - return _underlying.hashCode(); - } -} diff --git a/src/main/java/leon/codegen/runtime/BigInt.java b/src/main/java/leon/codegen/runtime/BigInt.java deleted file mode 100644 index 338419c11b75c058576d6630071f19e282086e8c..0000000000000000000000000000000000000000 --- a/src/main/java/leon/codegen/runtime/BigInt.java +++ /dev/null @@ -1,92 +0,0 @@ -/* Copyright 2009-2016 EPFL, Lausanne */ - -package leon.codegen.runtime; - -import java.math.BigInteger; - -public final class BigInt { - public static final BigInt ZERO = new BigInt(BigInteger.ZERO); - public static final BigInt ONE = new BigInt(BigInteger.ONE); - - private final BigInteger _underlying; - - public final BigInteger underlying() { - return _underlying; - } - - private BigInt(BigInteger value) { - _underlying = value; - } - public BigInt(String value) { - _underlying = new BigInteger(value); - } - - public BigInt add(BigInt that) { - return new BigInt(_underlying.add(that.underlying())); - } - - public BigInt sub(BigInt that) { - return new BigInt(_underlying.subtract(that.underlying())); - } - - public BigInt mult(BigInt that) { - return new BigInt(_underlying.multiply(that.underlying())); - } - - public BigInt div(BigInt that) { - return new BigInt(_underlying.divide(that.underlying())); - } - - public BigInt rem(BigInt that) { - return new BigInt(_underlying.remainder(that.underlying())); - } - - public BigInt mod(BigInt that) { - if(that.underlying().compareTo(new BigInteger("0")) < 0) - return new BigInt(_underlying.mod(that.underlying().negate())); - else - return new BigInt(_underlying.mod(that.underlying())); - } - - public BigInt neg() { - return new BigInt(_underlying.negate()); - } - - - public boolean lessThan(BigInt that) { - return _underlying.compareTo(that.underlying()) < 0; - } - - public boolean lessEquals(BigInt that) { - return _underlying.compareTo(that.underlying()) <= 0; - } - - public boolean greaterThan(BigInt that) { - return _underlying.compareTo(that.underlying()) > 0; - } - - public boolean greaterEquals(BigInt that) { - return _underlying.compareTo(that.underlying()) >= 0; - } - - - @Override - public boolean equals(Object that) { - if(that == this) return true; - if(!(that instanceof BigInt)) return false; - - BigInt other = (BigInt)that; - return this.underlying().equals(other.underlying()); - } - - @Override - public String toString() { - return _underlying.toString(); - } - - @Override - public int hashCode() { - return _underlying.hashCode(); - } - -} diff --git a/src/main/java/leon/codegen/runtime/CaseClass.java b/src/main/java/leon/codegen/runtime/CaseClass.java deleted file mode 100644 index aeeb14a1bce2772366a96c6d3e89c8d9c31e1890..0000000000000000000000000000000000000000 --- a/src/main/java/leon/codegen/runtime/CaseClass.java +++ /dev/null @@ -1,11 +0,0 @@ -/* Copyright 2009-2016 EPFL, Lausanne */ - -package leon.codegen.runtime; - -public interface CaseClass { - int __getRead(); - - Object[] productElements(); - - String productName(); -} diff --git a/src/main/java/leon/codegen/runtime/FiniteLambda.java b/src/main/java/leon/codegen/runtime/FiniteLambda.java deleted file mode 100644 index fcdb340191923fe3f408484333171c242a946196..0000000000000000000000000000000000000000 --- a/src/main/java/leon/codegen/runtime/FiniteLambda.java +++ /dev/null @@ -1,44 +0,0 @@ -/* Copyright 2009-2015 EPFL, Lausanne */ - -package leon.codegen.runtime; - -import java.util.HashMap; - -public final class FiniteLambda extends Lambda { - public final HashMap<Tuple, Object> mapping = new HashMap<Tuple, Object>(); - public final Object dflt; - - public FiniteLambda(Object dflt) { - super(); - this.dflt = dflt; - } - - public void add(Tuple key, Object value) { - mapping.put(key, value); - } - - @Override - public Object apply(Object[] args) throws LeonCodeGenRuntimeException { - Tuple tuple = new Tuple(args); - if (mapping.containsKey(tuple)) { - return mapping.get(tuple); - } else { - return dflt; - } - } - - @Override - public boolean equals(Object that) { - if (that != null && (that instanceof FiniteLambda)) { - FiniteLambda l = (FiniteLambda) that; - return dflt.equals(l.dflt) && mapping.equals(l.mapping); - } else { - return false; - } - } - - @Override - public int hashCode() { - return 63 + 11 * mapping.hashCode() + (dflt == null ? 0 : dflt.hashCode()); - } -} diff --git a/src/main/java/leon/codegen/runtime/Lambda.java b/src/main/java/leon/codegen/runtime/Lambda.java deleted file mode 100644 index edb740d480f9619e0c4ec2620fa440efdbdd5f09..0000000000000000000000000000000000000000 --- a/src/main/java/leon/codegen/runtime/Lambda.java +++ /dev/null @@ -1,7 +0,0 @@ -/* Copyright 2009-2016 EPFL, Lausanne */ - -package leon.codegen.runtime; - -public abstract class Lambda { - public abstract Object apply(Object[] args) throws LeonCodeGenRuntimeException; -} diff --git a/src/main/java/leon/codegen/runtime/LeonCodeGenEvaluationException.java b/src/main/java/leon/codegen/runtime/LeonCodeGenEvaluationException.java deleted file mode 100644 index 69da9c5ea1d09a4311f7a68d8c09ac0bfa183d11..0000000000000000000000000000000000000000 --- a/src/main/java/leon/codegen/runtime/LeonCodeGenEvaluationException.java +++ /dev/null @@ -1,16 +0,0 @@ -/* Copyright 2009-2016 EPFL, Lausanne */ - -package leon.codegen.runtime; - -/** Such exceptions are thrown when the evaluator is asked to do something it - * cannot do, for instance evaluating a `choose` expression. It should be - * distinguished from `LeonCodeGenRuntimeException`s, which are thrown when - * the evaluator runs into a runtime error (.get on an undefined map, etc.). */ -public class LeonCodeGenEvaluationException extends Exception { - - private static final long serialVersionUID = -1824885944356173916L; - - public LeonCodeGenEvaluationException(String msg) { - super(msg); - } -} diff --git a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeException.java b/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeException.java deleted file mode 100644 index 63abf63a5f41fdbb5ed9edbb764d2b8a0e98f2e3..0000000000000000000000000000000000000000 --- a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeException.java +++ /dev/null @@ -1,14 +0,0 @@ -/* Copyright 2009-2016 EPFL, Lausanne */ - -package leon.codegen.runtime; - -/** Such exceptions are thrown when the evaluator encounters a runtime error, - * for instance `.get` with an undefined key on a map. */ -public class LeonCodeGenRuntimeException extends Exception { - - private static final long serialVersionUID = -8033159036464950965L; - - public LeonCodeGenRuntimeException(String msg) { - super(msg); - } -} diff --git a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeHashing.java b/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeHashing.java deleted file mode 100644 index feb40c3bd581055d8f65af336f83020e8be92201..0000000000000000000000000000000000000000 --- a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeHashing.java +++ /dev/null @@ -1,45 +0,0 @@ -/* Copyright 2009-2016 EPFL, Lausanne */ - -package leon.codegen.runtime; - -// MurmurHash3, reproduced from std. Scala lib. -public final class LeonCodeGenRuntimeHashing { - public static int seqHash(Object[] elements, int seed) { - // I feel good about this line. - int h = avalanche(seed ^ 0xcafebabe); - int sz = elements.length; - if(sz == 0) return h; - for (Object element : elements) { - h = mix(h, element.hashCode()); - } - return finalizeHash(h, sz); - } - - private static int mix(int hash, int data) { - int h = mixLast(hash, data); - h = Integer.rotateLeft(h, 13); - return h * 5 + 0xe6546b64; - } - - private static int mixLast(int hash, int data) { - int k = data; - k *= 0xcc9e2d51; - k = Integer.rotateLeft(k, 15); - k *= 0x1b873593; - return hash ^ k; - } - - private static int finalizeHash(int hash, int length) { - return avalanche(hash ^ length); - } - - private static int avalanche(int hash) { - int h = hash; - h ^= h >>> 16; - h *= 0x85ebca6b; - h ^= h >>> 13; - h *= 0xc2b2ae35; - h ^= h >>> 16; - return h; - } -} diff --git a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeMonitor.java b/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeMonitor.java deleted file mode 100644 index c89d49705d028ffd23965d7512ac85de0f851716..0000000000000000000000000000000000000000 --- a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeMonitor.java +++ /dev/null @@ -1,21 +0,0 @@ -/* Copyright 2009-2016 EPFL, Lausanne */ - -package leon.codegen.runtime; - -/** Such exceptions are thrown when the evaluator encounters a runtime error, - * for instance `.get` with an undefined key on a map. */ -public class LeonCodeGenRuntimeMonitor { - private int invocationsLeft; - - public LeonCodeGenRuntimeMonitor(int maxInvocations) { - this.invocationsLeft = maxInvocations; - } - - public void onInvoke() throws LeonCodeGenEvaluationException { - if(invocationsLeft > 0) { - invocationsLeft--; - } else if(invocationsLeft == 0) { - throw new LeonCodeGenEvaluationException("Maximum number of invocations reached."); - } - } -} diff --git a/src/main/java/leon/codegen/runtime/Map.java b/src/main/java/leon/codegen/runtime/Map.java deleted file mode 100644 index 19c94b4c2a331f3fe5b7d14f77358fb7f5147f1a..0000000000000000000000000000000000000000 --- a/src/main/java/leon/codegen/runtime/Map.java +++ /dev/null @@ -1,95 +0,0 @@ -/* Copyright 2009-2016 EPFL, Lausanne */ - -package leon.codegen.runtime; - -import java.util.Iterator; -import java.util.HashMap; - -/** If someone wants to make it an efficient implementation of immutable - * maps, go ahead. */ -public final class Map { - private final HashMap<Object,Object> _underlying; - - protected final HashMap<Object,Object> underlying() { - return _underlying; - } - - public Map() { - _underlying = new HashMap<Object,Object>(); - } - - private Map(HashMap<Object,Object> u) { - _underlying = u; - } - - // Uses mutation! Useful at building time. - public void add(Object key, Object value) { - _underlying.put(key, value); - } - - public Iterator<java.util.Map.Entry<Object,Object>> getElements() { - return _underlying.entrySet().iterator(); - } - - public boolean isDefinedAt(Object element) { - return _underlying.containsKey(element); - } - - public Object get(Object k) throws LeonCodeGenRuntimeException { - Object result = _underlying.get(k); - if(result == null) { - throw new LeonCodeGenRuntimeException("Get of undefined key."); - } - return result; - } - - public int size() { - return _underlying.size(); - } - - public Map union(Map s) { - HashMap<Object,Object> n = new HashMap<Object,Object>(_underlying); - n.putAll(s.underlying()); - return new Map(n); - } - - @Override - public boolean equals(Object that) { - if(that == this) return true; - if(!(that instanceof Map)) return false; - - Map other = (Map)that; - - if(this.size() != other.size()) return false; - - for(java.util.Map.Entry<Object,Object> entry : _underlying.entrySet()) { - Object there = other.underlying().get(entry.getKey()); - if(there == null || !entry.getValue().equals(there)) return false; - } - - return true; - } - - @Override - public String toString() { - StringBuilder sb = new StringBuilder(); - sb.append("Map("); - boolean first = true; - for(java.util.Map.Entry<Object,Object> entry : _underlying.entrySet()) { - if(!first) { - sb.append(", "); - first = false; - } - sb.append(entry.getKey().toString()); - sb.append(" -> "); - sb.append(entry.getValue().toString()); - } - sb.append(")"); - return sb.toString(); - } - - @Override - public int hashCode() { - return _underlying.hashCode(); - } -} diff --git a/src/main/java/leon/codegen/runtime/Rational.java b/src/main/java/leon/codegen/runtime/Rational.java deleted file mode 100644 index 2d09905d4839edbc97233f217f685b3d04f79178..0000000000000000000000000000000000000000 --- a/src/main/java/leon/codegen/runtime/Rational.java +++ /dev/null @@ -1,127 +0,0 @@ -/* Copyright 2009-2016 EPFL, Lausanne */ - -package leon.codegen.runtime; - -import java.math.BigInteger; - -public final class Rational { - - private final BigInteger _num; - private final BigInteger _denom; - - /** - * class invariant: the fractions are always normalized - * - * @param num - * numerator - * @param denom - * denominator - */ - public Rational(BigInteger num, BigInteger denom) { - BigInteger modNum = num.abs(); - BigInteger modDenom = denom.abs(); - BigInteger divisor = modNum.gcd(modDenom); - BigInteger simpNum = num.divide(divisor); - BigInteger simpDenom = denom.divide(divisor); - if (isLTZ(simpDenom)) { - _num = simpNum.negate(); - _denom = simpDenom.negate(); - } else { - _num = simpNum; - _denom = simpDenom; - } - } - - public Rational(String num, String denom) { - this(new BigInteger(num), new BigInteger(denom)); - } - - public BigInteger numerator() { - return _num; - } - - public BigInteger denominator() { - return _denom; - } - - public boolean isZero(BigInteger bi) { - return bi.signum() == 0; - } - - public boolean isLEZ(BigInteger bi) { - return bi.signum() != 1; - } - - public boolean isLTZ(BigInteger bi) { - return (bi.signum() == -1); - } - - public boolean isGEZ(BigInteger bi) { - return (bi.signum() != -1); - } - - public boolean isGTZ(BigInteger bi) { - return (bi.signum() == 1); - } - - public Rational add(Rational that) { - return new Rational(_num.multiply(that._denom).add( - that._num.multiply(_denom)), _denom.multiply(that._denom)); - } - - public Rational sub(Rational that) { - return new Rational(_num.multiply(that._denom).subtract( - that._num.multiply(_denom)), _denom.multiply(that._denom)); - } - - public Rational mult(Rational that) { - return new Rational(_num.multiply(that._num), - _denom.multiply(that._denom)); - } - - public Rational div(Rational that) { - return new Rational(_num.multiply(that._denom), - _denom.multiply(that._num)); - } - - public Rational neg() { - return new Rational(_num.negate(), _denom); - } - - public boolean lessThan(Rational that) { - return isLTZ(this.sub(that)._num); - } - - public boolean lessEquals(Rational that) { - return isLEZ(this.sub(that)._num); - } - - public boolean greaterThan(Rational that) { - return isGTZ(this.sub(that)._num); - } - - public boolean greaterEquals(Rational that) { - return isGEZ(this.sub(that)._num); - } - - @Override - public boolean equals(Object that) { - if (that == this) - return true; - if (!(that instanceof Rational)) - return false; - - Rational other = (Rational) that; - return isZero(this.sub(other)._num); - } - - @Override - public String toString() { - return _num.toString() + "/" + _denom.toString(); - } - - @Override - public int hashCode() { - return _num.hashCode() ^ _denom.hashCode(); - } -} diff --git a/src/main/java/leon/codegen/runtime/Real.java b/src/main/java/leon/codegen/runtime/Real.java deleted file mode 100644 index 84aefb2419ef01f308461c8c9f10c0cf73871b8d..0000000000000000000000000000000000000000 --- a/src/main/java/leon/codegen/runtime/Real.java +++ /dev/null @@ -1,81 +0,0 @@ -/* Copyright 2009-2016 EPFL, Lausanne */ - -package leon.codegen.runtime; - -import java.math.BigInteger; -import java.math.BigDecimal; - -public final class Real { - - private final BigDecimal _underlying; - - public final BigDecimal underlying() { - return _underlying; - } - - private Real(BigDecimal value) { - _underlying = value; - } - - public Real(String value) { - _underlying = new BigDecimal(value); - } - - public Real add(Real that) { - return new Real(_underlying.add(that.underlying())); - } - - public Real sub(Real that) { - return new Real(_underlying.subtract(that.underlying())); - } - - public Real mult(Real that) { - return new Real(_underlying.multiply(that.underlying())); - } - - public Real div(Real that) { - return new Real(_underlying.divide(that.underlying())); - } - - public Real neg() { - return new Real(_underlying.negate()); - } - - - public boolean lessThan(Real that) { - return _underlying.compareTo(that.underlying()) < 0; - } - - public boolean lessEquals(Real that) { - return _underlying.compareTo(that.underlying()) <= 0; - } - - public boolean greaterThan(Real that) { - return _underlying.compareTo(that.underlying()) > 0; - } - - public boolean greaterEquals(Real that) { - return _underlying.compareTo(that.underlying()) >= 0; - } - - - @Override - public boolean equals(Object that) { - if(that == this) return true; - if(!(that instanceof Real)) return false; - - Real other = (Real)that; - return this.underlying().equals(other.underlying()); - } - - @Override - public String toString() { - return _underlying.toString(); - } - - @Override - public int hashCode() { - return _underlying.hashCode(); - } - -} diff --git a/src/main/java/leon/codegen/runtime/Set.java b/src/main/java/leon/codegen/runtime/Set.java deleted file mode 100644 index c361ba9e662a5b84bbd84391c856ab9853d66860..0000000000000000000000000000000000000000 --- a/src/main/java/leon/codegen/runtime/Set.java +++ /dev/null @@ -1,116 +0,0 @@ -/* Copyright 2009-2016 EPFL, Lausanne */ - -package leon.codegen.runtime; - -import java.util.Arrays; -import java.util.Iterator; -import java.util.HashSet; - -/** If someone wants to make it an efficient implementation of immutable - * sets, go ahead. */ -public final class Set { - private final HashSet<Object> _underlying; - - protected final HashSet<Object> underlying() { - return _underlying; - } - - public Set() { - _underlying = new HashSet<Object>(); - } - - public Set(Object[] elements) { - _underlying = new HashSet<Object>(Arrays.asList(elements)); - } - - private Set(HashSet<Object> u) { - _underlying = u; - } - - // Uses mutation! Useful at building time. - public void add(Object e) { - _underlying.add(e); - } - - public Iterator<Object> getElements() { - return _underlying.iterator(); - } - - public boolean contains(Object element) { - return _underlying.contains(element); - } - - public Set plus(Object e) { - Set n = new Set(new HashSet<Object>(_underlying)); - n.add(e); - return n; - } - - public boolean subsetOf(Set s) { - for(Object o : _underlying) { - if(!s.underlying().contains(o)) { - return false; - } - } - return true; - } - - public BigInt size() { - return new BigInt(""+_underlying.size()); - } - - public Set union(Set s) { - HashSet<Object> n = new HashSet<Object>(_underlying); - n.addAll(s.underlying()); - return new Set(n); - } - - public Set intersect(Set s) { - HashSet<Object> n = new HashSet<Object>(); - for(Object o : _underlying) { - if(s.underlying().contains(o)) { - n.add(o); - } - } - return new Set(n); - } - - public Set minus(Set s) { - HashSet<Object> n = new HashSet<Object>(_underlying); - for(Object o : s.underlying()) { - n.remove(o); - } - return new Set(n); - } - - @Override - public boolean equals(Object that) { - if(that == this) return true; - if(!(that instanceof Set)) return false; - - Set other = (Set)that; - - return this.size().equals(other.size()) && this.subsetOf(other); - } - - @Override - public String toString() { - StringBuilder sb = new StringBuilder(); - sb.append("Set("); - boolean first = true; - for(Object o : _underlying) { - if(!first) { - sb.append(", "); - first = false; - } - sb.append(o.toString()); - } - sb.append(")"); - return sb.toString(); - } - - @Override - public int hashCode() { - return _underlying.hashCode(); - } -} diff --git a/src/main/java/leon/codegen/runtime/StrOps.java b/src/main/java/leon/codegen/runtime/StrOps.java deleted file mode 100644 index 9f97e37a535b230386095fe0f37ad62d1ec59bf7..0000000000000000000000000000000000000000 --- a/src/main/java/leon/codegen/runtime/StrOps.java +++ /dev/null @@ -1,50 +0,0 @@ -/* Copyright 2009-2016 EPFL, Lausanne */ - -package leon.codegen.runtime; - -import org.apache.commons.lang3.StringEscapeUtils; - -public class StrOps { - public static String concat(String a, String b) { - return a + b; - } - - public static BigInt bigLength(String a) { - return new BigInt(a.length() + ""); - } - - public static String bigSubstring(String s, BigInt start, BigInt end) { - return s.substring(Integer.parseInt(start.toString()), Integer.parseInt(end.toString())); - } - - public static String bigIntToString(BigInt a) { - return a.toString(); - } - - public static String intToString(int a) { - return String.valueOf(a); - } - - public static String doubleToString(double a) { - return String.valueOf(a); - } - - public static String booleanToString(boolean a) { - if (a) - return "true"; - else - return "false"; - } - - public static String charToString(char a) { - return String.valueOf(a); - } - - public static String realToString(Real a) { - return ""; // TODO: Not supported at this moment. - } - - public static String escape(String s) { - return StringEscapeUtils.escapeJava(s); - } -} diff --git a/src/main/java/leon/codegen/runtime/Tuple.java b/src/main/java/leon/codegen/runtime/Tuple.java deleted file mode 100644 index 0b0405f04e61971a6ea0fe36f1d99b0b3646fe58..0000000000000000000000000000000000000000 --- a/src/main/java/leon/codegen/runtime/Tuple.java +++ /dev/null @@ -1,73 +0,0 @@ -/* Copyright 2009-2016 EPFL, Lausanne */ - -package leon.codegen.runtime; - -import java.util.Arrays; - -public final class Tuple { - private int __read = 0; - - public final int __getRead() { - return __read; - } - - private final Object[] elements; - - // You may think that using varargs here would show less of the internals, - // however the bytecode is exactly the same, so let's reflect the reality - // instead. - public Tuple(Object[] elements) { - this.elements = Arrays.copyOf(elements, elements.length); - } - - public final Object get(int index) { - if(index < 0 || index >= this.elements.length) { - throw new IllegalArgumentException("Invalid tuple index : " + index); - } - __read = (1 << (index)) | __read; - - return this.elements[index]; - } - - public final int getArity() { - return this.elements.length; - } - - @Override - public boolean equals(Object that) { - if(that == this) return true; - if(!(that instanceof Tuple)) return false; - Tuple other = (Tuple)that; - if(other.getArity() != this.getArity()) return false; - for(int i = 0; i < this.getArity(); i++) { - if(!other.get(i).equals(this.get(i))) return false; - } - return true; - } - - private int _hash = 0; - @Override - final public int hashCode() { - if(_hash != 0) return _hash; - int seed = ("Tuple" + getArity()).hashCode(); - int h = LeonCodeGenRuntimeHashing.seqHash(elements, seed); - _hash = h; - return h; - } - - @Override - public String toString() { - String str = "("; - boolean first = true; - for (Object obj : elements) { - if (first) { - first = false; - } else { - str += ", "; - } - str += obj == null ? "null" : obj.toString(); - } - str += ")"; - return str; - } -}