Skip to content

Commit 5addeaf

Browse files
committed
Updated documentation and removed unused exception
1 parent c5f53f2 commit 5addeaf

File tree

3 files changed

+18
-23
lines changed

3 files changed

+18
-23
lines changed

src/cbmc/cbmc_parse_options.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1116,7 +1116,7 @@ void cbmc_parse_optionst::help()
11161116
" --yices use Yices\n"
11171117
" --z3 use Z3\n"
11181118
" --refine use refinement procedure (experimental)\n"
1119-
" --sat-solver-invocation cmd command to invoke SAT solver process (experimental)\n"
1119+
" --sat-solver-invocation cmd command to invoke SAT solver process\n"
11201120
HELP_STRING_REFINEMENT_CBMC
11211121
" --outfile filename output formula to given file\n"
11221122
" --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)

src/solvers/sat/external_sat.cpp

Lines changed: 9 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,7 @@
1-
/*******************************************************************\
2-
3-
Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
4-
5-
\*******************************************************************/
1+
/// \file
2+
/// Allows call an external SAT solver to allow faster integration of
3+
/// newer SAT solvers
4+
/// \author Francis Botero <[email protected]>
65

76
#include "external_sat.h"
87

@@ -13,8 +12,6 @@ Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
1312
#include <util/string_utils.h>
1413
#include <util/tempfile.h>
1514

16-
#include <json/json_parser.h>
17-
1815
#include <chrono>
1916
#include <cstdlib>
2017
#include <fstream>
@@ -24,7 +21,7 @@ Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2421
#include <thread>
2522

2623
external_satt::external_satt(message_handlert &message_handler, std::string cmd)
27-
: cnf_clause_list_assignmentt(message_handler), _cmd(std::move(cmd))
24+
: cnf_clause_list_assignmentt(message_handler), solver_cmd(std::move(cmd))
2825
{
2926
}
3027

@@ -43,7 +40,7 @@ void external_satt::set_assignment(literalt, bool)
4340
UNIMPLEMENTED;
4441
}
4542

46-
inline void external_satt::write_cnf_file(std::string cnf_file)
43+
void external_satt::write_cnf_file(std::string cnf_file)
4744
{
4845
log.status() << "Writing temporary CNF" << messaget::eom;
4946
std::ofstream out(cnf_file);
@@ -57,18 +54,17 @@ inline void external_satt::write_cnf_file(std::string cnf_file)
5754
out.close();
5855
}
5956

60-
inline std::string external_satt::execute_solver(std::string cnf_file)
57+
std::string external_satt::execute_solver(std::string cnf_file)
6158
{
6259
log.status() << "Invoking SAT solver" << messaget::eom;
6360
std::ostringstream response_ostream;
64-
auto cmd_result = run(_cmd, {"", cnf_file}, "", response_ostream, "");
61+
auto cmd_result = run(solver_cmd, {"", cnf_file}, "", response_ostream, "");
6562

6663
log.status() << "Solver returned code: " << cmd_result << messaget::eom;
6764
return response_ostream.str();
6865
}
6966

70-
inline external_satt::resultt
71-
external_satt::parse_result(std::string solver_output)
67+
external_satt::resultt external_satt::parse_result(std::string solver_output)
7268
{
7369
std::istringstream response_istream(solver_output);
7470
std::string line;

src/solvers/sat/external_sat.h

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,13 @@
1-
/*******************************************************************\
1+
/// \file
2+
/// Allows call an external SAT solver to allow faster integration of
3+
/// newer SAT solvers
4+
/// \author Francis Botero <[email protected]>
25

3-
Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
46

5-
\*******************************************************************/
6-
7-
#ifndef CPROVER_SOLVERS_EXTERNAL_SAT_SAT_H
8-
#define CPROVER_SOLVERS_EXTERNAL_SAT_SAT_H
7+
#ifndef CPROVER_SOLVERS_SAT_EXTERNAL_SAT_H
8+
#define CPROVER_SOLVERS_SAT_EXTERNAL_SAT_H
99

1010
#include "cnf_clause_list.h"
11-
/// \brief Allows call an external SAT solver to allow faster integration of newer SAT solvers
1211
class external_satt : public cnf_clause_list_assignmentt
1312
{
1413
public:
@@ -31,12 +30,12 @@ class external_satt : public cnf_clause_list_assignmentt
3130

3231
protected:
3332
resultt do_prop_solve() override;
34-
std::string _cmd;
33+
std::string solver_cmd;
3534

3635
private:
3736
inline void write_cnf_file(std::string);
3837
inline std::string execute_solver(std::string);
3938
inline resultt parse_result(std::string);
4039
};
4140

42-
#endif // CPROVER_SOLVERS_EXTERNAL_SAT_SAT_H
41+
#endif // CPROVER_SOLVERS_SAT_EXTERNAL_SAT_H

0 commit comments

Comments
 (0)