mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-14 16:36:39 +00:00
Code Activity
2015 commits 42 branches 51 tags 169 MiB
Commit graph

207 commits

Author SHA1 Message Date
Christoph M. Wintersteiger
71e5f03b44 build fix 2015-01-21 13:04:05 +00:00
Christoph M. Wintersteiger
83023c7211 build fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 13:02:18 +00:00
Christoph M. Wintersteiger
0746ede537 BV SLS: Final adjustments 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-20 15:59:25 +00:00
Christoph M. Wintersteiger
61ba7f5e09 Merge branch 'bvsls' of https://git01.codeplex.com/z3 into unstable 
Conflicts:
	src/tactic/portfolio/default_tactic.cpp

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-20 15:15:31 +00:00
Christoph M. Wintersteiger
d20c7bc9ee Added is_qfaufbv_probe and is_qfauflia_probe. 
Potential performance disruption for some users:
Changed default_tactic to call the respective tactics,
where previously they would have run the default 'smt'
tactic.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 18:19:43 +00:00
Christoph M. Wintersteiger
d4ecc3c1be Disabled BV-SLS as default tactic in anticipation for integration 
with the unstable branch.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 15:59:20 +00:00
Christoph M. Wintersteiger
1f29b3e0a9 Merge branch 'unstable' of https://git01.codeplex.com/z3 into bvsls 2014-12-19 12:33:03 +00:00
Christoph M. Wintersteiger
75bae1b00c BV-SLS optimization 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-12-19 12:32:57 +00:00
Nuno Lopes
1a396b0bd2 [BV size reduction] fix bug in detection of signed upperbound 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-11-25 18:13:24 +00:00
Christoph M. Wintersteiger
53cfa47214 bugfix for bv_size_reduction 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-11-25 14:22:50 +00:00
Christoph M. Wintersteiger
213d816c0a Bugfix for bv_size_reduction. Thanks to user rsas for reporting this isse! 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-11-24 18:10:54 +00:00
Christoph M. Wintersteiger
cb3e9c9644 Bugfix for FPA models 2014-10-25 16:58:16 +01:00
Nikolaj Bjorner
8cf21dc242 fix tactic parameter checking to API, deal with compiler warnings in api_interp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-08 13:47:55 -07:00
Nikolaj Bjorner
b8b5c4d5b4 disable blanket validation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-08 13:21:34 -07:00
Nikolaj Bjorner
335f9a9be1 add parameter validation to tactic parameters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-08 10:55:24 -07:00
Christoph M. Wintersteiger
6b37b847a0 merge fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-09-11 00:27:37 +01:00
Christoph M. Wintersteiger
3660c617ea Merge branch 'unstable' of https://git01.codeplex.com/z3 into bvsls 
Conflicts:
	src/tactic/sls/sls_tactic.cpp

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-09-11 00:19:05 +01:00
Nikolaj Bjorner
36816e3b2f clear cache for crash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-06 19:03:37 -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
e4dedbbefc fix quantifier elimination bugs reported by Berdine and Bornat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-14 15:38:22 +02:00
Nikolaj Bjorner
4f7d872d59 fix model transformation bug in bit blaster rule transformer, reported by Sagar Chaki 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-08 11:21:19 +02: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
Christoph M. Wintersteiger
fceaf97c95 Merge branch 'unstable' of https://git01.codeplex.com/z3 into bvsls 2014-04-25 22:11:34 +01:00
Christoph M. Wintersteiger
39b562da44 compilation fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-25 22:03:26 +01:00
Christoph M. Wintersteiger
23dccdc7d5 compilation fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-25 21:54:08 +01:00
Christoph M. Wintersteiger
c9c40877a7 compilation fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-25 21:49:35 +01:00
Christoph M. Wintersteiger
4ff6a7c38d compilation fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-25 18:11:30 +01:00
Christoph M. Wintersteiger
bfdea4242c removed unused file 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-25 18:03:35 +01:00
Christoph M. Wintersteiger
a3f20774a8 BVSLS comments 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-25 17:17:47 +01:00
Andreas Froehlich
3df2967be9 Cleaned up final SLS version. Enjoy! 2014-04-25 13:56:15 +01:00
Christoph M. Wintersteiger
fb4c07a2ea FPA refactoring in preparation for FPA support in the kernel. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-23 18:36:38 +01:00
Andreas Froehlich
9ebfb119db Moved parameters to the right file. Almost clean. 2014-04-23 14:52:18 +01:00
Andreas Froehlich
c441bb4388 Backup before I touch early pruning ... 2014-04-22 16:10:44 +01:00
Andreas Froehlich
8346aed39c Fixed bug with VNS repick. 2014-04-22 01:07:30 +01:00
Andreas Froehlich
c1741d7941 Almost cleaned up version. 2014-04-22 00:32:45 +01:00
Andreas Froehlich
5ab65d52a6 Merge branch 'bvsls' of https://git01.codeplex.com/z3 into bvsls 
Conflicts:
	src/tactic/sls/sls_engine.cpp
	src/tactic/sls/sls_engine.h
	src/tactic/sls/sls_evaluator.h
	src/tactic/sls/sls_tracker.h
 2014-04-21 17:05:19 +01:00
Andreas Froehlich
ef1d8f2acc Current version before integration ... 2014-04-20 16:38:49 +01:00
Christoph M. Wintersteiger
52b54f395b FPA division bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-10 19:33:34 +01:00
Christoph M. Wintersteiger
f8ee58b301 bvsls bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-03-28 15:28:02 +00:00
Christoph M. Wintersteiger
0f5d2e010d bvsls refactoring 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-03-28 15:26:52 +00:00
Christoph M. Wintersteiger
24d662ba49 bvsls refactoring 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-03-28 14:58:59 +00:00
Christoph M. Wintersteiger
8e5659ac4c compilation fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-03-28 12:30:15 +00:00
Christoph M. Wintersteiger
176715aea0 compilation fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-03-28 12:28:40 +00:00
Christoph M. Wintersteiger
883762d54a removed dependency of bvsls on goal_refs 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-03-28 12:27:06 +00:00
Christoph M. Wintersteiger
c5e059211f bugfix 2014-03-27 13:37:04 +00:00
Christoph M. Wintersteiger
be2066a1a6 disabled old code 2014-03-27 13:34:21 +00:00
Christoph M. Wintersteiger
6f9a348f63 removed dependency of bvsls on goal_refs 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-03-26 17:26:06 +00:00
Christoph M. Wintersteiger
5f040e7480 Merge branch 'bvsls' of https://git01.codeplex.com/z3 into bvsls 2014-03-20 17:20:12 +00:00
Christoph M. Wintersteiger
041427b530 Merge branch 'unstable' of https://git01.codeplex.com/z3 into bvsls 2014-03-20 17:19:51 +00:00