diff options
Diffstat (limited to 'src/theory/arith/nl')
-rw-r--r-- | src/theory/arith/nl/cad/cdcac.h | 2 | ||||
-rw-r--r-- | src/theory/arith/nl/cad/cdcac_utils.h | 2 | ||||
-rw-r--r-- | src/theory/arith/nl/cad/constraints.h | 2 | ||||
-rw-r--r-- | src/theory/arith/nl/cad/projections.h | 2 | ||||
-rw-r--r-- | src/theory/arith/nl/cad/proof_checker.h | 2 | ||||
-rw-r--r-- | src/theory/arith/nl/cad/proof_generator.h | 2 | ||||
-rw-r--r-- | src/theory/arith/nl/cad/variable_ordering.h | 2 | ||||
-rw-r--r-- | src/theory/arith/nl/ext/proof_checker.h | 2 | ||||
-rw-r--r-- | src/theory/arith/nl/iand_utils.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/nl/icp/candidate.h | 2 | ||||
-rw-r--r-- | src/theory/arith/nl/icp/icp_solver.h | 2 | ||||
-rw-r--r-- | src/theory/arith/nl/icp/intersection.h | 2 | ||||
-rw-r--r-- | src/theory/arith/nl/icp/interval.h | 2 | ||||
-rw-r--r-- | src/theory/arith/nl/poly_conversion.h | 2 | ||||
-rw-r--r-- | src/theory/arith/nl/stats.h | 2 | ||||
-rw-r--r-- | src/theory/arith/nl/transcendental/proof_checker.h | 2 |
16 files changed, 16 insertions, 16 deletions
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 |