diff options
| -rw-r--r-- | src/api/cvc4cpp.cpp | 146 | ||||
| -rw-r--r-- | src/api/cvc4cpp.h | 138 | ||||
| -rw-r--r-- | src/parser/parser.cpp | 2 | ||||
| -rw-r--r-- | src/parser/parser.h | 3 | ||||
| -rw-r--r-- | src/parser/smt2/Smt2.g | 228 | ||||
| -rw-r--r-- | test/unit/api/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | test/unit/api/datatype_api_black.h | 57 | ||||
| -rw-r--r-- | test/unit/api/solver_black.h | 67 |
8 files changed, 519 insertions, 125 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index c0818f54f..dbbb4b535 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1461,6 +1461,14 @@ DatatypeConstructor::DatatypeConstructor(const CVC4::DatatypeConstructor& ctor) DatatypeConstructor::~DatatypeConstructor() {} +bool DatatypeConstructor::isResolved() const { return d_ctor->isResolved(); } + +Term DatatypeConstructor::getConstructorTerm() const +{ + CVC4_API_CHECK(isResolved()) << "Expected resolved datatype constructor."; + return Term(d_ctor->getConstructor()); +} + DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const { // CHECK: selector with name exists? @@ -1583,6 +1591,13 @@ Datatype::Datatype(const CVC4::Datatype& dtype) Datatype::~Datatype() {} +DatatypeConstructor Datatype::operator[](size_t idx) const +{ + // CHECK (maybe): is resolved? + CVC4_API_CHECK(idx < getNumConstructors()) << "Index out of bounds."; + return (*d_dtype)[idx]; +} + DatatypeConstructor Datatype::operator[](const std::string& name) const { // CHECK: cons with name exists? @@ -1735,6 +1750,8 @@ Solver::~Solver() {} /* Sorts Handling */ /* -------------------------------------------------------------------------- */ +Sort Solver::getNullSort(void) const { return Type(); } + Sort Solver::getBooleanSort(void) const { return d_exprMgr->booleanType(); } Sort Solver::getIntegerSort(void) const { return d_exprMgr->integerType(); } @@ -2051,14 +2068,14 @@ Term Solver::mkSepNil(Sort sort) const } } -Term Solver::mkString(const char* s) const +Term Solver::mkString(const char* s, bool useEscSequences) const { - return mkConstHelper<CVC4::String>(CVC4::String(s)); + return mkConstHelper<CVC4::String>(CVC4::String(s, useEscSequences)); } -Term Solver::mkString(const std::string& s) const +Term Solver::mkString(const std::string& s, bool useEscSequences) const { - return mkConstHelper<CVC4::String>(CVC4::String(s)); + return mkConstHelper<CVC4::String>(CVC4::String(s, useEscSequences)); } Term Solver::mkString(const unsigned char c) const @@ -2078,7 +2095,8 @@ Term Solver::mkUniverseSet(Sort sort) const CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; Term res = d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::UNIVERSE_SET); - (void)res.d_expr->getType(true); /* kick off type checking */ + // TODO(#2771): Reenable? + // (void)res.d_expr->getType(true); /* kick off type checking */ return res; } catch (TypeCheckingException& e) @@ -2105,7 +2123,8 @@ Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const try { CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string"; - CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 16, s) << "base 2 or 16"; + CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s) + << "base 2, 10, or 16"; return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(s, base)); } catch (std::invalid_argument& e) @@ -2114,6 +2133,28 @@ Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const } } +Term Solver::mkBVFromStrHelper(uint32_t size, + std::string s, + uint32_t base) const +{ + try + { + CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string"; + CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s) + << "base 2, 10, or 16"; + + Integer val(s, base); + CVC4_API_CHECK(val.modByPow2(size) == val) + << "Overflow in bitvector construction (specified bitvector size " + << size << " too small to hold value " << s << ")"; + return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(size, val)); + } + catch (std::invalid_argument& e) + { + throw CVC4ApiException(e.what()); + } +} + Term Solver::mkBitVector(const char* s, uint32_t base) const { CVC4_API_ARG_CHECK_NOT_NULL(s); @@ -2125,6 +2166,57 @@ Term Solver::mkBitVector(const std::string& s, uint32_t base) const return mkBVFromStrHelper(s, base); } +Term Solver::mkBitVector(uint32_t size, const char* s, uint32_t base) const +{ + CVC4_API_ARG_CHECK_NOT_NULL(s); + return mkBVFromStrHelper(size, s, base); +} + +Term Solver::mkBitVector(uint32_t size, std::string& s, uint32_t base) const +{ + return mkBVFromStrHelper(size, s, base); +} + +Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const +{ + CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) + << "Expected CVC4 to be compiled with SymFPU support"; + return mkConstHelper<CVC4::FloatingPoint>( + FloatingPoint::makeInf(FloatingPointSize(exp, sig), false)); +} + +Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const +{ + CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) + << "Expected CVC4 to be compiled with SymFPU support"; + return mkConstHelper<CVC4::FloatingPoint>( + FloatingPoint::makeInf(FloatingPointSize(exp, sig), true)); +} + +Term Solver::mkNaN(uint32_t exp, uint32_t sig) const +{ + CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) + << "Expected CVC4 to be compiled with SymFPU support"; + return mkConstHelper<CVC4::FloatingPoint>( + FloatingPoint::makeNaN(FloatingPointSize(exp, sig))); +} + +Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const +{ + CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) + << "Expected CVC4 to be compiled with SymFPU support"; + return mkConstHelper<CVC4::FloatingPoint>( + FloatingPoint::makeZero(FloatingPointSize(exp, sig), false)); +} + +Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const +{ + CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) + << "Expected CVC4 to be compiled with SymFPU support"; + return mkConstHelper<CVC4::FloatingPoint>( + FloatingPoint::makeZero(FloatingPointSize(exp, sig), true)); +} + Term Solver::mkConst(RoundingMode rm) const { try @@ -2655,6 +2747,23 @@ Term Solver::mkTerm(OpTerm opTerm, const std::vector<Term>& children) const } } +Term Solver::mkTuple(const std::vector<Sort>& sorts, + const std::vector<Term>& terms) const +{ + CVC4_API_CHECK(sorts.size() == terms.size()) + << "Expected the same number of sorts and elements"; + std::vector<Term> args; + for (size_t i = 0, size = sorts.size(); i < size; i++) + { + args.push_back(ensureTermSort(terms[i], sorts[i])); + } + + Sort s = mkTupleSort(sorts); + Datatype dt = s.getDatatype(); + args.insert(args.begin(), dt[0].getConstructorTerm()); + return mkTerm(APPLY_CONSTRUCTOR, args); +} + std::vector<Expr> Solver::termVectorToExprs( const std::vector<Term>& terms) const { @@ -3359,6 +3468,31 @@ void Solver::setOption(const std::string& option, d_smtEngine->setOption(option, value); } +Term Solver::ensureTermSort(const Term& t, const Sort& s) const +{ + CVC4_API_CHECK(t.getSort() == s || (t.getSort().isInteger() && s.isReal())) + << "Expected conversion from Int to Real"; + + if (t.getSort() == s) + { + return t; + } + + // Integers are reals, too + Assert(t.getSort().isReal()); + Term res = t; + if (t.getSort().isInteger()) + { + // Must cast to Real to ensure correct type is passed to parametric type + // constructors. We do this cast using division with 1. This has the + // advantage wrt using TO_REAL since (constant) division is always included + // in the theory. + res = mkTerm(DIVISION, *t.d_expr, mkReal(1)); + } + Assert(res.getSort() == s); + return res; +} + /** * !!! This is only temporarily available until the parser is fully migrated to * the new API. !!! diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 1f74a34a9..ef82a9174 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1135,7 +1135,7 @@ class CVC4_PUBLIC DatatypeConstructor /** * Constructor. * @param ctor the internal datatype constructor to be wrapped - * @return thte DatatypeConstructor + * @return the DatatypeConstructor */ DatatypeConstructor(const CVC4::DatatypeConstructor& ctor); @@ -1145,6 +1145,17 @@ class CVC4_PUBLIC DatatypeConstructor ~DatatypeConstructor(); /** + * @return true if this datatype constructor has been resolved. + */ + bool isResolved() const; + + /** + * Get the constructor operator of this datatype constructor. + * @return the constructor operator + */ + Term getConstructorTerm() 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. @@ -1286,6 +1297,13 @@ class CVC4_PUBLIC Datatype ~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. @@ -1521,6 +1539,11 @@ class CVC4_PUBLIC Solver /* .................................................................... */ /** + * @return sort null + */ + Sort getNullSort() const; + + /** * @return sort Boolean */ Sort getBooleanSort() const; @@ -1739,6 +1762,16 @@ class CVC4_PUBLIC Solver */ Term mkTerm(OpTerm opTerm, 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 Operator Terms */ /* .................................................................... */ @@ -1827,7 +1860,7 @@ class CVC4_PUBLIC Solver Term mkPi() const; /** - * Create a real constant. + * 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 or Integer (if 's' represents an integer) @@ -1835,7 +1868,7 @@ class CVC4_PUBLIC Solver Term mkReal(const char* s) const; /** - * Create a real constant. + * 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 or Integer (if 's' represents an integer) @@ -1931,16 +1964,20 @@ class CVC4_PUBLIC Solver /** * 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 char* s) const; + Term mkString(const char* s, bool useEscSequences = false) 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) const; + Term mkString(const std::string& s, bool useEscSequences = false) const; /** * Create a String constant. @@ -1973,21 +2010,84 @@ class CVC4_PUBLIC Solver /** * Create a bit-vector constant from a given string. - * @param s the string represetntation of the constant - * @param base the base of the string representation + * @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 char* s, uint32_t base = 2) const; /** * Create a bit-vector constant from a given string. - * @param s the string represetntation of the constant - * @param base the base of the string representation + * @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. + * @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 char* s, uint32_t base) const; + + /** + * Create a bit-vector constant of a given bit-width from a given string. + * @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, std::string& s, uint32_t base) 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 constant of kind: * - CONST_ROUNDINGMODE * @param rm the floating point rounding mode this constant represents @@ -2507,6 +2607,15 @@ class CVC4_PUBLIC Solver */ 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; + // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! ExprManager* getExprManager(void) const; @@ -2530,6 +2639,9 @@ class CVC4_PUBLIC Solver Term mkRealFromStrHelper(std::string s) const; /* Helper for mkBitVector functions that take a string as argument. */ Term mkBVFromStrHelper(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, 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 mkConst functions that take a string as argument. */ @@ -2539,6 +2651,14 @@ class CVC4_PUBLIC Solver template <typename T> Term mkConstFromIntHelper(Kind kind, T a) const; + /** + * Helper function that ensures that a given term is of sort real (as opposed + * to being of sort integer). + * @param term a term of sort integer or real + * @return a term of sort real + */ + Term ensureRealSort(Term expr) const; + /* The expression manager of this solver. */ std::unique_ptr<ExprManager> d_exprMgr; /* The SMT engine of this solver. */ diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 8ddefb2f4..71d226c98 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -81,6 +81,8 @@ ExprManager* Parser::getExprManager() const return d_solver->getExprManager(); } +api::Solver* Parser::getSolver() const { return d_solver; } + Expr Parser::getSymbol(const std::string& name, SymbolType type) { checkDeclaration(name, CHECK_DECLARED, type); assert(isDeclared(name, type)); diff --git a/src/parser/parser.h b/src/parser/parser.h index f22fc3789..8c18055a7 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -269,6 +269,9 @@ public: /** Get the associated <code>ExprManager</code>. */ ExprManager* getExprManager() const; + /** Get the associated solver. */ + api::Solver* getSolver() const; + /** Get the associated input. */ inline Input* getInput() const { return d_input; diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 7143824d6..e33ab7a70 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -100,6 +100,10 @@ namespace CVC4 { };/* struct myExpr */ }/* CVC4::parser::smt2 namespace */ }/* CVC4::parser namespace */ + + namespace api { + class Term; + } }/* CVC4 namespace */ }/* @parser::includes */ @@ -112,6 +116,7 @@ namespace CVC4 { #include <unordered_set> #include <vector> +#include "api/cvc4cpp.h" #include "base/output.h" #include "expr/expr.h" #include "expr/kind.h" @@ -141,6 +146,8 @@ using namespace CVC4::parser; #define MK_EXPR EXPR_MANAGER->mkExpr #undef MK_CONST #define MK_CONST EXPR_MANAGER->mkConst +#undef SOLVER +#define SOLVER PARSER_STATE->getSolver() #define UNSUPPORTED PARSER_STATE->unimplementedFeature static bool isClosed(const Expr& e, std::set<Expr>& free, std::unordered_set<Expr, ExprHashFunction>& closedCache) { @@ -878,7 +885,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] std::vector< Expr > let_vars; bool readingLet = false; std::string s; - CVC4::Expr atomExpr; + CVC4::api::Term atomTerm; } : LPAREN_TOK //read operator @@ -973,15 +980,16 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] PARSER_STATE->popScope(); } } - | termAtomic[atomExpr] { - Debug("parser-sygus") << "Sygus grammar " << fun << " : atomic " - << "expression " << atomExpr << std::endl; - std::stringstream ss; - ss << atomExpr; - sgt.d_expr = atomExpr; - sgt.d_name = ss.str(); - sgt.d_gterm_type = SygusGTerm::gterm_op; - } + | termAtomic[atomTerm] + { + Debug("parser-sygus") << "Sygus grammar " << fun << " : atomic " + << "expression " << atomTerm << std::endl; + std::stringstream ss; + ss << atomTerm; + sgt.d_expr = atomTerm.getExpr(); + sgt.d_name = ss.str(); + sgt.d_gterm_type = SygusGTerm::gterm_op; + } | symbol[name,CHECK_NONE,SYM_VARIABLE] { if( name[0] == '-' ){ //hack for unary minus @@ -1709,6 +1717,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] std::vector<Type> match_ptypes; Type type; Type type2; + api::Term atomTerm; } : /* a built-in operator application */ LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK @@ -2207,19 +2216,17 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] | LPAREN_TOK TUPLE_CONST_TOK termList[args,expr] RPAREN_TOK { - std::vector<Type> types; - for (std::vector<Expr>::const_iterator i = args.begin(); i != args.end(); - ++i) + std::vector<api::Sort> sorts; + std::vector<api::Term> terms; + for (const Expr& arg : args) { - types.push_back((*i).getType()); + sorts.emplace_back(arg.getType()); + terms.emplace_back(arg); } - DatatypeType t = EXPR_MANAGER->mkTupleType(types); - const Datatype& dt = t.getDatatype(); - args.insert(args.begin(), dt[0].getConstructor()); - expr = MK_EXPR(kind::APPLY_CONSTRUCTOR, args); + expr = SOLVER->mkTuple(sorts, terms).getExpr(); } | /* an atomic term (a term with no subterms) */ - termAtomic[expr] + termAtomic[atomTerm] { expr = atomTerm.getExpr(); } ; @@ -2227,128 +2234,145 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] * Matches an atomic term (a term with no subterms). * @return the expression expr representing the term or formula. */ -termAtomic[CVC4::Expr& expr] +termAtomic[CVC4::api::Term& atomTerm] @init { - std::vector<Expr> args; Type type; Type type2; std::string s; } /* constants */ : INTEGER_LITERAL - { expr = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); } - + { + std::string intStr = AntlrInput::tokenText($INTEGER_LITERAL); + atomTerm = SOLVER->mkReal(intStr); + } | DECIMAL_LITERAL - { // FIXME: This doesn't work because an SMT rational is not a - // valid GMP rational string - expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); - if(expr.getType().isInteger()) { - // Must cast to Real to ensure correct type is passed to parametric type constructors. - // We do this cast using division with 1. - // This has the advantage wrt using TO_REAL since (constant) division is always included in the theory. - expr = MK_EXPR(kind::DIVISION, expr, MK_CONST(Rational(1))); - } + { + std::string realStr = AntlrInput::tokenText($DECIMAL_LITERAL); + atomTerm = SOLVER->ensureTermSort(SOLVER->mkReal(realStr), + SOLVER->getRealSort()); } + // Pi constant + | REAL_PI_TOK { atomTerm = SOLVER->mkPi(); } + + // Constants using indexed identifiers, e.g. (_ +oo 8 24) (positive infinity + // as a 32-bit floating-point constant) | LPAREN_TOK INDEX_TOK ( bvLit=SIMPLE_SYMBOL size=INTEGER_LITERAL - { if(AntlrInput::tokenText($bvLit).find("bv") == 0) { - expr = MK_CONST( AntlrInput::tokenToBitvector($bvLit, $size) ); - } else { + { + if(AntlrInput::tokenText($bvLit).find("bv") == 0) + { + std::string bvStr = AntlrInput::tokenTextSubstr($bvLit, 2); + uint32_t bvSize = AntlrInput::tokenToUnsigned($size); + atomTerm = SOLVER->mkBitVector(bvSize, bvStr, 10); + } + else + { PARSER_STATE->parseError("Unexpected symbol `" + AntlrInput::tokenText($bvLit) + "'"); } } + + // Floating-point constants | FP_PINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { expr = MK_CONST(FloatingPoint::makeInf(FloatingPointSize(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb)), - false)); } + { + atomTerm = SOLVER->mkPosInf(AntlrInput::tokenToUnsigned($eb), + AntlrInput::tokenToUnsigned($sb)); + } | FP_NINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { expr = MK_CONST(FloatingPoint::makeInf(FloatingPointSize(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb)), - true)); } + { + atomTerm = SOLVER->mkNegInf(AntlrInput::tokenToUnsigned($eb), + AntlrInput::tokenToUnsigned($sb)); + } | FP_NAN_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { expr = MK_CONST(FloatingPoint::makeNaN(FloatingPointSize(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb)))); } - + { + atomTerm = SOLVER->mkNaN(AntlrInput::tokenToUnsigned($eb), + AntlrInput::tokenToUnsigned($sb)); + } | FP_PZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { expr = MK_CONST(FloatingPoint::makeZero(FloatingPointSize(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb)), - false)); } + { + atomTerm = SOLVER->mkPosZero(AntlrInput::tokenToUnsigned($eb), + AntlrInput::tokenToUnsigned($sb)); + } | FP_NZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { expr = MK_CONST(FloatingPoint::makeZero(FloatingPointSize(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb)), - true)); } + { + atomTerm = SOLVER->mkNegZero(AntlrInput::tokenToUnsigned($eb), + AntlrInput::tokenToUnsigned($sb)); + } + + // Empty heap constant in seperation logic | EMP_TOK sortSymbol[type,CHECK_DECLARED] sortSymbol[type2,CHECK_DECLARED] { - Expr v1 = PARSER_STATE->mkVar("_emp1", type); - Expr v2 = PARSER_STATE->mkVar("_emp2", type2); - expr = MK_EXPR(kind::SEP_EMP,v1,v2); + api::Term v1 = SOLVER->mkVar("_emp1", api::Sort(type)); + api::Term v2 = SOLVER->mkVar("_emp2", api::Sort(type2)); + atomTerm = SOLVER->mkTerm(api::SEP_EMP, v1, v2); } - // NOTE: Theory parametric constants go here + // NOTE: Theory parametric constants go here ) RPAREN_TOK + // Bit-vector constants | HEX_LITERAL - { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); - std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); - expr = MK_CONST( BitVector(hexString, 16) ); } - - | BINARY_LITERAL - { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); - std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); - expr = MK_CONST( BitVector(binString, 2) ); } - - | str[s,false] - { expr = MK_CONST( ::CVC4::String(s, true) ); } - | FP_RNE_TOK { expr = MK_CONST(roundNearestTiesToEven); } - | FP_RNA_TOK { expr = MK_CONST(roundNearestTiesToAway); } - | FP_RTP_TOK { expr = MK_CONST(roundTowardPositive); } - | FP_RTN_TOK { expr = MK_CONST(roundTowardNegative); } - | FP_RTZ_TOK { expr = MK_CONST(roundTowardZero); } - | FP_RNE_FULL_TOK { expr = MK_CONST(roundNearestTiesToEven); } - | FP_RNA_FULL_TOK { expr = MK_CONST(roundNearestTiesToAway); } - | FP_RTP_FULL_TOK { expr = MK_CONST(roundTowardPositive); } - | FP_RTN_FULL_TOK { expr = MK_CONST(roundTowardNegative); } - | FP_RTZ_FULL_TOK { expr = MK_CONST(roundTowardZero); } - - | REAL_PI_TOK { - expr = EXPR_MANAGER->mkNullaryOperator(EXPR_MANAGER->realType(), kind::PI); + { + assert(AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0); + std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); + atomTerm = SOLVER->mkBitVector(hexStr, 16); } - - | RENOSTR_TOK - { std::vector< Expr > nvec; - expr = MK_EXPR( CVC4::kind::REGEXP_EMPTY, nvec ); + | BINARY_LITERAL + { + assert(AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0); + std::string binStr = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); + atomTerm = SOLVER->mkBitVector(binStr, 2); + } + + // Floating-point rounding mode constants + | FP_RNE_TOK { atomTerm = SOLVER->mkConst(api::ROUND_NEAREST_TIES_TO_EVEN); } + | FP_RNA_TOK { atomTerm = SOLVER->mkConst(api::ROUND_NEAREST_TIES_TO_AWAY); } + | FP_RTP_TOK { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_POSITIVE); } + | FP_RTN_TOK { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_NEGATIVE); } + | FP_RTZ_TOK { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_ZERO); } + | FP_RNE_FULL_TOK { atomTerm = SOLVER->mkConst(api::ROUND_NEAREST_TIES_TO_EVEN); } + | FP_RNA_FULL_TOK { atomTerm = SOLVER->mkConst(api::ROUND_NEAREST_TIES_TO_AWAY); } + | FP_RTP_FULL_TOK { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_POSITIVE); } + | FP_RTN_FULL_TOK { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_NEGATIVE); } + | FP_RTZ_FULL_TOK { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_ZERO); } + + // String constant + | str[s,false] { atomTerm = SOLVER->mkString(s, true); } + + // Regular expression constants + | RENOSTR_TOK { atomTerm = SOLVER->mkRegexpEmpty(); } + | REALLCHAR_TOK { atomTerm = SOLVER->mkRegexpSigma(); } + + // Set constants + | EMPTYSET_TOK { atomTerm = SOLVER->mkEmptySet(SOLVER->getNullSort()); } + | UNIVSET_TOK + { + // the Boolean sort is a placeholder here since we don't have type info + // without type annotation + atomTerm = SOLVER->mkUniverseSet(SOLVER->getBooleanSort()); } - | REALLCHAR_TOK - { std::vector< Expr > nvec; - expr = MK_EXPR( CVC4::kind::REGEXP_SIGMA, nvec ); + // Separation logic constants + | NILREF_TOK + { + // the Boolean sort is a placeholder here since we don't have type info + // without type annotation + atomTerm = SOLVER->mkSepNil(SOLVER->getBooleanSort()); } - | EMPTYSET_TOK - { expr = MK_CONST( ::CVC4::EmptySet(Type())); } - - | UNIVSET_TOK - { //booleanType is placeholder here since we don't have type info without type annotation - expr = EXPR_MANAGER->mkNullaryOperator(EXPR_MANAGER->booleanType(), kind::UNIVERSE_SET); } - - | NILREF_TOK - { //booleanType is placeholder here since we don't have type info without type annotation - expr = EXPR_MANAGER->mkNullaryOperator(EXPR_MANAGER->booleanType(), kind::SEP_NIL); } - // NOTE: Theory constants go here + // NOTE: Theory constants go here + // Empty tuple constant | TUPLE_CONST_TOK - { std::vector<Type> types; - DatatypeType t = EXPR_MANAGER->mkTupleType(types); - const Datatype& dt = t.getDatatype(); - args.insert(args.begin(), dt[0].getConstructor()); - expr = MK_EXPR(kind::APPLY_CONSTRUCTOR, args); + { + atomTerm = SOLVER->mkTuple(std::vector<api::Sort>(), + std::vector<api::Term>()); } - ; /** diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt index 8a6be70b9..ca3c59750 100644 --- a/test/unit/api/CMakeLists.txt +++ b/test/unit/api/CMakeLists.txt @@ -1,7 +1,8 @@ #-----------------------------------------------------------------------------# # Add unit tests +cvc4_add_unit_test_black(datatype_api_black api) +cvc4_add_unit_test_black(opterm_black api) cvc4_add_unit_test_black(solver_black api) cvc4_add_unit_test_black(sort_black api) cvc4_add_unit_test_black(term_black api) -cvc4_add_unit_test_black(opterm_black api) diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h new file mode 100644 index 000000000..bca6a35ce --- /dev/null +++ b/test/unit/api/datatype_api_black.h @@ -0,0 +1,57 @@ +/********************* */ +/*! \file datatype_api_black.h + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 Black box testing of the datatype classes of the C++ API. + ** + ** Black box testing of the datatype classes of the C++ API. + **/ + +#include <cxxtest/TestSuite.h> + +#include "api/cvc4cpp.h" + +using namespace CVC4::api; + +class DatatypeBlack : public CxxTest::TestSuite +{ + public: + void setUp() override; + void tearDown() override; + + void testMkDatatypeSort(); + + private: + Solver d_solver; +}; + +void DatatypeBlack::setUp() {} + +void DatatypeBlack::tearDown() {} + +void DatatypeBlack::testMkDatatypeSort() +{ + DatatypeDecl dtypeSpec("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); + cons.addSelector(head); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + Sort listSort = d_solver.mkDatatypeSort(dtypeSpec); + Datatype d = listSort.getDatatype(); + DatatypeConstructor consConstr = d[0]; + DatatypeConstructor nilConstr = d[1]; + TS_ASSERT_THROWS(d[2], CVC4ApiException&); + TS_ASSERT(consConstr.isResolved()); + TS_ASSERT(nilConstr.isResolved()); + TS_ASSERT_THROWS_NOTHING(consConstr.getConstructorTerm()); + TS_ASSERT_THROWS_NOTHING(nilConstr.getConstructorTerm()); +} diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index d4082163a..76388d48f 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file api_guards_black.h +/*! \file solver_black.h ** \verbatim ** Top contributors (to current version): ** Aina Niemetz @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of the guards of the C++ API functions. + ** \brief Black box testing of the Solver class of the C++ API. ** - ** Black box testing of the guards of the C++ API functions. + ** Black box testing of the Solver class of the C++ API. **/ #include <cxxtest/TestSuite.h> @@ -29,10 +29,11 @@ class SolverBlack : public CxxTest::TestSuite void testGetBooleanSort(); void testGetIntegerSort(); + void testGetNullSort(); void testGetRealSort(); void testGetRegExpSort(); - void testGetStringSort(); void testGetRoundingmodeSort(); + void testGetStringSort(); void testMkArraySort(); void testMkBitVectorSort(); @@ -49,20 +50,22 @@ class SolverBlack : public CxxTest::TestSuite void testMkUninterpretedSort(); void testMkBitVector(); - void testMkBoundVar(); void testMkBoolean(); + void testMkBoundVar(); void testMkConst(); void testMkEmptySet(); void testMkFalse(); + void testMkFloatingPoint(); void testMkPi(); void testMkReal(); void testMkRegexpEmpty(); void testMkRegexpSigma(); void testMkSepNil(); void testMkString(); - void testMkUniverseSet(); void testMkTerm(); void testMkTrue(); + void testMkTuple(); + void testMkUniverseSet(); void testMkVar(); void testDeclareFun(); @@ -88,6 +91,11 @@ void SolverBlack::testGetIntegerSort() TS_ASSERT_THROWS_NOTHING(d_solver.getIntegerSort()); } +void SolverBlack::testGetNullSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.getNullSort()); +} + void SolverBlack::testGetRealSort() { TS_ASSERT_THROWS_NOTHING(d_solver.getRealSort()); @@ -248,6 +256,10 @@ void SolverBlack::testMkBitVector() TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVector(size2, val2)); TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVector("1010", 2)); TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVector("1010", 16)); + TS_ASSERT_THROWS(d_solver.mkBitVector(8, "101010101", 2), CVC4ApiException&); + TS_ASSERT_EQUALS(d_solver.mkBitVector(8, "01010101", 2).toString(), + "0bin01010101"); + TS_ASSERT_EQUALS(d_solver.mkBitVector(8, "F", 16).toString(), "0bin00001111"); } void SolverBlack::testMkBoundVar() @@ -411,6 +423,26 @@ void SolverBlack::testMkFalse() TS_ASSERT_THROWS_NOTHING(d_solver.mkFalse()); } +void SolverBlack::testMkFloatingPoint() +{ + if (CVC4::Configuration::isBuiltWithSymFPU()) + { + TS_ASSERT_THROWS_NOTHING(d_solver.mkPosInf(3, 5)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkNegInf(3, 5)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkNaN(3, 5)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkPosInf(3, 5)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkNegZero(3, 5)); + } + else + { + TS_ASSERT_THROWS(d_solver.mkPosInf(3, 5), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkNegInf(3, 5), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkNaN(3, 5), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkPosInf(3, 5), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkNegZero(3, 5), CVC4ApiException&); + } +} + void SolverBlack::testMkOpTerm() { // mkOpTerm(Kind kind, Kind k) @@ -507,6 +539,10 @@ void SolverBlack::testMkString() { TS_ASSERT_THROWS_NOTHING(d_solver.mkString("")); TS_ASSERT_THROWS_NOTHING(d_solver.mkString("asdfasdf")); + TS_ASSERT_EQUALS(d_solver.mkString("asdf\\nasdf").toString(), + "\"asdf\\\\nasdf\""); + TS_ASSERT_EQUALS(d_solver.mkString("asdf\\nasdf", true).toString(), + "\"asdf\\nasdf\""); } void SolverBlack::testMkTerm() @@ -599,10 +635,27 @@ void SolverBlack::testMkTrue() TS_ASSERT_THROWS_NOTHING(d_solver.mkTrue()); } +void SolverBlack::testMkTuple() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.mkTuple({d_solver.mkBitVectorSort(3)}, + {d_solver.mkBitVector("101", 2)})); + TS_ASSERT_THROWS_NOTHING( + d_solver.mkTuple({d_solver.getRealSort()}, {d_solver.mkReal("5")})); + + TS_ASSERT_THROWS(d_solver.mkTuple({}, {d_solver.mkBitVector("101", 2)}), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkTuple({d_solver.mkBitVectorSort(4)}, + {d_solver.mkBitVector("101", 2)}), + CVC4ApiException&); + TS_ASSERT_THROWS( + d_solver.mkTuple({d_solver.getIntegerSort()}, {d_solver.mkReal("5.3")}), + CVC4ApiException&); +} + void SolverBlack::testMkUniverseSet() { TS_ASSERT_THROWS(d_solver.mkUniverseSet(Sort()), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkUniverseSet(d_solver.getBooleanSort()), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver.mkUniverseSet(d_solver.getBooleanSort())); } void SolverBlack::testMkVar() |