mirror of
https://github.com/Z3Prover/z3
synced 2026-03-19 03:23:10 +00:00
6fb68ac010
* outline of signature for assignment based conflict generation Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * outline of interface contract Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove confusing construction Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add material in nra-solver to interface Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add marshaling from nlsat lemmas into core solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * tidy Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add call to check-assignment Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Nl2lin (#7795) * add linearized projection in nlsat * implement nlsat check for given assignment * add some comments * fixup loop Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * updates Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fixes Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * debug nl2lin Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Nl2lin (#7827) * fix linear projection * fix linear projection * use an explicit cell description in check_assignment * clean up (#7844) * Simplify no effect checks in nla_core.cpp Move up linear nlsat call to replace bounded nlsat. * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * detangle mess Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove the too early return Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * do not set use_nra_model to true Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * remove a comment Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add a hook to add new multiplication definitions in nla_core * add internalization routine that uses macro-expanded polynomial representation Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add internalization routine that uses macro-expanded polynomial representation Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fixup backtranslation to not use roots Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * call setup_assignment_solver instead of setup_solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * debug the setup, still not working Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * updated clang format Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * simplify Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * create polynomials with integer coefficients, use the hook to create new monomials Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * integrating changes from master related to work with polynomials Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add forgotten files Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Update nlsat_explain.cpp Remove a duplicate call * fix * move linear cell construction to levelwise * fix * fix * Port throttle and soundness fixes from master - Fix soundness: pop incomplete lemma from m_lemmas on add_lemma failure - Gracefully handle root atoms in add_lemma - Throttle check_assignment with failure counter (decrement on success) - Add arith.nl.nra_check_assignment parameter Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> * Add arith.nl.nra_check_assignment_max_fail parameter Replace hardcoded failure threshold with configurable parameter (default 10). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> * Add cha_abort_on_fail parameter to control failure counter decrement Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> * abort nla check_assignment after a set number of allowed failures Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Add missing AST query methods to Java API (#8977) * add Expr.isGround() to Java API Expose Z3_is_ground as a public method on Expr. Returns true when the expression contains no free variables. * add Expr.isLambda() to Java API Expose Z3_is_lambda as a public method on Expr. Returns true when the expression is a lambda quantifier. * add AST.getDepth() to Java API Expose Z3_get_depth as a public method on AST. Returns the maximum number of nodes on any path from root to leaf. * add ArraySort.getArity() to Java API Expose Z3_get_array_arity as a public method on ArraySort. Returns the number of dimensions of a multi-dimensional array sort. * add DatatypeSort.isRecursive() to Java API Expose Z3_is_recursive_datatype_sort as a public method on DatatypeSort. Returns true when the datatype refers to itself. * add FPExpr.isNumeral() to Java API Expose Z3_fpa_is_numeral as a public method on FPExpr. Returns true when the expression is a concrete floating-point value. * add isGroundExample test to JavaExample Test Expr.isGround() on constants, variables, and compound expressions. * add astDepthExample test to JavaExample Test AST.getDepth() on leaf nodes and nested expressions to verify the depth computation. * add arrayArityExample test to JavaExample Test ArraySort.getArity() on single-domain and multi-domain array sorts. * add recursiveDatatypeExample test to JavaExample Test DatatypeSort.isRecursive() on a recursive list datatype and a non-recursive pair datatype. * add fpNumeralExample test to JavaExample Test FPExpr.isNumeral() on a floating point constant and a symbolic variable. * add isLambdaExample test to JavaExample Test Expr.isLambda() on a lambda expression and a plain variable. * change the default number of failures in check_assignment to 7 Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Fix high and medium priority API coherence issues (Go, Java, C++, TypeScript) (#8983) * Initial plan * Add missing API functions to Go, Java, C++, and TypeScript bindings 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> * qf-s-benchmark: debug build + seq tracing + seq-fast/nseq-slow trace analysis (#8988) * Initial plan * Update qf-s-benchmark: debug build, seq tracing, trace analysis 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> * disable linear approximation by default to check the merge Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * set check_assignment to true Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fix restore_x by recalulating new column values Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fix restore_x by recalulating new column values Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fix a memory leak Signed-off-by: Lev Nachmanson <levnach@hotmail.com> --------- Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> Signed-off-by: Lev Nachmanson <levnach@hotmail.com> Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: ValentinPromies <44966217+ValentinPromies@users.noreply.github.com> Co-authored-by: Valentin Promies <valentin.promies@rwth-aachen.de> Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: Angelica Moreira <48168649+angelica-moreira@users.noreply.github.com> Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> |
||
|---|---|---|
| .. | ||
| arith_rewriter_params.pyg | ||
| array_rewriter_params.pyg | ||
| bit_blaster_params.h | ||
| bool_rewriter_params.pyg | ||
| bv_rewriter_params.pyg | ||
| CMakeLists.txt | ||
| context_params.cpp | ||
| context_params.h | ||
| dyn_ack_params.cpp | ||
| dyn_ack_params.h | ||
| fpa2bv_rewriter_params.pyg | ||
| fpa_rewriter_params.pyg | ||
| pattern_inference_params.cpp | ||
| pattern_inference_params.h | ||
| pattern_inference_params_helper.pyg | ||
| poly_rewriter_params.pyg | ||
| preprocessor_params.cpp | ||
| preprocessor_params.h | ||
| qi_params.cpp | ||
| qi_params.h | ||
| rewriter_params.pyg | ||
| sat_params.pyg | ||
| seq_rewriter_params.pyg | ||
| sls_params.pyg | ||
| smt_parallel_params.pyg | ||
| smt_params.cpp | ||
| smt_params.h | ||
| smt_params_helper.pyg | ||
| solver_params.pyg | ||
| tactic_params.pyg | ||
| theory_arith_params.cpp | ||
| theory_arith_params.h | ||
| theory_array_params.cpp | ||
| theory_array_params.h | ||
| theory_bv_params.cpp | ||
| theory_bv_params.h | ||
| theory_datatype_params.h | ||
| theory_pb_params.cpp | ||
| theory_pb_params.h | ||
| theory_seq_params.cpp | ||
| theory_seq_params.h | ||