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?
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?
/* 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(); }
}
}
-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
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)
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)
}
}
+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);
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
}
}
+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
{
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. !!!
/**
* Constructor.
* @param ctor the internal datatype constructor to be wrapped
- * @return thte DatatypeConstructor
+ * @return the DatatypeConstructor
*/
DatatypeConstructor(const CVC4::DatatypeConstructor& ctor);
*/
~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
*/
~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,
/* Sorts Handling */
/* .................................................................... */
+ /**
+ * @return sort null
+ */
+ Sort getNullSort() const;
+
/**
* @return sort Boolean
*/
*/
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 */
/* .................................................................... */
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)
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)
/**
* 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.
/**
* 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
*/
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;
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. */
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. */
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));
/** 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;
};/* struct myExpr */
}/* CVC4::parser::smt2 namespace */
}/* CVC4::parser namespace */
+
+ namespace api {
+ class Term;
+ }
}/* CVC4 namespace */
}/* @parser::includes */
#include <unordered_set>
#include <vector>
+#include "api/cvc4cpp.h"
#include "base/output.h"
#include "expr/expr.h"
#include "expr/kind.h"
#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) {
std::vector< Expr > let_vars;
bool readingLet = false;
std::string s;
- CVC4::Expr atomExpr;
+ CVC4::api::Term atomTerm;
}
: LPAREN_TOK
//read operator
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
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
| 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(); }
;
* 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>());
}
-
;
/**
#-----------------------------------------------------------------------------#
# 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)
--- /dev/null
+/********************* */
+/*! \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());
+}
/********************* */
-/*! \file api_guards_black.h
+/*! \file solver_black.h
** \verbatim
** Top contributors (to current version):
** Aina Niemetz
** 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>
void testGetBooleanSort();
void testGetIntegerSort();
+ void testGetNullSort();
void testGetRealSort();
void testGetRegExpSort();
- void testGetStringSort();
void testGetRoundingmodeSort();
+ void testGetStringSort();
void testMkArraySort();
void testMkBitVectorSort();
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();
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());
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()
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)
{
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()
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()
projects / cvc5.git / commitdiff