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

55 commits

Author SHA1 Message Date
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
Nikolaj Bjorner
eead1bbc48 missing else 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-23 09:24:39 -07:00
Nikolaj Bjorner
e1d5f484f1 simplify result from tactics, remove unused features from difference logic solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-04-23 08:46:46 -07:00
Leonardo de Moura
9abcde9a35 Fix typos 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-03-25 14:42:18 -07:00
Leonardo de Moura
cec328cfdc Add get_sort(expr * n) function that does not depend on ast_manager. Move power_of_two to rational class. Add arith_recognizers and bv_recognizers classes. The two new classes contain the 'read-only' methods from arith_util and bv_util. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-18 14:44:51 -08:00
Leonardo de Moura
4df172e971 Fix file name (use same naming convention) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-14 09:04:20 -08:00
Leonardo de Moura
e0f4d870fd Removed auxiliary constants created by the nnf tactic from Z3 models. Fixed model.compact parameter propagation problem. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-13 14:03:58 -08:00
Leonardo de Moura
a07b459fdf Added is_unique_value. Its semantics is equal to the old is_value method. The contract for is_value changed. See comments at ast.h for more information. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-07 12:53:51 -08:00
Leonardo de Moura
9754ccf8a1 fixing problems with the new parameter framework 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-04 11:16:42 -08:00
Leonardo de Moura
cf28cbab0a saved params work 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-29 17:19:12 -08:00
Leonardo de Moura
b70687acc9 cleanning solver initialization, and fixing named assertion support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-02 16:35:08 -07:00
Leonardo de Moura
b629dd7fdd fixed der tactic installation command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-30 08:38:20 -07:00