cprover
cvc_dec.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "cvc_dec.h"
10 
11 #include <cstring>
12 #include <cassert>
13 #include <cstdlib> // for system()
14 
15 #if defined(__linux__) || \
16  defined(__FreeBSD_kernel__) || \
17  defined(__GNU__) || \
18  defined(__unix__) || \
19  defined(__CYGWIN__) || \
20  defined(__MACH__)
21 #include <unistd.h>
22 #endif
23 
24 #ifdef _WIN32
25 #include <process.h>
26 #define getpid _getpid
27 #endif
28 
29 #include <util/prefix.h>
30 #include <util/string2int.h>
31 
33 {
34  temp_out_filename="cvc_dec_out_"+std::to_string(getpid())+".tmp";
35 
36  temp_out.open(
37  temp_out_filename.c_str(),
38  std::ios_base::out | std::ios_base::trunc);
39 }
40 
42 {
43  temp_out.close();
44 
45  if(temp_out_filename!="")
46  unlink(temp_out_filename.c_str());
47 
48  if(temp_result_filename!="")
49  unlink(temp_result_filename.c_str());
50 }
51 
53 {
54  out << "QUERY FALSE;\n";
55  out << "COUNTERMODEL;\n";
56 
57  temp_out.close();
58 
60  "cvc_dec_result_"+std::to_string(getpid())+".tmp";
61 
62  std::string command=
63  "cvcl "+temp_out_filename+" > "+temp_result_filename+" 2>&1";
64 
65  int res=system(command.c_str());
66  assert(0==res);
67 
68  status() << "Reading result from CVCL" << eom;
69 
70  return read_cvcl_result();
71 }
72 
73 void cvc_dect::read_assert(std::istream &in, std::string &line)
74 {
75  // strip ASSERT
76  line=std::string(line, strlen("ASSERT "), std::string::npos);
77  if(line=="")
78  return;
79 
80  // bit-vector
81  if(line[0]=='(')
82  {
83  // get identifier
85  line.find(' ');
86 
87  std::string identifier=std::string(line, 1, pos-1);
88 
89  // get value
90  if(!std::getline(in, line))
91  return;
92 
93  // skip spaces
94  pos=0;
95  while(pos<line.size() && line[pos]==' ') pos++;
96 
97  // get final ")"
98  std::string::size_type pos2=line.rfind(')');
99  if(pos2==std::string::npos)
100  return;
101 
102  std::string value=std::string(line, pos, pos2-pos);
103 
104  #if 0
105  std::cout << ">" << identifier << "< = >" << value << "<\n";
106  #endif
107  }
108  else
109  {
110  // boolean
111  bool value=true;
112 
113  if(has_prefix(line, "NOT "))
114  {
115  line=std::string(line, strlen("NOT "), std::string::npos);
116  value=false;
117  }
118 
119  if(line=="")
120  return;
121 
122  if(line[0]=='l')
123  {
124  unsigned number=unsafe_string2unsigned(line.substr(1));
125  assert(number<no_boolean_variables);
127  boolean_assignment[number]=value;
128  }
129  }
130 }
131 
133 {
134  std::ifstream in(temp_result_filename.c_str());
135 
136  std::string line;
137 
138  while(std::getline(in, line))
139  {
140  if(has_prefix(line, "Invalid."))
141  {
142  boolean_assignment.clear();
144 
145  while(std::getline(in, line))
146  {
147  if(has_prefix(line, "ASSERT "))
148  read_assert(in, line);
149  }
150 
151  return resultt::D_SATISFIABLE;
152  }
153  else if(has_prefix(line, "Valid."))
155  }
156 
157  error() << "Unexpected result from CVC-Lite" << eom;
158 
159  return resultt::D_ERROR;
160 }
std::string temp_result_filename
Definition: cvc_dec.h:25
std::ofstream temp_out
Definition: cvc_dec.h:24
mstreamt & status()
Definition: message.h:238
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:66
resultt read_cvcl_result()
Definition: cvc_dec.cpp:132
literalt pos(literalt a)
Definition: literal.h:193
std::ostream & out
Definition: cvc_conv.h:37
unsignedbv_typet size_type()
Definition: c_types.cpp:57
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
void read_assert(std::istream &in, std::string &line)
Definition: cvc_dec.cpp:73
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
virtual resultt dec_solve()
Definition: cvc_dec.cpp:52
std::string temp_out_filename
Definition: cvc_dec.h:25
std::vector< bool > boolean_assignment
Definition: cvc_conv.h:63
unsigned no_boolean_variables
Definition: cvc_conv.h:44
mstreamt & error()
Definition: message.h:223