summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/cvc/Cvc.g15
-rw-r--r--src/parser/smt2/Smt2.g6
-rw-r--r--src/parser/smt2/smt2.cpp39
-rw-r--r--src/parser/tptp/Tptp.g16
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)?
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback