Remove unused logging parameter

stanford-centaur · Sep 14, 2024 · 7f15f34 · 7f15f34
1 parent 58f61e1
commit 7f15f34
Show file tree

Hide file tree

Showing 9 changed files with 10 additions and 15 deletions.
diff --git a/engines/ceg_prophecy_arrays.cpp b/engines/ceg_prophecy_arrays.cpp
@@ -95,7 +95,7 @@ ProverResult CegProphecyArrays<MsatIC3IA>::prove()
     Property latest_prop(super::solver_,
                          super::solver_->make_term(Not, super::bad_));
     SmtSolver s = create_solver_for(super::solver_->get_solver_enum(),
-                                    super::engine_, false);
+                                    super::engine_);
     shared_ptr<Prover> prover = make_prover(super::engine_, latest_prop,
                                             abs_ts_, s, super::options_);
     res = prover->prove();
@@ -147,7 +147,7 @@ ProverResult CegProphecyArrays<Prover_T>::check_until(int k)
       Property latest_prop(super::solver_,
                            super::solver_->make_term(Not, super::bad_));
       SmtSolver s = create_solver_for(super::solver_->get_solver_enum(),
-                                      super::engine_, false);
+                                      super::engine_);
       shared_ptr<Prover> prover = make_prover(super::engine_, latest_prop,
                                               abs_ts_, s, super::options_);
       if (super::engine_ == IC3IA_ENGINE) {

diff --git a/engines/msat_ic3ia.cpp b/engines/msat_ic3ia.cpp
@@ -47,7 +47,7 @@ ProverResult MsatIC3IA::prove()
 
   // move everything over to a fresh solver
   shared_ptr<MsatSolver> msat_solver = static_pointer_cast<MsatSolver>(
-      create_solver_for(MSAT, MSAT_IC3IA, false));
+      create_solver_for(MSAT, MSAT_IC3IA));
   msat_env env = msat_solver->get_msat_env();
   ::ic3ia::TransitionSystem ic3ia_ts(env);
 

diff --git a/pono.cpp b/pono.cpp
@@ -245,7 +245,6 @@ 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.printing_smt_solver_);
 

diff --git a/smt/available_solvers.cpp b/smt/available_solvers.cpp
@@ -129,7 +129,7 @@ SmtSolver create_solver(SolverEnum se,
 }
 
 SmtSolver create_solver_for(
-    SolverEnum se, Engine e, bool logging, bool full_model, bool printing)
+    SolverEnum se, Engine e, bool full_model, bool printing)
 {
   SmtSolver s;
   bool ic3_engine = ic3_variants().find(e) != ic3_variants().end();
@@ -140,7 +140,7 @@ SmtSolver create_solver_for(
 
   if (se != MSAT) {
     // no special options yet for solvers other than mathsat
-    s = create_solver(se, logging, true, true, printing);
+    s = create_solver(se, false, true, true, printing);
   }
 #ifdef WITH_MSAT
   else if (se == MSAT && ic3_engine) {
@@ -161,14 +161,11 @@ SmtSolver create_solver_for(
     msat_config cfg = get_msat_config_for_ic3(false, opts);
     msat_env env = msat_create_env(cfg);
     s = std::make_shared<MsatSolver>(cfg, env);
-    if (logging) {
-      s = make_shared<LoggingSolver>(s);
-    }
     return s;
   }
 #endif
   else {
-    s = create_solver(se, logging);
+    s = create_solver(se);
   }
 
   assert(s);

diff --git a/smt/available_solvers.h b/smt/available_solvers.h
@@ -48,7 +48,6 @@ smt::SmtSolver create_solver(smt::SolverEnum se,
 // CegProphecyArrays uses it's own solver
 smt::SmtSolver create_solver_for(smt::SolverEnum se,
                                  Engine e,
-                                 bool logging,
                                  bool full_model = false,
                                  bool printing = false);
 

diff --git a/tests/test_ic3.cpp b/tests/test_ic3.cpp
@@ -20,7 +20,7 @@ class IC3UnitTests : public ::testing::Test,
  protected:
   void SetUp() override
   {
-    s = create_solver_for(GetParam(), IC3_BOOL, false);
+    s = create_solver_for(GetParam(), IC3_BOOL);
     boolsort = s->make_sort(BOOL);
     bvsort8 = s->make_sort(BV, 8);
   }

diff --git a/tests/test_ic3bits.cpp b/tests/test_ic3bits.cpp
@@ -20,7 +20,7 @@ class IC3BitsUnitTests : public ::testing::Test,
  protected:
   void SetUp() override
   {
-    s = create_solver_for(GetParam(), IC3_BITS, false);
+    s = create_solver_for(GetParam(), IC3_BITS);
     boolsort = s->make_sort(BOOL);
     bvsort8 = s->make_sort(BV, 8);
   }

diff --git a/tests/test_ic3ia.cpp b/tests/test_ic3ia.cpp
@@ -23,7 +23,7 @@ class IC3IAUnitTests : public ::testing::Test,
  protected:
   void SetUp() override
   {
-    s = create_solver_for(GetParam(), IC3IA_ENGINE, false);
+    s = create_solver_for(GetParam(), IC3IA_ENGINE);
     boolsort = s->make_sort(BOOL);
     bvsort8 = s->make_sort(BV, 8);
     intsort = s->make_sort(INT);

diff --git a/tests/test_pseudo_init_and_prop.cpp b/tests/test_pseudo_init_and_prop.cpp
@@ -17,7 +17,7 @@ class PseudoInitPropUnitTests : public ::testing::Test,
  protected:
   void SetUp() override
   {
-    s = create_solver(GetParam(), false);
+    s = create_solver(GetParam());
     bvsort8 = s->make_sort(BV, 8);
   }
   SmtSolver s;