mirror of
https://github.com/Z3Prover/z3
synced 2025-10-25 08:54:35 +00:00
6044389446
* very basic setup * ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove verbose output Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix #7745 axioms for len(substr(...)) escaped due to nested rewriting * ensure atomic constraints are processed by arithmetic solver * #7739 optimization add simplification rule for at(x, offset) = "" Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions. The example highlights some opportunities for simplification, noteworthy at(..) = "". The example is solved in both versions after adding this simplification. * fix unsound len(substr) axiom Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * FreshConst is_sort (#7748) * #7750 add pre-processing simplification * Add parameter validation for selected API functions * updates to ac-plugin fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop. * enable passive, add check for bloom up-to-date * add top-k fixed-sized min-heap priority queue for top scoring literals * set up worker thread batch manager for multithreaded batch cubes paradigm, need to debug as I am getting segfault still * fix bug in parallel solving batch setup * fix bug * allow for internalize implies * disable pre-processing during cubing * debugging * remove default constructor * remove a bunch of string copies * Update euf_ac_plugin.cpp include reduction rules in forward simplification * Update euf_completion.cpp try out restricting scope of equalities added by instantation * Update smt_parallel.cpp Drop non-relevant units from shared structures. * process cubes as lists of individual lits * merge * Add support for Algebraic Datatypes in JavaScript/TypeScript bindings (#7734) * Initial plan * Add datatype type definitions to types.ts (work in progress) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype type definitions with working TypeScript compilation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Implement core datatype functionality with TypeScript compilation success Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype implementation with full Context integration and tests Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * chipping away at the new code structure * comments * debug infinite recursion and split cubes on existing split atoms that aren't in the cube * share lemmas, learn from unsat core, try to debug a couple of things, there was a subtle bug that i have a hard time repro'ing * merge * fix #7603: race condition in Ctrl-C handling (#7755) * fix #7603: race condition in Ctrl-C handling * fix race in cancel_eh * fix build * add arithemtic saturation * add an option to register callback on quantifier instantiation Suppose a user propagator encodes axioms using quantifiers and uses E-matching for instantiation. If it wants to implement a custom priority scheme or drop some instances based on internal checks it can register a callback with quantifier instantiation * missing new closure Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add Z3_solver_propagate_on_binding to ml callback declarations Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add python file Signed-off-by: Lev Nachmanson <levnach@Levs-MacBook-Pro.local> * debug under defined calls Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * more untangle params Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * precalc parameters to define the eval order Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * remove a printout Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * rename a Python file Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add on_binding callbacks across APIs update release notes, add to Java, .Net, C++ * use jboolean in Native interface Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * register on_binding attribute Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix java build for java bindings Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * avoid interferring side-effects in function calls Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove theory_str and classes that are only used by it * remove automata from python build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove ref to theory_str Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * get the finest factorizations before project Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * rename add_lcs to add_lc Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * resolve bad bug about l2g and g2l translators using wrong global context. add some debug prints * initial attempt at dynamically switching from greedy to frugal splitting strategy in return_cubes. need to test. also there is some bug where the threads take forever to cancel? * Update RELEASE_NOTES.md * resolve bug about not translating managers correctly for the second phase of the greedy cubing, and the frugal fallback --------- Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> Signed-off-by: Lev Nachmanson <levnach@Levs-MacBook-Pro.local> Signed-off-by: Lev Nachmanson <levnach@hotmail.com> Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com> Co-authored-by: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt> Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Lev Nachmanson <levnach@hotmail.com> |
||
|---|---|---|
| .. | ||
| fuzzing | ||
| lp | ||
| algebraic.cpp | ||
| api.cpp | ||
| api_bug.cpp | ||
| arith_rewriter.cpp | ||
| arith_simplifier_plugin.cpp | ||
| ast.cpp | ||
| bdd.cpp | ||
| bit_blaster.cpp | ||
| bit_vector.cpp | ||
| bits.cpp | ||
| buffer.cpp | ||
| chashtable.cpp | ||
| check_assumptions.cpp | ||
| CMakeLists.txt | ||
| cnf_backbones.cpp | ||
| cube_clause.cpp | ||
| datalog_parser.cpp | ||
| ddnf.cpp | ||
| diff_logic.cpp | ||
| distribution.cpp | ||
| dl_context.cpp | ||
| dl_product_relation.cpp | ||
| dl_query.cpp | ||
| dl_relation.cpp | ||
| dl_table.cpp | ||
| dl_util.cpp | ||
| dlist.cpp | ||
| doc.cpp | ||
| egraph.cpp | ||
| escaped.cpp | ||
| euf_arith_plugin.cpp | ||
| euf_bv_plugin.cpp | ||
| ex.cpp | ||
| expr_rand.cpp | ||
| expr_substitution.cpp | ||
| ext_numeral.cpp | ||
| f2n.cpp | ||
| factor_rewriter.cpp | ||
| finder.cpp | ||
| fixed_bit_vector.cpp | ||
| for_each_file.cpp | ||
| for_each_file.h | ||
| get_consequences.cpp | ||
| get_implied_equalities.cpp | ||
| hashtable.cpp | ||
| heap.cpp | ||
| heap_trie.cpp | ||
| hilbert_basis.cpp | ||
| ho_matcher.cpp | ||
| horn_subsume_model_converter.cpp | ||
| hwf.cpp | ||
| im_float_config.h | ||
| inf_rational.cpp | ||
| interval.cpp | ||
| karr.cpp | ||
| list.cpp | ||
| main.cpp | ||
| map.cpp | ||
| matcher.cpp | ||
| memory.cpp | ||
| model2expr.cpp | ||
| model_based_opt.cpp | ||
| model_evaluator.cpp | ||
| model_retrieval.cpp | ||
| mpbq.cpp | ||
| mpf.cpp | ||
| mpff.cpp | ||
| mpfx.cpp | ||
| mpq.cpp | ||
| mpz.cpp | ||
| nlarith_util.cpp | ||
| nlsat.cpp | ||
| no_overflow.cpp | ||
| object_allocator.cpp | ||
| old_interval.cpp | ||
| optional.cpp | ||
| parray.cpp | ||
| pb2bv.cpp | ||
| pdd.cpp | ||
| pdd_solver.cpp | ||
| permutation.cpp | ||
| polynomial.cpp | ||
| polynorm.cpp | ||
| prime_generator.cpp | ||
| proof_checker.cpp | ||
| qe_arith.cpp | ||
| quant_elim.cpp | ||
| quant_solve.cpp | ||
| random.cpp | ||
| rational.cpp | ||
| rcf.cpp | ||
| region.cpp | ||
| sat_local_search.cpp | ||
| sat_lookahead.cpp | ||
| sat_user_scope.cpp | ||
| scoped_timer.cpp | ||
| scoped_vector.cpp | ||
| simple_parser.cpp | ||
| simplex.cpp | ||
| simplifier.cpp | ||
| sls_seq_plugin.cpp | ||
| sls_test.cpp | ||
| small_object_allocator.cpp | ||
| smt2print_parse.cpp | ||
| smt_context.cpp | ||
| solver_pool.cpp | ||
| sorting_network.cpp | ||
| stack.cpp | ||
| string_buffer.cpp | ||
| substitution.cpp | ||
| symbol.cpp | ||
| symbol_table.cpp | ||
| tbv.cpp | ||
| test_util.h | ||
| theory_dl.cpp | ||
| theory_pb.cpp | ||
| timeout.cpp | ||
| total_order.cpp | ||
| totalizer.cpp | ||
| trigo.cpp | ||
| udoc_relation.cpp | ||
| uint_set.cpp | ||
| upolynomial.cpp | ||
| value_generator.cpp | ||
| value_sweep.cpp | ||
| var_subst.cpp | ||
| vector.cpp | ||
| zstring.cpp | ||