From 12a255e36be1753a5675babd35f89ad4c6293013 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 24 Oct 2012 14:47:40 -0700 Subject: [PATCH] reorganizing the code Signed-off-by: Leonardo de Moura --- scripts/mk_make.py | 7 +- src/{ => api}/dll/dll.cpp | 0 src/{ => api}/dll/dll.rc | 0 src/{ => api}/dll/dll.vcxproj | 0 src/{ => api}/dll/resource.h | 0 src/{ => api}/dll/z3.def | 0 src/api/smtlib_solver.cpp | 1 - src/api/smtparser.cpp | 174 ----------------- src/{ => ast}/normal_forms/cnf.cpp | 0 src/{ => ast}/normal_forms/cnf.h | 0 src/{ => ast}/normal_forms/defined_names.cpp | 0 src/{ => ast}/normal_forms/defined_names.h | 0 src/{ => ast}/normal_forms/elim_term_ite.cpp | 0 src/{ => ast}/normal_forms/elim_term_ite.h | 0 src/{ => ast}/normal_forms/name_exprs.cpp | 0 src/{ => ast}/normal_forms/name_exprs.h | 0 src/{ => ast}/normal_forms/nnf.cpp | 2 - src/{ => ast}/normal_forms/nnf.h | 6 - src/{ => ast}/normal_forms/pull_quant.cpp | 0 src/{ => ast}/normal_forms/pull_quant.h | 0 src/ast/proof_checker/proof_checker.cpp | 10 +- src/ast/proof_checker/proof_checker.h | 2 +- src/{ => bindings}/dotnet/Microsoft.Z3/AST.cs | 0 .../dotnet/Microsoft.Z3/ASTMap.cs | 0 .../dotnet/Microsoft.Z3/ASTVector.cs | 0 .../dotnet/Microsoft.Z3/ApplyResult.cs | 0 .../dotnet/Microsoft.Z3/Constructor.cs | 0 .../dotnet/Microsoft.Z3/Context.cs | 0 .../dotnet/Microsoft.Z3/DecRefQUeue.cs | 0 .../dotnet/Microsoft.Z3/Enumerations.cs | 0 .../dotnet/Microsoft.Z3/Expr.cs | 0 .../dotnet/Microsoft.Z3/Fixedpoint.cs | 0 .../dotnet/Microsoft.Z3/FuncDecl.cs | 0 .../dotnet/Microsoft.Z3/FuncInterp.cs | 0 .../dotnet/Microsoft.Z3/Goal.cs | 0 src/{ => bindings}/dotnet/Microsoft.Z3/Log.cs | 0 .../dotnet/Microsoft.Z3/Microsoft.Z3.csproj | 0 .../Microsoft.Z3/Microsoft.Z3_35.csproj | 0 .../dotnet/Microsoft.Z3/Model.cs | 0 .../dotnet/Microsoft.Z3/Native.cs | 0 .../dotnet/Microsoft.Z3/Numeral.cs | 0 .../dotnet/Microsoft.Z3/ParamDescrs.cs | 0 .../dotnet/Microsoft.Z3/Params.cs | 0 .../dotnet/Microsoft.Z3/Pattern.cs | 0 .../dotnet/Microsoft.Z3/Probe.cs | 0 .../Microsoft.Z3/Properties/AssemblyInfo.cs | 0 .../dotnet/Microsoft.Z3/Quantifier.cs | 0 .../dotnet/Microsoft.Z3/Solver.cs | 0 .../dotnet/Microsoft.Z3/Sort.cs | 0 .../dotnet/Microsoft.Z3/Statistics.cs | 0 .../dotnet/Microsoft.Z3/Status.cs | 0 .../dotnet/Microsoft.Z3/Symbol.cs | 0 .../dotnet/Microsoft.Z3/Tactic.cs | 0 .../dotnet/Microsoft.Z3/Version.cs | 0 .../dotnet/Microsoft.Z3/Z3Exception.cs | 0 .../dotnet/Microsoft.Z3/Z3Object.cs | 0 .../dotnet/Microsoft.Z3V3/AssemblyInfo.cpp | 0 .../dotnet/Microsoft.Z3V3/Microsoft.Z3V3.cpp | 0 .../dotnet/Microsoft.Z3V3/Microsoft.Z3V3.h | 0 .../Microsoft.Z3V3/Microsoft.Z3V3.vcxproj | 0 src/{ => bindings}/ml/README-linux | 0 src/{ => bindings}/ml/README-osx | 0 src/{ => bindings}/ml/README-test-linux | 0 src/{ => bindings}/ml/README-test-osx | 0 src/{ => bindings}/ml/README-test-win | 0 src/{ => bindings}/ml/README-win | 0 .../ml/add_error_checking.V3.sed | 0 src/{ => bindings}/ml/add_error_checking.sed | 0 src/{ => bindings}/ml/build-lib.cmd | 0 src/{ => bindings}/ml/build-lib.sh | 0 src/{ => bindings}/ml/build-test.cmd | 0 src/{ => bindings}/ml/build-test.sh | 0 src/{ => bindings}/ml/build.cmd | 0 src/{ => bindings}/ml/build.sed | 0 src/{ => bindings}/ml/clean.cmd | 0 src/{ => bindings}/ml/cleantmp.cmd | 0 src/{ => bindings}/ml/compile_mlapi.cmd | 0 src/{ => bindings}/ml/error_handling.idl | 0 src/{ => bindings}/ml/exec.cmd | 0 src/{ => bindings}/ml/exec.sh | 0 src/{ => bindings}/ml/generate_mlapi.cmd | 0 src/{ => bindings}/ml/import.cmd | 0 src/{ => bindings}/ml/mlx_get_app_args.idl | 0 src/{ => bindings}/ml/mlx_get_array_sort.idl | 0 .../ml/mlx_get_datatype_sort.idl | 0 src/{ => bindings}/ml/mlx_get_domains.idl | 0 src/{ => bindings}/ml/mlx_get_error_msg.idl | 0 .../ml/mlx_get_pattern_terms.idl | 0 src/{ => bindings}/ml/mlx_get_tuple_sort.idl | 0 src/{ => bindings}/ml/mlx_mk_context_x.idl | 0 src/{ => bindings}/ml/mlx_mk_datatypes.idl | 0 src/{ => bindings}/ml/mlx_mk_numeral.idl | 0 src/{ => bindings}/ml/mlx_mk_sort.idl | 0 src/{ => bindings}/ml/mlx_mk_symbol.idl | 0 src/{ => bindings}/ml/mlx_model.idl | 0 src/{ => bindings}/ml/mlx_numeral_refine.idl | 0 src/{ => bindings}/ml/mlx_parse_smtlib.idl | 0 src/{ => bindings}/ml/mlx_sort_refine.idl | 0 src/{ => bindings}/ml/mlx_statistics.idl | 0 src/{ => bindings}/ml/mlx_symbol_refine.idl | 0 src/{ => bindings}/ml/mlx_term_refine.idl | 0 src/{ => bindings}/ml/queen.ml | 0 src/{ => bindings}/ml/queen.regress.err | 0 src/{ => bindings}/ml/queen.regress.out | 0 src/{ => bindings}/ml/test_capi.regress.err | 0 src/{ => bindings}/ml/test_capi.regress.out | 0 src/{ => bindings}/ml/test_mlapi.cmd | 0 src/{ => bindings}/ml/test_mlapi.ml | 0 src/{ => bindings}/ml/test_mlapi.regress.err | 0 src/{ => bindings}/ml/test_mlapi.regress.out | 0 src/{ => bindings}/ml/test_mlapiV3.ml | 0 .../ml/test_mlapiV3.regress.err | 0 .../ml/test_mlapiV3.regress.out | 0 src/{ => bindings}/ml/test_theory.ml | 0 src/{ => bindings}/ml/update-ml-doc.cmd | 0 src/{ => bindings}/ml/x3.ml | 0 src/{ => bindings}/ml/x3V3.ml | 0 src/{ => bindings}/ml/x3V3.mli | 0 src/{ => bindings}/ml/z3.idl | 0 src/{ => bindings}/ml/z3.ml | 0 src/{ => bindings}/ml/z3.mli | 0 src/{ => bindings}/ml/z3_stubs.c | 0 src/{ => bindings}/ml/z3_theory_stubs.c | 0 src/{ => bindings}/python/README.txt | 0 src/{ => bindings}/python/example.py | 0 src/{ => bindings}/python/z3.py | 0 src/{ => bindings}/python/z3consts.py | 0 src/{ => bindings}/python/z3core.py | 0 src/{ => bindings}/python/z3poly.py | 0 src/{ => bindings}/python/z3printer.py | 0 src/{ => bindings}/python/z3tactics.py | 0 src/{ => bindings}/python/z3test.py | 0 src/{ => bindings}/python/z3types.py | 0 src/{ => dead}/spc/README | 0 src/{ => dead}/spc/fvi.h | 0 src/{ => dead}/spc/fvi_def.h | 0 src/{ => dead}/spc/kbo.cpp | 0 src/{ => dead}/spc/kbo.h | 0 src/{ => dead}/spc/lpo.cpp | 0 src/{ => dead}/spc/lpo.h | 0 src/{ => dead}/spc/marker.h | 0 src/{ => dead}/spc/normalize_vars.cpp | 0 src/{ => dead}/spc/normalize_vars.h | 0 src/{ => dead}/spc/order.cpp | 0 src/{ => dead}/spc/order.h | 0 src/{ => dead}/spc/precedence.cpp | 0 src/{ => dead}/spc/precedence.h | 0 src/{ => dead}/spc/preprocessor.cpp | 0 src/{ => dead}/spc/preprocessor.h | 0 src/{ => dead}/spc/sparse_use_list.h | 0 src/{ => dead}/spc/spc_asserted_literals.cpp | 0 src/{ => dead}/spc/spc_asserted_literals.h | 0 src/{ => dead}/spc/spc_clause.cpp | 0 src/{ => dead}/spc/spc_clause.h | 0 src/{ => dead}/spc/spc_clause_pos_set.h | 0 src/{ => dead}/spc/spc_clause_selection.cpp | 0 src/{ => dead}/spc/spc_clause_selection.h | 0 src/{ => dead}/spc/spc_context.cpp | 0 src/{ => dead}/spc/spc_context.h | 0 src/{ => dead}/spc/spc_decl_plugin.cpp | 0 src/{ => dead}/spc/spc_decl_plugin.h | 0 src/{ => dead}/spc/spc_der.cpp | 0 src/{ => dead}/spc/spc_der.h | 0 src/{ => dead}/spc/spc_eq_resolution.cpp | 0 src/{ => dead}/spc/spc_eq_resolution.h | 0 src/{ => dead}/spc/spc_factoring.cpp | 0 src/{ => dead}/spc/spc_factoring.h | 0 src/{ => dead}/spc/spc_justification.cpp | 0 src/{ => dead}/spc/spc_justification.h | 0 src/{ => dead}/spc/spc_literal.cpp | 0 src/{ => dead}/spc/spc_literal.h | 0 src/{ => dead}/spc/spc_literal_selection.cpp | 0 src/{ => dead}/spc/spc_literal_selection.h | 0 src/{ => dead}/spc/spc_prover.cpp | 0 src/{ => dead}/spc/spc_prover.h | 0 src/{ => dead}/spc/spc_rewriter.cpp | 0 src/{ => dead}/spc/spc_rewriter.h | 0 src/{ => dead}/spc/spc_semantic_tautology.cpp | 0 src/{ => dead}/spc/spc_semantic_tautology.h | 0 src/{ => dead}/spc/spc_statistics.cpp | 0 src/{ => dead}/spc/spc_statistics.h | 0 src/{ => dead}/spc/spc_subsumption.cpp | 0 src/{ => dead}/spc/spc_subsumption.h | 0 src/{ => dead}/spc/spc_superposition.cpp | 0 src/{ => dead}/spc/spc_superposition.h | 0 src/{ => dead}/spc/spc_unary_inference.cpp | 0 src/{ => dead}/spc/spc_unary_inference.h | 0 src/{ => dead}/spc/splay_tree.h | 0 src/{ => dead}/spc/splay_tree_def.h | 0 src/{ => dead}/spc/splay_tree_map.h | 0 src/{ => dead}/spc/use_list.cpp | 0 src/{ => dead}/spc/use_list.h | 0 src/test/fvi.cpp | 158 ---------------- src/test/main.cpp | 2 - src/test/splay_tree.cpp | 175 ------------------ 195 files changed, 11 insertions(+), 526 deletions(-) rename src/{ => api}/dll/dll.cpp (100%) rename src/{ => api}/dll/dll.rc (100%) rename src/{ => api}/dll/dll.vcxproj (100%) rename src/{ => api}/dll/resource.h (100%) rename src/{ => api}/dll/z3.def (100%) rename src/{ => ast}/normal_forms/cnf.cpp (100%) rename src/{ => ast}/normal_forms/cnf.h (100%) rename src/{ => ast}/normal_forms/defined_names.cpp (100%) rename src/{ => ast}/normal_forms/defined_names.h (100%) rename src/{ => ast}/normal_forms/elim_term_ite.cpp (100%) rename src/{ => ast}/normal_forms/elim_term_ite.h (100%) rename src/{ => ast}/normal_forms/name_exprs.cpp (100%) rename src/{ => ast}/normal_forms/name_exprs.h (100%) rename src/{ => ast}/normal_forms/nnf.cpp (99%) rename src/{ => ast}/normal_forms/nnf.h (85%) rename src/{ => ast}/normal_forms/pull_quant.cpp (100%) rename src/{ => ast}/normal_forms/pull_quant.h (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/AST.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/ASTMap.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/ASTVector.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/ApplyResult.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Constructor.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Context.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/DecRefQUeue.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Enumerations.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Expr.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Fixedpoint.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/FuncDecl.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/FuncInterp.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Goal.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Log.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Microsoft.Z3.csproj (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Microsoft.Z3_35.csproj (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Model.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Native.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Numeral.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/ParamDescrs.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Params.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Pattern.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Probe.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Properties/AssemblyInfo.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Quantifier.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Solver.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Sort.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Statistics.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Status.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Symbol.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Tactic.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Version.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Z3Exception.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3/Z3Object.cs (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3V3/AssemblyInfo.cpp (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3V3/Microsoft.Z3V3.cpp (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3V3/Microsoft.Z3V3.h (100%) rename src/{ => bindings}/dotnet/Microsoft.Z3V3/Microsoft.Z3V3.vcxproj (100%) rename src/{ => bindings}/ml/README-linux (100%) rename src/{ => bindings}/ml/README-osx (100%) rename src/{ => bindings}/ml/README-test-linux (100%) rename src/{ => bindings}/ml/README-test-osx (100%) rename src/{ => bindings}/ml/README-test-win (100%) rename src/{ => bindings}/ml/README-win (100%) rename src/{ => bindings}/ml/add_error_checking.V3.sed (100%) rename src/{ => bindings}/ml/add_error_checking.sed (100%) rename src/{ => bindings}/ml/build-lib.cmd (100%) rename src/{ => bindings}/ml/build-lib.sh (100%) rename src/{ => bindings}/ml/build-test.cmd (100%) rename src/{ => bindings}/ml/build-test.sh (100%) rename src/{ => bindings}/ml/build.cmd (100%) rename src/{ => bindings}/ml/build.sed (100%) rename src/{ => bindings}/ml/clean.cmd (100%) rename src/{ => bindings}/ml/cleantmp.cmd (100%) rename src/{ => bindings}/ml/compile_mlapi.cmd (100%) rename src/{ => bindings}/ml/error_handling.idl (100%) rename src/{ => bindings}/ml/exec.cmd (100%) rename src/{ => bindings}/ml/exec.sh (100%) rename src/{ => bindings}/ml/generate_mlapi.cmd (100%) rename src/{ => bindings}/ml/import.cmd (100%) rename src/{ => bindings}/ml/mlx_get_app_args.idl (100%) rename src/{ => bindings}/ml/mlx_get_array_sort.idl (100%) rename src/{ => bindings}/ml/mlx_get_datatype_sort.idl (100%) rename src/{ => bindings}/ml/mlx_get_domains.idl (100%) rename src/{ => bindings}/ml/mlx_get_error_msg.idl (100%) rename src/{ => bindings}/ml/mlx_get_pattern_terms.idl (100%) rename src/{ => bindings}/ml/mlx_get_tuple_sort.idl (100%) rename src/{ => bindings}/ml/mlx_mk_context_x.idl (100%) rename src/{ => bindings}/ml/mlx_mk_datatypes.idl (100%) rename src/{ => bindings}/ml/mlx_mk_numeral.idl (100%) rename src/{ => bindings}/ml/mlx_mk_sort.idl (100%) rename src/{ => bindings}/ml/mlx_mk_symbol.idl (100%) rename src/{ => bindings}/ml/mlx_model.idl (100%) rename src/{ => bindings}/ml/mlx_numeral_refine.idl (100%) rename src/{ => bindings}/ml/mlx_parse_smtlib.idl (100%) rename src/{ => bindings}/ml/mlx_sort_refine.idl (100%) rename src/{ => bindings}/ml/mlx_statistics.idl (100%) rename src/{ => bindings}/ml/mlx_symbol_refine.idl (100%) rename src/{ => bindings}/ml/mlx_term_refine.idl (100%) rename src/{ => bindings}/ml/queen.ml (100%) rename src/{ => bindings}/ml/queen.regress.err (100%) rename src/{ => bindings}/ml/queen.regress.out (100%) rename src/{ => bindings}/ml/test_capi.regress.err (100%) rename src/{ => bindings}/ml/test_capi.regress.out (100%) rename src/{ => bindings}/ml/test_mlapi.cmd (100%) rename src/{ => bindings}/ml/test_mlapi.ml (100%) rename src/{ => bindings}/ml/test_mlapi.regress.err (100%) rename src/{ => bindings}/ml/test_mlapi.regress.out (100%) rename src/{ => bindings}/ml/test_mlapiV3.ml (100%) rename src/{ => bindings}/ml/test_mlapiV3.regress.err (100%) rename src/{ => bindings}/ml/test_mlapiV3.regress.out (100%) rename src/{ => bindings}/ml/test_theory.ml (100%) rename src/{ => bindings}/ml/update-ml-doc.cmd (100%) rename src/{ => bindings}/ml/x3.ml (100%) rename src/{ => bindings}/ml/x3V3.ml (100%) rename src/{ => bindings}/ml/x3V3.mli (100%) rename src/{ => bindings}/ml/z3.idl (100%) rename src/{ => bindings}/ml/z3.ml (100%) rename src/{ => bindings}/ml/z3.mli (100%) rename src/{ => bindings}/ml/z3_stubs.c (100%) rename src/{ => bindings}/ml/z3_theory_stubs.c (100%) rename src/{ => bindings}/python/README.txt (100%) rename src/{ => bindings}/python/example.py (100%) rename src/{ => bindings}/python/z3.py (100%) rename src/{ => bindings}/python/z3consts.py (100%) rename src/{ => bindings}/python/z3core.py (100%) rename src/{ => bindings}/python/z3poly.py (100%) rename src/{ => bindings}/python/z3printer.py (100%) rename src/{ => bindings}/python/z3tactics.py (100%) rename src/{ => bindings}/python/z3test.py (100%) rename src/{ => bindings}/python/z3types.py (100%) rename src/{ => dead}/spc/README (100%) rename src/{ => dead}/spc/fvi.h (100%) rename src/{ => dead}/spc/fvi_def.h (100%) rename src/{ => dead}/spc/kbo.cpp (100%) rename src/{ => dead}/spc/kbo.h (100%) rename src/{ => dead}/spc/lpo.cpp (100%) rename src/{ => dead}/spc/lpo.h (100%) rename src/{ => dead}/spc/marker.h (100%) rename src/{ => dead}/spc/normalize_vars.cpp (100%) rename src/{ => dead}/spc/normalize_vars.h (100%) rename src/{ => dead}/spc/order.cpp (100%) rename src/{ => dead}/spc/order.h (100%) rename src/{ => dead}/spc/precedence.cpp (100%) rename src/{ => dead}/spc/precedence.h (100%) rename src/{ => dead}/spc/preprocessor.cpp (100%) rename src/{ => dead}/spc/preprocessor.h (100%) rename src/{ => dead}/spc/sparse_use_list.h (100%) rename src/{ => dead}/spc/spc_asserted_literals.cpp (100%) rename src/{ => dead}/spc/spc_asserted_literals.h (100%) rename src/{ => dead}/spc/spc_clause.cpp (100%) rename src/{ => dead}/spc/spc_clause.h (100%) rename src/{ => dead}/spc/spc_clause_pos_set.h (100%) rename src/{ => dead}/spc/spc_clause_selection.cpp (100%) rename src/{ => dead}/spc/spc_clause_selection.h (100%) rename src/{ => dead}/spc/spc_context.cpp (100%) rename src/{ => dead}/spc/spc_context.h (100%) rename src/{ => dead}/spc/spc_decl_plugin.cpp (100%) rename src/{ => dead}/spc/spc_decl_plugin.h (100%) rename src/{ => dead}/spc/spc_der.cpp (100%) rename src/{ => dead}/spc/spc_der.h (100%) rename src/{ => dead}/spc/spc_eq_resolution.cpp (100%) rename src/{ => dead}/spc/spc_eq_resolution.h (100%) rename src/{ => dead}/spc/spc_factoring.cpp (100%) rename src/{ => dead}/spc/spc_factoring.h (100%) rename src/{ => dead}/spc/spc_justification.cpp (100%) rename src/{ => dead}/spc/spc_justification.h (100%) rename src/{ => dead}/spc/spc_literal.cpp (100%) rename src/{ => dead}/spc/spc_literal.h (100%) rename src/{ => dead}/spc/spc_literal_selection.cpp (100%) rename src/{ => dead}/spc/spc_literal_selection.h (100%) rename src/{ => dead}/spc/spc_prover.cpp (100%) rename src/{ => dead}/spc/spc_prover.h (100%) rename src/{ => dead}/spc/spc_rewriter.cpp (100%) rename src/{ => dead}/spc/spc_rewriter.h (100%) rename src/{ => dead}/spc/spc_semantic_tautology.cpp (100%) rename src/{ => dead}/spc/spc_semantic_tautology.h (100%) rename src/{ => dead}/spc/spc_statistics.cpp (100%) rename src/{ => dead}/spc/spc_statistics.h (100%) rename src/{ => dead}/spc/spc_subsumption.cpp (100%) rename src/{ => dead}/spc/spc_subsumption.h (100%) rename src/{ => dead}/spc/spc_superposition.cpp (100%) rename src/{ => dead}/spc/spc_superposition.h (100%) rename src/{ => dead}/spc/spc_unary_inference.cpp (100%) rename src/{ => dead}/spc/spc_unary_inference.h (100%) rename src/{ => dead}/spc/splay_tree.h (100%) rename src/{ => dead}/spc/splay_tree_def.h (100%) rename src/{ => dead}/spc/splay_tree_map.h (100%) rename src/{ => dead}/spc/use_list.cpp (100%) rename src/{ => dead}/spc/use_list.h (100%) delete mode 100644 src/test/fvi.cpp delete mode 100644 src/test/splay_tree.cpp diff --git a/scripts/mk_make.py b/scripts/mk_make.py index 3af14b8cb..7bea93605 100644 --- a/scripts/mk_make.py +++ b/scripts/mk_make.py @@ -13,7 +13,6 @@ parse_options() add_lib('util', []) add_lib('polynomial', ['util'], 'math/polynomial') add_lib('sat', ['util']) -# nlsat only reuses the file sat_types.h from sat add_lib('nlsat', ['polynomial', 'sat']) add_lib('subpaving', ['util'], 'math/subpaving') add_lib('ast', ['util', 'polynomial']) @@ -32,15 +31,14 @@ add_lib('tactic', ['ast', 'model']) add_lib('old_params', ['model', 'simplifier']) add_lib('cmd_context', ['tactic', 'rewriter', 'model', 'old_params', 'simplifier']) add_lib('substitution', ['ast'], 'ast/substitution') -add_lib('normal_forms', ['tactic', 'old_params']) +add_lib('normal_forms', ['rewriter', 'old_params'], 'ast/normal_forms') add_lib('pattern', ['normal_forms'], 'ast/pattern') -add_lib('spc', ['simplifier', 'substitution', 'old_params', 'pattern']) add_lib('parser_util', ['ast']) add_lib('smt2parser', ['cmd_context', 'parser_util']) add_lib('macros', ['simplifier', 'old_params'], 'ast/macros') add_lib('grobner', ['ast'], 'math/grobner') add_lib('euclid', ['util'], 'math/euclid') -add_lib('proof_checker', ['rewriter', 'spc'], 'ast/proof_checker') +add_lib('proof_checker', ['rewriter', 'old_params'], 'ast/proof_checker') add_lib('bit_blaster', ['rewriter', 'simplifier', 'old_params', 'tactic'], 'tactic/bit_blaster') add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util']) @@ -60,7 +58,6 @@ add_lib('aig', ['tactic'], 'tactic/aig') # 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']) add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig', 'muz_qe'], 'tactic/smtlogic_tactics') -# TODO: rewrite ufbv_strategy as a tactic and move to smtlogic_tactics. add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv_tactic') add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig', 'muz_qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') # TODO: delete SMT 1.0 frontend diff --git a/src/dll/dll.cpp b/src/api/dll/dll.cpp similarity index 100% rename from src/dll/dll.cpp rename to src/api/dll/dll.cpp diff --git a/src/dll/dll.rc b/src/api/dll/dll.rc similarity index 100% rename from src/dll/dll.rc rename to src/api/dll/dll.rc diff --git a/src/dll/dll.vcxproj b/src/api/dll/dll.vcxproj similarity index 100% rename from src/dll/dll.vcxproj rename to src/api/dll/dll.vcxproj diff --git a/src/dll/resource.h b/src/api/dll/resource.h similarity index 100% rename from src/dll/resource.h rename to src/api/dll/resource.h diff --git a/src/dll/z3.def b/src/api/dll/z3.def similarity index 100% rename from src/dll/z3.def rename to src/api/dll/z3.def diff --git a/src/api/smtlib_solver.cpp b/src/api/smtlib_solver.cpp index d268d7ac2..1aff13a3d 100644 --- a/src/api/smtlib_solver.cpp +++ b/src/api/smtlib_solver.cpp @@ -23,7 +23,6 @@ Revision History: #include"ast_pp.h" #include"ast_ll_pp.h" #include"well_sorted.h" -#include"spc_prover.h" #include"model.h" #include"model_v2_pp.h" #include"solver.h" diff --git a/src/api/smtparser.cpp b/src/api/smtparser.cpp index 04f9ba619..ea073ea5e 100644 --- a/src/api/smtparser.cpp +++ b/src/api/smtparser.cpp @@ -37,9 +37,6 @@ Revision History: #include"error_codes.h" #include"pattern_validation.h" #include"unifier.h" -#include"kbo.h" -#include"lpo.h" -#include"substitution_tree.h" #include"timeit.h" #include"var_subst.h" #include"well_sorted.h" @@ -2261,23 +2258,6 @@ private: symbol datatypes("datatypes"); symbol unify("unify"); symbol unify_fail("unify-fail"); -#if !defined(SMTCOMP) && !defined(_EXTERNAL_RELEASE) - symbol kbo_lt("kbo_lt"); - symbol kbo_gt("kbo_gt"); - symbol kbo_eq("kbo_eq"); - symbol kbo_un("kbo_un"); - symbol lpo_lt("lpo_lt"); - symbol lpo_gt("lpo_gt"); - symbol lpo_eq("lpo_eq"); - symbol lpo_un("lpo_un"); - symbol st_insert("st_insert"); - symbol st_erase("st_erase"); - symbol st_reset("st_reset"); - symbol st_unify("st_unify"); - symbol st_inst("st_inst"); - symbol st_gen("st_gen"); - symbol st_display("st_display"); -#endif symbol assumption("assumption"); symbol assumption_core("assumption-core"); symbol define_sorts_sym("define_sorts"); @@ -2427,46 +2407,6 @@ private: ++proto_exprs; continue; } -#if !defined(SMTCOMP) && !defined(_EXTERNAL_RELEASE) - if ((kbo_lt == e->string() || kbo_gt == e->string() || kbo_eq == e->string() || kbo_un == e->string()) && e1) { - if (!test_kbo(e1, e->string())) { - return false; - } - ++proto_exprs; - continue; - } - if ((lpo_lt == e->string() || lpo_gt == e->string() || lpo_eq == e->string() || lpo_un == e->string()) && e1) { - if (!test_lpo(e1, e->string())) { - return false; - } - ++proto_exprs; - continue; - } - if ((st_insert == e->string() || st_erase == e->string()) && e1) { - if (!test_st(e1, e->string())) { - return false; - } - ++proto_exprs; - continue; - } - if ((st_unify == e->string() || st_inst == e->string() || st_gen == e->string()) && e1) { - if (!test_st_visit(e1, e->string())) { - return false; - } - ++proto_exprs; - continue; - } - if (st_reset == e->string()) { - m_st.reset(); - ++proto_exprs; - continue; - } - if (st_display == e->string()) { - m_st.display(std::cout); - ++proto_exprs; - continue; - } -#endif if (m_notes == e->string() && e1) { ++proto_exprs; continue; @@ -4607,120 +4547,6 @@ private: } } -#if !defined(SMTCOMP) && !defined(_EXTERNAL_RELEASE) - bool test_order(proto_expr * e, order & ord, symbol expected) { - proto_expr* const * children = e->children(); - if (!children || !children[0] || !children[1]) { - set_error("invalid unification problem", e); - } - - expr_ref f1(m_manager), f2(m_manager); - if (!make_expression(children[0], f1) || !make_expression(children[1], f2)) - return false; - unsigned num_vars1 = 0; - unsigned num_vars2 = 0; - if (is_forall(f1)) { - num_vars1 = to_quantifier(f1)->get_num_decls(); - f1 = to_quantifier(f1)->get_expr(); - } - if (is_forall(f2)) { - num_vars2 = to_quantifier(f2)->get_num_decls(); - f2 = to_quantifier(f2)->get_expr(); - } - ord.reserve(1, std::max(num_vars1, num_vars2)); - order::result r = ord.compare(f1.get(), f2.get()); - if ((r == order::UNCOMPARABLE && expected != symbol("kbo_un") && expected != symbol("lpo_un")) || - (r == order::LESSER && expected != symbol("kbo_lt") && expected != symbol("lpo_lt")) || - (r == order::GREATER && expected != symbol("kbo_gt") && expected != symbol("lpo_gt")) || - (r == order::EQUAL && expected != symbol("kbo_eq") && expected != symbol("lpo_eq")) || - r == order::UNKNOWN) { - get_err() << "WRONG ANSWER\n"; - UNREACHABLE(); - } - else - std::cout << "order: succeeded\n"; - return true; - } - - bool test_kbo(proto_expr * e, symbol expected) { - precedence * p = alloc(arbitrary_precedence); - kbo k(m_manager, p); - return test_order(e, k, expected); - } - - bool test_lpo(proto_expr * e, symbol expected) { - precedence * ps[2] = { alloc(arity_precedence), alloc(arbitrary_precedence) }; - precedence * p = alloc(lex_precedence, 2, ps); - lpo l(m_manager, p); - return test_order(e, l, expected); - } - - bool test_st(proto_expr * e, symbol op) { - expr_ref f(m_manager); - if (!make_expression(e, f)) - return false; - - if (is_forall(f)) - f = to_quantifier(f)->get_expr(); - - if (!is_app(f)) - set_error("invalid st operation", e); - - if (op == symbol("st_insert")) - m_st.insert(to_app(f)); - else - m_st.erase(to_app(f)); - - return true; - } - - - - - class simple_st_visitor : public st_visitor { - unsigned m_delta; - public: - simple_st_visitor(substitution & s, unsigned d):st_visitor(s), m_delta(d) {} - virtual bool operator()(expr * e) { - std::cout << "found:\n" << mk_pp(e, m_subst.get_manager()) << "\n"; - unsigned deltas[2] = { 0, m_delta }; - std::cout << "substitution:\n"; - // m_subst.display(std::cout); std::cout << "\n"; - m_subst.display(std::cout, 2, deltas); - std::cout << "\n"; - return true; - } - }; - - bool test_st_visit(proto_expr * e, symbol op) { - expr_ref f(m_manager); - if (!make_expression(e, f)) - return false; - - unsigned num_vars = 0; - if (is_forall(f)) { - num_vars = to_quantifier(f)->get_num_decls(); - f = to_quantifier(f)->get_expr(); - } - if (!is_app(f)) - set_error("invalid st operation", e); - substitution s(m_manager); - s.reserve(3, std::max(num_vars, m_st.get_approx_num_regs())); - - simple_st_visitor v(s, num_vars); - - std::cout << "searching for " << op << ":\n" << mk_pp(f, m_manager) << "\n\n"; - if (op == symbol("st_unify")) - m_st.unify(to_app(f), v); - else if (op == symbol("st_inst")) - m_st.inst(to_app(f), v); - else - m_st.gen(to_app(f), v); - std::cout << "done.\n"; - return true; - } -#endif - bool declare_axioms(proto_expr * e) { proto_expr* const * children = e->children(); while (children && *children) { diff --git a/src/normal_forms/cnf.cpp b/src/ast/normal_forms/cnf.cpp similarity index 100% rename from src/normal_forms/cnf.cpp rename to src/ast/normal_forms/cnf.cpp diff --git a/src/normal_forms/cnf.h b/src/ast/normal_forms/cnf.h similarity index 100% rename from src/normal_forms/cnf.h rename to src/ast/normal_forms/cnf.h diff --git a/src/normal_forms/defined_names.cpp b/src/ast/normal_forms/defined_names.cpp similarity index 100% rename from src/normal_forms/defined_names.cpp rename to src/ast/normal_forms/defined_names.cpp diff --git a/src/normal_forms/defined_names.h b/src/ast/normal_forms/defined_names.h similarity index 100% rename from src/normal_forms/defined_names.h rename to src/ast/normal_forms/defined_names.h diff --git a/src/normal_forms/elim_term_ite.cpp b/src/ast/normal_forms/elim_term_ite.cpp similarity index 100% rename from src/normal_forms/elim_term_ite.cpp rename to src/ast/normal_forms/elim_term_ite.cpp diff --git a/src/normal_forms/elim_term_ite.h b/src/ast/normal_forms/elim_term_ite.h similarity index 100% rename from src/normal_forms/elim_term_ite.h rename to src/ast/normal_forms/elim_term_ite.h diff --git a/src/normal_forms/name_exprs.cpp b/src/ast/normal_forms/name_exprs.cpp similarity index 100% rename from src/normal_forms/name_exprs.cpp rename to src/ast/normal_forms/name_exprs.cpp diff --git a/src/normal_forms/name_exprs.h b/src/ast/normal_forms/name_exprs.h similarity index 100% rename from src/normal_forms/name_exprs.h rename to src/ast/normal_forms/name_exprs.h diff --git a/src/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp similarity index 99% rename from src/normal_forms/nnf.cpp rename to src/ast/normal_forms/nnf.cpp index 566eac8d7..ec168a247 100644 --- a/src/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -29,8 +29,6 @@ Notes: #include"ast_smt2_pp.h" -#include"tactical.h" - class skolemizer { typedef act_cache cache; diff --git a/src/normal_forms/nnf.h b/src/ast/normal_forms/nnf.h similarity index 85% rename from src/normal_forms/nnf.h rename to src/ast/normal_forms/nnf.h index 5674bd635..685083ff7 100644 --- a/src/normal_forms/nnf.h +++ b/src/ast/normal_forms/nnf.h @@ -51,10 +51,4 @@ public: void reset_cache(); }; -class tactic; -// Skolem Normal Form -tactic * mk_snf_tactic(ast_manager & m, params_ref const & p = params_ref()); -// Negation Normal Form -tactic * mk_nnf_tactic(ast_manager & m, params_ref const & p = params_ref()); - #endif /* _NNF_H_ */ diff --git a/src/normal_forms/pull_quant.cpp b/src/ast/normal_forms/pull_quant.cpp similarity index 100% rename from src/normal_forms/pull_quant.cpp rename to src/ast/normal_forms/pull_quant.cpp diff --git a/src/normal_forms/pull_quant.h b/src/ast/normal_forms/pull_quant.h similarity index 100% rename from src/normal_forms/pull_quant.h rename to src/ast/normal_forms/pull_quant.h diff --git a/src/ast/proof_checker/proof_checker.cpp b/src/ast/proof_checker/proof_checker.cpp index 9e2a3f260..6a9df1ef4 100644 --- a/src/ast/proof_checker/proof_checker.cpp +++ b/src/ast/proof_checker/proof_checker.cpp @@ -1,7 +1,7 @@ #include "proof_checker.h" #include "ast_ll_pp.h" #include "ast_pp.h" -#include "spc_decl_plugin.h" +// include "spc_decl_plugin.h" #include "ast_smt_pp.h" #include "arith_decl_plugin.h" #include "front_end_params.h" @@ -86,7 +86,7 @@ proof_checker::proof_checker(ast_manager& m) : m_manager(m), m_todo(m), m_marked m.register_plugin(fam_name, alloc(hyp_decl_plugin)); } m_hyp_fid = m.get_family_id(fam_name); - m_spc_fid = m.get_family_id("spc"); + // m_spc_fid = m.get_family_id("spc"); m_nil = m_manager.mk_const(m_hyp_fid, OP_NIL); } @@ -117,13 +117,16 @@ bool proof_checker::check1(proof* p, expr_ref_vector& side_conditions) { if (p->get_family_id() == m_manager.get_basic_family_id()) { return check1_basic(p, side_conditions); } +#if 0 if (p->get_family_id() == m_spc_fid) { return check1_spc(p, side_conditions); } +#endif return false; } bool proof_checker::check1_spc(proof* p, expr_ref_vector& side_conditions) { +#if 0 decl_kind k = p->get_decl_kind(); bool is_univ = false; expr_ref fact(m_manager), fml(m_manager); @@ -174,6 +177,9 @@ bool proof_checker::check1_spc(proof* p, expr_ref_vector& side_conditions) { UNREACHABLE(); } return false; +#else + return true; +#endif } bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) { diff --git a/src/ast/proof_checker/proof_checker.h b/src/ast/proof_checker/proof_checker.h index 8c4740ea2..6704f154a 100644 --- a/src/ast/proof_checker/proof_checker.h +++ b/src/ast/proof_checker/proof_checker.h @@ -29,7 +29,7 @@ class proof_checker { expr_ref_vector m_pinned; obj_map m_hypotheses; family_id m_hyp_fid; - family_id m_spc_fid; + // family_id m_spc_fid; app_ref m_nil; bool m_dump_lemmas; std::string m_logic; diff --git a/src/dotnet/Microsoft.Z3/AST.cs b/src/bindings/dotnet/Microsoft.Z3/AST.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/AST.cs rename to src/bindings/dotnet/Microsoft.Z3/AST.cs diff --git a/src/dotnet/Microsoft.Z3/ASTMap.cs b/src/bindings/dotnet/Microsoft.Z3/ASTMap.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/ASTMap.cs rename to src/bindings/dotnet/Microsoft.Z3/ASTMap.cs diff --git a/src/dotnet/Microsoft.Z3/ASTVector.cs b/src/bindings/dotnet/Microsoft.Z3/ASTVector.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/ASTVector.cs rename to src/bindings/dotnet/Microsoft.Z3/ASTVector.cs diff --git a/src/dotnet/Microsoft.Z3/ApplyResult.cs b/src/bindings/dotnet/Microsoft.Z3/ApplyResult.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/ApplyResult.cs rename to src/bindings/dotnet/Microsoft.Z3/ApplyResult.cs diff --git a/src/dotnet/Microsoft.Z3/Constructor.cs b/src/bindings/dotnet/Microsoft.Z3/Constructor.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Constructor.cs rename to src/bindings/dotnet/Microsoft.Z3/Constructor.cs diff --git a/src/dotnet/Microsoft.Z3/Context.cs b/src/bindings/dotnet/Microsoft.Z3/Context.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Context.cs rename to src/bindings/dotnet/Microsoft.Z3/Context.cs diff --git a/src/dotnet/Microsoft.Z3/DecRefQUeue.cs b/src/bindings/dotnet/Microsoft.Z3/DecRefQUeue.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/DecRefQUeue.cs rename to src/bindings/dotnet/Microsoft.Z3/DecRefQUeue.cs diff --git a/src/dotnet/Microsoft.Z3/Enumerations.cs b/src/bindings/dotnet/Microsoft.Z3/Enumerations.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Enumerations.cs rename to src/bindings/dotnet/Microsoft.Z3/Enumerations.cs diff --git a/src/dotnet/Microsoft.Z3/Expr.cs b/src/bindings/dotnet/Microsoft.Z3/Expr.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Expr.cs rename to src/bindings/dotnet/Microsoft.Z3/Expr.cs diff --git a/src/dotnet/Microsoft.Z3/Fixedpoint.cs b/src/bindings/dotnet/Microsoft.Z3/Fixedpoint.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Fixedpoint.cs rename to src/bindings/dotnet/Microsoft.Z3/Fixedpoint.cs diff --git a/src/dotnet/Microsoft.Z3/FuncDecl.cs b/src/bindings/dotnet/Microsoft.Z3/FuncDecl.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/FuncDecl.cs rename to src/bindings/dotnet/Microsoft.Z3/FuncDecl.cs diff --git a/src/dotnet/Microsoft.Z3/FuncInterp.cs b/src/bindings/dotnet/Microsoft.Z3/FuncInterp.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/FuncInterp.cs rename to src/bindings/dotnet/Microsoft.Z3/FuncInterp.cs diff --git a/src/dotnet/Microsoft.Z3/Goal.cs b/src/bindings/dotnet/Microsoft.Z3/Goal.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Goal.cs rename to src/bindings/dotnet/Microsoft.Z3/Goal.cs diff --git a/src/dotnet/Microsoft.Z3/Log.cs b/src/bindings/dotnet/Microsoft.Z3/Log.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Log.cs rename to src/bindings/dotnet/Microsoft.Z3/Log.cs diff --git a/src/dotnet/Microsoft.Z3/Microsoft.Z3.csproj b/src/bindings/dotnet/Microsoft.Z3/Microsoft.Z3.csproj similarity index 100% rename from src/dotnet/Microsoft.Z3/Microsoft.Z3.csproj rename to src/bindings/dotnet/Microsoft.Z3/Microsoft.Z3.csproj diff --git a/src/dotnet/Microsoft.Z3/Microsoft.Z3_35.csproj b/src/bindings/dotnet/Microsoft.Z3/Microsoft.Z3_35.csproj similarity index 100% rename from src/dotnet/Microsoft.Z3/Microsoft.Z3_35.csproj rename to src/bindings/dotnet/Microsoft.Z3/Microsoft.Z3_35.csproj diff --git a/src/dotnet/Microsoft.Z3/Model.cs b/src/bindings/dotnet/Microsoft.Z3/Model.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Model.cs rename to src/bindings/dotnet/Microsoft.Z3/Model.cs diff --git a/src/dotnet/Microsoft.Z3/Native.cs b/src/bindings/dotnet/Microsoft.Z3/Native.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Native.cs rename to src/bindings/dotnet/Microsoft.Z3/Native.cs diff --git a/src/dotnet/Microsoft.Z3/Numeral.cs b/src/bindings/dotnet/Microsoft.Z3/Numeral.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Numeral.cs rename to src/bindings/dotnet/Microsoft.Z3/Numeral.cs diff --git a/src/dotnet/Microsoft.Z3/ParamDescrs.cs b/src/bindings/dotnet/Microsoft.Z3/ParamDescrs.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/ParamDescrs.cs rename to src/bindings/dotnet/Microsoft.Z3/ParamDescrs.cs diff --git a/src/dotnet/Microsoft.Z3/Params.cs b/src/bindings/dotnet/Microsoft.Z3/Params.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Params.cs rename to src/bindings/dotnet/Microsoft.Z3/Params.cs diff --git a/src/dotnet/Microsoft.Z3/Pattern.cs b/src/bindings/dotnet/Microsoft.Z3/Pattern.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Pattern.cs rename to src/bindings/dotnet/Microsoft.Z3/Pattern.cs diff --git a/src/dotnet/Microsoft.Z3/Probe.cs b/src/bindings/dotnet/Microsoft.Z3/Probe.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Probe.cs rename to src/bindings/dotnet/Microsoft.Z3/Probe.cs diff --git a/src/dotnet/Microsoft.Z3/Properties/AssemblyInfo.cs b/src/bindings/dotnet/Microsoft.Z3/Properties/AssemblyInfo.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Properties/AssemblyInfo.cs rename to src/bindings/dotnet/Microsoft.Z3/Properties/AssemblyInfo.cs diff --git a/src/dotnet/Microsoft.Z3/Quantifier.cs b/src/bindings/dotnet/Microsoft.Z3/Quantifier.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Quantifier.cs rename to src/bindings/dotnet/Microsoft.Z3/Quantifier.cs diff --git a/src/dotnet/Microsoft.Z3/Solver.cs b/src/bindings/dotnet/Microsoft.Z3/Solver.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Solver.cs rename to src/bindings/dotnet/Microsoft.Z3/Solver.cs diff --git a/src/dotnet/Microsoft.Z3/Sort.cs b/src/bindings/dotnet/Microsoft.Z3/Sort.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Sort.cs rename to src/bindings/dotnet/Microsoft.Z3/Sort.cs diff --git a/src/dotnet/Microsoft.Z3/Statistics.cs b/src/bindings/dotnet/Microsoft.Z3/Statistics.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Statistics.cs rename to src/bindings/dotnet/Microsoft.Z3/Statistics.cs diff --git a/src/dotnet/Microsoft.Z3/Status.cs b/src/bindings/dotnet/Microsoft.Z3/Status.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Status.cs rename to src/bindings/dotnet/Microsoft.Z3/Status.cs diff --git a/src/dotnet/Microsoft.Z3/Symbol.cs b/src/bindings/dotnet/Microsoft.Z3/Symbol.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Symbol.cs rename to src/bindings/dotnet/Microsoft.Z3/Symbol.cs diff --git a/src/dotnet/Microsoft.Z3/Tactic.cs b/src/bindings/dotnet/Microsoft.Z3/Tactic.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Tactic.cs rename to src/bindings/dotnet/Microsoft.Z3/Tactic.cs diff --git a/src/dotnet/Microsoft.Z3/Version.cs b/src/bindings/dotnet/Microsoft.Z3/Version.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Version.cs rename to src/bindings/dotnet/Microsoft.Z3/Version.cs diff --git a/src/dotnet/Microsoft.Z3/Z3Exception.cs b/src/bindings/dotnet/Microsoft.Z3/Z3Exception.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Z3Exception.cs rename to src/bindings/dotnet/Microsoft.Z3/Z3Exception.cs diff --git a/src/dotnet/Microsoft.Z3/Z3Object.cs b/src/bindings/dotnet/Microsoft.Z3/Z3Object.cs similarity index 100% rename from src/dotnet/Microsoft.Z3/Z3Object.cs rename to src/bindings/dotnet/Microsoft.Z3/Z3Object.cs diff --git a/src/dotnet/Microsoft.Z3V3/AssemblyInfo.cpp b/src/bindings/dotnet/Microsoft.Z3V3/AssemblyInfo.cpp similarity index 100% rename from src/dotnet/Microsoft.Z3V3/AssemblyInfo.cpp rename to src/bindings/dotnet/Microsoft.Z3V3/AssemblyInfo.cpp diff --git a/src/dotnet/Microsoft.Z3V3/Microsoft.Z3V3.cpp b/src/bindings/dotnet/Microsoft.Z3V3/Microsoft.Z3V3.cpp similarity index 100% rename from src/dotnet/Microsoft.Z3V3/Microsoft.Z3V3.cpp rename to src/bindings/dotnet/Microsoft.Z3V3/Microsoft.Z3V3.cpp diff --git a/src/dotnet/Microsoft.Z3V3/Microsoft.Z3V3.h b/src/bindings/dotnet/Microsoft.Z3V3/Microsoft.Z3V3.h similarity index 100% rename from src/dotnet/Microsoft.Z3V3/Microsoft.Z3V3.h rename to src/bindings/dotnet/Microsoft.Z3V3/Microsoft.Z3V3.h diff --git a/src/dotnet/Microsoft.Z3V3/Microsoft.Z3V3.vcxproj b/src/bindings/dotnet/Microsoft.Z3V3/Microsoft.Z3V3.vcxproj similarity index 100% rename from src/dotnet/Microsoft.Z3V3/Microsoft.Z3V3.vcxproj rename to src/bindings/dotnet/Microsoft.Z3V3/Microsoft.Z3V3.vcxproj diff --git a/src/ml/README-linux b/src/bindings/ml/README-linux similarity index 100% rename from src/ml/README-linux rename to src/bindings/ml/README-linux diff --git a/src/ml/README-osx b/src/bindings/ml/README-osx similarity index 100% rename from src/ml/README-osx rename to src/bindings/ml/README-osx diff --git a/src/ml/README-test-linux b/src/bindings/ml/README-test-linux similarity index 100% rename from src/ml/README-test-linux rename to src/bindings/ml/README-test-linux diff --git a/src/ml/README-test-osx b/src/bindings/ml/README-test-osx similarity index 100% rename from src/ml/README-test-osx rename to src/bindings/ml/README-test-osx diff --git a/src/ml/README-test-win b/src/bindings/ml/README-test-win similarity index 100% rename from src/ml/README-test-win rename to src/bindings/ml/README-test-win diff --git a/src/ml/README-win b/src/bindings/ml/README-win similarity index 100% rename from src/ml/README-win rename to src/bindings/ml/README-win diff --git a/src/ml/add_error_checking.V3.sed b/src/bindings/ml/add_error_checking.V3.sed similarity index 100% rename from src/ml/add_error_checking.V3.sed rename to src/bindings/ml/add_error_checking.V3.sed diff --git a/src/ml/add_error_checking.sed b/src/bindings/ml/add_error_checking.sed similarity index 100% rename from src/ml/add_error_checking.sed rename to src/bindings/ml/add_error_checking.sed diff --git a/src/ml/build-lib.cmd b/src/bindings/ml/build-lib.cmd similarity index 100% rename from src/ml/build-lib.cmd rename to src/bindings/ml/build-lib.cmd diff --git a/src/ml/build-lib.sh b/src/bindings/ml/build-lib.sh similarity index 100% rename from src/ml/build-lib.sh rename to src/bindings/ml/build-lib.sh diff --git a/src/ml/build-test.cmd b/src/bindings/ml/build-test.cmd similarity index 100% rename from src/ml/build-test.cmd rename to src/bindings/ml/build-test.cmd diff --git a/src/ml/build-test.sh b/src/bindings/ml/build-test.sh similarity index 100% rename from src/ml/build-test.sh rename to src/bindings/ml/build-test.sh diff --git a/src/ml/build.cmd b/src/bindings/ml/build.cmd similarity index 100% rename from src/ml/build.cmd rename to src/bindings/ml/build.cmd diff --git a/src/ml/build.sed b/src/bindings/ml/build.sed similarity index 100% rename from src/ml/build.sed rename to src/bindings/ml/build.sed diff --git a/src/ml/clean.cmd b/src/bindings/ml/clean.cmd similarity index 100% rename from src/ml/clean.cmd rename to src/bindings/ml/clean.cmd diff --git a/src/ml/cleantmp.cmd b/src/bindings/ml/cleantmp.cmd similarity index 100% rename from src/ml/cleantmp.cmd rename to src/bindings/ml/cleantmp.cmd diff --git a/src/ml/compile_mlapi.cmd b/src/bindings/ml/compile_mlapi.cmd similarity index 100% rename from src/ml/compile_mlapi.cmd rename to src/bindings/ml/compile_mlapi.cmd diff --git a/src/ml/error_handling.idl b/src/bindings/ml/error_handling.idl similarity index 100% rename from src/ml/error_handling.idl rename to src/bindings/ml/error_handling.idl diff --git a/src/ml/exec.cmd b/src/bindings/ml/exec.cmd similarity index 100% rename from src/ml/exec.cmd rename to src/bindings/ml/exec.cmd diff --git a/src/ml/exec.sh b/src/bindings/ml/exec.sh similarity index 100% rename from src/ml/exec.sh rename to src/bindings/ml/exec.sh diff --git a/src/ml/generate_mlapi.cmd b/src/bindings/ml/generate_mlapi.cmd similarity index 100% rename from src/ml/generate_mlapi.cmd rename to src/bindings/ml/generate_mlapi.cmd diff --git a/src/ml/import.cmd b/src/bindings/ml/import.cmd similarity index 100% rename from src/ml/import.cmd rename to src/bindings/ml/import.cmd diff --git a/src/ml/mlx_get_app_args.idl b/src/bindings/ml/mlx_get_app_args.idl similarity index 100% rename from src/ml/mlx_get_app_args.idl rename to src/bindings/ml/mlx_get_app_args.idl diff --git a/src/ml/mlx_get_array_sort.idl b/src/bindings/ml/mlx_get_array_sort.idl similarity index 100% rename from src/ml/mlx_get_array_sort.idl rename to src/bindings/ml/mlx_get_array_sort.idl diff --git a/src/ml/mlx_get_datatype_sort.idl b/src/bindings/ml/mlx_get_datatype_sort.idl similarity index 100% rename from src/ml/mlx_get_datatype_sort.idl rename to src/bindings/ml/mlx_get_datatype_sort.idl diff --git a/src/ml/mlx_get_domains.idl b/src/bindings/ml/mlx_get_domains.idl similarity index 100% rename from src/ml/mlx_get_domains.idl rename to src/bindings/ml/mlx_get_domains.idl diff --git a/src/ml/mlx_get_error_msg.idl b/src/bindings/ml/mlx_get_error_msg.idl similarity index 100% rename from src/ml/mlx_get_error_msg.idl rename to src/bindings/ml/mlx_get_error_msg.idl diff --git a/src/ml/mlx_get_pattern_terms.idl b/src/bindings/ml/mlx_get_pattern_terms.idl similarity index 100% rename from src/ml/mlx_get_pattern_terms.idl rename to src/bindings/ml/mlx_get_pattern_terms.idl diff --git a/src/ml/mlx_get_tuple_sort.idl b/src/bindings/ml/mlx_get_tuple_sort.idl similarity index 100% rename from src/ml/mlx_get_tuple_sort.idl rename to src/bindings/ml/mlx_get_tuple_sort.idl diff --git a/src/ml/mlx_mk_context_x.idl b/src/bindings/ml/mlx_mk_context_x.idl similarity index 100% rename from src/ml/mlx_mk_context_x.idl rename to src/bindings/ml/mlx_mk_context_x.idl diff --git a/src/ml/mlx_mk_datatypes.idl b/src/bindings/ml/mlx_mk_datatypes.idl similarity index 100% rename from src/ml/mlx_mk_datatypes.idl rename to src/bindings/ml/mlx_mk_datatypes.idl diff --git a/src/ml/mlx_mk_numeral.idl b/src/bindings/ml/mlx_mk_numeral.idl similarity index 100% rename from src/ml/mlx_mk_numeral.idl rename to src/bindings/ml/mlx_mk_numeral.idl diff --git a/src/ml/mlx_mk_sort.idl b/src/bindings/ml/mlx_mk_sort.idl similarity index 100% rename from src/ml/mlx_mk_sort.idl rename to src/bindings/ml/mlx_mk_sort.idl diff --git a/src/ml/mlx_mk_symbol.idl b/src/bindings/ml/mlx_mk_symbol.idl similarity index 100% rename from src/ml/mlx_mk_symbol.idl rename to src/bindings/ml/mlx_mk_symbol.idl diff --git a/src/ml/mlx_model.idl b/src/bindings/ml/mlx_model.idl similarity index 100% rename from src/ml/mlx_model.idl rename to src/bindings/ml/mlx_model.idl diff --git a/src/ml/mlx_numeral_refine.idl b/src/bindings/ml/mlx_numeral_refine.idl similarity index 100% rename from src/ml/mlx_numeral_refine.idl rename to src/bindings/ml/mlx_numeral_refine.idl diff --git a/src/ml/mlx_parse_smtlib.idl b/src/bindings/ml/mlx_parse_smtlib.idl similarity index 100% rename from src/ml/mlx_parse_smtlib.idl rename to src/bindings/ml/mlx_parse_smtlib.idl diff --git a/src/ml/mlx_sort_refine.idl b/src/bindings/ml/mlx_sort_refine.idl similarity index 100% rename from src/ml/mlx_sort_refine.idl rename to src/bindings/ml/mlx_sort_refine.idl diff --git a/src/ml/mlx_statistics.idl b/src/bindings/ml/mlx_statistics.idl similarity index 100% rename from src/ml/mlx_statistics.idl rename to src/bindings/ml/mlx_statistics.idl diff --git a/src/ml/mlx_symbol_refine.idl b/src/bindings/ml/mlx_symbol_refine.idl similarity index 100% rename from src/ml/mlx_symbol_refine.idl rename to src/bindings/ml/mlx_symbol_refine.idl diff --git a/src/ml/mlx_term_refine.idl b/src/bindings/ml/mlx_term_refine.idl similarity index 100% rename from src/ml/mlx_term_refine.idl rename to src/bindings/ml/mlx_term_refine.idl diff --git a/src/ml/queen.ml b/src/bindings/ml/queen.ml similarity index 100% rename from src/ml/queen.ml rename to src/bindings/ml/queen.ml diff --git a/src/ml/queen.regress.err b/src/bindings/ml/queen.regress.err similarity index 100% rename from src/ml/queen.regress.err rename to src/bindings/ml/queen.regress.err diff --git a/src/ml/queen.regress.out b/src/bindings/ml/queen.regress.out similarity index 100% rename from src/ml/queen.regress.out rename to src/bindings/ml/queen.regress.out diff --git a/src/ml/test_capi.regress.err b/src/bindings/ml/test_capi.regress.err similarity index 100% rename from src/ml/test_capi.regress.err rename to src/bindings/ml/test_capi.regress.err diff --git a/src/ml/test_capi.regress.out b/src/bindings/ml/test_capi.regress.out similarity index 100% rename from src/ml/test_capi.regress.out rename to src/bindings/ml/test_capi.regress.out diff --git a/src/ml/test_mlapi.cmd b/src/bindings/ml/test_mlapi.cmd similarity index 100% rename from src/ml/test_mlapi.cmd rename to src/bindings/ml/test_mlapi.cmd diff --git a/src/ml/test_mlapi.ml b/src/bindings/ml/test_mlapi.ml similarity index 100% rename from src/ml/test_mlapi.ml rename to src/bindings/ml/test_mlapi.ml diff --git a/src/ml/test_mlapi.regress.err b/src/bindings/ml/test_mlapi.regress.err similarity index 100% rename from src/ml/test_mlapi.regress.err rename to src/bindings/ml/test_mlapi.regress.err diff --git a/src/ml/test_mlapi.regress.out b/src/bindings/ml/test_mlapi.regress.out similarity index 100% rename from src/ml/test_mlapi.regress.out rename to src/bindings/ml/test_mlapi.regress.out diff --git a/src/ml/test_mlapiV3.ml b/src/bindings/ml/test_mlapiV3.ml similarity index 100% rename from src/ml/test_mlapiV3.ml rename to src/bindings/ml/test_mlapiV3.ml diff --git a/src/ml/test_mlapiV3.regress.err b/src/bindings/ml/test_mlapiV3.regress.err similarity index 100% rename from src/ml/test_mlapiV3.regress.err rename to src/bindings/ml/test_mlapiV3.regress.err diff --git a/src/ml/test_mlapiV3.regress.out b/src/bindings/ml/test_mlapiV3.regress.out similarity index 100% rename from src/ml/test_mlapiV3.regress.out rename to src/bindings/ml/test_mlapiV3.regress.out diff --git a/src/ml/test_theory.ml b/src/bindings/ml/test_theory.ml similarity index 100% rename from src/ml/test_theory.ml rename to src/bindings/ml/test_theory.ml diff --git a/src/ml/update-ml-doc.cmd b/src/bindings/ml/update-ml-doc.cmd similarity index 100% rename from src/ml/update-ml-doc.cmd rename to src/bindings/ml/update-ml-doc.cmd diff --git a/src/ml/x3.ml b/src/bindings/ml/x3.ml similarity index 100% rename from src/ml/x3.ml rename to src/bindings/ml/x3.ml diff --git a/src/ml/x3V3.ml b/src/bindings/ml/x3V3.ml similarity index 100% rename from src/ml/x3V3.ml rename to src/bindings/ml/x3V3.ml diff --git a/src/ml/x3V3.mli b/src/bindings/ml/x3V3.mli similarity index 100% rename from src/ml/x3V3.mli rename to src/bindings/ml/x3V3.mli diff --git a/src/ml/z3.idl b/src/bindings/ml/z3.idl similarity index 100% rename from src/ml/z3.idl rename to src/bindings/ml/z3.idl diff --git a/src/ml/z3.ml b/src/bindings/ml/z3.ml similarity index 100% rename from src/ml/z3.ml rename to src/bindings/ml/z3.ml diff --git a/src/ml/z3.mli b/src/bindings/ml/z3.mli similarity index 100% rename from src/ml/z3.mli rename to src/bindings/ml/z3.mli diff --git a/src/ml/z3_stubs.c b/src/bindings/ml/z3_stubs.c similarity index 100% rename from src/ml/z3_stubs.c rename to src/bindings/ml/z3_stubs.c diff --git a/src/ml/z3_theory_stubs.c b/src/bindings/ml/z3_theory_stubs.c similarity index 100% rename from src/ml/z3_theory_stubs.c rename to src/bindings/ml/z3_theory_stubs.c diff --git a/src/python/README.txt b/src/bindings/python/README.txt similarity index 100% rename from src/python/README.txt rename to src/bindings/python/README.txt diff --git a/src/python/example.py b/src/bindings/python/example.py similarity index 100% rename from src/python/example.py rename to src/bindings/python/example.py diff --git a/src/python/z3.py b/src/bindings/python/z3.py similarity index 100% rename from src/python/z3.py rename to src/bindings/python/z3.py diff --git a/src/python/z3consts.py b/src/bindings/python/z3consts.py similarity index 100% rename from src/python/z3consts.py rename to src/bindings/python/z3consts.py diff --git a/src/python/z3core.py b/src/bindings/python/z3core.py similarity index 100% rename from src/python/z3core.py rename to src/bindings/python/z3core.py diff --git a/src/python/z3poly.py b/src/bindings/python/z3poly.py similarity index 100% rename from src/python/z3poly.py rename to src/bindings/python/z3poly.py diff --git a/src/python/z3printer.py b/src/bindings/python/z3printer.py similarity index 100% rename from src/python/z3printer.py rename to src/bindings/python/z3printer.py diff --git a/src/python/z3tactics.py b/src/bindings/python/z3tactics.py similarity index 100% rename from src/python/z3tactics.py rename to src/bindings/python/z3tactics.py diff --git a/src/python/z3test.py b/src/bindings/python/z3test.py similarity index 100% rename from src/python/z3test.py rename to src/bindings/python/z3test.py diff --git a/src/python/z3types.py b/src/bindings/python/z3types.py similarity index 100% rename from src/python/z3types.py rename to src/bindings/python/z3types.py diff --git a/src/spc/README b/src/dead/spc/README similarity index 100% rename from src/spc/README rename to src/dead/spc/README diff --git a/src/spc/fvi.h b/src/dead/spc/fvi.h similarity index 100% rename from src/spc/fvi.h rename to src/dead/spc/fvi.h diff --git a/src/spc/fvi_def.h b/src/dead/spc/fvi_def.h similarity index 100% rename from src/spc/fvi_def.h rename to src/dead/spc/fvi_def.h diff --git a/src/spc/kbo.cpp b/src/dead/spc/kbo.cpp similarity index 100% rename from src/spc/kbo.cpp rename to src/dead/spc/kbo.cpp diff --git a/src/spc/kbo.h b/src/dead/spc/kbo.h similarity index 100% rename from src/spc/kbo.h rename to src/dead/spc/kbo.h diff --git a/src/spc/lpo.cpp b/src/dead/spc/lpo.cpp similarity index 100% rename from src/spc/lpo.cpp rename to src/dead/spc/lpo.cpp diff --git a/src/spc/lpo.h b/src/dead/spc/lpo.h similarity index 100% rename from src/spc/lpo.h rename to src/dead/spc/lpo.h diff --git a/src/spc/marker.h b/src/dead/spc/marker.h similarity index 100% rename from src/spc/marker.h rename to src/dead/spc/marker.h diff --git a/src/spc/normalize_vars.cpp b/src/dead/spc/normalize_vars.cpp similarity index 100% rename from src/spc/normalize_vars.cpp rename to src/dead/spc/normalize_vars.cpp diff --git a/src/spc/normalize_vars.h b/src/dead/spc/normalize_vars.h similarity index 100% rename from src/spc/normalize_vars.h rename to src/dead/spc/normalize_vars.h diff --git a/src/spc/order.cpp b/src/dead/spc/order.cpp similarity index 100% rename from src/spc/order.cpp rename to src/dead/spc/order.cpp diff --git a/src/spc/order.h b/src/dead/spc/order.h similarity index 100% rename from src/spc/order.h rename to src/dead/spc/order.h diff --git a/src/spc/precedence.cpp b/src/dead/spc/precedence.cpp similarity index 100% rename from src/spc/precedence.cpp rename to src/dead/spc/precedence.cpp diff --git a/src/spc/precedence.h b/src/dead/spc/precedence.h similarity index 100% rename from src/spc/precedence.h rename to src/dead/spc/precedence.h diff --git a/src/spc/preprocessor.cpp b/src/dead/spc/preprocessor.cpp similarity index 100% rename from src/spc/preprocessor.cpp rename to src/dead/spc/preprocessor.cpp diff --git a/src/spc/preprocessor.h b/src/dead/spc/preprocessor.h similarity index 100% rename from src/spc/preprocessor.h rename to src/dead/spc/preprocessor.h diff --git a/src/spc/sparse_use_list.h b/src/dead/spc/sparse_use_list.h similarity index 100% rename from src/spc/sparse_use_list.h rename to src/dead/spc/sparse_use_list.h diff --git a/src/spc/spc_asserted_literals.cpp b/src/dead/spc/spc_asserted_literals.cpp similarity index 100% rename from src/spc/spc_asserted_literals.cpp rename to src/dead/spc/spc_asserted_literals.cpp diff --git a/src/spc/spc_asserted_literals.h b/src/dead/spc/spc_asserted_literals.h similarity index 100% rename from src/spc/spc_asserted_literals.h rename to src/dead/spc/spc_asserted_literals.h diff --git a/src/spc/spc_clause.cpp b/src/dead/spc/spc_clause.cpp similarity index 100% rename from src/spc/spc_clause.cpp rename to src/dead/spc/spc_clause.cpp diff --git a/src/spc/spc_clause.h b/src/dead/spc/spc_clause.h similarity index 100% rename from src/spc/spc_clause.h rename to src/dead/spc/spc_clause.h diff --git a/src/spc/spc_clause_pos_set.h b/src/dead/spc/spc_clause_pos_set.h similarity index 100% rename from src/spc/spc_clause_pos_set.h rename to src/dead/spc/spc_clause_pos_set.h diff --git a/src/spc/spc_clause_selection.cpp b/src/dead/spc/spc_clause_selection.cpp similarity index 100% rename from src/spc/spc_clause_selection.cpp rename to src/dead/spc/spc_clause_selection.cpp diff --git a/src/spc/spc_clause_selection.h b/src/dead/spc/spc_clause_selection.h similarity index 100% rename from src/spc/spc_clause_selection.h rename to src/dead/spc/spc_clause_selection.h diff --git a/src/spc/spc_context.cpp b/src/dead/spc/spc_context.cpp similarity index 100% rename from src/spc/spc_context.cpp rename to src/dead/spc/spc_context.cpp diff --git a/src/spc/spc_context.h b/src/dead/spc/spc_context.h similarity index 100% rename from src/spc/spc_context.h rename to src/dead/spc/spc_context.h diff --git a/src/spc/spc_decl_plugin.cpp b/src/dead/spc/spc_decl_plugin.cpp similarity index 100% rename from src/spc/spc_decl_plugin.cpp rename to src/dead/spc/spc_decl_plugin.cpp diff --git a/src/spc/spc_decl_plugin.h b/src/dead/spc/spc_decl_plugin.h similarity index 100% rename from src/spc/spc_decl_plugin.h rename to src/dead/spc/spc_decl_plugin.h diff --git a/src/spc/spc_der.cpp b/src/dead/spc/spc_der.cpp similarity index 100% rename from src/spc/spc_der.cpp rename to src/dead/spc/spc_der.cpp diff --git a/src/spc/spc_der.h b/src/dead/spc/spc_der.h similarity index 100% rename from src/spc/spc_der.h rename to src/dead/spc/spc_der.h diff --git a/src/spc/spc_eq_resolution.cpp b/src/dead/spc/spc_eq_resolution.cpp similarity index 100% rename from src/spc/spc_eq_resolution.cpp rename to src/dead/spc/spc_eq_resolution.cpp diff --git a/src/spc/spc_eq_resolution.h b/src/dead/spc/spc_eq_resolution.h similarity index 100% rename from src/spc/spc_eq_resolution.h rename to src/dead/spc/spc_eq_resolution.h diff --git a/src/spc/spc_factoring.cpp b/src/dead/spc/spc_factoring.cpp similarity index 100% rename from src/spc/spc_factoring.cpp rename to src/dead/spc/spc_factoring.cpp diff --git a/src/spc/spc_factoring.h b/src/dead/spc/spc_factoring.h similarity index 100% rename from src/spc/spc_factoring.h rename to src/dead/spc/spc_factoring.h diff --git a/src/spc/spc_justification.cpp b/src/dead/spc/spc_justification.cpp similarity index 100% rename from src/spc/spc_justification.cpp rename to src/dead/spc/spc_justification.cpp diff --git a/src/spc/spc_justification.h b/src/dead/spc/spc_justification.h similarity index 100% rename from src/spc/spc_justification.h rename to src/dead/spc/spc_justification.h diff --git a/src/spc/spc_literal.cpp b/src/dead/spc/spc_literal.cpp similarity index 100% rename from src/spc/spc_literal.cpp rename to src/dead/spc/spc_literal.cpp diff --git a/src/spc/spc_literal.h b/src/dead/spc/spc_literal.h similarity index 100% rename from src/spc/spc_literal.h rename to src/dead/spc/spc_literal.h diff --git a/src/spc/spc_literal_selection.cpp b/src/dead/spc/spc_literal_selection.cpp similarity index 100% rename from src/spc/spc_literal_selection.cpp rename to src/dead/spc/spc_literal_selection.cpp diff --git a/src/spc/spc_literal_selection.h b/src/dead/spc/spc_literal_selection.h similarity index 100% rename from src/spc/spc_literal_selection.h rename to src/dead/spc/spc_literal_selection.h diff --git a/src/spc/spc_prover.cpp b/src/dead/spc/spc_prover.cpp similarity index 100% rename from src/spc/spc_prover.cpp rename to src/dead/spc/spc_prover.cpp diff --git a/src/spc/spc_prover.h b/src/dead/spc/spc_prover.h similarity index 100% rename from src/spc/spc_prover.h rename to src/dead/spc/spc_prover.h diff --git a/src/spc/spc_rewriter.cpp b/src/dead/spc/spc_rewriter.cpp similarity index 100% rename from src/spc/spc_rewriter.cpp rename to src/dead/spc/spc_rewriter.cpp diff --git a/src/spc/spc_rewriter.h b/src/dead/spc/spc_rewriter.h similarity index 100% rename from src/spc/spc_rewriter.h rename to src/dead/spc/spc_rewriter.h diff --git a/src/spc/spc_semantic_tautology.cpp b/src/dead/spc/spc_semantic_tautology.cpp similarity index 100% rename from src/spc/spc_semantic_tautology.cpp rename to src/dead/spc/spc_semantic_tautology.cpp diff --git a/src/spc/spc_semantic_tautology.h b/src/dead/spc/spc_semantic_tautology.h similarity index 100% rename from src/spc/spc_semantic_tautology.h rename to src/dead/spc/spc_semantic_tautology.h diff --git a/src/spc/spc_statistics.cpp b/src/dead/spc/spc_statistics.cpp similarity index 100% rename from src/spc/spc_statistics.cpp rename to src/dead/spc/spc_statistics.cpp diff --git a/src/spc/spc_statistics.h b/src/dead/spc/spc_statistics.h similarity index 100% rename from src/spc/spc_statistics.h rename to src/dead/spc/spc_statistics.h diff --git a/src/spc/spc_subsumption.cpp b/src/dead/spc/spc_subsumption.cpp similarity index 100% rename from src/spc/spc_subsumption.cpp rename to src/dead/spc/spc_subsumption.cpp diff --git a/src/spc/spc_subsumption.h b/src/dead/spc/spc_subsumption.h similarity index 100% rename from src/spc/spc_subsumption.h rename to src/dead/spc/spc_subsumption.h diff --git a/src/spc/spc_superposition.cpp b/src/dead/spc/spc_superposition.cpp similarity index 100% rename from src/spc/spc_superposition.cpp rename to src/dead/spc/spc_superposition.cpp diff --git a/src/spc/spc_superposition.h b/src/dead/spc/spc_superposition.h similarity index 100% rename from src/spc/spc_superposition.h rename to src/dead/spc/spc_superposition.h diff --git a/src/spc/spc_unary_inference.cpp b/src/dead/spc/spc_unary_inference.cpp similarity index 100% rename from src/spc/spc_unary_inference.cpp rename to src/dead/spc/spc_unary_inference.cpp diff --git a/src/spc/spc_unary_inference.h b/src/dead/spc/spc_unary_inference.h similarity index 100% rename from src/spc/spc_unary_inference.h rename to src/dead/spc/spc_unary_inference.h diff --git a/src/spc/splay_tree.h b/src/dead/spc/splay_tree.h similarity index 100% rename from src/spc/splay_tree.h rename to src/dead/spc/splay_tree.h diff --git a/src/spc/splay_tree_def.h b/src/dead/spc/splay_tree_def.h similarity index 100% rename from src/spc/splay_tree_def.h rename to src/dead/spc/splay_tree_def.h diff --git a/src/spc/splay_tree_map.h b/src/dead/spc/splay_tree_map.h similarity index 100% rename from src/spc/splay_tree_map.h rename to src/dead/spc/splay_tree_map.h diff --git a/src/spc/use_list.cpp b/src/dead/spc/use_list.cpp similarity index 100% rename from src/spc/use_list.cpp rename to src/dead/spc/use_list.cpp diff --git a/src/spc/use_list.h b/src/dead/spc/use_list.h similarity index 100% rename from src/spc/use_list.h rename to src/dead/spc/use_list.h diff --git a/src/test/fvi.cpp b/src/test/fvi.cpp deleted file mode 100644 index 6861699a8..000000000 --- a/src/test/fvi.cpp +++ /dev/null @@ -1,158 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - fvi.cpp - -Abstract: - - Feature Vector Indexing. - -Author: - - Leonardo de Moura (leonardo) 2008-02-01. - -Revision History: - ---*/ -#ifdef _WINDOWS -#include"fvi_def.h" -#include"trace.h" - -typedef vector data; - -static int to_feature(int val) { - return val % 4; -} - -static std::ostream & operator<<(std::ostream & out, data const & d) { - out << "["; - data::const_iterator it = d.begin(); - data::const_iterator end = d.end(); - for (bool first = true; it != end; ++it, first = false) - out << (first ? "" : " ") << *it << ":" << to_feature(*it); - out << "]"; - return out; -} - -#define NUM_FEATURES 5 - -struct to_feature_vector { - unsigned m_num_features; - - to_feature_vector(unsigned n):m_num_features(n) {} - - void operator()(data * d, unsigned * f) { - for (unsigned i = 0; i < m_num_features; i++) { - f[i] = to_feature((*d)[i]); - } - } -}; - -struct data_hash { - unsigned operator()(data * d) const { - unsigned r = 0; - data::iterator it = d->begin(); - data::iterator end = d->end(); - for (; it != end; ++it) - r += *it; - return r; - } -}; - -ptr_vector g_datas; - -static void collect() { - std::for_each(g_datas.begin(), g_datas.end(), delete_proc()); -} - -static data * mk_random_data() { - data * d = alloc(data); - for (unsigned i = 0; i < NUM_FEATURES; i++) - d->push_back(rand() % 1000); - g_datas.push_back(d); - return d; -} - -struct le_visitor { - data * m_data; - - le_visitor(data * d):m_data(d) {} - - bool operator()(data * other) { - // TRACE("fvi", tout << *other << " <= " << *m_data << "\n";); - for (unsigned i = 0; i < NUM_FEATURES; i++) { - SASSERT(to_feature((*other)[i]) <= to_feature((*m_data)[i])); - } - return true; - } -}; - -static void tst1(unsigned n1) { - typedef fvi data_set; - data_set index1(NUM_FEATURES, to_feature_vector(NUM_FEATURES)); - ptr_vector index2; - - for (unsigned i = 0; i < n1; i++) { - int op = rand()%6; - if (op < 3) { - data * d = mk_random_data(); - if (!index1.contains(d)) { - // TRACE("fvi", tout << "inserting: " << *d << "\n";); - index1.insert(d); - index2.push_back(d); - SASSERT(std::find(index2.begin(), index2.end(), d) != index2.end()); - SASSERT(index1.contains(d)); - } - } - else if (op < 4) { - if (!index2.empty()) { - unsigned idx = rand() % index2.size(); - if (index2[idx]) { - SASSERT(index1.contains(index2[idx])); - } - } - } - else if (op < 5) { - if (!index2.empty()) { - unsigned idx = rand() % index2.size(); - if (index2[idx]) { - // TRACE("fvi", tout << "erasing: " << *(index2[idx]) << "\n";); - index1.erase(index2[idx]); - SASSERT(!index1.contains(index2[idx])); - index2[idx] = 0; - } - } - } - else { - if (!index2.empty()) { - unsigned idx = rand() % index2.size(); - data * d = index2[idx]; - if (d) - index1.visit(d, le_visitor(d)); - } - } - } - - TRACE("fvi", - data_set::statistics s; - index1.stats(s); - tout << "size: " << s.m_size << "\n"; - tout << "num. nodes: " << s.m_num_nodes << "\n"; - tout << "num. leaves: " << s.m_num_leaves << "\n"; - tout << "min. leaf size: " << s.m_min_leaf_size << "\n"; - tout << "max. leaf size: " << s.m_max_leaf_size << "\n"; - ); -} - -void tst_fvi() { - for (unsigned i = 0; i < 1000; i++) - tst1(100); - tst1(10000); - collect(); -} -#else -void tst_fvi() { -} -#endif diff --git a/src/test/main.cpp b/src/test/main.cpp index edeced68d..60773e762 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -151,8 +151,6 @@ int main(int argc, char ** argv) { TST(list); TST(small_object_allocator); TST(timeout); - TST(splay_tree); - TST(fvi); TST(proof_checker); TST(simplifier); TST(bv_simplifier_plugin); diff --git a/src/test/splay_tree.cpp b/src/test/splay_tree.cpp deleted file mode 100644 index d5533ff7c..000000000 --- a/src/test/splay_tree.cpp +++ /dev/null @@ -1,175 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - splay_tree.cpp - -Abstract: - - Splay trees - -Author: - - Leonardo de Moura (leonardo) 2008-01-31. - -Revision History: - ---*/ - -#include"splay_tree_map.h" -#include"splay_tree_def.h" -#include"trace.h" -#include"vector.h" -#include"map.h" -#include"timeit.h" - -struct icomp { - int operator()(int k1, int k2) const { - return k1 - k2; - } -}; - -struct visitor { - bool m_out; - int m_prev; - unsigned m_num; - - visitor(bool f = true):m_out(f), m_prev(-1), m_num(0) {} - - void operator()(int k, int d) { - SASSERT(m_prev < k); - SASSERT(d == 2 * k); - m_num++; - m_prev = k; - if (m_out) { - TRACE_CODE(tout << k << " ";); - } - } -}; - -static void tst1(unsigned n) { - splay_tree_map s1; - svector s2(n, false); - unsigned size = 0; - - unsigned num_op = rand()%1000; - for (unsigned i = 0; i < num_op; i++) { - unsigned op = rand()%5; - if (op < 3) { - unsigned idx = rand() % n; - TRACE("splay_tree_detail", tout << "inserting: " << idx << "\n";); - if (!s2[idx]) { - size++; - } - s2[idx] = true; - s1.insert(idx, idx*2); - } - else if (op < 4) { - unsigned idx = rand() % n; - TRACE("splay_tree_detail", tout << "erasing: " << idx << "\n";); - if (s2[idx]) { - size--; - } - s2[idx] = false; - s1.erase(idx); - } - else { - SASSERT((size == 0) == s1.empty()); - for (unsigned idx = 0; idx < n; idx++) { - unsigned idx2 = rand() % n; - DEBUG_CODE( - int v; - SASSERT(s2[idx2] == s1.find(idx2, v)); - SASSERT(!s2[idx2] || v == 2*idx2); - ); - } - } - - TRACE("splay_tree", - visitor v; - s1.visit(v); - tout << "\n"; - int idx = rand()%n; - tout << "smaller than: " << idx << "\n"; - visitor v2; - s1.visit_le(v2, idx); - tout << "\n"; - tout << "greater than: " << idx << "\n"; - visitor v3; - s1.visit_ge(v3, idx); - tout << "\n";); - - visitor v(false); - s1.visit(v); - CTRACE("splay_tree", v.m_num != size, s1.display(tout); tout << "\n";); - SASSERT(v.m_num == size); - } - s1.reset(); - SASSERT(s1.empty()); - TRACE("splay_tree", - visitor v;; - s1.visit(v); - SASSERT(v.m_num == 0); - tout << "\n";); -} - -static void tst_perf(int n1, int n2, int n3, int n4, int n5) { - u_map values1; - svector idxs; - splay_tree_map values2; - - { - timeit t(true, "building: "); - for (int i = 0; i < n2; i++) { - int idx = rand() % n1; - idxs.push_back(idx); - values1.insert(idxs[i], i); - } - - for (int i = 0; i < n2; i++) { - values2.insert(idxs[i], i); - } - - } - - int s1, s2; - { - timeit t(true, "u_map: "); - s1 = 0; - for (int j = 0; j < n4; j++) { - for (int i = 0; i < n5; i++) { - int v; - values1.find(idxs[i], v); - s1 += v; - } - } - } - std::cout << s1 << "\n"; - { - timeit t(true, "splay_tree: "); - s2 = 0; - for (int j = 0; j < n4; j++) { - for (int i = 0; i < n5; i++) { - int v; - values2.find(idxs[i], v); - s2 += v; - } - } - // for (int i = 0; i < n5; i++) { - // std::cout << idxs[i] << " "; - // } - std::cout << "\n"; - // values2.display(std::cout); - } - std::cout << s2 << "\n"; - -} - -void tst_splay_tree() { - for (unsigned i = 0; i < 100; i++) { - tst1(1 + rand()%31); - tst1(1 + rand()%100); - } - // tst_perf(10000000, 1000000, 10000, 1000000, 100); -}