diff options
Diffstat (limited to 'src/theory/quantifiers/cegqi')
16 files changed, 45 insertions, 45 deletions
diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index b0a5688b2..29881a3a4 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -25,10 +25,10 @@ #include "util/random.h" using namespace std; -using namespace CVC4::kind; -using namespace CVC4::context; +using namespace CVC5::kind; +using namespace CVC5::context; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -1036,4 +1036,4 @@ Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci, } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h index 00b23307e..e6cfa31c6 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h @@ -22,7 +22,7 @@ #include "theory/quantifiers/cegqi/ceg_instantiator.h" #include "theory/quantifiers/cegqi/vts_term_cache.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -209,6 +209,6 @@ class ArithInstantiator : public Instantiator } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index 1c60058ff..2c163421e 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -23,9 +23,9 @@ #include "util/random.h" using namespace std; -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -759,4 +759,4 @@ void BvInstantiatorPreprocess::collectExtracts( } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h index 743a27af3..4bfda133e 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h @@ -21,7 +21,7 @@ #include "theory/quantifiers/bv_inverter.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -209,6 +209,6 @@ class BvInstantiatorPreprocess : public InstantiatorPreprocess } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp index c0ef3561f..85faea4b1 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp @@ -17,9 +17,9 @@ #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { namespace utils { @@ -342,4 +342,4 @@ Node normalizePvEqual( } // namespace utils } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h index 13b86cff4..576d68d06 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h @@ -20,7 +20,7 @@ #include "expr/attribute.h" #include "expr/node.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -104,5 +104,5 @@ Node normalizePvEqual( } // namespace utils } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp index c9bc63308..bb81d2790 100644 --- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp @@ -20,9 +20,9 @@ #include "theory/datatypes/theory_datatypes_utils.h" using namespace std; -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -180,4 +180,4 @@ Node DtInstantiator::solve_dt(Node v, Node a, Node b, Node sa, Node sb) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h index 97cb7a4ee..c0386465d 100644 --- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h @@ -20,7 +20,7 @@ #include "expr/node.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -91,6 +91,6 @@ class DtInstantiator : public Instantiator } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 5c6a932fd..118c505fc 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -32,9 +32,9 @@ #include "theory/rewriter.h" using namespace std; -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -1636,6 +1636,6 @@ bool Instantiator::processEqualTerm(CegInstantiator* ci, return ci->constructInstantiationInc(pv, n, pv_prop, sf); } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index 800398fb9..03161399c 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -23,7 +23,7 @@ #include "theory/inference_id.h" #include "util/statistics_registry.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -820,8 +820,8 @@ class InstantiatorPreprocess } }; -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 59b4cc7bd..d6a504713 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -26,10 +26,10 @@ #include "theory/rewriter.h" using namespace std; -using namespace CVC4::kind; -using namespace CVC4::context; +using namespace CVC5::kind; +using namespace CVC5::context; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -546,4 +546,4 @@ bool InstStrategyCegqi::processNestedQe(Node q, bool isPreregister) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index e0496a462..a5b79fb00 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -26,7 +26,7 @@ #include "theory/quantifiers/quant_module.h" #include "util/statistics_registry.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -215,6 +215,6 @@ class InstStrategyCegqi : public QuantifiersModule } } -} +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/cegqi/nested_qe.cpp b/src/theory/quantifiers/cegqi/nested_qe.cpp index 0e938ddae..9efc0ec31 100644 --- a/src/theory/quantifiers/cegqi/nested_qe.cpp +++ b/src/theory/quantifiers/cegqi/nested_qe.cpp @@ -19,7 +19,7 @@ #include "expr/subs.h" #include "theory/smt_engine_subsolver.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -152,4 +152,4 @@ Node NestedQe::doQe(Node q) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/cegqi/nested_qe.h b/src/theory/quantifiers/cegqi/nested_qe.h index 21a49424a..29df5d16b 100644 --- a/src/theory/quantifiers/cegqi/nested_qe.h +++ b/src/theory/quantifiers/cegqi/nested_qe.h @@ -23,7 +23,7 @@ #include "context/cdhashmap.h" #include "expr/node.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -81,6 +81,6 @@ class NestedQe } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp index 912fee2fd..1a7431038 100644 --- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp +++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp @@ -19,9 +19,9 @@ #include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/rewriter.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace quantifiers { @@ -296,4 +296,4 @@ bool VtsTermCache::containsVtsInfinity(Node n, bool isFree) } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.h b/src/theory/quantifiers/cegqi/vts_term_cache.h index 4f18933ec..53c198213 100644 --- a/src/theory/quantifiers/cegqi/vts_term_cache.h +++ b/src/theory/quantifiers/cegqi/vts_term_cache.h @@ -21,7 +21,7 @@ #include "expr/attribute.h" #include "expr/node.h" -namespace CVC4 { +namespace CVC5 { namespace theory { /** Attribute to mark Skolems as virtual terms */ @@ -140,6 +140,6 @@ class VtsTermCache } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H */ |