From d8c584b57e36e1cea6bdc5c6cfcc400cf7e66dd9 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 4 Jul 2026 18:30:28 -0700 Subject: [PATCH] SMT2 backend: move satisfying assignment from smt2_convt to smt2_dect The class smt2_convt performs conversion only, and by design, does not have any means to calculate a satisfying assignment. Hence, this moves the data structures and methods for managing satisfying assignments to smt2_dect. --- src/solvers/smt2/smt2_conv.cpp | 88 -------------------------------- src/solvers/smt2/smt2_conv.h | 24 ++++++--- src/solvers/smt2/smt2_dec.cpp | 91 ++++++++++++++++++++++++++++++++-- src/solvers/smt2/smt2_dec.h | 13 +++++ 4 files changed, 117 insertions(+), 99 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 8ee689aabec..ee99ba84a02 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -37,7 +37,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -140,29 +139,6 @@ std::string smt2_convt::decision_procedure_text() const return "SMT2"; } -void smt2_convt::print_assignment(std::ostream &os) const -{ - // Boolean stuff - - for(std::size_t v=0; vsecond.value; - return expr; - } - else if(expr.id()==ID_nondet_symbol) - { - const irep_idt &id=to_nondet_symbol_expr(expr).get_identifier(); - - identifier_mapt::const_iterator it=identifier_map.find(id); - - if(it!=identifier_map.end()) - return it->second.value; - } - else if(expr.id() == ID_literal) - { - auto l = to_literal_expr(expr).get_literal(); - if(l_get(l).is_true()) - return true_exprt(); - else - return false_exprt(); - } - else if(expr.id() == ID_not) - { - auto op = get(to_not_expr(expr).op()); - if(op == true) - return false_exprt(); - else if(op == false) - return true_exprt(); - } - else if( - expr.is_constant() || expr.id() == ID_empty_union || - (!expr.has_operands() && (expr.id() == ID_struct || expr.id() == ID_array))) - { - return expr; - } - else if(expr.has_operands()) - { - exprt copy = expr; - for(auto &op : copy.operands()) - { - exprt eval_op = get(op); - if(eval_op.is_nil()) - return nil_exprt{}; - op = std::move(eval_op); - } - return copy; - } - - return nil_exprt(); -} - constant_exprt smt2_convt::parse_literal( const irept &src, const typet &type) @@ -1036,11 +953,6 @@ void smt2_convt::convert_literal(const literalt l) } } -void smt2_convt::push() -{ - UNIMPLEMENTED; -} - void smt2_convt::push(const std::vector &_assumptions) { INVARIANT(assumptions.empty(), "nested contexts are not supported"); diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index ca94493a6be..3c19b7f0bae 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -73,12 +72,25 @@ 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; - void print_assignment(std::ostream &out) const override; + + // unimplemented + exprt get(const exprt &expr) const override + { + UNIMPLEMENTED; + } + + // unimplemented + void print_assignment(std::ostream &out) const override + { + UNIMPLEMENTED; + } /// Unimplemented - void push() override; + void push() override + { + UNIMPLEMENTED; + } /// Currently, only implements a single stack element (no nested contexts) void push(const std::vector &_assumptions) override; @@ -164,7 +176,6 @@ class smt2_convt : public stack_decision_proceduret void convert_string_literal(const std::string &); literalt convert(const exprt &expr); - tvt l_get(literalt l) const; // auxiliary methods exprt prepare_for_convert_expr(const exprt &expr); @@ -251,12 +262,10 @@ class smt2_convt : public stack_decision_proceduret // `identifier_map`. bool is_bound; typet type; - exprt value; identifiert(typet type, bool is_bound) : is_bound(is_bound), type(std::move(type)) { - value.make_nil(); } }; @@ -291,7 +300,6 @@ class smt2_convt : public stack_decision_proceduret // Boolean part std::size_t no_boolean_variables; - std::vector boolean_assignment; }; #endif // CPROVER_SOLVERS_SMT2_SMT2_CONV_H diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index cbe6ecb8ebc..52abc715600 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/src/solvers/smt2/smt2_dec.cpp @@ -13,6 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include "smt2irep.h" #include @@ -222,11 +224,11 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in) if(res != resultt::D_SATISFIABLE) return res; - for(auto &assignment : identifier_map) + for(auto &identifier : identifier_map) { - std::string conv_id = drop_quotes(convert_identifier(assignment.first)); + std::string conv_id = drop_quotes(convert_identifier(identifier.first)); const irept &value = parsed_values[conv_id]; - assignment.second.value = parse_rec(value, assignment.second.type); + value_map[identifier.first] = parse_rec(value, identifier.second.type); } // Booleans @@ -277,3 +279,86 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in) return res; } + +void smt2_dect::print_assignment(std::ostream &os) const +{ + // Boolean stuff + + for(std::size_t v = 0; v < boolean_assignment.size(); v++) + os << "b" << v << "=" << boolean_assignment[v] << "\n"; + + // others +} + +tvt smt2_dect::l_get(literalt l) const +{ + if(l.is_true()) + return tvt(true); + if(l.is_false()) + return tvt(false); + + INVARIANT( + l.var_no() < boolean_assignment.size(), + "variable number shall be within bounds"); + return tvt(boolean_assignment[l.var_no()] ^ l.sign()); +} + +exprt smt2_dect::get(const exprt &expr) const +{ + if(expr.id() == ID_symbol) + { + const irep_idt &id = to_symbol_expr(expr).identifier(); + + auto it = value_map.find(id); + + if(it != value_map.end()) + return it->second; + else + return expr; + } + else if(expr.id() == ID_nondet_symbol) + { + const irep_idt &id = to_nondet_symbol_expr(expr).get_identifier(); + + auto it = value_map.find(id); + + if(it != value_map.end()) + return it->second; + } + else if(expr.id() == ID_literal) + { + auto l = to_literal_expr(expr).get_literal(); + if(l_get(l).is_true()) + return true_exprt(); + else + return false_exprt(); + } + else if(expr.id() == ID_not) + { + auto op = get(to_not_expr(expr).op()); + if(op == true) + return false_exprt(); + else if(op == false) + return true_exprt(); + } + else if( + expr.is_constant() || expr.id() == ID_empty_union || + (!expr.has_operands() && (expr.id() == ID_struct || expr.id() == ID_array))) + { + return expr; + } + else if(expr.has_operands()) + { + exprt copy = expr; + for(auto &op : copy.operands()) + { + exprt eval_op = get(op); + if(eval_op.is_nil()) + return nil_exprt{}; + op = std::move(eval_op); + } + return copy; + } + + return nil_exprt(); +} diff --git a/src/solvers/smt2/smt2_dec.h b/src/solvers/smt2/smt2_dec.h index 2b51118aee2..aefbdb9cf84 100644 --- a/src/solvers/smt2/smt2_dec.h +++ b/src/solvers/smt2/smt2_dec.h @@ -10,6 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_SOLVERS_SMT2_SMT2_DEC_H #define CPROVER_SOLVERS_SMT2_SMT2_DEC_H +#include + #include "smt2_conv.h" class message_handlert; @@ -41,6 +43,10 @@ class smt2_dect : protected smt2_stringstreamt, public smt2_convt std::string decision_procedure_text() const override; + void print_assignment(std::ostream &) const override; + + exprt get(const exprt &) const override; + protected: std::string solver_binary_or_empty; message_handlert &message_handler; @@ -51,6 +57,13 @@ class smt2_dect : protected smt2_stringstreamt, public smt2_convt std::stringstream cached_output; resultt read_result(std::istream &in); + + // satisfying assignment + std::vector boolean_assignment; + tvt l_get(literalt) const; + + typedef std::unordered_map value_mapt; + value_mapt value_map; }; #endif // CPROVER_SOLVERS_SMT2_SMT2_DEC_H