Do not expose set_frozen

Is only used inside the prop_conv_solvert hierarchy anymore.

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

@@ -18,15 +18,3 @@ 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

@@ -34,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,23 @@ 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.

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);
@@ -67,10 +61,10 @@ class prop_conv_solvert : public conflict_providert,
 
   exprt handle(const exprt &expr) override;
 
-  void set_all_frozen() override
-  {
-    freeze_all = true;
-  }
+  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.h

@@ -115,9 +115,6 @@ class smt2_convt:public prop_convt
 
   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