mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity
17283 commits 23 branches 48 tags 156 MiB
Commit graph

17283 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 9fc4015c46 remove ternary clause optimization 
Removing ternary clause optimization from sat_solver simplifies special case handling of ternary clauses throughout the sat solver and dependent solvers (pb_solver). Benchmarking on QF_BV suggests the ternary clause optimization does not have any effect. While removing ternary clause optimization two bugs in unit propagation were also uncovered: it missed propagations when the only a single undef literal remained in the non-watched literals and it did not update blocked literals in cases where it could in the watch list. These performance bugs were for general clauses, ternary clause propagation did not miss propagations (and don't use blocked literals), but fixing these issues for general clauses appear to have made ternary clause optimization irrelevant based on what was measured.
 2022-10-30 03:57:39 -07:00
Nikolaj Bjorner 0da0fa2b27 #6429 2022-10-29 13:43:07 -07:00
Nikolaj Bjorner 0e651eee04 #6421 2022-10-28 14:12:28 -07:00
Facundo Domínguez 91cdc082c4
Optimize calls to Z3_eval_smtlib2_string (#6422) 
* Allow reseting the stream of smt2::scanner

* Put the parser of parse_smt2_commands in the cmd_context

* Move parser streams to cmd_context

* Move parser fields from cmd_context to api::context

* Move forward declarations from cmd_context.h to api_context.h

* Change parse_smt2_commands_with_parser to use *& instead of **

* Add tests for Z3_eval_smtlib2_string

* Don't reuse the streams in Z3_eval_smtlib2_string

* Fix indentation

* Add back unnecessary deleted line

Co-authored-by: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
 2022-10-28 13:57:22 -07:00
Nikolaj Bjorner a409a4a677 enforce flat within QF_BV tactic, cap in-processing var-elim loops 2022-10-27 20:10:55 -07:00
Nikolaj Bjorner 1fae3aa152 rename set-flat to set-flat-and-or to allow to differentiate parameters 2022-10-27 11:22:57 -07:00
Nikolaj Bjorner fe1b4bf5ce disable ternary, fixes to propagation, make bv_rewrites for multiplier n-ary 2022-10-26 23:44:38 -07:00
Nikolaj Bjorner 5352a0106d fix #6426 2022-10-26 12:20:55 -07:00
Nikolaj Bjorner 2258b9b9b6 #6423 2022-10-26 12:06:11 -07:00
Nuno Lopes 1720addc4e remove a bunch of string copies in the API 
thanks to C++20
 2022-10-26 18:22:55 +01:00
Nikolaj Bjorner a4ece21461 toggle enable-ternary to true 2022-10-25 10:44:23 -07:00
Nikolaj Bjorner 154fed7783 introduce globally visible macro for controlling use of ternary, turn them off 2022-10-25 10:30:18 -07:00
Nikolaj Bjorner c62c5e9d23 add opportunistic, missing, bv rewrites 
- x >> x logical = 0
- ~x = -1 -x
- x * (y << z) = (x * y) << z
 2022-10-25 10:29:48 -07:00
Nikolaj Bjorner 09a2ba4931 remove artificial usage of function, it causes another compiler warning to refer to a function without arguments. 2022-10-25 10:28:25 -07:00
Nikolaj Bjorner c672c3a250 fix regression introduced in #6143 2022-10-25 09:39:11 -07:00
Nikolaj Bjorner e1a00f4917 remove unused experimental feature - diff 2022-10-24 16:13:24 -07:00
Nikolaj Bjorner 280887cc5a remove deprecated theory aware drat functionality 
it is handled by the on-clause callback that is owned by the smt solver.
 2022-10-24 08:32:10 -07:00
Nuno Lopes cb3c86736c fix build 2022-10-24 10:23:50 +01:00
Nuno Lopes 4431fd17ce memory_manager: add support for MacOS & Windows to the new size tracking system 2022-10-24 10:09:56 +01:00
Nikolaj Bjorner a24b5a64e1 #6364 proviso for ignore int 2022-10-24 00:48:57 -07:00
Nikolaj Bjorner 5c7eaec566 #6364 - remove option of redundant clauses from internalization 
gc-ing definitions leads to unsoundness when they are not replayed.
Instead of attempting to replay definitions theory internalization is irredundant by default.
This is also the old solver behavior where TH_LEMMA is essentially never used, but is valid for top-level theory lemmas.
 2022-10-24 00:38:31 -07:00
Nikolaj Bjorner c8e1e180ea prefix Boolean variables in log with b 2022-10-23 11:05:50 -07:00
Nikolaj Bjorner 6393ed78d7 remove useless log 2022-10-23 11:05:33 -07:00
Nikolaj Bjorner ddbca68270 minor formatting update 2022-10-23 11:05:09 -07:00
Nikolaj Bjorner 4a1d76cf49 #6418 - add best-effort for nested and/or (from ite literals) 2022-10-23 11:03:51 -07:00
Nikolaj Bjorner 071a1447e3 fix #6418 2022-10-23 11:03:00 -07:00
Nikolaj Bjorner e3a44254c9 fix #6415 2022-10-22 11:18:16 -07:00
Nikolaj Bjorner 7eee7914bd align format of quantifier instantiation with new core 
So far the format is

(forall ((x Int)) body) (not (body[t/x]))

The alternative could be the clause

(not (forall ((x Int)) body)) body[t/x]

they just better be consistent between engines
 2022-10-21 15:26:00 -07:00
Nikolaj Bjorner 53adc2afee update debugging information for new core 2022-10-21 15:24:44 -07:00
Nikolaj Bjorner ad5fa9433f add experiment with quot-rem encoding 
experiment seeks to determine whether quot-rem encoding can substitute the division circuit encoding.
A first test suggests it makes no difference.
 2022-10-21 09:25:45 -07:00
Nikolaj Bjorner 31914d8ecf simplify purified expressions 2022-10-21 03:47:57 -07:00
Nikolaj Bjorner 842e8057bc log also quantifier generation (besides binding) 
We add also logging for quantifier generation.
It is auxiliary information that is of use for diagnostics (axiom profiler).
 2022-10-20 17:49:15 -07:00
Nikolaj Bjorner c1b355f342 #6364 
throttle on upwards propagation of default was too restrictive
 2022-10-20 17:48:17 -07:00
Nikolaj Bjorner 6d6752b2aa #6364 2022-10-20 16:39:43 -07:00
Nikolaj Bjorner 354bc50400 Update .gitignore 2022-10-20 13:15:43 -07:00
Nikolaj Bjorner edad727cd5 #6364 
ensure substitutions are applied to eliminate internal variables from results
 2022-10-20 13:14:54 -07:00
Nikolaj Bjorner 5976978062 move std functions up for potential alignment issues 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-20 09:11:15 -07:00
Nikolaj Bjorner fc30461828 unused variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-20 09:09:06 -07:00
Nikolaj Bjorner 6292b06c67 ensure that initialization order for euf_solver is aligned 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-20 08:48:15 -07:00
Nikolaj Bjorner 2f1514a259 initialization of proof_cmds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-20 08:38:23 -07:00
Nikolaj Bjorner 65ea4925b3 initialization of proof_cmds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-20 08:37:21 -07:00
Nikolaj Bjorner 2842c27e92 #6364 2022-10-20 04:48:13 -07:00
Nikolaj Bjorner f6595c161f add examples with proof replay 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-19 17:43:56 -07:00
Nikolaj Bjorner 88d10f7fe4 add example for monitoring proof logs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-19 13:37:51 -07:00
Nikolaj Bjorner a90c4f65cf increment version per release notes 
incrementing minor version because the API has a new function.
This breaks log replay against old dlls and inclusion against z3++.h.
 2022-10-19 13:21:26 -07:00
dependabot[bot] f6d554118f
Bump docker/build-push-action from 3.1.1 to 3.2.0 (#6405) 2022-10-19 21:14:43 +01:00
Nikolaj Bjorner 4c79e63c1b Update parse-api.ts 2022-10-19 12:52:58 -07:00
Nikolaj Bjorner b084852397 update release notes, fix bug in replay of Boolean variables in new core 2022-10-19 12:12:32 -07:00
Nikolaj Bjorner 07dd1065db added API to monitor clause inferences 
See RELEASE_NOTES for more information
examples pending.
 2022-10-19 08:34:55 -07:00
Nikolaj Bjorner 77cbd89420 remove once pragma from cpp file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-18 14:57:49 -07:00