From 760b12c4cbb6b921d983970b5517143b0cb167b4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 25 Oct 2012 14:46:17 -0700
Subject: [PATCH] auto generate install_tactics procedure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
scripts/mk_make.py | 5 ++
scripts/mk_util.py | 73 ++++++++++++++++++-
src/api/api_context.cpp | 4 +-
src/cmd_context/tactic_cmds.cpp | 6 +-
.../portfolio => dead}/install_tactics.cpp | 0
.../portfolio => dead}/install_tactics.h | 0
src/tactic/nlsat/nlsat_tactic.h | 4 +
src/tactic/sat/sat_tactic.h | 5 ++
8 files changed, 93 insertions(+), 4 deletions(-)
rename src/{tactic/portfolio => dead}/install_tactics.cpp (100%)
rename src/{tactic/portfolio => dead}/install_tactics.h (100%)
diff --git a/scripts/mk_make.py b/scripts/mk_make.py
index 931ebb06d..a2c640661 100644
--- a/scripts/mk_make.py
+++ b/scripts/mk_make.py
@@ -66,7 +66,12 @@ add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', dll_name='z3')
add_dot_net_dll('dotnet', ['api_dll'], 'bindings/dotnet/Microsoft.Z3', dll_name='Microsoft.Z3', assembly_info_dir='Properties')
add_dot_net_dll('dotnetV3', ['api_dll'], 'bindings/dotnet/Microsoft.Z3V3', dll_name='Microsoft.Z3V3')
+
mk_auto_src()
update_version(4, 2, 0, 0)
+mk_all_install_tactic_cpps()
+
+#
mk_makefile()
+
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index d4593166f..93d4504c9 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -234,6 +234,10 @@ class Component:
def has_assembly_info(self):
return False
+ # Return true if the component needs builder to generate an install_tactics.cpp file
+ def require_install_tactics(self):
+ return False
+
class LibComponent(Component):
def __init__(self, name, path, deps):
Component.__init__(self, name, path, deps)
@@ -305,6 +309,9 @@ class ExeComponent(Component):
out.write(' $(LINK_EXTRA_FLAGS)\n')
out.write('%s: %s\n\n' % (self.name, exefile))
+ def require_install_tactics(self):
+ return ('tactic' in self.deps) and ('cmd_context' in self.deps)
+
# All executables are included in the all: rule
def main_component(self):
return True
@@ -354,6 +361,9 @@ class DLLComponent(Component):
def main_component(self):
return True
+ def require_install_tactics(self):
+ return ('tactic' in self.deps) and ('cmd_context' in self.deps)
+
class DotNetDLLComponent(Component):
def __init__(self, name, dll_name, path, deps, assembly_info_dir):
Component.__init__(self, name, path, deps)
@@ -367,6 +377,7 @@ class DotNetDLLComponent(Component):
def mk_makefile(self, out):
if IS_WINDOW:
# TODO
+ out.write('%s: \n\n' % self.name)
return
def main_component(self):
@@ -531,11 +542,69 @@ def update_assembly_info_version(assemblyinfo, major, minor, build, revision, is
num_updates = num_updates + 1
else:
fout.write(line)
- if VERBOSE:
- print "%s version numbers updated at '%s'" % (num_updates, assemblyinfo)
+ # if VERBOSE:
+ # print "%s version numbers updated at '%s'" % (num_updates, assemblyinfo)
assert num_updates == 2, "unexpected number of version number updates"
fin.close()
fout.close()
shutil.move(tmp, assemblyinfo)
if VERBOSE:
print "Updated %s" % assemblyinfo
+
+ADD_TACTIC_DATA=[]
+
+def ADD_TACTIC(name, descr, cmd):
+ global ADD_TACTIC_DATA
+ ADD_TACTIC_DATA.append((name, descr, cmd))
+
+# Generate an install_tactics.cpp at path.
+# This file implements the procedure
+# void install_tactics(tactic_manager & ctx)
+# It installs all tactics in the given component (name) list cnames
+# The procedure looks for ADD_TACTIC commands in the .h files of these components.
+def mk_install_tactic_cpp(cnames, path):
+ global ADD_TACTIC_DATA
+ ADD_TACTIC_DATA = []
+ fullname = '%s/install_tactic.cpp' % path
+ fout = open(fullname, 'w')
+ fout.write('// Automatically generated file.\n')
+ fout.write('#include"tactic.h"\n')
+ fout.write('#include"tactic_cmds.h"\n')
+ fout.write('#include"cmd_context.h"\n')
+ pat = re.compile('[ \t]*ADD_TACTIC(.*)')
+ for cname in cnames:
+ c = _Name2Component[cname]
+ h_files = filter(lambda f: f.endswith('.h'), os.listdir(c.src_dir))
+ for h_file in h_files:
+ fin = open("%s/%s" % (c.src_dir, h_file), 'r')
+ for line in fin:
+ if pat.match(line):
+ fout.write('#include"%s"\n' % h_file)
+ exec line.strip('\n ') in globals()
+ # First pass will just generate the tactic factories
+ idx = 0
+ for data in ADD_TACTIC_DATA:
+ fout.write('MK_SIMPLE_TACTIC_FACTORY(__Z3_local_factory_%s, %s);\n' % (idx, data[2]))
+ idx = idx + 1
+ fout.write('#define ADD_TACTIC_CMD(NAME, DESCR, FACTORY) ctx.insert(alloc(tactic_cmd, symbol(NAME), DESCR, alloc(FACTORY)))\n')
+ fout.write('#define ADD_PROBE(NAME, DESCR, PROBE) ctx.insert(alloc(probe_info, symbol(NAME), DESCR, PROBE))\n')
+ fout.write('void install_tactics(tactic_manager & ctx) {\n')
+ idx = 0
+ for data in ADD_TACTIC_DATA:
+ fout.write(' ADD_TACTIC_CMD("%s", "%s", __Z3_local_factory_%s);\n' % (data[0], data[1], idx))
+ idx = idx + 1
+ fout.write('}\n')
+ if VERBOSE:
+ print "Generated '%s'" % fullname
+
+def mk_all_install_tactic_cpps():
+ if not ONLY_MAKEFILES:
+ for c in _Components:
+ if c.require_install_tactics():
+ cnames = []
+ cnames.extend(c.deps)
+ cnames.append(c.name)
+ mk_install_tactic_cpp(cnames, c.src_dir)
+
+def get_component(name):
+ return _Name2Component[name]
diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index a6046a83e..0da0186a0 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -25,9 +25,11 @@ Revision History:
#include"ast_ll_pp.h"
#include"api_log_macros.h"
#include"api_util.h"
-#include"install_tactics.h"
#include"reg_decl_plugins.h"
+// The install_tactics procedure is automatically generated
+void install_tactics(tactic_manager & ctx);
+
namespace api {
static void default_error_handler(Z3_context, Z3_error_code c) {
diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp
index f6d9a5e5f..32adb5f47 100644
--- a/src/cmd_context/tactic_cmds.cpp
+++ b/src/cmd_context/tactic_cmds.cpp
@@ -390,13 +390,17 @@ public:
}
};
-
+// The install_tactics procedure is automatically generated for every
+// component that includes the cmd_context & tactic modules.
+void install_tactics(tactic_manager & ctx);
+
void install_core_tactic_cmds(cmd_context & ctx) {
ctx.insert(alloc(declare_tactic_cmd));
ctx.insert(alloc(get_user_tactics_cmd));
ctx.insert(alloc(help_tactic_cmd));
ctx.insert(alloc(check_sat_using_tactict_cmd));
ctx.insert(alloc(apply_tactic_cmd));
+ install_tactics(ctx);
}
static tactic * mk_and_then(cmd_context & ctx, sexpr * n) {
diff --git a/src/tactic/portfolio/install_tactics.cpp b/src/dead/install_tactics.cpp
similarity index 100%
rename from src/tactic/portfolio/install_tactics.cpp
rename to src/dead/install_tactics.cpp
diff --git a/src/tactic/portfolio/install_tactics.h b/src/dead/install_tactics.h
similarity index 100%
rename from src/tactic/portfolio/install_tactics.h
rename to src/dead/install_tactics.h
diff --git a/src/tactic/nlsat/nlsat_tactic.h b/src/tactic/nlsat/nlsat_tactic.h
index 93dfe74db..afd63e01a 100644
--- a/src/tactic/nlsat/nlsat_tactic.h
+++ b/src/tactic/nlsat/nlsat_tactic.h
@@ -25,4 +25,8 @@ class tactic;
tactic * mk_nlsat_tactic(ast_manager & m, params_ref const & p = params_ref());
+/*
+ ADD_TACTIC('nlsat', '(try to) solve goal using a nonlinear arithmetic solver.', 'mk_nlsat_tactic(m, p)')
+*/
+
#endif
diff --git a/src/tactic/sat/sat_tactic.h b/src/tactic/sat/sat_tactic.h
index 405afaccd..fcffaa494 100644
--- a/src/tactic/sat/sat_tactic.h
+++ b/src/tactic/sat/sat_tactic.h
@@ -27,4 +27,9 @@ tactic * mk_sat_tactic(ast_manager & m, params_ref const & p = params_ref());
tactic * mk_sat_preprocessor_tactic(ast_manager & m, params_ref const & p = params_ref());
+/*
+ ADD_TACTIC('sat', '(try to) solve goal using a SAT solver.', 'mk_sat_tactic(m, p)')
+ ADD_TACTIC('sat-preprocess', 'Apply SAT solver preprocessing procedures (bounded resolution, Boolean constant propagation, 2-SAT, subsumption, subsumption resolution).', 'mk_sat_preprocessor_tactic(m, p)')
+*/
+
#endif