diff options
36 files changed, 257 insertions, 426 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 6ee1409d6..18db5d5ab 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -243,8 +243,7 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{ {APPLY_SELECTOR, cvc5::Kind::APPLY_SELECTOR}, {APPLY_CONSTRUCTOR, cvc5::Kind::APPLY_CONSTRUCTOR}, {APPLY_TESTER, cvc5::Kind::APPLY_TESTER}, - {TUPLE_UPDATE, cvc5::Kind::TUPLE_UPDATE}, - {RECORD_UPDATE, cvc5::Kind::RECORD_UPDATE}, + {APPLY_UPDATER, cvc5::Kind::APPLY_UPDATER}, {DT_SIZE, cvc5::Kind::DT_SIZE}, {TUPLE_PROJECT, cvc5::Kind::TUPLE_PROJECT}, /* Separation Logic ---------------------------------------------------- */ @@ -550,10 +549,7 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction> {cvc5::Kind::APPLY_CONSTRUCTOR, APPLY_CONSTRUCTOR}, {cvc5::Kind::APPLY_SELECTOR_TOTAL, INTERNAL_KIND}, {cvc5::Kind::APPLY_TESTER, APPLY_TESTER}, - {cvc5::Kind::TUPLE_UPDATE_OP, TUPLE_UPDATE}, - {cvc5::Kind::TUPLE_UPDATE, TUPLE_UPDATE}, - {cvc5::Kind::RECORD_UPDATE_OP, RECORD_UPDATE}, - {cvc5::Kind::RECORD_UPDATE, RECORD_UPDATE}, + {cvc5::Kind::APPLY_UPDATER, APPLY_UPDATER}, {cvc5::Kind::DT_SIZE, DT_SIZE}, {cvc5::Kind::TUPLE_PROJECT, TUPLE_PROJECT}, /* Separation Logic ------------------------------------------------ */ @@ -661,8 +657,7 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction> /* Set of kinds for indexed operators */ const static std::unordered_set<Kind> s_indexed_kinds( - {RECORD_UPDATE, - DIVISIBLE, + {DIVISIBLE, IAND, BITVECTOR_REPEAT, BITVECTOR_ZERO_EXTEND, @@ -672,7 +667,6 @@ const static std::unordered_set<Kind> s_indexed_kinds( INT_TO_BITVECTOR, FLOATINGPOINT_TO_UBV, FLOATINGPOINT_TO_SBV, - TUPLE_UPDATE, BITVECTOR_EXTRACT, FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, FLOATINGPOINT_TO_FP_FLOATINGPOINT, @@ -718,7 +712,8 @@ bool isDefinedKind(Kind k) { return k > UNDEFINED_KIND && k < LAST_KIND; } bool isApplyKind(cvc5::Kind k) { return (k == cvc5::Kind::APPLY_UF || k == cvc5::Kind::APPLY_CONSTRUCTOR - || k == cvc5::Kind::APPLY_SELECTOR || k == cvc5::Kind::APPLY_TESTER); + || k == cvc5::Kind::APPLY_SELECTOR || k == cvc5::Kind::APPLY_TESTER + || k == cvc5::Kind::APPLY_UPDATER); } #ifdef CVC5_ASSERTIONS @@ -1194,6 +1189,15 @@ bool Sort::isTester() const CVC5_API_TRY_CATCH_END; } +bool Sort::isUpdater() const +{ + CVC5_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isUpdater(); + //////// + CVC5_API_TRY_CATCH_END; +} + bool Sort::isFunction() const { CVC5_API_TRY_CATCH_BEGIN; @@ -1852,7 +1856,6 @@ size_t Op::getNumIndices() const switch (k) { case DIVISIBLE: size = 1; break; - case RECORD_UPDATE: size = 1; break; case BITVECTOR_REPEAT: size = 1; break; case BITVECTOR_ZERO_EXTEND: size = 1; break; case BITVECTOR_SIGN_EXTEND: size = 1; break; @@ -1862,7 +1865,6 @@ size_t Op::getNumIndices() const case IAND: size = 1; break; case FLOATINGPOINT_TO_UBV: size = 1; break; case FLOATINGPOINT_TO_SBV: size = 1; break; - case TUPLE_UPDATE: size = 1; break; case REGEXP_REPEAT: size = 1; break; case BITVECTOR_EXTRACT: size = 2; break; case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: size = 2; break; @@ -1892,12 +1894,10 @@ std::string Op::getIndices() const CVC5_API_CHECK(!d_node->isNull()) << "Expecting a non-null internal expression. This Op is not indexed."; Kind k = intToExtKind(d_node->getKind()); - CVC5_API_CHECK(k == DIVISIBLE || k == RECORD_UPDATE) - << "Can't get string index from" - << " kind " << kindToString(k); + CVC5_API_CHECK(k == DIVISIBLE) << "Can't get string index from" + << " kind " << kindToString(k); //////// all checks before this line - return k == DIVISIBLE ? d_node->getConst<Divisible>().k.toString() - : d_node->getConst<RecordUpdate>().getField(); + return d_node->getConst<Divisible>().k.toString(); //////// CVC5_API_TRY_CATCH_END; } @@ -1938,7 +1938,6 @@ uint32_t Op::getIndices() const case FLOATINGPOINT_TO_SBV: i = d_node->getConst<FloatingPointToSBV>().d_bv_size.d_size; break; - case TUPLE_UPDATE: i = d_node->getConst<TupleUpdate>().getIndex(); break; case REGEXP_REPEAT: i = d_node->getConst<RegExpRepeat>().d_repeatAmount; break; @@ -3062,6 +3061,15 @@ Term DatatypeSelector::getSelectorTerm() const //////// CVC5_API_TRY_CATCH_END; } +Term DatatypeSelector::getUpdaterTerm() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return Term(d_solver, d_stor->getUpdater()); + //////// + CVC5_API_TRY_CATCH_END; +} Sort DatatypeSelector::getRangeSort() const { @@ -3424,7 +3432,17 @@ Term Datatype::getConstructorTerm(const std::string& name) const CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; //////// all checks before this line - return getConstructor(name).getConstructorTerm(); + return getConstructorForName(name).getConstructorTerm(); + //////// + CVC5_API_TRY_CATCH_END; +} + +DatatypeSelector Datatype::getSelector(const std::string& name) const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return getSelectorForName(name); //////// CVC5_API_TRY_CATCH_END; } @@ -3579,6 +3597,30 @@ DatatypeConstructor Datatype::getConstructorForName( return DatatypeConstructor(d_solver, (*d_dtype)[index]); } +DatatypeSelector Datatype::getSelectorForName(const std::string& name) const +{ + bool foundSel = false; + size_t index = 0; + size_t sindex = 0; + for (size_t i = 0, ncons = getNumConstructors(); i < ncons; i++) + { + int si = (*d_dtype)[i].getSelectorIndexForName(name); + if (si >= 0) + { + sindex = static_cast<size_t>(si); + index = i; + foundSel = true; + break; + } + } + if (!foundSel) + { + CVC5_API_CHECK(foundSel) + << "No select " << name << " for datatype " << getName() << " exists"; + } + return DatatypeSelector(d_solver, (*d_dtype)[index][sindex]); +} + Datatype::const_iterator::const_iterator(const Solver* slv, const cvc5::DType& dtype, bool begin) @@ -5806,29 +5848,18 @@ Op Solver::mkOp(Kind kind, const std::string& arg) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_KIND_CHECK(kind); - CVC5_API_KIND_CHECK_EXPECTED((kind == RECORD_UPDATE) || (kind == DIVISIBLE), - kind) - << "RECORD_UPDATE or DIVISIBLE"; + CVC5_API_KIND_CHECK_EXPECTED((kind == DIVISIBLE), kind) << "DIVISIBLE"; //////// all checks before this line Op res; - if (kind == RECORD_UPDATE) - { - res = Op(this, - kind, - *mkValHelper<cvc5::RecordUpdate>(cvc5::RecordUpdate(arg)).d_node); - } - else - { - /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP - * throws an std::invalid_argument exception. For consistency, we treat it - * as invalid. */ - CVC5_API_ARG_CHECK_EXPECTED(arg != ".", arg) - << "a string representing an integer, real or rational value."; - res = Op(this, - kind, - *mkValHelper<cvc5::Divisible>(cvc5::Divisible(cvc5::Integer(arg))) - .d_node); - } + /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP + * throws an std::invalid_argument exception. For consistency, we treat it + * as invalid. */ + CVC5_API_ARG_CHECK_EXPECTED(arg != ".", arg) + << "a string representing an integer, real or rational value."; + res = Op(this, + kind, + *mkValHelper<cvc5::Divisible>(cvc5::Divisible(cvc5::Integer(arg))) + .d_node); return res; //////// CVC5_API_TRY_CATCH_END; @@ -5905,11 +5936,6 @@ Op Solver::mkOp(Kind kind, uint32_t arg) const *mkValHelper<cvc5::FloatingPointToSBV>(cvc5::FloatingPointToSBV(arg)) .d_node); break; - case TUPLE_UPDATE: - res = Op(this, - kind, - *mkValHelper<cvc5::TupleUpdate>(cvc5::TupleUpdate(arg)).d_node); - break; case REGEXP_REPEAT: res = Op(this, diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 1e857085b..16f58ee80 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -399,6 +399,11 @@ class CVC5_EXPORT Sort */ bool isTester() const; /** + * Is this a datatype updater sort? + * @return true if the sort is a datatype updater sort + */ + bool isUpdater() const; + /** * Is this a function sort? * @return true if the sort is a function sort */ @@ -1575,6 +1580,7 @@ class CVC5_EXPORT DatatypeDecl */ class CVC5_EXPORT DatatypeSelector { + friend class Datatype; friend class DatatypeConstructor; friend class Solver; @@ -1598,6 +1604,12 @@ class CVC5_EXPORT DatatypeSelector */ Term getSelectorTerm() const; + /** + * Get the upater operator of this datatype selector. + * @return the updater term + */ + Term getUpdaterTerm() const; + /** @return the range sort of this argument. */ Sort getRangeSort() const; @@ -1908,6 +1920,15 @@ class CVC5_EXPORT Datatype */ Term getConstructorTerm(const std::string& name) const; + /** + * Get the datatype constructor with the given name. + * This is a linear search through the constructors and their selectors, so + * in case of multiple, similarly-named selectors, the first is returned. + * @param name the name of the datatype selector + * @return the datatype selector with the given name + */ + DatatypeSelector getSelector(const std::string& name) const; + /** @return the name of this Datatype. */ std::string getName() const; @@ -2070,6 +2091,13 @@ class CVC5_EXPORT Datatype DatatypeConstructor getConstructorForName(const std::string& name) const; /** + * Return selector for name. + * @param name The name of selector to find + * @return the selector object for the name + */ + DatatypeSelector getSelectorForName(const std::string& name) const; + + /** * Helper for isNull checks. This prevents calling an API function with * CVC5_API_CHECK_NOT_NULL */ @@ -2890,7 +2918,6 @@ class CVC5_EXPORT Solver /** * Create operator of kind: - * - RECORD_UPDATE * - DIVISIBLE (to support arbitrary precision integers) * See enum Kind for a description of the parameters. * @param kind the kind of the operator diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index f7658412c..0375b5e60 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -1918,11 +1918,11 @@ enum CVC5_EXPORT Kind : int32_t */ APPLY_CONSTRUCTOR, /** - * Datatype selector application. + * Datatype selector application, which is undefined if misapplied. * * Parameters: * - 1: Selector (operator) - * - 2: Datatype term (undefined if mis-applied) + * - 2: Datatype term * * Create with: * - `Solver::mkTerm(const Op& op, const Term& child) const` @@ -1940,56 +1940,20 @@ enum CVC5_EXPORT Kind : int32_t * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ APPLY_TESTER, -#if 0 - /* Parametric datatype term. */ - PARAMETRIC_DATATYPE, - /* type ascription, for datatype constructor applications; - * first parameter is an ASCRIPTION_TYPE, second is the datatype constructor - * application being ascribed */ - APPLY_TYPE_ASCRIPTION, -#endif - /** - * Operator for a tuple update. - * - * Parameters: - * - 1: Index of the tuple to be updated - * - * Create with: - * - `Solver::mkOp(Kind kind, uint32_t param) const` - * - * Apply tuple update. - * - * Parameters: - * - 1: Op of kind TUPLE_UPDATE (which references an index) - * - 2: Tuple - * - 3: Element to store in the tuple at the given index - * - * Create with: - * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const` - * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` - */ - TUPLE_UPDATE, /** - * Operator for a record update. + * Datatype update application, which does not change the argument if + * misapplied. * * Parameters: - * - 1: Name of the field to be updated - * - * Create with: - * - `Solver::mkOp(Kind kind, const std::string& param) const` - * - * Record update. - * - * Parameters: - * - 1: Op of kind RECORD_UPDATE (which references a field) - * - 2: Record term to update - * - 3: Element to store in the record in the given field + * - 1: Updater (operator) + * - 2: Datatype term + * - 3: Value to update a field of the datatype term with * * Create with: - * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const` - * - `Solver::mkTerm(const Op& op,, const std::vector<Term>& children) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ - RECORD_UPDATE, + APPLY_UPDATER, /** * Match expressions. * For example, the smt2 syntax match term diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 6302b7e43..e4c0eb915 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -32,6 +32,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": DatatypeConstructor operator[](const string& name) except + DatatypeConstructor getConstructor(const string& name) except + Term getConstructorTerm(const string& name) except + + DatatypeSelector getSelector(const string& name) except + size_t getNumConstructors() except + bint isParametric() except + bint isCodatatype() except + @@ -89,6 +90,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": DatatypeSelector() except + string getName() except + Term getSelectorTerm() except + + Term getUpdaterTerm() except + Sort getRangeSort() except + string toString() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 135eeb165..11742ca08 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -109,6 +109,12 @@ cdef class Datatype: term.cterm = self.cd.getConstructorTerm(name.encode()) return term + def getSelector(self, str name): + """Return a selector by name.""" + cdef DatatypeSelector ds = DatatypeSelector(self.solver) + ds.cds = self.cd.getSelector(name.encode()) + return ds + def getNumConstructors(self): """:return: number of constructors.""" return self.cd.getNumConstructors() @@ -267,6 +273,11 @@ cdef class DatatypeSelector: term.cterm = self.cds.getSelectorTerm() return term + def getUpdaterTerm(self): + cdef Term term = Term(self.solver) + term.cterm = self.cds.getUpdaterTerm() + return term + def getRangeSort(self): cdef Sort sort = Sort(self.solver) sort.csort = self.cds.getRangeSort() diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 28cf23f57..9bf63dcfc 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -112,8 +112,6 @@ libcvc5_add_sources( dtype_cons.cpp dtype_selector.h dtype_selector.cpp - record.cpp - record.h sequence.cpp sequence.h subs.cpp diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index 07b8aa5f1..c1893d3f4 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -109,7 +109,7 @@ const DType& DType::datatypeOf(Node item) size_t DType::indexOf(Node item) { Assert(item.getType().isConstructor() || item.getType().isTester() - || item.getType().isSelector()); + || item.getType().isSelector() || item.getType().isUpdater()); return indexOfInternal(item); } @@ -125,7 +125,7 @@ size_t DType::indexOfInternal(Node item) size_t DType::cindexOf(Node item) { - Assert(item.getType().isSelector()); + Assert(item.getType().isSelector() || item.getType().isUpdater()); return cindexOfInternal(item); } size_t DType::cindexOfInternal(Node item) diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 0a0781819..780fda9ab 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -724,7 +724,7 @@ TypeNode NodeManager::mkDatatypeUpdateType(TypeNode domain, TypeNode range) domain.isDatatype(), domain, "cannot create non-datatype upater type"); // It is a function type domain x range -> domain, we store only the // arguments - return mkTypeNode(kind::DT_UPDATE_TYPE, domain, range); + return mkTypeNode(kind::UPDATER_TYPE, domain, range); } TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index ) { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 8b99f5743..9952baf89 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -34,6 +34,8 @@ namespace cvc5 { +using Record = std::vector<std::pair<std::string, TypeNode>>; + namespace api { class Solver; } diff --git a/src/expr/record.cpp b/src/expr/record.cpp deleted file mode 100644 index 0792de20c..000000000 --- a/src/expr/record.cpp +++ /dev/null @@ -1,27 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Tim King - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * A class representing a record definition. - */ - -#include "expr/record.h" - -#include "base/check.h" -#include "base/output.h" - -namespace cvc5 { - -std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) { - return out << "[" << t.getField() << "]"; -} - -} // namespace cvc5 diff --git a/src/expr/record.h b/src/expr/record.h deleted file mode 100644 index ecf6c8d32..000000000 --- a/src/expr/record.h +++ /dev/null @@ -1,60 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Tim King, Mathias Preiner, Morgan Deters - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * A class representing a Record definition. - */ - -#include "cvc5_public.h" - -#ifndef CVC5__RECORD_H -#define CVC5__RECORD_H - -#include <iostream> -#include <string> -#include <vector> -#include <utility> - -// Forward Declarations -namespace cvc5 { -// This forward delcartion is required to resolve a cicular dependency with -// Record which is a referenced in a Kind file. -class TypeNode; -} // namespace cvc5 - -namespace cvc5 { - -// operators for record update -class RecordUpdate -{ - std::string d_field; - - public: - RecordUpdate(const std::string& field) : d_field(field) {} - std::string getField() const { return d_field; } - bool operator==(const RecordUpdate& t) const { return d_field == t.d_field; } - bool operator!=(const RecordUpdate& t) const { return d_field != t.d_field; } -}; /* class RecordUpdate */ - -struct RecordUpdateHashFunction -{ - inline size_t operator()(const RecordUpdate& t) const { - return std::hash<std::string>()(t.getField()); - } -}; /* struct RecordUpdateHashFunction */ - -std::ostream& operator<<(std::ostream& out, const RecordUpdate& t); - -using Record = std::vector<std::pair<std::string, TypeNode>>; - -} // namespace cvc5 - -#endif /* CVC5__RECORD_H */ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 483983e6e..bd435a392 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -249,7 +249,7 @@ bool TypeNode::isClosedEnumerable() bool TypeNode::isFirstClass() const { return getKind() != kind::CONSTRUCTOR_TYPE && getKind() != kind::SELECTOR_TYPE - && getKind() != kind::TESTER_TYPE && getKind() != kind::DT_UPDATE_TYPE + && getKind() != kind::TESTER_TYPE && getKind() != kind::UPDATER_TYPE && (getKind() != kind::TYPE_CONSTANT || (getConst<TypeConstant>() != REGEXP_TYPE && getConst<TypeConstant>() != SEXPR_TYPE)); @@ -633,10 +633,7 @@ bool TypeNode::isSelector() const { return getKind() == kind::SELECTOR_TYPE; } bool TypeNode::isTester() const { return getKind() == kind::TESTER_TYPE; } -bool TypeNode::isDatatypeUpdater() const -{ - return getKind() == kind::DT_UPDATE_TYPE; -} +bool TypeNode::isUpdater() const { return getKind() == kind::UPDATER_TYPE; } bool TypeNode::isCodatatype() const { diff --git a/src/expr/type_node.h b/src/expr/type_node.h index d73d64b43..0ab1d0217 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -652,7 +652,7 @@ public: bool isTester() const; /** Is this a datatype updater type */ - bool isDatatypeUpdater() const; + bool isUpdater() const; /** Get the internal Datatype specification from a datatype type */ const DType& getDType() const; diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 039eaf0ad..6e3332651 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1636,7 +1636,11 @@ tupleStore[cvc5::api::Term& f] | DOT ( tupleStore[f2] | recordStore[f2] ) ) | ASSIGN_TOK term[f2] ) - { f = SOLVER->mkTerm(SOLVER->mkOp(api::TUPLE_UPDATE,k), f, f2); } + { + const api::Datatype& dt = f.getSort().getDatatype(); + f = SOLVER->mkTerm( + api::APPLY_UPDATER, dt[0][k].getUpdaterTerm(), f, f2); + } ; /** @@ -1665,7 +1669,11 @@ recordStore[cvc5::api::Term& f] | DOT ( tupleStore[f2] | recordStore[f2] ) ) | ASSIGN_TOK term[f2] ) - { f = SOLVER->mkTerm(SOLVER->mkOp(api::RECORD_UPDATE,id), f, f2); } + { + const api::Datatype& dt = f.getSort().getDatatype(); + f = SOLVER->mkTerm( + api::APPLY_UPDATER, dt[0][id].getUpdaterTerm(), f, f2); + } ; /** Parses a unary minus term. */ diff --git a/src/parser/parse_op.cpp b/src/parser/parse_op.cpp index 3f7df3794..772b73b1e 100644 --- a/src/parser/parse_op.cpp +++ b/src/parser/parse_op.cpp @@ -20,7 +20,7 @@ namespace cvc5 { std::ostream& operator<<(std::ostream& os, const ParseOp& p) { std::stringstream out; - out << "(ParseOp "; + out << "(ParseOp"; if (!p.d_expr.isNull()) { out << " :expr " << p.d_expr; diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 84c1e66f3..31f8517cd 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -154,6 +154,10 @@ api::Kind Parser::getKindForFunction(api::Term fun) { return api::APPLY_TESTER; } + else if (t.isUpdater()) + { + return api::APPLY_UPDATER; + } return api::UNDEFINED_KIND; } diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 4a612ce6f..dc9a324bb 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1643,6 +1643,22 @@ identifier[cvc5::ParseOp& p] api::DatatypeConstructor dc = d.getConstructor(f.toString()); p.d_expr = dc.getTesterTerm(); } + | UPDATE_TOK term[f, f2] + { + if (!f.getSort().isSelector()) + { + PARSER_STATE->parseError( + "Bad syntax for test (_ update X), X must be a selector."); + } + std::string sname = f.toString(); + // get the datatype that f belongs to + api::Sort sf = f.getSort().getSelectorDomainSort(); + api::Datatype d = sf.getDatatype(); + // find the selector + api::DatatypeSelector ds = d.getSelector(f.toString()); + // get the updater term + p.d_expr = ds.getUpdaterTerm(); + } | TUPLE_SEL_TOK m=INTEGER_LITERAL { // we adopt a special syntax (_ tupSel n) @@ -2226,6 +2242,7 @@ DECLARE_CODATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'dec PAR_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'par'; COMPREHENSION_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SETS) }?'comprehension'; TESTER_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'is'; +UPDATE_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'update'; MATCH_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'match'; GET_MODEL_TOK : 'get-model'; BLOCK_MODEL_TOK : 'block-model'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 9d4267dd2..2f19d16f0 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -135,6 +135,7 @@ void Smt2::addDatatypesOperators() if (!strictModeEnabled()) { + Parser::addOperator(api::APPLY_UPDATER); addOperator(api::DT_SIZE, "dt.size"); } } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index e6e227879..8f433256d 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -487,18 +487,6 @@ void CvcPrinter::toStreamNode(std::ostream& out, out << " -> BOOLEAN"; return; break; - case kind::TUPLE_UPDATE: - toStreamNode(out, n[0], depth, true, lbind); - out << " WITH ." << n.getOperator().getConst<TupleUpdate>().getIndex() << " := "; - toStreamNode(out, n[1], depth, true, lbind); - return; - break; - case kind::RECORD_UPDATE: - toStreamNode(out, n[0], depth, true, lbind); - out << " WITH ." << n.getOperator().getConst<RecordUpdate>().getField() << " := "; - toStreamNode(out, n[1], depth, true, lbind); - return; - break; // ARRAYS case kind::ARRAY_TYPE: diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index ae8d37713..eb80bd5a2 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -918,7 +918,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::APPLY_TESTER: case kind::APPLY_SELECTOR: case kind::APPLY_SELECTOR_TOTAL: - case kind::APPLY_DT_UPDATE: + case kind::APPLY_UPDATER: case kind::PARAMETRIC_DATATYPE: break; // separation logic diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index a6d3a45bc..744160c8b 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -48,6 +48,10 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) { return rewriteTester(in); } + else if (kind == APPLY_UPDATER) + { + return rewriteUpdater(in); + } else if (kind == kind::DT_SIZE) { if (in[0].getKind() == kind::APPLY_CONSTRUCTOR) @@ -473,6 +477,28 @@ RewriteResponse DatatypesRewriter::rewriteTester(TNode in) return RewriteResponse(REWRITE_DONE, in); } +RewriteResponse DatatypesRewriter::rewriteUpdater(TNode in) +{ + Assert (in.getKind()==APPLY_UPDATER); + if (in[0].getKind() == APPLY_CONSTRUCTOR) + { + Node op = in.getOperator(); + size_t cindex = utils::indexOf(in[0].getOperator()); + size_t cuindex = utils::cindexOf(op); + if (cindex==cuindex) + { + NodeManager * nm = NodeManager::currentNM(); + size_t updateIndex = utils::indexOf(op); + std::vector<Node> children(in[0].begin(), in[0].end()); + children[updateIndex] = in[1]; + children.insert(children.begin(),in[0].getOperator()); + return RewriteResponse(REWRITE_DONE, nm->mkNode(APPLY_CONSTRUCTOR, children)); + } + return RewriteResponse(REWRITE_DONE, in[0]); + } + return RewriteResponse(REWRITE_DONE, in); +} + Node DatatypesRewriter::normalizeCodatatypeConstant(Node n) { Trace("dt-nconst") << "Normalize " << n << std::endl; @@ -843,51 +869,40 @@ TrustNode DatatypesRewriter::expandDefinition(Node n) } } break; - case TUPLE_UPDATE: - case RECORD_UPDATE: + case APPLY_UPDATER: { Assert(tn.isDatatype()); const DType& dt = tn.getDType(); + Node op = n.getOperator(); + size_t updateIndex = utils::indexOf(op); + size_t cindex = utils::cindexOf(op); + const DTypeConstructor& dc = dt[cindex]; NodeBuilder b(APPLY_CONSTRUCTOR); - b << dt[0].getConstructor(); - size_t size, updateIndex; - if (n.getKind() == TUPLE_UPDATE) - { - Assert(tn.isTuple()); - size = tn.getTupleLength(); - updateIndex = n.getOperator().getConst<TupleUpdate>().getIndex(); - } - else - { - Assert(tn.isRecord()); - const DTypeConstructor& recCons = dt[0]; - size = recCons.getNumArgs(); - // get the index for the name - updateIndex = recCons.getSelectorIndexForName( - n.getOperator().getConst<RecordUpdate>().getField()); - } - Debug("tuprec") << "expr is " << n << std::endl; - Debug("tuprec") << "updateIndex is " << updateIndex << std::endl; - Debug("tuprec") << "t is " << tn << std::endl; - Debug("tuprec") << "t has arity " << size << std::endl; - for (size_t i = 0; i < size; ++i) + b << dc.getConstructor(); + Trace("dt-expand") << "Expand updater " << n << std::endl; + Trace("dt-expand") << "expr is " << n << std::endl; + Trace("dt-expand") << "updateIndex is " << updateIndex << std::endl; + Trace("dt-expand") << "t is " << tn << std::endl; + for (size_t i = 0, size = dc.getNumArgs(); i < size; ++i) { if (i == updateIndex) { b << n[1]; - Debug("tuprec") << "arg " << i << " gets updated to " << n[1] - << std::endl; } else { b << nm->mkNode( - APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(tn, i), n[0]); - Debug("tuprec") << "arg " << i << " copies " - << b[b.getNumChildren() - 1] << std::endl; + APPLY_SELECTOR_TOTAL, dc.getSelectorInternal(tn, i), n[0]); } } ret = b; - Debug("tuprec") << "return " << ret << std::endl; + if (dt.getNumConstructors() > 1) + { + // must be the right constructor to update + Node tester = nm->mkNode(APPLY_TESTER, dc.getTester(), n[0]); + ret = nm->mkNode(ITE, tester, ret, n[0]); + } + Trace("dt-expand") << "return " << ret << std::endl; } break; default: break; diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index c9a40ff7b..89e1901fa 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -58,6 +58,8 @@ class DatatypesRewriter : public TheoryRewriter static RewriteResponse rewriteSelector(TNode in); /** rewrite tester term in */ static RewriteResponse rewriteTester(TNode in); + /** rewrite updater term in */ + static RewriteResponse rewriteUpdater(TNode in); /** collect references * diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 4cabddd96..1b7808a8b 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -32,9 +32,9 @@ cardinality TESTER_TYPE \ "theory/builtin/theory_builtin_type_rules.h" # tester type has a constructor type -operator DT_UPDATE_TYPE 2 "datatype update" +operator UPDATER_TYPE 2 "datatype update" # can re-use function cardinality -cardinality DT_UPDATE_TYPE \ +cardinality UPDATER_TYPE \ "::cvc5::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" @@ -45,7 +45,7 @@ parameterized APPLY_SELECTOR_TOTAL [SELECTOR_TYPE] 1 "selector application; para parameterized APPLY_TESTER TESTER_TYPE 1 "tester application; first parameter is a tester, second is a datatype term" -parameterized APPLY_DT_UPDATE DT_UPDATE_TYPE 2 "datatype update application; first parameter is an update, second is a datatype term to update, third is the value to update with" +parameterized APPLY_UPDATER UPDATER_TYPE 2 "datatype updater application; first parameter is an update, second is a datatype term to update, third is the value to update with" constant DATATYPE_TYPE \ ::cvc5::DatatypeIndexConstant \ @@ -89,30 +89,12 @@ typerule APPLY_CONSTRUCTOR ::cvc5::theory::datatypes::DatatypeConstructorTypeRul typerule APPLY_SELECTOR ::cvc5::theory::datatypes::DatatypeSelectorTypeRule typerule APPLY_SELECTOR_TOTAL ::cvc5::theory::datatypes::DatatypeSelectorTypeRule typerule APPLY_TESTER ::cvc5::theory::datatypes::DatatypeTesterTypeRule -typerule APPLY_DT_UPDATE ::cvc5::theory::datatypes::DatatypeUpdateTypeRule +typerule APPLY_UPDATER ::cvc5::theory::datatypes::DatatypeUpdateTypeRule typerule APPLY_TYPE_ASCRIPTION ::cvc5::theory::datatypes::DatatypeAscriptionTypeRule # constructor applications are constant if they are applied only to constants construle APPLY_CONSTRUCTOR ::cvc5::theory::datatypes::DatatypeConstructorTypeRule -constant TUPLE_UPDATE_OP \ - ::cvc5::TupleUpdate \ - ::cvc5::TupleUpdateHashFunction \ - "util/tuple.h" \ - "operator for a tuple update; payload is an instance of the cvc5::TupleUpdate class" -parameterized TUPLE_UPDATE TUPLE_UPDATE_OP 2 "tuple update; first parameter is a TUPLE_UPDATE_OP (which references an index), second is the tuple, third is the element to store in the tuple at the given index" -typerule TUPLE_UPDATE_OP ::cvc5::theory::datatypes::TupleUpdateOpTypeRule -typerule TUPLE_UPDATE ::cvc5::theory::datatypes::TupleUpdateTypeRule - -constant RECORD_UPDATE_OP \ - ::cvc5::RecordUpdate \ - ::cvc5::RecordUpdateHashFunction \ - "expr/record.h" \ - "operator for a record update; payload is an instance cvc5::RecordUpdate class" -parameterized RECORD_UPDATE RECORD_UPDATE_OP 2 "record update; first parameter is a RECORD_UPDATE_OP (which references a field), second is a record term to update, third is the element to store in the record in the given field" -typerule RECORD_UPDATE_OP ::cvc5::theory::datatypes::RecordUpdateOpTypeRule -typerule RECORD_UPDATE ::cvc5::theory::datatypes::RecordUpdateTypeRule - operator DT_SIZE 1 "datatypes size" typerule DT_SIZE ::cvc5::theory::datatypes::DtSizeTypeRule diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp index 63f48668c..c9bfd98df 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.cpp +++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp @@ -207,7 +207,7 @@ TypeNode DatatypeUpdateTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::APPLY_DT_UPDATE); + Assert(n.getKind() == kind::APPLY_UPDATER); TypeNode updType = n.getOperator().getType(check); Assert(updType.getNumChildren() == 2); if (check) @@ -288,78 +288,6 @@ Cardinality ConstructorProperties::computeCardinality(TypeNode type) return c; } -TypeNode TupleUpdateTypeRule::computeType(NodeManager* nodeManager, - TNode n, - bool check) -{ - Assert(n.getKind() == kind::TUPLE_UPDATE); - const TupleUpdate& tu = n.getOperator().getConst<TupleUpdate>(); - TypeNode tupleType = n[0].getType(check); - TypeNode newValue = n[1].getType(check); - if (check) - { - if (!tupleType.isTuple()) - { - throw TypeCheckingExceptionPrivate( - n, "Tuple-update expression formed over non-tuple"); - } - if (tu.getIndex() >= tupleType.getTupleLength()) - { - std::stringstream ss; - ss << "Tuple-update expression index `" << tu.getIndex() - << "' is not a valid index; tuple type only has " - << tupleType.getTupleLength() << " fields"; - throw TypeCheckingExceptionPrivate(n, ss.str().c_str()); - } - } - return tupleType; -} - -TypeNode TupleUpdateOpTypeRule::computeType(NodeManager* nodeManager, - TNode n, - bool check) -{ - Assert(n.getKind() == kind::TUPLE_UPDATE_OP); - return nodeManager->builtinOperatorType(); -} - -TypeNode RecordUpdateTypeRule::computeType(NodeManager* nodeManager, - TNode n, - bool check) -{ - Assert(n.getKind() == kind::RECORD_UPDATE); - NodeManagerScope nms(nodeManager); - const RecordUpdate& ru = n.getOperator().getConst<RecordUpdate>(); - TypeNode recordType = n[0].getType(check); - TypeNode newValue = n[1].getType(check); - if (check) - { - if (!recordType.isRecord()) - { - throw TypeCheckingExceptionPrivate( - n, "Record-update expression formed over non-record"); - } - const DType& dt = recordType.getDType(); - const DTypeConstructor& recCons = dt[0]; - if (recCons.getSelectorIndexForName(ru.getField()) == -1) - { - std::stringstream ss; - ss << "Record-update field `" << ru.getField() - << "' is not a valid field name for the record type"; - throw TypeCheckingExceptionPrivate(n, ss.str().c_str()); - } - } - return recordType; -} - -TypeNode RecordUpdateOpTypeRule::computeType(NodeManager* nodeManager, - TNode n, - bool check) -{ - Assert(n.getKind() == kind::RECORD_UPDATE_OP); - return nodeManager->builtinOperatorType(); -} - TypeNode DtSizeTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 3bf4660e6..cf57a6c0d 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -44,32 +44,14 @@ struct DatatypeUpdateTypeRule static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; -struct DatatypeAscriptionTypeRule { - static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); -}; - -struct ConstructorProperties { - static Cardinality computeCardinality(TypeNode type); -}; - -struct TupleUpdateTypeRule { - static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); -}; - -class TupleUpdateOpTypeRule +struct DatatypeAscriptionTypeRule { - public: - static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); -}; - -struct RecordUpdateTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; -class RecordUpdateOpTypeRule +struct ConstructorProperties { - public: - static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); + static Cardinality computeCardinality(TypeNode type); }; class DtSizeTypeRule { diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp index f651d5f84..bf74347d0 100644 --- a/src/theory/datatypes/theory_datatypes_utils.cpp +++ b/src/theory/datatypes/theory_datatypes_utils.cpp @@ -117,7 +117,7 @@ const DType& datatypeOf(Node n) case CONSTRUCTOR_TYPE: return t[t.getNumChildren() - 1].getDType(); case SELECTOR_TYPE: case TESTER_TYPE: - case DT_UPDATE_TYPE: return t[0].getDType(); + case UPDATER_TYPE: return t[0].getDType(); default: Unhandled() << "arg must be a datatype constructor, selector, or tester"; } diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 79a44f426..5fd0003bf 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -77,7 +77,6 @@ libcvc5_add_sources( statistics_value.h string.cpp string.h - tuple.h unsafe_interrupt_exception.h utility.cpp utility.h diff --git a/src/util/tuple.h b/src/util/tuple.h deleted file mode 100644 index 733ecf189..000000000 --- a/src/util/tuple.h +++ /dev/null @@ -1,53 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Morgan Deters, Mathias Preiner, Tim King - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Tuple operators. - */ - -#include "cvc5_public.h" - -#ifndef CVC5__TUPLE_H -#define CVC5__TUPLE_H - -#include <iostream> -#include <vector> -#include <utility> - -namespace cvc5 { - -class TupleUpdate -{ - unsigned d_index; - - public: - TupleUpdate(unsigned index) : d_index(index) {} - unsigned getIndex() const { return d_index; } - bool operator==(const TupleUpdate& t) const { return d_index == t.d_index; } - bool operator!=(const TupleUpdate& t) const { return d_index != t.d_index; } -}; /* class TupleUpdate */ - -struct TupleUpdateHashFunction -{ - inline size_t operator()(const TupleUpdate& t) const { - return t.getIndex(); - } -}; /* struct TupleUpdateHashFunction */ - -std::ostream& operator<<(std::ostream& out, const TupleUpdate& t); - -inline std::ostream& operator<<(std::ostream& out, const TupleUpdate& t) { - return out << "[" << t.getIndex() << "]"; -} - -} // namespace cvc5 - -#endif /* CVC5__TUPLE_H */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 9bda5cff1..538868c6c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -480,6 +480,8 @@ set(regress_0_tests regress0/datatypes/issue5280-no-nrec.smt2 regress0/datatypes/jsat-2.6.smt2 regress0/datatypes/list-bool.smt2 + regress0/datatypes/list-update.smt2 + regress0/datatypes/list-update-sat.smt2 regress0/datatypes/model-subterms-min.smt2 regress0/datatypes/mutually-recursive.cvc regress0/datatypes/pair-bool-bool.cvc diff --git a/test/regress/regress0/datatypes/list-update-sat.smt2 b/test/regress/regress0/datatypes/list-update-sat.smt2 new file mode 100644 index 000000000..9f424e595 --- /dev/null +++ b/test/regress/regress0/datatypes/list-update-sat.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-info :status sat) +(declare-datatypes ((list 0)) ( +((cons (head Int) (tail list)) (nil)) +)) +(declare-fun a () list) +(assert (= ((_ update head) a 3) (cons 3 nil))) +(check-sat) diff --git a/test/regress/regress0/datatypes/list-update.smt2 b/test/regress/regress0/datatypes/list-update.smt2 new file mode 100644 index 000000000..178f1a000 --- /dev/null +++ b/test/regress/regress0/datatypes/list-update.smt2 @@ -0,0 +1,10 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-datatypes ((list 0)) ( +((cons (head Int) (tail list)) (nil)) +)) +(declare-fun a () list) +(declare-fun b () list) +(assert ((_ is cons) a)) +(assert (= ((_ update head) a 3) ((_ update head) b 4))) +(check-sat) diff --git a/test/unit/api/datatype_api_black.cpp b/test/unit/api/datatype_api_black.cpp index 3fbdcc0b5..f82e722d3 100644 --- a/test/unit/api/datatype_api_black.cpp +++ b/test/unit/api/datatype_api_black.cpp @@ -214,6 +214,10 @@ TEST_F(TestApiBlackDatatype, datatypeNames) ASSERT_EQ(dselTail.getName(), std::string("tail")); ASSERT_EQ(dselTail.getRangeSort(), dtypeSort); + // get selector from datatype + ASSERT_NO_THROW(dt.getSelector("head")); + ASSERT_THROW(dt.getSelector("cons"), CVC5ApiException); + // possible to construct null datatype declarations if not using solver ASSERT_THROW(DatatypeDecl().getName(), CVC5ApiException); } diff --git a/test/unit/api/op_black.cpp b/test/unit/api/op_black.cpp index 7183fa7a7..8c4e31c22 100644 --- a/test/unit/api/op_black.cpp +++ b/test/unit/api/op_black.cpp @@ -50,7 +50,6 @@ TEST_F(TestApiBlackOp, getNumIndices) { Op plus = d_solver.mkOp(PLUS); Op divisible = d_solver.mkOp(DIVISIBLE, 4); - Op record_update = d_solver.mkOp(RECORD_UPDATE, "test"); Op bitvector_repeat = d_solver.mkOp(BITVECTOR_REPEAT, 5); Op bitvector_zero_extend = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6); Op bitvector_sign_extend = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7); @@ -60,7 +59,6 @@ TEST_F(TestApiBlackOp, getNumIndices) Op iand = d_solver.mkOp(IAND, 3); Op floatingpoint_to_ubv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 11); Op floatingopint_to_sbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13); - Op tuple_update = d_solver.mkOp(TUPLE_UPDATE, 5); Op floatingpoint_to_fp_ieee_bitvector = d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 25); Op floatingpoint_to_fp_floatingpoint = @@ -76,7 +74,6 @@ TEST_F(TestApiBlackOp, getNumIndices) ASSERT_EQ(0, plus.getNumIndices()); ASSERT_EQ(1, divisible.getNumIndices()); - ASSERT_EQ(1, record_update.getNumIndices()); ASSERT_EQ(1, bitvector_repeat.getNumIndices()); ASSERT_EQ(1, bitvector_zero_extend.getNumIndices()); ASSERT_EQ(1, bitvector_sign_extend.getNumIndices()); @@ -86,7 +83,6 @@ TEST_F(TestApiBlackOp, getNumIndices) ASSERT_EQ(1, iand.getNumIndices()); ASSERT_EQ(1, floatingpoint_to_ubv.getNumIndices()); ASSERT_EQ(1, floatingopint_to_sbv.getNumIndices()); - ASSERT_EQ(1, tuple_update.getNumIndices()); ASSERT_EQ(2, floatingpoint_to_fp_ieee_bitvector.getNumIndices()); ASSERT_EQ(2, floatingpoint_to_fp_floatingpoint.getNumIndices()); ASSERT_EQ(2, floatingpoint_to_fp_real.getNumIndices()); @@ -105,11 +101,6 @@ TEST_F(TestApiBlackOp, getIndicesString) ASSERT_TRUE(divisible_ot.isIndexed()); std::string divisible_idx = divisible_ot.getIndices<std::string>(); ASSERT_EQ(divisible_idx, "4"); - - Op record_update_ot = d_solver.mkOp(RECORD_UPDATE, "test"); - std::string record_update_idx = record_update_ot.getIndices<std::string>(); - ASSERT_EQ(record_update_idx, "test"); - ASSERT_THROW(record_update_ot.getIndices<uint32_t>(), CVC5ApiException); } TEST_F(TestApiBlackOp, getIndicesUint) @@ -155,11 +146,6 @@ TEST_F(TestApiBlackOp, getIndicesUint) uint32_t floatingpoint_to_sbv_idx = floatingpoint_to_sbv_ot.getIndices<uint32_t>(); ASSERT_EQ(floatingpoint_to_sbv_idx, 13); - - Op tuple_update_ot = d_solver.mkOp(TUPLE_UPDATE, 5); - uint32_t tuple_update_idx = tuple_update_ot.getIndices<uint32_t>(); - ASSERT_EQ(tuple_update_idx, 5); - ASSERT_THROW(tuple_update_ot.getIndices<std::string>(), CVC5ApiException); } TEST_F(TestApiBlackOp, getIndicesPairUint) diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index c0258be9a..f7e6a3783 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -544,7 +544,6 @@ TEST_F(TestApiBlackSolver, mkOp) ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, EQUAL), CVC5ApiException); // mkOp(Kind kind, const std::string& arg) - ASSERT_NO_THROW(d_solver.mkOp(RECORD_UPDATE, "asdf")); ASSERT_NO_THROW(d_solver.mkOp(DIVISIBLE, "2147483648")); ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, "asdf"), CVC5ApiException); diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp index c2b924bfa..d1b096bda 100644 --- a/test/unit/api/sort_black.cpp +++ b/test/unit/api/sort_black.cpp @@ -153,11 +153,20 @@ TEST_F(TestApiBlackSort, isTester) { Sort dt_sort = create_datatype_sort(); Datatype dt = dt_sort.getDatatype(); - Sort cons_sort = dt[0].getTesterTerm().getSort(); - ASSERT_TRUE(cons_sort.isTester()); + Sort testerSort = dt[0].getTesterTerm().getSort(); + ASSERT_TRUE(testerSort.isTester()); ASSERT_NO_THROW(Sort().isTester()); } +TEST_F(TestApiBlackSort, isUpdater) +{ + Sort dt_sort = create_datatype_sort(); + Datatype dt = dt_sort.getDatatype(); + Sort updaterSort = dt[0][0].getUpdaterTerm().getSort(); + ASSERT_TRUE(updaterSort.isUpdater()); + ASSERT_NO_THROW(Sort().isUpdater()); +} + TEST_F(TestApiBlackSort, isFunction) { Sort fun_sort = d_solver.mkFunctionSort(d_solver.getRealSort(), diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp index 5844868f1..a19ab31a1 100644 --- a/test/unit/util/datatype_black.cpp +++ b/test/unit/util/datatype_black.cpp @@ -249,9 +249,9 @@ TEST_F(TestUtilBlackDatatype, listIntUpdate) Node zero = d_nodeManager->mkConst(Rational(0)); Node truen = d_nodeManager->mkConst(true); // construct an update term - Node uterm = d_nodeManager->mkNode(kind::APPLY_DT_UPDATE, updater, gt, zero); + Node uterm = d_nodeManager->mkNode(kind::APPLY_UPDATER, updater, gt, zero); // construct a non well-formed update term - ASSERT_THROW(d_nodeManager->mkNode(kind::APPLY_DT_UPDATE, updater, gt, truen) + ASSERT_THROW(d_nodeManager->mkNode(kind::APPLY_UPDATER, updater, gt, truen) .getType(true), TypeCheckingExceptionPrivate); } |