Merge branch 'master' of https://github.com/Z3Prover/z3

scripts/mk_project.py

@@ -81,17 +81,17 @@ def init_project_def():
             includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files)
     add_exe('shell', ['api', 'sat', 'extra_cmds','opt'], exe_name='z3')
     add_exe('test', ['api', 'fuzzing', 'simplex'], exe_name='test-z3', install=False)
-    add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', 
+    _libz3Component = add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll',
-            reexports=['api'], 
+                              reexports=['api'],
-            dll_name='libz3', 
+                              dll_name='libz3',
-            static=build_static_lib(),
+                              static=build_static_lib(),
-            export_files=API_files)
+                              export_files=API_files)
     add_dot_net_dll('dotnet', ['api_dll'], 'api/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties')
     add_java_dll('java', ['api_dll'], 'api/java', dll_name='libz3java', package_name="com.microsoft.z3", manifest_file='manifest')
     add_ml_lib('ml', ['api_dll'], 'api/ml', lib_name='libz3ml')
     add_hlib('cpp', 'api/c++', includes2install=['z3++.h'])
     set_z3py_dir('api/python')
-    add_python_install()
+    add_python_install(_libz3Component)
     # Examples
     add_cpp_example('cpp_example', 'c++') 
     add_cpp_example('z3_tptp', 'tptp') 

scripts/mk_util.py

@@ -718,7 +718,9 @@ def parse_options():
             display_help(1)
     # Handle the Python package directory
     if IS_WINDOWS:
-        PYTHON_INSTALL_ENABLED = True
+        # Installing under Windows doesn't make sense as the install prefix is used
+        # but that doesn't make sense under Windows
+        PYTHON_INSTALL_ENABLED = False
     else:
         if not PYTHON_PACKAGE_DIR.startswith(PREFIX):
             print(("Warning: The detected Python package directory (%s)"
@@ -726,7 +728,14 @@ def parse_options():
                    ". This would lead to a broken Python installation."
                    "Use --pypkgdir= to change the Python package directory") %
                   (PYTHON_PACKAGE_DIR, PREFIX))
-            PYTHON_INSTALL_ENABLED = False
+            if IS_OSX and PYTHON_PACKAGE_DIR.startswith('/Library/'):
+                print("Using hack to install Python bindings, this might lead to a broken system")
+                PYTHON_INSTALL_ENABLED = True
+            else:
+                print("Disabling install of Python bindings")
+                PYTHON_INSTALL_ENABLED = False
+        else:
+            PYTHON_INSTALL_ENABLED = True
 
 # Return a list containing a file names included using '#include' in
 # the given C/C++ file named fname.
@@ -1216,11 +1225,23 @@ class DLLComponent(Component):
         else:
             return self.name + '$(SO_EXT)'
 
+    def dll_file(self):
+        """
+            Return file name of component suitable for use in a Makefile
+        """
+        return '%s$(SO_EXT)' % self.dll_name
+
+    def install_path(self):
+        """
+            Return install location of component (relative to prefix)
+            suitable for use in a Makefile
+        """
+        return os.path.join(INSTALL_LIB_DIR, self.dll_file())
+
     def mk_makefile(self, out):
         Component.mk_makefile(self, out)
         # generate rule for (SO_EXT)
-        dllfile = '%s$(SO_EXT)' % self.dll_name
+        out.write('%s:' % self.dll_file())
-        out.write('%s:' % dllfile)
         deps = sort_components(self.deps)
         objs = []
         for cppfile in get_cpp_files(self.src_dir):
@@ -1240,7 +1261,7 @@ class DLLComponent(Component):
                 c_dep = get_component(dep)
                 out.write(' ' + c_dep.get_link_name())
         out.write('\n')
-        out.write('\t$(LINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS)' % dllfile)
+        out.write('\t$(LINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS)' % self.dll_file())
         for obj in objs:
             out.write(' ')
             out.write(obj)
@@ -1256,9 +1277,9 @@ class DLLComponent(Component):
         if self.static:
             self.mk_static(out)
             libfile = '%s$(LIB_EXT)' % self.dll_name
-            out.write('%s: %s %s\n\n' % (self.name, dllfile, libfile))
+            out.write('%s: %s %s\n\n' % (self.name, self.dll_file(), libfile))
         else:
-            out.write('%s: %s\n\n' % (self.name, dllfile))
+            out.write('%s: %s\n\n' % (self.name, self.dll_file()))
 
     def mk_static(self, out):
         # generate rule for lib
@@ -1303,30 +1324,13 @@ class DLLComponent(Component):
 
     def mk_install(self, out):
         if self.install:
-            dllfile = '%s$(SO_EXT)' % self.dll_name
+            MakeRuleCmd.install_files(out, self.dll_file(), self.install_path())
-            dllInstallPath = os.path.join(INSTALL_LIB_DIR, dllfile)
-            MakeRuleCmd.install_files(out, dllfile, dllInstallPath)
-            if not is_python_install_enabled():
-                return
-            pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
-            if IS_WINDOWS:
-                MakeRuleCmd.install_files(out, dllfile, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
-            else:
-                # Create symbolic link to save space.
-                # It's important that this symbolic link be relative (rather
-                # than absolute) so that the install is relocatable (needed for
-                # staged installs that use DESTDIR).
-                MakeRuleCmd.create_relative_symbolic_link(out, dllInstallPath, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
             if self.static:
                 libfile = '%s$(LIB_EXT)' % self.dll_name
                 MakeRuleCmd.install_files(out, libfile, os.path.join(INSTALL_LIB_DIR, libfile))
 
     def mk_uninstall(self, out):
-        dllfile = '%s$(SO_EXT)' % self.dll_name
+        MakeRuleCmd.remove_installed_files(out, self.install_path())
-        MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, dllfile))
-        if is_python_install_enabled():
-            pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
-            MakeRuleCmd.remove_installed_files(out, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
         libfile = '%s$(LIB_EXT)' % self.dll_name
         MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, libfile))
 
@@ -1348,29 +1352,74 @@ class DLLComponent(Component):
                         '%s.a' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
 
 class PythonInstallComponent(Component):
-    def __init__(self, name):
+    def __init__(self, name, libz3Component):
+        assert isinstance(libz3Component, DLLComponent)
         Component.__init__(self, name, None, [])
+        self.pythonPkgDir = None
+        self.in_prefix_install = True
+        self.libz3Component = libz3Component
+        if not PYTHON_INSTALL_ENABLED:
+            return
+
+        if self.is_osx_hack():
+            # Use full path that is outside of install prefix
+            self.pythonPkgDir = PYTHON_PACKAGE_DIR
+            self.in_prefix_install = False
+            assert os.path.isabs(self.pythonPkgDir)
+        else:
+            # Use path inside the prefix (should be the normal case)
+            assert PYTHON_PACKAGE_DIR.startswith(PREFIX)
+            self.pythonPkgDir = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
+            assert not os.path.isabs(self.pythonPkgDir)
+            assert self.in_prefix_install
+
+    def is_osx_hack(self):
+        return IS_OSX and not PYTHON_PACKAGE_DIR.startswith(PREFIX)
 
     def main_component(self):
         return False    
     
-    def install_deps(self, out):
-        if not is_python_install_enabled():
-            return
-        pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
-        MakeRuleCmd.make_install_directory(out, pythonPkgDirWithoutPrefix)
-
     def mk_install(self, out):
         if not is_python_install_enabled():
             return
-        pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
+        MakeRuleCmd.make_install_directory(out, self.pythonPkgDir, in_prefix=self.in_prefix_install)
-        MakeRuleCmd.install_files(out, 'z3*.py', pythonPkgDirWithoutPrefix)
+
-        if sys.version >= "3":
+        # Sym-link or copy libz3 into python package directory
-            pythonPycacheDir = os.path.join(pythonPkgDirWithoutPrefix, '__pycache__')
+        if IS_WINDOWS or self.is_osx_hack():
-            MakeRuleCmd.make_install_directory(out, pythonPycacheDir)
+            MakeRuleCmd.install_files(out,
-            MakeRuleCmd.install_files(out, '{}*.pyc'.format(os.path.join('__pycache__', 'z3')), pythonPycacheDir)
+                                      self.libz3Component.dll_file(),
+                                      os.path.join(self.pythonPkgDir,
+                                                   self.libz3Component.dll_file()),
+                                      in_prefix=self.in_prefix_install
+                                     )
         else:
-            MakeRuleCmd.install_files(out, 'z3*.pyc', pythonPkgDirWithoutPrefix)
+            # Create symbolic link to save space.
+            # It's important that this symbolic link be relative (rather
+            # than absolute) so that the install is relocatable (needed for
+            # staged installs that use DESTDIR).
+            MakeRuleCmd.create_relative_symbolic_link(out,
+                                                      self.libz3Component.install_path(),
+                                                      os.path.join(self.pythonPkgDir,
+                                                                   self.libz3Component.dll_file()
+                                                                  ),
+                                                     )
+
+        MakeRuleCmd.install_files(out, 'z3*.py', self.pythonPkgDir,
+                                  in_prefix=self.in_prefix_install)
+        if sys.version >= "3":
+            pythonPycacheDir = os.path.join(self.pythonPkgDir, '__pycache__')
+            MakeRuleCmd.make_install_directory(out,
+                                               pythonPycacheDir,
+                                               in_prefix=self.in_prefix_install)
+            MakeRuleCmd.install_files(out,
+                                      '{}*.pyc'.format(os.path.join('__pycache__', 'z3')),
+                                      pythonPycacheDir,
+                                      in_prefix=self.in_prefix_install)
+        else:
+            MakeRuleCmd.install_files(out,
+                                      'z3*.pyc',
+                                      self.pythonPkgDir,
+                                      in_prefix=self.in_prefix_install)
         if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib():
             if os.uname()[0] == 'Darwin':
                 LD_LIBRARY_PATH = "DYLD_LIBRARY_PATH"
@@ -1383,10 +1432,21 @@ class PythonInstallComponent(Component):
     def mk_uninstall(self, out):
         if not is_python_install_enabled():
             return
-        pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
+        MakeRuleCmd.remove_installed_files(out,
-        MakeRuleCmd.remove_installed_files(out, '{}*.py'.format(os.path.join(pythonPkgDirWithoutPrefix, 'z3')))
+                                           os.path.join(self.pythonPkgDir,
-        MakeRuleCmd.remove_installed_files(out, '{}*.pyc'.format(os.path.join(pythonPkgDirWithoutPrefix, 'z3')))
+                                                        self.libz3Component.dll_file()),
-        MakeRuleCmd.remove_installed_files(out, '{}*.pyc'.format(os.path.join(pythonPkgDirWithoutPrefix, '__pycache__', 'z3')))
+                                           in_prefix=self.in_prefix_install
+                                          )
+        MakeRuleCmd.remove_installed_files(out,
+                                           '{}*.py'.format(os.path.join(self.pythonPkgDir, 'z3')),
+                                           in_prefix=self.in_prefix_install)
+        MakeRuleCmd.remove_installed_files(out,
+                                           '{}*.pyc'.format(os.path.join(self.pythonPkgDir, 'z3')),
+                                           in_prefix=self.in_prefix_install)
+        MakeRuleCmd.remove_installed_files(out,
+                                           '{}*.pyc'.format(os.path.join(self.pythonPkgDir, '__pycache__', 'z3')),
+                                           in_prefix=self.in_prefix_install
+                                          )
 
     def mk_makefile(self, out):
         return
@@ -1791,13 +1851,13 @@ class MLComponent(Component):
             self.mk_ml_meta(os.path.join('src/api/ml/META'), os.path.join(BUILD_DIR, self.sub_dir, 'META'), VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION)
 
     def mk_install_deps(self, out):
-        if OCAMLFIND != '':
+        if is_ml_enabled() and OCAMLFIND != '':
             out.write(get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT) ')
             out.write(os.path.join(self.sub_dir, 'z3ml.cmxa '))
             out.write(os.path.join(self.sub_dir, 'META '))
 
     def mk_install(self, out):
-        if OCAMLFIND != '':
+        if is_ml_enabled() and OCAMLFIND != '':
             out.write('\t@%s remove Z3\n' % (OCAMLFIND))
             out.write('\t@%s install Z3 %s' % (OCAMLFIND, (os.path.join(self.sub_dir, 'META'))))
             for m in self.modules:
@@ -1823,7 +1883,7 @@ class MLComponent(Component):
             out.write('\n')
 
     def mk_uninstall(self, out):
-        if OCAMLFIND != '':
+        if is_ml_enabled() and OCAMLFIND != '':
             out.write('\t@%s remove Z3\n' % (OCAMLFIND))
 
     def main_component(self):
@@ -2017,6 +2077,7 @@ def add_extra_exe(name, deps=[], path=None, exe_name=None, install=True):
 def add_dll(name, deps=[], path=None, dll_name=None, export_files=[], reexports=[], install=True, static=False):
     c = DLLComponent(name, dll_name, path, deps, export_files, reexports, install, static)
     reg_component(name, c)
+    return c
 
 def add_dot_net_dll(name, deps=[], path=None, dll_name=None, assembly_info_dir=None):
     c = DotNetDLLComponent(name, dll_name, path, deps, assembly_info_dir)
@@ -2026,9 +2087,9 @@ def add_java_dll(name, deps=[], path=None, dll_name=None, package_name=None, man
     c = JavaDLLComponent(name, dll_name, package_name, manifest_file, path, deps)
     reg_component(name, c)
 
-def add_python_install():
+def add_python_install(libz3Component):
     name = 'python_install'
-    reg_component(name, PythonInstallComponent(name))
+    reg_component(name, PythonInstallComponent(name, libz3Component))
 
 def add_ml_lib(name, deps=[], path=None, lib_name=None):
     c = MLComponent(name, lib_name, path, deps)
@@ -3468,37 +3529,56 @@ class MakeRuleCmd(object):
         return "$(DESTDIR)$(PREFIX)/"
 
     @classmethod
-    def install_files(cls, out, src_pattern, dest):
+    def _install_root(cls, path, in_prefix, out):
+        if in_prefix:
+            assert not os.path.isabs(path)
+            install_root = cls.install_root()
+        else:
+            # This hack only exists for the Python bindings on OSX
+            # which are sometimes not installed inside the prefix.
+            # In all other cases installing outside the prefix is
+            # misleading and dangerous!
+            assert IS_OSX
+            assert os.path.isabs(path)
+            install_root = "$(DESTDIR)"
+            cls.write_cmd(out, 'echo "WARNING: {} is not in the install prefix. This will likely lead to a broken installation."'.format(path))
+        return install_root
+
+    @classmethod
+    def install_files(cls, out, src_pattern, dest, in_prefix=True):
         assert len(dest) > 0
         assert isinstance(src_pattern, str)
         assert not ' ' in src_pattern
         assert isinstance(dest, str)
         assert not ' ' in dest
         assert not os.path.isabs(src_pattern)
-        assert not os.path.isabs(dest)
+        install_root = cls._install_root(dest, in_prefix, out)
+
         cls.write_cmd(out, "cp {src_pattern} {install_root}{dest}".format(
             src_pattern=src_pattern,
-            install_root=cls.install_root(),
+            install_root=install_root,
             dest=dest))
 
     @classmethod
-    def remove_installed_files(cls, out, pattern):
+    def remove_installed_files(cls, out, pattern, in_prefix=True):
         assert len(pattern) > 0
         assert isinstance(pattern, str)
         assert not ' ' in pattern
-        assert not os.path.isabs(pattern)
+        install_root = cls._install_root(pattern, in_prefix, out)
+
         cls.write_cmd(out, "rm -f {install_root}{pattern}".format(
-            install_root=cls.install_root(),
+            install_root=install_root,
             pattern=pattern))
 
     @classmethod
-    def make_install_directory(cls, out, dir):
+    def make_install_directory(cls, out, dir, in_prefix=True):
         assert len(dir) > 0
         assert isinstance(dir, str)
         assert not ' ' in dir
-        assert not os.path.isabs(dir)
+        install_root = cls._install_root(dir, in_prefix, out)
+
         cls.write_cmd(out, "mkdir -p {install_root}{dir}".format(
-            install_root=cls.install_root(),
+            install_root=install_root,
             dir=dir))
 
     @classmethod
@@ -3537,10 +3617,11 @@ class MakeRuleCmd(object):
         # it's a file
         if link_name[-1] != '/':
             # link_name is a file
-            temp_path = '/' + os.path.dirname(link_name)
+            temp_path = os.path.dirname(link_name)
         else:
             # link_name is a directory
-            temp_path = '/' + link_name[:-1]
+            temp_path = link_name[:-1]
+        temp_path = '/' + temp_path
         relative_path = ""
         targetAsAbs = '/' + target
         assert os.path.isabs(targetAsAbs)
@@ -3564,7 +3645,7 @@ class MakeRuleCmd(object):
         assert isinstance(target, str)
         assert isinstance(link_name, str)
         assert not os.path.isabs(target)
-        assert not os.path.isabs(link_name)
+
         cls.write_cmd(out, 'ln -s {target} {install_root}{link_name}'.format(
             target=target,
             install_root=cls.install_root(),

src/muz/rel/dl_base.cpp

@@ -484,126 +484,4 @@ namespace datalog {
         }
         brw.mk_or(disjs.size(), disjs.c_ptr(), fml);        
     }
-
-    class table_plugin::min_fn : public table_min_fn{
-        table_signature m_sig;
-        const unsigned_vector m_group_by_cols;
-        const unsigned m_col;
-    public:
-        min_fn(const table_signature & t_sig, const unsigned_vector& group_by_cols, const unsigned col)
-            : m_sig(t_sig),
-            m_group_by_cols(group_by_cols),
-            m_col(col) {}
-
-        virtual table_base* operator()(table_base const& t) {
-            //return reference_implementation(t);
-            return reference_implementation_with_hash(t);
-        }
-
-    private:
-
-        /**
-        Reference implementation with negation:
-
-        T1 = join(T, T) by group_cols
-        T2 = { (t1,t2) in T1 | t1[col] > t2[col] }
-        T3 = { t1 | (t1,t2) in T2 }
-        T4 = T \ T3
-
-        The point of this reference implementation is to show
-        that the minimum requires negation (set difference).
-        This is relevant for fixed point computations.
-        */
-        virtual table_base * reference_implementation(const table_base & t) {
-            relation_manager & manager = t.get_manager();
-            scoped_ptr<table_join_fn> join_fn = manager.mk_join_fn(t, t, m_group_by_cols, m_group_by_cols);
-            scoped_rel<table_base> join_table = (*join_fn)(t, t);
-
-            table_base::iterator join_table_it = join_table->begin();
-            table_base::iterator join_table_end = join_table->end();
-            table_fact row;
-
-            table_element i, j;
-
-            for (; join_table_it != join_table_end; ++join_table_it) {
-                join_table_it->get_fact(row);
-                i = row[m_col];
-                j = row[t.num_columns() + m_col];
-
-                if (i > j) {
-                    continue;
-                }
-
-                join_table->remove_fact(row);
-            }
-
-            unsigned_vector cols(t.num_columns());
-            for (unsigned k = 0; k < cols.size(); ++k) {
-                cols[k] = cols.size() + k;
-                SASSERT(cols[k] < join_table->num_columns());
-            }
-
-            scoped_ptr<table_transformer_fn> project_fn = manager.mk_project_fn(*join_table, cols);
-            scoped_rel<table_base> gt_table = (*project_fn)(*join_table);
-
-            for (unsigned k = 0; k < cols.size(); ++k) {
-                cols[k] = k;
-                SASSERT(cols[k] < t.num_columns());
-                SASSERT(cols[k] < gt_table->num_columns());
-            }
-
-            table_base * result = t.clone();
-            scoped_ptr<table_intersection_filter_fn> diff_fn = manager.mk_filter_by_negation_fn(*result, *gt_table, cols, cols);
-            (*diff_fn)(*result, *gt_table);
-            return result;
-        }
-
-        typedef map < table_fact, table_element, svector_hash_proc<table_element_hash>,
-            vector_eq_proc<table_fact> > group_map;
-
-        // Thanks to Nikolaj who kindly helped with the second reference implementation!
-        virtual table_base * reference_implementation_with_hash(const table_base & t) {
-            group_map group;
-            table_base::iterator it = t.begin();
-            table_base::iterator end = t.end();
-            table_fact row, row2;
-            table_element current_value, min_value;
-            for (; it != end; ++it) {
-                it->get_fact(row);
-                current_value = row[m_col];
-                group_by(row, row2);
-                group_map::entry* entry = group.find_core(row2);
-                if (!entry) {
-                    group.insert(row2, current_value);
-                }
-                else if (entry->get_data().m_value > current_value) {
-                    entry->get_data().m_value = current_value;
-                }
-            }
-            table_base* result = t.get_plugin().mk_empty(m_sig);
-            table_base::iterator it2 = t.begin();
-            for (; it2 != end; ++it2) {
-                it2->get_fact(row);
-                current_value = row[m_col];
-                group_by(row, row2);
-                VERIFY(group.find(row2, min_value));
-                if (min_value == current_value) {
-                    result->add_fact(row);
-                }
-            }
-            return result;
-        }
-
-        void group_by(table_fact const& in, table_fact& out) {
-            out.reset();
-            for (unsigned i = 0; i < m_group_by_cols.size(); ++i) {
-                out.push_back(in[m_group_by_cols[i]]);
-            }
-        }
-    };
-
-    table_min_fn * table_plugin::mk_min_fn(const table_base & t,
-        unsigned_vector & group_by_cols, const unsigned col) {
-        return alloc(table_plugin::min_fn, t.get_signature(), group_by_cols, col);
-    }
 }

src/muz/rel/dl_base.h

@@ -192,29 +192,6 @@ namespace datalog {
             virtual base_object * operator()(const base_object & t1, const base_object & t2) = 0;
         };
 
-        /**
-        \brief Aggregate minimum value
-
-        Informally, we want to group rows in a table \c t by \c group_by_cols and
-        return the minimum value in column \c col among each group.
-
-        Let \c t be a table with N columns.
-        Let \c group_by_cols be a set of column identifers for table \c t such that |group_by_cols| < N.
-        Let \c col be a column identifier for table \c t such that \c col is not in \c group_by_cols.
-
-        Let R_col be a set of rows in table \c t such that, for all rows r_i, r_j in R_col
-        and column identifiers k in \c group_by_cols, r_i[k] = r_j[k].
-
-        For each R_col, we want to restrict R_col to those rows whose value in column \c col is minimal.
-
-        min_fn(R, group_by_cols, col) =
-        { row in R | forall row' in R . row'[group_by_cols] = row[group_by_cols] => row'[col] >= row[col] }
-        */
-        class min_fn : public base_fn {
-        public:
-            virtual base_object * operator()(const base_object & t) = 0;
-        };
-
         class transformer_fn : public base_fn {
         public:
             virtual base_object * operator()(const base_object & t) = 0;
@@ -879,7 +856,6 @@ namespace datalog {
 
     typedef table_infrastructure::base_fn base_table_fn;
     typedef table_infrastructure::join_fn table_join_fn;
-    typedef table_infrastructure::min_fn table_min_fn;
     typedef table_infrastructure::transformer_fn table_transformer_fn;
     typedef table_infrastructure::union_fn table_union_fn;
     typedef table_infrastructure::mutator_fn table_mutator_fn;
@@ -1044,7 +1020,6 @@ namespace datalog {
 
     class table_plugin : public table_infrastructure::plugin_object {
         friend class relation_manager;
-        class min_fn;
     protected:
         table_plugin(symbol const& n, relation_manager & manager) : plugin_object(n, manager) {}
     public:
@@ -1052,9 +1027,6 @@ namespace datalog {
         virtual bool can_handle_signature(const table_signature & s) { return s.functional_columns()==0; }
 
     protected:
-        virtual  table_min_fn * mk_min_fn(const table_base & t,
-            unsigned_vector & group_by_cols, const unsigned col);
-
         /**
            If the returned value is non-zero, the returned object must take ownership of \c mapper.
            Otherwise \c mapper must remain unmodified.

src/muz/rel/dl_compiler.cpp

@@ -467,9 +467,6 @@ namespace datalog {
         // whether to dealloc the previous result
         bool dealloc = true;
 
-        // setup information for min aggregation
-        unsigned_vector group_by_cols;
-
         if(pt_len == 2) {
             reg_idx t1_reg=tail_regs[0];
             reg_idx t2_reg=tail_regs[1];

src/muz/rel/dl_instruction.cpp

@@ -25,7 +25,6 @@ Revision History:
 #include"rel_context.h"
 #include"debug.h"
 #include"warning.h"
-#include"dl_table_relation.h"
 
 namespace datalog {
 
@@ -886,60 +885,6 @@ namespace datalog {
                 removed_cols, result);
     }
 
-    class instr_min : public instruction {
-        reg_idx m_source_reg;
-        reg_idx m_target_reg;
-        unsigned_vector m_group_by_cols;
-        unsigned m_min_col;
-    public:
-        instr_min(reg_idx source_reg, reg_idx target_reg, const unsigned_vector & group_by_cols, unsigned min_col)
-            : m_source_reg(source_reg),
-            m_target_reg(target_reg),
-            m_group_by_cols(group_by_cols),
-            m_min_col(min_col) {
-        }
-        virtual bool perform(execution_context & ctx) {
-            log_verbose(ctx);
-            if (!ctx.reg(m_source_reg)) {
-                ctx.make_empty(m_target_reg);
-                return true;
-            }
-
-            const relation_base & s = *ctx.reg(m_source_reg);
-            if (!s.from_table()) {
-                throw default_exception(default_exception::fmt(), "relation is not a table %s",
-                    s.get_plugin().get_name().bare_str());
-            }
-            ++ctx.m_stats.m_min;
-            const table_relation & tr = static_cast<const table_relation &>(s);
-            const table_base & source_t = tr.get_table();
-            relation_manager & r_manager = s.get_manager();
-
-            const relation_signature & r_sig = s.get_signature();
-            scoped_ptr<table_min_fn> fn = r_manager.mk_min_fn(source_t, m_group_by_cols, m_min_col);
-            table_base * target_t = (*fn)(source_t);
-
-            TRACE("dl",
-                tout << "% ";
-                target_t->display(tout);
-                tout << "\n";);
-
-            relation_base * target_r = r_manager.mk_table_relation(r_sig, target_t);
-            ctx.set_reg(m_target_reg, target_r);
-            return true;
-        }
-        virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const {
-            out << " MIN AGGR ";
-        }
-        virtual void make_annotations(execution_context & ctx) {
-        }
-    };
-
-    instruction * instruction::mk_min(reg_idx source, reg_idx target, const unsigned_vector & group_by_cols,
-        const unsigned min_col) {
-        return alloc(instr_min, source, target, group_by_cols, min_col);
-    }
-
     class instr_select_equal_and_project : public instruction {
         reg_idx m_src;
         reg_idx m_result;

src/muz/rel/dl_relation_manager.cpp

@@ -1023,12 +1023,6 @@ namespace datalog {
         return res;
     }
 
-    table_min_fn * relation_manager::mk_min_fn(const table_base & t,
-        unsigned_vector & group_by_cols, const unsigned col)
-    {
-        return t.get_plugin().mk_min_fn(t, group_by_cols, col);
-    }
-
     class relation_manager::auxiliary_table_transformer_fn {
         table_fact m_row;
     public:

src/muz/rel/dl_relation_manager.h

@@ -251,9 +251,6 @@ namespace datalog {
             return mk_join_fn(t1, t2, cols1.size(), cols1.c_ptr(), cols2.c_ptr(), allow_product_relation);
         }
 
-        table_min_fn * mk_min_fn(const table_base & t,
-            unsigned_vector & group_by_cols, const unsigned col);
-
         /**
             \brief Return functor that transforms a table into one that lacks columns listed in
             \c removed_cols array.

src/muz/rel/rel_context.cpp

@@ -291,27 +291,19 @@ namespace datalog {
         return res;
     }
 
-#define _MIN_DONE_ 1
-
     void rel_context::transform_rules() {
         rule_transformer transf(m_context);
-#ifdef _MIN_DONE_
         transf.register_plugin(alloc(mk_coi_filter, m_context));
-#endif
         transf.register_plugin(alloc(mk_filter_rules, m_context));        
         transf.register_plugin(alloc(mk_simple_joins, m_context));
         if (m_context.unbound_compressor()) {
             transf.register_plugin(alloc(mk_unbound_compressor, m_context));
         }
-#ifdef _MIN_DONE_
         if (m_context.similarity_compressor()) {
             transf.register_plugin(alloc(mk_similarity_compressor, m_context)); 
         }
-#endif
         transf.register_plugin(alloc(mk_partial_equivalence_transformer, m_context));
-#ifdef _MIN_DONE_
         transf.register_plugin(alloc(mk_rule_inliner, m_context));
-#endif
         transf.register_plugin(alloc(mk_interp_tail_simplifier, m_context));
         transf.register_plugin(alloc(mk_separate_negated_tails, m_context));
 

src/test/dl_table.cpp

@@ -95,78 +95,8 @@ void test_dl_bitvector_table() {
     test_table(mk_bv_table);
 }
 
-void test_table_min() {
-    std::cout << "----- test_table_min -----\n";
-    datalog::table_signature sig;
-    sig.push_back(2);
-    sig.push_back(4);
-    sig.push_back(8);
-    smt_params params;
-    ast_manager ast_m;
-    datalog::register_engine re;
-    datalog::context ctx(ast_m, re, params);
-    datalog::relation_manager & m = ctx.get_rel_context()->get_rmanager();
-
-    m.register_plugin(alloc(datalog::bitvector_table_plugin, m));
-
-    datalog::table_base* tbl = mk_bv_table(m, sig);
-    datalog::table_base& table = *tbl;
-
-    datalog::table_fact row, row1, row2, row3;
-    row.push_back(1);
-    row.push_back(2);
-    row.push_back(5);
-
-    // Group (1,2,*)
-    row1 = row;
-    row[2] = 6;
-    row2 = row;
-    row[2] = 5;
-    row3 = row;
-
-    table.add_fact(row1);
-    table.add_fact(row2);
-    table.add_fact(row3);
-
-    // Group (1,3,*)
-    row[1] = 3;
-    row1 = row;
-    row[2] = 7;
-    row2 = row;
-    row[2] = 4;
-    row3 = row;
-
-    table.add_fact(row1);
-    table.add_fact(row2);
-    table.add_fact(row3);
-
-    table.display(std::cout);
-
-    unsigned_vector group_by(2);
-    group_by[0] = 0;
-    group_by[1] = 1;
-
-    datalog::table_min_fn * min_fn = m.mk_min_fn(table, group_by, 2);
-    datalog::table_base * min_tbl = (*min_fn)(table);
-
-    min_tbl->display(std::cout);
-
-    row[1] = 2;
-    row[2] = 5;
-    SASSERT(min_tbl->contains_fact(row));
-
-    row[1] = 3;
-    row[2] = 4;
-    SASSERT(min_tbl->contains_fact(row));
-
-    dealloc(min_fn);
-    min_tbl->deallocate();
-    tbl->deallocate();
-}
-
 void tst_dl_table() {
     test_dl_bitvector_table();
-    test_table_min();
 }
 #else
 void tst_dl_table() {