15 #if defined(__linux__) || \ 16 defined(__FreeBSD_kernel__) || \ 18 defined(__unix__) || \ 19 defined(__CYGWIN__) || \ 26 #define getpid _getpid 38 std::ios_base::out | std::ios_base::trunc);
54 out <<
"QUERY FALSE;\n";
55 out <<
"COUNTERMODEL;\n";
60 "cvc_dec_result_"+std::to_string(getpid())+
".tmp";
65 int res=system(command.c_str());
68 status() <<
"Reading result from CVCL" << eom;
70 return read_cvcl_result();
76 line=std::string(line, strlen(
"ASSERT "), std::string::npos);
87 std::string identifier=std::string(line, 1, pos-1);
90 if(!std::getline(in, line))
95 while(pos<line.size() && line[
pos]==
' ') pos++;
99 if(pos2==std::string::npos)
102 std::string value=std::string(line, pos, pos2-pos);
105 std::cout <<
">" << identifier <<
"< = >" << value <<
"<\n";
115 line=std::string(line, strlen(
"NOT "), std::string::npos);
125 assert(number<no_boolean_variables);
126 assert(no_boolean_variables==boolean_assignment.size());
127 boolean_assignment[number]=value;
138 while(std::getline(in, line))
142 boolean_assignment.clear();
143 boolean_assignment.resize(no_boolean_variables);
145 while(std::getline(in, line))
148 read_assert(in, line);
151 return resultt::D_SATISFIABLE;
154 return resultt::D_UNSATISFIABLE;
157 error() <<
"Unexpected result from CVC-Lite" << eom;
159 return resultt::D_ERROR;
std::string temp_result_filename
unsigned unsafe_string2unsigned(const std::string &str, int base)
resultt read_cvcl_result()
unsignedbv_typet size_type()
void read_assert(std::istream &in, std::string &line)
bool has_prefix(const std::string &s, const std::string &prefix)
virtual resultt dec_solve()
std::string temp_out_filename