mirror of
https://github.com/Z3Prover/z3
synced 2025-04-16 22:05:36 +00:00
af54a79acc
* fixing issue #4651 * regression fix * fix #4662 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * reenabled lift_ites_throttled with an additional filter, without the filter finding the model in report #4651 goes from .02s to 20s, also updated pretty printing of regexes to be more accurate * removing temp testing variable * Allow to skip System.loadLibrary() calls from Java Native class (#4667) * using intended utility methods for sort detection * adding ack/model Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add smt params dependency Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * missing file Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * deps Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * order Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * persist fields Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * dbg build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * reset caches Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * sr Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix cmake build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * shuffle dependencies Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * warnings /errors Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * update include Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * missing cmakelists Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * update cmake Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add depend Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add depend Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * virtual method Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * path Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * move parameters from ast/rewriter to params Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * move fpa Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix warnings Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove pragma Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * dbg Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * updated sat_smt Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix #4651 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * encoding options #4665 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * expose name inclusion as optional Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix misc issues around #4661 introduced when adding lazy push/pop to selected theories Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove lazy push from theory_lra Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix dotnet build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * release nodes Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * free memory in egraph Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * avoid duplicate class names frame in sat_scc and sat_smt Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding euf Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * elaborate on smt/drat format outline, expose euf mode as config Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * mk-var during copy Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * move theory_var_list into id_var_list and utilities from smt-enode into it, prepare for theory variables in egraph Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * with bounded Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Remove duplicate binary condition. Fixes #4668. * butterfly effect on fp? Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * prepare for theory plugins Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * file Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * build fix * remove SMTFD Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * SMTFD is back (#4676) * fixing issue #4651 * regression fix * reenabled lift_ites_throttled with an additional filter, without the filter finding the model in report #4651 goes from .02s to 20s, also updated pretty printing of regexes to be more accurate * removing temp testing variable * using intended utility methods for sort detection * misc edits related to nonground regexes * bug fix of state id off by 1 calculation error and improved pretty printing with regex tooltip generated in dgml state graph * removed unused method declaration * improved id to regex value map info in generated dgml * reorgd callback function for state pretty printer * updated some comments Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: Sergey Vladimirov <vlsergey@gmail.com> Co-authored-by: Christoph M. Wintersteiger <cwinter@microsoft.com> Co-authored-by: Arie Gurfinkel <arie.gurfinkel@gmail.com> |
||
|---|---|---|
| .. | ||
| params | ||
| proto_model | ||
| tactic | ||
| arith_eq_adapter.cpp | ||
| arith_eq_adapter.h | ||
| arith_eq_solver.cpp | ||
| arith_eq_solver.h | ||
| asserted_formulas.cpp | ||
| asserted_formulas.h | ||
| cached_var_subst.cpp | ||
| cached_var_subst.h | ||
| CMakeLists.txt | ||
| cost_evaluator.cpp | ||
| cost_evaluator.h | ||
| database.h | ||
| database.smt | ||
| diff_logic.h | ||
| dyn_ack.cpp | ||
| dyn_ack.h | ||
| elim_term_ite.cpp | ||
| elim_term_ite.h | ||
| expr_context_simplifier.cpp | ||
| expr_context_simplifier.h | ||
| fingerprints.cpp | ||
| fingerprints.h | ||
| mam.cpp | ||
| mam.h | ||
| old_interval.cpp | ||
| old_interval.h | ||
| qi_queue.cpp | ||
| qi_queue.h | ||
| seq_axioms.cpp | ||
| seq_axioms.h | ||
| seq_eq_solver.cpp | ||
| seq_ne_solver.cpp | ||
| seq_offset_eq.cpp | ||
| seq_offset_eq.h | ||
| seq_regex.cpp | ||
| seq_regex.h | ||
| seq_skolem.cpp | ||
| seq_skolem.h | ||
| seq_unicode.cpp | ||
| seq_unicode.h | ||
| smt2_extra_cmds.cpp | ||
| smt2_extra_cmds.h | ||
| smt_almost_cg_table.cpp | ||
| smt_almost_cg_table.h | ||
| smt_arith_value.cpp | ||
| smt_arith_value.h | ||
| smt_b_justification.h | ||
| smt_bool_var_data.h | ||
| smt_case_split_queue.cpp | ||
| smt_case_split_queue.h | ||
| smt_cg_table.cpp | ||
| smt_cg_table.h | ||
| smt_checker.cpp | ||
| smt_checker.h | ||
| smt_clause.cpp | ||
| smt_clause.h | ||
| smt_clause_proof.cpp | ||
| smt_clause_proof.h | ||
| smt_conflict_resolution.cpp | ||
| smt_conflict_resolution.h | ||
| smt_consequences.cpp | ||
| smt_context.cpp | ||
| smt_context.h | ||
| smt_context_inv.cpp | ||
| smt_context_pp.cpp | ||
| smt_context_stat.cpp | ||
| smt_enode.cpp | ||
| smt_enode.h | ||
| smt_eq_justification.h | ||
| smt_failure.h | ||
| smt_farkas_util.cpp | ||
| smt_farkas_util.h | ||
| smt_for_each_relevant_expr.cpp | ||
| smt_for_each_relevant_expr.h | ||
| smt_implied_equalities.cpp | ||
| smt_implied_equalities.h | ||
| smt_induction.cpp | ||
| smt_induction.h | ||
| smt_internalizer.cpp | ||
| smt_justification.cpp | ||
| smt_justification.h | ||
| smt_kernel.cpp | ||
| smt_kernel.h | ||
| smt_literal.cpp | ||
| smt_literal.h | ||
| smt_lookahead.cpp | ||
| smt_lookahead.h | ||
| smt_model_checker.cpp | ||
| smt_model_checker.h | ||
| smt_model_finder.cpp | ||
| smt_model_finder.h | ||
| smt_model_generator.cpp | ||
| smt_model_generator.h | ||
| smt_parallel.cpp | ||
| smt_parallel.h | ||
| smt_quantifier.cpp | ||
| smt_quantifier.h | ||
| smt_quantifier_instances.h | ||
| smt_quantifier_stat.cpp | ||
| smt_quantifier_stat.h | ||
| smt_quick_checker.cpp | ||
| smt_quick_checker.h | ||
| smt_relevancy.cpp | ||
| smt_relevancy.h | ||
| smt_setup.cpp | ||
| smt_setup.h | ||
| smt_solver.cpp | ||
| smt_solver.h | ||
| smt_statistics.cpp | ||
| smt_statistics.h | ||
| smt_theory.cpp | ||
| smt_theory.h | ||
| smt_types.h | ||
| smt_value_sort.cpp | ||
| smt_value_sort.h | ||
| spanning_tree.h | ||
| spanning_tree_base.h | ||
| spanning_tree_def.h | ||
| theory_arith.cpp | ||
| theory_arith.h | ||
| theory_arith_aux.h | ||
| theory_arith_core.h | ||
| theory_arith_def.h | ||
| theory_arith_eq.h | ||
| theory_arith_int.h | ||
| theory_arith_inv.h | ||
| theory_arith_nl.h | ||
| theory_arith_pp.h | ||
| theory_array.cpp | ||
| theory_array.h | ||
| theory_array_bapa.cpp | ||
| theory_array_bapa.h | ||
| theory_array_base.cpp | ||
| theory_array_base.h | ||
| theory_array_full.cpp | ||
| theory_array_full.h | ||
| theory_bv.cpp | ||
| theory_bv.h | ||
| theory_datatype.cpp | ||
| theory_datatype.h | ||
| theory_dense_diff_logic.cpp | ||
| theory_dense_diff_logic.h | ||
| theory_dense_diff_logic_def.h | ||
| theory_diff_logic.cpp | ||
| theory_diff_logic.h | ||
| theory_diff_logic_def.h | ||
| theory_dl.cpp | ||
| theory_dl.h | ||
| theory_dummy.cpp | ||
| theory_dummy.h | ||
| theory_fpa.cpp | ||
| theory_fpa.h | ||
| theory_lra.cpp | ||
| theory_lra.h | ||
| theory_opt.cpp | ||
| theory_opt.h | ||
| theory_pb.cpp | ||
| theory_pb.h | ||
| theory_recfun.cpp | ||
| theory_recfun.h | ||
| theory_seq.cpp | ||
| theory_seq.h | ||
| theory_seq_empty.h | ||
| theory_special_relations.cpp | ||
| theory_special_relations.h | ||
| theory_str.cpp | ||
| theory_str.h | ||
| theory_str_mc.cpp | ||
| theory_str_regex.cpp | ||
| theory_utvpi.cpp | ||
| theory_utvpi.h | ||
| theory_utvpi_def.h | ||
| theory_wmaxsat.cpp | ||
| theory_wmaxsat.h | ||
| user_propagator.cpp | ||
| user_propagator.h | ||
| uses_theory.cpp | ||
| uses_theory.h | ||
| watch_list.cpp | ||
| watch_list.h | ||