final renaming

kondylidou · Jan 31, 2025 · 824b5fb · 824b5fb
1 parent 4a8ce59
commit 824b5fb
Show file tree

Hide file tree

Showing 6 changed files with 19 additions and 19 deletions.
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -901,8 +901,8 @@ libcvc5_add_sources(
   theory/quantifiers/lazy_trie.h
   theory/quantifiers/master_eq_notify.cpp
   theory/quantifiers/master_eq_notify.h
-  theory/quantifiers/mbqi_fast_sygus.cpp
-  theory/quantifiers/mbqi_fast_sygus.h
+  theory/quantifiers/mbqi_enum.cpp
+  theory/quantifiers/mbqi_enum.h
   theory/quantifiers/oracle_checker.cpp
   theory/quantifiers/oracle_checker.h
   theory/quantifiers/oracle_engine.cpp

diff --git a/src/theory/quantifiers/inst_strategy_mbqi.cpp b/src/theory/quantifiers/inst_strategy_mbqi.cpp
@@ -19,7 +19,7 @@
 #include "expr/skolem_manager.h"
 #include "expr/subs.h"
 #include "printer/smt2/smt2_printer.h"
-#include "theory/quantifiers/mbqi_fast_sygus.h"
+#include "theory/quantifiers/mbqi_enum.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
@@ -52,7 +52,7 @@ InstStrategyMbqi::InstStrategyMbqi(Env& env,
 
   if (options().quantifiers.mbqiEnum)
   {
-    d_msenum.reset(new MbqiFastSygus(env, *this));
+    d_msenum.reset(new mbqiEnum(env, *this));
   }
 }
 

diff --git a/src/theory/quantifiers/inst_strategy_mbqi.h b/src/theory/quantifiers/inst_strategy_mbqi.h
@@ -32,7 +32,7 @@ class SolverEngine;
 namespace theory {
 namespace quantifiers {
 
-class MbqiFastSygus;
+class mbqiEnum;
 
 /**
  * InstStrategyMbqi
@@ -47,7 +47,7 @@ class MbqiFastSygus;
  */
 class InstStrategyMbqi : public QuantifiersModule
 {
-  friend class MbqiFastSygus;
+  friend class mbqiEnum;
  public:
   InstStrategyMbqi(Env& env,
                    QuantifiersState& qs,
@@ -139,7 +139,7 @@ class InstStrategyMbqi : public QuantifiersModule
   /** Kinds that cannot appear in queries */
   std::unordered_set<Kind, kind::KindHashFunction> d_nonClosedKinds;
   /** Submodule for sygus enum */
-  std::unique_ptr<MbqiFastSygus> d_msenum;
+  std::unique_ptr<mbqiEnum> d_msenum;
   /* Set of global ground terms in assertions (outside of quantifiers). */
   context::CDHashSet<Node> d_globalSyms;
 };

diff --git a/src/theory/quantifiers/mbqi_fast_sygus.cpp → src/theory/quantifiers/mbqi_enum.cpp b/src/theory/quantifiers/mbqi_fast_sygus.cpp → src/theory/quantifiers/mbqi_enum.cpp
@@ -13,7 +13,7 @@
  * A class for augmenting model-based instantiations via fast sygus enumeration.
  */
 
-#include "theory/quantifiers/mbqi_fast_sygus.h"
+#include "theory/quantifiers/mbqi_enum.h"
 
 #include "expr/node_algorithm.h"
 #include "expr/skolem_manager.h"
@@ -184,12 +184,12 @@ bool MQuantInfo::shouldEnumerate(const TypeNode& tn)
   return true;
 }
 
-MbqiFastSygus::MbqiFastSygus(Env& env, InstStrategyMbqi& parent)
+mbqiEnum::mbqiEnum(Env& env, InstStrategyMbqi& parent)
     : EnvObj(env), d_parent(parent)
 {
 }
 
-MQuantInfo& MbqiFastSygus::getOrMkQuantInfo(const Node& q)
+MQuantInfo& mbqiEnum::getOrMkQuantInfo(const Node& q)
 {
   auto [it, inserted] = d_qinfo.try_emplace(q);
   if (inserted)
@@ -199,7 +199,7 @@ MQuantInfo& MbqiFastSygus::getOrMkQuantInfo(const Node& q)
   return it->second;
 }
 
-bool MbqiFastSygus::constructInstantiation(
+bool mbqiEnum::constructInstantiation(
     const Node& q,
     const Node& query,
     const std::vector<Node>& vars,

diff --git a/src/theory/quantifiers/mbqi_fast_sygus.h → src/theory/quantifiers/mbqi_enum.h b/src/theory/quantifiers/mbqi_fast_sygus.h → src/theory/quantifiers/mbqi_enum.h
@@ -15,8 +15,8 @@
 
 #include "cvc5_private.h"
 
-#ifndef CVC5__THEORY__QUANTIFIERS__MBQI_FAST_SYGUS_H
-#define CVC5__THEORY__QUANTIFIERS__MBQI_FAST_SYGUS_H
+#ifndef CVC5__THEORY__QUANTIFIERS__MBQI_ENUM_H
+#define CVC5__THEORY__QUANTIFIERS__MBQI_ENUM_H
 
 #include <map>
 #include <unordered_map>
@@ -108,14 +108,14 @@ class MQuantInfo
 };
 
 /**
- * MbqiFastSygus, which postprocesses an instantiation from MBQI based on
+ * mbqiEnum, which postprocesses an instantiation from MBQI based on
  * sygus enumeration.
  */
-class MbqiFastSygus : protected EnvObj
+class mbqiEnum : protected EnvObj
 {
  public:
-  MbqiFastSygus(Env& env, InstStrategyMbqi& parent);
-  ~MbqiFastSygus() {}
+  mbqiEnum(Env& env, InstStrategyMbqi& parent);
+  ~mbqiEnum() {}
 
   /**
    * Updates mvs to the desired instantiation of q. Returns true if successful.
@@ -158,4 +158,4 @@ class MbqiFastSygus : protected EnvObj
 }  // namespace theory
 }  // namespace cvc5::internal
 
-#endif /* CVC5__THEORY__QUANTIFIERS__MBQI_FAST_SYGUS_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__MBQI_ENUM_H */
diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h
@@ -29,7 +29,7 @@
 #include "theory/quantifiers/inst_strategy_mbqi.h"
 #include "theory/quantifiers/inst_strategy_pool.h"
 #include "theory/quantifiers/inst_strategy_sub_conflict.h"
-#include "theory/quantifiers/mbqi_fast_sygus.h"
+#include "theory/quantifiers/mbqi_enum.h"
 #include "theory/quantifiers/oracle_engine.h"
 #include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/quantifiers/quant_split.h"