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/arith | |
parent | b6db4446a28d498af8fb4e629392985dfe2a976c (diff) |
Rename public and private headers in src/include. (#6352)
Diffstat (limited to 'src/theory/arith')
54 files changed, 55 insertions, 54 deletions
diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h index 7ed76ff05..f7266c578 100644 --- a/src/theory/arith/approx_simplex.h +++ b/src/theory/arith/approx_simplex.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once #include <vector> diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h index 28385f8ac..4d181b39f 100644 --- a/src/theory/arith/arith_ite_utils.h +++ b/src/theory/arith/arith_ite_utils.h @@ -18,7 +18,7 @@ // Pass 1: label the ite as (constant) or (+ constant variable) -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__ARITH_ITE_UTILS_H #define CVC5__THEORY__ARITH__ARITH_ITE_UTILS_H diff --git a/src/theory/arith/arith_msum.h b/src/theory/arith/arith_msum.h index bc5cb15dd..3c205c9b7 100644 --- a/src/theory/arith/arith_msum.h +++ b/src/theory/arith/arith_msum.h @@ -13,7 +13,7 @@ * Arithmetic utilities regarding monomial sums. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__MSUM_H #define CVC5__THEORY__ARITH__MSUM_H diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h index cea7d0695..ea24e5066 100644 --- a/src/theory/arith/arith_preprocess.h +++ b/src/theory/arith/arith_preprocess.h @@ -13,7 +13,7 @@ * Arithmetic preprocess. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__ARITH_PREPROCESS_H #define CVC5__THEORY__ARITH__ARITH_PREPROCESS_H diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index d7686658c..e476fbd62 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -16,7 +16,7 @@ * See theory/arith/normal_form.h for more information. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__ARITH_REWRITER_H #define CVC5__THEORY__ARITH__ARITH_REWRITER_H diff --git a/src/theory/arith/arith_state.h b/src/theory/arith/arith_state.h index 688665b65..0aa848f46 100644 --- a/src/theory/arith/arith_state.h +++ b/src/theory/arith/arith_state.h @@ -13,7 +13,7 @@ * Arithmetic theory state. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__ARITH_STATE_H #define CVC5__THEORY__ARITH__ARITH_STATE_H diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index 6e01d4a86..053730ec8 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__ARITH_STATIC_LEARNER_H #define CVC5__THEORY__ARITH__ARITH_STATIC_LEARNER_H diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index c2b98599d..0c6378bc2 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -13,7 +13,7 @@ * Common functions for dealing with nodes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__ARITH_UTILITIES_H #define CVC5__THEORY__ARITH__ARITH_UTILITIES_H diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h index 0272ade52..b95c39e9e 100644 --- a/src/theory/arith/arithvar.h +++ b/src/theory/arith/arithvar.h @@ -18,7 +18,7 @@ * This file also provides utilities for ArithVars. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h index fffc48c2b..c8b7f62a4 100644 --- a/src/theory/arith/arithvar_node_map.h +++ b/src/theory/arith/arithvar_node_map.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__ARITHVAR_NODE_MAP_H #define CVC5__THEORY__ARITH__ARITHVAR_NODE_MAP_H diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h index 311a70567..25676a8b6 100644 --- a/src/theory/arith/attempt_solution_simplex.h +++ b/src/theory/arith/attempt_solution_simplex.h @@ -51,7 +51,7 @@ * These are theory valid and are currently turned into lemmas */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h index 545c1c064..9a707df85 100644 --- a/src/theory/arith/bound_counts.h +++ b/src/theory/arith/bound_counts.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once #include "base/check.h" diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index b88f48e0c..c8abba880 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 856cf719a..bd27c6034 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -74,7 +74,7 @@ * proof. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__CONSTRAINT_H #define CVC5__THEORY__ARITH__CONSTRAINT_H diff --git a/src/theory/arith/constraint_forward.h b/src/theory/arith/constraint_forward.h index f6ceea311..5f0e124fb 100644 --- a/src/theory/arith/constraint_forward.h +++ b/src/theory/arith/constraint_forward.h @@ -22,9 +22,10 @@ #ifndef CVC5__THEORY__ARITH__CONSTRAINT_FORWARD_H #define CVC5__THEORY__ARITH__CONSTRAINT_FORWARD_H -#include "cvc4_private.h" #include <vector> +#include "cvc5_private.h" + namespace cvc5 { namespace theory { namespace arith { diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h index 86a3a165b..5929bbd5a 100644 --- a/src/theory/arith/cut_log.h +++ b/src/theory/arith/cut_log.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index fce3aebc8..7872ca01e 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index 4f3a5e604..5e020d66e 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -13,7 +13,7 @@ * A Diophantine equation solver for the theory of arithmetic. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__DIO_SOLVER_H #define CVC5__THEORY__ARITH__DIO_SOLVER_H diff --git a/src/theory/arith/dual_simplex.h b/src/theory/arith/dual_simplex.h index da0a11be8..7113bd329 100644 --- a/src/theory/arith/dual_simplex.h +++ b/src/theory/arith/dual_simplex.h @@ -51,7 +51,7 @@ * These are theory valid and are currently turned into lemmas */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h index 809ca6aaa..21cc557b6 100644 --- a/src/theory/arith/error_set.h +++ b/src/theory/arith/error_set.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h index 5217e988b..6c391393d 100644 --- a/src/theory/arith/fc_simplex.h +++ b/src/theory/arith/fc_simplex.h @@ -51,7 +51,7 @@ * These are theory valid and are currently turned into lemmas */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/arith/infer_bounds.h b/src/theory/arith/infer_bounds.h index 4b17b253d..8a65c7c66 100644 --- a/src/theory/arith/infer_bounds.h +++ b/src/theory/arith/infer_bounds.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h index 079f19fc2..287b89851 100644 --- a/src/theory/arith/inference_manager.h +++ b/src/theory/arith/inference_manager.h @@ -13,7 +13,7 @@ * Customized inference manager for the theory of nonlinear arithmetic. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__INFERENCE_MANAGER_H #define CVC5__THEORY__ARITH__INFERENCE_MANAGER_H diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index 0f47bc741..e07ed6051 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -26,7 +26,7 @@ * using both the Tableau and PartialModel. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h index 4962b865d..7713dd2c3 100644 --- a/src/theory/arith/matrix.h +++ b/src/theory/arith/matrix.h @@ -15,7 +15,7 @@ * This defines Matrix<T>, IntegerEqualityTables and Tableau. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h index eafe979a1..7973fda58 100644 --- a/src/theory/arith/nl/cad/cdcac.h +++ b/src/theory/arith/nl/cad/cdcac.h @@ -14,7 +14,7 @@ * https://arxiv.org/pdf/2003.05633.pdf. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__NL__CAD__CDCAC_H #define CVC5__THEORY__ARITH__NL__CAD__CDCAC_H diff --git a/src/theory/arith/nl/cad/cdcac_utils.h b/src/theory/arith/nl/cad/cdcac_utils.h index f0f3c357b..8fde21fde 100644 --- a/src/theory/arith/nl/cad/cdcac_utils.h +++ b/src/theory/arith/nl/cad/cdcac_utils.h @@ -13,7 +13,7 @@ * Implements utilities for cdcac. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H #define CVC5__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H diff --git a/src/theory/arith/nl/cad/constraints.h b/src/theory/arith/nl/cad/constraints.h index 3655ef5c0..f8a12065f 100644 --- a/src/theory/arith/nl/cad/constraints.h +++ b/src/theory/arith/nl/cad/constraints.h @@ -13,7 +13,7 @@ * Implements a container for CAD constraints. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__NL__CAD__CONSTRAINTS_H #define CVC5__THEORY__ARITH__NL__CAD__CONSTRAINTS_H diff --git a/src/theory/arith/nl/cad/projections.h b/src/theory/arith/nl/cad/projections.h index 25deb0d0d..129c3515a 100644 --- a/src/theory/arith/nl/cad/projections.h +++ b/src/theory/arith/nl/cad/projections.h @@ -13,7 +13,7 @@ * Implements utilities for CAD projection operators. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__NL__CAD_PROJECTIONS_H #define CVC5__THEORY__ARITH__NL__CAD_PROJECTIONS_H diff --git a/src/theory/arith/nl/cad/proof_checker.h b/src/theory/arith/nl/cad/proof_checker.h index 36d18c854..d7ce05b60 100644 --- a/src/theory/arith/nl/cad/proof_checker.h +++ b/src/theory/arith/nl/cad/proof_checker.h @@ -13,7 +13,7 @@ * CAD proof checker utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__NL__CAD__PROOF_CHECKER_H #define CVC5__THEORY__ARITH__NL__CAD__PROOF_CHECKER_H diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h index 440f25e49..27a711f75 100644 --- a/src/theory/arith/nl/cad/proof_generator.h +++ b/src/theory/arith/nl/cad/proof_generator.h @@ -13,7 +13,7 @@ * Implements the proof generator for CAD. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H #define CVC5__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H diff --git a/src/theory/arith/nl/cad/variable_ordering.h b/src/theory/arith/nl/cad/variable_ordering.h index 00fbc8f49..2de262089 100644 --- a/src/theory/arith/nl/cad/variable_ordering.h +++ b/src/theory/arith/nl/cad/variable_ordering.h @@ -13,7 +13,7 @@ * Implements variable orderings tailored to CAD. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H #define CVC5__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H diff --git a/src/theory/arith/nl/ext/proof_checker.h b/src/theory/arith/nl/ext/proof_checker.h index 21807a79d..400126510 100644 --- a/src/theory/arith/nl/ext/proof_checker.h +++ b/src/theory/arith/nl/ext/proof_checker.h @@ -13,7 +13,7 @@ * NlExt proof checker utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__NL__EXT__PROOF_CHECKER_H #define CVC5__THEORY__ARITH__NL__EXT__PROOF_CHECKER_H diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp index af0f5e169..cc35a4675 100644 --- a/src/theory/arith/nl/iand_utils.cpp +++ b/src/theory/arith/nl/iand_utils.cpp @@ -17,7 +17,7 @@ #include <cmath> -#include "cvc4_private.h" +#include "cvc5_private.h" #include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" diff --git a/src/theory/arith/nl/icp/candidate.h b/src/theory/arith/nl/icp/candidate.h index 932698d71..ee8017cb7 100644 --- a/src/theory/arith/nl/icp/candidate.h +++ b/src/theory/arith/nl/icp/candidate.h @@ -16,7 +16,7 @@ #ifndef CVC5__THEORY__ARITH__ICP__CANDIDATE_H #define CVC5__THEORY__ARITH__ICP__CANDIDATE_H -#include "cvc4_private.h" +#include "cvc5_private.h" #ifdef CVC5_POLY_IMP #include <poly/polyxx.h> diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h index e7eb83bd4..c1b4b6dde 100644 --- a/src/theory/arith/nl/icp/icp_solver.h +++ b/src/theory/arith/nl/icp/icp_solver.h @@ -16,7 +16,7 @@ #ifndef CVC5__THEORY__ARITH__ICP__ICP_SOLVER_H #define CVC5__THEORY__ARITH__ICP__ICP_SOLVER_H -#include "cvc4_private.h" +#include "cvc5_private.h" #ifdef CVC5_POLY_IMP #include <poly/polyxx.h> diff --git a/src/theory/arith/nl/icp/intersection.h b/src/theory/arith/nl/icp/intersection.h index 1911a397f..d7242054c 100644 --- a/src/theory/arith/nl/icp/intersection.h +++ b/src/theory/arith/nl/icp/intersection.h @@ -16,7 +16,7 @@ #ifndef CVC5__THEORY__ARITH__ICP__INTERSECTION_H #define CVC5__THEORY__ARITH__ICP__INTERSECTION_H -#include "cvc4_private.h" +#include "cvc5_private.h" #ifdef CVC5_POLY_IMP diff --git a/src/theory/arith/nl/icp/interval.h b/src/theory/arith/nl/icp/interval.h index 4b47ae954..521a1f8ab 100644 --- a/src/theory/arith/nl/icp/interval.h +++ b/src/theory/arith/nl/icp/interval.h @@ -16,7 +16,7 @@ #ifndef CVC5__THEORY__ARITH__ICP__INTERVAL_H #define CVC5__THEORY__ARITH__ICP__INTERVAL_H -#include "cvc4_private.h" +#include "cvc5_private.h" #ifdef CVC5_POLY_IMP #include <poly/polyxx.h> diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h index 9e2b71ffe..3213df0ce 100644 --- a/src/theory/arith/nl/poly_conversion.h +++ b/src/theory/arith/nl/poly_conversion.h @@ -16,7 +16,7 @@ #ifndef CVC5__THEORY__ARITH__NL__POLY_CONVERSION_H #define CVC5__THEORY__ARITH__NL__POLY_CONVERSION_H -#include "cvc4_private.h" +#include "cvc5_private.h" #ifdef CVC5_POLY_IMP diff --git a/src/theory/arith/nl/stats.h b/src/theory/arith/nl/stats.h index e80a66aca..988b647a6 100644 --- a/src/theory/arith/nl/stats.h +++ b/src/theory/arith/nl/stats.h @@ -13,7 +13,7 @@ * Statistics for non-linear arithmetic. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__NL__STATS_H #define CVC5__THEORY__ARITH__NL__STATS_H diff --git a/src/theory/arith/nl/transcendental/proof_checker.h b/src/theory/arith/nl/transcendental/proof_checker.h index 1c0a00ca8..8675afe39 100644 --- a/src/theory/arith/nl/transcendental/proof_checker.h +++ b/src/theory/arith/nl/transcendental/proof_checker.h @@ -13,7 +13,7 @@ * Proof checker utility for transcendental solver. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__PROOF_CHECKER_H #define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__PROOF_CHECKER_H diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index 021562926..2f2d56962 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__NORMAL_FORM_H #define CVC5__THEORY__ARITH__NORMAL_FORM_H diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index 9b4503dd5..b88281495 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -17,7 +17,7 @@ * and information derived from these. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__PARTIAL_MODEL_H #define CVC5__THEORY__ARITH__PARTIAL_MODEL_H diff --git a/src/theory/arith/proof_checker.h b/src/theory/arith/proof_checker.h index 341660c69..402656154 100644 --- a/src/theory/arith/proof_checker.h +++ b/src/theory/arith/proof_checker.h @@ -13,7 +13,7 @@ * Arithmetic proof checker utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__PROOF_CHECKER_H #define CVC5__THEORY__ARITH__PROOF_CHECKER_H diff --git a/src/theory/arith/proof_macros.h b/src/theory/arith/proof_macros.h index 168ebfba6..c794c3b00 100644 --- a/src/theory/arith/proof_macros.h +++ b/src/theory/arith/proof_macros.h @@ -14,7 +14,7 @@ * or unsat cores are enabled. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__PROOF_MACROS_H #define CVC5__THEORY__ARITH__PROOF_MACROS_H diff --git a/src/theory/arith/rewrites.h b/src/theory/arith/rewrites.h index a3a62097d..24b6abdd5 100644 --- a/src/theory/arith/rewrites.h +++ b/src/theory/arith/rewrites.h @@ -13,7 +13,7 @@ * Type for rewrites for arithmetic. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__REWRITES_H #define CVC5__THEORY__ARITH__REWRITES_H diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 4cd9562e3..9cbb5bac2 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -51,7 +51,7 @@ * These are theory valid and are currently turned into lemmas */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/arith/simplex_update.h b/src/theory/arith/simplex_update.h index 8431db16b..6216f53f6 100644 --- a/src/theory/arith/simplex_update.h +++ b/src/theory/arith/simplex_update.h @@ -25,7 +25,7 @@ * using both the Tableau and PartialModel. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h index f6d97523d..7b2656752 100644 --- a/src/theory/arith/soi_simplex.h +++ b/src/theory/arith/soi_simplex.h @@ -51,7 +51,7 @@ * These are theory valid and are currently turned into lemmas */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 4c34016b8..edec26260 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/arith/tableau_sizes.h b/src/theory/arith/tableau_sizes.h index 755a7b0ca..f23966c3c 100644 --- a/src/theory/arith/tableau_sizes.h +++ b/src/theory/arith/tableau_sizes.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index b65159f50..26a33e247 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -13,7 +13,7 @@ * Arithmetic theory. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 1f5f565e2..2d56a26c7 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -15,7 +15,7 @@ * [[ Add file-specific comments here ]] */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H #define CVC5__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h index 8abb23312..2b5582956 100644 --- a/src/theory/arith/type_enumerator.h +++ b/src/theory/arith/type_enumerator.h @@ -13,7 +13,7 @@ * Enumerators for rationals and integers. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARITH__TYPE_ENUMERATOR_H #define CVC5__THEORY__ARITH__TYPE_ENUMERATOR_H |