ezsat: Support for assumptions in Sat command

YosysHQ · Apr 9, 2024 · c807ef4 · c807ef4
1 parent d62a47b
commit c807ef4
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 8 deletions.
diff --git a/libs/ezsat/ezcommand.cc b/libs/ezsat/ezcommand.cc
@@ -9,19 +9,20 @@ ezSATCommand::~ezSATCommand() {}
 
 bool ezSATCommand::solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions)
 {
-	if (!assumptions.empty()) {
-		Yosys::log_error("Assumptions are not supported yet by command-based Sat solver\n");
-	}
 	const std::string tempdir_name = Yosys::make_temp_dir(Yosys::get_base_tmpdir() + "/yosys-sat-XXXXXX");
 	const std::string cnf_filename = Yosys::stringf("%s/problem.cnf", tempdir_name.c_str());
 	const std::string sat_command = Yosys::stringf("%s %s", command.c_str(), cnf_filename.c_str());
 	FILE *dimacs = fopen(cnf_filename.c_str(), "w");
-	printDIMACS(dimacs);
-	fclose(dimacs);
 
 	std::vector<int> modelIdx;
 	for (auto id : modelExpressions)
 		modelIdx.push_back(bind(id));
+	std::vector<std::vector<int>> extraClauses;
+	for (auto id : assumptions)
+		extraClauses.push_back({bind(id)});
+
+	printDIMACS(dimacs, false, extraClauses);
+	fclose(dimacs);
 
 	bool status_sat = false;
 	bool status_unsat = false;

diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
@@ -1222,7 +1222,7 @@ ezSATvec ezSAT::vec(const std::vector<int> &vec)
 	return ezSATvec(*this, vec);
 }
 
-void ezSAT::printDIMACS(FILE *f, bool verbose) const
+void ezSAT::printDIMACS(FILE *f, bool verbose, const std::vector<std::vector<int>> &extraClauses) const
 {
 	if (cnfConsumed) {
 		fprintf(stderr, "Usage error: printDIMACS() must not be called after cnfConsumed()!");
@@ -1259,8 +1259,10 @@ void ezSAT::printDIMACS(FILE *f, bool verbose) const
 	std::vector<std::vector<int>> all_clauses;
 	getFullCnf(all_clauses);
 	assert(cnfClausesCount == int(all_clauses.size()));
+	for (auto c : extraClauses)
+		all_clauses.push_back(c);
 
-	fprintf(f, "p cnf %d %d\n", cnfVariableCount, cnfClausesCount);
+	fprintf(f, "p cnf %d %d\n", cnfVariableCount, (int) all_clauses.size());
 	int maxClauseLen = 0;
 	for (auto &clause : all_clauses)
 		maxClauseLen = std::max(int(clause.size()), maxClauseLen);

diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h
@@ -295,7 +295,7 @@ class ezSAT
 
 	// printing CNF and internal state
 
-	void printDIMACS(FILE *f, bool verbose = false) const;
+	void printDIMACS(FILE *f, bool verbose = false, const std::vector<std::vector<int>> &extraClauses = std::vector<std::vector<int>>()) const;
 	void printInternalState(FILE *f) const;
 
 	// more sophisticated constraints (designed to be used directly with assume(..))