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 <algorithm>
16 #include <cstdlib>
17 #include <fstream>
18 #include <sstream>
19 #include <string>
20 
21 external_satt::external_satt(message_handlert &message_handler, std::string cmd)
22  : cnf_clause_list_assignmentt(message_handler), solver_cmd(std::move(cmd))
23 {
24 }
25 
26 const std::string external_satt::solver_text()
27 {
28  return "External SAT solver";
29 }
30 
32 {
34 }
35 
37 {
39 }
40 
41 void external_satt::write_cnf_file(std::string cnf_file)
42 {
43  log.status() << "Writing temporary CNF" << messaget::eom;
44  std::ofstream out(cnf_file);
45 
46  // We start counting at 1, thus there is one variable fewer.
47  out << "p cnf " << (no_variables() - 1) << ' '
48  << no_clauses() + assumptions.size() << '\n';
49 
50  // output the problem clauses
51  for(auto &c : clauses)
52  dimacs_cnft::write_dimacs_clause(c, out, false);
53 
54  // output the assumption clauses
55  for(const auto &literal : assumptions)
56  {
57  if(!literal.is_constant())
58  out << literal.dimacs() << " 0\n";
59  }
60 
61  out.close();
62 }
63 
64 std::string external_satt::execute_solver(std::string cnf_file)
65 {
66  log.status() << "Invoking SAT solver" << messaget::eom;
67  std::ostringstream response_ostream;
68  auto cmd_result = run(solver_cmd, {"", cnf_file}, "", response_ostream, "");
69 
70  log.status() << "Solver returned code: " << cmd_result << messaget::eom;
71  return response_ostream.str();
72 }
73 
75 {
76  std::istringstream response_istream(solver_output);
77  std::string line;
79  std::vector<bool> assigned_variables(no_variables(), false);
80  assignment.insert(assignment.begin(), no_variables(), tvt(false));
81 
82  while(getline(response_istream, line))
83  {
84  if(line[0] == 's')
85  {
86  auto parts = split_string(line, ' ');
87  if(parts.size() < 2)
88  {
89  log.error() << "external SAT solver has provided an unexpected "
90  "response in results.\nUnexpected reponse: "
91  << line << messaget::eom;
92  return resultt::P_ERROR;
93  }
94 
95  auto status = parts[1];
96  log.status() << "result:" << status << messaget::eom;
97  if(status == "UNSATISFIABLE")
98  {
100  }
101  if(status == "SATISFIABLE")
102  {
103  result = resultt::P_SATISFIABLE;
104  }
105  if(status == "TIMEOUT")
106  {
107  log.error() << "external SAT solver reports a timeout" << messaget::eom;
108  return resultt::P_ERROR;
109  }
110  }
111 
112  if(line[0] == 'v')
113  {
114  auto assignments = split_string(line, ' ');
115 
116  // remove the first element which should be 'v' identifying
117  // the line as the satisfying assignments
118  assignments.erase(assignments.begin());
119  auto number_of_variables = no_variables();
120  for(auto &assignment_string : assignments)
121  {
122  try
123  {
124  signed long long as_long = std::stol(assignment_string);
125  size_t index = std::labs(as_long);
126 
127  if(index >= number_of_variables)
128  {
129  log.error() << "SAT assignment " << as_long
130  << " out of range of CBMC largest variable of "
131  << (number_of_variables - 1) << messaget::eom;
132  return resultt::P_ERROR;
133  }
134  assignment[index] = tvt(as_long >= 0);
135  assigned_variables[index] = true;
136  }
137  catch(...)
138  {
139  log.error() << "SAT assignment " << assignment_string
140  << " caused an exception while processing"
141  << messaget::eom;
142  return resultt::P_ERROR;
143  }
144  }
145  // Assignments can span multiple lines so returning early isn't an option
146  }
147  }
148 
149  if(result == resultt::P_SATISFIABLE)
150  {
151  // We don't need to check zero
152  for(size_t index = 1; index < no_variables(); index++)
153  {
154  if(!assigned_variables[index])
155  {
156  log.error() << "No assignment was found for literal: " << index
157  << messaget::eom;
158  return resultt::P_ERROR;
159  }
160  }
161  return resultt::P_SATISFIABLE;
162  }
163 
164  log.error() << "external SAT solver has provided an unexpected response"
165  << messaget::eom;
166  return resultt::P_ERROR;
167 }
168 
170 {
171  // are we assuming 'false'?
172  if(
173  std::find(assumptions.begin(), assumptions.end(), const_literal(false)) !=
174  assumptions.end())
175  {
177  }
178 
179  // create a temporary file
180  temporary_filet cnf_file("external-sat", ".cnf");
181  write_cnf_file(cnf_file());
182  auto output = execute_solver(cnf_file());
183  return parse_result(output);
184 }
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:41
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:36
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:39
external_satt::do_prop_solve
resultt do_prop_solve() override
Definition: external_sat.cpp:169
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:21
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:31
const_literal
literalt const_literal(bool value)
Definition: literal.h:188
external_satt::solver_text
const std::string solver_text() override
Definition: external_sat.cpp:26
message_handlert
Definition: message.h:28
propt::resultt
resultt
Definition: prop.h:99
external_satt::assumptions
bvt assumptions
Definition: external_sat.h:37
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:36
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:64
external_satt::parse_result
resultt parse_result(std::string)
Definition: external_sat.cpp:74