base -> core

Z3Prover · Nov 30, 2021 · b5efb87 · b5efb87
1 parent 959f4c9
commit b5efb87
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 6 deletions.
diff --git a/src/solver/solver.h b/src/solver/solver.h
@@ -48,7 +48,7 @@ solver* mk_smt2_solver(ast_manager& m, params_ref const& p);
      - statistics
      - results based on check_sat_result API
 */
-class solver : public check_sat_result, public user_propagator::base{
+class solver : public check_sat_result, public user_propagator::core {
     params_ref  m_params;
     symbol      m_cancel_backup_file;
 public:

diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h
@@ -20,11 +20,11 @@ Module Name:
 --*/
 #pragma once
 
-#include "tactic/goal.h"
 #include "util/params.h"
+#include "util/lbool.h"
 #include "util/statistics.h"
+#include "tactic/goal.h"
 #include "tactic/tactic_exception.h"
-#include "util/lbool.h"
 
 class progress_callback;
 

diff --git a/src/tactic/user_propagator_base.h b/src/tactic/user_propagator_base.h
@@ -24,7 +24,7 @@ namespace user_propagator {
     typedef std::function<void(void*,unsigned)>        pop_eh_t;
 
 
-    class base {
+    class core {
     public:
 
         virtual void user_propagate_init(
@@ -33,8 +33,7 @@ namespace user_propagator {
             pop_eh_t&                                    pop_eh,
             fresh_eh_t&                                  fresh_eh) {
             throw default_exception("user-propagators are only supported on the SMT solver");
-        }
-
+        }        
 
         virtual void user_propagate_register_fixed(fixed_eh_t& fixed_eh) {
             throw default_exception("user-propagators are only supported on the SMT solver");