mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-08 04:01:22 +00:00
Code Activity

Fix default quantifier weight to prevent performance regression

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2025-07-15 16:10:18 +00:00
parent 55873e17e3
commit 93f9353e9c
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/ast.h
View file

@ -2020,12 +2020,12 @@ public:
public:
quantifier * mk_quantifier(quantifier_kind k, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body,
int weight = 0, symbol const & qid = symbol::null, symbol const & skid = symbol::null,
int weight = 1, symbol const & qid = symbol::null, symbol const & skid = symbol::null,
unsigned num_patterns = 0, expr * const * patterns = nullptr,
unsigned num_no_patterns = 0, expr * const * no_patterns = nullptr);
quantifier * mk_forall(unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body,
int weight = 0, symbol const & qid = symbol::null, symbol const & skid = symbol::null,
int weight = 1, symbol const & qid = symbol::null, symbol const & skid = symbol::null,
unsigned num_patterns = 0, expr * const * patterns = nullptr,
unsigned num_no_patterns = 0, expr * const * no_patterns = nullptr) {
return mk_quantifier(forall_k, num_decls, decl_sorts, decl_names, body, weight, qid, skid, num_patterns, patterns,
@ -2033,7 +2033,7 @@ public:
}
quantifier * mk_exists(unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body,
int weight = 0, symbol const & qid = symbol::null, symbol const & skid = symbol::null,
int weight = 1, symbol const & qid = symbol::null, symbol const & skid = symbol::null,
unsigned num_patterns = 0, expr * const * patterns = nullptr,
unsigned num_no_patterns = 0, expr * const * no_patterns = nullptr) {
return mk_quantifier(exists_k, num_decls, decl_sorts, decl_names, body, weight, qid, skid, num_patterns, patterns,