public void add ( final Formula formula ) { final Formula cnf = formula . cnf ( ) ; switch ( cnf . type ( ) ) { case TRUE : break ; case FALSE : case LITERAL : case OR : this . addClause ( generateClauseVector ( cnf ) , null ) ; break ; case AND : for ( final Formula op : cnf ) { this . addClause ( generateClauseVector ( op ) , null ) ; } break ; default : throw new IllegalStateException ( "Unexpected formula type in CNF: " + cnf . type ( ) ) ; } }
Adds an arbitrary formula to the solver .