diff options
Diffstat (limited to 'src/theory')
191 files changed, 538 insertions, 538 deletions
diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h index 2d06e4be9..a9e7aa92c 100644 --- a/src/theory/arith/arith_ite_utils.h +++ b/src/theory/arith/arith_ite_utils.h @@ -19,8 +19,8 @@ #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> @@ -115,4 +115,4 @@ private: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H */ +#endif /* CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H */ diff --git a/src/theory/arith/arith_msum.h b/src/theory/arith/arith_msum.h index 44cce854c..8a9dbf791 100644 --- a/src/theory/arith/arith_msum.h +++ b/src/theory/arith/arith_msum.h @@ -14,8 +14,8 @@ #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> @@ -185,4 +185,4 @@ class ArithMSum } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARITH__MSUM_H */ +#endif /* CVC4__THEORY__ARITH__MSUM_H */ diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 88b931229..de6b3f228 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -17,8 +17,8 @@ #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" @@ -76,4 +76,4 @@ private: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARITH__ARITH_REWRITER_H */ +#endif /* CVC4__THEORY__ARITH__ARITH_REWRITER_H */ diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index d5f432187..bc77f8ec0 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -17,8 +17,8 @@ #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> @@ -72,4 +72,4 @@ private: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H */ +#endif /* CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H */ diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index aabc5326d..c8e92dfd3 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -16,8 +16,8 @@ #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> @@ -307,4 +307,4 @@ inline Node mkPi() }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARITH__ARITH_UTILITIES_H */ +#endif /* CVC4__THEORY__ARITH__ARITH_UTILITIES_H */ diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h index 308d63b0c..03b061504 100644 --- a/src/theory/arith/arithvar_node_map.h +++ b/src/theory/arith/arithvar_node_map.h @@ -17,8 +17,8 @@ #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" @@ -92,4 +92,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H */ +#endif /* CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H */ diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 36a347feb..f2c0c4b02 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -72,8 +72,8 @@ #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> @@ -1209,4 +1209,4 @@ private: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARITH__CONSTRAINT_H */ +#endif /* CVC4__THEORY__ARITH__CONSTRAINT_H */ diff --git a/src/theory/arith/constraint_forward.h b/src/theory/arith/constraint_forward.h index 4be468f80..5f3f2251d 100644 --- a/src/theory/arith/constraint_forward.h +++ b/src/theory/arith/constraint_forward.h @@ -16,8 +16,8 @@ ** 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> @@ -46,4 +46,4 @@ static const RationalVectorP RationalVectorPSentinel = NULL; }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARITH__CONSTRAINT_FORWARD_H */ +#endif /* CVC4__THEORY__ARITH__CONSTRAINT_FORWARD_H */ diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index a7842ddb2..0c26f9c55 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -17,8 +17,8 @@ #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> @@ -423,4 +423,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARITH__DIO_SOLVER_H */ +#endif /* CVC4__THEORY__ARITH__DIO_SOLVER_H */ diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index 043aa0db7..7452e322b 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -15,8 +15,8 @@ ** 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> @@ -1013,4 +1013,4 @@ class NonlinearExtension { } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H */ +#endif /* CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H */ diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index 36f8f20ad..a3d173cc7 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -17,8 +17,8 @@ #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> @@ -1393,4 +1393,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARITH__NORMAL_FORM_H */ +#endif /* CVC4__THEORY__ARITH__NORMAL_FORM_H */ diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index 6bc01f2f2..5006c6a9c 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -18,8 +18,8 @@ #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> @@ -416,4 +416,4 @@ private: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARITH__PARTIAL_MODEL_H */ +#endif /* CVC4__THEORY__ARITH__PARTIAL_MODEL_H */ diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index b75563f76..c32b612e2 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -16,8 +16,8 @@ #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 { @@ -185,4 +185,4 @@ class DivisibleOpTypeRule }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H */ +#endif /* CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H */ diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h index 2a6d55715..5c6bf63ce 100644 --- a/src/theory/arith/type_enumerator.h +++ b/src/theory/arith/type_enumerator.h @@ -16,8 +16,8 @@ #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" @@ -104,4 +104,4 @@ class IntegerEnumerator : public TypeEnumeratorBase<IntegerEnumerator> { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H */ +#endif /* CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H */ diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index c221569bb..7e18f9ed2 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -15,8 +15,8 @@ #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> @@ -211,4 +211,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARRAYS__ARRAY_INFO_H */ +#endif /* CVC4__THEORY__ARRAYS__ARRAY_INFO_H */ diff --git a/src/theory/arrays/array_proof_reconstruction.h b/src/theory/arrays/array_proof_reconstruction.h index 3c656de1a..37b014d35 100644 --- a/src/theory/arrays/array_proof_reconstruction.h +++ b/src/theory/arrays/array_proof_reconstruction.h @@ -15,8 +15,8 @@ #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" @@ -56,4 +56,4 @@ private: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H */ +#endif /* CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H */ diff --git a/src/theory/arrays/static_fact_manager.h b/src/theory/arrays/static_fact_manager.h index 135e46790..6b68edf26 100644 --- a/src/theory/arrays/static_fact_manager.h +++ b/src/theory/arrays/static_fact_manager.h @@ -18,8 +18,8 @@ #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> @@ -113,4 +113,4 @@ inline void StaticFactManager::setCanon(TNode n, TNode newParent) { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /*__CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H */ +#endif /*CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H */ diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 51e95844f..be80a081d 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -16,8 +16,8 @@ #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> @@ -491,4 +491,4 @@ class TheoryArrays : public Theory { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H */ +#endif /* CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H */ diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 21cc56dbc..5f3fcf48d 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -17,8 +17,8 @@ #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> @@ -509,4 +509,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H */ +#endif /* CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H */ diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index e789b8445..78756176d 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -16,8 +16,8 @@ #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" @@ -227,4 +227,4 @@ struct ArrayPartialSelectTypeRule { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H */ +#endif /* CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H */ diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h index 2e09763e4..5ca156b2e 100644 --- a/src/theory/arrays/type_enumerator.h +++ b/src/theory/arrays/type_enumerator.h @@ -16,8 +16,8 @@ #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" @@ -158,4 +158,4 @@ class ArrayEnumerator : public TypeEnumeratorBase<ArrayEnumerator> { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H */ +#endif /* CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H */ diff --git a/src/theory/arrays/union_find.h b/src/theory/arrays/union_find.h index 5b552c7f8..1f38f1280 100644 --- a/src/theory/arrays/union_find.h +++ b/src/theory/arrays/union_find.h @@ -18,8 +18,8 @@ #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> @@ -139,4 +139,4 @@ inline void UnionFind<NodeType, NodeHash>::setCanon(TNode n, TNode newParent) { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /*__CVC4__THEORY__ARRAYS__UNION_FIND_H */ +#endif /*CVC4__THEORY__ARRAYS__UNION_FIND_H */ diff --git a/src/theory/assertion.h b/src/theory/assertion.h index d68ff87aa..863a7e893 100644 --- a/src/theory/assertion.h +++ b/src/theory/assertion.h @@ -17,8 +17,8 @@ #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" @@ -49,4 +49,4 @@ std::ostream& operator<<(std::ostream& out, const Assertion& a); }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__ASSERTION_H */ +#endif /* CVC4__THEORY__ASSERTION_H */ diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index c5e1cc022..9c4798898 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -16,8 +16,8 @@ #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> @@ -313,4 +313,4 @@ class CircuitPropagator } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */ +#endif /* CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */ diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index 44abdf87d..abe024282 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -16,8 +16,8 @@ #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" @@ -44,4 +44,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__BOOLEANS__THEORY_BOOL_H */ +#endif /* CVC4__THEORY__BOOLEANS__THEORY_BOOL_H */ diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index d071e4e3d..02267cf2c 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -77,7 +77,7 @@ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode) /* 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); diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h index 4aad1e63f..250f36efa 100644 --- a/src/theory/booleans/theory_bool_rewriter.h +++ b/src/theory/booleans/theory_bool_rewriter.h @@ -17,8 +17,8 @@ #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" @@ -42,4 +42,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H */ +#endif /* CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H */ diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h index 427a1addb..18329b8b9 100644 --- a/src/theory/booleans/theory_bool_type_rules.h +++ b/src/theory/booleans/theory_bool_type_rules.h @@ -16,8 +16,8 @@ #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 { @@ -74,4 +74,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY_BOOL_TYPE_RULES_H */ +#endif /* CVC4__THEORY_BOOL_TYPE_RULES_H */ diff --git a/src/theory/booleans/type_enumerator.h b/src/theory/booleans/type_enumerator.h index 9628ee6e2..361216b10 100644 --- a/src/theory/booleans/type_enumerator.h +++ b/src/theory/booleans/type_enumerator.h @@ -16,8 +16,8 @@ #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" @@ -67,4 +67,4 @@ class BooleanEnumerator : public TypeEnumeratorBase<BooleanEnumerator> { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__BOOLEANS__TYPE_ENUMERATOR_H */ +#endif /* CVC4__THEORY__BOOLEANS__TYPE_ENUMERATOR_H */ diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index 3b2a57397..8a7d1bf7b 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -16,8 +16,8 @@ #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" @@ -38,4 +38,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H */ +#endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H */ diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h index 2fe91e8cb..5f703fa00 100644 --- a/src/theory/builtin/theory_builtin_rewriter.h +++ b/src/theory/builtin/theory_builtin_rewriter.h @@ -17,8 +17,8 @@ #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" @@ -130,4 +130,4 @@ private: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H */ +#endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H */ diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index adeec48a9..2c726d12f 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -16,8 +16,8 @@ #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" @@ -375,4 +375,4 @@ class SExprProperties { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H */ +#endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H */ diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h index 63c34161c..8ce17306f 100644 --- a/src/theory/builtin/type_enumerator.h +++ b/src/theory/builtin/type_enumerator.h @@ -16,8 +16,8 @@ #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" @@ -108,4 +108,4 @@ class FunctionEnumerator : public TypeEnumeratorBase<FunctionEnumerator> }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__BUILTIN_TYPE_ENUMERATOR_H */ +#endif /* CVC4__THEORY__BUILTIN_TYPE_ENUMERATOR_H */ diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h index 09e3ce10c..5472aa5a2 100644 --- a/src/theory/bv/abstraction.h +++ b/src/theory/bv/abstraction.h @@ -16,8 +16,8 @@ #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> diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h index cc821d333..8b63a9aa6 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.h +++ b/src/theory/bv/bitblast/aig_bitblaster.h @@ -16,8 +16,8 @@ #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" @@ -111,4 +111,4 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*> } // namespace bv } // namespace theory } // namespace CVC4 -#endif // __CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H +#endif // CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h index 6b8cafb7b..9e668e258 100644 --- a/src/theory/bv/bitblast/bitblast_strategies_template.h +++ b/src/theory/bv/bitblast/bitblast_strategies_template.h @@ -16,8 +16,8 @@ #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> diff --git a/src/theory/bv/bitblast/bitblast_utils.h b/src/theory/bv/bitblast/bitblast_utils.h index a4c4261d2..f2bee22e5 100644 --- a/src/theory/bv/bitblast/bitblast_utils.h +++ b/src/theory/bv/bitblast/bitblast_utils.h @@ -16,8 +16,8 @@ #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> @@ -269,4 +269,4 @@ T inline sLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqu } // namespace theory } // namespace CVC4 -#endif // __CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H +#endif // CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h index f29882b0d..df7cc4f11 100644 --- a/src/theory/bv/bitblast/bitblaster.h +++ b/src/theory/bv/bitblast/bitblaster.h @@ -16,8 +16,8 @@ #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> @@ -286,4 +286,4 @@ Node TBitblaster<T>::getTermModel(TNode node, bool fullModel) } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__BV__BITBLAST__BITBLASTER_H */ +#endif /* CVC4__THEORY__BV__BITBLAST__BITBLASTER_H */ diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h index 296014b76..d407b8131 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.h +++ b/src/theory/bv/bitblast/eager_bitblaster.h @@ -16,8 +16,8 @@ #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> @@ -88,4 +88,4 @@ class BitblastingRegistrar : public prop::Registrar } // namespace bv } // namespace theory } // namespace CVC4 -#endif // __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H +#endif // CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h index 920b669a6..ac5cd5c7f 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.h +++ b/src/theory/bv/bitblast/lazy_bitblaster.h @@ -16,8 +16,8 @@ #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" @@ -176,4 +176,4 @@ class TLazyBitblaster : public TBitblaster<Node> } // namespace bv } // namespace theory } // namespace CVC4 -#endif // __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H +#endif // CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h index 5322cca9a..8e42d5cab 100644 --- a/src/theory/bv/bv_eager_solver.h +++ b/src/theory/bv/bv_eager_solver.h @@ -16,8 +16,8 @@ #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> @@ -68,4 +68,4 @@ class EagerBitblastSolver { } // namespace theory } // namespace CVC4 -#endif // __CVC4__THEORY__BV__BV_EAGER_SOLVER_H +#endif // CVC4__THEORY__BV__BV_EAGER_SOLVER_H diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index a3a2f0445..07facf4af 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -16,8 +16,8 @@ #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> @@ -282,4 +282,4 @@ public: } } -#endif /* __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H */ +#endif /* CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H */ diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h index c1ac95946..75f39b6e0 100644 --- a/src/theory/bv/bv_quick_check.h +++ b/src/theory/bv/bv_quick_check.h @@ -16,8 +16,8 @@ #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> @@ -172,4 +172,4 @@ public: } /* theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__BV_QUICK_CHECK_H */ +#endif /* CVC4__BV_QUICK_CHECK_H */ diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 84a6f1b35..60660eda9 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -14,8 +14,8 @@ ** 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" @@ -117,4 +117,4 @@ class SubtheorySolver { } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__BV__BV_SUBTHEORY_H */ +#endif /* CVC4__THEORY__BV__BV_SUBTHEORY_H */ diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h index b64b229f9..e18c886df 100644 --- a/src/theory/bv/bv_subtheory_inequality.h +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -16,8 +16,8 @@ #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> @@ -83,4 +83,4 @@ public: } } -#endif /* __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */ +#endif /* CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */ diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index ec715d2f5..3ddbcaf36 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -28,8 +28,8 @@ #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 { @@ -251,4 +251,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__BV__SLICER_BV_H */ +#endif /* CVC4__THEORY__BV__SLICER_BV_H */ diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 55aad0ba7..7ca98f2ea 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -16,8 +16,8 @@ #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> @@ -273,4 +273,4 @@ public: }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__BV__THEORY_BV_H */ +#endif /* CVC4__THEORY__BV__THEORY_BV_H */ diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 8009daf3c..bf707c268 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -17,8 +17,8 @@ #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" @@ -109,4 +109,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__BV__THEORY_BV_REWRITER_H */ +#endif /* CVC4__THEORY__BV__THEORY_BV_REWRITER_H */ diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 79c69b9f0..64d04a37e 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -18,8 +18,8 @@ #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 { @@ -525,4 +525,4 @@ class BitVectorAckermanizationUremTypeRule } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H */ +#endif /* CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H */ diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h index 0bb67be42..90aae339b 100644 --- a/src/theory/bv/type_enumerator.h +++ b/src/theory/bv/type_enumerator.h @@ -16,8 +16,8 @@ #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" @@ -63,4 +63,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__BV__TYPE_ENUMERATOR_H */ +#endif /* CVC4__THEORY__BV__TYPE_ENUMERATOR_H */ diff --git a/src/theory/care_graph.h b/src/theory/care_graph.h index 12e63aa26..55851c1a4 100644 --- a/src/theory/care_graph.h +++ b/src/theory/care_graph.h @@ -16,8 +16,8 @@ #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> @@ -59,4 +59,4 @@ typedef std::set<CarePair> CareGraph; } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__CARE_GRAPH_H */ +#endif /* CVC4__THEORY__CARE_GRAPH_H */ diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index a6103a8c5..6c1d64e5b 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -16,8 +16,8 @@ #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" @@ -258,4 +258,4 @@ private: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H */ +#endif /* CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H */ diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index b10ec169b..95c259f2b 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -16,8 +16,8 @@ #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> diff --git a/src/theory/datatypes/sygus_simple_sym.h b/src/theory/datatypes/sygus_simple_sym.h index 0a4ed0c6e..815466d00 100644 --- a/src/theory/datatypes/sygus_simple_sym.h +++ b/src/theory/datatypes/sygus_simple_sym.h @@ -14,8 +14,8 @@ #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" @@ -104,4 +104,4 @@ class SygusSimpleSymBreak } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H */ +#endif /* CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H */ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index e5d037b38..b4803e69a 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -16,8 +16,8 @@ #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> @@ -370,4 +370,4 @@ private: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H */ +#endif /* CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H */ diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 6f7635209..22ac074f0 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -16,8 +16,8 @@ #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" @@ -433,4 +433,4 @@ class DtSyguEvalTypeRule } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H */ +#endif /* CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H */ diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index fff4731f3..a294324fa 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -16,8 +16,8 @@ #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" @@ -185,4 +185,4 @@ class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H */ +#endif /* CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H */ diff --git a/src/theory/decision_manager.h b/src/theory/decision_manager.h index 1cf0e5115..6825c1cf4 100644 --- a/src/theory/decision_manager.h +++ b/src/theory/decision_manager.h @@ -15,8 +15,8 @@ #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" @@ -116,4 +116,4 @@ class DecisionManager } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__DECISION_MANAGER__H */ +#endif /* CVC4__THEORY__DECISION_MANAGER__H */ diff --git a/src/theory/decision_strategy.h b/src/theory/decision_strategy.h index a01cf25c0..65b80b7f6 100644 --- a/src/theory/decision_strategy.h +++ b/src/theory/decision_strategy.h @@ -15,8 +15,8 @@ #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" @@ -143,4 +143,4 @@ class DecisionStrategySingleton : public DecisionStrategyFmf } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__DECISION_STRATEGY__H */ +#endif /* CVC4__THEORY__DECISION_STRATEGY__H */ diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h index fc96ea115..5c0e9b944 100644 --- a/src/theory/evaluator.h +++ b/src/theory/evaluator.h @@ -17,8 +17,8 @@ #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> @@ -110,4 +110,4 @@ class Evaluator } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__EVALUATOR_H */ +#endif /* CVC4__THEORY__EVALUATOR_H */ diff --git a/src/theory/example/ecdata.h b/src/theory/example/ecdata.h index 9941a6b89..c646725e8 100644 --- a/src/theory/example/ecdata.h +++ b/src/theory/example/ecdata.h @@ -17,8 +17,8 @@ #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" @@ -255,4 +255,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__UF__TIM__ECDATA_H */ +#endif /* CVC4__THEORY__UF__TIM__ECDATA_H */ diff --git a/src/theory/example/theory_uf_tim.h b/src/theory/example/theory_uf_tim.h index ba9733a95..20fd6bcfb 100644 --- a/src/theory/example/theory_uf_tim.h +++ b/src/theory/example/theory_uf_tim.h @@ -22,8 +22,8 @@ #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" @@ -210,4 +210,4 @@ typedef expr::Attribute<ECAttrTag, ECData*, ECCleanupStrategy> ECAttr; }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H */ +#endif /* CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H */ diff --git a/src/theory/ext_theory.h b/src/theory/ext_theory.h index 0ad314f6f..7ac79a4d6 100644 --- a/src/theory/ext_theory.h +++ b/src/theory/ext_theory.h @@ -30,8 +30,8 @@ #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> @@ -247,4 +247,4 @@ class ExtTheory } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__EXT_THEORY_H */ +#endif /* CVC4__THEORY__EXT_THEORY_H */ diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index 163da6fac..753030408 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -18,8 +18,8 @@ #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" @@ -355,4 +355,4 @@ class FpConverter } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__FP__THEORY_FP_H */ +#endif /* CVC4__THEORY__FP__THEORY_FP_H */ diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 49d457d7a..ad093f924 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -17,8 +17,8 @@ #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> @@ -148,4 +148,4 @@ class TheoryFp : public Theory { } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__FP__THEORY_FP_H */ +#endif /* CVC4__THEORY__FP__THEORY_FP_H */ diff --git a/src/theory/fp/theory_fp_rewriter.h b/src/theory/fp/theory_fp_rewriter.h index ec042dfe9..fef97afea 100644 --- a/src/theory/fp/theory_fp_rewriter.h +++ b/src/theory/fp/theory_fp_rewriter.h @@ -17,8 +17,8 @@ #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" @@ -64,4 +64,4 @@ class TheoryFpRewriter { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__FP__THEORY_FP_REWRITER_H */ +#endif /* CVC4__THEORY__FP__THEORY_FP_REWRITER_H */ diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h index 307247608..4022cc278 100644 --- a/src/theory/fp/theory_fp_type_rules.h +++ b/src/theory/fp/theory_fp_type_rules.h @@ -20,8 +20,8 @@ // 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 { @@ -806,4 +806,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H */ +#endif /* CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H */ diff --git a/src/theory/fp/type_enumerator.h b/src/theory/fp/type_enumerator.h index cd73ff824..4494fd40f 100644 --- a/src/theory/fp/type_enumerator.h +++ b/src/theory/fp/type_enumerator.h @@ -17,8 +17,8 @@ #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" @@ -132,4 +132,4 @@ class RoundingModeEnumerator } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__FP__TYPE_ENUMERATOR_H */ +#endif /* CVC4__THEORY__FP__TYPE_ENUMERATOR_H */ diff --git a/src/theory/interrupted.h b/src/theory/interrupted.h index 291528a78..905a98689 100644 --- a/src/theory/interrupted.h +++ b/src/theory/interrupted.h @@ -26,8 +26,8 @@ #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" @@ -40,4 +40,4 @@ class Interrupted : public CVC4::Exception { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__INTERRUPTED_H */ +#endif /* CVC4__THEORY__INTERRUPTED_H */ diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index 4c35b8d7f..a765472dd 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -18,8 +18,8 @@ #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> @@ -279,4 +279,4 @@ std::ostream& operator<<(std::ostream& out, const LogicInfo& logic) CVC4_PUBLIC; }/* CVC4 namespace */ -#endif /* __CVC4__LOGIC_INFO_H */ +#endif /* CVC4__LOGIC_INFO_H */ diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 38fd94003..347177b93 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -16,8 +16,8 @@ #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> @@ -194,4 +194,4 @@ class OutputChannel { } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__OUTPUT_CHANNEL_H */ +#endif /* CVC4__THEORY__OUTPUT_CHANNEL_H */ diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h index 5ab7d0fc2..b5d68f233 100644 --- a/src/theory/quantifiers/alpha_equivalence.h +++ b/src/theory/quantifiers/alpha_equivalence.h @@ -14,8 +14,8 @@ #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" diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h index e02c85866..3a7dc2da8 100644 --- a/src/theory/quantifiers/anti_skolem.h +++ b/src/theory/quantifiers/anti_skolem.h @@ -14,8 +14,8 @@ #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> diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h index b4cfe2bed..746bfba9a 100644 --- a/src/theory/quantifiers/bv_inverter.h +++ b/src/theory/quantifiers/bv_inverter.h @@ -14,8 +14,8 @@ #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> @@ -130,4 +130,4 @@ class BvInverter } // namespace theory } // namespace CVC4 -#endif /* __CVC4__BV_INVERTER_H */ +#endif /* CVC4__BV_INVERTER_H */ diff --git a/src/theory/quantifiers/bv_inverter_utils.h b/src/theory/quantifiers/bv_inverter_utils.h index 4ab677f0e..264b42ef5 100644 --- a/src/theory/quantifiers/bv_inverter_utils.h +++ b/src/theory/quantifiers/bv_inverter_utils.h @@ -14,8 +14,8 @@ #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" diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index 9daaa970e..b68b20998 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -14,8 +14,8 @@ #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> @@ -145,4 +145,4 @@ class CandidateRewriteDatabaseGen } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H */ diff --git a/src/theory/quantifiers/candidate_rewrite_filter.h b/src/theory/quantifiers/candidate_rewrite_filter.h index 63d5d6fec..af9ac6d87 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.h +++ b/src/theory/quantifiers/candidate_rewrite_filter.h @@ -16,8 +16,8 @@ #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" @@ -223,4 +223,4 @@ class CandidateRewriteFilter } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h index 5bc75f801..8799ce1cd 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h @@ -14,8 +14,8 @@ #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" @@ -203,4 +203,4 @@ class ArithInstantiator : public Instantiator } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h index b9c35b3e0..466eba6a2 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h @@ -14,8 +14,8 @@ #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" @@ -211,4 +211,4 @@ class BvInstantiatorPreprocess : public InstantiatorPreprocess } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h index 3156e745c..7c72a29f2 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h @@ -14,8 +14,8 @@ #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" diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h index ea3db0e9b..cf9736abe 100644 --- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h @@ -14,8 +14,8 @@ #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" @@ -93,4 +93,4 @@ class DtInstantiator : public Instantiator } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h index 2ed76ba27..05932de7e 100644 --- a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h @@ -14,8 +14,8 @@ #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> @@ -106,4 +106,4 @@ class EprInstantiator : public Instantiator } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index a813c91b0..0a09f39c7 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -15,8 +15,8 @@ #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" diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index c5c90b64a..ebebb808d 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -15,8 +15,8 @@ #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" diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h index 6d0a1625c..969b6bf93 100644 --- a/src/theory/quantifiers/dynamic_rewrite.h +++ b/src/theory/quantifiers/dynamic_rewrite.h @@ -14,8 +14,8 @@ #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> @@ -121,4 +121,4 @@ class DynamicRewriter } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H */ diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h index d2718fa1f..8cff12477 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.h +++ b/src/theory/quantifiers/ematching/candidate_generator.h @@ -14,8 +14,8 @@ #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" @@ -212,4 +212,4 @@ class CandidateGeneratorConsExpand : public CandidateGeneratorQE }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */ diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index b57db5799..6f0ff0635 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -14,8 +14,8 @@ #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> @@ -275,4 +275,4 @@ class HigherOrderTrigger : public Trigger } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H */ diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index f9fd2be25..3995c67b4 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -14,8 +14,8 @@ #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" diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index d715d7f7a..5eb992368 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -14,8 +14,8 @@ #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" diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index cd82e67a3..139adcb04 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -14,8 +14,8 @@ #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> @@ -95,4 +95,4 @@ class InstantiationEngine : public QuantifiersModule { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */ diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index 9a65f0c02..f276585d6 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -14,8 +14,8 @@ #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> @@ -464,4 +464,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__TRIGGER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_H */ diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h index be1d6d81d..69cd12a70 100644 --- a/src/theory/quantifiers/equality_infer.h +++ b/src/theory/quantifiers/equality_infer.h @@ -14,8 +14,8 @@ #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> diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h index 9b62c5714..e4eeeffa7 100644 --- a/src/theory/quantifiers/equality_query.h +++ b/src/theory/quantifiers/equality_query.h @@ -14,8 +14,8 @@ #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" @@ -120,4 +120,4 @@ class EqualityQueryQuantifiersEngine : public EqualityQuery }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H */ +#endif /* CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H */ diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index 9420b495a..233ef39f7 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -14,8 +14,8 @@ #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> @@ -106,4 +106,4 @@ class ExprMiner } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H */ diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h index dc0a8fab5..1c8aab826 100644 --- a/src/theory/quantifiers/expr_miner_manager.h +++ b/src/theory/quantifiers/expr_miner_manager.h @@ -14,8 +14,8 @@ #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" @@ -120,4 +120,4 @@ class ExpressionMinerManager } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H */ diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h index 920732e0f..836e15b7b 100644 --- a/src/theory/quantifiers/extended_rewrite.h +++ b/src/theory/quantifiers/extended_rewrite.h @@ -14,8 +14,8 @@ #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> @@ -250,4 +250,4 @@ class ExtendedRewriter } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H */ diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index dc257ea0a..bdf1d7c15 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -14,8 +14,8 @@ #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" @@ -218,4 +218,4 @@ class FirstOrderModelFmc : public FirstOrderModel }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__FIRST_ORDER_MODEL_H */ +#endif /* CVC4__FIRST_ORDER_MODEL_H */ diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index 1eab28fd9..55ed5bdd2 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -15,8 +15,8 @@ #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" diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index d662898c3..7dd1991f5 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -14,8 +14,8 @@ #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" @@ -162,4 +162,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H */ diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index b5f9c809a..1b4d24779 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -14,8 +14,8 @@ #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" @@ -60,4 +60,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H */ diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index 4202988ae..41bc312e7 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -14,8 +14,8 @@ #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" @@ -67,4 +67,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H */ diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h index f455d4a47..0282f0e40 100644 --- a/src/theory/quantifiers/fun_def_process.h +++ b/src/theory/quantifiers/fun_def_process.h @@ -14,8 +14,8 @@ #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> diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index db2f7b8a0..d298c43a8 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -14,8 +14,8 @@ #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> @@ -102,4 +102,4 @@ typedef CVC4::theory::inst::InstMatch InstMatch; }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */ diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h index 6f5b16bb1..4854616db 100644 --- a/src/theory/quantifiers/inst_match_trie.h +++ b/src/theory/quantifiers/inst_match_trie.h @@ -14,8 +14,8 @@ #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> @@ -436,4 +436,4 @@ class InstMatchTrieOrdered } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */ diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h index d82991b0a..d45b078ce 100644 --- a/src/theory/quantifiers/inst_propagator.h +++ b/src/theory/quantifiers/inst_propagator.h @@ -14,8 +14,8 @@ #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> diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index f011efdfc..920e643bc 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -14,8 +14,8 @@ #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" diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 25f333fbb..2fdb494e9 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -14,8 +14,8 @@ #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> @@ -374,4 +374,4 @@ class Instantiate : public QuantifiersUtil } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */ diff --git a/src/theory/quantifiers/lazy_trie.h b/src/theory/quantifiers/lazy_trie.h index ce6d841cc..8f822fcc0 100644 --- a/src/theory/quantifiers/lazy_trie.h +++ b/src/theory/quantifiers/lazy_trie.h @@ -12,8 +12,8 @@ ** \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" @@ -170,4 +170,4 @@ class LazyTrieMulti } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H */ diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h index 7a6182394..9793ea0a7 100644 --- a/src/theory/quantifiers/local_theory_ext.h +++ b/src/theory/quantifiers/local_theory_ext.h @@ -14,8 +14,8 @@ #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" diff --git a/src/theory/quantifiers/quant_epr.h b/src/theory/quantifiers/quant_epr.h index 9eda74d25..1284dde33 100644 --- a/src/theory/quantifiers/quant_epr.h +++ b/src/theory/quantifiers/quant_epr.h @@ -14,8 +14,8 @@ #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> @@ -101,4 +101,4 @@ class QuantEPR } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANT_EPR_H */ +#endif /* CVC4__THEORY__QUANT_EPR_H */ diff --git a/src/theory/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h index 43bb4c548..26a4630cd 100644 --- a/src/theory/quantifiers/quant_relevance.h +++ b/src/theory/quantifiers/quant_relevance.h @@ -14,8 +14,8 @@ #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> @@ -68,4 +68,4 @@ class QuantRelevance : public QuantifiersUtil } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANT_RELEVANCE_H */ +#endif /* CVC4__THEORY__QUANT_RELEVANCE_H */ diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index ec40bc52f..1a2aaa6cf 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -14,8 +14,8 @@ #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" diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index ba59c18e8..43861d6e9 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -14,8 +14,8 @@ #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> @@ -237,4 +237,4 @@ public: } } -#endif /* __CVC4__THEORY__QUANT_UTIL_H */ +#endif /* CVC4__THEORY__QUANT_UTIL_H */ diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 46cb5a4ce..329f9d08a 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -16,8 +16,8 @@ #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" diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index e44672d66..09f26b65b 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -16,8 +16,8 @@ #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" @@ -188,6 +188,6 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */ diff --git a/src/theory/quantifiers/query_generator.h b/src/theory/quantifiers/query_generator.h index b283d818b..749c78c85 100644 --- a/src/theory/quantifiers/query_generator.h +++ b/src/theory/quantifiers/query_generator.h @@ -15,8 +15,8 @@ #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> @@ -113,4 +113,4 @@ class QueryGenerator : public ExprMiner } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS___H */ +#endif /* CVC4__THEORY__QUANTIFIERS___H */ diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index ff419666f..8f348b471 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -14,8 +14,8 @@ #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" @@ -163,4 +163,4 @@ class RelevantDomain : public QuantifiersUtil }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */ diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index 88a9882ca..bbd6a1534 100644 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -15,8 +15,8 @@ #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" diff --git a/src/theory/quantifiers/single_inv_partition.h b/src/theory/quantifiers/single_inv_partition.h index 1a01f3b8b..0a4af3185 100644 --- a/src/theory/quantifiers/single_inv_partition.h +++ b/src/theory/quantifiers/single_inv_partition.h @@ -14,8 +14,8 @@ #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> @@ -294,4 +294,4 @@ class SingleInvocationPartition } /* namespace CVC4::theory */ } /* namespace CVC4 */ -#endif /* __CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H */ diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index 3db3aa838..f07bbdfd3 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -14,8 +14,8 @@ #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> @@ -143,4 +143,4 @@ class Skolemize } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H */ diff --git a/src/theory/quantifiers/solution_filter.h b/src/theory/quantifiers/solution_filter.h index 80af05eb8..bd4c62a09 100644 --- a/src/theory/quantifiers/solution_filter.h +++ b/src/theory/quantifiers/solution_filter.h @@ -14,8 +14,8 @@ #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> @@ -72,4 +72,4 @@ class SolutionFilterStrength : public ExprMiner } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H */ diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index 93b972fbc..4b24cbb1c 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -14,8 +14,8 @@ #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" diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h index bdafe7bef..40117af6c 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h @@ -14,8 +14,8 @@ #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" diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index f706e3d97..a295f6a40 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -14,8 +14,8 @@ #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" @@ -209,4 +209,4 @@ class Cegis : public SygusModule } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__CEGIS_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__CEGIS_H */ diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index 4255966c6..a2e7be1c1 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -13,8 +13,8 @@ **/ #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> diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h index 4d4c85703..687641e60 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.h +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h @@ -14,8 +14,8 @@ **/ #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" diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h index 5bfe60f49..d4c466b03 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator.h @@ -14,8 +14,8 @@ #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> @@ -454,4 +454,4 @@ class SygusEnumerator : public EnumValGenerator } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H */ diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.h b/src/theory/quantifiers/sygus/sygus_eval_unfold.h index ad1e3331d..adc54c6a7 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.h +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h @@ -14,8 +14,8 @@ #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" @@ -113,4 +113,4 @@ class SygusEvalUnfold } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H */ diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h index 522d6ee8a..ec29ab2a1 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.h +++ b/src/theory/quantifiers/sygus/sygus_explain.h @@ -14,8 +14,8 @@ #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> @@ -241,4 +241,4 @@ class SygusExplain } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H */ diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index e39943866..7dfa9b478 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -15,8 +15,8 @@ #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" diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h index e186fb02c..ae701113c 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h @@ -14,8 +14,8 @@ **/ #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> diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.h b/src/theory/quantifiers/sygus/sygus_grammar_red.h index eb43b5c3c..8ed080a30 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.h @@ -14,8 +14,8 @@ #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" @@ -116,4 +116,4 @@ class SygusRedundantCons } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H */ diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index a5b32cb0d..feb2d3313 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -14,8 +14,8 @@ #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> @@ -300,4 +300,4 @@ class NegContainsSygusInvarianceTest : public SygusInvarianceTest } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H */ diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index 07bce1791..d5e1de3fc 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -14,8 +14,8 @@ #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" @@ -148,4 +148,4 @@ class SygusModule } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H */ diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index 3738c40b7..e82ce01da 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -14,8 +14,8 @@ #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" diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h index 86e066b6b..e9ee340f4 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.h +++ b/src/theory/quantifiers/sygus/sygus_process_conj.h @@ -15,8 +15,8 @@ #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> diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index ee23d9732..bc3a58f9e 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -14,8 +14,8 @@ #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" @@ -215,4 +215,4 @@ class SygusRepairConst } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */ diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index f7a218ec0..a5215628c 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -14,8 +14,8 @@ #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" @@ -196,4 +196,4 @@ class SygusUnif } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index fced29871..7e9c5abd2 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -14,8 +14,8 @@ #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" @@ -489,4 +489,4 @@ class SygusUnifIo : public SygusUnif } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index 0f0b2c533..ada99dbaf 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -14,8 +14,8 @@ #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" @@ -434,4 +434,4 @@ class SygusUnifRl : public SygusUnif } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h index 54933a2af..1c691bd84 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.h +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h @@ -14,8 +14,8 @@ #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" @@ -429,4 +429,4 @@ class SygusUnifStrategy } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */ diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 923d1d57c..83a7eaa45 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -15,8 +15,8 @@ #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> diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index 2dbd20827..d5337e5d1 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -15,8 +15,8 @@ #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" diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index cdeaf1803..0f3d650d3 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -14,8 +14,8 @@ #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> @@ -599,4 +599,4 @@ class TermDbSygus { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */ diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index 3a2c42b9d..429b6f511 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -14,8 +14,8 @@ #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" @@ -322,4 +322,4 @@ class SygusSampler : public LazyTrieEvaluator } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H */ diff --git a/src/theory/quantifiers/term_canonize.h b/src/theory/quantifiers/term_canonize.h index b433992c8..8f7b8722e 100644 --- a/src/theory/quantifiers/term_canonize.h +++ b/src/theory/quantifiers/term_canonize.h @@ -14,8 +14,8 @@ #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" @@ -89,4 +89,4 @@ class TermCanonize } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H */ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index fcbd65729..148a18958 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -14,8 +14,8 @@ #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> @@ -409,4 +409,4 @@ class TermDb : public QuantifiersUtil { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */ diff --git a/src/theory/quantifiers/term_enumeration.h b/src/theory/quantifiers/term_enumeration.h index ed6529ef1..279680b1f 100644 --- a/src/theory/quantifiers/term_enumeration.h +++ b/src/theory/quantifiers/term_enumeration.h @@ -14,8 +14,8 @@ #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> @@ -82,4 +82,4 @@ class TermEnumeration } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H */ diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 061da81df..1f2eea1c5 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -14,8 +14,8 @@ #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> @@ -379,4 +379,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H */ diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index f6e19f700..b5b07f2e6 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -16,8 +16,8 @@ #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" @@ -62,4 +62,4 @@ class TheoryQuantifiers : public Theory { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H */ diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index 18aa7f6ee..ad1c4c69b 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -16,8 +16,8 @@ #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" @@ -229,4 +229,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H */ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 37d2deb40..61e9053f5 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -14,8 +14,8 @@ #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> @@ -431,4 +431,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS_ENGINE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS_ENGINE_H */ diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index 6e990051a..d972a7a84 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -14,8 +14,8 @@ #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> @@ -313,4 +313,4 @@ class RepBoundExt }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__REP_SET_H */ +#endif /* CVC4__THEORY__REP_SET_H */ diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 8d5d3442a..ae044f6d7 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -16,8 +16,8 @@ #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" @@ -331,4 +331,4 @@ class TheorySep : public Theory { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__SEP__THEORY_SEP_H */ +#endif /* CVC4__THEORY__SEP__THEORY_SEP_H */ diff --git a/src/theory/sep/theory_sep_rewriter.h b/src/theory/sep/theory_sep_rewriter.h index 6112632d8..f4639efa3 100644 --- a/src/theory/sep/theory_sep_rewriter.h +++ b/src/theory/sep/theory_sep_rewriter.h @@ -17,8 +17,8 @@ #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" @@ -49,4 +49,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__SEP__THEORY_SEP_REWRITER_H */ +#endif /* CVC4__THEORY__SEP__THEORY_SEP_REWRITER_H */ diff --git a/src/theory/sep/theory_sep_type_rules.h b/src/theory/sep/theory_sep_type_rules.h index 52a72e5dc..29adeda5a 100644 --- a/src/theory/sep/theory_sep_type_rules.h +++ b/src/theory/sep/theory_sep_type_rules.h @@ -16,8 +16,8 @@ #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 { @@ -112,4 +112,4 @@ struct SepNilTypeRule { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H */ +#endif /* CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H */ diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h index 9c5e4e9c8..d7c68a574 100644 --- a/src/theory/sets/normal_form.h +++ b/src/theory/sets/normal_form.h @@ -16,8 +16,8 @@ #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 { diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 3caa4ae16..414ba4b28 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -16,8 +16,8 @@ #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> @@ -71,4 +71,4 @@ class TheorySets : public Theory }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__SETS__THEORY_SETS_H */ +#endif /* CVC4__THEORY__SETS__THEORY_SETS_H */ diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 5cda78271..3014b2f2a 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -16,8 +16,8 @@ #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" @@ -334,4 +334,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H */ +#endif /* CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H */ diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h index af071dc60..463d02d6d 100644 --- a/src/theory/sets/theory_sets_rewriter.h +++ b/src/theory/sets/theory_sets_rewriter.h @@ -16,8 +16,8 @@ #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" @@ -89,4 +89,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H */ +#endif /* CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H */ diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h index cb6532abf..5a6745367 100644 --- a/src/theory/sets/theory_sets_type_enumerator.h +++ b/src/theory/sets/theory_sets_type_enumerator.h @@ -18,8 +18,8 @@ #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" @@ -183,4 +183,4 @@ class SetEnumerator : public TypeEnumeratorBase<SetEnumerator> { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__SETS__TYPE_ENUMERATOR_H */ +#endif /* CVC4__THEORY__SETS__TYPE_ENUMERATOR_H */ diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 1ba30f1e6..7e6038423 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -16,8 +16,8 @@ #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" @@ -428,4 +428,4 @@ struct SetsProperties { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H */ +#endif /* CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H */ diff --git a/src/theory/sort_inference.h b/src/theory/sort_inference.h index 98c85ebe7..5b28f669d 100644 --- a/src/theory/sort_inference.h +++ b/src/theory/sort_inference.h @@ -14,8 +14,8 @@ #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> diff --git a/src/theory/strings/normal_form.h b/src/theory/strings/normal_form.h index 73036e68f..3d1326570 100644 --- a/src/theory/strings/normal_form.h +++ b/src/theory/strings/normal_form.h @@ -14,8 +14,8 @@ #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> @@ -156,4 +156,4 @@ class NormalForm } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__STRINGS__NORMAL_FORM_H */ +#endif /* CVC4__THEORY__STRINGS__NORMAL_FORM_H */ diff --git a/src/theory/strings/regexp_elim.h b/src/theory/strings/regexp_elim.h index 6d2f28eaa..dbd4102b6 100644 --- a/src/theory/strings/regexp_elim.h +++ b/src/theory/strings/regexp_elim.h @@ -14,8 +14,8 @@ **/ #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" @@ -63,4 +63,4 @@ class RegExpElimination } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__STRINGS__REGEXP_ELIM_H */ +#endif /* CVC4__THEORY__STRINGS__REGEXP_ELIM_H */ diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index 4a7b7b293..b2e3667fc 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -16,8 +16,8 @@ #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> @@ -100,4 +100,4 @@ class RegExpOpr { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__STRINGS__REGEXP__OPERATION_H */ +#endif /* CVC4__THEORY__STRINGS__REGEXP__OPERATION_H */ diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h index 8b78e6ebc..13b66557a 100644 --- a/src/theory/strings/regexp_solver.h +++ b/src/theory/strings/regexp_solver.h @@ -15,8 +15,8 @@ #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" @@ -103,4 +103,4 @@ class RegExpSolver } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_H */ +#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_H */ diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index fd40e2521..c1e3c7214 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -14,8 +14,8 @@ #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> @@ -168,4 +168,4 @@ class SkolemCache } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__STRINGS__SKOLEM_CACHE_H */ +#endif /* CVC4__THEORY__STRINGS__SKOLEM_CACHE_H */ diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index e9d82a7b2..8371a27ea 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -16,8 +16,8 @@ #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" @@ -1166,4 +1166,4 @@ private: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_H */ +#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_H */ diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index daa109682..b96d619ef 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -16,8 +16,8 @@ #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" @@ -86,4 +86,4 @@ private: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__STRINGS__PREPROCESS_H */ +#endif /* CVC4__THEORY__STRINGS__PREPROCESS_H */ diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index 61031ea87..e8886d43b 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -15,8 +15,8 @@ #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> @@ -751,4 +751,4 @@ class TheoryStringsRewriter { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_REWRITER_H */ +#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_REWRITER_H */ diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 3ad28ee0f..91de8ac01 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -17,8 +17,8 @@ #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 { @@ -490,4 +490,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H */ +#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H */ diff --git a/src/theory/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h index 7327042e2..5ca0b624d 100644 --- a/src/theory/strings/type_enumerator.h +++ b/src/theory/strings/type_enumerator.h @@ -16,8 +16,8 @@ #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> @@ -128,4 +128,4 @@ class StringEnumeratorLength { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H */ +#endif /* CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H */ diff --git a/src/theory/subs_minimize.h b/src/theory/subs_minimize.h index 3f351de7e..3ffd588f1 100644 --- a/src/theory/subs_minimize.h +++ b/src/theory/subs_minimize.h @@ -14,8 +14,8 @@ #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> @@ -97,4 +97,4 @@ class SubstitutionMinimize } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__SUBS_MINIMIZE_H */ +#endif /* CVC4__THEORY__SUBS_MINIMIZE_H */ diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 31e98de3b..c19fb12f6 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -16,8 +16,8 @@ #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> @@ -199,4 +199,4 @@ std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::itera }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__SUBSTITUTIONS_H */ +#endif /* CVC4__THEORY__SUBSTITUTIONS_H */ diff --git a/src/theory/theory.h b/src/theory/theory.h index 02a0c9caf..cabb17f48 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -16,8 +16,8 @@ #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> @@ -915,4 +915,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__THEORY_H */ +#endif /* CVC4__THEORY__THEORY_H */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index ca761f97d..701d5cefb 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -16,8 +16,8 @@ #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> @@ -932,4 +932,4 @@ private: }/* CVC4 namespace */ -#endif /* __CVC4__THEORY_ENGINE_H */ +#endif /* CVC4__THEORY_ENGINE_H */ diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index c2bece0b4..baf3a401c 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -14,8 +14,8 @@ #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> @@ -351,4 +351,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__THEORY_MODEL_H */ +#endif /* CVC4__THEORY__THEORY_MODEL_H */ diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h index 91734fcf8..ce090b14d 100644 --- a/src/theory/theory_model_builder.h +++ b/src/theory/theory_model_builder.h @@ -14,8 +14,8 @@ #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> @@ -259,4 +259,4 @@ class TheoryEngineModelBuilder : public ModelBuilder } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__THEORY_MODEL_BUILDER_H */ +#endif /* CVC4__THEORY__THEORY_MODEL_BUILDER_H */ diff --git a/src/theory/theory_registrar.h b/src/theory/theory_registrar.h index 2e46fa4d8..822ae086c 100644 --- a/src/theory/theory_registrar.h +++ b/src/theory/theory_registrar.h @@ -20,8 +20,8 @@ #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" @@ -44,4 +44,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__THEORY_REGISTRAR_H */ +#endif /* CVC4__THEORY__THEORY_REGISTRAR_H */ diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index 889ea6eb1..ecda12dee 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -16,8 +16,8 @@ #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> @@ -124,4 +124,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__THEORY_TEST_UTILS_H */ +#endif /* CVC4__THEORY__THEORY_TEST_UTILS_H */ diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h index a68e3ca61..a92cfd2af 100644 --- a/src/theory/type_enumerator.h +++ b/src/theory/type_enumerator.h @@ -16,8 +16,8 @@ #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" @@ -185,4 +185,4 @@ class TypeEnumerator { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__TYPE_ENUMERATOR_H */ +#endif /* CVC4__THEORY__TYPE_ENUMERATOR_H */ diff --git a/src/theory/type_set.h b/src/theory/type_set.h index cada9422d..aed7ad80c 100644 --- a/src/theory/type_set.h +++ b/src/theory/type_set.h @@ -14,8 +14,8 @@ #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> @@ -87,4 +87,4 @@ class TypeSet } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__TYPE_SET_H */ +#endif /* CVC4__THEORY__TYPE_SET_H */ diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index 75216d10e..3813bb697 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -17,8 +17,8 @@ #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> @@ -360,4 +360,4 @@ struct TriggerInfo { } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H */ +#endif /* CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H */ diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index dd79b571a..d528e948f 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -41,8 +41,8 @@ #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> @@ -176,4 +176,4 @@ std::ostream& operator<<(std::ostream& out, const ::CVC4::theory::uf::SymmetryBr }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__UF__SYMMETRY_BREAKER_H */ +#endif /* CVC4__THEORY__UF__SYMMETRY_BREAKER_H */ diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index fb873e7dc..72dc04b10 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -17,8 +17,8 @@ #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" @@ -315,4 +315,4 @@ private: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__UF__THEORY_UF_H */ +#endif /* CVC4__THEORY__UF__THEORY_UF_H */ diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index f8c947d7a..4454b7e8c 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -14,8 +14,8 @@ #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" diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index d9b2cccaa..bad4189d6 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -17,8 +17,8 @@ #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" @@ -213,4 +213,4 @@ public: //conversion between HO_APPLY AND APPLY_UF }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__UF__THEORY_UF_REWRITER_H */ +#endif /* CVC4__THEORY__UF__THEORY_UF_REWRITER_H */ diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 41577f217..5dac994aa 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -14,8 +14,8 @@ #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" @@ -476,4 +476,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY_UF_STRONG_SOLVER_H */ +#endif /* CVC4__THEORY_UF_STRONG_SOLVER_H */ diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 013eb89a0..cb373b535 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -16,8 +16,8 @@ #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 { @@ -178,4 +178,4 @@ class HoApplyTypeRule { } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H */ +#endif /* CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H */ diff --git a/src/theory/valuation.h b/src/theory/valuation.h index c5abdb6ae..89f286a5e 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -18,8 +18,8 @@ #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" @@ -151,4 +151,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__VALUATION_H */ +#endif /* CVC4__THEORY__VALUATION_H */ |