diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 15 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 6 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 39 | ||||
-rw-r--r-- | src/parser/tptp/Tptp.g | 16 |
4 files changed, 30 insertions, 46 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 292871d2a..0bb41b483 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -2177,13 +2177,6 @@ simpleTerm[CVC4::api::Term& f] * literals, we can use the push/pop scope. */ /* PARSER_STATE->popScope(); */ t = SOLVER->mkArraySort(t, t2); - if(!f.isValue()) { - std::stringstream ss; - ss << "expected constant term inside array constant, but found " - << "nonconstant term" << std::endl - << "the term: " << f; - PARSER_STATE->parseError(ss.str()); - } if(!t2.isComparableTo(f.getSort())) { std::stringstream ss; ss << "type mismatch inside array constant term:" << std::endl @@ -2207,18 +2200,12 @@ simpleTerm[CVC4::api::Term& f] std::stringstream strRat; strRat << r; f = SOLVER->mkReal(strRat.str()); - if(f.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. - f = MK_TERM(api::DIVISION, f, SOLVER->mkReal(1)); - } } | INTEGER_LITERAL { Rational r = AntlrInput::tokenToRational($INTEGER_LITERAL); std::stringstream strRat; strRat << r; - f = SOLVER->mkReal(strRat.str()); + f = SOLVER->mkInteger(strRat.str()); } /* bitvector literals */ | HEX_LITERAL diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 7c1c5dc3e..7647f8e53 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1710,7 +1710,7 @@ identifier[CVC4::ParseOp& p] // we adopt a special syntax (_ tupSel n) p.d_kind = api::APPLY_SELECTOR; // put m in expr so that the caller can deal with this case - p.d_expr = SOLVER->mkReal(AntlrInput::tokenToUnsigned($m)); + p.d_expr = SOLVER->mkInteger(AntlrInput::tokenToUnsigned($m)); } | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals] { @@ -1735,7 +1735,7 @@ termAtomic[CVC4::api::Term& atomTerm] : INTEGER_LITERAL { std::string intStr = AntlrInput::tokenText($INTEGER_LITERAL); - atomTerm = SOLVER->mkReal(intStr); + atomTerm = SOLVER->mkInteger(intStr); } | DECIMAL_LITERAL { @@ -1830,7 +1830,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr] { std::stringstream sIntLit; sIntLit << $INTEGER_LITERAL; - api::Term n = SOLVER->mkReal(sIntLit.str()); + api::Term n = SOLVER->mkInteger(sIntLit.str()); std::vector<api::Term> values; values.push_back( n ); std::string attr_name(AntlrInput::tokenText($tok)); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 629164593..edeb47f06 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1055,33 +1055,22 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) parseError("Too many arguments to array constant."); } api::Term constVal = args[0]; - if (!constVal.isValue()) + + // To parse array constants taking reals whose values are specified by + // rationals, e.g. ((as const (Array Int Real)) (/ 1 3)), we must handle + // the fact that (/ 1 3) is the division of constants 1 and 3, and not + // the resulting constant rational value. Thus, we must construct the + // resulting rational here. This also is applied for integral real values + // like 5.0 which are converted to (/ 5 1) to distinguish them from + // integer constants. We must ensure numerator and denominator are + // constant and the denominator is non-zero. + if (constVal.getKind() == api::DIVISION) { - // To parse array constants taking reals whose values are specified by - // rationals, e.g. ((as const (Array Int Real)) (/ 1 3)), we must handle - // the fact that (/ 1 3) is the division of constants 1 and 3, and not - // the resulting constant rational value. Thus, we must construct the - // resulting rational here. This also is applied for integral real values - // like 5.0 which are converted to (/ 5 1) to distinguish them from - // integer constants. We must ensure numerator and denominator are - // constant and the denominator is non-zero. - if (constVal.getKind() == api::DIVISION && constVal[0].isValue() - && constVal[1].isValue() - && !constVal[1].getExpr().getConst<Rational>().isZero()) - { - std::stringstream sdiv; - sdiv << constVal[0] << "/" << constVal[1]; - constVal = d_solver->mkReal(sdiv.str()); - } - if (!constVal.isValue()) - { - std::stringstream ss; - ss << "expected constant term inside array constant, but found " - << "nonconstant term:" << std::endl - << "the term: " << constVal; - parseError(ss.str()); - } + std::stringstream sdiv; + sdiv << constVal[0] << "/" << constVal[1]; + constVal = d_solver->mkReal(sdiv.str()); } + if (!p.d_type.getArrayElementSort().isComparableTo(constVal.getSort())) { std::stringstream ss; diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index b99376685..8e29c25f1 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -477,7 +477,7 @@ definedPred[CVC4::ParseOp& p] api::Term body = MK_TERM(api::AND, MK_TERM(api::NOT, - MK_TERM(api::EQUAL, r, SOLVER->mkReal(0))), + MK_TERM(api::EQUAL, r, SOLVER->mkInteger(0))), MK_TERM(api::EQUAL, qr, MK_TERM(api::MULT, n, rr))); api::Term bvl = MK_TERM(api::BOUND_VAR_LIST, q, r); body = MK_TERM(api::EXISTS, bvl, body); @@ -537,7 +537,7 @@ thfDefinedPred[CVC4::ParseOp& p] api::Term body = MK_TERM( api::AND, MK_TERM(api::NOT, - MK_TERM(api::EQUAL, r, SOLVER->mkReal(0))), + MK_TERM(api::EQUAL, r, SOLVER->mkInteger(0))), MK_TERM(api::EQUAL, qr, MK_TERM(api::MULT, n, rr))); api::Term bvl = MK_TERM(api::BOUND_VAR_LIST, q, r); body = MK_TERM(api::EXISTS, bvl, body); @@ -708,7 +708,7 @@ definedFun[CVC4::ParseOp& p] n, SOLVER->mkReal(2)), SOLVER->mkReal(1, 2))), - SOLVER->mkReal(2)))); + SOLVER->mkInteger(2)))); p.d_kind = api::LAMBDA; p.d_expr = MK_TERM(api::LAMBDA, formals, expr); } @@ -1747,7 +1747,15 @@ NUMBER : ( SIGN[pos]? num=DECIMAL { std::stringstream ss; ss << ( pos ? "" : "-" ) << AntlrInput::tokenText($num); - PARSER_STATE->d_tmp_expr = SOLVER->mkReal(ss.str()); + std::string str = ss.str(); + if (str.find(".") == std::string::npos) + { + PARSER_STATE->d_tmp_expr = SOLVER->mkInteger(str); + } + else + { + PARSER_STATE->d_tmp_expr = SOLVER->mkReal(str); + } } | SIGN[pos]? num=DECIMAL DOT den=DECIMAL (EXPONENT SIGN[posE]? e=DECIMAL)? { |