*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
SEXPR,
/**
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
*
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
EQ_RANGE,
*
* - Create Term of this Kind with:
* - Solver::mkSepNil(const Sort&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
SEP_NIL,
/**
*
* - Create Term of this Kind with:
* - Solver::mkSepEmp() const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
SEP_EMP,
/**
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
SEP_PTO,
/**
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
SEP_STAR,
/**
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
SEP_WAND,
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
SET_COMPREHENSION,
/**
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
SET_CHOOSE,
/**
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
SET_IS_SINGLETON,
/**
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
SET_MAP,
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
RELATION_JOIN_IMAGE,
/**
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
RELATION_IDEN,
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
BAG_DUPLICATE_REMOVAL,
/**
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
BAG_CARD,
/**
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
BAG_CHOOSE,
/**
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
BAG_IS_SINGLETON,
/**
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
BAG_FROM_SET,
/**
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
BAG_TO_SET,
/**
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
BAG_MAP,
/**
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
BAG_FILTER,
/**
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
BAG_FOLD,
/**
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
TABLE_PRODUCT,
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
INST_POOL,
/**
* A instantantiation-add-to-pool annotation.
*
* @note Should only be used as a child of #INST_PATTERN_LIST.
- *
+ *
* An instantantiation-add-to-pool annotation indicates that when a quantified
* formula is instantiated, the instantiated version of a term should be
* added to the given pool.
- *
+ *
* For example, consider a quantified formula:
- *
+ *
* \rst
* .. code:: lisp
*
* (FORALL (VARIABLE_LIST x) F
* (INST_PATTERN_LIST (INST_ADD_TO_POOL (ADD x 1) p)))
* \endrst
- *
+ *
* where assume that @f$x@f$ has type Int. When this quantified formula is
* instantiated with, e.g., the term @f$t@f$, the term `(ADD t 1)` is added to pool @f$p@f$.
*
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
INST_ADD_TO_POOL,
/**
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ *
+ * \rst
+ * .. warning:: This kind is experimental and may be changed or removed in
+ * future versions.
+ * \endrst
*/
SKOLEM_ADD_TO_POOL,
/**