diff options
Diffstat (limited to 'src/theory/quantifiers')
80 files changed, 213 insertions, 213 deletions
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 */ |