Commit 15eb340c authored by Masahiko Sakai's avatar Masahiko Sakai
Browse files

cnf production

parent a89667ad

Main.C

+3 −3
Original line number Diff line number Diff line
@@ -369,10 +369,10 @@ void parseOptions(int argc, char** argv) 
	&& opt_solver != st_Glucose10)

      reportf("We set -GM because of -extract-ucore.\n"), opt_solver = st_GlueMiniSat;



/*

    if (opt_cnf != NULL && (opt_solver == st_ES1Sat || opt_solver == st_CCMiniSat))

      reportf("-cnf option is not handled by ES1Sat/CCMiniSat.  We set -M2 instead.\n"), opt_solver = st_MiniSat22;

    if (opt_cnf != NULL && (opt_solver == st_ES1Sat || opt_solver == st_CCMiniSat || opt_solver == st_SatELite))

      reportf("-cnf option is not supported by ES1Sat/CCMiniSat/Satelite.  We set -GM instead.\n"), opt_solver = st_GlueMiniSat;



/*

    if (opt_cnf != NULL && opt_simp_solver)

      reportf("We set -noSimp because of -cnf.\n"), opt_simp_solver = false;

*/

Solver.h

+2 −1
Original line number Diff line number Diff line
@@ -476,7 +476,8 @@ public: 
        } else if (simp_glueminisat) {

            simp_glueminisat->toDimacs(filename);

        } else

            assert(false);

	    reportf("-cnf: unsupported option.\n"),exit(1);

//            assert(false);

    }

    //- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -