Improve creating strategy solvers and invariants

Instead of allocating strategy solvers and abstract values in
ssa_analyzer based on CLI options, make domains responsible for
allocating adequate solvers.

Each abstract domain must implement methods new_value and
new_strategy_solver that return a unique_ptr to a new abstract value and
new strategy solver for the domain, respectively. These methods are then
called from ssa_analyzer, which simplifies the code a lot.

This change required some unification of interfaces of strategy solver
constructors.

Author: viktormalik

src/2ls/dynamic_cfg.h

@@ -14,6 +14,7 @@ Author: Peter Schrammel
 
 #include <util/std_expr.h>
 #include <util/graph.h>
+#include <util/i2string.h>
 #include <goto-programs/goto_program.h>
 
 #include <ssa/ssa_unwinder.h>

src/domains/domain.h

@@ -21,10 +21,13 @@ Author: Peter Schrammel
 #include <util/replace_expr.h>
 #include <util/namespace.h>
 #include <solvers/refinement/bv_refinement.h>
+#include <memory>
 #include "symbolic_path.h"
+#include "incremental_solver.h"
 
 // Forward declaration - real is in template_generator_base.h
 class template_generator_baset;
+class strategy_solver_baset;
 
 class local_SSAt;
 
@@ -104,6 +107,14 @@ class domaint
     basic_valuet basic_value;
   };
 
+  /// Create a new empty abstract value for the domain
+  virtual std::unique_ptr<valuet> new_value()=0;
+  /// Create a new strategy solver for the domain
+  virtual std::unique_ptr<strategy_solver_baset> new_strategy_solver(
+    incremental_solvert &,
+    const local_SSAt &,
+    message_handlert &)=0;
+
   // General methods for the strategy solver
   // Each generic strategy solver should implement at least these.
 

src/domains/equality_domain.h

@@ -63,6 +63,11 @@ class equality_domaint:public simple_domaint
     equ_valuet *clone() override { return new equ_valuet(*this); }
   };
 
+  std::unique_ptr<domaint::valuet> new_value() override
+  {
+    return std::unique_ptr<domaint::valuet>(new equ_valuet());
+  }
+
   void initialize() override;
 
   void initialize_value(domaint::valuet &value) override;

src/domains/heap_domain.h

@@ -87,6 +87,11 @@ class heap_domaint:public simple_domaint
     heap_valuet *clone() override { return new heap_valuet(*this); }
   };
 
+  std::unique_ptr<domaint::valuet> new_value() override
+  {
+    return std::unique_ptr<domaint::valuet>(new heap_valuet());
+  }
+
   // Initialize value and domain
   void initialize_value(domaint::valuet &value) override;
 

src/domains/incremental_solver.h

@@ -19,7 +19,6 @@ Author: Peter Schrammel
 #include <solvers/refinement/bv_refinement.h>
 #include <solvers/sat/satcheck.h>
 
-#include "domain.h"
 #include "util.h"
 
 // #define DISPLAY_FORMULA

src/domains/lexlinrank_domain.h

@@ -92,6 +92,11 @@ class lexlinrank_domaint:public simple_domaint
     templ_valuet *clone() override { return new templ_valuet(*this); }
   };
 
+  std::unique_ptr<domaint::valuet> new_value() override
+  {
+    return std::unique_ptr<domaint::valuet>(new templ_valuet());
+  }
+
   lexlinrank_domaint(
     unsigned _domain_number,
     replace_mapt &_renaming_map,

src/domains/linrank_domain.h

@@ -69,6 +69,11 @@ class linrank_domaint:public simple_domaint
     templ_valuet *clone() override { return new templ_valuet(*this); }
   };
 
+  std::unique_ptr<domaint::valuet> new_value() override
+  {
+    return std::unique_ptr<domaint::valuet>(new templ_valuet());
+  }
+
   linrank_domaint(
     unsigned _domain_number,
     replace_mapt &_renaming_map,

src/domains/predabs_domain.h

@@ -52,6 +52,11 @@ class predabs_domaint:public simple_domaint
     templ_valuet *clone() override { return new templ_valuet(*this); }
   };
 
+  std::unique_ptr<domaint::valuet> new_value() override
+  {
+    return std::unique_ptr<domaint::valuet>(new templ_valuet());
+  }
+
   predabs_domaint(
     unsigned _domain_number,
     replace_mapt &_renaming_map,

src/domains/product_domain.cpp

@@ -13,6 +13,7 @@ Author: Viktor Malik
 /// Designed to work with strategy_solver_productt.
 
 #include "product_domain.h"
+#include "strategy_solver_product.h"
 
 void product_domaint::initialize_value(domaint::valuet &_value)
 {
@@ -81,3 +82,17 @@ void product_domaint::remove_all_sympath_restrictions()
   for(auto &domain : domains)
     domain->remove_all_sympath_restrictions();
 }
+
+std::unique_ptr<strategy_solver_baset> product_domaint::new_strategy_solver(
+  incremental_solvert &solver,
+  const local_SSAt &SSA,
+  message_handlert &message_handler)
+{
+  solver_vect solvers;
+  for(auto &d : domains)
+    solvers.push_back(
+      std::move(d->new_strategy_solver(solver, SSA, message_handler)));
+  return std::unique_ptr<strategy_solver_baset>(
+    new strategy_solver_productt(
+      *this, std::move(solvers), solver, SSA, message_handler));
+}

src/domains/product_domain.h

@@ -48,6 +48,14 @@ class product_domaint:public domaint
     }
   };
 
+  std::unique_ptr<domaint::valuet> new_value() override
+  {
+    value_vect values;
+    for(auto &d : domains)
+      values.push_back(std::move(d->new_value()));
+    return std::unique_ptr<valuet>(new valuet(std::move(values)));
+  }
+
   // Most of the domain methods are implemented in such way that the
   // corresponding method is called for each domain.
 
@@ -78,6 +86,11 @@ class product_domaint:public domaint
     return result;
   }
 
+  std::unique_ptr<strategy_solver_baset> new_strategy_solver(
+    incremental_solvert &solvert,
+    const local_SSAt &at,
+    message_handlert &handlert) override;
+
   // Product domain contains a vector of domains
   domain_vect domains;