This removes the special case of TUPLE_UPDATE and RECORD_UPDATE in favor of the more general datatype update.
Datatype update is handled analogously to APPLY_SELECTOR / APPLY_TESTER.
{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 ---------------------------------------------------- */
{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 ------------------------------------------------ */
/* 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,
INT_TO_BITVECTOR,
FLOATINGPOINT_TO_UBV,
FLOATINGPOINT_TO_SBV,
- TUPLE_UPDATE,
BITVECTOR_EXTRACT,
FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
FLOATINGPOINT_TO_FP_FLOATINGPOINT,
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
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;
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;
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;
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;
}
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;
////////
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
{
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;
}
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)
{
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;
*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,
* @return true if the sort is a tester 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
*/
class CVC5_EXPORT DatatypeSelector
{
+ friend class Datatype;
friend class DatatypeConstructor;
friend class Solver;
*/
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;
*/
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;
*/
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
/**
* 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
*/
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`
* - `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
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 +
DatatypeSelector() except +
string getName() except +
Term getSelectorTerm() except +
+ Term getUpdaterTerm() except +
Sort getRangeSort() except +
string toString() except +
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()
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()
dtype_cons.cpp
dtype_selector.h
dtype_selector.cpp
- record.cpp
- record.h
sequence.cpp
sequence.h
subs.cpp
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);
}
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)
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 ) {
namespace cvc5 {
+using Record = std::vector<std::pair<std::string, TypeNode>>;
+
namespace api {
class Solver;
}
+++ /dev/null
-/******************************************************************************
- * 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
+++ /dev/null
-/******************************************************************************
- * 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 */
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));
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
{
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;
| 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);
+ }
;
/**
| 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. */
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;
{
return api::APPLY_TESTER;
}
+ else if (t.isUpdater())
+ {
+ return api::APPLY_UPDATER;
+ }
return api::UNDEFINED_KIND;
}
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)
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';
if (!strictModeEnabled())
{
+ Parser::addOperator(api::APPLY_UPDATER);
addOperator(api::DT_SIZE, "dt.size");
}
}
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:
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
{
return rewriteTester(in);
}
+ else if (kind == APPLY_UPDATER)
+ {
+ return rewriteUpdater(in);
+ }
else if (kind == kind::DT_SIZE)
{
if (in[0].getKind() == kind::APPLY_CONSTRUCTOR)
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;
}
}
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;
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
*
"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"
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 \
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
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)
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)
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 {
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";
}
statistics_value.h
string.cpp
string.h
- tuple.h
unsafe_interrupt_exception.h
utility.cpp
utility.h
+++ /dev/null
-/******************************************************************************
- * 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 */
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
--- /dev/null
+(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)
--- /dev/null
+(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)
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);
}
{
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);
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 =
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());
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());
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)
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)
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);
{
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(),
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);
}
projects / cvc5.git / commitdiff