Valuation implements Substitution { public boolean isLeq(final Valuation that) { if (that.getDecls().size() > this.getDecls().size()) { return false; } for (final Decl<?> varDecl : that.getDecls()) { if (!that.eval(varDecl).equals(this.eval(varDecl))) { return false; } } return true; }  @Override abstract Optional<LitExpr<DeclType>> eval(final Decl<DeclType> decl); abstract Map<Decl<?>, LitExpr<?>> toMap(); Expr<BoolType> toExpr(); boolean isLeq(final Valuation that); @Override int hashCode(); @Override boolean equals(final Object obj); @Override String toString();  }
@Test public void testLeq() { final Valuation v1 = ImmutableValuation.builder().put(ca, Int(1)).build(); final Valuation v2 = ImmutableValuation.builder().put(ca, Int(2)).build(); final Valuation v3 = ImmutableValuation.builder().put(cb, Int(1)).build(); final Valuation v4 = ImmutableValuation.builder().put(ca, Int(1)).put(cb, Int(1)).build(); Assert.assertTrue(v1.isLeq(v1)); Assert.assertFalse(v2.isLeq(v1)); Assert.assertFalse(v3.isLeq(v1)); Assert.assertTrue(v4.isLeq(v1)); Assert.assertFalse(v1.isLeq(v2)); Assert.assertTrue(v2.isLeq(v2)); Assert.assertFalse(v3.isLeq(v2)); Assert.assertFalse(v4.isLeq(v2)); Assert.assertFalse(v1.isLeq(v3)); Assert.assertFalse(v2.isLeq(v3)); Assert.assertTrue(v3.isLeq(v3)); Assert.assertTrue(v4.isLeq(v3)); Assert.assertFalse(v1.isLeq(v4)); Assert.assertFalse(v2.isLeq(v4)); Assert.assertFalse(v3.isLeq(v4)); Assert.assertTrue(v4.isLeq(v4)); }