cprover
satcheck_zcore.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "satcheck_zcore.h"
10
11#include <fstream>
12
13#include <util/invariant.h>
14#include <util/string2int.h>
15
16#include <cstring>
17
19{
20}
21
23{
24}
25
27{
30}
31
33{
34 return "ZCore";
35}
36
38{
39 // We start counting at 1, thus there is one variable fewer.
40 {
41 std::string msg=
42 std::to_string(no_variables()-1)+" variables, "+
43 std::to_string(no_clauses())+" clauses";
44 log.statistics() << msg << messaget::eom;
45 }
46
47 // get the core
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";
52
53 {
54 std::ofstream out(cnf_file.c_str(), std::ios::out);
56 }
57
58 // generate resolve_trace
59 system(std::string("zchaff_verify "+cnf_file+" > "+output_file).c_str());
60
61 // get core
62 system(
63 std::string("zcore "+cnf_file+" "+trace_file+" >> "+output_file).c_str());
64
65 in_core.clear();
66
67 // read result
68 {
69 std::ifstream in(core_file.c_str());
70
71 while(true)
72 {
73 std::string line;
74 if(!std::getline(in, line))
75 break;
76
77 if(!(line.substr(0, 1)=="c" || line.substr(0, 1)=="p"))
78 {
79 const char *p=line.c_str();
80
81 while(true)
82 {
83 int l=unsafe_str2int(p);
84 if(l==0)
85 break;
86
87 if(l<0)
88 l=-l;
89
90 in_core.insert(l);
91
92 // next one
93 const char *q=strchr(p, ' ');
94 while(*q==' ') q++;
95 if(q==NULL)
96 break;
97 p=q;
98 }
99 }
100 }
101 }
102
103 if(in_core.empty())
104 return P_ERROR;
105
106 remove(cnf_file.c_str());
107 // remove(core_file.c_str());
108 remove(trace_file.c_str());
109 // remove(output_file.c_str());
110
111 return P_UNSATISFIABLE;
112}
size_t no_clauses() const override
virtual size_t no_variables() const override
Definition: cnf.h:42
virtual void write_dimacs_cnf(std::ostream &out)
Definition: dimacs_cnf.cpp:40
mstreamt & statistics() const
Definition: message.h:419
static eomt eom
Definition: message.h:297
resultt
Definition: prop.h:97
messaget log
Definition: prop.h:128
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
Definition: threeval.h:20
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.