From 683687b153f88a07fed8fa0f66c4c93ec67a18b0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 31 Oct 2012 10:54:59 -0700
Subject: [PATCH 1/5] more cleanup
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
scripts/mk_project.py | 3 +-
src/ast/ast_dag_pp.cpp | 353 ---------------------
src/ast/ast_dag_pp.h | 31 --
src/ast/expr2dot.cpp | 84 -----
src/ast/expr2dot.h | 27 --
src/{util => math/interval}/interval.h | 0
src/{util => math/interval}/interval_def.h | 0
src/{util => muz_qe}/imdd.cpp | 0
src/{util => muz_qe}/imdd.h | 0
src/{util => muz_qe}/interval_skip_list.h | 0
src/{util => muz_qe}/skip_list_base.h | 0
src/{util => smt}/diff_logic.h | 0
src/{util => smt}/old_interval.cpp | 0
src/{util => smt}/old_interval.h | 0
src/tactic/sls/sls_tactic.cpp | 12 -
15 files changed, 2 insertions(+), 508 deletions(-)
delete mode 100644 src/ast/ast_dag_pp.cpp
delete mode 100644 src/ast/ast_dag_pp.h
delete mode 100644 src/ast/expr2dot.cpp
delete mode 100644 src/ast/expr2dot.h
rename src/{util => math/interval}/interval.h (100%)
rename src/{util => math/interval}/interval_def.h (100%)
rename src/{util => muz_qe}/imdd.cpp (100%)
rename src/{util => muz_qe}/imdd.h (100%)
rename src/{util => muz_qe}/interval_skip_list.h (100%)
rename src/{util => muz_qe}/skip_list_base.h (100%)
rename src/{util => smt}/diff_logic.h (100%)
rename src/{util => smt}/old_interval.cpp (100%)
rename src/{util => smt}/old_interval.h (100%)
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 3c7d6e70a..d6c97c8ac 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -14,7 +14,8 @@ def init_project_def():
add_lib('polynomial', ['util'], 'math/polynomial')
add_lib('sat', ['util'])
add_lib('nlsat', ['polynomial', 'sat'])
- add_lib('subpaving', ['util'], 'math/subpaving')
+ add_lib('interval', ['util'], 'math/interval')
+ add_lib('subpaving', ['interval'], 'math/subpaving')
add_lib('ast', ['util', 'polynomial'])
add_lib('rewriter', ['ast', 'polynomial'], 'ast/rewriter')
add_lib('model', ['rewriter'])
diff --git a/src/ast/ast_dag_pp.cpp b/src/ast/ast_dag_pp.cpp
deleted file mode 100644
index 893ef09b6..000000000
--- a/src/ast/ast_dag_pp.cpp
+++ /dev/null
@@ -1,353 +0,0 @@
-/*++
-Copyright (c) 2007 Microsoft Corporation
-
-Module Name:
-
- ast_dag_pp.cpp
-
-Abstract:
-
- AST low level pretty printer.
-
-Author:
-
- Leonardo de Moura (leonardo) 2006-10-19.
- Nikolaj Bjorner (nbjorner) 2007-07-17
-
-Revision History:
-
---*/
-
-#include<iostream>
-#include"for_each_ast.h"
-#include"arith_decl_plugin.h"
-#include"bv_decl_plugin.h"
-#include"ast_pp.h"
-
-class dag_printer {
- ast_manager& m_manager;
- std::ostream & m_out;
- ast_mark& m_mark;
- bool m_initialized;
- svector<symbol> m_names;
- family_id m_basic_fid;
- family_id m_bv_fid;
- family_id m_arith_fid;
- family_id m_array_fid;
- arith_util m_arith;
- bv_util m_bv;
- bool m_enable_shortcut;
-
- void process_ast(ast* a) {
- for_each_ast(*this, m_mark, a);
- }
-
- void process_info(decl_info* info) {
- if (!info) {
- return;
- }
- unsigned num_params = info->get_num_parameters();
- for (unsigned i = 0; i < num_params; ++i) {
- parameter const& p = info->get_parameter(i);
-
- if (p.is_ast() && !m_mark.is_marked(p.get_ast())) {
- process_ast(p.get_ast());
- }
- }
- }
-
- template<typename T>
- void display_children(unsigned num_children, T * const * children) {
- for (unsigned i = 0; i < num_children; i++) {
- display_node_id(children[i]);
- }
- }
-
- void display_node_id(ast* n) {
- unsigned id = n->get_id();
- switch(n->get_kind()) {
- case AST_FUNC_DECL:
- case AST_SORT:
- m_out << "$d" << (id - (1 << 31)) << " ";
- break;
- default:
- m_out << "$" << id << " ";
- break;
- }
- }
-
- void display_parameter(parameter const& p)
- {
- if (p.is_int()) {
- m_out << p.get_int() << " ";
- }
- else if (p.is_ast()) {
- SASSERT(p.is_ast());
- display_node_id(p.get_ast());
- }
- else if (p.is_rational()) {
- m_out << p.get_rational() << " ";
- }
- else if (p.is_symbol()) {
- display_symbol(p.get_symbol());
- }
- else {
- UNREACHABLE();
- }
- }
-
- // Display:
- // App name [ parameters] arguments
- //
- void display_builtin(app* n) {
- func_decl* d = n->get_decl();
- unsigned num_params = d->get_num_parameters();
-
- m_out << "App ";
- display_node_id(n);
- display_symbol(d->get_name());
- if (num_params > 0) {
- m_out << "[ ";
- for (unsigned i = 0; i < num_params; ++i) {
- display_parameter(d->get_parameter(i));
- }
- m_out << "] ";
- }
- display_children(n->get_num_args(), n->get_args());
- m_out << "\n";
- }
-
- void display_info(func_decl_info* info) {
- if (!info) {
- return;
- }
- m_out << "BUILTIN " << get_family_name(info->get_family_id()) << " " << info->get_decl_kind() << " ";
-
- if (info->is_associative()) {
- m_out << ":assoc ";
- }
- if (info->is_commutative()) {
- m_out << ":comm ";
- }
- if (info->is_injective()) {
- m_out << ":inj ";
- }
- for (unsigned i = 0; i < info->get_num_parameters(); ++i) {
- display_parameter(info->get_parameter(i));
- }
- }
-
- void display_info(sort_info* info) {
- if (!info) {
- return;
- }
- m_out << "BUILTIN " << get_family_name(info->get_family_id()) << " " << info->get_decl_kind() << " ";
- // TODO: remove this if... it doesn't make sense...
- if (!info->is_infinite() && !info->is_very_big()) {
- m_out << "Size " << info->get_num_elements().size() << " ";
- }
- for (unsigned i = 0; i < info->get_num_parameters(); ++i) {
- display_parameter(info->get_parameter(i));
- }
- }
-
- symbol get_family_name(family_id id) {
- if (id == null_family_id) {
- return symbol("null");
- }
- if (!m_initialized) {
- svector<symbol> names;
- svector<family_id> range;
- m_manager.get_dom(names);
- m_manager.get_range(range);
- m_names.resize(range.size());
- for (unsigned i = 0; i < range.size(); ++i) {
- SASSERT(range[i] < static_cast<family_id>(range.size()));
- m_names[range[i]] = names[i];
- }
- m_initialized = true;
- }
- SASSERT(id < static_cast<family_id>(m_names.size()));
- return m_names[id];
- }
-
- bool has_special_char(char const* s) {
- while (s && *s) {
- if (*s == ' ') {
- return true;
- }
- ++s;
- }
- return false;
- }
-
- void display_symbol(symbol const& s) {
- if (s.is_numerical()) {
- m_out << s << " ";
- }
- else if (!(s.bare_str()[0])) {
- m_out << "\"null\" ";
- }
- else if (!has_special_char(s.bare_str())) {
- m_out << s << " ";
- }
- else {
- char const* r = s.bare_str();
- m_out << "\"";
- while (*r) {
- if (*r == ' ' || *r == '\n' ||
- *r == '\t' || *r == '\r') {
- m_out << "\\" << ((unsigned)(*r));
- }
- else {
- m_out << *r;
- }
- ++r;
- }
- m_out << "\" ";
- }
- }
-
-public:
-
- dag_printer(ast_manager& mgr, std::ostream & out, ast_mark& mark):
- m_manager(mgr),
- m_out(out),
- m_mark(mark),
- m_initialized(false),
- m_basic_fid(mgr.get_basic_family_id()),
- m_bv_fid(mgr.get_family_id("bv")),
- m_arith_fid(mgr.get_family_id("arith")),
- m_array_fid(mgr.get_family_id("array")),
- m_arith(mgr),
- m_bv(mgr),
- m_enable_shortcut(true)
- {
- }
-
- void operator()(sort * n) {
- process_info(n->get_info());
- m_out << "Ty ";
- display_node_id(n);
- display_symbol(n->get_name());
- display_info(n->get_info());
- m_out << "\n";
- }
-
- void pp_num(app* n, rational const& r) {
- m_out << "Num ";
- display_node_id(n);
- m_out << r << " ";
- display_node_id(m_manager.get_sort(n));
- m_out << "\n";
- }
-
- void operator()(var * n) {
- process_ast(n->get_sort());
- m_out << "Var ";
- display_node_id(n);
- m_out << n->get_idx() << " ";
- display_node_id(n->get_sort());
- m_out << "\n";
- }
-
- void operator()(func_decl * n) {
-
- process_info(n->get_info());
-
- family_id fid = n->get_family_id();
- if (m_arith_fid == fid &&
- n->get_info()->get_decl_kind() == OP_NUM) {
- return;
- }
-
- if (m_bv_fid == fid &&
- n->get_info()->get_decl_kind() == OP_BV_NUM) {
- return;
- }
-
- m_out << "Dec ";
- display_node_id(n);
- display_symbol(n->get_name());
- unsigned dom_size = n->get_arity();
- for (unsigned i = 0; i < dom_size; ++i) {
- display_node_id(n->get_domain(i));
- }
- display_node_id(n->get_range());
- display_info(n->get_info());
- m_out << "\n";
- }
-
- void operator()(app * n) {
- process_ast(n->get_decl());
- family_id fid = n->get_family_id();
- unsigned bv_size;
- rational val;
- if (m_arith.is_numeral(n, val)) {
- pp_num(n, val);
- }
- else if (m_bv.is_numeral(n, val, bv_size)) {
- pp_num(n, val);
- }
- else if (m_enable_shortcut &&
- fid != null_family_id &&
- (fid == m_basic_fid || fid == m_bv_fid || fid == m_array_fid || fid == m_arith_fid)) {
- display_builtin(n);
- }
- else if (n->get_num_args() == 0 && fid == null_family_id) {
- func_decl* d = n->get_decl();
- m_out << "Const ";
- display_node_id(n);
- display_symbol(d->get_name());
- display_node_id(d->get_range());
- m_out << "\n";
- }
- else {
- m_out << "Fun ";
- display_node_id(n);
- display_node_id(n->get_decl());
- display_children(n->get_num_args(), n->get_args());
- m_out << "\n";
- }
- }
-
- void operator()(quantifier * n) {
- m_out << "Qua ";
- display_node_id(n);
- m_out << (n->is_forall() ? "FORALL" : "EXISTS") << " ";
- m_out << n->get_weight() << " ";
- if (symbol::null != n->get_skid()) {
- m_out << "\"" << n->get_skid() << "\" ";
- }
- else {
- m_out << "\"null\" ";
- }
- if (symbol::null != n->get_qid()) {
- m_out << "\"" << n->get_qid() << "\" ";
- }
- else {
- m_out << "\"null\" ";
- }
- unsigned num_decls = n->get_num_decls();
- m_out << num_decls << " ";
- for (unsigned i = 0; i < num_decls; i++) {
- m_out << n->get_decl_name(i) << " ";
- display_node_id(n->get_decl_sort(i));
- }
- m_out << n->get_num_patterns() << " ";
- display_children(n->get_num_patterns(), n->get_patterns());
- display_node_id(n->get_expr());
- m_out << "\n";
- }
-};
-
-void ast_dag_pp(std::ostream & out, ast_manager& mgr, ast_mark& mark, ast * n) {
- dag_printer p(mgr, out, mark);
- for_each_ast(p, mark, n, true);
-}
-
-void ast_dag_pp(std::ostream & out, ast_manager& mgr, ast * n) {
- ast_mark mark;
- ast_dag_pp(out, mgr, mark, n);
-}
-
diff --git a/src/ast/ast_dag_pp.h b/src/ast/ast_dag_pp.h
deleted file mode 100644
index fa933e22f..000000000
--- a/src/ast/ast_dag_pp.h
+++ /dev/null
@@ -1,31 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
- ast_dag_pp.h
-
-Abstract:
-
- AST low level pretty printer.
-
-Author:
-
- Leonardo de Moura (leonardo) 2006-10-19.
-
-Revision History:
-
---*/
-#ifndef _AST_DAG_PP_H_
-#define _AST_DAG_PP_H_
-
-#include<iostream>
-
-class ast;
-
-void ast_dag_pp(std::ostream & out, ast_manager& mgr, ast * n);
-
-void ast_dag_pp(std::ostream & out, ast_manager& mgr, ast_mark& mark, ast * n);
-
-#endif /* _AST_DAG_PP_H_ */
-
diff --git a/src/ast/expr2dot.cpp b/src/ast/expr2dot.cpp
deleted file mode 100644
index b0fef27d0..000000000
--- a/src/ast/expr2dot.cpp
+++ /dev/null
@@ -1,84 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
- expr2dot.cpp
-
-Abstract:
-
- <abstract>
-
-Author:
-
- Leonardo de Moura (leonardo) 2008-03-07.
-
-Revision History:
-
---*/
-#include"expr2dot.h"
-#include"for_each_expr.h"
-
-class dot_printer {
- std::ostream & m_out;
- ast_manager & m_manager;
- bool m_proofs_only;
-public:
- dot_printer(std::ostream & out, ast_manager & m, bool proofs):
- m_out(out),
- m_manager(m),
- m_proofs_only(proofs) {
- }
-
- char const * get_color(app * n) {
- if (m_manager.is_unit_resolution(n))
- return "blue";
- else if (m_manager.is_lemma(n))
- return "gold";
- else if (m_manager.is_transitivity(n))
- return "red";
- else if (m_manager.is_monotonicity(n))
- return "green";
- else
- return "black";
- }
-
- void operator()(var * n) {
- if (!m_proofs_only) {
- m_out << n->get_id() << "[label=\"\",shape=circle];\n";
- }
- }
-
- void operator()(quantifier * n) {
- if (!m_proofs_only) {
- m_out << n->get_id() << "[label=\"\",shape=circle,color=gray];\n";
- m_out << n->get_expr()->get_id() << " -> " << n->get_id() << ";\n";
- }
- }
-
- void operator()(app * n) {
- if (!m_proofs_only || m_manager.is_proof(n)) {
- char const * c = get_color(n);
- m_out << n->get_id() << "[label=\"\",shape=circle,color=" << c << "];\n";
- if (m_proofs_only) {
- unsigned num = m_manager.get_num_parents(n);
- for (unsigned i = 0; i < num; i++)
- m_out << m_manager.get_parent(n, i)->get_id() << " -> " << n->get_id() << " [color=" << c << "];\n";
- }
- else {
- unsigned num = n->get_num_args();
- for (unsigned i = 0; i < num; i++)
- m_out << n->get_arg(i)->get_id() << " -> " << n->get_id() << " [color=" << c << "];\n";
- }
- }
- }
-};
-
-void expr2dot(std::ostream & out, expr * n, ast_manager & m, bool proofs) {
- out << "digraph \"ast\" {\n";
- dot_printer p(out, m, proofs);
- for_each_expr(p, n);
- out << "}\n";
-}
-
-
diff --git a/src/ast/expr2dot.h b/src/ast/expr2dot.h
deleted file mode 100644
index 54c65b034..000000000
--- a/src/ast/expr2dot.h
+++ /dev/null
@@ -1,27 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
- expr2dot.h
-
-Abstract:
-
- Convert expressions into a .DOT file
-
-Author:
-
- Leonardo de Moura (leonardo) 2008-03-07.
-
-Revision History:
-
---*/
-#ifndef _EXPR2DOT_H_
-#define _EXPR2DOT_H_
-
-#include"ast.h"
-
-void expr2dot(std::ostream & out, expr * a, ast_manager & m, bool proofs = false);
-
-#endif /* _AST2DOT_H_ */
-
diff --git a/src/util/interval.h b/src/math/interval/interval.h
similarity index 100%
rename from src/util/interval.h
rename to src/math/interval/interval.h
diff --git a/src/util/interval_def.h b/src/math/interval/interval_def.h
similarity index 100%
rename from src/util/interval_def.h
rename to src/math/interval/interval_def.h
diff --git a/src/util/imdd.cpp b/src/muz_qe/imdd.cpp
similarity index 100%
rename from src/util/imdd.cpp
rename to src/muz_qe/imdd.cpp
diff --git a/src/util/imdd.h b/src/muz_qe/imdd.h
similarity index 100%
rename from src/util/imdd.h
rename to src/muz_qe/imdd.h
diff --git a/src/util/interval_skip_list.h b/src/muz_qe/interval_skip_list.h
similarity index 100%
rename from src/util/interval_skip_list.h
rename to src/muz_qe/interval_skip_list.h
diff --git a/src/util/skip_list_base.h b/src/muz_qe/skip_list_base.h
similarity index 100%
rename from src/util/skip_list_base.h
rename to src/muz_qe/skip_list_base.h
diff --git a/src/util/diff_logic.h b/src/smt/diff_logic.h
similarity index 100%
rename from src/util/diff_logic.h
rename to src/smt/diff_logic.h
diff --git a/src/util/old_interval.cpp b/src/smt/old_interval.cpp
similarity index 100%
rename from src/util/old_interval.cpp
rename to src/smt/old_interval.cpp
diff --git a/src/util/old_interval.h b/src/smt/old_interval.h
similarity index 100%
rename from src/util/old_interval.h
rename to src/smt/old_interval.h
diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp
index 1b95cb1ed..0ad845095 100644
--- a/src/tactic/sls/sls_tactic.cpp
+++ b/src/tactic/sls/sls_tactic.cpp
@@ -31,7 +31,6 @@ Notes:
#include"max_bv_sharing_tactic.h"
#include"simplify_tactic.h"
#include"stopwatch.h"
-#include"expr2dot.h"
#include"propagate_values_tactic.h"
#include"sls_tactic.h"
#include"nnf_tactic.h"
@@ -1727,17 +1726,6 @@ class sls_tactic : public tactic {
}
void operator()(goal_ref const & g, model_converter_ref & mc) {
- //#ifdef _DEBUG
- //ptr_vector<expr> es;
- //for (unsigned i = 0; i < g->size(); i++)
- // es.push_back(g->form(i));
- //expr_ref a(m_manager);
- //a = m_manager.mk_and(g->size(), es.c_ptr());
- //std::ofstream dot_out("top.dot", std::ios::out);
- //expr2dot(dot_out, a, m_manager);
- //dot_out.close();
- //#endif
-
if (g->inconsistent()) {
mc = 0;
return;
From 92eb2ec8026833afe2c7e38e2ddc43b47c9d6a13 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 31 Oct 2012 11:02:14 -0700
Subject: [PATCH 2/5] missing update
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
src/muz_qe/pdr_interpolant_provider.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/muz_qe/pdr_interpolant_provider.cpp b/src/muz_qe/pdr_interpolant_provider.cpp
index a243ed899..85655c737 100644
--- a/src/muz_qe/pdr_interpolant_provider.cpp
+++ b/src/muz_qe/pdr_interpolant_provider.cpp
@@ -307,7 +307,7 @@ lbool interpolant_provider_impl::get_interpolant(expr * f1, expr * f2, expr_ref&
}
front_end_params dummy_params;
- cmd_context cctx(dummy_params, false, &m);
+ cmd_context cctx(&dummy_params, false, &m);
for_each_expr(used_symbol_inserter(cctx), f1);
parse_smt2_commands(cctx, std::istringstream(res_text), false);
From 81193fd550b419ce517776cc3dd6865efa119fb9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 31 Oct 2012 11:16:43 -0700
Subject: [PATCH 3/5] add default template instance
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
src/math/interval/interval_mpq.cpp | 21 +++++++++++++++++++++
1 file changed, 21 insertions(+)
create mode 100644 src/math/interval/interval_mpq.cpp
diff --git a/src/math/interval/interval_mpq.cpp b/src/math/interval/interval_mpq.cpp
new file mode 100644
index 000000000..fa7cec853
--- /dev/null
+++ b/src/math/interval/interval_mpq.cpp
@@ -0,0 +1,21 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+ interval_mpq.cpp
+
+Abstract:
+
+ Instantiate template using defaults.
+
+Author:
+
+ Leonardo de Moura (leonardo) 2012-10-31.
+
+Revision History:
+
+--*/
+#include"interval_def.h"
+
+template class interval_manager<im_default_config>;
From 7cea9cdefef12fa36b3029f47743aab0fc2fed10 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 31 Oct 2012 13:09:05 -0700
Subject: [PATCH 4/5] enable pdb for release mode 32bit
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
scripts/config-vs-release.mk | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/scripts/config-vs-release.mk b/scripts/config-vs-release.mk
index 16c9b0d37..d2c44f704 100644
--- a/scripts/config-vs-release.mk
+++ b/scripts/config-vs-release.mk
@@ -1,6 +1,6 @@
CC=cl
CXX=cl
-CXXFLAGS=/nologo /c /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /openmp /Gd /analyze- /arch:SSE2
+CXXFLAGS=/nologo /c /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /openmp /Gd /analyze- /arch:SSE2
CXX_OUT_FLAG=/Fo
OBJ_EXT=.obj
LIB_EXT=.lib
@@ -10,13 +10,13 @@ AR_OUTFLAG=/OUT:
EXE_EXT=.exe
LINK=cl
LINK_FLAGS=/nologo /MD
-LINK_EXTRA_FLAGS=/link /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT
+LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT
LINK_OUT_FLAG=/Fe
SO_EXT=.dll
SLINK=cl
SLINK_FLAGS=/nologo /LD
-SLINK_EXTRA_FLAGS=/link /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO
+SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO
SLINK_OUT_FLAG=/Fe
From ccdb253b4799371a6821a13d35095d8b97ede44b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 31 Oct 2012 13:14:37 -0700
Subject: [PATCH 5/5] added add_extra_exe command to build framework
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
scripts/mk_util.py | 11 +++++++++++
1 file changed, 11 insertions(+)
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 7db1b5f21..82865a4ac 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -503,6 +503,13 @@ class ExeComponent(Component):
'%s/bin/%s.exe' % (dist_path, self.exe_name))
+class ExtraExeComponent(ExeComponent):
+ def __init__(self, name, exe_name, path, deps, install):
+ ExeComponent.__init__(self, name, exe_name, path, deps, install)
+
+ def main_component(self):
+ return False
+
class DLLComponent(Component):
def __init__(self, name, dll_name, path, deps, export_files, reexports, install):
Component.__init__(self, name, path, deps)
@@ -752,6 +759,10 @@ def add_exe(name, deps=[], path=None, exe_name=None, install=True):
c = ExeComponent(name, exe_name, path, deps, install)
reg_component(name, c)
+def add_extra_exe(name, deps=[], path=None, exe_name=None, install=True):
+ c = ExtraExeComponent(name, exe_name, path, deps, install)
+ reg_component(name, c)
+
def add_dll(name, deps=[], path=None, dll_name=None, export_files=[], reexports=[], install=True):
c = DLLComponent(name, dll_name, path, deps, export_files, reexports, install)
reg_component(name, c)