cprover
dplib_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 "dplib_dec.h"
10 
11 #include <cstring>
12 #include <cassert>
13 
14 #if defined(__linux__) || \
15  defined(__FreeBSD_kernel__) || \
16  defined(__GNU__) || \
17  defined(__unix__) || \
18  defined(__CYGWIN__) || \
19  defined(__MACH__)
20 #include <unistd.h>
21 #endif
22 
23 #ifdef _WIN32
24 #include <process.h>
25 #define getpid _getpid
26 #endif
27 
28 #include <util/prefix.h>
29 #include <util/string2int.h>
30 
32 {
33  temp_out_filename="dplib_dec_out_"+std::to_string(getpid())+".tmp";
34 
35  temp_out.open(
36  temp_out_filename.c_str(),
37  std::ios_base::out | std::ios_base::trunc);
38 }
39 
41 {
42  temp_out.close();
43 
44  if(temp_out_filename!="")
45  unlink(temp_out_filename.c_str());
46 
47  if(temp_result_filename!="")
48  unlink(temp_result_filename.c_str());
49 }
50 
52 {
53  dplib_prop.out << "QUERY FALSE;\n";
54  dplib_prop.out << "COUNTERMODEL;\n";
55 
56  post_process();
57 
58  temp_out.close();
59 
61  "dplib_dec_result_"+std::to_string(getpid())+".tmp";
62 
63  std::string command=
64  "dplibl "+temp_out_filename+" > "+temp_result_filename+" 2>&1";
65 
66  int res=system(command.c_str());
67  assert(0 == res);
68 
69  status("Reading result from CVCL");
70 
71  return read_dplib_result();
72 }
73 
74 void dplib_dect::read_assert(std::istream &in, std::string &line)
75 {
76  // strip ASSERT
77  line=std::string(line, strlen("ASSERT "), std::string::npos);
78  if(line=="")
79  return;
80 
81  // bit-vector
82  if(line[0]=='(')
83  {
84  // get identifier
86  line.find(' ');
87 
88  std::string identifier=std::string(line, 1, pos-1);
89 
90  // get value
91  if(!std::getline(in, line))
92  return;
93 
94  // skip spaces
95  pos=0;
96  while(pos<line.size() && line[pos]==' ') pos++;
97 
98  // get final ")"
99  std::string::size_type pos2=line.rfind(')');
100  if(pos2==std::string::npos)
101  return;
102 
103  std::string value=std::string(line, pos, pos2-pos);
104 
105  #if 0
106  std::cout << ">" << identifier << "< = >" << value << "<\n";
107  #endif
108  }
109  else
110  {
111  // boolean
112  tvt value=tvt(true);
113 
114  if(has_prefix(line, "NOT "))
115  {
116  line=std::string(line, strlen("NOT "), std::string::npos);
117  value=tvt(false);
118  }
119 
120  if(line=="")
121  return;
122 
123  if(line[0]=='l')
124  {
125  unsigned number=unsafe_str2unsigned(line.c_str()+1);
126  assert(number<dplib_prop.no_variables());
127  dplib_prop.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  dplib_prop.reset_assignment();
143 
144  while(std::getline(in, line))
145  {
146  if(has_prefix(line, "ASSERT "))
147  read_assert(in, line);
148  }
149 
150  return D_SATISFIABLE;
151  }
152  else if(has_prefix(line, "Valid."))
153  return D_UNSATISFIABLE;
154  }
155 
156  error("Unexpected result from CVC-Lite");
157 
158  return D_ERROR;
159 }
virtual resultt dec_solve()
Definition: dplib_dec.cpp:51
std::string temp_out_filename
Definition: dplib_dec.h:25
mstreamt & status()
Definition: message.h:238
literalt pos(literalt a)
Definition: literal.h:193
unsignedbv_typet size_type()
Definition: c_types.cpp:57
void read_assert(std::istream &in, std::string &line)
Definition: dplib_dec.cpp:74
Definition: threeval.h:19
std::ofstream temp_out
Definition: dplib_dec.h:24
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
std::string temp_result_filename
Definition: dplib_dec.h:25
mstreamt & error()
Definition: message.h:223
resultt read_dplib_result()
Definition: dplib_dec.cpp:132