Add option to create printing solver

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;

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;

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);

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) {

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)