summaryrefslogtreecommitdiff
path: root/passes
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-02-18 09:29:08 +0100
committerClifford Wolf <clifford@clifford.at>2014-02-18 09:29:08 +0100
commita78bba1f5cf5b8c312c453e5c2c1a57b6946bebd (patch)
tree25597d5ed2f6bbcb8009ad69f4c7ede4768e8c8c /passes
parent32af10fa9b0fb8c86451a15f780288da13d4ab99 (diff)
Added "sat -dump_cnf"
Diffstat (limited to 'passes')
-rw-r--r--passes/sat/sat.cc39
1 files changed, 34 insertions, 5 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 3b4a394e..d18a220d 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -878,6 +878,10 @@ struct SatPass : public Pass {
log(" -dump_vcd <vcd-file-name>\n");
log(" dump SAT model (counter example in proof) to VCD file\n");
log("\n");
+ log(" -dump_cnf <cnf-file-name>\n");
+ log(" dump CNF of SAT problem (in DIMACS format). in temporal induction\n");
+ log(" proofs this is the CNF of the first induction step.\n");
+ log("\n");
log("The following additional options can be used to set up a proof. If also -seq\n");
log("is passed, a temporal induction proof is performed.\n");
log("\n");
@@ -933,7 +937,7 @@ struct SatPass : public Pass {
bool ignore_div_by_zero = false, set_init_undef = false, set_init_zero = false, max_undef = false;
bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false;
bool ignore_unknown_cells = false, falsify = false, tempinduct_def = false, set_init_def = false;
- std::string vcd_file_name;
+ std::string vcd_file_name, cnf_file_name;
log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
@@ -1115,6 +1119,10 @@ struct SatPass : public Pass {
vcd_file_name = args[++argidx];
continue;
}
+ if (args[argidx] == "-dump_cnf" && argidx+1 < args.size()) {
+ cnf_file_name = args[++argidx];
+ continue;
+ }
break;
}
extra_args(args, argidx, design);
@@ -1255,6 +1263,19 @@ struct SatPass : public Pass {
}
else
{
+ if (!cnf_file_name.empty())
+ {
+ FILE *f = fopen(cnf_file_name.c_str(), "w");
+ if (!f)
+ log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno));
+
+ log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str());
+ cnf_file_name.clear();
+
+ inductstep.ez.printDIMACS(f, false);
+ fclose(f);
+ }
+
log("\n[induction step] Solving problem with %d variables and %d clauses..\n",
inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
@@ -1333,10 +1354,18 @@ struct SatPass : public Pass {
}
sathelper.generate_model();
-#if 0
- // print CNF for debugging
- sathelper.ez.printDIMACS(stdout, true);
-#endif
+ if (!cnf_file_name.empty())
+ {
+ FILE *f = fopen(cnf_file_name.c_str(), "w");
+ if (!f)
+ log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno));
+
+ log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str());
+ cnf_file_name.clear();
+
+ sathelper.ez.printDIMACS(f, false);
+ fclose(f);
+ }
int rerun_counter = 0;