* These macros implement guards for the cvc5 C++ API functions.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__API__CHECKS_H
#define CVC5__API__CHECKS_H
* signal-handling code.
*/
-#include "cvc4_private_library.h"
+#include "cvc5_private_library.h"
#ifndef CVC5__CHECK_H
#define CVC5__CHECK_H
* about the CVC4 library.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__CONFIGURATION_H
#define CVC5__CONFIGURATION_H
* Provide compile-time configuration information about the cvc5 library.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__CONFIGURATION_PRIVATE_H
#define CVC5__CONFIGURATION_PRIVATE_H
* cvc5's exception base class and some associated utilities.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__EXCEPTION_H
#define CVC5__EXCEPTION_H
* This class provides a single notification that must be overwritten.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__LISTENER_H
#define CVC5__LISTENER_H
* - InsertIfNotPresent
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__BASE__MAP_UTIL_H
#define CVC5__BASE__MAP_UTIL_H
* "(get-assertions)" command in an SMT-LIBv2 script).
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__SMT__MODAL_EXCEPTION_H
#define CVC5__SMT__MODAL_EXCEPTION_H
* Output utility classes and functions.
*/
-#include "cvc4_private_library.h"
+#include "cvc5_private_library.h"
#ifndef CVC5__OUTPUT_H
#define CVC5__OUTPUT_H
* Contains a backtrackable list.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__UTIL__BACKTRACKABLE_H
#define CVC5__UTIL__BACKTRACKABLE_H
* than the maximum key.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* possible.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__CONTEXT__CDHASHMAP_H
#define CVC5__CONTEXT__CDHASHMAP_H
* yourself, because it has a default template argument.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__CONTEXT__CDHASHMAP_FORWARD_H
#define CVC5__CONTEXT__CDHASHMAP_FORWARD_H
* Context-dependent set class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__CONTEXT__CDHASHSET_H
#define CVC5__CONTEXT__CDHASHSET_H
* yourself, because it has a default template argument.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__CONTEXT__CDSET_FORWARD_H
#define CVC5__CONTEXT__CDSET_FORWARD_H
* - Supports insertAtContextLevelZero() if the element is not in the map.
*/
-#include "cvc4_private.h"
-
#include <deque>
#include <functional>
#include <unordered_map>
#include "base/output.h"
#include "context/cdinsert_hashmap_forward.h"
#include "context/context.h"
+#include "cvc5_private.h"
#include "expr/node.h"
#pragma once
* yourself, because it has a default template argument.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__CONTEXT__CDINSERT_HASHMAP_FORWARD_H
#define CVC5__CONTEXT__CDINSERT_HASHMAP_FORWARD_H
* simply shortened.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__CONTEXT__CDLIST_H
#define CVC5__CONTEXT__CDLIST_H
* different compilation units).
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__CONTEXT__CDLIST_FORWARD_H
#define CVC5__CONTEXT__CDLIST_FORWARD_H
* assignment.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* A context-dependent object.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__CONTEXT__CDO_H
#define CVC5__CONTEXT__CDO_H
* size_t for tracking the previous size of the list.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__CONTEXT__CDQUEUE_H
#define CVC5__CONTEXT__CDQUEUE_H
* The implementation is currently not full featured.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__CONTEXT__CDTRAIL_QUEUE_H
#define CVC5__CONTEXT__CDTRAIL_QUEUE_H
* Context class and context manager.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__CONTEXT__CONTEXT_H
#define CVC5__CONTEXT__CONTEXT_H
* Designed for use by ContextManager.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__CONTEXT__CONTEXT_MM_H
#define CVC5__CONTEXT__CONTEXT_MM_H
* Rewriter attributes.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__DECISION__DECISION_ATTRIBUTES_H
#define CVC5__DECISION__DECISION_ATTRIBUTES_H
* Decision engine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__DECISION__DECISION_ENGINE_H
#define CVC5__DECISION__DECISION_ENGINE_H
* Decision strategy.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__DECISION__DECISION_STRATEGY_H
#define CVC5__DECISION__DECISION_STRATEGY_H
* It needs access to the simplified but non-clausal formula.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__DECISION__JUSTIFICATION_HEURISTIC
#define CVC5__DECISION__JUSTIFICATION_HEURISTIC
* same for all indices).
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__ARRAY_STORE_ALL_H
#define CVC5__ARRAY_STORE_ALL_H
* 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
* 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 */
* 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
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* 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
* 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
* 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
* A class representing a datatype definition.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__EXPR__DTYPE_H
#define CVC5__EXPR__DTYPE_H
* 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
* 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
* A class for empty bags.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__EMPTY_BAG_H
#define CVC5__EMPTY_BAG_H
* \todo document this file
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__EMPTY_SET_H
#define CVC5__EMPTY_SET_H
* Expr IO manipulation classes.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__EXPR__EXPR_IOMANIP_H
#define CVC5__EXPR__EXPR_IOMANIP_H
* manipulable, and packed.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__KIND_MAP_H
#define CVC5__KIND_MAP_H
* Template for the Node kind header.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__KIND_H
#define CVC5__KIND_H
* Lazy proof utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__EXPR__LAZY_PROOF_H
#define CVC5__EXPR__LAZY_PROOF_H
* 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
* 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
* Template for the metakind header.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__KIND__METAKIND_H
#define CVC5__KIND__METAKIND_H
* Reference-counted encapsulation of a pointer to node information.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
// circular dependency
#include "expr/node_value.h"
* 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
* d_nv is deallocated.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
/* strong dependency; make sure node is included first */
#include "expr/node.h"
* A manager for Nodes.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
/* circular dependency; force node.h first */
//#include "expr/attribute.h"
* 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
* Iterators for traversing nodes.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__EXPR__NODE_TRAVERSAL_H
#define CVC5__EXPR__NODE_TRAVERSAL_H
* 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
* NodeValue instances.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
// circular dependency
#include "expr/metakind.h"
#pragma once
-#include "cvc4_private.h"
-
#include <vector>
+#include "cvc5_private.h"
#include "expr/node.h"
namespace cvc5 {
* Proof utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__EXPR__PROOF_H
#define CVC5__EXPR__PROOF_H
* Proof checker utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__EXPR__PROOF_CHECKER_H
#define CVC5__EXPR__PROOF_CHECKER_H
* 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
* 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
* Proof node utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__EXPR__PROOF_NODE_H
#define CVC5__EXPR__PROOF_NODE_H
* 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
* 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
* 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
* 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
* Proof rule enumeration.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__EXPR__PROOF_RULE_H
#define CVC5__EXPR__PROOF_RULE_H
* Proof set utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__EXPR__PROOF_SET_H
#define CVC5__EXPR__PROOF_SET_H
* 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
* A class representing a Record definition.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__RECORD_H
#define CVC5__RECORD_H
* The sequence data type.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__EXPR__SEQUENCE_H
#define CVC5__EXPR__SEQUENCE_H
* Skolem manager utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__EXPR__SKOLEM_MANAGER_H
#define CVC5__EXPR__SKOLEM_MANAGER_H
*
* 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
* The symbol manager.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__EXPR__SYMBOL_MANAGER_H
#define CVC5__EXPR__SYMBOL_MANAGER_H
* 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
* 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
* 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
* Term context utilities.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__EXPR__TERM_CONTEXT_H
#define CVC5__EXPR__TERM_CONTEXT_H
* 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
* Term context.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__EXPR__TERM_CONTEXT_STACK_H
#define CVC5__EXPR__TERM_CONTEXT_STACK_H
* 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
* A type checker.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
// ordering dependence
#include "expr/node.h"
* 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"
* 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
* Reference-counted encapsulation of a pointer to node information.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
// circular dependency
#include "expr/node_value.h"
* Template for the Type properties header.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__TYPE_PROPERTIES_H
#define CVC5__TYPE_PROPERTIES_H
* Representation of constants of uninterpreted sorts.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__UNINTERPRETED_CONSTANT_H
#define CVC5__UNINTERPRETED_CONSTANT_H
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Mathias Preiner, Morgan Deters, Tim King
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Inclusion of this file marks a header as private and generates a warning
- * when the file is included improperly.
- */
-
-#ifndef CVC5_PRIVATE_H
-#define CVC5_PRIVATE_H
-
-#if ! (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST))
-# error A private CVC4 header was included when not building the library or private unit test code.
-#endif /* ! (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) */
-
-
-#include "cvc4_public.h"
-#include "cvc4autoconfig.h"
-
-#endif /* CVC5_PRIVATE_H */
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Andres Noetzli, Mathias Preiner, Tim King
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Inclusion of this file marks a header as private and generates a warning
- * when the file is included improperly.
- */
-
-#ifndef CVC5_PRIVATE_LIBRARY_H
-#define CVC5_PRIVATE_LIBRARY_H
-
-#if !(defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST) \
- || defined(__BUILDING_CVC4PARSERLIB) \
- || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST) \
- || defined(__BUILDING_CVC4DRIVER))
-# error A "private library" CVC4 header was included when not building the library, driver, or private unit test code.
-#endif /* ! (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST || __BUILDING_CVC4PARSERLIB || __BUILDING_CVC4PARSERLIB_UNIT_TEST || __BUILDING_CVC4DRIVER) */
-
-#include "cvc4_public.h"
-#include "cvc4autoconfig.h"
-
-#endif /* CVC5_PRIVATE_LIBRARY_H */
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Morgan Deters, Mathias Preiner
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Macros that should be defined everywhere during the building of
- * the libraries and driver binary, and also exported to the user.
- */
-
-#ifndef CVC5_PUBLIC_H
-#define CVC5_PUBLIC_H
-
-#include <stddef.h>
-#include <stdint.h>
-
-// CVC5_UNUSED is to mark something (e.g. local variable, function)
-// as being _possibly_ unused, so that the compiler generates no
-// warning about it. This might be the case for e.g. a variable
-// only used in DEBUG builds.
-
-#ifdef __GNUC__
-#define CVC5_UNUSED __attribute__((__unused__))
-#define CVC5_NORETURN __attribute__((__noreturn__))
-#define CVC5_CONST_FUNCTION __attribute__((__const__))
-#define CVC5_PURE_FUNCTION __attribute__((__pure__))
-#define CVC5_WARN_UNUSED_RESULT __attribute__((__warn_unused_result__))
-#else /* ! __GNUC__ */
-#define CVC5_UNUSED
-#define CVC5_NORETURN
-#define CVC5_CONST_FUNCTION
-#define CVC5_PURE_FUNCTION
-#define CVC5_WARN_UNUSED_RESULT
-#endif /* __GNUC__ */
-
-#endif /* CVC5_PUBLIC_H */
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Morgan Deters, Tim King
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Inclusion of this file marks a header as private and generates a warning
- * when the file is included improperly.
- */
-
-#ifndef __CVC4PARSER_PRIVATE_H
-#define __CVC4PARSER_PRIVATE_H
-
-#if ! (defined(__BUILDING_CVC4PARSERLIB) || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST))
-# error A private CVC4 parser header was included when not building the parser library or private unit test code.
-#endif /* ! (__BUILDING_CVC4PARSERLIB || __BUILDING_CVC4PARSERLIB_UNIT_TEST) */
-
-#include "cvc4parser_public.h"
-// It would be nice to #include "cvc4autoconfig.h" here, but there are conflicts
-// with antlr3's autoheader stuff, which they export :(
-//
-// #include "cvc4autoconfig.h"
-
-#endif /* __CVC4PARSER_PRIVATE_H */
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Morgan Deters
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Macros that should be defined everywhere during the building of the
- * libraries and driver binary, and also exported to the user.
- */
-
-#ifndef __CVC4PARSER_PUBLIC_H
-#define __CVC4PARSER_PUBLIC_H
-
-#include "cvc4_public.h"
-
-#endif /* __CVC4PARSER_PUBLIC_H */
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Mathias Preiner, Morgan Deters, Tim King
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Inclusion of this file marks a header as private and generates a warning
+ * when the file is included improperly.
+ */
+
+#ifndef CVC5_PRIVATE_H
+#define CVC5_PRIVATE_H
+
+#if !(defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST))
+# error A private CVC4 header was included when not building the library or private unit test code.
+#endif /* ! (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) */
+
+#include "cvc4autoconfig.h"
+#include "cvc5_public.h"
+
+#endif /* CVC5_PRIVATE_H */
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andres Noetzli, Mathias Preiner, Tim King
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Inclusion of this file marks a header as private and generates a warning
+ * when the file is included improperly.
+ */
+
+#ifndef CVC5_PRIVATE_LIBRARY_H
+#define CVC5_PRIVATE_LIBRARY_H
+
+#if !(defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST) \
+ || defined(__BUILDING_CVC4PARSERLIB) \
+ || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST) \
+ || defined(__BUILDING_CVC4DRIVER))
+# error A "private library" CVC4 header was included when not building the library, driver, or private unit test code.
+#endif /* ! (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST || \
+ __BUILDING_CVC4PARSERLIB || __BUILDING_CVC4PARSERLIB_UNIT_TEST || \
+ __BUILDING_CVC4DRIVER) */
+
+#include "cvc4autoconfig.h"
+#include "cvc5_public.h"
+
+#endif /* CVC5_PRIVATE_LIBRARY_H */
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Morgan Deters, Mathias Preiner
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Macros that should be defined everywhere during the building of
+ * the libraries and driver binary, and also exported to the user.
+ */
+
+#ifndef CVC5_PUBLIC_H
+#define CVC5_PUBLIC_H
+
+#include <stddef.h>
+#include <stdint.h>
+
+// CVC5_UNUSED is to mark something (e.g. local variable, function)
+// as being _possibly_ unused, so that the compiler generates no
+// warning about it. This might be the case for e.g. a variable
+// only used in DEBUG builds.
+
+#ifdef __GNUC__
+#define CVC5_UNUSED __attribute__((__unused__))
+#define CVC5_NORETURN __attribute__((__noreturn__))
+#define CVC5_CONST_FUNCTION __attribute__((__const__))
+#define CVC5_PURE_FUNCTION __attribute__((__pure__))
+#define CVC5_WARN_UNUSED_RESULT __attribute__((__warn_unused_result__))
+#else /* ! __GNUC__ */
+#define CVC5_UNUSED
+#define CVC5_NORETURN
+#define CVC5_CONST_FUNCTION
+#define CVC5_PURE_FUNCTION
+#define CVC5_WARN_UNUSED_RESULT
+#endif /* __GNUC__ */
+
+#endif /* CVC5_PUBLIC_H */
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Morgan Deters, Tim King
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Inclusion of this file marks a header as private and generates a warning
+ * when the file is included improperly.
+ */
+
+#ifndef __CVC4PARSER_PRIVATE_H
+#define __CVC4PARSER_PRIVATE_H
+
+#if !(defined(__BUILDING_CVC4PARSERLIB) \
+ || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST))
+# error A private CVC4 parser header was included when not building the parser library or private unit test code.
+#endif /* ! (__BUILDING_CVC4PARSERLIB || __BUILDING_CVC4PARSERLIB_UNIT_TEST) \
+ */
+
+#include "cvc5parser_public.h"
+// It would be nice to #include "cvc4autoconfig.h" here, but there are conflicts
+// with antlr3's autoheader stuff, which they export :(
+//
+// #include "cvc4autoconfig.h"
+
+#endif /* __CVC4PARSER_PRIVATE_H */
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Morgan Deters
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Macros that should be defined everywhere during the building of the
+ * libraries and driver binary, and also exported to the user.
+ */
+
+#ifndef __CVC4PARSER_PUBLIC_H
+#define __CVC4PARSER_PUBLIC_H
+
+#include "cvc5_public.h"
+
+#endif /* __CVC4PARSER_PUBLIC_H */
* Replacement for clock_gettime() for systems without it (Windows).
*/
-// #warning "TODO(taking): Make lib/clock_gettime.h cvc4_private.h again."
+// #warning "TODO(taking): Make lib/clock_gettime.h cvc5_private.h again."
#include "lib/clock_gettime.h"
* Replacement for clock_gettime() for systems without it (Windows).
*/
-#include "cvc4_private_library.h"
+#include "cvc5_private_library.h"
#ifndef CVC5__LIB__CLOCK_GETTIME_H
#define CVC5__LIB__CLOCK_GETTIME_H
* Replacement for ffs() for systems without it (like Win32).
*/
-#include "cvc4_private.h"
-
#include "lib/ffs.h"
+#include "cvc5_private.h"
+
#ifdef __cplusplus
extern "C" {
#endif /* __cplusplus */
* Replacement for ffs() for systems without it (like Win32).
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__LIB__FFS_H
#define CVC5__LIB__FFS_H
#define CVC5__LIB__REPLACEMENTS_H
#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT)
-# include "cvc4_private.h"
+#include "cvc5_private.h"
#else
# if defined(__BUILDING_CVC4PARSERLIB) || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST)
-# include "cvc4parser_private.h"
+#include "cvc5parser_private.h"
# else
#if defined(__BUILDING_CVC4DRIVER) || defined(__BUILDING_CVC5_SYSTEM_TEST) \
|| defined(__BUILDING_STATISTICS_FOR_EXPORT)
* Replacement for strtok_r() for systems without it (like Win32).
*/
-#include "cvc4_private.h"
-
#include "lib/strtok_r.h"
+
#include <stdio.h>
#include <string.h>
+#include "cvc5_private.h"
#ifdef __cplusplus
extern "C" {
* Replacement for strtok_r() for systems without it (like Win32).
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__LIB__STRTOK_R_H
#define CVC5__LIB__STRTOK_R_H
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__BASE_HANDLERS_H
#define CVC5__BASE_HANDLERS_H
* Rewriter attributes.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__OPTIONS__DECISION_WEIGHT_H
#define CVC5__OPTIONS__DECISION_WEIGHT_H
* Definition of input and output languages.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__LANGUAGE_H
#define CVC5__LANGUAGE_H
* expands this template and generates a <module>_options.h file.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__OPTIONS__${id}$_H
#define CVC5__OPTIONS__${id}$_H
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__OPEN_OSTREAM_H
#define CVC5__OPEN_OSTREAM_H
* Options-related exceptions.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__OPTION_EXCEPTION_H
#define CVC5__OPTION_EXCEPTION_H
* Global (command-line, set-option, ...) parameters for SMT.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__OPTIONS__OPTIONS_H
#define CVC5__OPTIONS__OPTIONS_H
* Interface for custom handlers and predicates options.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__OPTIONS__OPTIONS_HANDLER_H
#define CVC5__OPTIONS__OPTIONS_HANDLER_H
* Global (command-line, set-option, ...) parameters for SMT.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__OPTIONS__OPTIONS_HOLDER_H
#define CVC5__OPTIONS__OPTIONS_HOLDER_H
* Base class for option listener.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__OPTIONS__OPTIONS_LISTENER_H
#define CVC5__OPTIONS__OPTIONS_LISTENER_H
* \todo document this file
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__PRINTER__MODES_H
#define CVC5__PRINTER__MODES_H
* Definition of input and output languages.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__OPTIONS__SET_LANGUAGE_H
#define CVC5__OPTIONS__SET_LANGUAGE_H
#include "base/check.h"
#include "base/output.h"
-#include "cvc4parser_private.h"
+#include "cvc5parser_private.h"
#include "parser/bounded_token_buffer.h"
#include "parser/input.h"
#include "parser/line_buffer.h"
* achieve that and stores the lines received so far in a LineBuffer.
*/
-#include "cvc4parser_private.h"
+#include "cvc5parser_private.h"
#ifndef CVC5__PARSER__ANTLR_LINE_BUFFERED_INPUT_H
#define CVC5__PARSER__ANTLR_LINE_BUFFERED_INPUT_H
* "hidden".
*/
-#include "cvc4parser_private.h"
+#include "cvc5parser_private.h"
#ifndef CVC5__PARSER__BOUNDED_TOKEN_BUFFER_H
#define CVC5__PARSER__BOUNDED_TOKEN_BUFFER_H
* tokens will be bounded (e.g., if you're using a bounded token stream).
*/
-#include "cvc4parser_private.h"
+#include "cvc5parser_private.h"
#ifndef CVC5__PARSER__BOUNDED_TOKEN_FACTORY_H
#define CVC5__PARSER__BOUNDED_TOKEN_FACTORY_H
* The parser class for the CVC language.
*/
-#include "cvc4parser_private.h"
+#include "cvc5parser_private.h"
#ifndef CVC5__PARSER__CVC_H
#define CVC5__PARSER__CVC_H
* [[ Add lengthier description here ]]
*/
-#include "cvc4parser_private.h"
+#include "cvc5parser_private.h"
#ifndef CVC5__PARSER__CVC_INPUT_H
#define CVC5__PARSER__CVC_INPUT_H
* Base for parser inputs.
*/
-#include "cvc4parser_public.h"
+#include "cvc5parser_public.h"
#ifndef CVC5__PARSER__INPUT_H
#define CVC5__PARSER__INPUT_H
* within the line.
*/
-#include "cvc4parser_private.h"
+#include "cvc5parser_private.h"
#ifndef CVC5__PARSER__LINE_BUFFER_H
#define CVC5__PARSER__LINE_BUFFER_H
* ANTLR input buffer from a memory-mapped file.
*/
-#include "cvc4parser_private.h"
+#include "cvc5parser_private.h"
#ifndef CVC5__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H
#define CVC5__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H
* Definitions of parsed operators.
*/
-#include "cvc4parser_public.h"
+#include "cvc5parser_public.h"
#ifndef CVC5__PARSER__PARSE_OP_H
#define CVC5__PARSER__PARSE_OP_H
* A collection of state for use by parser implementations.
*/
-#include "cvc4parser_public.h"
+#include "cvc5parser_public.h"
#ifndef CVC5__PARSER__PARSER_H
#define CVC5__PARSER__PARSER_H
* A builder for parsers.
*/
-#include "cvc4parser_public.h"
+#include "cvc5parser_public.h"
#ifndef CVC5__PARSER__PARSER_BUILDER_H
#define CVC5__PARSER__PARSER_BUILDER_H
* Exception class for parse errors.
*/
-#include "cvc4parser_public.h"
+#include "cvc5parser_public.h"
#ifndef CVC5__PARSER__PARSER_EXCEPTION_H
#define CVC5__PARSER__PARSER_EXCEPTION_H
* Definitions of SMT2 constants.
*/
-#include "cvc4parser_private.h"
+#include "cvc5parser_private.h"
#ifndef CVC5__PARSER__SMT2_H
#define CVC5__PARSER__SMT2_H
* [[ Add file-specific comments here ]]
*/
-#include "cvc4parser_private.h"
+#include "cvc5parser_private.h"
#ifndef CVC5__PARSER__SMT2_INPUT_H
#define CVC5__PARSER__SMT2_INPUT_H
* [[ Add file-specific comments here ]]
*/
-#include "cvc4parser_private.h"
+#include "cvc5parser_private.h"
#ifndef CVC5__PARSER__SYGUS_INPUT_H
#define CVC5__PARSER__SYGUS_INPUT_H
* Definition of TPTP parser.
*/
-#include "parser/antlr_input.h" // Needs to go first.
-
-#include "cvc4parser_private.h"
+#include "cvc5parser_private.h"
+#include "parser/antlr_input.h" // Needs to go first.
#ifndef CVC5__PARSER__TPTP_H
#define CVC5__PARSER__TPTP_H
* [[ Add file-specific comments here ]]
*/
-#include "cvc4parser_private.h"
+#include "cvc5parser_private.h"
#ifndef CVC5__PARSER__TPTP_INPUT_H
#define CVC5__PARSER__TPTP_INPUT_H
* preprocessing passes.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PREPROCESSING__ASSERTION_PIPELINE_H
#define CVC5__PREPROCESSING__ASSERTION_PIPELINE_H
* 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
* assertions.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PREPROCESSING__PASSES__APPLY_SUBSTS_H
#define CVC5__PREPROCESSING__PASSES__APPLY_SUBSTS_H
*
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PREPROCESSING__PASSES__BOOL_TO_BV_H
#define CVC5__PREPROCESSING__PASSES__BOOL_TO_BV_H
* 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
* 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
* 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
* 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
* 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
*
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef __CVC5__PREPROCESSING__PASSES__BV_TO_INT_H
#define __CVC5__PREPROCESSING__PASSES__BV_TO_INT_H
* 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
* 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
* 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
* 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
* 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
* 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
* 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
* 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
* 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
* 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
* \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
* 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
* 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
* 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
* 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
* 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
* 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
* 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
* 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
* 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
* 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
* do work that only needs to be done once.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PREPROCESSING__PREPROCESSING_PASS_H
#define CVC5__PREPROCESSING__PREPROCESSING_PASS_H
* from the solver and interact with it without getting full access.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
#define CVC5__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
* This file defines the classes PreprocessingPassRegistry, which keeps track
* of the available preprocessing passes.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H
#define CVC5__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H
*'96
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__ITE_UTILITIES_H
#define CVC5__ITE_UTILITIES_H
* The pretty-printer interface for the AST output language.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PRINTER__AST_PRINTER_H
#define CVC5__PRINTER__AST_PRINTER_H
* The pretty-printer interface for the CVC output language.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PRINTER__CVC_PRINTER_H
#define CVC5__PRINTER__CVC_PRINTER_H
* A let binding.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PRINTER__LET_BINDING_H
#define CVC5__PRINTER__LET_BINDING_H
* Base of the pretty-printer interface.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PRINTER__PRINTER_H
#define CVC5__PRINTER__PRINTER_H
* The pretty-printer interface for the SMT2 output language.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PRINTER__SMT2_PRINTER_H
#define CVC5__PRINTER__SMT2_PRINTER_H
* The pretty-printer interface for the TPTP output language.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PRINTER__TPTP_PRINTER_H
#define CVC5__PRINTER__TPTP_PRINTER_H
* solver for a clause.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PROOF__CLAUSE_ID_H
#define CVC5__PROOF__CLAUSE_ID_H
* A manager for CnfProofs.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__CNF_PROOF_H
#define CVC5__CNF_PROOF_H
* The module for printing dot proofs.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PROOF__DOT__DOT_PRINTER_H
#define CVC5__PROOF__DOT__DOT_PRINTER_H
* A manager for Proofs.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PROOF_MANAGER_H
#define CVC5__PROOF_MANAGER_H
* Resolution proof.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SAT__PROOF_H
#define CVC5__SAT__PROOF_H
* Resolution proof.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SAT__PROOF_IMPLEMENTATION_H
#define CVC5__SAT__PROOF_IMPLEMENTATION_H
* Representation of unsat cores.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__UNSAT_CORE_H
#define CVC5__UNSAT_CORE_H
* solver.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PROP__BVSATSOLVERNOTIFY_H
#define CVC5__PROP__BVSATSOLVERNOTIFY_H
* Implementation of the minisat for cvc4 (bit-vectors).
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* Implementation of the CaDiCaL SAT solver for CVC4 (bit-vectors).
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PROP__CADICAL_H
#define CVC5__PROP__CADICAL_H
* internals such as the representation and translation of [??? -Chris]
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PROP__CNF_STREAM_H
#define CVC5__PROP__CNF_STREAM_H
* Implementation of the cryptominisat sat solver for cvc4 (bit-vectors).
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PROP__CRYPTOMINISAT_H
#define CVC5__PROP__CRYPTOMINISAT_H
* Wrapper for the Kissat SAT solver (for theory of bit-vectors).
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PROP__KISSAT_H
#define CVC5__PROP__KISSAT_H
#include "base/check.h"
#include "base/output.h"
#include "context/context.h"
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#include "expr/proof_node_manager.h"
#include "proof/clause_id.h"
#include "prop/minisat/core/SolverTypes.h"
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef Minisat_SolverTypes_h
#define Minisat_SolverTypes_h
#define Minisat_SimpSolver_h
#include "base/check.h"
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#include "proof/clause_id.h"
#include "prop/minisat/core/Solver.h"
#include "prop/minisat/mtl/Queue.h"
* The proof-producing CNF stream.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PROP__PROOF_CNF_STREAM_H
#define CVC5__PROP__PROOF_CNF_STREAM_H
* The module for processing proof nodes in the prop engine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PROP__PROOF_POST_PROCESSOR_H
#define CVC5__PROP__PROOF_POST_PROCESSOR_H
* Main interface point between cvc5's SMT infrastructure and the SAT solver.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PROP_ENGINE_H
#define CVC5__PROP_ENGINE_H
* The proof manager of PropEngine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PROP_PROOF_MANAGER_H
#define CVC5__PROP_PROOF_MANAGER_H
* TheoryEngine class directly.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PROP__REGISTRAR_H
#define CVC5__PROP__REGISTRAR_H
* The proof manager for Minisat.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SAT_PROOF_MANAGER_H
#define CVC5__SAT_PROOF_MANAGER_H
* SAT Solver.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PROP__SAT_SOLVER_H
#define CVC5__PROP__SAT_SOLVER_H
* SAT Solver creation facility
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PROP__SAT_SOLVER_FACTORY_H
#define CVC5__PROP__SAT_SOLVER_FACTORY_H
#pragma once
-#include "cvc4_private.h"
-
#include <sstream>
#include <string>
#include <unordered_set>
#include <vector>
+#include "cvc5_private.h"
+
namespace cvc5 {
namespace prop {
* Skolem definition manager.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PROP__SKOLEM_DEF_MANAGER_H
#define CVC5__PROP__SKOLEM_DEF_MANAGER_H
* SAT Solver.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__PROP__SAT_H
#define CVC5__PROP__SAT_H
* The solver for abduction queries.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__ABDUCTION_SOLVER_H
#define CVC5__SMT__ABDUCTION_SOLVER_H
* Utility for constructing and maintaining abstract values.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__ABSTRACT_VALUES_H
#define CVC5__SMT__ABSTRACT_VALUES_H
* The module for storing assertions for an SMT engine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__ASSERTIONS_H
#define CVC5__SMT__ASSERTIONS_H
* Utility for checking models.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__CHECK_MODELS_H
#define CVC5__SMT__CHECK_MODELS_H
* code.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__COMMAND_H
#define CVC5__COMMAND_H
* Defined function data structure.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__DEFINED_FUNCTION_H
#define CVC5__SMT__DEFINED_FUNCTION_H
* Dump utility classes and functions.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__DUMP_H
#define CVC5__DUMP_H
* The dump manager of the SmtEngine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__DUMP_MANAGER_H
#define CVC5__SMT__DUMP_MANAGER_H
* internal code
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__SMT__ENV_H
#define CVC5__SMT__ENV_H
* The module for processing assertions for an SMT engine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__EXPAND_DEFINITIONS_H
#define CVC5__SMT__EXPAND_DEFINITIONS_H
* The solver for interpolation queries.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__INTERPOLATION_SOLVER_H
#define CVC5__SMT__INTERPOLATION_SOLVER_H
* Listener classes for SMT engine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__LISTENERS_H
#define CVC5__SMT__LISTENERS_H
* is used while running in a quantifier-free logic).
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__SMT__LOGIC_EXCEPTION_H
#define CVC5__SMT__LOGIC_EXCEPTION_H
* related to ostreams.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__MANAGED_OSTREAMS_H
#define CVC5__MANAGED_OSTREAMS_H
* Model class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__MODEL_H
#define CVC5__MODEL_H
* Utility for blocking the current model.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef __CVC5__THEORY__MODEL_BLOCKER_H
#define __CVC5__THEORY__MODEL_BLOCKER_H
* Utility for building model cores.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__MODEL_CORE_BUILDER_H
#define CVC5__THEORY__MODEL_CORE_BUILDER_H
* Datastructures used for printing commands internally.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__NODE_COMMAND_H
#define CVC5__SMT__NODE_COMMAND_H
* The solver for optimization queries.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__OPTIMIZATION_SOLVER_H
#define CVC5__SMT__OPTIMIZATION_SOLVER_H
* The module for proofs for preprocessing in an SMT engine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__PREPROCESS_PROOF_GENERATOR_H
#define CVC5__SMT__PREPROCESS_PROOF_GENERATOR_H
* The preprocessor of the SmtEngine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__PREPROCESSOR_H
#define CVC5__SMT__PREPROCESSOR_H
* The module for processing assertions for an SMT engine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__PROCESS_ASSERTIONS_H
#define CVC5__SMT__PROCESS_ASSERTIONS_H
* The proof manager of SmtEngine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__PROOF_MANAGER_H
#define CVC5__SMT__PROOF_MANAGER_H
* The module for processing proof nodes.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__PROOF_POST_PROCESSOR_H
#define CVC5__SMT__PROOF_POST_PROCESSOR_H
* The solver for quantifier elimination queries.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__QUANT_ELIM_SOLVER_H
#define CVC5__SMT__QUANT_ELIM_SOLVER_H
* SmtEngine: the main public entry point of libcvc5.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__SMT_ENGINE_H
#define CVC5__SMT_ENGINE_H
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__SMT_ENGINE_SCOPE_H
#define CVC5__SMT__SMT_ENGINE_SCOPE_H
* Utility for maintaining the state of the SMT engine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__SMT_ENGINE_STATE_H
#define CVC5__SMT__SMT_ENGINE_STATE_H
* Statistics for SMT engine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__SMT_ENGINE_STATS_H
#define CVC5__SMT__SMT_ENGINE_STATS_H
* Enumeration type for the mode of an SmtEngine.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__SMT__SMT_MODE_H
#define CVC5__SMT__SMT_MODE_H
* The solver for SMT queries in an SmtEngine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__SMT_SOLVER_H
#define CVC5__SMT__SMT_SOLVER_H
* Accessor for the SmtEngine's StatisticsRegistry.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* The solver for SyGuS queries.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__SYGUS_SOLVER_H
#define CVC5__SMT__SYGUS_SOLVER_H
* Removal of term formulas.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* The unsat core manager of SmtEngine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__UNSAT_CORE_MANAGER_H
#define CVC5__SMT__UNSAT_CORE_MANAGER_H
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__UPDATE_OSTREAM_H
#define CVC5__UPDATE_OSTREAM_H
* The module for managing witness form conversion in proofs.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SMT__WITNESS_FORM_H
#define CVC5__SMT__WITNESS_FORM_H
* Simple, commonly-used routines for Boolean simplification.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__BOOLEAN_SIMPLIFICATION_H
#define CVC5__BOOLEAN_SIMPLIFICATION_H
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
#include <vector>
// Pass 1: label the ite as (constant) or (+ constant variable)
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARITH__ARITH_ITE_UTILS_H
#define CVC5__THEORY__ARITH__ARITH_ITE_UTILS_H
* Arithmetic utilities regarding monomial sums.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARITH__MSUM_H
#define CVC5__THEORY__ARITH__MSUM_H
* Arithmetic preprocess.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARITH__ARITH_PREPROCESS_H
#define CVC5__THEORY__ARITH__ARITH_PREPROCESS_H
* See theory/arith/normal_form.h for more information.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARITH__ARITH_REWRITER_H
#define CVC5__THEORY__ARITH__ARITH_REWRITER_H
* Arithmetic theory state.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARITH__ARITH_STATE_H
#define CVC5__THEORY__ARITH__ARITH_STATE_H
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARITH__ARITH_STATIC_LEARNER_H
#define CVC5__THEORY__ARITH__ARITH_STATIC_LEARNER_H
* Common functions for dealing with nodes.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARITH__ARITH_UTILITIES_H
#define CVC5__THEORY__ARITH__ARITH_UTILITIES_H
* This file also provides utilities for ArithVars.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARITH__ARITHVAR_NODE_MAP_H
#define CVC5__THEORY__ARITH__ARITHVAR_NODE_MAP_H
* These are theory valid and are currently turned into lemmas
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
#include "base/check.h"
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* proof.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARITH__CONSTRAINT_H
#define CVC5__THEORY__ARITH__CONSTRAINT_H
#ifndef CVC5__THEORY__ARITH__CONSTRAINT_FORWARD_H
#define CVC5__THEORY__ARITH__CONSTRAINT_FORWARD_H
-#include "cvc4_private.h"
#include <vector>
+#include "cvc5_private.h"
+
namespace cvc5 {
namespace theory {
namespace arith {
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* A Diophantine equation solver for the theory of arithmetic.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARITH__DIO_SOLVER_H
#define CVC5__THEORY__ARITH__DIO_SOLVER_H
* These are theory valid and are currently turned into lemmas
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* These are theory valid and are currently turned into lemmas
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* Customized inference manager for the theory of nonlinear arithmetic.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARITH__INFERENCE_MANAGER_H
#define CVC5__THEORY__ARITH__INFERENCE_MANAGER_H
* using both the Tableau and PartialModel.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* This defines Matrix<T>, IntegerEqualityTables and Tableau.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* 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
* 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
* 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
* 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
* 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
* 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
* 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
* 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
#include <cmath>
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#include "theory/arith/nl/nl_model.h"
#include "theory/rewriter.h"
#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>
#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>
#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
#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>
#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
* 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
* 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
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARITH__NORMAL_FORM_H
#define CVC5__THEORY__ARITH__NORMAL_FORM_H
* and information derived from these.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARITH__PARTIAL_MODEL_H
#define CVC5__THEORY__ARITH__PARTIAL_MODEL_H
* Arithmetic proof checker utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARITH__PROOF_CHECKER_H
#define CVC5__THEORY__ARITH__PROOF_CHECKER_H
* or unsat cores are enabled.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARITH__PROOF_MACROS_H
#define CVC5__THEORY__ARITH__PROOF_MACROS_H
* Type for rewrites for arithmetic.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARITH__REWRITES_H
#define CVC5__THEORY__ARITH__REWRITES_H
* These are theory valid and are currently turned into lemmas
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* using both the Tableau and PartialModel.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* These are theory valid and are currently turned into lemmas
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* Arithmetic theory.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* [[ Add file-specific comments here ]]
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
#define CVC5__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
* Enumerators for rationals and integers.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARITH__TYPE_ENUMERATOR_H
#define CVC5__THEORY__ARITH__TYPE_ENUMERATOR_H
* for each term of type array.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARRAYS__ARRAY_INFO_H
#define CVC5__THEORY__ARRAYS__ARRAY_INFO_H
* Arrays inference manager.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARRAYS__INFERENCE_MANAGER_H
#define CVC5__THEORY__ARRAYS__INFERENCE_MANAGER_H
* Array proof checker utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARRAYS__PROOF_CHECKER_H
#define CVC5__THEORY__ARRAYS__PROOF_CHECKER_H
* Arrays skolem cache.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARRAYS__SKOLEM_CACHE_H
#define CVC5__THEORY__ARRAYS__SKOLEM_CACHE_H
* Theory of arrays.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARRAYS__THEORY_ARRAYS_H
#define CVC5__THEORY__ARRAYS__THEORY_ARRAYS_H
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
#define CVC5__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
* Typing and cardinality rules for the theory of arrays.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
#define CVC5__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
* An enumerator for arrays.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H
#define CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H
* stack. Refactored from the UF union-find.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARRAYS__UNION_FIND_H
#define CVC5__THEORY__ARRAYS__UNION_FIND_H
* The representation of the assertions sent to theories.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ASSERTION_H
#define CVC5__THEORY__ASSERTION_H
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* Solver for the theory of bags.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BAG__SOLVER_H
#define CVC5__THEORY__BAG__SOLVER_H
* Bags theory rewriter.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BAGS__THEORY_BAGS_REWRITER_H
#define CVC5__THEORY__BAGS__THEORY_BAGS_REWRITER_H
* Statistics for the theory of bags.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BAGS_STATISTICS_H
#define CVC5__THEORY__BAGS_STATISTICS_H
* Inference information utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BAGS__INFER_INFO_H
#define CVC5__THEORY__BAGS__INFER_INFO_H
* Inference generator utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BAGS__INFERENCE_GENERATOR_H
#define CVC5__THEORY__BAGS__INFERENCE_GENERATOR_H
* The inference manager for the theory of bags.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BAGS__INFERENCE_MANAGER_H
#define CVC5__THEORY__BAGS__INFERENCE_MANAGER_H
* A class for MK_BAG operator.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__MAKE_BAG_OP_H
#define CVC5__MAKE_BAG_OP_H
#include <expr/node.h>
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BAGS__NORMAL_FORM_H
#define CVC5__THEORY__BAGS__NORMAL_FORM_H
* Type for rewrites for bags.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BAGS__REWRITES_H
#define CVC5__THEORY__BAGS__REWRITES_H
* Bags state object.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BAGS__THEORY_SOLVER_STATE_H
#define CVC5__THEORY__BAGS__THEORY_SOLVER_STATE_H
* Bags state object.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BAGS__TERM_REGISTRY_H
#define CVC5__THEORY__BAGS__TERM_REGISTRY_H
* Bags theory.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BAGS__THEORY_BAGS_H
#define CVC5__THEORY__BAGS__THEORY_BAGS_H
* Type enumerator for bags
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BAGS__TYPE_ENUMERATOR_H
#define CVC5__THEORY__BAGS__TYPE_ENUMERATOR_H
* Bags theory type rules.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H
#define CVC5__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H
* A non-clausal circuit propagator for Boolean simplification.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
#define CVC5__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
* Boolean proof checker utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BOOLEANS__PROOF_CHECKER_H
#define CVC5__THEORY__BOOLEANS__PROOF_CHECKER_H
* Proofs for the non-clausal circuit propagator.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BOOLEANS__PROOF_CIRCUIT_PROPAGATOR_H
#define CVC5__THEORY__BOOLEANS__PROOF_CIRCUIT_PROPAGATOR_H
* The theory of booleans.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BOOLEANS__THEORY_BOOL_H
#define CVC5__THEORY__BOOLEANS__THEORY_BOOL_H
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H
#define CVC5__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H
* [[ Add file-specific comments here ]]
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY_BOOL_TYPE_RULES_H
#define CVC5__THEORY_BOOL_TYPE_RULES_H
* An enumerator for Booleans.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BOOLEANS__TYPE_ENUMERATOR_H
#define CVC5__THEORY__BOOLEANS__TYPE_ENUMERATOR_H
* Equality proof checker utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BUILTIN__PROOF_CHECKER_H
#define CVC5__THEORY__BUILTIN__PROOF_CHECKER_H
* Built-in theory.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BUILTIN__THEORY_BUILTIN_H
#define CVC5__THEORY__BUILTIN__THEORY_BUILTIN_H
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
#define CVC5__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
* Type rules for the builtin theory.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H
#define CVC5__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H
* Enumerator for uninterpreted sorts and functions.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BUILTIN__TYPE_ENUMERATOR_H
#define CVC5__THEORY__BUILTIN__TYPE_ENUMERATOR_H
* Bitvector theory.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__ABSTRACTION_H
#define CVC5__THEORY__BV__ABSTRACTION_H
#include "theory/bv/bitblast/aig_bitblaster.h"
#include "base/check.h"
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#include "options/bv_options.h"
#include "prop/cnf_stream.h"
#include "prop/sat_solver.h"
* AIG Bitblaster based on ABC.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
#define CVC5__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
* Implementation of bitblasting functions for various operators.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
#define CVC5__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
* Various utility functions for bit-blasting.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
#define CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
* Wrapper around the SAT solver used for bitblasting.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__BITBLAST__BITBLASTER_H
#define CVC5__THEORY__BV__BITBLAST__BITBLASTER_H
#include "theory/bv/bitblast/eager_bitblaster.h"
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#include "options/bv_options.h"
#include "options/smt_options.h"
#include "prop/cnf_stream.h"
* Bitblaster for the eager BV solver.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
#define CVC5__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
#include "theory/bv/bitblast/lazy_bitblaster.h"
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#include "options/bv_options.h"
#include "prop/cnf_stream.h"
#include "prop/sat_solver.h"
* Bitblaster for the lazy bv solver.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
#define CVC5__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
*
* A bit-blaster wrapper around BBSimple for proof logging.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H
#define CVC5__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H
*
* Bitblaster for simple BV solver.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H
#define CVC5__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H
* Eager bit-blasting solver.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__BV_EAGER_SOLVER_H
#define CVC5__THEORY__BV__BV_EAGER_SOLVER_H
* Algebraic solver.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__BV_INEQUALITY__GRAPH_H
#define CVC5__THEORY__BV__BV_INEQUALITY__GRAPH_H
* Sandboxed SAT solver for bv quickchecks.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__BV_QUICK_CHECK_H
#define CVC5__BV_QUICK_CHECK_H
* Describes the interface for the internal bit-vector solver of TheoryBV.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__BV_SOLVER_H
#define CVC5__THEORY__BV__BV_SOLVER_H
* Bit-blasting solver that supports multiple SAT back ends.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__BV_SOLVER_BITBLAST_H
#define CVC5__THEORY__BV__BV_SOLVER_BITBLAST_H
* Lazy bit-vector solver.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__BV_SOLVER_LAZY_H
#define CVC5__THEORY__BV__BV_SOLVER_LAZY_H
* Simple bit-blast solver that sends bit-blast lemmas directly to MiniSat.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__BV_SOLVER_SIMPLE_H
#define CVC5__THEORY__BV__BV_SOLVER_SIMPLE_H
#ifndef CVC5__THEORY__BV__BV_SUBTHEORY_H
#define CVC5__THEORY__BV__BV_SUBTHEORY_H
-#include "cvc4_private.h"
-#include "context/context.h"
#include "context/cdqueue.h"
-#include "theory/uf/equality_engine.h"
+#include "context/context.h"
+#include "cvc5_private.h"
#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
namespace cvc5 {
* Algebraic solver.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* Algebraic solver.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* Algebraic solver.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* Algebraic solver.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
#define CVC5__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
* A translation utility from bit-vectors to integers.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef __CVC5__THEORY__BV__INT_BLASTER__H
#define __CVC5__THEORY__BV__INT_BLASTER__H
* Bit-Vector proof checker utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__PROOF_CHECKER_H
#define CVC5__THEORY__BV__PROOF_CHECKER_H
* Bitvector theory.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__SLICER_BV_H
#define CVC5__THEORY__BV__SLICER_BV_H
* Theory of bit-vectors.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__THEORY_BV_H
#define CVC5__THEORY__BV__THEORY_BV_H
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__THEORY_BV_REWRITER_H
#define CVC5__THEORY__BV__THEORY_BV_REWRITER_H
* Bitvector theory typing rules.
*/
-#include "cvc4_private.h"
-
#include <algorithm>
+#include "cvc5_private.h"
+
#ifndef CVC5__THEORY__BV__THEORY_BV_TYPE_RULES_H
#define CVC5__THEORY__BV__THEORY_BV_TYPE_RULES_H
* Util functions for theory BV.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* An enumerator for bitvectors.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__TYPE_ENUMERATOR_H
#define CVC5__THEORY__BV__TYPE_ENUMERATOR_H
* The care graph datastructure.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__CARE_GRAPH_H
#define CVC5__THEORY__CARE_GRAPH_H
* Management of a care graph based approach for theory combination.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__COMBINATION_CARE_GRAPH__H
#define CVC5__THEORY__COMBINATION_CARE_GRAPH__H
* Abstract interface for theory combination.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__COMBINATION_ENGINE__H
#define CVC5__THEORY__COMBINATION_ENGINE__H
* Rewriter for the theory of (co)inductive datatypes.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__DATATYPES__DATATYPES_REWRITER_H
#define CVC5__THEORY__DATATYPES__DATATYPES_REWRITER_H
* Inference to proof conversion for datatypes.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__DATATYPES__INFER_PROOF_CONS_H
#define CVC5__THEORY__DATATYPES__INFER_PROOF_CONS_H
* Datatypes inference.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__DATATYPES__INFERENCE_H
#define CVC5__THEORY__DATATYPES__INFERENCE_H
* Datatypes inference manager.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__DATATYPES__INFERENCE_MANAGER_H
#define CVC5__THEORY__DATATYPES__INFERENCE_MANAGER_H
* Datatypes proof checker utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__DATATYPES__PROOF_CHECKER_H
#define CVC5__THEORY__DATATYPES__PROOF_CHECKER_H
* Util functions for sygus datatypes.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__SYGUS_DATATYPE_UTILS_H
#define CVC5__THEORY__STRINGS__SYGUS_DATATYPE_UTILS_H
* The sygus extension of the theory of datatypes.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__DATATYPES__SYGUS_EXTENSION_H
#define CVC5__THEORY__DATATYPES__SYGUS_EXTENSION_H
* Simple symmetry breaking for sygus.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H
#define CVC5__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H
* Theory of datatypes.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__DATATYPES__THEORY_DATATYPES_H
#define CVC5__THEORY__DATATYPES__THEORY_DATATYPES_H
* Theory of datatypes.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
#define CVC5__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
* Util functions for theory datatypes.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__THEORY_DATATYPES_UTILS_H
#define CVC5__THEORY__STRINGS__THEORY_DATATYPES_UTILS_H
* A class for TupleProjectOp operator.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__PROJECT_OP_H
#define CVC5__PROJECT_OP_H
* An enumerator for datatypes.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__DATATYPES__TYPE_ENUMERATOR_H
#define CVC5__THEORY__DATATYPES__TYPE_ENUMERATOR_H
* theory solvers within TheoryEngine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__DECISION_MANAGER__H
#define CVC5__THEORY__DECISION_MANAGER__H
* for use in the DecisionManager of TheoryEngine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__DECISION_STRATEGY__H
#define CVC5__THEORY__DECISION_STRATEGY__H
* The eager proof generator class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__EAGER_PROOF_GENERATOR_H
#define CVC5__THEORY__EAGER_PROOF_GENERATOR_H
* Utilities for management of equality engines.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__EE_MANAGER__H
#define CVC5__THEORY__EE_MANAGER__H
* all theories.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__EE_MANAGER_DISTRIBUTED__H
#define CVC5__THEORY__EE_MANAGER_DISTRIBUTED__H
* Setup information for an equality engine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__EE_SETUP_INFO__H
#define CVC5__THEORY__EE_SETUP_INFO__H
* The theory engine output channel.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__ENGINE_OUTPUT_CHANNEL_H
#define CVC5__THEORY__ENGINE_OUTPUT_CHANNEL_H
* quickly, without going through the rewriter.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__EVALUATOR_H
#define CVC5__THEORY__EVALUATOR_H
* x = "A" ^ str.contains( str.++( x, z ), "B" ) => str.contains( z, "B" )
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__EXT_THEORY_H
#define CVC5__THEORY__EXT_THEORY_H
* !!! This header is not to be included in any other headers !!!
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__FP__FP_CONVERTER_H
#define CVC5__THEORY__FP__FP_CONVERTER_H
* Theory of floating-point arithmetic.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__FP__THEORY_FP_H
#define CVC5__THEORY__FP__THEORY_FP_H
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__FP__THEORY_FP_REWRITER_H
#define CVC5__THEORY__FP__THEORY_FP_REWRITER_H
* Type rules for the theory of floating-point arithmetic.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__FP__THEORY_FP_TYPE_RULES_H
#define CVC5__THEORY__FP__THEORY_FP_TYPE_RULES_H
* An enumerator for floating-point numbers.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__FP__TYPE_ENUMERATOR_H
#define CVC5__THEORY__FP__TYPE_ENUMERATOR_H
* Incompleteness enumeration.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__INCOMPLETE_ID_H
#define CVC5__THEORY__INCOMPLETE_ID_H
* Inference enumeration.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__INFERENCE_ID_H
#define CVC5__THEORY__INFERENCE_ID_H
* A buffered inference manager.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__INFERENCE_MANAGER_BUFFERED_H
#define CVC5__THEORY__INFERENCE_MANAGER_BUFFERED_H
* proper management of CVC4 components.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__INTERRUPTED_H
#define CVC5__THEORY__INTERRUPTED_H
* The lazy tree proof generator class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__LAZY_TREE_PROOF_GENERATOR_H
#define CVC5__THEORY__LAZY_TREE_PROOF_GENERATOR_H
* configuration information).
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__LOGIC_INFO_H
#define CVC5__LOGIC_INFO_H
* Abstract management of models for TheoryEngine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__MODEL_MANAGER__H
#define CVC5__THEORY__MODEL_MANAGER__H
* Management of a distributed approach for model generation.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__MODEL_MANAGER_DISTRIBUTED__H
#define CVC5__THEORY__MODEL_MANAGER_DISTRIBUTED__H
* The theory output channel interface.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__OUTPUT_CHANNEL_H
#define CVC5__THEORY__OUTPUT_CHANNEL_H
* Alpha equivalence checking.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__ALPHA_EQUIVALENCE_H
#define CVC5__ALPHA_EQUIVALENCE_H
* Inverse rules for bit-vector operators.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__BV_INVERTER_H
#define CVC5__BV_INVERTER_H
* Inverse rules for bit-vector operators.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__BV_INVERTER_UTILS_H
#define CVC5__BV_INVERTER_UTILS_H
* candidate_rewrite_database
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
#define CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
* filtering based on congruence, variable ordering, and matching.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H
#define CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H
* Arithmetic instantiator.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H
#define CVC5__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H
* ceg_bv_instantiator
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H
#define CVC5__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H
* Implementation of ceg_bv_instantiator.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__BV_INSTANTIATOR_UTILS_H
#define CVC5__BV_INSTANTIATOR_UTILS_H
* ceg_dt_instantiator
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H
#define CVC5__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H
* Counterexample-guided quantifier instantiation.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
#define CVC5__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
* Counterexample-guided quantifier instantiation.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
#define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
* based on nested quantifier elimination.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H
#define CVC5__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H
* Virtual term substitution term cache.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H
#define CVC5__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H
* conjecture generator class
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CONJECTURE_GENERATOR_H
#define CONJECTURE_GENERATOR_H
* dynamic_rewriter
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
#define CVC5__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
* Theory uf candidate generator.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
#define CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
* Higher-order trigger class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__HO_TRIGGER_H
#define CVC5__THEORY__QUANTIFIERS__HO_TRIGGER_H
* Inst match generator base class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__IM_GENERATOR_H
#define CVC5__THEORY__QUANTIFIERS__IM_GENERATOR_H
* Inst match generator class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
* multi inst match generator class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_H
#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_H
* Multi-linear inst match generator class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H
#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H
* Simple inst match generator class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H
#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H
* Instantiation engine strategy base class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_H
#define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_H
* E-matching instantiation strategies.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__INST_STRATEGY_E_MATCHING_H
#define CVC5__INST_STRATEGY_E_MATCHING_H
* The user-provided E-matching instantiation strategy.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__INST_STRATEGY_E_MATCHING_USER_H
#define CVC5__INST_STRATEGY_E_MATCHING_USER_H
* Instantiation Engine classes.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
#define CVC5__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
* Pattern term selector class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__PATTERN_TERM_SELECTOR_H
#define CVC5__THEORY__QUANTIFIERS__PATTERN_TERM_SELECTOR_H
* Trigger class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_H
#define CVC5__THEORY__QUANTIFIERS__TRIGGER_H
* Trigger trie class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H
#define CVC5__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H
* Trigger term info class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H
#define CVC5__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H
* Trigger trie class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_TRIE_H
#define CVC5__THEORY__QUANTIFIERS__TRIGGER_TRIE_H
* Variable match generator class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H
#define CVC5__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H
* Equality query class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
#define CVC5__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
* expr_miner
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__EXPRESSION_MINER_H
#define CVC5__THEORY__QUANTIFIERS__EXPRESSION_MINER_H
* Expression miner manager, which manages individual expression miners.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H
#define CVC5__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H
* extended rewriting class
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H
#define CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H
* Model extended classes.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__FIRST_ORDER_MODEL_H
#define CVC5__FIRST_ORDER_MODEL_H
* Bounded integers module
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__BOUNDED_INTEGERS_H
#define CVC5__BOUNDED_INTEGERS_H
* First order model for full model check.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__FMF__FIRST_ORDER_MODEL_FMC_H
#define CVC5__THEORY__QUANTIFIERS__FMF__FIRST_ORDER_MODEL_FMC_H
* Full model check class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
#define CVC5__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
* Model Builder class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__MODEL_BUILDER_H
#define CVC5__THEORY__QUANTIFIERS__MODEL_BUILDER_H
* Model Engine class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H
#define CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H
* Techniques for evaluating terms with recursively defined functions.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__QUANTIFIERS_FUN_DEF_EVALUATOR_H
#define CVC5__QUANTIFIERS_FUN_DEF_EVALUATOR_H
* Inst match class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_H
#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_H
* Inst match trie class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
* Enumerative instantiation.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__INST_STRATEGY_ENUMERATIVE_H
#define CVC5__INST_STRATEGY_ENUMERATIVE_H
* Pool-based instantiation strategy
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H
#define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H
* instantiate
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__INSTANTIATE_H
#define CVC5__THEORY__QUANTIFIERS__INSTANTIATE_H
* List of instantiations.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H
#define CVC5__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H
* Quantifiers proof checker utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__PROOF_CHECKER_H
#define CVC5__THEORY__QUANTIFIERS__PROOF_CHECKER_H
* Quantifiers bound inference.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H
#define CVC5__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H
* Quantifiers conflict find class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef QUANT_CONFLICT_FIND
#define QUANT_CONFLICT_FIND
* quantifier module
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANT_MODULE_H
#define CVC5__THEORY__QUANT_MODULE_H
* quantifier relevance
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANT_RELEVANCE_H
#define CVC5__THEORY__QUANT_RELEVANCE_H
* Quantifiers representative bound utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H
#define CVC5__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H
* dynamic quantifiers splitting
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANT_SPLIT_H
#define CVC5__THEORY__QUANT_SPLIT_H
* quantifier util
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANT_UTIL_H
#define CVC5__THEORY__QUANT_UTIL_H
* Attributes for the theory quantifiers.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
* Utility for quantifiers inference manager.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H
#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H
* Class for initializing the modules of quantifiers engine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H
#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H
* The quantifiers registry.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
* Rewriter for the theory of inductive quantifiers.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
* Utility for quantifiers state.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H
#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H
* Quantifiers statistics class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H
#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H
* of generated expressions.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__QUERY_GENERATOR_H
#define CVC5__THEORY__QUANTIFIERS__QUERY_GENERATOR_H
* Relevant domain class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
#define CVC5__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
* Utility for single invocation partitioning.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
#define CVC5__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
* Utilities for skolemization.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SKOLEMIZE_H
#define CVC5__THEORY__QUANTIFIERS__SKOLEMIZE_H
* Utility for filtering sygus solutions.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SOLUTION_FILTER_H
#define CVC5__THEORY__QUANTIFIERS__SOLUTION_FILTER_H
* Utility for processing single invocation synthesis conjectures.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
#define CVC5__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
* cegis
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__CEGIS_H
#define CVC5__THEORY__QUANTIFIERS__CEGIS_H
* Cegis core connective module.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H
#define CVC5__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H
*
* cegis with unification techinques.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H
* Class for streaming concrete values (through substitutions) from
* enumerated abstract ones.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
* This class caches the evaluation of nodes on a fixed list of examples.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__EXAMPLE_EVAL_CACHE_H
#define CVC5__THEORY__QUANTIFIERS__EXAMPLE_EVAL_CACHE_H
* (functions applied to concrete arguments only).
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__EXAMPLE_INFER_H
#define CVC5__THEORY__QUANTIFIERS__EXAMPLE_INFER_H
* on substitutions with a fixed domain.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H
#define CVC5__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H
* Utility class for Sygus Reconstruct module.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H
#define CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H
* Utility class for Sygus Reconstruct module.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
#define CVC5__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
* sygus_enumerator
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H
* Basic sygus enumerator class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H
* sygus_eval_unfold
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H
* sygus explanations
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H
* grammars that encode syntactic restrictions for SyGuS.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
*
* Class for simplifying SyGuS grammars after they are encoded into datatypes.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H
* sygus_grammar_red
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H
* Sygus invariance tests.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
* sygus_module
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_MODULE_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_MODULE_H
* Utility for processing programming by examples synthesis conjectures.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_PBE_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_PBE_H
* Techniqures for static preprocessing and analysis of sygus conjectures.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H
* Utility for reconstructing terms to match a grammar.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H
* sygus_repair_const
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H
* A shared statistics class for sygus.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_STATS_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_STATS_H
* sygus_unif
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_H
* sygus_unif_io
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H
* sygus_unif_rl
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H
* sygus_unif_strat
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H
* Generic sygus utilities.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H
* conjecture.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
#define CVC5__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
* in particular, those described in Reynolds et al CAV 2015.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYNTH_ENGINE_H
#define CVC5__THEORY__QUANTIFIERS__SYNTH_ENGINE_H
* Utility for inferring templates for invariant problems.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H
* Term database sygus class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H
#define CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H
* transition system.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H
#define CVC5__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H
* Sygus type info data structure.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H
* Type node identifier trie data structure.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H
* SyGuS instantiator class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INST_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_INST_H
* sygus_sampler
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
* Term database class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H
#define CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H
* Utilities for term enumeration.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__TERM_ENUMERATION_H
#define CVC5__THEORY__QUANTIFIERS__TERM_ENUMERATION_H
* Utilities for term enumeration.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__TERM_POOLS_H
#define CVC5__THEORY__QUANTIFIERS__TERM_POOLS_H
* Term registry class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__TERM_REGISTRY_H
#define CVC5__THEORY__QUANTIFIERS__TERM_REGISTRY_H
* Term utilities class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__TERM_UTIL_H
#define CVC5__THEORY__QUANTIFIERS__TERM_UTIL_H
* Theory of quantifiers.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
#define CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
* Theory of quantifiers.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H
#define CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H
* Theory instantiator, Instantiation Engine classes.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS_ENGINE_H
#define CVC5__THEORY__QUANTIFIERS_ENGINE_H
* Relevance manager.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__RELEVANCE_MANAGER__H
#define CVC5__THEORY__RELEVANCE_MANAGER__H
* Representative set class and utilities.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__REP_SET_H
#define CVC5__THEORY__REP_SET_H
* The Rewriter class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* Rewriter attributes.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* from the Theory kinds files.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* Theory of separation logic.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__SEP__THEORY_SEP_H
#define CVC5__THEORY__SEP__THEORY_SEP_H
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__SEP__THEORY_SEP_REWRITER_H
#define CVC5__THEORY__SEP__THEORY_SEP_REWRITER_H
* Typing and cardinality rules for the theory of sep.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__SEP__THEORY_SEP_TYPE_RULES_H
#define CVC5__THEORY__SEP__THEORY_SEP_TYPE_RULES_H
* 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
* 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
* 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
* 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
* 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
* 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
* 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
* Sets theory.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__SETS__THEORY_SETS_H
#define CVC5__THEORY__SETS__THEORY_SETS_H
* 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
* 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
* 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
* 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
* Base class for shared solver.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__SHARED_SOLVER__H
#define CVC5__THEORY__SHARED_SOLVER__H
* Shared solver in the distributed architecture.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__SHARED_SOLVER_DISTRIBUTED__H
#define CVC5__THEORY__SHARED_SOLVER_DISTRIBUTED__H
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* The skolem lemma utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__SKOLEM_LEMMA_H
#define CVC5__THEORY__SKOLEM_LEMMA_H
* Utilities for initializing subsolvers (copies of SmtEngine) during solving.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__SMT_ENGINE_SUBSOLVER_H
#define CVC5__THEORY__SMT_ENGINE_SUBSOLVER_H
* Pre-process step for performing sort inference.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__SORT_INFERENCE_H
#define CVC5__SORT_INFERENCE_H
* Arithmetic entailment computation for string terms.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__ARITH_ENTAIL_H
#define CVC5__THEORY__STRINGS__ARITH_ENTAIL_H
* theory of strings.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__BASE_SOLVER_H
#define CVC5__THEORY__STRINGS__BASE_SOLVER_H
* string concatenation plus length constraints.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__CORE_SOLVER_H
#define CVC5__THEORY__STRINGS__CORE_SOLVER_H
* The eager solver.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__EAGER_SOLVER_H
#define CVC5__THEORY__STRINGS__EAGER_SOLVER_H
* Equivalence class info for the theory of strings.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__EQC_INFO_H
#define CVC5__THEORY__STRINGS__EQC_INFO_H
* Solver for extended functions of theory of strings.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__EXTF_SOLVER_H
#define CVC5__THEORY__STRINGS__EXTF_SOLVER_H
* Inference information utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__INFER_INFO_H
#define CVC5__THEORY__STRINGS__INFER_INFO_H
* Inference to proof conversion.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__INFER_PROOF_CONS_H
#define CVC5__THEORY__STRINGS__INFER_PROOF_CONS_H
* Customized inference manager for the theory of strings.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__INFERENCE_MANAGER_H
#define CVC5__THEORY__STRINGS__INFERENCE_MANAGER_H
* Normal form datastructure for the theory of strings.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__NORMAL_FORM_H
#define CVC5__THEORY__STRINGS__NORMAL_FORM_H
* Strings proof checker utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__PROOF_CHECKER_H
#define CVC5__THEORY__STRINGS__PROOF_CHECKER_H
* Techniques for eliminating regular expressions.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__REGEXP_ELIM_H
#define CVC5__THEORY__STRINGS__REGEXP_ELIM_H
* Entailment tests involving regular expressions.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__REGEXP_ENTAIL_H
#define CVC5__THEORY__STRINGS__REGEXP_ENTAIL_H
* Symbolic Regular Expression Operations
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__REGEXP__OPERATION_H
#define CVC5__THEORY__STRINGS__REGEXP__OPERATION_H
* Regular expression solver for the theory of strings.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__REGEXP_SOLVER_H
#define CVC5__THEORY__STRINGS__REGEXP_SOLVER_H
* Type for rewrites for strings.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__REWRITES_H
#define CVC5__THEORY__STRINGS__REWRITES_H
* Rewriter for the theory of strings and sequences.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__SEQUENCES_REWRITER_H
#define CVC5__THEORY__STRINGS__SEQUENCES_REWRITER_H
* Statistics for the theory of strings/sequences.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__SEQUENCES_STATS_H
#define CVC5__THEORY__STRINGS__SEQUENCES_STATS_H
* A cache of skolems for theory of strings.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__SKOLEM_CACHE_H
#define CVC5__THEORY__STRINGS__SKOLEM_CACHE_H
* The solver state of the theory of strings.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__SOLVER_STATE_H
#define CVC5__THEORY__STRINGS__SOLVER_STATE_H
* Strategy of the theory of strings.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__STRATEGY_H
#define CVC5__THEORY__STRINGS__STRATEGY_H
* Entailment tests involving strings.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__STRING_ENTAIL_H
#define CVC5__THEORY__STRINGS__STRING_ENTAIL_H
* A finite model finding decision strategy for strings.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__STRINGS_FMF_H
#define CVC5__THEORY__STRINGS__STRINGS_FMF_H
* Rewrite rules for string-specific operators in theory of strings.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__STRINGS_REWRITER_H
#define CVC5__THEORY__STRINGS__STRINGS_REWRITER_H
* Term registry for the theory of strings.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__TERM_REGISTRY_H
#define CVC5__THEORY__STRINGS__TERM_REGISTRY_H
* Theory of strings.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__THEORY_STRINGS_H
#define CVC5__THEORY__STRINGS__THEORY_STRINGS_H
* Strings Preprocess.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__PREPROCESS_H
#define CVC5__THEORY__STRINGS__PREPROCESS_H
* Typing rules for the theory of strings and regexps.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
#define CVC5__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
* Util functions for theory strings.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__THEORY_STRINGS_UTILS_H
#define CVC5__THEORY__STRINGS__THEORY_STRINGS_UTILS_H
* Enumerators for strings.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__TYPE_ENUMERATOR_H
#define CVC5__THEORY__STRINGS__TYPE_ENUMERATOR_H
* Utility functions for words.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__STRINGS__WORD_H
#define CVC5__THEORY__STRINGS__WORD_H
* Substitution minimization.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__SUBS_MINIMIZE_H
#define CVC5__THEORY__SUBS_MINIMIZE_H
* A substitution mapping for theory simplification.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__SUBSTITUTIONS_H
#define CVC5__THEORY__SUBSTITUTIONS_H
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* Base of the theory interface.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__THEORY_H
#define CVC5__THEORY__THEORY_H
* The theory engine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY_ENGINE_H
#define CVC5__THEORY_ENGINE_H
* The theory engine proof generator.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY_ENGINE_PROOF_GENERATOR_H
#define CVC5__THEORY_ENGINE_PROOF_GENERATOR_H
* The theory equality notify utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__THEORY_EQ_NOTIFY_H
#define CVC5__THEORY__THEORY_EQ_NOTIFY_H
* \todo document this file
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__THEORY__THEORY_ID_H
#define CVC5__THEORY__THEORY_ID_H
* The theory inference utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__THEORY_INFERENCE_H
#define CVC5__THEORY__THEORY_INFERENCE_H
* An inference manager for Theory.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__THEORY_INFERENCE_MANAGER_H
#define CVC5__THEORY__THEORY_INFERENCE_MANAGER_H
* Model class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__THEORY_MODEL_H
#define CVC5__THEORY__THEORY_MODEL_H
* Model class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__THEORY_MODEL_BUILDER_H
#define CVC5__THEORY__THEORY_MODEL_BUILDER_H
* The theory preprocessor.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__THEORY_PREPROCESSOR_H
#define CVC5__THEORY__THEORY_PREPROCESSOR_H
* Theory proof step buffer utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__THEORY_PROOF_STEP_BUFFER_H
#define CVC5__THEORY__THEORY_PROOF_STEP_BUFFER_H
* The interface that theory rewriters implement.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__THEORY_REWRITER_H
#define CVC5__THEORY__THEORY_REWRITER_H
* A theory state for Theory.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__THEORY_STATE_H
#define CVC5__THEORY__THEORY_STATE_H
* kinds files to produce the final header.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* The trust node utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__TRUST_NODE_H
#define CVC5__THEORY__TRUST_NODE_H
* Trust substitutions.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__TRUST_SUBSTITUTIONS_H
#define CVC5__THEORY__TRUST_SUBSTITUTIONS_H
* Enumerators for types.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__TYPE_ENUMERATOR_H
#define CVC5__THEORY__TYPE_ENUMERATOR_H
* Type set class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__TYPE_SET_H
#define CVC5__THEORY__TYPE_SET_H
* Theory of UF with cardinality.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY_UF_STRONG_SOLVER_H
#define CVC5__THEORY_UF_STRONG_SOLVER_H
* A proof as produced by the equality engine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#include "expr/node.h"
#include "theory/uf/equality_engine_types.h"
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__UF__EQUALITY_ENGINE_H
#define CVC5__THEORY__UF__EQUALITY_ENGINE_H
* Iterator class for equality engine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__UF__EQUALITY_ENGINE_ITERATOR_H
#define CVC5__THEORY__UF__EQUALITY_ENGINE_ITERATOR_H
* The virtual class for notifications from the equality engine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__UF__EQUALITY_ENGINE_NOTIFY_H
#define CVC5__THEORY__UF__EQUALITY_ENGINE_NOTIFY_H
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__UF__EQUALITY_ENGINE_TYPES_H
#define CVC5__THEORY__UF__EQUALITY_ENGINE_TYPES_H
* The higher-order extension of TheoryUF.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef __CVC5__THEORY__UF__HO_EXTENSION_H
#define __CVC5__THEORY__UF__HO_EXTENSION_H
* Equality proof checker utility.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__UF__PROOF_CHECKER_H
#define CVC5__THEORY__UF__PROOF_CHECKER_H
* The proof-producing equality engine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__UF__PROOF_EQUALITY_ENGINE_H
#define CVC5__THEORY__UF__PROOF_EQUALITY_ENGINE_H
* </pre>
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__UF__SYMMETRY_BREAKER_H
#define CVC5__THEORY__UF__SYMMETRY_BREAKER_H
* All implementations of TheoryUF should inherit from this class.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__UF__THEORY_UF_H
#define CVC5__THEORY__UF__THEORY_UF_H
* Model for Theory UF.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY_UF_MODEL_H
#define CVC5__THEORY_UF_MODEL_H
* \todo document this file
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__UF__THEORY_UF_REWRITER_H
#define CVC5__THEORY__UF__THEORY_UF_REWRITER_H
* [[ Add file-specific comments here ]]
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__UF__THEORY_UF_TYPE_RULES_H
#define CVC5__THEORY__UF__THEORY_UF_TYPE_RULES_H
* takes a Valuation, which delegates to TheoryEngine.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__THEORY__VALUATION_H
#define CVC5__THEORY__VALUATION_H
* Representation of abstract values.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#pragma once
* (http://gcc.gnu.org/onlinedocs/libstdc++/ext/pb_ds/priority_queue.html)
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__BIN_HEAP_H
#define CVC5__BIN_HEAP_H
* A fixed-size bit-vector, implemented as a wrapper around Integer.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__BITVECTOR_H
#define CVC5__BITVECTOR_H
* A hash function for Boolean.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__BOOL_H
#define CVC5__BOOL_H
* give the cardinality of sorts.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__CARDINALITY_H
#define CVC5__CARDINALITY_H
* Utilities for cardinality classes.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__UTIL__CARDINALITY_CLASS_H
#define CVC5__UTIL__CARDINALITY_CLASS_H
* The derived utility classes DenseSet and DenseMultiset are also defined.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#pragma once
* \todo document this file
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__DIVISIBLE_H
#define CVC5__DIVISIBLE_H
* This file contains the data structures used by the constant and parametric
* types of the floating point theory.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__FLOATINGPOINT_H
#define CVC5__FLOATINGPOINT_H
*
* !!! This header is not to be included in any other headers !!!
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H
#define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H
* BitVector.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H
#define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H
*
* The class representing a floating-point format.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__FLOATINGPOINT_SIZE_H
#define CVC5__FLOATINGPOINT_SIZE_H
* \todo document this file
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__GMP_UTIL_H
#define CVC5__GMP_UTIL_H
* \todo document this file
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__HASH_H
#define CVC5__HASH_H
* The integer AND operator.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__IAND_H
#define CVC5__IAND_H
* Standardized type for efficient array indexing.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__INDEX_H
#define CVC5__INDEX_H
* Utils for indexed root predicates.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__UTIL__INDEXED_ROOT_PREDICATE_H
#define CVC5__UTIL__INDEXED_ROOT_PREDICATE_H
* A multiprecision integer constant; wraps a CLN multiprecision integer.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__INTEGER_H
#define CVC5__INTEGER_H
* A multiprecision integer constant; wraps a GMP multiprecision integer.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__INTEGER_H
#define CVC5__INTEGER_H
* Nothing using a value of T
* - High level of assurance that a value is not used before it is set.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__UTIL__MAYBE_H
#define CVC5__UTIL__MAYBE_H
* Utilities for using ostreams.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__UTIL__OSTREAM_UTIL_H
#define CVC5__UTIL__OSTREAM_UTIL_H
* Utilities for working with LibPoly.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__POLY_UTIL_H
#define CVC5__POLY_UTIL_H
* generators, scrambled. ACM Trans. Math. Softw. 42(4): 30:1-30:23, 2016).
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__UTIL__RANDOM_H
#define CVC5__UTIL__RANDOM_H
* Multiprecision rational constants; wraps a CLN multiprecision rational.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__RATIONAL_H
#define CVC5__RATIONAL_H
* Multiprecision rational constants; wraps a GMP multiprecision rational.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__RATIONAL_H
#define CVC5__RATIONAL_H
* Algebraic number constants; wraps a libpoly algebraic number.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__REAL_ALGEBRAIC_NUMBER_H
#define CVC5__REAL_ALGEBRAIC_NUMBER_H
* Data structures for regular expression operators.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__UTIL__REGEXP_H
#define CVC5__UTIL__REGEXP_H
* time limits.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__RESOURCE_MANAGER_H
#define CVC5__RESOURCE_MANAGER_H
* Encapsulation of the result of a query.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__RESULT_H
#define CVC5__RESULT_H
*
* The definition of rounding mode values.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__ROUNDINGMODE_H
#define CVC5__ROUNDINGMODE_H
* IMPORTANT: The `toString(obj)` function *must not* perform any allocations
* or call other functions that are not async-signal-safe.
*
- * This header is a "cvc4_private_library.h" header because it is private but
+ * This header is a "cvc5_private_library.h" header because it is private but
* the safe_print functions are used in the driver. See also the description
* of "statistics_registry.h" for more information on
- * "cvc4_private_library.h".
+ * "cvc5_private_library.h".
*/
-#include "cvc4_private_library.h"
+#include "cvc5_private_library.h"
#ifndef CVC5__SAFE_PRINT_H
#define CVC5__SAFE_PRINT_H
* with biased and unbiased distributions.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__UTIL_FLOATINGPOINT_SAMPLER_H
#define CVC5__UTIL_FLOATINGPOINT_SAMPLER_H
* These are VERY overly verbose and keep much more data than is needed.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__SEXPR_H
#define CVC5__SEXPR_H
* Quotes a string if necessary for smt2.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__UTIL__SMT2_QUOTE_STRING_H
#define CVC5__UTIL__SMT2_QUOTE_STRING_H
* \todo document this file
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__STATISTICS_H
#define CVC5__STATISTICS_H
* Registration and documentation for all public statistics.
*/
-#include "cvc4_private_library.h"
+#include "cvc5_private_library.h"
#ifndef CVC5__UTIL__STATISTICS_PUBLIC_H
#define CVC5__UTIL__STATISTICS_PUBLIC_H
* The StatisticsRegistry that issues statistic proxy objects.
*/
-#include "cvc4_private_library.h"
+#include "cvc5_private_library.h"
#ifndef CVC5__UTIL__STATISTICS_REG_H
#define CVC5__UTIL__STATISTICS_REG_H
* to) statistics, the statistics registry, and some other associated
* classes.
*
- * This file is somewhat unique in that it is a "cvc4_private_library.h"
+ * This file is somewhat unique in that it is a "cvc5_private_library.h"
* header. Because of this, most classes need to be marked as CVC4_EXPORT.
* This is because CVC4_EXPORT is connected to the visibility of the linkage
* in the object files for the class. It does not dictate what headers are
* (like operator++() or operator+=())
*/
-#include "cvc4_private_library.h"
+#include "cvc5_private_library.h"
#ifndef CVC5__STATISTICS_REGISTRY_H
#define CVC5__STATISTICS_REGISTRY_H
* change the statistic data, but shield the regular user from the internals.
*/
-#include "cvc4_private_library.h"
+#include "cvc5_private_library.h"
#ifndef CVC5__UTIL__STATISTICS_STATS_H
#define CVC5__UTIL__STATISTICS_STATS_H
* conversion to the API type `Stat`.
*/
-#include "cvc4_private_library.h"
+#include "cvc5_private_library.h"
#ifndef CVC5__UTIL__STATISTICS_VALUE_H
#define CVC5__UTIL__STATISTICS_VALUE_H
* Base statistic classes.
*/
-#include "cvc4_private_library.h"
+#include "cvc5_private_library.h"
#ifndef CVC5__UTIL__STATS_BASE_H
#define CVC5__UTIL__STATS_BASE_H
* Stat classes that represent histograms.
*/
-#include "cvc4_private_library.h"
+#include "cvc5_private_library.h"
#ifndef CVC5__UTIL__STATS_HISTOGRAM_H
#define CVC5__UTIL__STATS_HISTOGRAM_H
* Stat classes that hold timers.
*/
-#include "cvc4_private_library.h"
+#include "cvc5_private_library.h"
#ifndef CVC5__UTIL__STATS_TIMER_H
#define CVC5__UTIL__STATS_TIMER_H
* Statistic utilities.
*/
-#include "cvc4_private_library.h"
+#include "cvc5_private_library.h"
#ifndef CVC5__UTIL__STATS_UTILS_H
#define CVC5__UTIL__STATS_UTILS_H
* The string data type.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__UTIL__STRING_H
#define CVC5__UTIL__STRING_H
* Tuple operators.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__TUPLE_H
#define CVC5__TUPLE_H
* and is interrupted in an unsafe state.
*/
-#include "cvc4_public.h"
+#include "cvc5_public.h"
#ifndef CVC5__UNSAFE_INTERRUPT_EXCEPTION_H
#define CVC5__UNSAFE_INTERRUPT_EXCEPTION_H
* Some standard STL-related utility functions for CVC4.
*/
-#include "cvc4_private.h"
+#include "cvc5_private.h"
#ifndef CVC5__UTILITY_H
#define CVC5__UTILITY_H