Commit c892f86e authored by Masahiko Sakai's avatar Masahiko Sakai

on cnf generation

parent 7cbac981
......@@ -95,6 +95,7 @@ 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
Modified on Jul 27, 2016
- Fixed a bug related to -ngr option.
......
* 2 variables
* 1 clauses
-2 x1 3 x2 >= 2;
......@@ -97,7 +97,7 @@ int main(int argc, char** argv)
// added by nabesima
if (!compe) {
printf(GLUEGlueMiniSat_VERSION"\n");
printf(GlueMiniSat_VERSION"\n");
printf("Command: ");
for (int i=0; i < argc; i++)
printf("%s ", argv[i]);
......
......@@ -1779,7 +1779,10 @@ static Var mapVar(Var x, vec<Var>& map, Var& max)
{
if (map.size() <= x || map[x] == -1){
map.growTo(x+1, -1);
map[x] = max++;
// modified by nabesima (use original variable name)
//map[x] = max++;
map[x] = x;
if (max < x) max = x;
}
return map[x];
}
......@@ -1836,7 +1839,11 @@ void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
// added by nabesima
// Unit clauses are added
assert(decisionLevel() == 0);
cnt += trail.size();
for (int i = 0; i < trail.size(); i++){
assert(value(trail[i]) != l_False);
mapVar(var(trail[i]), map, max);
}
cnt += trail.size();
fprintf(f, "p cnf %d %d\n", max, cnt);
......
......@@ -29,7 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
// added by nabesima
#include "RecentVals.h"
#define GLUEGlueMiniSat_VERSION "glueminisat2.2.6-ucore-h"
#define GlueMiniSat_VERSION "glueminisat2.2.6-ucore-i"
namespace GlueMiniSat {
......
......@@ -84,7 +84,7 @@ int main(int argc, char** argv)
if (compe)
S.verbosity = 0;
else {
printf(GLUEGlueMiniSat_VERSION"\n");
printf(GlueMiniSat_VERSION"\n");
printf("Command: ");
for (int i=0; i < argc; i++)
printf("%s ", argv[i]);
......
......@@ -99,7 +99,7 @@ int main(int argc, char** argv)
// added by nabesima
if (!compe) {
printf(GLUEGlueMiniSat_VERSION"\n");
printf(GlueMiniSat_VERSION"\n");
printf("Command: ");
for (int i=0; i < argc; i++)
printf("%s ", argv[i]);
......
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