Nikolaj Bjorner
|
0150a4bf3f
|
add params
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-04-16 10:08:10 -07:00 |
|
Nikolaj Bjorner
|
a37303a045
|
move parallel-tactic to solver level
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-04-16 08:21:21 -07:00 |
|
Nikolaj Bjorner
|
cd35caff52
|
clean up parallel tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-04-16 03:18:57 -07:00 |
|
Nikolaj Bjorner
|
012a96fd81
|
adding smt parallel solving
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-04-15 16:16:48 -07:00 |
|
Nikolaj Bjorner
|
252fb4af6e
|
add backtracking conquer
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-04-14 15:34:33 -07:00 |
|
Nikolaj Bjorner
|
d58a9d2528
|
fix accounting for branches
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-04-13 22:04:14 -07:00 |
|
Nikolaj Bjorner
|
c5a30285a8
|
add filter cubes parameter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-04-13 17:03:49 -07:00 |
|
Nikolaj Bjorner
|
a3e651156a
|
parallel params
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-04-13 16:23:35 -07:00 |
|
Nikolaj Bjorner
|
f7e49501af
|
updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-04-13 16:22:36 -07:00 |
|
Nikolaj Bjorner
|
d57bca8f8c
|
fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-04-10 10:43:55 +08:00 |
|
Nikolaj Bjorner
|
00685ff04f
|
Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt
|
2018-04-08 15:46:41 -07:00 |
|
Nikolaj Bjorner
|
f2dfc0dc24
|
including all touched tautology literals each round
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-04-08 15:46:21 -07:00 |
|
Nikolaj Bjorner
|
21738d9750
|
fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-04-06 15:59:55 -07:00 |
|
Nikolaj Bjorner
|
a954ab7d8d
|
flip literals in ATEs produced using RI
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-04-06 08:38:01 -07:00 |
|
Nikolaj Bjorner
|
528dc8a3f8
|
disable bdd variable elimination
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-31 17:05:22 -07:00 |
|
Nikolaj Bjorner
|
55eb11d91b
|
fix bug in blocked clause elimination: it was ignoring unit literals
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-31 13:26:20 -07:00 |
|
Nikolaj Bjorner
|
aa2721517b
|
model conversion and acce tracking
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-30 16:24:22 -07:00 |
|
Nikolaj Bjorner
|
8533238582
|
add propagation after binary addition
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-26 15:56:05 -07:00 |
|
Nikolaj Bjorner
|
51d62684e1
|
move propagation to after binary clause addition
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-26 15:51:00 -07:00 |
|
Nikolaj Bjorner
|
d60d0b8a7a
|
fix indent
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-26 15:19:14 -07:00 |
|
Nikolaj Bjorner
|
96b717f494
|
propagate during asymmetric branching
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-26 15:17:41 -07:00 |
|
Nikolaj Bjorner
|
7063ad81cc
|
updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-25 19:42:06 -07:00 |
|
Nikolaj Bjorner
|
c4ff5c7ac7
|
remove lns code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-25 18:32:16 -07:00 |
|
Nikolaj Bjorner
|
a79400a01b
|
fix bugs in scc_tr
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-25 14:55:42 -07:00 |
|
Nikolaj Bjorner
|
bfc0b214ab
|
update script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-21 14:49:36 -07:00 |
|
Nikolaj Bjorner
|
12f147403c
|
update script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-21 14:13:27 -07:00 |
|
Nikolaj Bjorner
|
5d68a09233
|
update script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-21 11:25:38 -07:00 |
|
Nikolaj Bjorner
|
1470dbf517
|
back to path
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-21 10:57:40 -07:00 |
|
Nikolaj Bjorner
|
ba30365e2d
|
updated script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-21 10:26:09 -07:00 |
|
Nikolaj Bjorner
|
9765a6d0d3
|
updated script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-21 09:23:01 -07:00 |
|
Nikolaj Bjorner
|
fe30b7edb6
|
fix mac build error
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-21 03:16:58 -07:00 |
|
Nikolaj Bjorner
|
f86a9b4b70
|
check-error
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-21 02:44:53 -07:00 |
|
Nikolaj Bjorner
|
d27527d4df
|
fix mac build error
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-20 20:49:57 -07:00 |
|
Nikolaj Bjorner
|
bd7ba4b612
|
fix mac build error
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-20 20:16:47 -07:00 |
|
Nikolaj Bjorner
|
81260c7ffb
|
fix mac build error
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-20 19:53:25 -07:00 |
|
Nikolaj Bjorner
|
4b71bfc95d
|
mac build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-20 19:19:42 -07:00 |
|
Nikolaj Bjorner
|
ff2924e83b
|
fix mac build error
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-20 17:19:40 -07:00 |
|
Nikolaj Bjorner
|
6304578111
|
mac
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-20 17:08:26 -07:00 |
|
Nikolaj Bjorner
|
16d2c2c506
|
mac
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-20 17:06:54 -07:00 |
|
Nikolaj Bjorner
|
116f0e0c70
|
cd below
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-20 17:05:12 -07:00 |
|
Nikolaj Bjorner
|
971f83997c
|
add ls
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-20 17:02:19 -07:00 |
|
Nikolaj Bjorner
|
76eae5fa5c
|
add mac build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-20 16:57:01 -07:00 |
|
Nikolaj Bjorner
|
dc01266354
|
fixing after clone
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-19 20:50:24 -07:00 |
|
Nikolaj Bjorner
|
d5bd7878b3
|
fix example test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-19 20:03:47 -07:00 |
|
Nikolaj Bjorner
|
d5811a13eb
|
add test-benchmarks
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-19 19:18:05 -07:00 |
|
Nikolaj Bjorner
|
b727a3463d
|
update vsts
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-19 18:21:34 -07:00 |
|
Nikolaj Bjorner
|
b002477d1a
|
fix java API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-19 18:10:57 -07:00 |
|
Nikolaj Bjorner
|
ac2fe879ae
|
update script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-19 15:55:00 -07:00 |
|
Nikolaj Bjorner
|
965da74d01
|
Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt
|
2018-03-19 15:49:40 -07:00 |
|
Nikolaj Bjorner
|
9598045435
|
fix java
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-19 15:49:28 -07:00 |
|