From 90e615eb3920bd60173e967c85cbcaf4f34a032c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 Oct 2021 11:49:53 -0500 Subject: [PATCH] Use codatatype bound variables for codatatype values (#7425) Previously, we had conflated codatatype bound variables and uninterpreted constants (as they have the same functionality). However, we should separate these concepts so we can ensure that uninterpreted constants are only used for uninterpreted sorts. --- src/expr/CMakeLists.txt | 2 + src/expr/codatatype_bound_variable.cpp | 113 ++++++++++++++++++ src/expr/codatatype_bound_variable.h | 91 ++++++++++++++ src/expr/uninterpreted_constant.cpp | 6 +- src/theory/datatypes/datatypes_rewriter.cpp | 10 +- src/theory/datatypes/kinds | 9 ++ src/theory/datatypes/theory_datatypes.cpp | 8 +- .../datatypes/theory_datatypes_type_rules.cpp | 8 ++ .../datatypes/theory_datatypes_type_rules.h | 6 + src/theory/datatypes/type_enumerator.cpp | 5 +- src/theory/theory_model_builder.cpp | 2 +- test/python/unit/api/test_solver.py | 9 -- test/unit/api/solver_black.cpp | 9 -- 13 files changed, 247 insertions(+), 31 deletions(-) create mode 100644 src/expr/codatatype_bound_variable.cpp create mode 100644 src/expr/codatatype_bound_variable.h diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index e73960676..467500868 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -26,6 +26,8 @@ libcvc5_add_sources( bound_var_manager.h cardinality_constraint.cpp cardinality_constraint.h + codatatype_bound_variable.cpp + codatatype_bound_variable.h emptyset.cpp emptyset.h emptybag.cpp diff --git a/src/expr/codatatype_bound_variable.cpp b/src/expr/codatatype_bound_variable.cpp new file mode 100644 index 000000000..a6a9d8e3e --- /dev/null +++ b/src/expr/codatatype_bound_variable.cpp @@ -0,0 +1,113 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * 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. + * **************************************************************************** + * + * Representation of bound variables in codatatype values + */ + +#include "expr/codatatype_bound_variable.h" + +#include +#include +#include +#include + +#include "base/check.h" +#include "expr/type_node.h" + +using namespace std; + +namespace cvc5 { + +CodatatypeBoundVariable::CodatatypeBoundVariable(const TypeNode& type, + Integer index) + : d_type(new TypeNode(type)), d_index(index) +{ + PrettyCheckArgument(type.isCodatatype(), + type, + "codatatype bound variables can only be created for " + "codatatype sorts, not `%s'", + type.toString().c_str()); + PrettyCheckArgument( + index >= 0, + index, + "index >= 0 required for codatatype bound variable index, not `%s'", + index.toString().c_str()); +} + +CodatatypeBoundVariable::~CodatatypeBoundVariable() {} + +CodatatypeBoundVariable::CodatatypeBoundVariable( + const CodatatypeBoundVariable& other) + : d_type(new TypeNode(other.getType())), d_index(other.getIndex()) +{ +} + +const TypeNode& CodatatypeBoundVariable::getType() const { return *d_type; } +const Integer& CodatatypeBoundVariable::getIndex() const { return d_index; } +bool CodatatypeBoundVariable::operator==( + const CodatatypeBoundVariable& cbv) const +{ + return getType() == cbv.getType() && d_index == cbv.d_index; +} +bool CodatatypeBoundVariable::operator!=( + const CodatatypeBoundVariable& cbv) const +{ + return !(*this == cbv); +} + +bool CodatatypeBoundVariable::operator<( + const CodatatypeBoundVariable& cbv) const +{ + return getType() < cbv.getType() + || (getType() == cbv.getType() && d_index < cbv.d_index); +} +bool CodatatypeBoundVariable::operator<=( + const CodatatypeBoundVariable& cbv) const +{ + return getType() < cbv.getType() + || (getType() == cbv.getType() && d_index <= cbv.d_index); +} +bool CodatatypeBoundVariable::operator>( + const CodatatypeBoundVariable& cbv) const +{ + return !(*this <= cbv); +} +bool CodatatypeBoundVariable::operator>=( + const CodatatypeBoundVariable& cbv) const +{ + return !(*this < cbv); +} + +std::ostream& operator<<(std::ostream& out, const CodatatypeBoundVariable& cbv) +{ + std::stringstream ss; + ss << cbv.getType(); + std::string st(ss.str()); + // must remove delimiting quotes from the name of the type + // this prevents us from printing symbols like |@cbv_|T|_n| + std::string q("|"); + size_t pos; + while ((pos = st.find(q)) != std::string::npos) + { + st.replace(pos, 1, ""); + } + return out << "cbv_" << st.c_str() << "_" << cbv.getIndex(); +} + +size_t CodatatypeBoundVariableHashFunction::operator()( + const CodatatypeBoundVariable& cbv) const +{ + return std::hash()(cbv.getType()) + * IntegerHashFunction()(cbv.getIndex()); +} + +} // namespace cvc5 diff --git a/src/expr/codatatype_bound_variable.h b/src/expr/codatatype_bound_variable.h new file mode 100644 index 000000000..9af8476d5 --- /dev/null +++ b/src/expr/codatatype_bound_variable.h @@ -0,0 +1,91 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * 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. + * **************************************************************************** + * + * Representation of bound variables in codatatype values + */ + +#include "cvc5_public.h" + +#ifndef CVC5__EXPR__CODATATYPE_BOUND_VARIABLE_H +#define CVC5__EXPR__CODATATYPE_BOUND_VARIABLE_H + +#include +#include + +#include "util/integer.h" + +namespace cvc5 { + +class TypeNode; + +/** + * In theory, codatatype values are represented in using a MU-notation form, + * where recursive values may contain free constants indexed by their de Bruijn + * indices. This is sometimes written: + * MU x. (cons 0 x). + * where the MU binder is label for a term position, which x references. + * Instead of constructing an explicit MU binder (which is problematic for + * canonicity), we use de Bruijn indices for representing bound variables, + * whose index indicates the level in which it is nested. For example, we + * represent the above value as: + * (cons 0 @cbv_0) + * In the above value, @cbv_0 is a pointer to its direct parent, so the above + * value represents the infinite list (cons 0 (cons 0 (cons 0 ... ))). + * Another example, the value: + * (cons 0 (cons 1 @cbv_1)) + * @cbv_1 is pointer to the top most node of this value, so this is value + * represents the infinite list (cons 0 (cons 1 (cons 0 (cons 1 ...)))). The + * value: + * (cons 0 (cons 1 @cbv_0)) + * on the other hand represents the lasso: + * (cons 0 (cons 1 (cons 1 (cons 1 ... )))) + * + * This class is used for representing the indexed bound variables in the above + * values. It is considered a constant (isConst is true). However, constants + * of codatatype type are normalized by the rewriter (see datatypes rewriter + * normalizeCodatatypeConstant) to ensure their canonicity, via a variant + * of Hopcroft's algorithm. + */ +class CodatatypeBoundVariable +{ + public: + CodatatypeBoundVariable(const TypeNode& type, Integer index); + ~CodatatypeBoundVariable(); + + CodatatypeBoundVariable(const CodatatypeBoundVariable& other); + + const TypeNode& getType() const; + const Integer& getIndex() const; + bool operator==(const CodatatypeBoundVariable& cbv) const; + bool operator!=(const CodatatypeBoundVariable& cbv) const; + bool operator<(const CodatatypeBoundVariable& cbv) const; + bool operator<=(const CodatatypeBoundVariable& cbv) const; + bool operator>(const CodatatypeBoundVariable& cbv) const; + bool operator>=(const CodatatypeBoundVariable& cbv) const; + + private: + std::unique_ptr d_type; + const Integer d_index; +}; +std::ostream& operator<<(std::ostream& out, const CodatatypeBoundVariable& cbv); + +/** + * Hash function for codatatype bound variables. + */ +struct CodatatypeBoundVariableHashFunction +{ + size_t operator()(const CodatatypeBoundVariable& cbv) const; +}; + +} // namespace cvc5 + +#endif /* CVC5__UNINTERPRETED_CONSTANT_H */ diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp index ef354568d..709ec112f 100644 --- a/src/expr/uninterpreted_constant.cpp +++ b/src/expr/uninterpreted_constant.cpp @@ -31,7 +31,11 @@ UninterpretedConstant::UninterpretedConstant(const TypeNode& type, Integer index) : d_type(new TypeNode(type)), d_index(index) { - //PrettyCheckArgument(type.isSort(), type, "uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str()); + PrettyCheckArgument(type.isSort(), + type, + "uninterpreted constants can only be created for " + "uninterpreted sorts, not `%s'", + type.toString().c_str()); PrettyCheckArgument(index >= 0, index, "index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str()); } diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index c446504fd..fd957baaa 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -16,12 +16,12 @@ #include "theory/datatypes/datatypes_rewriter.h" #include "expr/ascription_type.h" +#include "expr/codatatype_bound_variable.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "expr/skolem_manager.h" #include "expr/sygus_datatype.h" -#include "expr/uninterpreted_constant.h" #include "options/datatypes_options.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/datatypes/theory_datatypes_utils.h" @@ -729,7 +729,7 @@ Node DatatypesRewriter::collectRef(Node n, else { // a loop - const Integer& i = n.getConst().getIndex(); + const Integer& i = n.getConst().getIndex(); uint32_t index = i.toUnsignedInt(); if (index >= sk.size()) { @@ -771,7 +771,7 @@ Node DatatypesRewriter::normalizeCodatatypeConstantEqc( { int debruijn = depth - it->second - 1; return NodeManager::currentNM()->mkConst( - UninterpretedConstant(n.getType(), debruijn)); + CodatatypeBoundVariable(n.getType(), debruijn)); } std::vector children; bool childChanged = false; @@ -798,10 +798,10 @@ Node DatatypesRewriter::replaceDebruijn(Node n, TypeNode orig_tn, unsigned depth) { - if (n.getKind() == kind::UNINTERPRETED_CONSTANT && n.getType() == orig_tn) + if (n.getKind() == kind::CODATATYPE_BOUND_VARIABLE && n.getType() == orig_tn) { unsigned index = - n.getConst().getIndex().toUnsignedInt(); + n.getConst().getIndex().toUnsignedInt(); if (index == depth) { return orig; diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 41d5ded76..cb3a78cf2 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -145,4 +145,13 @@ parameterized TUPLE_PROJECT TUPLE_PROJECT_OP 1 \ typerule TUPLE_PROJECT_OP "SimpleTypeRule" typerule TUPLE_PROJECT ::cvc5::theory::datatypes::TupleProjectTypeRule +# For representing codatatype values +constant CODATATYPE_BOUND_VARIABLE \ + class \ + CodatatypeBoundVariable \ + ::cvc5::CodatatypeBoundVariableHashFunction \ + "expr/codatatype_bound_variable.h" \ + "the kind of expressions representing bound variables in codatatype constants, which are de Bruijn indexed variables; payload is an instance of the cvc5::CodatatypeBoundVariable class (used in models)" +typerule CODATATYPE_BOUND_VARIABLE ::cvc5::theory::datatypes::CodatatypeBoundVariableTypeRule + endtheory diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index c892ffc11..0cbeaa515 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -18,11 +18,11 @@ #include #include "base/check.h" +#include "expr/codatatype_bound_variable.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/kind.h" #include "expr/skolem_manager.h" -#include "expr/uninterpreted_constant.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" @@ -1290,10 +1290,10 @@ bool TheoryDatatypes::collectModelValues(TheoryModel* m, Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, int >& vmap, int depth ){ std::map< Node, int >::iterator itv = vmap.find( n ); + NodeManager* nm = NodeManager::currentNM(); if( itv!=vmap.end() ){ int debruijn = depth - 1 - itv->second; - return NodeManager::currentNM()->mkConst( - UninterpretedConstant(n.getType(), debruijn)); + return nm->mkConst(CodatatypeBoundVariable(n.getType(), debruijn)); }else if( n.getType().isDatatype() ){ Node nc = eqc_cons[n]; if( !nc.isNull() ){ @@ -1308,7 +1308,7 @@ Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_c children.push_back( rv ); } vmap.erase( n ); - return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); + return nm->mkNode(APPLY_CONSTRUCTOR, children); } } return n; diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp index 503eaf4df..86a11357b 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.cpp +++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp @@ -18,6 +18,7 @@ #include #include "expr/ascription_type.h" +#include "expr/codatatype_bound_variable.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/type_matcher.h" @@ -597,6 +598,13 @@ TypeNode TupleProjectTypeRule::computeType(NodeManager* nm, TNode n, bool check) return nm->mkTupleType(types); } +TypeNode CodatatypeBoundVariableTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + return n.getConst().getType(); +} + } // namespace datatypes } // namespace theory } // namespace cvc5 diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index cf57a6c0d..7cf98aa74 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -99,6 +99,12 @@ class TupleProjectTypeRule static TypeNode computeType(NodeManager* nm, TNode n, bool check); }; +class CodatatypeBoundVariableTypeRule +{ + public: + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; + } // namespace datatypes } // namespace theory } // namespace cvc5 diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index 39b48ece9..6528f1052 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -16,6 +16,7 @@ #include "theory/datatypes/type_enumerator.h" #include "expr/ascription_type.h" +#include "expr/codatatype_bound_variable.h" #include "expr/dtype_cons.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/theory_datatypes_utils.h" @@ -108,8 +109,8 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ { if (d_child_enum) { - ret = NodeManager::currentNM()->mkConst( - UninterpretedConstant(d_type, d_size_limit)); + NodeManager* nm = NodeManager::currentNM(); + ret = nm->mkConst(CodatatypeBoundVariable(d_type, d_size_limit)); } else { diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 33dbe9ffa..1a0549a0a 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -224,7 +224,7 @@ bool TheoryEngineModelBuilder::isExcludedCdtValue( { Trace("model-builder-debug") << " ...matches with " << eqc << " -> " << eqc_m << std::endl; - if (eqc_m.getKind() == kind::UNINTERPRETED_CONSTANT) + if (eqc_m.getKind() == kind::CODATATYPE_BOUND_VARIABLE) { Trace("model-builder-debug") << "*** " << val << " is excluded datatype for " << eqc diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py index db49f8bea..29d637dc6 100644 --- a/test/python/unit/api/test_solver.py +++ b/test/python/unit/api/test_solver.py @@ -381,15 +381,6 @@ def test_mk_rounding_mode(solver): solver.mkRoundingMode(pycvc5.RoundTowardZero) -def test_mk_uninterpreted_const(solver): - solver.mkUninterpretedConst(solver.getBooleanSort(), 1) - with pytest.raises(RuntimeError): - solver.mkUninterpretedConst(pycvc5.Sort(solver), 1) - slv = pycvc5.Solver() - with pytest.raises(RuntimeError): - slv.mkUninterpretedConst(solver.getBooleanSort(), 1) - - def test_mk_abstract_value(solver): solver.mkAbstractValue("1") with pytest.raises(ValueError): diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index 19113ae13..f90018101 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -376,15 +376,6 @@ TEST_F(TestApiBlackSolver, mkRoundingMode) ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO)); } -TEST_F(TestApiBlackSolver, mkUninterpretedConst) -{ - ASSERT_NO_THROW(d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1)); - ASSERT_THROW(d_solver.mkUninterpretedConst(Sort(), 1), CVC5ApiException); - Solver slv; - ASSERT_THROW(slv.mkUninterpretedConst(d_solver.getBooleanSort(), 1), - CVC5ApiException); -} - TEST_F(TestApiBlackSolver, mkAbstractValue) { ASSERT_NO_THROW(d_solver.mkAbstractValue(std::string("1"))); -- 2.30.2