Commit a6485c17 authored by Masahiko Sakai's avatar Masahiko Sakai

producing cnf

parent c892f86e
......@@ -91,11 +91,14 @@ Known BUGs:
- -S may result wrong answer.
- Combination of -Simp and -es1 may result wrong answer.
Modified on Jun 19, 2018
- Fixed a bug when creating cnf.
Modified on Oct 31, 2016
- Fixed a bug showing unaccurate SAT-solving time when interrupted.
- Fixed a bug on switching bdd/sort/adder strategies.
- Fixed a bug on combinating -A and -Simp
- Fixed a bug in producing cnf files when used glueminisat
- Fixed a bug in producing cnf files when used glueminisat (with -noSimp)
Modified on Jul 27, 2016
- Fixed a bug related to -ngr option.
......
......@@ -473,6 +473,8 @@ public:
satelite->simplifyDB(true);
} else if (glueminisat) {
glueminisat->toDimacs(filename);
} else if (simp_glueminisat) {
simp_glueminisat->toDimacs(filename);
} else
assert(false);
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment