#include <map>
#include <memory>
+#include <optional>
#include <set>
#include <sstream>
#include <string>
#include <unordered_map>
#include <unordered_set>
+#include <variant>
#include <vector>
#include "api/cpp/cvc5_kind.h"
class DTypeConstructor;
class DTypeSelector;
class NodeManager;
-class SmtEngine;
+class SolverEngine;
class TypeNode;
class Options;
class Random;
+class Rational;
class Result;
class StatisticsRegistry;
+namespace main {
+class CommandExecutor;
+}
+
namespace api {
class Solver;
}
};
+/**
+ * Exception for unsupported command arguments.
+ * If thrown, API objects can still be used.
+ */
+class CVC5_EXPORT CVC5ApiUnsupportedException : public CVC5ApiRecoverableException
+{
+ public:
+ /**
+ * Construct with message from a string.
+ * @param str The error message.
+ */
+ CVC5ApiUnsupportedException(const std::string& str)
+ : CVC5ApiRecoverableException(str)
+ {
+ }
+ /**
+ * Construct with message from a string stream.
+ * @param stream The error message.
+ */
+ CVC5ApiUnsupportedException(const std::stringstream& stream)
+ : CVC5ApiRecoverableException(stream.str())
+ {
+ }
+};
+
+/**
+ * An option-related API exception.
+ * If thrown, API objects can still be used.
+ */
+class CVC5_EXPORT CVC5ApiOptionException : public CVC5ApiRecoverableException
+{
+ public:
+ /**
+ * Construct with message from a string.
+ * @param str The error message.
+ */
+ CVC5ApiOptionException(const std::string& str)
+ : CVC5ApiRecoverableException(str)
+ {
+ }
+ /**
+ * Construct with message from a string stream.
+ * @param stream The error message.
+ */
+ CVC5ApiOptionException(const std::stringstream& stream)
+ : CVC5ApiRecoverableException(stream.str())
+ {
+ }
+};
+
/* -------------------------------------------------------------------------- */
/* Result */
/* -------------------------------------------------------------------------- */
bool isNotEntailed() const;
/**
- * Return true if query was a checkEntailed() () query and cvc5 was not able
- * to determine if it is entailed.
+ * Return true if query was a checkEntailed() query and cvc5 was not able to
+ * determine if it is entailed.
*/
bool isEntailmentUnknown() const;
/**
* The interal result wrapped by this result.
- * Note: This is a shared_ptr rather than a unique_ptr since cvc5::Result is
- * not ref counted.
+ *
+ * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr``
+ * since ``cvc5::Result`` is not ref counted.
*/
std::shared_ptr<cvc5::Result> d_result;
};
friend class DatatypeConstructorDecl;
friend class DatatypeSelector;
friend class DatatypeDecl;
+ friend class Datatype;
friend class Op;
friend class Solver;
friend class Grammar;
*/
bool operator>=(const Sort& s) const;
+ /**
+ * @return true if the sort has a symbol.
+ */
+ bool hasSymbol() const;
+
+ /**
+ * Asserts hasSymbol().
+ * @return the raw symbol of the sort.
+ */
+ std::string getSymbol() const;
+
/**
* @return true if this Sort is a null sort.
*/
/**
* Is this a Boolean sort?
- * @return true if the sort is a Boolean sort
+ * @return true if the sort is the Boolean sort
*/
bool isBoolean() const;
/**
* Is this a integer sort?
- * @return true if the sort is a integer sort
+ * @return true if the sort is the integer sort
*/
bool isInteger() const;
/**
* Is this a real sort?
- * @return true if the sort is a real sort
+ * @return true if the sort is the real sort
*/
bool isReal() const;
bool isDatatype() const;
/**
- * Is this a parametric datatype sort?
+ * Is this a parametric datatype sort? A parametric datatype sort is either
+ * one that is returned by a call to Solver::mkDatatypeSort() or
+ * Solver::mkDatatypeSorts() for a parametric datatype, or an instantiated
+ * datatype sort returned by Sort::instantiate() for parametric datatype
+ * sort `s`.
* @return true if the sort is a parametric datatype sort
*/
bool isParametricDatatype() const;
* @return true if the sort is a tester sort
*/
bool isTester() const;
+ /**
+ * Is this a datatype updater sort?
+ * @return true if the sort is a datatype updater sort
+ */
+ bool isUpdater() const;
/**
* Is this a function sort?
* @return true if the sort is a function sort
/**
* Is this an array sort?
- * @return true if the sort is a array sort
+ * @return true if the sort is an array sort
*/
bool isArray() const;
bool isSequence() const;
/**
- * Is this a sort kind?
- * @return true if this is a sort kind
+ * Is this an uninterpreted sort?
+ * @return true if this is an uninterpreted sort
*/
bool isUninterpretedSort() const;
/**
* Is this a first-class sort?
* First-class sorts are sorts for which:
- * (1) we handle equalities between terms of that type, and
- * (2) they are allowed to be parameters of parametric sorts (e.g. index or
- * element sorts of arrays).
+ * 1. we handle equalities between terms of that type, and
+ * 2. they are allowed to be parameters of parametric sorts (e.g. index or
+ * element sorts of arrays).
*
* Examples of sorts that are not first-class include sort constructor sorts
* and regular expression sorts.
* or return value for any term that is function-like.
* This is mainly to avoid higher order.
*
- * Note that arrays are explicitly not considered function-like here.
+ * @note Arrays are explicitly not considered function-like here.
*
* @return true if this is a function-like sort
*/
/**
* @return the codomain sort of a tester sort, which is the Boolean sort
+ *
+ * @note We mainly need this for the symbol table, which doesn't have
+ * access to the solver object.
*/
Sort getTesterCodomainSort() const;
Sort getArrayIndexSort() const;
/**
- * @return the array element sort of an array element sort
+ * @return the array element sort of an array sort
*/
Sort getArrayElementSort() const;
std::string getUninterpretedSortName() const;
/**
- * @return true if an uninterpreted sort is parameterezied
+ * @return true if an uninterpreted sort is parameterized
*/
bool isUninterpretedSortParameterized() const;
/**
* @return the bit-width of the bit-vector sort
*/
- uint32_t getBVSize() const;
+ uint32_t getBitVectorSize() const;
/* Floating-point sort ------------------------------------------------- */
/**
* @return the bit-width of the exponent of the floating-point sort
*/
- uint32_t getFPExponentSize() const;
+ uint32_t getFloatingPointExponentSize() const;
/**
* @return the width of the significand of the floating-point sort
*/
- uint32_t getFPSignificandSize() const;
+ uint32_t getFloatingPointSignificandSize() const;
/* Datatype sort ------------------------------------------------------- */
/**
- * @return the parameter sorts of a datatype sort
+ *
+ * Return the parameters of a parametric datatype sort. If this sort is a
+ * non-instantiated parametric datatype, this returns the parameter sorts of
+ * the underlying datatype. If this sort is an instantiated parametric
+ * datatype, then this returns the sort parameters that were used to
+ * construct the sort via Sort::instantiate().
+ *
+ * @return the parameter sorts of a parametric datatype sort.
*/
std::vector<Sort> getDatatypeParamSorts() const;
const Solver* d_solver;
/**
- * The interal type wrapped by this sort.
- * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
- * to memory allocation (cvc5::Type is already ref counted, so this
- * could be a unique_ptr instead).
+ * The internal type wrapped by this sort.
+ *
+ * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr`` to
+ * avoid overhead due to memory allocation (``cvc5::Type`` is already
+ * ref counted, so this could be a ``std::unique_ptr`` instead).
*/
std::shared_ptr<cvc5::TypeNode> d_type;
};
/* Op */
/* -------------------------------------------------------------------------- */
+class Term;
+
/**
* A cvc5 operator.
* An operator is a term that represents certain operators, instantiated
*/
size_t getNumIndices() const;
+ /**
+ * Get the index at position i.
+ * @param i the position of the index to return
+ * @return the index at position i
+ */
+
+ Term operator[](size_t i) const;
+
/**
* Get the indices used to create this Op.
* Supports the following template arguments:
bool isNullHelper() const;
/**
- * Note: An indexed operator has a non-null internal node, d_node
- * Note 2: We use a helper method to avoid having API functions call
- * other API functions (we need to call this internally)
+ * @note An indexed operator has a non-null internal node (``d_node``).
+ *
+ * @note We use a helper method to avoid having API functions call other API
+ * functions (we need to call this internally).
+ *
* @return true iff this Op is indexed
*/
bool isIndexedHelper() const;
+ /**
+ * Helper for getNumIndices
+ * @return the number of indices of this op
+ */
+ size_t getNumIndicesHelper() const;
+
+ /**
+ * Helper for operator[](size_t index).
+ * @param index position of the index. Should be less than getNumIndicesHelper().
+ * @return the index at position index
+ */
+ Term getIndexHelper(size_t index) const;
+
/**
* The associated solver object.
*/
/**
* The internal node wrapped by this operator.
- * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
- * to memory allocation (cvc5::Node is already ref counted, so this
- * could be a unique_ptr instead).
+ *
+ * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr`` to
+ * avoid overhead due to memory allocation (``cvc5::Node`` is already
+ * ref counted, so this could be a ``std::unique_ptr`` instead).
*/
std::shared_ptr<cvc5::Node> d_node;
};
public:
/**
- * Constructor.
+ * Constructor for a null term.
*/
Term();
bool operator!=(const Term& t) const;
/**
- * Comparison for ordering on terms.
+ * Comparison for ordering on terms by their id.
* @param t the term to compare to
* @return true if this term is less than t
*/
bool operator<(const Term& t) const;
/**
- * Comparison for ordering on terms.
+ * Comparison for ordering on terms by their id.
* @param t the term to compare to
* @return true if this term is greater than t
*/
bool operator>(const Term& t) const;
/**
- * Comparison for ordering on terms.
+ * Comparison for ordering on terms by their id.
* @param t the term to compare to
* @return true if this term is less than or equal to t
*/
bool operator<=(const Term& t) const;
/**
- * Comparison for ordering on terms.
+ * Comparison for ordering on terms by their id.
* @param t the term to compare to
* @return true if this term is greater than or equal to t
*/
Term substitute(const Term& term, const Term& replacement) const;
/**
- * @return the result of simulatenously replacing 'terms' by 'replacements'
+ * @return the result of simultaneously replacing 'terms' by 'replacements'
* in this term
*/
Term substitute(const std::vector<Term>& terms,
bool hasOp() const;
/**
+ * @note This is safe to call when hasOp() returns true.
+ *
* @return the Op used to create this term
- * Note: This is safe to call when hasOp() returns true.
*/
Op getOp() const;
/**
- * @return true if this Term is a null term
+ * @return true if the term has a symbol.
*/
- bool isNull() const;
+ bool hasSymbol() const;
/**
- * Return the base (element stored at all indices) of a constant array
- * throws an exception if the kind is not CONST_ARRAY
- * @return the base value
+ * Asserts hasSymbol().
+ * @return the raw symbol of the term.
*/
- Term getConstArrayBase() const;
+ std::string getSymbol() const;
/**
- * Return the elements of a constant sequence
- * throws an exception if the kind is not CONST_SEQUENCE
- * @return the elements of the constant sequence.
+ * @return true if this Term is a null term
*/
- std::vector<Term> getConstSequenceElements() const;
+ bool isNull() const;
/**
* Boolean negation.
/**
* Iterator for the children of a Term.
- * Note: This treats uninterpreted functions as Term just like any other term
- * for example, the term f(x, y) will have Kind APPLY_UF and three
- * children: f, x, and y
+ * @note This treats uninterpreted functions as Term just like any other term
+ * for example, the term ``f(x, y)`` will have Kind ``APPLY_UF`` and
+ * three children: ``f``, ``x``, and ``y``
*/
- class const_iterator : public std::iterator<std::input_iterator_tag, Term>
+ class CVC5_EXPORT const_iterator
{
friend class Term;
public:
+ /* The following types are required by trait std::iterator_traits */
+
+ /** Iterator tag */
+ using iterator_category = std::forward_iterator_tag;
+
+ /** The type of the item */
+ using value_type = Term;
+
+ /** The pointer type of the item */
+ using pointer = const Term*;
+
+ /** The reference type of the item */
+ using reference = const Term&;
+
+ /** The type returned when two iterators are subtracted */
+ using difference_type = std::ptrdiff_t;
+
+ /* End of std::iterator_traits required types */
+
/**
* Null Constructor.
*/
/**
* Constructor
* @param slv the associated solver object
- * @param e a shared pointer to the node that we're iterating over
+ * @param e a ``std::shared pointer`` to the node that we're iterating over
* @param p the position of the iterator (e.g. which child it's on)
*/
const_iterator(const Solver* slv,
const_iterator end() const;
/**
- * @return true if the term is an integer that fits within std::int32_t.
+ * Get integer or real value sign. Must be called on integer or real values,
+ * or otherwise an exception is thrown.
+ * @return 0 if this term is zero, -1 if this term is a negative real or
+ * integer value, 1 if this term is a positive real or integer value.
*/
- bool isInt32() const;
+ int32_t getRealOrIntegerValueSign() const;
/**
- * @return the stored integer as a std::int32_t.
- * Note: Asserts isInt32().
+ * @return true if the term is an integer value that fits within int32_t.
*/
- std::int32_t getInt32() const;
+ bool isInt32Value() const;
/**
- * @return true if the term is an integer that fits within std::uint32_t.
+ * Asserts isInt32Value().
+ * @return the integer term as a int32_t.
*/
- bool isUInt32() const;
+ int32_t getInt32Value() const;
/**
- * @return the stored integer as a std::uint32_t.
- * Note: Asserts isUInt32().
+ * @return true if the term is an integer value that fits within uint32_t.
*/
- std::uint32_t getUInt32() const;
+ bool isUInt32Value() const;
/**
- * @return true if the term is an integer that fits within std::int64_t.
+ * Asserts isUInt32Value().
+ * @return the integer term as a uint32_t.
*/
- bool isInt64() const;
+ uint32_t getUInt32Value() const;
/**
- * @return the stored integer as a std::int64_t.
- * Note: Asserts isInt64().
+ * @return true if the term is an integer value that fits within int64_t.
*/
- std::int64_t getInt64() const;
+ bool isInt64Value() const;
/**
- * @return true if the term is an integer that fits within std::uint64_t.
+ * Asserts isInt64Value().
+ * @return the integer term as a int64_t.
*/
- bool isUInt64() const;
+ int64_t getInt64Value() const;
/**
- * @return the stored integer as a std::uint64_t.
- * Note: Asserts isUInt64().
+ * @return true if the term is an integer value that fits within uint64_t.
*/
- std::uint64_t getUInt64() const;
+ bool isUInt64Value() const;
/**
- * @return true if the term is an integer.
+ * Asserts isUInt64Value().
+ * @return the integer term as a uint64_t.
*/
- bool isInteger() const;
+ uint64_t getUInt64Value() const;
+ /**
+ * @return true if the term is an integer value.
+ */
+ bool isIntegerValue() const;
/**
- * @return the stored integer in (decimal) string representation.
- * Note: Asserts isInteger().
+ * Asserts isIntegerValue().
+ * @return the integer term in (decimal) string representation.
*/
- std::string getInteger() const;
+ std::string getIntegerValue() const;
/**
- * @return true if the term is a string constant.
+ * @return true if the term is a string value.
*/
- bool isString() const;
+ bool isStringValue() const;
+ /**
+ * Asserts isStringValue().
+ * @note This method is not to be confused with toString(), which returns
+ * some string representation of the term, whatever data it may hold.
+ * @return the string term as a native string value.
+ */
+ std::wstring getStringValue() const;
+
+ /**
+ * @return true if the term is a rational value whose numerator and
+ * denominator fit within int32_t and uint32_t, respectively.
+ */
+ bool isReal32Value() const;
+ /**
+ * Asserts isReal32Value().
+ * @return the representation of a rational value as a pair of its numerator
+ * and denominator.
+ */
+ std::pair<int32_t, uint32_t> getReal32Value() const;
+ /**
+ * @return true if the term is a rational value whose numerator and
+ * denominator fit within int64_t and uint64_t, respectively.
+ */
+ bool isReal64Value() const;
+ /**
+ * Asserts isReal64Value().
+ * @return the representation of a rational value as a pair of its numerator
+ * and denominator.
+ */
+ std::pair<int64_t, uint64_t> getReal64Value() const;
+ /**
+ * @note A term of kind PI is not considered to be a real value.
+ * @return true if the term is a rational value.
+ */
+ bool isRealValue() const;
+ /**
+ * Asserts isRealValue().
+ * @return the representation of a rational value as a (rational) string.
+ */
+ std::string getRealValue() const;
+
+ /**
+ * @return true if the term is a constant array.
+ */
+ bool isConstArray() const;
+ /**
+ * Asserts isConstArray().
+ * @return the base (element stored at all indices) of a constant array
+ */
+ Term getConstArrayBase() const;
+
+ /**
+ * @return true if the term is a Boolean value.
+ */
+ bool isBooleanValue() const;
+ /**
+ * Asserts isBooleanValue().
+ * @return the representation of a Boolean value as a native Boolean value.
+ */
+ bool getBooleanValue() const;
+
+ /**
+ * @return true if the term is a bit-vector value.
+ */
+ bool isBitVectorValue() const;
+ /**
+ * Asserts isBitVectorValue().
+ * @return the representation of a bit-vector value in string representation.
+ * Supported bases are 2 (bit string), 10 (decimal string) or 16 (hexadecimal
+ * string).
+ */
+ std::string getBitVectorValue(uint32_t base = 2) const;
+
+ /**
+ * @return true if the term is an abstract value.
+ */
+ bool isAbstractValue() const;
+ /**
+ * Asserts isAbstractValue().
+ * @return the representation of an abstract value as a string.
+ */
+ std::string getAbstractValue() const;
+
+ /**
+ * @return true if the term is a tuple value.
+ */
+ bool isTupleValue() const;
+ /**
+ * Asserts isTupleValue().
+ * @return the representation of a tuple value as a vector of terms.
+ */
+ std::vector<Term> getTupleValue() const;
+
/**
- * @return the stored string constant.
+ * @return true if the term is the floating-point value for positive zero.
+ */
+ bool isFloatingPointPosZero() const;
+ /**
+ * @return true if the term is the floating-point value for negative zero.
+ */
+ bool isFloatingPointNegZero() const;
+ /**
+ * @return true if the term is the floating-point value for positive
+ * infinity.
+ */
+ bool isFloatingPointPosInf() const;
+ /**
+ * @return true if the term is the floating-point value for negative
+ * infinity.
+ */
+ bool isFloatingPointNegInf() const;
+ /**
+ * @return true if the term is the floating-point value for not a number.
+ */
+ bool isFloatingPointNaN() const;
+ /**
+ * @return true if the term is a floating-point value.
+ */
+ bool isFloatingPointValue() const;
+ /**
+ * Asserts isFloatingPointValue().
+ * @return the representation of a floating-point value as a tuple of the
+ * exponent width, the significand width and a bit-vector value.
+ */
+ std::tuple<uint32_t, uint32_t, Term> getFloatingPointValue() const;
+
+ /**
+ * @return true if the term is a set value.
+ *
+ * A term is a set value if it is considered to be a (canonical) constant set
+ * value. A canonical set value is one whose AST is:
*
- * Note: This method is not to be confused with toString() which returns the
- * term in some string representation, whatever data it may hold.
- * Asserts isString().
+ * (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
+ *
+ * where `c1 ... cn` are values ordered by id such that `c1 > ... > cn` (see
+ * also @ref Term::operator>(const Term&) const).
+ *
+ * @note A universe set term `(kind SET_UNIVERSE)` is not considered to be
+ * a set value.
+ */
+ bool isSetValue() const;
+ /**
+ * Asserts isSetValue().
+ * @return the representation of a set value as a set of terms.
+ */
+ std::set<Term> getSetValue() const;
+
+ /**
+ * @return true if the term is a sequence value.
+ */
+ bool isSequenceValue() const;
+ /**
+ * Asserts isSequenceValue().
+ * @note It is usually necessary for sequences to call Solver::simplify()
+ * to turn a sequence that is constructed by, e.g., concatenation of
+ * unit sequences, into a sequence value.
+ * @return the representation of a sequence value as a vector of terms.
+ */
+ std::vector<Term> getSequenceValue() const;
+
+ /**
+ * @return true if the term is a value from an uninterpreted sort.
*/
- std::wstring getString() const;
+ bool isUninterpretedValue() const;
+ /**
+ bool @return() const;
+ * Asserts isUninterpretedValue().
+ * @return the representation of an uninterpreted value as a pair of its
+ sort and its
+ * index.
+ */
+ std::pair<Sort, int32_t> getUninterpretedValue() const;
protected:
/**
/** Helper to convert a vector of Terms to internal Nodes. */
std::vector<Node> static termVectorToNodes(const std::vector<Term>& terms);
+ /** Helper method to collect all elements of a set. */
+ static void collectSet(std::set<Term>& set,
+ const cvc5::Node& node,
+ const Solver* slv);
+ /** Helper method to collect all elements of a sequence. */
+ static void collectSequence(std::vector<Term>& seq,
+ const cvc5::Node& node,
+ const Solver* slv);
+
/**
* Constructor.
* @param slv the associated solver object
bool isCastedReal() const;
/**
* The internal node wrapped by this term.
- * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
- * to memory allocation (cvc5::Node is already ref counted, so this
- * could be a unique_ptr instead).
+ * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr`` to
+ * avoid overhead due to memory allocation (``cvc5::Node`` is already
+ * ref counted, so this could be a ``std::unique_ptr`` instead).
*/
std::shared_ptr<cvc5::Node> d_node;
};
/**
* Add datatype selector declaration.
* @param name the name of the datatype selector declaration to add
- * @param sort the range sort of the datatype selector declaration to add
+ * @param sort the codomain sort of the datatype selector declaration to add
*/
void addSelector(const std::string& name, const Sort& sort);
/**
- * Add datatype selector declaration whose range type is the datatype itself.
+ * Add datatype selector declaration whose codomain type is the datatype
+ * itself.
* @param name the name of the datatype selector declaration to add
*/
void addSelectorSelf(const std::string& name);
*/
bool isNullHelper() const;
+ /**
+ * Is the underlying constructor resolved (i.e. has it been used to declare
+ * a datatype already)?
+ */
+ bool isResolved() const;
+
/**
* The associated solver object.
*/
/**
* The internal (intermediate) datatype constructor wrapped by this
* datatype constructor declaration.
- * Note: This is a shared_ptr rather than a unique_ptr since
- * cvc5::DTypeConstructor is not ref counted.
+ * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr``
+ * since ``cvc5::DTypeConstructor`` is not ref counted.
*/
std::shared_ptr<cvc5::DTypeConstructor> d_ctor;
};
/**
* The internal (intermediate) datatype wrapped by this datatype
* declaration.
- * Note: This is a shared_ptr rather than a unique_ptr since cvc5::DType is
- * not ref counted.
+ * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr``
+ * since ``cvc5::DType`` is not ref counted.
*/
std::shared_ptr<cvc5::DType> d_dtype;
};
*/
class CVC5_EXPORT DatatypeSelector
{
+ friend class Datatype;
friend class DatatypeConstructor;
friend class Solver;
*/
Term getSelectorTerm() const;
- /** @return the range sort of this argument. */
- Sort getRangeSort() const;
+ /**
+ * Get the updater operator of this datatype selector.
+ * @return the updater term
+ */
+ Term getUpdaterTerm() const;
+
+ /** @return the codomain sort of this selector. */
+ Sort getCodomainSort() const;
/**
* @return true if this DatatypeSelector is a null object
/**
* The internal datatype selector wrapped by this datatype selector.
- * Note: This is a shared_ptr rather than a unique_ptr since cvc5::DType is
- * not ref counted.
+ * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr``
+ * since ``cvc5::DType`` is not ref counted.
*/
std::shared_ptr<cvc5::DTypeSelector> d_stor;
};
*
* This method is required for constructors of parametric datatypes whose
* return type cannot be determined by type inference. For example, given:
- * (declare-datatype List (par (T) ((nil) (cons (head T) (tail (List T))))))
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (declare-datatype List
+ * (par (T) ((nil) (cons (head T) (tail (List T))))))
+ * \endverbatim
+ *
* The type of nil terms need to be provided by the user. In SMT version 2.6,
* this is done via the syntax for qualified identifiers:
- * (as nil (List Int))
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (as nil (List Int))
+ * \endverbatim
+ *
* This method is equivalent of applying the above, where this
* DatatypeConstructor is the one corresponding to nil, and retSort is
- * (List Int).
+ * ``(List Int)``.
*
- * Furthermore note that the returned constructor term t is an operator,
- * while Solver::mkTerm(APPLY_CONSTRUCTOR, t) is used to construct the above
- * (nullary) application of nil.
+ * @note the returned constructor term ``t`` is an operator, while
+ * ``Solver::mkTerm(APPLY_CONSTRUCTOR, t)`` is used to construct the
+ * above (nullary) application of nil.
*
* @param retSort the desired return sort of the constructor
* @return the constructor term
*/
- Term getSpecializedConstructorTerm(const Sort& retSort) const;
+ Term getInstantiatedConstructorTerm(const Sort& retSort) const;
/**
* Get the tester operator of this datatype constructor.
* Iterator for the selectors of a datatype constructor.
*/
class const_iterator
- : public std::iterator<std::input_iterator_tag, DatatypeConstructor>
{
friend class DatatypeConstructor; // to access constructor
public:
+ /* The following types are required by trait std::iterator_traits */
+
+ /** Iterator tag */
+ using iterator_category = std::forward_iterator_tag;
+
+ /** The type of the item */
+ using value_type = DatatypeConstructor;
+
+ /** The pointer type of the item */
+ using pointer = const DatatypeConstructor*;
+
+ /** The reference type of the item */
+ using reference = const DatatypeConstructor&;
+
+ /** The type returned when two iterators are subtracted */
+ using difference_type = std::ptrdiff_t;
+
+ /* End of std::iterator_traits required types */
+
/** Nullary constructor (required for Cython). */
const_iterator();
/**
* The internal datatype constructor wrapped by this datatype constructor.
- * Note: This is a shared_ptr rather than a unique_ptr since cvc5::DType is
- * not ref counted.
+ * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr``
+ * since ``cvc5::DType`` is not ref counted.
*/
std::shared_ptr<cvc5::DTypeConstructor> d_ctor;
};
*/
Term getConstructorTerm(const std::string& name) const;
+ /**
+ * Get the datatype constructor with the given name.
+ * This is a linear search through the constructors and their selectors, so
+ * in case of multiple, similarly-named selectors, the first is returned.
+ * @param name the name of the datatype selector
+ * @return the datatype selector with the given name
+ */
+ DatatypeSelector getSelector(const std::string& name) const;
+
/** @return the name of this Datatype. */
std::string getName() const;
/** @return the number of constructors for this Datatype. */
size_t getNumConstructors() const;
+ /**
+ * @return the parameters of this datatype, if it is parametric. An exception
+ * is thrown if this datatype is not parametric.
+ */
+ std::vector<Sort> getParameters() const;
+
/** @return true if this datatype is parametric */
bool isParametric() const;
* Does this datatype have nested recursion? This method returns false if a
* value of this datatype includes a subterm of its type that is nested
* beneath a non-datatype type constructor. For example, a datatype
- * T containing a constructor having a selector with range type (Set T) has
- * nested recursion.
+ * T containing a constructor having a selector with codomain type (Set T)
+ * has nested recursion.
*
* @return true if this datatype has nested recursion
*/
/**
* Iterator for the constructors of a datatype.
*/
- class const_iterator : public std::iterator<std::input_iterator_tag, Datatype>
+ class const_iterator
{
friend class Datatype; // to access constructor
public:
+ /* The following types are required by trait std::iterator_traits */
+
+ /** Iterator tag */
+ using iterator_category = std::forward_iterator_tag;
+
+ /** The type of the item */
+ using value_type = Datatype;
+
+ /** The pointer type of the item */
+ using pointer = const Datatype*;
+
+ /** The reference type of the item */
+ using reference = const Datatype&;
+
+ /** The type returned when two iterators are subtracted */
+ using difference_type = std::ptrdiff_t;
+
+ /* End of std::iterator_traits required types */
+
/** Nullary constructor (required for Cython). */
const_iterator();
*/
DatatypeConstructor getConstructorForName(const std::string& name) const;
+ /**
+ * Return selector for name.
+ * @param name The name of selector to find
+ * @return the selector object for the name
+ */
+ DatatypeSelector getSelectorForName(const std::string& name) const;
+
/**
* Helper for isNull checks. This prevents calling an API function with
* CVC5_API_CHECK_NOT_NULL
/**
* The internal datatype wrapped by this datatype.
- * Note: This is a shared_ptr rather than a unique_ptr since cvc5::DType is
- * not ref counted.
+ * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr``
+ * since ``cvc5::DType`` is not ref counted.
*/
std::shared_ptr<cvc5::DType> d_dtype;
};
/**
* Allow \p ntSymbol to be any input variable to corresponding
* synth-fun/synth-inv with the same sort as \p ntSymbol.
- * @param ntSymbol the non-terminal allowed to be any input constant
+ * @param ntSymbol the non-terminal allowed to be any input variable
*/
void addAnyVariable(const Term& ntSymbol);
* with bound variables via purifySygusGTerm, and binding these variables
* via a lambda.
*
+ * @note Create unresolved sorts with Solver::mkUnresolvedSort().
+ *
* @param dt the non-terminal's datatype to which a constructor is added
* @param term the sygus operator of the constructor
* @param ntsToUnres mapping from non-terminals to their unresolved sorts
* Standard 754.
* \endverbatim
*/
-enum CVC5_EXPORT RoundingMode
+enum RoundingMode
{
/**
* Round to the nearest even number.
ROUND_NEAREST_TIES_TO_EVEN,
/**
* Round towards positive infinity (+oo).
- * The result shall be the format’s floating-point number (possibly +oo)
+ * The result shall be the format's floating-point number (possibly +oo)
* closest to and no less than the infinitely precise result.
*/
ROUND_TOWARD_POSITIVE,
/**
* Round towards negative infinity (-oo).
- * The result shall be the format’s floating-point number (possibly -oo)
+ * The result shall be the format's floating-point number (possibly -oo)
* closest to and no less than the infinitely precise result.
*/
ROUND_TOWARD_NEGATIVE,
/**
* Round towards zero.
- * The result shall be the format’s floating-point number closest to and no
+ * The result shall be the format's floating-point number closest to and no
* greater in magnitude than the infinitely precise result.
*/
ROUND_TOWARD_ZERO,
} // namespace std
namespace cvc5::api {
+/* -------------------------------------------------------------------------- */
+/* Options */
+/* -------------------------------------------------------------------------- */
+
+/**
+ * Provides access to options that can not be communicated via the regular
+ * getOption() or getOptionInfo() methods. This class does not store the options
+ * itself, but only acts as a wrapper to the solver object. It can thus no
+ * longer be used after the solver object has been destroyed.
+ */
+class CVC5_EXPORT DriverOptions
+{
+ friend class Solver;
+
+ public:
+ /** Access the solvers input stream */
+ std::istream& in() const;
+ /** Access the solvers error output stream */
+ std::ostream& err() const;
+ /** Access the solvers output stream */
+ std::ostream& out() const;
+
+ private:
+ DriverOptions(const Solver& solver);
+ const Solver& d_solver;
+};
+
+/**
+ * Holds some description about a particular option, including its name, its
+ * aliases, whether the option was explicitly set by the user, and information
+ * concerning its value. The `valueInfo` member holds any of the following
+ * alternatives:
+ * - VoidInfo if the option holds no value (or the value has no native type)
+ * - ValueInfo<T> if the option is of type bool or std::string, holds the
+ * current value and the default value.
+ * - NumberInfo<T> if the option is of type int64_t, uint64_t or double, holds
+ * the current and default value, as well as the minimum and maximum.
+ * - ModeInfo if the option is a mode option, holds the current and default
+ * values, as well as a list of valid modes.
+ * Additionally, this class provides convenience functions to obtain the
+ * current value of an option in a type-safe manner using boolValue(),
+ * stringValue(), intValue(), uintValue() and doubleValue(). They assert that
+ * the option has the respective type and return the current value.
+ */
+struct CVC5_EXPORT OptionInfo
+{
+ /** Has no value information */
+ struct VoidInfo {};
+ /** Has the current and the default value */
+ template <typename T>
+ struct ValueInfo
+ {
+ T defaultValue;
+ T currentValue;
+ };
+ /** Default value, current value, minimum and maximum of a numeric value */
+ template <typename T>
+ struct NumberInfo
+ {
+ T defaultValue;
+ T currentValue;
+ std::optional<T> minimum;
+ std::optional<T> maximum;
+ };
+ /** Default value, current value and choices of a mode option */
+ struct ModeInfo
+ {
+ std::string defaultValue;
+ std::string currentValue;
+ std::vector<std::string> modes;
+ };
+
+ /** The option name */
+ std::string name;
+ /** The option name aliases */
+ std::vector<std::string> aliases;
+ /** Whether the option was explicitly set by the user */
+ bool setByUser;
+ /** The option value information */
+ std::variant<VoidInfo,
+ ValueInfo<bool>,
+ ValueInfo<std::string>,
+ NumberInfo<int64_t>,
+ NumberInfo<uint64_t>,
+ NumberInfo<double>,
+ ModeInfo>
+ valueInfo;
+ /** Obtain the current value as a bool. Asserts that valueInfo holds a bool.
+ */
+ bool boolValue() const;
+ /** Obtain the current value as a string. Asserts that valueInfo holds a
+ * string. */
+ std::string stringValue() const;
+ /** Obtain the current value as as int. Asserts that valueInfo holds an int.
+ */
+ int64_t intValue() const;
+ /** Obtain the current value as a uint. Asserts that valueInfo holds a uint.
+ */
+ uint64_t uintValue() const;
+ /** Obtain the current value as a double. Asserts that valueInfo holds a
+ * double. */
+ double doubleValue() const;
+};
+
+/**
+ * Print a `OptionInfo` object to an ``std::ostream``.
+ */
+std::ostream& operator<<(std::ostream& os, const OptionInfo& oi) CVC5_EXPORT;
+
/* -------------------------------------------------------------------------- */
/* Statistics */
/* -------------------------------------------------------------------------- */
using BaseType = std::map<std::string, Stat>;
/** Custom iterator to hide certain statistics from regular iteration */
- class iterator
+ class CVC5_EXPORT iterator
{
public:
friend class Statistics;
/**
* Retrieve the statistic with the given name.
* Asserts that a statistic with the given name actually exists and throws
- * a `CVC4ApiRecoverableException` if it does not.
+ * a `CVC5ApiRecoverableException` if it does not.
* @param name Name of the statistic.
* @return The statistic with the given name.
*/
friend class DatatypeConstructor;
friend class DatatypeConstructorDecl;
friend class DatatypeSelector;
+ friend class DriverOptions;
friend class Grammar;
friend class Op;
friend class cvc5::Command;
+ friend class cvc5::main::CommandExecutor;
friend class Sort;
friend class Term;
+ private:
+ /*
+ * Constructs a solver with the given original options. This should only be
+ * used internally when the Solver is reset.
+ */
+ Solver(std::unique_ptr<Options>&& original);
+
public:
/* .................................................................... */
/* Constructors/Destructors */
/**
* Constructor.
- * @param opts an optional pointer to a solver options object
* @return the Solver
*/
- Solver(Options* opts = nullptr);
+ Solver();
/**
* Destructor.
Solver(const Solver&) = delete;
Solver& operator=(const Solver&) = delete;
- /* .................................................................... */
- /* Solver Configuration */
- /* .................................................................... */
-
- bool supportsFloatingPoint() const;
-
/* .................................................................... */
/* Sorts Handling */
/* .................................................................... */
* This method is called when the DatatypeDecl objects dtypedecls have been
* built using "unresolved" sorts.
*
- * We associate each sort in unresolvedSorts with exacly one datatype from
+ * We associate each sort in unresolvedSorts with exactly one datatype from
* dtypedecls. In particular, it must have the same name as exactly one
* datatype declaration in dtypedecls.
*
* When constructing datatypes, unresolved sorts are replaced by the datatype
* sort constructed for the datatype declaration it is associated with.
*
+ * @note Create unresolved sorts with Solver::mkUnresolvedSort().
+ *
* @param dtypedecls the datatype declarations from which the sort is created
* @param unresolvedSorts the list of unresolved sorts
* @return the datatype sorts
/**
* Create function sort.
- * @param domain the sort of the fuction argument
+ * @param domain the sort of the function argument
* @param codomain the sort of the function return value
* @return the function sort
*/
*/
Sort mkUninterpretedSort(const std::string& symbol) const;
+ /**
+ * Create an unresolved sort.
+ *
+ * This is for creating yet unresolved sort placeholders for mutually
+ * recursive datatypes.
+ *
+ * @param symbol the symbol of the sort
+ * @param arity the number of sort parameters of the sort
+ * @return the unresolved sort
+ */
+ Sort mkUnresolvedSort(const std::string& symbol, size_t arity = 0) const;
+
/**
* Create a sort constructor sort.
* @param symbol the symbol of the sort
/* .................................................................... */
/**
- * Create an operator for a builtin Kind
+ * Create an operator for a builtin Kind.
+ *
* The Kind may not be the Kind for an indexed operator
- * (e.g. BITVECTOR_EXTRACT)
- * Note: in this case, the Op simply wraps the Kind.
- * The Kind can be used in mkTerm directly without
- * creating an op first.
+ * (e.g. BITVECTOR_EXTRACT).
+ *
+ * @note In this case, the ``Op`` simply wraps the ``Kind``. The Kind can be
+ * used in ``Solver::mkTerm`` directly without creating an ``Op`` first.
* @param kind the kind to wrap
*/
Op mkOp(Kind kind) const;
/**
* Create operator of kind:
- * - RECORD_UPDATE
* - DIVISIBLE (to support arbitrary precision integers)
* See enum Kind for a description of the parameters.
* @param kind the kind of the operator
Term mkReal(int64_t num, int64_t den) const;
/**
- * Create a regular expression empty term.
- * @return the empty term
+ * Create a regular expression all (re.all) term.
+ * @return the all term
*/
- Term mkRegexpEmpty() const;
+ Term mkRegexpAll() const;
/**
- * Create a regular expression sigma term.
- * @return the sigma term
+ * Create a regular expression allchar (re.allchar) term.
+ * @return the allchar term
*/
- Term mkRegexpSigma() const;
+ Term mkRegexpAllchar() const;
+
+ /**
+ * Create a regular expression none (re.none) term.
+ * @return the none term
+ */
+ Term mkRegexpNone() const;
/**
* Create a constant representing an empty set of the given sort.
Term mkEmptyBag(const Sort& sort) const;
/**
- * Create a separation logic nil term.
+ * Create a separation logic empty term.
+ * @return the separation logic empty term
+ */
+ Term mkSepEmp() const;
+
+ /**
+ * Create a separation logic nil term.
* @param sort the sort of the nil term
* @return the separation logic nil term
*/
Term mkSepNil(const Sort& sort) const;
/**
- * Create a String constant.
+ * Create a String constant from a `std::string` which may contain SMT-LIB
+ * compatible escape sequences like `\u1234` to encode unicode characters.
* @param s the string this constant represents
- * @param useEscSequences determines whether escape sequences in \p s should
- * be converted to the corresponding character
+ * @param useEscSequences determines whether escape sequences in `s` should
+ * be converted to the corresponding unicode character
* @return the String constant
*/
Term mkString(const std::string& s, bool useEscSequences = false) const;
/**
- * Create a String constant.
- * @param c the character this constant represents
- * @return the String constant
- */
- Term mkString(const unsigned char c) const;
-
- /**
- * Create a String constant.
- * @param s a list of unsigned (unicode) values this constant represents as
- * string
+ * Create a String constant from a `std::wstring`.
+ * This method does not support escape sequences as `std::wstring` already
+ * supports unicode characters.
+ * @param s the string this constant represents
* @return the String constant
*/
- Term mkString(const std::vector<uint32_t>& s) const;
-
- /**
- * Create a character constant from a given string.
- * @param s the string denoting the code point of the character (in base 16)
- * @return the character constant
- */
- Term mkChar(const std::string& s) const;
+ Term mkString(const std::wstring& s) const;
/**
* Create an empty sequence of the given element sort.
/**
* Create a bit-vector constant of given size and value.
+ *
+ * @note The given value must fit into a bit-vector of the given size.
+ *
* @param size the bit-width of the bit-vector sort
* @param val the value of the constant
* @return the bit-vector constant
*/
Term mkBitVector(uint32_t size, uint64_t val = 0) const;
- /**
- * Create a bit-vector constant from a given string of base 2, 10 or 16.
- *
- * The size of resulting bit-vector is
- * - base 2: the size of the binary string
- * - base 10: the min. size required to represent the decimal as a bit-vector
- * - base 16: the max. size required to represent the hexadecimal as a
- * bit-vector (4 * size of the given value string)
- *
- * @param s the string representation of the constant
- * @param base the base of the string representation (2, 10, or 16)
- * @return the bit-vector constant
- */
- Term mkBitVector(const std::string& s, uint32_t base = 2) const;
-
/**
* Create a bit-vector constant of a given bit-width from a given string of
* base 2, 10 or 16.
+ *
+ * @note The given value must fit into a bit-vector of the given size.
+ *
* @param size the bit-width of the constant
* @param s the string representation of the constant
* @param base the base of the string representation (2, 10, or 16)
Term mkConstArray(const Sort& sort, const Term& val) const;
/**
- * Create a positive infinity floating-point constant. Requires cvc5 to be
- * compiled with SymFPU support.
+ * Create a positive infinity floating-point constant.
* @param exp Number of bits in the exponent
* @param sig Number of bits in the significand
* @return the floating-point constant
Term mkPosInf(uint32_t exp, uint32_t sig) const;
/**
- * Create a negative infinity floating-point constant. Requires cvc5 to be
- * compiled with SymFPU support.
+ * Create a negative infinity floating-point constant.
* @param exp Number of bits in the exponent
* @param sig Number of bits in the significand
* @return the floating-point constant
Term mkNegInf(uint32_t exp, uint32_t sig) const;
/**
- * Create a not-a-number (NaN) floating-point constant. Requires cvc5 to be
- * compiled with SymFPU support.
+ * Create a not-a-number (NaN) floating-point constant.
* @param exp Number of bits in the exponent
* @param sig Number of bits in the significand
* @return the floating-point constant
Term mkNaN(uint32_t exp, uint32_t sig) const;
/**
- * Create a positive zero (+0.0) floating-point constant. Requires cvc5 to be
- * compiled with SymFPU support.
+ * Create a positive zero (+0.0) floating-point constant.
* @param exp Number of bits in the exponent
* @param sig Number of bits in the significand
* @return the floating-point constant
Term mkPosZero(uint32_t exp, uint32_t sig) const;
/**
- * Create a negative zero (-0.0) floating-point constant. Requires cvc5 to be
- * compiled with SymFPU support.
+ * Create a negative zero (-0.0) floating-point constant.
* @param exp Number of bits in the exponent
* @param sig Number of bits in the significand
* @return the floating-point constant
/**
* Create an abstract value constant.
+ * The given index needs to be a positive integer in base 10.
* @param index Index of the abstract value
*/
Term mkAbstractValue(const std::string& index) const;
/**
* Create an abstract value constant.
+ * The given index needs to be positive.
* @param index Index of the abstract value
*/
Term mkAbstractValue(uint64_t index) const;
/**
- * Create a floating-point constant (requires cvc5 to be compiled with symFPU
- * support).
+ * Create a floating-point constant.
* @param exp Size of the exponent
* @param sig Size of the significand
* @param val Value of the floating-point constant as a bit-vector term
*/
Term mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const;
+ /**
+ * Create a cardinality constraint for an uninterpreted sort.
+ * @param sort the sort the cardinality constraint is for
+ * @param upperBound the upper bound on the cardinality of the sort
+ * @return the cardinality constraint
+ */
+ Term mkCardinalityConstraint(const Sort& sort, uint32_t upperBound) const;
+
/* .................................................................... */
/* Create Variables */
/* .................................................................... */
/**
* Create (first-order) constant (0-arity function symbol).
+ *
* SMT-LIB:
- * \verbatim
- * ( declare-const <symbol> <sort> )
- * ( declare-fun <symbol> ( ) <sort> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (declare-const <symbol> <sort>)
+ * (declare-fun <symbol> () <sort>)
* \endverbatim
*
* @param sort the sort of the constant
/**
* Assert a formula.
+ *
* SMT-LIB:
- * \verbatim
- * ( assert <term> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (assert <term>)
* \endverbatim
+ *
* @param term the formula to assert
*/
void assertFormula(const Term& term) const;
/**
* Check satisfiability.
+ *
* SMT-LIB:
- * \verbatim
- * ( check-sat )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (check-sat)
* \endverbatim
+ *
* @return the result of the satisfiability check.
*/
Result checkSat() const;
/**
* Check satisfiability assuming the given formula.
+ *
* SMT-LIB:
- * \verbatim
- * ( check-sat-assuming ( <prop_literal> ) )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (check-sat-assuming ( <prop_literal> ))
* \endverbatim
+ *
* @param assumption the formula to assume
* @return the result of the satisfiability check.
*/
/**
* Check satisfiability assuming the given formulas.
+ *
* SMT-LIB:
- * \verbatim
- * ( check-sat-assuming ( <prop_literal>+ ) )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (check-sat-assuming ( <prop_literal>+ ))
* \endverbatim
+ *
* @param assumptions the formulas to assume
* @return the result of the satisfiability check.
*/
/**
* Create datatype sort.
+ *
* SMT-LIB:
- * \verbatim
- * ( declare-datatype <symbol> <datatype_decl> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (declare-datatype <symbol> <datatype_decl>)
* \endverbatim
+ *
* @param symbol the name of the datatype sort
* @param ctors the constructor declarations of the datatype sort
* @return the datatype sort
/**
* Declare n-ary function symbol.
+ *
* SMT-LIB:
- * \verbatim
- * ( declare-fun <symbol> ( <sort>* ) <sort> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (declare-fun <symbol> ( <sort>* ) <sort>)
* \endverbatim
+ *
* @param symbol the name of the function
* @param sorts the sorts of the parameters to this function
* @param sort the sort of the return value of this function
/**
* Declare uninterpreted sort.
+ *
* SMT-LIB:
- * \verbatim
- * ( declare-sort <symbol> <numeral> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (declare-sort <symbol> <numeral>)
* \endverbatim
+ *
* @param symbol the name of the sort
* @param arity the arity of the sort
* @return the sort
/**
* Define n-ary function.
+ *
* SMT-LIB:
- * \verbatim
- * ( define-fun <function_def> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (define-fun <function_def>)
* \endverbatim
+ *
* @param symbol the name of the function
* @param bound_vars the parameters to this function
* @param sort the sort of the return value of this function
const Sort& sort,
const Term& term,
bool global = false) const;
- /**
- * Define n-ary function.
- * SMT-LIB:
- * \verbatim
- * ( define-fun <function_def> )
- * \endverbatim
- * Create parameter 'fun' with mkConst().
- * @param fun the sorted function
- * @param bound_vars the parameters to this function
- * @param term the function body
- * @param global determines whether this definition is global (i.e. persists
- * when popping the context)
- * @return the function
- */
- Term defineFun(const Term& fun,
- const std::vector<Term>& bound_vars,
- const Term& term,
- bool global = false) const;
/**
* Define recursive function.
+ *
* SMT-LIB:
- * \verbatim
- * ( define-fun-rec <function_def> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (define-fun-rec <function_def>)
* \endverbatim
+ *
* @param symbol the name of the function
* @param bound_vars the parameters to this function
* @param sort the sort of the return value of this function
/**
* Define recursive function.
+ *
* SMT-LIB:
- * \verbatim
- * ( define-fun-rec <function_def> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (define-fun-rec <function_def>)
* \endverbatim
+ *
* Create parameter 'fun' with mkConst().
* @param fun the sorted function
* @param bound_vars the parameters to this function
/**
* Define recursive functions.
+ *
* SMT-LIB:
- * \verbatim
- * ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (define-funs-rec
+ * ( <function_decl>_1 ... <function_decl>_n )
+ * ( <term>_1 ... <term>_n )
+ * )
* \endverbatim
+ *
* Create elements of parameter 'funs' with mkConst().
* @param funs the sorted functions
* @param bound_vars the list of parameters to the functions
/**
* Echo a given string to the given output stream.
+ *
* SMT-LIB:
- * \verbatim
- * ( echo <std::string> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (echo <string>)
* \endverbatim
+ *
* @param out the output stream
* @param str the string to echo
*/
/**
* Get the list of asserted formulas.
+ *
* SMT-LIB:
- * \verbatim
- * ( get-assertions )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-assertions)
* \endverbatim
+ *
* @return the list of asserted formulas
*/
std::vector<Term> getAssertions() const;
/**
* Get info from the solver.
- * SMT-LIB: \verbatim( get-info <info_flag> )\verbatim
+ *
+ * SMT-LIB:
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-info <info_flag>)
+ * \endverbatim
+ *
* @return the info
*/
std::string getInfo(const std::string& flag) const;
/**
* Get the value of a given option.
+ *
* SMT-LIB:
- * \verbatim
- * ( get-option <keyword> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-option <keyword>)
* \endverbatim
+ *
* @param option the option for which the value is queried
* @return a string representation of the option value
*/
std::string getOption(const std::string& option) const;
+ /**
+ * Get all option names that can be used with `setOption`, `getOption` and
+ * `getOptionInfo`.
+ * @return all option names
+ */
+ std::vector<std::string> getOptionNames() const;
+
+ /**
+ * Get some information about the given option. Check the `OptionInfo` class
+ * for more details on which information is available.
+ * @return information about the given option
+ */
+ OptionInfo getOptionInfo(const std::string& option) const;
+
+ /**
+ * Get the driver options, which provide access to options that can not be
+ * communicated properly via getOption() and getOptionInfo().
+ * @return a DriverOptions object.
+ */
+ DriverOptions getDriverOptions() const;
+
/**
* Get the set of unsat ("failed") assumptions.
+ *
* SMT-LIB:
- * \verbatim
- * ( get-unsat-assumptions )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-unsat-assumptions)
+ *
+ * Requires to enable option
+ * :ref:`produce-unsat-assumptions <lbl-option-produce-unsat-assumptions>`.
* \endverbatim
- * Requires to enable option 'produce-unsat-assumptions'.
+ *
* @return the set of unsat assumptions.
*/
std::vector<Term> getUnsatAssumptions() const;
/**
* Get the unsatisfiable core.
+ *
* SMT-LIB:
- * \verbatim
- * ( get-unsat-core )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-unsat-core)
+ *
+ * Requires to enable option
+ * :ref:`produce-unsat-cores <lbl-option-produce-unsat-cores>`.
* \endverbatim
- * Requires to enable option 'produce-unsat-cores'.
+ *
* @return a set of terms representing the unsatisfiable core
*/
std::vector<Term> getUnsatCore() const;
/**
- * Get the value of the given term.
+ * Get a difficulty estimate for an asserted formula. This method is
+ * intended to be called immediately after any response to a checkSat.
+ *
+ * @return a map from (a subset of) the input assertions to a real value that
+ * is an estimate of how difficult each assertion was to solve.
+ * Unmentioned assertions can be assumed to have zero difficulty.
+ */
+ std::map<Term, Term> getDifficulty() const;
+
+ /**
+ * Get the refutation proof
+ *
* SMT-LIB:
- * \verbatim
- * ( get-value ( <term> ) )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-proof)
+ *
+ * Requires to enable option
+ * :ref:`produce-proofs <lbl-option-produce-proofs>`.
* \endverbatim
+ *
+ * @return a string representing the proof, according to the value of
+ * proof-format-mode.
+ */
+ std::string getProof() const;
+
+ /**
+ * Get the value of the given term in the current model.
+ *
+ * SMT-LIB:
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-value ( <term> ))
+ * \endverbatim
+ *
* @param term the term for which the value is queried
* @return the value of the given term
*/
Term getValue(const Term& term) const;
+
/**
- * Get the values of the given terms.
+ * Get the values of the given terms in the current model.
+ *
* SMT-LIB:
- * \verbatim
- * ( get-value ( <term>+ ) )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-value ( <term>* ))
* \endverbatim
+ *
* @param terms the terms for which the value is queried
* @return the values of the given terms
*/
std::vector<Term> getValue(const std::vector<Term>& terms) const;
+ /**
+ * Get the domain elements of uninterpreted sort s in the current model. The
+ * current model interprets s as the finite sort whose domain elements are
+ * given in the return value of this method.
+ *
+ * @param s The uninterpreted sort in question
+ * @return the domain elements of s in the current model
+ */
+ std::vector<Term> getModelDomainElements(const Sort& s) const;
+
+ /**
+ * This returns false if the model value of free constant v was not essential
+ * for showing the satisfiability of the last call to checkSat using the
+ * current model. This method will only return false (for any v) if
+ * option
+ * \verbatim:rst:inline
+ * :ref:`model-cores <lbl-option-model-cores>`
+ * \endverbatim
+ * has been set.
+ *
+ * @param v The term in question
+ * @return true if v is a model core symbol
+ */
+ bool isModelCoreSymbol(const Term& v) const;
+
+ /**
+ * Get the model
+ *
+ * SMT-LIB:
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-model)
+ *
+ * Requires to enable option
+ * :ref:`produce-models <lbl-option-produce-models>`.
+ * \endverbatim
+ *
+ * \endverbatim
+ *
+ * @param sorts The list of uninterpreted sorts that should be printed in the
+ * model.
+ * @param vars The list of free constants that should be printed in the
+ * model. A subset of these may be printed based on isModelCoreSymbol.
+ * @return a string representing the model.
+ */
+ std::string getModel(const std::vector<Sort>& sorts,
+ const std::vector<Term>& vars) const;
+
/**
* Do quantifier elimination.
+ *
* SMT-LIB:
- * \verbatim
- * ( get-qe <q> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-qe <q>)
* \endverbatim
+ *
* Requires a logic that supports quantifier elimination. Currently, the only
* logics supported by quantifier elimination is LRA and LIA.
- * @param q a quantified formula of the form:
- * Q x1...xn. P( x1...xn, y1...yn )
- * where P( x1...xn, y1...yn ) is a quantifier-free formula
- * @return a formula ret such that, given the current set of formulas A
- * asserted to this solver:
- * - ( A ^ q ) and ( A ^ ret ) are equivalent
- * - ret is quantifier-free formula containing only free variables in
- * y1...yn.
+ *
+ * @note Quantifier Elimination is is only complete for LRA and LIA.
+ *
+ * @param q a quantified formula of the form
+ * @f$Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)@f$
+ * where
+ * @f$Q\bar{x}@f$ is a set of quantified variables of the form
+ * @f$Q x_1...x_k@f$ and
+ * @f$P( x_1...x_i, y_1...y_j )@f$ is a quantifier-free formula
+ * @return a formula @f$\phi@f$ such that, given the current set of formulas
+ * @f$A@f$ asserted to this solver:
+ * - @f$(A \wedge q)@f$ and @f$(A \wedge \phi)@f$ are equivalent
+ * - @f$\phi@f$ is quantifier-free formula containing only free
+ * variables in @f$y_1...y_n@f$.
*/
Term getQuantifierElimination(const Term& q) const;
/**
* Do partial quantifier elimination, which can be used for incrementally
* computing the result of a quantifier elimination.
+ *
* SMT-LIB:
- * \verbatim
- * ( get-qe-disjunct <q> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-qe-disjunct <q>)
* \endverbatim
+ *
* Requires a logic that supports quantifier elimination. Currently, the only
* logics supported by quantifier elimination is LRA and LIA.
- * @param q a quantified formula of the form:
- * Q x1...xn. P( x1...xn, y1...yn )
- * where P( x1...xn, y1...yn ) is a quantifier-free formula
- * @return a formula ret such that, given the current set of formulas A
- * asserted to this solver:
- * - (A ^ q) => (A ^ ret) if Q is forall or (A ^ ret) => (A ^ q) if Q is
- * exists,
- * - ret is quantifier-free formula containing only free variables in
- * y1...yn,
- * - If Q is exists, let A^Q_n be the formula
- * A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n
- * where for each i=1,...n, formula ret^Q_i is the result of calling
- * getQuantifierEliminationDisjunct for q with the set of assertions
- * A^Q_{i-1}. Similarly, if Q is forall, then let A^Q_n be
- * A ^ ret^Q_1 ^ ... ^ ret^Q_n
- * where ret^Q_i is the same as above. In either case, we have
- * that ret^Q_j will eventually be true or false, for some finite j.
+ * @param q a quantified formula of the form
+ * @f$Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)@f$
+ * where
+ * @f$Q\bar{x}@f$ is a set of quantified variables of the form
+ * @f$Q x_1...x_k@f$ and
+ * @f$P( x_1...x_i, y_1...y_j )@f$ is a quantifier-free formula
+ * @return a formula @f$\phi@f$ such that, given the current set of formulas
+ * @f$A@f$ asserted to this solver:
+ * - @f$(A \wedge q \implies A \wedge \phi)@f$ if @f$Q@f$ is
+ * @f$\forall@f$, and @f$(A \wedge \phi \implies A \wedge q)@f$ if
+ * @f$Q@f$ is @f$\exists@f$
+ * - @f$\phi@f$ is quantifier-free formula containing only free
+ * variables in @f$y_1...y_n@f$
+ * - If @f$Q@f$ is @f$\exists@f$, let @f$(A \wedge Q_n)@f$ be the
+ * formula
+ * @f$(A \wedge \neg (\phi \wedge Q_1) \wedge ... \wedge
+ * \neg (\phi \wedge Q_n))@f$
+ * where for each @f$i = 1...n@f$,
+ * formula @f$(\phi \wedge Q_i)@f$ is the result of calling
+ * Solver::getQuantifierEliminationDisjunct() for @f$q@f$ with the
+ * set of assertions @f$(A \wedge Q_{i-1})@f$.
+ * Similarly, if @f$Q@f$ is @f$\forall@f$, then let
+ * @f$(A \wedge Q_n)@f$ be
+ * @f$(A \wedge (\phi \wedge Q_1) \wedge ... \wedge (\phi \wedge
+ * Q_n))@f$
+ * where @f$(\phi \wedge Q_i)@f$ is the same as above.
+ * In either case, we have that @f$(\phi \wedge Q_j)@f$ will
+ * eventually be true or false, for some finite j.
*/
Term getQuantifierEliminationDisjunct(const Term& q) const;
* @param locSort The location sort of the heap
* @param dataSort The data sort of the heap
*/
- void declareSeparationHeap(const Sort& locSort, const Sort& dataSort) const;
+ void declareSepHeap(const Sort& locSort, const Sort& dataSort) const;
/**
* When using separation logic, obtain the term for the heap.
* @return The term for the heap
*/
- Term getSeparationHeap() const;
+ Term getValueSepHeap() const;
/**
* When using separation logic, obtain the term for nil.
* @return The term for nil
*/
- Term getSeparationNilTerm() const;
+ Term getValueSepNil() const;
/**
* Declare a symbolic pool of terms with the given initial value.
+ *
* SMT-LIB:
- * \verbatim
- * ( declare-pool <symbol> <sort> ( <term>* ) )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (declare-pool <symbol> <sort> ( <term>* ))
* \endverbatim
+ *
* @param symbol The name of the pool
* @param sort The sort of the elements of the pool.
* @param initValue The initial value of the pool
const std::vector<Term>& initValue) const;
/**
* Pop (a) level(s) from the assertion stack.
+ *
* SMT-LIB:
- * \verbatim
- * ( pop <numeral> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (pop <numeral>)
* \endverbatim
+ *
* @param nscopes the number of levels to pop
*/
void pop(uint32_t nscopes = 1) const;
/**
* Get an interpolant
+ *
* SMT-LIB:
- * \verbatim
- * ( get-interpol <conj> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-interpol <conj>)
+ *
+ * Requires to enable option
+ * :ref:`produce-interpols <lbl-option-produce-interpols>`.
* \endverbatim
- * Requires to enable option 'produce-interpols'.
+ *
* @param conj the conjecture term
* @param output a Term I such that A->I and I->B are valid, where A is the
* current set of assertions and B is given in the input by conj.
/**
* Get an interpolant
+ *
* SMT-LIB:
- * \verbatim
- * ( get-interpol <conj> <g> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-interpol <conj> <grammar>)
+ *
+ * Requires to enable option
+ * :ref:`produce-interpols <lbl-option-produce-interpols>`.
* \endverbatim
- * Requires to enable option 'produce-interpols'.
+ *
* @param conj the conjecture term
* @param grammar the grammar for the interpolant I
* @param output a Term I such that A->I and I->B are valid, where A is the
/**
* Get an abduct.
+ *
* SMT-LIB:
- * \verbatim
- * ( get-abduct <conj> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-abduct <conj>)
+ *
+ * Requires to enable option
+ * :ref:`produce-abducts <lbl-option-produce-abducts>`.
* \endverbatim
- * Requires enabling option 'produce-abducts'
+ *
* @param conj the conjecture term
- * @param output a term C such that A^C is satisfiable, and A^~B^C is
- * unsatisfiable, where A is the current set of assertions and B is
- * given in the input by conj
- * @return true if it gets C successfully, false otherwise
+ * @param output a term @f$C@f$ such that @f$(A \wedge C)@f$ is satisfiable,
+ * and @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where
+ * @f$A@f$ is the current set of assertions and @f$B@f$ is
+ * given in the input by ``conj``.
+ * @return true if it gets abduct @f$C@f$ successfully, false otherwise
*/
bool getAbduct(const Term& conj, Term& output) const;
/**
* Get an abduct.
+ *
* SMT-LIB:
- * \verbatim
- * ( get-abduct <conj> <g> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-abduct <conj> <grammar>)
+ *
+ * Requires to enable option
+ * :ref:`produce-abducts <lbl-option-produce-abducts>`.
* \endverbatim
- * Requires enabling option 'produce-abducts'
+ *
* @param conj the conjecture term
- * @param grammar the grammar for the abduct C
- * @param output a term C such that A^C is satisfiable, and A^~B^C is
- * unsatisfiable, where A is the current set of assertions and B is
- * given in the input by conj
- * @return true if it gets C successfully, false otherwise
+ * @param grammar the grammar for the abduct @f$C@f$
+ * @param output a term C such that @f$(A \wedge C)@f$ is satisfiable, and
+ * @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where @f$A@f$ is
+ * the current set of assertions and @f$B@f$ is given in the input by
+ * ``conj``
+ * @return true if it gets abduct @f$C@f$ successfully, false otherwise
*/
bool getAbduct(const Term& conj, Grammar& grammar, Term& output) const;
+ /**
+ * Get the next abduct. Can only be called immediately after a successful
+ * call to get-abduct or get-abduct-next. Is guaranteed to produce a
+ * syntactically different abduct wrt the last returned abduct if successful.
+ *
+ * SMT-LIB:
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-abduct-next)
+ *
+ * Requires to enable incremental mode, and option
+ * :ref:`produce-abducts <lbl-option-produce-abducts>`.
+ * \endverbatim
+ *
+ * @param output a term C such that @f$(A \wedge C)@f$ is satisfiable, and
+ * @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where @f$A@f$ is
+ * the current set of assertions and @f$B@f$ is given in the input by
+ * the last call to getAbduct.
+ * @return true if it gets abduct @f$C@f$ successfully, false otherwise
+ */
+ bool getAbductNext(Term& output) const;
+
/**
* Block the current model. Can be called only if immediately preceded by a
* SAT or INVALID query.
+ *
* SMT-LIB:
- * \verbatim
- * ( block-model )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (block-model)
+ *
+ * Requires enabling option
+ * :ref:`produce-models <lbl-option-produce-models>`.
+ * 'produce-models' and setting option
+ * :ref:`block-models <lbl-option-block-models>`.
+ * to a mode other than ``none``.
* \endverbatim
- * Requires enabling 'produce-models' option and setting 'block-models' option
- * to a mode other than "none".
*/
void blockModel() const;
/**
* Block the current model values of (at least) the values in terms. Can be
* called only if immediately preceded by a SAT or NOT_ENTAILED query.
+ *
* SMT-LIB:
- * \verbatim
- * ( block-model-values ( <terms>+ ) )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (block-model-values ( <terms>+ ))
+ *
+ * Requires enabling option
+ * :ref:`produce-models <lbl-option-produce-models>`.
+ * 'produce-models' and setting option
+ * :ref:`block-models <lbl-option-block-models>`.
+ * to a mode other than ``none``.
* \endverbatim
- * Requires enabling 'produce-models' option and setting 'block-models' option
- * to a mode other than "none".
*/
void blockModelValues(const std::vector<Term>& terms) const;
/**
* Push (a) level(s) to the assertion stack.
+ *
* SMT-LIB:
- * \verbatim
- * ( push <numeral> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (push <numeral>)
* \endverbatim
+ *
* @param nscopes the number of levels to push
*/
void push(uint32_t nscopes = 1) const;
/**
* Remove all assertions.
+ *
* SMT-LIB:
- * \verbatim
- * ( reset-assertions )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (reset-assertions)
* \endverbatim
+ *
*/
void resetAssertions() const;
/**
* Set info.
+ *
* SMT-LIB:
- * \verbatim
- * ( set-info <attribute> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (set-info <attribute>)
* \endverbatim
+ *
* @param keyword the info flag
* @param value the value of the info flag
*/
/**
* Set logic.
+ *
* SMT-LIB:
- * \verbatim
- * ( set-logic <symbol> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (set-logic <symbol>)
* \endverbatim
+ *
* @param logic the logic to set
*/
void setLogic(const std::string& logic) const;
/**
* Set option.
+ *
* SMT-LIB:
- * \verbatim
- * ( set-option <option> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (set-option :<option> <value>)
* \endverbatim
+ *
* @param option the option name
* @param value the option value
*/
void setOption(const std::string& option, const std::string& value) const;
/**
- * If needed, convert this term to a given sort. Note that the sort of the
- * term must be convertible into the target sort. Currently only Int to Real
- * conversions are supported.
+ * If needed, convert this term to a given sort.
+ *
+ * @note The sort of the term must be convertible into the target sort.
+ * Currently only Int to Real conversions are supported.
* @param t the term
* @param s the target sort
* @return the term wrapped into a sort conversion if needed
/**
* Append \p symbol to the current list of universal variables.
+ *
* SyGuS v2:
- * \verbatim
- * ( declare-var <symbol> <sort> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (declare-var <symbol> <sort>)
* \endverbatim
+ *
* @param sort the sort of the universal variable
* @param symbol the name of the universal variable
* @return the universal variable
/**
* Synthesize n-ary function.
+ *
* SyGuS v2:
- * \verbatim
- * ( synth-fun <symbol> ( <boundVars>* ) <sort> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (synth-fun <symbol> ( <boundVars>* ) <sort>)
* \endverbatim
+ *
* @param symbol the name of the function
* @param boundVars the parameters to this function
* @param sort the sort of the return value of this function
/**
* Synthesize n-ary function following specified syntactic constraints.
+ *
* SyGuS v2:
- * \verbatim
- * ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (synth-fun <symbol> ( <boundVars>* ) <sort> <grammar>)
* \endverbatim
+ *
* @param symbol the name of the function
* @param boundVars the parameters to this function
* @param sort the sort of the return value of this function
/**
* Synthesize invariant.
+ *
* SyGuS v2:
- * \verbatim
- * ( synth-inv <symbol> ( <boundVars>* ) )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (synth-inv <symbol> ( <boundVars>* ))
* \endverbatim
+ *
* @param symbol the name of the invariant
* @param boundVars the parameters to this invariant
* @return the invariant
/**
* Synthesize invariant following specified syntactic constraints.
+ *
* SyGuS v2:
- * \verbatim
- * ( synth-inv <symbol> ( <boundVars>* ) <g> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (synth-inv <symbol> ( <boundVars>* ) <grammar>)
* \endverbatim
+ *
* @param symbol the name of the invariant
* @param boundVars the parameters to this invariant
* @param grammar the syntactic constraints
/**
* Add a forumla to the set of Sygus constraints.
+ *
* SyGuS v2:
- * \verbatim
- * ( constraint <term> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (constraint <term>)
* \endverbatim
+ *
* @param term the formula to add as a constraint
*/
void addSygusConstraint(const Term& term) const;
+ /**
+ * Add a forumla to the set of Sygus assumptions.
+ *
+ * SyGuS v2:
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (assume <term>)
+ * \endverbatim
+ *
+ * @param term the formula to add as an assumption
+ */
+ void addSygusAssume(const Term& term) const;
+
/**
* Add a set of Sygus constraints to the current state that correspond to an
* invariant synthesis problem.
+ *
* SyGuS v2:
- * \verbatim
- * ( inv-constraint <inv> <pre> <trans> <post> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (inv-constraint <inv> <pre> <trans> <post>)
* \endverbatim
+ *
* @param inv the function-to-synthesize
* @param pre the pre-condition
* @param trans the transition relation
* Try to find a solution for the synthesis conjecture corresponding to the
* current list of functions-to-synthesize, universal variables and
* constraints.
+ *
* SyGuS v2:
- * \verbatim
- * ( check-synth )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (check-synth)
* \endverbatim
- * @return the result of the synthesis conjecture.
+ *
+ * @return the result of the check, which is unsat if the check succeeded,
+ * in which case solutions are available via getSynthSolutions.
*/
Result checkSynth() const;
+ /**
+ * Try to find a next solution for the synthesis conjecture corresponding to
+ * the current list of functions-to-synthesize, universal variables and
+ * constraints. Must be called immediately after a successful call to
+ * check-synth or check-synth-next. Requires incremental mode.
+ *
+ * SyGuS v2:
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (check-synth-next)
+ * \endverbatim
+ *
+ * @return the result of the check, which is unsat if the check succeeded,
+ * in which case solutions are available via getSynthSolutions.
+ */
+ Result checkSynthNext() const;
+
/**
* Get the synthesis solution of the given term. This method should be called
* immediately after the solver answers unsat for sygus input.
*/
std::vector<Term> getSynthSolutions(const std::vector<Term>& terms) const;
- /**
- * Print solution for synthesis conjecture to the given output stream.
- * @param out the output stream
- */
- void printSynthSolution(std::ostream& out) const;
-
- // !!! This is only temporarily available until the parser is fully migrated
- // to the new API. !!!
- SmtEngine* getSmtEngine(void) const;
-
- // !!! This is only temporarily available until options are refactored at
- // the driver level. !!!
- Options& getOptions(void);
-
/**
* Returns a snapshot of the current state of the statistic values of this
* solver. The returned object is completely decoupled from the solver and
*/
Statistics getStatistics() const;
+ /**
+ * Whether the output stream for the given tag is enabled. Tags can be enabled
+ * with the `output` option (and `-o <tag>` on the command line). Raises an
+ * exception when an invalid tag is given.
+ */
+ bool isOutputOn(const std::string& tag) const;
+
+ /**
+ * Returns an output stream for the given tag. Tags can be enabled with the
+ * `output` option (and `-o <tag>` on the command line). Raises an exception
+ * when an invalid tag is given.
+ */
+ std::ostream& getOutput(const std::string& tag) const;
+
private:
/** @return the node manager of this solver */
NodeManager* getNodeManager(void) const;
/** Reset the API statistics */
void resetStatistics();
+ /**
+ * Print the statistics to the given file descriptor, suitable for usage in
+ * signal handlers.
+ */
+ void printStatisticsSafe(int fd) const;
+
/** Helper to check for API misuse in mkOp functions. */
void checkMkTerm(Kind kind, uint32_t nchildren) const;
/** Helper for mk-functions that call d_nodeMgr->mkConst(). */
template <typename T>
- Term mkValHelper(T t) const;
+ Term mkValHelper(const T& t) const;
+ /** Helper for making rational values. */
+ Term mkRationalValHelper(const Rational& r, bool isInt = true) const;
/** Helper for mkReal functions that take a string as argument. */
- Term mkRealFromStrHelper(const std::string& s) const;
+ Term mkRealOrIntegerFromStrHelper(const std::string& s,
+ bool isInt = true) const;
/** Helper for mkBitVector functions that take a string as argument. */
Term mkBVFromStrHelper(const std::string& s, uint32_t base) const;
/**
/**
* Synthesize n-ary function following specified syntactic constraints.
+ *
* SMT-LIB:
- * \verbatim
- * ( synth-fun <symbol> ( <boundVars>* ) <sort> <g>? )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (synth-fun <symbol> ( <boundVars>* ) <sort> <grammar>?)
* \endverbatim
+ *
* @param symbol the name of the function
* @param boundVars the parameters to this function
* @param sort the sort of the return value of this function
/** Keep a copy of the original option settings (for resets). */
std::unique_ptr<Options> d_originalOptions;
/** The node manager of this solver. */
- std::unique_ptr<NodeManager> d_nodeMgr;
+ NodeManager* d_nodeMgr;
/** The statistics collected on the Api level. */
std::unique_ptr<APIStatistics> d_stats;
/** The SMT engine of this solver. */
- std::unique_ptr<SmtEngine> d_smtEngine;
+ std::unique_ptr<SolverEngine> d_slv;
/** The random number generator of this solver. */
std::unique_ptr<Random> d_rng;
};
projects / cvc5.git / blobdiff