slhv_convt_framework established

src/esbmc/bmc.cpp

@@ -162,6 +162,13 @@ void bmct::generate_smt_from_equation(
     "Encoding to solver time: {}s", time2string(encode_stop - encode_start));
 }
 
+std::string bmct::generate_slhv_smt_from_equation(z3_slhv_convt& slhv_solver, symex_target_equationt &eq) {
+  log_status("generate slhv formula from equation");
+  std::string result;
+
+  return result;
+}
+
 smt_convt::resultt
 bmct::run_decision_procedure(smt_convt &smt_conv, symex_target_equationt &eq)
 {
@@ -190,6 +197,8 @@ bmct::run_decision_procedure(smt_convt &smt_conv, symex_target_equationt &eq)
   return dec_result;
 }
 
+
+
 void bmct::report_success()
 {
   log_success("\nVERIFICATION SUCCESSFUL");
@@ -638,13 +647,21 @@ smt_convt::resultt bmct::run_thread(std::shared_ptr<symex_target_equationt> &eq)
       return smt_convt::P_UNSATISFIABLE;
     }
 
-    if (!options.get_bool_option("smt-during-symex"))
+    if (!options.get_bool_option("smt-during-symex") && !options.get_bool_option("z3-slhv"))
     {
       runtime_solver =
         std::unique_ptr<smt_convt>(create_solver("", ns, options));
       log_status("smt_convt created");
     }
 
+    if (!options.get_bool_option("smt-during-symex") && options.get_bool_option("z3-slhv")) {
+
+      z3_slhv_convt* slhv_conv = new z3_slhv_convt(ns, options);
+      slhv_converter = std::unique_ptr<z3_slhv_convt>(slhv_conv);
+      ;
+      std::string smt_str = generate_slhv_smt_from_equation(*slhv_converter, *eq);
+    }
+
     if (
       options.get_bool_option("multi-property") &&
       options.get_bool_option("base-case"))

src/esbmc/bmc.h

@@ -32,6 +32,7 @@ class bmct
   namespacet ns;
 
   std::unique_ptr<smt_convt> runtime_solver;
+  std::unique_ptr<z3_slhv_convt> slhv_converter;
   std::unique_ptr<reachability_treet> symex;
 
   virtual smt_convt::resultt
@@ -71,6 +72,8 @@ class bmct
 
   void
   generate_smt_from_equation(smt_convt &smt_conv, symex_target_equationt &eq);
+
+  std::string generate_slhv_smt_from_equation(z3_slhv_convt& slhv_solver, symex_target_equationt &eq);
 };
 
 #endif

src/goto-symex/symex_target_equation.h

@@ -10,6 +10,7 @@
 #include <list>
 #include <map>
 #include <solvers/smt/smt_conv.h>
+#include <solvers/z3-slhv/z3_slhv_conv.h>
 #include <util/config.h>
 #include <irep2/irep2.h>
 #include <util/namespace.h>
@@ -72,6 +73,8 @@ class symex_target_equationt : public symex_targett
     const sourcet &source) override;
 
   virtual void convert(smt_convt &smt_conv);
+  std::string convert2slhv(z3_slhv_convt& slhv_convt);
+
   void convert_internal_step(
     smt_convt &smt_conv,
     smt_astt &assumpt_ast,

src/solvers/solve.cpp

@@ -5,6 +5,7 @@
 #include <solvers/smt/smt_array.h>
 #include <solvers/smt/tuple/smt_tuple_node.h>
 #include <solvers/smt/tuple/smt_tuple_sym.h>
+#include <solvers/z3-slhv/z3_slhv_conv.h>
 
 #include <unordered_map>
 
@@ -16,7 +17,6 @@ solver_creator create_new_cvc_solver;
 solver_creator create_new_mathsat_solver;
 solver_creator create_new_yices_solver;
 solver_creator create_new_bitwuzla_solver;
-solver_creator create_new_z3_slhv_solver;
 
 static const std::unordered_map<std::string, solver_creator *> esbmc_solvers = {
 #ifdef SMTLIB
@@ -43,11 +43,10 @@ static const std::unordered_map<std::string, solver_creator *> esbmc_solvers = {
 #ifdef BITWUZLA
   {"bitwuzla", create_new_bitwuzla_solver}
 #endif
-#ifdef Z3_SLHV
-  {"z3-slhv", create_new_z3_slhv_solver}
-#endif
 };
 
+
+
 static const std::string all_solvers[] = {
   "smtlib",
   "z3",
@@ -56,8 +55,7 @@ static const std::string all_solvers[] = {
   "cvc",
   "mathsat",
   "yices",
-  "bitwuzla",
-  "z3-slhv"};
+  "bitwuzla"};
 
 static std::string pick_default_solver()
 {
@@ -124,14 +122,13 @@ smt_convt *create_solver(
   array_iface *array_api = nullptr;
   fp_convt *fp_api = nullptr;
 
+
   solver_creator &factory = pick_solver(solver_name, options);
   smt_convt *ctx = factory(options, ns, &tuple_api, &array_api, &fp_api);
-
   bool node_flat = options.get_bool_option("tuple-node-flattener");
   bool sym_flat = options.get_bool_option("tuple-sym-flattener");
   bool array_flat = options.get_bool_option("array-flattener");
   bool fp_to_bv = options.get_bool_option("fp2bv");
-
   // Pick a tuple flattener to use. If the solver has native support, and no
   // options were given, use that by default
   if (tuple_api != nullptr && !node_flat && !sym_flat)
@@ -145,7 +142,6 @@ smt_convt *create_solver(
   // Default: node flattener
   else
     ctx->set_tuple_iface(new smt_tuple_node_flattener(ctx, ns));
-
   // Pick an array flattener to use. Again, pick the solver native one by
   // default, or the one specified, or if none of the above then use the built
   // in arrays -> to BV flattener.
@@ -155,13 +151,11 @@ smt_convt *create_solver(
     ctx->set_array_iface(new array_convt(ctx));
   else
     ctx->set_array_iface(new array_convt(ctx));
-
   if (fp_api == nullptr || fp_to_bv)
     ctx->set_fp_conv(new fp_convt(ctx));
   else
     ctx->set_fp_conv(fp_api);
-
-  // TODO: SLHV
   ctx->smt_post_init();
   return ctx;
+
 }

src/solvers/solve.h

@@ -14,6 +14,11 @@ typedef smt_convt *(solver_creator)(
   array_iface **array_api,
   fp_convt **fp_api);
 
+// slhv added
+typedef smt_convt *(slhv_solver_creator)(
+  const optionst &options,
+  const namespacet &ns);
+
 smt_convt *create_solver(
   std::string solver_name,
   const namespacet &ns,

src/solvers/z3-slhv/z3_slhv_conv.cpp

@@ -1,16 +1,78 @@
 #include <cassert>
 #include <iostream>
+#include <solvers/smt/smt_conv.h>
 #include <z3_slhv_conv.h>
 
 
-smt_convt *create_new_z3_slhv_solver(
-    const optionst &options,
-    const namespacet &ns
-) {
-    z3_slhv_convt* conv = new z3_slhv_convt(ns, options);
-    return conv;
-}
-
 z3_slhv_convt::z3_slhv_convt(const namespacet &_ns, const optionst& _options) : smt_convt(_ns, _options) {
     // initialize the z3 based slhv converter here
+}
+
+z3_slhv_convt::~z3_slhv_convt() {
+  delete_all_asts();
+}
+void z3_slhv_convt::push_ctx() {
+
+}
+
+void z3_slhv_convt::pop_ctx() {
+
+}
+
+void z3_slhv_convt::assert_ast(smt_astt a) {
+
+}
+
+smt_convt::resultt z3_slhv_convt::dec_solve() {
+  return P_SMTLIB;
+}
+
+const std::string z3_slhv_convt::solver_text() {
+  return "Z3-slhv";
+}
+
+smt_astt z3_slhv_convt::mk_smt_int(const BigInt &theint) {
+
+}
+
+smt_astt z3_slhv_convt::mk_smt_real(const std::string &str) {
+
+}
+
+smt_astt z3_slhv_convt::mk_smt_bv(const BigInt &theint, smt_sortt s) {
+
+}
+smt_astt z3_slhv_convt::mk_smt_bool(bool val){
+
+}
+smt_astt z3_slhv_convt::mk_smt_symbol(const std::string &name, smt_sortt s){
+
+}
+smt_astt z3_slhv_convt::mk_extract(smt_astt a, unsigned int high, unsigned int low){
+
+}
+smt_astt z3_slhv_convt::mk_sign_ext(smt_astt a, unsigned int topwidth){
+
+}
+smt_astt z3_slhv_convt::mk_zero_ext(smt_astt a, unsigned int topwidth){
+
+}
+smt_astt z3_slhv_convt::mk_concat(smt_astt a, smt_astt b){
+
+}
+smt_astt z3_slhv_convt::mk_ite(smt_astt cond, smt_astt t, smt_astt f){
+
+}
+bool z3_slhv_convt::get_bool(smt_astt a){
+
+}
+BigInt z3_slhv_convt::get_bv(smt_astt a, bool is_signed){
+
+}
+smt_astt z3_slhv_convt::overflow_arith(const expr2tc &expr){
+
+}
+
+void z3_slhv_convt::dump_smt(){
+
 }

src/solvers/z3-slhv/z3_slhv_conv.h

@@ -11,10 +11,13 @@ class z3_slhv_smt_ast : public solver_smt_ast<z3::expr>
 {
 public:
   using solver_smt_ast<z3::expr>::solver_smt_ast;
-  ~z3_smt_ast() override = default;
+  ~z3_slhv_smt_ast() override = default;
 
   smt_astt
-  update(smt_convt *ctx, smt_astt value, unsigned int idx, expr2tc idx_expr)
+  update(smt_convt *ctx,
+    smt_astt value,
+    unsigned int idx,
+    expr2tc idx_expr)
     const override;
 
   smt_astt project(smt_convt *ctx, unsigned int elem) const override;
@@ -30,12 +33,15 @@ class z3_slhv_convt : public smt_convt {
     z3_slhv_convt(const namespacet &ns, const optionst &options);
     ~z3_slhv_convt() override;
 public:
+    // interface for translation
+    // TODO slhv: move to the api later, currently we use the smt-lib2 string translation
+    // interfaces of smt_convt need implementation
     void push_ctx() override;
     void pop_ctx() override;
 
     void assert_ast(smt_astt a) override;
-    resultt dec_solver() override;
-    std::string solver_text() override;
+    resultt dec_solve() override;
+    const std::string solver_text() override;
 
     smt_astt mk_smt_int(const BigInt &theint) override;
     smt_astt mk_smt_real(const std::string &str) override;
@@ -49,10 +55,10 @@ class z3_slhv_convt : public smt_convt {
     smt_astt mk_ite(smt_astt cond, smt_astt t, smt_astt f) override;
     bool get_bool(smt_astt a) override;
     BigInt get_bv(smt_astt a, bool is_signed) override;
-    smt_astt overflow_arith(const expr2tc *&expr) override;
+    smt_astt overflow_arith(const expr2tc &expr) override;
 
     void dump_smt() override;
 
-}
+};
 
 #endif