mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity
5060 commits 24 branches 48 tags 158 MiB
Commit graph

66 commits

Author SHA1 Message Date
Nuno Lopes
aed4619066 reduce-args: fixed unsoundness introduced in my previous commit 
skip an UF arg if it's quantified
e.g. forall a . f(a, b) -> f(b) (but not f)
 2016-03-17 13:14:43 +00:00
Nuno Lopes
d6c3260db7 reduce_args_tactic: make it aware that 'a + const' may be a unique value in bv theory 
it allows us to remove UFs that are of the form f(a + 1), f(a + 2), etc..
 2016-03-10 10:15:09 +00:00
Nikolaj Bjorner
03a0a6f6a1 refactor occurrence utility for common use (to be used in ctx_simplifier) per Nuno's suggestion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-09 15:53:02 -08:00
Nuno Lopes
e7a360ca08 ctx_simplify: remove virtual push() method 2016-02-28 17:57:40 +00:00
Nuno Lopes
c693c990df bv_bounds: speedup up to 10x in larger formulas 
introduce a may_simplify() function to short-circuit evaluation of expression trees that are guaranteed to not be simplifiable
 2016-02-25 16:53:35 +00:00
Nuno Lopes
64888b6b19 ctx_simplify: fix bug in simplification of or exprs 
this triggered when the or covers the whole space -> true
 2016-02-23 10:37:01 +00:00
Nikolaj Bjorner
63c138c08e add option to enable equality propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-21 11:16:13 -08:00
Nikolaj Bjorner
d4f41c0420 add goal context for simplifier, disable equality creation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-20 10:13:24 -08:00
Nuno Lopes
7d3af70a63 ctx-simplify: fix mem leak of simplifier 2016-02-19 11:08:01 +00:00
Nuno Lopes
121b3b60f3 bv_bounds/ctx_simplify: improve handling of (ite x a b) where (not x) is proved to be false 2016-02-19 09:42:42 +00:00
Nuno Lopes
d32b4c71d1 [bv_bounds] introduce a tight bit in intervals to denote they are tight (over and under approx) 
use this to ensure certain transformations remain sound
 2016-02-18 15:53:11 +00:00
Nuno Lopes
c05a0dfa61 revert my previous attempt to simplify the destructor of ctx-simplify 
there can be assertions at level 0
 2016-02-16 13:10:17 +00:00
Nuno Lopes
293566d464 ctx-simplify: simplify destructor 2016-02-16 09:53:04 +00:00
Nuno Lopes
98c5a5c86c move ctx_propagate_assertions class to .cpp file 2016-02-16 09:34:45 +00:00
Nikolaj Bjorner
07953342ac Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-15 17:29:54 -08:00
Nikolaj Bjorner
d3805bbdf6 fix location of level retrieval 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-15 17:29:46 -08:00
Nuno Lopes
96f6bf7028 ctx_simplify: simplify ite if then/else values become equal 2016-02-15 12:06:20 +00:00
Nikolaj Bjorner
45999b254c hoist simplifier functionality out of context loop to allow plugging in other contextual simplification methods 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-12 18:58:37 +00:00
Nikolaj Bjorner
eae17a43a2 Fix #430: disable rewriting of concatentations with constants because it breaks equality propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-05 11:00:17 +00:00
Nikolaj Bjorner
cf970fd76a Fix #430: disable rewriting of concatentations with constants because it breaks equality propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-05 10:59:24 +00:00
Nikolaj Bjorner
8e26c97782 tuning bit-vector operations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-21 13:09:03 +02: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
4132fc2d91 ensure limit children are safe for race conditions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-12 10:18:51 -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
981f8226fe moving to resource managed cancellation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-11 13:36:47 -08:00
Nikolaj Bjorner
76c9abada2 remove dbg pp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-23 11:00:19 -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
4bc044c982 update header guards to be C++ style. Fixes issue #9 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-08 23:18:40 -07:00
Nikolaj Bjorner
5f484c069b fix distribute forall, fixes issue #138 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-23 14:15:14 +02:00
Nikolaj Bjorner
301f441801 bypass simplifier if (m_is_clausal) { 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-22 09:02:08 -07:00
Nikolaj Bjorner
e6725b2344 merge unstable into opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-26 12:12:24 -07:00
Nikolaj Bjorner
904ab4bf9e address race condition in cleanup methods 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-05 11:18:34 -07:00
Nikolaj Bjorner
19050d1c4c merge Fixedpoint.cs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-28 12:20:48 -07:00
Nikolaj Bjorner
103e49d9b4 Add option to control explosion of cofactor-term-ite following example by Anvesh 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-06-18 09:53:47 -07:00
Nikolaj Bjorner
1ed7643d32 Add option to control explosion of cofactor-term-ite following example by Anvesh 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-06-18 09:52:59 -07:00
Nikolaj Bjorner
2c69aa0df1 fix duplicate class 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-22 00:06:34 -07:00
Nikolaj Bjorner
c14c65465a working on stand-alone simplex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-26 19:46:42 -08:00
Nikolaj Bjorner
3fa0e6f3fb testing decomposition during pre-processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-02 16:05:26 -08:00
Nikolaj Bjorner
8d0d123a4c pareto take 3 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-02 01:45:34 -08:00
Nikolaj Bjorner
a307bd67e0 pareto take 3 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-02 01:35:31 -08:00
Nikolaj Bjorner
a0e98ca39b working on pb pre-processing/subsumption 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-26 10:14:05 -08:00
Nikolaj Bjorner
0641c4f694 working on pre-processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-26 09:53:33 -08:00
Nikolaj Bjorner
70c4432bb4 working on pb pre-processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-23 13:22:21 -08:00
Nikolaj Bjorner
0c2ec6951a working on pre-processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-23 03:25:22 -08:00
Nikolaj Bjorner
24f2fd380c adding pre-processing of BP constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-23 01:33:24 -08:00
Anh-Dung Phan
034b33b6da Remove m_final from spanning tree representation 2013-11-06 13:30:29 -08:00
Nikolaj Bjorner
89989627d0 add blast method for ite terms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-04 13:33:02 -08:00
Nikolaj Bjorner
9b34350646 test output predicates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-10-13 06:25:26 -07:00
Leonardo de Moura
2b59f2ecc2 Fix issue https://z3.codeplex.com/workitem/37 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-06 18:29:29 -07:00