diff -c -r stp_dimacs/AST/AST.cpp stp/AST/AST.cpp *** stp_dimacs/AST/AST.cpp 2009-04-27 21:58:49.000000000 +0200 --- stp/AST/AST.cpp 2009-04-27 20:22:57.000000000 +0200 *************** *** 57,66 **** bool smtlib_parser_enable = false; //print the input back bool print_STPinput_back = false; ! ! // dump DIMACS output ! bool dump_dimacs = false; ! //global BEEVMGR for the parser BeevMgr * globalBeevMgr_for_parser; --- 57,63 ---- bool smtlib_parser_enable = false; //print the input back bool print_STPinput_back = false; ! //global BEEVMGR for the parser BeevMgr * globalBeevMgr_for_parser; Only in stp_dimacs/AST: ASTKind.cpp Only in stp_dimacs/AST: ASTKind.h Only in stp_dimacs/AST: ASTKind.o Only in stp_dimacs/AST: AST.o diff -c -r stp_dimacs/AST/ASTUtil.h stp/AST/ASTUtil.h *** stp_dimacs/AST/ASTUtil.h 2009-04-27 21:58:33.000000000 +0200 --- stp/AST/ASTUtil.h 2009-04-27 20:22:57.000000000 +0200 *************** *** 77,85 **** //print the input back extern bool print_STPinput_back; - // dump DIMACS output - extern bool dump_dimacs; - extern void (*vc_error_hdlr)(const char* err_msg); /*Spacer class is basically just an int, but the new class allows overloading of << with a special definition that prints the int as --- 77,82 ---- Only in stp_dimacs/AST: ASTUtil.o Only in stp_dimacs/AST: BitBlast.o Only in stp_dimacs/AST: libast.a Only in stp_dimacs/AST: SimpBool.o Only in stp_dimacs/AST: ToCNF.o diff -c -r stp_dimacs/AST/ToSAT.cpp stp/AST/ToSAT.cpp *** stp_dimacs/AST/ToSAT.cpp 2009-04-27 22:00:42.000000000 +0200 --- stp/AST/ToSAT.cpp 2009-04-27 20:22:57.000000000 +0200 *************** *** 85,112 **** satSolverClause.push(l); } newS.addClause(satSolverClause); - - #if 0 // clause printing. ! if ( BEEV::print_clauses ) ! { ! //newS.printClause >(satSolverClause); ! //cout << " 0 "; ! //cout << endl; ! } ! #endif ! if(newS.okay()) { ! continue; } else { ! PrintStats(newS); ! return false; } ! if(!newS.simplify()) { ! PrintStats(newS); ! return false; } } --- 85,106 ---- satSolverClause.push(l); } newS.addClause(satSolverClause); // clause printing. ! // (printClause >)(satSolverClause); ! // cout << " 0 "; ! // cout << endl; ! if(newS.okay()) { ! continue; } else { ! PrintStats(newS); ! return false; } ! if(!newS.simplify()) { ! PrintStats(newS); ! return false; } } *************** *** 116,126 **** return false; } - if ( BEEV::dump_dimacs ) - { - newS.toDimacs("output.dimacs"); - } - //PrintActivityLevels_Of_SATVars("Before SAT:",newS); //ChangeActivityLevels_Of_SATVars(newS); //PrintActivityLevels_Of_SATVars("Before SAT and after initial bias:",newS); --- 110,115 ---- *************** *** 128,134 **** //PrintActivityLevels_Of_SATVars("After SAT",newS); PrintStats(newS); - if (newS.okay()) return true; else --- 117,122 ---- Only in stp_dimacs/AST: .ToSAT.cpp.swp Only in stp_dimacs/AST: ToSAT.o Only in stp_dimacs/AST: Transform.o Only in stp_dimacs/bin: stp Only in stp_dimacs/bitvec: consteval.o Only in stp_dimacs/bitvec: libconsteval.a Only in stp_dimacs/c_interface: c_interface.o Only in stp_dimacs/c_interface: libcinterface.a Only in stp_dimacs: config.info Only in stp_dimacs/constantbv: constantbv.o Only in stp_dimacs/constantbv: libconstantbv.a Only in stp_dimacs: DIMACS.README Only in stp_dimacs/lib: libstp.a Only in stp_dimacs: Makefile Only in stp_dimacs/parser: let-funcs.o Only in stp_dimacs/parser: lexCVC.cpp Only in stp_dimacs/parser: lexCVC.o Only in stp_dimacs/parser: lexSMT.cpp Only in stp_dimacs/parser: lexSMT.o diff -c -r stp_dimacs/parser/main.cpp stp/parser/main.cpp *** stp_dimacs/parser/main.cpp 2009-04-27 21:58:51.000000000 +0200 --- stp/parser/main.cpp 2009-04-27 20:23:03.000000000 +0200 *************** *** 85,91 **** helpstring += "-x : flatten nested XORs\n"; helpstring += "-h : help\n"; helpstring += "-m : use the SMTLIB parser\n"; ! helpstring += "-o : dump DIMACS output to file output.dimacs\n"; bool smtlibParser = false; --- 85,91 ---- helpstring += "-x : flatten nested XORs\n"; helpstring += "-h : help\n"; helpstring += "-m : use the SMTLIB parser\n"; ! bool smtlibParser = false; *************** *** 154,162 **** case 'z': BEEV::print_sat_varorder = true; break; - case 'o': - BEEV::dump_dimacs = true; - break; default: fprintf(stderr,usage,prog); cout << helpstring; --- 154,159 ---- Only in stp_dimacs/parser: main.o Only in stp_dimacs/parser: parseCVC.cpp Only in stp_dimacs/parser: parseCVC_defs.h Only in stp_dimacs/parser: parseCVC.o Only in stp_dimacs/parser: parseSMT.cpp Only in stp_dimacs/parser: parseSMT_defs.h Only in stp_dimacs/parser: parseSMT.o Only in stp_dimacs/parser: y.output Only in stp_dimacs/parser: y.tab.c Only in stp_dimacs/parser: y.tab.h Only in stp_dimacs/sat/core: depend.mk Only in stp_dimacs/sat/core: libminisat.a diff -c -r stp_dimacs/sat/core/Solver.C stp/sat/core/Solver.C *** stp_dimacs/sat/core/Solver.C 2009-04-27 21:53:15.000000000 +0200 --- stp/sat/core/Solver.C 2009-04-27 20:22:57.000000000 +0200 *************** *** 743,783 **** } } - //================================================================================================= - // Convert to DIMACS: - - void Solver::toDimacs(FILE* f, Clause& c) - { - if (satisfied(c)) return; - - for (int i = 0; i < c.size(); i++) - if (value(c[i]) != l_False) - fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", var(c[i])+1); - fprintf(f, "0\n"); - } - - - void Solver::toDimacs(const char* file) - { - assert(decisionLevel() == 0); - FILE* f = fopen(file, "wr"); - if (f != NULL){ - - // Cannot use removeClauses here because it is not safe - // to deallocate them at this point. Could be improved. - int cnt = 0; - for (int i = 0; i < clauses.size(); i++) - if (!satisfied(*clauses[i])) - cnt++; - - fprintf(f, "p cnf %d %d\n", nVars(), cnt); - - for (int i = 0; i < clauses.size(); i++) - toDimacs(f, *clauses[i]); - - fprintf(stderr, "Wrote %d clauses...\n", clauses.size()); - }else - fprintf(stderr, "could not open file %s\n", file); - } - }; --- 743,746 ---- diff -c -r stp_dimacs/sat/core/Solver.h stp/sat/core/Solver.h *** stp_dimacs/sat/core/Solver.h 2009-04-27 21:55:36.000000000 +0200 --- stp/sat/core/Solver.h 2009-04-27 20:22:57.000000000 +0200 *************** *** 237,243 **** uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision levels. double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ... - public: // Debug: void printLit (Lit l); template --- 237,242 ---- *************** *** 245,257 **** void verifyModel (); void checkLiteralCount(); - // DIMACSify - public: - void toDimacs (const char* file); - protected: - void toDimacs (FILE* f, Clause& c); - - protected: // Static helpers: // --- 244,249 ---- Only in stp_dimacs/sat/core: Solver.or Only in stp_dimacs/sat/simp: .Main.C.swp Only in stp_dimacs/simplifier: bvsolver.o Only in stp_dimacs/simplifier: libsimplifier.a Only in stp_dimacs/simplifier: simplifier.o Only in stp_dimacs: stpbin