From 4df14f1e09549be607123c66b7dd206e8e244c89 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 27 May 2020 18:05:07 -0500 Subject: [PATCH] Add the Expr-level sequence datatype (#4526) This adds the expr-level sequence datatypes. This is required for further progress on sequences. However, note that this class may be deleted in the further when the Expr level is replaced. --- src/CMakeLists.txt | 1 + src/bindings/java/CMakeLists.txt | 1 + src/cvc4.i | 1 + src/expr/CMakeLists.txt | 4 ++ src/expr/expr.i | 1 + src/expr/expr_manager.i | 1 + src/expr/expr_sequence.cpp | 98 ++++++++++++++++++++++++++++++++ src/expr/expr_sequence.h | 76 +++++++++++++++++++++++++ src/expr/expr_sequence.i | 18 ++++++ src/expr/sequence.cpp | 12 ++++ src/expr/sequence.h | 4 ++ src/theory/strings/kinds | 6 ++ 12 files changed, 223 insertions(+) create mode 100644 src/expr/expr_sequence.cpp create mode 100644 src/expr/expr_sequence.h create mode 100644 src/expr/expr_sequence.i diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index ff11897e9..e9be4dd3e 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -923,6 +923,7 @@ install(FILES expr/datatype.h expr/emptyset.h expr/expr_iomanip.h + expr/expr_sequence.h expr/record.h expr/symbol_table.h expr/type.h diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt index c5abf9b27..2cecf15e9 100644 --- a/src/bindings/java/CMakeLists.txt +++ b/src/bindings/java/CMakeLists.txt @@ -65,6 +65,7 @@ set(gen_java_files ${CMAKE_CURRENT_BINARY_DIR}/ExprHashFunction.java ${CMAKE_CURRENT_BINARY_DIR}/ExprManager.java ${CMAKE_CURRENT_BINARY_DIR}/ExprManagerMapCollection.java + ${CMAKE_CURRENT_BINARY_DIR}/ExprSequence.java ${CMAKE_CURRENT_BINARY_DIR}/FloatingPoint.java ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointConvertSort.java ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointSize.java diff --git a/src/cvc4.i b/src/cvc4.i index 01fd088a8..6b3598a2f 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -286,6 +286,7 @@ std::set CVC4::JavaInputStreamAdapter::s_adapters; %include "expr/array_store_all.i" %include "expr/ascription_type.i" %include "expr/emptyset.i" +%include "expr/expr_sequence.i" %include "expr/datatype.i" %include "expr/record.i" %include "proof/unsat_core.i" diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index f2a4377d0..413041213 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -12,6 +12,8 @@ libcvc4_add_sources( expr_iomanip.cpp expr_iomanip.h expr_manager_scope.h + expr_sequence.cpp + expr_sequence.h kind_map.h match_trie.cpp match_trie.h @@ -32,6 +34,8 @@ libcvc4_add_sources( node_traversal.h node_value.cpp node_value.h + sequence.cpp + sequence.h node_visitor.h proof.cpp proof.h diff --git a/src/expr/expr.i b/src/expr/expr.i index 14ccf213c..14228d7c5 100644 --- a/src/expr/expr.i +++ b/src/expr/expr.i @@ -146,6 +146,7 @@ namespace CVC4 { %template(getConstBoolean) CVC4::Expr::getConst; %template(getConstDatatypeIndexConstant) CVC4::Expr::getConst; %template(getConstEmptySet) CVC4::Expr::getConst; +%template(getConstExprSequence) CVC4::Expr::getConst; %template(getConstFloatingPoint) CVC4::Expr::getConst; %template(getConstKind) CVC4::Expr::getConst; %template(getConstRational) CVC4::Expr::getConst; diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i index f8251e752..5a5e7a9d4 100644 --- a/src/expr/expr_manager.i +++ b/src/expr/expr_manager.i @@ -57,6 +57,7 @@ %template(mkConst) CVC4::ExprManager::mkConst; %template(mkConst) CVC4::ExprManager::mkConst; %template(mkConst) CVC4::ExprManager::mkConst; +%template(mkConst) CVC4::ExprManager::mkConst; %template(mkConst) CVC4::ExprManager::mkConst; #ifdef SWIGPYTHON /* The python bindings cannot differentiate between bool and other basic diff --git a/src/expr/expr_sequence.cpp b/src/expr/expr_sequence.cpp new file mode 100644 index 000000000..4f761c8f7 --- /dev/null +++ b/src/expr/expr_sequence.cpp @@ -0,0 +1,98 @@ +/********************* */ +/*! \file expr_sequence.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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.\endverbatim + ** + ** \brief Implementation of the sequence data type. + **/ + +#include "expr/expr_sequence.h" + +#include "expr/expr.h" +#include "expr/node.h" +#include "expr/sequence.h" +#include "expr/type.h" +#include "expr/type_node.h" + +namespace CVC4 { + +ExprSequence::ExprSequence(const Type& t, const std::vector& seq) +{ + d_type.reset(new Type(t)); + std::vector nseq; + for (const Expr& e : seq) + { + nseq.push_back(Node::fromExpr(e)); + } + d_sequence.reset(new Sequence(TypeNode::fromType(t), nseq)); +} +ExprSequence::~ExprSequence() {} + +ExprSequence::ExprSequence(const ExprSequence& other) + : d_type(new Type(other.getType())), + d_sequence(new Sequence(other.getSequence())) +{ +} + +ExprSequence& ExprSequence::operator=(const ExprSequence& other) +{ + (*d_type) = other.getType(); + (*d_sequence) = other.getSequence(); + return *this; +} + +const Type& ExprSequence::getType() const { return *d_type; } + +const Sequence& ExprSequence::getSequence() const { return *d_sequence; } + +bool ExprSequence::operator==(const ExprSequence& es) const +{ + return getType() == es.getType() && getSequence() == es.getSequence(); +} + +bool ExprSequence::operator!=(const ExprSequence& es) const +{ + return !(*this == es); +} + +bool ExprSequence::operator<(const ExprSequence& es) const +{ + return (getType() < es.getType()) + || (getType() == es.getType() && getSequence() < es.getSequence()); +} + +bool ExprSequence::operator<=(const ExprSequence& es) const +{ + return (getType() < es.getType()) + || (getType() == es.getType() && getSequence() <= es.getSequence()); +} + +bool ExprSequence::operator>(const ExprSequence& es) const +{ + return !(*this <= es); +} + +bool ExprSequence::operator>=(const ExprSequence& es) const +{ + return !(*this < es); +} + +std::ostream& operator<<(std::ostream& os, const ExprSequence& s) +{ + return os << "__expr_sequence__(" << s.getType() << ", " << s.getSequence() + << ")"; +} + +size_t ExprSequenceHashFunction::operator()(const ExprSequence& es) const +{ + uint64_t hash = fnv1a::fnv1a_64(TypeHashFunction()(es.getType())); + return static_cast(SequenceHashFunction()(es.getSequence()), hash); +} + +} // namespace CVC4 diff --git a/src/expr/expr_sequence.h b/src/expr/expr_sequence.h new file mode 100644 index 000000000..9515a9244 --- /dev/null +++ b/src/expr/expr_sequence.h @@ -0,0 +1,76 @@ +/********************* */ +/*! \file expr_sequence.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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.\endverbatim + ** + ** \brief The sequence data type. + **/ + +#include "cvc4_public.h" + +#ifndef CVC4__EXPR__EXPR_SEQUENCE_H +#define CVC4__EXPR__EXPR_SEQUENCE_H + +#include +#include +#include + +namespace CVC4 { + +// messy; Expr needs ExprSequence (because it's the payload of a +// CONSTANT-kinded expression), and ExprSequence needs Expr. +class Type; +class Expr; +class Sequence; + +/** The CVC4 sequence class + * + * This data structure is the domain of values for the sequence type. + */ +class CVC4_PUBLIC ExprSequence +{ + public: + /** constructors for ExprSequence + * + * Internally, a CVC4::ExprSequence is represented by a vector of Nodes + * (d_seq), where each Node in this vector must be a constant. + */ + ExprSequence(const Type& type, const std::vector& seq); + ~ExprSequence(); + + ExprSequence(const ExprSequence& other); + ExprSequence& operator=(const ExprSequence& other); + + bool operator==(const ExprSequence& es) const; + bool operator!=(const ExprSequence& es) const; + bool operator<(const ExprSequence& es) const; + bool operator<=(const ExprSequence& es) const; + bool operator>(const ExprSequence& es) const; + bool operator>=(const ExprSequence& es) const; + + const Type& getType() const; + const Sequence& getSequence() const; + + private: + /** The element type of the sequence */ + std::unique_ptr d_type; + /** The data of the sequence */ + std::unique_ptr d_sequence; +}; /* class ExprSequence */ + +struct CVC4_PUBLIC ExprSequenceHashFunction +{ + size_t operator()(const ::CVC4::ExprSequence& s) const; +}; /* struct ExprSequenceHashFunction */ + +std::ostream& operator<<(std::ostream& os, const ExprSequence& s) CVC4_PUBLIC; + +} // namespace CVC4 + +#endif /* CVC4__EXPR__SEQUENCE_H */ diff --git a/src/expr/expr_sequence.i b/src/expr/expr_sequence.i new file mode 100644 index 000000000..42e130466 --- /dev/null +++ b/src/expr/expr_sequence.i @@ -0,0 +1,18 @@ +%{ +#include "expr/expr_sequence.h" +%} + +%rename(equals) CVC4::ExprSequence::operator==(const ExprSequence&) const; +%ignore CVC4::ExprSequence::operator!=(const ExprSequence&) const; +%ignore CVC4::ExprSequence::getSequence() const; + +%rename(less) CVC4::ExprSequence::operator<(const ExprSequence&) const; +%rename(lessEqual) CVC4::ExprSequence::operator<=(const ExprSequence&) const; +%rename(greater) CVC4::ExprSequence::operator>(const ExprSequence&) const; +%rename(greaterEqual) CVC4::ExprSequence::operator>=(const ExprSequence&) const; + +%rename(apply) CVC4::ExprSequenceHashFunction::operator()(const ExprSequence&) const; + +%ignore CVC4::operator<<(std::ostream& out, const ExprSequence& es); + +%include "expr/expr_sequence.h" diff --git a/src/expr/sequence.cpp b/src/expr/sequence.cpp index e42a67bbe..f70a70027 100644 --- a/src/expr/sequence.cpp +++ b/src/expr/sequence.cpp @@ -14,6 +14,8 @@ #include "expr/sequence.h" +#include "expr/expr_sequence.h" + using namespace std; namespace CVC4 { @@ -297,6 +299,16 @@ bool Sequence::noOverlapWith(const Sequence& y) const size_t Sequence::maxSize() { return std::numeric_limits::max(); } +ExprSequence Sequence::toExprSequence() +{ + std::vector seq; + for (const Node& n : d_seq) + { + seq.push_back(n.toExpr()); + } + return ExprSequence(d_type.toType(), seq); +} + std::ostream& operator<<(std::ostream& os, const Sequence& s) { const std::vector& vec = s.getVec(); diff --git a/src/expr/sequence.h b/src/expr/sequence.h index 833e79441..2e0721b4a 100644 --- a/src/expr/sequence.h +++ b/src/expr/sequence.h @@ -144,6 +144,10 @@ class Sequence */ static size_t maxSize(); + //!!!!!!!!!!!!!!! temporary + ExprSequence toExprSequence(); + //!!!!!!!!!!!!!!! end temporary + private: /** * Returns a negative number if *this < y, 0 if *this and y are equal and a diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 06f05a8af..27ffe5d26 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -58,6 +58,12 @@ constant CONST_STRING \ "util/string.h" \ "a string of characters" +constant CONST_SEQUENCE \ + ::CVC4::ExprSequence \ + ::CVC4::ExprSequenceHashFunction \ + "expr/expr_sequence.h" \ + "a sequence of characters" + # equal equal / less than / output operator STRING_TO_REGEXP 1 "convert string to regexp" operator REGEXP_CONCAT 2: "regexp concat" -- 2.30.2