diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-14 11:56:47 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-14 18:56:47 +0000 |
| commit | e5c26181dab76704ad9a47126585fe2ec9d6cac2 (patch) | |
| tree | 4f9d5a275091b73e825e0105be457c2b57f67d31 /src/theory/quantifiers/ematching | |
| parent | b6db4446a28d498af8fb4e629392985dfe2a976c (diff) | |
Rename public and private headers in src/include. (#6352)
Diffstat (limited to 'src/theory/quantifiers/ematching')
17 files changed, 17 insertions, 17 deletions
diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h index 69f0556dc..12c667fb5 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.h +++ b/src/theory/quantifiers/ematching/candidate_generator.h @@ -13,7 +13,7 @@ * Theory uf candidate generator. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H #define CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index ec38da7e6..64f03e7fa 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -13,7 +13,7 @@ * Higher-order trigger class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__HO_TRIGGER_H #define CVC5__THEORY__QUANTIFIERS__HO_TRIGGER_H diff --git a/src/theory/quantifiers/ematching/im_generator.h b/src/theory/quantifiers/ematching/im_generator.h index 8452a01da..12126b31b 100644 --- a/src/theory/quantifiers/ematching/im_generator.h +++ b/src/theory/quantifiers/ematching/im_generator.h @@ -13,7 +13,7 @@ * Inst match generator base class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__IM_GENERATOR_H #define CVC5__THEORY__QUANTIFIERS__IM_GENERATOR_H diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index 617ff3bec..8634890b4 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -13,7 +13,7 @@ * Inst match generator class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H #define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.h b/src/theory/quantifiers/ematching/inst_match_generator_multi.h index db319e5e6..c3549f870 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.h @@ -13,7 +13,7 @@ * multi inst match generator class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_H #define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_H diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h index a1912c24f..e15d476a3 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h @@ -13,7 +13,7 @@ * Multi-linear inst match generator class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H #define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.h b/src/theory/quantifiers/ematching/inst_match_generator_simple.h index 2113eda88..8078087c8 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.h @@ -13,7 +13,7 @@ * Simple inst match generator class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H #define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h index ea67c32ce..575134710 100644 --- a/src/theory/quantifiers/ematching/inst_strategy.h +++ b/src/theory/quantifiers/ematching/inst_strategy.h @@ -13,7 +13,7 @@ * Instantiation engine strategy base class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_H #define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_H diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index 491f77df1..fd3bb995d 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -13,7 +13,7 @@ * E-matching instantiation strategies. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__INST_STRATEGY_E_MATCHING_H #define CVC5__INST_STRATEGY_E_MATCHING_H diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h index d16b46bf9..064958ce2 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h @@ -13,7 +13,7 @@ * The user-provided E-matching instantiation strategy. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__INST_STRATEGY_E_MATCHING_USER_H #define CVC5__INST_STRATEGY_E_MATCHING_USER_H diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index bd840813d..45e137dd5 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -13,7 +13,7 @@ * Instantiation Engine classes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H #define CVC5__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.h b/src/theory/quantifiers/ematching/pattern_term_selector.h index ee43bd38a..3be8c49ea 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.h +++ b/src/theory/quantifiers/ematching/pattern_term_selector.h @@ -13,7 +13,7 @@ * Pattern term selector class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__PATTERN_TERM_SELECTOR_H #define CVC5__THEORY__QUANTIFIERS__PATTERN_TERM_SELECTOR_H diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index 13748d931..dbfae5382 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -13,7 +13,7 @@ * Trigger class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_H #define CVC5__THEORY__QUANTIFIERS__TRIGGER_H diff --git a/src/theory/quantifiers/ematching/trigger_database.h b/src/theory/quantifiers/ematching/trigger_database.h index 541428519..8dbcde7bf 100644 --- a/src/theory/quantifiers/ematching/trigger_database.h +++ b/src/theory/quantifiers/ematching/trigger_database.h @@ -13,7 +13,7 @@ * Trigger trie class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H #define CVC5__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H diff --git a/src/theory/quantifiers/ematching/trigger_term_info.h b/src/theory/quantifiers/ematching/trigger_term_info.h index 1973ad9a4..753d0850c 100644 --- a/src/theory/quantifiers/ematching/trigger_term_info.h +++ b/src/theory/quantifiers/ematching/trigger_term_info.h @@ -13,7 +13,7 @@ * Trigger term info class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H #define CVC5__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H diff --git a/src/theory/quantifiers/ematching/trigger_trie.h b/src/theory/quantifiers/ematching/trigger_trie.h index 136ae29cb..80a378d53 100644 --- a/src/theory/quantifiers/ematching/trigger_trie.h +++ b/src/theory/quantifiers/ematching/trigger_trie.h @@ -13,7 +13,7 @@ * Trigger trie class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_TRIE_H #define CVC5__THEORY__QUANTIFIERS__TRIGGER_TRIE_H diff --git a/src/theory/quantifiers/ematching/var_match_generator.h b/src/theory/quantifiers/ematching/var_match_generator.h index 9707437a8..e664ac1db 100644 --- a/src/theory/quantifiers/ematching/var_match_generator.h +++ b/src/theory/quantifiers/ematching/var_match_generator.h @@ -12,7 +12,7 @@ * Variable match generator class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H #define CVC5__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H |