summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/cegqi
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/cegqi')
-rw-r--r--src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp8
-rw-r--r--src/theory/quantifiers/cegqi/ceg_arith_instantiator.h4
-rw-r--r--src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp6
-rw-r--r--src/theory/quantifiers/cegqi/ceg_bv_instantiator.h4
-rw-r--r--src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp6
-rw-r--r--src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h4
-rw-r--r--src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp6
-rw-r--r--src/theory/quantifiers/cegqi/ceg_dt_instantiator.h4
-rw-r--r--src/theory/quantifiers/cegqi/ceg_instantiator.cpp10
-rw-r--r--src/theory/quantifiers/cegqi/ceg_instantiator.h8
-rw-r--r--src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp8
-rw-r--r--src/theory/quantifiers/cegqi/inst_strategy_cegqi.h4
-rw-r--r--src/theory/quantifiers/cegqi/nested_qe.cpp4
-rw-r--r--src/theory/quantifiers/cegqi/nested_qe.h4
-rw-r--r--src/theory/quantifiers/cegqi/vts_term_cache.cpp6
-rw-r--r--src/theory/quantifiers/cegqi/vts_term_cache.h4
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback