mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-19 07:09:03 +00:00
Code Activity
5124 commits 23 branches 48 tags 157 MiB
Commit graph

148 commits

Author SHA1 Message Date
Nikolaj Bjorner d614fedde2 more merges with qsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 12:41:41 -07:00
Nikolaj Bjorner f951372f03 fix regression in internalizing bit-vectors, reported by Mikolas Janota 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-18 13:54:42 -07:00
Christoph M. Wintersteiger 9dd53c091a guard on m_preprocess in inc_sat_solver 2016-03-11 12:02:49 +00:00
Nikolaj Bjorner 335a1dba6e guarding bb_rewriter now that it gets reset 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-08 16:50:06 -08:00
Nikolaj Bjorner 5994c5a948 fix partial model tracking over cancellation/exceptions, reported by August Shi. Fix regression test for fp-to-real, reset the pre-processor in inc_sat_solver on exceptions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-07 16:42:29 -08:00
Christoph M. Wintersteiger a51201298c Bugfix for assumptions in inc_sat_solver 2016-03-04 14:42:38 +00:00
Christoph M. Wintersteiger 1aeea763ff Assertion fix in inc_sat_solver 2016-03-02 18:39:28 +00:00
Christoph M. Wintersteiger bf40bb8005 Bugfix for inc_sat_solver 2016-03-02 18:27:01 +00:00
Christoph M. Wintersteiger 68416bf6bc whitespace 2016-03-02 18:25:56 +00:00
Nikolaj Bjorner 9efc7f4aea turn on model completion in validation code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-29 09:06:20 -08:00
Dan Liew 6c966bba59 Fix incorrect (off by one) bound check. Also assert that we don't 
increment ``m_num_segments`` beyond the maximum value
(``c_max_segments``).

This is related to #436.

When doing an AddressSanitized build and running the ``c_example``
it looks like Z3 tries to create too many segments and index out of
bounds. Fixing the checks here causes them to fail which should help
us narrow down the problem.
 2016-02-16 14:04:21 +00:00
Nikolaj Bjorner 5ce85aba40 removing const qualifiers, perhaps this helps for #420 and adding assert to enable Clang analysis earlier for issue #440 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-09 22:23:37 +00:00
Nikolaj Bjorner 85d44c5d66 fix axioms for extract, add extensionality checking for shared variables, convert exceptions to unknown status per #419 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-18 11:09:41 +05:30
Nikolaj Bjorner 00f3a1fe81 fix memory leak in SAT solver exposed by regression tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-06 11:47:45 -08:00
Nikolaj Bjorner aec5a38b14 fix memory leak in SAT solver exposed by regression tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-06 11:44:55 -08:00
Nikolaj Bjorner a7e2fb31e3 updates to resource exceptions, update master possibly handle pull request issue 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-12 11:36:49 -08:00
Nikolaj Bjorner 2a051719d8 cleanup deprecated critical sections, fix cancellation for par_or_else tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-12 09:43:00 -08:00
Nikolaj Bjorner baee4225a7 reworking cancellation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-11 16:21:24 -08:00
Nikolaj Bjorner c1a6163bda disable aig tactic in inc_sat_solver (it can blow up the size of formulas significantly without sharing) and fix configuration update bug for optimization context exposed in example by Corina 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-20 14:34:31 -08:00
Nikolaj Bjorner c58e640563 extract labels for optimal model. Fix to #325 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-18 14:53:08 -08:00
Nikolaj Bjorner 1758799ef4 add translate facility to inc_sat_solver. Limit lemma copying to unit lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-07 10:00:14 -08:00
Nikolaj Bjorner b4cb51cdb3 working on Forking/Serializing a z3 Solver #209 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-06 17:29:24 -08:00
Nikolaj Bjorner 9b3e242990 adding rlimit resource limit facility to provide platform and architecture independent method for canceling activities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-28 13:37:59 -07:00
Christoph M. Wintersteiger 79d69cd5f0 Added FP to_ieee_bv to fpa_rewriter to enable model evaluation. 2015-09-16 12:57:05 +01:00
Nikolaj Bjorner f94152c857 fix build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-15 10:54:01 +02:00
Nikolaj Bjorner 2bff98ca5d enable incremental bit-vector solving 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-01 09:52:48 -07: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 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 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 2fe0c05556 tuning pd-maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-28 20:25:25 -07:00
Nikolaj Bjorner 78313c614d updateing pd-maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-27 15:43:35 -07: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 b2ebd095cb fix for unintialized variable m_conflict_lvl 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-24 17:01:46 -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 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 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
Christoph M. Wintersteiger 5e0aaee2c7 Made num_clauses in sat_solver public 2015-08-04 15:26:03 +01:00