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

4102 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 2bff98ca5d enable incremental bit-vector solving 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-01 09:52:48 -07:00
Christoph M. Wintersteiger 5b8d0617d4 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-09-01 17:52:30 +01:00
Christoph M. Wintersteiger 336fa6ae83 Bugfix for FP to BV conversion of UFs 2015-09-01 17:52:19 +01:00
Nikolaj Bjorner cc5d719d9e enable incremental bit-vector solving 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-01 09:48:35 -07:00
Nikolaj Bjorner 963981b3a6 fix memory alias bug and non-termination bug exposed by issue #184 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-31 14:45:10 -07:00
Nikolaj Bjorner 0ed38ed59b add option for using corr set and use partial cores 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-30 14:48:24 -07:00
Nikolaj Bjorner 7f219e84de check cancellation flag in min/max. Fixes issue #206 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-29 15:51:58 -07:00
Nikolaj Bjorner dd01f6be46 fix blockers for pd-maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-29 15:42:19 -07:00
Nikolaj Bjorner e4ce6b6d74 update pd-maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-29 14:23:32 -07:00
Nikolaj Bjorner 0bc45ca250 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-08-28 20:25:40 -07:00
Nikolaj Bjorner 2fe0c05556 tuning pd-maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-28 20:25:25 -07:00
Christoph M. Wintersteiger 8feed01034 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-08-28 15:41:16 +01:00
Christoph M. Wintersteiger f4c8463619 Bugfix for FP theory 
Fixes #207
 2015-08-28 15:41:03 +01:00
Nikolaj Bjorner f073f49ec2 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-08-27 15:43:49 -07:00
Nikolaj Bjorner 78313c614d updateing pd-maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-27 15:43:35 -07:00
Christoph M. Wintersteiger 81eecafa66 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-08-27 18:17:38 +01:00
Christoph M. Wintersteiger 081ba9093a Bugfix for FP theory; handling of UFs and interpreted functions from other theories. 2015-08-27 18:17:26 +01:00
Nikolaj Bjorner 8622356375 working on pd-maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-27 08:09:46 -07:00
Nikolaj Bjorner 7c47809973 reworking pd-maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-26 16:33:53 -07:00
Nikolaj Bjorner af9143b64a tune initial propagation for pd-maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-25 17:15:31 -07:00
Nikolaj Bjorner d00d6a3506 enable Boolean propagation in AUFBV to fix inefficiency (bit-blasting destroys simplifications that are possible by simple Boolean propagation). Fixes issue #194 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-25 13:21:33 -07:00
Nikolaj Bjorner 68b441770e Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-08-25 11:09:35 -07:00
Nikolaj Bjorner 7639eff29b retain default configuration between calls to SMT tactic so that values are not overwritten between calls to smt-setup. Fixes bug #196 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-25 11:09:10 -07:00
Nikolaj Bjorner b2ebd095cb fix for unintialized variable m_conflict_lvl 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-24 17:01:46 -07:00
Nikolaj Bjorner ef7915858b add filter to detect circumventing the default semantics of bit-vector division with the use of the sat-based bit-vector solver. Provides a way to fix issue #190 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-24 16:27:07 -07:00
Nikolaj Bjorner ee5f1ad6b6 fix issue #203: domain range was one too large 
Signed-off-by: unknown <nbjorner@nikolaj-z.redmond.corp.microsoft.com>
 2015-08-24 15:55:40 -07:00
unknown 4ce80f1aed Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-08-24 09:33:37 -07:00
Christoph M. Wintersteiger 8c11299be6 Bugfix for theory_fpa, when datatypes contain floats. 
Fixes #201.
 2015-08-24 15:09:02 +01:00
unknown 3c4b5e22b8 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-08-23 14:25:24 -07:00
Nikolaj Bjorner 46e0ff486b fix wcnf front-end and unsat case in pd 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-23 14:25:11 -07:00
Nikolaj Bjorner 149549dd52 fix wcnf front-end and unsat case in pd 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-23 14:24:51 -07:00
unknown 42c7277ea8 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-08-23 12:09:51 -07:00
Nikolaj Bjorner ee458fa601 revising pd-maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-23 12:09:07 -07:00
Nikolaj Bjorner 76c9abada2 remove dbg pp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-23 11:00:19 -07:00
unknown b06c4d985e Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-08-23 10:58:28 -07:00
unknown 2b48092541 local sat solver change 
Signed-off-by: unknown <nbjorner@nikolaj-z.redmond.corp.microsoft.com>
 2015-08-23 10:58:12 -07:00
Nikolaj Bjorner 546a9b8f03 revising pd-maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-23 10:53:39 -07:00
Nikolaj Bjorner da0c12cdba move display method to before first SAT call 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-21 18:29:36 -07:00
Nikolaj Bjorner a78fc031bc adding facility to dump wcnf benchmarks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-21 07:26:49 -07:00
Nikolaj Bjorner 954e612188 redoing pd-maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-20 18:09:43 -07:00
Nikolaj Bjorner a9807878ea reworking pd-maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-20 12:20:30 -07:00
Nikolaj Bjorner e3cb0e2d8b reworking pd-maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-20 12:06:27 -07:00
Nikolaj Bjorner 980e74b4ff add tactic to recognize small discrete domains and convert them into bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-20 06:39:11 -07:00
Nikolaj Bjorner 7c87096237 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-08-18 19:10:44 -07:00
Christoph M. Wintersteiger 9ad065a538 Bugfixes for the optimization module in the ML API 2015-08-15 23:51:43 +01:00
Nikolaj Bjorner 655b44c07b make :weight understand both decimal and integral values, remove dweight, remove deprecated commands for optimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-15 00:48:22 +02:00
Nikolaj Bjorner 94d83b7be9 n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-14 14:12:14 +02:00
Nikolaj Bjorner cd838e5cf4 fix bug reported in issue #193: MBQI needs to avoid instantiating data-types that contain model values in nested positions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-13 14:29:48 +02:00
Nikolaj Bjorner 702af71a2d Check more frequently for cancelation flags to address grep0095.stp.smt2 in issue #178. Z3 spends time in pre-processing simplification, which indicates there is some opportunity to tune this portion of the code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-11 23:14:34 +02:00
Nikolaj Bjorner 424f34d3d9 enable smt tactic to be used even if cores are enabled, as long as no cores are tracked, fixes issue #189 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-11 11:16:41 +02:00