48 std::string cnf_file=
"cnf.dimacs";
49 std::string core_file=
"unsat_core.cnf";
50 std::string trace_file=
"resolve_trace";
51 std::string output_file=
"cnf.out";
54 std::ofstream out(cnf_file.c_str(), std::ios::out);
59 system(std::string(
"zchaff_verify "+cnf_file+
" > "+output_file).c_str());
63 std::string(
"zcore "+cnf_file+
" "+trace_file+
" >> "+output_file).c_str());
69 std::ifstream in(core_file.c_str());
74 if(!std::getline(in, line))
77 if(!(line.substr(0, 1)==
"c" || line.substr(0, 1)==
"p"))
79 const char *p=line.c_str();
83 int l=unsafe_str2int(p);
93 const char *q=strchr(p,
' ');
106 remove(cnf_file.c_str());
108 remove(trace_file.c_str());
111 return P_UNSATISFIABLE;
size_t no_clauses() const override
virtual size_t no_variables() const override
virtual void write_dimacs_cnf(std::ostream &out)
mstreamt & statistics() const
tvt l_get(literalt a) const override
virtual ~satcheck_zcoret()
resultt do_prop_solve() override
std::set< unsigned > in_core
const std::string solver_text() override
#define UNREACHABLE
This should be used to mark dead code.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.