summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/parser/smt2/Smt2.g43
-rw-r--r--src/parser/smt2/smt2.cpp42
-rw-r--r--src/parser/smt2/smt2.h8
-rw-r--r--src/printer/smt2/smt2_printer.cpp18
-rw-r--r--test/regress/CMakeLists.txt1
-rw-r--r--test/regress/regress0/datatypes/tuple_update.smt26
6 files changed, 81 insertions, 37 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 8f9e01c6c..674aeca1f 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1577,12 +1577,13 @@ termNonVariable[cvc5::api::Term& expr, cvc5::api::Term& expr2]
* - For declared functions f, we return (2).
* - For indexed functions like testers (_ is C) and bitvector extract
* (_ extract n m), we return (3) for the appropriate operator.
- * - For tuple selectors (_ tupSel n), we return (1) and (3). api::Kind is set to
- * APPLY_SELECTOR, and expr is set to n, which is to be interpreted by the
- * caller as the n^th generic tuple selector. We do this since there is no
- * AST expression representing generic tuple select, and we do not have enough
- * type information at this point to know the type of the tuple we will be
- * selecting from.
+ * - For tuple selectors (_ tuple_select n) and updaters (_ tuple_update n), we
+ * return (1) and (3). api::Kind is set to APPLY_SELECTOR or APPLY_UPDATER
+ * respectively, and expr is set to n, which is to be interpreted by the
+ * caller as the n^th generic tuple selector or updater. We do this since there
+ * is no AST expression representing generic tuple select, and we do not have
+ * enough type information at this point to know the type of the tuple we will
+ * be selecting from.
*
* (Ascripted Identifiers)
*
@@ -1703,7 +1704,35 @@ identifier[cvc5::ParseOp& p]
}
| sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
{
- p.d_op = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals);
+ std::string opName = AntlrInput::tokenText($sym);
+ api::Kind k = PARSER_STATE->getIndexedOpKind(opName);
+ if (k == api::APPLY_UPDATER)
+ {
+ // we adopt a special syntax (_ tuple_update n) for tuple updaters
+ if (numerals.size() != 1)
+ {
+ PARSER_STATE->parseError(
+ "Unexpected syntax for tuple selector or updater.");
+ }
+ // The operator is dependent upon inferring the type of the arguments,
+ // and hence the type is not available yet. Hence, we remember the
+ // index as a numeral in the parse operator.
+ p.d_kind = k;
+ p.d_expr = SOLVER->mkInteger(numerals[0]);
+ }
+ else if (numerals.size() == 1)
+ {
+ p.d_op = SOLVER->mkOp(k, numerals[0]);
+ }
+ else if (numerals.size() == 2)
+ {
+ p.d_op = SOLVER->mkOp(k, numerals[0], numerals[1]);
+ }
+ else
+ {
+ PARSER_STATE->parseError(
+ "Unexpected number of numerals for indexed symbol.");
+ }
}
)
RPAREN_TOK
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 2fd4a5596..40716d908 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -135,6 +135,7 @@ void Smt2::addDatatypesOperators()
{
Parser::addOperator(api::APPLY_UPDATER);
addOperator(api::DT_SIZE, "dt.size");
+ addIndexedOperator(api::APPLY_UPDATER, api::APPLY_UPDATER, "tuple_update");
}
}
@@ -382,25 +383,15 @@ api::Term Smt2::mkIndexedConstant(const std::string& name,
return api::Term();
}
-api::Op Smt2::mkIndexedOp(const std::string& name,
- const std::vector<uint64_t>& numerals)
+api::Kind Smt2::getIndexedOpKind(const std::string& name)
{
const auto& kIt = d_indexedOpKindMap.find(name);
if (kIt != d_indexedOpKindMap.end())
{
- api::Kind k = (*kIt).second;
- if (numerals.size() == 1)
- {
- return d_solver->mkOp(k, numerals[0]);
- }
- else if (numerals.size() == 2)
- {
- return d_solver->mkOp(k, numerals[0], numerals[1]);
- }
+ return (*kIt).second;
}
-
parseError(std::string("Unknown indexed function `") + name + "'");
- return api::Op();
+ return api::UNDEFINED_KIND;
}
api::Term Smt2::bindDefineFunRec(
@@ -1037,22 +1028,24 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
Debug("parser") << "applyParseOp: return store all " << ret << std::endl;
return ret;
}
- else if (p.d_kind == api::APPLY_SELECTOR && !p.d_expr.isNull())
+ else if ((p.d_kind == api::APPLY_SELECTOR || p.d_kind == api::APPLY_UPDATER)
+ && !p.d_expr.isNull())
{
// tuple selector case
if (!p.d_expr.isUInt64Value())
{
- parseError("index of tupSel is larger than size of uint64_t");
+ parseError(
+ "index of tuple select or update is larger than size of uint64_t");
}
uint64_t n = p.d_expr.getUInt64Value();
- if (args.size() != 1)
+ if (args.size() != (p.d_kind == api::APPLY_SELECTOR ? 1 : 2))
{
- parseError("tupSel should only be applied to one tuple argument");
+ parseError("wrong number of arguments for tuple select or update");
}
api::Sort t = args[0].getSort();
if (!t.isTuple())
{
- parseError("tupSel applied to non-tuple");
+ parseError("tuple select or update applied to non-tuple");
}
size_t length = t.getTupleLength();
if (n >= length)
@@ -1062,8 +1055,17 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
parseError(ss.str());
}
const api::Datatype& dt = t.getDatatype();
- api::Term ret = d_solver->mkTerm(
- api::APPLY_SELECTOR, dt[0][n].getSelectorTerm(), args[0]);
+ api::Term ret;
+ if (p.d_kind == api::APPLY_SELECTOR)
+ {
+ ret = d_solver->mkTerm(
+ api::APPLY_SELECTOR, dt[0][n].getSelectorTerm(), args[0]);
+ }
+ else
+ {
+ ret = d_solver->mkTerm(
+ api::APPLY_UPDATER, dt[0][n].getUpdaterTerm(), args[0], args[1]);
+ }
Debug("parser") << "applyParseOp: return selector " << ret << std::endl;
return ret;
}
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 97eb95c00..fd68732fe 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -121,15 +121,13 @@ class Smt2 : public Parser
const std::vector<uint64_t>& numerals);
/**
- * Creates an indexed operator term, e.g. (_ extract 5 0).
+ * Creates an indexed operator kind, e.g. BITVECTOR_EXTRACT for "extract".
*
* @param name The name of the operator (e.g. "extract")
- * @param numerals The parameters for the operator (e.g. [5, 0])
- * @return The operator term corresponding to the indexed operator or a parse
+ * @return The kind corresponding to the indexed operator or a parse
* error if the name is not valid.
*/
- api::Op mkIndexedOp(const std::string& name,
- const std::vector<uint64_t>& numerals);
+ api::Kind getIndexedOpKind(const std::string& name);
/**
* Returns the expression that name should be interpreted as.
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 6217276b1..3c0fe838b 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -791,11 +791,19 @@ void Smt2Printer::toStream(std::ostream& out,
size_t index = DType::indexOf(op);
const DType& dt = DType::datatypeOf(op);
size_t cindex = DType::cindexOf(op);
- out << "(_ update ";
- toStream(out,
- dt[cindex][index].getSelector(),
- toDepth < 0 ? toDepth : toDepth - 1);
- out << ") ";
+ if (dt.isTuple())
+ {
+ stillNeedToPrintParams = false;
+ out << "(_ tuple_update " << DType::indexOf(op) << ") ";
+ }
+ else
+ {
+ out << "(_ update ";
+ toStream(out,
+ dt[cindex][index].getSelector(),
+ toDepth < 0 ? toDepth : toDepth - 1);
+ out << ") ";
+ }
}
break;
case kind::APPLY_SELECTOR_TOTAL:
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 301e26bf9..47d352695 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -522,6 +522,7 @@ set(regress_0_tests
regress0/datatypes/tuple-no-clash.cvc
regress0/datatypes/tuple-record-bug.cvc
regress0/datatypes/tuple.cvc
+ regress0/datatypes/tuple_update.smt2
regress0/datatypes/tuples-empty.smt2
regress0/datatypes/tuples-multitype.smt2
regress0/datatypes/typed_v10l30054.cvc
diff --git a/test/regress/regress0/datatypes/tuple_update.smt2 b/test/regress/regress0/datatypes/tuple_update.smt2
new file mode 100644
index 000000000..9812da728
--- /dev/null
+++ b/test/regress/regress0/datatypes/tuple_update.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () (Tuple Int Int))
+(declare-fun y () (Tuple Int Int))
+(assert (= ((_ tuple_update 0) x 1) ((_ tuple_update 1) y 2)))
+(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback