@Test public void testSatAssignmentToLong() { BDDInteger dstIp = new BDDPacket().getDstIp(); long value = 12345; BDD bdd = dstIp.value(value); assertThat(dstIp.getValueSatisfying(bdd), equalTo(Optional.of(value))); value = 0xFFFFFFFFL; bdd = dstIp.value(value); assertThat(dstIp.getValueSatisfying(bdd), equalTo(Optional.of(value))); }
public Long satAssignmentToLong(BDD satAssignment) { checkArgument(satAssignment.isAssignment(), "not a satisfying assignment"); if (_hasVariablesOnly) { return satAssignmentToLong(satAssignment.minAssignmentBits()); } if (_bitvec.length > Long.SIZE) { throw new IllegalArgumentException( "Can't get a representative of a BDDInteger with more than Long.SIZE bits"); } long value = 0; for (int i = 0; i < _bitvec.length; i++) { BDD bitBDD = _bitvec[_bitvec.length - i - 1]; if (!satAssignment.diffSat(bitBDD)) { value |= 1L << i; } } return value; }
BDDInteger { public Long satAssignmentToLong(BDD satAssignment) { checkArgument(satAssignment.isAssignment(), "not a satisfying assignment"); if (_hasVariablesOnly) { return satAssignmentToLong(satAssignment.minAssignmentBits()); } if (_bitvec.length > Long.SIZE) { throw new IllegalArgumentException( "Can't get a representative of a BDDInteger with more than Long.SIZE bits"); } long value = 0; for (int i = 0; i < _bitvec.length; i++) { BDD bitBDD = _bitvec[_bitvec.length - i - 1]; if (!satAssignment.diffSat(bitBDD)) { value |= 1L << i; } } return value; } }
BDDInteger { public Long satAssignmentToLong(BDD satAssignment) { checkArgument(satAssignment.isAssignment(), "not a satisfying assignment"); if (_hasVariablesOnly) { return satAssignmentToLong(satAssignment.minAssignmentBits()); } if (_bitvec.length > Long.SIZE) { throw new IllegalArgumentException( "Can't get a representative of a BDDInteger with more than Long.SIZE bits"); } long value = 0; for (int i = 0; i < _bitvec.length; i++) { BDD bitBDD = _bitvec[_bitvec.length - i - 1]; if (!satAssignment.diffSat(bitBDD)) { value |= 1L << i; } } return value; } private  BDDInteger(BDDFactory factory, int length);  BDDInteger(BDDInteger other); }
BDDInteger { public Long satAssignmentToLong(BDD satAssignment) { checkArgument(satAssignment.isAssignment(), "not a satisfying assignment"); if (_hasVariablesOnly) { return satAssignmentToLong(satAssignment.minAssignmentBits()); } if (_bitvec.length > Long.SIZE) { throw new IllegalArgumentException( "Can't get a representative of a BDDInteger with more than Long.SIZE bits"); } long value = 0; for (int i = 0; i < _bitvec.length; i++) { BDD bitBDD = _bitvec[_bitvec.length - i - 1]; if (!satAssignment.diffSat(bitBDD)) { value |= 1L << i; } } return value; } private  BDDInteger(BDDFactory factory, int length);  BDDInteger(BDDInteger other); boolean hasVariablesOnly(); int size(); static BDDInteger makeFromIndex(
      BDDFactory factory, int length, int start, boolean reverse); Optional<Long> getValueSatisfying(BDD bdd); Long satAssignmentToLong(BDD satAssignment); Long satAssignmentToLong(BitSet bits); List<Long> getValuesSatisfying(BDD bdd, int max); static BDDInteger makeFromValue(BDDFactory factory, int length, long value); BDDInteger ite(BDD b, BDDInteger other); BDD value(long val); BDD leq(long val); BDD geq(long val); BDD range(long a, long b); void setValue(long val); void setValue(BDDInteger other); BDDInteger add(BDDInteger other); BDDInteger sub(BDDInteger var1); BDD[] getBitvec(); @Nonnull BDD getVars(); BDDFactory getFactory(); @Override boolean equals(Object o); @Override int hashCode(); }
BDDInteger { public Long satAssignmentToLong(BDD satAssignment) { checkArgument(satAssignment.isAssignment(), "not a satisfying assignment"); if (_hasVariablesOnly) { return satAssignmentToLong(satAssignment.minAssignmentBits()); } if (_bitvec.length > Long.SIZE) { throw new IllegalArgumentException( "Can't get a representative of a BDDInteger with more than Long.SIZE bits"); } long value = 0; for (int i = 0; i < _bitvec.length; i++) { BDD bitBDD = _bitvec[_bitvec.length - i - 1]; if (!satAssignment.diffSat(bitBDD)) { value |= 1L << i; } } return value; } private  BDDInteger(BDDFactory factory, int length);  BDDInteger(BDDInteger other); boolean hasVariablesOnly(); int size(); static BDDInteger makeFromIndex(
      BDDFactory factory, int length, int start, boolean reverse); Optional<Long> getValueSatisfying(BDD bdd); Long satAssignmentToLong(BDD satAssignment); Long satAssignmentToLong(BitSet bits); List<Long> getValuesSatisfying(BDD bdd, int max); static BDDInteger makeFromValue(BDDFactory factory, int length, long value); BDDInteger ite(BDD b, BDDInteger other); BDD value(long val); BDD leq(long val); BDD geq(long val); BDD range(long a, long b); void setValue(long val); void setValue(BDDInteger other); BDDInteger add(BDDInteger other); BDDInteger sub(BDDInteger var1); BDD[] getBitvec(); @Nonnull BDD getVars(); BDDFactory getFactory(); @Override boolean equals(Object o); @Override int hashCode();  }