summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2018-11-05 08:26:32 -0800
committerGitHub <noreply@github.com>2018-11-05 08:26:32 -0800
commitdfcfb2c663fff40254d85e88f65d6219d2bbec90 (patch)
tree263e7c9dbb863bbf2f38b595977624a23cfb3341 /src/expr
parent15bb7984ee8c75c6b33fefe5754172f468f43ed8 (diff)
parent700ee947a84ee8df9a7a50d44999a48ccc2626d8 (diff)
Merge branch 'master' into fixConfigureTypofixConfigureTypo
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/.gitignore6
-rw-r--r--src/expr/Makefile4
-rw-r--r--src/expr/Makefile.am228
-rw-r--r--src/expr/datatype.cpp6
-rw-r--r--src/expr/datatype.h4
-rw-r--r--src/expr/node_algorithm.cpp55
-rw-r--r--src/expr/node_algorithm.h5
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback