Merge pull request #2215 from boqwxp/qbfsat-solver-options

qbfsat, smt2, smtio: Add `-solver-option` to allow specifying SMT-LIBv2 `(set-option ...)` commands

backends/smt2/smt2.cc

@@ -1387,6 +1387,10 @@ struct Smt2Backend : public Backend {
 		log("        use the given template file. the line containing only the token '%%%%'\n");
 		log("        is replaced with the regular output of this command.\n");
 		log("\n");
+		log("    -solver-option <option> <value>\n");
+		log("        emit a `; yosys-smt2-solver-option` directive for yosys-smtbmc to write\n");
+		log("        the given option as a `(set-option ...)` command in the SMT-LIBv2.\n");
+		log("\n");
 		log("[1] For more information on SMT-LIBv2 visit http://smt-lib.org/ or read David\n");
 		log("R. Cok's tutorial: http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf\n");
 		log("\n");
@@ -1441,6 +1445,7 @@ struct Smt2Backend : public Backend {
 		std::ifstream template_f;
 		bool bvmode = true, memmode = true, wiresmode = false, verbose = false, statebv = false, statedt = false;
 		bool forallmode = false;
+		dict<std::string, std::string> solver_options;
 
 		log_header(design, "Executing SMT2 backend.\n");
 
@@ -1484,6 +1489,11 @@ struct Smt2Backend : public Backend {
 				verbose = true;
 				continue;
 			}
+			if (args[argidx] == "-solver-option" && argidx+2 < args.size()) {
+				solver_options.emplace(args[argidx+1], args[argidx+2]);
+				argidx += 2;
+				continue;
+			}
 			break;
 		}
 		extra_args(f, filename, args, argidx);
@@ -1514,6 +1524,9 @@ struct Smt2Backend : public Backend {
 		if (statedt)
 			*f << stringf("; yosys-smt2-stdt\n");
 
+		for (auto &it : solver_options)
+			*f << stringf("; yosys-smt2-solver-option %s %s\n", it.first.c_str(), it.second.c_str());
+
 		std::vector<RTLIL::Module*> sorted_modules;
 
 		// extract module dependencies

backends/smt2/smtio.py

@@ -124,6 +124,7 @@ class SmtIo:
         self.timeout = 0
         self.produce_models = True
         self.smt2cache = [list()]
+        self.smt2_options = dict()
         self.p = None
         self.p_index = solvers_index
         solvers_index += 1
@@ -258,14 +259,24 @@ class SmtIo:
         for stmt in self.info_stmts:
             self.write(stmt)
 
-        if self.forall and self.solver == "yices":
-            self.write("(set-option :yices-ef-max-iters 1000000000)")
-
         if self.produce_models:
             self.write("(set-option :produce-models true)")
 
+        #See the SMT-LIB Standard, Section 4.1.7
+        modestart_options = [":global-declarations", ":interactive-mode", ":produce-assertions", ":produce-assignments", ":produce-models", ":produce-proofs", ":produce-unsat-assumptions", ":produce-unsat-cores", ":random-seed"]
+        for key, val in self.smt2_options.items():
+            if key in modestart_options:
+                self.write("(set-option {} {})".format(key, val))
+
         self.write("(set-logic %s)" % self.logic)
 
+        if self.forall and self.solver == "yices":
+            self.write("(set-option :yices-ef-max-iters 1000000000)")
+
+        for key, val in self.smt2_options.items():
+            if key not in modestart_options:
+                self.write("(set-option {} {})".format(key, val))
+
     def timestamp(self):
         secs = int(time() - self.start_time)
         return "## %3d:%02d:%02d " % (secs // (60*60), (secs // 60) % 60, secs % 60)
@@ -468,6 +479,9 @@ class SmtIo:
 
         fields = stmt.split()
 
+        if fields[1] == "yosys-smt2-solver-option":
+            self.smt2_options[fields[2]] = fields[3]
+
         if fields[1] == "yosys-smt2-nomem":
             if self.logic is None:
                 self.logic_ax = False

passes/sat/qbfsat.cc

@@ -215,7 +215,6 @@ QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt,
 	//Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g --binary [--dump-smt2 <file>]`
 	QbfSolutionType ret;
 	const std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc";
-	const std::string smt2_command = stringf("write_smt2 -stbv -wires %s/problem%d.smt2", tempdir_name.c_str(), iter_num);
 	const std::string smtbmc_warning = "z3: WARNING:";
 	const std::string smtbmc_cmd = stringf("%s -s %s %s -t 1 -g --binary %s %s/problem%d.smt2 2>&1",
 			yosys_smtbmc_exe.c_str(), opt.get_solver_name().c_str(),
@@ -223,6 +222,10 @@ QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt,
 			(opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file : "").c_str(),
 			tempdir_name.c_str(), iter_num);
 
+	std::string smt2_command = "write_smt2 -stbv -wires ";
+	for (auto &solver_opt : opt.solver_options)
+		smt2_command += stringf("-solver-option %s %s ", solver_opt.first.c_str(), solver_opt.second.c_str());
+	smt2_command += stringf("%s/problem%d.smt2", tempdir_name.c_str(), iter_num);
 	Pass::call(mod->design, smt2_command);
 
 	auto process_line = [&ret, &smtbmc_warning, &opt, &quiet](const std::string &line) {
@@ -419,6 +422,13 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) {
 			}
 			continue;
 		}
+		else if (args[opt.argidx] == "-solver-option") {
+			if (args.size() <= opt.argidx + 2)
+				log_cmd_error("solver option name and value not fully specified.\n");
+			opt.solver_options.emplace(args[opt.argidx+1], args[opt.argidx+2]);
+			opt.argidx += 2;
+			continue;
+		}
 		else if (args[opt.argidx] == "-timeout") {
 			if (args.size() <= opt.argidx + 1)
 				log_cmd_error("timeout not specified.\n");
@@ -533,6 +543,9 @@ struct QbfSatPass : public Pass {
 		log("        Use a particular solver. Choose one of: \"z3\", \"yices\", and \"cvc4\".\n");
 		log("        (default: yices)\n");
 		log("\n");
+		log("    -solver-option <name> <value>\n");
+		log("        Set the specified solver option in the SMT-LIBv2 problem file.\n");
+		log("\n");
 		log("    -timeout <value>\n");
 		log("        Set the per-iteration timeout in seconds.\n");
 		log("        (default: no timeout)\n");

passes/sat/qbfsat.h

@@ -31,6 +31,7 @@ struct QbfSolveOptions {
 	bool nobisection = false, sat = false, unsat = false, show_smtbmc = false;
 	enum Solver{Z3, Yices, CVC4} solver = Yices;
 	enum OptimizationLevel{O0, O1, O2} oflag = O0;
+	dict<std::string, std::string> solver_options;
 	int timeout = 0;
 	std::string specialize_soln_file = "";
 	std::string write_soln_soln_file = "";