Merge branch 'master' into fixErrorSetfixErrorSet

8 files changed, 333 insertions, 5 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index e73960676..45ce01edb 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
@@ -95,6 +97,8 @@ libcvc5_add_sources(
   sygus_datatype.h
   uninterpreted_constant.cpp
   uninterpreted_constant.h
+  variadic_trie.cpp
+  variadic_trie.h
 )
 
 libcvc5_add_sources(GENERATED
diff --git a/src/expr/cardinality_constraint.cpp b/src/expr/cardinality_constraint.cpp
index 3841228fb..695f5d4a3 100644
--- a/src/expr/cardinality_constraint.cpp
+++ b/src/expr/cardinality_constraint.cpp
@@ -56,6 +56,13 @@ std::ostream& operator<<(std::ostream& out, const CardinalityConstraint& cc)
              << ')';
 }
 
+size_t CardinalityConstraintHashFunction::operator()(
+    const CardinalityConstraint& cc) const
+{
+  return std::hash<TypeNode>()(cc.getType())
+         * IntegerHashFunction()(cc.getUpperBound());
+}
+
 CombinedCardinalityConstraint::CombinedCardinalityConstraint(const Integer& ub)
     : d_ubound(ub)
 {
diff --git a/src/expr/cardinality_constraint.h b/src/expr/cardinality_constraint.h
index a51ba545c..b2bfa836f 100644
--- a/src/expr/cardinality_constraint.h
+++ b/src/expr/cardinality_constraint.h
@@ -60,10 +60,10 @@ class CardinalityConstraint
 
 std::ostream& operator<<(std::ostream& out, const CardinalityConstraint& cc);
 
-using CardinalityConstraintHashFunction = PairHashFunction<TypeNode,
-                                                           Integer,
-                                                           std::hash<TypeNode>,
-                                                           IntegerHashFunction>;
+struct CardinalityConstraintHashFunction
+{
+  size_t operator()(const CardinalityConstraint& cc) const;
+};
 
 /**
  * A combined cardinality constraint, handled in the cardinality extension of
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 <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
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 <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 */
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/expr/variadic_trie.cpp b/src/expr/variadic_trie.cpp
new file mode 100644
index 000000000..bd27780e9
--- /dev/null
+++ b/src/expr/variadic_trie.cpp
@@ -0,0 +1,55 @@
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Variadic trie utility
+ */
+
+#include "expr/variadic_trie.h"
+
+namespace cvc5 {
+
+bool VariadicTrie::add(Node n, const std::vector<Node>& i)
+{
+  VariadicTrie* curr = this;
+  for (const Node& ic : i)
+  {
+    curr = &(curr->d_children[ic]);
+  }
+  if (curr->d_data.isNull())
+  {
+    curr->d_data = n;
+    return true;
+  }
+  return false;
+}
+
+bool VariadicTrie::hasSubset(const std::vector<Node>& is) const
+{
+  if (!d_data.isNull())
+  {
+    return true;
+  }
+  for (const std::pair<const Node, VariadicTrie>& p : d_children)
+  {
+    Node n = p.first;
+    if (std::find(is.begin(), is.end(), n) != is.end())
+    {
+      if (p.second.hasSubset(is))
+      {
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+}  // namespace cvc5
diff --git a/src/expr/variadic_trie.h b/src/expr/variadic_trie.h
new file mode 100644
index 000000000..aa7ca1e37
--- /dev/null
+++ b/src/expr/variadic_trie.h
@@ -0,0 +1,54 @@
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Variadic trie utility
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__EXPR__VARIADIC_TRIE_H
+#define CVC5__EXPR__VARIADIC_TRIE_H
+
+#include <map>
+#include <vector>
+
+#include "expr/node.h"
+
+namespace cvc5 {
+
+/**
+ * A trie that stores data at undetermined depth. Storing data at
+ * undetermined depth is in contrast to the NodeTrie (expr/node_trie.h), which
+ * assumes all data is stored at a fixed depth.
+ *
+ * Since data can be stored at any depth, we require both a d_children field
+ * and a d_data field.
+ */
+class VariadicTrie
+{
+ public:
+  /** the children of this node */
+  std::map<Node, VariadicTrie> d_children;
+  /** the data at this node */
+  Node d_data;
+  /**
+   * Add data with identifier n indexed by i, return true if data is not already
+   * stored at the node indexed by i.
+   */
+  bool add(Node n, const std::vector<Node>& i);
+  /** Is there any data in this trie that is indexed by any subset of is? */
+  bool hasSubset(const std::vector<Node>& is) const;
+};
+
+}  // namespace cvc5
+
+#endif /* CVC5__EXPR__VARIADIC_TRIE_H */