From 603c0ccc4614024dfcd34333cd427ac56e229a47 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 17 Sep 2018 18:49:08 -0500 Subject: [PATCH] Move inst_strategy_cbqi to inst_strategy_cegqi (#2477) --- src/Makefile.am | 4 ++-- .../{inst_strategy_cbqi.cpp => inst_strategy_cegqi.cpp} | 4 ++-- .../cegqi/{inst_strategy_cbqi.h => inst_strategy_cegqi.h} | 6 +++--- src/theory/quantifiers/instantiate.cpp | 2 +- src/theory/quantifiers/sygus/ce_guided_single_inv.h | 2 +- src/theory/quantifiers_engine.cpp | 2 +- 6 files changed, 10 insertions(+), 10 deletions(-) rename src/theory/quantifiers/cegqi/{inst_strategy_cbqi.cpp => inst_strategy_cegqi.cpp} (99%) rename src/theory/quantifiers/cegqi/{inst_strategy_cbqi.h => inst_strategy_cegqi.h} (98%) diff --git a/src/Makefile.am b/src/Makefile.am index caad72fd5..bdba671ca 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -450,8 +450,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/cegqi/ceg_dt_instantiator.h \ theory/quantifiers/cegqi/ceg_epr_instantiator.cpp \ theory/quantifiers/cegqi/ceg_epr_instantiator.h \ - theory/quantifiers/cegqi/inst_strategy_cbqi.cpp \ - theory/quantifiers/cegqi/inst_strategy_cbqi.h \ + theory/quantifiers/cegqi/inst_strategy_cegqi.cpp \ + theory/quantifiers/cegqi/inst_strategy_cegqi.h \ theory/quantifiers/conjecture_generator.cpp \ theory/quantifiers/conjecture_generator.h \ theory/quantifiers/dynamic_rewrite.cpp \ diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp similarity index 99% rename from src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp rename to src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 8c9b39ea4..3ea3e72e4 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file inst_strategy_cbqi.cpp +/*! \file inst_strategy_cegqi.cpp ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Morgan Deters @@ -11,7 +11,7 @@ ** ** \brief Implementation of counterexample-guided quantifier instantiation strategies **/ -#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h" +#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h similarity index 98% rename from src/theory/quantifiers/cegqi/inst_strategy_cbqi.h rename to src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index c3cbf8100..0a19727b8 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file inst_strategy_cbqi.h +/*! \file inst_strategy_cegqi.h ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Mathias Preiner @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__INST_STRATEGY_CBQI_H -#define __CVC4__INST_STRATEGY_CBQI_H +#ifndef __CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H +#define __CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H #include "theory/decision_manager.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 13597c338..96a28cde6 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -17,7 +17,7 @@ #include "options/quantifiers_options.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h" +#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/term_database.h" diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index 09829e894..b27163549 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -20,7 +20,7 @@ #include "context/cdlist.h" #include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h" #include "theory/quantifiers/inst_match_trie.h" -#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h" +#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "theory/quantifiers/single_inv_partition.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 305f3182d..516f31efc 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -22,7 +22,7 @@ #include "theory/quantifiers/alpha_equivalence.h" #include "theory/quantifiers/anti_skolem.h" #include "theory/quantifiers/bv_inverter.h" -#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h" +#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "theory/quantifiers/conjecture_generator.h" #include "theory/quantifiers/ematching/inst_strategy_e_matching.h" #include "theory/quantifiers/ematching/instantiation_engine.h" -- 2.30.2