diff options
Diffstat (limited to 'src/expr')
59 files changed, 59 insertions, 61 deletions
diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h index 75b1a6d06..3b94f4f9f 100644 --- a/src/expr/array_store_all.h +++ b/src/expr/array_store_all.h @@ -14,7 +14,7 @@ * same for all indices). */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__ARRAY_STORE_ALL_H #define CVC5__ARRAY_STORE_ALL_H diff --git a/src/expr/ascription_type.h b/src/expr/ascription_type.h index bb8967abd..05874f6e8 100644 --- a/src/expr/ascription_type.h +++ b/src/expr/ascription_type.h @@ -13,7 +13,7 @@ * A class representing a parameter for the type ascription operator. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__ASCRIPTION_TYPE_H #define CVC5__ASCRIPTION_TYPE_H diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 7ddc01427..e42338bbb 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -13,7 +13,7 @@ * Node attributes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" /* There are strong constraints on ordering of declarations of * attributes and nodes due to template use */ diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index e1c6f759f..c82e62836 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -13,7 +13,7 @@ * Node attributes' internals. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H # error expr/attribute_internals.h should only be included by expr/attribute.h diff --git a/src/expr/attribute_unique_id.h b/src/expr/attribute_unique_id.h index df7194f5a..ae86ba256 100644 --- a/src/expr/attribute_unique_id.h +++ b/src/expr/attribute_unique_id.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/expr/bound_var_manager.h b/src/expr/bound_var_manager.h index fdfbc8460..4c9c0af20 100644 --- a/src/expr/bound_var_manager.h +++ b/src/expr/bound_var_manager.h @@ -13,7 +13,7 @@ * Bound variable manager. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__BOUND_VAR_MANAGER_H #define CVC5__EXPR__BOUND_VAR_MANAGER_H diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h index 89e8b196d..4ac0b9add 100644 --- a/src/expr/buffered_proof_generator.h +++ b/src/expr/buffered_proof_generator.h @@ -13,7 +13,7 @@ * A proof generator for buffered proof steps. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H #define CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H diff --git a/src/expr/datatype_index.h b/src/expr/datatype_index.h index c46bcda85..f5f636b29 100644 --- a/src/expr/datatype_index.h +++ b/src/expr/datatype_index.h @@ -13,7 +13,7 @@ * A class representing an index to a datatype living in NodeManager. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__DATATYPE_INDEX_H #define CVC5__DATATYPE_INDEX_H diff --git a/src/expr/dtype.h b/src/expr/dtype.h index 2837e37af..da16729cc 100644 --- a/src/expr/dtype.h +++ b/src/expr/dtype.h @@ -13,7 +13,7 @@ * A class representing a datatype definition. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__DTYPE_H #define CVC5__EXPR__DTYPE_H diff --git a/src/expr/dtype_cons.h b/src/expr/dtype_cons.h index 55d940d91..a6268aad1 100644 --- a/src/expr/dtype_cons.h +++ b/src/expr/dtype_cons.h @@ -13,7 +13,7 @@ * A class representing a datatype definition. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__DTYPE_CONS_H #define CVC5__EXPR__DTYPE_CONS_H diff --git a/src/expr/dtype_selector.h b/src/expr/dtype_selector.h index 391d233ca..1c7d63d65 100644 --- a/src/expr/dtype_selector.h +++ b/src/expr/dtype_selector.h @@ -13,7 +13,7 @@ * A class representing a datatype selector. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__DTYPE_SELECTOR_H #define CVC5__EXPR__DTYPE_SELECTOR_H diff --git a/src/expr/emptybag.h b/src/expr/emptybag.h index 78c573674..16f7d3d9c 100644 --- a/src/expr/emptybag.h +++ b/src/expr/emptybag.h @@ -13,7 +13,7 @@ * A class for empty bags. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__EMPTY_BAG_H #define CVC5__EMPTY_BAG_H diff --git a/src/expr/emptyset.h b/src/expr/emptyset.h index a545e48b0..d3bdd1ec4 100644 --- a/src/expr/emptyset.h +++ b/src/expr/emptyset.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__EMPTY_SET_H #define CVC5__EMPTY_SET_H diff --git a/src/expr/expr_iomanip.h b/src/expr/expr_iomanip.h index 35ee6c324..a04ed9f39 100644 --- a/src/expr/expr_iomanip.h +++ b/src/expr/expr_iomanip.h @@ -13,7 +13,7 @@ * Expr IO manipulation classes. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__EXPR__EXPR_IOMANIP_H #define CVC5__EXPR__EXPR_IOMANIP_H diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h index 1add4eb31..3c5f27c49 100644 --- a/src/expr/kind_map.h +++ b/src/expr/kind_map.h @@ -16,7 +16,7 @@ * manipulable, and packed. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__KIND_MAP_H #define CVC5__KIND_MAP_H diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index c4fc6fc73..d5fc3967c 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -13,7 +13,7 @@ * Template for the Node kind header. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__KIND_H #define CVC5__KIND_H diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h index 21a862691..6bec9ffb9 100644 --- a/src/expr/lazy_proof.h +++ b/src/expr/lazy_proof.h @@ -13,7 +13,7 @@ * Lazy proof utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__LAZY_PROOF_H #define CVC5__EXPR__LAZY_PROOF_H diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h index 5a91e3e29..fa965f8bb 100644 --- a/src/expr/lazy_proof_chain.h +++ b/src/expr/lazy_proof_chain.h @@ -13,7 +13,7 @@ * Lazy proof chain utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__LAZY_PROOF_CHAIN_H #define CVC5__EXPR__LAZY_PROOF_CHAIN_H diff --git a/src/expr/match_trie.h b/src/expr/match_trie.h index e17b711fc..e483b23fe 100644 --- a/src/expr/match_trie.h +++ b/src/expr/match_trie.h @@ -13,7 +13,7 @@ * Implements a match trie, also known as a discrimination tree. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__MATCH_TRIE_H #define CVC5__EXPR__MATCH_TRIE_H diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 2af169577..0747b97fa 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -13,7 +13,7 @@ * Template for the metakind header. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__KIND__METAKIND_H #define CVC5__KIND__METAKIND_H diff --git a/src/expr/node.h b/src/expr/node.h index bd2120695..181fc2e52 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -13,7 +13,7 @@ * Reference-counted encapsulation of a pointer to node information. */ -#include "cvc4_private.h" +#include "cvc5_private.h" // circular dependency #include "expr/node_value.h" diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index b55802fd4..010724c80 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -16,7 +16,7 @@ * be included in source files. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__NODE_ALGORITHM_H #define CVC5__EXPR__NODE_ALGORITHM_H diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index dd9a41146..a7da518ab 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -131,7 +131,7 @@ * d_nv is deallocated. */ -#include "cvc4_private.h" +#include "cvc5_private.h" /* strong dependency; make sure node is included first */ #include "expr/node.h" diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 39d0510a6..5ca6823d9 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -13,7 +13,7 @@ * A manager for Nodes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" /* circular dependency; force node.h first */ //#include "expr/attribute.h" diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h index d4ebed9a3..de6082ead 100644 --- a/src/expr/node_self_iterator.h +++ b/src/expr/node_self_iterator.h @@ -13,7 +13,7 @@ * Iterator supporting Node "self-iteration." */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__NODE_SELF_ITERATOR_H #define CVC5__EXPR__NODE_SELF_ITERATOR_H diff --git a/src/expr/node_traversal.h b/src/expr/node_traversal.h index 095494edb..6489e19c8 100644 --- a/src/expr/node_traversal.h +++ b/src/expr/node_traversal.h @@ -13,7 +13,7 @@ * Iterators for traversing nodes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__NODE_TRAVERSAL_H #define CVC5__EXPR__NODE_TRAVERSAL_H diff --git a/src/expr/node_trie.h b/src/expr/node_trie.h index 5519f4666..8617d19f5 100644 --- a/src/expr/node_trie.h +++ b/src/expr/node_trie.h @@ -13,7 +13,7 @@ * A trie class for Nodes and TNodes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__NODE_TRIE_H #define CVC5__EXPR__NODE_TRIE_H diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 268fadeef..3aa927bdb 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -18,7 +18,7 @@ * NodeValue instances. */ -#include "cvc4_private.h" +#include "cvc5_private.h" // circular dependency #include "expr/metakind.h" diff --git a/src/expr/node_visitor.h b/src/expr/node_visitor.h index 52755e9fa..73de7c02d 100644 --- a/src/expr/node_visitor.h +++ b/src/expr/node_visitor.h @@ -15,10 +15,9 @@ #pragma once -#include "cvc4_private.h" - #include <vector> +#include "cvc5_private.h" #include "expr/node.h" namespace cvc5 { diff --git a/src/expr/proof.h b/src/expr/proof.h index de599a252..25ab1fd23 100644 --- a/src/expr/proof.h +++ b/src/expr/proof.h @@ -13,7 +13,7 @@ * Proof utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__PROOF_H #define CVC5__EXPR__PROOF_H diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h index a6aa1e557..69be40ad0 100644 --- a/src/expr/proof_checker.h +++ b/src/expr/proof_checker.h @@ -13,7 +13,7 @@ * Proof checker utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__PROOF_CHECKER_H #define CVC5__EXPR__PROOF_CHECKER_H diff --git a/src/expr/proof_ensure_closed.h b/src/expr/proof_ensure_closed.h index 71bfa86fd..3d126a4a1 100644 --- a/src/expr/proof_ensure_closed.h +++ b/src/expr/proof_ensure_closed.h @@ -13,7 +13,7 @@ * Debug checks for ensuring proofs are closed. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__PROOF_ENSURE_CLOSED_H #define CVC5__EXPR__PROOF_ENSURE_CLOSED_H diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h index e95cf3a3c..2e87ab756 100644 --- a/src/expr/proof_generator.h +++ b/src/expr/proof_generator.h @@ -13,7 +13,7 @@ * The abstract proof generator class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__PROOF_GENERATOR_H #define CVC5__EXPR__PROOF_GENERATOR_H diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h index abac0431c..08d2a0245 100644 --- a/src/expr/proof_node.h +++ b/src/expr/proof_node.h @@ -13,7 +13,7 @@ * Proof node utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__PROOF_NODE_H #define CVC5__EXPR__PROOF_NODE_H diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h index 58d0098d1..4c89dd4bc 100644 --- a/src/expr/proof_node_algorithm.h +++ b/src/expr/proof_node_algorithm.h @@ -13,7 +13,7 @@ * Proof node algorithm utilities. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__PROOF_NODE_ALGORITHM_H #define CVC5__EXPR__PROOF_NODE_ALGORITHM_H diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h index d83143e82..853d22de7 100644 --- a/src/expr/proof_node_manager.h +++ b/src/expr/proof_node_manager.h @@ -13,7 +13,7 @@ * Proof node manager utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__PROOF_NODE_MANAGER_H #define CVC5__EXPR__PROOF_NODE_MANAGER_H diff --git a/src/expr/proof_node_to_sexpr.h b/src/expr/proof_node_to_sexpr.h index 46fb32308..d4cca8eae 100644 --- a/src/expr/proof_node_to_sexpr.h +++ b/src/expr/proof_node_to_sexpr.h @@ -13,7 +13,7 @@ * Conversion from ProofNode to s-expressions. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__PROOF_NODE_TO_SEXPR_H #define CVC5__EXPR__PROOF_NODE_TO_SEXPR_H diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h index be54de207..3146160bb 100644 --- a/src/expr/proof_node_updater.h +++ b/src/expr/proof_node_updater.h @@ -13,7 +13,7 @@ * A utility for updating proof nodes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__PROOF_NODE_UPDATER_H #define CVC5__EXPR__PROOF_NODE_UPDATER_H diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 11b4c1bb0..d2aa75d8c 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -13,7 +13,7 @@ * Proof rule enumeration. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__PROOF_RULE_H #define CVC5__EXPR__PROOF_RULE_H diff --git a/src/expr/proof_set.h b/src/expr/proof_set.h index 7193f5572..5ea9c1021 100644 --- a/src/expr/proof_set.h +++ b/src/expr/proof_set.h @@ -13,7 +13,7 @@ * Proof set utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__PROOF_SET_H #define CVC5__EXPR__PROOF_SET_H diff --git a/src/expr/proof_step_buffer.h b/src/expr/proof_step_buffer.h index b74ced0f1..b9350cf45 100644 --- a/src/expr/proof_step_buffer.h +++ b/src/expr/proof_step_buffer.h @@ -13,7 +13,7 @@ * Proof step and proof step buffer utilities. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__PROOF_STEP_BUFFER_H #define CVC5__EXPR__PROOF_STEP_BUFFER_H diff --git a/src/expr/record.h b/src/expr/record.h index 555d0ae08..ecf6c8d32 100644 --- a/src/expr/record.h +++ b/src/expr/record.h @@ -13,7 +13,7 @@ * A class representing a Record definition. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__RECORD_H #define CVC5__RECORD_H diff --git a/src/expr/sequence.h b/src/expr/sequence.h index b2018d0eb..40cadb858 100644 --- a/src/expr/sequence.h +++ b/src/expr/sequence.h @@ -13,7 +13,7 @@ * The sequence data type. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__EXPR__SEQUENCE_H #define CVC5__EXPR__SEQUENCE_H diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index dd228e598..13d0491a6 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -13,7 +13,7 @@ * Skolem manager utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__SKOLEM_MANAGER_H #define CVC5__EXPR__SKOLEM_MANAGER_H diff --git a/src/expr/sygus_datatype.h b/src/expr/sygus_datatype.h index ef0fa4de7..fa3fce5b2 100644 --- a/src/expr/sygus_datatype.h +++ b/src/expr/sygus_datatype.h @@ -12,7 +12,7 @@ * * A class for constructing SyGuS datatypes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__SYGUS_DATATYPE_H #define CVC5__EXPR__SYGUS_DATATYPE_H diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h index 9f951ebfb..53057d0b1 100644 --- a/src/expr/symbol_manager.h +++ b/src/expr/symbol_manager.h @@ -13,7 +13,7 @@ * The symbol manager. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__EXPR__SYMBOL_MANAGER_H #define CVC5__EXPR__SYMBOL_MANAGER_H diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index 5539adefb..cd80c0eba 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -13,7 +13,7 @@ * Convenience class for scoping variable and type declarations. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__SYMBOL_TABLE_H #define CVC5__SYMBOL_TABLE_H diff --git a/src/expr/tconv_seq_proof_generator.h b/src/expr/tconv_seq_proof_generator.h index 960a2f081..ba8c438b2 100644 --- a/src/expr/tconv_seq_proof_generator.h +++ b/src/expr/tconv_seq_proof_generator.h @@ -13,7 +13,7 @@ * Term conversion sequence proof generator utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__TCONV_SEQ_PROOF_GENERATOR_H #define CVC5__EXPR__TCONV_SEQ_PROOF_GENERATOR_H diff --git a/src/expr/term_canonize.h b/src/expr/term_canonize.h index 188359e58..6b9cf9cb9 100644 --- a/src/expr/term_canonize.h +++ b/src/expr/term_canonize.h @@ -13,7 +13,7 @@ * Utilities for constructing canonical terms. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__TERM_CANONIZE_H #define CVC5__EXPR__TERM_CANONIZE_H diff --git a/src/expr/term_context.h b/src/expr/term_context.h index 320c8e65b..37d2ef6bd 100644 --- a/src/expr/term_context.h +++ b/src/expr/term_context.h @@ -13,7 +13,7 @@ * Term context utilities. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__TERM_CONTEXT_H #define CVC5__EXPR__TERM_CONTEXT_H diff --git a/src/expr/term_context_node.h b/src/expr/term_context_node.h index cc60f01b5..ac89b0d71 100644 --- a/src/expr/term_context_node.h +++ b/src/expr/term_context_node.h @@ -13,7 +13,7 @@ * Term context node utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__TERM_CONTEXT_NODE_H #define CVC5__EXPR__TERM_CONTEXT_NODE_H diff --git a/src/expr/term_context_stack.h b/src/expr/term_context_stack.h index 51cf922aa..e3412793f 100644 --- a/src/expr/term_context_stack.h +++ b/src/expr/term_context_stack.h @@ -13,7 +13,7 @@ * Term context. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__TERM_CONTEXT_STACK_H #define CVC5__EXPR__TERM_CONTEXT_STACK_H diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h index 946c31acb..bc0987478 100644 --- a/src/expr/term_conversion_proof_generator.h +++ b/src/expr/term_conversion_proof_generator.h @@ -13,7 +13,7 @@ * Term conversion proof generator utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H #define CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h index 077158749..c072ca4d4 100644 --- a/src/expr/type_checker.h +++ b/src/expr/type_checker.h @@ -13,7 +13,7 @@ * A type checker. */ -#include "cvc4_private.h" +#include "cvc5_private.h" // ordering dependence #include "expr/node.h" diff --git a/src/expr/type_checker_util.h b/src/expr/type_checker_util.h index 5bdfbb02f..e837659ad 100644 --- a/src/expr/type_checker_util.h +++ b/src/expr/type_checker_util.h @@ -18,10 +18,9 @@ * for them. */ -#include "cvc4_private.h" - #include <sstream> +#include "cvc5_private.h" #include "expr/kind.h" #include "expr/node.h" #include "expr/node_manager.h" diff --git a/src/expr/type_matcher.h b/src/expr/type_matcher.h index 0d5cc9265..e7b839234 100644 --- a/src/expr/type_matcher.h +++ b/src/expr/type_matcher.h @@ -13,7 +13,7 @@ * A class representing a type matcher. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__EXPR__TYPE_MATCHER_H #define CVC5__EXPR__TYPE_MATCHER_H diff --git a/src/expr/type_node.h b/src/expr/type_node.h index dab7fd394..d1b5edf22 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -13,7 +13,7 @@ * Reference-counted encapsulation of a pointer to node information. */ -#include "cvc4_private.h" +#include "cvc5_private.h" // circular dependency #include "expr/node_value.h" diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h index 799233378..77a671a68 100644 --- a/src/expr/type_properties_template.h +++ b/src/expr/type_properties_template.h @@ -13,7 +13,7 @@ * Template for the Type properties header. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__TYPE_PROPERTIES_H #define CVC5__TYPE_PROPERTIES_H diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h index edf2cf154..4a86ba510 100644 --- a/src/expr/uninterpreted_constant.h +++ b/src/expr/uninterpreted_constant.h @@ -13,7 +13,7 @@ * Representation of constants of uninterpreted sorts. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__UNINTERPRETED_CONSTANT_H #define CVC5__UNINTERPRETED_CONSTANT_H |