Skip to content

Commit bf69ae6

Browse files
committed
Add incremental smt2 solving to solver factory
Because the new smt2 incremental support is being initially introduced in parallel to the existing support, we need the solver factory to make the new separate solver when the new option is specified.
1 parent b0fd00d commit bf69ae6

File tree

6 files changed

+128
-0
lines changed

6 files changed

+128
-0
lines changed

src/goto-checker/solver_factory.cpp

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,7 @@ Author: Daniel Kroening, Peter Schrammel
3232
#include <solvers/sat/dimacs_cnf.h>
3333
#include <solvers/sat/external_sat.h>
3434
#include <solvers/sat/satcheck.h>
35+
#include <solvers/smt2_incremental/smt2_incremental_decision_procedure.h>
3536
#include <solvers/strings/string_refinement.h>
3637

3738
solver_factoryt::solver_factoryt(
@@ -140,6 +141,10 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_solver()
140141
}
141142
else if(options.get_bool_option("refine-strings"))
142143
return get_string_refinement();
144+
const auto incremental_smt2_solver =
145+
options.get_option("incremental-smt2-solver");
146+
if(!incremental_smt2_solver.empty())
147+
return get_incremental_smt2(incremental_smt2_solver);
143148
if(options.get_bool_option("smt2"))
144149
return get_smt2(get_smt2_solver_type());
145150
return get_default();
@@ -321,6 +326,16 @@ solver_factoryt::get_string_refinement()
321326
std::move(decision_procedure), std::move(prop));
322327
}
323328

329+
std::unique_ptr<solver_factoryt::solvert>
330+
solver_factoryt::get_incremental_smt2(std::string solver_command)
331+
{
332+
no_beautification();
333+
334+
return util_make_unique<solvert>(
335+
util_make_unique<smt2_incremental_decision_proceduret>(
336+
std::move(solver_command)));
337+
}
338+
324339
std::unique_ptr<solver_factoryt::solvert>
325340
solver_factoryt::get_smt2(smt2_dect::solvert solver)
326341
{

src/goto-checker/solver_factory.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,7 @@ class solver_factoryt final
7575
std::unique_ptr<solvert> get_external_sat();
7676
std::unique_ptr<solvert> get_bv_refinement();
7777
std::unique_ptr<solvert> get_string_refinement();
78+
std::unique_ptr<solvert> get_incremental_smt2(std::string solver_command);
7879
std::unique_ptr<solvert> get_smt2(smt2_dect::solvert solver);
7980

8081
smt2_dect::solvert get_smt2_solver_type() const;

src/solvers/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -192,6 +192,7 @@ SRC = $(BOOLEFORCE_SRC) \
192192
smt2/smt2_parser.cpp \
193193
smt2/smt2_tokenizer.cpp \
194194
smt2/smt2irep.cpp \
195+
smt2_incremental/smt2_incremental_decision_procedure.cpp \
195196
# Empty last line
196197

197198
include ../common
Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
solvers
2+
util
Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
// Author: Diffblue Ltd.
2+
3+
#include "smt2_incremental_decision_procedure.h"
4+
5+
#include <util/expr.h>
6+
7+
smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
8+
std::string solver_command)
9+
: solver_command{std::move(solver_command)}
10+
{
11+
}
12+
13+
exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)
14+
{
15+
UNIMPLEMENTED;
16+
return exprt();
17+
}
18+
19+
exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
20+
{
21+
UNIMPLEMENTED;
22+
return exprt();
23+
}
24+
25+
void smt2_incremental_decision_proceduret::print_assignment(
26+
std::ostream &out) const
27+
{
28+
UNIMPLEMENTED;
29+
}
30+
31+
std::string
32+
smt2_incremental_decision_proceduret::decision_procedure_text() const
33+
{
34+
return "incremental SMT2 solving via \"" + solver_command + "\"";
35+
}
36+
37+
std::size_t
38+
smt2_incremental_decision_proceduret::get_number_of_solver_calls() const
39+
{
40+
UNIMPLEMENTED;
41+
return 0;
42+
}
43+
44+
void smt2_incremental_decision_proceduret::set_to(const exprt &expr, bool value)
45+
{
46+
UNIMPLEMENTED;
47+
}
48+
49+
void smt2_incremental_decision_proceduret::push(
50+
const std::vector<exprt> &assumptions)
51+
{
52+
UNIMPLEMENTED;
53+
}
54+
55+
void smt2_incremental_decision_proceduret::push()
56+
{
57+
UNIMPLEMENTED;
58+
}
59+
60+
void smt2_incremental_decision_proceduret::pop()
61+
{
62+
UNIMPLEMENTED;
63+
}
64+
65+
decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
66+
{
67+
UNIMPLEMENTED;
68+
return decision_proceduret::resultt::D_SATISFIABLE;
69+
}
Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
// Author: Diffblue Ltd.
2+
3+
/// \file
4+
/// Decision procedure with incremental SMT2 solving.
5+
6+
#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
7+
#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
8+
9+
#include <solvers/stack_decision_procedure.h>
10+
11+
class smt2_incremental_decision_proceduret final
12+
: public stack_decision_proceduret
13+
{
14+
public:
15+
/// \param solver_command: The command and arguments for invoking the smt2
16+
/// solver.
17+
explicit smt2_incremental_decision_proceduret(std::string solver_command);
18+
19+
// Implementation of public decision_proceduret member functions.
20+
exprt handle(const exprt &expr) override;
21+
exprt get(const exprt &expr) const override;
22+
void print_assignment(std::ostream &out) const override;
23+
std::string decision_procedure_text() const override;
24+
std::size_t get_number_of_solver_calls() const override;
25+
void set_to(const exprt &expr, bool value) override;
26+
27+
// Implementation of public stack_decision_proceduret member functions.
28+
void push(const std::vector<exprt> &assumptions) override;
29+
void push() override;
30+
void pop() override;
31+
32+
protected:
33+
// Implementation of protected decision_proceduret member function.
34+
resultt dec_solve() override;
35+
36+
/// This is where we store the solver command for reporting the solver used.
37+
std::string solver_command;
38+
};
39+
40+
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H

0 commit comments

Comments
 (0)