diff options
Diffstat (limited to 'src/theory/sets')
| -rw-r--r-- | src/theory/sets/cardinality_extension.h | 2 | ||||
| -rw-r--r-- | src/theory/sets/inference_manager.h | 2 | ||||
| -rw-r--r-- | src/theory/sets/normal_form.h | 2 | ||||
| -rw-r--r-- | src/theory/sets/singleton_op.h | 2 | ||||
| -rw-r--r-- | src/theory/sets/skolem_cache.h | 2 | ||||
| -rw-r--r-- | src/theory/sets/solver_state.h | 2 | ||||
| -rw-r--r-- | src/theory/sets/term_registry.h | 2 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets.h | 2 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_private.h | 2 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_rewriter.h | 2 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_type_enumerator.h | 2 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_type_rules.h | 2 |
12 files changed, 12 insertions, 12 deletions
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 |