summaryrefslogtreecommitdiff
path: root/src/theory/arith/nl
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/nl')
-rw-r--r--src/theory/arith/nl/cad/cdcac.h2
-rw-r--r--src/theory/arith/nl/cad/cdcac_utils.h2
-rw-r--r--src/theory/arith/nl/cad/constraints.h2
-rw-r--r--src/theory/arith/nl/cad/projections.h2
-rw-r--r--src/theory/arith/nl/cad/proof_checker.h2
-rw-r--r--src/theory/arith/nl/cad/proof_generator.h2
-rw-r--r--src/theory/arith/nl/cad/variable_ordering.h2
-rw-r--r--src/theory/arith/nl/ext/proof_checker.h2
-rw-r--r--src/theory/arith/nl/iand_utils.cpp2
-rw-r--r--src/theory/arith/nl/icp/candidate.h2
-rw-r--r--src/theory/arith/nl/icp/icp_solver.h2
-rw-r--r--src/theory/arith/nl/icp/intersection.h2
-rw-r--r--src/theory/arith/nl/icp/interval.h2
-rw-r--r--src/theory/arith/nl/poly_conversion.h2
-rw-r--r--src/theory/arith/nl/stats.h2
-rw-r--r--src/theory/arith/nl/transcendental/proof_checker.h2
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback