summaryrefslogtreecommitdiff
path: root/passes
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-02-18 09:03:16 +0100
committerClifford Wolf <clifford@clifford.at>2014-02-18 09:03:16 +0100
commit13051e6acf6c1fd506a49d258c3d99c1334c78cc (patch)
treede43540b84ae2918200c246c5ea6c051aeb65712 /passes
parent02e6f2c5be8c5514cc8cdb7b3344f6170fb87af9 (diff)
Added "sat -initsteps"
Diffstat (limited to 'passes')
-rw-r--r--passes/sat/sat.cc43
1 files changed, 29 insertions, 14 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 2cd15d01..2dc7a16b 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -903,6 +903,9 @@ struct SatPass : public Pass {
log(" -maxsteps <N>\n");
log(" Set a maximum length for the induction.\n");
log("\n");
+ log(" -initsteps <N>\n");
+ log(" Set initial length for the induction.\n");
+ log("\n");
log(" -timeout <N>\n");
log(" Maximum number of seconds a single SAT instance may take.\n");
log("\n");
@@ -925,7 +928,7 @@ struct SatPass : public Pass {
std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_any_undef_at, sets_all_undef_at;
std::vector<std::string> shows, sets_def, sets_any_undef, sets_all_undef;
- int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0;
+ int loopcount = 0, seq_len = 0, maxsteps = 0, initsteps = 0, timeout = 0;
bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false;
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;
@@ -970,6 +973,10 @@ struct SatPass : public Pass {
maxsteps = atoi(args[++argidx].c_str());
continue;
}
+ if (args[argidx] == "-initsteps" && argidx+1 < args.size()) {
+ initsteps = atoi(args[++argidx].c_str());
+ continue;
+ }
if (args[argidx] == "-ignore_div_by_zero") {
ignore_div_by_zero = true;
continue;
@@ -1240,21 +1247,29 @@ struct SatPass : public Pass {
if (inductlen > 1)
inductstep.force_unique_state(1, inductlen + 1);
- log("\n[induction step] Solving problem with %d variables and %d clauses..\n",
- inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
-
- if (!inductstep.solve(inductstep.ez.NOT(property))) {
- if (inductstep.gotTimeout)
- goto timeout;
- log("Induction step proven: SUCCESS!\n");
- print_qed();
- goto tip_success;
+ if (inductlen < initsteps)
+ {
+ log("\n[induction step] Skipping problem with %d variables and %d clauses (below initsteps).\n",
+ inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
+ inductstep.ez.assume(property);
}
+ else
+ {
+ log("\n[induction step] Solving problem with %d variables and %d clauses..\n",
+ inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
+
+ if (!inductstep.solve(inductstep.ez.NOT(property))) {
+ if (inductstep.gotTimeout)
+ goto timeout;
+ log("Induction step proven: SUCCESS!\n");
+ print_qed();
+ goto tip_success;
+ }
- log("Induction step failed. Incrementing induction length.\n");
- inductstep.ez.assume(property);
-
- inductstep.print_model();
+ log("Induction step failed. Incrementing induction length.\n");
+ inductstep.ez.assume(property);
+ inductstep.print_model();
+ }
}
log("\nReached maximum number of time steps -> proof failed.\n");