#define InternalError() CVC5_FATAL() << "Internal error detected "
-#define IllegalArgument(arg, msg...) \
- throw ::cvc5::internal::IllegalArgumentException( \
- "", \
- #arg, \
- __PRETTY_FUNCTION__, \
- ::cvc5::internal::IllegalArgumentException::formatVariadic(msg).c_str());
+#define IllegalArgument(arg, msg...) \
+ throw cvc5::internal::IllegalArgumentException( \
+ "", \
+ #arg, \
+ __PRETTY_FUNCTION__, \
+ cvc5::internal::IllegalArgumentException::formatVariadic(msg).c_str());
// This cannot use check argument directly as this forces
// CheckArgument to use a va_list. This is unsupported in Swig.
-#define PrettyCheckArgument(cond, arg, msg...) \
- do \
- { \
- if (__builtin_expect((!(cond)), false)) \
- { \
- throw ::cvc5::internal::IllegalArgumentException( \
- #cond, \
- #arg, \
- __PRETTY_FUNCTION__, \
- ::cvc5::internal::IllegalArgumentException::formatVariadic(msg).c_str()); \
- } \
+#define PrettyCheckArgument(cond, arg, msg...) \
+ do \
+ { \
+ if (__builtin_expect((!(cond)), false)) \
+ { \
+ throw cvc5::internal::IllegalArgumentException( \
+ #cond, \
+ #arg, \
+ __PRETTY_FUNCTION__, \
+ cvc5::internal::IllegalArgumentException::formatVariadic(msg) \
+ .c_str()); \
+ } \
} while (0)
#define AlwaysAssertArgument(cond, arg, msg...) \
do \
{ \
if (__builtin_expect((!(cond)), false)) \
{ \
- throw ::cvc5::internal::AssertArgumentException( \
+ throw cvc5::internal::AssertArgumentException( \
#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ##msg); \
} \
} while (0)
const char* tail CVC5_UNUSED)
{
if(__builtin_expect( ( !cond ), false )) {
- throw ::cvc5::internal::IllegalArgumentException("", "", tail);
+ throw cvc5::internal::IllegalArgumentException("", "", tail);
}
}
template <class T>
inline void CheckArgument(bool cond, const T& arg CVC5_UNUSED)
{
if(__builtin_expect( ( !cond ), false )) {
- throw ::cvc5::internal::IllegalArgumentException("", "", "");
+ throw cvc5::internal::IllegalArgumentException("", "", "");
}
}
* Supports:
* - std::map
* - std::unordered_map
- * - cvc5::internal::context::CDHashmap
- * - cvc5::internal::context::CDInsertHashmap
+ * - context::CDHashmap
+ * - context::CDInsertHashmap
* The ContainsKey function is also compatible with std::[unordered_]set.
*
* Currently implemented classes of functions:
#ifdef CVC5_MUZZLE
-#define Warning \
- ::cvc5::internal::__cvc5_true() ? ::cvc5::internal::nullStream : ::cvc5::internal::WarningChannel
-#define WarningOnce \
- ::cvc5::internal::__cvc5_true() ? ::cvc5::internal::nullStream : ::cvc5::internal::WarningChannel
-#define TraceIsOn ::cvc5::internal::__cvc5_true() ? false : ::cvc5::internal::TraceChannel.isOn
-#define Trace(tag) ::cvc5::internal::__cvc5_true() ? ::cvc5::internal::nullStream : ::cvc5::internal::TraceChannel()
+#define Warning \
+ cvc5::internal::__cvc5_true() ? cvc5::internal::nullStream \
+ : cvc5::internal::WarningChannel
+#define WarningOnce \
+ cvc5::internal::__cvc5_true() ? cvc5::internal::nullStream \
+ : cvc5::internal::WarningChannel
+#define TraceIsOn \
+ cvc5::internal::__cvc5_true() ? false : cvc5::internal::TraceChannel.isOn
+#define Trace(tag) \
+ cvc5::internal::__cvc5_true() ? cvc5::internal::nullStream \
+ : cvc5::internal::TraceChannel()
#else /* CVC5_MUZZLE */
-#define Warning \
- (!::cvc5::internal::WarningChannel.isOn()) ? ::cvc5::internal::nullStream : ::cvc5::internal::WarningChannel
-#define WarningOnce \
- (!::cvc5::internal::WarningChannel.isOn() \
- || !::cvc5::internal::WarningChannel.warnOnce(__FILE__, __LINE__)) \
- ? ::cvc5::internal::nullStream \
- : ::cvc5::internal::WarningChannel
+#define Warning \
+ (!cvc5::internal::WarningChannel.isOn()) ? cvc5::internal::nullStream \
+ : cvc5::internal::WarningChannel
+#define WarningOnce \
+ (!cvc5::internal::WarningChannel.isOn() \
+ || !cvc5::internal::WarningChannel.warnOnce(__FILE__, __LINE__)) \
+ ? cvc5::internal::nullStream \
+ : cvc5::internal::WarningChannel
#ifdef CVC5_TRACING
-#define TraceIsOn ::cvc5::internal::TraceChannel.isOn
-#define Trace(tag) !::cvc5::internal::TraceChannel.isOn(tag) ? ::cvc5::internal::nullStream : ::cvc5::internal::TraceChannel()
+#define TraceIsOn cvc5::internal::TraceChannel.isOn
+#define Trace(tag) \
+ !cvc5::internal::TraceChannel.isOn(tag) ? cvc5::internal::nullStream \
+ : cvc5::internal::TraceChannel()
#else /* CVC5_TRACING */
-#define TraceIsOn ::cvc5::internal::__cvc5_true() ? false : ::cvc5::internal::TraceChannel.isOn
-#define Trace(tag) ::cvc5::internal::__cvc5_true() ? ::cvc5::internal::nullStream : ::cvc5::internal::TraceChannel()
+#define TraceIsOn \
+ cvc5::internal::__cvc5_true() ? false : cvc5::internal::TraceChannel.isOn
+#define Trace(tag) \
+ cvc5::internal::__cvc5_true() ? cvc5::internal::nullStream \
+ : cvc5::internal::TraceChannel()
#endif /* CVC5_TRACING */
#endif /* CVC5_MUZZLE */
#include "base/configuration.h"
-const bool ::cvc5::internal::Configuration::GIT_BUILD = @GIT_BUILD@;
-const bool ::cvc5::internal::Configuration::CVC5_IS_RELEASE = @CVC5_IS_RELEASE@;
-const char* const ::cvc5::internal::Configuration::CVC5_VERSION = "@CVC5_VERSION@";
-const char* const ::cvc5::internal::Configuration::CVC5_FULL_VERSION = "@CVC5_FULL_VERSION@";
-const char* const ::cvc5::internal::Configuration::CVC5_GIT_INFO = "@CVC5_GIT_INFO@";
+const bool cvc5::internal::Configuration::GIT_BUILD = @GIT_BUILD@;
+const bool cvc5::internal::Configuration::CVC5_IS_RELEASE = @CVC5_IS_RELEASE@;
+const char* const cvc5::internal::Configuration::CVC5_VERSION = "@CVC5_VERSION@";
+const char* const cvc5::internal::Configuration::CVC5_FULL_VERSION = "@CVC5_FULL_VERSION@";
+const char* const cvc5::internal::Configuration::CVC5_GIT_INFO = "@CVC5_GIT_INFO@";
#include "context/cdhashmap_forward.h"
#include "context/context.h"
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
// Auxiliary class: almost the same as CDO (see cdo.h)
}; /* class CDHashMap<> */
-} // namespace context
-} // namespace cvc5::internal
+} // namespace cvc5::context
#endif /* CVC5__CONTEXT__CDHASHMAP_H */
/// \cond internals
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
template <class Key, class Data, class HashFcn = std::hash<Key> >
class CDHashMap;
-} // namespace context
-} // namespace cvc5::internal
+} // namespace cvc5::context
/// \endcond
#include "context/cdinsert_hashmap.h"
#include "context/context.h"
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
template <class V, class HashFcn = std::hash<V>>
class CDHashSet : protected CDInsertHashMap<V, bool, HashFcn>
}; /* class CDHashSet */
-} // namespace context
-} // namespace cvc5::internal
+} // namespace cvc5::context
#endif /* CVC5__CONTEXT__CDHASHSET_H */
#include <functional>
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
template <class V, class HashFcn = std::hash<V> >
class CDHashSet;
-} // namespace context
-} // namespace cvc5::internal
+} // namespace cvc5::context
#endif /* CVC5__CONTEXT__CDSET_FORWARD_H */
#pragma once
-namespace cvc5::internal {
-namespace context {
-
+namespace cvc5::context {
template <class Key, class Data, class HashFcn = std::hash<Key> >
class InsertHashMap {
};/* class CDInsertHashMap<> */
template <class Data, class HashFcn>
-class CDInsertHashMap<TNode, Data, HashFcn> : public ContextObj {
+class CDInsertHashMap<internal::TNode, Data, HashFcn> : public ContextObj
+{
/* CDInsertHashMap is challenging to get working with TNode.
* Consider using CDHashMap<TNode,...> instead.
*
"Cannot create a CDInsertHashMap with TNode keys");
};
-} // namespace context
-} // namespace cvc5::internal
+} // namespace cvc5::context
#include <functional>
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
template <class Key, class Data, class HashFcn = std::hash<Key> >
class CDInsertHashMap;
-} // namespace context
-} // namespace cvc5::internal
+} // namespace cvc5::context
#endif /* CVC5__CONTEXT__CDINSERT_HASHMAP_FORWARD_H */
#include "context/context.h"
#include "context/context_mm.h"
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
/**
* Generic context-dependent dynamic array. Note that for efficiency,
"Cannot create a CDList with a ContextMemoryAllocator.");
};
-} // namespace context
-} // namespace cvc5::internal
+} // namespace cvc5::context
#endif /* CVC5__CONTEXT__CDLIST_H */
/// \cond internals
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
template <class T>
class DefaultCleanUp {
/// \endcond
-} // namespace context
-} // namespace cvc5::internal
+} // namespace cvc5::context
#endif /* CVC5__CONTEXT__CDLIST_FORWARD_H */
#include "context/cdo.h"
#include "context/context.h"
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
class CDRaised {
private:
}
};/* class CDMaybe<T> */
-} // namespace context
-} // namespace cvc5::internal
+} // namespace cvc5::context
#include "context/context.h"
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
/**
* Most basic template for context-dependent objects. Simply makes a copy
};/* class CDO */
-} // namespace context
-} // namespace cvc5::internal
+} // namespace cvc5::context
#endif /* CVC5__CONTEXT__CDO_H */
#include "context/context.h"
#include "context/cdlist.h"
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
template <class T, class CleanUp = DefaultCleanUp<T>, class Allocator = std::allocator<T> >
class CDQueue;
};/* class CDQueue<> */
-} // namespace context
-} // namespace cvc5::internal
+} // namespace cvc5::context
#endif /* CVC5__CONTEXT__CDQUEUE_H */
#include "context/cdlist.h"
#include "context/cdo.h"
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
class Context;
};/* class CDTrailQueue<> */
-} // namespace context
-} // namespace cvc5::internal
+} // namespace cvc5::context
#endif /* CVC5__CONTEXT__CDTRAIL_QUEUE_H */
#include "base/check.h"
#include "context/context.h"
-namespace cvc5::internal {
-namespace context {
-
+namespace cvc5::context {
Context::Context() : d_pCNOpre(NULL), d_pCNOpost(NULL) {
// Create new memory manager
d_garbage.push_back(obj);
}
-} // namespace context
-} // namespace cvc5::internal
+} // namespace cvc5::context
#include "base/output.h"
#include "context/context_mm.h"
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
class Context;
class Scope;
d_pContextObjList = pContextObj;
}
-} // namespace context
-} // namespace cvc5::internal
+} // namespace cvc5::context
#endif /* CVC5__CONTEXT__CONTEXT_H */
#include "base/output.h"
#include "context/context_mm.h"
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
#ifndef CVC5_DEBUG_CONTEXT_MEMORY_MANAGER
#endif /* CVC5_DEBUG_CONTEXT_MEMORY_MANAGER */
-} // namespace context
-} // namespace cvc5::internal
+} // namespace cvc5::context
#endif
#include <vector>
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
#ifndef CVC5_DEBUG_CONTEXT_MEMORY_MANAGER
return a1.d_mm != a2.d_mm;
}
-} // namespace context
-} // namespace cvc5::internal
+} // namespace cvc5::context
#endif /* CVC5__CONTEXT__CONTEXT_MM_H */
* decide whether it's safe to modify big expressions by changing the grouping of
* the arguments. */
/* TODO: This could be generated. */
-bool isAssociative(::cvc5::internal::Kind k)
+bool isAssociative(cvc5::internal::Kind k)
{
switch(k) {
case kind::AND:
}
}
-std::string kindToString(::cvc5::internal::Kind k) { return toString(k); }
+std::string kindToString(cvc5::internal::Kind k) { return toString(k); }
} // namespace kind
namespace theory {
-TheoryId kindToTheoryId(::cvc5::internal::Kind k)
+TheoryId kindToTheoryId(cvc5::internal::Kind k)
{
switch (k)
{
throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind");
}
-TheoryId typeConstantToTheoryId(::cvc5::internal::TypeConstant typeConstant)
+TheoryId typeConstantToTheoryId(cvc5::internal::TypeConstant typeConstant)
{
switch (typeConstant)
{
// import Kind into the "cvc5" namespace but keep the individual kind
// constants under kind::
-typedef ::cvc5::internal::kind::Kind_t Kind;
+typedef cvc5::internal::kind::Kind_t Kind;
namespace kind {
* decide whether it's safe to modify big expressions by changing the grouping of
* the arguments. */
/* TODO: This could be generated. */
-bool isAssociative(::cvc5::internal::Kind k);
-std::string kindToString(::cvc5::internal::Kind k);
+bool isAssociative(cvc5::internal::Kind k);
+std::string kindToString(cvc5::internal::Kind k);
struct KindHashFunction
{
- inline size_t operator()(::cvc5::internal::Kind k) const { return k; }
+ inline size_t operator()(cvc5::internal::Kind k) const { return k; }
}; /* struct KindHashFunction */
} // namespace kind
namespace theory {
-::cvc5::internal::theory::TheoryId kindToTheoryId(::cvc5::internal::Kind k);
-::cvc5::internal::theory::TheoryId typeConstantToTheoryId(
- ::cvc5::internal::TypeConstant typeConstant);
+cvc5::internal::theory::TheoryId kindToTheoryId(cvc5::internal::Kind k);
+cvc5::internal::theory::TheoryId typeConstantToTheoryId(
+ cvc5::internal::TypeConstant typeConstant);
} // namespace theory
} // namespace cvc5::internal
template <Kind k, class T, bool pool>
struct NodeValueConstCompare
{
- static bool compare(const ::cvc5::internal::expr::NodeValue* x,
- const ::cvc5::internal::expr::NodeValue* y)
+ static bool compare(const cvc5::internal::expr::NodeValue* x,
+ const cvc5::internal::expr::NodeValue* y)
{
if (pool)
{
return x->getConst<T>() == y->getConst<T>();
}
- static size_t constHash(const ::cvc5::internal::expr::NodeValue* nv)
+ static size_t constHash(const cvc5::internal::expr::NodeValue* nv)
{
return nv->getConst<T>().hash();
}
};
-size_t NodeValueCompare::constHash(const ::cvc5::internal::expr::NodeValue* nv)
+size_t NodeValueCompare::constHash(const cvc5::internal::expr::NodeValue* nv)
{
Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
// clang-format off
${metakind_constHashes}
// clang-format on
-default: Unhandled() << ::cvc5::internal::expr::NodeValue::dKindToKind(nv->d_kind);
+ default:
+ Unhandled() << cvc5::internal::expr::NodeValue::dKindToKind(nv->d_kind);
}
}
template <bool pool>
-bool NodeValueCompare::compare(const ::cvc5::internal::expr::NodeValue* nv1,
- const ::cvc5::internal::expr::NodeValue* nv2)
+bool NodeValueCompare::compare(const cvc5::internal::expr::NodeValue* nv1,
+ const cvc5::internal::expr::NodeValue* nv2)
{
if(nv1->d_kind != nv2->d_kind) {
return false;
// clang-format off
${metakind_compares}
// clang-format on
-default: Unhandled() << ::cvc5::internal::expr::NodeValue::dKindToKind(nv1->d_kind);
+default:
+ Unhandled() << cvc5::internal::expr::NodeValue::dKindToKind(nv1->d_kind);
}
}
return false;
}
- ::cvc5::internal::expr::NodeValue::const_nv_iterator i = nv1->nv_begin();
- ::cvc5::internal::expr::NodeValue::const_nv_iterator j = nv2->nv_begin();
- ::cvc5::internal::expr::NodeValue::const_nv_iterator i_end = nv1->nv_end();
+ cvc5::internal::expr::NodeValue::const_nv_iterator i = nv1->nv_begin();
+ cvc5::internal::expr::NodeValue::const_nv_iterator j = nv2->nv_begin();
+ cvc5::internal::expr::NodeValue::const_nv_iterator i_end = nv1->nv_end();
while(i != i_end) {
if((*i) != (*j)) {
}
template bool NodeValueCompare::compare<true>(
- const ::cvc5::internal::expr::NodeValue* nv1, const ::cvc5::internal::expr::NodeValue* nv2);
+ const cvc5::internal::expr::NodeValue* nv1,
+ const cvc5::internal::expr::NodeValue* nv2);
template bool NodeValueCompare::compare<false>(
- const ::cvc5::internal::expr::NodeValue* nv1, const ::cvc5::internal::expr::NodeValue* nv2);
+ const cvc5::internal::expr::NodeValue* nv1,
+ const cvc5::internal::expr::NodeValue* nv2);
void nodeValueConstantToStream(std::ostream& out,
- const ::cvc5::internal::expr::NodeValue* nv)
+ const cvc5::internal::expr::NodeValue* nv)
{
Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
// clang-format off
${metakind_constPrinters}
// clang-format on
-default: Unhandled() << ::cvc5::internal::expr::NodeValue::dKindToKind(nv->d_kind);
+default:
+ Unhandled() << cvc5::internal::expr::NodeValue::dKindToKind(nv->d_kind);
}
}
* This doesn't support "non-inlined" NodeValues, which shouldn't need this
* kind of cleanup.
*/
-void deleteNodeValueConstant(::cvc5::internal::expr::NodeValue* nv)
+void deleteNodeValueConstant(cvc5::internal::expr::NodeValue* nv)
{
Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
// clang-format off
${metakind_constDeleters}
// clang-format on
-default: Unhandled() << ::cvc5::internal::expr::NodeValue::dKindToKind(nv->d_kind);
+default:
+ Unhandled() << cvc5::internal::expr::NodeValue::dKindToKind(nv->d_kind);
}
}
// re-enable the strict-aliasing warning
# pragma GCC diagnostic warning "-Wstrict-aliasing"
-uint32_t getMinArityForKind(::cvc5::internal::Kind k)
+uint32_t getMinArityForKind(cvc5::internal::Kind k)
{
static const unsigned lbs[] = {
0, /* NULL_EXPR */
return lbs[k];
}
-uint32_t getMaxArityForKind(::cvc5::internal::Kind k)
+uint32_t getMaxArityForKind(cvc5::internal::Kind k)
{
static const unsigned ubs[] = {
0, /* NULL_EXPR */
* example, since the kind of functions is just VARIABLE, it should map
* VARIABLE to APPLY_UF.
*/
-Kind operatorToKind(::cvc5::internal::expr::NodeValue* nv)
+Kind operatorToKind(cvc5::internal::expr::NodeValue* nv)
{
if(nv->getKind() == kind::BUILTIN) {
return nv->getConst<Kind>();
struct NodeValueCompare {
template <bool pool>
- static bool compare(const ::cvc5::internal::expr::NodeValue* nv1,
- const ::cvc5::internal::expr::NodeValue* nv2);
- static size_t constHash(const ::cvc5::internal::expr::NodeValue* nv);
+ static bool compare(const cvc5::internal::expr::NodeValue* nv1,
+ const cvc5::internal::expr::NodeValue* nv2);
+ static size_t constHash(const cvc5::internal::expr::NodeValue* nv);
};/* struct NodeValueCompare */
/**
* @param nv the node value representing a constant node
*/
void nodeValueConstantToStream(std::ostream& out,
- const ::cvc5::internal::expr::NodeValue* nv);
+ const cvc5::internal::expr::NodeValue* nv);
/**
* Cleanup to be performed when a NodeValue zombie is collected, and
* This doesn't support "non-inlined" NodeValues, which shouldn't need this
* kind of cleanup.
*/
-void deleteNodeValueConstant(::cvc5::internal::expr::NodeValue* nv);
+void deleteNodeValueConstant(cvc5::internal::expr::NodeValue* nv);
/** Return the minimum arity of the given kind. */
-uint32_t getMinArityForKind(::cvc5::internal::Kind k);
+uint32_t getMinArityForKind(cvc5::internal::Kind k);
/** Return the maximum arity of the given kind. */
-uint32_t getMaxArityForKind(::cvc5::internal::Kind k);
+uint32_t getMaxArityForKind(cvc5::internal::Kind k);
} // namespace metakind
// import MetaKind into the "cvc5::internal::kind" namespace but keep the
// individual MetaKind constants under kind::metakind::
-typedef ::cvc5::internal::kind::metakind::MetaKind_t MetaKind;
+typedef cvc5::internal::kind::metakind::MetaKind_t MetaKind;
/**
* Get the metakind for a particular kind.
* example, since the kind of functions is just VARIABLE, it should map
* VARIABLE to APPLY_UF.
*/
-Kind operatorToKind(::cvc5::internal::expr::NodeValue* nv);
+Kind operatorToKind(cvc5::internal::expr::NodeValue* nv);
} // namespace kind
struct NodeValuePoolEq {
bool operator()(const NodeValue* nv1, const NodeValue* nv2) const
{
- return ::cvc5::internal::kind::metakind::NodeValueCompare::compare<true>(nv1, nv2);
+ return cvc5::internal::kind::metakind::NodeValueCompare::compare<true>(nv1,
+ nv2);
}
};
namespace kind {
namespace metakind {
- template < ::cvc5::internal::Kind k, class T, bool pool>
+ template <cvc5::internal::Kind k, class T, bool pool>
struct NodeValueConstCompare;
struct NodeValueCompare;
class NodeValue
{
template <bool>
- friend class ::cvc5::internal::NodeTemplate;
- friend class ::cvc5::internal::TypeNode;
- friend class ::cvc5::internal::NodeBuilder;
- friend class ::cvc5::internal::NodeManager;
+ friend class cvc5::internal::NodeTemplate;
+ friend class cvc5::internal::TypeNode;
+ friend class cvc5::internal::NodeBuilder;
+ friend class cvc5::internal::NodeManager;
template <Kind k, class T, bool pool>
friend struct kind::metakind::NodeValueConstCompare;
#include "context/cdlist.h"
#include "context/cdo.h"
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5 {
namespace cvc5::internal {
-using ::cvc5::internal::context::CDHashMap;
-using ::cvc5::internal::context::CDHashSet;
-using ::cvc5::internal::context::Context;
-using ::std::copy;
-using ::std::endl;
-using ::std::ostream_iterator;
-using ::std::pair;
-using ::std::string;
-using ::std::vector;
+using context::CDHashMap;
+using context::CDHashSet;
+using context::Context;
+using std::copy;
+using std::endl;
+using std::ostream_iterator;
+using std::pair;
+using std::string;
+using std::vector;
/** Overloaded type trie.
*
private:
/** Learned literal map */
- typedef context::CDHashSet<Node> NodeSet;
+ using NodeSet = context::CDHashSet<Node>;
/** Learned literals */
NodeSet d_learnedLits;
};
#include "theory/substitutions.h"
#include "util/statistics_stats.h"
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
class Context;
}
+namespace cvc5::internal {
namespace preprocessing {
namespace passes {
Solver::Solver(Env& env,
cvc5::internal::prop::TheoryProxy* proxy,
- cvc5::internal::context::Context* context,
- cvc5::internal::context::UserContext* userContext,
+ context::Context* context,
+ context::UserContext* userContext,
ProofNodeManager* pnm,
bool enableIncremental)
: EnvObj(env),
cvc5::internal::prop::TheoryProxy* d_proxy;
/** The contexts from the SMT solver */
- cvc5::internal::context::Context* d_context;
+ context::Context* d_context;
/** The current assertion level (user) */
int assertionLevel;
//
Solver(Env& env,
cvc5::internal::prop::TheoryProxy* proxy,
- cvc5::internal::context::Context* context,
- cvc5::internal::context::UserContext* userContext,
+ context::Context* context,
+ context::UserContext* userContext,
ProofNodeManager* pnm,
bool enableIncremental = false);
virtual ~Solver();
static void toSatClause (const Minisat::Clause& clause, SatClause& sat_clause);
void initialize(context::Context* context,
TheoryProxy* theoryProxy,
- cvc5::internal::context::UserContext* userContext,
+ context::UserContext* userContext,
ProofNodeManager* pnm) override;
ClauseId addClause(SatClause& clause, bool removable) override;
SimpSolver::SimpSolver(Env& env,
cvc5::internal::prop::TheoryProxy* proxy,
- cvc5::internal::context::Context* context,
- cvc5::internal::context::UserContext* userContext,
+ context::Context* context,
+ context::UserContext* userContext,
ProofNodeManager* pnm,
bool enableIncremental)
: Solver(env, proxy, context, userContext, pnm, enableIncremental),
//
SimpSolver(Env& env,
cvc5::internal::prop::TheoryProxy* proxy,
- cvc5::internal::context::Context* context,
- cvc5::internal::context::UserContext* userContext,
+ context::Context* context,
+ context::UserContext* userContext,
ProofNodeManager* pnm,
bool enableIncremental = false);
~SimpSolver();
virtual void initialize(context::Context* context,
prop::TheoryProxy* theoryProxy,
- cvc5::internal::context::UserContext* userContext,
+ context::UserContext* userContext,
ProofNodeManager* pnm) = 0;
virtual void push() = 0;
#include "theory/theory_id.h"
#include "util/statistics_registry.h"
+namespace cvc5::context {
+class Context;
+class UserContext;
+} // namespace cvc5::context
+
namespace cvc5::internal {
class NodeManager;
}
using OutputTag = options::OutputTag;
-namespace context {
-class Context;
-class UserContext;
-} // namespace context
-
namespace smt {
class PfManager;
}
#include <memory>
#include "expr/node.h"
+
+namespace cvc5::context {
+class Context;
+class UserContext;
+} // namespace cvc5::context
+
namespace cvc5::internal {
class Env;
class Options;
class StatisticsRegistry;
-namespace context {
-class Context;
-class UserContext;
-} // namespace context
namespace options {
enum class OutputTag;
}
using namespace cvc5::internal::smt;
using namespace cvc5::internal::preprocessing;
using namespace cvc5::internal::prop;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
using namespace cvc5::internal::theory;
namespace cvc5::internal {
{
return d_state->getStatus();
}
-context::UserContext* SolverEngine::getUserContext()
+UserContext* SolverEngine::getUserContext()
{
return d_env->getUserContext();
}
-context::Context* SolverEngine::getContext() { return d_env->getContext(); }
+Context* SolverEngine::getContext()
+{
+ return d_env->getContext();
+}
TheoryEngine* SolverEngine::getTheoryEngine()
{
std::vector<Node> SolverEngine::getAssertionsInternal()
{
Assert(d_state->isFullyInited());
- const context::CDList<Node>& al = d_asserts->getAssertionList();
+ const CDList<Node>& al = d_asserts->getAssertionList();
std::vector<Node> res;
for (const Node& n : al)
{
void SolverEngine::checkModel(bool hardFailure)
{
- const context::CDList<Node>& al = d_asserts->getAssertionList();
+ const CDList<Node>& al = d_asserts->getAssertionList();
// we always enable the assertion list, so it is able to be checked
TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime);
#include "util/result.h"
#include "util/synth_result.h"
+namespace cvc5::context {
+class Context;
+class UserContext;
+} // namespace cvc5::context
+
namespace cvc5 {
class Solver;
/* -------------------------------------------------------------------------- */
-/* -------------------------------------------------------------------------- */
-
-namespace context {
-class Context;
-class UserContext;
-} // namespace context
-
-/* -------------------------------------------------------------------------- */
-
namespace preprocessing {
class PreprocessingPassContext;
}
namespace theory {
namespace arith {
-
-ArithStaticLearner::ArithStaticLearner(context::Context* userContext) :
- d_minMap(userContext),
- d_maxMap(userContext),
- d_statistics()
+ArithStaticLearner::ArithStaticLearner(context::Context* userContext)
+ : d_minMap(userContext), d_maxMap(userContext), d_statistics()
{
}
#include "theory/arith/delta_rational.h"
#include "util/statistics_stats.h"
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
class Context;
}
+
+namespace cvc5::internal {
namespace theory {
namespace arith {
CDNodeToMinMaxMap d_maxMap;
public:
- ArithStaticLearner(context::Context* userContext);
- ~ArithStaticLearner();
- void staticLearning(TNode n, NodeBuilder& learned);
-
- void addBound(TNode n);
+ ArithStaticLearner(context::Context* userContext);
+ ~ArithStaticLearner();
+ void staticLearning(TNode n, NodeBuilder& learned);
- private:
- void process(TNode n, NodeBuilder& learned, const TNodeSet& defTrue);
+ void addBound(TNode n);
- void iteMinMax(TNode n, NodeBuilder& learned);
- void iteConstant(TNode n, NodeBuilder& learned);
-
- /**
- * These fields are designed to be accessible to ArithStaticLearner methods.
- */
- class Statistics
- {
- public:
- IntStat d_iteMinMaxApplications;
- IntStat d_iteConstantApplications;
-
- Statistics();
- };
+private:
+ void process(TNode n, NodeBuilder& learned, const TNodeSet& defTrue);
+
+ void iteMinMax(TNode n, NodeBuilder& learned);
+ void iteConstant(TNode n, NodeBuilder& learned);
+
+ /**
+ * These fields are designed to be accessible to ArithStaticLearner methods.
+ */
+ class Statistics
+ {
+ public:
+ IntStat d_iteMinMaxApplications;
+ IntStat d_iteConstantApplications;
+
+ Statistics();
+ };
Statistics d_statistics;
#include "util/dense_map.h"
#include "util/statistics_stats.h"
+namespace cvc5::context {
+class Context;
+class UserContext;
+} // namespace cvc5::context
+
namespace cvc5::internal {
class ProofNodeManager;
class EagerProofGenerator;
-namespace context {
-class Context;
-class UserContext;
-}
-
namespace theory {
struct EeSetupInfo;
return v < d_varDatabases.size();
}
-
-ConstraintDatabase::Watches::Watches(context::Context* satContext, context::Context* userContext):
- d_constraintProofs(satContext),
- d_canBePropagatedWatches(satContext),
- d_assertionOrderWatches(satContext),
- d_splitWatches(userContext)
+ConstraintDatabase::Watches::Watches(context::Context* satContext,
+ context::Context* userContext)
+ : d_constraintProofs(satContext),
+ d_canBePropagatedWatches(satContext),
+ d_assertionOrderWatches(satContext),
+ d_splitWatches(userContext)
{}
#include "theory/arith/delta_rational.h"
#include "util/statistics_stats.h"
+namespace cvc5::context {
+class Context;
+}
namespace cvc5::internal {
class ProofNodeManager;
class EagerProofGenerator;
-namespace context {
-class Context;
-}
namespace theory {
namespace arith {
*/
enum ConstraintType {LowerBound, Equality, UpperBound, Disequality};
-
typedef context::CDList<ConstraintCP> CDConstraintList;
typedef std::unordered_map<Node, ConstraintP> NodetoConstraintMap;
*/
CDConstraintList d_antecedents;
- typedef context::CDList<ConstraintRule, Constraint::ConstraintRuleCleanup> ConstraintRuleList;
- typedef context::CDList<ConstraintP, Constraint::CanBePropagatedCleanup> CBPList;
- typedef context::CDList<ConstraintP, Constraint::AssertionOrderCleanup> AOList;
+ typedef context::CDList<ConstraintRule, Constraint::ConstraintRuleCleanup>
+ ConstraintRuleList;
+ typedef context::CDList<ConstraintP, Constraint::CanBePropagatedCleanup>
+ CBPList;
+ typedef context::CDList<ConstraintP, Constraint::AssertionOrderCleanup>
+ AOList;
typedef context::CDList<ConstraintP, Constraint::SplitCleanup> SplitList;
-
-
/**
* The watch lists are collected together as they need to be garbage collected
* carefully.
#include "util/rational.h"
#include "util/statistics_stats.h"
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
class Context;
}
+namespace cvc5::internal {
namespace theory {
namespace arith {
*/
context::CDO<size_t> d_nextInputConstraintToEnqueue;
-
/**
* We maintain a map from the variables associated with proofs to an input constraint.
* These variables can then be used in polynomial manipulations.
// /** Compare by d_minimal. */
// struct TrailMinimalCoefficientOrder {
// const context::CDList<Constraint>& d_trail;
- // TrailMinimalCoefficientOrder(const context::CDList<Constraint>& trail):
+ // TrailMinimalCoefficientOrder(const context::CDList<Constraint>&
+ // trail):
// d_trail(trail)
// {}
*/
context::CDQueue<TrailIndex> d_decompositionLemmaQueue;
-public:
-
+ public:
/** Construct a Diophantine equation solver with the given context. */
DioSolver(Env& env);
} // namespace
CoveringsProofGenerator::CoveringsProofGenerator(context::Context* ctx,
- ProofNodeManager* pnm)
+ ProofNodeManager* pnm)
: d_pnm(pnm), d_proofs(pnm, ctx), d_current(nullptr)
{
d_false = NodeManager::currentNM()->mkConst<bool>(false);
#include "expr/subs.h"
#include "smt/env_obj.h"
-namespace cvc5::internal {
-
-namespace context {
+namespace cvc5::context {
class Context;
}
+namespace cvc5::internal {
+
namespace theory {
class TheoryModel;
namespace theory {
namespace arith {
-ArithVariables::ArithVariables(context::Context* c, DeltaComputeCallback deltaComputingFunc)
- : d_vars(),
- d_safeAssignment(),
- d_numberOfVariables(0),
- d_pool(),
- d_released(),
- d_nodeToArithVarMap(),
- d_boundsQueue(),
- d_enqueueingBoundCounts(true),
- d_lbRevertHistory(c, true, LowerBoundCleanUp(this)),
- d_ubRevertHistory(c, true, UpperBoundCleanUp(this)),
- d_deltaIsSafe(false),
- d_delta(-1,1),
- d_deltaComputingFunc(deltaComputingFunc)
+ArithVariables::ArithVariables(context::Context* c,
+ DeltaComputeCallback deltaComputingFunc)
+ : d_vars(),
+ d_safeAssignment(),
+ d_numberOfVariables(0),
+ d_pool(),
+ d_released(),
+ d_nodeToArithVarMap(),
+ d_boundsQueue(),
+ d_enqueueingBoundCounts(true),
+ d_lbRevertHistory(c, true, LowerBoundCleanUp(this)),
+ d_ubRevertHistory(c, true, UpperBoundCleanUp(this)),
+ d_deltaIsSafe(false),
+ d_delta(-1, 1),
+ d_deltaComputingFunc(deltaComputingFunc)
{ }
ArithVar ArithVariables::getNumberOfVariables() const {
#include "theory/arith/constraint_forward.h"
#include "theory/arith/delta_rational.h"
-namespace cvc5::internal {
-namespace context {
+namespace cvc5::context {
class Context;
}
+namespace cvc5::internal {
namespace theory {
namespace arith {
public:
-
- ArithVariables(context::Context* c, DeltaComputeCallback deltaComputation);
-
- /**
- * This sets the lower bound for a variable in the current context.
- * This must be stronger the previous constraint.
- */
- void setLowerBoundConstraint(ConstraintP lb);
-
- /**
- * This sets the upper bound for a variable in the current context.
- * This must be stronger the previous constraint.
- */
- void setUpperBoundConstraint(ConstraintP ub);
-
- /** Returns the constraint for the upper bound of a variable. */
- inline ConstraintP getUpperBoundConstraint(ArithVar x) const{
- return d_vars[x].d_ub;
- }
+ ArithVariables(context::Context* c, DeltaComputeCallback deltaComputation);
+
+ /**
+ * This sets the lower bound for a variable in the current context.
+ * This must be stronger the previous constraint.
+ */
+ void setLowerBoundConstraint(ConstraintP lb);
+
+ /**
+ * This sets the upper bound for a variable in the current context.
+ * This must be stronger the previous constraint.
+ */
+ void setUpperBoundConstraint(ConstraintP ub);
+
+ /** Returns the constraint for the upper bound of a variable. */
+ inline ConstraintP getUpperBoundConstraint(ArithVar x) const
+ {
+ return d_vars[x].d_ub;
+ }
/** Returns the constraint for the lower bound of a variable. */
inline ConstraintP getLowerBoundConstraint(ArithVar x) const{
return d_vars[x].d_lb;
void branchVector(const std::vector<ArithVar>& lemmas);
context::CDO<unsigned> d_cutCount;
- context::CDHashSet<ArithVar, std::hash<ArithVar> > d_cutInContext;
+ context::CDHashSet<ArithVar, std::hash<ArithVar>> d_cutInContext;
context::CDO<bool> d_likelyIntegerInfeasible;
-
context::CDO<bool> d_guessedCoeffSet;
ArithRatPairVec d_guessedCoeffs;
in_stores->deleteSelf();
}
-ArrayInfo::ArrayInfo(context::Context* c,
- std::string statisticsPrefix)
+ArrayInfo::ArrayInfo(context::Context* c, std::string statisticsPrefix)
: ct(c),
info_map(),
d_mergeInfoTimer(smtStatisticsRegistry().registerTimer(
class Info {
public:
- context::CDO<bool> isNonLinear;
- context::CDO<bool> rIntro1Applied;
- context::CDO<TNode> modelRep;
- context::CDO<TNode> constArr;
- context::CDO<TNode> weakEquivPointer;
- context::CDO<TNode> weakEquivIndex;
- context::CDO<TNode> weakEquivSecondary;
- context::CDO<TNode> weakEquivSecondaryReason;
- CTNodeList* indices;
- CTNodeList* stores;
- CTNodeList* in_stores;
-
- Info(context::Context* c);
- ~Info();
-
- /**
- * prints the information
- */
- void print() const {
- Assert(indices != NULL && stores != NULL && in_stores != NULL);
- Trace("arrays-info")<<" indices ";
- printList(indices);
- Trace("arrays-info")<<" stores ";
- printList(stores);
- Trace("arrays-info")<<" in_stores ";
- printList(in_stores);
- }
+ context::CDO<bool> isNonLinear;
+ context::CDO<bool> rIntro1Applied;
+ context::CDO<TNode> modelRep;
+ context::CDO<TNode> constArr;
+ context::CDO<TNode> weakEquivPointer;
+ context::CDO<TNode> weakEquivIndex;
+ context::CDO<TNode> weakEquivSecondary;
+ context::CDO<TNode> weakEquivSecondaryReason;
+ CTNodeList* indices;
+ CTNodeList* stores;
+ CTNodeList* in_stores;
+
+ Info(context::Context* c);
+ ~Info();
+
+ /**
+ * prints the information
+ */
+ void print() const
+ {
+ Assert(indices != NULL && stores != NULL && in_stores != NULL);
+ Trace("arrays-info") << " indices ";
+ printList(indices);
+ Trace("arrays-info") << " stores ";
+ printList(stores);
+ Trace("arrays-info") << " in_stores ";
+ printList(in_stores);
+ }
};/* class Info */
typedef std::unordered_map<Node, Info*> CNodeInfoMap;
*/
class ArrayInfo {
private:
- context::Context* ct;
- CNodeInfoMap info_map;
-
- CTNodeList* emptyList;
-
- /* == STATISTICS == */
-
- /** time spent in preregisterTerm() */
- TimerStat d_mergeInfoTimer;
- AverageStat d_avgIndexListLength;
- AverageStat d_avgStoresListLength;
- AverageStat d_avgInStoresListLength;
- IntStat d_listsCount;
- IntStat d_callsMergeInfo;
- IntStat d_maxList;
- SizeStat<CNodeInfoMap> d_tableSize;
-
- /**
- * checks if a certain element is in the list l
- * FIXME: better way to check for duplicates?
- */
-
- /**
- * helper method that merges two lists into the first
- * without adding duplicates
- */
- void mergeLists(CTNodeList* la, const CTNodeList* lb) const;
+ context::Context* ct;
+ CNodeInfoMap info_map;
+
+ CTNodeList* emptyList;
+
+ /* == STATISTICS == */
+
+ /** time spent in preregisterTerm() */
+ TimerStat d_mergeInfoTimer;
+ AverageStat d_avgIndexListLength;
+ AverageStat d_avgStoresListLength;
+ AverageStat d_avgInStoresListLength;
+ IntStat d_listsCount;
+ IntStat d_callsMergeInfo;
+ IntStat d_maxList;
+ SizeStat<CNodeInfoMap> d_tableSize;
+
+ /**
+ * checks if a certain element is in the list l
+ * FIXME: better way to check for duplicates?
+ */
+
+ /**
+ * helper method that merges two lists into the first
+ * without adding duplicates
+ */
+ void mergeLists(CTNodeList* la, const CTNodeList* lb) const;
public:
const Info* emptyInfo;
&& weakEquiv)
{
// Replay all array merges to update weak equivalence data structures
- context::CDList<Node>::iterator it = d_arrayMerges.begin(), iend = d_arrayMerges.end();
+ context::CDList<Node>::iterator it = d_arrayMerges.begin(),
+ iend = d_arrayMerges.end();
TNode a, b, eq;
for (; it != iend; ++it) {
eq = *it;
using RowLemmaType = std::tuple<TNode, TNode, TNode, TNode>;
context::CDQueue<RowLemmaType> d_RowQueue;
- context::CDHashSet<RowLemmaType, RowLemmaTypeHashFunction > d_RowAlreadyAdded;
+ context::CDHashSet<RowLemmaType, RowLemmaTypeHashFunction> d_RowAlreadyAdded;
typedef context::CDHashSet<Node> CDNodeSet;
context::CDList<TNode> d_constReadsList;
context::Context* d_constReadsContext;
/** Helper class to keep d_constReadsContext in sync with satContext */
- class ContextPopper : public context::ContextNotifyObj {
+ class ContextPopper : public context::ContextNotifyObj
+ {
context::Context* d_satContext;
context::Context* d_contextToPop;
- protected:
- void contextNotifyPop() override
- {
- if (d_contextToPop->getLevel() > d_satContext->getLevel())
- {
- d_contextToPop->pop();
- }
+
+ protected:
+ void contextNotifyPop() override
+ {
+ if (d_contextToPop->getLevel() > d_satContext->getLevel())
+ {
+ d_contextToPop->pop();
+ }
}
- public:
+
+ public:
ContextPopper(context::Context* context, context::Context* contextToPop)
- :context::ContextNotifyObj(context), d_satContext(context),
- d_contextToPop(contextToPop)
- {}
+ : context::ContextNotifyObj(context),
+ d_satContext(context),
+ d_contextToPop(contextToPop)
+ {
+ }
- };/* class ContextPopper */
+ }; /* class ContextPopper */
ContextPopper d_contextPopper;
// The decision requests we have for the core
#include "expr/node.h"
#include "context/cdo.h"
-namespace cvc5::internal {
-
-namespace context {
- class Context;
- } // namespace context
+namespace cvc5::context {
+class Context;
+}
+namespace cvc5::internal {
namespace theory {
namespace arrays {
// NodeType \in { Node, TNode }
template <class NodeType, class NodeHash>
-class UnionFind : context::ContextNotifyObj {
+class UnionFind : context::ContextNotifyObj
+{
/** Our underlying map type. */
typedef std::unordered_map<NodeType, NodeType, NodeHash> MapType;
context::CDO<size_t> d_offset;
public:
- UnionFind(context::Context* ctxt) :
- context::ContextNotifyObj(ctxt),
- d_offset(ctxt, 0) {
+ UnionFind(context::Context* ctxt)
+ : context::ContextNotifyObj(ctxt), d_offset(ctxt, 0)
+ {
}
/**
*/
void notify();
-};/* class UnionFind<> */
+}; /* class UnionFind<> */
template <class NodeType, class NodeHash>
inline TNode UnionFind<NodeType, NodeHash>::debugFind(TNode n) const {
using namespace cvc5::internal;
AtomRequests::AtomRequests(context::Context* context)
-: d_allRequests(context)
-, d_requests(context)
-, d_triggerToRequestMap(context)
+ : d_allRequests(context),
+ d_requests(context),
+ d_triggerToRequestMap(context)
{}
AtomRequests::element_index AtomRequests::getList(TNode trigger) const {
#include "util/rational.h"
using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
using namespace cvc5::internal::kind;
namespace cvc5::internal {
#include "util/rational.h"
using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
using namespace cvc5::internal::kind;
namespace cvc5::internal {
d_bbInputFacts(context()),
d_assumptions(context()),
d_assertions(context()),
- d_epg(pnm ? new EagerProofGenerator(pnm, userContext(), "")
- : nullptr),
+ d_epg(pnm ? new EagerProofGenerator(pnm, userContext(), "") : nullptr),
d_factLiteralCache(context()),
d_literalFactCache(context()),
d_propagate(options().bv.bitvectorPropagate),
/** an SolverEngine for context */
context::Context* d_context;
-
};
} // namespace cvc5::internal
using namespace cvc5::internal;
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
using namespace cvc5::internal::theory;
using namespace cvc5::internal::theory::datatypes;
using namespace std;
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
}
TheoryDatatypes::EqcInfo::EqcInfo(context::Context* c)
- : d_inst(c, false),
- d_constructor(c, Node::null()),
- d_selectors(c, false)
+ : d_inst(c, false), d_constructor(c, Node::null()), d_selectors(c, false)
{}
bool TheoryDatatypes::hasLabel( EqcInfo* eqc, Node n ){
class EqcInfo
{
public:
- EqcInfo( context::Context* c );
- ~EqcInfo(){}
- //whether we have instantiatied this eqc
- context::CDO< bool > d_inst;
- //constructor equal to this eqc
- context::CDO< Node > d_constructor;
- //all selectors whose argument is this eqc
- context::CDO< bool > d_selectors;
+ EqcInfo(context::Context* c);
+ ~EqcInfo() {}
+ // whether we have instantiatied this eqc
+ context::CDO<bool> d_inst;
+ // constructor equal to this eqc
+ context::CDO<Node> d_constructor;
+ // all selectors whose argument is this eqc
+ context::CDO<bool> d_selectors;
};
/** does eqc of n have a label (do we know its constructor)? */
bool hasLabel( EqcInfo* eqc, Node n );
*/
class EngineOutputChannel : public theory::OutputChannel
{
- friend class TheoryEngine;
+ friend class internal::TheoryEngine;
public:
EngineOutputChannel(TheoryEngine* engine, theory::TheoryId theory);
#include "util/floatingpoint_literal_symfpu.h"
namespace symfpu {
-using namespace ::cvc5::internal::theory::fp::symfpuSymbolic;
-
-#define CVC5_SYM_ITE_DFN(T) \
- template <> \
- struct ite<symbolicProposition, T> \
- { \
- static const T iteOp(const symbolicProposition& _cond, \
- const T& _l, \
- const T& _r) \
- { \
- ::cvc5::internal::NodeManager* nm = ::cvc5::internal::NodeManager::currentNM(); \
- \
- ::cvc5::internal::Node cond = _cond; \
- ::cvc5::internal::Node l = _l; \
- ::cvc5::internal::Node r = _r; \
- \
- /* Handle some common symfpu idioms */ \
- if (cond.isConst()) \
- { \
- return (cond == nm->mkConst(::cvc5::internal::BitVector(1U, 1U))) ? l : r; \
- } \
- else \
- { \
- if (l.getKind() == ::cvc5::internal::kind::BITVECTOR_ITE) \
- { \
- if (l[1] == r) \
- { \
- return nm->mkNode( \
- ::cvc5::internal::kind::BITVECTOR_ITE, \
- nm->mkNode(::cvc5::internal::kind::BITVECTOR_AND, \
- cond, \
- nm->mkNode(::cvc5::internal::kind::BITVECTOR_NOT, l[0])), \
- l[2], \
- r); \
- } \
- else if (l[2] == r) \
- { \
- return nm->mkNode( \
- ::cvc5::internal::kind::BITVECTOR_ITE, \
- nm->mkNode(::cvc5::internal::kind::BITVECTOR_AND, cond, l[0]), \
- l[1], \
- r); \
- } \
- } \
- else if (r.getKind() == ::cvc5::internal::kind::BITVECTOR_ITE) \
- { \
- if (r[1] == l) \
- { \
- return nm->mkNode( \
- ::cvc5::internal::kind::BITVECTOR_ITE, \
- nm->mkNode(::cvc5::internal::kind::BITVECTOR_AND, \
- nm->mkNode(::cvc5::internal::kind::BITVECTOR_NOT, cond), \
- nm->mkNode(::cvc5::internal::kind::BITVECTOR_NOT, r[0])), \
- r[2], \
- l); \
- } \
- else if (r[2] == l) \
- { \
- return nm->mkNode( \
- ::cvc5::internal::kind::BITVECTOR_ITE, \
- nm->mkNode(::cvc5::internal::kind::BITVECTOR_AND, \
- nm->mkNode(::cvc5::internal::kind::BITVECTOR_NOT, cond), \
- r[0]), \
- r[1], \
- l); \
- } \
- } \
- } \
- return T(nm->mkNode(::cvc5::internal::kind::BITVECTOR_ITE, cond, l, r)); \
- } \
+using namespace cvc5::internal::theory::fp::symfpuSymbolic;
+
+#define CVC5_SYM_ITE_DFN(T) \
+ template <> \
+ struct ite<symbolicProposition, T> \
+ { \
+ static const T iteOp(const symbolicProposition& _cond, \
+ const T& _l, \
+ const T& _r) \
+ { \
+ cvc5::internal::NodeManager* nm = \
+ cvc5::internal::NodeManager::currentNM(); \
+ \
+ cvc5::internal::Node cond = _cond; \
+ cvc5::internal::Node l = _l; \
+ cvc5::internal::Node r = _r; \
+ \
+ /* Handle some common symfpu idioms */ \
+ if (cond.isConst()) \
+ { \
+ return (cond == nm->mkConst(cvc5::internal::BitVector(1U, 1U))) ? l \
+ : r; \
+ } \
+ else \
+ { \
+ if (l.getKind() == cvc5::internal::kind::BITVECTOR_ITE) \
+ { \
+ if (l[1] == r) \
+ { \
+ return nm->mkNode( \
+ cvc5::internal::kind::BITVECTOR_ITE, \
+ nm->mkNode( \
+ cvc5::internal::kind::BITVECTOR_AND, \
+ cond, \
+ nm->mkNode(cvc5::internal::kind::BITVECTOR_NOT, l[0])), \
+ l[2], \
+ r); \
+ } \
+ else if (l[2] == r) \
+ { \
+ return nm->mkNode( \
+ cvc5::internal::kind::BITVECTOR_ITE, \
+ nm->mkNode(cvc5::internal::kind::BITVECTOR_AND, cond, l[0]), \
+ l[1], \
+ r); \
+ } \
+ } \
+ else if (r.getKind() == cvc5::internal::kind::BITVECTOR_ITE) \
+ { \
+ if (r[1] == l) \
+ { \
+ return nm->mkNode( \
+ cvc5::internal::kind::BITVECTOR_ITE, \
+ nm->mkNode( \
+ cvc5::internal::kind::BITVECTOR_AND, \
+ nm->mkNode(cvc5::internal::kind::BITVECTOR_NOT, cond), \
+ nm->mkNode(cvc5::internal::kind::BITVECTOR_NOT, r[0])), \
+ r[2], \
+ l); \
+ } \
+ else if (r[2] == l) \
+ { \
+ return nm->mkNode( \
+ cvc5::internal::kind::BITVECTOR_ITE, \
+ nm->mkNode( \
+ cvc5::internal::kind::BITVECTOR_AND, \
+ nm->mkNode(cvc5::internal::kind::BITVECTOR_NOT, cond), \
+ r[0]), \
+ r[1], \
+ l); \
+ } \
+ } \
+ } \
+ return T(nm->mkNode(cvc5::internal::kind::BITVECTOR_ITE, cond, l, r)); \
+ } \
}
// Can (unsurprisingly) only ITE things which contain Nodes
symbolicBitVector<true> leadingZero(symbolicBitVector<true>::zero(1));
symbolicBitVector<true> base(symbolicBitVector<true>::allOnes(w - 1));
- return symbolicBitVector<true>(::cvc5::internal::NodeManager::currentNM()->mkNode(
- ::cvc5::internal::kind::BITVECTOR_CONCAT, leadingZero, base));
+ return symbolicBitVector<true>(
+ cvc5::internal::NodeManager::currentNM()->mkNode(
+ cvc5::internal::kind::BITVECTOR_CONCAT, leadingZero, base));
}
template <>
symbolicBitVector<true> leadingOne(symbolicBitVector<true>::one(1));
symbolicBitVector<true> base(symbolicBitVector<true>::zero(w - 1));
- return symbolicBitVector<true>(::cvc5::internal::NodeManager::currentNM()->mkNode(
- ::cvc5::internal::kind::BITVECTOR_CONCAT, leadingOne, base));
+ return symbolicBitVector<true>(
+ cvc5::internal::NodeManager::currentNM()->mkNode(
+ cvc5::internal::kind::BITVECTOR_CONCAT, leadingOne, base));
}
template <>
Node FpWordBlaster::propToNode(const prop& p) const
{
NodeManager* nm = NodeManager::currentNM();
- Node value =
- nm->mkNode(kind::EQUAL, p, nm->mkConst(::cvc5::internal::BitVector(1U, 1U)));
+ Node value = nm->mkNode(
+ kind::EQUAL, p, nm->mkConst(cvc5::internal::BitVector(1U, 1U)));
return value;
}
Node FpWordBlaster::ubvToNode(const ubv& u) const { return u; }
NodeManager* nm = NodeManager::currentNM();
handleLemma(
- nm->mkNode(kind::EQUAL, addA, nm->mkConst(::cvc5::internal::BitVector(1U, 1U))),
+ nm->mkNode(
+ kind::EQUAL, addA, nm->mkConst(cvc5::internal::BitVector(1U, 1U))),
InferenceId::FP_EQUATE_TERM);
++oldSize;
NodeManager* nm = NodeManager::currentNM();
handleLemma(
- nm->mkNode(kind::EQUAL,
- node,
- nm->mkNode(kind::EQUAL,
- wordBlasted,
- nm->mkConst(::cvc5::internal::BitVector(1U, 1U)))),
+ nm->mkNode(
+ kind::EQUAL,
+ node,
+ nm->mkNode(kind::EQUAL,
+ wordBlasted,
+ nm->mkConst(cvc5::internal::BitVector(1U, 1U)))),
InferenceId::FP_EQUATE_TERM);
}
else
/**
* Initialize the rewriter.
*/
-TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u)
-{
- /* Set up the pre-rewrite dispatch table */
- for (uint32_t i = 0; i < kind::LAST_KIND; ++i)
+ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u)
{
- d_preRewriteTable[i] = rewrite::notFP;
- }
+ /* Set up the pre-rewrite dispatch table */
+ for (uint32_t i = 0; i < kind::LAST_KIND; ++i)
+ {
+ d_preRewriteTable[i] = rewrite::notFP;
+ }
- /******** Constants ********/
- /* No rewriting possible for constants */
- d_preRewriteTable[kind::CONST_FLOATINGPOINT] = rewrite::identity;
- d_preRewriteTable[kind::CONST_ROUNDINGMODE] = rewrite::identity;
-
- /******** Sorts(?) ********/
- /* These kinds should only appear in types */
- // d_preRewriteTable[kind::ROUNDINGMODE_TYPE] = rewrite::type;
- d_preRewriteTable[kind::FLOATINGPOINT_TYPE] = rewrite::type;
-
- /******** Operations ********/
- d_preRewriteTable[kind::FLOATINGPOINT_FP] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_ABS] = rewrite::compactAbs;
- d_preRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation;
- d_preRewriteTable[kind::FLOATINGPOINT_ADD] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_SUB] =
- rewrite::convertSubtractionToAddition;
- d_preRewriteTable[kind::FLOATINGPOINT_MULT] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_DIV] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_FMA] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_SQRT] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_REM] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_RTI] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_MIN] = rewrite::compactMinMax;
- d_preRewriteTable[kind::FLOATINGPOINT_MAX] = rewrite::compactMinMax;
- d_preRewriteTable[kind::FLOATINGPOINT_MIN_TOTAL] = rewrite::compactMinMax;
- d_preRewriteTable[kind::FLOATINGPOINT_MAX_TOTAL] = rewrite::compactMinMax;
-
- /******** Comparisons ********/
- d_preRewriteTable[kind::FLOATINGPOINT_EQ] =
- rewrite::then<rewrite::breakChain, rewrite::ieeeEqToEq>;
- d_preRewriteTable[kind::FLOATINGPOINT_LEQ] =
- rewrite::then<rewrite::breakChain, rewrite::leqId>;
- d_preRewriteTable[kind::FLOATINGPOINT_LT] =
- rewrite::then<rewrite::breakChain, rewrite::ltId>;
- d_preRewriteTable[kind::FLOATINGPOINT_GEQ] =
- rewrite::then<rewrite::breakChain, rewrite::geqToleq>;
- d_preRewriteTable[kind::FLOATINGPOINT_GT] =
- rewrite::then<rewrite::breakChain, rewrite::gtTolt>;
-
- /******** Classifications ********/
- d_preRewriteTable[kind::FLOATINGPOINT_IS_NORMAL] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_IS_SUBNORMAL] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_IS_ZERO] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_IS_INF] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_IS_NAN] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_IS_NEG] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_IS_POS] = rewrite::identity;
-
- /******** Conversions ********/
- d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_FP] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_REAL] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_SBV] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_UBV] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_TO_UBV_TOTAL] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_TO_SBV_TOTAL] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_TO_REAL_TOTAL] = rewrite::identity;
-
- /******** Variables ********/
- d_preRewriteTable[kind::VARIABLE] = rewrite::variable;
- d_preRewriteTable[kind::BOUND_VARIABLE] = rewrite::variable;
- d_preRewriteTable[kind::SKOLEM] = rewrite::variable;
- d_preRewriteTable[kind::INST_CONSTANT] = rewrite::variable;
-
- d_preRewriteTable[kind::EQUAL] = rewrite::equal;
-
- /******** Components for bit-blasting ********/
- d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_NAN] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_INF] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_ZERO] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGN] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_EXPONENT] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND] =
- rewrite::identity;
- d_preRewriteTable[kind::ROUNDINGMODE_BITBLAST] = rewrite::identity;
-
- /* Set up the post-rewrite dispatch table */
- for (uint32_t i = 0; i < kind::LAST_KIND; ++i)
- {
- d_postRewriteTable[i] = rewrite::notFP;
- }
+ /******** Constants ********/
+ /* No rewriting possible for constants */
+ d_preRewriteTable[kind::CONST_FLOATINGPOINT] = rewrite::identity;
+ d_preRewriteTable[kind::CONST_ROUNDINGMODE] = rewrite::identity;
+
+ /******** Sorts(?) ********/
+ /* These kinds should only appear in types */
+ // d_preRewriteTable[kind::ROUNDINGMODE_TYPE] = rewrite::type;
+ d_preRewriteTable[kind::FLOATINGPOINT_TYPE] = rewrite::type;
+
+ /******** Operations ********/
+ d_preRewriteTable[kind::FLOATINGPOINT_FP] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_ABS] = rewrite::compactAbs;
+ d_preRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation;
+ d_preRewriteTable[kind::FLOATINGPOINT_ADD] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_SUB] =
+ rewrite::convertSubtractionToAddition;
+ d_preRewriteTable[kind::FLOATINGPOINT_MULT] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_DIV] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_FMA] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_SQRT] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_REM] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_RTI] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_MIN] = rewrite::compactMinMax;
+ d_preRewriteTable[kind::FLOATINGPOINT_MAX] = rewrite::compactMinMax;
+ d_preRewriteTable[kind::FLOATINGPOINT_MIN_TOTAL] = rewrite::compactMinMax;
+ d_preRewriteTable[kind::FLOATINGPOINT_MAX_TOTAL] = rewrite::compactMinMax;
+
+ /******** Comparisons ********/
+ d_preRewriteTable[kind::FLOATINGPOINT_EQ] =
+ rewrite::then<rewrite::breakChain, rewrite::ieeeEqToEq>;
+ d_preRewriteTable[kind::FLOATINGPOINT_LEQ] =
+ rewrite::then<rewrite::breakChain, rewrite::leqId>;
+ d_preRewriteTable[kind::FLOATINGPOINT_LT] =
+ rewrite::then<rewrite::breakChain, rewrite::ltId>;
+ d_preRewriteTable[kind::FLOATINGPOINT_GEQ] =
+ rewrite::then<rewrite::breakChain, rewrite::geqToleq>;
+ d_preRewriteTable[kind::FLOATINGPOINT_GT] =
+ rewrite::then<rewrite::breakChain, rewrite::gtTolt>;
+
+ /******** Classifications ********/
+ d_preRewriteTable[kind::FLOATINGPOINT_IS_NORMAL] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_IS_SUBNORMAL] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_IS_ZERO] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_IS_INF] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_IS_NAN] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_IS_NEG] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_IS_POS] = rewrite::identity;
+
+ /******** Conversions ********/
+ d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV] =
+ rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_FP] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_REAL] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_SBV] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_UBV] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_TO_UBV_TOTAL] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_TO_SBV_TOTAL] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_TO_REAL_TOTAL] = rewrite::identity;
+
+ /******** Variables ********/
+ d_preRewriteTable[kind::VARIABLE] = rewrite::variable;
+ d_preRewriteTable[kind::BOUND_VARIABLE] = rewrite::variable;
+ d_preRewriteTable[kind::SKOLEM] = rewrite::variable;
+ d_preRewriteTable[kind::INST_CONSTANT] = rewrite::variable;
+
+ d_preRewriteTable[kind::EQUAL] = rewrite::equal;
+
+ /******** Components for bit-blasting ********/
+ d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_NAN] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_INF] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_ZERO] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGN] = rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_EXPONENT] =
+ rewrite::identity;
+ d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND] =
+ rewrite::identity;
+ d_preRewriteTable[kind::ROUNDINGMODE_BITBLAST] = rewrite::identity;
+
+ /* Set up the post-rewrite dispatch table */
+ for (uint32_t i = 0; i < kind::LAST_KIND; ++i)
+ {
+ d_postRewriteTable[i] = rewrite::notFP;
+ }
- /******** Constants ********/
- /* No rewriting possible for constants */
- d_postRewriteTable[kind::CONST_FLOATINGPOINT] = rewrite::identity;
- d_postRewriteTable[kind::CONST_ROUNDINGMODE] = rewrite::identity;
-
- /******** Sorts(?) ********/
- /* These kinds should only appear in types */
- // d_postRewriteTable[kind::ROUNDINGMODE_TYPE] = rewrite::type;
- d_postRewriteTable[kind::FLOATINGPOINT_TYPE] = rewrite::type;
-
- /******** Operations ********/
- d_postRewriteTable[kind::FLOATINGPOINT_FP] = rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_ABS] = rewrite::compactAbs;
- d_postRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation;
- d_postRewriteTable[kind::FLOATINGPOINT_ADD] = rewrite::reorderBinaryOperation;
- d_postRewriteTable[kind::FLOATINGPOINT_SUB] = rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_MULT] =
- rewrite::reorderBinaryOperation;
- d_postRewriteTable[kind::FLOATINGPOINT_DIV] = rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_FMA] = rewrite::reorderFMA;
- d_postRewriteTable[kind::FLOATINGPOINT_SQRT] = rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_REM] = rewrite::compactRemainder;
- d_postRewriteTable[kind::FLOATINGPOINT_RTI] = rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_MIN] = rewrite::compactMinMax;
- d_postRewriteTable[kind::FLOATINGPOINT_MAX] = rewrite::compactMinMax;
- d_postRewriteTable[kind::FLOATINGPOINT_MIN_TOTAL] = rewrite::compactMinMax;
- d_postRewriteTable[kind::FLOATINGPOINT_MAX_TOTAL] = rewrite::compactMinMax;
-
- /******** Comparisons ********/
- d_postRewriteTable[kind::FLOATINGPOINT_EQ] = rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_LEQ] = rewrite::leqId;
- d_postRewriteTable[kind::FLOATINGPOINT_LT] = rewrite::ltId;
- d_postRewriteTable[kind::FLOATINGPOINT_GEQ] = rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_GT] = rewrite::identity;
-
- /******** Classifications ********/
- d_postRewriteTable[kind::FLOATINGPOINT_IS_NORMAL] =
- rewrite::removeSignOperations;
- d_postRewriteTable[kind::FLOATINGPOINT_IS_SUBNORMAL] =
- rewrite::removeSignOperations;
- d_postRewriteTable[kind::FLOATINGPOINT_IS_ZERO] =
- rewrite::removeSignOperations;
- d_postRewriteTable[kind::FLOATINGPOINT_IS_INF] =
- rewrite::removeSignOperations;
- d_postRewriteTable[kind::FLOATINGPOINT_IS_NAN] =
- rewrite::removeSignOperations;
- d_postRewriteTable[kind::FLOATINGPOINT_IS_NEG] = rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_IS_POS] = rewrite::identity;
-
- /******** Conversions ********/
- d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV] =
- rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_FP] = rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_REAL] = rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_SBV] =
- rewrite::toFPSignedBV;
- d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_UBV] = rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_TO_UBV_TOTAL] = rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_TO_SBV_TOTAL] = rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_TO_REAL_TOTAL] = rewrite::identity;
-
- /******** Variables ********/
- d_postRewriteTable[kind::VARIABLE] = rewrite::variable;
- d_postRewriteTable[kind::BOUND_VARIABLE] = rewrite::variable;
- d_postRewriteTable[kind::SKOLEM] = rewrite::variable;
- d_postRewriteTable[kind::INST_CONSTANT] = rewrite::variable;
-
- d_postRewriteTable[kind::EQUAL] = rewrite::equal;
-
- /******** Components for bit-blasting ********/
- d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_NAN] = rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_INF] = rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_ZERO] = rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGN] = rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_EXPONENT] =
- rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND] =
- rewrite::identity;
- d_postRewriteTable[kind::ROUNDINGMODE_BITBLAST] = rewrite::identity;
-
- /* Set up the post-rewrite constant fold table */
- for (uint32_t i = 0; i < kind::LAST_KIND; ++i)
- {
- // Note that this is identity, not notFP
- // Constant folding is called after post-rewrite
- // So may have to deal with cases of things being
- // re-written to non-floating-point sorts (i.e. true).
- d_constantFoldTable[i] = rewrite::identity;
- }
+ /******** Constants ********/
+ /* No rewriting possible for constants */
+ d_postRewriteTable[kind::CONST_FLOATINGPOINT] = rewrite::identity;
+ d_postRewriteTable[kind::CONST_ROUNDINGMODE] = rewrite::identity;
+
+ /******** Sorts(?) ********/
+ /* These kinds should only appear in types */
+ // d_postRewriteTable[kind::ROUNDINGMODE_TYPE] = rewrite::type;
+ d_postRewriteTable[kind::FLOATINGPOINT_TYPE] = rewrite::type;
+
+ /******** Operations ********/
+ d_postRewriteTable[kind::FLOATINGPOINT_FP] = rewrite::identity;
+ d_postRewriteTable[kind::FLOATINGPOINT_ABS] = rewrite::compactAbs;
+ d_postRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation;
+ d_postRewriteTable[kind::FLOATINGPOINT_ADD] =
+ rewrite::reorderBinaryOperation;
+ d_postRewriteTable[kind::FLOATINGPOINT_SUB] = rewrite::identity;
+ d_postRewriteTable[kind::FLOATINGPOINT_MULT] =
+ rewrite::reorderBinaryOperation;
+ d_postRewriteTable[kind::FLOATINGPOINT_DIV] = rewrite::identity;
+ d_postRewriteTable[kind::FLOATINGPOINT_FMA] = rewrite::reorderFMA;
+ d_postRewriteTable[kind::FLOATINGPOINT_SQRT] = rewrite::identity;
+ d_postRewriteTable[kind::FLOATINGPOINT_REM] = rewrite::compactRemainder;
+ d_postRewriteTable[kind::FLOATINGPOINT_RTI] = rewrite::identity;
+ d_postRewriteTable[kind::FLOATINGPOINT_MIN] = rewrite::compactMinMax;
+ d_postRewriteTable[kind::FLOATINGPOINT_MAX] = rewrite::compactMinMax;
+ d_postRewriteTable[kind::FLOATINGPOINT_MIN_TOTAL] = rewrite::compactMinMax;
+ d_postRewriteTable[kind::FLOATINGPOINT_MAX_TOTAL] = rewrite::compactMinMax;
+
+ /******** Comparisons ********/
+ d_postRewriteTable[kind::FLOATINGPOINT_EQ] = rewrite::identity;
+ d_postRewriteTable[kind::FLOATINGPOINT_LEQ] = rewrite::leqId;
+ d_postRewriteTable[kind::FLOATINGPOINT_LT] = rewrite::ltId;
+ d_postRewriteTable[kind::FLOATINGPOINT_GEQ] = rewrite::identity;
+ d_postRewriteTable[kind::FLOATINGPOINT_GT] = rewrite::identity;
+
+ /******** Classifications ********/
+ d_postRewriteTable[kind::FLOATINGPOINT_IS_NORMAL] =
+ rewrite::removeSignOperations;
+ d_postRewriteTable[kind::FLOATINGPOINT_IS_SUBNORMAL] =
+ rewrite::removeSignOperations;
+ d_postRewriteTable[kind::FLOATINGPOINT_IS_ZERO] =
+ rewrite::removeSignOperations;
+ d_postRewriteTable[kind::FLOATINGPOINT_IS_INF] =
+ rewrite::removeSignOperations;
+ d_postRewriteTable[kind::FLOATINGPOINT_IS_NAN] =
+ rewrite::removeSignOperations;
+ d_postRewriteTable[kind::FLOATINGPOINT_IS_NEG] = rewrite::identity;
+ d_postRewriteTable[kind::FLOATINGPOINT_IS_POS] = rewrite::identity;
+
+ /******** Conversions ********/
+ d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV] =
+ rewrite::identity;
+ d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_FP] = rewrite::identity;
+ d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_REAL] = rewrite::identity;
+ d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_SBV] =
+ rewrite::toFPSignedBV;
+ d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_UBV] = rewrite::identity;
+ d_postRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity;
+ d_postRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity;
+ d_postRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity;
+ d_postRewriteTable[kind::FLOATINGPOINT_TO_UBV_TOTAL] = rewrite::identity;
+ d_postRewriteTable[kind::FLOATINGPOINT_TO_SBV_TOTAL] = rewrite::identity;
+ d_postRewriteTable[kind::FLOATINGPOINT_TO_REAL_TOTAL] = rewrite::identity;
+
+ /******** Variables ********/
+ d_postRewriteTable[kind::VARIABLE] = rewrite::variable;
+ d_postRewriteTable[kind::BOUND_VARIABLE] = rewrite::variable;
+ d_postRewriteTable[kind::SKOLEM] = rewrite::variable;
+ d_postRewriteTable[kind::INST_CONSTANT] = rewrite::variable;
+
+ d_postRewriteTable[kind::EQUAL] = rewrite::equal;
+
+ /******** Components for bit-blasting ********/
+ d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_NAN] = rewrite::identity;
+ d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_INF] = rewrite::identity;
+ d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_ZERO] = rewrite::identity;
+ d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGN] = rewrite::identity;
+ d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_EXPONENT] =
+ rewrite::identity;
+ d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND] =
+ rewrite::identity;
+ d_postRewriteTable[kind::ROUNDINGMODE_BITBLAST] = rewrite::identity;
+
+ /* Set up the post-rewrite constant fold table */
+ for (uint32_t i = 0; i < kind::LAST_KIND; ++i)
+ {
+ // Note that this is identity, not notFP
+ // Constant folding is called after post-rewrite
+ // So may have to deal with cases of things being
+ // re-written to non-floating-point sorts (i.e. true).
+ d_constantFoldTable[i] = rewrite::identity;
+ }
- /******** Constants ********/
- /* Already folded! */
- d_constantFoldTable[kind::CONST_FLOATINGPOINT] = rewrite::identity;
- d_constantFoldTable[kind::CONST_ROUNDINGMODE] = rewrite::identity;
-
- /******** Sorts(?) ********/
- /* These kinds should only appear in types */
- d_constantFoldTable[kind::FLOATINGPOINT_TYPE] = rewrite::type;
-
- /******** Operations ********/
- d_constantFoldTable[kind::FLOATINGPOINT_FP] = constantFold::fpLiteral;
- d_constantFoldTable[kind::FLOATINGPOINT_ABS] = constantFold::abs;
- d_constantFoldTable[kind::FLOATINGPOINT_NEG] = constantFold::neg;
- d_constantFoldTable[kind::FLOATINGPOINT_ADD] = constantFold::add;
- d_constantFoldTable[kind::FLOATINGPOINT_MULT] = constantFold::mult;
- d_constantFoldTable[kind::FLOATINGPOINT_DIV] = constantFold::div;
- d_constantFoldTable[kind::FLOATINGPOINT_FMA] = constantFold::fma;
- d_constantFoldTable[kind::FLOATINGPOINT_SQRT] = constantFold::sqrt;
- d_constantFoldTable[kind::FLOATINGPOINT_REM] = constantFold::rem;
- d_constantFoldTable[kind::FLOATINGPOINT_RTI] = constantFold::rti;
- d_constantFoldTable[kind::FLOATINGPOINT_MIN] = constantFold::min;
- d_constantFoldTable[kind::FLOATINGPOINT_MAX] = constantFold::max;
- d_constantFoldTable[kind::FLOATINGPOINT_MIN_TOTAL] = constantFold::minTotal;
- d_constantFoldTable[kind::FLOATINGPOINT_MAX_TOTAL] = constantFold::maxTotal;
-
- /******** Comparisons ********/
- d_constantFoldTable[kind::FLOATINGPOINT_LEQ] = constantFold::leq;
- d_constantFoldTable[kind::FLOATINGPOINT_LT] = constantFold::lt;
-
- /******** Classifications ********/
- d_constantFoldTable[kind::FLOATINGPOINT_IS_NORMAL] = constantFold::isNormal;
- d_constantFoldTable[kind::FLOATINGPOINT_IS_SUBNORMAL] =
- constantFold::isSubnormal;
- d_constantFoldTable[kind::FLOATINGPOINT_IS_ZERO] = constantFold::isZero;
- d_constantFoldTable[kind::FLOATINGPOINT_IS_INF] = constantFold::isInfinite;
- d_constantFoldTable[kind::FLOATINGPOINT_IS_NAN] = constantFold::isNaN;
- d_constantFoldTable[kind::FLOATINGPOINT_IS_NEG] = constantFold::isNegative;
- d_constantFoldTable[kind::FLOATINGPOINT_IS_POS] = constantFold::isPositive;
-
- /******** Conversions ********/
- d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV] =
- constantFold::convertFromIEEEBitVectorLiteral;
- d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_FP] =
- constantFold::constantConvert;
- d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_REAL] =
- constantFold::convertFromRealLiteral;
- d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_SBV] =
- constantFold::convertFromSBV;
- d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_UBV] =
- constantFold::convertFromUBV;
- d_constantFoldTable[kind::FLOATINGPOINT_TO_UBV] = constantFold::convertToUBV;
- d_constantFoldTable[kind::FLOATINGPOINT_TO_SBV] = constantFold::convertToSBV;
- d_constantFoldTable[kind::FLOATINGPOINT_TO_REAL] =
- constantFold::convertToReal;
- d_constantFoldTable[kind::FLOATINGPOINT_TO_UBV_TOTAL] =
- constantFold::convertToUBVTotal;
- d_constantFoldTable[kind::FLOATINGPOINT_TO_SBV_TOTAL] =
- constantFold::convertToSBVTotal;
- d_constantFoldTable[kind::FLOATINGPOINT_TO_REAL_TOTAL] =
- constantFold::convertToRealTotal;
-
- /******** Variables ********/
- d_constantFoldTable[kind::VARIABLE] = rewrite::variable;
- d_constantFoldTable[kind::BOUND_VARIABLE] = rewrite::variable;
-
- d_constantFoldTable[kind::EQUAL] = constantFold::equal;
-
- /******** Components for bit-blasting ********/
- d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_NAN] =
- constantFold::componentFlag;
- d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_INF] =
- constantFold::componentFlag;
- d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_ZERO] =
- constantFold::componentFlag;
- d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_SIGN] =
- constantFold::componentFlag;
- d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_EXPONENT] =
- constantFold::componentExponent;
- d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND] =
- constantFold::componentSignificand;
- d_constantFoldTable[kind::ROUNDINGMODE_BITBLAST] =
- constantFold::roundingModeBitBlast;
+ /******** Constants ********/
+ /* Already folded! */
+ d_constantFoldTable[kind::CONST_FLOATINGPOINT] = rewrite::identity;
+ d_constantFoldTable[kind::CONST_ROUNDINGMODE] = rewrite::identity;
+
+ /******** Sorts(?) ********/
+ /* These kinds should only appear in types */
+ d_constantFoldTable[kind::FLOATINGPOINT_TYPE] = rewrite::type;
+
+ /******** Operations ********/
+ d_constantFoldTable[kind::FLOATINGPOINT_FP] = constantFold::fpLiteral;
+ d_constantFoldTable[kind::FLOATINGPOINT_ABS] = constantFold::abs;
+ d_constantFoldTable[kind::FLOATINGPOINT_NEG] = constantFold::neg;
+ d_constantFoldTable[kind::FLOATINGPOINT_ADD] = constantFold::add;
+ d_constantFoldTable[kind::FLOATINGPOINT_MULT] = constantFold::mult;
+ d_constantFoldTable[kind::FLOATINGPOINT_DIV] = constantFold::div;
+ d_constantFoldTable[kind::FLOATINGPOINT_FMA] = constantFold::fma;
+ d_constantFoldTable[kind::FLOATINGPOINT_SQRT] = constantFold::sqrt;
+ d_constantFoldTable[kind::FLOATINGPOINT_REM] = constantFold::rem;
+ d_constantFoldTable[kind::FLOATINGPOINT_RTI] = constantFold::rti;
+ d_constantFoldTable[kind::FLOATINGPOINT_MIN] = constantFold::min;
+ d_constantFoldTable[kind::FLOATINGPOINT_MAX] = constantFold::max;
+ d_constantFoldTable[kind::FLOATINGPOINT_MIN_TOTAL] = constantFold::minTotal;
+ d_constantFoldTable[kind::FLOATINGPOINT_MAX_TOTAL] = constantFold::maxTotal;
+
+ /******** Comparisons ********/
+ d_constantFoldTable[kind::FLOATINGPOINT_LEQ] = constantFold::leq;
+ d_constantFoldTable[kind::FLOATINGPOINT_LT] = constantFold::lt;
+
+ /******** Classifications ********/
+ d_constantFoldTable[kind::FLOATINGPOINT_IS_NORMAL] = constantFold::isNormal;
+ d_constantFoldTable[kind::FLOATINGPOINT_IS_SUBNORMAL] =
+ constantFold::isSubnormal;
+ d_constantFoldTable[kind::FLOATINGPOINT_IS_ZERO] = constantFold::isZero;
+ d_constantFoldTable[kind::FLOATINGPOINT_IS_INF] = constantFold::isInfinite;
+ d_constantFoldTable[kind::FLOATINGPOINT_IS_NAN] = constantFold::isNaN;
+ d_constantFoldTable[kind::FLOATINGPOINT_IS_NEG] = constantFold::isNegative;
+ d_constantFoldTable[kind::FLOATINGPOINT_IS_POS] = constantFold::isPositive;
+
+ /******** Conversions ********/
+ d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV] =
+ constantFold::convertFromIEEEBitVectorLiteral;
+ d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_FP] =
+ constantFold::constantConvert;
+ d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_REAL] =
+ constantFold::convertFromRealLiteral;
+ d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_SBV] =
+ constantFold::convertFromSBV;
+ d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_UBV] =
+ constantFold::convertFromUBV;
+ d_constantFoldTable[kind::FLOATINGPOINT_TO_UBV] =
+ constantFold::convertToUBV;
+ d_constantFoldTable[kind::FLOATINGPOINT_TO_SBV] =
+ constantFold::convertToSBV;
+ d_constantFoldTable[kind::FLOATINGPOINT_TO_REAL] =
+ constantFold::convertToReal;
+ d_constantFoldTable[kind::FLOATINGPOINT_TO_UBV_TOTAL] =
+ constantFold::convertToUBVTotal;
+ d_constantFoldTable[kind::FLOATINGPOINT_TO_SBV_TOTAL] =
+ constantFold::convertToSBVTotal;
+ d_constantFoldTable[kind::FLOATINGPOINT_TO_REAL_TOTAL] =
+ constantFold::convertToRealTotal;
+
+ /******** Variables ********/
+ d_constantFoldTable[kind::VARIABLE] = rewrite::variable;
+ d_constantFoldTable[kind::BOUND_VARIABLE] = rewrite::variable;
+
+ d_constantFoldTable[kind::EQUAL] = constantFold::equal;
+
+ /******** Components for bit-blasting ********/
+ d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_NAN] =
+ constantFold::componentFlag;
+ d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_INF] =
+ constantFold::componentFlag;
+ d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_ZERO] =
+ constantFold::componentFlag;
+ d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_SIGN] =
+ constantFold::componentFlag;
+ d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_EXPONENT] =
+ constantFold::componentExponent;
+ d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND] =
+ constantFold::componentSignificand;
+ d_constantFoldTable[kind::ROUNDINGMODE_BITBLAST] =
+ constantFold::roundingModeBitBlast;
}
/**
using namespace std;
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
using namespace std;
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
using namespace std;
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
}
}
-
-ConjectureGenerator::EqcInfo::EqcInfo( context::Context* c ) : d_rep( c, Node::null() ){
-
+ConjectureGenerator::EqcInfo::EqcInfo(context::Context* c)
+ : d_rep(c, Node::null())
+{
}
ConjectureGenerator::EqcInfo* ConjectureGenerator::getOrMakeEqcInfo( TNode n, bool doMake ) {
NotifyClass d_notify;
class EqcInfo{
public:
- EqcInfo( context::Context* c );
- //representative
- context::CDO< Node > d_rep;
+ EqcInfo(context::Context* c);
+ // representative
+ context::CDO<Node> d_rep;
};
/** get or make eqc info */
EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false );
#include "theory/quantifiers/term_util.h"
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
using namespace cvc5::internal::theory::quantifiers::inst;
namespace cvc5::internal {
#include "theory/quantifiers/term_database.h"
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
using namespace std;
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
/** Pointer to the model */
FirstOrderModel* d_model;
/** quantifiers equality inference */
- context::CDO< unsigned > d_eqi_counter;
+ context::CDO<unsigned> d_eqi_counter;
/** internal representatives */
std::map< TypeNode, std::map< Node, Node > > d_int_rep;
/** rep score */
#include "theory/quantifiers/term_util.h"
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
typedef context::CDHashMap<Node, int> NodeIntMap;
typedef context::CDHashMap<Node, Node> NodeNodeMap;
typedef context::CDHashMap<int, bool> IntBoolMap;
-private:
+
+ private:
//for determining bounds
bool hasNonBoundVar( Node f, Node b, std::map< Node, bool >& visited );
bool hasNonBoundVar( Node f, Node b );
#include "theory/rewriter.h"
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
using namespace std;
using namespace cvc5::internal;
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
using namespace cvc5::internal::theory;
using namespace cvc5::internal::theory::quantifiers;
#include "theory/quantifiers/term_database.h"
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
#include "theory/quantifiers/term_database.h"
#include "theory/uf/equality_engine_iterator.h"
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
#include "theory/quantifiers/term_util.h"
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
#include "theory/quantifiers/term_tuple_enumerator.h"
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
#include "theory/rewriter.h"
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
using namespace std;
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
using namespace std;
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
*/
class QuantifiersModules
{
- friend class ::cvc5::internal::theory::QuantifiersEngine;
+ friend class theory::QuantifiersEngine;
public:
QuantifiersModules();
using namespace std;
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
using namespace std;
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
using namespace std;
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
#include "theory/uf/equality_engine.h"
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
#include "theory/valuation.h"
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
*/
class QuantifiersEngine : protected EnvObj
{
- friend class ::cvc5::internal::TheoryEngine;
+ friend class internal::TheoryEngine;
typedef context::CDHashMap<Node, bool> BoolMap;
typedef context::CDHashSet<Node> NodeSet;
d_im.conflictEqConstantMerge(a, b);
}
-
-TheorySep::HeapAssertInfo::HeapAssertInfo( context::Context* c ) : d_pto(c), d_has_neg_pto(c,false) {
-
+TheorySep::HeapAssertInfo::HeapAssertInfo(context::Context* c)
+ : d_pto(c), d_has_neg_pto(c, false)
+{
}
TheorySep::HeapAssertInfo * TheorySep::getOrMakeEqcInfo( Node n, bool doMake ) {
class HeapAssertInfo {
public:
- HeapAssertInfo( context::Context* c );
- ~HeapAssertInfo(){}
- context::CDO< Node > d_pto;
- context::CDO< bool > d_has_neg_pto;
+ HeapAssertInfo(context::Context* c);
+ ~HeapAssertInfo() {}
+ context::CDO<Node> d_pto;
+ context::CDO<bool> d_has_neg_pto;
};
std::map< Node, HeapAssertInfo * > d_eqc_info;
HeapAssertInfo * getOrMakeEqcInfo( Node n, bool doMake = false );
class EqcInfo
{
public:
- EqcInfo( context::Context* c );
- ~EqcInfo(){}
- // singleton or emptyset equal to this eqc
- context::CDO< Node > d_singleton;
+ EqcInfo(context::Context* c);
+ ~EqcInfo() {}
+ // singleton or emptyset equal to this eqc
+ context::CDO<Node> d_singleton;
};
/** information necessary for equivalence classes */
std::map< Node, EqcInfo* > d_eqc_info;
class Env;
class TheoryEngine;
-class SharedTermsDatabase : public context::ContextNotifyObj {
+class SharedTermsDatabase : public context::ContextNotifyObj
+{
public:
/** A container for a list of shared terms */
typedef std::vector<TNode> shared_terms_list;
#include "theory/strings/word.h"
#include "util/rational.h"
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
using namespace cvc5::internal::kind;
namespace cvc5::internal {
#include "theory/strings/word.h"
#include "util/rational.h"
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
using namespace cvc5::internal::kind;
namespace cvc5::internal {
#include "util/rational.h"
using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
using namespace cvc5::internal::kind;
namespace cvc5::internal {
#include "util/string.h"
using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
using namespace cvc5::internal::kind;
namespace cvc5::internal {
{
eq::EqualityEngine* ee = d_state.getEqualityEngine();
std::map< Node, std::map< Node, bool > > processed;
-
+
const context::CDList<Node>& deqs = d_state.getDisequalityList();
NodeManager* nm = NodeManager::currentNM();
#include "theory/strings/word.h"
using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
using namespace cvc5::internal::kind;
namespace cvc5::internal {
#include "util/statistics_registry.h"
using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
using namespace cvc5::internal::kind;
namespace cvc5::internal {
#include "util/rational.h"
using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
using namespace cvc5::internal::kind;
namespace cvc5::internal {
#include "util/statistics_value.h"
using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
using namespace cvc5::internal::kind;
namespace cvc5::internal {
d_processed_memberships(context()),
d_regexp_opr(env, tr.getSkolemCache())
{
- d_emptyString = NodeManager::currentNM()->mkConst(::cvc5::internal::String(""));
+ d_emptyString = NodeManager::currentNM()->mkConst(cvc5::internal::String(""));
d_emptyRegexp = NodeManager::currentNM()->mkNode(REGEXP_NONE);
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
Node val;
if (isPrefix)
{
- val = NodeManager::currentNM()->mkConstInt(::cvc5::internal::Rational(0));
+ val = NodeManager::currentNM()->mkConstInt(cvc5::internal::Rational(0));
}
else
{
#include "util/rational.h"
using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
using namespace cvc5::internal::kind;
namespace cvc5::internal {
#include "util/rational.h"
using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
using namespace cvc5::internal::kind;
namespace cvc5::internal {
#include "util/string.h"
using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
using namespace cvc5::internal::kind;
namespace cvc5::internal {
#include "theory/valuation.h"
using namespace std;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
using namespace cvc5::internal::kind;
namespace cvc5::internal {
class Theory : protected EnvObj
{
friend class CarePairArgumentCallback;
- friend class ::cvc5::internal::TheoryEngine;
+ friend class internal::TheoryEngine;
protected:
/** Name of this theory instance. Along with the TheoryId this should
if (d_logicInfo.isSharingEnabled()) {
Trace(tag) << "Shared terms of " << theory->getId() << ": " << endl;
- context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
+ context::CDList<TNode>::const_iterator
+ it = theory->shared_terms_begin(),
+ it_end = theory->shared_terms_end();
for (unsigned i = 0; it != it_end; ++ it, ++i) {
Trace(tag) << "[" << i << "]: " << (*it) << endl;
}
for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
Theory* theory = d_theoryTable[theoryId];
if(theory && d_logicInfo.isTheoryEnabled(theoryId)) {
- for(context::CDList<Assertion>::const_iterator it = theory->facts_begin(),
- it_end = theory->facts_end();
- it != it_end;
- ++it) {
+ for (context::CDList<Assertion>::const_iterator
+ it = theory->facts_begin(),
+ it_end = theory->facts_end();
+ it != it_end;
+ ++it)
+ {
Node assertion = (*it).d_assertion;
if (hasRelevantAssertions
&& relevantAssertions.find(assertion) == relevantAssertions.end())
using namespace std;
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
using namespace std;
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
using namespace std;
using namespace cvc5::internal::kind;
-using namespace cvc5::internal::context;
+using namespace cvc5::context;
namespace cvc5::internal {
namespace theory {
typedef RegionNodeInfo::DiseqList DiseqList;
Region::Region(SortModel* cf, context::Context* c)
- : d_cf( cf )
- , d_testCliqueSize( c, 0 )
- , d_splitsSize( c, 0 )
- , d_testClique( c )
- , d_splits( c )
- , d_reps_size( c, 0 )
- , d_total_diseq_external( c, 0 )
- , d_total_diseq_internal( c, 0 )
- , d_valid( c, true ) {}
+ : d_cf(cf),
+ d_testCliqueSize(c, 0),
+ d_splitsSize(c, 0),
+ d_testClique(c),
+ d_splits(c),
+ d_reps_size(c, 0),
+ d_total_diseq_external(c, 0),
+ d_total_diseq_internal(c, 0),
+ d_valid(c, true)
+{
+}
Region::~Region() {
for(iterator i = begin(), iend = end(); i != iend; ++i) {
/** disequality list for node */
class DiseqList {
public:
- DiseqList( context::Context* c )
- : d_size( c, 0 ), d_disequalities( c ) {}
- ~DiseqList(){}
-
- void setDisequal( Node n, bool valid ){
- Assert((!isSet(n)) || getDisequalityValue(n) != valid);
- d_disequalities[ n ] = valid;
- d_size = d_size + ( valid ? 1 : -1 );
+ DiseqList(context::Context* c) : d_size(c, 0), d_disequalities(c) {}
+ ~DiseqList() {}
+
+ void setDisequal(Node n, bool valid)
+ {
+ Assert((!isSet(n)) || getDisequalityValue(n) != valid);
+ d_disequalities[n] = valid;
+ d_size = d_size + (valid ? 1 : -1);
}
bool isSet(Node n) const {
return d_disequalities.find(n) != d_disequalities.end();
iterator end() { return d_disequalities.end(); }
private:
- context::CDO< int > d_size;
- NodeBoolMap d_disequalities;
+ context::CDO<int> d_size;
+ NodeBoolMap d_disequalities;
}; /* class DiseqList */
public:
/** constructor */
- RegionNodeInfo( context::Context* c )
- : d_internal(c), d_external(c), d_valid(c, true) {
+ RegionNodeInfo(context::Context* c)
+ : d_internal(c), d_external(c), d_valid(c, true)
+ {
d_disequalities[0] = &d_internal;
d_disequalities[1] = &d_external;
}
private:
DiseqList d_internal;
DiseqList d_external;
- context::CDO< bool > d_valid;
+ context::CDO<bool> d_valid;
DiseqList* d_disequalities[2];
}; /* class RegionNodeInfo */
SortModel* d_cf;
context::CDO<size_t> d_testCliqueSize;
- context::CDO< unsigned > d_splitsSize;
+ context::CDO<unsigned> d_splitsSize;
//a postulated clique
NodeBoolMap d_testClique;
//disequalities needed for this clique to happen
//number of valid representatives in this region
context::CDO<size_t> d_reps_size;
//total disequality size (external)
- context::CDO< unsigned > d_total_diseq_external;
+ context::CDO<unsigned> d_total_diseq_external;
//total disequality size (internal)
- context::CDO< unsigned > d_total_diseq_internal;
+ context::CDO<unsigned> d_total_diseq_internal;
/** set rep */
void setRep( Node n, bool valid );
//region node infomation
std::map< Node, RegionNodeInfo* > d_nodes;
//whether region is valid
- context::CDO< bool > d_valid;
+ context::CDO<bool> d_valid;
public:
//constructor
- Region( SortModel* cf, context::Context* c );
+ Region(SortModel* cf, context::Context* c);
virtual ~Region();
typedef std::map< Node, RegionNodeInfo* >::iterator iterator;
/** the score for each node for splitting */
NodeIntMap d_split_score;
/** number of valid disequalities in d_disequalities */
- context::CDO< unsigned > d_disequalities_index;
+ context::CDO<unsigned> d_disequalities_index;
/** list of all disequalities */
std::vector< Node > d_disequalities;
/** number of representatives in all regions */
- context::CDO< unsigned > d_reps;
+ context::CDO<unsigned> d_reps;
/** get number of disequalities from node n to region ri */
int getNumDisequalitiesToRegion( Node n, int ri );
/** cardinality literals */
std::map<uint32_t, Node> d_cardinality_literal;
/** whether a positive cardinality constraint has been asserted */
- context::CDO< bool > d_hasCard;
+ context::CDO<bool> d_hasCard;
/** clique lemmas that have been asserted */
std::map< int, std::vector< std::vector< Node > > > d_cliques;
/** maximum negatively asserted cardinality */
/** list of fresh representatives allocated */
std::vector< Node > d_fresh_aloc_reps;
/** whether we are initialized */
- context::CDO< bool > d_initialized;
+ context::CDO<bool> d_initialized;
/** simple check cardinality */
void simpleCheckCardinality();
* Class for keeping an incremental congruence closure over a set of terms. It provides
* notifications via an EqualityEngineNotify object.
*/
-class EqualityEngine : public context::ContextNotifyObj, protected EnvObj {
-
+class EqualityEngine : public context::ContextNotifyObj, protected EnvObj
+{
friend class EqClassesIterator;
friend class EqClassIterator;
namespace theory {
namespace uf {
-using namespace ::cvc5::internal::context;
+using namespace cvc5::context;
SymmetryBreaker::Template::Template() :
d_template(),
std::ostream& operator<<(
std::ostream& out,
- const ::cvc5::internal::theory::uf::SymmetryBreaker::Permutation& p);
+ const cvc5::internal::theory::uf::SymmetryBreaker::Permutation& p);
} // namespace cvc5::internal
{
inline size_t operator()(const FloatingPointToBV& fptbv) const
{
- UnsignedHashFunction< ::cvc5::internal::BitVectorSize> f;
+ UnsignedHashFunction<cvc5::internal::BitVectorSize> f;
return (key ^ 0x46504256) ^ f(fptbv.d_bv_size);
}
}; /* struct FloatingPointToBVHashFunction */
namespace symfpu {
-#define CVC5_LIT_ITE_DFN(T) \
- template <> \
- struct ite<::cvc5::internal::symfpuLiteral::Cvc5Prop, T> \
- { \
- static const T& iteOp(const ::cvc5::internal::symfpuLiteral::Cvc5Prop& cond, \
- const T& l, \
- const T& r) \
- { \
- return cond ? l : r; \
- } \
+#define CVC5_LIT_ITE_DFN(T) \
+ template <> \
+ struct ite<cvc5::internal::symfpuLiteral::Cvc5Prop, T> \
+ { \
+ static const T& iteOp(const cvc5::internal::symfpuLiteral::Cvc5Prop& cond, \
+ const T& l, \
+ const T& r) \
+ { \
+ return cond ? l : r; \
+ } \
}
-CVC5_LIT_ITE_DFN(::cvc5::internal::symfpuLiteral::traits::rm);
-CVC5_LIT_ITE_DFN(::cvc5::internal::symfpuLiteral::traits::prop);
-CVC5_LIT_ITE_DFN(::cvc5::internal::symfpuLiteral::traits::sbv);
-CVC5_LIT_ITE_DFN(::cvc5::internal::symfpuLiteral::traits::ubv);
+CVC5_LIT_ITE_DFN(cvc5::internal::symfpuLiteral::traits::rm);
+CVC5_LIT_ITE_DFN(cvc5::internal::symfpuLiteral::traits::prop);
+CVC5_LIT_ITE_DFN(cvc5::internal::symfpuLiteral::traits::sbv);
+CVC5_LIT_ITE_DFN(cvc5::internal::symfpuLiteral::traits::ubv);
#undef CVC5_LIT_ITE_DFN
} // namespace symfpu
using Cvc5BitWidth = uint32_t;
using Cvc5Prop = bool;
-using Cvc5RM = ::cvc5::internal::RoundingMode;
-using Cvc5FPSize = ::cvc5::internal::FloatingPointSize;
+using Cvc5RM = cvc5::internal::RoundingMode;
+using Cvc5FPSize = cvc5::internal::FloatingPointSize;
using Cvc5UnsignedBitVector = wrappedBitVector<false>;
using Cvc5SignedBitVector = wrappedBitVector<true>;
namespace strings {
-size_t StringHashFunction::operator()(const ::cvc5::internal::String& s) const
+size_t StringHashFunction::operator()(const cvc5::internal::String& s) const
{
uint64_t ret = fnv1a::offsetBasis;
for (unsigned c : s.d_str)
struct StringHashFunction
{
- size_t operator()(const ::cvc5::internal::String& s) const;
+ size_t operator()(const cvc5::internal::String& s) const;
}; /* struct StringHashFunction */
} // namespace strings
namespace cvc5::internal {
-using context::CDHashMap;
-using context::CDInsertHashMap;
-using context::Context;
+using cvc5::context::CDHashMap;
+using cvc5::context::CDInsertHashMap;
+using cvc5::context::Context;
namespace test {
* directory for licensing information.
* ****************************************************************************
*
- * Black box testing of context::CDMap<>.
+ * Black box testing of cvc5::context::CDMap<>.
*/
#include <map>
namespace cvc5::internal {
namespace test {
-using context::CDHashMap;
-using context::Context;
+using cvc5::context::CDHashMap;
+using cvc5::context::Context;
class TestContextBlackCDHashMap : public TestContext
{
* directory for licensing information.
* ****************************************************************************
*
- * White box testing of context::CDMap<>.
+ * White box testing of cvc5::context::CDMap<>.
*/
#include "base/check.h"
* directory for licensing information.
* ****************************************************************************
*
- * Black box testing of context::CDList<>.
+ * Black box testing of cvc5::context::CDList<>.
*/
#include <limits.h>
* directory for licensing information.
* ****************************************************************************
*
- * Black box testing of context::CDO<>.
+ * Black box testing of cvc5::context::CDO<>.
*/
#include <iostream>
* directory for licensing information.
* ****************************************************************************
*
- * Black box testing of context::Context.
+ * Black box testing of cvc5::context::Context.
*/
#include <iostream>
* directory for licensing information.
* ****************************************************************************
*
- * Black box testing of context::ContextMemoryManager.
+ * Black box testing of cvc5::context::ContextMemoryManager.
*/
#include <cstring>
* directory for licensing information.
* ****************************************************************************
*
- * White box testing of context::Context.
+ * White box testing of cvc5::context::Context.
*/
#include "base/check.h"
namespace cvc5::internal {
-using namespace context;
+using namespace cvc5::context;
using namespace prop;
using namespace smt;
using namespace theory;
TestSmt::SetUp();
d_theoryEngine = d_slvEngine->getTheoryEngine();
d_satSolver.reset(new FakeSatSolver());
- d_cnfContext.reset(new context::Context());
+ d_cnfContext.reset(new Context());
d_cnfRegistrar.reset(new prop::NullRegistrar);
d_cnfStream.reset(new prop::CnfStream(d_slvEngine->getEnv(),
d_satSolver.get(),
class TestContext : public TestInternal
{
protected:
- void SetUp() override { d_context.reset(new context::Context()); }
- std::unique_ptr<context::Context> d_context;
+ void SetUp() override { d_context.reset(new cvc5::context::Context()); }
+ std::unique_ptr<cvc5::context::Context> d_context;
};
} // namespace test
using namespace theory;
using namespace expr;
-using namespace context;
+using namespace cvc5::context;
using namespace kind;
using namespace theory::bv;
projects / cvc5.git / commitdiff