private void addClauseSetWithRelaxation ( final Variable relaxationVar , final Formula formula ) { switch ( formula . type ( ) ) { case TRUE : break ; case FALSE : case LITERAL : case OR : this . addClauseWithRelaxation ( relaxationVar , formula ) ; break ; case AND : for ( final Formula op : formula ) { this . addClauseWithRelaxation ( relaxationVar , op ) ; } break ; default : throw new IllegalArgumentException ( "Input formula ist not a valid CNF: " + formula ) ; } }
Adds a formula which is already in CNF with a given relaxation to the solver .