diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-11-05 08:26:32 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-11-05 08:26:32 -0800 |
commit | dfcfb2c663fff40254d85e88f65d6219d2bbec90 (patch) | |
tree | 263e7c9dbb863bbf2f38b595977624a23cfb3341 /src/expr | |
parent | 15bb7984ee8c75c6b33fefe5754172f468f43ed8 (diff) | |
parent | 700ee947a84ee8df9a7a50d44999a48ccc2626d8 (diff) |
Merge branch 'master' into fixConfigureTypofixConfigureTypo
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/.gitignore | 6 | ||||
-rw-r--r-- | src/expr/Makefile | 4 | ||||
-rw-r--r-- | src/expr/Makefile.am | 228 | ||||
-rw-r--r-- | src/expr/datatype.cpp | 6 | ||||
-rw-r--r-- | src/expr/datatype.h | 4 | ||||
-rw-r--r-- | src/expr/node_algorithm.cpp | 55 | ||||
-rw-r--r-- | src/expr/node_algorithm.h | 5 |
7 files changed, 65 insertions, 243 deletions
diff --git a/src/expr/.gitignore b/src/expr/.gitignore deleted file mode 100644 index 238db3ad3..000000000 --- a/src/expr/.gitignore +++ /dev/null @@ -1,6 +0,0 @@ -/kind.h -/metakind.h -/expr.cpp -/expr.h -/expr_manager.cpp -/expr_manager.h diff --git a/src/expr/Makefile b/src/expr/Makefile deleted file mode 100644 index eff3b332e..000000000 --- a/src/expr/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../.. -srcdir = src/expr - -include $(topdir)/Makefile.subdir diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am deleted file mode 100644 index f8f9dbd11..000000000 --- a/src/expr/Makefile.am +++ /dev/null @@ -1,228 +0,0 @@ -# if coverage is enabled: -# COVERAGE_ON = yes from configure.ac -# Using an inline conditional function to choose between absolute and -# relative paths for options files -# lcov does not support relative paths and src/options and src/expr -# in particular were breaking it -# Building with coverage will cause portability issues in some cases - -VPATH = $(if $(COVERAGE_ON), $(realpath @srcdir@), @srcdir@) - -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - $(if $(COVERAGE_ON), -I@abs_builddir@/.. -I@abs_srcdir@/../include -I@abs_srcdir@/.., \ - -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/..) -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libexpr.la - -# For some reason statistics were in libutil. No idea why though. -libexpr_la_SOURCES = \ - array.h \ - array_store_all.cpp \ - array_store_all.h \ - ascription_type.h \ - attribute.h \ - attribute.cpp \ - attribute_internals.h \ - attribute_unique_id.h \ - chain.h \ - emptyset.cpp \ - emptyset.h \ - expr_iomanip.cpp \ - expr_iomanip.h \ - expr_manager_scope.h \ - expr_stream.h \ - kind_map.h \ - matcher.h \ - node.cpp \ - node.h \ - node_algorithm.cpp \ - node_algorithm.h \ - node_builder.h \ - node_manager.cpp \ - node_manager.h \ - node_manager_attributes.h \ - node_manager_listeners.cpp \ - node_manager_listeners.h \ - node_self_iterator.h \ - node_value.cpp \ - node_value.h \ - pickle_data.cpp \ - pickle_data.h \ - pickler.cpp \ - pickler.h \ - symbol_table.cpp \ - symbol_table.h \ - type.cpp \ - type.h \ - type_checker.h \ - type_node.cpp \ - type_node.h \ - variable_type_map.h \ - datatype.h \ - datatype.cpp \ - record.cpp \ - record.h \ - uninterpreted_constant.cpp \ - uninterpreted_constant.h - -nodist_libexpr_la_SOURCES = \ - kind.h \ - kind.cpp \ - metakind.h \ - metakind.cpp \ - type_properties.h \ - expr.h \ - expr.cpp \ - expr_manager.h \ - expr_manager.cpp \ - type_checker.cpp - -EXTRA_DIST = \ - array.i \ - chain.i \ - array_store_all.i \ - ascription_type.i \ - datatype.i \ - emptyset.i \ - kind_template.h \ - kind_template.cpp \ - metakind_template.h \ - metakind_template.cpp \ - type_properties_template.h \ - expr_manager_template.h \ - expr_manager_template.cpp \ - expr_template.h \ - expr_template.cpp \ - type_checker_template.cpp \ - mkkind \ - mkmetakind \ - mkexpr \ - expr_stream.i \ - expr_manager.i \ - symbol_table.i \ - type.i \ - kind.i \ - expr.i \ - record.i \ - variable_type_map.i \ - uninterpreted_constant.i - -BUILT_SOURCES = \ - kind.h \ - kind.cpp \ - metakind.h \ - metakind.cpp \ - type_properties.h \ - expr.h \ - expr.cpp \ - expr_manager.h \ - expr_manager.cpp \ - type_checker.cpp \ - $(top_builddir)/src/expr/.subdirs - -CLEANFILES = \ - kind.h \ - kind.cpp \ - metakind.h \ - metakind.cpp \ - expr.h \ - expr.cpp \ - expr_manager.h \ - expr_manager.cpp \ - type_checker.cpp \ - type_properties.h \ - $(top_builddir)/src/expr/.subdirs - -$(top_builddir)/src/expr/.subdirs: $(top_srcdir)/src/Makefile.theories @top_srcdir@/src/mksubdirs - $(AM_V_at)test -d $(top_builddir)/src/expr || mkdir $(top_builddir)/src/expr - $(AM_V_at)chmod +x @top_srcdir@/src/mksubdirs - $(AM_V_at)( @top_srcdir@/src/mksubdirs $(if $(COVERAGE_ON), "$(abs_top_srcdir)", "$(top_srcdir)")) > $(top_builddir)/src/expr/.subdirs.tmp - @if ! diff -q $(top_builddir)/src/expr/.subdirs $(top_builddir)/src/expr/.subdirs.tmp &>/dev/null; then \ - echo " GEN " $@; \ - $(am__mv) $(top_builddir)/src/expr/.subdirs.tmp $(top_builddir)/src/expr/.subdirs; \ - fi - -kind.h: kind_template.h mkkind @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mkkind - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mkkind \ - $< \ - `cat @top_builddir@/src/expr/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -kind.cpp: kind_template.cpp mkkind @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mkkind - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mkkind \ - $< \ - `cat @top_builddir@/src/expr/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -metakind.h: metakind_template.h mkmetakind @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mkmetakind - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mkmetakind \ - $< \ - `cat @top_builddir@/src/expr/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -metakind.cpp: metakind_template.cpp mkmetakind @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mkmetakind - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mkmetakind \ - $< \ - `cat @top_builddir@/src/expr/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -type_properties.h: type_properties_template.h mkkind @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mkkind - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mkkind \ - $< \ - `cat @top_builddir@/src/expr/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -expr.h: expr_template.h mkexpr @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mkexpr - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mkexpr \ - $< \ - `cat @top_builddir@/src/expr/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -expr.cpp: expr_template.cpp mkexpr @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mkexpr - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mkexpr \ - $< \ - `cat @top_builddir@/src/expr/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -expr_manager.h: expr_manager_template.h mkexpr @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mkexpr - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mkexpr \ - $< \ - `cat @top_builddir@/src/expr/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -expr_manager.cpp: expr_manager_template.cpp mkexpr @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mkexpr - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mkexpr \ - $< \ - `cat @top_builddir@/src/expr/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -type_checker.cpp: type_checker_template.cpp mkexpr @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds - $(AM_V_at)chmod +x @srcdir@/mkexpr - $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@/mkexpr \ - $< \ - `cat @top_builddir@/src/expr/.subdirs` \ - > $@) || (rm -f $@ && exit 1) - -.PHONY: builts -builts: $(BUILT_SOURCES) diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 037a1beb2..8bedd4979 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -173,8 +173,8 @@ void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){ } void Datatype::addSygusConstructor(Expr op, - std::string& cname, - std::vector<Type>& cargs, + const std::string& cname, + const std::vector<Type>& cargs, std::shared_ptr<SygusPrintCallback> spc, int weight) { @@ -1316,7 +1316,7 @@ void DatatypeConstructorArg::toStream(std::ostream& out) const else if (d_selector.isNull()) { string typeName = d_name.substr(d_name.find('\0') + 1); - out << (typeName == "") ? "[self]" : typeName; + out << ((typeName == "") ? "[self]" : typeName); return; } else diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 3fbb7e17b..615ad0e10 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -691,8 +691,8 @@ public: * constructors. */ void addSygusConstructor(Expr op, - std::string& cname, - std::vector<Type>& cargs, + const std::string& cname, + const std::vector<Type>& cargs, std::shared_ptr<SygusPrintCallback> spc = nullptr, int weight = -1); diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 4bbfb5df8..3905ad5c9 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -63,6 +63,61 @@ bool hasSubterm(TNode n, TNode t, bool strict) return false; } +bool hasSubtermMulti(TNode n, TNode t) +{ + std::unordered_map<TNode, bool, TNodeHashFunction> visited; + std::unordered_map<TNode, bool, TNodeHashFunction> contains; + std::unordered_map<TNode, bool, TNodeHashFunction>::iterator it; + std::vector<TNode> visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + + if (it == visited.end()) + { + if (cur == t) + { + visited[cur] = true; + contains[cur] = true; + } + else + { + visited[cur] = false; + visit.push_back(cur); + for (const Node& cc : cur) + { + visit.push_back(cc); + } + } + } + else if (!it->second) + { + bool doesContain = false; + for (const Node& cn : cur) + { + it = contains.find(cn); + Assert(it != visited.end()); + if (it->second) + { + if (doesContain) + { + // two children have t, return true + return true; + } + doesContain = true; + } + } + contains[cur] = doesContain; + visited[cur] = true; + } + } while (!visit.empty()); + return false; +} + struct HasBoundVarTag { }; diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index 7453bc292..d825d7f57 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -39,6 +39,11 @@ namespace expr { bool hasSubterm(TNode n, TNode t, bool strict = false); /** + * Check if the node n has >1 occurrences of a subterm t. + */ +bool hasSubtermMulti(TNode n, TNode t); + +/** * Returns true iff the node n contains a bound variable, that is a node of * kind BOUND_VARIABLE. This bound variable may or may not be free. * @param n The node under investigation |