cprover
external_sat.cpp
Go to the documentation of this file.
1 
6 #include "external_sat.h"
7 
8 #include "dimacs_cnf.h"
9 
10 #include <util/exception_utils.h>
11 #include <util/run.h>
12 #include <util/string_utils.h>
13 #include <util/tempfile.h>
14 
15 #include <chrono>
16 #include <cstdlib>
17 #include <fstream>
18 #include <random>
19 #include <sstream>
20 #include <string>
21 #include <thread>
22 
23 external_satt::external_satt(message_handlert &message_handler, std::string cmd)
24  : cnf_clause_list_assignmentt(message_handler), solver_cmd(std::move(cmd))
25 {
26 }
27 
28 const std::string external_satt::solver_text()
29 {
30  return "External SAT solver";
31 }
32 
34 {
36 }
37 
39 {
41 }
42 
43 void external_satt::write_cnf_file(std::string cnf_file)
44 {
45  log.status() << "Writing temporary CNF" << messaget::eom;
46  std::ofstream out(cnf_file);
47 
48  // We start counting at 1, thus there is one variable fewer.
49  out << "p cnf " << (no_variables() - 1) << ' ' << no_clauses() << '\n';
50 
51  for(auto &c : clauses)
52  dimacs_cnft::write_dimacs_clause(c, out, false);
53 
54  out.close();
55 }
56 
57 std::string external_satt::execute_solver(std::string cnf_file)
58 {
59  log.status() << "Invoking SAT solver" << messaget::eom;
60  std::ostringstream response_ostream;
61  auto cmd_result = run(solver_cmd, {"", cnf_file}, "", response_ostream, "");
62 
63  log.status() << "Solver returned code: " << cmd_result << messaget::eom;
64  return response_ostream.str();
65 }
66 
68 {
69  std::istringstream response_istream(solver_output);
70  std::string line;
72  std::vector<bool> assigned_variables(no_variables(), false);
73  assignment.insert(assignment.begin(), no_variables(), tvt(false));
74 
75  while(getline(response_istream, line))
76  {
77  if(line[0] == 's')
78  {
79  auto parts = split_string(line, ' ');
80  if(parts.size() < 2)
81  {
82  log.error() << "external SAT solver has provided an unexpected "
83  "response in results.\nUnexpected reponse: "
84  << line << messaget::eom;
85  return resultt::P_ERROR;
86  }
87 
88  auto status = parts[1];
89  log.status() << "result:" << status << messaget::eom;
90  if(status == "UNSATISFIABLE")
91  {
93  }
94  if(status == "SATISFIABLE")
95  {
96  result = resultt::P_SATISFIABLE;
97  }
98  if(status == "TIMEOUT")
99  {
100  log.error() << "external SAT solver reports a timeout" << messaget::eom;
101  return resultt::P_ERROR;
102  }
103  }
104 
105  if(line[0] == 'v')
106  {
107  auto assignments = split_string(line, ' ');
108 
109  // remove the first element which should be 'v' identifying
110  // the line as the satisfying assignments
111  assignments.erase(assignments.begin());
112  auto number_of_variables = no_variables();
113  for(auto &assignment_string : assignments)
114  {
115  try
116  {
117  signed long long as_long = std::stol(assignment_string);
118  size_t index = std::labs(as_long);
119 
120  if(index >= number_of_variables)
121  {
122  log.error() << "SAT assignment " << as_long
123  << " out of range of CBMC largest variable of "
124  << (number_of_variables - 1) << messaget::eom;
125  return resultt::P_ERROR;
126  }
127  assignment[index] = tvt(as_long >= 0);
128  assigned_variables[index] = true;
129  }
130  catch(...)
131  {
132  log.error() << "SAT assignment " << assignment_string
133  << " caused an exception while processing"
134  << messaget::eom;
135  return resultt::P_ERROR;
136  }
137  }
138  // Assignments can span multiple lines so returning early isn't an option
139  }
140  }
141 
142  if(result == resultt::P_SATISFIABLE)
143  {
144  // We don't need to check zero
145  for(size_t index = 1; index < no_variables(); index++)
146  {
147  if(!assigned_variables[index])
148  {
149  log.error() << "No assignment was found for literal: " << index
150  << messaget::eom;
151  return resultt::P_ERROR;
152  }
153  }
154  return resultt::P_SATISFIABLE;
155  }
156 
157  log.error() << "external SAT solver has provided an unexpected response"
158  << messaget::eom;
159  return resultt::P_ERROR;
160 }
161 
163 {
164  // create a temporary file
165  temporary_filet cnf_file("external-sat", ".cnf");
166  write_cnf_file(cnf_file());
167  auto output = execute_solver(cnf_file());
168  return parse_result(output);
169 }
exception_utils.h
tempfile.h
UNIMPLEMENTED
#define UNIMPLEMENTED
Definition: invariant.h:523
cnf_clause_listt::clauses
clausest clauses
Definition: cnf_clause_list.h:85
string_utils.h
messaget::status
mstreamt & status() const
Definition: message.h:414
propt::resultt::P_UNSATISFIABLE
@ P_UNSATISFIABLE
cnf_clause_list_assignmentt
Definition: cnf_clause_list.h:92
run
int run(const std::string &what, const std::vector< std::string > &argv)
Definition: run.cpp:49
external_satt::write_cnf_file
void write_cnf_file(std::string)
Definition: external_sat.cpp:43
messaget::eom
static eomt eom
Definition: message.h:297
run.h
dimacs_cnft::write_dimacs_clause
static void write_dimacs_clause(const bvt &, std::ostream &, bool break_lines)
Definition: dimacs_cnf.cpp:54
external_satt::solver_cmd
std::string solver_cmd
Definition: external_sat.h:32
cnf_clause_listt::no_clauses
size_t no_clauses() const override
Definition: cnf_clause_list.h:42
split_string
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Definition: string_utils.cpp:40
external_satt::do_prop_solve
resultt do_prop_solve() override
Definition: external_sat.cpp:162
messaget::error
mstreamt & error() const
Definition: message.h:399
external_sat.h
Allows calling an external SAT solver to allow faster integration of newer SAT solvers.
propt::resultt::P_ERROR
@ P_ERROR
propt::resultt::P_SATISFIABLE
@ P_SATISFIABLE
external_satt::external_satt
external_satt(message_handlert &message_handler, std::string cmd)
Definition: external_sat.cpp:23
external_satt::is_in_conflict
bool is_in_conflict(literalt) const override
Returns true if an assumption is in the final conflict.
Definition: external_sat.cpp:33
external_satt::solver_text
const std::string solver_text() override
Definition: external_sat.cpp:28
message_handlert
Definition: message.h:28
propt::resultt
resultt
Definition: prop.h:99
tvt
Definition: threeval.h:20
dimacs_cnf.h
literalt
Definition: literal.h:26
propt::log
messaget log
Definition: prop.h:130
cnft::no_variables
virtual size_t no_variables() const override
Definition: cnf.h:41
external_satt::set_assignment
void set_assignment(literalt, bool) override
Definition: external_sat.cpp:38
cnf_clause_list_assignmentt::assignment
assignmentt assignment
Definition: cnf_clause_list.h:126
temporary_filet
Definition: tempfile.h:24
external_satt::execute_solver
std::string execute_solver(std::string)
Definition: external_sat.cpp:57
external_satt::parse_result
resultt parse_result(std::string)
Definition: external_sat.cpp:67