From 2451303cf879250dce33685867cef927e29f0bb8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C3=81ron=20Ricardo=20Perez-Lopez?= Date: Thu, 29 Aug 2024 16:08:30 -0400 Subject: [PATCH] Add option to create printing solver (#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. --- options/options.cpp | 10 ++++++++++ options/options.h | 3 +++ pono.cpp | 12 ++++-------- smt/available_solvers.cpp | 29 ++++++++++++++++++----------- smt/available_solvers.h | 18 ++++++++++++------ 5 files changed, 47 insertions(+), 25 deletions(-) diff --git a/options/options.cpp b/options/options.cpp index 8ec0fc3c..f326db5a 100644 --- 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 index 4baaa2db..186d1273 100644 --- 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 index 6f456f9e..05d17a2c 100644 --- a/pono.cpp +++ b/pono.cpp @@ -14,19 +14,14 @@ ** **/ +#include #include #include -#include "assert.h" #ifdef WITH_PROFILING #include #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(s); diff --git a/smt/available_solvers.cpp b/smt/available_solvers.cpp index ebe51c3a..941346e2 100644 --- a/smt/available_solvers.cpp +++ b/smt/available_solvers.cpp @@ -16,11 +16,14 @@ #include "smt/available_solvers.h" +#include +#include #include #include #include -#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,9 +69,10 @@ const std::vector 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); @@ -78,6 +80,7 @@ SmtSolver create_solver_base(SolverEnum se, bool logging) } 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,15 +107,20 @@ 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"); @@ -119,10 +128,8 @@ SmtSolver create_solver(SolverEnum se, 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 index a22e78de..1c020b5c 100644 --- a/smt/available_solvers.h +++ b/smt/available_solvers.h @@ -16,7 +16,8 @@ #pragma once -#include +#include +#include #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)