001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 package escjava.pa.generic; 004 005 import javafe.util.*; 006 007 /* Represents a clause (disjunction of literals) over up to 64 variables. 008 Clause represented by low bits in "stars" and "bits". 009 "stars" has a 1 in bit n if variable n is not mentioned in clause. 010 If "stars" has a 0 in bit n then variable n is mentioned in clause, and 011 its sign is given by bit n of "bits". 012 */ 013 public class Disjunction { 014 public long stars; 015 public long bits; 016 017 public Disjunction(long stars, long bits) { 018 Assert.notFalse( (stars & bits) == 0 ); 019 this.stars = stars; 020 this.bits = bits; 021 } 022 public Disjunction(/*@ non_null @*/ Disjunction d) { 023 this( d.stars, d.bits); 024 } 025 // Yields Disjunction for false 026 public Disjunction() { 027 this( -1L, 0L); 028 } 029 public /*@ non_null @*/ String toString() { 030 return "("+Long.toBinaryString(stars)+","+Long.toBinaryString(bits)+")"; 031 } 032 public boolean equals(Object o) { 033 if( o instanceof Disjunction ) { 034 Disjunction d = (Disjunction)o; 035 return d.stars == stars && d.bits == bits; 036 } else { 037 return false; 038 } 039 } 040 }