diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-05 19:31:28 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-05 19:31:28 -0700 |
| commit | d2e454e0dfc06e16fe0a4228168b21cf1311fc35 (patch) | |
| tree | 65063161aa9e21348182b13251524c58b0ca49c5 /src/api/cvc4cpp.h | |
| parent | 00a20b53ce998f52b18303a7a680e6a00acc098c (diff) | |
New C++ Api: Rename and move headers. (#6292)
Diffstat (limited to 'src/api/cvc4cpp.h')
| -rw-r--r-- | src/api/cvc4cpp.h | 3659 |
1 files changed, 0 insertions, 3659 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h deleted file mode 100644 index 8f4977b28..000000000 --- a/src/api/cvc4cpp.h +++ /dev/null @@ -1,3659 +0,0 @@ -/********************* */ -/*! \file cvc4cpp.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The CVC4 C++ API. - ** - ** The CVC4 C++ API. - **/ - -#include "cvc4_export.h" - -#ifndef CVC4__API__CVC4CPP_H -#define CVC4__API__CVC4CPP_H - -#include "api/cvc4cppkind.h" - -#include <map> -#include <memory> -#include <set> -#include <sstream> -#include <string> -#include <unordered_map> -#include <unordered_set> -#include <vector> - -namespace cvc5 { - -template <bool ref_count> -class NodeTemplate; -typedef NodeTemplate<true> Node; - -class Command; -class DType; -class DTypeConstructor; -class DTypeSelector; -class NodeManager; -class SmtEngine; -class TypeNode; -class Options; -class Random; -class Result; - -namespace api { - -class Solver; -struct Statistics; - -/* -------------------------------------------------------------------------- */ -/* Exception */ -/* -------------------------------------------------------------------------- */ - -class CVC4_EXPORT CVC4ApiException : public std::exception -{ - public: - CVC4ApiException(const std::string& str) : d_msg(str) {} - CVC4ApiException(const std::stringstream& stream) : d_msg(stream.str()) {} - std::string getMessage() const { return d_msg; } - const char* what() const noexcept override { return d_msg.c_str(); } - - private: - std::string d_msg; -}; - -class CVC4_EXPORT CVC4ApiRecoverableException : public CVC4ApiException -{ - public: - CVC4ApiRecoverableException(const std::string& str) : CVC4ApiException(str) {} - CVC4ApiRecoverableException(const std::stringstream& stream) - : CVC4ApiException(stream.str()) - { - } -}; - -/* -------------------------------------------------------------------------- */ -/* Result */ -/* -------------------------------------------------------------------------- */ - -/** - * Encapsulation of a three-valued solver result, with explanations. - */ -class CVC4_EXPORT Result -{ - friend class Solver; - - public: - enum UnknownExplanation - { - REQUIRES_FULL_CHECK, - INCOMPLETE, - TIMEOUT, - RESOURCEOUT, - MEMOUT, - INTERRUPTED, - NO_STATUS, - UNSUPPORTED, - OTHER, - UNKNOWN_REASON - }; - - /** Constructor. */ - Result(); - - /** - * Return true if Result is empty, i.e., a nullary Result, and not an actual - * result returned from a checkSat() (and friends) query. - */ - bool isNull() const; - - /** - * Return true if query was a satisfiable checkSat() or checkSatAssuming() - * query. - */ - bool isSat() const; - - /** - * Return true if query was an unsatisfiable checkSat() or - * checkSatAssuming() query. - */ - bool isUnsat() const; - - /** - * Return true if query was a checkSat() or checkSatAssuming() query and - * CVC4 was not able to determine (un)satisfiability. - */ - bool isSatUnknown() const; - - /** - * Return true if corresponding query was an entailed checkEntailed() query. - */ - bool isEntailed() const; - - /** - * Return true if corresponding query was a checkEntailed() query that is - * not entailed. - */ - bool isNotEntailed() const; - - /** - * Return true if query was a checkEntailed() () query and CVC4 was not able - * to determine if it is entailed. - */ - bool isEntailmentUnknown() const; - - /** - * Operator overloading for equality of two results. - * @param r the result to compare to for equality - * @return true if the results are equal - */ - bool operator==(const Result& r) const; - - /** - * Operator overloading for disequality of two results. - * @param r the result to compare to for disequality - * @return true if the results are disequal - */ - bool operator!=(const Result& r) const; - - /** - * @return an explanation for an unknown query result. - */ - UnknownExplanation getUnknownExplanation() const; - - /** - * @return a string representation of this result. - */ - std::string toString() const; - - private: - /** - * Constructor. - * @param r the internal result that is to be wrapped by this result - * @return the Result - */ - Result(const cvc5::Result& r); - - /** - * 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. - */ - std::shared_ptr<cvc5::Result> d_result; -}; - -/** - * Serialize a Result to given stream. - * @param out the output stream - * @param r the result to be serialized to the given output stream - * @return the output stream - */ -std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_EXPORT; - -/** - * Serialize an UnknownExplanation to given stream. - * @param out the output stream - * @param r the explanation to be serialized to the given output stream - * @return the output stream - */ -std::ostream& operator<<(std::ostream& out, - enum Result::UnknownExplanation e) CVC4_EXPORT; - -/* -------------------------------------------------------------------------- */ -/* Sort */ -/* -------------------------------------------------------------------------- */ - -class Datatype; - -/** - * The sort of a CVC4 term. - */ -class CVC4_EXPORT Sort -{ - friend class cvc5::Command; - friend class DatatypeConstructor; - friend class DatatypeConstructorDecl; - friend class DatatypeSelector; - friend class DatatypeDecl; - friend class Op; - friend class Solver; - friend class Grammar; - friend struct SortHashFunction; - friend class Term; - - public: - /** - * Constructor. - */ - Sort(); - - /** - * Destructor. - */ - ~Sort(); - - /** - * Comparison for structural equality. - * @param s the sort to compare to - * @return true if the sorts are equal - */ - bool operator==(const Sort& s) const; - - /** - * Comparison for structural disequality. - * @param s the sort to compare to - * @return true if the sorts are not equal - */ - bool operator!=(const Sort& s) const; - - /** - * Comparison for ordering on sorts. - * @param s the sort to compare to - * @return true if this sort is less than s - */ - bool operator<(const Sort& s) const; - - /** - * Comparison for ordering on sorts. - * @param s the sort to compare to - * @return true if this sort is greater than s - */ - bool operator>(const Sort& s) const; - - /** - * Comparison for ordering on sorts. - * @param s the sort to compare to - * @return true if this sort is less than or equal to s - */ - bool operator<=(const Sort& s) const; - - /** - * Comparison for ordering on sorts. - * @param s the sort to compare to - * @return true if this sort is greater than or equal to s - */ - bool operator>=(const Sort& s) const; - - /** - * @return true if this Sort is a null sort. - */ - bool isNull() const; - - /** - * Is this a Boolean sort? - * @return true if the sort is a Boolean sort - */ - bool isBoolean() const; - - /** - * Is this a integer sort? - * @return true if the sort is a integer sort - */ - bool isInteger() const; - - /** - * Is this a real sort? - * @return true if the sort is a real sort - */ - bool isReal() const; - - /** - * Is this a string sort? - * @return true if the sort is the string sort - */ - bool isString() const; - - /** - * Is this a regexp sort? - * @return true if the sort is the regexp sort - */ - bool isRegExp() const; - - /** - * Is this a rounding mode sort? - * @return true if the sort is the rounding mode sort - */ - bool isRoundingMode() const; - - /** - * Is this a bit-vector sort? - * @return true if the sort is a bit-vector sort - */ - bool isBitVector() const; - - /** - * Is this a floating-point sort? - * @return true if the sort is a floating-point sort - */ - bool isFloatingPoint() const; - - /** - * Is this a datatype sort? - * @return true if the sort is a datatype sort - */ - bool isDatatype() const; - - /** - * Is this a parametric datatype sort? - * @return true if the sort is a parametric datatype sort - */ - bool isParametricDatatype() const; - - /** - * Is this a constructor sort? - * @return true if the sort is a constructor sort - */ - bool isConstructor() const; - - /** - * Is this a selector sort? - * @return true if the sort is a selector sort - */ - bool isSelector() const; - - /** - * Is this a tester sort? - * @return true if the sort is a tester sort - */ - bool isTester() const; - /** - * Is this a function sort? - * @return true if the sort is a function sort - */ - bool isFunction() const; - - /** - * Is this a predicate sort? - * That is, is this a function sort mapping to Boolean? All predicate - * sorts are also function sorts. - * @return true if the sort is a predicate sort - */ - bool isPredicate() const; - - /** - * Is this a tuple sort? - * @return true if the sort is a tuple sort - */ - bool isTuple() const; - - /** - * Is this a record sort? - * @return true if the sort is a record sort - */ - bool isRecord() const; - - /** - * Is this an array sort? - * @return true if the sort is a array sort - */ - bool isArray() const; - - /** - * Is this a Set sort? - * @return true if the sort is a Set sort - */ - bool isSet() const; - - /** - * Is this a Bag sort? - * @return true if the sort is a Bag sort - */ - bool isBag() const; - - /** - * Is this a Sequence sort? - * @return true if the sort is a Sequence sort - */ - bool isSequence() const; - - /** - * Is this a sort kind? - * @return true if this is a sort kind - */ - bool isUninterpretedSort() const; - - /** - * Is this a sort constructor kind? - * @return true if this is a sort constructor kind - */ - bool isSortConstructor() 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). - * - * Examples of sorts that are not first-class include sort constructor sorts - * and regular expression sorts. - * - * @return true if this is a first-class sort - */ - bool isFirstClass() const; - - /** - * Is this a function-LIKE sort? - * - * Anything function-like except arrays (e.g., datatype selectors) is - * considered a function here. Function-like terms can not be the argument - * 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. - * - * @return true if this is a function-like sort - */ - bool isFunctionLike() const; - - /** - * Is this sort a subsort of the given sort? - * @return true if this sort is a subsort of s - */ - bool isSubsortOf(const Sort& s) const; - - /** - * Is this sort comparable to the given sort (i.e., do they share - * a common ancestor in the subsort tree)? - * @return true if this sort is comparable to s - */ - bool isComparableTo(const Sort& s) const; - - /** - * @return the underlying datatype of a datatype sort - */ - Datatype getDatatype() const; - - /** - * Instantiate a parameterized datatype/sort sort. - * Create sorts parameter with Solver::mkParamSort(). - * @param params the list of sort parameters to instantiate with - */ - Sort instantiate(const std::vector<Sort>& params) const; - - /** - * Substitution of Sorts. - * @param sort the subsort to be substituted within this sort. - * @param replacement the sort replacing the substituted subsort. - */ - Sort substitute(const Sort& sort, const Sort& replacement) const; - - /** - * Simultaneous substitution of Sorts. - * @param sorts the subsorts to be substituted within this sort. - * @param replacements the sort replacing the substituted subsorts. - */ - Sort substitute(const std::vector<Sort>& sorts, - const std::vector<Sort>& replacements) const; - - /** - * Output a string representation of this sort to a given stream. - * @param out the output stream - */ - void toStream(std::ostream& out) const; - - /** - * @return a string representation of this sort - */ - std::string toString() const; - - /* Constructor sort ------------------------------------------------------- */ - - /** - * @return the arity of a constructor sort - */ - size_t getConstructorArity() const; - - /** - * @return the domain sorts of a constructor sort - */ - std::vector<Sort> getConstructorDomainSorts() const; - - /** - * @return the codomain sort of a constructor sort - */ - Sort getConstructorCodomainSort() const; - - /* Selector sort ------------------------------------------------------- */ - - /** - * @return the domain sort of a selector sort - */ - Sort getSelectorDomainSort() const; - - /** - * @return the codomain sort of a selector sort - */ - Sort getSelectorCodomainSort() const; - - /* Tester sort ------------------------------------------------------- */ - - /** - * @return the domain sort of a tester sort - */ - Sort getTesterDomainSort() const; - - /** - * @return the codomain sort of a tester sort, which is the Boolean sort - */ - Sort getTesterCodomainSort() const; - - /* Function sort ------------------------------------------------------- */ - - /** - * @return the arity of a function sort - */ - size_t getFunctionArity() const; - - /** - * @return the domain sorts of a function sort - */ - std::vector<Sort> getFunctionDomainSorts() const; - - /** - * @return the codomain sort of a function sort - */ - Sort getFunctionCodomainSort() const; - - /* Array sort ---------------------------------------------------------- */ - - /** - * @return the array index sort of an array sort - */ - Sort getArrayIndexSort() const; - - /** - * @return the array element sort of an array element sort - */ - Sort getArrayElementSort() const; - - /* Set sort ------------------------------------------------------------ */ - - /** - * @return the element sort of a set sort - */ - Sort getSetElementSort() const; - - /* Bag sort ------------------------------------------------------------ */ - - /** - * @return the element sort of a bag sort - */ - Sort getBagElementSort() const; - - /* Sequence sort ------------------------------------------------------- */ - - /** - * @return the element sort of a sequence sort - */ - Sort getSequenceElementSort() const; - - /* Uninterpreted sort -------------------------------------------------- */ - - /** - * @return the name of an uninterpreted sort - */ - std::string getUninterpretedSortName() const; - - /** - * @return true if an uninterpreted sort is parameterezied - */ - bool isUninterpretedSortParameterized() const; - - /** - * @return the parameter sorts of an uninterpreted sort - */ - std::vector<Sort> getUninterpretedSortParamSorts() const; - - /* Sort constructor sort ----------------------------------------------- */ - - /** - * @return the name of a sort constructor sort - */ - std::string getSortConstructorName() const; - - /** - * @return the arity of a sort constructor sort - */ - size_t getSortConstructorArity() const; - - /* Bit-vector sort ----------------------------------------------------- */ - - /** - * @return the bit-width of the bit-vector sort - */ - uint32_t getBVSize() const; - - /* Floating-point sort ------------------------------------------------- */ - - /** - * @return the bit-width of the exponent of the floating-point sort - */ - uint32_t getFPExponentSize() const; - - /** - * @return the width of the significand of the floating-point sort - */ - uint32_t getFPSignificandSize() const; - - /* Datatype sort ------------------------------------------------------- */ - - /** - * @return the parameter sorts of a datatype sort - */ - std::vector<Sort> getDatatypeParamSorts() const; - - /** - * @return the arity of a datatype sort - */ - size_t getDatatypeArity() const; - - /* Tuple sort ---------------------------------------------------------- */ - - /** - * @return the length of a tuple sort - */ - size_t getTupleLength() const; - - /** - * @return the element sorts of a tuple sort - */ - std::vector<Sort> getTupleSorts() const; - - private: - /** @return the internal wrapped TypeNode of this sort. */ - const cvc5::TypeNode& getTypeNode(void) const; - - /** Helper to convert a set of Sorts to internal TypeNodes. */ - std::set<TypeNode> static sortSetToTypeNodes(const std::set<Sort>& sorts); - /** Helper to convert a vector of Sorts to internal TypeNodes. */ - std::vector<TypeNode> static sortVectorToTypeNodes( - const std::vector<Sort>& sorts); - /** Helper to convert a vector of internal TypeNodes to Sorts. */ - std::vector<Sort> static typeNodeVectorToSorts( - const Solver* slv, const std::vector<TypeNode>& types); - - /** - * Constructor. - * @param slv the associated solver object - * @param t the internal type that is to be wrapped by this sort - * @return the Sort - */ - Sort(const Solver* slv, const cvc5::TypeNode& t); - - /** - * Helper for isNull checks. This prevents calling an API function with - * CVC4_API_CHECK_NOT_NULL - */ - bool isNullHelper() const; - - /** - * The associated solver object. - */ - 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). - */ - std::shared_ptr<cvc5::TypeNode> d_type; -}; - -/** - * Serialize a sort to given stream. - * @param out the output stream - * @param s the sort to be serialized to the given output stream - * @return the output stream - */ -std::ostream& operator<<(std::ostream& out, const Sort& s) CVC4_EXPORT; - -/** - * Hash function for Sorts. - */ -struct CVC4_EXPORT SortHashFunction -{ - size_t operator()(const Sort& s) const; -}; - -/* -------------------------------------------------------------------------- */ -/* Op */ -/* -------------------------------------------------------------------------- */ - -/** - * A CVC4 operator. - * An operator is a term that represents certain operators, instantiated - * with its required parameters, e.g., a term of kind BITVECTOR_EXTRACT. - */ -class CVC4_EXPORT Op -{ - friend class Solver; - friend class Term; - friend struct OpHashFunction; - - public: - /** - * Constructor. - */ - Op(); - - /** - * Destructor. - */ - ~Op(); - - /** - * Syntactic equality operator. - * Return true if both operators are syntactically identical. - * Both operators must belong to the same solver object. - * @param t the operator to compare to for equality - * @return true if the operators are equal - */ - bool operator==(const Op& t) const; - - /** - * Syntactic disequality operator. - * Return true if both operators differ syntactically. - * Both terms must belong to the same solver object. - * @param t the operator to compare to for disequality - * @return true if operators are disequal - */ - bool operator!=(const Op& t) const; - - /** - * @return the kind of this operator - */ - Kind getKind() const; - - /** - * @return true if this operator is a null term - */ - bool isNull() const; - - /** - * @return true iff this operator is indexed - */ - bool isIndexed() const; - - /** - * Get the indices used to create this Op. - * Supports the following template arguments: - * - string - * - Kind - * - uint32_t - * - pair<uint32_t, uint32_t> - * Check the Op Kind with getKind() to determine which argument to use. - * @return the indices used to create this Op - */ - template <typename T> - T getIndices() const; - - /** - * @return a string representation of this operator - */ - std::string toString() const; - - private: - /** - * Constructor for a single kind (non-indexed operator). - * @param slv the associated solver object - * @param k the kind of this Op - */ - Op(const Solver* slv, const Kind k); - - /** - * Constructor. - * @param slv the associated solver object - * @param k the kind of this Op - * @param n the internal node that is to be wrapped by this term - * @return the Term - */ - Op(const Solver* slv, const Kind k, const cvc5::Node& n); - - /** - * Helper for isNull checks. This prevents calling an API function with - * CVC4_API_CHECK_NOT_NULL - */ - 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) - * @return true iff this Op is indexed - */ - bool isIndexedHelper() const; - - /** - * The associated solver object. - */ - const Solver* d_solver; - - /** The kind of this operator. */ - Kind d_kind; - - /** - * 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). - */ - std::shared_ptr<cvc5::Node> d_node; -}; - -/* -------------------------------------------------------------------------- */ -/* Term */ -/* -------------------------------------------------------------------------- */ - -/** - * A CVC4 Term. - */ -class CVC4_EXPORT Term -{ - friend class cvc5::Command; - friend class Datatype; - friend class DatatypeConstructor; - friend class DatatypeSelector; - friend class Solver; - friend class Grammar; - friend struct TermHashFunction; - - public: - /** - * Constructor. - */ - Term(); - - /** - * Destructor. - */ - ~Term(); - - /** - * Syntactic equality operator. - * Return true if both terms are syntactically identical. - * Both terms must belong to the same solver object. - * @param t the term to compare to for equality - * @return true if the terms are equal - */ - bool operator==(const Term& t) const; - - /** - * Syntactic disequality operator. - * Return true if both terms differ syntactically. - * Both terms must belong to the same solver object. - * @param t the term to compare to for disequality - * @return true if terms are disequal - */ - bool operator!=(const Term& t) const; - - /** - * Comparison for ordering on terms. - * @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. - * @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. - * @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. - * @param t the term to compare to - * @return true if this term is greater than or equal to t - */ - bool operator>=(const Term& t) const; - - /** @return the number of children of this term */ - size_t getNumChildren() const; - - /** - * Get the child term at a given index. - * @param index the index of the child term to return - * @return the child term with the given index - */ - Term operator[](size_t index) const; - - /** - * @return the id of this term - */ - uint64_t getId() const; - - /** - * @return the kind of this term - */ - Kind getKind() const; - - /** - * @return the sort of this term - */ - Sort getSort() const; - - /** - * @return the result of replacing 'term' by 'replacement' in this term - */ - Term substitute(const Term& term, const Term& replacement) const; - - /** - * @return the result of simulatenously replacing 'terms' by 'replacements' - * in this term - */ - Term substitute(const std::vector<Term>& terms, - const std::vector<Term>& replacements) const; - - /** - * @return true iff this term has an operator - */ - bool hasOp() const; - - /** - * @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 - */ - bool isNull() 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 - */ - Term getConstArrayBase() 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. - */ - std::vector<Term> getConstSequenceElements() const; - - /** - * Boolean negation. - * @return the Boolean negation of this term - */ - Term notTerm() const; - - /** - * Boolean and. - * @param t a Boolean term - * @return the conjunction of this term and the given term - */ - Term andTerm(const Term& t) const; - - /** - * Boolean or. - * @param t a Boolean term - * @return the disjunction of this term and the given term - */ - Term orTerm(const Term& t) const; - - /** - * Boolean exclusive or. - * @param t a Boolean term - * @return the exclusive disjunction of this term and the given term - */ - Term xorTerm(const Term& t) const; - - /** - * Equality. - * @param t a Boolean term - * @return the Boolean equivalence of this term and the given term - */ - Term eqTerm(const Term& t) const; - - /** - * Boolean implication. - * @param t a Boolean term - * @return the implication of this term and the given term - */ - Term impTerm(const Term& t) const; - - /** - * If-then-else with this term as the Boolean condition. - * @param then_t the 'then' term - * @param else_t the 'else' term - * @return the if-then-else term with this term as the Boolean condition - */ - Term iteTerm(const Term& then_t, const Term& else_t) const; - - /** - * @return a string representation of this term - */ - std::string toString() const; - - /** - * 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 - */ - class const_iterator : public std::iterator<std::input_iterator_tag, Term> - { - friend class Term; - - public: - /** - * Null Constructor. - */ - const_iterator(); - - /** - * Constructor - * @param slv the associated solver object - * @param e a 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 std::shared_ptr<cvc5::Node>& e, - uint32_t p); - - /** - * Copy constructor. - */ - const_iterator(const const_iterator& it); - - /** - * Assignment operator. - * @param it the iterator to assign to - * @return the reference to the iterator after assignment - */ - const_iterator& operator=(const const_iterator& it); - - /** - * Equality operator. - * @param it the iterator to compare to for equality - * @return true if the iterators are equal - */ - bool operator==(const const_iterator& it) const; - - /** - * Disequality operator. - * @param it the iterator to compare to for disequality - * @return true if the iterators are disequal - */ - bool operator!=(const const_iterator& it) const; - - /** - * Increment operator (prefix). - * @return a reference to the iterator after incrementing by one - */ - const_iterator& operator++(); - - /** - * Increment operator (postfix). - * @return a reference to the iterator after incrementing by one - */ - const_iterator operator++(int); - - /** - * Dereference operator. - * @return the term this iterator points to - */ - Term operator*() const; - - private: - /** - * The associated solver object. - */ - const Solver* d_solver; - /** The original node to be iterated over. */ - std::shared_ptr<cvc5::Node> d_origNode; - /** Keeps track of the iteration position. */ - uint32_t d_pos; - }; - - /** - * @return an iterator to the first child of this Term - */ - const_iterator begin() const; - - /** - * @return an iterator to one-off-the-last child of this Term - */ - const_iterator end() const; - - /** - * @return true if the term is an integer that fits within std::int32_t. - */ - bool isInt32() const; - /** - * @return the stored integer as a std::int32_t. - * Note: Asserts isInt32(). - */ - std::int32_t getInt32() const; - /** - * @return true if the term is an integer that fits within std::uint32_t. - */ - bool isUInt32() const; - /** - * @return the stored integer as a std::uint32_t. - * Note: Asserts isUInt32(). - */ - std::uint32_t getUInt32() const; - /** - * @return true if the term is an integer that fits within std::int64_t. - */ - bool isInt64() const; - /** - * @return the stored integer as a std::int64_t. - * Note: Asserts isInt64(). - */ - std::int64_t getInt64() const; - /** - * @return true if the term is an integer that fits within std::uint64_t. - */ - bool isUInt64() const; - /** - * @return the stored integer as a std::uint64_t. - * Note: Asserts isUInt64(). - */ - std::uint64_t getUInt64() const; - /** - * @return true if the term is an integer. - */ - bool isInteger() const; - /** - * @return the stored integer in (decimal) string representation. - * Note: Asserts isInteger(). - */ - std::string getInteger() const; - - /** - * @return true if the term is a string constant. - */ - bool isString() const; - /** - * @return the stored string constant. - * - * 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(). - */ - std::wstring getString() const; - - protected: - /** - * The associated solver object. - */ - const Solver* d_solver; - - private: - /** Helper to convert a vector of Terms to internal Nodes. */ - std::vector<Node> static termVectorToNodes(const std::vector<Term>& terms); - - /** - * Constructor. - * @param slv the associated solver object - * @param n the internal node that is to be wrapped by this term - * @return the Term - */ - Term(const Solver* slv, const cvc5::Node& n); - - /** @return the internal wrapped Node of this term. */ - const cvc5::Node& getNode(void) const; - - /** - * Helper for isNull checks. This prevents calling an API function with - * CVC4_API_CHECK_NOT_NULL - */ - bool isNullHelper() const; - - /** - * Helper function that returns the kind of the term, which takes into - * account special cases of the conversion for internal to external kinds. - * @return the kind of this term - */ - Kind getKindHelper() const; - - /** - * @return true if the current term is a constant integer that is casted into - * real using the operator CAST_TO_REAL, and returns false otherwise - */ - 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). - */ - std::shared_ptr<cvc5::Node> d_node; -}; - -/** - * Hash function for Terms. - */ -struct CVC4_EXPORT TermHashFunction -{ - size_t operator()(const Term& t) const; -}; - -/** - * Serialize a term to given stream. - * @param out the output stream - * @param t the term to be serialized to the given output stream - * @return the output stream - */ -std::ostream& operator<<(std::ostream& out, const Term& t) CVC4_EXPORT; - -/** - * Serialize a vector of terms to given stream. - * @param out the output stream - * @param vector the vector of terms to be serialized to the given stream - * @return the output stream - */ -std::ostream& operator<<(std::ostream& out, - const std::vector<Term>& vector) CVC4_EXPORT; - -/** - * Serialize a set of terms to the given stream. - * @param out the output stream - * @param set the set of terms to be serialized to the given stream - * @return the output stream - */ -std::ostream& operator<<(std::ostream& out, - const std::set<Term>& set) CVC4_EXPORT; - -/** - * Serialize an unordered_set of terms to the given stream. - * - * @param out the output stream - * @param unordered_set the set of terms to be serialized to the given stream - * @return the output stream - */ -std::ostream& operator<<(std::ostream& out, - const std::unordered_set<Term, TermHashFunction>& - unordered_set) CVC4_EXPORT; - -/** - * Serialize a map of terms to the given stream. - * - * @param out the output stream - * @param map the map of terms to be serialized to the given stream - * @return the output stream - */ -template <typename V> -std::ostream& operator<<(std::ostream& out, - const std::map<Term, V>& map) CVC4_EXPORT; - -/** - * Serialize an unordered_map of terms to the given stream. - * - * @param out the output stream - * @param unordered_map the map of terms to be serialized to the given stream - * @return the output stream - */ -template <typename V> -std::ostream& operator<<(std::ostream& out, - const std::unordered_map<Term, V, TermHashFunction>& - unordered_map) CVC4_EXPORT; - -/** - * Serialize an operator to given stream. - * @param out the output stream - * @param t the operator to be serialized to the given output stream - * @return the output stream - */ -std::ostream& operator<<(std::ostream& out, const Op& t) CVC4_EXPORT; - -/** - * Hash function for Ops. - */ -struct CVC4_EXPORT OpHashFunction -{ - size_t operator()(const Op& t) const; -}; - -/* -------------------------------------------------------------------------- */ -/* Datatypes */ -/* -------------------------------------------------------------------------- */ - -class DatatypeConstructorIterator; -class DatatypeIterator; - -/** - * A CVC4 datatype constructor declaration. - */ -class CVC4_EXPORT DatatypeConstructorDecl -{ - friend class DatatypeDecl; - friend class Solver; - - public: - /** Constructor. */ - DatatypeConstructorDecl(); - - /** - * Destructor. - */ - ~DatatypeConstructorDecl(); - - /** - * 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 - */ - void addSelector(const std::string& name, const Sort& sort); - /** - * Add datatype selector declaration whose range type is the datatype itself. - * @param name the name of the datatype selector declaration to add - */ - void addSelectorSelf(const std::string& name); - - /** - * @return true if this DatatypeConstructorDecl is a null declaration. - */ - bool isNull() const; - - /** - * @return a string representation of this datatype constructor declaration - */ - std::string toString() const; - - private: - /** - * Constructor. - * @param slv the associated solver object - * @param name the name of the datatype constructor - * @return the DatatypeConstructorDecl - */ - DatatypeConstructorDecl(const Solver* slv, const std::string& name); - - /** - * Helper for isNull checks. This prevents calling an API function with - * CVC4_API_CHECK_NOT_NULL - */ - bool isNullHelper() const; - - /** - * The associated solver object. - */ - const Solver* d_solver; - - /** - * 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. - */ - std::shared_ptr<cvc5::DTypeConstructor> d_ctor; -}; - -class Solver; - -/** - * A CVC4 datatype declaration. - */ -class CVC4_EXPORT DatatypeDecl -{ - friend class DatatypeConstructorArg; - friend class Solver; - friend class Grammar; - - public: - /** Constructor. */ - DatatypeDecl(); - - /** - * Destructor. - */ - ~DatatypeDecl(); - - /** - * Add datatype constructor declaration. - * @param ctor the datatype constructor declaration to add - */ - void addConstructor(const DatatypeConstructorDecl& ctor); - - /** Get the number of constructors (so far) for this Datatype declaration. */ - size_t getNumConstructors() const; - - /** Is this Datatype declaration parametric? */ - bool isParametric() const; - - /** - * @return true if this DatatypeDecl is a null object - */ - bool isNull() const; - - /** - * @return a string representation of this datatype declaration - */ - std::string toString() const; - - /** @return the name of this datatype declaration. */ - std::string getName() const; - - private: - /** - * Constructor. - * @param slv the associated solver object - * @param name the name of the datatype - * @param isCoDatatype true if a codatatype is to be constructed - * @return the DatatypeDecl - */ - DatatypeDecl(const Solver* slv, - const std::string& name, - bool isCoDatatype = false); - - /** - * Constructor for parameterized datatype declaration. - * Create sorts parameter with Solver::mkParamSort(). - * @param slv the associated solver object - * @param name the name of the datatype - * @param param the sort parameter - * @param isCoDatatype true if a codatatype is to be constructed - */ - DatatypeDecl(const Solver* slv, - const std::string& name, - const Sort& param, - bool isCoDatatype = false); - - /** - * Constructor for parameterized datatype declaration. - * Create sorts parameter with Solver::mkParamSort(). - * @param slv the associated solver object - * @param name the name of the datatype - * @param params a list of sort parameters - * @param isCoDatatype true if a codatatype is to be constructed - */ - DatatypeDecl(const Solver* slv, - const std::string& name, - const std::vector<Sort>& params, - bool isCoDatatype = false); - - /** @return the internal wrapped Dtype of this datatype declaration. */ - cvc5::DType& getDatatype(void) const; - - /** - * Helper for isNull checks. This prevents calling an API function with - * CVC4_API_CHECK_NOT_NULL - */ - bool isNullHelper() const; - - /** - * The associated solver object. - */ - const Solver* d_solver; - - /** - * 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. - */ - std::shared_ptr<cvc5::DType> d_dtype; -}; - -/** - * A CVC4 datatype selector. - */ -class CVC4_EXPORT DatatypeSelector -{ - friend class DatatypeConstructor; - friend class Solver; - - public: - /** - * Constructor. - */ - DatatypeSelector(); - - /** - * Destructor. - */ - ~DatatypeSelector(); - - /** @return the name of this Datatype selector. */ - std::string getName() const; - - /** - * Get the selector operator of this datatype selector. - * @return the selector term - */ - Term getSelectorTerm() const; - - /** @return the range sort of this argument. */ - Sort getRangeSort() const; - - /** - * @return true if this DatatypeSelector is a null object - */ - bool isNull() const; - - /** - * @return a string representation of this datatype selector - */ - std::string toString() const; - - private: - /** - * Constructor. - * @param slv the associated solver object - * @param stor the internal datatype selector to be wrapped - * @return the DatatypeSelector - */ - DatatypeSelector(const Solver* slv, const cvc5::DTypeSelector& stor); - - /** - * Helper for isNull checks. This prevents calling an API function with - * CVC4_API_CHECK_NOT_NULL - */ - bool isNullHelper() const; - - /** - * The associated solver object. - */ - const Solver* d_solver; - - /** - * 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. - */ - std::shared_ptr<cvc5::DTypeSelector> d_stor; -}; - -/** - * A CVC4 datatype constructor. - */ -class CVC4_EXPORT DatatypeConstructor -{ - friend class Datatype; - friend class Solver; - - public: - /** - * Constructor. - */ - DatatypeConstructor(); - - /** - * Destructor. - */ - ~DatatypeConstructor(); - - /** @return the name of this Datatype constructor. */ - std::string getName() const; - - /** - * Get the constructor operator of this datatype constructor. - * @return the constructor term - */ - Term getConstructorTerm() const; - - /** - * Get the constructor operator of this datatype constructor whose return - * type is retSort. This method is intended to be used on constructors of - * parametric datatypes and can be seen as returning the constructor - * term that has been explicitly cast to the given sort. - * - * 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)))))) - * 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)) - * This method is equivalent of applying the above, where this - * DatatypeConstructor is the one corresponding to nil, and retSort is - * (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. - * - * @param retSort the desired return sort of the constructor - * @return the constructor term - */ - Term getSpecializedConstructorTerm(const Sort& retSort) const; - - /** - * Get the tester operator of this datatype constructor. - * @return the tester operator - */ - Term getTesterTerm() const; - - /** - * @return the number of selectors (so far) of this Datatype constructor. - */ - size_t getNumSelectors() const; - - /** @return the i^th DatatypeSelector. */ - DatatypeSelector operator[](size_t index) const; - /** - * Get the datatype selector with the given name. - * This is a linear search through the selectors, so in case of - * multiple, similarly-named selectors, the first is returned. - * @param name the name of the datatype selector - * @return the first datatype selector with the given name - */ - DatatypeSelector operator[](const std::string& name) const; - DatatypeSelector getSelector(const std::string& name) const; - - /** - * Get the term representation of the datatype selector with the given name. - * This is a linear search through the arguments, so in case of multiple, - * similarly-named arguments, the selector for the first is returned. - * @param name the name of the datatype selector - * @return a term representing the datatype selector with the given name - */ - Term getSelectorTerm(const std::string& name) const; - - /** - * @return true if this DatatypeConstructor is a null object - */ - bool isNull() const; - - /** - * @return a string representation of this datatype constructor - */ - std::string toString() const; - - /** - * 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: - /** Nullary constructor (required for Cython). */ - const_iterator(); - - /** - * Assignment operator. - * @param it the iterator to assign to - * @return the reference to the iterator after assignment - */ - const_iterator& operator=(const const_iterator& it); - - /** - * Equality operator. - * @param it the iterator to compare to for equality - * @return true if the iterators are equal - */ - bool operator==(const const_iterator& it) const; - - /** - * Disequality operator. - * @param it the iterator to compare to for disequality - * @return true if the iterators are disequal - */ - bool operator!=(const const_iterator& it) const; - - /** - * Increment operator (prefix). - * @return a reference to the iterator after incrementing by one - */ - const_iterator& operator++(); - - /** - * Increment operator (postfix). - * @return a reference to the iterator after incrementing by one - */ - const_iterator operator++(int); - - /** - * Dereference operator. - * @return a reference to the selector this iterator points to - */ - const DatatypeSelector& operator*() const; - - /** - * Dereference operator. - * @return a pointer to the selector this iterator points to - */ - const DatatypeSelector* operator->() const; - - private: - /** - * Constructor. - * @param slv the associated Solver object - * @param ctor the internal datatype constructor to iterate over - * @param true if this is a begin() iterator - */ - const_iterator(const Solver* slv, - const cvc5::DTypeConstructor& ctor, - bool begin); - - /** - * The associated solver object. - */ - const Solver* d_solver; - - /** - * A pointer to the list of selectors of the internal datatype - * constructor to iterate over. - * This pointer is maintained for operators == and != only. - */ - const void* d_int_stors; - - /** The list of datatype selector (wrappers) to iterate over. */ - std::vector<DatatypeSelector> d_stors; - - /** The current index of the iterator. */ - size_t d_idx; - }; - - /** - * @return an iterator to the first selector of this constructor - */ - const_iterator begin() const; - - /** - * @return an iterator to one-off-the-last selector of this constructor - */ - const_iterator end() const; - - private: - /** - * Constructor. - * @param ctor the internal datatype constructor to be wrapped - * @return the DatatypeConstructor - */ - DatatypeConstructor(const Solver* slv, const cvc5::DTypeConstructor& ctor); - - /** - * 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 - * CVC4_API_CHECK_NOT_NULL - */ - bool isNullHelper() const; - - /** - * The associated solver object. - */ - const Solver* d_solver; - - /** - * 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. - */ - std::shared_ptr<cvc5::DTypeConstructor> d_ctor; -}; - -/* - * A CVC4 datatype. - */ -class CVC4_EXPORT Datatype -{ - friend class Solver; - friend class Sort; - - public: - /** Constructor. */ - Datatype(); - - /** - * Destructor. - */ - ~Datatype(); - - /** - * Get the datatype constructor at a given index. - * @param idx the index of the datatype constructor to return - * @return the datatype constructor with the given index - */ - DatatypeConstructor operator[](size_t idx) const; - - /** - * Get the datatype constructor with the given name. - * This is a linear search through the constructors, so in case of multiple, - * similarly-named constructors, the first is returned. - * @param name the name of the datatype constructor - * @return the datatype constructor with the given name - */ - DatatypeConstructor operator[](const std::string& name) const; - DatatypeConstructor getConstructor(const std::string& name) const; - - /** - * Get a term representing the datatype constructor with the given name. - * This is a linear search through the constructors, so in case of multiple, - * similarly-named constructors, the - * first is returned. - */ - Term getConstructorTerm(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 true if this datatype is parametric */ - bool isParametric() const; - - /** @return true if this datatype corresponds to a co-datatype */ - bool isCodatatype() const; - - /** @return true if this datatype corresponds to a tuple */ - bool isTuple() const; - - /** @return true if this datatype corresponds to a record */ - bool isRecord() const; - - /** @return true if this datatype is finite */ - bool isFinite() const; - - /** - * Is this datatype well-founded? If this datatype is not a codatatype, - * this returns false if there are no values of this datatype that are of - * finite size. - * - * @return true if this datatype is well-founded - */ - bool isWellFounded() 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. - * - * @return true if this datatype has nested recursion - */ - bool hasNestedRecursion() const; - - /** - * @return true if this Datatype is a null object - */ - bool isNull() const; - - /** - * @return a string representation of this datatype - */ - std::string toString() const; - - /** - * Iterator for the constructors of a datatype. - */ - class const_iterator : public std::iterator<std::input_iterator_tag, Datatype> - { - friend class Datatype; // to access constructor - - public: - /** Nullary constructor (required for Cython). */ - const_iterator(); - - /** - * Assignment operator. - * @param it the iterator to assign to - * @return the reference to the iterator after assignment - */ - const_iterator& operator=(const const_iterator& it); - - /** - * Equality operator. - * @param it the iterator to compare to for equality - * @return true if the iterators are equal - */ - bool operator==(const const_iterator& it) const; - - /** - * Disequality operator. - * @param it the iterator to compare to for disequality - * @return true if the iterators are disequal - */ - bool operator!=(const const_iterator& it) const; - - /** - * Increment operator (prefix). - * @return a reference to the iterator after incrementing by one - */ - const_iterator& operator++(); - - /** - * Increment operator (postfix). - * @return a reference to the iterator after incrementing by one - */ - const_iterator operator++(int); - - /** - * Dereference operator. - * @return a reference to the constructor this iterator points to - */ - const DatatypeConstructor& operator*() const; - - /** - * Dereference operator. - * @return a pointer to the constructor this iterator points to - */ - const DatatypeConstructor* operator->() const; - - private: - /** - * Constructor. - * @param slv the associated Solver object - * @param dtype the internal datatype to iterate over - * @param true if this is a begin() iterator - */ - const_iterator(const Solver* slv, const cvc5::DType& dtype, bool begin); - - /** - * The associated solver object. - */ - const Solver* d_solver; - - /** - * A pointer to the list of constructors of the internal datatype - * to iterate over. - * This pointer is maintained for operators == and != only. - */ - const void* d_int_ctors; - - /** The list of datatype constructor (wrappers) to iterate over. */ - std::vector<DatatypeConstructor> d_ctors; - - /** The current index of the iterator. */ - size_t d_idx; - }; - - /** - * @return an iterator to the first constructor of this datatype - */ - const_iterator begin() const; - - /** - * @return an iterator to one-off-the-last constructor of this datatype - */ - const_iterator end() const; - - private: - /** - * Constructor. - * @param dtype the internal datatype to be wrapped - * @return the Datatype - */ - Datatype(const Solver* slv, const cvc5::DType& dtype); - - /** - * Return constructor for name. - * @param name The name of constructor to find - * @return the constructor object for the name - */ - DatatypeConstructor getConstructorForName(const std::string& name) const; - - /** - * Helper for isNull checks. This prevents calling an API function with - * CVC4_API_CHECK_NOT_NULL - */ - bool isNullHelper() const; - - /** - * The associated solver object. - */ - const Solver* d_solver; - - /** - * 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. - */ - std::shared_ptr<cvc5::DType> d_dtype; -}; - -/** - * Serialize a datatype declaration to given stream. - * @param out the output stream - * @param dtdecl the datatype declaration to be serialized to the given stream - * @return the output stream - */ -std::ostream& operator<<(std::ostream& out, - const DatatypeDecl& dtdecl) CVC4_EXPORT; - -/** - * Serialize a datatype constructor declaration to given stream. - * @param out the output stream - * @param ctordecl the datatype constructor declaration to be serialized - * @return the output stream - */ -std::ostream& operator<<(std::ostream& out, - const DatatypeConstructorDecl& ctordecl) CVC4_EXPORT; - -/** - * Serialize a vector of datatype constructor declarations to given stream. - * @param out the output stream - * @param vector the vector of datatype constructor declarations to be - * serialized to the given stream - * @return the output stream - */ -std::ostream& operator<<(std::ostream& out, - const std::vector<DatatypeConstructorDecl>& vector); - -/** - * Serialize a datatype to given stream. - * @param out the output stream - * @param dtdecl the datatype to be serialized to given stream - * @return the output stream - */ -std::ostream& operator<<(std::ostream& out, const Datatype& dtype) CVC4_EXPORT; - -/** - * Serialize a datatype constructor to given stream. - * @param out the output stream - * @param ctor the datatype constructor to be serialized to given stream - * @return the output stream - */ -std::ostream& operator<<(std::ostream& out, - const DatatypeConstructor& ctor) CVC4_EXPORT; - -/** - * Serialize a datatype selector to given stream. - * @param out the output stream - * @param ctor the datatype selector to be serialized to given stream - * @return the output stream - */ -std::ostream& operator<<(std::ostream& out, - const DatatypeSelector& stor) CVC4_EXPORT; - -/* -------------------------------------------------------------------------- */ -/* Grammar */ -/* -------------------------------------------------------------------------- */ - -/** - * A Sygus Grammar. - */ -class CVC4_EXPORT Grammar -{ - friend class cvc5::Command; - friend class Solver; - - public: - /** - * Add <rule> to the set of rules corresponding to <ntSymbol>. - * @param ntSymbol the non-terminal to which the rule is added - * @param rule the rule to add - */ - void addRule(const Term& ntSymbol, const Term& rule); - - /** - * Add <rules> to the set of rules corresponding to <ntSymbol>. - * @param ntSymbol the non-terminal to which the rules are added - * @param rule the rules to add - */ - void addRules(const Term& ntSymbol, const std::vector<Term>& rules); - - /** - * Allow <ntSymbol> to be an arbitrary constant. - * @param ntSymbol the non-terminal allowed to be any constant - */ - void addAnyConstant(const Term& ntSymbol); - - /** - * Allow <ntSymbol> to be any input variable to corresponding - * synth-fun/synth-inv with the same sort as <ntSymbol>. - * @param ntSymbol the non-terminal allowed to be any input constant - */ - void addAnyVariable(const Term& ntSymbol); - - /** - * @return a string representation of this grammar. - */ - std::string toString() const; - - /** - * Nullary constructor. Needed for the Cython API. - */ - Grammar(); - - private: - /** - * Constructor. - * @param slv the solver that created this grammar - * @param sygusVars the input variables to synth-fun/synth-var - * @param ntSymbols the non-terminals of this grammar - */ - Grammar(const Solver* slv, - const std::vector<Term>& sygusVars, - const std::vector<Term>& ntSymbols); - - /** - * @return the resolved datatype of the Start symbol of the grammar - */ - Sort resolve(); - - /** - * Adds a constructor to sygus datatype <dt> whose sygus operator is <term>. - * - * <ntsToUnres> contains a mapping from non-terminal symbols to the - * unresolved sorts they correspond to. This map indicates how the argument - * <term> should be interpreted (instances of symbols from the domain of - * <ntsToUnres> correspond to constructor arguments). - * - * The sygus operator that is actually added to <dt> corresponds to replacing - * each occurrence of non-terminal symbols from the domain of <ntsToUnres> - * with bound variables via purifySygusGTerm, and binding these variables - * via a lambda. - * - * @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 - */ - void addSygusConstructorTerm( - DatatypeDecl& dt, - const Term& term, - const std::unordered_map<Term, Sort, TermHashFunction>& ntsToUnres) const; - - /** - * Purify SyGuS grammar term. - * - * This returns a term where all occurrences of non-terminal symbols (those - * in the domain of <ntsToUnres>) are replaced by fresh variables. For - * each variable replaced in this way, we add the fresh variable it is - * replaced with to <args>, and the unresolved sorts corresponding to the - * non-terminal symbol to <cargs> (constructor args). In other words, <args> - * contains the free variables in the term returned by this method (which - * should be bound by a lambda), and <cargs> contains the sorts of the - * arguments of the sygus constructor. - * - * @param term the term to purify - * @param args the free variables in the term returned by this method - * @param cargs the sorts of the arguments of the sygus constructor - * @param ntsToUnres mapping from non-terminals to their unresolved sorts - * @return the purfied term - */ - Term purifySygusGTerm( - const Term& term, - std::vector<Term>& args, - std::vector<Sort>& cargs, - const std::unordered_map<Term, Sort, TermHashFunction>& ntsToUnres) const; - - /** - * This adds constructors to <dt> for sygus variables in <d_sygusVars> whose - * sort is argument <sort>. This method should be called when the sygus - * grammar term (Variable sort) is encountered. - * - * @param dt the non-terminal's datatype to which the constructors are added - * @param sort the sort of the sygus variables to add - */ - void addSygusConstructorVariables(DatatypeDecl& dt, const Sort& sort) const; - - /** - * Check if <rule> contains variables that are neither parameters of - * the corresponding synthFun/synthInv nor non-terminals. - * @param rule the non-terminal allowed to be any constant - * @return <true> if <rule> contains free variables and <false> otherwise - */ - bool containsFreeVariables(const Term& rule) const; - - /** The solver that created this grammar. */ - const Solver* d_solver; - /** Input variables to the corresponding function/invariant to synthesize.*/ - std::vector<Term> d_sygusVars; - /** The non-terminal symbols of this grammar. */ - std::vector<Term> d_ntSyms; - /** The mapping from non-terminal symbols to their production terms. */ - std::unordered_map<Term, std::vector<Term>, TermHashFunction> d_ntsToTerms; - /** The set of non-terminals that can be arbitrary constants. */ - std::unordered_set<Term, TermHashFunction> d_allowConst; - /** The set of non-terminals that can be sygus variables. */ - std::unordered_set<Term, TermHashFunction> d_allowVars; - /** Did we call resolve() before? */ - bool d_isResolved; -}; - -/** - * Serialize a grammar to given stream. - * @param out the output stream - * @param g the grammar to be serialized to the given output stream - * @return the output stream - */ -std::ostream& operator<<(std::ostream& out, const Grammar& g) CVC4_EXPORT; - -/* -------------------------------------------------------------------------- */ -/* Rounding Mode for Floating Points */ -/* -------------------------------------------------------------------------- */ - -/** - * A CVC4 floating point rounding mode. - */ -enum CVC4_EXPORT RoundingMode -{ - ROUND_NEAREST_TIES_TO_EVEN, - ROUND_TOWARD_POSITIVE, - ROUND_TOWARD_NEGATIVE, - ROUND_TOWARD_ZERO, - ROUND_NEAREST_TIES_TO_AWAY, -}; - -/** - * Hash function for RoundingModes. - */ -struct CVC4_EXPORT RoundingModeHashFunction -{ - inline size_t operator()(const RoundingMode& rm) const; -}; - -/* -------------------------------------------------------------------------- */ -/* Solver */ -/* -------------------------------------------------------------------------- */ - -/* - * A CVC4 solver. - */ -class CVC4_EXPORT Solver -{ - friend class Datatype; - friend class DatatypeDecl; - friend class DatatypeConstructor; - friend class DatatypeConstructorDecl; - friend class DatatypeSelector; - friend class Grammar; - friend class Op; - friend class cvc5::Command; - friend class Sort; - friend class Term; - - public: - /* .................................................................... */ - /* Constructors/Destructors */ - /* .................................................................... */ - - /** - * Constructor. - * @param opts an optional pointer to a solver options object - * @return the Solver - */ - Solver(Options* opts = nullptr); - - /** - * Destructor. - */ - ~Solver(); - - /** - * Disallow copy/assignment. - */ - Solver(const Solver&) = delete; - Solver& operator=(const Solver&) = delete; - - /* .................................................................... */ - /* Solver Configuration */ - /* .................................................................... */ - - bool supportsFloatingPoint() const; - - /* .................................................................... */ - /* Sorts Handling */ - /* .................................................................... */ - - /** - * @return sort null - */ - Sort getNullSort() const; - - /** - * @return sort Boolean - */ - Sort getBooleanSort() const; - - /** - * @return sort Integer (in CVC4, Integer is a subtype of Real) - */ - Sort getIntegerSort() const; - - /** - * @return sort Real - */ - Sort getRealSort() const; - - /** - * @return sort RegExp - */ - Sort getRegExpSort() const; - - /** - * @return sort RoundingMode - */ - Sort getRoundingModeSort() const; - - /** - * @return sort String - */ - Sort getStringSort() const; - - /** - * Create an array sort. - * @param indexSort the array index sort - * @param elemSort the array element sort - * @return the array sort - */ - Sort mkArraySort(const Sort& indexSort, const Sort& elemSort) const; - - /** - * Create a bit-vector sort. - * @param size the bit-width of the bit-vector sort - * @return the bit-vector sort - */ - Sort mkBitVectorSort(uint32_t size) const; - - /** - * Create a floating-point sort. - * @param exp the bit-width of the exponent of the floating-point sort. - * @param sig the bit-width of the significand of the floating-point sort. - */ - Sort mkFloatingPointSort(uint32_t exp, uint32_t sig) const; - - /** - * Create a datatype sort. - * @param dtypedecl the datatype declaration from which the sort is created - * @return the datatype sort - */ - Sort mkDatatypeSort(const DatatypeDecl& dtypedecl) const; - - /** - * Create a vector of datatype sorts. The names of the datatype declarations - * must be distinct. - * - * @param dtypedecls the datatype declarations from which the sort is created - * @return the datatype sorts - */ - std::vector<Sort> mkDatatypeSorts( - const std::vector<DatatypeDecl>& dtypedecls) const; - - /** - * Create a vector of datatype sorts using unresolved sorts. The names of - * the datatype declarations in dtypedecls must be distinct. - * - * 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 - * 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. - * - * @param dtypedecls the datatype declarations from which the sort is created - * @param unresolvedSorts the list of unresolved sorts - * @return the datatype sorts - */ - std::vector<Sort> mkDatatypeSorts( - const std::vector<DatatypeDecl>& dtypedecls, - const std::set<Sort>& unresolvedSorts) const; - - /** - * Create function sort. - * @param domain the sort of the fuction argument - * @param codomain the sort of the function return value - * @return the function sort - */ - Sort mkFunctionSort(const Sort& domain, const Sort& codomain) const; - - /** - * Create function sort. - * @param sorts the sort of the function arguments - * @param codomain the sort of the function return value - * @return the function sort - */ - Sort mkFunctionSort(const std::vector<Sort>& sorts, - const Sort& codomain) const; - - /** - * Create a sort parameter. - * @param symbol the name of the sort - * @return the sort parameter - */ - Sort mkParamSort(const std::string& symbol) const; - - /** - * Create a predicate sort. - * @param sorts the list of sorts of the predicate - * @return the predicate sort - */ - Sort mkPredicateSort(const std::vector<Sort>& sorts) const; - - /** - * Create a record sort - * @param fields the list of fields of the record - * @return the record sort - */ - Sort mkRecordSort( - const std::vector<std::pair<std::string, Sort>>& fields) const; - - /** - * Create a set sort. - * @param elemSort the sort of the set elements - * @return the set sort - */ - Sort mkSetSort(const Sort& elemSort) const; - - /** - * Create a bag sort. - * @param elemSort the sort of the bag elements - * @return the bag sort - */ - Sort mkBagSort(const Sort& elemSort) const; - - /** - * Create a sequence sort. - * @param elemSort the sort of the sequence elements - * @return the sequence sort - */ - Sort mkSequenceSort(const Sort& elemSort) const; - - /** - * Create an uninterpreted sort. - * @param symbol the name of the sort - * @return the uninterpreted sort - */ - Sort mkUninterpretedSort(const std::string& symbol) const; - - /** - * Create a sort constructor sort. - * @param symbol the symbol of the sort - * @param arity the arity of the sort - * @return the sort constructor sort - */ - Sort mkSortConstructorSort(const std::string& symbol, size_t arity) const; - - /** - * Create a tuple sort. - * @param sorts of the elements of the tuple - * @return the tuple sort - */ - Sort mkTupleSort(const std::vector<Sort>& sorts) const; - - /* .................................................................... */ - /* Create Terms */ - /* .................................................................... */ - - /** - * Create 0-ary term of given kind. - * @param kind the kind of the term - * @return the Term - */ - Term mkTerm(Kind kind) const; - - /** - * Create a unary term of given kind. - * @param kind the kind of the term - * @param child the child of the term - * @return the Term - */ - Term mkTerm(Kind kind, const Term& child) const; - - /** - * Create binary term of given kind. - * @param kind the kind of the term - * @param child1 the first child of the term - * @param child2 the second child of the term - * @return the Term - */ - Term mkTerm(Kind kind, const Term& child1, const Term& child2) const; - - /** - * Create ternary term of given kind. - * @param kind the kind of the term - * @param child1 the first child of the term - * @param child2 the second child of the term - * @param child3 the third child of the term - * @return the Term - */ - Term mkTerm(Kind kind, - const Term& child1, - const Term& child2, - const Term& child3) const; - - /** - * Create n-ary term of given kind. - * @param kind the kind of the term - * @param children the children of the term - * @return the Term - */ - Term mkTerm(Kind kind, const std::vector<Term>& children) const; - - /** - * Create nullary term of given kind from a given operator. - * Create operators with mkOp(). - * @param the operator - * @return the Term - */ - Term mkTerm(const Op& op) const; - - /** - * Create unary term of given kind from a given operator. - * Create operators with mkOp(). - * @param the operator - * @child the child of the term - * @return the Term - */ - Term mkTerm(const Op& op, const Term& child) const; - - /** - * Create binary term of given kind from a given operator. - * Create operators with mkOp(). - * @param the operator - * @child1 the first child of the term - * @child2 the second child of the term - * @return the Term - */ - Term mkTerm(const Op& op, const Term& child1, const Term& child2) const; - - /** - * Create ternary term of given kind from a given operator. - * Create operators with mkOp(). - * @param the operator - * @child1 the first child of the term - * @child2 the second child of the term - * @child3 the third child of the term - * @return the Term - */ - Term mkTerm(const Op& op, - const Term& child1, - const Term& child2, - const Term& child3) const; - - /** - * Create n-ary term of given kind from a given operator. - * Create operators with mkOp(). - * @param op the operator - * @children the children of the term - * @return the Term - */ - Term mkTerm(const Op& op, const std::vector<Term>& children) const; - - /** - * Create a tuple term. Terms are automatically converted if sorts are - * compatible. - * @param sorts The sorts of the elements in the tuple - * @param terms The elements in the tuple - * @return the tuple Term - */ - Term mkTuple(const std::vector<Sort>& sorts, - const std::vector<Term>& terms) const; - - /* .................................................................... */ - /* Create Operators */ - /* .................................................................... */ - - /** - * 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. - * @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 - * @param arg the string argument to this operator - */ - Op mkOp(Kind kind, const std::string& arg) const; - - /** - * Create operator of kind: - * - DIVISIBLE - * - BITVECTOR_REPEAT - * - BITVECTOR_ZERO_EXTEND - * - BITVECTOR_SIGN_EXTEND - * - BITVECTOR_ROTATE_LEFT - * - BITVECTOR_ROTATE_RIGHT - * - INT_TO_BITVECTOR - * - FLOATINGPOINT_TO_UBV - * - FLOATINGPOINT_TO_UBV_TOTAL - * - FLOATINGPOINT_TO_SBV - * - FLOATINGPOINT_TO_SBV_TOTAL - * - TUPLE_UPDATE - * See enum Kind for a description of the parameters. - * @param kind the kind of the operator - * @param arg the uint32_t argument to this operator - */ - Op mkOp(Kind kind, uint32_t arg) const; - - /** - * Create operator of Kind: - * - BITVECTOR_EXTRACT - * - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR - * - FLOATINGPOINT_TO_FP_FLOATINGPOINT - * - FLOATINGPOINT_TO_FP_REAL - * - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR - * - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR - * - FLOATINGPOINT_TO_FP_GENERIC - * See enum Kind for a description of the parameters. - * @param kind the kind of the operator - * @param arg1 the first uint32_t argument to this operator - * @param arg2 the second uint32_t argument to this operator - */ - Op mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const; - - /** - * Create operator of Kind: - * - TUPLE_PROJECT - * See enum Kind for a description of the parameters. - * @param kind the kind of the operator - */ - Op mkOp(Kind kind, const std::vector<uint32_t>& args) const; - - /* .................................................................... */ - /* Create Constants */ - /* .................................................................... */ - - /** - * Create a Boolean true constant. - * @return the true constant - */ - Term mkTrue() const; - - /** - * Create a Boolean false constant. - * @return the false constant - */ - Term mkFalse() const; - - /** - * Create a Boolean constant. - * @return the Boolean constant - * @param val the value of the constant - */ - Term mkBoolean(bool val) const; - - /** - * Create a constant representing the number Pi. - * @return a constant representing Pi - */ - Term mkPi() const; - /** - * Create an integer constant from a string. - * @param s the string representation of the constant, may represent an - * integer (e.g., "123"). - * @return a constant of sort Integer assuming 's' represents an integer) - */ - Term mkInteger(const std::string& s) const; - - /** - * Create an integer constant from a c++ int. - * @param val the value of the constant - * @return a constant of sort Integer - */ - Term mkInteger(int64_t val) const; - - /** - * Create a real constant from a string. - * @param s the string representation of the constant, may represent an - * integer (e.g., "123") or real constant (e.g., "12.34" or "12/34"). - * @return a constant of sort Real - */ - Term mkReal(const std::string& s) const; - - /** - * Create a real constant from an integer. - * @param val the value of the constant - * @return a constant of sort Integer - */ - Term mkReal(int64_t val) const; - - /** - * Create a real constant from a rational. - * @param num the value of the numerator - * @param den the value of the denominator - * @return a constant of sort Real - */ - Term mkReal(int64_t num, int64_t den) const; - - /** - * Create a regular expression empty term. - * @return the empty term - */ - Term mkRegexpEmpty() const; - - /** - * Create a regular expression sigma term. - * @return the sigma term - */ - Term mkRegexpSigma() const; - - /** - * Create a constant representing an empty set of the given sort. - * @param sort the sort of the set elements. - * @return the empty set constant - */ - Term mkEmptySet(const Sort& sort) const; - - /** - * Create a constant representing an empty bag of the given sort. - * @param sort the sort of the bag elements. - * @return the empty bag constant - */ - Term mkEmptyBag(const Sort& sort) 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. - * @param s the string this constant represents - * @param useEscSequences determines whether escape sequences in \p s should - * be converted to the corresponding 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 - * @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; - - /** - * Create an empty sequence of the given element sort. - * @param sort The element sort of the sequence. - * @return the empty sequence with given element sort. - */ - Term mkEmptySequence(const Sort& sort) const; - - /** - * Create a universe set of the given sort. - * @param sort the sort of the set elements - * @return the universe set constant - */ - Term mkUniverseSet(const Sort& sort) const; - - /** - * Create a bit-vector constant of given size and value. - * @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. - * @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) - * @return the bit-vector constant - */ - Term mkBitVector(uint32_t size, const std::string& s, uint32_t base) const; - - /** - * Create a constant array with the provided constant value stored at every - * index - * @param sort the sort of the constant array (must be an array sort) - * @param val the constant value to store (must match the sort's element sort) - * @return the constant array term - */ - Term mkConstArray(const Sort& sort, const Term& val) const; - - /** - * Create a positive infinity floating-point constant. Requires CVC4 to be - * compiled with SymFPU support. - * @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 CVC4 to be - * compiled with SymFPU support. - * @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 CVC4 to be - * compiled with SymFPU support. - * @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 CVC4 to be - * compiled with SymFPU support. - * @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 CVC4 to be - * compiled with SymFPU support. - * @param exp Number of bits in the exponent - * @param sig Number of bits in the significand - * @return the floating-point constant - */ - Term mkNegZero(uint32_t exp, uint32_t sig) const; - - /** - * Create a roundingmode constant. - * @param rm the floating point rounding mode this constant represents - */ - Term mkRoundingMode(RoundingMode rm) const; - - /** - * Create uninterpreted constant. - * @param arg1 Sort of the constant - * @param arg2 Index of the constant - */ - Term mkUninterpretedConst(const Sort& sort, int32_t index) const; - - /** - * Create an abstract value constant. - * @param index Index of the abstract value - */ - Term mkAbstractValue(const std::string& index) const; - - /** - * Create an abstract value constant. - * @param index Index of the abstract value - */ - Term mkAbstractValue(uint64_t index) const; - - /** - * Create a floating-point constant (requires CVC4 to be compiled with symFPU - * support). - * @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 Variables */ - /* .................................................................... */ - - /** - * Create (first-order) constant (0-arity function symbol). - * SMT-LIB: ( declare-const <symbol> <sort> ) - * SMT-LIB: ( declare-fun <symbol> ( ) <sort> ) - * - * @param sort the sort of the constant - * @param symbol the name of the constant - * @return the first-order constant - */ - Term mkConst(const Sort& sort, const std::string& symbol) const; - /** - * Create (first-order) constant (0-arity function symbol), with a default - * symbol name. - * - * @param sort the sort of the constant - * @return the first-order constant - */ - Term mkConst(const Sort& sort) const; - - /** - * Create a bound variable to be used in a binder (i.e. a quantifier, a - * lambda, or a witness binder). - * @param sort the sort of the variable - * @param symbol the name of the variable - * @return the variable - */ - Term mkVar(const Sort& sort, const std::string& symbol = std::string()) const; - - /* .................................................................... */ - /* Create datatype constructor declarations */ - /* .................................................................... */ - - DatatypeConstructorDecl mkDatatypeConstructorDecl(const std::string& name); - - /* .................................................................... */ - /* Create datatype declarations */ - /* .................................................................... */ - - /** - * Create a datatype declaration. - * @param name the name of the datatype - * @param isCoDatatype true if a codatatype is to be constructed - * @return the DatatypeDecl - */ - DatatypeDecl mkDatatypeDecl(const std::string& name, - bool isCoDatatype = false); - - /** - * Create a datatype declaration. - * Create sorts parameter with Solver::mkParamSort(). - * @param name the name of the datatype - * @param param the sort parameter - * @param isCoDatatype true if a codatatype is to be constructed - * @return the DatatypeDecl - */ - DatatypeDecl mkDatatypeDecl(const std::string& name, - Sort param, - bool isCoDatatype = false); - - /** - * Create a datatype declaration. - * Create sorts parameter with Solver::mkParamSort(). - * @param name the name of the datatype - * @param params a list of sort parameters - * @param isCoDatatype true if a codatatype is to be constructed - * @return the DatatypeDecl - */ - DatatypeDecl mkDatatypeDecl(const std::string& name, - const std::vector<Sort>& params, - bool isCoDatatype = false); - - /* .................................................................... */ - /* Formula Handling */ - /* .................................................................... */ - - /** - * Simplify a formula without doing "much" work. Does not involve - * the SAT Engine in the simplification, but uses the current - * definitions, assertions, and the current partial model, if one - * has been constructed. It also involves theory normalization. - * @param t the formula to simplify - * @return the simplified formula - */ - Term simplify(const Term& t); - - /** - * Assert a formula. - * SMT-LIB: ( assert <term> ) - * @param term the formula to assert - */ - void assertFormula(const Term& term) const; - - /** - * Check satisfiability. - * SMT-LIB: ( check-sat ) - * @return the result of the satisfiability check. - */ - Result checkSat() const; - - /** - * Check satisfiability assuming the given formula. - * SMT-LIB: ( check-sat-assuming ( <prop_literal> ) ) - * @param assumption the formula to assume - * @return the result of the satisfiability check. - */ - Result checkSatAssuming(const Term& assumption) const; - - /** - * Check satisfiability assuming the given formulas. - * SMT-LIB: ( check-sat-assuming ( <prop_literal>+ ) ) - * @param assumptions the formulas to assume - * @return the result of the satisfiability check. - */ - Result checkSatAssuming(const std::vector<Term>& assumptions) const; - - /** - * Check entailment of the given formula w.r.t. the current set of assertions. - * @param term the formula to check entailment for - * @return the result of the entailment check. - */ - Result checkEntailed(const Term& term) const; - - /** - * Check entailment of the given set of given formulas w.r.t. the current - * set of assertions. - * @param terms the terms to check entailment for - * @return the result of the entailmentcheck. - */ - Result checkEntailed(const std::vector<Term>& terms) const; - - /** - * Create datatype sort. - * SMT-LIB: ( declare-datatype <symbol> <datatype_decl> ) - * @param symbol the name of the datatype sort - * @param ctors the constructor declarations of the datatype sort - * @return the datatype sort - */ - Sort declareDatatype(const std::string& symbol, - const std::vector<DatatypeConstructorDecl>& ctors) const; - - /** - * Declare n-ary function symbol. - * SMT-LIB: ( declare-fun <symbol> ( <sort>* ) <sort> ) - * @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 - * @return the function - */ - Term declareFun(const std::string& symbol, - const std::vector<Sort>& sorts, - const Sort& sort) const; - - /** - * Declare uninterpreted sort. - * SMT-LIB: ( declare-sort <symbol> <numeral> ) - * @param symbol the name of the sort - * @param arity the arity of the sort - * @return the sort - */ - Sort declareSort(const std::string& symbol, uint32_t arity) const; - - /** - * Define n-ary function. - * SMT-LIB: ( define-fun <function_def> ) - * @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 - * @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 std::string& symbol, - const std::vector<Term>& bound_vars, - const Sort& sort, - const Term& term, - bool global = false) const; - /** - * Define n-ary function. - * SMT-LIB: ( define-fun <function_def> ) - * 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: ( define-fun-rec <function_def> ) - * @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 - * @param term the function body - * @param global determines whether this definition is global (i.e. persists - * when popping the context) - * @return the function - */ - Term defineFunRec(const std::string& symbol, - const std::vector<Term>& bound_vars, - const Sort& sort, - const Term& term, - bool global = false) const; - - /** - * Define recursive function. - * SMT-LIB: ( define-fun-rec <function_def> ) - * 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 defineFunRec(const Term& fun, - const std::vector<Term>& bound_vars, - const Term& term, - bool global = false) const; - - /** - * Define recursive functions. - * SMT-LIB: ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) ) - * Create elements of parameter 'funs' with mkConst(). - * @param funs the sorted functions - * @param bound_vars the list of parameters to the functions - * @param term the list of function bodies of the functions - * @param global determines whether this definition is global (i.e. persists - * when popping the context) - * @return the function - */ - void defineFunsRec(const std::vector<Term>& funs, - const std::vector<std::vector<Term>>& bound_vars, - const std::vector<Term>& terms, - bool global = false) const; - - /** - * Echo a given string to the given output stream. - * SMT-LIB: ( echo <std::string> ) - * @param out the output stream - * @param str the string to echo - */ - void echo(std::ostream& out, const std::string& str) const; - - /** - * Get the list of asserted formulas. - * SMT-LIB: ( get-assertions ) - * @return the list of asserted formulas - */ - std::vector<Term> getAssertions() const; - - /** - * Get info from the solver. - * SMT-LIB: ( get-info <info_flag> ) - * @return the info - */ - std::string getInfo(const std::string& flag) const; - - /** - * Get the value of a given option. - * SMT-LIB: ( get-option <keyword> ) - * @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 the set of unsat ("failed") assumptions. - * SMT-LIB: ( get-unsat-assumptions ) - * Requires to enable option 'produce-unsat-assumptions'. - * @return the set of unsat assumptions. - */ - std::vector<Term> getUnsatAssumptions() const; - - /** - * Get the unsatisfiable core. - * SMT-LIB: ( get-unsat-core ) - * 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. - * SMT-LIB: ( get-value ( <term> ) ) - * @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. - * SMT-LIB: ( get-value ( <term>+ ) ) - * @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; - - /** - * Do quantifier elimination. - * SMT-LIB: ( get-qe <q> ) - * 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. - */ - 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: ( get-qe-disjunct <q> ) - * 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. - */ - Term getQuantifierEliminationDisjunct(const Term& q) const; - - /** - * When using separation logic, this sets the location sort and the - * datatype sort to the given ones. This method should be invoked exactly - * once, before any separation logic constraints are provided. - * @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; - - /** - * When using separation logic, obtain the term for the heap. - * @return The term for the heap - */ - Term getSeparationHeap() const; - - /** - * When using separation logic, obtain the term for nil. - * @return The term for nil - */ - Term getSeparationNilTerm() const; - - /** - * Pop (a) level(s) from the assertion stack. - * SMT-LIB: ( pop <numeral> ) - * @param nscopes the number of levels to pop - */ - void pop(uint32_t nscopes = 1) const; - - /** - * Get an interpolant - * SMT-LIB: ( get-interpol <conj> ) - * 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. - * @return true if it gets I successfully, false otherwise. - */ - bool getInterpolant(const Term& conj, Term& output) const; - - /** - * Get an interpolant - * SMT-LIB: ( get-interpol <conj> <g> ) - * 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 - * current set of assertions and B is given in the input by conj. - * @return true if it gets I successfully, false otherwise. - */ - bool getInterpolant(const Term& conj, Grammar& grammar, Term& output) const; - - /** - * Get an abduct. - * SMT-LIB: ( get-abduct <conj> ) - * 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 - */ - bool getAbduct(const Term& conj, Term& output) const; - - /** - * Get an abduct. - * SMT-LIB: ( get-abduct <conj> <g> ) - * 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 - */ - bool getAbduct(const Term& conj, Grammar& grammar, Term& output) const; - - /** - * Block the current model. Can be called only if immediately preceded by a - * SAT or INVALID query. - * SMT-LIB: ( block-model ) - * 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: ( block-model-values ( <terms>+ ) ) - * Requires enabling 'produce-models' option and setting 'block-models' option - * to a mode other than "none". - */ - void blockModelValues(const std::vector<Term>& terms) const; - - /** - * Print all instantiations made by the quantifiers module. - * @param out the output stream - */ - void printInstantiations(std::ostream& out) const; - - /** - * Push (a) level(s) to the assertion stack. - * SMT-LIB: ( push <numeral> ) - * @param nscopes the number of levels to push - */ - void push(uint32_t nscopes = 1) const; - - /** - * Remove all assertions. - * SMT-LIB: ( reset-assertions ) - */ - void resetAssertions() const; - - /** - * Set info. - * SMT-LIB: ( set-info <attribute> ) - * @param keyword the info flag - * @param value the value of the info flag - */ - void setInfo(const std::string& keyword, const std::string& value) const; - - /** - * Set logic. - * SMT-LIB: ( set-logic <symbol> ) - * @param logic the logic to set - */ - void setLogic(const std::string& logic) const; - - /** - * Set option. - * SMT-LIB: ( set-option <option> ) - * @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. - * @param s the target sort - * @return the term wrapped into a sort conversion if needed - */ - Term ensureTermSort(const Term& t, const Sort& s) const; - - /** - * Append <symbol> to the current list of universal variables. - * SyGuS v2: ( declare-var <symbol> <sort> ) - * @param sort the sort of the universal variable - * @param symbol the name of the universal variable - * @return the universal variable - */ - Term mkSygusVar(const Sort& sort, - const std::string& symbol = std::string()) const; - - /** - * Create a Sygus grammar. The first non-terminal is treated as the starting - * non-terminal, so the order of non-terminals matters. - * - * @param boundVars the parameters to corresponding synth-fun/synth-inv - * @param ntSymbols the pre-declaration of the non-terminal symbols - * @return the grammar - */ - Grammar mkSygusGrammar(const std::vector<Term>& boundVars, - const std::vector<Term>& ntSymbols) const; - - /** - * Synthesize n-ary function. - * SyGuS v2: ( synth-fun <symbol> ( <boundVars>* ) <sort> ) - * @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 - * @return the function - */ - Term synthFun(const std::string& symbol, - const std::vector<Term>& boundVars, - const Sort& sort) const; - - /** - * Synthesize n-ary function following specified syntactic constraints. - * SyGuS v2: ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> ) - * @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 - * @param grammar the syntactic constraints - * @return the function - */ - Term synthFun(const std::string& symbol, - const std::vector<Term>& boundVars, - Sort sort, - Grammar& grammar) const; - - /** - * Synthesize invariant. - * SyGuS v2: ( synth-inv <symbol> ( <boundVars>* ) ) - * @param symbol the name of the invariant - * @param boundVars the parameters to this invariant - * @param sort the sort of the return value of this invariant - * @return the invariant - */ - Term synthInv(const std::string& symbol, - const std::vector<Term>& boundVars) const; - - /** - * Synthesize invariant following specified syntactic constraints. - * SyGuS v2: ( synth-inv <symbol> ( <boundVars>* ) <g> ) - * @param symbol the name of the invariant - * @param boundVars the parameters to this invariant - * @param sort the sort of the return value of this invariant - * @param grammar the syntactic constraints - * @return the invariant - */ - Term synthInv(const std::string& symbol, - const std::vector<Term>& boundVars, - Grammar& grammar) const; - - /** - * Add a forumla to the set of Sygus constraints. - * SyGuS v2: ( constraint <term> ) - * @param term the formula to add as a constraint - */ - void addSygusConstraint(const Term& term) const; - - /** - * Add a set of Sygus constraints to the current state that correspond to an - * invariant synthesis problem. - * SyGuS v2: ( inv-constraint <inv> <pre> <trans> <post> ) - * @param inv the function-to-synthesize - * @param pre the pre-condition - * @param trans the transition relation - * @param post the post-condition - */ - void addSygusInvConstraint(Term inv, Term pre, Term trans, Term post) const; - - /** - * Try to find a solution for the synthesis conjecture corresponding to the - * current list of functions-to-synthesize, universal variables and - * constraints. - * SyGuS v2: ( check-synth ) - * @return the result of the synthesis conjecture. - */ - Result checkSynth() const; - - /** - * Get the synthesis solution of the given term. This method should be called - * immediately after the solver answers unsat for sygus input. - * @param term the term for which the synthesis solution is queried - * @return the synthesis solution of the given term - */ - Term getSynthSolution(Term term) const; - - /** - * Get the synthesis solutions of the given terms. This method should be - * called immediately after the solver answers unsat for sygus input. - * @param terms the terms for which the synthesis solutions is queried - * @return the synthesis solutions of the given terms - */ - 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); - - private: - /** @return the node manager of this solver */ - NodeManager* getNodeManager(void) 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; - /** Helper for mkReal functions that take a string as argument. */ - Term mkRealFromStrHelper(const std::string& s) const; - /** Helper for mkBitVector functions that take a string as argument. */ - Term mkBVFromStrHelper(const std::string& s, uint32_t base) const; - /** - * Helper for mkBitVector functions that take a string and a size as - * arguments. - */ - Term mkBVFromStrHelper(uint32_t size, - const std::string& s, - uint32_t base) const; - /** Helper for mkBitVector functions that take an integer as argument. */ - Term mkBVFromIntHelper(uint32_t size, uint64_t val) const; - /** Helper for functions that create tuple sorts. */ - Sort mkTupleSortHelper(const std::vector<Sort>& sorts) const; - /** Helper for mkTerm functions that create Term from a Kind */ - Term mkTermFromKind(Kind kind) const; - /** Helper for mkChar functions that take a string as argument. */ - Term mkCharFromStrHelper(const std::string& s) const; - /** Get value helper, which accounts for subtyping */ - Term getValueHelper(const Term& term) const; - - /** - * Helper function that ensures that a given term is of sort real (as opposed - * to being of sort integer). - * @param t a term of sort integer or real - * @return a term of sort real - */ - Term ensureRealSort(const Term& t) const; - - /** - * Create n-ary term of given kind. This handles the cases of left/right - * associative operators, chainable operators, and cases when the number of - * children exceeds the maximum arity for the kind. - * @param kind the kind of the term - * @param children the children of the term - * @return the Term - */ - Term mkTermHelper(Kind kind, const std::vector<Term>& children) const; - - /** - * Create n-ary term of given kind from a given operator. - * @param op the operator - * @param children the children of the term - * @return the Term - */ - Term mkTermHelper(const Op& op, const std::vector<Term>& children) const; - - /** - * Create a vector of datatype sorts, using unresolved sorts. - * @param dtypedecls the datatype declarations from which the sort is created - * @param unresolvedSorts the list of unresolved sorts - * @return the datatype sorts - */ - std::vector<Sort> mkDatatypeSortsInternal( - const std::vector<DatatypeDecl>& dtypedecls, - const std::set<Sort>& unresolvedSorts) const; - - /** - * Synthesize n-ary function following specified syntactic constraints. - * SMT-LIB: ( synth-fun <symbol> ( <boundVars>* ) <sort> <g>? ) - * @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 - * @param isInv determines whether this is synth-fun or synth-inv - * @param g the syntactic constraints - * @return the function - */ - Term synthFunHelper(const std::string& symbol, - const std::vector<Term>& boundVars, - const Sort& sort, - bool isInv = false, - Grammar* grammar = nullptr) const; - - /** Check whether string s is a valid decimal integer. */ - bool isValidInteger(const std::string& s) const; - - /** Increment the term stats counter. */ - void increment_term_stats(Kind kind) const; - /** Increment the vars stats (if 'is_var') or consts stats counter. */ - void increment_vars_consts_stats(const Sort& sort, bool is_var) const; - - /** 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; - /** The statistics collected on the Api level. */ - std::unique_ptr<Statistics> d_stats; - /** The SMT engine of this solver. */ - std::unique_ptr<SmtEngine> d_smtEngine; - /** The random number generator of this solver. */ - std::unique_ptr<Random> d_rng; -}; - -} // namespace api -} // namespace cvc5 -#endif |