From e5c26181dab76704ad9a47126585fe2ec9d6cac2 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 14 Apr 2021 11:56:47 -0700 Subject: Rename public and private headers in src/include. (#6352) --- src/theory/uf/cardinality_extension.h | 2 +- src/theory/uf/eq_proof.h | 2 +- src/theory/uf/equality_engine.h | 2 +- src/theory/uf/equality_engine_iterator.h | 2 +- src/theory/uf/equality_engine_notify.h | 2 +- src/theory/uf/equality_engine_types.h | 2 +- src/theory/uf/ho_extension.h | 2 +- src/theory/uf/proof_checker.h | 2 +- src/theory/uf/proof_equality_engine.h | 2 +- src/theory/uf/symmetry_breaker.h | 2 +- src/theory/uf/theory_uf.h | 2 +- src/theory/uf/theory_uf_model.h | 2 +- src/theory/uf/theory_uf_rewriter.h | 2 +- src/theory/uf/theory_uf_type_rules.h | 2 +- 14 files changed, 14 insertions(+), 14 deletions(-) (limited to 'src/theory/uf') diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h index d071264f2..53c850897 100644 --- a/src/theory/uf/cardinality_extension.h +++ b/src/theory/uf/cardinality_extension.h @@ -13,7 +13,7 @@ * Theory of UF with cardinality. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY_UF_STRONG_SOLVER_H #define CVC5__THEORY_UF_STRONG_SOLVER_H diff --git a/src/theory/uf/eq_proof.h b/src/theory/uf/eq_proof.h index 70be8e939..c938c8d9d 100644 --- a/src/theory/uf/eq_proof.h +++ b/src/theory/uf/eq_proof.h @@ -13,7 +13,7 @@ * A proof as produced by the equality engine. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #include "expr/node.h" #include "theory/uf/equality_engine_types.h" diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 7cc2918d0..d8a8f3916 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__UF__EQUALITY_ENGINE_H #define CVC5__THEORY__UF__EQUALITY_ENGINE_H diff --git a/src/theory/uf/equality_engine_iterator.h b/src/theory/uf/equality_engine_iterator.h index a5e521ee4..6a4b281df 100644 --- a/src/theory/uf/equality_engine_iterator.h +++ b/src/theory/uf/equality_engine_iterator.h @@ -13,7 +13,7 @@ * Iterator class for equality engine. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__UF__EQUALITY_ENGINE_ITERATOR_H #define CVC5__THEORY__UF__EQUALITY_ENGINE_ITERATOR_H diff --git a/src/theory/uf/equality_engine_notify.h b/src/theory/uf/equality_engine_notify.h index b634f3dcc..f5447923a 100644 --- a/src/theory/uf/equality_engine_notify.h +++ b/src/theory/uf/equality_engine_notify.h @@ -13,7 +13,7 @@ * The virtual class for notifications from the equality engine. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__UF__EQUALITY_ENGINE_NOTIFY_H #define CVC5__THEORY__UF__EQUALITY_ENGINE_NOTIFY_H diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index 8a5692bde..2f4e14887 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__UF__EQUALITY_ENGINE_TYPES_H #define CVC5__THEORY__UF__EQUALITY_ENGINE_TYPES_H diff --git a/src/theory/uf/ho_extension.h b/src/theory/uf/ho_extension.h index 715afbe52..58320d07b 100644 --- a/src/theory/uf/ho_extension.h +++ b/src/theory/uf/ho_extension.h @@ -13,7 +13,7 @@ * The higher-order extension of TheoryUF. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef __CVC5__THEORY__UF__HO_EXTENSION_H #define __CVC5__THEORY__UF__HO_EXTENSION_H diff --git a/src/theory/uf/proof_checker.h b/src/theory/uf/proof_checker.h index 4ab6b0685..55f7db3ba 100644 --- a/src/theory/uf/proof_checker.h +++ b/src/theory/uf/proof_checker.h @@ -13,7 +13,7 @@ * Equality proof checker utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__UF__PROOF_CHECKER_H #define CVC5__THEORY__UF__PROOF_CHECKER_H diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index bf96dafc8..aed662c4c 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -13,7 +13,7 @@ * The proof-producing equality engine. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__UF__PROOF_EQUALITY_ENGINE_H #define CVC5__THEORY__UF__PROOF_EQUALITY_ENGINE_H diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index f2dd9c5f1..eb78f9101 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -37,7 +37,7 @@ * */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__UF__SYMMETRY_BREAKER_H #define CVC5__THEORY__UF__SYMMETRY_BREAKER_H diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 2f037fc88..c811e08e8 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -15,7 +15,7 @@ * All implementations of TheoryUF should inherit from this class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__UF__THEORY_UF_H #define CVC5__THEORY__UF__THEORY_UF_H diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index 6e634b61e..f386c2f99 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -13,7 +13,7 @@ * Model for Theory UF. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY_UF_MODEL_H #define CVC5__THEORY_UF_MODEL_H diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index 8788bd732..4a06c0322 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__UF__THEORY_UF_REWRITER_H #define CVC5__THEORY__UF__THEORY_UF_REWRITER_H diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 473aafcc8..e6383f80e 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -15,7 +15,7 @@ * [[ Add file-specific comments here ]] */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__UF__THEORY_UF_TYPE_RULES_H #define CVC5__THEORY__UF__THEORY_UF_TYPE_RULES_H -- cgit v1.2.3