SMT2 backend: move satisfying assignment from smt2_convt to smt2_dect

src/solvers/smt2/smt2_conv.cpp

@@ -37,7 +37,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_expr.h>
 #include <util/string2int.h>
 #include <util/string_constant.h>
-#include <util/threeval.h>
 
 #include <solvers/flattening/boolbv_width.h>
 #include <solvers/flattening/c_bit_field_replacement_type.h>
@@ -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; v<boolean_assignment.size(); v++)
-    os << "b" << v << "=" << boolean_assignment[v] << "\n";
-
-  // others
-}
-
-tvt smt2_convt::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());
-}
-
 void smt2_convt::write_header()
 {
   out << "; SMT 2" << "\n";
@@ -300,65 +276,6 @@ decision_proceduret::resultt smt2_convt::dec_solve(const exprt &assumption)
   return decision_proceduret::resultt::D_ERROR;
 }
 
-exprt smt2_convt::get(const exprt &expr) const
-{
-  if(expr.id()==ID_symbol)
-  {
-    const irep_idt &id = to_symbol_expr(expr).identifier();
-
-    identifier_mapt::const_iterator it=identifier_map.find(id);
-
-    if(it!=identifier_map.end())
-      return it->second.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<exprt> &_assumptions)
 {
   INVARIANT(assumptions.empty(), "nested contexts are not supported");

src/solvers/smt2/smt2_conv.h

@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/pointer_expr.h>
 #include <util/std_expr.h>
-#include <util/threeval.h>
 
 #include <cstdint>
 #include <map>
@@ -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<exprt> &_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<bool> boolean_assignment;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_SMT2_CONV_H

src/solvers/smt2/smt2_dec.cpp

@@ -13,6 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/run.h>
 #include <util/tempfile.h>
 
+#include <solvers/prop/literal_expr.h>
+
 #include "smt2irep.h"
 
 #include <fstream>
@@ -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();
+}

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 <util/threeval.h>
+
 #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<bool> boolean_assignment;
+  tvt l_get(literalt) const;
+
+  typedef std::unordered_map<irep_idt, exprt> value_mapt;
+  value_mapt value_map;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_SMT2_DEC_H