diff --git a/mk_make.py b/mk_make.py
index 7b75f7d98..1ae145066 100644
--- a/mk_make.py
+++ b/mk_make.py
@@ -1,5 +1,12 @@
-import os
-import glob
+############################################
+# Copyright (c) 2012 Microsoft Corporation
+#
+# Scripts for generate Makefiles and Visual
+# Studio project files.
+#
+# Author: Leonardo de Moura (leonardo)
+############################################
+from mk_util import *
BUILD_DIR='build-test'
SRC_DIR='src'
@@ -9,153 +16,9 @@ VS_COMMON_OPTIONS='WIN32;_WINDOWS;ASYNC_COMMANDS'
VS_DBG_OPTIONS='Z3DEBUG;_TRACE;_DEBUG'
VS_RELEASE_OPTIONS='NDEBUG;_EXTERNAL_RELEASE'
-def is_debug(mode):
- return mode == 'Debug'
-
-def is_x64(platform):
- return platform == 'x64'
-
-def mk_dir(d):
- if not os.path.exists(d):
- os.makedirs(d)
-
# Initialization
mk_dir(BUILD_DIR)
-def module_src_dir(name):
- return '%s%s%s' % (SRC_DIR, os.sep, name)
-
-def module_build_dir(name):
- return '%s%s%s' % (BUILD_DIR, os.sep, name)
-
-def vs_header(f):
- f.write(
-'\n'
-'\n')
-
-GUI = 0
-Name2GUI = {}
-
-def vs_project_configurations(f, name):
- global GUI, Name2GUI
- f.write(' \n')
- for mode in MODES:
- for platform in PLATFORMS:
- f.write(' \n' % (mode, platform))
- f.write(' %s\n' % mode)
- f.write(' %s\n' % platform)
- f.write(' \n')
- f.write(' \n')
-
- f.write(' \n')
- f.write(' {00000000-0000-0000-000--%s}\n' % GUI)
- f.write(' %s\n' % name)
- f.write(' Win32Proj\n')
- f.write(' \n')
- f.write(' \n')
- Name2GUI[name] = GUI
- GUI = GUI + 1
-
-def vs_lib_configurations(f, name):
- for mode in MODES:
- for platform in PLATFORMS:
- f.write(' \n' % (mode, platform))
- f.write(' StaticLibrary\n')
- f.write(' Unicode\n')
- f.write(' false\n')
- f.write(' \n')
-
- f.write(' \n')
- f.write(' \n')
- f.write(' \n')
- f.write(' \n')
- f.write(' \n')
- f.write(' \n')
-
- f.write(' \n')
- for mode in MODES:
- for platform in PLATFORMS:
- if is_x64(platform):
- f.write(' $(SolutionDir)$(Platform)\$(Configuration)\\n' %
- (mode, platform))
- else:
- f.write(' $(SolutionDir)$(Configuration)\\n' % (mode, platform))
- for mode in MODES:
- for platform in PLATFORMS:
- f.write(' %s\n' % (mode, platform, name))
- f.write(' .lib\n' % (mode, platform))
- f.write(' \n')
-
-def vs_compilation_options(f, name, deps):
- for mode in MODES:
- for platform in PLATFORMS:
- f.write(' \n' % (mode, platform))
- if is_x64(platform):
- f.write(' \n')
- f.write(' X64\n')
- f.write(' \n')
- f.write(' \n')
- if is_debug(mode):
- f.write(' Disabled\n')
- else:
- f.write(' Full\n')
- options = VS_COMMON_OPTIONS
- if is_debug(mode):
- options = "%s;%s" % (options, VS_DBG_OPTIONS)
- else:
- options = "%s;%s" % (options, VS_RELEASE_OPTIONS)
- if is_x64(platform):
- options = "%s;_AMD64_" % options
- f.write(' %s;%%(PreprocessorDefinitions)\n' % options)
- if is_debug(mode):
- f.write(' true\n')
- f.write(' EnableFastChecks\n')
- f.write(' Level3\n')
- f.write(' MultiThreadedDebugDLL\n')
- f.write(' true\n')
- f.write(' ProgramDatabase\n')
- f.write(' ')
- f.write('..\..\src\%s' % name)
- for dep in deps:
- f.write(';..\..\src\%s' % dep)
- f.write('\n')
- f.write(' \n')
- f.write(' \n')
- f.write(' $(OutDir)%s.lib\n' % name)
- f.write(' %(AdditionalLibraryDirectories)\n')
- if is_x64(platform):
- f.write(' MachineX64\n')
- else:
- f.write(' MachineX86\n')
- f.write(' \n')
- f.write(' \n')
-
-def add_vs_cpps(f, name):
- f.write(' \n')
- srcs = module_src_dir(name)
- for cppfile in glob.glob(os.path.join(srcs, '*.cpp')):
- f.write(' \n' % (os.sep, os.sep, cppfile))
- f.write(' \n')
-
-def vs_footer(f):
- f.write(
-' \n'
-' \n'
-' \n'
-'\n')
-
-def add_lib(name, deps):
- module_dir = module_build_dir(name)
- mk_dir(module_dir)
-
- vs_proj = open('%s%s%s.vcxproj' % (module_dir, os.sep, name), 'w')
- vs_header(vs_proj)
- vs_project_configurations(vs_proj, name)
- vs_lib_configurations(vs_proj, name)
- vs_compilation_options(vs_proj, name, deps)
- add_vs_cpps(vs_proj, name)
- vs_footer(vs_proj)
-
add_lib('util', [])
add_lib('polynomial', ['util'])
add_lib('sat', ['util', 'sat_core'])
@@ -163,6 +26,11 @@ add_lib('nlsat', ['util', 'sat_core', 'polynomial'])
add_lib('subpaving', ['util'])
add_lib('ast', ['util', 'polynomial'])
add_lib('rewriter', ['util', 'ast', 'polynomial'])
-add_lib('model', ['util', 'ast', 'rewriter'])
+# Simplifier module will be deleted in the future.
+# It has been replaced with rewriter module.
+add_lib('simplifier', ['util', 'ast', 'rewriter'])
+# Model module should not depend on simplifier module.
+# We must replace all occurrences of simplifier with rewriter.
+add_lib('model', ['util', 'ast', 'rewriter', 'simplifier'])
add_lib('tactic', ['util', 'ast'])
diff --git a/mk_util.py b/mk_util.py
new file mode 100644
index 000000000..5073504c6
--- /dev/null
+++ b/mk_util.py
@@ -0,0 +1,155 @@
+############################################
+# Copyright (c) 2012 Microsoft Corporation
+#
+# Auxiliary scripts for generate Makefiles and Visual
+# Studio project files.
+#
+# Author: Leonardo de Moura (leonardo)
+############################################
+import os
+import glob
+
+def is_debug(mode):
+ return mode == 'Debug'
+
+def is_x64(platform):
+ return platform == 'x64'
+
+def mk_dir(d):
+ if not os.path.exists(d):
+ os.makedirs(d)
+
+def module_src_dir(name):
+ return '%s%s%s' % (SRC_DIR, os.sep, name)
+
+def module_build_dir(name):
+ return '%s%s%s' % (BUILD_DIR, os.sep, name)
+
+def vs_header(f):
+ f.write(
+'\n'
+'\n')
+
+GUI = 0
+Name2GUI = {}
+
+def vs_project_configurations(f, name):
+ global GUI, Name2GUI
+ f.write(' \n')
+ for mode in MODES:
+ for platform in PLATFORMS:
+ f.write(' \n' % (mode, platform))
+ f.write(' %s\n' % mode)
+ f.write(' %s\n' % platform)
+ f.write(' \n')
+ f.write(' \n')
+
+ f.write(' \n')
+ f.write(' {00000000-0000-0000-000--%s}\n' % GUI)
+ f.write(' %s\n' % name)
+ f.write(' Win32Proj\n')
+ f.write(' \n')
+ f.write(' \n')
+ Name2GUI[name] = GUI
+ GUI = GUI + 1
+
+def vs_lib_configurations(f, name):
+ for mode in MODES:
+ for platform in PLATFORMS:
+ f.write(' \n' % (mode, platform))
+ f.write(' StaticLibrary\n')
+ f.write(' Unicode\n')
+ f.write(' false\n')
+ f.write(' \n')
+
+ f.write(' \n')
+ f.write(' \n')
+ f.write(' \n')
+ f.write(' \n')
+ f.write(' \n')
+ f.write(' \n')
+
+ f.write(' \n')
+ for mode in MODES:
+ for platform in PLATFORMS:
+ if is_x64(platform):
+ f.write(' $(SolutionDir)$(Platform)\$(Configuration)\\n' %
+ (mode, platform))
+ else:
+ f.write(' $(SolutionDir)$(Configuration)\\n' % (mode, platform))
+ for mode in MODES:
+ for platform in PLATFORMS:
+ f.write(' %s\n' % (mode, platform, name))
+ f.write(' .lib\n' % (mode, platform))
+ f.write(' \n')
+
+def vs_compilation_options(f, name, deps):
+ for mode in MODES:
+ for platform in PLATFORMS:
+ f.write(' \n' % (mode, platform))
+ if is_x64(platform):
+ f.write(' \n')
+ f.write(' X64\n')
+ f.write(' \n')
+ f.write(' \n')
+ if is_debug(mode):
+ f.write(' Disabled\n')
+ else:
+ f.write(' Full\n')
+ options = VS_COMMON_OPTIONS
+ if is_debug(mode):
+ options = "%s;%s" % (options, VS_DBG_OPTIONS)
+ else:
+ options = "%s;%s" % (options, VS_RELEASE_OPTIONS)
+ if is_x64(platform):
+ options = "%s;_AMD64_" % options
+ f.write(' %s;%%(PreprocessorDefinitions)\n' % options)
+ if is_debug(mode):
+ f.write(' true\n')
+ f.write(' EnableFastChecks\n')
+ f.write(' Level3\n')
+ f.write(' MultiThreadedDebugDLL\n')
+ f.write(' true\n')
+ f.write(' ProgramDatabase\n')
+ f.write(' ')
+ f.write('..\..\src\%s' % name)
+ for dep in deps:
+ f.write(';..\..\src\%s' % dep)
+ f.write('\n')
+ f.write(' \n')
+ f.write(' \n')
+ f.write(' $(OutDir)%s.lib\n' % name)
+ f.write(' %(AdditionalLibraryDirectories)\n')
+ if is_x64(platform):
+ f.write(' MachineX64\n')
+ else:
+ f.write(' MachineX86\n')
+ f.write(' \n')
+ f.write(' \n')
+
+def add_vs_cpps(f, name):
+ f.write(' \n')
+ srcs = module_src_dir(name)
+ for cppfile in glob.glob(os.path.join(srcs, '*.cpp')):
+ f.write(' \n' % (os.sep, os.sep, cppfile))
+ f.write(' \n')
+
+def vs_footer(f):
+ f.write(
+' \n'
+' \n'
+' \n'
+'\n')
+
+def add_lib(name, deps):
+ module_dir = module_build_dir(name)
+ mk_dir(module_dir)
+
+ vs_proj = open('%s%s%s.vcxproj' % (module_dir, os.sep, name), 'w')
+ vs_header(vs_proj)
+ vs_project_configurations(vs_proj, name)
+ vs_lib_configurations(vs_proj, name)
+ vs_compilation_options(vs_proj, name, deps)
+ add_vs_cpps(vs_proj, name)
+ vs_footer(vs_proj)
+
diff --git a/lib/expr_map.cpp b/src/ast/expr_map.cpp
similarity index 100%
rename from lib/expr_map.cpp
rename to src/ast/expr_map.cpp
diff --git a/lib/expr_map.h b/src/ast/expr_map.h
similarity index 100%
rename from lib/expr_map.h
rename to src/ast/expr_map.h
diff --git a/lib/func_decl_dependencies.cpp b/src/ast/func_decl_dependencies.cpp
similarity index 100%
rename from lib/func_decl_dependencies.cpp
rename to src/ast/func_decl_dependencies.cpp
diff --git a/lib/func_decl_dependencies.h b/src/ast/func_decl_dependencies.h
similarity index 100%
rename from lib/func_decl_dependencies.h
rename to src/ast/func_decl_dependencies.h
diff --git a/lib/used_symbols.h b/src/ast/used_symbols.h
similarity index 100%
rename from lib/used_symbols.h
rename to src/ast/used_symbols.h
diff --git a/src/model/model_smt2_pp.cpp b/src/framework/model_smt2_pp.cpp
similarity index 100%
rename from src/model/model_smt2_pp.cpp
rename to src/framework/model_smt2_pp.cpp
diff --git a/src/model/model_smt2_pp.h b/src/framework/model_smt2_pp.h
similarity index 100%
rename from src/model/model_smt2_pp.h
rename to src/framework/model_smt2_pp.h
diff --git a/src/model/model.cpp b/src/model/model.cpp
index 9f2569ce5..4a9767cb0 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -20,7 +20,6 @@ Revision History:
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include"var_subst.h"
-#include"front_end_params.h"
#include"array_decl_plugin.h"
#include"well_sorted.h"
#include"used_symbols.h"
diff --git a/src/model/model_evaluator_params.cpp b/src/model/model_evaluator_params.cpp
deleted file mode 100644
index bfb4e2ee5..000000000
--- a/src/model/model_evaluator_params.cpp
+++ /dev/null
@@ -1,76 +0,0 @@
-/*++
-Copyright (c) 2011 Microsoft Corporation
-
-Module Name:
-
- model_evaluator_params.cpp
-
-Abstract:
-
- New parameter setting support for rewriter.
-
-Author:
-
- Leonardo (leonardo) 2011-04-22
-
-Notes:
-
---*/
-#include"model_evaluator_params.h"
-
-model_evaluator_params::model_evaluator_params() {
- reset();
-}
-
-void model_evaluator_params::reset() {
- m_model_completion = false;
- m_cache = true;
- m_max_steps = UINT_MAX;
- m_max_memory = UINT_MAX;
-}
-
-#define PARAM(name) param_names.push_back(name)
-
-void model_evaluator_params::get_params(svector & param_names) const {
- PARAM(":model-completion");
- PARAM(":cache");
- PARAM(":max-steps");
- PARAM(":max-memory");
-}
-
-#define DESCR(NAME, DR) if (strcmp(name, NAME) == 0) return DR
-
-char const * model_evaluator_params::get_param_descr(char const * name) const {
- DESCR(":model-completion", "(default: false) assigns an interpretation to symbols that are not intepreted by the model.");
- DESCR(":cache", "(default: true) cache intermediate results.");
- DESCR(":max-steps", "(default: infty) maximum number of steps.");
- DESCR(":max-memory", "(default: infty) maximum amount of memory in megabytes.");
- return 0;
-}
-
-#define RBOOL(NAME) if (strcmp(name, NAME) == 0) return CPK_BOOL
-#define RUINT(NAME) if (strcmp(name, NAME) == 0) return CPK_UINT
-
-param_kind model_evaluator_params::get_param_kind(char const * name) const {
- RBOOL(":model-completion");
- RBOOL(":cache");
- RUINT(":max-steps");
- RUINT(":max-memory");
- return CPK_INVALID;
-}
-
-#define SET(NAME, FIELD) if (strcmp(name, NAME) == 0) { FIELD = value; return true; }
-
-bool model_evaluator_params::set_bool_param(char const * name, bool value) {
- SET(":model-completion", m_model_completion);
- SET(":cache", m_cache);
- return false;
-}
-
-bool model_evaluator_params::set_uint_param(char const * name, unsigned value) {
- SET(":max-steps", m_max_steps);
- SET(":max-memory", m_max_memory);
- return false;
-}
-
-
diff --git a/src/model/proto_model.cpp b/src/model/proto_model.cpp
index 34f017eb8..4b5d201b9 100644
--- a/src/model/proto_model.cpp
+++ b/src/model/proto_model.cpp
@@ -20,7 +20,6 @@ Revision History:
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include"var_subst.h"
-#include"front_end_params.h"
#include"array_decl_plugin.h"
#include"well_sorted.h"
#include"used_symbols.h"
diff --git a/src/model/value.cpp b/src/model/value.cpp
deleted file mode 100644
index b81bbbb0b..000000000
--- a/src/model/value.cpp
+++ /dev/null
@@ -1,42 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
- value.cpp
-
-Abstract:
-
-
-
-Author:
-
- Leonardo de Moura (leonardo) 2007-08-17.
-
-Revision History:
-
---*/
-#include"value.h"
-
-void bool_value::display(std::ostream & out) const {
- out << (m_value ? "true" : "false");
-}
-
-unsigned bool_value::hash() const {
- return m_value ? 1 : 0;
-}
-
-bool bool_value::operator==(const value & other) const {
- const bool_value * o = dynamic_cast(&other);
- return o && m_value == o->m_value;
-}
-
-basic_factory::basic_factory(ast_manager & m):
- value_factory(symbol("basic"), m),
- m_bool(m) {
- m_bool = m.mk_type(m.get_basic_family_id(), BOOL_SORT);
- m_true = alloc(bool_value, true, m_bool.get());
- m_false = alloc(bool_value, false, m_bool.get());
-}
-
-
diff --git a/src/model/value.h b/src/model/value.h
deleted file mode 100644
index 2055449b8..000000000
--- a/src/model/value.h
+++ /dev/null
@@ -1,162 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
- value.h
-
-Abstract:
-
- Abstract class used to represent values in a model.
-
-Author:
-
- Leonardo de Moura (leonardo) 2007-08-14.
-
-Revision History:
-
---*/
-#ifndef _VALUE_H_
-#define _VALUE_H_
-
-#include"core_model.h"
-#include"ast.h"
-#include"ref.h"
-
-class model;
-
-class value {
- partition_id m_partition_id;
- unsigned m_ref_count;
- type_ast * m_type;
-
- friend class model;
-
- void set_partition_id(partition_id id) {
- m_partition_id = id;
- }
-
-public:
- value(type_ast * ty):
- m_partition_id(null_partition_id),
- m_ref_count(0),
- m_type(ty) {
- }
-
- virtual ~value() {}
-
- void inc_ref() { m_ref_count ++; }
-
- void dec_ref() {
- SASSERT(m_ref_count > 0);
- m_ref_count--;
- if (m_ref_count == 0) {
- dealloc(this);
- }
- }
-
- partition_id get_partition_id() { return m_partition_id; }
-
- type_ast * get_type() const { return m_type; }
-
- virtual void display(std::ostream & out) const = 0;
-
- virtual unsigned hash() const = 0;
-
- virtual bool operator==(const value & other) const = 0;
-
- virtual void infer_types(ast_vector & result) { /* default: do nothing */ }
-
- virtual void collect_used_partitions(svector & result) { /* default: do nothing */ }
-};
-
-inline std::ostream & operator<<(std::ostream & target, const value & v) {
- v.display(target);
- return target;
-}
-
-class value_factory {
- family_id m_fid;
-public:
- value_factory(symbol fname, ast_manager & m):
- m_fid(m.get_family_id(fname)) {
- }
-
- virtual ~value_factory() {}
-
- // Return some value of the given type
- virtual value * get_some_value(type_ast * ty) = 0;
-
- // Return two distinct values of the given type
- virtual bool get_some_values(type_ast * ty, ref & v1, ref & v2) = 0;
-
- // Return a fresh value of the given type
- virtual value * get_fresh_value(type_ast * ty) = 0;
-
- virtual value * update_value(value * source, const svector & pid2pid) {
- return source;
- }
-
- family_id get_family_id() const { return m_fid; }
-};
-
-class bool_value : public value {
- friend class basic_factory;
- bool m_value;
-
- bool_value(bool v, type_ast * ty):
- value(ty),
- m_value(v) {
- }
-
-public:
-
- bool get_value() const {
- return m_value;
- }
-
- virtual void display(std::ostream & out) const;
-
- virtual unsigned hash() const;
-
- virtual bool operator==(const value & other) const;
-};
-
-class basic_factory : public value_factory {
- ast_ref m_bool;
- ref m_true;
- ref m_false;
-public:
- basic_factory(ast_manager & m);
-
- virtual ~basic_factory() {}
-
- bool_value * get_true() const {
- return m_true.get();
- }
-
- bool_value * get_false() const {
- return m_false.get();
- }
-
- // Return some value of the given type
- virtual value * get_some_value(type_ast * ty) {
- return get_false();
- }
-
- // Return two distinct values of the given type
- virtual bool get_some_values(type_ast * ty, ref & v1, ref & v2) {
- v1 = get_false();
- v2 = get_true();
- return true;
- }
-
- // Return a fresh value of the given type
- virtual value * get_fresh_value(type_ast * ty) {
- // it is not possible to create new fresh values...
- return 0;
- }
-};
-
-#endif /* _VALUE_H_ */
-
diff --git a/lib/dl_simplifier_plugin.cpp b/src/muz/dl_simplifier_plugin.cpp
similarity index 100%
rename from lib/dl_simplifier_plugin.cpp
rename to src/muz/dl_simplifier_plugin.cpp
diff --git a/lib/dl_simplifier_plugin.h b/src/muz/dl_simplifier_plugin.h
similarity index 100%
rename from lib/dl_simplifier_plugin.h
rename to src/muz/dl_simplifier_plugin.h
diff --git a/lib/arith_simplifier_params.h b/src/simplifier/arith_simplifier_params.h
similarity index 100%
rename from lib/arith_simplifier_params.h
rename to src/simplifier/arith_simplifier_params.h
diff --git a/lib/arith_simplifier_plugin.cpp b/src/simplifier/arith_simplifier_plugin.cpp
similarity index 100%
rename from lib/arith_simplifier_plugin.cpp
rename to src/simplifier/arith_simplifier_plugin.cpp
diff --git a/lib/arith_simplifier_plugin.h b/src/simplifier/arith_simplifier_plugin.h
similarity index 100%
rename from lib/arith_simplifier_plugin.h
rename to src/simplifier/arith_simplifier_plugin.h
diff --git a/lib/base_simplifier.h b/src/simplifier/base_simplifier.h
similarity index 100%
rename from lib/base_simplifier.h
rename to src/simplifier/base_simplifier.h
diff --git a/lib/basic_simplifier_plugin.cpp b/src/simplifier/basic_simplifier_plugin.cpp
similarity index 100%
rename from lib/basic_simplifier_plugin.cpp
rename to src/simplifier/basic_simplifier_plugin.cpp
diff --git a/lib/basic_simplifier_plugin.h b/src/simplifier/basic_simplifier_plugin.h
similarity index 100%
rename from lib/basic_simplifier_plugin.h
rename to src/simplifier/basic_simplifier_plugin.h
diff --git a/lib/bv_simplifier_params.h b/src/simplifier/bv_simplifier_params.h
similarity index 100%
rename from lib/bv_simplifier_params.h
rename to src/simplifier/bv_simplifier_params.h
diff --git a/lib/bv_simplifier_plugin.cpp b/src/simplifier/bv_simplifier_plugin.cpp
similarity index 100%
rename from lib/bv_simplifier_plugin.cpp
rename to src/simplifier/bv_simplifier_plugin.cpp
diff --git a/lib/bv_simplifier_plugin.h b/src/simplifier/bv_simplifier_plugin.h
similarity index 100%
rename from lib/bv_simplifier_plugin.h
rename to src/simplifier/bv_simplifier_plugin.h
diff --git a/lib/datatype_simplifier_plugin.cpp b/src/simplifier/datatype_simplifier_plugin.cpp
similarity index 100%
rename from lib/datatype_simplifier_plugin.cpp
rename to src/simplifier/datatype_simplifier_plugin.cpp
diff --git a/lib/datatype_simplifier_plugin.h b/src/simplifier/datatype_simplifier_plugin.h
similarity index 100%
rename from lib/datatype_simplifier_plugin.h
rename to src/simplifier/datatype_simplifier_plugin.h
diff --git a/lib/poly_simplifier_plugin.cpp b/src/simplifier/poly_simplifier_plugin.cpp
similarity index 100%
rename from lib/poly_simplifier_plugin.cpp
rename to src/simplifier/poly_simplifier_plugin.cpp
diff --git a/lib/poly_simplifier_plugin.h b/src/simplifier/poly_simplifier_plugin.h
similarity index 100%
rename from lib/poly_simplifier_plugin.h
rename to src/simplifier/poly_simplifier_plugin.h
diff --git a/lib/simplifier.cpp b/src/simplifier/simplifier.cpp
similarity index 100%
rename from lib/simplifier.cpp
rename to src/simplifier/simplifier.cpp
diff --git a/lib/simplifier.h b/src/simplifier/simplifier.h
similarity index 100%
rename from lib/simplifier.h
rename to src/simplifier/simplifier.h
diff --git a/lib/simplifier_plugin.cpp b/src/simplifier/simplifier_plugin.cpp
similarity index 100%
rename from lib/simplifier_plugin.cpp
rename to src/simplifier/simplifier_plugin.cpp
diff --git a/lib/simplifier_plugin.h b/src/simplifier/simplifier_plugin.h
similarity index 100%
rename from lib/simplifier_plugin.h
rename to src/simplifier/simplifier_plugin.h
diff --git a/lib/plugin_manager.h b/src/util/plugin_manager.h
similarity index 100%
rename from lib/plugin_manager.h
rename to src/util/plugin_manager.h
diff --git a/src/util/smt2_util.cpp b/src/util/smt2_util.cpp
new file mode 100644
index 000000000..70979cc01
--- /dev/null
+++ b/src/util/smt2_util.cpp
@@ -0,0 +1,62 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+ smt2_util.cpp
+
+Abstract:
+
+ Goodies for SMT2 standard
+
+Author:
+
+ Leonardo (leonardo) 2012-10-20
+
+Notes:
+
+--*/
+#include"smt2_util.h"
+
+bool is_smt2_simple_symbol_char(char s) {
+ return
+ ('0' <= s && s <= '9') ||
+ ('a' <= s && s <= 'z') ||
+ ('A' <= s && s <= 'Z') ||
+ s == '~' || s == '!' || s == '@' || s == '$' || s == '%' || s == '^' || s == '&' ||
+ s == '*' || s == '_' || s == '-' || s == '+' || s == '=' || s == '<' || s == '>' ||
+ s == '.' || s == '?' || s == '/';
+}
+
+bool is_smt2_quoted_symbol(char const * s) {
+ if (s == 0)
+ return false;
+ if ('0' <= s[0] && s[0] <= '9')
+ return true;
+ unsigned len = static_cast(strlen(s));
+ for (unsigned i = 0; i < len; i++)
+ if (!is_smt2_simple_symbol_char(s[i]))
+ return true;
+ return false;
+}
+
+bool is_smt2_quoted_symbol(symbol const & s) {
+ if (s.is_numerical())
+ return false;
+ return is_smt2_quoted_symbol(s.bare_str());
+}
+
+std::string mk_smt2_quoted_symbol(symbol const & s) {
+ SASSERT(is_smt2_quoted_symbol(s));
+ string_buffer<> buffer;
+ buffer.append('|');
+ char const * str = s.bare_str();
+ while (*str) {
+ if (*str == '|' || *str == '\\')
+ buffer.append('\\');
+ buffer.append(*str);
+ str++;
+ }
+ buffer.append('|');
+ return std::string(buffer.c_str());
+}
diff --git a/src/util/smt2_util.h b/src/util/smt2_util.h
new file mode 100644
index 000000000..c2ab4a727
--- /dev/null
+++ b/src/util/smt2_util.h
@@ -0,0 +1,29 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+ smt2_util.h
+
+Abstract:
+
+ Goodies for SMT2 standard
+
+Author:
+
+ Leonardo (leonardo) 2012-10-20
+
+Notes:
+
+--*/
+#ifndef _SMT2_UTIL_H_
+#define _SMT2_UTIL_H_
+
+#include"symbol.h"
+
+bool is_smt2_simple_symbol_char(char c);
+bool is_smt2_quoted_symbol(char const * s);
+bool is_smt2_quoted_symbol(symbol const & s);
+std::string mk_smt2_quoted_symbol(symbol const & s);
+
+#endif