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.
bound_var_manager.h
cardinality_constraint.cpp
cardinality_constraint.h
+ codatatype_bound_variable.cpp
+ codatatype_bound_variable.h
emptyset.cpp
emptyset.h
emptybag.cpp
--- /dev/null
+/******************************************************************************
+ * 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 <algorithm>
+#include <iostream>
+#include <sstream>
+#include <string>
+
+#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<TypeNode>()(cbv.getType())
+ * IntegerHashFunction()(cbv.getIndex());
+}
+
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * 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 <iosfwd>
+#include <memory>
+
+#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<TypeNode> 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 */
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());
}
#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"
else
{
// a loop
- const Integer& i = n.getConst<UninterpretedConstant>().getIndex();
+ const Integer& i = n.getConst<CodatatypeBoundVariable>().getIndex();
uint32_t index = i.toUnsignedInt();
if (index >= sk.size())
{
{
int debruijn = depth - it->second - 1;
return NodeManager::currentNM()->mkConst(
- UninterpretedConstant(n.getType(), debruijn));
+ CodatatypeBoundVariable(n.getType(), debruijn));
}
std::vector<Node> children;
bool childChanged = false;
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<UninterpretedConstant>().getIndex().toUnsignedInt();
+ n.getConst<CodatatypeBoundVariable>().getIndex().toUnsignedInt();
if (index == depth)
{
return orig;
typerule TUPLE_PROJECT_OP "SimpleTypeRule<RBuiltinOperator>"
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
#include <sstream>
#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"
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() ){
children.push_back( rv );
}
vmap.erase( n );
- return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
+ return nm->mkNode(APPLY_CONSTRUCTOR, children);
}
}
return n;
#include <sstream>
#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"
return nm->mkTupleType(types);
}
+TypeNode CodatatypeBoundVariableTypeRule::computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+{
+ return n.getConst<CodatatypeBoundVariable>().getType();
+}
+
} // namespace datatypes
} // namespace theory
} // namespace cvc5
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
#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"
{
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
{
{
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
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):
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")));
projects / cvc5.git / commitdiff