diff options
Diffstat (limited to 'src/preprocessing/passes')
30 files changed, 30 insertions, 30 deletions
diff --git a/src/preprocessing/passes/ackermann.h b/src/preprocessing/passes/ackermann.h index c7d65d5cc..b51c4b344 100644 --- a/src/preprocessing/passes/ackermann.h +++ b/src/preprocessing/passes/ackermann.h @@ -22,7 +22,7 @@ * https://cs.nyu.edu/media/publications/hadarean_liana.pdf */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__ACKERMANN_H #define CVC5__PREPROCESSING__PASSES__ACKERMANN_H diff --git a/src/preprocessing/passes/apply_substs.h b/src/preprocessing/passes/apply_substs.h index 6b6155114..67b7996f5 100644 --- a/src/preprocessing/passes/apply_substs.h +++ b/src/preprocessing/passes/apply_substs.h @@ -16,7 +16,7 @@ * assertions. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__APPLY_SUBSTS_H #define CVC5__PREPROCESSING__PASSES__APPLY_SUBSTS_H diff --git a/src/preprocessing/passes/bool_to_bv.h b/src/preprocessing/passes/bool_to_bv.h index de6a82a13..ec14490a0 100644 --- a/src/preprocessing/passes/bool_to_bv.h +++ b/src/preprocessing/passes/bool_to_bv.h @@ -14,7 +14,7 @@ * */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__BOOL_TO_BV_H #define CVC5__PREPROCESSING__PASSES__BOOL_TO_BV_H diff --git a/src/preprocessing/passes/bv_abstraction.h b/src/preprocessing/passes/bv_abstraction.h index 7e07653da..0f3db2f59 100644 --- a/src/preprocessing/passes/bv_abstraction.h +++ b/src/preprocessing/passes/bv_abstraction.h @@ -22,7 +22,7 @@ * https://cs.nyu.edu/media/publications/hadarean_liana.pdf */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__BV_ABSTRACTION_H #define CVC5__PREPROCESSING__PASSES__BV_ABSTRACTION_H diff --git a/src/preprocessing/passes/bv_eager_atoms.h b/src/preprocessing/passes/bv_eager_atoms.h index 87fd87c91..ca2f8b5a6 100644 --- a/src/preprocessing/passes/bv_eager_atoms.h +++ b/src/preprocessing/passes/bv_eager_atoms.h @@ -16,7 +16,7 @@ * and allows to use eager bit-blasting in the BV solver. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H #define CVC5__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h index ceda3a885..a71f4ce3f 100644 --- a/src/preprocessing/passes/bv_gauss.h +++ b/src/preprocessing/passes/bv_gauss.h @@ -16,7 +16,7 @@ * Elimination if possible. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H #define CVC5__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H diff --git a/src/preprocessing/passes/bv_intro_pow2.h b/src/preprocessing/passes/bv_intro_pow2.h index fe4b7dceb..0ec0f4df6 100644 --- a/src/preprocessing/passes/bv_intro_pow2.h +++ b/src/preprocessing/passes/bv_intro_pow2.h @@ -17,7 +17,7 @@ * can be enabled via option `--bv-intro-pow2`. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__BV_INTRO_POW2_H #define CVC5__PREPROCESSING__PASSES__BV_INTRO_POW2_H diff --git a/src/preprocessing/passes/bv_to_bool.h b/src/preprocessing/passes/bv_to_bool.h index 442812a20..d05899cb9 100644 --- a/src/preprocessing/passes/bv_to_bool.h +++ b/src/preprocessing/passes/bv_to_bool.h @@ -13,7 +13,7 @@ * Preprocessing pass that lifts bit-vectors of size 1 to booleans. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__BV_TO_BOOL_H #define CVC5__PREPROCESSING__PASSES__BV_TO_BOOL_H diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h index d8d9e1262..b8fa00e95 100644 --- a/src/preprocessing/passes/bv_to_int.h +++ b/src/preprocessing/passes/bv_to_int.h @@ -64,7 +64,7 @@ * */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef __CVC5__PREPROCESSING__PASSES__BV_TO_INT_H #define __CVC5__PREPROCESSING__PASSES__BV_TO_INT_H diff --git a/src/preprocessing/passes/extended_rewriter_pass.h b/src/preprocessing/passes/extended_rewriter_pass.h index 69c456720..02986aea1 100644 --- a/src/preprocessing/passes/extended_rewriter_pass.h +++ b/src/preprocessing/passes/extended_rewriter_pass.h @@ -15,7 +15,7 @@ * Applies the extended rewriter to assertions. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H #define CVC5__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H diff --git a/src/preprocessing/passes/foreign_theory_rewrite.h b/src/preprocessing/passes/foreign_theory_rewrite.h index 2fc90e4c6..87299074a 100644 --- a/src/preprocessing/passes/foreign_theory_rewrite.h +++ b/src/preprocessing/passes/foreign_theory_rewrite.h @@ -15,7 +15,7 @@ * Simplifies nodes of one theory using rewrites from another. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H #define CVC5__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h index 5b5f7db4d..c7febf95d 100644 --- a/src/preprocessing/passes/global_negate.h +++ b/src/preprocessing/passes/global_negate.h @@ -22,7 +22,7 @@ * checks for unsat instead of sat. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__GLOBAL_NEGATE_H #define CVC5__PREPROCESSING__PASSES__GLOBAL_NEGATE_H diff --git a/src/preprocessing/passes/ho_elim.h b/src/preprocessing/passes/ho_elim.h index 998e4f353..a2574ff39 100644 --- a/src/preprocessing/passes/ho_elim.h +++ b/src/preprocessing/passes/ho_elim.h @@ -15,7 +15,7 @@ * Eliminates higher-order constraints. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef __CVC5__PREPROCESSING__PASSES__HO_ELIM_PASS_H #define __CVC5__PREPROCESSING__PASSES__HO_ELIM_PASS_H diff --git a/src/preprocessing/passes/int_to_bv.h b/src/preprocessing/passes/int_to_bv.h index e25154199..5d6ac15e4 100644 --- a/src/preprocessing/passes/int_to_bv.h +++ b/src/preprocessing/passes/int_to_bv.h @@ -17,7 +17,7 @@ * option. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__INT_TO_BV_H #define CVC5__PREPROCESSING__PASSES__INT_TO_BV_H diff --git a/src/preprocessing/passes/ite_removal.h b/src/preprocessing/passes/ite_removal.h index 5b9ac4beb..0371d11c7 100644 --- a/src/preprocessing/passes/ite_removal.h +++ b/src/preprocessing/passes/ite_removal.h @@ -13,7 +13,7 @@ * Remove ITEs from the assertions. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__ITE_REMOVAL_H #define CVC5__PREPROCESSING__PASSES__ITE_REMOVAL_H diff --git a/src/preprocessing/passes/ite_simp.h b/src/preprocessing/passes/ite_simp.h index 1cbe6d904..62a01b45a 100644 --- a/src/preprocessing/passes/ite_simp.h +++ b/src/preprocessing/passes/ite_simp.h @@ -13,7 +13,7 @@ * ITE simplification preprocessing pass. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__ITE_SIMP_H #define CVC5__PREPROCESSING__PASSES__ITE_SIMP_H diff --git a/src/preprocessing/passes/miplib_trick.h b/src/preprocessing/passes/miplib_trick.h index 5f5af1661..e9c331d92 100644 --- a/src/preprocessing/passes/miplib_trick.h +++ b/src/preprocessing/passes/miplib_trick.h @@ -13,7 +13,7 @@ * The MIPLIB trick preprocessing pass. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__MIPLIB_TRICK_H #define CVC5__PREPROCESSING__PASSES__MIPLIB_TRICK_H diff --git a/src/preprocessing/passes/nl_ext_purify.h b/src/preprocessing/passes/nl_ext_purify.h index 7b6c24ced..211373e35 100644 --- a/src/preprocessing/passes/nl_ext_purify.h +++ b/src/preprocessing/passes/nl_ext_purify.h @@ -16,7 +16,7 @@ * variables. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__NL_EXT_PURIFY_H #define CVC5__PREPROCESSING__PASSES__NL_EXT_PURIFY_H diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h index 80dae3972..e4987fbde 100644 --- a/src/preprocessing/passes/non_clausal_simp.h +++ b/src/preprocessing/passes/non_clausal_simp.h @@ -13,7 +13,7 @@ * Non-clausal simplification preprocessing pass. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H #define CVC5__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H diff --git a/src/preprocessing/passes/pseudo_boolean_processor.h b/src/preprocessing/passes/pseudo_boolean_processor.h index 5b259dd55..cf68bc8fb 100644 --- a/src/preprocessing/passes/pseudo_boolean_processor.h +++ b/src/preprocessing/passes/pseudo_boolean_processor.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H #define CVC5__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h index 54215b620..b856222f8 100644 --- a/src/preprocessing/passes/quantifier_macros.h +++ b/src/preprocessing/passes/quantifier_macros.h @@ -13,7 +13,7 @@ * Pre-process step for detecting quantifier macro definitions. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H #define CVC5__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H diff --git a/src/preprocessing/passes/quantifiers_preprocess.h b/src/preprocessing/passes/quantifiers_preprocess.h index 50781a8ef..511b51459 100644 --- a/src/preprocessing/passes/quantifiers_preprocess.h +++ b/src/preprocessing/passes/quantifiers_preprocess.h @@ -16,7 +16,7 @@ * pre-skolemization to existential quantifiers */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H #define CVC5__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H diff --git a/src/preprocessing/passes/real_to_int.h b/src/preprocessing/passes/real_to_int.h index d33a49dfb..9f0eb529f 100644 --- a/src/preprocessing/passes/real_to_int.h +++ b/src/preprocessing/passes/real_to_int.h @@ -15,7 +15,7 @@ * Converts real operations into integer operations. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__REAL_TO_INT_H #define CVC5__PREPROCESSING__PASSES__REAL_TO_INT_H diff --git a/src/preprocessing/passes/rewrite.h b/src/preprocessing/passes/rewrite.h index 3ecc4cd22..fcc250e17 100644 --- a/src/preprocessing/passes/rewrite.h +++ b/src/preprocessing/passes/rewrite.h @@ -15,7 +15,7 @@ * Calls the rewriter on every assertion. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__REWRITE_H #define CVC5__PREPROCESSING__PASSES__REWRITE_H diff --git a/src/preprocessing/passes/sep_skolem_emp.h b/src/preprocessing/passes/sep_skolem_emp.h index 70f25ffb4..7dfdb66a2 100644 --- a/src/preprocessing/passes/sep_skolem_emp.h +++ b/src/preprocessing/passes/sep_skolem_emp.h @@ -13,7 +13,7 @@ * The sep-pre-skolem-emp eprocessing pass. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H #define CVC5__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H diff --git a/src/preprocessing/passes/static_learning.h b/src/preprocessing/passes/static_learning.h index 8163ba638..ac9ab6251 100644 --- a/src/preprocessing/passes/static_learning.h +++ b/src/preprocessing/passes/static_learning.h @@ -13,7 +13,7 @@ * The static learning preprocessing pass. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__STATIC_LEARNING_H #define CVC5__PREPROCESSING__PASSES__STATIC_LEARNING_H diff --git a/src/preprocessing/passes/strings_eager_pp.h b/src/preprocessing/passes/strings_eager_pp.h index 5f2977938..fd89fefc7 100644 --- a/src/preprocessing/passes/strings_eager_pp.h +++ b/src/preprocessing/passes/strings_eager_pp.h @@ -13,7 +13,7 @@ * The strings eager preprocess utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H #define CVC5__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H diff --git a/src/preprocessing/passes/theory_preprocess.h b/src/preprocessing/passes/theory_preprocess.h index f8264e622..2b284bf91 100644 --- a/src/preprocessing/passes/theory_preprocess.h +++ b/src/preprocessing/passes/theory_preprocess.h @@ -15,7 +15,7 @@ * Calls Theory::preprocess(...) on every assertion of the formula. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__THEORY_PREPROCESS_H #define CVC5__PREPROCESSING__PASSES__THEORY_PREPROCESS_H diff --git a/src/preprocessing/passes/theory_rewrite_eq.h b/src/preprocessing/passes/theory_rewrite_eq.h index e88678eb5..729252dd6 100644 --- a/src/preprocessing/passes/theory_rewrite_eq.h +++ b/src/preprocessing/passes/theory_rewrite_eq.h @@ -13,7 +13,7 @@ * The TheoryRewriteEq preprocessing pass. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H #define CVC5__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H diff --git a/src/preprocessing/passes/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h index 914d450b0..31ae01504 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.h +++ b/src/preprocessing/passes/unconstrained_simplifier.h @@ -17,7 +17,7 @@ * Bruttomesso's PhD thesis. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H #define CVC5__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H |