Add option to create printing solver (stanford-centaur#343)

This allows the user to set an option, `--printing-smt-solver`, that will result in a solver instance being constructed using the `create_printing_solver` function in smt-switch. This will dump all formulas sent to the solver by Pono in SMT-LIB format. This allows one to replay the queries in the standalone solvers and is useful for debugging. Also fixed some related comments and header includes.
CyanoKobalamyne · Aug 29, 2024 · 2451303 · 2451303
1 parent f4583db
commit 2451303
Show file tree

Hide file tree

Showing 5 changed files with 47 additions and 25 deletions.
diff --git a/options/options.cpp b/options/options.cpp
@@ -45,6 +45,7 @@ enum optionIndex
   CLK,
   SMT_SOLVER,
   LOGGING_SMT_SOLVER,
+  PRINTING_SMT_SOLVER,
   NO_IC3_PREGEN,
   NO_IC3_INDGEN,
   IC3_GEN_MAX_ITER,
@@ -186,6 +187,14 @@ const option::Descriptor usage[] = {
     "guarantees the exact term structure that was created. Good "
     "for avoiding term rewriting at the API level or sort aliasing. "
     "(default: false)" },
+  { PRINTING_SMT_SOLVER,
+    0,
+    "",
+    "printing-smt-solver",
+    Arg::None,
+    "  --printing-smt-solver \tDump all SMT queries to standard error output "
+    "in SMT-LIB format while solving. Uses smt-switch's create_printing_solver "
+    "function. (default: false)" },
   { WITNESS,
     0,
     "",
@@ -685,6 +694,7 @@ ProverResult PonoOptions::parse_and_set_options(int argc,
           break;
         }
         case LOGGING_SMT_SOLVER: logging_smt_solver_ = true; break;
+        case PRINTING_SMT_SOLVER: printing_smt_solver_ = true; break;
         case WITNESS: witness_ = true; break;
         case STATICCOI: static_coi_ = true; break;
         case SHOW_INVAR: show_invar_ = true; break;

diff --git a/options/options.h b/options/options.h
@@ -96,6 +96,7 @@ class PonoOptions
         random_seed_(default_random_seed),
         smt_solver_(default_smt_solver_),
         logging_smt_solver_(default_logging_smt_solver_),
+        printing_smt_solver_(default_printing_smt_solver_),
         static_coi_(default_static_coi_),
         show_invar_(default_show_invar_),
         check_invar_(default_check_invar_),
@@ -187,6 +188,7 @@ class PonoOptions
   std::string filename_;
   smt::SolverEnum smt_solver_;  ///< underlying smt solver
   bool logging_smt_solver_;
+  bool printing_smt_solver_;
   bool static_coi_;
   bool show_invar_;   ///< display invariant when running from command line
   bool check_invar_;  ///< check invariants (if available) when run through CLI
@@ -307,6 +309,7 @@ class PonoOptions
   //      good solver for the provided engine automatically
   static const smt::SolverEnum default_smt_solver_ = smt::BTOR;
   static const bool default_logging_smt_solver_ = false;
+  static const bool default_printing_smt_solver_ = false;
   static const bool default_ic3_pregen_ = true;
   static const bool default_ic3_indgen_ = true;
   static const unsigned int default_ic3_gen_max_iter_ = 2;

diff --git a/pono.cpp b/pono.cpp
@@ -14,19 +14,14 @@
 **
 **/
 
+#include <cassert>
 #include <csignal>
 #include <iostream>
-#include "assert.h"
 
 #ifdef WITH_PROFILING
 #include <gperftools/profiler.h>
 #endif
 
-#include "smt-switch/boolector_factory.h"
-#ifdef WITH_MSAT
-#include "smt-switch/msat_factory.h"
-#endif
-
 #include "core/fts.h"
 #include "frontends/btor2_encoder.h"
 #include "frontends/smv_encoder.h"
@@ -41,8 +36,8 @@
 #include "smt-switch/logging_solver.h"
 #include "smt/available_solvers.h"
 #include "utils/logger.h"
-#include "utils/timestamp.h"
 #include "utils/make_provers.h"
+#include "utils/timestamp.h"
 #include "utils/ts_analysis.h"
 
 using namespace pono;
@@ -251,7 +246,8 @@ int main(int argc, char ** argv)
     SmtSolver s = create_solver_for(pono_options.smt_solver_,
                                     pono_options.engine_,
                                     false,
-                                    pono_options.ceg_prophecy_arrays_);
+                                    pono_options.ceg_prophecy_arrays_,
+                                    pono_options.printing_smt_solver_);
 
     if (pono_options.logging_smt_solver_) {
       s = make_shared<LoggingSolver>(s);

diff --git a/smt/available_solvers.cpp b/smt/available_solvers.cpp
@@ -16,11 +16,14 @@
 
 #include "smt/available_solvers.h"
 
+#include <cassert>
+#include <iostream>
 #include <unordered_map>
 #include <unordered_set>
 #include <vector>
 
-#include "assert.h"
+#include "smt-switch/logging_solver.h"
+#include "smt-switch/printing_solver.h"
 
 // these two always included
 #include "smt-switch/boolector_factory.h"
@@ -34,10 +37,8 @@
 #include "smt-switch/msat_factory.h"
 // these are for setting specific options
 // e.g. in create_solver_for
-#include "smt-switch/logging_solver.h"
 #include "smt-switch/msat_solver.h"
 #include "smt/msat_options.h"
-
 #endif
 
 #if WITH_YICES2
@@ -68,16 +69,18 @@ const std::vector<SolverEnum> solver_enums({
 
 // internal method for creating a particular solver
 // doesn't set any options
-SmtSolver create_solver_base(SolverEnum se, bool logging)
+SmtSolver create_solver_base(SolverEnum se, bool logging, bool printing = false)
 {
   SmtSolver s;
+  auto printing_style = smt::PrintingStyleEnum::DEFAULT_STYLE;
   switch (se) {
     case BTOR: {
       s = BoolectorSolverFactory::create(logging);
       break;
     }
     case CVC5: {
       s = Cvc5SolverFactory::create(logging);
+      printing_style = smt::PrintingStyleEnum::CVC5_STYLE;
       break;
     }
 #if WITH_BITWUZLA
@@ -89,6 +92,7 @@ SmtSolver create_solver_base(SolverEnum se, bool logging)
 #if WITH_MSAT
     case MSAT: {
       s = MsatSolverFactory::create(logging);
+      printing_style = smt::PrintingStyleEnum::MSAT_STYLE;
       break;
     }
 #endif
@@ -103,26 +107,29 @@ SmtSolver create_solver_base(SolverEnum se, bool logging)
     }
   }
 
+  if (printing) {
+    s = smt::create_printing_solver(s, &cerr, printing_style);
+  }
+
   return s;
 }
 
 SmtSolver create_solver(SolverEnum se,
                         bool logging,
                         bool incremental,
-                        bool produce_model)
+                        bool produce_model,
+                        bool printing)
 {
-  SmtSolver s = create_solver_base(se, logging);
+  SmtSolver s = create_solver_base(se, logging, printing);
 
   s->set_opt("incremental", incremental ? "true" : "false");
   s->set_opt("produce-models", produce_model ? "true" : "false");
 
   return s;
 }
 
-SmtSolver create_solver_for(SolverEnum se,
-                            Engine e,
-                            bool logging,
-                            bool full_model)
+SmtSolver create_solver_for(
+    SolverEnum se, Engine e, bool logging, bool full_model, bool printing)
 {
   SmtSolver s;
   bool ic3_engine = ic3_variants().find(e) != ic3_variants().end();
@@ -133,7 +140,7 @@ SmtSolver create_solver_for(SolverEnum se,
 
   if (se != MSAT) {
     // no special options yet for solvers other than mathsat
-    s = create_solver(se, logging);
+    s = create_solver(se, logging, true, true, printing);
   }
 #ifdef WITH_MSAT
   else if (se == MSAT && ic3_engine) {

diff --git a/smt/available_solvers.h b/smt/available_solvers.h
@@ -16,7 +16,8 @@
 
 #pragma once
 
-#include <iostream>
+#include <unordered_set>
+#include <vector>
 
 #include "options/options.h"
 #include "smt-switch/smt.h"
@@ -27,12 +28,16 @@ namespace pono {
  *  @param se the SolverEnum to identify which type of solver
  *  @param logging whether or not to keep track of term DAG at smt-switch level
  *         defaults to false because generally slower
- *  @param set the incremental option for the solver
- *  @param set the procude-model option for the solver
+ *  @param incremental set the incremental option for the solver
+ *  @param produce_model set the produce-model option for the solver
+ *  @param printing whether or not dump SMT-LIB sent to solver to standard error
  *  @return an SmtSolver
  */
-smt::SmtSolver create_solver(smt::SolverEnum se, bool logging=false,
-                             bool incremental=true, bool produce_model=true);
+smt::SmtSolver create_solver(smt::SolverEnum se,
+                             bool logging = false,
+                             bool incremental = true,
+                             bool produce_model = true,
+                             bool printing = false);
 
 // same as create_solver but will set reasonable options
 // for particular engines (mostly IC3-variants)
@@ -44,7 +49,8 @@ smt::SmtSolver create_solver(smt::SolverEnum se, bool logging=false,
 smt::SmtSolver create_solver_for(smt::SolverEnum se,
                                  Engine e,
                                  bool logging,
-                                 bool full_model = false);
+                                 bool full_model = false,
+                                 bool printing = false);
 
 // same as create_solver but will set reasonable options
 // for a reducing solver (e.g. produce-models off)