Merge pull request #4577 from peterschrammel/do-not-expose-set-frozen

Do not expose set frozen [depends: 4573]

Author: peterschrammel

src/goto-checker/bmc_util.cpp

@@ -365,7 +365,6 @@ std::chrono::duration<double> prepare_property_decider(
   property_decider.update_properties_goals_from_symex_target_equation(
     properties);
   property_decider.convert_goals();
-  property_decider.freeze_goal_variables();
 
   auto solver_stop = std::chrono::steady_clock::now();
   return std::chrono::duration<double>(solver_stop - solver_start);

src/goto-checker/goto_symex_property_decider.cpp

@@ -74,16 +74,7 @@ void goto_symex_property_decidert::convert_goals()
     // Our goal is to falsify a property, i.e., we will
     // add the negation of the property as goal.
     goal_pair.second.condition =
-      !solver->prop_conv().convert(goal_pair.second.as_expr());
-  }
-}
-
-void goto_symex_property_decidert::freeze_goal_variables()
-{
-  for(const auto &goal_pair : goal_map)
-  {
-    if(!goal_pair.second.condition.is_constant())
-      solver->prop_conv().set_frozen(goal_pair.second.condition);
+      solver->prop_conv().handle(not_exprt(goal_pair.second.as_expr()));
   }
 }
 
@@ -98,7 +89,7 @@ void goto_symex_property_decidert::add_constraint_from_goals(
       select_property(goal_pair.first) &&
       !goal_pair.second.condition.is_false())
     {
-      disjuncts.push_back(literal_exprt(goal_pair.second.condition));
+      disjuncts.push_back(goal_pair.second.condition);
     }
   }
 
@@ -134,7 +125,7 @@ void goto_symex_property_decidert::update_properties_status_from_goals(
     {
       auto &status = properties.at(goal_pair.first).status;
       if(
-        solver->prop_conv().l_get(goal_pair.second.condition).is_true() &&
+        solver->prop_conv().get(goal_pair.second.condition).is_true() &&
         status != property_statust::FAIL)
       {
         status |= property_statust::FAIL;

src/goto-checker/goto_symex_property_decider.h

@@ -79,7 +79,7 @@ class goto_symex_property_decidert
     std::vector<symex_target_equationt::SSA_stepst::iterator> instances;
 
     /// The goal variable
-    literalt condition;
+    exprt condition;
 
     exprt as_expr() const;
   };

src/solvers/decision_procedure.h

@@ -30,9 +30,13 @@ class decision_proceduret
   /// For a Boolean expression \p expr, add the constraint 'not expr'
   void set_to_false(const exprt &expr);
 
-  /// Generate a handle for an expression; this offers an efficient way
+  /// Generate a handle, which is an expression that
+  /// has the same value as the argument in any model
+  /// that is generated; this offers an efficient way
   /// to refer to the expression in subsequent calls to \ref get or
-  /// \ref set_to
+  /// \ref set_to.
+  /// The returned expression may be the expression itself or a more compact
+  /// but solver-specific representation.
   virtual exprt handle(const exprt &expr) = 0;
 
   /// Result of running the decision procedure

src/solvers/prop/prop_conv.cpp

@@ -14,41 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <algorithm>
 
-exprt prop_convt::handle(const exprt &expr)
-{
-  // We can only improve Booleans.
-  if(expr.type().id() != ID_bool)
-    return expr;
-
-  // We convert to a literal to obtain a 'small' handle
-  literalt l = convert(expr);
-
-  // The literal may be a constant as a result of non-trivial
-  // propagation. We return constants as such.
-  if(l.is_true())
-    return true_exprt();
-  else if(l.is_false())
-    return false_exprt();
-
-  // freeze to enable incremental use
-  set_frozen(l);
-
-  return literal_exprt(l);
-}
-
 void prop_convt::set_assumptions(const bvt &)
 {
   UNREACHABLE;
 }
-
-void prop_convt::set_frozen(const literalt)
-{
-  UNREACHABLE;
-}
-
-void prop_convt::set_frozen(const bvt &bv)
-{
-  for(const auto &bit : bv)
-    if(!bit.is_constant())
-      set_frozen(bit);
-}

src/solvers/prop/prop_conv.h

@@ -26,13 +26,6 @@ class prop_convt:public decision_proceduret
 
   using decision_proceduret::operator();
 
-  /// returns a 'handle', which is an expression that
-  /// has the same value as the argument in any model
-  /// that is generated.
-  /// This may be the expression itself or a more compact
-  /// but solver-specific representation.
-  exprt handle(const exprt &expr) override;
-
   /// Convert a Boolean expression and return the corresponding literal
   virtual literalt convert(const exprt &expr) = 0;
 
@@ -41,11 +34,8 @@ class prop_convt:public decision_proceduret
   virtual tvt l_get(literalt l) const = 0;
 
   // incremental solving
-  virtual void set_frozen(literalt a);
-  virtual void set_frozen(const bvt &);
   virtual void set_assumptions(const bvt &_assumptions);
   virtual bool has_set_assumptions() const { return false; }
-  virtual void set_all_frozen() {}
 };
 
 #endif // CPROVER_SOLVERS_PROP_PROP_CONV_H

src/solvers/prop/prop_conv_solver.cpp

@@ -15,6 +15,45 @@ bool prop_conv_solvert::is_in_conflict(const exprt &expr) const
   return prop.is_in_conflict(to_literal_expr(expr).get_literal());
 }
 
+void prop_conv_solvert::set_frozen(const bvt &bv)
+{
+  for(const auto &bit : bv)
+    if(!bit.is_constant())
+      set_frozen(bit);
+}
+
+void prop_conv_solvert::set_frozen(literalt a)
+{
+  prop.set_frozen(a);
+}
+
+void prop_conv_solvert::set_all_frozen()
+{
+  freeze_all = true;
+}
+
+exprt prop_conv_solvert::handle(const exprt &expr)
+{
+  // We can only improve Booleans.
+  if(expr.type().id() != ID_bool)
+    return expr;
+
+  // We convert to a literal to obtain a 'small' handle
+  literalt l = convert(expr);
+
+  // The literal may be a constant as a result of non-trivial
+  // propagation. We return constants as such.
+  if(l.is_true())
+    return true_exprt();
+  else if(l.is_false())
+    return false_exprt();
+
+  // freeze to enable incremental use
+  set_frozen(l);
+
+  return literal_exprt(l);
+}
+
 bool prop_conv_solvert::literal(const symbol_exprt &expr, literalt &dest) const
 {
   PRECONDITION(expr.type().id() == ID_bool);

src/solvers/prop/prop_conv_solver.h

@@ -46,16 +46,10 @@ class prop_conv_solvert : public conflict_providert,
   }
   exprt get(const exprt &expr) const override;
 
-  // overloading from prop_convt
-  using prop_convt::set_frozen;
   tvt l_get(literalt a) const override
   {
     return prop.l_get(a);
   }
-  void set_frozen(literalt a) override
-  {
-    prop.set_frozen(a);
-  }
   void set_assumptions(const bvt &_assumptions) override
   {
     prop.set_assumptions(_assumptions);
@@ -64,10 +58,13 @@ class prop_conv_solvert : public conflict_providert,
   {
     return prop.has_set_assumptions();
   }
-  void set_all_frozen() override
-  {
-    freeze_all = true;
-  }
+
+  exprt handle(const exprt &expr) override;
+
+  void set_frozen(literalt);
+  void set_frozen(const bvt &);
+  void set_all_frozen();
+
   literalt convert(const exprt &expr) override;
   bool is_in_conflict(const exprt &expr) const override;
 

src/solvers/smt2/smt2_conv.cpp

@@ -661,6 +661,15 @@ literalt smt2_convt::convert(const exprt &expr)
   return l;
 }
 
+exprt smt2_convt::handle(const exprt &expr)
+{
+  // We can only improve Booleans.
+  if(expr.type().id() != ID_bool)
+    return expr;
+
+  return literal_exprt(convert(expr));
+}
+
 void smt2_convt::convert_literal(const literalt l)
 {
   if(l==const_literal(false))

src/solvers/smt2/smt2_conv.h

@@ -113,10 +113,8 @@ class smt2_convt:public prop_convt
   bool use_array_of_bool;
   bool emit_set_logic;
 
+  exprt handle(const exprt &expr) override;
   literalt convert(const exprt &expr) override;
-  void set_frozen(literalt) override
-  { /* not needed */
-  }
   void set_to(const exprt &expr, bool value) override;
   exprt get(const exprt &expr) const override;
   std::string decision_procedure_text() const override