public ImmutableFormulaList encode ( final PBConstraint constraint ) { if ( constraint . isCC ( ) ) return this . ccEncoder . encode ( constraint ) ; final Formula normalized = constraint . normalize ( ) ; switch ( normalized . type ( ) ) { case TRUE : return new ImmutableFormulaList ( FType . AND ) ; case FALSE : return new ImmutableFormulaList ( FType . AND , this . f . falsum ( ) ) ; case PBC : final PBConstraint pbc = ( PBConstraint ) normalized ; if ( pbc . isCC ( ) ) return this . ccEncoder . encode ( pbc ) ; return new ImmutableFormulaList ( FType . AND , this . encode ( pbc . operands ( ) , pbc . coefficients ( ) , pbc . rhs ( ) ) ) ; case AND : final List < Formula > list = new LinkedList <> ( ) ; for ( final Formula op : normalized ) { switch ( op . type ( ) ) { case FALSE : return new ImmutableFormulaList ( FType . AND , this . f . falsum ( ) ) ; case PBC : list . addAll ( this . encode ( ( PBConstraint ) op ) . toList ( ) ) ; break ; default : throw new IllegalArgumentException ( "Illegal return value of PBConstraint.normalize" ) ; } } return new ImmutableFormulaList ( FType . AND , list ) ; default : throw new IllegalArgumentException ( "Illegal return value of PBConstraint.normalize" ) ; } }
Encodes a pseudo - Boolean constraint and returns its CNF encoding .