diff --git a/mk_make.py b/mk_make.py index d52d423d8..288f4dfbc 100644 --- a/mk_make.py +++ b/mk_make.py @@ -16,29 +16,44 @@ set_vs_options('WIN32;_WINDOWS;ASYNC_COMMANDS', 'Z3DEBUG;_TRACE;_DEBUG', 'NDEBUG;_EXTERNAL_RELEASE') +add_header('api_headers') add_lib('util', []) add_lib('polynomial', ['util']) -add_lib('sat', ['util', 'sat_core']) -add_lib('nlsat', ['util', 'sat_core', 'polynomial']) +add_lib('sat', ['util']) +# nlsat only reuses the file sat_types.h from sat +add_lib('nlsat', ['polynomial', 'sat']) add_lib('subpaving', ['util']) add_lib('ast', ['util', 'polynomial']) -add_lib('rewriter', ['util', 'ast', 'polynomial']) -# Old (non-modular) parameter framework. It has been subsumed by util\params.h. -# However, it is still used by many old components. -add_lib('old_params', ['util', 'ast', 'model']) +add_lib('rewriter', ['ast', 'polynomial']) # Simplifier module will be deleted in the future. # It has been replaced with rewriter module. -add_lib('simplifier', ['util', 'ast', 'rewriter', 'old_params']) +add_lib('simplifier', ['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', 'old_params']) -add_lib('framework', ['util', 'ast', 'model', 'old_params', 'simplifier', 'rewriter']) +add_lib('model', ['rewriter', 'simplifier']) +# Old (non-modular) parameter framework. It has been subsumed by util\params.h. +# However, it is still used by many old components. +add_lib('old_params', ['model', 'simplifier']) +add_lib('framework', ['rewriter', 'model', 'old_params', 'simplifier']) # Assertion set is the old tactic framework used in Z3 3.x. It will be deleted as soon as we finish the porting old # code to the new tactic framework. -add_lib('assertion_set', ['util', 'ast', 'framework', 'model', 'rewriter', 'old_params']) -add_lib('normal_forms', ['util', 'ast', 'old_params', 'simplifier', 'rewriter', 'assertion_set', 'framework', 'model']) -add_lib('spc', ['util', 'ast', 'simplifier', 'pattern', 'model', 'old_params', 'normal_forms', 'rewriter']) -add_lib('parser_util', ['util', 'ast']) -add_lib('smt2parser', ['util', 'ast', 'framework', 'model', 'old_params', 'rewriter', 'parser_util']) -add_lib('pattern', ['util', 'ast', 'simplifier', 'old_params']) -add_lib('smt', ['util', 'ast', 'assertion_set']) +add_lib('assertion_set', ['framework']) +add_lib('substitution', ['ast']) +add_lib('normal_forms', ['framework', 'assertion_set']) +add_lib('pattern', ['normal_forms']) +add_lib('spc', ['simplifier', 'substitution', 'old_params', 'pattern']) +add_lib('parser_util', ['ast']) +add_lib('smt2parser', ['framework', 'parser_util']) +add_lib('macros', ['simplifier', 'old_params']) +add_lib('grobner', ['ast']) +add_lib('euclid', ['util']) +add_lib('proof_checker', ['rewriter', 'spc']) +add_lib('bit_blaster', ['rewriter', 'simplifier', 'old_params', 'framework', 'assertion_set']) +add_lib('smt', ['assertion_set', 'bit_blaster', 'macros', 'normal_forms', 'framework', + 'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util']) +add_lib('sat_tactic', ['framework', 'sat']) +add_lib('sat_strategy', ['assertion_set', 'sat_tactic']) +# TODO: split muz_qe into muz, qe. Perhaps, we should also consider breaking muz into muz and pdr. +add_lib('muz_qe', ['smt', 'sat', 'smt2parser']) +# TODO: delete SMT 1.0 frontend +add_lib('smtparser', ['api_headers', 'smt', 'spc']) diff --git a/mk_util.py b/mk_util.py index 191c9787f..8935b54b3 100644 --- a/mk_util.py +++ b/mk_util.py @@ -35,6 +35,16 @@ VS_COMMON_OPTIONS='WIN32' VS_DBG_OPTIONS='_DEBUG' VS_RELEASE_OPTIONS='NDEBUG' +HEADERS = [] +LIBS = [] +LIB_DEPS = {} + +class MKException(Exception): + def __init__(self, value): + self.value = value + def __str__(self): + return repr(self.value) + def set_vs_options(common, dbg, release): global VS_COMMON_OPTIONS, VS_DBG_OPTIONS, VS_RELEASE_OPTIONS VS_COMMON_OPTIONS = common @@ -172,8 +182,39 @@ def vs_footer(f): ' \n' ' \n' '\n') - + +def check_new_component(name): + if (name in HEADERS) or (name in LIBS): + raise MKException("Component '%s' was already defined" % name) + +# Add a directory containing only .h files +def add_header(name): + check_new_component(name) + HEADERS.append(name) + +def find_all_deps(name, deps): + new_deps = [] + for dep in deps: + if dep in LIBS: + if not (dep in new_deps): + new_deps.append(dep) + for dep_dep in LIB_DEPS[dep]: + if not (dep_dep in new_deps): + new_deps.append(dep_dep) + elif dep in HEADERS: + if not (dep in new_deps): + new_deps.append(dep) + else: + raise MKException("Unknown component '%s' at '%s'." % (dep, name)) + return new_deps + def add_lib(name, deps): + check_new_component(name) + LIBS.append(name) + deps = find_all_deps(name, deps) + LIB_DEPS[name] = deps + print "Dependencies for '%s': %s" % (name, deps) + module_dir = module_build_dir(name) mk_dir(module_dir) diff --git a/lib/z3.h b/src/api_headers/z3.h similarity index 100% rename from lib/z3.h rename to src/api_headers/z3.h diff --git a/lib/z3_api.h b/src/api_headers/z3_api.h similarity index 100% rename from lib/z3_api.h rename to src/api_headers/z3_api.h diff --git a/lib/z3_internal_types.h b/src/api_headers/z3_internal_types.h similarity index 100% rename from lib/z3_internal_types.h rename to src/api_headers/z3_internal_types.h diff --git a/lib/z3_macros.h b/src/api_headers/z3_macros.h similarity index 100% rename from lib/z3_macros.h rename to src/api_headers/z3_macros.h diff --git a/lib/z3_v1.h b/src/api_headers/z3_v1.h similarity index 100% rename from lib/z3_v1.h rename to src/api_headers/z3_v1.h diff --git a/lib/expr2var.cpp b/src/ast/expr2var.cpp similarity index 100% rename from lib/expr2var.cpp rename to src/ast/expr2var.cpp diff --git a/lib/expr2var.h b/src/ast/expr2var.h similarity index 100% rename from lib/expr2var.h rename to src/ast/expr2var.h diff --git a/lib/expr_abstract.cpp b/src/ast/expr_abstract.cpp similarity index 100% rename from lib/expr_abstract.cpp rename to src/ast/expr_abstract.cpp diff --git a/lib/expr_abstract.h b/src/ast/expr_abstract.h similarity index 100% rename from lib/expr_abstract.h rename to src/ast/expr_abstract.h diff --git a/lib/expr_functors.cpp b/src/ast/expr_functors.cpp similarity index 100% rename from lib/expr_functors.cpp rename to src/ast/expr_functors.cpp diff --git a/lib/expr_functors.h b/src/ast/expr_functors.h similarity index 100% rename from lib/expr_functors.h rename to src/ast/expr_functors.h diff --git a/src/spc/expr_stat.cpp b/src/ast/expr_stat.cpp similarity index 100% rename from src/spc/expr_stat.cpp rename to src/ast/expr_stat.cpp diff --git a/src/spc/expr_stat.h b/src/ast/expr_stat.h similarity index 100% rename from src/spc/expr_stat.h rename to src/ast/expr_stat.h diff --git a/lib/static_features.cpp b/src/ast/static_features.cpp similarity index 100% rename from lib/static_features.cpp rename to src/ast/static_features.cpp diff --git a/lib/static_features.h b/src/ast/static_features.h similarity index 100% rename from lib/static_features.h rename to src/ast/static_features.h diff --git a/lib/trail.h b/src/ast/trail.h similarity index 100% rename from lib/trail.h rename to src/ast/trail.h diff --git a/lib/bit_blaster.cpp b/src/bit_blaster/bit_blaster.cpp similarity index 100% rename from lib/bit_blaster.cpp rename to src/bit_blaster/bit_blaster.cpp diff --git a/lib/bit_blaster.h b/src/bit_blaster/bit_blaster.h similarity index 100% rename from lib/bit_blaster.h rename to src/bit_blaster/bit_blaster.h diff --git a/lib/bit_blaster_model_converter.cpp b/src/bit_blaster/bit_blaster_model_converter.cpp similarity index 100% rename from lib/bit_blaster_model_converter.cpp rename to src/bit_blaster/bit_blaster_model_converter.cpp diff --git a/lib/bit_blaster_model_converter.h b/src/bit_blaster/bit_blaster_model_converter.h similarity index 100% rename from lib/bit_blaster_model_converter.h rename to src/bit_blaster/bit_blaster_model_converter.h diff --git a/lib/bit_blaster_rewriter.cpp b/src/bit_blaster/bit_blaster_rewriter.cpp similarity index 100% rename from lib/bit_blaster_rewriter.cpp rename to src/bit_blaster/bit_blaster_rewriter.cpp diff --git a/lib/bit_blaster_rewriter.h b/src/bit_blaster/bit_blaster_rewriter.h similarity index 100% rename from lib/bit_blaster_rewriter.h rename to src/bit_blaster/bit_blaster_rewriter.h diff --git a/lib/bit_blaster_tactic.cpp b/src/bit_blaster/bit_blaster_tactic.cpp similarity index 100% rename from lib/bit_blaster_tactic.cpp rename to src/bit_blaster/bit_blaster_tactic.cpp diff --git a/lib/bit_blaster_tactic.h b/src/bit_blaster/bit_blaster_tactic.h similarity index 100% rename from lib/bit_blaster_tactic.h rename to src/bit_blaster/bit_blaster_tactic.h diff --git a/lib/bit_blaster_tpl.h b/src/bit_blaster/bit_blaster_tpl.h similarity index 100% rename from lib/bit_blaster_tpl.h rename to src/bit_blaster/bit_blaster_tpl.h diff --git a/lib/bit_blaster_tpl_def.h b/src/bit_blaster/bit_blaster_tpl_def.h similarity index 100% rename from lib/bit_blaster_tpl_def.h rename to src/bit_blaster/bit_blaster_tpl_def.h diff --git a/lib/bv1_blaster_tactic.cpp b/src/bit_blaster/bv1_blaster_tactic.cpp similarity index 100% rename from lib/bv1_blaster_tactic.cpp rename to src/bit_blaster/bv1_blaster_tactic.cpp diff --git a/lib/bv1_blaster_tactic.h b/src/bit_blaster/bv1_blaster_tactic.h similarity index 100% rename from lib/bv1_blaster_tactic.h rename to src/bit_blaster/bv1_blaster_tactic.h diff --git a/lib/eager_bit_blaster.cpp b/src/bit_blaster/eager_bit_blaster.cpp similarity index 100% rename from lib/eager_bit_blaster.cpp rename to src/bit_blaster/eager_bit_blaster.cpp diff --git a/lib/eager_bit_blaster.h b/src/bit_blaster/eager_bit_blaster.h similarity index 100% rename from lib/eager_bit_blaster.h rename to src/bit_blaster/eager_bit_blaster.h diff --git a/lib/expr_weight.cpp b/src/dead/expr_weight.cpp similarity index 100% rename from lib/expr_weight.cpp rename to src/dead/expr_weight.cpp diff --git a/lib/expr_weight.h b/src/dead/expr_weight.h similarity index 100% rename from lib/expr_weight.h rename to src/dead/expr_weight.h diff --git a/lib/smt_euf.cpp b/src/dead/smt_euf.cpp similarity index 100% rename from lib/smt_euf.cpp rename to src/dead/smt_euf.cpp diff --git a/lib/smt_euf.h b/src/dead/smt_euf.h similarity index 100% rename from lib/smt_euf.h rename to src/dead/smt_euf.h diff --git a/lib/euclidean_solver.cpp b/src/euclid/euclidean_solver.cpp similarity index 100% rename from lib/euclidean_solver.cpp rename to src/euclid/euclidean_solver.cpp diff --git a/lib/euclidean_solver.h b/src/euclid/euclidean_solver.h similarity index 100% rename from lib/euclidean_solver.h rename to src/euclid/euclidean_solver.h diff --git a/lib/goal_shared_occs.cpp b/src/framework/goal_shared_occs.cpp similarity index 100% rename from lib/goal_shared_occs.cpp rename to src/framework/goal_shared_occs.cpp diff --git a/lib/goal_shared_occs.h b/src/framework/goal_shared_occs.h similarity index 100% rename from lib/goal_shared_occs.h rename to src/framework/goal_shared_occs.h diff --git a/lib/strategic_solver.cpp b/src/framework/strategic_solver.cpp similarity index 100% rename from lib/strategic_solver.cpp rename to src/framework/strategic_solver.cpp diff --git a/lib/strategic_solver.h b/src/framework/strategic_solver.h similarity index 100% rename from lib/strategic_solver.h rename to src/framework/strategic_solver.h diff --git a/lib/grobner.cpp b/src/grobner/grobner.cpp similarity index 100% rename from lib/grobner.cpp rename to src/grobner/grobner.cpp diff --git a/lib/grobner.h b/src/grobner/grobner.h similarity index 100% rename from lib/grobner.h rename to src/grobner/grobner.h diff --git a/lib/macro_finder.cpp b/src/macros/macro_finder.cpp similarity index 100% rename from lib/macro_finder.cpp rename to src/macros/macro_finder.cpp diff --git a/lib/macro_finder.h b/src/macros/macro_finder.h similarity index 100% rename from lib/macro_finder.h rename to src/macros/macro_finder.h diff --git a/lib/macro_manager.cpp b/src/macros/macro_manager.cpp similarity index 100% rename from lib/macro_manager.cpp rename to src/macros/macro_manager.cpp diff --git a/lib/macro_manager.h b/src/macros/macro_manager.h similarity index 100% rename from lib/macro_manager.h rename to src/macros/macro_manager.h diff --git a/lib/macro_substitution.cpp b/src/macros/macro_substitution.cpp similarity index 100% rename from lib/macro_substitution.cpp rename to src/macros/macro_substitution.cpp diff --git a/lib/macro_substitution.h b/src/macros/macro_substitution.h similarity index 100% rename from lib/macro_substitution.h rename to src/macros/macro_substitution.h diff --git a/lib/macro_util.cpp b/src/macros/macro_util.cpp similarity index 100% rename from lib/macro_util.cpp rename to src/macros/macro_util.cpp diff --git a/lib/macro_util.h b/src/macros/macro_util.h similarity index 100% rename from lib/macro_util.h rename to src/macros/macro_util.h diff --git a/lib/quasi_macros.cpp b/src/macros/quasi_macros.cpp similarity index 100% rename from lib/quasi_macros.cpp rename to src/macros/quasi_macros.cpp diff --git a/lib/quasi_macros.h b/src/macros/quasi_macros.h similarity index 100% rename from lib/quasi_macros.h rename to src/macros/quasi_macros.h diff --git a/src/old_params/model_params.cpp b/src/model/model_params.cpp similarity index 100% rename from src/old_params/model_params.cpp rename to src/model/model_params.cpp diff --git a/src/old_params/model_params.h b/src/model/model_params.h similarity index 100% rename from src/old_params/model_params.h rename to src/model/model_params.h diff --git a/src/muz_qe/README b/src/muz_qe/README new file mode 100644 index 000000000..5d6f433b8 --- /dev/null +++ b/src/muz_qe/README @@ -0,0 +1 @@ +muZ and Quantifier Elimination modules \ No newline at end of file diff --git a/lib/arith_bounds_tactic.cpp b/src/muz_qe/arith_bounds_tactic.cpp similarity index 100% rename from lib/arith_bounds_tactic.cpp rename to src/muz_qe/arith_bounds_tactic.cpp diff --git a/lib/arith_bounds_tactic.h b/src/muz_qe/arith_bounds_tactic.h similarity index 100% rename from lib/arith_bounds_tactic.h rename to src/muz_qe/arith_bounds_tactic.h diff --git a/lib/dl_base.cpp b/src/muz_qe/dl_base.cpp similarity index 100% rename from lib/dl_base.cpp rename to src/muz_qe/dl_base.cpp diff --git a/lib/dl_base.h b/src/muz_qe/dl_base.h similarity index 100% rename from lib/dl_base.h rename to src/muz_qe/dl_base.h diff --git a/lib/dl_bmc_engine.cpp b/src/muz_qe/dl_bmc_engine.cpp similarity index 100% rename from lib/dl_bmc_engine.cpp rename to src/muz_qe/dl_bmc_engine.cpp diff --git a/lib/dl_bmc_engine.h b/src/muz_qe/dl_bmc_engine.h similarity index 100% rename from lib/dl_bmc_engine.h rename to src/muz_qe/dl_bmc_engine.h diff --git a/lib/dl_bound_relation.cpp b/src/muz_qe/dl_bound_relation.cpp similarity index 100% rename from lib/dl_bound_relation.cpp rename to src/muz_qe/dl_bound_relation.cpp diff --git a/lib/dl_bound_relation.h b/src/muz_qe/dl_bound_relation.h similarity index 100% rename from lib/dl_bound_relation.h rename to src/muz_qe/dl_bound_relation.h diff --git a/lib/dl_check_table.cpp b/src/muz_qe/dl_check_table.cpp similarity index 100% rename from lib/dl_check_table.cpp rename to src/muz_qe/dl_check_table.cpp diff --git a/lib/dl_check_table.h b/src/muz_qe/dl_check_table.h similarity index 100% rename from lib/dl_check_table.h rename to src/muz_qe/dl_check_table.h diff --git a/lib/dl_cmds.cpp b/src/muz_qe/dl_cmds.cpp similarity index 100% rename from lib/dl_cmds.cpp rename to src/muz_qe/dl_cmds.cpp diff --git a/lib/dl_cmds.h b/src/muz_qe/dl_cmds.h similarity index 100% rename from lib/dl_cmds.h rename to src/muz_qe/dl_cmds.h diff --git a/lib/dl_compiler.cpp b/src/muz_qe/dl_compiler.cpp similarity index 100% rename from lib/dl_compiler.cpp rename to src/muz_qe/dl_compiler.cpp diff --git a/lib/dl_compiler.h b/src/muz_qe/dl_compiler.h similarity index 100% rename from lib/dl_compiler.h rename to src/muz_qe/dl_compiler.h diff --git a/lib/dl_context.cpp b/src/muz_qe/dl_context.cpp similarity index 100% rename from lib/dl_context.cpp rename to src/muz_qe/dl_context.cpp diff --git a/lib/dl_context.h b/src/muz_qe/dl_context.h similarity index 100% rename from lib/dl_context.h rename to src/muz_qe/dl_context.h diff --git a/lib/dl_costs.cpp b/src/muz_qe/dl_costs.cpp similarity index 100% rename from lib/dl_costs.cpp rename to src/muz_qe/dl_costs.cpp diff --git a/lib/dl_costs.h b/src/muz_qe/dl_costs.h similarity index 100% rename from lib/dl_costs.h rename to src/muz_qe/dl_costs.h diff --git a/lib/dl_external_relation.cpp b/src/muz_qe/dl_external_relation.cpp similarity index 100% rename from lib/dl_external_relation.cpp rename to src/muz_qe/dl_external_relation.cpp diff --git a/lib/dl_external_relation.h b/src/muz_qe/dl_external_relation.h similarity index 100% rename from lib/dl_external_relation.h rename to src/muz_qe/dl_external_relation.h diff --git a/lib/dl_finite_product_relation.cpp b/src/muz_qe/dl_finite_product_relation.cpp similarity index 100% rename from lib/dl_finite_product_relation.cpp rename to src/muz_qe/dl_finite_product_relation.cpp diff --git a/lib/dl_finite_product_relation.h b/src/muz_qe/dl_finite_product_relation.h similarity index 100% rename from lib/dl_finite_product_relation.h rename to src/muz_qe/dl_finite_product_relation.h diff --git a/lib/dl_instruction.cpp b/src/muz_qe/dl_instruction.cpp similarity index 100% rename from lib/dl_instruction.cpp rename to src/muz_qe/dl_instruction.cpp diff --git a/lib/dl_instruction.h b/src/muz_qe/dl_instruction.h similarity index 100% rename from lib/dl_instruction.h rename to src/muz_qe/dl_instruction.h diff --git a/lib/dl_interval_relation.cpp b/src/muz_qe/dl_interval_relation.cpp similarity index 100% rename from lib/dl_interval_relation.cpp rename to src/muz_qe/dl_interval_relation.cpp diff --git a/lib/dl_interval_relation.h b/src/muz_qe/dl_interval_relation.h similarity index 100% rename from lib/dl_interval_relation.h rename to src/muz_qe/dl_interval_relation.h diff --git a/lib/dl_mk_bit_blast.cpp b/src/muz_qe/dl_mk_bit_blast.cpp similarity index 100% rename from lib/dl_mk_bit_blast.cpp rename to src/muz_qe/dl_mk_bit_blast.cpp diff --git a/lib/dl_mk_bit_blast.h b/src/muz_qe/dl_mk_bit_blast.h similarity index 100% rename from lib/dl_mk_bit_blast.h rename to src/muz_qe/dl_mk_bit_blast.h diff --git a/lib/dl_mk_coalesce.cpp b/src/muz_qe/dl_mk_coalesce.cpp similarity index 100% rename from lib/dl_mk_coalesce.cpp rename to src/muz_qe/dl_mk_coalesce.cpp diff --git a/lib/dl_mk_coalesce.h b/src/muz_qe/dl_mk_coalesce.h similarity index 100% rename from lib/dl_mk_coalesce.h rename to src/muz_qe/dl_mk_coalesce.h diff --git a/lib/dl_mk_coi_filter.cpp b/src/muz_qe/dl_mk_coi_filter.cpp similarity index 100% rename from lib/dl_mk_coi_filter.cpp rename to src/muz_qe/dl_mk_coi_filter.cpp diff --git a/lib/dl_mk_coi_filter.h b/src/muz_qe/dl_mk_coi_filter.h similarity index 100% rename from lib/dl_mk_coi_filter.h rename to src/muz_qe/dl_mk_coi_filter.h diff --git a/lib/dl_mk_explanations.cpp b/src/muz_qe/dl_mk_explanations.cpp similarity index 100% rename from lib/dl_mk_explanations.cpp rename to src/muz_qe/dl_mk_explanations.cpp diff --git a/lib/dl_mk_explanations.h b/src/muz_qe/dl_mk_explanations.h similarity index 100% rename from lib/dl_mk_explanations.h rename to src/muz_qe/dl_mk_explanations.h diff --git a/lib/dl_mk_filter_rules.cpp b/src/muz_qe/dl_mk_filter_rules.cpp similarity index 100% rename from lib/dl_mk_filter_rules.cpp rename to src/muz_qe/dl_mk_filter_rules.cpp diff --git a/lib/dl_mk_filter_rules.h b/src/muz_qe/dl_mk_filter_rules.h similarity index 100% rename from lib/dl_mk_filter_rules.h rename to src/muz_qe/dl_mk_filter_rules.h diff --git a/lib/dl_mk_interp_tail_simplifier.cpp b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp similarity index 100% rename from lib/dl_mk_interp_tail_simplifier.cpp rename to src/muz_qe/dl_mk_interp_tail_simplifier.cpp diff --git a/lib/dl_mk_interp_tail_simplifier.h b/src/muz_qe/dl_mk_interp_tail_simplifier.h similarity index 100% rename from lib/dl_mk_interp_tail_simplifier.h rename to src/muz_qe/dl_mk_interp_tail_simplifier.h diff --git a/lib/dl_mk_magic_sets.cpp b/src/muz_qe/dl_mk_magic_sets.cpp similarity index 100% rename from lib/dl_mk_magic_sets.cpp rename to src/muz_qe/dl_mk_magic_sets.cpp diff --git a/lib/dl_mk_magic_sets.h b/src/muz_qe/dl_mk_magic_sets.h similarity index 100% rename from lib/dl_mk_magic_sets.h rename to src/muz_qe/dl_mk_magic_sets.h diff --git a/lib/dl_mk_partial_equiv.cpp b/src/muz_qe/dl_mk_partial_equiv.cpp similarity index 100% rename from lib/dl_mk_partial_equiv.cpp rename to src/muz_qe/dl_mk_partial_equiv.cpp diff --git a/lib/dl_mk_partial_equiv.h b/src/muz_qe/dl_mk_partial_equiv.h similarity index 100% rename from lib/dl_mk_partial_equiv.h rename to src/muz_qe/dl_mk_partial_equiv.h diff --git a/lib/dl_mk_rule_inliner.cpp b/src/muz_qe/dl_mk_rule_inliner.cpp similarity index 100% rename from lib/dl_mk_rule_inliner.cpp rename to src/muz_qe/dl_mk_rule_inliner.cpp diff --git a/lib/dl_mk_rule_inliner.h b/src/muz_qe/dl_mk_rule_inliner.h similarity index 100% rename from lib/dl_mk_rule_inliner.h rename to src/muz_qe/dl_mk_rule_inliner.h diff --git a/lib/dl_mk_similarity_compressor.cpp b/src/muz_qe/dl_mk_similarity_compressor.cpp similarity index 100% rename from lib/dl_mk_similarity_compressor.cpp rename to src/muz_qe/dl_mk_similarity_compressor.cpp diff --git a/lib/dl_mk_similarity_compressor.h b/src/muz_qe/dl_mk_similarity_compressor.h similarity index 100% rename from lib/dl_mk_similarity_compressor.h rename to src/muz_qe/dl_mk_similarity_compressor.h diff --git a/lib/dl_mk_simple_joins.cpp b/src/muz_qe/dl_mk_simple_joins.cpp similarity index 100% rename from lib/dl_mk_simple_joins.cpp rename to src/muz_qe/dl_mk_simple_joins.cpp diff --git a/lib/dl_mk_simple_joins.h b/src/muz_qe/dl_mk_simple_joins.h similarity index 100% rename from lib/dl_mk_simple_joins.h rename to src/muz_qe/dl_mk_simple_joins.h diff --git a/lib/dl_mk_slice.cpp b/src/muz_qe/dl_mk_slice.cpp similarity index 100% rename from lib/dl_mk_slice.cpp rename to src/muz_qe/dl_mk_slice.cpp diff --git a/lib/dl_mk_slice.h b/src/muz_qe/dl_mk_slice.h similarity index 100% rename from lib/dl_mk_slice.h rename to src/muz_qe/dl_mk_slice.h diff --git a/lib/dl_mk_subsumption_checker.cpp b/src/muz_qe/dl_mk_subsumption_checker.cpp similarity index 100% rename from lib/dl_mk_subsumption_checker.cpp rename to src/muz_qe/dl_mk_subsumption_checker.cpp diff --git a/lib/dl_mk_subsumption_checker.h b/src/muz_qe/dl_mk_subsumption_checker.h similarity index 100% rename from lib/dl_mk_subsumption_checker.h rename to src/muz_qe/dl_mk_subsumption_checker.h diff --git a/lib/dl_mk_unbound_compressor.cpp b/src/muz_qe/dl_mk_unbound_compressor.cpp similarity index 100% rename from lib/dl_mk_unbound_compressor.cpp rename to src/muz_qe/dl_mk_unbound_compressor.cpp diff --git a/lib/dl_mk_unbound_compressor.h b/src/muz_qe/dl_mk_unbound_compressor.h similarity index 100% rename from lib/dl_mk_unbound_compressor.h rename to src/muz_qe/dl_mk_unbound_compressor.h diff --git a/lib/dl_mk_unfold.cpp b/src/muz_qe/dl_mk_unfold.cpp similarity index 100% rename from lib/dl_mk_unfold.cpp rename to src/muz_qe/dl_mk_unfold.cpp diff --git a/lib/dl_mk_unfold.h b/src/muz_qe/dl_mk_unfold.h similarity index 100% rename from lib/dl_mk_unfold.h rename to src/muz_qe/dl_mk_unfold.h diff --git a/lib/dl_product_relation.cpp b/src/muz_qe/dl_product_relation.cpp similarity index 100% rename from lib/dl_product_relation.cpp rename to src/muz_qe/dl_product_relation.cpp diff --git a/lib/dl_product_relation.h b/src/muz_qe/dl_product_relation.h similarity index 100% rename from lib/dl_product_relation.h rename to src/muz_qe/dl_product_relation.h diff --git a/lib/dl_relation_manager.cpp b/src/muz_qe/dl_relation_manager.cpp similarity index 100% rename from lib/dl_relation_manager.cpp rename to src/muz_qe/dl_relation_manager.cpp diff --git a/lib/dl_relation_manager.h b/src/muz_qe/dl_relation_manager.h similarity index 100% rename from lib/dl_relation_manager.h rename to src/muz_qe/dl_relation_manager.h diff --git a/lib/dl_rule.cpp b/src/muz_qe/dl_rule.cpp similarity index 100% rename from lib/dl_rule.cpp rename to src/muz_qe/dl_rule.cpp diff --git a/lib/dl_rule.h b/src/muz_qe/dl_rule.h similarity index 100% rename from lib/dl_rule.h rename to src/muz_qe/dl_rule.h diff --git a/lib/dl_rule_set.cpp b/src/muz_qe/dl_rule_set.cpp similarity index 100% rename from lib/dl_rule_set.cpp rename to src/muz_qe/dl_rule_set.cpp diff --git a/lib/dl_rule_set.h b/src/muz_qe/dl_rule_set.h similarity index 100% rename from lib/dl_rule_set.h rename to src/muz_qe/dl_rule_set.h diff --git a/lib/dl_rule_subsumption_index.cpp b/src/muz_qe/dl_rule_subsumption_index.cpp similarity index 100% rename from lib/dl_rule_subsumption_index.cpp rename to src/muz_qe/dl_rule_subsumption_index.cpp diff --git a/lib/dl_rule_subsumption_index.h b/src/muz_qe/dl_rule_subsumption_index.h similarity index 100% rename from lib/dl_rule_subsumption_index.h rename to src/muz_qe/dl_rule_subsumption_index.h diff --git a/lib/dl_rule_transformer.cpp b/src/muz_qe/dl_rule_transformer.cpp similarity index 100% rename from lib/dl_rule_transformer.cpp rename to src/muz_qe/dl_rule_transformer.cpp diff --git a/lib/dl_rule_transformer.h b/src/muz_qe/dl_rule_transformer.h similarity index 100% rename from lib/dl_rule_transformer.h rename to src/muz_qe/dl_rule_transformer.h diff --git a/lib/dl_sieve_relation.cpp b/src/muz_qe/dl_sieve_relation.cpp similarity index 100% rename from lib/dl_sieve_relation.cpp rename to src/muz_qe/dl_sieve_relation.cpp diff --git a/lib/dl_sieve_relation.h b/src/muz_qe/dl_sieve_relation.h similarity index 100% rename from lib/dl_sieve_relation.h rename to src/muz_qe/dl_sieve_relation.h diff --git a/src/muz/dl_simplifier_plugin.cpp b/src/muz_qe/dl_simplifier_plugin.cpp similarity index 100% rename from src/muz/dl_simplifier_plugin.cpp rename to src/muz_qe/dl_simplifier_plugin.cpp diff --git a/src/muz/dl_simplifier_plugin.h b/src/muz_qe/dl_simplifier_plugin.h similarity index 100% rename from src/muz/dl_simplifier_plugin.h rename to src/muz_qe/dl_simplifier_plugin.h diff --git a/lib/dl_skip_table.cpp b/src/muz_qe/dl_skip_table.cpp similarity index 100% rename from lib/dl_skip_table.cpp rename to src/muz_qe/dl_skip_table.cpp diff --git a/lib/dl_skip_table.h b/src/muz_qe/dl_skip_table.h similarity index 100% rename from lib/dl_skip_table.h rename to src/muz_qe/dl_skip_table.h diff --git a/lib/dl_smt_relation.cpp b/src/muz_qe/dl_smt_relation.cpp similarity index 100% rename from lib/dl_smt_relation.cpp rename to src/muz_qe/dl_smt_relation.cpp diff --git a/lib/dl_smt_relation.h b/src/muz_qe/dl_smt_relation.h similarity index 100% rename from lib/dl_smt_relation.h rename to src/muz_qe/dl_smt_relation.h diff --git a/lib/dl_sparse_table.cpp b/src/muz_qe/dl_sparse_table.cpp similarity index 100% rename from lib/dl_sparse_table.cpp rename to src/muz_qe/dl_sparse_table.cpp diff --git a/lib/dl_sparse_table.h b/src/muz_qe/dl_sparse_table.h similarity index 100% rename from lib/dl_sparse_table.h rename to src/muz_qe/dl_sparse_table.h diff --git a/lib/dl_table.cpp b/src/muz_qe/dl_table.cpp similarity index 100% rename from lib/dl_table.cpp rename to src/muz_qe/dl_table.cpp diff --git a/lib/dl_table.h b/src/muz_qe/dl_table.h similarity index 100% rename from lib/dl_table.h rename to src/muz_qe/dl_table.h diff --git a/lib/dl_table_plugin.h b/src/muz_qe/dl_table_plugin.h similarity index 100% rename from lib/dl_table_plugin.h rename to src/muz_qe/dl_table_plugin.h diff --git a/lib/dl_table_relation.cpp b/src/muz_qe/dl_table_relation.cpp similarity index 100% rename from lib/dl_table_relation.cpp rename to src/muz_qe/dl_table_relation.cpp diff --git a/lib/dl_table_relation.h b/src/muz_qe/dl_table_relation.h similarity index 100% rename from lib/dl_table_relation.h rename to src/muz_qe/dl_table_relation.h diff --git a/lib/dl_util.cpp b/src/muz_qe/dl_util.cpp similarity index 100% rename from lib/dl_util.cpp rename to src/muz_qe/dl_util.cpp diff --git a/lib/dl_util.h b/src/muz_qe/dl_util.h similarity index 100% rename from lib/dl_util.h rename to src/muz_qe/dl_util.h diff --git a/lib/dl_vector_relation.h b/src/muz_qe/dl_vector_relation.h similarity index 100% rename from lib/dl_vector_relation.h rename to src/muz_qe/dl_vector_relation.h diff --git a/lib/horn_subsume_model_converter.cpp b/src/muz_qe/horn_subsume_model_converter.cpp similarity index 99% rename from lib/horn_subsume_model_converter.cpp rename to src/muz_qe/horn_subsume_model_converter.cpp index 83061ca6f..a203a9fee 100644 --- a/lib/horn_subsume_model_converter.cpp +++ b/src/muz_qe/horn_subsume_model_converter.cpp @@ -24,6 +24,7 @@ Revision History: #include "model_smt2_pp.h" #include "bool_rewriter.h" #include "th_rewriter.h" +#include "for_each_expr.h" void horn_subsume_model_converter::insert(app* head, expr* body) { func_decl_ref pred(m); diff --git a/lib/horn_subsume_model_converter.h b/src/muz_qe/horn_subsume_model_converter.h similarity index 100% rename from lib/horn_subsume_model_converter.h rename to src/muz_qe/horn_subsume_model_converter.h diff --git a/lib/model2expr.cpp b/src/muz_qe/model2expr.cpp similarity index 100% rename from lib/model2expr.cpp rename to src/muz_qe/model2expr.cpp diff --git a/lib/model2expr.h b/src/muz_qe/model2expr.h similarity index 100% rename from lib/model2expr.h rename to src/muz_qe/model2expr.h diff --git a/lib/nlarith_util.cpp b/src/muz_qe/nlarith_util.cpp similarity index 100% rename from lib/nlarith_util.cpp rename to src/muz_qe/nlarith_util.cpp diff --git a/lib/nlarith_util.h b/src/muz_qe/nlarith_util.h similarity index 100% rename from lib/nlarith_util.h rename to src/muz_qe/nlarith_util.h diff --git a/lib/pdr_context.cpp b/src/muz_qe/pdr_context.cpp similarity index 100% rename from lib/pdr_context.cpp rename to src/muz_qe/pdr_context.cpp diff --git a/lib/pdr_context.h b/src/muz_qe/pdr_context.h similarity index 100% rename from lib/pdr_context.h rename to src/muz_qe/pdr_context.h diff --git a/lib/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp similarity index 100% rename from lib/pdr_dl_interface.cpp rename to src/muz_qe/pdr_dl_interface.cpp diff --git a/lib/pdr_dl_interface.h b/src/muz_qe/pdr_dl_interface.h similarity index 100% rename from lib/pdr_dl_interface.h rename to src/muz_qe/pdr_dl_interface.h diff --git a/lib/pdr_farkas_learner.cpp b/src/muz_qe/pdr_farkas_learner.cpp similarity index 99% rename from lib/pdr_farkas_learner.cpp rename to src/muz_qe/pdr_farkas_learner.cpp index 6494bd223..9dbe91d0b 100644 --- a/lib/pdr_farkas_learner.cpp +++ b/src/muz_qe/pdr_farkas_learner.cpp @@ -29,7 +29,6 @@ Revision History: #include "pdr_util.h" #include "pdr_farkas_learner.h" #include "th_rewriter.h" -#include "smtparser.h" #include "pdr_interpolant_provider.h" #include "ast_ll_pp.h" #include "arith_bounds_tactic.h" @@ -858,6 +857,7 @@ namespace pdr { void farkas_learner::test(char const* filename) { +#if 0 if (!filename) { test(); return; @@ -886,6 +886,7 @@ namespace pdr { expr_ref_vector lemmas(m); bool res = fl.get_lemma_guesses(A, B, lemmas); std::cout << "lemmas: " << pp_cube(lemmas, m) << "\n"; +#endif } }; diff --git a/lib/pdr_farkas_learner.h b/src/muz_qe/pdr_farkas_learner.h similarity index 100% rename from lib/pdr_farkas_learner.h rename to src/muz_qe/pdr_farkas_learner.h diff --git a/lib/pdr_generalizers.cpp b/src/muz_qe/pdr_generalizers.cpp similarity index 100% rename from lib/pdr_generalizers.cpp rename to src/muz_qe/pdr_generalizers.cpp diff --git a/lib/pdr_generalizers.h b/src/muz_qe/pdr_generalizers.h similarity index 100% rename from lib/pdr_generalizers.h rename to src/muz_qe/pdr_generalizers.h diff --git a/lib/pdr_interpolant_provider.cpp b/src/muz_qe/pdr_interpolant_provider.cpp similarity index 100% rename from lib/pdr_interpolant_provider.cpp rename to src/muz_qe/pdr_interpolant_provider.cpp diff --git a/lib/pdr_interpolant_provider.h b/src/muz_qe/pdr_interpolant_provider.h similarity index 100% rename from lib/pdr_interpolant_provider.h rename to src/muz_qe/pdr_interpolant_provider.h diff --git a/lib/pdr_manager.cpp b/src/muz_qe/pdr_manager.cpp similarity index 100% rename from lib/pdr_manager.cpp rename to src/muz_qe/pdr_manager.cpp diff --git a/lib/pdr_manager.h b/src/muz_qe/pdr_manager.h similarity index 100% rename from lib/pdr_manager.h rename to src/muz_qe/pdr_manager.h diff --git a/lib/pdr_prop_solver.cpp b/src/muz_qe/pdr_prop_solver.cpp similarity index 100% rename from lib/pdr_prop_solver.cpp rename to src/muz_qe/pdr_prop_solver.cpp diff --git a/lib/pdr_prop_solver.h b/src/muz_qe/pdr_prop_solver.h similarity index 100% rename from lib/pdr_prop_solver.h rename to src/muz_qe/pdr_prop_solver.h diff --git a/lib/pdr_quantifiers.cpp b/src/muz_qe/pdr_quantifiers.cpp similarity index 100% rename from lib/pdr_quantifiers.cpp rename to src/muz_qe/pdr_quantifiers.cpp diff --git a/lib/pdr_quantifiers.h b/src/muz_qe/pdr_quantifiers.h similarity index 100% rename from lib/pdr_quantifiers.h rename to src/muz_qe/pdr_quantifiers.h diff --git a/lib/pdr_reachable_cache.cpp b/src/muz_qe/pdr_reachable_cache.cpp similarity index 100% rename from lib/pdr_reachable_cache.cpp rename to src/muz_qe/pdr_reachable_cache.cpp diff --git a/lib/pdr_reachable_cache.h b/src/muz_qe/pdr_reachable_cache.h similarity index 100% rename from lib/pdr_reachable_cache.h rename to src/muz_qe/pdr_reachable_cache.h diff --git a/lib/pdr_smt_context_manager.cpp b/src/muz_qe/pdr_smt_context_manager.cpp similarity index 100% rename from lib/pdr_smt_context_manager.cpp rename to src/muz_qe/pdr_smt_context_manager.cpp diff --git a/lib/pdr_smt_context_manager.h b/src/muz_qe/pdr_smt_context_manager.h similarity index 100% rename from lib/pdr_smt_context_manager.h rename to src/muz_qe/pdr_smt_context_manager.h diff --git a/lib/pdr_sym_mux.cpp b/src/muz_qe/pdr_sym_mux.cpp similarity index 100% rename from lib/pdr_sym_mux.cpp rename to src/muz_qe/pdr_sym_mux.cpp diff --git a/lib/pdr_sym_mux.h b/src/muz_qe/pdr_sym_mux.h similarity index 100% rename from lib/pdr_sym_mux.h rename to src/muz_qe/pdr_sym_mux.h diff --git a/lib/pdr_util.cpp b/src/muz_qe/pdr_util.cpp similarity index 100% rename from lib/pdr_util.cpp rename to src/muz_qe/pdr_util.cpp diff --git a/lib/pdr_util.h b/src/muz_qe/pdr_util.h similarity index 100% rename from lib/pdr_util.h rename to src/muz_qe/pdr_util.h diff --git a/lib/proof_utils.cpp b/src/muz_qe/proof_utils.cpp similarity index 100% rename from lib/proof_utils.cpp rename to src/muz_qe/proof_utils.cpp diff --git a/lib/proof_utils.h b/src/muz_qe/proof_utils.h similarity index 100% rename from lib/proof_utils.h rename to src/muz_qe/proof_utils.h diff --git a/lib/qe.cpp b/src/muz_qe/qe.cpp similarity index 100% rename from lib/qe.cpp rename to src/muz_qe/qe.cpp diff --git a/lib/qe.h b/src/muz_qe/qe.h similarity index 100% rename from lib/qe.h rename to src/muz_qe/qe.h diff --git a/lib/qe_arith_plugin.cpp b/src/muz_qe/qe_arith_plugin.cpp similarity index 100% rename from lib/qe_arith_plugin.cpp rename to src/muz_qe/qe_arith_plugin.cpp diff --git a/lib/qe_array_plugin.cpp b/src/muz_qe/qe_array_plugin.cpp similarity index 100% rename from lib/qe_array_plugin.cpp rename to src/muz_qe/qe_array_plugin.cpp diff --git a/lib/qe_bool_plugin.cpp b/src/muz_qe/qe_bool_plugin.cpp similarity index 100% rename from lib/qe_bool_plugin.cpp rename to src/muz_qe/qe_bool_plugin.cpp diff --git a/lib/qe_bv_plugin.cpp b/src/muz_qe/qe_bv_plugin.cpp similarity index 100% rename from lib/qe_bv_plugin.cpp rename to src/muz_qe/qe_bv_plugin.cpp diff --git a/lib/qe_cmd.cpp b/src/muz_qe/qe_cmd.cpp similarity index 100% rename from lib/qe_cmd.cpp rename to src/muz_qe/qe_cmd.cpp diff --git a/lib/qe_cmd.h b/src/muz_qe/qe_cmd.h similarity index 100% rename from lib/qe_cmd.h rename to src/muz_qe/qe_cmd.h diff --git a/lib/qe_datatype_plugin.cpp b/src/muz_qe/qe_datatype_plugin.cpp similarity index 100% rename from lib/qe_datatype_plugin.cpp rename to src/muz_qe/qe_datatype_plugin.cpp diff --git a/lib/qe_dl_plugin.cpp b/src/muz_qe/qe_dl_plugin.cpp similarity index 100% rename from lib/qe_dl_plugin.cpp rename to src/muz_qe/qe_dl_plugin.cpp diff --git a/lib/qe_lite.cpp b/src/muz_qe/qe_lite.cpp similarity index 100% rename from lib/qe_lite.cpp rename to src/muz_qe/qe_lite.cpp diff --git a/lib/qe_lite.h b/src/muz_qe/qe_lite.h similarity index 100% rename from lib/qe_lite.h rename to src/muz_qe/qe_lite.h diff --git a/lib/qe_sat_tactic.cpp b/src/muz_qe/qe_sat_tactic.cpp similarity index 100% rename from lib/qe_sat_tactic.cpp rename to src/muz_qe/qe_sat_tactic.cpp diff --git a/lib/qe_sat_tactic.h b/src/muz_qe/qe_sat_tactic.h similarity index 100% rename from lib/qe_sat_tactic.h rename to src/muz_qe/qe_sat_tactic.h diff --git a/lib/qe_tactic.cpp b/src/muz_qe/qe_tactic.cpp similarity index 100% rename from lib/qe_tactic.cpp rename to src/muz_qe/qe_tactic.cpp diff --git a/lib/qe_tactic.h b/src/muz_qe/qe_tactic.h similarity index 100% rename from lib/qe_tactic.h rename to src/muz_qe/qe_tactic.h diff --git a/lib/replace_proof_converter.cpp b/src/muz_qe/replace_proof_converter.cpp similarity index 100% rename from lib/replace_proof_converter.cpp rename to src/muz_qe/replace_proof_converter.cpp diff --git a/lib/replace_proof_converter.h b/src/muz_qe/replace_proof_converter.h similarity index 100% rename from lib/replace_proof_converter.h rename to src/muz_qe/replace_proof_converter.h diff --git a/lib/unit_subsumption_tactic.cpp b/src/muz_qe/unit_subsumption_tactic.cpp similarity index 100% rename from lib/unit_subsumption_tactic.cpp rename to src/muz_qe/unit_subsumption_tactic.cpp diff --git a/lib/unit_subsumption_tactic.h b/src/muz_qe/unit_subsumption_tactic.h similarity index 100% rename from lib/unit_subsumption_tactic.h rename to src/muz_qe/unit_subsumption_tactic.h diff --git a/lib/elim_term_ite.cpp b/src/normal_forms/elim_term_ite.cpp similarity index 100% rename from lib/elim_term_ite.cpp rename to src/normal_forms/elim_term_ite.cpp diff --git a/lib/elim_term_ite.h b/src/normal_forms/elim_term_ite.h similarity index 100% rename from lib/elim_term_ite.h rename to src/normal_forms/elim_term_ite.h diff --git a/src/pattern/pattern_inference.cpp b/src/pattern/pattern_inference.cpp index 07e649905..79cf41a71 100644 --- a/src/pattern/pattern_inference.cpp +++ b/src/pattern/pattern_inference.cpp @@ -87,7 +87,7 @@ bool smaller_pattern::operator()(unsigned num_bindings, expr * p1, expr * p2) { return process(p1, p2); } -pattern_inference::pattern_inference(ast_manager & m, pattern_inference_params & params): +pattern_inference::pattern_inference(ast_manager & m, pattern_inference_params & params, pattern_database * db): simplifier(m), m_params(params), m_bfid(m.get_basic_family_id()), @@ -99,7 +99,7 @@ pattern_inference::pattern_inference(ast_manager & m, pattern_inference_params & m_pattern_weight_lt(m_candidates_info), m_collect(m, *this), m_contains_subpattern(*this), - m_database(m) { + m_database(db) { if (params.m_pi_arith == AP_NO) register_forbidden_family(m_afid); enable_ac_support(false); @@ -574,8 +574,6 @@ void pattern_inference::mk_patterns(unsigned num_bindings, m_candidates.reset(); } -#include"database.h" // defines g_pattern_database - void pattern_inference::reduce1_quantifier(quantifier * q) { TRACE("pattern_inference", tout << "processing:\n" << mk_pp(q, m_manager) << "\n";); if (!q->is_forall()) { @@ -585,11 +583,10 @@ void pattern_inference::reduce1_quantifier(quantifier * q) { int weight = q->get_weight(); - if (m_params.m_pi_use_database) { - m_database.initialize(g_pattern_database); + if (m_database) { app_ref_vector new_patterns(m_manager); unsigned new_weight; - if (m_database.match_quantifier(q, new_patterns, new_weight)) { + if (m_database->match_quantifier(q, new_patterns, new_weight)) { #ifdef Z3DEBUG for (unsigned i = 0; i < new_patterns.size(); i++) { SASSERT(is_well_sorted(m_manager, new_patterns.get(i))); } #endif diff --git a/src/pattern/pattern_inference.h b/src/pattern/pattern_inference.h index 057a74f76..c477b0228 100644 --- a/src/pattern/pattern_inference.h +++ b/src/pattern/pattern_inference.h @@ -28,7 +28,13 @@ Revision History: #include"obj_hashtable.h" #include"obj_pair_hashtable.h" #include"map.h" -#include"expr_pattern_match.h" + +class pattern_database { +public: + virtual ~pattern_database() {} + virtual void initialize(char const * smt_patterns) = 0; + virtual bool match_quantifier(quantifier * qf, app_ref_vector & patterns, unsigned & weight) = 0; +}; /** \brief A pattern p_1 is smaller than a pattern p_2 iff @@ -188,8 +194,8 @@ class pattern_inference : public simplifier { } }; - ptr_vector m_pre_patterns; - expr_pattern_match m_database; + ptr_vector m_pre_patterns; + pattern_database * m_database; void candidates2unary_patterns(ptr_vector const & candidate_patterns, ptr_vector & remaining_candidate_patterns, @@ -217,7 +223,7 @@ class pattern_inference : public simplifier { virtual void reduce1_quantifier(quantifier * q); public: - pattern_inference(ast_manager & m, pattern_inference_params & params); + pattern_inference(ast_manager & m, pattern_inference_params & params, pattern_database * db); void register_forbidden_family(family_id fid) { SASSERT(fid != m_bfid); diff --git a/lib/proof_checker.cpp b/src/proof_checker/proof_checker.cpp similarity index 100% rename from lib/proof_checker.cpp rename to src/proof_checker/proof_checker.cpp diff --git a/lib/proof_checker.h b/src/proof_checker/proof_checker.h similarity index 100% rename from lib/proof_checker.h rename to src/proof_checker/proof_checker.h diff --git a/lib/factor_rewriter.cpp b/src/rewriter/factor_rewriter.cpp similarity index 100% rename from lib/factor_rewriter.cpp rename to src/rewriter/factor_rewriter.cpp diff --git a/lib/factor_rewriter.h b/src/rewriter/factor_rewriter.h similarity index 100% rename from lib/factor_rewriter.h rename to src/rewriter/factor_rewriter.h diff --git a/lib/quant_hoist.cpp b/src/rewriter/quant_hoist.cpp similarity index 100% rename from lib/quant_hoist.cpp rename to src/rewriter/quant_hoist.cpp diff --git a/lib/quant_hoist.h b/src/rewriter/quant_hoist.h similarity index 100% rename from lib/quant_hoist.h rename to src/rewriter/quant_hoist.h diff --git a/src/sat_core/sat_types.h b/src/sat/sat_types.h similarity index 100% rename from src/sat_core/sat_types.h rename to src/sat/sat_types.h diff --git a/lib/assertion_set2sat.cpp b/src/sat_strategy/assertion_set2sat.cpp similarity index 90% rename from lib/assertion_set2sat.cpp rename to src/sat_strategy/assertion_set2sat.cpp index 11fc66228..b81c32e51 100644 --- a/lib/assertion_set2sat.cpp +++ b/src/sat_strategy/assertion_set2sat.cpp @@ -715,3 +715,77 @@ void sat2assertion_set::set_cancel(bool f) { m_imp->set_cancel(f); } } + +// HACK introduced during code reorg. +// NOTE: the whole file will be deleted. +struct collect_boolean_interface_proc2 { + struct visitor { + obj_hashtable & m_r; + visitor(obj_hashtable & r):m_r(r) {} + void operator()(var * n) {} + void operator()(app * n) { if (is_uninterp_const(n)) m_r.insert(n); } + void operator()(quantifier * n) {} + }; + + ast_manager & m; + expr_fast_mark2 fvisited; + expr_fast_mark1 tvisited; + ptr_vector todo; + visitor proc; + + collect_boolean_interface_proc2(ast_manager & _m, obj_hashtable & r): + m(_m), + proc(r) { + } + + void process(expr * f) { + if (fvisited.is_marked(f)) + return; + fvisited.mark(f); + todo.push_back(f); + while (!todo.empty()) { + expr * t = todo.back(); + todo.pop_back(); + if (is_uninterp_const(t)) + continue; + if (is_app(t) && to_app(t)->get_family_id() == m.get_basic_family_id() && to_app(t)->get_num_args() > 0) { + decl_kind k = to_app(t)->get_decl_kind(); + if (k == OP_OR || k == OP_NOT || k == OP_IFF || ((k == OP_EQ || k == OP_ITE) && m.is_bool(to_app(t)->get_arg(1)))) { + unsigned num = to_app(t)->get_num_args(); + for (unsigned i = 0; i < num; i++) { + expr * arg = to_app(t)->get_arg(i); + if (fvisited.is_marked(arg)) + continue; + fvisited.mark(arg); + todo.push_back(arg); + } + } + } + else { + quick_for_each_expr(proc, tvisited, t); + } + } + } + + template + void operator()(T const & g) { + unsigned sz = g.size(); + for (unsigned i = 0; i < sz; i++) + process(g.form(i)); + } + + void operator()(unsigned sz, expr * const * fs) { + for (unsigned i = 0; i < sz; i++) + process(fs[i]); + } +}; + +template +void collect_boolean_interface_core2(T const & s, obj_hashtable & r) { + collect_boolean_interface_proc2 proc(s.m(), r); + proc(s); +} + +void collect_boolean_interface(assertion_set const & s, obj_hashtable & r) { + collect_boolean_interface_core2(s, r); +} diff --git a/lib/assertion_set2sat.h b/src/sat_strategy/assertion_set2sat.h similarity index 96% rename from lib/assertion_set2sat.h rename to src/sat_strategy/assertion_set2sat.h index b58f6d647..8f90b1367 100644 --- a/lib/assertion_set2sat.h +++ b/src/sat_strategy/assertion_set2sat.h @@ -35,6 +35,9 @@ Notes: #include"model_converter.h" #include"atom2bool_var.h" +class assertion_set; // TODO: delete +void collect_boolean_interface(assertion_set const & s, obj_hashtable & r); + MK_ST_EXCEPTION(assertion_set2sat_exception); class assertion_set2sat { diff --git a/lib/sat_solver_strategy.cpp b/src/sat_strategy/sat_solver_strategy.cpp similarity index 100% rename from lib/sat_solver_strategy.cpp rename to src/sat_strategy/sat_solver_strategy.cpp diff --git a/lib/sat_solver_strategy.h b/src/sat_strategy/sat_solver_strategy.h similarity index 100% rename from lib/sat_solver_strategy.h rename to src/sat_strategy/sat_solver_strategy.h diff --git a/lib/atom2bool_var.cpp b/src/sat_tactic/atom2bool_var.cpp similarity index 95% rename from lib/atom2bool_var.cpp rename to src/sat_tactic/atom2bool_var.cpp index 8176fdb53..935eeb28e 100644 --- a/lib/atom2bool_var.cpp +++ b/src/sat_tactic/atom2bool_var.cpp @@ -19,7 +19,6 @@ Notes: #include"atom2bool_var.h" #include"ast_smt2_pp.h" #include"ref_util.h" -#include"assertion_set.h" // TODO delete #include"goal.h" void atom2bool_var::mk_inv(expr_ref_vector & lit2expr) const { @@ -107,10 +106,6 @@ void collect_boolean_interface_core(T const & s, obj_hashtable & r) { proc(s); } -void collect_boolean_interface(assertion_set const & s, obj_hashtable & r) { - collect_boolean_interface_core(s, r); -} - void collect_boolean_interface(goal const & g, obj_hashtable & r) { collect_boolean_interface_core(g, r); } diff --git a/lib/atom2bool_var.h b/src/sat_tactic/atom2bool_var.h similarity index 87% rename from lib/atom2bool_var.h rename to src/sat_tactic/atom2bool_var.h index 8dbff5ea4..4d6ce79e0 100644 --- a/lib/atom2bool_var.h +++ b/src/sat_tactic/atom2bool_var.h @@ -35,10 +35,8 @@ public: bool interpreted_atoms() const { return expr2var::interpreted_vars(); } }; -class assertion_set; // TODO: delete class goal; -void collect_boolean_interface(assertion_set const & s, obj_hashtable & r); // TODO delete void collect_boolean_interface(goal const & g, obj_hashtable & r); void collect_boolean_interface(ast_manager & m, unsigned num, expr * const * fs, obj_hashtable & r); diff --git a/lib/goal2sat.cpp b/src/sat_tactic/goal2sat.cpp similarity index 100% rename from lib/goal2sat.cpp rename to src/sat_tactic/goal2sat.cpp diff --git a/lib/goal2sat.h b/src/sat_tactic/goal2sat.h similarity index 100% rename from lib/goal2sat.h rename to src/sat_tactic/goal2sat.h diff --git a/lib/sat_tactic.cpp b/src/sat_tactic/sat_tactic.cpp similarity index 100% rename from lib/sat_tactic.cpp rename to src/sat_tactic/sat_tactic.cpp diff --git a/lib/sat_tactic.h b/src/sat_tactic/sat_tactic.h similarity index 100% rename from lib/sat_tactic.h rename to src/sat_tactic/sat_tactic.h diff --git a/src/old_params/arith_simplifier_params.cpp b/src/simplifier/arith_simplifier_params.cpp similarity index 100% rename from src/old_params/arith_simplifier_params.cpp rename to src/simplifier/arith_simplifier_params.cpp diff --git a/src/old_params/arith_simplifier_params.h b/src/simplifier/arith_simplifier_params.h similarity index 100% rename from src/old_params/arith_simplifier_params.h rename to src/simplifier/arith_simplifier_params.h diff --git a/lib/bit2int.cpp b/src/simplifier/bit2int.cpp similarity index 100% rename from lib/bit2int.cpp rename to src/simplifier/bit2int.cpp diff --git a/lib/bit2int.h b/src/simplifier/bit2int.h similarity index 100% rename from lib/bit2int.h rename to src/simplifier/bit2int.h diff --git a/lib/bv_elim.cpp b/src/simplifier/bv_elim.cpp similarity index 100% rename from lib/bv_elim.cpp rename to src/simplifier/bv_elim.cpp diff --git a/lib/bv_elim.h b/src/simplifier/bv_elim.h similarity index 100% rename from lib/bv_elim.h rename to src/simplifier/bv_elim.h diff --git a/src/old_params/bv_simplifier_params.h b/src/simplifier/bv_simplifier_params.h similarity index 100% rename from src/old_params/bv_simplifier_params.h rename to src/simplifier/bv_simplifier_params.h diff --git a/lib/distribute_forall.cpp b/src/simplifier/distribute_forall.cpp similarity index 100% rename from lib/distribute_forall.cpp rename to src/simplifier/distribute_forall.cpp diff --git a/lib/distribute_forall.h b/src/simplifier/distribute_forall.h similarity index 100% rename from lib/distribute_forall.h rename to src/simplifier/distribute_forall.h diff --git a/lib/elim_bounds.cpp b/src/simplifier/elim_bounds.cpp similarity index 100% rename from lib/elim_bounds.cpp rename to src/simplifier/elim_bounds.cpp diff --git a/lib/elim_bounds.h b/src/simplifier/elim_bounds.h similarity index 100% rename from lib/elim_bounds.h rename to src/simplifier/elim_bounds.h diff --git a/lib/inj_axiom.cpp b/src/simplifier/inj_axiom.cpp similarity index 100% rename from lib/inj_axiom.cpp rename to src/simplifier/inj_axiom.cpp diff --git a/lib/inj_axiom.h b/src/simplifier/inj_axiom.h similarity index 100% rename from lib/inj_axiom.h rename to src/simplifier/inj_axiom.h diff --git a/lib/maximise_ac_sharing.cpp b/src/simplifier/maximise_ac_sharing.cpp similarity index 100% rename from lib/maximise_ac_sharing.cpp rename to src/simplifier/maximise_ac_sharing.cpp diff --git a/lib/maximise_ac_sharing.h b/src/simplifier/maximise_ac_sharing.h similarity index 100% rename from lib/maximise_ac_sharing.h rename to src/simplifier/maximise_ac_sharing.h diff --git a/lib/pull_ite_tree.cpp b/src/simplifier/pull_ite_tree.cpp similarity index 100% rename from lib/pull_ite_tree.cpp rename to src/simplifier/pull_ite_tree.cpp diff --git a/lib/pull_ite_tree.h b/src/simplifier/pull_ite_tree.h similarity index 100% rename from lib/pull_ite_tree.h rename to src/simplifier/pull_ite_tree.h diff --git a/src/old_params/theory_array_params.h b/src/simplifier/theory_array_params.h similarity index 100% rename from src/old_params/theory_array_params.h rename to src/simplifier/theory_array_params.h diff --git a/lib/arith_eq_adapter.cpp b/src/smt/arith_eq_adapter.cpp similarity index 100% rename from lib/arith_eq_adapter.cpp rename to src/smt/arith_eq_adapter.cpp diff --git a/lib/arith_eq_adapter.h b/src/smt/arith_eq_adapter.h similarity index 100% rename from lib/arith_eq_adapter.h rename to src/smt/arith_eq_adapter.h diff --git a/lib/arith_eq_solver.cpp b/src/smt/arith_eq_solver.cpp similarity index 100% rename from lib/arith_eq_solver.cpp rename to src/smt/arith_eq_solver.cpp diff --git a/lib/arith_eq_solver.h b/src/smt/arith_eq_solver.h similarity index 100% rename from lib/arith_eq_solver.h rename to src/smt/arith_eq_solver.h diff --git a/lib/arith_solver_plugin.cpp b/src/smt/arith_solver_plugin.cpp similarity index 100% rename from lib/arith_solver_plugin.cpp rename to src/smt/arith_solver_plugin.cpp diff --git a/lib/arith_solver_plugin.h b/src/smt/arith_solver_plugin.h similarity index 100% rename from lib/arith_solver_plugin.h rename to src/smt/arith_solver_plugin.h diff --git a/lib/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp similarity index 99% rename from lib/asserted_formulas.cpp rename to src/smt/asserted_formulas.cpp index 6f7d8827e..f5d9c4891 100644 --- a/lib/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -42,7 +42,7 @@ Revision History: #include"warning.h" #include"eager_bit_blaster.h" #include"bit2int.h" -#include"qe.h" +// #include"qe.h" #include"distribute_forall.h" #include"demodulator.h" #include"quasi_macros.h" @@ -64,7 +64,6 @@ asserted_formulas::asserted_formulas(ast_manager & m, front_end_params & p): m_bv_sharing(m), m_user_rewriter(m), m_inconsistent(false), - m_quant_elim(m, p), m_cancel_flag(false) { m_bsimp = 0; @@ -574,10 +573,9 @@ void asserted_formulas::display_ll(std::ostream & out, ast_mark & pp_visited) co } void asserted_formulas::collect_statistics(statistics & st) const { - m_quant_elim.collect_statistics(st); + // m_quant_elim.collect_statistics(st); } - /** \brief Functor used to order solved equations x = t, in a way they can be solved efficiently. @@ -1107,7 +1105,7 @@ void asserted_formulas::reduce_and_solve() { void asserted_formulas::infer_patterns() { IF_IVERBOSE(10, verbose_stream() << "pattern inference...\n";); TRACE("before_pattern_inference", display(tout);); - pattern_inference infer(m_manager, m_params); + pattern_inference infer(m_manager, m_params, m_database.get()); expr_ref_vector new_exprs(m_manager); proof_ref_vector new_prs(m_manager); unsigned i = m_asserted_qhead; @@ -1433,8 +1431,13 @@ void asserted_formulas::apply_der() { MK_SIMPLIFIER(cheap_quant_fourier_motzkin, elim_bounds_star functor(m_manager), "elim_bounds", "cheap fourier-motzkin", true); -MK_SIMPLIFIER(quant_elim, qe::expr_quant_elim_star1 &functor = m_quant_elim, - "quantifiers", "quantifier elimination procedures", true); +// MK_SIMPLIFIER(quant_elim, qe::expr_quant_elim_star1 &functor = m_quant_elim, +// "quantifiers", "quantifier elimination procedures", true); + +bool asserted_formulas::quant_elim() { + throw default_exception("QUANT_ELIM option is deprecated, please consider using the 'qe' tactic."); + return false; +} MK_SIMPLIFIER(apply_eager_bit_blaster, eager_bit_blaster functor(m_manager, m_params), "eager_bb", "eager bit blasting", false); diff --git a/lib/asserted_formulas.h b/src/smt/asserted_formulas.h similarity index 89% rename from lib/asserted_formulas.h rename to src/smt/asserted_formulas.h index 6ea0e793b..a89385958 100644 --- a/lib/asserted_formulas.h +++ b/src/smt/asserted_formulas.h @@ -29,25 +29,27 @@ Revision History: #include"solver_plugin.h" #include"maximise_ac_sharing.h" #include"bit2int.h" -#include"qe.h" +// #include"qe.h" #include"statistics.h" #include"user_rewriter.h" +#include"pattern_inference.h" class arith_simplifier_plugin; class bv_simplifier_plugin; class asserted_formulas { - ast_manager & m_manager; - front_end_params & m_params; - simplifier m_pre_simplifier; - subst_simplifier m_simplifier; - basic_simplifier_plugin * m_bsimp; - bv_simplifier_plugin * m_bvsimp; - defined_names m_defined_names; - static_features m_static_features; - expr_ref_vector m_asserted_formulas; // formulas asserted by user - proof_ref_vector m_asserted_formula_prs; // proofs for the asserted formulas. - unsigned m_asserted_qhead; + ast_manager & m_manager; + front_end_params & m_params; + scoped_ptr m_database; + simplifier m_pre_simplifier; + subst_simplifier m_simplifier; + basic_simplifier_plugin * m_bsimp; + bv_simplifier_plugin * m_bvsimp; + defined_names m_defined_names; + static_features m_static_features; + expr_ref_vector m_asserted_formulas; // formulas asserted by user + proof_ref_vector m_asserted_formula_prs; // proofs for the asserted formulas. + unsigned m_asserted_qhead; expr_map m_subst; ptr_vector m_vars; // domain of m_subst @@ -69,7 +71,7 @@ class asserted_formulas { user_rewriter m_user_rewriter; bool m_inconsistent; - qe::expr_quant_elim_star1 m_quant_elim; + // qe::expr_quant_elim_star1 m_quant_elim; struct scope { unsigned m_asserted_formulas_lim; @@ -166,6 +168,8 @@ public: void collect_statistics(statistics & st) const; // TODO: improve precision of the following method. bool has_quantifiers() const { return m_simplifier.visited_quantifier(); /* approximation */ } + + void set_pattern_database(pattern_database * db) { m_database = db; } // ----------------------------------- // diff --git a/lib/cached_var_subst.cpp b/src/smt/cached_var_subst.cpp similarity index 100% rename from lib/cached_var_subst.cpp rename to src/smt/cached_var_subst.cpp diff --git a/lib/cached_var_subst.h b/src/smt/cached_var_subst.h similarity index 100% rename from lib/cached_var_subst.h rename to src/smt/cached_var_subst.h diff --git a/lib/cost_evaluator.cpp b/src/smt/cost_evaluator.cpp similarity index 100% rename from lib/cost_evaluator.cpp rename to src/smt/cost_evaluator.cpp diff --git a/lib/cost_evaluator.h b/src/smt/cost_evaluator.h similarity index 100% rename from lib/cost_evaluator.h rename to src/smt/cost_evaluator.h diff --git a/src/pattern/database.h b/src/smt/database.h similarity index 100% rename from src/pattern/database.h rename to src/smt/database.h diff --git a/src/pattern/database.smt b/src/smt/database.smt similarity index 100% rename from src/pattern/database.smt rename to src/smt/database.smt diff --git a/lib/demodulator.cpp b/src/smt/demodulator.cpp similarity index 100% rename from lib/demodulator.cpp rename to src/smt/demodulator.cpp diff --git a/lib/demodulator.h b/src/smt/demodulator.h similarity index 100% rename from lib/demodulator.h rename to src/smt/demodulator.h diff --git a/lib/dyn_ack.cpp b/src/smt/dyn_ack.cpp similarity index 100% rename from lib/dyn_ack.cpp rename to src/smt/dyn_ack.cpp diff --git a/lib/dyn_ack.h b/src/smt/dyn_ack.h similarity index 100% rename from lib/dyn_ack.h rename to src/smt/dyn_ack.h diff --git a/lib/expr_context_simplifier.cpp b/src/smt/expr_context_simplifier.cpp similarity index 100% rename from lib/expr_context_simplifier.cpp rename to src/smt/expr_context_simplifier.cpp diff --git a/lib/expr_context_simplifier.h b/src/smt/expr_context_simplifier.h similarity index 100% rename from lib/expr_context_simplifier.h rename to src/smt/expr_context_simplifier.h diff --git a/lib/fingerprints.cpp b/src/smt/fingerprints.cpp similarity index 100% rename from lib/fingerprints.cpp rename to src/smt/fingerprints.cpp diff --git a/lib/fingerprints.h b/src/smt/fingerprints.h similarity index 100% rename from lib/fingerprints.h rename to src/smt/fingerprints.h diff --git a/lib/mam.cpp b/src/smt/mam.cpp similarity index 100% rename from lib/mam.cpp rename to src/smt/mam.cpp diff --git a/lib/mam.h b/src/smt/mam.h similarity index 100% rename from lib/mam.h rename to src/smt/mam.h diff --git a/lib/qi_queue.cpp b/src/smt/qi_queue.cpp similarity index 100% rename from lib/qi_queue.cpp rename to src/smt/qi_queue.cpp diff --git a/lib/qi_queue.h b/src/smt/qi_queue.h similarity index 100% rename from lib/qi_queue.h rename to src/smt/qi_queue.h diff --git a/lib/smt_almost_cg_table.cpp b/src/smt/smt_almost_cg_table.cpp similarity index 100% rename from lib/smt_almost_cg_table.cpp rename to src/smt/smt_almost_cg_table.cpp diff --git a/lib/smt_almost_cg_table.h b/src/smt/smt_almost_cg_table.h similarity index 100% rename from lib/smt_almost_cg_table.h rename to src/smt/smt_almost_cg_table.h diff --git a/lib/smt_b_justification.h b/src/smt/smt_b_justification.h similarity index 100% rename from lib/smt_b_justification.h rename to src/smt/smt_b_justification.h diff --git a/lib/smt_bool_var_data.h b/src/smt/smt_bool_var_data.h similarity index 100% rename from lib/smt_bool_var_data.h rename to src/smt/smt_bool_var_data.h diff --git a/lib/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp similarity index 100% rename from lib/smt_case_split_queue.cpp rename to src/smt/smt_case_split_queue.cpp diff --git a/lib/smt_case_split_queue.h b/src/smt/smt_case_split_queue.h similarity index 100% rename from lib/smt_case_split_queue.h rename to src/smt/smt_case_split_queue.h diff --git a/lib/smt_cg_table.cpp b/src/smt/smt_cg_table.cpp similarity index 100% rename from lib/smt_cg_table.cpp rename to src/smt/smt_cg_table.cpp diff --git a/lib/smt_cg_table.h b/src/smt/smt_cg_table.h similarity index 100% rename from lib/smt_cg_table.h rename to src/smt/smt_cg_table.h diff --git a/lib/smt_checker.cpp b/src/smt/smt_checker.cpp similarity index 100% rename from lib/smt_checker.cpp rename to src/smt/smt_checker.cpp diff --git a/lib/smt_checker.h b/src/smt/smt_checker.h similarity index 100% rename from lib/smt_checker.h rename to src/smt/smt_checker.h diff --git a/lib/smt_clause.cpp b/src/smt/smt_clause.cpp similarity index 100% rename from lib/smt_clause.cpp rename to src/smt/smt_clause.cpp diff --git a/lib/smt_clause.h b/src/smt/smt_clause.h similarity index 100% rename from lib/smt_clause.h rename to src/smt/smt_clause.h diff --git a/lib/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp similarity index 100% rename from lib/smt_conflict_resolution.cpp rename to src/smt/smt_conflict_resolution.cpp diff --git a/lib/smt_conflict_resolution.h b/src/smt/smt_conflict_resolution.h similarity index 100% rename from lib/smt_conflict_resolution.h rename to src/smt/smt_conflict_resolution.h diff --git a/lib/smt_context.cpp b/src/smt/smt_context.cpp similarity index 100% rename from lib/smt_context.cpp rename to src/smt/smt_context.cpp diff --git a/lib/smt_context.h b/src/smt/smt_context.h similarity index 100% rename from lib/smt_context.h rename to src/smt/smt_context.h diff --git a/lib/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp similarity index 100% rename from lib/smt_context_inv.cpp rename to src/smt/smt_context_inv.cpp diff --git a/lib/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp similarity index 100% rename from lib/smt_context_pp.cpp rename to src/smt/smt_context_pp.cpp diff --git a/lib/smt_context_stat.cpp b/src/smt/smt_context_stat.cpp similarity index 100% rename from lib/smt_context_stat.cpp rename to src/smt/smt_context_stat.cpp diff --git a/lib/smt_enode.cpp b/src/smt/smt_enode.cpp similarity index 100% rename from lib/smt_enode.cpp rename to src/smt/smt_enode.cpp diff --git a/lib/smt_enode.h b/src/smt/smt_enode.h similarity index 100% rename from lib/smt_enode.h rename to src/smt/smt_enode.h diff --git a/lib/smt_eq_justification.h b/src/smt/smt_eq_justification.h similarity index 100% rename from lib/smt_eq_justification.h rename to src/smt/smt_eq_justification.h diff --git a/lib/smt_failure.h b/src/smt/smt_failure.h similarity index 100% rename from lib/smt_failure.h rename to src/smt/smt_failure.h diff --git a/lib/smt_for_each_relevant_expr.cpp b/src/smt/smt_for_each_relevant_expr.cpp similarity index 100% rename from lib/smt_for_each_relevant_expr.cpp rename to src/smt/smt_for_each_relevant_expr.cpp diff --git a/lib/smt_for_each_relevant_expr.h b/src/smt/smt_for_each_relevant_expr.h similarity index 100% rename from lib/smt_for_each_relevant_expr.h rename to src/smt/smt_for_each_relevant_expr.h diff --git a/lib/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp similarity index 100% rename from lib/smt_internalizer.cpp rename to src/smt/smt_internalizer.cpp diff --git a/lib/smt_justification.cpp b/src/smt/smt_justification.cpp similarity index 100% rename from lib/smt_justification.cpp rename to src/smt/smt_justification.cpp diff --git a/lib/smt_justification.h b/src/smt/smt_justification.h similarity index 100% rename from lib/smt_justification.h rename to src/smt/smt_justification.h diff --git a/lib/smt_literal.cpp b/src/smt/smt_literal.cpp similarity index 100% rename from lib/smt_literal.cpp rename to src/smt/smt_literal.cpp diff --git a/lib/smt_literal.h b/src/smt/smt_literal.h similarity index 100% rename from lib/smt_literal.h rename to src/smt/smt_literal.h diff --git a/lib/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp similarity index 100% rename from lib/smt_model_checker.cpp rename to src/smt/smt_model_checker.cpp diff --git a/lib/smt_model_checker.h b/src/smt/smt_model_checker.h similarity index 100% rename from lib/smt_model_checker.h rename to src/smt/smt_model_checker.h diff --git a/lib/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp similarity index 100% rename from lib/smt_model_finder.cpp rename to src/smt/smt_model_finder.cpp diff --git a/lib/smt_model_finder.h b/src/smt/smt_model_finder.h similarity index 100% rename from lib/smt_model_finder.h rename to src/smt/smt_model_finder.h diff --git a/lib/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp similarity index 100% rename from lib/smt_model_generator.cpp rename to src/smt/smt_model_generator.cpp diff --git a/lib/smt_model_generator.h b/src/smt/smt_model_generator.h similarity index 100% rename from lib/smt_model_generator.h rename to src/smt/smt_model_generator.h diff --git a/lib/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp similarity index 100% rename from lib/smt_quantifier.cpp rename to src/smt/smt_quantifier.cpp diff --git a/lib/smt_quantifier.h b/src/smt/smt_quantifier.h similarity index 100% rename from lib/smt_quantifier.h rename to src/smt/smt_quantifier.h diff --git a/lib/smt_quantifier_instances.h b/src/smt/smt_quantifier_instances.h similarity index 100% rename from lib/smt_quantifier_instances.h rename to src/smt/smt_quantifier_instances.h diff --git a/lib/smt_quantifier_stat.cpp b/src/smt/smt_quantifier_stat.cpp similarity index 100% rename from lib/smt_quantifier_stat.cpp rename to src/smt/smt_quantifier_stat.cpp diff --git a/lib/smt_quantifier_stat.h b/src/smt/smt_quantifier_stat.h similarity index 100% rename from lib/smt_quantifier_stat.h rename to src/smt/smt_quantifier_stat.h diff --git a/lib/smt_quick_checker.cpp b/src/smt/smt_quick_checker.cpp similarity index 100% rename from lib/smt_quick_checker.cpp rename to src/smt/smt_quick_checker.cpp diff --git a/lib/smt_quick_checker.h b/src/smt/smt_quick_checker.h similarity index 100% rename from lib/smt_quick_checker.h rename to src/smt/smt_quick_checker.h diff --git a/lib/smt_relevancy.cpp b/src/smt/smt_relevancy.cpp similarity index 100% rename from lib/smt_relevancy.cpp rename to src/smt/smt_relevancy.cpp diff --git a/lib/smt_relevancy.h b/src/smt/smt_relevancy.h similarity index 100% rename from lib/smt_relevancy.h rename to src/smt/smt_relevancy.h diff --git a/lib/smt_setup.cpp b/src/smt/smt_setup.cpp similarity index 100% rename from lib/smt_setup.cpp rename to src/smt/smt_setup.cpp diff --git a/lib/smt_setup.h b/src/smt/smt_setup.h similarity index 100% rename from lib/smt_setup.h rename to src/smt/smt_setup.h diff --git a/src/smt/smt_solver_strategy.cpp b/src/smt/smt_solver_strategy.cpp index 65dde6361..a7cd8a6b8 100644 --- a/src/smt/smt_solver_strategy.cpp +++ b/src/smt/smt_solver_strategy.cpp @@ -20,6 +20,8 @@ Notes: --*/ #include"smt_solver_strategy.h" #include"smt_solver.h" +#include"front_end_params.h" +#include"params2front_end_params.h" class as_st_solver : public assertion_set_strategy { scoped_ptr m_params; diff --git a/lib/smt_statistics.cpp b/src/smt/smt_statistics.cpp similarity index 100% rename from lib/smt_statistics.cpp rename to src/smt/smt_statistics.cpp diff --git a/lib/smt_statistics.h b/src/smt/smt_statistics.h similarity index 100% rename from lib/smt_statistics.h rename to src/smt/smt_statistics.h diff --git a/lib/smt_theory.cpp b/src/smt/smt_theory.cpp similarity index 100% rename from lib/smt_theory.cpp rename to src/smt/smt_theory.cpp diff --git a/lib/smt_theory.h b/src/smt/smt_theory.h similarity index 100% rename from lib/smt_theory.h rename to src/smt/smt_theory.h diff --git a/lib/smt_theory_var_list.h b/src/smt/smt_theory_var_list.h similarity index 100% rename from lib/smt_theory_var_list.h rename to src/smt/smt_theory_var_list.h diff --git a/lib/smt_types.h b/src/smt/smt_types.h similarity index 100% rename from lib/smt_types.h rename to src/smt/smt_types.h diff --git a/lib/solver_plugin.h b/src/smt/solver_plugin.h similarity index 100% rename from lib/solver_plugin.h rename to src/smt/solver_plugin.h diff --git a/lib/theory_arith.cpp b/src/smt/theory_arith.cpp similarity index 100% rename from lib/theory_arith.cpp rename to src/smt/theory_arith.cpp diff --git a/lib/theory_arith.h b/src/smt/theory_arith.h similarity index 100% rename from lib/theory_arith.h rename to src/smt/theory_arith.h diff --git a/lib/theory_arith_aux.h b/src/smt/theory_arith_aux.h similarity index 100% rename from lib/theory_arith_aux.h rename to src/smt/theory_arith_aux.h diff --git a/lib/theory_arith_core.h b/src/smt/theory_arith_core.h similarity index 100% rename from lib/theory_arith_core.h rename to src/smt/theory_arith_core.h diff --git a/lib/theory_arith_def.h b/src/smt/theory_arith_def.h similarity index 100% rename from lib/theory_arith_def.h rename to src/smt/theory_arith_def.h diff --git a/lib/theory_arith_eq.h b/src/smt/theory_arith_eq.h similarity index 100% rename from lib/theory_arith_eq.h rename to src/smt/theory_arith_eq.h diff --git a/lib/theory_arith_int.h b/src/smt/theory_arith_int.h similarity index 100% rename from lib/theory_arith_int.h rename to src/smt/theory_arith_int.h diff --git a/lib/theory_arith_inv.h b/src/smt/theory_arith_inv.h similarity index 100% rename from lib/theory_arith_inv.h rename to src/smt/theory_arith_inv.h diff --git a/lib/theory_arith_nl.h b/src/smt/theory_arith_nl.h similarity index 100% rename from lib/theory_arith_nl.h rename to src/smt/theory_arith_nl.h diff --git a/lib/theory_arith_pp.h b/src/smt/theory_arith_pp.h similarity index 100% rename from lib/theory_arith_pp.h rename to src/smt/theory_arith_pp.h diff --git a/lib/theory_array.cpp b/src/smt/theory_array.cpp similarity index 100% rename from lib/theory_array.cpp rename to src/smt/theory_array.cpp diff --git a/lib/theory_array.h b/src/smt/theory_array.h similarity index 100% rename from lib/theory_array.h rename to src/smt/theory_array.h diff --git a/lib/theory_array_base.cpp b/src/smt/theory_array_base.cpp similarity index 100% rename from lib/theory_array_base.cpp rename to src/smt/theory_array_base.cpp diff --git a/lib/theory_array_base.h b/src/smt/theory_array_base.h similarity index 100% rename from lib/theory_array_base.h rename to src/smt/theory_array_base.h diff --git a/lib/theory_array_full.cpp b/src/smt/theory_array_full.cpp similarity index 100% rename from lib/theory_array_full.cpp rename to src/smt/theory_array_full.cpp diff --git a/lib/theory_array_full.h b/src/smt/theory_array_full.h similarity index 100% rename from lib/theory_array_full.h rename to src/smt/theory_array_full.h diff --git a/lib/theory_bv.cpp b/src/smt/theory_bv.cpp similarity index 100% rename from lib/theory_bv.cpp rename to src/smt/theory_bv.cpp diff --git a/lib/theory_bv.h b/src/smt/theory_bv.h similarity index 100% rename from lib/theory_bv.h rename to src/smt/theory_bv.h diff --git a/lib/theory_datatype.cpp b/src/smt/theory_datatype.cpp similarity index 100% rename from lib/theory_datatype.cpp rename to src/smt/theory_datatype.cpp diff --git a/lib/theory_datatype.h b/src/smt/theory_datatype.h similarity index 100% rename from lib/theory_datatype.h rename to src/smt/theory_datatype.h diff --git a/lib/theory_dense_diff_logic.cpp b/src/smt/theory_dense_diff_logic.cpp similarity index 100% rename from lib/theory_dense_diff_logic.cpp rename to src/smt/theory_dense_diff_logic.cpp diff --git a/lib/theory_dense_diff_logic.h b/src/smt/theory_dense_diff_logic.h similarity index 100% rename from lib/theory_dense_diff_logic.h rename to src/smt/theory_dense_diff_logic.h diff --git a/lib/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h similarity index 100% rename from lib/theory_dense_diff_logic_def.h rename to src/smt/theory_dense_diff_logic_def.h diff --git a/lib/theory_diff_logic.cpp b/src/smt/theory_diff_logic.cpp similarity index 100% rename from lib/theory_diff_logic.cpp rename to src/smt/theory_diff_logic.cpp diff --git a/lib/theory_diff_logic.h b/src/smt/theory_diff_logic.h similarity index 100% rename from lib/theory_diff_logic.h rename to src/smt/theory_diff_logic.h diff --git a/lib/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h similarity index 100% rename from lib/theory_diff_logic_def.h rename to src/smt/theory_diff_logic_def.h diff --git a/lib/theory_dl.cpp b/src/smt/theory_dl.cpp similarity index 100% rename from lib/theory_dl.cpp rename to src/smt/theory_dl.cpp diff --git a/lib/theory_dl.h b/src/smt/theory_dl.h similarity index 100% rename from lib/theory_dl.h rename to src/smt/theory_dl.h diff --git a/lib/theory_dummy.cpp b/src/smt/theory_dummy.cpp similarity index 100% rename from lib/theory_dummy.cpp rename to src/smt/theory_dummy.cpp diff --git a/lib/theory_dummy.h b/src/smt/theory_dummy.h similarity index 100% rename from lib/theory_dummy.h rename to src/smt/theory_dummy.h diff --git a/lib/theory_instgen.cpp b/src/smt/theory_instgen.cpp similarity index 100% rename from lib/theory_instgen.cpp rename to src/smt/theory_instgen.cpp diff --git a/lib/theory_instgen.h b/src/smt/theory_instgen.h similarity index 100% rename from lib/theory_instgen.h rename to src/smt/theory_instgen.h diff --git a/lib/theory_seq_empty.h b/src/smt/theory_seq_empty.h similarity index 100% rename from lib/theory_seq_empty.h rename to src/smt/theory_seq_empty.h diff --git a/lib/user_rewriter.cpp b/src/smt/user_rewriter.cpp similarity index 100% rename from lib/user_rewriter.cpp rename to src/smt/user_rewriter.cpp diff --git a/lib/user_rewriter.h b/src/smt/user_rewriter.h similarity index 100% rename from lib/user_rewriter.h rename to src/smt/user_rewriter.h diff --git a/lib/uses_theory.cpp b/src/smt/uses_theory.cpp similarity index 100% rename from lib/uses_theory.cpp rename to src/smt/uses_theory.cpp diff --git a/lib/uses_theory.h b/src/smt/uses_theory.h similarity index 100% rename from lib/uses_theory.h rename to src/smt/uses_theory.h diff --git a/lib/watch_list.cpp b/src/smt/watch_list.cpp similarity index 100% rename from lib/watch_list.cpp rename to src/smt/watch_list.cpp diff --git a/lib/watch_list.h b/src/smt/watch_list.h similarity index 100% rename from lib/watch_list.h rename to src/smt/watch_list.h diff --git a/src/pattern/expr_pattern_match.cpp b/src/smtparser/expr_pattern_match.cpp similarity index 100% rename from src/pattern/expr_pattern_match.cpp rename to src/smtparser/expr_pattern_match.cpp diff --git a/src/pattern/expr_pattern_match.h b/src/smtparser/expr_pattern_match.h similarity index 94% rename from src/pattern/expr_pattern_match.h rename to src/smtparser/expr_pattern_match.h index eb3c05a94..f0075b1ba 100644 --- a/src/pattern/expr_pattern_match.h +++ b/src/smtparser/expr_pattern_match.h @@ -23,8 +23,9 @@ Notes: #include"ast.h" #include"map.h" #include"front_end_params.h" +#include"pattern_inference.h" -class expr_pattern_match { +class expr_pattern_match : public pattern_database { enum instr_kind { BACKTRACK, @@ -132,8 +133,8 @@ class expr_pattern_match { public: expr_pattern_match(ast_manager & manager); ~expr_pattern_match(); - bool match_quantifier(quantifier* qf, app_ref_vector& patterns, unsigned& weight); - void initialize(char const * database); + virtual bool match_quantifier(quantifier * qf, app_ref_vector & patterns, unsigned & weight); + virtual void initialize(char const * database); void display(std::ostream& out) const; private: diff --git a/lib/smtlib.cpp b/src/smtparser/smtlib.cpp similarity index 100% rename from lib/smtlib.cpp rename to src/smtparser/smtlib.cpp diff --git a/lib/smtlib.h b/src/smtparser/smtlib.h similarity index 100% rename from lib/smtlib.h rename to src/smtparser/smtlib.h diff --git a/lib/smtlib_solver.cpp b/src/smtparser/smtlib_solver.cpp similarity index 99% rename from lib/smtlib_solver.cpp rename to src/smtparser/smtlib_solver.cpp index f9ec045ce..ca5fa5555 100644 --- a/lib/smtlib_solver.cpp +++ b/src/smtparser/smtlib_solver.cpp @@ -26,7 +26,7 @@ Revision History: #include"spc_prover.h" #include"model.h" #include"model_v2_pp.h" -#include"expr2dot.h" +// #include"expr2dot.h" #include"solver.h" #include"smt_strategic_solver.h" #include"cmd_context.h" diff --git a/lib/smtlib_solver.h b/src/smtparser/smtlib_solver.h similarity index 100% rename from lib/smtlib_solver.h rename to src/smtparser/smtlib_solver.h diff --git a/lib/smtparser.cpp b/src/smtparser/smtparser.cpp similarity index 99% rename from lib/smtparser.cpp rename to src/smtparser/smtparser.cpp index 216f34b5b..e60ecb3e2 100644 --- a/lib/smtparser.cpp +++ b/src/smtparser/smtparser.cpp @@ -45,9 +45,9 @@ Revision History: #include"well_sorted.h" #include "str_hashtable.h" #include "front_end_params.h" -#include "z3_private.h" +// #include "z3_private.h" #include "stopwatch.h" -#include "dl_rule.h" +// #include "dl_rule.h" // private method defined in z3.cpp: front_end_params& Z3_API Z3_get_parameters(__in Z3_context c); diff --git a/lib/smtparser.h b/src/smtparser/smtparser.h similarity index 100% rename from lib/smtparser.h rename to src/smtparser/smtparser.h diff --git a/src/spc/expr_offset.h b/src/substitution/expr_offset.h similarity index 100% rename from src/spc/expr_offset.h rename to src/substitution/expr_offset.h diff --git a/src/spc/expr_offset_map.h b/src/substitution/expr_offset_map.h similarity index 100% rename from src/spc/expr_offset_map.h rename to src/substitution/expr_offset_map.h diff --git a/src/spc/matcher.cpp b/src/substitution/matcher.cpp similarity index 100% rename from src/spc/matcher.cpp rename to src/substitution/matcher.cpp diff --git a/src/spc/matcher.h b/src/substitution/matcher.h similarity index 100% rename from src/spc/matcher.h rename to src/substitution/matcher.h diff --git a/src/spc/substitution.cpp b/src/substitution/substitution.cpp similarity index 100% rename from src/spc/substitution.cpp rename to src/substitution/substitution.cpp diff --git a/src/spc/substitution.h b/src/substitution/substitution.h similarity index 100% rename from src/spc/substitution.h rename to src/substitution/substitution.h diff --git a/src/spc/substitution_tree.cpp b/src/substitution/substitution_tree.cpp similarity index 100% rename from src/spc/substitution_tree.cpp rename to src/substitution/substitution_tree.cpp diff --git a/src/spc/substitution_tree.h b/src/substitution/substitution_tree.h similarity index 100% rename from src/spc/substitution_tree.h rename to src/substitution/substitution_tree.h diff --git a/src/spc/unifier.cpp b/src/substitution/unifier.cpp similarity index 100% rename from src/spc/unifier.cpp rename to src/substitution/unifier.cpp diff --git a/src/spc/unifier.h b/src/substitution/unifier.h similarity index 100% rename from src/spc/unifier.h rename to src/substitution/unifier.h diff --git a/src/spc/var_offset_map.h b/src/substitution/var_offset_map.h similarity index 100% rename from src/spc/var_offset_map.h rename to src/substitution/var_offset_map.h diff --git a/lib/diff_logic.h b/src/util/diff_logic.h similarity index 100% rename from lib/diff_logic.h rename to src/util/diff_logic.h diff --git a/src/sat/luby.cpp b/src/util/luby.cpp similarity index 100% rename from src/sat/luby.cpp rename to src/util/luby.cpp diff --git a/src/sat/luby.h b/src/util/luby.h similarity index 100% rename from src/sat/luby.h rename to src/util/luby.h diff --git a/lib/union_find.h b/src/util/union_find.h similarity index 100% rename from lib/union_find.h rename to src/util/union_find.h