From 137339a2e17697e715d0ec3909176c5c13f3ab02 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 28 Aug 2013 12:08:47 -0700
Subject: [PATCH] split muz_qe into two directories
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
scripts/mk_project.py | 8 +-
src/{muz_qe => muz}/README | 0
src/{muz_qe => muz}/aig_exporter.cpp | 0
src/{muz_qe => muz}/aig_exporter.h | 0
src/{muz_qe => muz}/arith_bounds_tactic.cpp | 0
src/{muz_qe => muz}/arith_bounds_tactic.h | 0
src/{muz_qe => muz}/clp_context.cpp | 0
src/{muz_qe => muz}/clp_context.h | 0
src/{muz_qe => muz}/datalog_parser.cpp | 0
src/{muz_qe => muz}/datalog_parser.h | 0
src/{muz_qe => muz}/dl_base.cpp | 0
src/{muz_qe => muz}/dl_base.h | 0
src/{muz_qe => muz}/dl_bmc_engine.cpp | 0
src/{muz_qe => muz}/dl_bmc_engine.h | 0
src/{muz_qe => muz}/dl_boogie_proof.cpp | 4 +-
src/{muz_qe => muz}/dl_boogie_proof.h | 0
src/{muz_qe => muz}/dl_bound_relation.cpp | 0
src/{muz_qe => muz}/dl_bound_relation.h | 0
src/{muz_qe => muz}/dl_check_table.cpp | 0
src/{muz_qe => muz}/dl_check_table.h | 0
src/{muz_qe => muz}/dl_cmds.cpp | 0
src/{muz_qe => muz}/dl_cmds.h | 0
src/{muz_qe => muz}/dl_compiler.cpp | 0
src/{muz_qe => muz}/dl_compiler.h | 0
src/{muz_qe => muz}/dl_context.cpp | 12 +-
src/{muz_qe => muz}/dl_context.h | 0
src/{muz_qe => muz}/dl_costs.cpp | 0
src/{muz_qe => muz}/dl_costs.h | 0
src/{muz_qe => muz}/dl_external_relation.cpp | 0
src/{muz_qe => muz}/dl_external_relation.h | 0
.../dl_finite_product_relation.cpp | 0
.../dl_finite_product_relation.h | 0
src/{muz_qe => muz}/dl_instruction.cpp | 0
src/{muz_qe => muz}/dl_instruction.h | 0
src/{muz_qe => muz}/dl_interval_relation.cpp | 0
src/{muz_qe => muz}/dl_interval_relation.h | 0
src/{muz_qe => muz}/dl_mk_array_blast.cpp | 6 +-
src/{muz_qe => muz}/dl_mk_array_blast.h | 0
src/{muz_qe => muz}/dl_mk_backwards.cpp | 0
src/{muz_qe => muz}/dl_mk_backwards.h | 0
src/{muz_qe => muz}/dl_mk_bit_blast.cpp | 0
src/{muz_qe => muz}/dl_mk_bit_blast.h | 0
src/{muz_qe => muz}/dl_mk_coalesce.cpp | 0
src/{muz_qe => muz}/dl_mk_coalesce.h | 0
src/{muz_qe => muz}/dl_mk_coi_filter.cpp | 0
src/{muz_qe => muz}/dl_mk_coi_filter.h | 0
src/muz/dl_mk_different.h | 38 ++++++
src/{muz_qe => muz}/dl_mk_explanations.cpp | 0
src/{muz_qe => muz}/dl_mk_explanations.h | 0
src/{muz_qe => muz}/dl_mk_filter_rules.cpp | 0
src/{muz_qe => muz}/dl_mk_filter_rules.h | 0
.../dl_mk_interp_tail_simplifier.cpp | 2 +-
.../dl_mk_interp_tail_simplifier.h | 0
src/{muz_qe => muz}/dl_mk_karr_invariants.cpp | 2 +-
src/{muz_qe => muz}/dl_mk_karr_invariants.h | 0
src/{muz_qe => muz}/dl_mk_loop_counter.cpp | 0
src/{muz_qe => muz}/dl_mk_loop_counter.h | 0
src/{muz_qe => muz}/dl_mk_magic_sets.cpp | 0
src/{muz_qe => muz}/dl_mk_magic_sets.h | 0
src/{muz_qe => muz}/dl_mk_magic_symbolic.cpp | 0
src/{muz_qe => muz}/dl_mk_magic_symbolic.h | 0
src/{muz_qe => muz}/dl_mk_partial_equiv.cpp | 0
src/{muz_qe => muz}/dl_mk_partial_equiv.h | 0
.../dl_mk_quantifier_abstraction.cpp | 0
.../dl_mk_quantifier_abstraction.h | 0
.../dl_mk_quantifier_instantiation.cpp | 2 +-
.../dl_mk_quantifier_instantiation.h | 0
src/{muz_qe => muz}/dl_mk_rule_inliner.cpp | 0
src/{muz_qe => muz}/dl_mk_rule_inliner.h | 0
src/{muz_qe => muz}/dl_mk_scale.cpp | 0
src/{muz_qe => muz}/dl_mk_scale.h | 0
.../dl_mk_similarity_compressor.cpp | 0
.../dl_mk_similarity_compressor.h | 0
src/{muz_qe => muz}/dl_mk_simple_joins.cpp | 0
src/{muz_qe => muz}/dl_mk_simple_joins.h | 0
src/{muz_qe => muz}/dl_mk_slice.cpp | 2 +-
src/{muz_qe => muz}/dl_mk_slice.h | 0
.../dl_mk_subsumption_checker.cpp | 0
.../dl_mk_subsumption_checker.h | 0
.../dl_mk_unbound_compressor.cpp | 0
.../dl_mk_unbound_compressor.h | 0
src/{muz_qe => muz}/dl_mk_unfold.cpp | 0
src/{muz_qe => muz}/dl_mk_unfold.h | 0
src/{muz_qe => muz}/dl_product_relation.cpp | 0
src/{muz_qe => muz}/dl_product_relation.h | 0
src/{muz_qe => muz}/dl_relation_manager.cpp | 0
src/{muz_qe => muz}/dl_relation_manager.h | 0
src/{muz_qe => muz}/dl_rule.cpp | 4 +-
src/{muz_qe => muz}/dl_rule.h | 0
src/{muz_qe => muz}/dl_rule_set.cpp | 0
src/{muz_qe => muz}/dl_rule_set.h | 0
.../dl_rule_subsumption_index.cpp | 0
.../dl_rule_subsumption_index.h | 0
src/{muz_qe => muz}/dl_rule_transformer.cpp | 0
src/{muz_qe => muz}/dl_rule_transformer.h | 0
src/{muz_qe => muz}/dl_sieve_relation.cpp | 0
src/{muz_qe => muz}/dl_sieve_relation.h | 0
src/{muz_qe => muz}/dl_sparse_table.cpp | 0
src/{muz_qe => muz}/dl_sparse_table.h | 0
src/{muz_qe => muz}/dl_table.cpp | 0
src/{muz_qe => muz}/dl_table.h | 0
src/{muz_qe => muz}/dl_table_plugin.h | 0
src/{muz_qe => muz}/dl_table_relation.cpp | 0
src/{muz_qe => muz}/dl_table_relation.h | 0
src/{muz_qe => muz}/dl_util.cpp | 112 -----------------
src/{muz_qe => muz}/dl_util.h | 13 +-
src/{muz_qe => muz}/dl_vector_relation.h | 0
src/{muz_qe => muz}/equiv_proof_converter.cpp | 0
src/{muz_qe => muz}/equiv_proof_converter.h | 0
src/{muz_qe => muz}/fixedpoint_params.pyg | 0
src/{muz_qe => muz}/heap_trie.h | 0
src/{muz_qe => muz}/hilbert_basis.cpp | 0
src/{muz_qe => muz}/hilbert_basis.h | 0
src/{muz_qe => muz}/hnf.cpp | 2 +-
src/{muz_qe => muz}/hnf.h | 0
.../horn_subsume_model_converter.cpp | 0
.../horn_subsume_model_converter.h | 0
src/{muz_qe => muz}/horn_tactic.cpp | 2 +-
src/{muz_qe => muz}/horn_tactic.h | 0
src/{muz_qe => muz}/model2expr.cpp | 0
src/{muz_qe => muz}/model2expr.h | 0
src/{muz_qe => muz}/pdr_context.cpp | 11 +-
src/{muz_qe => muz}/pdr_context.h | 0
src/{muz_qe => muz}/pdr_dl_interface.cpp | 0
src/{muz_qe => muz}/pdr_dl_interface.h | 0
src/{muz_qe => muz}/pdr_farkas_learner.cpp | 2 +-
src/{muz_qe => muz}/pdr_farkas_learner.h | 0
src/{muz_qe => muz}/pdr_generalizers.cpp | 10 +-
src/{muz_qe => muz}/pdr_generalizers.h | 0
src/{muz_qe => muz}/pdr_manager.cpp | 6 +-
src/{muz_qe => muz}/pdr_manager.h | 0
src/{muz_qe => muz}/pdr_prop_solver.cpp | 2 +-
src/{muz_qe => muz}/pdr_prop_solver.h | 0
src/{muz_qe => muz}/pdr_reachable_cache.cpp | 0
src/{muz_qe => muz}/pdr_reachable_cache.h | 0
.../pdr_smt_context_manager.cpp | 0
src/{muz_qe => muz}/pdr_smt_context_manager.h | 0
src/{muz_qe => muz}/pdr_sym_mux.cpp | 0
src/{muz_qe => muz}/pdr_sym_mux.h | 0
src/{muz_qe => muz}/pdr_util.cpp | 2 +-
src/{muz_qe => muz}/pdr_util.h | 0
src/{muz_qe => muz}/proof_utils.cpp | 0
src/{muz_qe => muz}/proof_utils.h | 0
src/{muz_qe => muz}/rel_context.cpp | 0
src/{muz_qe => muz}/rel_context.h | 0
.../replace_proof_converter.cpp | 0
src/{muz_qe => muz}/replace_proof_converter.h | 0
src/{muz_qe => muz}/skip_list_base.h | 0
src/{muz_qe => muz}/tab_context.cpp | 6 +-
src/{muz_qe => muz}/tab_context.h | 0
.../unit_subsumption_tactic.cpp | 0
src/{muz_qe => muz}/unit_subsumption_tactic.h | 0
src/{muz_qe => muz}/vsubst_tactic.cpp | 0
src/{muz_qe => muz}/vsubst_tactic.h | 0
src/{muz_qe => qe}/nlarith_util.cpp | 0
src/{muz_qe => qe}/nlarith_util.h | 0
src/{muz_qe => qe}/qe.cpp | 6 +-
src/{muz_qe => qe}/qe.h | 0
src/{muz_qe => qe}/qe_arith_plugin.cpp | 0
src/{muz_qe => qe}/qe_array_plugin.cpp | 0
src/{muz_qe => qe}/qe_bool_plugin.cpp | 0
src/{muz_qe => qe}/qe_bv_plugin.cpp | 0
src/{muz_qe => qe}/qe_cmd.cpp | 0
src/{muz_qe => qe}/qe_cmd.h | 0
src/{muz_qe => qe}/qe_datatype_plugin.cpp | 0
src/{muz_qe => qe}/qe_dl_plugin.cpp | 0
src/{muz_qe => qe}/qe_lite.cpp | 9 +-
src/{muz_qe => qe}/qe_lite.h | 0
src/{muz_qe => qe}/qe_sat_tactic.cpp | 0
src/{muz_qe => qe}/qe_sat_tactic.h | 0
src/{muz_qe => qe}/qe_tactic.cpp | 0
src/{muz_qe => qe}/qe_tactic.h | 0
src/qe/qe_util.cpp | 116 ++++++++++++++++++
src/qe/qe_util.h | 37 ++++++
174 files changed, 242 insertions(+), 174 deletions(-)
rename src/{muz_qe => muz}/README (100%)
rename src/{muz_qe => muz}/aig_exporter.cpp (100%)
mode change 100755 => 100644
rename src/{muz_qe => muz}/aig_exporter.h (100%)
mode change 100755 => 100644
rename src/{muz_qe => muz}/arith_bounds_tactic.cpp (100%)
rename src/{muz_qe => muz}/arith_bounds_tactic.h (100%)
rename src/{muz_qe => muz}/clp_context.cpp (100%)
rename src/{muz_qe => muz}/clp_context.h (100%)
rename src/{muz_qe => muz}/datalog_parser.cpp (100%)
rename src/{muz_qe => muz}/datalog_parser.h (100%)
rename src/{muz_qe => muz}/dl_base.cpp (100%)
rename src/{muz_qe => muz}/dl_base.h (100%)
rename src/{muz_qe => muz}/dl_bmc_engine.cpp (100%)
rename src/{muz_qe => muz}/dl_bmc_engine.h (100%)
rename src/{muz_qe => muz}/dl_boogie_proof.cpp (99%)
rename src/{muz_qe => muz}/dl_boogie_proof.h (100%)
rename src/{muz_qe => muz}/dl_bound_relation.cpp (100%)
rename src/{muz_qe => muz}/dl_bound_relation.h (100%)
rename src/{muz_qe => muz}/dl_check_table.cpp (100%)
rename src/{muz_qe => muz}/dl_check_table.h (100%)
rename src/{muz_qe => muz}/dl_cmds.cpp (100%)
rename src/{muz_qe => muz}/dl_cmds.h (100%)
rename src/{muz_qe => muz}/dl_compiler.cpp (100%)
rename src/{muz_qe => muz}/dl_compiler.h (100%)
rename src/{muz_qe => muz}/dl_context.cpp (100%)
rename src/{muz_qe => muz}/dl_context.h (100%)
rename src/{muz_qe => muz}/dl_costs.cpp (100%)
rename src/{muz_qe => muz}/dl_costs.h (100%)
rename src/{muz_qe => muz}/dl_external_relation.cpp (100%)
rename src/{muz_qe => muz}/dl_external_relation.h (100%)
rename src/{muz_qe => muz}/dl_finite_product_relation.cpp (100%)
rename src/{muz_qe => muz}/dl_finite_product_relation.h (100%)
rename src/{muz_qe => muz}/dl_instruction.cpp (100%)
rename src/{muz_qe => muz}/dl_instruction.h (100%)
rename src/{muz_qe => muz}/dl_interval_relation.cpp (100%)
rename src/{muz_qe => muz}/dl_interval_relation.h (100%)
rename src/{muz_qe => muz}/dl_mk_array_blast.cpp (98%)
rename src/{muz_qe => muz}/dl_mk_array_blast.h (100%)
rename src/{muz_qe => muz}/dl_mk_backwards.cpp (100%)
rename src/{muz_qe => muz}/dl_mk_backwards.h (100%)
rename src/{muz_qe => muz}/dl_mk_bit_blast.cpp (100%)
rename src/{muz_qe => muz}/dl_mk_bit_blast.h (100%)
rename src/{muz_qe => muz}/dl_mk_coalesce.cpp (100%)
rename src/{muz_qe => muz}/dl_mk_coalesce.h (100%)
rename src/{muz_qe => muz}/dl_mk_coi_filter.cpp (100%)
rename src/{muz_qe => muz}/dl_mk_coi_filter.h (100%)
create mode 100644 src/muz/dl_mk_different.h
rename src/{muz_qe => muz}/dl_mk_explanations.cpp (100%)
rename src/{muz_qe => muz}/dl_mk_explanations.h (100%)
rename src/{muz_qe => muz}/dl_mk_filter_rules.cpp (100%)
rename src/{muz_qe => muz}/dl_mk_filter_rules.h (100%)
rename src/{muz_qe => muz}/dl_mk_interp_tail_simplifier.cpp (99%)
rename src/{muz_qe => muz}/dl_mk_interp_tail_simplifier.h (100%)
rename src/{muz_qe => muz}/dl_mk_karr_invariants.cpp (99%)
rename src/{muz_qe => muz}/dl_mk_karr_invariants.h (100%)
rename src/{muz_qe => muz}/dl_mk_loop_counter.cpp (100%)
rename src/{muz_qe => muz}/dl_mk_loop_counter.h (100%)
rename src/{muz_qe => muz}/dl_mk_magic_sets.cpp (100%)
rename src/{muz_qe => muz}/dl_mk_magic_sets.h (100%)
rename src/{muz_qe => muz}/dl_mk_magic_symbolic.cpp (100%)
rename src/{muz_qe => muz}/dl_mk_magic_symbolic.h (100%)
rename src/{muz_qe => muz}/dl_mk_partial_equiv.cpp (100%)
rename src/{muz_qe => muz}/dl_mk_partial_equiv.h (100%)
rename src/{muz_qe => muz}/dl_mk_quantifier_abstraction.cpp (100%)
rename src/{muz_qe => muz}/dl_mk_quantifier_abstraction.h (100%)
rename src/{muz_qe => muz}/dl_mk_quantifier_instantiation.cpp (99%)
rename src/{muz_qe => muz}/dl_mk_quantifier_instantiation.h (100%)
rename src/{muz_qe => muz}/dl_mk_rule_inliner.cpp (100%)
rename src/{muz_qe => muz}/dl_mk_rule_inliner.h (100%)
rename src/{muz_qe => muz}/dl_mk_scale.cpp (100%)
rename src/{muz_qe => muz}/dl_mk_scale.h (100%)
rename src/{muz_qe => muz}/dl_mk_similarity_compressor.cpp (100%)
rename src/{muz_qe => muz}/dl_mk_similarity_compressor.h (100%)
rename src/{muz_qe => muz}/dl_mk_simple_joins.cpp (100%)
rename src/{muz_qe => muz}/dl_mk_simple_joins.h (100%)
rename src/{muz_qe => muz}/dl_mk_slice.cpp (99%)
rename src/{muz_qe => muz}/dl_mk_slice.h (100%)
rename src/{muz_qe => muz}/dl_mk_subsumption_checker.cpp (100%)
rename src/{muz_qe => muz}/dl_mk_subsumption_checker.h (100%)
rename src/{muz_qe => muz}/dl_mk_unbound_compressor.cpp (100%)
rename src/{muz_qe => muz}/dl_mk_unbound_compressor.h (100%)
rename src/{muz_qe => muz}/dl_mk_unfold.cpp (100%)
rename src/{muz_qe => muz}/dl_mk_unfold.h (100%)
rename src/{muz_qe => muz}/dl_product_relation.cpp (100%)
rename src/{muz_qe => muz}/dl_product_relation.h (100%)
rename src/{muz_qe => muz}/dl_relation_manager.cpp (100%)
rename src/{muz_qe => muz}/dl_relation_manager.h (100%)
rename src/{muz_qe => muz}/dl_rule.cpp (99%)
rename src/{muz_qe => muz}/dl_rule.h (100%)
rename src/{muz_qe => muz}/dl_rule_set.cpp (100%)
rename src/{muz_qe => muz}/dl_rule_set.h (100%)
rename src/{muz_qe => muz}/dl_rule_subsumption_index.cpp (100%)
rename src/{muz_qe => muz}/dl_rule_subsumption_index.h (100%)
rename src/{muz_qe => muz}/dl_rule_transformer.cpp (100%)
rename src/{muz_qe => muz}/dl_rule_transformer.h (100%)
rename src/{muz_qe => muz}/dl_sieve_relation.cpp (100%)
rename src/{muz_qe => muz}/dl_sieve_relation.h (100%)
rename src/{muz_qe => muz}/dl_sparse_table.cpp (100%)
rename src/{muz_qe => muz}/dl_sparse_table.h (100%)
rename src/{muz_qe => muz}/dl_table.cpp (100%)
rename src/{muz_qe => muz}/dl_table.h (100%)
rename src/{muz_qe => muz}/dl_table_plugin.h (100%)
rename src/{muz_qe => muz}/dl_table_relation.cpp (100%)
rename src/{muz_qe => muz}/dl_table_relation.h (100%)
rename src/{muz_qe => muz}/dl_util.cpp (83%)
rename src/{muz_qe => muz}/dl_util.h (98%)
rename src/{muz_qe => muz}/dl_vector_relation.h (100%)
rename src/{muz_qe => muz}/equiv_proof_converter.cpp (100%)
rename src/{muz_qe => muz}/equiv_proof_converter.h (100%)
rename src/{muz_qe => muz}/fixedpoint_params.pyg (100%)
rename src/{muz_qe => muz}/heap_trie.h (100%)
rename src/{muz_qe => muz}/hilbert_basis.cpp (100%)
rename src/{muz_qe => muz}/hilbert_basis.h (100%)
rename src/{muz_qe => muz}/hnf.cpp (99%)
rename src/{muz_qe => muz}/hnf.h (100%)
rename src/{muz_qe => muz}/horn_subsume_model_converter.cpp (100%)
rename src/{muz_qe => muz}/horn_subsume_model_converter.h (100%)
rename src/{muz_qe => muz}/horn_tactic.cpp (99%)
rename src/{muz_qe => muz}/horn_tactic.h (100%)
rename src/{muz_qe => muz}/model2expr.cpp (100%)
rename src/{muz_qe => muz}/model2expr.h (100%)
rename src/{muz_qe => muz}/pdr_context.cpp (99%)
rename src/{muz_qe => muz}/pdr_context.h (100%)
rename src/{muz_qe => muz}/pdr_dl_interface.cpp (100%)
rename src/{muz_qe => muz}/pdr_dl_interface.h (100%)
rename src/{muz_qe => muz}/pdr_farkas_learner.cpp (99%)
rename src/{muz_qe => muz}/pdr_farkas_learner.h (100%)
rename src/{muz_qe => muz}/pdr_generalizers.cpp (99%)
rename src/{muz_qe => muz}/pdr_generalizers.h (100%)
rename src/{muz_qe => muz}/pdr_manager.cpp (98%)
rename src/{muz_qe => muz}/pdr_manager.h (100%)
rename src/{muz_qe => muz}/pdr_prop_solver.cpp (99%)
rename src/{muz_qe => muz}/pdr_prop_solver.h (100%)
rename src/{muz_qe => muz}/pdr_reachable_cache.cpp (100%)
rename src/{muz_qe => muz}/pdr_reachable_cache.h (100%)
rename src/{muz_qe => muz}/pdr_smt_context_manager.cpp (100%)
rename src/{muz_qe => muz}/pdr_smt_context_manager.h (100%)
rename src/{muz_qe => muz}/pdr_sym_mux.cpp (100%)
rename src/{muz_qe => muz}/pdr_sym_mux.h (100%)
rename src/{muz_qe => muz}/pdr_util.cpp (99%)
rename src/{muz_qe => muz}/pdr_util.h (100%)
rename src/{muz_qe => muz}/proof_utils.cpp (100%)
rename src/{muz_qe => muz}/proof_utils.h (100%)
rename src/{muz_qe => muz}/rel_context.cpp (100%)
rename src/{muz_qe => muz}/rel_context.h (100%)
rename src/{muz_qe => muz}/replace_proof_converter.cpp (100%)
rename src/{muz_qe => muz}/replace_proof_converter.h (100%)
rename src/{muz_qe => muz}/skip_list_base.h (100%)
rename src/{muz_qe => muz}/tab_context.cpp (99%)
rename src/{muz_qe => muz}/tab_context.h (100%)
rename src/{muz_qe => muz}/unit_subsumption_tactic.cpp (100%)
rename src/{muz_qe => muz}/unit_subsumption_tactic.h (100%)
rename src/{muz_qe => muz}/vsubst_tactic.cpp (100%)
rename src/{muz_qe => muz}/vsubst_tactic.h (100%)
rename src/{muz_qe => qe}/nlarith_util.cpp (100%)
rename src/{muz_qe => qe}/nlarith_util.h (100%)
rename src/{muz_qe => qe}/qe.cpp (99%)
rename src/{muz_qe => qe}/qe.h (100%)
rename src/{muz_qe => qe}/qe_arith_plugin.cpp (100%)
rename src/{muz_qe => qe}/qe_array_plugin.cpp (100%)
rename src/{muz_qe => qe}/qe_bool_plugin.cpp (100%)
rename src/{muz_qe => qe}/qe_bv_plugin.cpp (100%)
rename src/{muz_qe => qe}/qe_cmd.cpp (100%)
rename src/{muz_qe => qe}/qe_cmd.h (100%)
rename src/{muz_qe => qe}/qe_datatype_plugin.cpp (100%)
rename src/{muz_qe => qe}/qe_dl_plugin.cpp (100%)
rename src/{muz_qe => qe}/qe_lite.cpp (99%)
rename src/{muz_qe => qe}/qe_lite.h (100%)
rename src/{muz_qe => qe}/qe_sat_tactic.cpp (100%)
rename src/{muz_qe => qe}/qe_sat_tactic.h (100%)
rename src/{muz_qe => qe}/qe_tactic.cpp (100%)
rename src/{muz_qe => qe}/qe_tactic.h (100%)
create mode 100644 src/qe/qe_util.cpp
create mode 100644 src/qe/qe_util.h
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index e6e7d5dc8..44ad9ccbc 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -53,11 +53,11 @@ def init_project_def():
add_lib('fpa', ['core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa')
add_lib('smt_tactic', ['smt'], 'smt/tactic')
add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')
- # 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', 'aig_tactic'])
- add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'muz_qe'], 'tactic/smtlogics')
+ add_lib('qe', ['smt','sat'], 'qe')
+ add_lib('muz', ['smt', 'sat', 'smt2parser', 'aig_tactic','qe'])
+ add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'muz','qe'], 'tactic/smtlogics')
add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
- add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'muz_qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
+ add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'muz', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
add_lib('smtparser', ['portfolio'], 'parsers/smt')
API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h']
add_lib('api', ['portfolio', 'user_plugin', 'smtparser', 'realclosure'],
diff --git a/src/muz_qe/README b/src/muz/README
similarity index 100%
rename from src/muz_qe/README
rename to src/muz/README
diff --git a/src/muz_qe/aig_exporter.cpp b/src/muz/aig_exporter.cpp
old mode 100755
new mode 100644
similarity index 100%
rename from src/muz_qe/aig_exporter.cpp
rename to src/muz/aig_exporter.cpp
diff --git a/src/muz_qe/aig_exporter.h b/src/muz/aig_exporter.h
old mode 100755
new mode 100644
similarity index 100%
rename from src/muz_qe/aig_exporter.h
rename to src/muz/aig_exporter.h
diff --git a/src/muz_qe/arith_bounds_tactic.cpp b/src/muz/arith_bounds_tactic.cpp
similarity index 100%
rename from src/muz_qe/arith_bounds_tactic.cpp
rename to src/muz/arith_bounds_tactic.cpp
diff --git a/src/muz_qe/arith_bounds_tactic.h b/src/muz/arith_bounds_tactic.h
similarity index 100%
rename from src/muz_qe/arith_bounds_tactic.h
rename to src/muz/arith_bounds_tactic.h
diff --git a/src/muz_qe/clp_context.cpp b/src/muz/clp_context.cpp
similarity index 100%
rename from src/muz_qe/clp_context.cpp
rename to src/muz/clp_context.cpp
diff --git a/src/muz_qe/clp_context.h b/src/muz/clp_context.h
similarity index 100%
rename from src/muz_qe/clp_context.h
rename to src/muz/clp_context.h
diff --git a/src/muz_qe/datalog_parser.cpp b/src/muz/datalog_parser.cpp
similarity index 100%
rename from src/muz_qe/datalog_parser.cpp
rename to src/muz/datalog_parser.cpp
diff --git a/src/muz_qe/datalog_parser.h b/src/muz/datalog_parser.h
similarity index 100%
rename from src/muz_qe/datalog_parser.h
rename to src/muz/datalog_parser.h
diff --git a/src/muz_qe/dl_base.cpp b/src/muz/dl_base.cpp
similarity index 100%
rename from src/muz_qe/dl_base.cpp
rename to src/muz/dl_base.cpp
diff --git a/src/muz_qe/dl_base.h b/src/muz/dl_base.h
similarity index 100%
rename from src/muz_qe/dl_base.h
rename to src/muz/dl_base.h
diff --git a/src/muz_qe/dl_bmc_engine.cpp b/src/muz/dl_bmc_engine.cpp
similarity index 100%
rename from src/muz_qe/dl_bmc_engine.cpp
rename to src/muz/dl_bmc_engine.cpp
diff --git a/src/muz_qe/dl_bmc_engine.h b/src/muz/dl_bmc_engine.h
similarity index 100%
rename from src/muz_qe/dl_bmc_engine.h
rename to src/muz/dl_bmc_engine.h
diff --git a/src/muz_qe/dl_boogie_proof.cpp b/src/muz/dl_boogie_proof.cpp
similarity index 99%
rename from src/muz_qe/dl_boogie_proof.cpp
rename to src/muz/dl_boogie_proof.cpp
index e14512973..d11e4a932 100644
--- a/src/muz_qe/dl_boogie_proof.cpp
+++ b/src/muz/dl_boogie_proof.cpp
@@ -49,7 +49,7 @@ Example from Boogie:
#include "model_pp.h"
#include "proof_utils.h"
#include "ast_pp.h"
-#include "dl_util.h"
+#include "qe_util.h"
namespace datalog {
@@ -91,7 +91,7 @@ namespace datalog {
if (!m.is_implies(premise, l1, l2)) {
continue;
}
- datalog::flatten_and(l1, literals);
+ qe::flatten_and(l1, literals);
positions2.reset();
premises2.reset();
premises2.push_back(premise);
diff --git a/src/muz_qe/dl_boogie_proof.h b/src/muz/dl_boogie_proof.h
similarity index 100%
rename from src/muz_qe/dl_boogie_proof.h
rename to src/muz/dl_boogie_proof.h
diff --git a/src/muz_qe/dl_bound_relation.cpp b/src/muz/dl_bound_relation.cpp
similarity index 100%
rename from src/muz_qe/dl_bound_relation.cpp
rename to src/muz/dl_bound_relation.cpp
diff --git a/src/muz_qe/dl_bound_relation.h b/src/muz/dl_bound_relation.h
similarity index 100%
rename from src/muz_qe/dl_bound_relation.h
rename to src/muz/dl_bound_relation.h
diff --git a/src/muz_qe/dl_check_table.cpp b/src/muz/dl_check_table.cpp
similarity index 100%
rename from src/muz_qe/dl_check_table.cpp
rename to src/muz/dl_check_table.cpp
diff --git a/src/muz_qe/dl_check_table.h b/src/muz/dl_check_table.h
similarity index 100%
rename from src/muz_qe/dl_check_table.h
rename to src/muz/dl_check_table.h
diff --git a/src/muz_qe/dl_cmds.cpp b/src/muz/dl_cmds.cpp
similarity index 100%
rename from src/muz_qe/dl_cmds.cpp
rename to src/muz/dl_cmds.cpp
diff --git a/src/muz_qe/dl_cmds.h b/src/muz/dl_cmds.h
similarity index 100%
rename from src/muz_qe/dl_cmds.h
rename to src/muz/dl_cmds.h
diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz/dl_compiler.cpp
similarity index 100%
rename from src/muz_qe/dl_compiler.cpp
rename to src/muz/dl_compiler.cpp
diff --git a/src/muz_qe/dl_compiler.h b/src/muz/dl_compiler.h
similarity index 100%
rename from src/muz_qe/dl_compiler.h
rename to src/muz/dl_compiler.h
diff --git a/src/muz_qe/dl_context.cpp b/src/muz/dl_context.cpp
similarity index 100%
rename from src/muz_qe/dl_context.cpp
rename to src/muz/dl_context.cpp
index 7da9808e7..f5bfb6b5e 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz/dl_context.cpp
@@ -35,12 +35,6 @@ Revision History:
#include"dl_mk_similarity_compressor.h"
#include"dl_mk_unbound_compressor.h"
#include"dl_mk_subsumption_checker.h"
-#include"dl_compiler.h"
-#include"dl_instruction.h"
-#include"dl_context.h"
-#include"for_each_expr.h"
-#include"ast_smt_pp.h"
-#include"ast_smt2_pp.h"
#include"dl_mk_partial_equiv.h"
#include"dl_mk_bit_blast.h"
#include"dl_mk_array_blast.h"
@@ -49,6 +43,12 @@ Revision History:
#include"dl_mk_quantifier_abstraction.h"
#include"dl_mk_quantifier_instantiation.h"
#include"dl_mk_scale.h"
+#include"dl_compiler.h"
+#include"dl_instruction.h"
+#include"dl_context.h"
+#include"for_each_expr.h"
+#include"ast_smt_pp.h"
+#include"ast_smt2_pp.h"
#include"datatype_decl_plugin.h"
diff --git a/src/muz_qe/dl_context.h b/src/muz/dl_context.h
similarity index 100%
rename from src/muz_qe/dl_context.h
rename to src/muz/dl_context.h
diff --git a/src/muz_qe/dl_costs.cpp b/src/muz/dl_costs.cpp
similarity index 100%
rename from src/muz_qe/dl_costs.cpp
rename to src/muz/dl_costs.cpp
diff --git a/src/muz_qe/dl_costs.h b/src/muz/dl_costs.h
similarity index 100%
rename from src/muz_qe/dl_costs.h
rename to src/muz/dl_costs.h
diff --git a/src/muz_qe/dl_external_relation.cpp b/src/muz/dl_external_relation.cpp
similarity index 100%
rename from src/muz_qe/dl_external_relation.cpp
rename to src/muz/dl_external_relation.cpp
diff --git a/src/muz_qe/dl_external_relation.h b/src/muz/dl_external_relation.h
similarity index 100%
rename from src/muz_qe/dl_external_relation.h
rename to src/muz/dl_external_relation.h
diff --git a/src/muz_qe/dl_finite_product_relation.cpp b/src/muz/dl_finite_product_relation.cpp
similarity index 100%
rename from src/muz_qe/dl_finite_product_relation.cpp
rename to src/muz/dl_finite_product_relation.cpp
diff --git a/src/muz_qe/dl_finite_product_relation.h b/src/muz/dl_finite_product_relation.h
similarity index 100%
rename from src/muz_qe/dl_finite_product_relation.h
rename to src/muz/dl_finite_product_relation.h
diff --git a/src/muz_qe/dl_instruction.cpp b/src/muz/dl_instruction.cpp
similarity index 100%
rename from src/muz_qe/dl_instruction.cpp
rename to src/muz/dl_instruction.cpp
diff --git a/src/muz_qe/dl_instruction.h b/src/muz/dl_instruction.h
similarity index 100%
rename from src/muz_qe/dl_instruction.h
rename to src/muz/dl_instruction.h
diff --git a/src/muz_qe/dl_interval_relation.cpp b/src/muz/dl_interval_relation.cpp
similarity index 100%
rename from src/muz_qe/dl_interval_relation.cpp
rename to src/muz/dl_interval_relation.cpp
diff --git a/src/muz_qe/dl_interval_relation.h b/src/muz/dl_interval_relation.h
similarity index 100%
rename from src/muz_qe/dl_interval_relation.h
rename to src/muz/dl_interval_relation.h
diff --git a/src/muz_qe/dl_mk_array_blast.cpp b/src/muz/dl_mk_array_blast.cpp
similarity index 98%
rename from src/muz_qe/dl_mk_array_blast.cpp
rename to src/muz/dl_mk_array_blast.cpp
index 2bfb6807a..776a2da5b 100644
--- a/src/muz_qe/dl_mk_array_blast.cpp
+++ b/src/muz/dl_mk_array_blast.cpp
@@ -18,7 +18,7 @@ Revision History:
--*/
#include "dl_mk_array_blast.h"
-
+#include "qe_util.h"
namespace datalog {
@@ -101,7 +101,7 @@ namespace datalog {
bool mk_array_blast::ackermanize(rule const& r, expr_ref& body, expr_ref& head) {
expr_ref_vector conjs(m);
- flatten_and(body, conjs);
+ qe::flatten_and(body, conjs);
m_defs.reset();
m_sub.reset();
m_next_var = 0;
@@ -207,7 +207,7 @@ namespace datalog {
for (unsigned i = utsz; i < tsz; ++i) {
conjs.push_back(r.get_tail(i));
}
- flatten_and(conjs);
+ qe::flatten_and(conjs);
for (unsigned i = 0; i < conjs.size(); ++i) {
expr* x, *y, *e = conjs[i].get();
diff --git a/src/muz_qe/dl_mk_array_blast.h b/src/muz/dl_mk_array_blast.h
similarity index 100%
rename from src/muz_qe/dl_mk_array_blast.h
rename to src/muz/dl_mk_array_blast.h
diff --git a/src/muz_qe/dl_mk_backwards.cpp b/src/muz/dl_mk_backwards.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_backwards.cpp
rename to src/muz/dl_mk_backwards.cpp
diff --git a/src/muz_qe/dl_mk_backwards.h b/src/muz/dl_mk_backwards.h
similarity index 100%
rename from src/muz_qe/dl_mk_backwards.h
rename to src/muz/dl_mk_backwards.h
diff --git a/src/muz_qe/dl_mk_bit_blast.cpp b/src/muz/dl_mk_bit_blast.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_bit_blast.cpp
rename to src/muz/dl_mk_bit_blast.cpp
diff --git a/src/muz_qe/dl_mk_bit_blast.h b/src/muz/dl_mk_bit_blast.h
similarity index 100%
rename from src/muz_qe/dl_mk_bit_blast.h
rename to src/muz/dl_mk_bit_blast.h
diff --git a/src/muz_qe/dl_mk_coalesce.cpp b/src/muz/dl_mk_coalesce.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_coalesce.cpp
rename to src/muz/dl_mk_coalesce.cpp
diff --git a/src/muz_qe/dl_mk_coalesce.h b/src/muz/dl_mk_coalesce.h
similarity index 100%
rename from src/muz_qe/dl_mk_coalesce.h
rename to src/muz/dl_mk_coalesce.h
diff --git a/src/muz_qe/dl_mk_coi_filter.cpp b/src/muz/dl_mk_coi_filter.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_coi_filter.cpp
rename to src/muz/dl_mk_coi_filter.cpp
diff --git a/src/muz_qe/dl_mk_coi_filter.h b/src/muz/dl_mk_coi_filter.h
similarity index 100%
rename from src/muz_qe/dl_mk_coi_filter.h
rename to src/muz/dl_mk_coi_filter.h
diff --git a/src/muz/dl_mk_different.h b/src/muz/dl_mk_different.h
new file mode 100644
index 000000000..2def011f9
--- /dev/null
+++ b/src/muz/dl_mk_different.h
@@ -0,0 +1,38 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+ dl_mk_different_symbolic.h
+
+Abstract:
+
+ Create Horn clauses for different symbolic transformation.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2013-06-19
+
+Revision History:
+
+--*/
+#ifndef _DL_MK_DIFFERENT_SYMBOLIC_H_
+#define _DL_MK_DIFFERENT_SYMBOLIC_H_
+
+#include"dl_rule_transformer.h"
+
+namespace datalog {
+
+ class mk_different_symbolic : public rule_transformer::plugin {
+ ast_manager& m;
+ context& m_ctx;
+ public:
+ mk_different_symbolic(context & ctx, unsigned priority = 33037);
+ ~mk_different_symbolic();
+ rule_set * operator()(rule_set const & source);
+ };
+
+};
+
+#endif /* _DL_MK_DIFFERENT_SYMBOLIC_H_ */
+
diff --git a/src/muz_qe/dl_mk_explanations.cpp b/src/muz/dl_mk_explanations.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_explanations.cpp
rename to src/muz/dl_mk_explanations.cpp
diff --git a/src/muz_qe/dl_mk_explanations.h b/src/muz/dl_mk_explanations.h
similarity index 100%
rename from src/muz_qe/dl_mk_explanations.h
rename to src/muz/dl_mk_explanations.h
diff --git a/src/muz_qe/dl_mk_filter_rules.cpp b/src/muz/dl_mk_filter_rules.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_filter_rules.cpp
rename to src/muz/dl_mk_filter_rules.cpp
diff --git a/src/muz_qe/dl_mk_filter_rules.h b/src/muz/dl_mk_filter_rules.h
similarity index 100%
rename from src/muz_qe/dl_mk_filter_rules.h
rename to src/muz/dl_mk_filter_rules.h
diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp b/src/muz/dl_mk_interp_tail_simplifier.cpp
similarity index 99%
rename from src/muz_qe/dl_mk_interp_tail_simplifier.cpp
rename to src/muz/dl_mk_interp_tail_simplifier.cpp
index afd586627..b01b4326c 100644
--- a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp
+++ b/src/muz/dl_mk_interp_tail_simplifier.cpp
@@ -546,7 +546,7 @@ namespace datalog {
if (modified) {
m_conj.reset();
- flatten_and(simp_res, m_conj);
+ qe::flatten_and(simp_res, m_conj);
for (unsigned i = 0; i < m_conj.size(); ++i) {
expr* e = m_conj[i].get();
if (is_app(e)) {
diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.h b/src/muz/dl_mk_interp_tail_simplifier.h
similarity index 100%
rename from src/muz_qe/dl_mk_interp_tail_simplifier.h
rename to src/muz/dl_mk_interp_tail_simplifier.h
diff --git a/src/muz_qe/dl_mk_karr_invariants.cpp b/src/muz/dl_mk_karr_invariants.cpp
similarity index 99%
rename from src/muz_qe/dl_mk_karr_invariants.cpp
rename to src/muz/dl_mk_karr_invariants.cpp
index e4e5a1ff8..11bc850bb 100644
--- a/src/muz_qe/dl_mk_karr_invariants.cpp
+++ b/src/muz/dl_mk_karr_invariants.cpp
@@ -430,7 +430,7 @@ namespace datalog {
var* v, *w;
rational n1, n2;
expr_ref_vector conjs(m);
- datalog::flatten_and(cond, conjs);
+ qe::flatten_and(cond, conjs);
matrix& M = get_ineqs();
unsigned num_columns = get_signature().size();
diff --git a/src/muz_qe/dl_mk_karr_invariants.h b/src/muz/dl_mk_karr_invariants.h
similarity index 100%
rename from src/muz_qe/dl_mk_karr_invariants.h
rename to src/muz/dl_mk_karr_invariants.h
diff --git a/src/muz_qe/dl_mk_loop_counter.cpp b/src/muz/dl_mk_loop_counter.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_loop_counter.cpp
rename to src/muz/dl_mk_loop_counter.cpp
diff --git a/src/muz_qe/dl_mk_loop_counter.h b/src/muz/dl_mk_loop_counter.h
similarity index 100%
rename from src/muz_qe/dl_mk_loop_counter.h
rename to src/muz/dl_mk_loop_counter.h
diff --git a/src/muz_qe/dl_mk_magic_sets.cpp b/src/muz/dl_mk_magic_sets.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_magic_sets.cpp
rename to src/muz/dl_mk_magic_sets.cpp
diff --git a/src/muz_qe/dl_mk_magic_sets.h b/src/muz/dl_mk_magic_sets.h
similarity index 100%
rename from src/muz_qe/dl_mk_magic_sets.h
rename to src/muz/dl_mk_magic_sets.h
diff --git a/src/muz_qe/dl_mk_magic_symbolic.cpp b/src/muz/dl_mk_magic_symbolic.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_magic_symbolic.cpp
rename to src/muz/dl_mk_magic_symbolic.cpp
diff --git a/src/muz_qe/dl_mk_magic_symbolic.h b/src/muz/dl_mk_magic_symbolic.h
similarity index 100%
rename from src/muz_qe/dl_mk_magic_symbolic.h
rename to src/muz/dl_mk_magic_symbolic.h
diff --git a/src/muz_qe/dl_mk_partial_equiv.cpp b/src/muz/dl_mk_partial_equiv.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_partial_equiv.cpp
rename to src/muz/dl_mk_partial_equiv.cpp
diff --git a/src/muz_qe/dl_mk_partial_equiv.h b/src/muz/dl_mk_partial_equiv.h
similarity index 100%
rename from src/muz_qe/dl_mk_partial_equiv.h
rename to src/muz/dl_mk_partial_equiv.h
diff --git a/src/muz_qe/dl_mk_quantifier_abstraction.cpp b/src/muz/dl_mk_quantifier_abstraction.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_quantifier_abstraction.cpp
rename to src/muz/dl_mk_quantifier_abstraction.cpp
diff --git a/src/muz_qe/dl_mk_quantifier_abstraction.h b/src/muz/dl_mk_quantifier_abstraction.h
similarity index 100%
rename from src/muz_qe/dl_mk_quantifier_abstraction.h
rename to src/muz/dl_mk_quantifier_abstraction.h
diff --git a/src/muz_qe/dl_mk_quantifier_instantiation.cpp b/src/muz/dl_mk_quantifier_instantiation.cpp
similarity index 99%
rename from src/muz_qe/dl_mk_quantifier_instantiation.cpp
rename to src/muz/dl_mk_quantifier_instantiation.cpp
index ddbddca01..b24e3e81c 100644
--- a/src/muz_qe/dl_mk_quantifier_instantiation.cpp
+++ b/src/muz/dl_mk_quantifier_instantiation.cpp
@@ -48,7 +48,7 @@ namespace datalog {
for (unsigned j = 0; j < tsz; ++j) {
conjs.push_back(r.get_tail(j));
}
- datalog::flatten_and(conjs);
+ qe::flatten_and(conjs);
for (unsigned j = 0; j < conjs.size(); ++j) {
expr* e = conjs[j].get();
quantifier* q;
diff --git a/src/muz_qe/dl_mk_quantifier_instantiation.h b/src/muz/dl_mk_quantifier_instantiation.h
similarity index 100%
rename from src/muz_qe/dl_mk_quantifier_instantiation.h
rename to src/muz/dl_mk_quantifier_instantiation.h
diff --git a/src/muz_qe/dl_mk_rule_inliner.cpp b/src/muz/dl_mk_rule_inliner.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_rule_inliner.cpp
rename to src/muz/dl_mk_rule_inliner.cpp
diff --git a/src/muz_qe/dl_mk_rule_inliner.h b/src/muz/dl_mk_rule_inliner.h
similarity index 100%
rename from src/muz_qe/dl_mk_rule_inliner.h
rename to src/muz/dl_mk_rule_inliner.h
diff --git a/src/muz_qe/dl_mk_scale.cpp b/src/muz/dl_mk_scale.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_scale.cpp
rename to src/muz/dl_mk_scale.cpp
diff --git a/src/muz_qe/dl_mk_scale.h b/src/muz/dl_mk_scale.h
similarity index 100%
rename from src/muz_qe/dl_mk_scale.h
rename to src/muz/dl_mk_scale.h
diff --git a/src/muz_qe/dl_mk_similarity_compressor.cpp b/src/muz/dl_mk_similarity_compressor.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_similarity_compressor.cpp
rename to src/muz/dl_mk_similarity_compressor.cpp
diff --git a/src/muz_qe/dl_mk_similarity_compressor.h b/src/muz/dl_mk_similarity_compressor.h
similarity index 100%
rename from src/muz_qe/dl_mk_similarity_compressor.h
rename to src/muz/dl_mk_similarity_compressor.h
diff --git a/src/muz_qe/dl_mk_simple_joins.cpp b/src/muz/dl_mk_simple_joins.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_simple_joins.cpp
rename to src/muz/dl_mk_simple_joins.cpp
diff --git a/src/muz_qe/dl_mk_simple_joins.h b/src/muz/dl_mk_simple_joins.h
similarity index 100%
rename from src/muz_qe/dl_mk_simple_joins.h
rename to src/muz/dl_mk_simple_joins.h
diff --git a/src/muz_qe/dl_mk_slice.cpp b/src/muz/dl_mk_slice.cpp
similarity index 99%
rename from src/muz_qe/dl_mk_slice.cpp
rename to src/muz/dl_mk_slice.cpp
index 5b9d43acc..0df75324d 100644
--- a/src/muz_qe/dl_mk_slice.cpp
+++ b/src/muz/dl_mk_slice.cpp
@@ -619,7 +619,7 @@ namespace datalog {
for (unsigned j = r.get_uninterpreted_tail_size(); j < r.get_tail_size(); ++j) {
conjs.push_back(r.get_tail(j));
}
- datalog::flatten_and(conjs);
+ qe::flatten_and(conjs);
return conjs;
}
diff --git a/src/muz_qe/dl_mk_slice.h b/src/muz/dl_mk_slice.h
similarity index 100%
rename from src/muz_qe/dl_mk_slice.h
rename to src/muz/dl_mk_slice.h
diff --git a/src/muz_qe/dl_mk_subsumption_checker.cpp b/src/muz/dl_mk_subsumption_checker.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_subsumption_checker.cpp
rename to src/muz/dl_mk_subsumption_checker.cpp
diff --git a/src/muz_qe/dl_mk_subsumption_checker.h b/src/muz/dl_mk_subsumption_checker.h
similarity index 100%
rename from src/muz_qe/dl_mk_subsumption_checker.h
rename to src/muz/dl_mk_subsumption_checker.h
diff --git a/src/muz_qe/dl_mk_unbound_compressor.cpp b/src/muz/dl_mk_unbound_compressor.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_unbound_compressor.cpp
rename to src/muz/dl_mk_unbound_compressor.cpp
diff --git a/src/muz_qe/dl_mk_unbound_compressor.h b/src/muz/dl_mk_unbound_compressor.h
similarity index 100%
rename from src/muz_qe/dl_mk_unbound_compressor.h
rename to src/muz/dl_mk_unbound_compressor.h
diff --git a/src/muz_qe/dl_mk_unfold.cpp b/src/muz/dl_mk_unfold.cpp
similarity index 100%
rename from src/muz_qe/dl_mk_unfold.cpp
rename to src/muz/dl_mk_unfold.cpp
diff --git a/src/muz_qe/dl_mk_unfold.h b/src/muz/dl_mk_unfold.h
similarity index 100%
rename from src/muz_qe/dl_mk_unfold.h
rename to src/muz/dl_mk_unfold.h
diff --git a/src/muz_qe/dl_product_relation.cpp b/src/muz/dl_product_relation.cpp
similarity index 100%
rename from src/muz_qe/dl_product_relation.cpp
rename to src/muz/dl_product_relation.cpp
diff --git a/src/muz_qe/dl_product_relation.h b/src/muz/dl_product_relation.h
similarity index 100%
rename from src/muz_qe/dl_product_relation.h
rename to src/muz/dl_product_relation.h
diff --git a/src/muz_qe/dl_relation_manager.cpp b/src/muz/dl_relation_manager.cpp
similarity index 100%
rename from src/muz_qe/dl_relation_manager.cpp
rename to src/muz/dl_relation_manager.cpp
diff --git a/src/muz_qe/dl_relation_manager.h b/src/muz/dl_relation_manager.h
similarity index 100%
rename from src/muz_qe/dl_relation_manager.h
rename to src/muz/dl_relation_manager.h
diff --git a/src/muz_qe/dl_rule.cpp b/src/muz/dl_rule.cpp
similarity index 99%
rename from src/muz_qe/dl_rule.cpp
rename to src/muz/dl_rule.cpp
index 455f2c244..5ac580cb8 100644
--- a/src/muz_qe/dl_rule.cpp
+++ b/src/muz/dl_rule.cpp
@@ -263,7 +263,7 @@ namespace datalog {
if (m.is_implies(fml, e1, e2)) {
expr_ref_vector es(m);
head = ensure_app(e2);
- datalog::flatten_and(e1, es);
+ qe::flatten_and(e1, es);
for (unsigned i = 0; i < es.size(); ++i) {
body.push_back(ensure_app(es[i].get()));
}
@@ -380,7 +380,7 @@ namespace datalog {
for (unsigned i = 0; i < body.size(); ++i) {
r.push_back(body[i].get());
}
- flatten_and(r);
+ qe::flatten_and(r);
body.reset();
for (unsigned i = 0; i < r.size(); ++i) {
body.push_back(ensure_app(r[i].get()));
diff --git a/src/muz_qe/dl_rule.h b/src/muz/dl_rule.h
similarity index 100%
rename from src/muz_qe/dl_rule.h
rename to src/muz/dl_rule.h
diff --git a/src/muz_qe/dl_rule_set.cpp b/src/muz/dl_rule_set.cpp
similarity index 100%
rename from src/muz_qe/dl_rule_set.cpp
rename to src/muz/dl_rule_set.cpp
diff --git a/src/muz_qe/dl_rule_set.h b/src/muz/dl_rule_set.h
similarity index 100%
rename from src/muz_qe/dl_rule_set.h
rename to src/muz/dl_rule_set.h
diff --git a/src/muz_qe/dl_rule_subsumption_index.cpp b/src/muz/dl_rule_subsumption_index.cpp
similarity index 100%
rename from src/muz_qe/dl_rule_subsumption_index.cpp
rename to src/muz/dl_rule_subsumption_index.cpp
diff --git a/src/muz_qe/dl_rule_subsumption_index.h b/src/muz/dl_rule_subsumption_index.h
similarity index 100%
rename from src/muz_qe/dl_rule_subsumption_index.h
rename to src/muz/dl_rule_subsumption_index.h
diff --git a/src/muz_qe/dl_rule_transformer.cpp b/src/muz/dl_rule_transformer.cpp
similarity index 100%
rename from src/muz_qe/dl_rule_transformer.cpp
rename to src/muz/dl_rule_transformer.cpp
diff --git a/src/muz_qe/dl_rule_transformer.h b/src/muz/dl_rule_transformer.h
similarity index 100%
rename from src/muz_qe/dl_rule_transformer.h
rename to src/muz/dl_rule_transformer.h
diff --git a/src/muz_qe/dl_sieve_relation.cpp b/src/muz/dl_sieve_relation.cpp
similarity index 100%
rename from src/muz_qe/dl_sieve_relation.cpp
rename to src/muz/dl_sieve_relation.cpp
diff --git a/src/muz_qe/dl_sieve_relation.h b/src/muz/dl_sieve_relation.h
similarity index 100%
rename from src/muz_qe/dl_sieve_relation.h
rename to src/muz/dl_sieve_relation.h
diff --git a/src/muz_qe/dl_sparse_table.cpp b/src/muz/dl_sparse_table.cpp
similarity index 100%
rename from src/muz_qe/dl_sparse_table.cpp
rename to src/muz/dl_sparse_table.cpp
diff --git a/src/muz_qe/dl_sparse_table.h b/src/muz/dl_sparse_table.h
similarity index 100%
rename from src/muz_qe/dl_sparse_table.h
rename to src/muz/dl_sparse_table.h
diff --git a/src/muz_qe/dl_table.cpp b/src/muz/dl_table.cpp
similarity index 100%
rename from src/muz_qe/dl_table.cpp
rename to src/muz/dl_table.cpp
diff --git a/src/muz_qe/dl_table.h b/src/muz/dl_table.h
similarity index 100%
rename from src/muz_qe/dl_table.h
rename to src/muz/dl_table.h
diff --git a/src/muz_qe/dl_table_plugin.h b/src/muz/dl_table_plugin.h
similarity index 100%
rename from src/muz_qe/dl_table_plugin.h
rename to src/muz/dl_table_plugin.h
diff --git a/src/muz_qe/dl_table_relation.cpp b/src/muz/dl_table_relation.cpp
similarity index 100%
rename from src/muz_qe/dl_table_relation.cpp
rename to src/muz/dl_table_relation.cpp
diff --git a/src/muz_qe/dl_table_relation.h b/src/muz/dl_table_relation.h
similarity index 100%
rename from src/muz_qe/dl_table_relation.h
rename to src/muz/dl_table_relation.h
diff --git a/src/muz_qe/dl_util.cpp b/src/muz/dl_util.cpp
similarity index 83%
rename from src/muz_qe/dl_util.cpp
rename to src/muz/dl_util.cpp
index 1b1042345..0b88136e2 100644
--- a/src/muz_qe/dl_util.cpp
+++ b/src/muz/dl_util.cpp
@@ -40,118 +40,6 @@ namespace datalog {
ptr->deallocate();
}
- void flatten_and(expr_ref_vector& result) {
- ast_manager& m = result.get_manager();
- expr* e1, *e2, *e3;
- for (unsigned i = 0; i < result.size(); ++i) {
- if (m.is_and(result[i].get())) {
- app* a = to_app(result[i].get());
- unsigned num_args = a->get_num_args();
- for (unsigned j = 0; j < num_args; ++j) {
- result.push_back(a->get_arg(j));
- }
- result[i] = result.back();
- result.pop_back();
- --i;
- }
- else if (m.is_not(result[i].get(), e1) && m.is_not(e1, e2)) {
- result[i] = e2;
- --i;
- }
- else if (m.is_not(result[i].get(), e1) && m.is_or(e1)) {
- app* a = to_app(e1);
- unsigned num_args = a->get_num_args();
- for (unsigned j = 0; j < num_args; ++j) {
- result.push_back(m.mk_not(a->get_arg(j)));
- }
- result[i] = result.back();
- result.pop_back();
- --i;
- }
- else if (m.is_not(result[i].get(), e1) && m.is_implies(e1,e2,e3)) {
- result.push_back(e2);
- result[i] = m.mk_not(e3);
- --i;
- }
- else if (m.is_true(result[i].get()) ||
- (m.is_not(result[i].get(), e1) &&
- m.is_false(e1))) {
- result[i] = result.back();
- result.pop_back();
- --i;
- }
- else if (m.is_false(result[i].get()) ||
- (m.is_not(result[i].get(), e1) &&
- m.is_true(e1))) {
- result.reset();
- result.push_back(m.mk_false());
- return;
- }
- }
- }
-
- void flatten_and(expr* fml, expr_ref_vector& result) {
- SASSERT(result.get_manager().is_bool(fml));
- result.push_back(fml);
- flatten_and(result);
- }
-
- void flatten_or(expr_ref_vector& result) {
- ast_manager& m = result.get_manager();
- expr* e1, *e2, *e3;
- for (unsigned i = 0; i < result.size(); ++i) {
- if (m.is_or(result[i].get())) {
- app* a = to_app(result[i].get());
- unsigned num_args = a->get_num_args();
- for (unsigned j = 0; j < num_args; ++j) {
- result.push_back(a->get_arg(j));
- }
- result[i] = result.back();
- result.pop_back();
- --i;
- }
- else if (m.is_not(result[i].get(), e1) && m.is_not(e1, e2)) {
- result[i] = e2;
- --i;
- }
- else if (m.is_not(result[i].get(), e1) && m.is_and(e1)) {
- app* a = to_app(e1);
- unsigned num_args = a->get_num_args();
- for (unsigned j = 0; j < num_args; ++j) {
- result.push_back(m.mk_not(a->get_arg(j)));
- }
- result[i] = result.back();
- result.pop_back();
- --i;
- }
- else if (m.is_implies(result[i].get(),e2,e3)) {
- result.push_back(e3);
- result[i] = m.mk_not(e2);
- --i;
- }
- else if (m.is_false(result[i].get()) ||
- (m.is_not(result[i].get(), e1) &&
- m.is_true(e1))) {
- result[i] = result.back();
- result.pop_back();
- --i;
- }
- else if (m.is_true(result[i].get()) ||
- (m.is_not(result[i].get(), e1) &&
- m.is_false(e1))) {
- result.reset();
- result.push_back(m.mk_true());
- return;
- }
- }
- }
-
-
- void flatten_or(expr* fml, expr_ref_vector& result) {
- SASSERT(result.get_manager().is_bool(fml));
- result.push_back(fml);
- flatten_or(result);
- }
bool contains_var(expr * trm, unsigned var_idx) {
ptr_vector<sort> vars;
diff --git a/src/muz_qe/dl_util.h b/src/muz/dl_util.h
similarity index 98%
rename from src/muz_qe/dl_util.h
rename to src/muz/dl_util.h
index b92a33d1a..debb4d3e2 100644
--- a/src/muz_qe/dl_util.h
+++ b/src/muz/dl_util.h
@@ -30,6 +30,7 @@ Revision History:
#include"ast_counter.h"
#include"statistics.h"
#include"lbool.h"
+#include"qe_util.h"
namespace datalog {
@@ -107,18 +108,6 @@ namespace datalog {
typedef u_map<var *> varidx2var_map;
typedef obj_hashtable<func_decl> func_decl_set; //!< Rule dependencies.
typedef vector<std::string> string_vector;
-
-
- /**
- \brief Collect top-level conjunctions and disjunctions.
- */
- void flatten_and(expr_ref_vector& result);
-
- void flatten_and(expr* fml, expr_ref_vector& result);
-
- void flatten_or(expr_ref_vector& result);
-
- void flatten_or(expr* fml, expr_ref_vector& result);
bool contains_var(expr * trm, unsigned var_idx);
diff --git a/src/muz_qe/dl_vector_relation.h b/src/muz/dl_vector_relation.h
similarity index 100%
rename from src/muz_qe/dl_vector_relation.h
rename to src/muz/dl_vector_relation.h
diff --git a/src/muz_qe/equiv_proof_converter.cpp b/src/muz/equiv_proof_converter.cpp
similarity index 100%
rename from src/muz_qe/equiv_proof_converter.cpp
rename to src/muz/equiv_proof_converter.cpp
diff --git a/src/muz_qe/equiv_proof_converter.h b/src/muz/equiv_proof_converter.h
similarity index 100%
rename from src/muz_qe/equiv_proof_converter.h
rename to src/muz/equiv_proof_converter.h
diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz/fixedpoint_params.pyg
similarity index 100%
rename from src/muz_qe/fixedpoint_params.pyg
rename to src/muz/fixedpoint_params.pyg
diff --git a/src/muz_qe/heap_trie.h b/src/muz/heap_trie.h
similarity index 100%
rename from src/muz_qe/heap_trie.h
rename to src/muz/heap_trie.h
diff --git a/src/muz_qe/hilbert_basis.cpp b/src/muz/hilbert_basis.cpp
similarity index 100%
rename from src/muz_qe/hilbert_basis.cpp
rename to src/muz/hilbert_basis.cpp
diff --git a/src/muz_qe/hilbert_basis.h b/src/muz/hilbert_basis.h
similarity index 100%
rename from src/muz_qe/hilbert_basis.h
rename to src/muz/hilbert_basis.h
diff --git a/src/muz_qe/hnf.cpp b/src/muz/hnf.cpp
similarity index 99%
rename from src/muz_qe/hnf.cpp
rename to src/muz/hnf.cpp
index 36316cfa6..9d6f3c1ab 100644
--- a/src/muz_qe/hnf.cpp
+++ b/src/muz/hnf.cpp
@@ -214,7 +214,7 @@ private:
m_body.push_back(e1);
head = e2;
}
- datalog::flatten_and(m_body);
+ qe::flatten_and(m_body);
if (premise) {
p = m.mk_rewrite(fml0, mk_implies(m_body, head));
}
diff --git a/src/muz_qe/hnf.h b/src/muz/hnf.h
similarity index 100%
rename from src/muz_qe/hnf.h
rename to src/muz/hnf.h
diff --git a/src/muz_qe/horn_subsume_model_converter.cpp b/src/muz/horn_subsume_model_converter.cpp
similarity index 100%
rename from src/muz_qe/horn_subsume_model_converter.cpp
rename to src/muz/horn_subsume_model_converter.cpp
diff --git a/src/muz_qe/horn_subsume_model_converter.h b/src/muz/horn_subsume_model_converter.h
similarity index 100%
rename from src/muz_qe/horn_subsume_model_converter.h
rename to src/muz/horn_subsume_model_converter.h
diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz/horn_tactic.cpp
similarity index 99%
rename from src/muz_qe/horn_tactic.cpp
rename to src/muz/horn_tactic.cpp
index 1916839f4..07a0e2568 100644
--- a/src/muz_qe/horn_tactic.cpp
+++ b/src/muz/horn_tactic.cpp
@@ -141,7 +141,7 @@ class horn_tactic : public tactic {
expr_ref_vector args(m), body(m);
expr_ref head(m);
expr* a = 0, *a1 = 0;
- datalog::flatten_or(tmp, args);
+ qe::flatten_or(tmp, args);
for (unsigned i = 0; i < args.size(); ++i) {
a = args[i].get();
check_predicate(mark, a);
diff --git a/src/muz_qe/horn_tactic.h b/src/muz/horn_tactic.h
similarity index 100%
rename from src/muz_qe/horn_tactic.h
rename to src/muz/horn_tactic.h
diff --git a/src/muz_qe/model2expr.cpp b/src/muz/model2expr.cpp
similarity index 100%
rename from src/muz_qe/model2expr.cpp
rename to src/muz/model2expr.cpp
diff --git a/src/muz_qe/model2expr.h b/src/muz/model2expr.h
similarity index 100%
rename from src/muz_qe/model2expr.h
rename to src/muz/model2expr.h
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz/pdr_context.cpp
similarity index 99%
rename from src/muz_qe/pdr_context.cpp
rename to src/muz/pdr_context.cpp
index ff40be4f3..db85bc5a9 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz/pdr_context.cpp
@@ -45,6 +45,7 @@ Notes:
#include "smt_value_sort.h"
#include "proof_utils.h"
#include "dl_boogie_proof.h"
+#include "qe_util.h"
namespace pdr {
@@ -342,7 +343,7 @@ namespace pdr {
void pred_transformer::add_property(expr* lemma, unsigned lvl) {
expr_ref_vector lemmas(m);
- datalog::flatten_and(lemma, lemmas);
+ qe::flatten_and(lemma, lemmas);
for (unsigned i = 0; i < lemmas.size(); ++i) {
expr* lemma_i = lemmas[i].get();
if (add_property1(lemma_i, lvl)) {
@@ -587,7 +588,7 @@ namespace pdr {
for (unsigned i = ut_size; i < t_size; ++i) {
tail.push_back(rule.get_tail(i));
}
- datalog::flatten_and(tail);
+ qe::flatten_and(tail);
for (unsigned i = 0; i < tail.size(); ++i) {
expr_ref tmp(m);
var_subst(m, false)(tail[i].get(), var_reprs.size(), (expr*const*)var_reprs.c_ptr(), tmp);
@@ -778,7 +779,7 @@ namespace pdr {
ast_manager& m = pt().get_manager();
expr_ref_vector conjs(m);
obj_map<expr,expr*> model;
- datalog::flatten_and(state(), conjs);
+ qe::flatten_and(state(), conjs);
for (unsigned i = 0; i < conjs.size(); ++i) {
expr* e = conjs[i].get(), *e1, *e2;
if (m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) {
@@ -1979,7 +1980,7 @@ namespace pdr {
expr_ref_vector mdl(m), forms(m), Phi(m);
forms.push_back(T);
forms.push_back(phi);
- datalog::flatten_and(forms);
+ qe::flatten_and(forms);
ptr_vector<expr> forms1(forms.size(), forms.c_ptr());
if (use_model_generalizer) {
Phi.append(mev.minimize_model(forms1, M));
@@ -2035,7 +2036,7 @@ namespace pdr {
TRACE("pdr", tout << "Projected:\n" << mk_pp(phi1, m) << "\n";);
}
Phi.reset();
- datalog::flatten_and(phi1, Phi);
+ qe::flatten_and(phi1, Phi);
unsigned_vector indices;
vector<expr_ref_vector> child_states;
child_states.resize(preds.size(), expr_ref_vector(m));
diff --git a/src/muz_qe/pdr_context.h b/src/muz/pdr_context.h
similarity index 100%
rename from src/muz_qe/pdr_context.h
rename to src/muz/pdr_context.h
diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz/pdr_dl_interface.cpp
similarity index 100%
rename from src/muz_qe/pdr_dl_interface.cpp
rename to src/muz/pdr_dl_interface.cpp
diff --git a/src/muz_qe/pdr_dl_interface.h b/src/muz/pdr_dl_interface.h
similarity index 100%
rename from src/muz_qe/pdr_dl_interface.h
rename to src/muz/pdr_dl_interface.h
diff --git a/src/muz_qe/pdr_farkas_learner.cpp b/src/muz/pdr_farkas_learner.cpp
similarity index 99%
rename from src/muz_qe/pdr_farkas_learner.cpp
rename to src/muz/pdr_farkas_learner.cpp
index 8bc77ecc6..6202c913d 100644
--- a/src/muz_qe/pdr_farkas_learner.cpp
+++ b/src/muz/pdr_farkas_learner.cpp
@@ -320,7 +320,7 @@ namespace pdr {
expr_set bs;
expr_ref_vector blist(m_pr);
- datalog::flatten_and(B, blist);
+ qe::flatten_and(B, blist);
for (unsigned i = 0; i < blist.size(); ++i) {
bs.insert(blist[i].get());
}
diff --git a/src/muz_qe/pdr_farkas_learner.h b/src/muz/pdr_farkas_learner.h
similarity index 100%
rename from src/muz_qe/pdr_farkas_learner.h
rename to src/muz/pdr_farkas_learner.h
diff --git a/src/muz_qe/pdr_generalizers.cpp b/src/muz/pdr_generalizers.cpp
similarity index 99%
rename from src/muz_qe/pdr_generalizers.cpp
rename to src/muz/pdr_generalizers.cpp
index 8e15fa983..93a1c1844 100644
--- a/src/muz_qe/pdr_generalizers.cpp
+++ b/src/muz/pdr_generalizers.cpp
@@ -137,7 +137,7 @@ namespace pdr {
C = pm.mk_or(Bs);
TRACE("pdr", tout << "prop:\n" << mk_pp(A,m) << "\ngen:" << mk_pp(B, m) << "\nto: " << mk_pp(C, m) << "\n";);
core.reset();
- datalog::flatten_and(C, core);
+ qe::flatten_and(C, core);
uses_level = true;
}
}
@@ -157,7 +157,7 @@ namespace pdr {
}
void core_convex_hull_generalizer::operator()(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores) {
- // method3(n, core, uses_level, new_cores);
+ method3(n, core, uses_level, new_cores);
method1(n, core, uses_level, new_cores);
}
@@ -194,11 +194,11 @@ namespace pdr {
}
expr_ref fml = n.pt().get_formulas(n.level(), false);
expr_ref_vector fmls(m);
- datalog::flatten_and(fml, fmls);
+ qe::flatten_and(fml, fmls);
for (unsigned i = 0; i < fmls.size(); ++i) {
fml = m.mk_not(fmls[i].get());
core2.reset();
- datalog::flatten_and(fml, core2);
+ qe::flatten_and(fml, core2);
if (!mk_convex(core2, 1, conv2)) {
IF_VERBOSE(0, verbose_stream() << "Non-convex: " << mk_pp(pm.mk_and(core2), m) << "\n";);
continue;
@@ -332,7 +332,7 @@ namespace pdr {
for (unsigned i = 0; i < consequences.size(); ++i) {
es.reset();
tmp = m.mk_not(consequences[i].get());
- datalog::flatten_and(tmp, es);
+ qe::flatten_and(tmp, es);
if (!mk_convex(es, i, conv)) {
IF_VERBOSE(0, verbose_stream() << "Failed to create convex closure\n";);
return;
diff --git a/src/muz_qe/pdr_generalizers.h b/src/muz/pdr_generalizers.h
similarity index 100%
rename from src/muz_qe/pdr_generalizers.h
rename to src/muz/pdr_generalizers.h
diff --git a/src/muz_qe/pdr_manager.cpp b/src/muz/pdr_manager.cpp
similarity index 98%
rename from src/muz_qe/pdr_manager.cpp
rename to src/muz/pdr_manager.cpp
index 3e79e4f00..9eb10aba9 100644
--- a/src/muz_qe/pdr_manager.cpp
+++ b/src/muz/pdr_manager.cpp
@@ -56,7 +56,7 @@ namespace pdr {
expr_ref inductive_property::fixup_clause(expr* fml) const {
expr_ref_vector disjs(m);
- datalog::flatten_or(fml, disjs);
+ qe::flatten_or(fml, disjs);
expr_ref result(m);
bool_rewriter(m).mk_or(disjs.size(), disjs.c_ptr(), result);
return result;
@@ -65,7 +65,7 @@ namespace pdr {
expr_ref inductive_property::fixup_clauses(expr* fml) const {
expr_ref_vector conjs(m);
expr_ref result(m);
- datalog::flatten_and(fml, conjs);
+ qe::flatten_and(fml, conjs);
for (unsigned i = 0; i < conjs.size(); ++i) {
conjs[i] = fixup_clause(conjs[i].get());
}
@@ -238,7 +238,7 @@ namespace pdr {
expr_ref manager::mk_not_and(expr_ref_vector const& conjs) {
expr_ref result(m), e(m);
expr_ref_vector es(conjs);
- datalog::flatten_and(es);
+ qe::flatten_and(es);
for (unsigned i = 0; i < es.size(); ++i) {
m_brwr.mk_not(es[i].get(), e);
es[i] = e;
diff --git a/src/muz_qe/pdr_manager.h b/src/muz/pdr_manager.h
similarity index 100%
rename from src/muz_qe/pdr_manager.h
rename to src/muz/pdr_manager.h
diff --git a/src/muz_qe/pdr_prop_solver.cpp b/src/muz/pdr_prop_solver.cpp
similarity index 99%
rename from src/muz_qe/pdr_prop_solver.cpp
rename to src/muz/pdr_prop_solver.cpp
index eb3c0ee96..d9b22e04e 100644
--- a/src/muz_qe/pdr_prop_solver.cpp
+++ b/src/muz/pdr_prop_solver.cpp
@@ -76,7 +76,7 @@ namespace pdr {
}
void mk_safe(expr_ref_vector& conjs) {
- datalog::flatten_and(conjs);
+ qe::flatten_and(conjs);
expand_literals(conjs);
for (unsigned i = 0; i < conjs.size(); ++i) {
expr * lit = conjs[i].get();
diff --git a/src/muz_qe/pdr_prop_solver.h b/src/muz/pdr_prop_solver.h
similarity index 100%
rename from src/muz_qe/pdr_prop_solver.h
rename to src/muz/pdr_prop_solver.h
diff --git a/src/muz_qe/pdr_reachable_cache.cpp b/src/muz/pdr_reachable_cache.cpp
similarity index 100%
rename from src/muz_qe/pdr_reachable_cache.cpp
rename to src/muz/pdr_reachable_cache.cpp
diff --git a/src/muz_qe/pdr_reachable_cache.h b/src/muz/pdr_reachable_cache.h
similarity index 100%
rename from src/muz_qe/pdr_reachable_cache.h
rename to src/muz/pdr_reachable_cache.h
diff --git a/src/muz_qe/pdr_smt_context_manager.cpp b/src/muz/pdr_smt_context_manager.cpp
similarity index 100%
rename from src/muz_qe/pdr_smt_context_manager.cpp
rename to src/muz/pdr_smt_context_manager.cpp
diff --git a/src/muz_qe/pdr_smt_context_manager.h b/src/muz/pdr_smt_context_manager.h
similarity index 100%
rename from src/muz_qe/pdr_smt_context_manager.h
rename to src/muz/pdr_smt_context_manager.h
diff --git a/src/muz_qe/pdr_sym_mux.cpp b/src/muz/pdr_sym_mux.cpp
similarity index 100%
rename from src/muz_qe/pdr_sym_mux.cpp
rename to src/muz/pdr_sym_mux.cpp
diff --git a/src/muz_qe/pdr_sym_mux.h b/src/muz/pdr_sym_mux.h
similarity index 100%
rename from src/muz_qe/pdr_sym_mux.h
rename to src/muz/pdr_sym_mux.h
diff --git a/src/muz_qe/pdr_util.cpp b/src/muz/pdr_util.cpp
similarity index 99%
rename from src/muz_qe/pdr_util.cpp
rename to src/muz/pdr_util.cpp
index 3d93f8104..d23dc186e 100644
--- a/src/muz_qe/pdr_util.cpp
+++ b/src/muz/pdr_util.cpp
@@ -954,7 +954,7 @@ namespace pdr {
void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) {
ast_manager& m = fml.get_manager();
expr_ref_vector conjs(m);
- datalog::flatten_and(fml, conjs);
+ qe::flatten_and(fml, conjs);
obj_map<expr, unsigned> diseqs;
expr* n, *lhs, *rhs;
for (unsigned i = 0; i < conjs.size(); ++i) {
diff --git a/src/muz_qe/pdr_util.h b/src/muz/pdr_util.h
similarity index 100%
rename from src/muz_qe/pdr_util.h
rename to src/muz/pdr_util.h
diff --git a/src/muz_qe/proof_utils.cpp b/src/muz/proof_utils.cpp
similarity index 100%
rename from src/muz_qe/proof_utils.cpp
rename to src/muz/proof_utils.cpp
diff --git a/src/muz_qe/proof_utils.h b/src/muz/proof_utils.h
similarity index 100%
rename from src/muz_qe/proof_utils.h
rename to src/muz/proof_utils.h
diff --git a/src/muz_qe/rel_context.cpp b/src/muz/rel_context.cpp
similarity index 100%
rename from src/muz_qe/rel_context.cpp
rename to src/muz/rel_context.cpp
diff --git a/src/muz_qe/rel_context.h b/src/muz/rel_context.h
similarity index 100%
rename from src/muz_qe/rel_context.h
rename to src/muz/rel_context.h
diff --git a/src/muz_qe/replace_proof_converter.cpp b/src/muz/replace_proof_converter.cpp
similarity index 100%
rename from src/muz_qe/replace_proof_converter.cpp
rename to src/muz/replace_proof_converter.cpp
diff --git a/src/muz_qe/replace_proof_converter.h b/src/muz/replace_proof_converter.h
similarity index 100%
rename from src/muz_qe/replace_proof_converter.h
rename to src/muz/replace_proof_converter.h
diff --git a/src/muz_qe/skip_list_base.h b/src/muz/skip_list_base.h
similarity index 100%
rename from src/muz_qe/skip_list_base.h
rename to src/muz/skip_list_base.h
diff --git a/src/muz_qe/tab_context.cpp b/src/muz/tab_context.cpp
similarity index 99%
rename from src/muz_qe/tab_context.cpp
rename to src/muz/tab_context.cpp
index 4f4c14cc7..a56d16a0e 100644
--- a/src/muz_qe/tab_context.cpp
+++ b/src/muz/tab_context.cpp
@@ -208,7 +208,7 @@ namespace tb {
fmls.push_back(m_predicates[i]);
}
fmls.push_back(m_constraint);
- datalog::flatten_and(fmls);
+ qe::flatten_and(fmls);
bool_rewriter(m).mk_and(fmls.size(), fmls.c_ptr(), fml);
return fml;
}
@@ -337,7 +337,7 @@ namespace tb {
expr_ref tmp(m);
substitution subst(m);
subst.reserve(1, get_num_vars());
- datalog::flatten_and(m_constraint, fmls);
+ qe::flatten_and(m_constraint, fmls);
unsigned num_fmls = fmls.size();
for (unsigned i = 0; i < num_fmls; ++i) {
if (get_subst(rw, subst, i, fmls)) {
@@ -664,7 +664,7 @@ namespace tb {
m_qe(m_empty_set, false, fmls);
- datalog::flatten_and(fmls);
+ qe::flatten_and(fmls);
for (unsigned i = 0; i < fmls.size(); ++i) {
expr_ref n = normalize(fmls[i].get());
if (m_sat_lits.contains(n)) {
diff --git a/src/muz_qe/tab_context.h b/src/muz/tab_context.h
similarity index 100%
rename from src/muz_qe/tab_context.h
rename to src/muz/tab_context.h
diff --git a/src/muz_qe/unit_subsumption_tactic.cpp b/src/muz/unit_subsumption_tactic.cpp
similarity index 100%
rename from src/muz_qe/unit_subsumption_tactic.cpp
rename to src/muz/unit_subsumption_tactic.cpp
diff --git a/src/muz_qe/unit_subsumption_tactic.h b/src/muz/unit_subsumption_tactic.h
similarity index 100%
rename from src/muz_qe/unit_subsumption_tactic.h
rename to src/muz/unit_subsumption_tactic.h
diff --git a/src/muz_qe/vsubst_tactic.cpp b/src/muz/vsubst_tactic.cpp
similarity index 100%
rename from src/muz_qe/vsubst_tactic.cpp
rename to src/muz/vsubst_tactic.cpp
diff --git a/src/muz_qe/vsubst_tactic.h b/src/muz/vsubst_tactic.h
similarity index 100%
rename from src/muz_qe/vsubst_tactic.h
rename to src/muz/vsubst_tactic.h
diff --git a/src/muz_qe/nlarith_util.cpp b/src/qe/nlarith_util.cpp
similarity index 100%
rename from src/muz_qe/nlarith_util.cpp
rename to src/qe/nlarith_util.cpp
diff --git a/src/muz_qe/nlarith_util.h b/src/qe/nlarith_util.h
similarity index 100%
rename from src/muz_qe/nlarith_util.h
rename to src/qe/nlarith_util.h
diff --git a/src/muz_qe/qe.cpp b/src/qe/qe.cpp
similarity index 99%
rename from src/muz_qe/qe.cpp
rename to src/qe/qe.cpp
index 894a935b5..d0aafb896 100644
--- a/src/muz_qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -36,7 +36,7 @@ Revision History:
#include "expr_functors.h"
#include "quant_hoist.h"
#include "bool_rewriter.h"
-#include "dl_util.h"
+#include "qe_util.h"
#include "th_rewriter.h"
#include "smt_kernel.h"
#include "model_evaluator.h"
@@ -81,7 +81,7 @@ namespace qe {
ptr_vector<expr> todo;
ptr_vector<expr> conjs_closed, conjs_mixed, conjs_open;
- datalog::flatten_and(fml, conjs);
+ qe::flatten_and(fml, conjs);
for (unsigned i = 0; i < conjs.size(); ++i) {
todo.push_back(conjs[i].get());
@@ -306,7 +306,7 @@ namespace qe {
// conj_enum
conj_enum::conj_enum(ast_manager& m, expr* e): m(m), m_conjs(m) {
- datalog::flatten_and(e, m_conjs);
+ qe::flatten_and(e, m_conjs);
}
void conj_enum::extract_equalities(expr_ref_vector& eqs) {
diff --git a/src/muz_qe/qe.h b/src/qe/qe.h
similarity index 100%
rename from src/muz_qe/qe.h
rename to src/qe/qe.h
diff --git a/src/muz_qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp
similarity index 100%
rename from src/muz_qe/qe_arith_plugin.cpp
rename to src/qe/qe_arith_plugin.cpp
diff --git a/src/muz_qe/qe_array_plugin.cpp b/src/qe/qe_array_plugin.cpp
similarity index 100%
rename from src/muz_qe/qe_array_plugin.cpp
rename to src/qe/qe_array_plugin.cpp
diff --git a/src/muz_qe/qe_bool_plugin.cpp b/src/qe/qe_bool_plugin.cpp
similarity index 100%
rename from src/muz_qe/qe_bool_plugin.cpp
rename to src/qe/qe_bool_plugin.cpp
diff --git a/src/muz_qe/qe_bv_plugin.cpp b/src/qe/qe_bv_plugin.cpp
similarity index 100%
rename from src/muz_qe/qe_bv_plugin.cpp
rename to src/qe/qe_bv_plugin.cpp
diff --git a/src/muz_qe/qe_cmd.cpp b/src/qe/qe_cmd.cpp
similarity index 100%
rename from src/muz_qe/qe_cmd.cpp
rename to src/qe/qe_cmd.cpp
diff --git a/src/muz_qe/qe_cmd.h b/src/qe/qe_cmd.h
similarity index 100%
rename from src/muz_qe/qe_cmd.h
rename to src/qe/qe_cmd.h
diff --git a/src/muz_qe/qe_datatype_plugin.cpp b/src/qe/qe_datatype_plugin.cpp
similarity index 100%
rename from src/muz_qe/qe_datatype_plugin.cpp
rename to src/qe/qe_datatype_plugin.cpp
diff --git a/src/muz_qe/qe_dl_plugin.cpp b/src/qe/qe_dl_plugin.cpp
similarity index 100%
rename from src/muz_qe/qe_dl_plugin.cpp
rename to src/qe/qe_dl_plugin.cpp
diff --git a/src/muz_qe/qe_lite.cpp b/src/qe/qe_lite.cpp
similarity index 99%
rename from src/muz_qe/qe_lite.cpp
rename to src/qe/qe_lite.cpp
index 01537b574..130673527 100644
--- a/src/muz_qe/qe_lite.cpp
+++ b/src/qe/qe_lite.cpp
@@ -30,9 +30,8 @@ Revision History:
#include "bool_rewriter.h"
#include "var_subst.h"
#include "uint_set.h"
-#include "dl_util.h"
+#include "qe_util.h"
#include "th_rewriter.h"
-#include "dl_util.h"
#include "for_each_expr.h"
#include "expr_safe_replace.h"
#include "cooperate.h"
@@ -696,7 +695,7 @@ namespace eq {
m_subst(r, m_subst_map.size(), m_subst_map.c_ptr(), new_r);
m_rewriter(new_r);
conjs.reset();
- datalog::flatten_and(new_r, conjs);
+ qe::flatten_and(new_r, conjs);
reduced = true;
}
}
@@ -2387,7 +2386,7 @@ public:
void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml) {
expr_ref_vector disjs(m);
- datalog::flatten_or(fml, disjs);
+ qe::flatten_or(fml, disjs);
for (unsigned i = 0; i < disjs.size(); ++i) {
expr_ref_vector conjs(m);
conjs.push_back(disjs[i].get());
@@ -2400,7 +2399,7 @@ public:
void operator()(uint_set const& index_set, bool index_of_bound, expr_ref_vector& fmls) {
- datalog::flatten_and(fmls);
+ qe::flatten_and(fmls);
unsigned index;
if (has_unique_non_ground(fmls, index)) {
expr_ref fml(m);
diff --git a/src/muz_qe/qe_lite.h b/src/qe/qe_lite.h
similarity index 100%
rename from src/muz_qe/qe_lite.h
rename to src/qe/qe_lite.h
diff --git a/src/muz_qe/qe_sat_tactic.cpp b/src/qe/qe_sat_tactic.cpp
similarity index 100%
rename from src/muz_qe/qe_sat_tactic.cpp
rename to src/qe/qe_sat_tactic.cpp
diff --git a/src/muz_qe/qe_sat_tactic.h b/src/qe/qe_sat_tactic.h
similarity index 100%
rename from src/muz_qe/qe_sat_tactic.h
rename to src/qe/qe_sat_tactic.h
diff --git a/src/muz_qe/qe_tactic.cpp b/src/qe/qe_tactic.cpp
similarity index 100%
rename from src/muz_qe/qe_tactic.cpp
rename to src/qe/qe_tactic.cpp
diff --git a/src/muz_qe/qe_tactic.h b/src/qe/qe_tactic.h
similarity index 100%
rename from src/muz_qe/qe_tactic.h
rename to src/qe/qe_tactic.h
diff --git a/src/qe/qe_util.cpp b/src/qe/qe_util.cpp
new file mode 100644
index 000000000..629fe4b56
--- /dev/null
+++ b/src/qe/qe_util.cpp
@@ -0,0 +1,116 @@
+#include "qe_util.h"
+
+namespace qe {
+ void flatten_and(expr_ref_vector& result) {
+ ast_manager& m = result.get_manager();
+ expr* e1, *e2, *e3;
+ for (unsigned i = 0; i < result.size(); ++i) {
+ if (m.is_and(result[i].get())) {
+ app* a = to_app(result[i].get());
+ unsigned num_args = a->get_num_args();
+ for (unsigned j = 0; j < num_args; ++j) {
+ result.push_back(a->get_arg(j));
+ }
+ result[i] = result.back();
+ result.pop_back();
+ --i;
+ }
+ else if (m.is_not(result[i].get(), e1) && m.is_not(e1, e2)) {
+ result[i] = e2;
+ --i;
+ }
+ else if (m.is_not(result[i].get(), e1) && m.is_or(e1)) {
+ app* a = to_app(e1);
+ unsigned num_args = a->get_num_args();
+ for (unsigned j = 0; j < num_args; ++j) {
+ result.push_back(m.mk_not(a->get_arg(j)));
+ }
+ result[i] = result.back();
+ result.pop_back();
+ --i;
+ }
+ else if (m.is_not(result[i].get(), e1) && m.is_implies(e1,e2,e3)) {
+ result.push_back(e2);
+ result[i] = m.mk_not(e3);
+ --i;
+ }
+ else if (m.is_true(result[i].get()) ||
+ (m.is_not(result[i].get(), e1) &&
+ m.is_false(e1))) {
+ result[i] = result.back();
+ result.pop_back();
+ --i;
+ }
+ else if (m.is_false(result[i].get()) ||
+ (m.is_not(result[i].get(), e1) &&
+ m.is_true(e1))) {
+ result.reset();
+ result.push_back(m.mk_false());
+ return;
+ }
+ }
+ }
+
+ void flatten_and(expr* fml, expr_ref_vector& result) {
+ SASSERT(result.get_manager().is_bool(fml));
+ result.push_back(fml);
+ flatten_and(result);
+ }
+
+ void flatten_or(expr_ref_vector& result) {
+ ast_manager& m = result.get_manager();
+ expr* e1, *e2, *e3;
+ for (unsigned i = 0; i < result.size(); ++i) {
+ if (m.is_or(result[i].get())) {
+ app* a = to_app(result[i].get());
+ unsigned num_args = a->get_num_args();
+ for (unsigned j = 0; j < num_args; ++j) {
+ result.push_back(a->get_arg(j));
+ }
+ result[i] = result.back();
+ result.pop_back();
+ --i;
+ }
+ else if (m.is_not(result[i].get(), e1) && m.is_not(e1, e2)) {
+ result[i] = e2;
+ --i;
+ }
+ else if (m.is_not(result[i].get(), e1) && m.is_and(e1)) {
+ app* a = to_app(e1);
+ unsigned num_args = a->get_num_args();
+ for (unsigned j = 0; j < num_args; ++j) {
+ result.push_back(m.mk_not(a->get_arg(j)));
+ }
+ result[i] = result.back();
+ result.pop_back();
+ --i;
+ }
+ else if (m.is_implies(result[i].get(),e2,e3)) {
+ result.push_back(e3);
+ result[i] = m.mk_not(e2);
+ --i;
+ }
+ else if (m.is_false(result[i].get()) ||
+ (m.is_not(result[i].get(), e1) &&
+ m.is_true(e1))) {
+ result[i] = result.back();
+ result.pop_back();
+ --i;
+ }
+ else if (m.is_true(result[i].get()) ||
+ (m.is_not(result[i].get(), e1) &&
+ m.is_false(e1))) {
+ result.reset();
+ result.push_back(m.mk_true());
+ return;
+ }
+ }
+ }
+
+
+ void flatten_or(expr* fml, expr_ref_vector& result) {
+ SASSERT(result.get_manager().is_bool(fml));
+ result.push_back(fml);
+ flatten_or(result);
+ }
+}
diff --git a/src/qe/qe_util.h b/src/qe/qe_util.h
new file mode 100644
index 000000000..7e1fe7f79
--- /dev/null
+++ b/src/qe/qe_util.h
@@ -0,0 +1,37 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+ qe_util.h
+
+Abstract:
+
+ Utilities for quantifiers.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2013-08-28
+
+Revision History:
+
+--*/
+#ifndef _QE_UTIL_H_
+#define _QE_UTIL_H_
+
+#include "ast.h"
+
+namespace qe {
+ /**
+ \brief Collect top-level conjunctions and disjunctions.
+ */
+ void flatten_and(expr_ref_vector& result);
+
+ void flatten_and(expr* fml, expr_ref_vector& result);
+
+ void flatten_or(expr_ref_vector& result);
+
+ void flatten_or(expr* fml, expr_ref_vector& result);
+
+}
+#endif