3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-17 22:35:35 +00:00
z3/src/smt
Leonardo de Moura 3da69a4f1b Integrated structured branch into unstable branch (the official 'working in progress' branch)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-24 13:19:19 -07:00
..
tactic reorganizing the code 2012-10-23 21:53:34 -07:00
user_plugin reorganizing the code 2012-10-23 21:53:34 -07:00
arith_eq_adapter.cpp checkpoint 2012-10-21 13:32:12 -07:00
arith_eq_adapter.h checkpoint 2012-10-21 13:32:12 -07:00
arith_eq_solver.cpp checkpoint 2012-10-21 13:32:12 -07:00
arith_eq_solver.h checkpoint 2012-10-21 13:32:12 -07:00
arith_solver_plugin.cpp checkpoint 2012-10-21 13:32:12 -07:00
arith_solver_plugin.h checkpoint 2012-10-21 13:32:12 -07:00
asserted_formulas.cpp Integrated structured branch into unstable branch (the official 'working in progress' branch) 2012-10-24 13:19:19 -07:00
asserted_formulas.h checkpoint 2012-10-23 12:12:59 -07:00
cached_var_subst.cpp checkpoint 2012-10-21 13:32:12 -07:00
cached_var_subst.h checkpoint 2012-10-21 13:32:12 -07:00
cost_evaluator.cpp checkpoint 2012-10-21 13:32:12 -07:00
cost_evaluator.h checkpoint 2012-10-21 13:32:12 -07:00
ctx_solver_simplify_tactic.cpp checkpoint 2012-10-21 20:46:41 -07:00
ctx_solver_simplify_tactic.h checkpoint 2012-10-21 20:46:41 -07:00
database.h checkpoint 2012-10-21 13:32:12 -07:00
database.smt checkpoint 2012-10-21 13:32:12 -07:00
default_solver.cpp Isolating reg_decl_plugins 2012-10-24 11:27:50 -07:00
default_solver.h missing files... 2012-10-22 06:01:04 -07:00
dyn_ack.cpp checkpoint 2012-10-21 13:32:12 -07:00
dyn_ack.h checkpoint 2012-10-21 13:32:12 -07:00
expr_context_simplifier.cpp checkpoint 2012-10-21 13:32:12 -07:00
expr_context_simplifier.h checkpoint 2012-10-21 13:32:12 -07:00
fingerprints.cpp checkpoint 2012-10-21 13:32:12 -07:00
fingerprints.h checkpoint 2012-10-21 13:32:12 -07:00
mam.cpp checkpoint 2012-10-21 13:32:12 -07:00
mam.h checkpoint 2012-10-21 13:32:12 -07:00
mk_database.sh checkpoint 2012-10-21 20:46:41 -07:00
ni_solver.cpp checkpoint 2012-10-21 20:46:41 -07:00
ni_solver.h checkpoint 2012-10-21 20:46:41 -07:00
qi_queue.cpp checkpoint 2012-10-21 13:32:12 -07:00
qi_queue.h checkpoint 2012-10-21 13:32:12 -07:00
smt_almost_cg_table.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_almost_cg_table.h checkpoint 2012-10-21 13:32:12 -07:00
smt_b_justification.h checkpoint 2012-10-21 13:32:12 -07:00
smt_bool_var_data.h checkpoint 2012-10-21 13:32:12 -07:00
smt_case_split_queue.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_case_split_queue.h checkpoint 2012-10-21 13:32:12 -07:00
smt_cg_table.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_cg_table.h checkpoint 2012-10-21 13:32:12 -07:00
smt_checker.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_checker.h checkpoint 2012-10-21 13:32:12 -07:00
smt_clause.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_clause.h checkpoint 2012-10-21 13:32:12 -07:00
smt_conflict_resolution.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_conflict_resolution.h checkpoint 2012-10-21 13:32:12 -07:00
smt_context.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_context.h checkpoint 2012-10-21 13:32:12 -07:00
smt_context_inv.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_context_pp.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_context_stat.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_enode.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_enode.h checkpoint 2012-10-21 13:32:12 -07:00
smt_eq_justification.h checkpoint 2012-10-21 13:32:12 -07:00
smt_failure.h checkpoint 2012-10-21 13:32:12 -07:00
smt_for_each_relevant_expr.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_for_each_relevant_expr.h checkpoint 2012-10-21 13:32:12 -07:00
smt_implied_equalities.cpp checkpoint 2012-10-21 20:04:34 -07:00
smt_implied_equalities.h checkpoint 2012-10-21 20:04:34 -07:00
smt_internalizer.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_justification.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_justification.h checkpoint 2012-10-21 13:32:12 -07:00
smt_literal.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_literal.h checkpoint 2012-10-21 13:32:12 -07:00
smt_model_checker.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_model_checker.h checkpoint 2012-10-21 13:32:12 -07:00
smt_model_finder.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_model_finder.h checkpoint 2012-10-21 13:32:12 -07:00
smt_model_generator.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_model_generator.h checkpoint 2012-10-21 13:32:12 -07:00
smt_quantifier.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_quantifier.h checkpoint 2012-10-21 13:32:12 -07:00
smt_quantifier_instances.h checkpoint 2012-10-21 13:32:12 -07:00
smt_quantifier_stat.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_quantifier_stat.h checkpoint 2012-10-21 13:32:12 -07:00
smt_quick_checker.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_quick_checker.h checkpoint 2012-10-21 13:32:12 -07:00
smt_relevancy.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_relevancy.h checkpoint 2012-10-21 13:32:12 -07:00
smt_setup.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_setup.h checkpoint 2012-10-21 13:32:12 -07:00
smt_solver.cpp Reorganizing the code 2012-10-20 20:42:28 -07:00
smt_solver.h Reorganizing the code 2012-10-20 20:42:28 -07:00
smt_solver_strategy.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_solver_strategy.h Reorganizing the code 2012-10-20 22:03:58 -07:00
smt_statistics.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_statistics.h checkpoint 2012-10-21 13:32:12 -07:00
smt_theory.cpp checkpoint 2012-10-21 13:32:12 -07:00
smt_theory.h checkpoint 2012-10-21 13:32:12 -07:00
smt_theory_var_list.h checkpoint 2012-10-21 13:32:12 -07:00
smt_types.h checkpoint 2012-10-21 13:32:12 -07:00
solver_plugin.h checkpoint 2012-10-21 13:32:12 -07:00
theory_arith.cpp checkpoint 2012-10-21 13:32:12 -07:00
theory_arith.h checkpoint 2012-10-21 13:32:12 -07:00
theory_arith_aux.h checkpoint 2012-10-21 13:32:12 -07:00
theory_arith_core.h checkpoint 2012-10-21 13:32:12 -07:00
theory_arith_def.h checkpoint 2012-10-21 13:32:12 -07:00
theory_arith_eq.h checkpoint 2012-10-21 13:32:12 -07:00
theory_arith_int.h checkpoint 2012-10-21 13:32:12 -07:00
theory_arith_inv.h checkpoint 2012-10-21 13:32:12 -07:00
theory_arith_nl.h checkpoint 2012-10-21 13:32:12 -07:00
theory_arith_pp.h checkpoint 2012-10-21 13:32:12 -07:00
theory_array.cpp checkpoint 2012-10-21 13:32:12 -07:00
theory_array.h checkpoint 2012-10-21 13:32:12 -07:00
theory_array_base.cpp checkpoint 2012-10-21 13:32:12 -07:00
theory_array_base.h checkpoint 2012-10-21 13:32:12 -07:00
theory_array_full.cpp checkpoint 2012-10-21 13:32:12 -07:00
theory_array_full.h checkpoint 2012-10-21 13:32:12 -07:00
theory_bv.cpp checkpoint 2012-10-21 13:32:12 -07:00
theory_bv.h checkpoint 2012-10-21 13:32:12 -07:00
theory_datatype.cpp checkpoint 2012-10-21 13:32:12 -07:00
theory_datatype.h checkpoint 2012-10-21 13:32:12 -07:00
theory_dense_diff_logic.cpp checkpoint 2012-10-21 13:32:12 -07:00
theory_dense_diff_logic.h checkpoint 2012-10-21 13:32:12 -07:00
theory_dense_diff_logic_def.h checkpoint 2012-10-21 13:32:12 -07:00
theory_diff_logic.cpp checkpoint 2012-10-21 13:32:12 -07:00
theory_diff_logic.h checkpoint 2012-10-21 13:32:12 -07:00
theory_diff_logic_def.h checkpoint 2012-10-21 13:32:12 -07:00
theory_dl.cpp checkpoint 2012-10-21 13:32:12 -07:00
theory_dl.h checkpoint 2012-10-21 13:32:12 -07:00
theory_dummy.cpp checkpoint 2012-10-21 13:32:12 -07:00
theory_dummy.h checkpoint 2012-10-21 13:32:12 -07:00
theory_instgen.cpp checkpoint 2012-10-21 13:32:12 -07:00
theory_instgen.h checkpoint 2012-10-21 13:32:12 -07:00
theory_seq_empty.h checkpoint 2012-10-21 13:32:12 -07:00
union_find.h checkpoint 2012-10-23 12:12:59 -07:00
user_rewriter.cpp checkpoint 2012-10-21 13:32:12 -07:00
user_rewriter.h checkpoint 2012-10-21 13:32:12 -07:00
uses_theory.cpp checkpoint 2012-10-21 13:32:12 -07:00
uses_theory.h checkpoint 2012-10-21 13:32:12 -07:00
watch_list.cpp checkpoint 2012-10-21 13:32:12 -07:00
watch_list.h checkpoint 2012-10-21 13:32:12 -07:00