mirror of
				https://github.com/YosysHQ/yosys
				synced 2025-11-03 21:09:12 +00:00 
			
		
		
		
	Improved non-verbose ezSAT::printDIMACS() format
This commit is contained in:
		
							parent
							
								
									13051e6acf
								
							
						
					
					
						commit
						61a2bf57b4
					
				
					 1 changed files with 6 additions and 1 deletions
				
			
		| 
						 | 
				
			
			@ -1131,10 +1131,15 @@ void ezSAT::printDIMACS(FILE *f, bool verbose) const
 | 
			
		|||
	int maxClauseLen = 0;
 | 
			
		||||
	for (auto &clause : cnfClauses)
 | 
			
		||||
		maxClauseLen = std::max(int(clause.size()), maxClauseLen);
 | 
			
		||||
	if (!verbose)
 | 
			
		||||
		maxClauseLen = std::min(maxClauseLen, 3);
 | 
			
		||||
	for (auto &clause : cnfClauses) {
 | 
			
		||||
		for (auto idx : clause)
 | 
			
		||||
			fprintf(f, " %*d", digits, idx);
 | 
			
		||||
		fprintf(f, " %*d\n", (digits + 1)*int(maxClauseLen - clause.size()) + digits, 0);
 | 
			
		||||
		if (maxClauseLen >= int(clause.size()))
 | 
			
		||||
			fprintf(f, " %*d\n", (digits + 1)*int(maxClauseLen - clause.size()) + digits, 0);
 | 
			
		||||
		else
 | 
			
		||||
			fprintf(f, " %*d\n", digits, 0);
 | 
			
		||||
	}
 | 
			
		||||
}
 | 
			
		||||
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue