Fixes 2887.
#include "cvc4_public.h"
-#ifndef __CVC4__API__CVC4CPP_H
-#define __CVC4__API__CVC4CPP_H
+#ifndef CVC4__API__CVC4CPP_H
+#define CVC4__API__CVC4CPP_H
#include "api/cvc4cppkind.h"
#include "cvc4_public.h"
-#ifndef __CVC4__API__CVC4CPPKIND_H
-#define __CVC4__API__CVC4CPPKIND_H
+#ifndef CVC4__API__CVC4CPPKIND_H
+#define CVC4__API__CVC4CPPKIND_H
#include <ostream>
*
* Note that the underlying type of Kind must be signed (to enable range
* checks for validity). The size of this type depends on the size of
- * CVC4::Kind (__CVC4__EXPR__NODE_VALUE__NBITS__KIND, currently 10 bits,
+ * CVC4::Kind (CVC4__EXPR__NODE_VALUE__NBITS__KIND, currently 10 bits,
* see expr/metakind_template.h).
*/
enum CVC4_PUBLIC Kind : int32_t
#include "cvc4_public.h"
-#ifndef __CVC4__CONFIGURATION_H
-#define __CVC4__CONFIGURATION_H
+#ifndef CVC4__CONFIGURATION_H
+#define CVC4__CONFIGURATION_H
#include <string>
}/* CVC4 namespace */
-#endif /* __CVC4__CONFIGURATION_H */
+#endif /* CVC4__CONFIGURATION_H */
#include "cvc4_private.h"
-#ifndef __CVC4__CONFIGURATION_PRIVATE_H
-#define __CVC4__CONFIGURATION_PRIVATE_H
+#ifndef CVC4__CONFIGURATION_PRIVATE_H
+#define CVC4__CONFIGURATION_PRIVATE_H
#include <string>
}/* CVC4 namespace */
-#endif /* __CVC4__CONFIGURATION_PRIVATE_H */
+#endif /* CVC4__CONFIGURATION_PRIVATE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__ASSERT_H
-#define __CVC4__ASSERT_H
+#ifndef CVC4__ASSERT_H
+#define CVC4__ASSERT_H
#include <cstdarg>
#include <cstdio>
} /* CVC4 namespace */
-#endif /* __CVC4__ASSERT_H */
+#endif /* CVC4__ASSERT_H */
#include "cvc4_private.h"
-#ifndef __CVC4__CHECK_H
-#define __CVC4__CHECK_H
+#ifndef CVC4__CHECK_H
+#define CVC4__CHECK_H
#include <ostream>
} // namespace CVC4
-#endif /* __CVC4__CHECK_H */
+#endif /* CVC4__CHECK_H */
#include "cvc4_public.h"
-#ifndef __CVC4__EXCEPTION_H
-#define __CVC4__EXCEPTION_H
+#ifndef CVC4__EXCEPTION_H
+#define CVC4__EXCEPTION_H
#include <cstdarg>
#include <cstdlib>
}/* CVC4 namespace */
-#endif /* __CVC4__EXCEPTION_H */
+#endif /* CVC4__EXCEPTION_H */
#include "cvc4_public.h"
-#ifndef __CVC4__LISTENER_H
-#define __CVC4__LISTENER_H
+#ifndef CVC4__LISTENER_H
+#define CVC4__LISTENER_H
#include <list>
}/* CVC4 namespace */
-#endif /* __CVC4__LISTENER_H */
+#endif /* CVC4__LISTENER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__BASE__MAP_UTIL_H
-#define __CVC4__BASE__MAP_UTIL_H
+#ifndef CVC4__BASE__MAP_UTIL_H
+#define CVC4__BASE__MAP_UTIL_H
#include "base/cvc4_check.h"
} // namespace CVC4
-#endif /* __CVC4__BASE__MAP_UTIL_H */
+#endif /* CVC4__BASE__MAP_UTIL_H */
#include "cvc4_public.h"
-#ifndef __CVC4__SMT__MODAL_EXCEPTION_H
-#define __CVC4__SMT__MODAL_EXCEPTION_H
+#ifndef CVC4__SMT__MODAL_EXCEPTION_H
+#define CVC4__SMT__MODAL_EXCEPTION_H
#include "base/exception.h"
}/* CVC4 namespace */
-#endif /* __CVC4__SMT__MODAL_EXCEPTION_H */
+#endif /* CVC4__SMT__MODAL_EXCEPTION_H */
#include "cvc4_private_library.h"
-#ifndef __CVC4__OUTPUT_H
-#define __CVC4__OUTPUT_H
+#ifndef CVC4__OUTPUT_H
+#define CVC4__OUTPUT_H
#include <ios>
#include <iostream>
}/* CVC4 namespace */
-#endif /* __CVC4__OUTPUT_H */
+#endif /* CVC4__OUTPUT_H */
# error This should only be included from the Java bindings layer.
#endif /* SWIGJAVA */
-#ifndef __CVC4__BINDINGS__JAVA_ITERATOR_ADAPTER_H
-#define __CVC4__BINDINGS__JAVA_ITERATOR_ADAPTER_H
+#ifndef CVC4__BINDINGS__JAVA_ITERATOR_ADAPTER_H
+#define CVC4__BINDINGS__JAVA_ITERATOR_ADAPTER_H
namespace CVC4 {
}/* CVC4 namespace */
-#endif /* __CVC4__BINDINGS__JAVA_ITERATOR_ADAPTER_H */
+#endif /* CVC4__BINDINGS__JAVA_ITERATOR_ADAPTER_H */
#include <string>
#include <jni.h>
-#ifndef __CVC4__BINDINGS__JAVA_STREAM_ADAPTERS_H
-#define __CVC4__BINDINGS__JAVA_STREAM_ADAPTERS_H
+#ifndef CVC4__BINDINGS__JAVA_STREAM_ADAPTERS_H
+#define CVC4__BINDINGS__JAVA_STREAM_ADAPTERS_H
namespace CVC4 {
}/* CVC4 namespace */
-#endif /* __CVC4__BINDINGS__JAVA_STREAM_ADAPTERS_H */
+#endif /* CVC4__BINDINGS__JAVA_STREAM_ADAPTERS_H */
** Common swig checks and definitions, when generating swig interfaces.
**/
-#ifndef __CVC4__BINDINGS__SWIG_H
-#define __CVC4__BINDINGS__SWIG_H
+#ifndef CVC4__BINDINGS__SWIG_H
+#define CVC4__BINDINGS__SWIG_H
#ifndef SWIG
# error This file should only be included when generating swig interfaces.
// swig doesn't like GCC attributes
#define __attribute__(x)
-#endif /* __CVC4__BINDINGS__SWIG_H */
+#endif /* CVC4__BINDINGS__SWIG_H */
#include "cvc4_private.h"
-#ifndef __CVC4__UTIL__BACKTRACKABLE_H
-#define __CVC4__UTIL__BACKTRACKABLE_H
+#ifndef CVC4__UTIL__BACKTRACKABLE_H
+#define CVC4__UTIL__BACKTRACKABLE_H
#include <cstdlib>
#include <vector>
}/* CVC4 namespace */
-#endif /* __CVC4__UTIL__BACKTRACKABLE_H */
+#endif /* CVC4__UTIL__BACKTRACKABLE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__CONTEXT__CDHASHMAP_H
-#define __CVC4__CONTEXT__CDHASHMAP_H
+#ifndef CVC4__CONTEXT__CDHASHMAP_H
+#define CVC4__CONTEXT__CDHASHMAP_H
#include <functional>
#include <iterator>
}/* CVC4::context namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__CONTEXT__CDHASHMAP_H */
+#endif /* CVC4__CONTEXT__CDHASHMAP_H */
#include "cvc4_public.h"
-#ifndef __CVC4__CONTEXT__CDHASHMAP_FORWARD_H
-#define __CVC4__CONTEXT__CDHASHMAP_FORWARD_H
+#ifndef CVC4__CONTEXT__CDHASHMAP_FORWARD_H
+#define CVC4__CONTEXT__CDHASHMAP_FORWARD_H
#include <functional>
/// \endcond
-#endif /* __CVC4__CONTEXT__CDHASHMAP_FORWARD_H */
+#endif /* CVC4__CONTEXT__CDHASHMAP_FORWARD_H */
#include "cvc4_private.h"
-#ifndef __CVC4__CONTEXT__CDHASHSET_H
-#define __CVC4__CONTEXT__CDHASHSET_H
+#ifndef CVC4__CONTEXT__CDHASHSET_H
+#define CVC4__CONTEXT__CDHASHSET_H
#include "base/cvc4_assert.h"
#include "context/context.h"
}/* CVC4::context namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__CONTEXT__CDHASHSET_H */
+#endif /* CVC4__CONTEXT__CDHASHSET_H */
#include "cvc4_public.h"
-#ifndef __CVC4__CONTEXT__CDSET_FORWARD_H
-#define __CVC4__CONTEXT__CDSET_FORWARD_H
+#ifndef CVC4__CONTEXT__CDSET_FORWARD_H
+#define CVC4__CONTEXT__CDSET_FORWARD_H
#include <functional>
} // namespace context
} // namespace CVC4
-#endif /* __CVC4__CONTEXT__CDSET_FORWARD_H */
+#endif /* CVC4__CONTEXT__CDSET_FORWARD_H */
#include "cvc4_public.h"
-#ifndef __CVC4__CONTEXT__CDINSERT_HASHMAP_FORWARD_H
-#define __CVC4__CONTEXT__CDINSERT_HASHMAP_FORWARD_H
+#ifndef CVC4__CONTEXT__CDINSERT_HASHMAP_FORWARD_H
+#define CVC4__CONTEXT__CDINSERT_HASHMAP_FORWARD_H
#include <functional>
} // namespace context
} // namespace CVC4
-#endif /* __CVC4__CONTEXT__CDINSERT_HASHMAP_FORWARD_H */
+#endif /* CVC4__CONTEXT__CDINSERT_HASHMAP_FORWARD_H */
#include "cvc4_private.h"
-#ifndef __CVC4__CONTEXT__CDLIST_H
-#define __CVC4__CONTEXT__CDLIST_H
+#ifndef CVC4__CONTEXT__CDLIST_H
+#define CVC4__CONTEXT__CDLIST_H
#include <iterator>
#include <memory>
}/* CVC4::context namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__CONTEXT__CDLIST_H */
+#endif /* CVC4__CONTEXT__CDLIST_H */
#include "cvc4_public.h"
-#ifndef __CVC4__CONTEXT__CDLIST_FORWARD_H
-#define __CVC4__CONTEXT__CDLIST_FORWARD_H
+#ifndef CVC4__CONTEXT__CDLIST_FORWARD_H
+#define CVC4__CONTEXT__CDLIST_FORWARD_H
#include <memory>
}/* CVC4::context namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__CONTEXT__CDLIST_FORWARD_H */
+#endif /* CVC4__CONTEXT__CDLIST_FORWARD_H */
#include "cvc4_private.h"
-#ifndef __CVC4__CONTEXT__CDO_H
-#define __CVC4__CONTEXT__CDO_H
+#ifndef CVC4__CONTEXT__CDO_H
+#define CVC4__CONTEXT__CDO_H
#include "base/cvc4_assert.h"
#include "context/context.h"
}/* CVC4::context namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__CONTEXT__CDO_H */
+#endif /* CVC4__CONTEXT__CDO_H */
#include "cvc4_private.h"
-#ifndef __CVC4__CONTEXT__CDQUEUE_H
-#define __CVC4__CONTEXT__CDQUEUE_H
+#ifndef CVC4__CONTEXT__CDQUEUE_H
+#define CVC4__CONTEXT__CDQUEUE_H
#include "context/context.h"
#include "context/cdlist.h"
}/* CVC4::context namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__CONTEXT__CDQUEUE_H */
+#endif /* CVC4__CONTEXT__CDQUEUE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__CONTEXT__CDTRAIL_QUEUE_H
-#define __CVC4__CONTEXT__CDTRAIL_QUEUE_H
+#ifndef CVC4__CONTEXT__CDTRAIL_QUEUE_H
+#define CVC4__CONTEXT__CDTRAIL_QUEUE_H
#include "context/context.h"
#include "context/cdlist.h"
}/* CVC4::context namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__CONTEXT__CDTRAIL_QUEUE_H */
+#endif /* CVC4__CONTEXT__CDTRAIL_QUEUE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__CONTEXT__CONTEXT_H
-#define __CVC4__CONTEXT__CONTEXT_H
+#ifndef CVC4__CONTEXT__CONTEXT_H
+#define CVC4__CONTEXT__CONTEXT_H
#include <cstdlib>
#include <cstring>
}/* CVC4::context namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__CONTEXT__CONTEXT_H */
+#endif /* CVC4__CONTEXT__CONTEXT_H */
#include "cvc4_private.h"
-#ifndef __CVC4__CONTEXT__CONTEXT_MM_H
-#define __CVC4__CONTEXT__CONTEXT_MM_H
+#ifndef CVC4__CONTEXT__CONTEXT_MM_H
+#define CVC4__CONTEXT__CONTEXT_MM_H
#include <deque>
#include <limits>
}/* CVC4::context namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__CONTEXT__CONTEXT_MM_H */
+#endif /* CVC4__CONTEXT__CONTEXT_MM_H */
#include "cvc4_private.h"
-#ifndef __CVC4__DECISION__DECISION_ATTRIBUTES_H
-#define __CVC4__DECISION__DECISION_ATTRIBUTES_H
+#ifndef CVC4__DECISION__DECISION_ATTRIBUTES_H
+#define CVC4__DECISION__DECISION_ATTRIBUTES_H
#include "options/decision_weight.h"
#include "expr/attribute.h"
}/* CVC4::decision namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__DECISION__DECISION_ATTRIBUTES_H */
+#endif /* CVC4__DECISION__DECISION_ATTRIBUTES_H */
#include "cvc4_private.h"
-#ifndef __CVC4__DECISION__DECISION_ENGINE_H
-#define __CVC4__DECISION__DECISION_ENGINE_H
+#ifndef CVC4__DECISION__DECISION_ENGINE_H
+#define CVC4__DECISION__DECISION_ENGINE_H
#include <vector>
}/* CVC4 namespace */
-#endif /* __CVC4__DECISION__DECISION_ENGINE_H */
+#endif /* CVC4__DECISION__DECISION_ENGINE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__DECISION__DECISION_STRATEGY_H
-#define __CVC4__DECISION__DECISION_STRATEGY_H
+#ifndef CVC4__DECISION__DECISION_STRATEGY_H
+#define CVC4__DECISION__DECISION_STRATEGY_H
#include "preprocessing/assertion_pipeline.h"
#include "prop/sat_solver_types.h"
}/* CVC4::decision namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__DECISION__DECISION_STRATEGY_H */
+#endif /* CVC4__DECISION__DECISION_STRATEGY_H */
#include "cvc4_private.h"
-#ifndef __CVC4__DECISION__JUSTIFICATION_HEURISTIC
-#define __CVC4__DECISION__JUSTIFICATION_HEURISTIC
+#ifndef CVC4__DECISION__JUSTIFICATION_HEURISTIC
+#define CVC4__DECISION__JUSTIFICATION_HEURISTIC
#include <unordered_set>
}/* namespace decision */
}/* namespace CVC4 */
-#endif /* __CVC4__DECISION__JUSTIFICATION_HEURISTIC */
+#endif /* CVC4__DECISION__JUSTIFICATION_HEURISTIC */
#include "cvc4_public.h"
-#ifndef __CVC4__ARRAY_H
-#define __CVC4__ARRAY_H
+#ifndef CVC4__ARRAY_H
+#define CVC4__ARRAY_H
// we get ArrayType right now by #including type.h.
// array.h is still useful for the auto-generated kinds #includes.
#include "expr/type.h"
-#endif /* __CVC4__ARRAY_H */
+#endif /* CVC4__ARRAY_H */
#include "cvc4_public.h"
-#ifndef __CVC4__ARRAY_STORE_ALL_H
-#define __CVC4__ARRAY_STORE_ALL_H
+#ifndef CVC4__ARRAY_STORE_ALL_H
+#define CVC4__ARRAY_STORE_ALL_H
#include <iosfwd>
#include <memory>
} // namespace CVC4
-#endif /* __CVC4__ARRAY_STORE_ALL_H */
+#endif /* CVC4__ARRAY_STORE_ALL_H */
#include "cvc4_public.h"
-#ifndef __CVC4__ASCRIPTION_TYPE_H
-#define __CVC4__ASCRIPTION_TYPE_H
+#ifndef CVC4__ASCRIPTION_TYPE_H
+#define CVC4__ASCRIPTION_TYPE_H
#include "expr/type.h"
}/* CVC4 namespace */
-#endif /* __CVC4__ASCRIPTION_TYPE_H */
+#endif /* CVC4__ASCRIPTION_TYPE_H */
#include "expr/node.h"
#include "expr/type_node.h"
-#ifndef __CVC4__EXPR__ATTRIBUTE_H
-#define __CVC4__EXPR__ATTRIBUTE_H
+#ifndef CVC4__EXPR__ATTRIBUTE_H
+#define CVC4__EXPR__ATTRIBUTE_H
#include <string>
#include <stdint.h>
}/* CVC4 namespace */
-#endif /* __CVC4__EXPR__ATTRIBUTE_H */
+#endif /* CVC4__EXPR__ATTRIBUTE_H */
# error expr/attribute_internals.h should only be included by expr/attribute.h
#endif /* CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H */
-#ifndef __CVC4__EXPR__ATTRIBUTE_INTERNALS_H
-#define __CVC4__EXPR__ATTRIBUTE_INTERNALS_H
+#ifndef CVC4__EXPR__ATTRIBUTE_INTERNALS_H
+#define CVC4__EXPR__ATTRIBUTE_INTERNALS_H
#include <cstdint>
#include <unordered_map>
}/* CVC4::expr namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__EXPR__ATTRIBUTE_INTERNALS_H */
+#endif /* CVC4__EXPR__ATTRIBUTE_INTERNALS_H */
#include "cvc4_public.h"
-#ifndef __CVC4__CHAIN_H
-#define __CVC4__CHAIN_H
+#ifndef CVC4__CHAIN_H
+#define CVC4__CHAIN_H
#include "expr/kind.h"
#include <iostream>
}/* CVC4 namespace */
-#endif /* __CVC4__CHAIN_H */
+#endif /* CVC4__CHAIN_H */
#include "cvc4_public.h"
-#ifndef __CVC4__DATATYPE_H
-#define __CVC4__DATATYPE_H
+#ifndef CVC4__DATATYPE_H
+#define CVC4__DATATYPE_H
#include <functional>
#include <iostream>
}/* CVC4 namespace */
-#endif /* __CVC4__DATATYPE_H */
+#endif /* CVC4__DATATYPE_H */
#include "cvc4_public.h"
-#ifndef __CVC4__EXPR__EXPR_IOMANIP_H
-#define __CVC4__EXPR__EXPR_IOMANIP_H
+#ifndef CVC4__EXPR__EXPR_IOMANIP_H
+#define CVC4__EXPR__EXPR_IOMANIP_H
#include <iosfwd>
}/* CVC4 namespace */
-#endif /* __CVC4__EXPR__EXPR_IOMANIP_H */
+#endif /* CVC4__EXPR__EXPR_IOMANIP_H */
#include "cvc4_private.h"
-#ifndef __CVC4__EXPR_MANAGER_SCOPE_H
-#define __CVC4__EXPR_MANAGER_SCOPE_H
+#ifndef CVC4__EXPR_MANAGER_SCOPE_H
+#define CVC4__EXPR_MANAGER_SCOPE_H
#include "expr/expr.h"
#include "expr/node_manager.h"
}/* CVC4 namespace */
-#endif /* __CVC4__EXPR_MANAGER_SCOPE_H */
+#endif /* CVC4__EXPR_MANAGER_SCOPE_H */
#include "cvc4_public.h"
-#ifndef __CVC4__EXPR_MANAGER_H
-#define __CVC4__EXPR_MANAGER_H
+#ifndef CVC4__EXPR_MANAGER_H
+#define CVC4__EXPR_MANAGER_H
#include <vector>
}/* CVC4 namespace */
-#endif /* __CVC4__EXPR_MANAGER_H */
+#endif /* CVC4__EXPR_MANAGER_H */
#include "cvc4_public.h"
-#ifndef __CVC4__EXPR_STREAM_H
-#define __CVC4__EXPR_STREAM_H
+#ifndef CVC4__EXPR_STREAM_H
+#define CVC4__EXPR_STREAM_H
#include "expr/expr.h"
}/* CVC4 namespace */
-#endif /* __CVC4__EXPR_STREAM_H */
+#endif /* CVC4__EXPR_STREAM_H */
// "expr.h" safely, then go on to completely declare their own stuff.
${includes}
-#ifndef __CVC4__EXPR_H
-#define __CVC4__EXPR_H
+#ifndef CVC4__EXPR_H
+#define CVC4__EXPR_H
#include <stdint.h>
#include <iosfwd>
}/* CVC4 namespace */
-#endif /* __CVC4__EXPR_H */
+#endif /* CVC4__EXPR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__KIND_MAP_H
-#define __CVC4__KIND_MAP_H
+#ifndef CVC4__KIND_MAP_H
+#define CVC4__KIND_MAP_H
#include <stdint.h>
#include <iterator>
}/* CVC4 namespace */
-#endif /* __CVC4__KIND_MAP_H */
+#endif /* CVC4__KIND_MAP_H */
#include "cvc4_public.h"
-#ifndef __CVC4__KIND_H
-#define __CVC4__KIND_H
+#ifndef CVC4__KIND_H
+#define CVC4__KIND_H
#include <iosfwd>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__KIND_H */
+#endif /* CVC4__KIND_H */
#include "cvc4_private.h"
-#ifndef __CVC4__MATCHER_H
-#define __CVC4__MATCHER_H
+#ifndef CVC4__MATCHER_H
+#define CVC4__MATCHER_H
#include <iosfwd>
#include <string>
}/* CVC4 namespace */
-#endif /* __CVC4__MATCHER_H */
+#endif /* CVC4__MATCHER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__KIND__METAKIND_H
-#define __CVC4__KIND__METAKIND_H
+#ifndef CVC4__KIND__METAKIND_H
+#define CVC4__KIND__METAKIND_H
#include <iosfwd>
namespace metakind {
/* these are #defines so their sum can be #if-checked in node_value.h */
-#define __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT 20
-#define __CVC4__EXPR__NODE_VALUE__NBITS__KIND 10
-#define __CVC4__EXPR__NODE_VALUE__NBITS__ID 40
-#define __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN 26
+#define CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT 20
+#define CVC4__EXPR__NODE_VALUE__NBITS__KIND 10
+#define CVC4__EXPR__NODE_VALUE__NBITS__ID 40
+#define CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN 26
static const unsigned MAX_CHILDREN =
- (1u << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1;
+ (1u << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1;
}/* CVC4::kind::metakind namespace */
}/* CVC4::kind namespace */
#include "expr/node_value.h"
-#endif /* __CVC4__KIND__METAKIND_H */
+#endif /* CVC4__KIND__METAKIND_H */
${metakind_includes}
-#ifdef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
+#ifdef CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
namespace CVC4 {
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */
+#endif /* CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */
// circular dependency
#include "expr/node_value.h"
-#ifndef __CVC4__NODE_H
-#define __CVC4__NODE_H
+#ifndef CVC4__NODE_H
+#define CVC4__NODE_H
#include <stdint.h>
}/* CVC4 namespace */
-#endif /* __CVC4__NODE_H */
+#endif /* CVC4__NODE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__EXPR__NODE_ALGORITHM_H
-#define __CVC4__EXPR__NODE_ALGORITHM_H
+#ifndef CVC4__EXPR__NODE_ALGORITHM_H
+#define CVC4__EXPR__NODE_ALGORITHM_H
#include <unordered_map>
#include <vector>
#include "expr/node.h"
#include "expr/type_node.h"
-#ifndef __CVC4__NODE_BUILDER_H
-#define __CVC4__NODE_BUILDER_H
+#ifndef CVC4__NODE_BUILDER_H
+#define CVC4__NODE_BUILDER_H
#include <cstdlib>
#include <iostream>
*/
inline void realloc() {
size_t newSize = 2 * size_t(d_nvMaxChildren);
- size_t hardLimit = (1lu << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1;
+ size_t hardLimit = (1lu << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1;
realloc(__builtin_expect( ( newSize > hardLimit ), false ) ? hardLimit : newSize);
}
void NodeBuilder<nchild_thresh>::realloc(size_t toSize) {
Assert( toSize > d_nvMaxChildren,
"attempt to realloc() a NodeBuilder to a smaller/equal size!" );
- Assert( toSize < (1lu << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN),
+ Assert( toSize < (1lu << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN),
"attempt to realloc() a NodeBuilder to size %u (beyond hard limit of %u)",
- toSize, (1lu << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1 );
+ toSize, (1lu << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1 );
if(__builtin_expect( ( nvIsAllocated() ), false )) {
// Ensure d_nv is not modified on allocation failure
}/* CVC4 namespace */
-#endif /* __CVC4__NODE_BUILDER_H */
+#endif /* CVC4__NODE_BUILDER_H */
#include "expr/expr.h"
#include "expr/expr_manager.h"
-#ifndef __CVC4__NODE_MANAGER_H
-#define __CVC4__NODE_MANAGER_H
+#ifndef CVC4__NODE_MANAGER_H
+#define CVC4__NODE_MANAGER_H
#include <vector>
#include <string>
}/* CVC4 namespace */
-#define __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
+#define CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
#include "expr/metakind.h"
-#undef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
+#undef CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
#include "expr/node_builder.h"
}/* CVC4 namespace */
-#endif /* __CVC4__NODE_MANAGER_H */
+#endif /* CVC4__NODE_MANAGER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__EXPR__NODE_MANAGER_LISTENERS_H
-#define __CVC4__EXPR__NODE_MANAGER_LISTENERS_H
+#ifndef CVC4__EXPR__NODE_MANAGER_LISTENERS_H
+#define CVC4__EXPR__NODE_MANAGER_LISTENERS_H
#include "base/listener.h"
#include "util/resource_manager.h"
}/* CVC4::expr namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__EXPR__NODE_MANAGER_LISTENERS_H */
+#endif /* CVC4__EXPR__NODE_MANAGER_LISTENERS_H */
#include "cvc4_private.h"
-#ifndef __CVC4__EXPR__NODE_SELF_ITERATOR_H
-#define __CVC4__EXPR__NODE_SELF_ITERATOR_H
+#ifndef CVC4__EXPR__NODE_SELF_ITERATOR_H
+#define CVC4__EXPR__NODE_SELF_ITERATOR_H
#include <iterator>
}/* CVC4::expr namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__EXPR__NODE_SELF_ITERATOR_H */
+#endif /* CVC4__EXPR__NODE_SELF_ITERATOR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__EXPR__NODE_TRIE_H
-#define __CVC4__EXPR__NODE_TRIE_H
+#ifndef CVC4__EXPR__NODE_TRIE_H
+#define CVC4__EXPR__NODE_TRIE_H
#include <map>
#include "expr/node.h"
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__EXPR__NODE_TRIE_H */
+#endif /* CVC4__EXPR__NODE_TRIE_H */
// circular dependency
#include "expr/metakind.h"
-#ifndef __CVC4__EXPR__NODE_VALUE_H
-#define __CVC4__EXPR__NODE_VALUE_H
+#ifndef CVC4__EXPR__NODE_VALUE_H
+#define CVC4__EXPR__NODE_VALUE_H
#include <stdint.h>
namespace expr {
-#if __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT + \
- __CVC4__EXPR__NODE_VALUE__NBITS__KIND + \
- __CVC4__EXPR__NODE_VALUE__NBITS__ID + \
- __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN != 96
+#if CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT + \
+ CVC4__EXPR__NODE_VALUE__NBITS__KIND + \
+ CVC4__EXPR__NODE_VALUE__NBITS__ID + \
+ CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN != 96
# error NodeValue header bit assignment does not sum to 96 !
#endif /* sum != 96 */
*/
class NodeValue {
- static const unsigned NBITS_REFCOUNT = __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT;
- static const unsigned NBITS_KIND = __CVC4__EXPR__NODE_VALUE__NBITS__KIND;
- static const unsigned NBITS_ID = __CVC4__EXPR__NODE_VALUE__NBITS__ID;
- static const unsigned NBITS_NCHILDREN = __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN;
+ static const unsigned NBITS_REFCOUNT = CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT;
+ static const unsigned NBITS_KIND = CVC4__EXPR__NODE_VALUE__NBITS__KIND;
+ static const unsigned NBITS_ID = CVC4__EXPR__NODE_VALUE__NBITS__ID;
+ static const unsigned NBITS_NCHILDREN = CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN;
/** Maximum reference count possible. Used for sticky
* reference-counting. Should be (1 << num_bits(d_rc)) - 1 */
}/* CVC4 namespace */
-#endif /* __CVC4__EXPR__NODE_VALUE_H */
+#endif /* CVC4__EXPR__NODE_VALUE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PICKLE_DATA_H
-#define __CVC4__PICKLE_DATA_H
+#ifndef CVC4__PICKLE_DATA_H
+#define CVC4__PICKLE_DATA_H
#include <sstream>
#include <deque>
namespace pickle {
const unsigned NBITS_BLOCK = 64;
-const unsigned NBITS_KIND = __CVC4__EXPR__NODE_VALUE__NBITS__KIND;
-const unsigned NBITS_NCHILDREN = __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN;
+const unsigned NBITS_KIND = CVC4__EXPR__NODE_VALUE__NBITS__KIND;
+const unsigned NBITS_NCHILDREN = CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN;
const unsigned NBITS_CONSTBLOCKS = 32;
struct BlockHeader {
}/* CVC4::expr namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PICKLE_DATA_H */
+#endif /* CVC4__PICKLE_DATA_H */
#include "cvc4_public.h"
-#ifndef __CVC4__PICKLER_H
-#define __CVC4__PICKLER_H
+#ifndef CVC4__PICKLER_H
+#define CVC4__PICKLER_H
#include "expr/variable_type_map.h"
#include "expr/expr.h"
}/* CVC4::expr namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PICKLER_H */
+#endif /* CVC4__PICKLER_H */
#include "cvc4_public.h"
-#ifndef __CVC4__RECORD_H
-#define __CVC4__RECORD_H
+#ifndef CVC4__RECORD_H
+#define CVC4__RECORD_H
#include <functional>
#include <iostream>
}/* CVC4 namespace */
-#endif /* __CVC4__RECORD_H */
+#endif /* CVC4__RECORD_H */
#include "cvc4_public.h"
-#ifndef __CVC4__SYMBOL_TABLE_H
-#define __CVC4__SYMBOL_TABLE_H
+#ifndef CVC4__SYMBOL_TABLE_H
+#define CVC4__SYMBOL_TABLE_H
#include <memory>
#include <string>
} // namespace CVC4
-#endif /* __CVC4__SYMBOL_TABLE_H */
+#endif /* CVC4__SYMBOL_TABLE_H */
#include "cvc4_public.h"
-#ifndef __CVC4__TYPE_H
-#define __CVC4__TYPE_H
+#ifndef CVC4__TYPE_H
+#define CVC4__TYPE_H
#include <climits>
#include <cstdint>
}/* CVC4 namespace */
-#endif /* __CVC4__TYPE_H */
+#endif /* CVC4__TYPE_H */
// ordering dependence
#include "expr/node.h"
-#ifndef __CVC4__EXPR__TYPE_CHECKER_H
-#define __CVC4__EXPR__TYPE_CHECKER_H
+#ifndef CVC4__EXPR__TYPE_CHECKER_H
+#define CVC4__EXPR__TYPE_CHECKER_H
namespace CVC4 {
namespace expr {
}/* CVC4::expr namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__EXPR__TYPE_CHECKER_H */
+#endif /* CVC4__EXPR__TYPE_CHECKER_H */
// circular dependency
#include "expr/node_value.h"
-#ifndef __CVC4__TYPE_NODE_H
-#define __CVC4__TYPE_NODE_H
+#ifndef CVC4__TYPE_NODE_H
+#define CVC4__TYPE_NODE_H
#include <stdint.h>
}/* CVC4 namespace */
-#endif /* __CVC4__NODE_H */
+#endif /* CVC4__NODE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__TYPE_PROPERTIES_H
-#define __CVC4__TYPE_PROPERTIES_H
+#ifndef CVC4__TYPE_PROPERTIES_H
+#define CVC4__TYPE_PROPERTIES_H
#line 23 "${template}"
}/* CVC4::kind namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__TYPE_PROPERTIES_H */
+#endif /* CVC4__TYPE_PROPERTIES_H */
#include "cvc4_public.h"
-#ifndef __CVC4__VARIABLE_TYPE_MAP_H
-#define __CVC4__VARIABLE_TYPE_MAP_H
+#ifndef CVC4__VARIABLE_TYPE_MAP_H
+#define CVC4__VARIABLE_TYPE_MAP_H
#include <unordered_map>
}/* CVC4 namespace */
-#endif /* __CVC4__VARIABLE_MAP_H */
+#endif /* CVC4__VARIABLE_MAP_H */
** most-commonly used CVC4 public-facing class interfaces.
**/
-#ifndef __CVC4__CVC4_H
-#define __CVC4__CVC4_H
+#ifndef CVC4__CVC4_H
+#define CVC4__CVC4_H
#include <cvc4/base/configuration.h>
#include <cvc4/base/exception.h>
#include <cvc4/util/integer.h>
#include <cvc4/util/rational.h>
-#endif /* __CVC4__CVC4_H */
+#endif /* CVC4__CVC4_H */
** warning when the file is included improperly.
**/
-#ifndef __CVC4_PRIVATE_H
-#define __CVC4_PRIVATE_H
+#ifndef CVC4_PRIVATE_H
+#define CVC4_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.
#include "cvc4_public.h"
#include "cvc4autoconfig.h"
-#endif /* __CVC4_PRIVATE_H */
+#endif /* CVC4_PRIVATE_H */
** warning when the file is included improperly.
**/
-#ifndef __CVC4_PRIVATE_LIBRARY_H
-#define __CVC4_PRIVATE_LIBRARY_H
+#ifndef CVC4_PRIVATE_LIBRARY_H
+#define CVC4_PRIVATE_LIBRARY_H
#if !(defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST) \
|| defined(__BUILDING_CVC4PARSERLIB) \
#include "cvc4_public.h"
#include "cvc4autoconfig.h"
-#endif /* __CVC4_PRIVATE_LIBRARY_H */
+#endif /* CVC4_PRIVATE_LIBRARY_H */
** the libraries and driver binary, and also exported to the user.
**/
-#ifndef __CVC4_PUBLIC_H
-#define __CVC4_PUBLIC_H
+#ifndef CVC4_PUBLIC_H
+#define CVC4_PUBLIC_H
#include <stdint.h>
# define CVC4_WARN_UNUSED_RESULT
#endif /* __GNUC__ */
-#endif /* __CVC4_PUBLIC_H */
+#endif /* CVC4_PUBLIC_H */
#include "cvc4_private_library.h"
-#ifndef __CVC4__LIB__CLOCK_GETTIME_H
-#define __CVC4__LIB__CLOCK_GETTIME_H
+#ifndef CVC4__LIB__CLOCK_GETTIME_H
+#define CVC4__LIB__CLOCK_GETTIME_H
#include "lib/replacements.h"
#endif /* __cplusplus */
#endif /* HAVE_CLOCK_GETTIME */
-#endif /*__CVC4__LIB__CLOCK_GETTIME_H */
+#endif /*CVC4__LIB__CLOCK_GETTIME_H */
#include "cvc4_private.h"
-#ifndef __CVC4__LIB__FFS_H
-#define __CVC4__LIB__FFS_H
+#ifndef CVC4__LIB__FFS_H
+#define CVC4__LIB__FFS_H
//We include this for HAVE_FFS
#include "cvc4autoconfig.h"
#endif /* __cplusplus */
#endif /* HAVE_FFS */
-#endif /* __CVC4__LIB__FFS_H */
+#endif /* CVC4__LIB__FFS_H */
** Common header for replacement function sources.
**/
-#ifndef __CVC4__LIB__REPLACEMENTS_H
-#define __CVC4__LIB__REPLACEMENTS_H
+#ifndef CVC4__LIB__REPLACEMENTS_H
+#define CVC4__LIB__REPLACEMENTS_H
#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT)
# include "cvc4_private.h"
# endif
#endif
-#endif /* __CVC4__LIB__REPLACEMENTS_H */
+#endif /* CVC4__LIB__REPLACEMENTS_H */
#include "cvc4_private.h"
-#ifndef __CVC4__LIB__STRTOK_R_H
-#define __CVC4__LIB__STRTOK_R_H
+#ifndef CVC4__LIB__STRTOK_R_H
+#define CVC4__LIB__STRTOK_R_H
#ifdef HAVE_STRTOK_R
#endif /* __cplusplus */
#endif /* HAVE_STRTOK_R */
-#endif /* __CVC4__LIB__STRTOK_R_H */
+#endif /* CVC4__LIB__STRTOK_R_H */
** \brief An additional layer between commands and invoking them.
**/
-#ifndef __CVC4__MAIN__COMMAND_EXECUTOR_H
-#define __CVC4__MAIN__COMMAND_EXECUTOR_H
+#ifndef CVC4__MAIN__COMMAND_EXECUTOR_H
+#define CVC4__MAIN__COMMAND_EXECUTOR_H
#include <iosfwd>
#include <string>
}/* CVC4::main namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__MAIN__COMMAND_EXECUTOR_H */
+#endif /* CVC4__MAIN__COMMAND_EXECUTOR_H */
** threads.
**/
-#ifndef __CVC4__MAIN__COMMAND_EXECUTOR_PORTFOLIO_H
-#define __CVC4__MAIN__COMMAND_EXECUTOR_PORTFOLIO_H
+#ifndef CVC4__MAIN__COMMAND_EXECUTOR_PORTFOLIO_H
+#define CVC4__MAIN__COMMAND_EXECUTOR_PORTFOLIO_H
#include "main/command_executor.h"
#include "main/portfolio_util.h"
}/* CVC4::main namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__MAIN__COMMAND_EXECUTOR_PORTFOLIO_H */
+#endif /* CVC4__MAIN__COMMAND_EXECUTOR_PORTFOLIO_H */
** \brief Interactive shell for CVC4
**/
-#ifndef __CVC4__INTERACTIVE_SHELL_H
-#define __CVC4__INTERACTIVE_SHELL_H
+#ifndef CVC4__INTERACTIVE_SHELL_H
+#define CVC4__INTERACTIVE_SHELL_H
#include <iosfwd>
#include <string>
}/* CVC4 namespace */
-#endif /* __CVC4__INTERACTIVE_SHELL_H */
+#endif /* CVC4__INTERACTIVE_SHELL_H */
#include "util/statistics.h"
#include "util/statistics_registry.h"
-#ifndef __CVC4__MAIN__MAIN_H
-#define __CVC4__MAIN__MAIN_H
+#ifndef CVC4__MAIN__MAIN_H
+#define CVC4__MAIN__MAIN_H
namespace CVC4 {
namespace main {
int runCvc4(int argc, char* argv[], CVC4::Options&);
void printUsage(CVC4::Options&, bool full = false);
-#endif /* __CVC4__MAIN__MAIN_H */
+#endif /* CVC4__MAIN__MAIN_H */
** (potentially cooperative) race
**/
-#ifndef __CVC4__PORTFOLIO_H
-#define __CVC4__PORTFOLIO_H
+#ifndef CVC4__PORTFOLIO_H
+#define CVC4__PORTFOLIO_H
#include <boost/function.hpp>
#include <utility>
}/* CVC4 namespace */
-#endif /* __CVC4__PORTFOLIO_H */
+#endif /* CVC4__PORTFOLIO_H */
** \brief Code relevant only for portfolio builds
**/
-#ifndef __CVC4__PORTFOLIO_UTIL_H
-#define __CVC4__PORTFOLIO_UTIL_H
+#ifndef CVC4__PORTFOLIO_UTIL_H
+#define CVC4__PORTFOLIO_UTIL_H
#include <queue>
}/* CVC4 namespace */
-#endif /* __CVC4__PORTFOLIO_UTIL_H */
+#endif /* CVC4__PORTFOLIO_UTIL_H */
#include "cvc4_public.h"
-#ifndef __CVC4__OPTIONS__ARGUMENT_EXTENDER_H
-#define __CVC4__OPTIONS__ARGUMENT_EXTENDER_H
+#ifndef CVC4__OPTIONS__ARGUMENT_EXTENDER_H
+#define CVC4__OPTIONS__ARGUMENT_EXTENDER_H
#include <cstddef>
}/* CVC4::options namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__OPTIONS__ARGUMENT_EXTENDER_H */
+#endif /* CVC4__OPTIONS__ARGUMENT_EXTENDER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__OPTIONS__ARGUMENT_EXTENDER_IMPLEMENTATION_H
-#define __CVC4__OPTIONS__ARGUMENT_EXTENDER_IMPLEMENTATION_H
+#ifndef CVC4__OPTIONS__ARGUMENT_EXTENDER_IMPLEMENTATION_H
+#define CVC4__OPTIONS__ARGUMENT_EXTENDER_IMPLEMENTATION_H
#include <cstddef>
#include <list>
}/* CVC4::options namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__OPTIONS__ARGUMENT_EXTENDER_IMPLEMENTATION_H */
+#endif /* CVC4__OPTIONS__ARGUMENT_EXTENDER_IMPLEMENTATION_H */
#include "cvc4_public.h"
-#ifndef __CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H
-#define __CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H
+#ifndef CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H
+#define CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H
#include <iostream>
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H */
+#endif /* CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H */
#include "cvc4_public.h"
-#ifndef __CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H
-#define __CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H
+#ifndef CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H
+#define CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H
#include <iostream>
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H */
+#endif /* CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H */
#include "cvc4_public.h"
-#ifndef __CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H
-#define __CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H
+#ifndef CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H
+#define CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H
#include <iostream>
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H */
+#endif /* CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__BASE_HANDLERS_H
-#define __CVC4__BASE_HANDLERS_H
+#ifndef CVC4__BASE_HANDLERS_H
+#define CVC4__BASE_HANDLERS_H
#include <iostream>
#include <string>
}/* CVC4::options namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__BASE_HANDLERS_H */
+#endif /* CVC4__BASE_HANDLERS_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H
-#define __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H
+#ifndef CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H
+#define CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H
#include <iosfwd>
}
-#endif /* __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H */
+#endif /* CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BV__BITBLAST_MODE_H
-#define __CVC4__THEORY__BV__BITBLAST_MODE_H
+#ifndef CVC4__THEORY__BV__BITBLAST_MODE_H
+#define CVC4__THEORY__BV__BITBLAST_MODE_H
#include <iosfwd>
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__BV__BITBLAST_MODE_H */
+#endif /* CVC4__THEORY__BV__BITBLAST_MODE_H */
#include "cvc4_public.h"
-#ifndef __CVC4__BASE__DATATYPES_MODES_H
-#define __CVC4__BASE__DATATYPES_MODES_H
+#ifndef CVC4__BASE__DATATYPES_MODES_H
+#define CVC4__BASE__DATATYPES_MODES_H
#include <iostream>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__BASE__DATATYPES_MODES_H */
+#endif /* CVC4__BASE__DATATYPES_MODES_H */
#include "cvc4_private.h"
-#ifndef __CVC4__SMT__DECISION_MODE_H
-#define __CVC4__SMT__DECISION_MODE_H
+#ifndef CVC4__SMT__DECISION_MODE_H
+#define CVC4__SMT__DECISION_MODE_H
#include <iosfwd>
}/* CVC4 namespace */
-#endif /* __CVC4__SMT__DECISION_MODE_H */
+#endif /* CVC4__SMT__DECISION_MODE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__OPTIONS__DECISION_WEIGHT_H
-#define __CVC4__OPTIONS__DECISION_WEIGHT_H
+#ifndef CVC4__OPTIONS__DECISION_WEIGHT_H
+#define CVC4__OPTIONS__DECISION_WEIGHT_H
namespace CVC4 {
namespace decision {
}/* CVC4::decision namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__OPTIONS__DECISION_WEIGHT_H */
+#endif /* CVC4__OPTIONS__DECISION_WEIGHT_H */
#include "cvc4_public.h"
-#ifndef __CVC4__LANGUAGE_H
-#define __CVC4__LANGUAGE_H
+#ifndef CVC4__LANGUAGE_H
+#define CVC4__LANGUAGE_H
#include <sstream>
#include <string>
}/* CVC4::language namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__LANGUAGE_H */
+#endif /* CVC4__LANGUAGE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__OPTIONS__${id}$_H
-#define __CVC4__OPTIONS__${id}$_H
+#ifndef CVC4__OPTIONS__${id}$_H
+#define CVC4__OPTIONS__${id}$_H
#include "options/options.h"
} // namespace options
} // namespace CVC4
-#endif /* __CVC4__OPTIONS__${id}$_H */
+#endif /* CVC4__OPTIONS__${id}$_H */
#include "cvc4_private.h"
-#ifndef __CVC4__OPEN_OSTREAM_H
-#define __CVC4__OPEN_OSTREAM_H
+#ifndef CVC4__OPEN_OSTREAM_H
+#define CVC4__OPEN_OSTREAM_H
#include <map>
#include <ostream>
}/* CVC4 namespace */
-#endif /* __CVC4__OPEN_OSTREAM_H */
+#endif /* CVC4__OPEN_OSTREAM_H */
#include "cvc4_public.h"
-#ifndef __CVC4__OPTION_EXCEPTION_H
-#define __CVC4__OPTION_EXCEPTION_H
+#ifndef CVC4__OPTION_EXCEPTION_H
+#define CVC4__OPTION_EXCEPTION_H
#include "base/exception.h"
}/* CVC4 namespace */
-#endif /* __CVC4__OPTION_EXCEPTION_H */
+#endif /* CVC4__OPTION_EXCEPTION_H */
#include "cvc4_public.h"
-#ifndef __CVC4__OPTIONS__OPTIONS_H
-#define __CVC4__OPTIONS__OPTIONS_H
+#ifndef CVC4__OPTIONS__OPTIONS_H
+#define CVC4__OPTIONS__OPTIONS_H
#include <fstream>
#include <ostream>
}/* CVC4 namespace */
-#endif /* __CVC4__OPTIONS__OPTIONS_H */
+#endif /* CVC4__OPTIONS__OPTIONS_H */
#include "cvc4_private.h"
-#ifndef __CVC4__OPTIONS__OPTIONS_HANDLER_H
-#define __CVC4__OPTIONS__OPTIONS_HANDLER_H
+#ifndef CVC4__OPTIONS__OPTIONS_HANDLER_H
+#define CVC4__OPTIONS__OPTIONS_HANDLER_H
#include <ostream>
#include <string>
}/* CVC4::options namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__OPTIONS__OPTIONS_HANDLER_H */
+#endif /* CVC4__OPTIONS__OPTIONS_HANDLER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__OPTIONS__OPTIONS_HOLDER_H
-#define __CVC4__OPTIONS__OPTIONS_HOLDER_H
+#ifndef CVC4__OPTIONS__OPTIONS_HOLDER_H
+#define CVC4__OPTIONS__OPTIONS_HOLDER_H
${headers_module}$
} // namespace options
} // namespace CVC4
-#endif /* __CVC4__OPTIONS__OPTIONS_HOLDER_H */
+#endif /* CVC4__OPTIONS__OPTIONS_HOLDER_H */
#include "cvc4_public.h"
-#ifndef __CVC4__PRINTER__MODES_H
-#define __CVC4__PRINTER__MODES_H
+#ifndef CVC4__PRINTER__MODES_H
+#define CVC4__PRINTER__MODES_H
#include <iostream>
}/* CVC4 namespace */
-#endif /* __CVC4__PRINTER__MODEL_FORMAT_H */
+#endif /* CVC4__PRINTER__MODEL_FORMAT_H */
#include "cvc4_public.h"
-#ifndef __CVC4__BASE__QUANTIFIERS_MODES_H
-#define __CVC4__BASE__QUANTIFIERS_MODES_H
+#ifndef CVC4__BASE__QUANTIFIERS_MODES_H
+#define CVC4__BASE__QUANTIFIERS_MODES_H
#include <iostream>
}/* CVC4 namespace */
-#endif /* __CVC4__BASE__QUANTIFIERS_MODES_H */
+#endif /* CVC4__BASE__QUANTIFIERS_MODES_H */
#include "cvc4_public.h"
-#ifndef __CVC4__OPTIONS__SET_LANGUAGE_H
-#define __CVC4__OPTIONS__SET_LANGUAGE_H
+#ifndef CVC4__OPTIONS__SET_LANGUAGE_H
+#define CVC4__OPTIONS__SET_LANGUAGE_H
#include <iostream>
#include "options/language.h"
}/* CVC4::language namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__OPTIONS__SET_LANGUAGE_H */
+#endif /* CVC4__OPTIONS__SET_LANGUAGE_H */
#include "cvc4_public.h"
-#ifndef __CVC4__SMT__MODES_H
-#define __CVC4__SMT__MODES_H
+#ifndef CVC4__SMT__MODES_H
+#define CVC4__SMT__MODES_H
#include <iosfwd>
} // namespace CVC4
-#endif /* __CVC4__SMT__MODES_H */
+#endif /* CVC4__SMT__MODES_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__STRINGS__PROCESS_LOOP_MODE_H
-#define __CVC4__THEORY__STRINGS__PROCESS_LOOP_MODE_H
+#ifndef CVC4__THEORY__STRINGS__PROCESS_LOOP_MODE_H
+#define CVC4__THEORY__STRINGS__PROCESS_LOOP_MODE_H
#include <iosfwd>
} // namespace CVC4
-#endif /* __CVC4__THEORY__BV__BITBLAST_MODE_H */
+#endif /* CVC4__THEORY__BV__BITBLAST_MODE_H */
#include "cvc4_public.h"
-#ifndef __CVC4__SMT__SYGUS_OUT_MODE_H
-#define __CVC4__SMT__SYGUS_OUT_MODE_H
+#ifndef CVC4__SMT__SYGUS_OUT_MODE_H
+#define CVC4__SMT__SYGUS_OUT_MODE_H
#include <iosfwd>
} /* CVC4 namespace */
-#endif /* __CVC4__SMT__SYGUS_OUT_MODE_H */
+#endif /* CVC4__SMT__SYGUS_OUT_MODE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__BASE__UFSS_MODE_H
-#define __CVC4__BASE__UFSS_MODE_H
+#ifndef CVC4__BASE__UFSS_MODE_H
+#define CVC4__BASE__UFSS_MODE_H
namespace CVC4 {
namespace theory {
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__BASE__UFSS_MODE_H */
+#endif /* CVC4__BASE__UFSS_MODE_H */
** Base for ANTLR parser classes.
**/
-#ifndef __CVC4__PARSER__ANTLR_INPUT_H
-#define __CVC4__PARSER__ANTLR_INPUT_H
+#ifndef CVC4__PARSER__ANTLR_INPUT_H
+#define CVC4__PARSER__ANTLR_INPUT_H
#include "cvc4parser_private.h"
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PARSER__ANTLR_INPUT_H */
+#endif /* CVC4__PARSER__ANTLR_INPUT_H */
#include "cvc4parser_private.h"
-#ifndef __CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H
-#define __CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H
+#ifndef CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H
+#define CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H
#include <antlr3.h>
#include <istream>
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H */
+#endif /* CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H */
** \todo document this file
**/
-#ifndef __CVC4__PARSER__ANTLR_TRACING_H
-#define __CVC4__PARSER__ANTLR_TRACING_H
+#ifndef CVC4__PARSER__ANTLR_TRACING_H
+#define CVC4__PARSER__ANTLR_TRACING_H
// only enable the hack with -DCVC4_TRACE_ANTLR
#ifdef CVC4_TRACE_ANTLR
#endif /* CVC4_TRACE_ANTLR */
-#endif /* __CVC4__PARSER__ANTLR_TRACING_H */
+#endif /* CVC4__PARSER__ANTLR_TRACING_H */
#include "cvc4parser_private.h"
-#ifndef __CVC4__PARSER__BOUNDED_TOKEN_BUFFER_H
-#define __CVC4__PARSER__BOUNDED_TOKEN_BUFFER_H
+#ifndef CVC4__PARSER__BOUNDED_TOKEN_BUFFER_H
+#define CVC4__PARSER__BOUNDED_TOKEN_BUFFER_H
#include <antlr3defs.h>
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PARSER__BOUNDED_TOKEN_BUFFER_H */
+#endif /* CVC4__PARSER__BOUNDED_TOKEN_BUFFER_H */
#include "cvc4parser_private.h"
-#ifndef __CVC4__PARSER__BOUNDED_TOKEN_FACTORY_H
-#define __CVC4__PARSER__BOUNDED_TOKEN_FACTORY_H
+#ifndef CVC4__PARSER__BOUNDED_TOKEN_FACTORY_H
+#define CVC4__PARSER__BOUNDED_TOKEN_FACTORY_H
namespace CVC4 {
namespace parser {
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PARSER__BOUNDED_TOKEN_FACTORY_H */
+#endif /* CVC4__PARSER__BOUNDED_TOKEN_FACTORY_H */
#include "cvc4parser_private.h"
-#ifndef __CVC4__PARSER__CVC_INPUT_H
-#define __CVC4__PARSER__CVC_INPUT_H
+#ifndef CVC4__PARSER__CVC_INPUT_H
+#define CVC4__PARSER__CVC_INPUT_H
#include "parser/antlr_input.h"
#include "parser/cvc/CvcLexer.h"
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PARSER__CVC_INPUT_H */
+#endif /* CVC4__PARSER__CVC_INPUT_H */
#include "cvc4parser_public.h"
-#ifndef __CVC4__PARSER__INPUT_H
-#define __CVC4__PARSER__INPUT_H
+#ifndef CVC4__PARSER__INPUT_H
+#define CVC4__PARSER__INPUT_H
#include <iostream>
#include <stdio.h>
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PARSER__ANTLR_INPUT_H */
+#endif /* CVC4__PARSER__ANTLR_INPUT_H */
#include "cvc4parser_private.h"
-#ifndef __CVC4__PARSER__LINE_BUFFER_H
-#define __CVC4__PARSER__LINE_BUFFER_H
+#ifndef CVC4__PARSER__LINE_BUFFER_H
+#define CVC4__PARSER__LINE_BUFFER_H
#include <cstdlib>
#include <istream>
} // namespace parser
} // namespace CVC4
-#endif /* __CVC4__PARSER__LINE_BUFFER_H */
+#endif /* CVC4__PARSER__LINE_BUFFER_H */
#include "cvc4parser_private.h"
-#ifndef __CVC4__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H
-#define __CVC4__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H
+#ifndef CVC4__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H
+#define CVC4__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H
#include <antlr3input.h>
#include <string>
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H */
+#endif /* CVC4__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H */
#include "cvc4parser_public.h"
-#ifndef __CVC4__PARSER__PARSER_STATE_H
-#define __CVC4__PARSER__PARSER_STATE_H
+#ifndef CVC4__PARSER__PARSER_STATE_H
+#define CVC4__PARSER__PARSER_STATE_H
#include <string>
#include <set>
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PARSER__PARSER_STATE_H */
+#endif /* CVC4__PARSER__PARSER_STATE_H */
#include "cvc4parser_public.h"
-#ifndef __CVC4__PARSER__PARSER_BUILDER_H
-#define __CVC4__PARSER__PARSER_BUILDER_H
+#ifndef CVC4__PARSER__PARSER_BUILDER_H
+#define CVC4__PARSER__PARSER_BUILDER_H
#include <string>
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PARSER__PARSER_BUILDER_H */
+#endif /* CVC4__PARSER__PARSER_BUILDER_H */
#include "cvc4parser_public.h"
-#ifndef __CVC4__PARSER__PARSER_EXCEPTION_H
-#define __CVC4__PARSER__PARSER_EXCEPTION_H
+#ifndef CVC4__PARSER__PARSER_EXCEPTION_H
+#define CVC4__PARSER__PARSER_EXCEPTION_H
#include <iostream>
#include <string>
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PARSER__PARSER_EXCEPTION_H */
+#endif /* CVC4__PARSER__PARSER_EXCEPTION_H */
#include "cvc4parser_private.h"
-#ifndef __CVC4__PARSER__SMT1_H
-#define __CVC4__PARSER__SMT1_H
+#ifndef CVC4__PARSER__SMT1_H
+#define CVC4__PARSER__SMT1_H
#include <string>
#include <unordered_map>
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PARSER__SMT1_H */
+#endif /* CVC4__PARSER__SMT1_H */
#include "cvc4parser_private.h"
-#ifndef __CVC4__PARSER__SMT1_INPUT_H
-#define __CVC4__PARSER__SMT1_INPUT_H
+#ifndef CVC4__PARSER__SMT1_INPUT_H
+#define CVC4__PARSER__SMT1_INPUT_H
#include "parser/antlr_input.h"
#include "parser/smt1/Smt1Lexer.h"
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PARSER__SMT1_INPUT_H */
+#endif /* CVC4__PARSER__SMT1_INPUT_H */
#include "cvc4parser_private.h"
-#ifndef __CVC4__PARSER__SMT2_H
-#define __CVC4__PARSER__SMT2_H
+#ifndef CVC4__PARSER__SMT2_H
+#define CVC4__PARSER__SMT2_H
#include <sstream>
#include <stack>
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PARSER__SMT2_H */
+#endif /* CVC4__PARSER__SMT2_H */
#include "cvc4parser_private.h"
-#ifndef __CVC4__PARSER__SMT2_INPUT_H
-#define __CVC4__PARSER__SMT2_INPUT_H
+#ifndef CVC4__PARSER__SMT2_INPUT_H
+#define CVC4__PARSER__SMT2_INPUT_H
#include "parser/antlr_input.h"
#include "parser/smt2/Smt2Lexer.h"
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PARSER__SMT2_INPUT_H */
+#endif /* CVC4__PARSER__SMT2_INPUT_H */
#include "cvc4parser_private.h"
-#ifndef __CVC4__PARSER__SYGUS_INPUT_H
-#define __CVC4__PARSER__SYGUS_INPUT_H
+#ifndef CVC4__PARSER__SYGUS_INPUT_H
+#define CVC4__PARSER__SYGUS_INPUT_H
#include "parser/antlr_input.h"
#include "parser/smt2/Smt2Lexer.h"
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PARSER__SYGUS_INPUT_H */
+#endif /* CVC4__PARSER__SYGUS_INPUT_H */
#include "cvc4parser_private.h"
-#ifndef __CVC4__PARSER__TPTP_H
-#define __CVC4__PARSER__TPTP_H
+#ifndef CVC4__PARSER__TPTP_H
+#define CVC4__PARSER__TPTP_H
#include <cassert>
#include <unordered_map>
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PARSER__TPTP_INPUT_H */
+#endif /* CVC4__PARSER__TPTP_INPUT_H */
#include "cvc4parser_private.h"
-#ifndef __CVC4__PARSER__TPTP_INPUT_H
-#define __CVC4__PARSER__TPTP_INPUT_H
+#ifndef CVC4__PARSER__TPTP_INPUT_H
+#define CVC4__PARSER__TPTP_INPUT_H
#include "parser/antlr_input.h"
#include "parser/tptp/TptpLexer.h"
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PARSER__TPTP_INPUT_H */
+#endif /* CVC4__PARSER__TPTP_INPUT_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__ASSERTION_PIPELINE_H
-#define __CVC4__PREPROCESSING__ASSERTION_PIPELINE_H
+#ifndef CVC4__PREPROCESSING__ASSERTION_PIPELINE_H
+#define CVC4__PREPROCESSING__ASSERTION_PIPELINE_H
#include <vector>
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__ASSERTION_PIPELINE_H */
+#endif /* CVC4__PREPROCESSING__ASSERTION_PIPELINE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H
-#define __CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H
+#ifndef CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H
+#define CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H
-#define __CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H
+#ifndef CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H
+#define CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H
#include <unordered_map>
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H */
+#endif /* CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
-#define __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
+#ifndef CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
+#define CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H */
+#endif /* CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H
-#define __CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H
+#ifndef CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H
+#define CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H */
+#endif /* CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H
-#define __CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H
+#ifndef CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H
+#define CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H
#include <unordered_map>
#include "expr/node.h"
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H
-#define __CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H
+#ifndef CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H
+#define CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H */
+#endif /* CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H
-#define __CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H
+#ifndef CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H
+#define CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H
-#define __CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H
+#ifndef CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H
+#define CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H */
+#endif /* CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H
-#define __CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H
+#ifndef CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H
+#define CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H */
+#endif /* CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H
-#define __CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H
+#ifndef CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H
+#define CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H */
+#endif /* CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H
-#define __CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H
+#ifndef CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H
+#define CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING_PASSES__GLOBAL_NEGATE_H */
+#endif /* CVC4__PREPROCESSING_PASSES__GLOBAL_NEGATE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__INT_TO_BV_H
-#define __CVC4__PREPROCESSING__PASSES__INT_TO_BV_H
+#ifndef CVC4__PREPROCESSING__PASSES__INT_TO_BV_H
+#define CVC4__PREPROCESSING__PASSES__INT_TO_BV_H
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PASSES__INT_TO_BV_H */
+#endif /* CVC4__PREPROCESSING__PASSES__INT_TO_BV_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H
-#define __CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H
+#ifndef CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H
+#define CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H
#include <unordered_set>
#include <vector>
} // namespace preprocessing
} // namespace CVC4
-#endif // __CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H
+#endif // CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__ITE_SIMP_H
-#define __CVC4__PREPROCESSING__PASSES__ITE_SIMP_H
+#ifndef CVC4__PREPROCESSING__PASSES__ITE_SIMP_H
+#define CVC4__PREPROCESSING__PASSES__ITE_SIMP_H
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H
-#define __CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H
+#ifndef CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H
+#define CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H */
+#endif /* CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H
-#define __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H
+#ifndef CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H
+#define CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H
#include <unordered_map>
#include <vector>
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H */
+#endif /* CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H
-#define __CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H
+#ifndef CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H
+#define CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H
#include <vector>
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
-#define __CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
+#ifndef CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
+#define CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
#include <unordered_set>
#include <vector>
} // namespace preprocessing
} // namespace CVC4
-#endif // __CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
+#endif // CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H
-#define __CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H
+#ifndef CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H
+#define CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H
#include <map>
#include <string>
} // preprocessing
} // CVC4
-#endif /*__CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H */
+#endif /*CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H
-#define __CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H
+#ifndef CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H
+#define CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H */
+#endif /* CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H
-#define __CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H
+#ifndef CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H
+#define CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H
#include <unordered_map>
#include <vector>
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H */
+#endif /* CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__REWRITE_H
-#define __CVC4__PREPROCESSING__PASSES__REWRITE_H
+#ifndef CVC4__PREPROCESSING__PASSES__REWRITE_H
+#define CVC4__PREPROCESSING__PASSES__REWRITE_H
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PASSES__REWRITE_H */
+#endif /* CVC4__PREPROCESSING__PASSES__REWRITE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H
-#define __CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H
+#ifndef CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H
+#define CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H */
+#endif /* CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H */
** \brief Sort inference preprocessing pass
**/
-#ifndef __CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_
-#define __CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_
+#ifndef CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_
+#define CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_
#include <map>
#include <string>
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ */
+#endif /* CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H
-#define __CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H
+#ifndef CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H
+#define CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H */
+#endif /* CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H */
** input into an abduction problem.
**/
-#ifndef __CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H
-#define __CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H
+#ifndef CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H
+#define CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H_ */
+#endif /* CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H_ */
** \brief SygusInference
**/
-#ifndef __CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_
-#define __CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_
+#ifndef CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_
+#define CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_
#include <map>
#include <string>
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ */
+#endif /* CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ */
** \brief Symmetry breaker for theories
**/
-#ifndef __CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_
-#define __CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_
+#ifndef CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_
+#define CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_
#include <map>
#include <string>
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_ */
+#endif /* CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_ */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__SYMMETRY_DETECT_H
-#define __CVC4__PREPROCESSING__PASSES__SYMMETRY_DETECT_H
+#ifndef CVC4__PREPROCESSING__PASSES__SYMMETRY_DETECT_H
+#define CVC4__PREPROCESSING__PASSES__SYMMETRY_DETECT_H
#include <map>
#include <string>
** where t1 and t2 are subterms of the input.
**/
-#ifndef __CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H
-#define __CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H
+#ifndef CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H
+#define CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H */
+#endif /* CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H
-#define __CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H
+#ifndef CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H
+#define CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H */
+#endif /* CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H
-#define __CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H
+#ifndef CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H
+#define CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H
#include <unordered_map>
#include <unordered_set>
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_H
-#define __CVC4__PREPROCESSING__PREPROCESSING_PASS_H
+#ifndef CVC4__PREPROCESSING__PREPROCESSING_PASS_H
+#define CVC4__PREPROCESSING__PREPROCESSING_PASS_H
#include <string>
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PREPROCESSING_PASS_H */
+#endif /* CVC4__PREPROCESSING__PREPROCESSING_PASS_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
-#define __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
+#ifndef CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
+#define CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
#include "context/cdo.h"
#include "context/context.h"
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H */
+#endif /* CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H */
**/
#include "cvc4_private.h"
-#ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H
-#define __CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H
+#ifndef CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H
+#define CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H
#include <memory>
#include <string>
} // namespace preprocessing
} // namespace CVC4
-#endif /* __CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H */
+#endif /* CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H */
#include "cvc4_private.h"
-#ifndef __CVC4__ITE_UTILITIES_H
-#define __CVC4__ITE_UTILITIES_H
+#ifndef CVC4__ITE_UTILITIES_H
+#define CVC4__ITE_UTILITIES_H
#include <unordered_map>
#include <vector>
#include "cvc4_private.h"
-#ifndef __CVC4__PRINTER__AST_PRINTER_H
-#define __CVC4__PRINTER__AST_PRINTER_H
+#ifndef CVC4__PRINTER__AST_PRINTER_H
+#define CVC4__PRINTER__AST_PRINTER_H
#include <iostream>
}/* CVC4::printer namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PRINTER__AST_PRINTER_H */
+#endif /* CVC4__PRINTER__AST_PRINTER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PRINTER__CVC_PRINTER_H
-#define __CVC4__PRINTER__CVC_PRINTER_H
+#ifndef CVC4__PRINTER__CVC_PRINTER_H
+#define CVC4__PRINTER__CVC_PRINTER_H
#include <iostream>
}/* CVC4::printer namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PRINTER__CVC_PRINTER_H */
+#endif /* CVC4__PRINTER__CVC_PRINTER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PRINTER__DAGIFICATION_VISITOR_H
-#define __CVC4__PRINTER__DAGIFICATION_VISITOR_H
+#ifndef CVC4__PRINTER__DAGIFICATION_VISITOR_H
+#define CVC4__PRINTER__DAGIFICATION_VISITOR_H
#include <string>
#include <unordered_map>
}/* CVC4::printer namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PRINTER__DAGIFICATION_VISITOR_H */
+#endif /* CVC4__PRINTER__DAGIFICATION_VISITOR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PRINTER__PRINTER_H
-#define __CVC4__PRINTER__PRINTER_H
+#ifndef CVC4__PRINTER__PRINTER_H
+#define CVC4__PRINTER__PRINTER_H
#include <map>
#include <string>
} // namespace CVC4
-#endif /* __CVC4__PRINTER__PRINTER_H */
+#endif /* CVC4__PRINTER__PRINTER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PRINTER__SMT2_PRINTER_H
-#define __CVC4__PRINTER__SMT2_PRINTER_H
+#ifndef CVC4__PRINTER__SMT2_PRINTER_H
+#define CVC4__PRINTER__SMT2_PRINTER_H
#include <iostream>
}/* CVC4::printer namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PRINTER__SMT2_PRINTER_H */
+#endif /* CVC4__PRINTER__SMT2_PRINTER_H */
#include "cvc4_public.h"
-#ifndef __CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H
-#define __CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H
+#ifndef CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H
+#define CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H
#include <vector>
} /* CVC4::printer namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H */
+#endif /* CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PRINTER__TPTP_PRINTER_H
-#define __CVC4__PRINTER__TPTP_PRINTER_H
+#ifndef CVC4__PRINTER__TPTP_PRINTER_H
+#define CVC4__PRINTER__TPTP_PRINTER_H
#include <iostream>
}/* CVC4::printer namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PRINTER__TPTP_PRINTER_H */
+#endif /* CVC4__PRINTER__TPTP_PRINTER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__ARITH__PROOF_H
-#define __CVC4__ARITH__PROOF_H
+#ifndef CVC4__ARITH__PROOF_H
+#define CVC4__ARITH__PROOF_H
#include <memory>
#include <unordered_set>
}/* CVC4 namespace */
-#endif /* __CVC4__ARITH__PROOF_H */
+#endif /* CVC4__ARITH__PROOF_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PROOF__ARITH_PROOF_RECORDER_H
-#define __CVC4__PROOF__ARITH_PROOF_RECORDER_H
+#ifndef CVC4__PROOF__ARITH_PROOF_RECORDER_H
+#define CVC4__PROOF__ARITH_PROOF_RECORDER_H
#include <map>
#include <set>
#include "cvc4_private.h"
-#ifndef __CVC4__ARRAY__PROOF_H
-#define __CVC4__ARRAY__PROOF_H
+#ifndef CVC4__ARRAY__PROOF_H
+#define CVC4__ARRAY__PROOF_H
#include <memory>
#include <unordered_set>
}/* CVC4 namespace */
-#endif /* __CVC4__ARRAY__PROOF_H */
+#endif /* CVC4__ARRAY__PROOF_H */
#include "cvc4_private.h"
-#ifndef __CVC4__BITVECTOR_PROOF_H
-#define __CVC4__BITVECTOR_PROOF_H
+#ifndef CVC4__BITVECTOR_PROOF_H
+#define CVC4__BITVECTOR_PROOF_H
#include <set>
#include <unordered_map>
}/* CVC4 namespace */
-#endif /* __CVC4__BITVECTOR__PROOF_H */
+#endif /* CVC4__BITVECTOR__PROOF_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
-#define __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
+#ifndef CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
+#define CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
#include <iostream>
#include <sstream>
} // namespace CVC4
-#endif /* __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H */
+#endif /* CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PROOF__CLAUSE_ID_H
-#define __CVC4__PROOF__CLAUSE_ID_H
+#ifndef CVC4__PROOF__CLAUSE_ID_H
+#define CVC4__PROOF__CLAUSE_ID_H
namespace CVC4 {
}/* CVC4 namespace */
-#endif /* __CVC4__PROOF__CLAUSE_ID_H */
+#endif /* CVC4__PROOF__CLAUSE_ID_H */
#include "cvc4_private.h"
-#ifndef __CVC4__CNF_PROOF_H
-#define __CVC4__CNF_PROOF_H
+#ifndef CVC4__CNF_PROOF_H
+#define CVC4__CNF_PROOF_H
#include <iosfwd>
#include <unordered_map>
} /* CVC4 namespace */
-#endif /* __CVC4__CNF_PROOF_H */
+#endif /* CVC4__CNF_PROOF_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PROOF__DIMACS_PRINTER_H
-#define __CVC4__PROOF__DIMACS_PRINTER_H
+#ifndef CVC4__PROOF__DIMACS_PRINTER_H
+#define CVC4__PROOF__DIMACS_PRINTER_H
#include <iosfwd>
#include <memory>
} // namespace proof
} // namespace CVC4
-#endif // __CVC4__PROOF__DIMACS_PRINTER_H
+#endif // CVC4__PROOF__DIMACS_PRINTER_H
**
**/
-#ifndef __CVC4__PROOF__DRAT__DRAT_PROOF_H
-#define __CVC4__PROOF__DRAT__DRAT_PROOF_H
+#ifndef CVC4__PROOF__DRAT__DRAT_PROOF_H
+#define CVC4__PROOF__DRAT__DRAT_PROOF_H
#include "cvc4_private.h"
#include "prop/sat_solver.h"
} // namespace proof
} // namespace CVC4
-#endif // __CVC4__PROOF__DRAT__DRAT_PROOF_H
+#endif // CVC4__PROOF__DRAT__DRAT_PROOF_H
#include "cvc4_private.h"
-#ifndef __CVC4__PROOF__ER__ER_PROOF_H
-#define __CVC4__PROOF__ER__ER_PROOF_H
+#ifndef CVC4__PROOF__ER__ER_PROOF_H
+#define CVC4__PROOF__ER__ER_PROOF_H
#include <memory>
#include <vector>
} // namespace proof
} // namespace CVC4
-#endif // __CVC4__PROOF__ER__ER_PROOF_H
+#endif // CVC4__PROOF__ER__ER_PROOF_H
#include "cvc4_private.h"
-#ifndef __CVC4__LEMMA_PROOF_H
-#define __CVC4__LEMMA_PROOF_H
+#ifndef CVC4__LEMMA_PROOF_H
+#define CVC4__LEMMA_PROOF_H
#include "expr/expr.h"
#include "proof/clause_id.h"
} /* CVC4 namespace */
-#endif /* __CVC4__LEMMA_PROOF_H */
+#endif /* CVC4__LEMMA_PROOF_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PROOF__LFSC_PROOF_PRINTER_H
-#define __CVC4__PROOF__LFSC_PROOF_PRINTER_H
+#ifndef CVC4__PROOF__LFSC_PROOF_PRINTER_H
+#define CVC4__PROOF__LFSC_PROOF_PRINTER_H
#include <iosfwd>
#include <string>
} // namespace proof
} // namespace CVC4
-#endif /* __CVC4__PROOF__LFSC_PROOF_PRINTER_H */
+#endif /* CVC4__PROOF__LFSC_PROOF_PRINTER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PROOF__LRAT__LRAT_PROOF_H
-#define __CVC4__PROOF__LRAT__LRAT_PROOF_H
+#ifndef CVC4__PROOF__LRAT__LRAT_PROOF_H
+#define CVC4__PROOF__LRAT__LRAT_PROOF_H
#include <iosfwd>
#include <string>
#include "cvc4_private.h"
-#ifndef __CVC4__PROOF__PROOF_H
-#define __CVC4__PROOF__PROOF_H
+#ifndef CVC4__PROOF__PROOF_H
+#define CVC4__PROOF__PROOF_H
#include "options/smt_options.h"
# define PSTATS(x)
#endif /* CVC4_PROOF_STATS */
-#endif /* __CVC4__PROOF__PROOF_H */
+#endif /* CVC4__PROOF__PROOF_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PROOF_MANAGER_H
-#define __CVC4__PROOF_MANAGER_H
+#ifndef CVC4__PROOF_MANAGER_H
+#define CVC4__PROOF_MANAGER_H
#include <iosfwd>
#include <memory>
-#endif /* __CVC4__PROOF_MANAGER_H */
+#endif /* CVC4__PROOF_MANAGER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PROOF_OUTPUT_CHANNEL_H
-#define __CVC4__PROOF_OUTPUT_CHANNEL_H
+#ifndef CVC4__PROOF_OUTPUT_CHANNEL_H
+#define CVC4__PROOF_OUTPUT_CHANNEL_H
#include <memory>
#include <set>
} /* CVC4 namespace */
-#endif /* __CVC4__PROOF_OUTPUT_CHANNEL_H */
+#endif /* CVC4__PROOF_OUTPUT_CHANNEL_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H
-#define __CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H
+#ifndef CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H
+#define CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H
#include <iosfwd>
} // namespace CVC4
-#endif /* __CVC4__PROOF__RESOLUTIONBITVECTORPROOF_H */
+#endif /* CVC4__PROOF__RESOLUTIONBITVECTORPROOF_H */
#include "cvc4_private.h"
-#ifndef __CVC4__SAT__PROOF_H
-#define __CVC4__SAT__PROOF_H
+#ifndef CVC4__SAT__PROOF_H
+#define CVC4__SAT__PROOF_H
#include <stdint.h>
} /* CVC4 namespace */
-#endif /* __CVC4__SAT__PROOF_H */
+#endif /* CVC4__SAT__PROOF_H */
#include "cvc4_private.h"
-#ifndef __CVC4__SAT__PROOF_IMPLEMENTATION_H
-#define __CVC4__SAT__PROOF_IMPLEMENTATION_H
+#ifndef CVC4__SAT__PROOF_IMPLEMENTATION_H
+#define CVC4__SAT__PROOF_IMPLEMENTATION_H
#include "proof/clause_id.h"
#include "proof/cnf_proof.h"
} /* CVC4 namespace */
-#endif /* __CVC4__SAT__PROOF_IMPLEMENTATION_H */
+#endif /* CVC4__SAT__PROOF_IMPLEMENTATION_H */
#include "cvc4_private.h"
-#ifndef __CVC4__SIMPLIFY_BOOLEAN_NODE_H
-#define __CVC4__SIMPLIFY_BOOLEAN_NODE_H
+#ifndef CVC4__SIMPLIFY_BOOLEAN_NODE_H
+#define CVC4__SIMPLIFY_BOOLEAN_NODE_H
namespace CVC4 {
}/* CVC4 namespace */
-#endif /* __CVC4__SIMPLIFY_BOOLEAN_NODE_H */
+#endif /* CVC4__SIMPLIFY_BOOLEAN_NODE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__SKOLEMIZATION_MANAGER_H
-#define __CVC4__SKOLEMIZATION_MANAGER_H
+#ifndef CVC4__SKOLEMIZATION_MANAGER_H
+#define CVC4__SKOLEMIZATION_MANAGER_H
#include <iostream>
#include <unordered_map>
-#endif /* __CVC4__SKOLEMIZATION_MANAGER_H */
+#endif /* CVC4__SKOLEMIZATION_MANAGER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY_PROOF_H
-#define __CVC4__THEORY_PROOF_H
+#ifndef CVC4__THEORY_PROOF_H
+#define CVC4__THEORY_PROOF_H
#include <iosfwd>
#include <unordered_map>
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY_PROOF_H */
+#endif /* CVC4__THEORY_PROOF_H */
#include "cvc4_private.h"
-#ifndef __CVC4__UF__PROOF_H
-#define __CVC4__UF__PROOF_H
+#ifndef CVC4__UF__PROOF_H
+#define CVC4__UF__PROOF_H
#include <memory>
#include <unordered_set>
}/* CVC4 namespace */
-#endif /* __CVC4__UF__PROOF_H */
+#endif /* CVC4__UF__PROOF_H */
#include "cvc4_public.h"
-#ifndef __CVC4__UNSAT_CORE_H
-#define __CVC4__UNSAT_CORE_H
+#ifndef CVC4__UNSAT_CORE_H
+#define CVC4__UNSAT_CORE_H
#include <iosfwd>
#include <vector>
}/* CVC4 namespace */
-#endif /* __CVC4__UNSAT_CORE_H */
+#endif /* CVC4__UNSAT_CORE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PROP__BVSATSOLVERNOTIFY_H
-#define __CVC4__PROP__BVSATSOLVERNOTIFY_H
+#ifndef CVC4__PROP__BVSATSOLVERNOTIFY_H
+#define CVC4__PROP__BVSATSOLVERNOTIFY_H
#include "prop/sat_solver_types.h"
#include "cvc4_private.h"
-#ifndef __CVC4__PROP__CADICAL_H
-#define __CVC4__PROP__CADICAL_H
+#ifndef CVC4__PROP__CADICAL_H
+#define CVC4__PROP__CADICAL_H
#ifdef CVC4_USE_CADICAL
} // namespace CVC4
#endif // CVC4_USE_CADICAL
-#endif // __CVC4__PROP__CADICAL_H
+#endif // CVC4__PROP__CADICAL_H
#include "cvc4_private.h"
-#ifndef __CVC4__PROP__CNF_STREAM_H
-#define __CVC4__PROP__CNF_STREAM_H
+#ifndef CVC4__PROP__CNF_STREAM_H
+#define CVC4__PROP__CNF_STREAM_H
#include "context/cdinsert_hashmap.h"
#include "context/cdlist.h"
} /* CVC4::prop namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__PROP__CNF_STREAM_H */
+#endif /* CVC4__PROP__CNF_STREAM_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PROP__CRYPTOMINISAT_H
-#define __CVC4__PROP__CRYPTOMINISAT_H
+#ifndef CVC4__PROP__CRYPTOMINISAT_H
+#define CVC4__PROP__CRYPTOMINISAT_H
#ifdef CVC4_USE_CRYPTOMINISAT
} // namespace CVC4
#endif // CVC4_USE_CRYPTOMINISAT
-#endif // __CVC4__PROP__CRYPTOMINISAT_H
+#endif // CVC4__PROP__CRYPTOMINISAT_H
#include "cvc4_private.h"
-#ifndef __CVC4__PROP_ENGINE_H
-#define __CVC4__PROP_ENGINE_H
+#ifndef CVC4__PROP_ENGINE_H
+#define CVC4__PROP_ENGINE_H
#include <sys/time.h>
}/* CVC4::prop namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PROP_ENGINE_H */
+#endif /* CVC4__PROP_ENGINE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PROP__REGISTRAR_H
-#define __CVC4__PROP__REGISTRAR_H
+#ifndef CVC4__PROP__REGISTRAR_H
+#define CVC4__PROP__REGISTRAR_H
namespace CVC4 {
namespace prop {
}/* CVC4::prop namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PROP__REGISTRAR_H */
+#endif /* CVC4__PROP__REGISTRAR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PROP__SAT_SOLVER_H
-#define __CVC4__PROP__SAT_SOLVER_H
+#ifndef CVC4__PROP__SAT_SOLVER_H
+#define CVC4__PROP__SAT_SOLVER_H
#include <stdint.h>
}/* CVC4::prop namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PROP__SAT_MODULE_H */
+#endif /* CVC4__PROP__SAT_MODULE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__PROP__SAT_SOLVER_FACTORY_H
-#define __CVC4__PROP__SAT_SOLVER_FACTORY_H
+#ifndef CVC4__PROP__SAT_SOLVER_FACTORY_H
+#define CVC4__PROP__SAT_SOLVER_FACTORY_H
#include <string>
#include <vector>
} // namespace prop
} // namespace CVC4
-#endif // __CVC4__PROP__SAT_SOLVER_FACTORY_H
+#endif // CVC4__PROP__SAT_SOLVER_FACTORY_H
#include "cvc4_private.h"
-#ifndef __CVC4__PROP__SAT_H
-#define __CVC4__PROP__SAT_H
+#ifndef CVC4__PROP__SAT_H
+#define CVC4__PROP__SAT_H
// Just defining this for now, since there's no other SAT solver bindings.
// Optional blocks below will be unconditionally included
-#define __CVC4_USE_MINISAT
+#define CVC4_USE_MINISAT
#include <iosfwd>
#include <unordered_set>
}/* CVC4 namespace */
-#endif /* __CVC4__PROP__SAT_H */
+#endif /* CVC4__PROP__SAT_H */
#include "cvc4_public.h"
-#ifndef __CVC4__COMMAND_H
-#define __CVC4__COMMAND_H
+#ifndef CVC4__COMMAND_H
+#define CVC4__COMMAND_H
#include <iosfwd>
#include <map>
} /* CVC4 namespace */
-#endif /* __CVC4__COMMAND_H */
+#endif /* CVC4__COMMAND_H */
#include "cvc4_private.h"
-#ifndef __CVC4__SMT__COMMAND_LIST_H
-#define __CVC4__SMT__COMMAND_LIST_H
+#ifndef CVC4__SMT__COMMAND_LIST_H
+#define CVC4__SMT__COMMAND_LIST_H
#include "context/cdlist.h"
}/* CVC4::smt namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__SMT__COMMAND_LIST_H */
+#endif /* CVC4__SMT__COMMAND_LIST_H */
#include "cvc4_private.h"
-#ifndef __CVC4__DUMP_H
-#define __CVC4__DUMP_H
+#ifndef CVC4__DUMP_H
+#define CVC4__DUMP_H
#include "base/output.h"
#include "smt/command.h"
}/* CVC4 namespace */
-#endif /* __CVC4__DUMP_H */
+#endif /* CVC4__DUMP_H */
#include "cvc4_public.h"
-#ifndef __CVC4__SMT__LOGIC_EXCEPTION_H
-#define __CVC4__SMT__LOGIC_EXCEPTION_H
+#ifndef CVC4__SMT__LOGIC_EXCEPTION_H
+#define CVC4__SMT__LOGIC_EXCEPTION_H
#include "base/exception.h"
}/* CVC4 namespace */
-#endif /* __CVC4__SMT__LOGIC_EXCEPTION_H */
+#endif /* CVC4__SMT__LOGIC_EXCEPTION_H */
#include "cvc4_private.h"
-#ifndef __CVC4__LOGIC_REQUEST_H
-#define __CVC4__LOGIC_REQUEST_H
+#ifndef CVC4__LOGIC_REQUEST_H
+#define CVC4__LOGIC_REQUEST_H
#include "expr/kind.h"
}/* CVC4 namespace */
-#endif /* __CVC4__LOGIC_REQUEST_H */
+#endif /* CVC4__LOGIC_REQUEST_H */
#include "cvc4_private.h"
-#ifndef __CVC4__MANAGED_OSTREAMS_H
-#define __CVC4__MANAGED_OSTREAMS_H
+#ifndef CVC4__MANAGED_OSTREAMS_H
+#define CVC4__MANAGED_OSTREAMS_H
#include <ostream>
}/* CVC4 namespace */
-#endif /* __CVC4__MANAGED_OSTREAMS_H */
+#endif /* CVC4__MANAGED_OSTREAMS_H */
#include "cvc4_private.h"
-#ifndef __CVC4__MODEL_H
-#define __CVC4__MODEL_H
+#ifndef CVC4__MODEL_H
+#define CVC4__MODEL_H
#include <iosfwd>
#include <vector>
}/* CVC4 namespace */
-#endif /* __CVC4__MODEL_H */
+#endif /* CVC4__MODEL_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__MODEL_CORE_BUILDER_H
-#define __CVC4__THEORY__MODEL_CORE_BUILDER_H
+#ifndef CVC4__THEORY__MODEL_CORE_BUILDER_H
+#define CVC4__THEORY__MODEL_CORE_BUILDER_H
#include <vector>
} // namespace CVC4
-#endif /* __CVC4__THEORY__MODEL_CORE_BUILDER_H */
+#endif /* CVC4__THEORY__MODEL_CORE_BUILDER_H */
#include "cvc4_public.h"
-#ifndef __CVC4__SMT_ENGINE_H
-#define __CVC4__SMT_ENGINE_H
+#ifndef CVC4__SMT_ENGINE_H
+#define CVC4__SMT_ENGINE_H
#include <string>
#include <vector>
}/* CVC4 namespace */
-#endif /* __CVC4__SMT_ENGINE_H */
+#endif /* CVC4__SMT_ENGINE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__SMT__SMT_ENGINE_SCOPE_H
-#define __CVC4__SMT__SMT_ENGINE_SCOPE_H
+#ifndef CVC4__SMT__SMT_ENGINE_SCOPE_H
+#define CVC4__SMT__SMT_ENGINE_SCOPE_H
#include "expr/node_manager.h"
}/* CVC4::smt namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__SMT__SMT_ENGINE_SCOPE_H */
+#endif /* CVC4__SMT__SMT_ENGINE_SCOPE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__UPDATE_OSTREAM_H
-#define __CVC4__UPDATE_OSTREAM_H
+#ifndef CVC4__UPDATE_OSTREAM_H
+#define CVC4__UPDATE_OSTREAM_H
#include <ostream>
}/* CVC4 namespace */
-#endif /* __CVC4__UPDATE_OSTREAM_H */
+#endif /* CVC4__UPDATE_OSTREAM_H */
#include "cvc4_private.h"
-#ifndef __CVC4__BOOLEAN_SIMPLIFICATION_H
-#define __CVC4__BOOLEAN_SIMPLIFICATION_H
+#ifndef CVC4__BOOLEAN_SIMPLIFICATION_H
+#define CVC4__BOOLEAN_SIMPLIFICATION_H
#include <vector>
#include <algorithm>
}/* CVC4 namespace */
-#endif /* __CVC4__BOOLEAN_SIMPLIFICATION_H */
+#endif /* CVC4__BOOLEAN_SIMPLIFICATION_H */
#include "cvc4_public.h"
-#ifndef __CVC4__SMT_UTIL__LEMMA_CHANNELS_H
-#define __CVC4__SMT_UTIL__LEMMA_CHANNELS_H
+#ifndef CVC4__SMT_UTIL__LEMMA_CHANNELS_H
+#define CVC4__SMT_UTIL__LEMMA_CHANNELS_H
#include <iosfwd>
#include <string>
} /* namespace CVC4 */
-#endif /* __CVC4__SMT_UTIL__LEMMA_CHANNELS_H */
+#endif /* CVC4__SMT_UTIL__LEMMA_CHANNELS_H */
#include "cvc4_public.h"
-#ifndef __CVC4__LEMMA_INPUT_CHANNEL_H
-#define __CVC4__LEMMA_INPUT_CHANNEL_H
+#ifndef CVC4__LEMMA_INPUT_CHANNEL_H
+#define CVC4__LEMMA_INPUT_CHANNEL_H
#include "expr/expr.h"
}/* CVC4 namespace */
-#endif /* __CVC4__LEMMA_INPUT_CHANNEL_H */
+#endif /* CVC4__LEMMA_INPUT_CHANNEL_H */
#include "cvc4_public.h"
-#ifndef __CVC4__LEMMA_OUTPUT_CHANNEL_H
-#define __CVC4__LEMMA_OUTPUT_CHANNEL_H
+#ifndef CVC4__LEMMA_OUTPUT_CHANNEL_H
+#define CVC4__LEMMA_OUTPUT_CHANNEL_H
#include "expr/expr.h"
}/* CVC4 namespace */
-#endif /* __CVC4__LEMMA_OUTPUT_CHANNEL_H */
+#endif /* CVC4__LEMMA_OUTPUT_CHANNEL_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
-#define __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
+#ifndef CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
+#define CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
#include <unordered_map>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H */
+#endif /* CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ARITH__MSUM_H
-#define __CVC4__THEORY__ARITH__MSUM_H
+#ifndef CVC4__THEORY__ARITH__MSUM_H
+#define CVC4__THEORY__ARITH__MSUM_H
#include <map>
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARITH__MSUM_H */
+#endif /* CVC4__THEORY__ARITH__MSUM_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ARITH__ARITH_REWRITER_H
-#define __CVC4__THEORY__ARITH__ARITH_REWRITER_H
+#ifndef CVC4__THEORY__ARITH__ARITH_REWRITER_H
+#define CVC4__THEORY__ARITH__ARITH_REWRITER_H
#include "theory/theory.h"
#include "theory/rewriter.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARITH__ARITH_REWRITER_H */
+#endif /* CVC4__THEORY__ARITH__ARITH_REWRITER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
-#define __CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
+#ifndef CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
+#define CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
#include <set>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H */
+#endif /* CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ARITH__ARITH_UTILITIES_H
-#define __CVC4__THEORY__ARITH__ARITH_UTILITIES_H
+#ifndef CVC4__THEORY__ARITH__ARITH_UTILITIES_H
+#define CVC4__THEORY__ARITH__ARITH_UTILITIES_H
#include <unordered_map>
#include <unordered_set>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARITH__ARITH_UTILITIES_H */
+#endif /* CVC4__THEORY__ARITH__ARITH_UTILITIES_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H
-#define __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H
+#ifndef CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H
+#define CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H
#include "theory/arith/arithvar.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H */
+#endif /* CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ARITH__CONSTRAINT_H
-#define __CVC4__THEORY__ARITH__CONSTRAINT_H
+#ifndef CVC4__THEORY__ARITH__CONSTRAINT_H
+#define CVC4__THEORY__ARITH__CONSTRAINT_H
#include <unordered_map>
#include <list>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARITH__CONSTRAINT_H */
+#endif /* CVC4__THEORY__ARITH__CONSTRAINT_H */
** minimize interaction between header files.
**/
-#ifndef __CVC4__THEORY__ARITH__CONSTRAINT_FORWARD_H
-#define __CVC4__THEORY__ARITH__CONSTRAINT_FORWARD_H
+#ifndef CVC4__THEORY__ARITH__CONSTRAINT_FORWARD_H
+#define CVC4__THEORY__ARITH__CONSTRAINT_FORWARD_H
#include "cvc4_private.h"
#include <vector>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARITH__CONSTRAINT_FORWARD_H */
+#endif /* CVC4__THEORY__ARITH__CONSTRAINT_FORWARD_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ARITH__DIO_SOLVER_H
-#define __CVC4__THEORY__ARITH__DIO_SOLVER_H
+#ifndef CVC4__THEORY__ARITH__DIO_SOLVER_H
+#define CVC4__THEORY__ARITH__DIO_SOLVER_H
#include <unordered_map>
#include <utility>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARITH__DIO_SOLVER_H */
+#endif /* CVC4__THEORY__ARITH__DIO_SOLVER_H */
** multiplication via axiom instantiations.
**/
-#ifndef __CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H
-#define __CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H
+#ifndef CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H
+#define CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H
#include <stdint.h>
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H */
+#endif /* CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ARITH__NORMAL_FORM_H
-#define __CVC4__THEORY__ARITH__NORMAL_FORM_H
+#ifndef CVC4__THEORY__ARITH__NORMAL_FORM_H
+#define CVC4__THEORY__ARITH__NORMAL_FORM_H
#include <algorithm>
#include <list>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARITH__NORMAL_FORM_H */
+#endif /* CVC4__THEORY__ARITH__NORMAL_FORM_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ARITH__PARTIAL_MODEL_H
-#define __CVC4__THEORY__ARITH__PARTIAL_MODEL_H
+#ifndef CVC4__THEORY__ARITH__PARTIAL_MODEL_H
+#define CVC4__THEORY__ARITH__PARTIAL_MODEL_H
#include <list>
#include <vector>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARITH__PARTIAL_MODEL_H */
+#endif /* CVC4__THEORY__ARITH__PARTIAL_MODEL_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
-#define __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
+#ifndef CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
+#define CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
namespace CVC4 {
namespace theory {
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H */
+#endif /* CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
-#define __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
+#ifndef CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
+#define CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
#include "expr/kind.h"
#include "expr/type_node.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H */
+#endif /* CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ARRAYS__ARRAY_INFO_H
-#define __CVC4__THEORY__ARRAYS__ARRAY_INFO_H
+#ifndef CVC4__THEORY__ARRAYS__ARRAY_INFO_H
+#define CVC4__THEORY__ARRAYS__ARRAY_INFO_H
#include <iostream>
#include <map>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARRAYS__ARRAY_INFO_H */
+#endif /* CVC4__THEORY__ARRAYS__ARRAY_INFO_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H
-#define __CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H
+#ifndef CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H
+#define CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H
#include "theory/uf/equality_engine.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H */
+#endif /* CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H
-#define __CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H
+#ifndef CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H
+#define CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H
#include <utility>
#include <vector>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /*__CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H */
+#endif /*CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
-#define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
+#ifndef CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
+#define CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
#include <tuple>
#include <unordered_map>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H */
+#endif /* CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
-#define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
+#ifndef CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
+#define CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
#include <unordered_map>
#include <unordered_set>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H */
+#endif /* CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
-#define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
+#ifndef CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
+#define CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
#include "theory/arrays/theory_arrays_rewriter.h" // for array-constant attributes
#include "theory/type_enumerator.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H */
+#endif /* CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H
-#define __CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H
+#ifndef CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H
+#define CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H
#include "theory/type_enumerator.h"
#include "expr/type_node.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H */
+#endif /* CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ARRAYS__UNION_FIND_H
-#define __CVC4__THEORY__ARRAYS__UNION_FIND_H
+#ifndef CVC4__THEORY__ARRAYS__UNION_FIND_H
+#define CVC4__THEORY__ARRAYS__UNION_FIND_H
#include <utility>
#include <vector>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /*__CVC4__THEORY__ARRAYS__UNION_FIND_H */
+#endif /*CVC4__THEORY__ARRAYS__UNION_FIND_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ASSERTION_H
-#define __CVC4__THEORY__ASSERTION_H
+#ifndef CVC4__THEORY__ASSERTION_H
+#define CVC4__THEORY__ASSERTION_H
#include "expr/node.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ASSERTION_H */
+#endif /* CVC4__THEORY__ASSERTION_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
-#define __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
+#ifndef CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
+#define CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
#include <functional>
#include <unordered_map>
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */
+#endif /* CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BOOLEANS__THEORY_BOOL_H
-#define __CVC4__THEORY__BOOLEANS__THEORY_BOOL_H
+#ifndef CVC4__THEORY__BOOLEANS__THEORY_BOOL_H
+#define CVC4__THEORY__BOOLEANS__THEORY_BOOL_H
#include "theory/theory.h"
#include "context/context.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__BOOLEANS__THEORY_BOOL_H */
+#endif /* CVC4__THEORY__BOOLEANS__THEORY_BOOL_H */
/* Trickery to stay under number of children possible in a node */
NodeManager* nodeManager = NodeManager::currentNM();
- static const unsigned MAX_CHILDREN = (1u << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN ) - 1;
+ static const unsigned MAX_CHILDREN = (1u << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN ) - 1;
if (childList.size() < MAX_CHILDREN) {
Node retNode = nodeManager->mkNode(k, childList);
return RewriteResponse(REWRITE_DONE, retNode);
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H
-#define __CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H
+#ifndef CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H
+#define CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H
#include "theory/rewriter.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H */
+#endif /* CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY_BOOL_TYPE_RULES_H
-#define __CVC4__THEORY_BOOL_TYPE_RULES_H
+#ifndef CVC4__THEORY_BOOL_TYPE_RULES_H
+#define CVC4__THEORY_BOOL_TYPE_RULES_H
namespace CVC4 {
namespace theory {
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY_BOOL_TYPE_RULES_H */
+#endif /* CVC4__THEORY_BOOL_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BOOLEANS__TYPE_ENUMERATOR_H
-#define __CVC4__THEORY__BOOLEANS__TYPE_ENUMERATOR_H
+#ifndef CVC4__THEORY__BOOLEANS__TYPE_ENUMERATOR_H
+#define CVC4__THEORY__BOOLEANS__TYPE_ENUMERATOR_H
#include "theory/type_enumerator.h"
#include "expr/type_node.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__BOOLEANS__TYPE_ENUMERATOR_H */
+#endif /* CVC4__THEORY__BOOLEANS__TYPE_ENUMERATOR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H
-#define __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H
+#ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H
+#define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H
#include "theory/theory.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H */
+#endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
-#define __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
+#ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
+#define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
#include "theory/rewriter.h"
#include "theory/theory.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H */
+#endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H
-#define __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H
+#ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H
+#define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H
#include "expr/node.h"
#include "expr/type_node.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H */
+#endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BUILTIN__TYPE_ENUMERATOR_H
-#define __CVC4__THEORY__BUILTIN__TYPE_ENUMERATOR_H
+#ifndef CVC4__THEORY__BUILTIN__TYPE_ENUMERATOR_H
+#define CVC4__THEORY__BUILTIN__TYPE_ENUMERATOR_H
#include "expr/kind.h"
#include "expr/type_node.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__BUILTIN_TYPE_ENUMERATOR_H */
+#endif /* CVC4__THEORY__BUILTIN_TYPE_ENUMERATOR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BV__ABSTRACTION_H
-#define __CVC4__THEORY__BV__ABSTRACTION_H
+#ifndef CVC4__THEORY__BV__ABSTRACTION_H
+#define CVC4__THEORY__BV__ABSTRACTION_H
#include <unordered_map>
#include <unordered_set>
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
-#define __CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
+#ifndef CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
+#define CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
#include "theory/bv/bitblast/bitblaster.h"
#include "prop/sat_solver.h"
} // namespace bv
} // namespace theory
} // namespace CVC4
-#endif // __CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
+#endif // CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
-#define __CVC4__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
+#ifndef CVC4__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
+#define CVC4__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
#include <cmath>
#include <ostream>
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
-#define __CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
+#ifndef CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
+#define CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
#include <ostream>
} // namespace theory
} // namespace CVC4
-#endif // __CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
+#endif // CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BV__BITBLAST__BITBLASTER_H
-#define __CVC4__THEORY__BV__BITBLAST__BITBLASTER_H
+#ifndef CVC4__THEORY__BV__BITBLAST__BITBLASTER_H
+#define CVC4__THEORY__BV__BITBLAST__BITBLASTER_H
#include <unordered_map>
#include <unordered_set>
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__BV__BITBLAST__BITBLASTER_H */
+#endif /* CVC4__THEORY__BV__BITBLAST__BITBLASTER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
-#define __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
+#ifndef CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
+#define CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
#include <unordered_set>
} // namespace bv
} // namespace theory
} // namespace CVC4
-#endif // __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
+#endif // CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
-#define __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
+#ifndef CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
+#define CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
#include "proof/resolution_bitvector_proof.h"
#include "theory/bv/bitblast/bitblaster.h"
} // namespace bv
} // namespace theory
} // namespace CVC4
-#endif // __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
+#endif // CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BV__BV_EAGER_SOLVER_H
-#define __CVC4__THEORY__BV__BV_EAGER_SOLVER_H
+#ifndef CVC4__THEORY__BV__BV_EAGER_SOLVER_H
+#define CVC4__THEORY__BV__BV_EAGER_SOLVER_H
#include <unordered_set>
#include <vector>
} // namespace theory
} // namespace CVC4
-#endif // __CVC4__THEORY__BV__BV_EAGER_SOLVER_H
+#endif // CVC4__THEORY__BV__BV_EAGER_SOLVER_H
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
-#define __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
+#ifndef CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
+#define CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
#include <list>
#include <queue>
}
}
-#endif /* __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H */
+#endif /* CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H */
#include "cvc4_private.h"
-#ifndef __CVC4__BV_QUICK_CHECK_H
-#define __CVC4__BV_QUICK_CHECK_H
+#ifndef CVC4__BV_QUICK_CHECK_H
+#define CVC4__BV_QUICK_CHECK_H
#include <vector>
#include <unordered_set>
} /* theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__BV_QUICK_CHECK_H */
+#endif /* CVC4__BV_QUICK_CHECK_H */
** Interface for bit-vectors sub-solvers.
**/
-#ifndef __CVC4__THEORY__BV__BV_SUBTHEORY_H
-#define __CVC4__THEORY__BV__BV_SUBTHEORY_H
+#ifndef CVC4__THEORY__BV__BV_SUBTHEORY_H
+#define CVC4__THEORY__BV__BV_SUBTHEORY_H
#include "cvc4_private.h"
#include "context/context.h"
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__BV__BV_SUBTHEORY_H */
+#endif /* CVC4__THEORY__BV__BV_SUBTHEORY_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
-#define __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
+#ifndef CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
+#define CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
#include <unordered_set>
}
}
-#endif /* __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */
+#endif /* CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */
#include "util/index.h"
#include "util/statistics_registry.h"
-#ifndef __CVC4__THEORY__BV__SLICER_BV_H
-#define __CVC4__THEORY__BV__SLICER_BV_H
+#ifndef CVC4__THEORY__BV__SLICER_BV_H
+#define CVC4__THEORY__BV__SLICER_BV_H
namespace CVC4 {
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__BV__SLICER_BV_H */
+#endif /* CVC4__THEORY__BV__SLICER_BV_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BV__THEORY_BV_H
-#define __CVC4__THEORY__BV__THEORY_BV_H
+#ifndef CVC4__THEORY__BV__THEORY_BV_H
+#define CVC4__THEORY__BV__THEORY_BV_H
#include <unordered_map>
#include <unordered_set>
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__BV__THEORY_BV_H */
+#endif /* CVC4__THEORY__BV__THEORY_BV_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BV__THEORY_BV_REWRITER_H
-#define __CVC4__THEORY__BV__THEORY_BV_REWRITER_H
+#ifndef CVC4__THEORY__BV__THEORY_BV_REWRITER_H
+#define CVC4__THEORY__BV__THEORY_BV_REWRITER_H
#include "theory/rewriter.h"
#include "util/statistics_registry.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__BV__THEORY_BV_REWRITER_H */
+#endif /* CVC4__THEORY__BV__THEORY_BV_REWRITER_H */
#include <algorithm>
-#ifndef __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
-#define __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
+#ifndef CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
+#define CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
namespace CVC4 {
namespace theory {
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H */
+#endif /* CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BV__TYPE_ENUMERATOR_H
-#define __CVC4__THEORY__BV__TYPE_ENUMERATOR_H
+#ifndef CVC4__THEORY__BV__TYPE_ENUMERATOR_H
+#define CVC4__THEORY__BV__TYPE_ENUMERATOR_H
#include "expr/kind.h"
#include "expr/type_node.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__BV__TYPE_ENUMERATOR_H */
+#endif /* CVC4__THEORY__BV__TYPE_ENUMERATOR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__CARE_GRAPH_H
-#define __CVC4__THEORY__CARE_GRAPH_H
+#ifndef CVC4__THEORY__CARE_GRAPH_H
+#define CVC4__THEORY__CARE_GRAPH_H
#include <set>
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__CARE_GRAPH_H */
+#endif /* CVC4__THEORY__CARE_GRAPH_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H
-#define __CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H
+#ifndef CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H
+#define CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H
#include "expr/node_manager_attributes.h"
#include "options/datatypes_options.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H */
+#endif /* CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__DATATYPES__DATATYPES_SYGUS_NEW_H
-#define __CVC4__THEORY__DATATYPES__DATATYPES_SYGUS_NEW_H
+#ifndef CVC4__THEORY__DATATYPES__DATATYPES_SYGUS_NEW_H
+#define CVC4__THEORY__DATATYPES__DATATYPES_SYGUS_NEW_H
#include <iostream>
#include <map>
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H
-#define __CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H
+#ifndef CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H
+#define CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H
#include <map>
#include "theory/quantifiers/sygus/term_database_sygus.h"
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H */
+#endif /* CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H
-#define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H
+#ifndef CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H
+#define CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H
#include <iostream>
#include <map>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H */
+#endif /* CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
-#define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
+#ifndef CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
+#define CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
#include "expr/matcher.h"
//#include "expr/attribute.h"
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H */
+#endif /* CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H
-#define __CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H
+#ifndef CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H
+#define CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H
#include "theory/type_enumerator.h"
#include "expr/type_node.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H */
+#endif /* CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__DECISION_MANAGER__H
-#define __CVC4__THEORY__DECISION_MANAGER__H
+#ifndef CVC4__THEORY__DECISION_MANAGER__H
+#define CVC4__THEORY__DECISION_MANAGER__H
#include <map>
#include "theory/decision_strategy.h"
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__DECISION_MANAGER__H */
+#endif /* CVC4__THEORY__DECISION_MANAGER__H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__DECISION_STRATEGY__H
-#define __CVC4__THEORY__DECISION_STRATEGY__H
+#ifndef CVC4__THEORY__DECISION_STRATEGY__H
+#define CVC4__THEORY__DECISION_STRATEGY__H
#include <map>
#include "context/cdo.h"
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__DECISION_STRATEGY__H */
+#endif /* CVC4__THEORY__DECISION_STRATEGY__H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__EVALUATOR_H
-#define __CVC4__THEORY__EVALUATOR_H
+#ifndef CVC4__THEORY__EVALUATOR_H
+#define CVC4__THEORY__EVALUATOR_H
#include <utility>
#include <vector>
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__EVALUATOR_H */
+#endif /* CVC4__THEORY__EVALUATOR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__UF__TIM__ECDATA_H
-#define __CVC4__THEORY__UF__TIM__ECDATA_H
+#ifndef CVC4__THEORY__UF__TIM__ECDATA_H
+#define CVC4__THEORY__UF__TIM__ECDATA_H
#include "expr/node.h"
#include "context/context.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__UF__TIM__ECDATA_H */
+#endif /* CVC4__THEORY__UF__TIM__ECDATA_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H
-#define __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H
+#ifndef CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H
+#define CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H
#include "expr/node.h"
#include "expr/attribute.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H */
+#endif /* CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__EXT_THEORY_H
-#define __CVC4__THEORY__EXT_THEORY_H
+#ifndef CVC4__THEORY__EXT_THEORY_H
+#define CVC4__THEORY__EXT_THEORY_H
#include <map>
#include <set>
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__EXT_THEORY_H */
+#endif /* CVC4__THEORY__EXT_THEORY_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__FP__FP_CONVERTER_H
-#define __CVC4__THEORY__FP__FP_CONVERTER_H
+#ifndef CVC4__THEORY__FP__FP_CONVERTER_H
+#define CVC4__THEORY__FP__FP_CONVERTER_H
#include "base/cvc4_assert.h"
#include "context/cdhashmap.h"
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__FP__THEORY_FP_H */
+#endif /* CVC4__THEORY__FP__THEORY_FP_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__FP__THEORY_FP_H
-#define __CVC4__THEORY__FP__THEORY_FP_H
+#ifndef CVC4__THEORY__FP__THEORY_FP_H
+#define CVC4__THEORY__FP__THEORY_FP_H
#include <string>
#include <utility>
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__FP__THEORY_FP_H */
+#endif /* CVC4__THEORY__FP__THEORY_FP_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__FP__THEORY_FP_REWRITER_H
-#define __CVC4__THEORY__FP__THEORY_FP_REWRITER_H
+#ifndef CVC4__THEORY__FP__THEORY_FP_REWRITER_H
+#define CVC4__THEORY__FP__THEORY_FP_REWRITER_H
#include "theory/rewriter.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__FP__THEORY_FP_REWRITER_H */
+#endif /* CVC4__THEORY__FP__THEORY_FP_REWRITER_H */
// This is only needed for checking that components are only applied to leaves.
#include "theory/theory.h"
-#ifndef __CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H
-#define __CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H
+#ifndef CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H
+#define CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H
namespace CVC4 {
namespace theory {
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H */
+#endif /* CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__FP__TYPE_ENUMERATOR_H
-#define __CVC4__THEORY__FP__TYPE_ENUMERATOR_H
+#ifndef CVC4__THEORY__FP__TYPE_ENUMERATOR_H
+#define CVC4__THEORY__FP__TYPE_ENUMERATOR_H
#include "expr/kind.h"
#include "expr/type_node.h"
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__FP__TYPE_ENUMERATOR_H */
+#endif /* CVC4__THEORY__FP__TYPE_ENUMERATOR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__INTERRUPTED_H
-#define __CVC4__THEORY__INTERRUPTED_H
+#ifndef CVC4__THEORY__INTERRUPTED_H
+#define CVC4__THEORY__INTERRUPTED_H
#include "base/exception.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__INTERRUPTED_H */
+#endif /* CVC4__THEORY__INTERRUPTED_H */
#include "cvc4_public.h"
-#ifndef __CVC4__LOGIC_INFO_H
-#define __CVC4__LOGIC_INFO_H
+#ifndef CVC4__LOGIC_INFO_H
+#define CVC4__LOGIC_INFO_H
#include <string>
#include <vector>
}/* CVC4 namespace */
-#endif /* __CVC4__LOGIC_INFO_H */
+#endif /* CVC4__LOGIC_INFO_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__OUTPUT_CHANNEL_H
-#define __CVC4__THEORY__OUTPUT_CHANNEL_H
+#ifndef CVC4__THEORY__OUTPUT_CHANNEL_H
+#define CVC4__THEORY__OUTPUT_CHANNEL_H
#include <memory>
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__OUTPUT_CHANNEL_H */
+#endif /* CVC4__THEORY__OUTPUT_CHANNEL_H */
#include "cvc4_private.h"
-#ifndef __CVC4__ALPHA_EQUIVALENCE_H
-#define __CVC4__ALPHA_EQUIVALENCE_H
+#ifndef CVC4__ALPHA_EQUIVALENCE_H
+#define CVC4__ALPHA_EQUIVALENCE_H
#include "theory/quantifiers_engine.h"
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANT_ANTI_SKOLEM_H
-#define __CVC4__THEORY__QUANT_ANTI_SKOLEM_H
+#ifndef CVC4__THEORY__QUANT_ANTI_SKOLEM_H
+#define CVC4__THEORY__QUANT_ANTI_SKOLEM_H
#include <map>
#include <vector>
#include "cvc4_private.h"
-#ifndef __CVC4__BV_INVERTER_H
-#define __CVC4__BV_INVERTER_H
+#ifndef CVC4__BV_INVERTER_H
+#define CVC4__BV_INVERTER_H
#include <map>
#include <unordered_map>
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__BV_INVERTER_H */
+#endif /* CVC4__BV_INVERTER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__BV_INVERTER_UTILS_H
-#define __CVC4__BV_INVERTER_UTILS_H
+#ifndef CVC4__BV_INVERTER_UTILS_H
+#define CVC4__BV_INVERTER_UTILS_H
#include "expr/node.h"
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
-#define __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
+#ifndef CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
+#define CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
#include <map>
#include <memory>
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H
-#define __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H
+#ifndef CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H
+#define CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H
#include <map>
#include "theory/quantifiers/dynamic_rewrite.h"
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H
-#define __CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H
+#ifndef CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H
+#define CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H
#include <vector>
#include "expr/node.h"
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H
-#define __CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H
+#ifndef CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H
+#define CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H
#include <unordered_map>
#include "theory/quantifiers/bv_inverter.h"
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__BV_INSTANTIATOR_UTILS_H
-#define __CVC4__BV_INSTANTIATOR_UTILS_H
+#ifndef CVC4__BV_INSTANTIATOR_UTILS_H
+#define CVC4__BV_INSTANTIATOR_UTILS_H
#include "expr/attribute.h"
#include "expr/node.h"
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H
-#define __CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H
+#ifndef CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H
+#define CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H
#include "expr/node.h"
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H
-#define __CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H
+#ifndef CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H
+#define CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H
#include <map>
#include <vector>
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
-#define __CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
+#ifndef CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
+#define CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
#include "theory/quantifiers_engine.h"
#include "util/statistics_registry.h"
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
-#define __CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
+#ifndef CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
+#define CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
#include "theory/decision_manager.h"
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
-#define __CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
+#ifndef CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
+#define CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
#include <map>
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
-#define __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
+#ifndef CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
+#define CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H
-#define __CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H
+#ifndef CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H
+#define CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H
#include <map>
#include <unordered_set>
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
-#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
+#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
+#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
#include <map>
#include "expr/node_trie.h"
#include "cvc4_private.h"
-#ifndef __CVC4__INST_STRATEGY_E_MATCHING_H
-#define __CVC4__INST_STRATEGY_E_MATCHING_H
+#ifndef CVC4__INST_STRATEGY_E_MATCHING_H
+#define CVC4__INST_STRATEGY_E_MATCHING_H
#include "context/context.h"
#include "context/context_mm.h"
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
-#define __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
+#ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
+#define CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
#include <memory>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__TRIGGER_H
-#define __CVC4__THEORY__QUANTIFIERS__TRIGGER_H
+#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_H
+#define CVC4__THEORY__QUANTIFIERS__TRIGGER_H
#include <map>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__TRIGGER_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H
-#define __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H
+#ifndef CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H
+#define CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H
#include <iostream>
#include <map>
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
-#define __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
+#ifndef CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
+#define CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
#include "context/cdo.h"
#include "context/context.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H */
+#endif /* CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H
-#define __CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H
+#ifndef CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H
+#define CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H
#include <map>
#include <memory>
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H
-#define __CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H
+#ifndef CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H
+#define CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H
#include "expr/node.h"
#include "theory/quantifiers/candidate_rewrite_database.h"
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H
-#define __CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H
+#ifndef CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H
+#define CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H
#include <unordered_map>
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__FIRST_ORDER_MODEL_H
-#define __CVC4__FIRST_ORDER_MODEL_H
+#ifndef CVC4__FIRST_ORDER_MODEL_H
+#define CVC4__FIRST_ORDER_MODEL_H
#include "theory/theory_model.h"
#include "theory/uf/theory_uf_model.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__FIRST_ORDER_MODEL_H */
+#endif /* CVC4__FIRST_ORDER_MODEL_H */
#include "cvc4_private.h"
-#ifndef __CVC4__BOUNDED_INTEGERS_H
-#define __CVC4__BOUNDED_INTEGERS_H
+#ifndef CVC4__BOUNDED_INTEGERS_H
+#define CVC4__BOUNDED_INTEGERS_H
#include "theory/quantifiers_engine.h"
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
-#define __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
+#ifndef CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
+#define CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
#include "theory/quantifiers/fmf/model_builder.h"
#include "theory/quantifiers/first_order_model.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
-#define __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
+#ifndef CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
+#define CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
#include "theory/quantifiers_engine.h"
#include "theory/theory_model_builder.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H
-#define __CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H
+#ifndef CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H
+#define CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H
#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/fmf/model_builder.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__QUANTIFIERS_FUN_DEF_PROCESS_H
-#define __CVC4__QUANTIFIERS_FUN_DEF_PROCESS_H
+#ifndef CVC4__QUANTIFIERS_FUN_DEF_PROCESS_H
+#define CVC4__QUANTIFIERS_FUN_DEF_PROCESS_H
#include <iostream>
#include <string>
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
-#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
+#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
+#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
#include <vector>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
-#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
+#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
+#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
#include <map>
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */
#include "cvc4_private.h"
-#ifndef __CVC4__QUANTIFIERS_INST_PROPAGATOR_H
-#define __CVC4__QUANTIFIERS_INST_PROPAGATOR_H
+#ifndef CVC4__QUANTIFIERS_INST_PROPAGATOR_H
+#define CVC4__QUANTIFIERS_INST_PROPAGATOR_H
#include <iostream>
#include <map>
#include "cvc4_private.h"
-#ifndef __CVC4__INST_STRATEGY_ENUMERATIVE_H
-#define __CVC4__INST_STRATEGY_ENUMERATIVE_H
+#ifndef CVC4__INST_STRATEGY_ENUMERATIVE_H
+#define CVC4__INST_STRATEGY_ENUMERATIVE_H
#include "context/context.h"
#include "context/context_mm.h"
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
-#define __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
+#ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
+#define CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
#include <map>
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */
** \brief lazy trie
**/
-#ifndef __CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H
-#define __CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H
+#ifndef CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H
+#define CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H
#include "expr/node.h"
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__LOCAL_THEORY_EXT_H
-#define __CVC4__THEORY__LOCAL_THEORY_EXT_H
+#ifndef CVC4__THEORY__LOCAL_THEORY_EXT_H
+#define CVC4__THEORY__LOCAL_THEORY_EXT_H
#include "context/cdo.h"
#include "expr/node_trie.h"
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANT_EPR_H
-#define __CVC4__THEORY__QUANT_EPR_H
+#ifndef CVC4__THEORY__QUANT_EPR_H
+#define CVC4__THEORY__QUANT_EPR_H
#include <map>
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANT_EPR_H */
+#endif /* CVC4__THEORY__QUANT_EPR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANT_RELEVANCE_H
-#define __CVC4__THEORY__QUANT_RELEVANCE_H
+#ifndef CVC4__THEORY__QUANT_RELEVANCE_H
+#define CVC4__THEORY__QUANT_RELEVANCE_H
#include <map>
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANT_RELEVANCE_H */
+#endif /* CVC4__THEORY__QUANT_RELEVANCE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANT_SPLIT_H
-#define __CVC4__THEORY__QUANT_SPLIT_H
+#ifndef CVC4__THEORY__QUANT_SPLIT_H
+#define CVC4__THEORY__QUANT_SPLIT_H
#include "theory/quantifiers_engine.h"
#include "context/cdo.h"
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANT_UTIL_H
-#define __CVC4__THEORY__QUANT_UTIL_H
+#ifndef CVC4__THEORY__QUANT_UTIL_H
+#define CVC4__THEORY__QUANT_UTIL_H
#include <iostream>
#include <map>
}
}
-#endif /* __CVC4__THEORY__QUANT_UTIL_H */
+#endif /* CVC4__THEORY__QUANT_UTIL_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
-#define __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
+#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
+#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
#include "expr/attribute.h"
#include "expr/node.h"
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
-#define __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
+#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
+#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
#include "theory/rewriter.h"
#include "theory/quantifiers_engine.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__QUERY_GENERATOR_H
-#define __CVC4__THEORY__QUANTIFIERS__QUERY_GENERATOR_H
+#ifndef CVC4__THEORY__QUANTIFIERS__QUERY_GENERATOR_H
+#define CVC4__THEORY__QUANTIFIERS__QUERY_GENERATOR_H
#include <map>
#include <unordered_set>
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__QUANTIFIERS___H */
+#endif /* CVC4__THEORY__QUANTIFIERS___H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
-#define __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
+#ifndef CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
+#define CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/quant_util.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */
#include "cvc4_private.h"
-#ifndef __CVC4__REWRITE_ENGINE_H
-#define __CVC4__REWRITE_ENGINE_H
+#ifndef CVC4__REWRITE_ENGINE_H
+#define CVC4__REWRITE_ENGINE_H
#include "context/context.h"
#include "context/context_mm.h"
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
-#define __CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
+#define CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
#include <map>
#include <vector>
} /* namespace CVC4::theory */
} /* namespace CVC4 */
-#endif /* __CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H
-#define __CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H
+#define CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H
#include <unordered_map>
#include <unordered_set>
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H
-#define __CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H
+#define CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H
#include <map>
#include <unordered_set>
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
-#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
+#ifndef CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
+#define CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
#include "context/cdlist.h"
#include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h"
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H
-#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H
+#ifndef CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H
+#define CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H
#include "context/cdhashmap.h"
#include "theory/quantifiers_engine.h"
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__CEGIS_H
-#define __CVC4__THEORY__QUANTIFIERS__CEGIS_H
+#ifndef CVC4__THEORY__QUANTIFIERS__CEGIS_H
+#define CVC4__THEORY__QUANTIFIERS__CEGIS_H
#include <map>
#include "theory/quantifiers/sygus/sygus_module.h"
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__CEGIS_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__CEGIS_H */
**/
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H
-#define __CVC4__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H
#include <map>
#include <vector>
**/
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
-#define __CVC4__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
#include "expr/node.h"
#include "theory/quantifiers/sygus/synth_conjecture.h"
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H
-#define __CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H
#include <map>
#include <unordered_set>
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H
-#define __CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H
#include <map>
#include "expr/node.h"
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H
-#define __CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H
#include <vector>
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
-#define __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
#include "theory/quantifiers_engine.h"
**/
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H
-#define __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H
#include <map>
#include <memory>
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H
-#define __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H
#include <map>
#include "theory/quantifiers_engine.h"
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
-#define __CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
#include <unordered_map>
#include <vector>
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
-#define __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
#include <map>
#include "expr/node.h"
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H
-#define __CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H
#include "context/cdhashmap.h"
#include "theory/quantifiers/sygus/sygus_module.h"
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H
-#define __CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H
#include <map>
#include <unordered_map>
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H
-#define __CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H
#include <unordered_set>
#include "expr/node.h"
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H
-#define __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H
#include <map>
#include "expr/node.h"
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H
-#define __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H
#include <map>
#include "theory/quantifiers/sygus/sygus_unif.h"
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H
-#define __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H
#include <map>
#include "options/main_options.h"
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H
-#define __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H
#include <map>
#include "expr/node.h"
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
-#define __CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
+#define CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
#include <memory>
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H
-#define __CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H
+#define CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H
#include "context/cdhashmap.h"
#include "theory/quantifiers/sygus/synth_conjecture.h"
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H
-#define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H
+#ifndef CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H
+#define CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H
#include <unordered_set>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
-#define __CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
#include <map>
#include "theory/evaluator.h"
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H
-#define __CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H
+#ifndef CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H
+#define CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H
#include <map>
#include "expr/node.h"
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
-#define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
+#ifndef CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
+#define CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
#include <map>
#include <unordered_set>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H
-#define __CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H
+#ifndef CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H
+#define CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H
#include <unordered_map>
#include <vector>
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H
-#define __CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H
+#ifndef CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H
+#define CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H
#include <map>
#include <unordered_set>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
-#define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
+#ifndef CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
+#define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
#include "context/cdhashmap.h"
#include "context/context.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H
-#define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H
+#ifndef CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H
+#define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H
#include "expr/matcher.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS_ENGINE_H
-#define __CVC4__THEORY__QUANTIFIERS_ENGINE_H
+#ifndef CVC4__THEORY__QUANTIFIERS_ENGINE_H
+#define CVC4__THEORY__QUANTIFIERS_ENGINE_H
#include <iostream>
#include <map>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS_ENGINE_H */
+#endif /* CVC4__THEORY__QUANTIFIERS_ENGINE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__REP_SET_H
-#define __CVC4__THEORY__REP_SET_H
+#ifndef CVC4__THEORY__REP_SET_H
+#define CVC4__THEORY__REP_SET_H
#include <map>
#include <vector>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__REP_SET_H */
+#endif /* CVC4__THEORY__REP_SET_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__SEP__THEORY_SEP_H
-#define __CVC4__THEORY__SEP__THEORY_SEP_H
+#ifndef CVC4__THEORY__SEP__THEORY_SEP_H
+#define CVC4__THEORY__SEP__THEORY_SEP_H
#include "context/cdhashmap.h"
#include "context/cdhashset.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__SEP__THEORY_SEP_H */
+#endif /* CVC4__THEORY__SEP__THEORY_SEP_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__SEP__THEORY_SEP_REWRITER_H
-#define __CVC4__THEORY__SEP__THEORY_SEP_REWRITER_H
+#ifndef CVC4__THEORY__SEP__THEORY_SEP_REWRITER_H
+#define CVC4__THEORY__SEP__THEORY_SEP_REWRITER_H
#include "theory/rewriter.h"
#include "theory/type_enumerator.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__SEP__THEORY_SEP_REWRITER_H */
+#endif /* CVC4__THEORY__SEP__THEORY_SEP_REWRITER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H
-#define __CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H
+#ifndef CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H
+#define CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H
namespace CVC4 {
namespace theory {
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H */
+#endif /* CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__SETS__NORMAL_FORM_H
-#define __CVC4__THEORY__SETS__NORMAL_FORM_H
+#ifndef CVC4__THEORY__SETS__NORMAL_FORM_H
+#define CVC4__THEORY__SETS__NORMAL_FORM_H
namespace CVC4 {
namespace theory {
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__SETS__THEORY_SETS_H
-#define __CVC4__THEORY__SETS__THEORY_SETS_H
+#ifndef CVC4__THEORY__SETS__THEORY_SETS_H
+#define CVC4__THEORY__SETS__THEORY_SETS_H
#include <memory>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__SETS__THEORY_SETS_H */
+#endif /* CVC4__THEORY__SETS__THEORY_SETS_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H
-#define __CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H
+#ifndef CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H
+#define CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H
#include "context/cdhashset.h"
#include "context/cdqueue.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H */
+#endif /* CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H
-#define __CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H
+#ifndef CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H
+#define CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H
#include "theory/rewriter.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H */
+#endif /* CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__SETS__TYPE_ENUMERATOR_H
-#define __CVC4__THEORY__SETS__TYPE_ENUMERATOR_H
+#ifndef CVC4__THEORY__SETS__TYPE_ENUMERATOR_H
+#define CVC4__THEORY__SETS__TYPE_ENUMERATOR_H
#include "theory/type_enumerator.h"
#include "expr/type_node.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__SETS__TYPE_ENUMERATOR_H */
+#endif /* CVC4__THEORY__SETS__TYPE_ENUMERATOR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H
-#define __CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H
+#ifndef CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H
+#define CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H
#include "theory/sets/normal_form.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H */
+#endif /* CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef __CVC4__SORT_INFERENCE_H
-#define __CVC4__SORT_INFERENCE_H
+#ifndef CVC4__SORT_INFERENCE_H
+#define CVC4__SORT_INFERENCE_H
#include <iostream>
#include <string>
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__STRINGS__NORMAL_FORM_H
-#define __CVC4__THEORY__STRINGS__NORMAL_FORM_H
+#ifndef CVC4__THEORY__STRINGS__NORMAL_FORM_H
+#define CVC4__THEORY__STRINGS__NORMAL_FORM_H
#include <map>
#include <vector>
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__STRINGS__NORMAL_FORM_H */
+#endif /* CVC4__THEORY__STRINGS__NORMAL_FORM_H */
**/
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__STRINGS__REGEXP_ELIM_H
-#define __CVC4__THEORY__STRINGS__REGEXP_ELIM_H
+#ifndef CVC4__THEORY__STRINGS__REGEXP_ELIM_H
+#define CVC4__THEORY__STRINGS__REGEXP_ELIM_H
#include "expr/node.h"
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__STRINGS__REGEXP_ELIM_H */
+#endif /* CVC4__THEORY__STRINGS__REGEXP_ELIM_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__STRINGS__REGEXP__OPERATION_H
-#define __CVC4__THEORY__STRINGS__REGEXP__OPERATION_H
+#ifndef CVC4__THEORY__STRINGS__REGEXP__OPERATION_H
+#define CVC4__THEORY__STRINGS__REGEXP__OPERATION_H
#include <vector>
#include <set>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__STRINGS__REGEXP__OPERATION_H */
+#endif /* CVC4__THEORY__STRINGS__REGEXP__OPERATION_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__STRINGS__REGEXP_SOLVER_H
-#define __CVC4__THEORY__STRINGS__REGEXP_SOLVER_H
+#ifndef CVC4__THEORY__STRINGS__REGEXP_SOLVER_H
+#define CVC4__THEORY__STRINGS__REGEXP_SOLVER_H
#include <map>
#include "context/cdhashset.h"
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_H */
+#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__STRINGS__SKOLEM_CACHE_H
-#define __CVC4__THEORY__STRINGS__SKOLEM_CACHE_H
+#ifndef CVC4__THEORY__STRINGS__SKOLEM_CACHE_H
+#define CVC4__THEORY__STRINGS__SKOLEM_CACHE_H
#include <map>
#include <tuple>
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__STRINGS__SKOLEM_CACHE_H */
+#endif /* CVC4__THEORY__STRINGS__SKOLEM_CACHE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__STRINGS__THEORY_STRINGS_H
-#define __CVC4__THEORY__STRINGS__THEORY_STRINGS_H
+#ifndef CVC4__THEORY__STRINGS__THEORY_STRINGS_H
+#define CVC4__THEORY__STRINGS__THEORY_STRINGS_H
#include "context/cdhashset.h"
#include "context/cdlist.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_H */
+#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__STRINGS__PREPROCESS_H
-#define __CVC4__THEORY__STRINGS__PREPROCESS_H
+#ifndef CVC4__THEORY__STRINGS__PREPROCESS_H
+#define CVC4__THEORY__STRINGS__PREPROCESS_H
#include <vector>
#include "context/cdhashmap.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__STRINGS__PREPROCESS_H */
+#endif /* CVC4__THEORY__STRINGS__PREPROCESS_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__STRINGS__THEORY_STRINGS_REWRITER_H
-#define __CVC4__THEORY__STRINGS__THEORY_STRINGS_REWRITER_H
+#ifndef CVC4__THEORY__STRINGS__THEORY_STRINGS_REWRITER_H
+#define CVC4__THEORY__STRINGS__THEORY_STRINGS_REWRITER_H
#include <utility>
#include <vector>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_REWRITER_H */
+#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_REWRITER_H */
#include "cvc4_private.h"
#include "options/strings_options.h"
-#ifndef __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
-#define __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
+#ifndef CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
+#define CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
namespace CVC4 {
namespace theory {
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H */
+#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H
-#define __CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H
+#ifndef CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H
+#define CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H
#include <sstream>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H */
+#endif /* CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__SUBS_MINIMIZE_H
-#define __CVC4__THEORY__SUBS_MINIMIZE_H
+#ifndef CVC4__THEORY__SUBS_MINIMIZE_H
+#define CVC4__THEORY__SUBS_MINIMIZE_H
#include <vector>
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__SUBS_MINIMIZE_H */
+#endif /* CVC4__THEORY__SUBS_MINIMIZE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__SUBSTITUTIONS_H
-#define __CVC4__THEORY__SUBSTITUTIONS_H
+#ifndef CVC4__THEORY__SUBSTITUTIONS_H
+#define CVC4__THEORY__SUBSTITUTIONS_H
//#include <algorithm>
#include <utility>
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__SUBSTITUTIONS_H */
+#endif /* CVC4__THEORY__SUBSTITUTIONS_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__THEORY_H
-#define __CVC4__THEORY__THEORY_H
+#ifndef CVC4__THEORY__THEORY_H
+#define CVC4__THEORY__THEORY_H
#include <iosfwd>
#include <map>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__THEORY_H */
+#endif /* CVC4__THEORY__THEORY_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY_ENGINE_H
-#define __CVC4__THEORY_ENGINE_H
+#ifndef CVC4__THEORY_ENGINE_H
+#define CVC4__THEORY_ENGINE_H
#include <deque>
#include <memory>
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY_ENGINE_H */
+#endif /* CVC4__THEORY_ENGINE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__THEORY_MODEL_H
-#define __CVC4__THEORY__THEORY_MODEL_H
+#ifndef CVC4__THEORY__THEORY_MODEL_H
+#define CVC4__THEORY__THEORY_MODEL_H
#include <unordered_map>
#include <unordered_set>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__THEORY_MODEL_H */
+#endif /* CVC4__THEORY__THEORY_MODEL_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__THEORY_MODEL_BUILDER_H
-#define __CVC4__THEORY__THEORY_MODEL_BUILDER_H
+#ifndef CVC4__THEORY__THEORY_MODEL_BUILDER_H
+#define CVC4__THEORY__THEORY_MODEL_BUILDER_H
#include <unordered_map>
#include <unordered_set>
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__THEORY_MODEL_BUILDER_H */
+#endif /* CVC4__THEORY__THEORY_MODEL_BUILDER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__THEORY_REGISTRAR_H
-#define __CVC4__THEORY__THEORY_REGISTRAR_H
+#ifndef CVC4__THEORY__THEORY_REGISTRAR_H
+#define CVC4__THEORY__THEORY_REGISTRAR_H
#include "prop/registrar.h"
#include "theory/theory_engine.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__THEORY_REGISTRAR_H */
+#endif /* CVC4__THEORY__THEORY_REGISTRAR_H */
#include "cvc4_public.h"
-#ifndef __CVC4__THEORY__THEORY_TEST_UTILS_H
-#define __CVC4__THEORY__THEORY_TEST_UTILS_H
+#ifndef CVC4__THEORY__THEORY_TEST_UTILS_H
+#define CVC4__THEORY__THEORY_TEST_UTILS_H
#include <iostream>
#include <memory>
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__THEORY_TEST_UTILS_H */
+#endif /* CVC4__THEORY__THEORY_TEST_UTILS_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__TYPE_ENUMERATOR_H
-#define __CVC4__THEORY__TYPE_ENUMERATOR_H
+#ifndef CVC4__THEORY__TYPE_ENUMERATOR_H
+#define CVC4__THEORY__TYPE_ENUMERATOR_H
#include "base/exception.h"
#include "base/cvc4_assert.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__TYPE_ENUMERATOR_H */
+#endif /* CVC4__THEORY__TYPE_ENUMERATOR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__TYPE_SET_H
-#define __CVC4__THEORY__TYPE_SET_H
+#ifndef CVC4__THEORY__TYPE_SET_H
+#define CVC4__THEORY__TYPE_SET_H
#include <unordered_map>
#include <unordered_set>
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__TYPE_SET_H */
+#endif /* CVC4__THEORY__TYPE_SET_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H
-#define __CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H
+#ifndef CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H
+#define CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H
#include <string>
#include <iostream>
} // namespace theory
} // namespace CVC4
-#endif /* __CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H */
+#endif /* CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__UF__SYMMETRY_BREAKER_H
-#define __CVC4__THEORY__UF__SYMMETRY_BREAKER_H
+#ifndef CVC4__THEORY__UF__SYMMETRY_BREAKER_H
+#define CVC4__THEORY__UF__SYMMETRY_BREAKER_H
#include <iostream>
#include <list>
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__UF__SYMMETRY_BREAKER_H */
+#endif /* CVC4__THEORY__UF__SYMMETRY_BREAKER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__UF__THEORY_UF_H
-#define __CVC4__THEORY__UF__THEORY_UF_H
+#ifndef CVC4__THEORY__UF__THEORY_UF_H
+#define CVC4__THEORY__UF__THEORY_UF_H
#include "context/cdhashset.h"
#include "context/cdo.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__UF__THEORY_UF_H */
+#endif /* CVC4__THEORY__UF__THEORY_UF_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY_UF_MODEL_H
-#define __CVC4__THEORY_UF_MODEL_H
+#ifndef CVC4__THEORY_UF_MODEL_H
+#define CVC4__THEORY_UF_MODEL_H
#include "theory/theory_model.h"
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__UF__THEORY_UF_REWRITER_H
-#define __CVC4__THEORY__UF__THEORY_UF_REWRITER_H
+#ifndef CVC4__THEORY__UF__THEORY_UF_REWRITER_H
+#define CVC4__THEORY__UF__THEORY_UF_REWRITER_H
#include "expr/node_algorithm.h"
#include "theory/rewriter.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__UF__THEORY_UF_REWRITER_H */
+#endif /* CVC4__THEORY__UF__THEORY_UF_REWRITER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY_UF_STRONG_SOLVER_H
-#define __CVC4__THEORY_UF_STRONG_SOLVER_H
+#ifndef CVC4__THEORY_UF_STRONG_SOLVER_H
+#define CVC4__THEORY_UF_STRONG_SOLVER_H
#include "context/cdhashmap.h"
#include "context/context.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY_UF_STRONG_SOLVER_H */
+#endif /* CVC4__THEORY_UF_STRONG_SOLVER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H
-#define __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H
+#ifndef CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H
+#define CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H
namespace CVC4 {
namespace theory {
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H */
+#endif /* CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__VALUATION_H
-#define __CVC4__THEORY__VALUATION_H
+#ifndef CVC4__THEORY__VALUATION_H
+#define CVC4__THEORY__VALUATION_H
#include "expr/node.h"
#include "options/theoryof_mode.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__VALUATION_H */
+#endif /* CVC4__THEORY__VALUATION_H */
#include "cvc4_private.h"
-#ifndef __CVC4__BIN_HEAP_H
-#define __CVC4__BIN_HEAP_H
+#ifndef CVC4__BIN_HEAP_H
+#define CVC4__BIN_HEAP_H
#include <limits>
#include <functional>
}/* CVC4 namespace */
-#endif /* __CVC4__BIN_HEAP_H */
+#endif /* CVC4__BIN_HEAP_H */
#include "cvc4_public.h"
-#ifndef __CVC4__BITVECTOR_H
-#define __CVC4__BITVECTOR_H
+#ifndef CVC4__BITVECTOR_H
+#define CVC4__BITVECTOR_H
#include <cstdint>
#include <iosfwd>
} // namespace CVC4
-#endif /* __CVC4__BITVECTOR_H */
+#endif /* CVC4__BITVECTOR_H */
#include "cvc4_public.h"
-#ifndef __CVC4__BOOL_H
-#define __CVC4__BOOL_H
+#ifndef CVC4__BOOL_H
+#define CVC4__BOOL_H
namespace CVC4 {
}/* CVC4 namespace */
-#endif /* __CVC4__BOOL_H */
+#endif /* CVC4__BOOL_H */
#include "cvc4_public.h"
-#ifndef __CVC4__CARDINALITY_H
-#define __CVC4__CARDINALITY_H
+#ifndef CVC4__CARDINALITY_H
+#define CVC4__CARDINALITY_H
#include <iostream>
#include <utility>
} /* CVC4 namespace */
-#endif /* __CVC4__CARDINALITY_H */
+#endif /* CVC4__CARDINALITY_H */
#include "cvc4_public.h"
-#ifndef __CVC4__CHANNEL_H
-#define __CVC4__CHANNEL_H
+#ifndef CVC4__CHANNEL_H
+#define CVC4__CHANNEL_H
#include <boost/circular_buffer.hpp>
#include <boost/thread/mutex.hpp>
}/* CVC4 namespace */
-#endif /* __CVC4__CHANNEL_H */
+#endif /* CVC4__CHANNEL_H */
#include "cvc4_private.h"
-#ifndef __CVC4__DEBUG_H
-#define __CVC4__DEBUG_H
+#ifndef CVC4__DEBUG_H
+#define CVC4__DEBUG_H
#include <cassert>
# define cvc4assert(x) /*__builtin_expect( ( x ), true )*/
#endif /* CVC4_ASSERTIONS */
-#endif /* __CVC4__DEBUG_H */
+#endif /* CVC4__DEBUG_H */
#include "cvc4_public.h"
-#ifndef __CVC4__DIVISIBLE_H
-#define __CVC4__DIVISIBLE_H
+#ifndef CVC4__DIVISIBLE_H
+#define CVC4__DIVISIBLE_H
#include <iosfwd>
}/* CVC4 namespace */
-#endif /* __CVC4__DIVISIBLE_H */
+#endif /* CVC4__DIVISIBLE_H */
**/
#include "cvc4_public.h"
-#ifndef __CVC4__FLOATINGPOINT_H
-#define __CVC4__FLOATINGPOINT_H
+#ifndef CVC4__FLOATINGPOINT_H
+#define CVC4__FLOATINGPOINT_H
#include "util/bitvector.h"
#include "util/rational.h"
}/* CVC4 namespace */
-#endif /* __CVC4__FLOATINGPOINT_H */
+#endif /* CVC4__FLOATINGPOINT_H */
#include "cvc4_public.h"
-#ifndef __CVC4__GMP_UTIL_H
-#define __CVC4__GMP_UTIL_H
+#ifndef CVC4__GMP_UTIL_H
+#define CVC4__GMP_UTIL_H
/*
* Older versions of GMP in combination with newer versions of GCC and C++11
}/* CVC4 namespace */
-#endif /* __CVC4__GMP_UTIL_H */
+#endif /* CVC4__GMP_UTIL_H */
#include "cvc4_public.h"
-#ifndef __CVC4__HASH_H
-#define __CVC4__HASH_H
+#ifndef CVC4__HASH_H
+#define CVC4__HASH_H
#include <cstdint>
#include <functional>
}/* CVC4 namespace */
-#endif /* __CVC4__HASH_H */
+#endif /* CVC4__HASH_H */
#include "cvc4_private.h"
-#ifndef __CVC4__INDEX_H
-#define __CVC4__INDEX_H
+#ifndef CVC4__INDEX_H
+#define CVC4__INDEX_H
#include <cstdint>
}/* CVC4 namespace */
-#endif /* __CVC4__INDEX_H */
+#endif /* CVC4__INDEX_H */
#include "cvc4_public.h"
-#ifndef __CVC4__INTEGER_H
-#define __CVC4__INTEGER_H
+#ifndef CVC4__INTEGER_H
+#define CVC4__INTEGER_H
#include <cln/input.h>
#include <cln/integer.h>
}/* CVC4 namespace */
-#endif /* __CVC4__INTEGER_H */
+#endif /* CVC4__INTEGER_H */
#include "cvc4_public.h"
-#ifndef __CVC4__INTEGER_H
-#define __CVC4__INTEGER_H
+#ifndef CVC4__INTEGER_H
+#define CVC4__INTEGER_H
#include <string>
#include <iosfwd>
}/* CVC4 namespace */
-#endif /* __CVC4__INTEGER_H */
+#endif /* CVC4__INTEGER_H */
**/
#include "cvc4_public.h"
-#ifndef __CVC4__UTIL__MAYBE_H
-#define __CVC4__UTIL__MAYBE_H
+#ifndef CVC4__UTIL__MAYBE_H
+#define CVC4__UTIL__MAYBE_H
#include <ostream>
}/* CVC4 namespace */
-#endif /* __CVC4__UTIL__MAYBE_H */
+#endif /* CVC4__UTIL__MAYBE_H */
#include "cvc4_private.h"
-#ifndef __CVC4__UTIL__OSTREAM_UTIL_H
-#define __CVC4__UTIL__OSTREAM_UTIL_H
+#ifndef CVC4__UTIL__OSTREAM_UTIL_H
+#define CVC4__UTIL__OSTREAM_UTIL_H
#include <ios>
#include <ostream>
} // namespace CVC4
-#endif /* __CVC4__UTIL__OSTREAM_UTIL_H */
+#endif /* CVC4__UTIL__OSTREAM_UTIL_H */
#include "cvc4_public.h"
-#ifndef __CVC4__PROOF_H
-#define __CVC4__PROOF_H
+#ifndef CVC4__PROOF_H
+#define CVC4__PROOF_H
#include <iosfwd>
#include <unordered_map>
}/* CVC4 namespace */
-#endif /* __CVC4__PROOF_H */
+#endif /* CVC4__PROOF_H */
#include "cvc4_private.h"
-#ifndef __CVC4__UTIL__RANDOM_H
-#define __CVC4__UTIL__RANDOM_H
+#ifndef CVC4__UTIL__RANDOM_H
+#define CVC4__UTIL__RANDOM_H
namespace CVC4 {
#include "cvc4_public.h"
-#ifndef __CVC4__RATIONAL_H
-#define __CVC4__RATIONAL_H
+#ifndef CVC4__RATIONAL_H
+#define CVC4__RATIONAL_H
#include <gmp.h>
#include <string>
}/* CVC4 namespace */
-#endif /* __CVC4__RATIONAL_H */
+#endif /* CVC4__RATIONAL_H */
#include "cvc4_public.h"
-#ifndef __CVC4__RATIONAL_H
-#define __CVC4__RATIONAL_H
+#ifndef CVC4__RATIONAL_H
+#define CVC4__RATIONAL_H
/*
* Older versions of GMP in combination with newer versions of GCC and C++11
}/* CVC4 namespace */
-#endif /* __CVC4__RATIONAL_H */
+#endif /* CVC4__RATIONAL_H */
#include "cvc4_public.h"
-#ifndef __CVC4__REGEXP_H
-#define __CVC4__REGEXP_H
+#ifndef CVC4__REGEXP_H
+#define CVC4__REGEXP_H
#include <cstddef>
#include <functional>
} // namespace CVC4
-#endif /* __CVC4__REGEXP_H */
+#endif /* CVC4__REGEXP_H */
#include "cvc4_public.h"
-#ifndef __CVC4__RESOURCE_MANAGER_H
-#define __CVC4__RESOURCE_MANAGER_H
+#ifndef CVC4__RESOURCE_MANAGER_H
+#define CVC4__RESOURCE_MANAGER_H
#include <cstddef>
#include <sys/time.h>
}/* CVC4 namespace */
-#endif /* __CVC4__RESOURCE_MANAGER_H */
+#endif /* CVC4__RESOURCE_MANAGER_H */
#include "cvc4_public.h"
-#ifndef __CVC4__RESULT_H
-#define __CVC4__RESULT_H
+#ifndef CVC4__RESULT_H
+#define CVC4__RESULT_H
#include <iostream>
#include <string>
} /* CVC4 namespace */
-#endif /* __CVC4__RESULT_H */
+#endif /* CVC4__RESULT_H */
#include "cvc4_private_library.h"
-#ifndef __CVC4__SAFE_PRINT_H
-#define __CVC4__SAFE_PRINT_H
+#ifndef CVC4__SAFE_PRINT_H
+#define CVC4__SAFE_PRINT_H
#if __cplusplus >= 201103L
// For c++11 and newer
} /* CVC4 namespace */
-#endif /* __CVC4__SAFE_PRINT_H */
+#endif /* CVC4__SAFE_PRINT_H */
#include "cvc4_private.h"
-#ifndef __CVC4__UTIL_FLOATINGPOINT_SAMPLER_H
-#define __CVC4__UTIL_FLOATINGPOINT_SAMPLER_H
+#ifndef CVC4__UTIL_FLOATINGPOINT_SAMPLER_H
+#define CVC4__UTIL_FLOATINGPOINT_SAMPLER_H
#include "util/floatingpoint.h"
#include "util/random.h"
} // namespace CVC4
-#endif /* __CVC4__UTIL_FLOATINGPOINT_SAMPLER_H */
+#endif /* CVC4__UTIL_FLOATINGPOINT_SAMPLER_H */
#include "cvc4_public.h"
-#ifndef __CVC4__SEXPR_H
-#define __CVC4__SEXPR_H
+#ifndef CVC4__SEXPR_H
+#define CVC4__SEXPR_H
#include <iomanip>
#include <iosfwd>
} /* CVC4 namespace */
-#endif /* __CVC4__SEXPR_H */
+#endif /* CVC4__SEXPR_H */
#include "cvc4_private.h"
-#ifndef __CVC4__UTIL__SMT2_QUOTE_STRING_H
-#define __CVC4__UTIL__SMT2_QUOTE_STRING_H
+#ifndef CVC4__UTIL__SMT2_QUOTE_STRING_H
+#define CVC4__UTIL__SMT2_QUOTE_STRING_H
#include <string>
}/* CVC4 namespace */
-#endif /* __CVC4__UTIL__SMT2_QUOTE_STRING_H */
+#endif /* CVC4__UTIL__SMT2_QUOTE_STRING_H */
#include "cvc4_public.h"
-#ifndef __CVC4__STATISTICS_H
-#define __CVC4__STATISTICS_H
+#ifndef CVC4__STATISTICS_H
+#define CVC4__STATISTICS_H
#include <iterator>
#include <ostream>
}/* CVC4 namespace */
-#endif /* __CVC4__STATISTICS_H */
+#endif /* CVC4__STATISTICS_H */
#include "util/ostream_util.h"
#ifdef CVC4_STATISTICS_ON
-# define __CVC4_USE_STATISTICS true
+# define CVC4_USE_STATISTICS true
#else
-# define __CVC4_USE_STATISTICS false
+# define CVC4_USE_STATISTICS false
#endif
StatisticsRegistry::StatisticsRegistry(const std::string& name) : Stat(name)
{
d_prefix = name;
- if(__CVC4_USE_STATISTICS) {
+ if(CVC4_USE_STATISTICS) {
PrettyCheckArgument(d_name.find(s_regDelim) == std::string::npos, name,
"StatisticsRegistry names cannot contain the string \"%s\"",
s_regDelim.c_str());
}
void TimerStat::start() {
- if(__CVC4_USE_STATISTICS) {
+ if(CVC4_USE_STATISTICS) {
PrettyCheckArgument(!d_running, *this, "timer already running");
clock_gettime(CLOCK_MONOTONIC, &d_start);
d_running = true;
}/* TimerStat::start() */
void TimerStat::stop() {
- if(__CVC4_USE_STATISTICS) {
+ if(CVC4_USE_STATISTICS) {
CVC4_CHECK(d_running) << "timer not running";
::timespec end;
clock_gettime(CLOCK_MONOTONIC, &end);
timespec TimerStat::getData() const {
::timespec data = d_data;
- if(__CVC4_USE_STATISTICS && d_running) {
+ if(CVC4_USE_STATISTICS && d_running) {
::timespec end;
clock_gettime(CLOCK_MONOTONIC, &end);
data += end - d_start;
SExpr TimerStat::getValue() const {
::timespec data = d_data;
- if(__CVC4_USE_STATISTICS && d_running) {
+ if(CVC4_USE_STATISTICS && d_running) {
::timespec end;
clock_gettime(CLOCK_MONOTONIC, &end);
data += end - d_start;
}/* CVC4 namespace */
-#undef __CVC4_USE_STATISTICS
+#undef CVC4_USE_STATISTICS
#include "cvc4_private_library.h"
-#ifndef __CVC4__STATISTICS_REGISTRY_H
-#define __CVC4__STATISTICS_REGISTRY_H
+#ifndef CVC4__STATISTICS_REGISTRY_H
+#define CVC4__STATISTICS_REGISTRY_H
#include <stdint.h>
std::ostream& operator<<(std::ostream& os, const timespec& t) CVC4_PUBLIC;
#ifdef CVC4_STATISTICS_ON
-# define __CVC4_USE_STATISTICS true
+# define CVC4_USE_STATISTICS true
#else
-# define __CVC4_USE_STATISTICS false
+# define CVC4_USE_STATISTICS false
#endif
*/
Stat(const std::string& name) : d_name(name)
{
- if(__CVC4_USE_STATISTICS) {
+ if(CVC4_USE_STATISTICS) {
CheckArgument(d_name.find(", ") == std::string::npos, name,
"Statistics names cannot include a comma (',')");
}
* May be redefined by a child class
*/
virtual void flushStat(std::ostream& out) const {
- if(__CVC4_USE_STATISTICS) {
+ if(CVC4_USE_STATISTICS) {
out << d_name << ", ";
flushInformation(out);
}
* May be redefined by a child class
*/
virtual void safeFlushStat(int fd) const {
- if (__CVC4_USE_STATISTICS) {
+ if (CVC4_USE_STATISTICS) {
safe_print(fd, d_name);
safe_print(fd, ", ");
safeFlushInformation(fd);
/** Flush the value of the statistic to the given output stream. */
void flushInformation(std::ostream& out) const override
{
- if(__CVC4_USE_STATISTICS) {
+ if(CVC4_USE_STATISTICS) {
out << getData();
}
}
void safeFlushInformation(int fd) const override
{
- if (__CVC4_USE_STATISTICS) {
+ if (CVC4_USE_STATISTICS) {
safe_print<T>(fd, getDataRef());
}
}
/** Set this reference statistic to refer to the given data cell. */
void setData(const T& t) override
{
- if(__CVC4_USE_STATISTICS) {
+ if(CVC4_USE_STATISTICS) {
d_data = &t;
}
}
/** Set the underlying data value to the given value. */
void setData(const T& t) override
{
- if(__CVC4_USE_STATISTICS) {
+ if(CVC4_USE_STATISTICS) {
d_data = t;
}
}
/** Identical to setData(). */
BackedStat<T>& operator=(const T& t) {
- if(__CVC4_USE_STATISTICS) {
+ if(CVC4_USE_STATISTICS) {
d_data = t;
}
return *this;
/** Increment the underlying integer statistic. */
IntStat& operator++() {
- if(__CVC4_USE_STATISTICS) {
+ if(CVC4_USE_STATISTICS) {
++d_data;
}
return *this;
/** Increment the underlying integer statistic by the given amount. */
IntStat& operator+=(int64_t val) {
- if(__CVC4_USE_STATISTICS) {
+ if(CVC4_USE_STATISTICS) {
d_data += val;
}
return *this;
/** Keep the maximum of the current statistic value and the given one. */
void maxAssign(int64_t val) {
- if(__CVC4_USE_STATISTICS) {
+ if(CVC4_USE_STATISTICS) {
if(d_data < val) {
d_data = val;
}
/** Keep the minimum of the current statistic value and the given one. */
void minAssign(int64_t val) {
- if(__CVC4_USE_STATISTICS) {
+ if(CVC4_USE_STATISTICS) {
if(d_data > val) {
d_data = val;
}
/** Add an entry to the running-average calculation. */
void addEntry(double e) {
- if(__CVC4_USE_STATISTICS) {
+ if(CVC4_USE_STATISTICS) {
++d_count;
d_sum += e;
setData(d_sum / d_count);
void flushInformation(std::ostream& out) const override
{
- if(__CVC4_USE_STATISTICS) {
+ if(CVC4_USE_STATISTICS) {
typename Histogram::const_iterator i = d_hist.begin();
typename Histogram::const_iterator end = d_hist.end();
out << "[";
void safeFlushInformation(int fd) const override
{
- if (__CVC4_USE_STATISTICS) {
+ if (CVC4_USE_STATISTICS) {
typename Histogram::const_iterator i = d_hist.begin();
typename Histogram::const_iterator end = d_hist.end();
safe_print(fd, "[");
}
HistogramStat& operator<<(const T& val){
- if(__CVC4_USE_STATISTICS) {
+ if(CVC4_USE_STATISTICS) {
if(d_hist.find(val) == d_hist.end()){
d_hist.insert(std::make_pair(val,0));
}
};/* class RegisterStatistic */
-#undef __CVC4_USE_STATISTICS
+#undef CVC4_USE_STATISTICS
}/* CVC4 namespace */
-#endif /* __CVC4__STATISTICS_REGISTRY_H */
+#endif /* CVC4__STATISTICS_REGISTRY_H */
#include "cvc4_public.h"
-#ifndef __CVC4__TUPLE_H
-#define __CVC4__TUPLE_H
+#ifndef CVC4__TUPLE_H
+#define CVC4__TUPLE_H
#include <iostream>
#include <string>
}/* CVC4 namespace */
-#endif /* __CVC4__TUPLE_H */
+#endif /* CVC4__TUPLE_H */
#include "cvc4_public.h"
-#ifndef __CVC4__UNSAFE_INTERRUPT_EXCEPTION_H
-#define __CVC4__UNSAFE_INTERRUPT_EXCEPTION_H
+#ifndef CVC4__UNSAFE_INTERRUPT_EXCEPTION_H
+#define CVC4__UNSAFE_INTERRUPT_EXCEPTION_H
#include "base/exception.h"
}/* CVC4 namespace */
-#endif /* __CVC4__UNSAFE_INTERRUPT_EXCEPTION_H */
+#endif /* CVC4__UNSAFE_INTERRUPT_EXCEPTION_H */
#include "cvc4_private.h"
-#ifndef __CVC4__UTILITY_H
-#define __CVC4__UTILITY_H
+#ifndef CVC4__UTILITY_H
+#define CVC4__UTILITY_H
#include <algorithm>
#include <utility>
}/* CVC4 namespace */
-#endif /* __CVC4__UTILITY_H */
+#endif /* CVC4__UTILITY_H */