diff options
Diffstat (limited to 'src/theory')
376 files changed, 380 insertions, 379 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 diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index 71033c77b..bbb9e8c62 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -14,7 +14,7 @@ * for each term of type array. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARRAYS__ARRAY_INFO_H #define CVC5__THEORY__ARRAYS__ARRAY_INFO_H diff --git a/src/theory/arrays/inference_manager.h b/src/theory/arrays/inference_manager.h index b9809dbbb..93feb0a53 100644 --- a/src/theory/arrays/inference_manager.h +++ b/src/theory/arrays/inference_manager.h @@ -13,7 +13,7 @@ * Arrays inference manager. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARRAYS__INFERENCE_MANAGER_H #define CVC5__THEORY__ARRAYS__INFERENCE_MANAGER_H diff --git a/src/theory/arrays/proof_checker.h b/src/theory/arrays/proof_checker.h index a3970baeb..9064dbfca 100644 --- a/src/theory/arrays/proof_checker.h +++ b/src/theory/arrays/proof_checker.h @@ -13,7 +13,7 @@ * Array proof checker utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARRAYS__PROOF_CHECKER_H #define CVC5__THEORY__ARRAYS__PROOF_CHECKER_H diff --git a/src/theory/arrays/skolem_cache.h b/src/theory/arrays/skolem_cache.h index d4b774479..12578c01f 100644 --- a/src/theory/arrays/skolem_cache.h +++ b/src/theory/arrays/skolem_cache.h @@ -13,7 +13,7 @@ * Arrays skolem cache. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARRAYS__SKOLEM_CACHE_H #define CVC5__THEORY__ARRAYS__SKOLEM_CACHE_H diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index af71f20f9..188573152 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -13,7 +13,7 @@ * Theory of arrays. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARRAYS__THEORY_ARRAYS_H #define CVC5__THEORY__ARRAYS__THEORY_ARRAYS_H diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 3a0be799c..0bbfc0846 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H #define CVC5__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index 529cd2fb2..9a69ff8f4 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -13,7 +13,7 @@ * Typing and cardinality rules for the theory of arrays. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H #define CVC5__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h index 16b90730b..181a42da4 100644 --- a/src/theory/arrays/type_enumerator.h +++ b/src/theory/arrays/type_enumerator.h @@ -13,7 +13,7 @@ * An enumerator for arrays. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H #define CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H diff --git a/src/theory/arrays/union_find.h b/src/theory/arrays/union_find.h index b592eb307..c1a09491f 100644 --- a/src/theory/arrays/union_find.h +++ b/src/theory/arrays/union_find.h @@ -14,7 +14,7 @@ * stack. Refactored from the UF union-find. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARRAYS__UNION_FIND_H #define CVC5__THEORY__ARRAYS__UNION_FIND_H diff --git a/src/theory/assertion.h b/src/theory/assertion.h index fe807c020..f7d9b5be0 100644 --- a/src/theory/assertion.h +++ b/src/theory/assertion.h @@ -13,7 +13,7 @@ * The representation of the assertions sent to theories. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ASSERTION_H #define CVC5__THEORY__ASSERTION_H diff --git a/src/theory/atom_requests.h b/src/theory/atom_requests.h index cfdbba860..0d2bf0bb4 100644 --- a/src/theory/atom_requests.h +++ b/src/theory/atom_requests.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/bags/bag_solver.h b/src/theory/bags/bag_solver.h index 4c15b0243..5fb49fab7 100644 --- a/src/theory/bags/bag_solver.h +++ b/src/theory/bags/bag_solver.h @@ -13,7 +13,7 @@ * Solver for the theory of bags. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BAG__SOLVER_H #define CVC5__THEORY__BAG__SOLVER_H diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h index 2cdcffec1..10fa65aa5 100644 --- a/src/theory/bags/bags_rewriter.h +++ b/src/theory/bags/bags_rewriter.h @@ -13,7 +13,7 @@ * Bags theory rewriter. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BAGS__THEORY_BAGS_REWRITER_H #define CVC5__THEORY__BAGS__THEORY_BAGS_REWRITER_H diff --git a/src/theory/bags/bags_statistics.h b/src/theory/bags/bags_statistics.h index be95cf7ca..c0bca3444 100644 --- a/src/theory/bags/bags_statistics.h +++ b/src/theory/bags/bags_statistics.h @@ -13,7 +13,7 @@ * Statistics for the theory of bags. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BAGS_STATISTICS_H #define CVC5__THEORY__BAGS_STATISTICS_H diff --git a/src/theory/bags/infer_info.h b/src/theory/bags/infer_info.h index a55755e68..b0519993b 100644 --- a/src/theory/bags/infer_info.h +++ b/src/theory/bags/infer_info.h @@ -13,7 +13,7 @@ * Inference information utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BAGS__INFER_INFO_H #define CVC5__THEORY__BAGS__INFER_INFO_H diff --git a/src/theory/bags/inference_generator.h b/src/theory/bags/inference_generator.h index 32a49e611..252b9641e 100644 --- a/src/theory/bags/inference_generator.h +++ b/src/theory/bags/inference_generator.h @@ -13,7 +13,7 @@ * Inference generator utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BAGS__INFERENCE_GENERATOR_H #define CVC5__THEORY__BAGS__INFERENCE_GENERATOR_H diff --git a/src/theory/bags/inference_manager.h b/src/theory/bags/inference_manager.h index fff6c7690..a74515d37 100644 --- a/src/theory/bags/inference_manager.h +++ b/src/theory/bags/inference_manager.h @@ -13,7 +13,7 @@ * The inference manager for the theory of bags. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BAGS__INFERENCE_MANAGER_H #define CVC5__THEORY__BAGS__INFERENCE_MANAGER_H diff --git a/src/theory/bags/make_bag_op.h b/src/theory/bags/make_bag_op.h index aa602d364..4756009ae 100644 --- a/src/theory/bags/make_bag_op.h +++ b/src/theory/bags/make_bag_op.h @@ -13,7 +13,7 @@ * A class for MK_BAG operator. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__MAKE_BAG_OP_H #define CVC5__MAKE_BAG_OP_H diff --git a/src/theory/bags/normal_form.h b/src/theory/bags/normal_form.h index 362dedb34..124ecdf5f 100644 --- a/src/theory/bags/normal_form.h +++ b/src/theory/bags/normal_form.h @@ -15,7 +15,7 @@ #include <expr/node.h> -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BAGS__NORMAL_FORM_H #define CVC5__THEORY__BAGS__NORMAL_FORM_H diff --git a/src/theory/bags/rewrites.h b/src/theory/bags/rewrites.h index cde671f1c..f5977332a 100644 --- a/src/theory/bags/rewrites.h +++ b/src/theory/bags/rewrites.h @@ -13,7 +13,7 @@ * Type for rewrites for bags. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BAGS__REWRITES_H #define CVC5__THEORY__BAGS__REWRITES_H diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h index 8560388d0..9c2222e95 100644 --- a/src/theory/bags/solver_state.h +++ b/src/theory/bags/solver_state.h @@ -13,7 +13,7 @@ * Bags state object. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BAGS__THEORY_SOLVER_STATE_H #define CVC5__THEORY__BAGS__THEORY_SOLVER_STATE_H diff --git a/src/theory/bags/term_registry.h b/src/theory/bags/term_registry.h index 6e3a5fadb..6255f3b00 100644 --- a/src/theory/bags/term_registry.h +++ b/src/theory/bags/term_registry.h @@ -13,7 +13,7 @@ * Bags state object. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BAGS__TERM_REGISTRY_H #define CVC5__THEORY__BAGS__TERM_REGISTRY_H diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h index 482181ad2..7b9299f54 100644 --- a/src/theory/bags/theory_bags.h +++ b/src/theory/bags/theory_bags.h @@ -13,7 +13,7 @@ * Bags theory. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BAGS__THEORY_BAGS_H #define CVC5__THEORY__BAGS__THEORY_BAGS_H diff --git a/src/theory/bags/theory_bags_type_enumerator.h b/src/theory/bags/theory_bags_type_enumerator.h index f4efb7ce2..4a5fdde74 100644 --- a/src/theory/bags/theory_bags_type_enumerator.h +++ b/src/theory/bags/theory_bags_type_enumerator.h @@ -13,7 +13,7 @@ * Type enumerator for bags */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BAGS__TYPE_ENUMERATOR_H #define CVC5__THEORY__BAGS__TYPE_ENUMERATOR_H diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h index 4e4fe0716..a633d604f 100644 --- a/src/theory/bags/theory_bags_type_rules.h +++ b/src/theory/bags/theory_bags_type_rules.h @@ -13,7 +13,7 @@ * Bags theory type rules. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H #define CVC5__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 0c02ba9bd..443be0ec7 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -13,7 +13,7 @@ * A non-clausal circuit propagator for Boolean simplification. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H #define CVC5__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H diff --git a/src/theory/booleans/proof_checker.h b/src/theory/booleans/proof_checker.h index bf503089b..47a1ce633 100644 --- a/src/theory/booleans/proof_checker.h +++ b/src/theory/booleans/proof_checker.h @@ -13,7 +13,7 @@ * Boolean proof checker utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BOOLEANS__PROOF_CHECKER_H #define CVC5__THEORY__BOOLEANS__PROOF_CHECKER_H diff --git a/src/theory/booleans/proof_circuit_propagator.h b/src/theory/booleans/proof_circuit_propagator.h index d26ce3cf8..624a17f2f 100644 --- a/src/theory/booleans/proof_circuit_propagator.h +++ b/src/theory/booleans/proof_circuit_propagator.h @@ -13,7 +13,7 @@ * Proofs for the non-clausal circuit propagator. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BOOLEANS__PROOF_CIRCUIT_PROPAGATOR_H #define CVC5__THEORY__BOOLEANS__PROOF_CIRCUIT_PROPAGATOR_H diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index 10190262a..dd574a455 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -13,7 +13,7 @@ * The theory of booleans. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BOOLEANS__THEORY_BOOL_H #define CVC5__THEORY__BOOLEANS__THEORY_BOOL_H diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h index 03b85e947..d3b12db37 100644 --- a/src/theory/booleans/theory_bool_rewriter.h +++ b/src/theory/booleans/theory_bool_rewriter.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H #define CVC5__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h index c7f9ad4ad..6c9aea0ae 100644 --- a/src/theory/booleans/theory_bool_type_rules.h +++ b/src/theory/booleans/theory_bool_type_rules.h @@ -15,7 +15,7 @@ * [[ Add file-specific comments here ]] */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY_BOOL_TYPE_RULES_H #define CVC5__THEORY_BOOL_TYPE_RULES_H diff --git a/src/theory/booleans/type_enumerator.h b/src/theory/booleans/type_enumerator.h index 088468d43..93b6b875a 100644 --- a/src/theory/booleans/type_enumerator.h +++ b/src/theory/booleans/type_enumerator.h @@ -13,7 +13,7 @@ * An enumerator for Booleans. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BOOLEANS__TYPE_ENUMERATOR_H #define CVC5__THEORY__BOOLEANS__TYPE_ENUMERATOR_H diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index 8aedda650..38eea31c5 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -13,7 +13,7 @@ * Equality proof checker utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BUILTIN__PROOF_CHECKER_H #define CVC5__THEORY__BUILTIN__PROOF_CHECKER_H diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index 01946b584..27492cb53 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -13,7 +13,7 @@ * Built-in theory. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BUILTIN__THEORY_BUILTIN_H #define CVC5__THEORY__BUILTIN__THEORY_BUILTIN_H diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h index 7f4d4ade3..7d5cde3c2 100644 --- a/src/theory/builtin/theory_builtin_rewriter.h +++ b/src/theory/builtin/theory_builtin_rewriter.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H #define CVC5__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 1c067f048..87ba12ed1 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -13,7 +13,7 @@ * Type rules for the builtin theory. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H #define CVC5__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h index 9bfea2760..980792f94 100644 --- a/src/theory/builtin/type_enumerator.h +++ b/src/theory/builtin/type_enumerator.h @@ -13,7 +13,7 @@ * Enumerator for uninterpreted sorts and functions. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BUILTIN__TYPE_ENUMERATOR_H #define CVC5__THEORY__BUILTIN__TYPE_ENUMERATOR_H diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h index 892c5d344..b099a33cd 100644 --- a/src/theory/bv/abstraction.h +++ b/src/theory/bv/abstraction.h @@ -13,7 +13,7 @@ * Bitvector theory. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BV__ABSTRACTION_H #define CVC5__THEORY__BV__ABSTRACTION_H diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp index 0a6f1e39d..8c80f9d19 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.cpp +++ b/src/theory/bv/bitblast/aig_bitblaster.cpp @@ -16,7 +16,7 @@ #include "theory/bv/bitblast/aig_bitblaster.h" #include "base/check.h" -#include "cvc4_private.h" +#include "cvc5_private.h" #include "options/bv_options.h" #include "prop/cnf_stream.h" #include "prop/sat_solver.h" diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h index 95c7bd4d9..a7dfb00e5 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.h +++ b/src/theory/bv/bitblast/aig_bitblaster.h @@ -13,7 +13,7 @@ * AIG Bitblaster based on ABC. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BV__BITBLAST__AIG_BITBLASTER_H #define CVC5__THEORY__BV__BITBLAST__AIG_BITBLASTER_H diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h index e79859d7c..bb895fff2 100644 --- a/src/theory/bv/bitblast/bitblast_strategies_template.h +++ b/src/theory/bv/bitblast/bitblast_strategies_template.h @@ -13,7 +13,7 @@ * Implementation of bitblasting functions for various operators. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H #define CVC5__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H diff --git a/src/theory/bv/bitblast/bitblast_utils.h b/src/theory/bv/bitblast/bitblast_utils.h index 81c6538c5..6b532308f 100644 --- a/src/theory/bv/bitblast/bitblast_utils.h +++ b/src/theory/bv/bitblast/bitblast_utils.h @@ -13,7 +13,7 @@ * Various utility functions for bit-blasting. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H #define CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h index 24a833fcc..2a7931aa0 100644 --- a/src/theory/bv/bitblast/bitblaster.h +++ b/src/theory/bv/bitblast/bitblaster.h @@ -13,7 +13,7 @@ * Wrapper around the SAT solver used for bitblasting. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BV__BITBLAST__BITBLASTER_H #define CVC5__THEORY__BV__BITBLAST__BITBLASTER_H diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index ed02746ed..fcd33e775 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -15,7 +15,7 @@ #include "theory/bv/bitblast/eager_bitblaster.h" -#include "cvc4_private.h" +#include "cvc5_private.h" #include "options/bv_options.h" #include "options/smt_options.h" #include "prop/cnf_stream.h" diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h index 1458b0dab..765f3051e 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.h +++ b/src/theory/bv/bitblast/eager_bitblaster.h @@ -13,7 +13,7 @@ * Bitblaster for the eager BV solver. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H #define CVC5__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index 3a2bb6432..12f584442 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -15,7 +15,7 @@ #include "theory/bv/bitblast/lazy_bitblaster.h" -#include "cvc4_private.h" +#include "cvc5_private.h" #include "options/bv_options.h" #include "prop/cnf_stream.h" #include "prop/sat_solver.h" diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h index 52230c3b5..7ca2063a3 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.h +++ b/src/theory/bv/bitblast/lazy_bitblaster.h @@ -13,7 +13,7 @@ * Bitblaster for the lazy bv solver. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H #define CVC5__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H diff --git a/src/theory/bv/bitblast/proof_bitblaster.h b/src/theory/bv/bitblast/proof_bitblaster.h index a42ebb86f..bd5232a76 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.h +++ b/src/theory/bv/bitblast/proof_bitblaster.h @@ -12,7 +12,7 @@ * * A bit-blaster wrapper around BBSimple for proof logging. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H #define CVC5__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H diff --git a/src/theory/bv/bitblast/simple_bitblaster.h b/src/theory/bv/bitblast/simple_bitblaster.h index 8ae016799..04a35bc4f 100644 --- a/src/theory/bv/bitblast/simple_bitblaster.h +++ b/src/theory/bv/bitblast/simple_bitblaster.h @@ -12,7 +12,7 @@ * * Bitblaster for simple BV solver. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H #define CVC5__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h index dd2e29818..4b6c4fc5b 100644 --- a/src/theory/bv/bv_eager_solver.h +++ b/src/theory/bv/bv_eager_solver.h @@ -13,7 +13,7 @@ * Eager bit-blasting solver. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BV__BV_EAGER_SOLVER_H #define CVC5__THEORY__BV__BV_EAGER_SOLVER_H diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index 2464bf51a..0fa96e619 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -13,7 +13,7 @@ * Algebraic solver. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BV__BV_INEQUALITY__GRAPH_H #define CVC5__THEORY__BV__BV_INEQUALITY__GRAPH_H diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h index 46859bf98..57bcca261 100644 --- a/src/theory/bv/bv_quick_check.h +++ b/src/theory/bv/bv_quick_check.h @@ -13,7 +13,7 @@ * Sandboxed SAT solver for bv quickchecks. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__BV_QUICK_CHECK_H #define CVC5__BV_QUICK_CHECK_H diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h index 5115f0485..282be6bfc 100644 --- a/src/theory/bv/bv_solver.h +++ b/src/theory/bv/bv_solver.h @@ -15,7 +15,7 @@ * Describes the interface for the internal bit-vector solver of TheoryBV. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BV__BV_SOLVER_H #define CVC5__THEORY__BV__BV_SOLVER_H diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h index 961ed9bc8..8d6b8304e 100644 --- a/src/theory/bv/bv_solver_bitblast.h +++ b/src/theory/bv/bv_solver_bitblast.h @@ -13,7 +13,7 @@ * Bit-blasting solver that supports multiple SAT back ends. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BV__BV_SOLVER_BITBLAST_H #define CVC5__THEORY__BV__BV_SOLVER_BITBLAST_H diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h index 9129b1c69..42f59eda4 100644 --- a/src/theory/bv/bv_solver_lazy.h +++ b/src/theory/bv/bv_solver_lazy.h @@ -13,7 +13,7 @@ * Lazy bit-vector solver. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BV__BV_SOLVER_LAZY_H #define CVC5__THEORY__BV__BV_SOLVER_LAZY_H diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h index 477f480b3..6994d755d 100644 --- a/src/theory/bv/bv_solver_simple.h +++ b/src/theory/bv/bv_solver_simple.h @@ -13,7 +13,7 @@ * Simple bit-blast solver that sends bit-blast lemmas directly to MiniSat. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BV__BV_SOLVER_SIMPLE_H #define CVC5__THEORY__BV__BV_SOLVER_SIMPLE_H diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 6b25bb256..8a81a5ef8 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -16,11 +16,11 @@ #ifndef CVC5__THEORY__BV__BV_SUBTHEORY_H #define CVC5__THEORY__BV__BV_SUBTHEORY_H -#include "cvc4_private.h" -#include "context/context.h" #include "context/cdqueue.h" -#include "theory/uf/equality_engine.h" +#include "context/context.h" +#include "cvc5_private.h" #include "theory/theory.h" +#include "theory/uf/equality_engine.h" namespace cvc5 { diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h index 7f77924cf..93fe9d21d 100644 --- a/src/theory/bv/bv_subtheory_algebraic.h +++ b/src/theory/bv/bv_subtheory_algebraic.h @@ -13,7 +13,7 @@ * Algebraic solver. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 749ea58b2..a3238ae61 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -13,7 +13,7 @@ * Algebraic solver. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index cca2a99e4..2400eb31b 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -13,7 +13,7 @@ * Algebraic solver. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h index 8c7badde7..b554062c0 100644 --- a/src/theory/bv/bv_subtheory_inequality.h +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -13,7 +13,7 @@ * Algebraic solver. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H #define CVC5__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H diff --git a/src/theory/bv/int_blaster.h b/src/theory/bv/int_blaster.h index 6b7118f11..7fb463721 100644 --- a/src/theory/bv/int_blaster.h +++ b/src/theory/bv/int_blaster.h @@ -13,7 +13,7 @@ * A translation utility from bit-vectors to integers. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef __CVC5__THEORY__BV__INT_BLASTER__H #define __CVC5__THEORY__BV__INT_BLASTER__H diff --git a/src/theory/bv/proof_checker.h b/src/theory/bv/proof_checker.h index 7ca68bbfe..674678ff8 100644 --- a/src/theory/bv/proof_checker.h +++ b/src/theory/bv/proof_checker.h @@ -13,7 +13,7 @@ * Bit-Vector proof checker utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BV__PROOF_CHECKER_H #define CVC5__THEORY__BV__PROOF_CHECKER_H diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index df725c65c..d90cc501a 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -13,7 +13,7 @@ * Bitvector theory. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BV__SLICER_BV_H #define CVC5__THEORY__BV__SLICER_BV_H diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 924be4a38..0546e83ac 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -13,7 +13,7 @@ * Theory of bit-vectors. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BV__THEORY_BV_H #define CVC5__THEORY__BV__THEORY_BV_H diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index e5eeec25d..412c824aa 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h index e2412d869..4320e3b81 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h +++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h index bd3d50cda..cdb0a6f81 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_core.h +++ b/src/theory/bv/theory_bv_rewrite_rules_core.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 3767b9f1f..63d618da2 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index eec878e92..023bbf55c 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 77425d430..949dbce1a 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 88c2ee6e0..dca6bc9b4 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BV__THEORY_BV_REWRITER_H #define CVC5__THEORY__BV__THEORY_BV_REWRITER_H diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 0cc549c46..3c3ae0780 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -13,10 +13,10 @@ * Bitvector theory typing rules. */ -#include "cvc4_private.h" - #include <algorithm> +#include "cvc5_private.h" + #ifndef CVC5__THEORY__BV__THEORY_BV_TYPE_RULES_H #define CVC5__THEORY__BV__THEORY_BV_TYPE_RULES_H diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 35b1e764c..4844c1a93 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -13,7 +13,7 @@ * Util functions for theory BV. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h index a53b799a5..f660fb903 100644 --- a/src/theory/bv/type_enumerator.h +++ b/src/theory/bv/type_enumerator.h @@ -13,7 +13,7 @@ * An enumerator for bitvectors. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__BV__TYPE_ENUMERATOR_H #define CVC5__THEORY__BV__TYPE_ENUMERATOR_H diff --git a/src/theory/care_graph.h b/src/theory/care_graph.h index 175190e15..626fbdfe9 100644 --- a/src/theory/care_graph.h +++ b/src/theory/care_graph.h @@ -13,7 +13,7 @@ * The care graph datastructure. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__CARE_GRAPH_H #define CVC5__THEORY__CARE_GRAPH_H diff --git a/src/theory/combination_care_graph.h b/src/theory/combination_care_graph.h index 404d4e435..437831678 100644 --- a/src/theory/combination_care_graph.h +++ b/src/theory/combination_care_graph.h @@ -13,7 +13,7 @@ * Management of a care graph based approach for theory combination. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__COMBINATION_CARE_GRAPH__H #define CVC5__THEORY__COMBINATION_CARE_GRAPH__H diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h index b8bff9db3..6430e2325 100644 --- a/src/theory/combination_engine.h +++ b/src/theory/combination_engine.h @@ -13,7 +13,7 @@ * Abstract interface for theory combination. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__COMBINATION_ENGINE__H #define CVC5__THEORY__COMBINATION_ENGINE__H diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 9b1a6b9e2..b7a62be5e 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -13,7 +13,7 @@ * Rewriter for the theory of (co)inductive datatypes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__DATATYPES__DATATYPES_REWRITER_H #define CVC5__THEORY__DATATYPES__DATATYPES_REWRITER_H diff --git a/src/theory/datatypes/infer_proof_cons.h b/src/theory/datatypes/infer_proof_cons.h index e865f10ea..9e6b6d339 100644 --- a/src/theory/datatypes/infer_proof_cons.h +++ b/src/theory/datatypes/infer_proof_cons.h @@ -13,7 +13,7 @@ * Inference to proof conversion for datatypes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__DATATYPES__INFER_PROOF_CONS_H #define CVC5__THEORY__DATATYPES__INFER_PROOF_CONS_H diff --git a/src/theory/datatypes/inference.h b/src/theory/datatypes/inference.h index 012774414..db1d2b4b0 100644 --- a/src/theory/datatypes/inference.h +++ b/src/theory/datatypes/inference.h @@ -13,7 +13,7 @@ * Datatypes inference. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__DATATYPES__INFERENCE_H #define CVC5__THEORY__DATATYPES__INFERENCE_H diff --git a/src/theory/datatypes/inference_manager.h b/src/theory/datatypes/inference_manager.h index 85af607bc..2642ae0c5 100644 --- a/src/theory/datatypes/inference_manager.h +++ b/src/theory/datatypes/inference_manager.h @@ -13,7 +13,7 @@ * Datatypes inference manager. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__DATATYPES__INFERENCE_MANAGER_H #define CVC5__THEORY__DATATYPES__INFERENCE_MANAGER_H diff --git a/src/theory/datatypes/proof_checker.h b/src/theory/datatypes/proof_checker.h index b1c527d19..76fcee411 100644 --- a/src/theory/datatypes/proof_checker.h +++ b/src/theory/datatypes/proof_checker.h @@ -13,7 +13,7 @@ * Datatypes proof checker utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__DATATYPES__PROOF_CHECKER_H #define CVC5__THEORY__DATATYPES__PROOF_CHECKER_H diff --git a/src/theory/datatypes/sygus_datatype_utils.h b/src/theory/datatypes/sygus_datatype_utils.h index 81be67a96..77aa7ac54 100644 --- a/src/theory/datatypes/sygus_datatype_utils.h +++ b/src/theory/datatypes/sygus_datatype_utils.h @@ -13,7 +13,7 @@ * Util functions for sygus datatypes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__SYGUS_DATATYPE_UTILS_H #define CVC5__THEORY__STRINGS__SYGUS_DATATYPE_UTILS_H diff --git a/src/theory/datatypes/sygus_extension.h b/src/theory/datatypes/sygus_extension.h index 291f3a32a..25f56b334 100644 --- a/src/theory/datatypes/sygus_extension.h +++ b/src/theory/datatypes/sygus_extension.h @@ -13,7 +13,7 @@ * The sygus extension of the theory of datatypes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__DATATYPES__SYGUS_EXTENSION_H #define CVC5__THEORY__DATATYPES__SYGUS_EXTENSION_H diff --git a/src/theory/datatypes/sygus_simple_sym.h b/src/theory/datatypes/sygus_simple_sym.h index 8fd3061e7..872a2805f 100644 --- a/src/theory/datatypes/sygus_simple_sym.h +++ b/src/theory/datatypes/sygus_simple_sym.h @@ -13,7 +13,7 @@ * Simple symmetry breaking for sygus. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H #define CVC5__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 5617682ef..eb55ce6b0 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -13,7 +13,7 @@ * Theory of datatypes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__DATATYPES__THEORY_DATATYPES_H #define CVC5__THEORY__DATATYPES__THEORY_DATATYPES_H diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 52540e792..815cfafda 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -13,7 +13,7 @@ * Theory of datatypes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H #define CVC5__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H diff --git a/src/theory/datatypes/theory_datatypes_utils.h b/src/theory/datatypes/theory_datatypes_utils.h index f12ce9fbb..6824e0fb0 100644 --- a/src/theory/datatypes/theory_datatypes_utils.h +++ b/src/theory/datatypes/theory_datatypes_utils.h @@ -13,7 +13,7 @@ * Util functions for theory datatypes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__THEORY_DATATYPES_UTILS_H #define CVC5__THEORY__STRINGS__THEORY_DATATYPES_UTILS_H diff --git a/src/theory/datatypes/tuple_project_op.h b/src/theory/datatypes/tuple_project_op.h index 88bfdc3d9..efa16b906 100644 --- a/src/theory/datatypes/tuple_project_op.h +++ b/src/theory/datatypes/tuple_project_op.h @@ -13,7 +13,7 @@ * A class for TupleProjectOp operator. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__PROJECT_OP_H #define CVC5__PROJECT_OP_H diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index fbee35f3d..759c50db0 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -13,7 +13,7 @@ * An enumerator for datatypes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__DATATYPES__TYPE_ENUMERATOR_H #define CVC5__THEORY__DATATYPES__TYPE_ENUMERATOR_H diff --git a/src/theory/decision_manager.h b/src/theory/decision_manager.h index 3390b09c0..d9ec39eea 100644 --- a/src/theory/decision_manager.h +++ b/src/theory/decision_manager.h @@ -14,7 +14,7 @@ * theory solvers within TheoryEngine. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__DECISION_MANAGER__H #define CVC5__THEORY__DECISION_MANAGER__H diff --git a/src/theory/decision_strategy.h b/src/theory/decision_strategy.h index b27783dd6..8b5f75108 100644 --- a/src/theory/decision_strategy.h +++ b/src/theory/decision_strategy.h @@ -14,7 +14,7 @@ * for use in the DecisionManager of TheoryEngine. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__DECISION_STRATEGY__H #define CVC5__THEORY__DECISION_STRATEGY__H diff --git a/src/theory/eager_proof_generator.h b/src/theory/eager_proof_generator.h index 5f4ffa1ec..3a9ddd9d6 100644 --- a/src/theory/eager_proof_generator.h +++ b/src/theory/eager_proof_generator.h @@ -13,7 +13,7 @@ * The eager proof generator class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__EAGER_PROOF_GENERATOR_H #define CVC5__THEORY__EAGER_PROOF_GENERATOR_H diff --git a/src/theory/ee_manager.h b/src/theory/ee_manager.h index 8becbda1c..51216a614 100644 --- a/src/theory/ee_manager.h +++ b/src/theory/ee_manager.h @@ -13,7 +13,7 @@ * Utilities for management of equality engines. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__EE_MANAGER__H #define CVC5__THEORY__EE_MANAGER__H diff --git a/src/theory/ee_manager_distributed.h b/src/theory/ee_manager_distributed.h index 96deabfca..0bf184a57 100644 --- a/src/theory/ee_manager_distributed.h +++ b/src/theory/ee_manager_distributed.h @@ -14,7 +14,7 @@ * all theories. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__EE_MANAGER_DISTRIBUTED__H #define CVC5__THEORY__EE_MANAGER_DISTRIBUTED__H diff --git a/src/theory/ee_setup_info.h b/src/theory/ee_setup_info.h index c3146f723..f6139d109 100644 --- a/src/theory/ee_setup_info.h +++ b/src/theory/ee_setup_info.h @@ -13,7 +13,7 @@ * Setup information for an equality engine. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__EE_SETUP_INFO__H #define CVC5__THEORY__EE_SETUP_INFO__H diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h index 493edd512..ff9bdfa64 100644 --- a/src/theory/engine_output_channel.h +++ b/src/theory/engine_output_channel.h @@ -13,7 +13,7 @@ * The theory engine output channel. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ENGINE_OUTPUT_CHANNEL_H #define CVC5__THEORY__ENGINE_OUTPUT_CHANNEL_H diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h index d73039a18..211b3060d 100644 --- a/src/theory/evaluator.h +++ b/src/theory/evaluator.h @@ -16,7 +16,7 @@ * quickly, without going through the rewriter. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__EVALUATOR_H #define CVC5__THEORY__EVALUATOR_H diff --git a/src/theory/ext_theory.h b/src/theory/ext_theory.h index 019ac9b39..425c6fe6c 100644 --- a/src/theory/ext_theory.h +++ b/src/theory/ext_theory.h @@ -29,7 +29,7 @@ * x = "A" ^ str.contains( str.++( x, z ), "B" ) => str.contains( z, "B" ) */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__EXT_THEORY_H #define CVC5__THEORY__EXT_THEORY_H diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index 146751e50..4225be84a 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -19,7 +19,7 @@ * !!! This header is not to be included in any other headers !!! */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__FP__FP_CONVERTER_H #define CVC5__THEORY__FP__FP_CONVERTER_H diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index feda238e1..af53a50c6 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -13,7 +13,7 @@ * Theory of floating-point arithmetic. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__FP__THEORY_FP_H #define CVC5__THEORY__FP__THEORY_FP_H diff --git a/src/theory/fp/theory_fp_rewriter.h b/src/theory/fp/theory_fp_rewriter.h index 8c634abe2..cc76d4dee 100644 --- a/src/theory/fp/theory_fp_rewriter.h +++ b/src/theory/fp/theory_fp_rewriter.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__FP__THEORY_FP_REWRITER_H #define CVC5__THEORY__FP__THEORY_FP_REWRITER_H diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h index 5c9eaf342..023d9dc17 100644 --- a/src/theory/fp/theory_fp_type_rules.h +++ b/src/theory/fp/theory_fp_type_rules.h @@ -13,7 +13,7 @@ * Type rules for the theory of floating-point arithmetic. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__FP__THEORY_FP_TYPE_RULES_H #define CVC5__THEORY__FP__THEORY_FP_TYPE_RULES_H diff --git a/src/theory/fp/type_enumerator.h b/src/theory/fp/type_enumerator.h index 0d22bc62d..c7c99adf2 100644 --- a/src/theory/fp/type_enumerator.h +++ b/src/theory/fp/type_enumerator.h @@ -13,7 +13,7 @@ * An enumerator for floating-point numbers. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__FP__TYPE_ENUMERATOR_H #define CVC5__THEORY__FP__TYPE_ENUMERATOR_H diff --git a/src/theory/incomplete_id.h b/src/theory/incomplete_id.h index 8d419be45..1e917c942 100644 --- a/src/theory/incomplete_id.h +++ b/src/theory/incomplete_id.h @@ -13,7 +13,7 @@ * Incompleteness enumeration. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__INCOMPLETE_ID_H #define CVC5__THEORY__INCOMPLETE_ID_H diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 7730a7d14..9e1c78113 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -13,7 +13,7 @@ * Inference enumeration. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__INFERENCE_ID_H #define CVC5__THEORY__INFERENCE_ID_H diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h index 7c2806495..5dd01b802 100644 --- a/src/theory/inference_manager_buffered.h +++ b/src/theory/inference_manager_buffered.h @@ -13,7 +13,7 @@ * A buffered inference manager. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__INFERENCE_MANAGER_BUFFERED_H #define CVC5__THEORY__INFERENCE_MANAGER_BUFFERED_H diff --git a/src/theory/interrupted.h b/src/theory/interrupted.h index 618d5ac38..e85917e00 100644 --- a/src/theory/interrupted.h +++ b/src/theory/interrupted.h @@ -25,7 +25,7 @@ * proper management of CVC4 components. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__INTERRUPTED_H #define CVC5__THEORY__INTERRUPTED_H diff --git a/src/theory/lazy_tree_proof_generator.h b/src/theory/lazy_tree_proof_generator.h index 509a93d80..7ab921a70 100644 --- a/src/theory/lazy_tree_proof_generator.h +++ b/src/theory/lazy_tree_proof_generator.h @@ -13,7 +13,7 @@ * The lazy tree proof generator class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__LAZY_TREE_PROOF_GENERATOR_H #define CVC5__THEORY__LAZY_TREE_PROOF_GENERATOR_H diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index c2110ded1..fa06e93a4 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -14,7 +14,7 @@ * configuration information). */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__LOGIC_INFO_H #define CVC5__LOGIC_INFO_H diff --git a/src/theory/model_manager.h b/src/theory/model_manager.h index c6dad704d..50cd6a3d2 100644 --- a/src/theory/model_manager.h +++ b/src/theory/model_manager.h @@ -13,7 +13,7 @@ * Abstract management of models for TheoryEngine. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__MODEL_MANAGER__H #define CVC5__THEORY__MODEL_MANAGER__H diff --git a/src/theory/model_manager_distributed.h b/src/theory/model_manager_distributed.h index 91a83bb00..1a79eec9a 100644 --- a/src/theory/model_manager_distributed.h +++ b/src/theory/model_manager_distributed.h @@ -13,7 +13,7 @@ * Management of a distributed approach for model generation. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__MODEL_MANAGER_DISTRIBUTED__H #define CVC5__THEORY__MODEL_MANAGER_DISTRIBUTED__H diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 615484358..8e802f875 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -13,7 +13,7 @@ * The theory output channel interface. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__OUTPUT_CHANNEL_H #define CVC5__THEORY__OUTPUT_CHANNEL_H diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h index 0b6f6bbba..886830229 100644 --- a/src/theory/quantifiers/alpha_equivalence.h +++ b/src/theory/quantifiers/alpha_equivalence.h @@ -13,7 +13,7 @@ * Alpha equivalence checking. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__ALPHA_EQUIVALENCE_H #define CVC5__ALPHA_EQUIVALENCE_H diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h index 28d894cbb..bf6c31b1b 100644 --- a/src/theory/quantifiers/bv_inverter.h +++ b/src/theory/quantifiers/bv_inverter.h @@ -13,7 +13,7 @@ * Inverse rules for bit-vector operators. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__BV_INVERTER_H #define CVC5__BV_INVERTER_H diff --git a/src/theory/quantifiers/bv_inverter_utils.h b/src/theory/quantifiers/bv_inverter_utils.h index 47ec13453..734dbd56c 100644 --- a/src/theory/quantifiers/bv_inverter_utils.h +++ b/src/theory/quantifiers/bv_inverter_utils.h @@ -13,7 +13,7 @@ * Inverse rules for bit-vector operators. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__BV_INVERTER_UTILS_H #define CVC5__BV_INVERTER_UTILS_H diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index 56b259c71..1a2add6eb 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -13,7 +13,7 @@ * candidate_rewrite_database */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H #define CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H diff --git a/src/theory/quantifiers/candidate_rewrite_filter.h b/src/theory/quantifiers/candidate_rewrite_filter.h index baf788eb0..7d2d9088c 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.h +++ b/src/theory/quantifiers/candidate_rewrite_filter.h @@ -15,7 +15,7 @@ * filtering based on congruence, variable ordering, and matching. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H #define CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h index 9a0c5489a..6d65ae16c 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h @@ -13,7 +13,7 @@ * Arithmetic instantiator. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H #define CVC5__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h index 4089be74a..a1774de1c 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h @@ -13,7 +13,7 @@ * ceg_bv_instantiator */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H #define CVC5__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h index 5b413bc5c..15b13433a 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h @@ -13,7 +13,7 @@ * Implementation of ceg_bv_instantiator. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__BV_INSTANTIATOR_UTILS_H #define CVC5__BV_INSTANTIATOR_UTILS_H diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h index d17a1737a..72746a39b 100644 --- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h @@ -13,7 +13,7 @@ * ceg_dt_instantiator */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H #define CVC5__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index 03613bac8..2264127cf 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -13,7 +13,7 @@ * Counterexample-guided quantifier instantiation. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H #define CVC5__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index bc6421279..7ab0f1b8f 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -13,7 +13,7 @@ * Counterexample-guided quantifier instantiation. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H #define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H diff --git a/src/theory/quantifiers/cegqi/nested_qe.h b/src/theory/quantifiers/cegqi/nested_qe.h index f7ffcc6c6..020d15d3a 100644 --- a/src/theory/quantifiers/cegqi/nested_qe.h +++ b/src/theory/quantifiers/cegqi/nested_qe.h @@ -14,7 +14,7 @@ * based on nested quantifier elimination. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H #define CVC5__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.h b/src/theory/quantifiers/cegqi/vts_term_cache.h index 284bc9c25..d3a6558cf 100644 --- a/src/theory/quantifiers/cegqi/vts_term_cache.h +++ b/src/theory/quantifiers/cegqi/vts_term_cache.h @@ -13,7 +13,7 @@ * Virtual term substitution term cache. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H #define CVC5__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 894a7c80f..e8b5e260a 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -13,7 +13,7 @@ * conjecture generator class */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CONJECTURE_GENERATOR_H #define CONJECTURE_GENERATOR_H diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h index d26192857..3187b7c03 100644 --- a/src/theory/quantifiers/dynamic_rewrite.h +++ b/src/theory/quantifiers/dynamic_rewrite.h @@ -13,7 +13,7 @@ * dynamic_rewriter */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H #define CVC5__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H 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 diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h index 5f3afdc3a..4809cc6c2 100644 --- a/src/theory/quantifiers/equality_query.h +++ b/src/theory/quantifiers/equality_query.h @@ -13,7 +13,7 @@ * Equality query class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS_EQUALITY_QUERY_H #define CVC5__THEORY__QUANTIFIERS_EQUALITY_QUERY_H diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index bcbb72927..36fae1549 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -13,7 +13,7 @@ * expr_miner */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__EXPRESSION_MINER_H #define CVC5__THEORY__QUANTIFIERS__EXPRESSION_MINER_H diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h index e4b28f7d6..32bc4744f 100644 --- a/src/theory/quantifiers/expr_miner_manager.h +++ b/src/theory/quantifiers/expr_miner_manager.h @@ -13,7 +13,7 @@ * Expression miner manager, which manages individual expression miners. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H #define CVC5__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h index eacb0035f..29194ff36 100644 --- a/src/theory/quantifiers/extended_rewrite.h +++ b/src/theory/quantifiers/extended_rewrite.h @@ -13,7 +13,7 @@ * extended rewriting class */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H #define CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index ee3634de5..04b1fdb63 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -13,7 +13,7 @@ * Model extended classes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__FIRST_ORDER_MODEL_H #define CVC5__FIRST_ORDER_MODEL_H diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index 2c57ccf18..8e3b9f607 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -13,7 +13,7 @@ * Bounded integers module */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__BOUNDED_INTEGERS_H #define CVC5__BOUNDED_INTEGERS_H diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.h b/src/theory/quantifiers/fmf/first_order_model_fmc.h index 5db438093..3c35fdbe8 100644 --- a/src/theory/quantifiers/fmf/first_order_model_fmc.h +++ b/src/theory/quantifiers/fmf/first_order_model_fmc.h @@ -13,7 +13,7 @@ * First order model for full model check. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__FMF__FIRST_ORDER_MODEL_FMC_H #define CVC5__THEORY__QUANTIFIERS__FMF__FIRST_ORDER_MODEL_FMC_H diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index 431ca60a7..fd50d632f 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -13,7 +13,7 @@ * Full model check class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H #define CVC5__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index fa58d512d..df866fbe1 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -13,7 +13,7 @@ * Model Builder class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__MODEL_BUILDER_H #define CVC5__THEORY__QUANTIFIERS__MODEL_BUILDER_H diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index 4e4fd1730..89150bda4 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -13,7 +13,7 @@ * Model Engine class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H #define CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H diff --git a/src/theory/quantifiers/fun_def_evaluator.h b/src/theory/quantifiers/fun_def_evaluator.h index 656da77d7..54565b4ee 100644 --- a/src/theory/quantifiers/fun_def_evaluator.h +++ b/src/theory/quantifiers/fun_def_evaluator.h @@ -13,7 +13,7 @@ * Techniques for evaluating terms with recursively defined functions. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__QUANTIFIERS_FUN_DEF_EVALUATOR_H #define CVC5__QUANTIFIERS_FUN_DEF_EVALUATOR_H diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index f758478da..27b679623 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -13,7 +13,7 @@ * Inst match class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_H #define CVC5__THEORY__QUANTIFIERS__INST_MATCH_H diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h index 2a622cb2a..83bd8d3b1 100644 --- a/src/theory/quantifiers/inst_match_trie.h +++ b/src/theory/quantifiers/inst_match_trie.h @@ -13,7 +13,7 @@ * Inst match trie class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H #define CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index 9eadf4472..a298e3a8a 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -13,7 +13,7 @@ * Enumerative instantiation. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__INST_STRATEGY_ENUMERATIVE_H #define CVC5__INST_STRATEGY_ENUMERATIVE_H diff --git a/src/theory/quantifiers/inst_strategy_pool.h b/src/theory/quantifiers/inst_strategy_pool.h index 8eceaf35a..acdc0010b 100644 --- a/src/theory/quantifiers/inst_strategy_pool.h +++ b/src/theory/quantifiers/inst_strategy_pool.h @@ -13,7 +13,7 @@ * Pool-based instantiation strategy */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H #define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index ddfba8804..f420c0f62 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -13,7 +13,7 @@ * instantiate */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INSTANTIATE_H #define CVC5__THEORY__QUANTIFIERS__INSTANTIATE_H diff --git a/src/theory/quantifiers/instantiation_list.h b/src/theory/quantifiers/instantiation_list.h index cf747e7ea..d97383ba0 100644 --- a/src/theory/quantifiers/instantiation_list.h +++ b/src/theory/quantifiers/instantiation_list.h @@ -13,7 +13,7 @@ * List of instantiations. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H #define CVC5__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H diff --git a/src/theory/quantifiers/proof_checker.h b/src/theory/quantifiers/proof_checker.h index cf918a0c0..618ac8301 100644 --- a/src/theory/quantifiers/proof_checker.h +++ b/src/theory/quantifiers/proof_checker.h @@ -13,7 +13,7 @@ * Quantifiers proof checker utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__PROOF_CHECKER_H #define CVC5__THEORY__QUANTIFIERS__PROOF_CHECKER_H diff --git a/src/theory/quantifiers/quant_bound_inference.h b/src/theory/quantifiers/quant_bound_inference.h index 024984ce6..0bcb5937a 100644 --- a/src/theory/quantifiers/quant_bound_inference.h +++ b/src/theory/quantifiers/quant_bound_inference.h @@ -13,7 +13,7 @@ * Quantifiers bound inference. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H #define CVC5__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index ca558ce40..b533a3f12 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -13,7 +13,7 @@ * Quantifiers conflict find class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef QUANT_CONFLICT_FIND #define QUANT_CONFLICT_FIND diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h index 91792150a..a3e306a4e 100644 --- a/src/theory/quantifiers/quant_module.h +++ b/src/theory/quantifiers/quant_module.h @@ -13,7 +13,7 @@ * quantifier module */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANT_MODULE_H #define CVC5__THEORY__QUANT_MODULE_H diff --git a/src/theory/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h index 4c0d6de0b..c22e560f9 100644 --- a/src/theory/quantifiers/quant_relevance.h +++ b/src/theory/quantifiers/quant_relevance.h @@ -13,7 +13,7 @@ * quantifier relevance */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANT_RELEVANCE_H #define CVC5__THEORY__QUANT_RELEVANCE_H diff --git a/src/theory/quantifiers/quant_rep_bound_ext.h b/src/theory/quantifiers/quant_rep_bound_ext.h index 032cc47b5..999d50546 100644 --- a/src/theory/quantifiers/quant_rep_bound_ext.h +++ b/src/theory/quantifiers/quant_rep_bound_ext.h @@ -13,7 +13,7 @@ * Quantifiers representative bound utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H #define CVC5__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index e37ac7a7d..06b9c59f5 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -13,7 +13,7 @@ * dynamic quantifiers splitting */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANT_SPLIT_H #define CVC5__THEORY__QUANT_SPLIT_H diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 85c891117..1e7927dc0 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -13,7 +13,7 @@ * quantifier util */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANT_UTIL_H #define CVC5__THEORY__QUANT_UTIL_H diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 0a72945c1..b3fdd09da 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -13,7 +13,7 @@ * Attributes for the theory quantifiers. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H diff --git a/src/theory/quantifiers/quantifiers_inference_manager.h b/src/theory/quantifiers/quantifiers_inference_manager.h index cd61413ee..5cb42e33c 100644 --- a/src/theory/quantifiers/quantifiers_inference_manager.h +++ b/src/theory/quantifiers/quantifiers_inference_manager.h @@ -13,7 +13,7 @@ * Utility for quantifiers inference manager. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h index dabee00f9..659be0381 100644 --- a/src/theory/quantifiers/quantifiers_modules.h +++ b/src/theory/quantifiers/quantifiers_modules.h @@ -13,7 +13,7 @@ * Class for initializing the modules of quantifiers engine. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H diff --git a/src/theory/quantifiers/quantifiers_registry.h b/src/theory/quantifiers/quantifiers_registry.h index 901bd3d51..ee99a284a 100644 --- a/src/theory/quantifiers/quantifiers_registry.h +++ b/src/theory/quantifiers/quantifiers_registry.h @@ -13,7 +13,7 @@ * The quantifiers registry. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index ecee8fab4..c2f60c7f9 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -13,7 +13,7 @@ * Rewriter for the theory of inductive quantifiers. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H diff --git a/src/theory/quantifiers/quantifiers_state.h b/src/theory/quantifiers/quantifiers_state.h index 38b4bf6c8..e4a05b078 100644 --- a/src/theory/quantifiers/quantifiers_state.h +++ b/src/theory/quantifiers/quantifiers_state.h @@ -13,7 +13,7 @@ * Utility for quantifiers state. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H diff --git a/src/theory/quantifiers/quantifiers_statistics.h b/src/theory/quantifiers/quantifiers_statistics.h index 441a96f3c..f03d27ee3 100644 --- a/src/theory/quantifiers/quantifiers_statistics.h +++ b/src/theory/quantifiers/quantifiers_statistics.h @@ -13,7 +13,7 @@ * Quantifiers statistics class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H diff --git a/src/theory/quantifiers/query_generator.h b/src/theory/quantifiers/query_generator.h index 465853212..6955245f7 100644 --- a/src/theory/quantifiers/query_generator.h +++ b/src/theory/quantifiers/query_generator.h @@ -14,7 +14,7 @@ * of generated expressions. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__QUERY_GENERATOR_H #define CVC5__THEORY__QUANTIFIERS__QUERY_GENERATOR_H diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 8dbc7c89d..5581e932f 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -13,7 +13,7 @@ * Relevant domain class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H #define CVC5__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H diff --git a/src/theory/quantifiers/single_inv_partition.h b/src/theory/quantifiers/single_inv_partition.h index 1a360f678..90b8fb3ea 100644 --- a/src/theory/quantifiers/single_inv_partition.h +++ b/src/theory/quantifiers/single_inv_partition.h @@ -13,7 +13,7 @@ * Utility for single invocation partitioning. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H #define CVC5__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index 148dff1b6..412f7a069 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -13,7 +13,7 @@ * Utilities for skolemization. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SKOLEMIZE_H #define CVC5__THEORY__QUANTIFIERS__SKOLEMIZE_H diff --git a/src/theory/quantifiers/solution_filter.h b/src/theory/quantifiers/solution_filter.h index 1af4fbb16..43545d6d9 100644 --- a/src/theory/quantifiers/solution_filter.h +++ b/src/theory/quantifiers/solution_filter.h @@ -13,7 +13,7 @@ * Utility for filtering sygus solutions. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SOLUTION_FILTER_H #define CVC5__THEORY__QUANTIFIERS__SOLUTION_FILTER_H diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index 9e51f0955..72d41592a 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -13,7 +13,7 @@ * Utility for processing single invocation synthesis conjectures. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H #define CVC5__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 6aa9808d5..db2c44ca9 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -13,7 +13,7 @@ * cegis */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CEGIS_H #define CVC5__THEORY__QUANTIFIERS__CEGIS_H diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h index b284af7e1..d8f6fb203 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.h +++ b/src/theory/quantifiers/sygus/cegis_core_connective.h @@ -13,7 +13,7 @@ * Cegis core connective module. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H #define CVC5__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index 4ec2be938..b2c3ba2be 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -12,7 +12,7 @@ * * cegis with unification techinques. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H #define CVC5__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h index 5907cebe2..3e849e9a7 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.h +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h @@ -13,7 +13,7 @@ * Class for streaming concrete values (through substitutions) from * enumerated abstract ones. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H #define CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H diff --git a/src/theory/quantifiers/sygus/example_eval_cache.h b/src/theory/quantifiers/sygus/example_eval_cache.h index 54d788e69..2bc783c0f 100644 --- a/src/theory/quantifiers/sygus/example_eval_cache.h +++ b/src/theory/quantifiers/sygus/example_eval_cache.h @@ -13,7 +13,7 @@ * This class caches the evaluation of nodes on a fixed list of examples. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__EXAMPLE_EVAL_CACHE_H #define CVC5__THEORY__QUANTIFIERS__EXAMPLE_EVAL_CACHE_H diff --git a/src/theory/quantifiers/sygus/example_infer.h b/src/theory/quantifiers/sygus/example_infer.h index 2ca206b49..921e52c3c 100644 --- a/src/theory/quantifiers/sygus/example_infer.h +++ b/src/theory/quantifiers/sygus/example_infer.h @@ -14,7 +14,7 @@ * (functions applied to concrete arguments only). */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__EXAMPLE_INFER_H #define CVC5__THEORY__QUANTIFIERS__EXAMPLE_INFER_H diff --git a/src/theory/quantifiers/sygus/example_min_eval.h b/src/theory/quantifiers/sygus/example_min_eval.h index 7168c8ae2..6ed6f151f 100644 --- a/src/theory/quantifiers/sygus/example_min_eval.h +++ b/src/theory/quantifiers/sygus/example_min_eval.h @@ -14,7 +14,7 @@ * on substitutions with a fixed domain. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H #define CVC5__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H diff --git a/src/theory/quantifiers/sygus/rcons_obligation_info.h b/src/theory/quantifiers/sygus/rcons_obligation_info.h index 80bb207a5..f1a48d561 100644 --- a/src/theory/quantifiers/sygus/rcons_obligation_info.h +++ b/src/theory/quantifiers/sygus/rcons_obligation_info.h @@ -13,7 +13,7 @@ * Utility class for Sygus Reconstruct module. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H #define CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H diff --git a/src/theory/quantifiers/sygus/rcons_type_info.h b/src/theory/quantifiers/sygus/rcons_type_info.h index 35fae4ebf..d1d38c3f3 100644 --- a/src/theory/quantifiers/sygus/rcons_type_info.h +++ b/src/theory/quantifiers/sygus/rcons_type_info.h @@ -13,7 +13,7 @@ * Utility class for Sygus Reconstruct module. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H #define CVC5__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h index 847d3d011..c7efae3bb 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator.h @@ -13,7 +13,7 @@ * sygus_enumerator */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h index 506c6619b..434118af0 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h @@ -13,7 +13,7 @@ * Basic sygus enumerator class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.h b/src/theory/quantifiers/sygus/sygus_eval_unfold.h index 630743141..c9a0b0ba5 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.h +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h @@ -13,7 +13,7 @@ * sygus_eval_unfold */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h index 66af638e0..4e2473af4 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.h +++ b/src/theory/quantifiers/sygus/sygus_explain.h @@ -13,7 +13,7 @@ * sygus explanations */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index 293053694..8745f7d61 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -14,7 +14,7 @@ * grammars that encode syntactic restrictions for SyGuS. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h index 7d9a0f0f4..f1d8e01e0 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h @@ -12,7 +12,7 @@ * * Class for simplifying SyGuS grammars after they are encoded into datatypes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.h b/src/theory/quantifiers/sygus/sygus_grammar_red.h index c6181cd2c..2146e1f73 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.h @@ -13,7 +13,7 @@ * sygus_grammar_red */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index 521603ca4..0fc610580 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -13,7 +13,7 @@ * Sygus invariance tests. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index 632a2995c..f2c3f02de 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -13,7 +13,7 @@ * sygus_module */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_MODULE_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_MODULE_H diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index 831dfc2f0..1be4e2b91 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -13,7 +13,7 @@ * Utility for processing programming by examples synthesis conjectures. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_PBE_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_PBE_H diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h index df5fd0706..3a2c6eb4d 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.h +++ b/src/theory/quantifiers/sygus/sygus_process_conj.h @@ -13,7 +13,7 @@ * Techniqures for static preprocessing and analysis of sygus conjectures. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.h b/src/theory/quantifiers/sygus/sygus_reconstruct.h index af3a24007..334b95e71 100644 --- a/src/theory/quantifiers/sygus/sygus_reconstruct.h +++ b/src/theory/quantifiers/sygus/sygus_reconstruct.h @@ -13,7 +13,7 @@ * Utility for reconstructing terms to match a grammar. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index 8e0321f7c..1a2159b10 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -13,7 +13,7 @@ * sygus_repair_const */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H diff --git a/src/theory/quantifiers/sygus/sygus_stats.h b/src/theory/quantifiers/sygus/sygus_stats.h index 429d6b272..20b0633aa 100644 --- a/src/theory/quantifiers/sygus/sygus_stats.h +++ b/src/theory/quantifiers/sygus/sygus_stats.h @@ -13,7 +13,7 @@ * A shared statistics class for sygus. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_STATS_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_STATS_H diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index 3d6a9323e..2e9e34aa6 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -13,7 +13,7 @@ * sygus_unif */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_H diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index 61e9a35c7..ef6732cd6 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -13,7 +13,7 @@ * sygus_unif_io */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index e0eedf7dc..356c908dc 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -13,7 +13,7 @@ * sygus_unif_rl */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h index cc220f578..11950b0c2 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.h +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h @@ -13,7 +13,7 @@ * sygus_unif_strat */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H diff --git a/src/theory/quantifiers/sygus/sygus_utils.h b/src/theory/quantifiers/sygus/sygus_utils.h index 962e1b385..acdd8550e 100644 --- a/src/theory/quantifiers/sygus/sygus_utils.h +++ b/src/theory/quantifiers/sygus/sygus_utils.h @@ -13,7 +13,7 @@ * Generic sygus utilities. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H #define CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 1aa0913c2..a7ecd4ead 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -14,7 +14,7 @@ * conjecture. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H #define CVC5__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index 2591f2d16..ec4ade86b 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -14,7 +14,7 @@ * in particular, those described in Reynolds et al CAV 2015. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYNTH_ENGINE_H #define CVC5__THEORY__QUANTIFIERS__SYNTH_ENGINE_H diff --git a/src/theory/quantifiers/sygus/template_infer.h b/src/theory/quantifiers/sygus/template_infer.h index 1674bf65b..f7053df46 100644 --- a/src/theory/quantifiers/sygus/template_infer.h +++ b/src/theory/quantifiers/sygus/template_infer.h @@ -13,7 +13,7 @@ * Utility for inferring templates for invariant problems. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H #define CVC5__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 09b87c9b8..c8a422a0e 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -13,7 +13,7 @@ * Term database sygus class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H #define CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H diff --git a/src/theory/quantifiers/sygus/transition_inference.h b/src/theory/quantifiers/sygus/transition_inference.h index be3842738..d6dec6f71 100644 --- a/src/theory/quantifiers/sygus/transition_inference.h +++ b/src/theory/quantifiers/sygus/transition_inference.h @@ -14,7 +14,7 @@ * transition system. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H #define CVC5__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H diff --git a/src/theory/quantifiers/sygus/type_info.h b/src/theory/quantifiers/sygus/type_info.h index 6fddf0574..7b22f826c 100644 --- a/src/theory/quantifiers/sygus/type_info.h +++ b/src/theory/quantifiers/sygus/type_info.h @@ -13,7 +13,7 @@ * Sygus type info data structure. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H #define CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H diff --git a/src/theory/quantifiers/sygus/type_node_id_trie.h b/src/theory/quantifiers/sygus/type_node_id_trie.h index 42f9088b1..01e7984c6 100644 --- a/src/theory/quantifiers/sygus/type_node_id_trie.h +++ b/src/theory/quantifiers/sygus/type_node_id_trie.h @@ -13,7 +13,7 @@ * Type node identifier trie data structure. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H #define CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h index cce3c138f..05c62d883 100644 --- a/src/theory/quantifiers/sygus_inst.h +++ b/src/theory/quantifiers/sygus_inst.h @@ -13,7 +13,7 @@ * SyGuS instantiator class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INST_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_INST_H diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index 67fcb2455..c56b1c0b1 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -13,7 +13,7 @@ * sygus_sampler */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index c6032aa73..a8551a581 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -13,7 +13,7 @@ * Term database class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H #define CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H diff --git a/src/theory/quantifiers/term_enumeration.h b/src/theory/quantifiers/term_enumeration.h index 0714754b1..50abef744 100644 --- a/src/theory/quantifiers/term_enumeration.h +++ b/src/theory/quantifiers/term_enumeration.h @@ -13,7 +13,7 @@ * Utilities for term enumeration. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__TERM_ENUMERATION_H #define CVC5__THEORY__QUANTIFIERS__TERM_ENUMERATION_H diff --git a/src/theory/quantifiers/term_pools.h b/src/theory/quantifiers/term_pools.h index 0664340a7..5a7556ad9 100644 --- a/src/theory/quantifiers/term_pools.h +++ b/src/theory/quantifiers/term_pools.h @@ -13,7 +13,7 @@ * Utilities for term enumeration. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__TERM_POOLS_H #define CVC5__THEORY__QUANTIFIERS__TERM_POOLS_H diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h index a9e80c802..5dfc3f78d 100644 --- a/src/theory/quantifiers/term_registry.h +++ b/src/theory/quantifiers/term_registry.h @@ -13,7 +13,7 @@ * Term registry class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__TERM_REGISTRY_H #define CVC5__THEORY__QUANTIFIERS__TERM_REGISTRY_H diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 20bf46c2a..fb664dab5 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -13,7 +13,7 @@ * Term utilities class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__TERM_UTIL_H #define CVC5__THEORY__QUANTIFIERS__TERM_UTIL_H diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 26fc4bc24..b5411aaba 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -13,7 +13,7 @@ * Theory of quantifiers. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H #define CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index 7d8d78260..7783c65d6 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -13,7 +13,7 @@ * Theory of quantifiers. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H #define CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index bed73d1fb..fd4889154 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -13,7 +13,7 @@ * Theory instantiator, Instantiation Engine classes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS_ENGINE_H #define CVC5__THEORY__QUANTIFIERS_ENGINE_H diff --git a/src/theory/relevance_manager.h b/src/theory/relevance_manager.h index ac0ad83b5..dc717157b 100644 --- a/src/theory/relevance_manager.h +++ b/src/theory/relevance_manager.h @@ -13,7 +13,7 @@ * Relevance manager. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__RELEVANCE_MANAGER__H #define CVC5__THEORY__RELEVANCE_MANAGER__H diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index 189267b3c..28cd6617c 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -13,7 +13,7 @@ * Representative set class and utilities. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__REP_SET_H #define CVC5__THEORY__REP_SET_H diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index 6232fb0e7..3f4676fa0 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -13,7 +13,7 @@ * The Rewriter class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/rewriter_attributes.h b/src/theory/rewriter_attributes.h index 51b51eb51..eef6eac21 100644 --- a/src/theory/rewriter_attributes.h +++ b/src/theory/rewriter_attributes.h @@ -13,7 +13,7 @@ * Rewriter attributes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h index 3cb3ac1bf..5c52e79b5 100644 --- a/src/theory/rewriter_tables_template.h +++ b/src/theory/rewriter_tables_template.h @@ -16,7 +16,7 @@ * from the Theory kinds files. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index d3b8fad40..2b90a46a3 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -13,7 +13,7 @@ * Theory of separation logic. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__SEP__THEORY_SEP_H #define CVC5__THEORY__SEP__THEORY_SEP_H diff --git a/src/theory/sep/theory_sep_rewriter.h b/src/theory/sep/theory_sep_rewriter.h index 965123c6f..6a8472555 100644 --- a/src/theory/sep/theory_sep_rewriter.h +++ b/src/theory/sep/theory_sep_rewriter.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__SEP__THEORY_SEP_REWRITER_H #define CVC5__THEORY__SEP__THEORY_SEP_REWRITER_H diff --git a/src/theory/sep/theory_sep_type_rules.h b/src/theory/sep/theory_sep_type_rules.h index 2ad1e79cf..676cb8d9d 100644 --- a/src/theory/sep/theory_sep_type_rules.h +++ b/src/theory/sep/theory_sep_type_rules.h @@ -13,7 +13,7 @@ * Typing and cardinality rules for the theory of sep. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__SEP__THEORY_SEP_TYPE_RULES_H #define CVC5__THEORY__SEP__THEORY_SEP_TYPE_RULES_H diff --git a/src/theory/sets/cardinality_extension.h b/src/theory/sets/cardinality_extension.h index 24981d4be..cd4ba5de0 100644 --- a/src/theory/sets/cardinality_extension.h +++ b/src/theory/sets/cardinality_extension.h @@ -13,7 +13,7 @@ * An extension of the theory sets for handling cardinality constraints. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__SETS__CARDINALITY_EXTENSION_H #define CVC5__THEORY__SETS__CARDINALITY_EXTENSION_H diff --git a/src/theory/sets/inference_manager.h b/src/theory/sets/inference_manager.h index 68cbfa4a7..bcb38ff5c 100644 --- a/src/theory/sets/inference_manager.h +++ b/src/theory/sets/inference_manager.h @@ -13,7 +13,7 @@ * The inference manager for the theory of sets. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__SETS__INFERENCE_MANAGER_H #define CVC5__THEORY__SETS__INFERENCE_MANAGER_H diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h index 7cbad751f..930f7da86 100644 --- a/src/theory/sets/normal_form.h +++ b/src/theory/sets/normal_form.h @@ -13,7 +13,7 @@ * Normal form for set constants. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__SETS__NORMAL_FORM_H #define CVC5__THEORY__SETS__NORMAL_FORM_H diff --git a/src/theory/sets/singleton_op.h b/src/theory/sets/singleton_op.h index 02d646290..41dd7e51e 100644 --- a/src/theory/sets/singleton_op.h +++ b/src/theory/sets/singleton_op.h @@ -13,7 +13,7 @@ * A class for singleton operator for sets. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__SINGLETON_OP_H #define CVC5__SINGLETON_OP_H diff --git a/src/theory/sets/skolem_cache.h b/src/theory/sets/skolem_cache.h index 3d1ce3628..a41886f9d 100644 --- a/src/theory/sets/skolem_cache.h +++ b/src/theory/sets/skolem_cache.h @@ -13,7 +13,7 @@ * A cache of skolems for theory of sets. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__SETS__SKOLEM_CACHE_H #define CVC5__THEORY__SETS__SKOLEM_CACHE_H diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h index db63596cc..94e06971c 100644 --- a/src/theory/sets/solver_state.h +++ b/src/theory/sets/solver_state.h @@ -13,7 +13,7 @@ * Sets state object. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__SETS__THEORY_SOLVER_STATE_H #define CVC5__THEORY__SETS__THEORY_SOLVER_STATE_H diff --git a/src/theory/sets/term_registry.h b/src/theory/sets/term_registry.h index 6b5a3d640..718559a0a 100644 --- a/src/theory/sets/term_registry.h +++ b/src/theory/sets/term_registry.h @@ -13,7 +13,7 @@ * Sets state object. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__SETS__TERM_REGISTRY_H #define CVC5__THEORY__SETS__TERM_REGISTRY_H diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index acb6b1910..bb8741e35 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -13,7 +13,7 @@ * Sets theory. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__SETS__THEORY_SETS_H #define CVC5__THEORY__SETS__THEORY_SETS_H diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 7f492bc88..9bca25ea2 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -13,7 +13,7 @@ * Sets theory implementation. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__SETS__THEORY_SETS_PRIVATE_H #define CVC5__THEORY__SETS__THEORY_SETS_PRIVATE_H diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h index e54b65d92..693731862 100644 --- a/src/theory/sets/theory_sets_rewriter.h +++ b/src/theory/sets/theory_sets_rewriter.h @@ -13,7 +13,7 @@ * Sets theory rewriter. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__SETS__THEORY_SETS_REWRITER_H #define CVC5__THEORY__SETS__THEORY_SETS_REWRITER_H diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h index 15ea9a59f..1de5fa0be 100644 --- a/src/theory/sets/theory_sets_type_enumerator.h +++ b/src/theory/sets/theory_sets_type_enumerator.h @@ -16,7 +16,7 @@ * starting with the empty set as the initial value. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__SETS__TYPE_ENUMERATOR_H #define CVC5__THEORY__SETS__TYPE_ENUMERATOR_H diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 1cac17d02..ca89728d6 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -13,7 +13,7 @@ * Sets theory type rules. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__SETS__THEORY_SETS_TYPE_RULES_H #define CVC5__THEORY__SETS__THEORY_SETS_TYPE_RULES_H diff --git a/src/theory/shared_solver.h b/src/theory/shared_solver.h index 19c7b998b..9198e5043 100644 --- a/src/theory/shared_solver.h +++ b/src/theory/shared_solver.h @@ -13,7 +13,7 @@ * Base class for shared solver. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__SHARED_SOLVER__H #define CVC5__THEORY__SHARED_SOLVER__H diff --git a/src/theory/shared_solver_distributed.h b/src/theory/shared_solver_distributed.h index c14147e53..dab190264 100644 --- a/src/theory/shared_solver_distributed.h +++ b/src/theory/shared_solver_distributed.h @@ -13,7 +13,7 @@ * Shared solver in the distributed architecture. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__SHARED_SOLVER_DISTRIBUTED__H #define CVC5__THEORY__SHARED_SOLVER_DISTRIBUTED__H diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index b94f34d6e..efc2b2154 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -14,7 +14,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/skolem_lemma.h b/src/theory/skolem_lemma.h index ede9d2d38..2cb1c6738 100644 --- a/src/theory/skolem_lemma.h +++ b/src/theory/skolem_lemma.h @@ -13,7 +13,7 @@ * The skolem lemma utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__SKOLEM_LEMMA_H #define CVC5__THEORY__SKOLEM_LEMMA_H diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h index ee2b4889a..f7985d651 100644 --- a/src/theory/smt_engine_subsolver.h +++ b/src/theory/smt_engine_subsolver.h @@ -13,7 +13,7 @@ * Utilities for initializing subsolvers (copies of SmtEngine) during solving. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__SMT_ENGINE_SUBSOLVER_H #define CVC5__THEORY__SMT_ENGINE_SUBSOLVER_H diff --git a/src/theory/sort_inference.h b/src/theory/sort_inference.h index f566a2133..1dc7ff3c3 100644 --- a/src/theory/sort_inference.h +++ b/src/theory/sort_inference.h @@ -13,7 +13,7 @@ * Pre-process step for performing sort inference. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__SORT_INFERENCE_H #define CVC5__SORT_INFERENCE_H diff --git a/src/theory/strings/arith_entail.h b/src/theory/strings/arith_entail.h index 55876522e..64e76e5b6 100644 --- a/src/theory/strings/arith_entail.h +++ b/src/theory/strings/arith_entail.h @@ -13,7 +13,7 @@ * Arithmetic entailment computation for string terms. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__ARITH_ENTAIL_H #define CVC5__THEORY__STRINGS__ARITH_ENTAIL_H diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h index 0065c3f5a..41cb3e608 100644 --- a/src/theory/strings/base_solver.h +++ b/src/theory/strings/base_solver.h @@ -14,7 +14,7 @@ * theory of strings. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__BASE_SOLVER_H #define CVC5__THEORY__STRINGS__BASE_SOLVER_H diff --git a/src/theory/strings/core_solver.h b/src/theory/strings/core_solver.h index e06d39446..143155f55 100644 --- a/src/theory/strings/core_solver.h +++ b/src/theory/strings/core_solver.h @@ -14,7 +14,7 @@ * string concatenation plus length constraints. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__CORE_SOLVER_H #define CVC5__THEORY__STRINGS__CORE_SOLVER_H diff --git a/src/theory/strings/eager_solver.h b/src/theory/strings/eager_solver.h index d3077f44d..cf4062bfe 100644 --- a/src/theory/strings/eager_solver.h +++ b/src/theory/strings/eager_solver.h @@ -13,7 +13,7 @@ * The eager solver. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__EAGER_SOLVER_H #define CVC5__THEORY__STRINGS__EAGER_SOLVER_H diff --git a/src/theory/strings/eqc_info.h b/src/theory/strings/eqc_info.h index f90dd9b87..1fd430c95 100644 --- a/src/theory/strings/eqc_info.h +++ b/src/theory/strings/eqc_info.h @@ -13,7 +13,7 @@ * Equivalence class info for the theory of strings. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__EQC_INFO_H #define CVC5__THEORY__STRINGS__EQC_INFO_H diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h index 6dfb3fa61..bfcf244d7 100644 --- a/src/theory/strings/extf_solver.h +++ b/src/theory/strings/extf_solver.h @@ -13,7 +13,7 @@ * Solver for extended functions of theory of strings. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__EXTF_SOLVER_H #define CVC5__THEORY__STRINGS__EXTF_SOLVER_H diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h index aab837826..22460d22d 100644 --- a/src/theory/strings/infer_info.h +++ b/src/theory/strings/infer_info.h @@ -13,7 +13,7 @@ * Inference information utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__INFER_INFO_H #define CVC5__THEORY__STRINGS__INFER_INFO_H diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h index 876a2c2a5..6b2c4dfc4 100644 --- a/src/theory/strings/infer_proof_cons.h +++ b/src/theory/strings/infer_proof_cons.h @@ -13,7 +13,7 @@ * Inference to proof conversion. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__INFER_PROOF_CONS_H #define CVC5__THEORY__STRINGS__INFER_PROOF_CONS_H diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index 111542b02..b18c64319 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -13,7 +13,7 @@ * Customized inference manager for the theory of strings. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__INFERENCE_MANAGER_H #define CVC5__THEORY__STRINGS__INFERENCE_MANAGER_H diff --git a/src/theory/strings/normal_form.h b/src/theory/strings/normal_form.h index d42c003bf..e3291e9bb 100644 --- a/src/theory/strings/normal_form.h +++ b/src/theory/strings/normal_form.h @@ -13,7 +13,7 @@ * Normal form datastructure for the theory of strings. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__NORMAL_FORM_H #define CVC5__THEORY__STRINGS__NORMAL_FORM_H diff --git a/src/theory/strings/proof_checker.h b/src/theory/strings/proof_checker.h index d3b17e2d2..d3ede53ec 100644 --- a/src/theory/strings/proof_checker.h +++ b/src/theory/strings/proof_checker.h @@ -13,7 +13,7 @@ * Strings proof checker utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__PROOF_CHECKER_H #define CVC5__THEORY__STRINGS__PROOF_CHECKER_H diff --git a/src/theory/strings/regexp_elim.h b/src/theory/strings/regexp_elim.h index e6d6702b7..5387548de 100644 --- a/src/theory/strings/regexp_elim.h +++ b/src/theory/strings/regexp_elim.h @@ -13,7 +13,7 @@ * Techniques for eliminating regular expressions. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__REGEXP_ELIM_H #define CVC5__THEORY__STRINGS__REGEXP_ELIM_H diff --git a/src/theory/strings/regexp_entail.h b/src/theory/strings/regexp_entail.h index 752ae5a69..44f0815b7 100644 --- a/src/theory/strings/regexp_entail.h +++ b/src/theory/strings/regexp_entail.h @@ -13,7 +13,7 @@ * Entailment tests involving regular expressions. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__REGEXP_ENTAIL_H #define CVC5__THEORY__STRINGS__REGEXP_ENTAIL_H diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index ba0d7e2cc..d0ed07308 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -13,7 +13,7 @@ * Symbolic Regular Expression Operations */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__REGEXP__OPERATION_H #define CVC5__THEORY__STRINGS__REGEXP__OPERATION_H diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h index d18c1998d..bf148a071 100644 --- a/src/theory/strings/regexp_solver.h +++ b/src/theory/strings/regexp_solver.h @@ -13,7 +13,7 @@ * Regular expression solver for the theory of strings. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__REGEXP_SOLVER_H #define CVC5__THEORY__STRINGS__REGEXP_SOLVER_H diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h index b4d6739f5..0173d309a 100644 --- a/src/theory/strings/rewrites.h +++ b/src/theory/strings/rewrites.h @@ -13,7 +13,7 @@ * Type for rewrites for strings. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__REWRITES_H #define CVC5__THEORY__STRINGS__REWRITES_H diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h index 6a337568c..1564a5ebc 100644 --- a/src/theory/strings/sequences_rewriter.h +++ b/src/theory/strings/sequences_rewriter.h @@ -13,7 +13,7 @@ * Rewriter for the theory of strings and sequences. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__SEQUENCES_REWRITER_H #define CVC5__THEORY__STRINGS__SEQUENCES_REWRITER_H diff --git a/src/theory/strings/sequences_stats.h b/src/theory/strings/sequences_stats.h index 891497ead..e442fcc0c 100644 --- a/src/theory/strings/sequences_stats.h +++ b/src/theory/strings/sequences_stats.h @@ -13,7 +13,7 @@ * Statistics for the theory of strings/sequences. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__SEQUENCES_STATS_H #define CVC5__THEORY__STRINGS__SEQUENCES_STATS_H diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index d64e4d5ae..b3ffa784f 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -13,7 +13,7 @@ * A cache of skolems for theory of strings. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__SKOLEM_CACHE_H #define CVC5__THEORY__STRINGS__SKOLEM_CACHE_H diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h index d63d2b63b..422c29760 100644 --- a/src/theory/strings/solver_state.h +++ b/src/theory/strings/solver_state.h @@ -13,7 +13,7 @@ * The solver state of the theory of strings. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__SOLVER_STATE_H #define CVC5__THEORY__STRINGS__SOLVER_STATE_H diff --git a/src/theory/strings/strategy.h b/src/theory/strings/strategy.h index 94d87c87e..c390c5594 100644 --- a/src/theory/strings/strategy.h +++ b/src/theory/strings/strategy.h @@ -13,7 +13,7 @@ * Strategy of the theory of strings. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__STRATEGY_H #define CVC5__THEORY__STRINGS__STRATEGY_H diff --git a/src/theory/strings/strings_entail.h b/src/theory/strings/strings_entail.h index 0a66f3126..7547bf809 100644 --- a/src/theory/strings/strings_entail.h +++ b/src/theory/strings/strings_entail.h @@ -13,7 +13,7 @@ * Entailment tests involving strings. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__STRING_ENTAIL_H #define CVC5__THEORY__STRINGS__STRING_ENTAIL_H diff --git a/src/theory/strings/strings_fmf.h b/src/theory/strings/strings_fmf.h index f29e74e40..ba9f0f4e1 100644 --- a/src/theory/strings/strings_fmf.h +++ b/src/theory/strings/strings_fmf.h @@ -13,7 +13,7 @@ * A finite model finding decision strategy for strings. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__STRINGS_FMF_H #define CVC5__THEORY__STRINGS__STRINGS_FMF_H diff --git a/src/theory/strings/strings_rewriter.h b/src/theory/strings/strings_rewriter.h index 1f0b13d5f..bfe780535 100644 --- a/src/theory/strings/strings_rewriter.h +++ b/src/theory/strings/strings_rewriter.h @@ -13,7 +13,7 @@ * Rewrite rules for string-specific operators in theory of strings. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__STRINGS_REWRITER_H #define CVC5__THEORY__STRINGS__STRINGS_REWRITER_H diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h index 1f0b7c975..f0543c282 100644 --- a/src/theory/strings/term_registry.h +++ b/src/theory/strings/term_registry.h @@ -13,7 +13,7 @@ * Term registry for the theory of strings. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__TERM_REGISTRY_H #define CVC5__THEORY__STRINGS__TERM_REGISTRY_H diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 4da1ae670..fb6df80c7 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -13,7 +13,7 @@ * Theory of strings. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__THEORY_STRINGS_H #define CVC5__THEORY__STRINGS__THEORY_STRINGS_H diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index 1639f3aa6..fe190532d 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -13,7 +13,7 @@ * Strings Preprocess. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__PREPROCESS_H #define CVC5__THEORY__STRINGS__PREPROCESS_H diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 496599252..4631b33c7 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -13,7 +13,7 @@ * Typing rules for the theory of strings and regexps. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H #define CVC5__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h index 8423e1f61..ec093031e 100644 --- a/src/theory/strings/theory_strings_utils.h +++ b/src/theory/strings/theory_strings_utils.h @@ -13,7 +13,7 @@ * Util functions for theory strings. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__THEORY_STRINGS_UTILS_H #define CVC5__THEORY__STRINGS__THEORY_STRINGS_UTILS_H diff --git a/src/theory/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h index a32b94d16..37319a278 100644 --- a/src/theory/strings/type_enumerator.h +++ b/src/theory/strings/type_enumerator.h @@ -13,7 +13,7 @@ * Enumerators for strings. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__TYPE_ENUMERATOR_H #define CVC5__THEORY__STRINGS__TYPE_ENUMERATOR_H diff --git a/src/theory/strings/word.h b/src/theory/strings/word.h index 90a8306f9..18bdad8b7 100644 --- a/src/theory/strings/word.h +++ b/src/theory/strings/word.h @@ -13,7 +13,7 @@ * Utility functions for words. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__STRINGS__WORD_H #define CVC5__THEORY__STRINGS__WORD_H diff --git a/src/theory/subs_minimize.h b/src/theory/subs_minimize.h index ac0d3e353..c78467508 100644 --- a/src/theory/subs_minimize.h +++ b/src/theory/subs_minimize.h @@ -13,7 +13,7 @@ * Substitution minimization. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__SUBS_MINIMIZE_H #define CVC5__THEORY__SUBS_MINIMIZE_H diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 993315a7a..06e39e7a9 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -13,7 +13,7 @@ * A substitution mapping for theory simplification. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__SUBSTITUTIONS_H #define CVC5__THEORY__SUBSTITUTIONS_H diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h index 3af07a6c9..04200ed70 100644 --- a/src/theory/term_registration_visitor.h +++ b/src/theory/term_registration_visitor.h @@ -14,7 +14,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/theory.h b/src/theory/theory.h index 7ca06d174..3d3ec0627 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -13,7 +13,7 @@ * Base of the theory interface. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__THEORY_H #define CVC5__THEORY__THEORY_H diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 09d33edc2..dcf4ff2c8 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -13,7 +13,7 @@ * The theory engine. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY_ENGINE_H #define CVC5__THEORY_ENGINE_H diff --git a/src/theory/theory_engine_proof_generator.h b/src/theory/theory_engine_proof_generator.h index 27bf2d289..167216226 100644 --- a/src/theory/theory_engine_proof_generator.h +++ b/src/theory/theory_engine_proof_generator.h @@ -13,7 +13,7 @@ * The theory engine proof generator. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY_ENGINE_PROOF_GENERATOR_H #define CVC5__THEORY_ENGINE_PROOF_GENERATOR_H diff --git a/src/theory/theory_eq_notify.h b/src/theory/theory_eq_notify.h index 31a99b098..1d6a9cdd1 100644 --- a/src/theory/theory_eq_notify.h +++ b/src/theory/theory_eq_notify.h @@ -13,7 +13,7 @@ * The theory equality notify utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__THEORY_EQ_NOTIFY_H #define CVC5__THEORY__THEORY_EQ_NOTIFY_H diff --git a/src/theory/theory_id.h b/src/theory/theory_id.h index fdefcbf22..3bd2df556 100644 --- a/src/theory/theory_id.h +++ b/src/theory/theory_id.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__THEORY__THEORY_ID_H #define CVC5__THEORY__THEORY_ID_H diff --git a/src/theory/theory_inference.h b/src/theory/theory_inference.h index 16a3f88ff..7d90c4554 100644 --- a/src/theory/theory_inference.h +++ b/src/theory/theory_inference.h @@ -13,7 +13,7 @@ * The theory inference utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__THEORY_INFERENCE_H #define CVC5__THEORY__THEORY_INFERENCE_H diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index c9d198e2c..89c4aec3f 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -13,7 +13,7 @@ * An inference manager for Theory. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__THEORY_INFERENCE_MANAGER_H #define CVC5__THEORY__THEORY_INFERENCE_MANAGER_H diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index da6cf8eec..42392c522 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -13,7 +13,7 @@ * Model class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__THEORY_MODEL_H #define CVC5__THEORY__THEORY_MODEL_H diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h index 2ed8e2be6..af3f30fb0 100644 --- a/src/theory/theory_model_builder.h +++ b/src/theory/theory_model_builder.h @@ -13,7 +13,7 @@ * Model class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__THEORY_MODEL_BUILDER_H #define CVC5__THEORY__THEORY_MODEL_BUILDER_H diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h index dad576ade..79b5dbe01 100644 --- a/src/theory/theory_preprocessor.h +++ b/src/theory/theory_preprocessor.h @@ -13,7 +13,7 @@ * The theory preprocessor. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__THEORY_PREPROCESSOR_H #define CVC5__THEORY__THEORY_PREPROCESSOR_H diff --git a/src/theory/theory_proof_step_buffer.h b/src/theory/theory_proof_step_buffer.h index f850c8ff7..328266b89 100644 --- a/src/theory/theory_proof_step_buffer.h +++ b/src/theory/theory_proof_step_buffer.h @@ -13,7 +13,7 @@ * Theory proof step buffer utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__THEORY_PROOF_STEP_BUFFER_H #define CVC5__THEORY__THEORY_PROOF_STEP_BUFFER_H diff --git a/src/theory/theory_rewriter.h b/src/theory/theory_rewriter.h index ad3100721..2477de51e 100644 --- a/src/theory/theory_rewriter.h +++ b/src/theory/theory_rewriter.h @@ -15,7 +15,7 @@ * The interface that theory rewriters implement. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__THEORY_REWRITER_H #define CVC5__THEORY__THEORY_REWRITER_H diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h index 933f44d2b..2c7bad60b 100644 --- a/src/theory/theory_state.h +++ b/src/theory/theory_state.h @@ -13,7 +13,7 @@ * A theory state for Theory. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__THEORY_STATE_H #define CVC5__THEORY__THEORY_STATE_H diff --git a/src/theory/theory_traits_template.h b/src/theory/theory_traits_template.h index 17ca81be5..75a922096 100644 --- a/src/theory/theory_traits_template.h +++ b/src/theory/theory_traits_template.h @@ -18,7 +18,7 @@ * kinds files to produce the final header. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/theory/trust_node.h b/src/theory/trust_node.h index 38ba20941..0a4f20c34 100644 --- a/src/theory/trust_node.h +++ b/src/theory/trust_node.h @@ -13,7 +13,7 @@ * The trust node utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__TRUST_NODE_H #define CVC5__THEORY__TRUST_NODE_H diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h index 087fdbab9..c875eca2f 100644 --- a/src/theory/trust_substitutions.h +++ b/src/theory/trust_substitutions.h @@ -13,7 +13,7 @@ * Trust substitutions. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__TRUST_SUBSTITUTIONS_H #define CVC5__THEORY__TRUST_SUBSTITUTIONS_H diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h index 782d15741..aaeea6a4f 100644 --- a/src/theory/type_enumerator.h +++ b/src/theory/type_enumerator.h @@ -13,7 +13,7 @@ * Enumerators for types. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__TYPE_ENUMERATOR_H #define CVC5__THEORY__TYPE_ENUMERATOR_H diff --git a/src/theory/type_set.h b/src/theory/type_set.h index 37552f6e5..229ec2001 100644 --- a/src/theory/type_set.h +++ b/src/theory/type_set.h @@ -13,7 +13,7 @@ * Type set class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__TYPE_SET_H #define CVC5__THEORY__TYPE_SET_H 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 @@ * </pre> */ -#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 diff --git a/src/theory/valuation.h b/src/theory/valuation.h index 9eaf24616..a1a3db706 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -17,7 +17,7 @@ * takes a Valuation, which delegates to TheoryEngine. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__VALUATION_H #define CVC5__THEORY__VALUATION_H |