mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity
2058 commits 23 branches 48 tags 157 MiB
Commit graph

2058 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
8fe2db1eed Merge branch 'bvsls' of https://git01.codeplex.com/z3 into opt 2014-04-25 18:11:48 +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
216b4d1aaa Merge branch 'bvsls' of https://git01.codeplex.com/z3 into opt 2014-04-25 18:06:03 +01:00
Christoph M. Wintersteiger
ac206bacbf Merge branch 'bvsls' of https://git01.codeplex.com/z3 into opt 
Conflicts:
	src/tactic/sls/sls_compilation_settings.h

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-25 18:05:53 +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
Nikolaj Bjorner
20cb8a3092 added pareto utility 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-25 03:00:31 +02:00
Andreas Froehlich
9ebfb119db Moved parameters to the right file. Almost clean. 2014-04-23 14:52:18 +01:00
Nikolaj Bjorner
55863b4bb5 fix build problems, fix scoping 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-23 14:05:59 +02:00
Nikolaj Bjorner
27fa7077a6 fix compiler warnings/errors reported by Robert White 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-23 09:22:31 +02:00
Nikolaj Bjorner
a5ec46b167 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2014-04-23 08:23:04 +02:00
Nikolaj Bjorner
23a74b3c26 fix assertions reported by Christoph 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-23 08:07:37 +02:00
Christoph M. Wintersteiger
859013e9c9 bvsls opt engine bugfix/debugging 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-22 19:13:43 +01:00
Andreas Froehlich
c441bb4388 Backup before I touch early pruning ... 2014-04-22 16:10:44 +01:00
Nikolaj Bjorner
d67b5226f0 fix compiler errors reported by Robert White 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-22 16:59:40 +02:00
Nikolaj Bjorner
3003049df8 fix bug in bcd2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-22 15:41:11 +02:00
Nikolaj Bjorner
d118f07e37 fix maximize name in C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-22 14:48:05 +02: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
Nikolaj Bjorner
beaa50e0d8 fixing sls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-21 18:07:02 +02: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
Nikolaj Bjorner
1f66e46c67 move sls functionality to solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-19 20:50:44 -07:00
Nikolaj Bjorner
3f5ed8ff11 coallesce common code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-19 20:27:39 -07:00
Nikolaj Bjorner
b300041075 resetting SLS engine between calls, moved statistics collection to engine 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-19 16:52:57 -07:00
Nikolaj Bjorner
ff154a09b3 sls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-19 12:12:51 -07:00
Nikolaj Bjorner
032e2618f6 refactor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-19 11:58:57 -07:00
Nikolaj Bjorner
5ead06bcef adding SLS solver layer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-18 10:29:52 -07:00
Nikolaj Bjorner
e3b346df6f working on bcd2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-18 08:04:18 -07:00
Nikolaj Bjorner
ae1656a92c working on bcd2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-17 15:37:03 -07:00
Nikolaj Bjorner
7237be768b fixing bugs in refactored code exposed from White's example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-17 11:06:43 -07:00
Nikolaj Bjorner
c84ab2fc01 tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-14 22:12:22 -07:00
Nikolaj Bjorner
e32666927b tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-14 21:59:39 -07:00
Nikolaj Bjorner
91dc527635 tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-14 21:18:18 -07:00
Nikolaj Bjorner
ac31e3856e refactor weighted maxsmt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-14 16:25:52 -07:00
Nikolaj Bjorner
00f45579cc refactor weighted maxsmt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-14 16:24:23 -07:00
Christoph M. Wintersteiger
64106af5ec bvsls_opt_engine fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-14 17:48:09 +01:00
Christoph M. Wintersteiger
71af72eed4 bugfix for bvsls_opt_engine 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-14 15:24:47 +01:00
Nikolaj Bjorner
1db7e0a149 fix compiler warnings reported by Robert White 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-04-02 15:54:28 +02:00
Nikolaj Bjorner
7fd6549a40 another sls example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-31 23:32:31 +02:00
Nikolaj Bjorner
deb325b8c2 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2014-03-31 23:31:06 +02:00
Nikolaj Bjorner
f321f19b20 adding bcd2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-31 23:30:59 +02:00
Christoph M. Wintersteiger
7d896e5a9a bvsls_opt_engine bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-03-31 17:58:19 +01:00
Christoph M. Wintersteiger
3bc31b6603 bvsls integration with opt::wmaxsmt 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-03-31 17:41:34 +01:00
Nikolaj Bjorner
d67f1f36c4 refactor weighted theory solver into own file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-29 16:54:12 -07:00
Nikolaj Bjorner
8d23b2b813 speed up parsing of large Datalog files, remove pinned 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-28 18:26:42 -07:00
Nikolaj Bjorner
efe2a70f6f integrating SLS 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-28 14:30:36 -07:00
Nikolaj Bjorner
3d7f208ce6 add bvsls module as backend to weighted maxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-28 13:32:31 -07:00
Christoph M. Wintersteiger
a26e299390 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2014-03-28 17:46:32 +00:00