From de2202a0514c5e16396fa0a83c315ff3003f7e96 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 28 Apr 2019 11:35:24 +0100 Subject: [PATCH 1/2] Make smt2_convt inherit from stack_decision_proceduret directly --- src/solvers/smt2/smt2_conv.h | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index 26f02603f12..bb109ed3cea 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -31,7 +31,7 @@ class constant_exprt; class index_exprt; class member_exprt; -class smt2_convt:public prop_convt +class smt2_convt : public stack_decision_proceduret { public: enum class solvert @@ -114,7 +114,6 @@ class smt2_convt:public prop_convt bool emit_set_logic; exprt handle(const exprt &expr) override; - literalt convert(const exprt &expr) override; void set_to(const exprt &expr, bool value) override; exprt get(const exprt &expr) const override; std::string decision_procedure_text() const override @@ -122,7 +121,6 @@ class smt2_convt:public prop_convt return "SMT2"; } void print_assignment(std::ostream &out) const override; - tvt l_get(literalt l) const override; /// Unimplemented void push() override; @@ -183,6 +181,9 @@ class smt2_convt:public prop_convt std::string convert_identifier(const irep_idt &identifier); + literalt convert(const exprt &expr); + tvt l_get(literalt l) const; + // auxiliary methods exprt prepare_for_convert_expr(const exprt &expr); exprt lower_byte_operators(const exprt &expr); From 1f754295956368aef4f1e17779800f87bf2dca10 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 28 Apr 2019 11:40:02 +0100 Subject: [PATCH 2/2] Clean-up smt2_convt interface Move definitions into .cpp file and make functions protected that don't need to be public. --- src/solvers/smt2/smt2_conv.cpp | 64 +++++++++++++++++++++++++++++++ src/solvers/smt2/smt2_conv.h | 69 ++++------------------------------ 2 files changed, 72 insertions(+), 61 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 40b002f9d0c..00dc414bda3 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -42,6 +42,70 @@ Author: Daniel Kroening, kroening@kroening.com // General todos #define SMT2_TODO(S) PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S) +smt2_convt::smt2_convt( + const namespacet &_ns, + const std::string &_benchmark, + const std::string &_notes, + const std::string &_logic, + solvert _solver, + std::ostream &_out) + : use_FPA_theory(false), + use_datatypes(false), + use_array_of_bool(false), + emit_set_logic(true), + ns(_ns), + out(_out), + benchmark(_benchmark), + notes(_notes), + logic(_logic), + solver(_solver), + boolbv_width(_ns), + pointer_logic(_ns), + no_boolean_variables(0) +{ + // We set some defaults differently + // for some solvers. + + switch(solver) + { + case solvert::GENERIC: + break; + + case solvert::BOOLECTOR: + break; + + case solvert::CPROVER_SMT2: + use_array_of_bool = true; + emit_set_logic = false; + break; + + case solvert::CVC3: + break; + + case solvert::CVC4: + break; + + case solvert::MATHSAT: + break; + + case solvert::YICES: + break; + + case solvert::Z3: + use_array_of_bool = true; + emit_set_logic = false; + use_datatypes = true; + break; + } + + write_header(); +} + +std::string smt2_convt::decision_procedure_text() const +{ + return "SMT2"; +} + void smt2_convt::print_assignment(std::ostream &os) const { // Boolean stuff diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index bb109ed3cea..b66883496bc 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -52,61 +52,9 @@ class smt2_convt : public stack_decision_proceduret const std::string &_notes, const std::string &_logic, solvert _solver, - std::ostream &_out) - : use_FPA_theory(false), - use_datatypes(false), - use_array_of_bool(false), - emit_set_logic(true), - ns(_ns), - out(_out), - benchmark(_benchmark), - notes(_notes), - logic(_logic), - solver(_solver), - boolbv_width(_ns), - pointer_logic(_ns), - no_boolean_variables(0) - { - // We set some defaults differently - // for some solvers. - - switch(solver) - { - case solvert::GENERIC: - break; - - case solvert::BOOLECTOR: - break; - - case solvert::CPROVER_SMT2: - use_array_of_bool = true; - emit_set_logic = false; - break; - - case solvert::CVC3: - break; - - case solvert::CVC4: - break; - - case solvert::MATHSAT: - break; - - case solvert::YICES: - break; - - case solvert::Z3: - use_array_of_bool=true; - emit_set_logic=false; - use_datatypes=true; - break; - } - - write_header(); - } + std::ostream &_out); ~smt2_convt() override = default; - resultt dec_solve() override; bool use_FPA_theory; bool use_datatypes; @@ -116,10 +64,7 @@ class smt2_convt : public stack_decision_proceduret exprt handle(const exprt &expr) override; void set_to(const exprt &expr, bool value) override; exprt get(const exprt &expr) const override; - std::string decision_procedure_text() const override - { - return "SMT2"; - } + std::string decision_procedure_text() const override; void print_assignment(std::ostream &out) const override; /// Unimplemented @@ -131,10 +76,6 @@ class smt2_convt : public stack_decision_proceduret /// Currently, only implements a single stack element (no nested contexts) void pop() override; - void convert_expr(const exprt &); - void convert_type(const typet &); - void convert_literal(const literalt); - std::size_t get_number_of_solver_calls() const override; protected: @@ -148,6 +89,8 @@ class smt2_convt : public stack_decision_proceduret std::size_t number_of_solver_calls = 0; + resultt dec_solve() override; + void write_header(); void write_footer(std::ostream &); @@ -181,6 +124,10 @@ class smt2_convt : public stack_decision_proceduret std::string convert_identifier(const irep_idt &identifier); + void convert_expr(const exprt &); + void convert_type(const typet &); + void convert_literal(const literalt); + literalt convert(const exprt &expr); tvt l_get(literalt l) const;