mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-24 16:34:36 +00:00
Code Activity
4467 commits 43 branches 52 tags 176 MiB
Commit graph

4467 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
c2db127a45 fix-eq bits and projection 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-18 14:04:06 -07:00
Nikolaj Bjorner
8384a27eca handle fix_eq functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-18 11:43:18 -07:00
Christoph M. Wintersteiger
bb56885147 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-09-18 17:10:38 +01:00
Christoph M. Wintersteiger
9949c7e31c fixed typos 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-09-18 17:09:22 +01:00
Nikolaj Bjorner
53ac452253 doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-18 06:39:59 -07:00
Nuno Lopes
61d67dc2de fix a few compiler warnings 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-18 14:38:40 +01:00
Nikolaj Bjorner
9116d38628 doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-18 06:07:03 -07:00
Nikolaj Bjorner
06f0037917 doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-18 05:53:20 -07:00
Nikolaj Bjorner
9a3a1835cc doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-18 05:52:09 -07:00
Nikolaj Bjorner
2a00f2b38c adding unit tests for doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-18 05:19:52 -07:00
Nikolaj Bjorner
4eadaabe64 doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-18 03:53:14 -07:00
Nikolaj Bjorner
4c3605421c doc snapshot 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-17 16:48:41 -07:00
Nikolaj Bjorner
45bfcda16c remove typename 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-17 16:37:53 -07:00
Nikolaj Bjorner
c6e0a62cb9 udoc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-17 15:42:35 -07:00
Nikolaj Bjorner
99ff13b651 opt + udoc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-17 11:39:25 -07:00
Nuno Lopes
4717d9d1f4 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-09-17 16:33:45 +01:00
Nuno Lopes
b95f5b0fea fix bug in the datalog compiler when using negation 
We now perform negation after filtering with interpreted constraints so that
the table reflects relevant columns which were not being added by the negation

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-17 16:33:27 +01:00
Nikolaj Bjorner
a85f1784db updated answer to binary interpolant 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-16 23:25:39 -07:00
Nikolaj Bjorner
7e91fb5c15 remove mk_or_reduced 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-16 22:14:58 -07:00
Nikolaj Bjorner
e32448d7ea more fun with docs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-16 21:46:39 -07:00
Nikolaj Bjorner
1636e35bf9 fix scope accounting bug in deprecated solver mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-16 20:11:44 -07:00
Nikolaj Bjorner
e8b9c251d5 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-09-16 17:13:20 -07:00
Nikolaj Bjorner
d01ca11001 reduce asymptotic overhead of asserting bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-16 17:13:09 -07:00
Nikolaj Bjorner
44e8833369 more udoc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-16 17:06:05 -07:00
Nikolaj Bjorner
f71730b0df porting fun 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-16 15:50:12 -07:00
Nikolaj Bjorner
1058de1aa7 adding udoc_relation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-16 13:22:04 -07:00
Nuno Lopes
79326e24df fix debug build.. 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-16 15:29:25 +01:00
Nuno Lopes
f7c3559c31 fix a few compiler warnings 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-16 15:26:01 +01:00
Nuno Lopes
d3570484bb Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-09-16 14:57:22 +01:00
Nuno Lopes
919e0a5ea2 Z3Py: fix bug in substitute() with a list of on variable 
e.g. print substitute(Int('x'), [(Int('x'), Int('y'))])

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-16 14:56:59 +01:00
Nikolaj Bjorner
887e6e5392 doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-16 00:45:17 -07:00
Nikolaj Bjorner
31c7f79afd fix bv size 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-15 22:13:56 -07:00
Nikolaj Bjorner
bae4d54955 fix bv size 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-15 22:11:35 -07:00
Nikolaj Bjorner
4e4346576a move to managed tbvs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-15 22:01:13 -07:00
Nikolaj Bjorner
d9dafe7b94 tbv utilities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-15 21:23:03 -07:00
Nikolaj Bjorner
cd12fa8461 adding fixed size bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-15 20:00:45 -07:00
Nikolaj Bjorner
c09903288f have free variable utility use a class for more efficient re-use 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-15 16:14:22 -07:00
Nikolaj Bjorner
73070585b8 fix bug in core generation in legacy core: it ignores complementary literals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-14 13:06:01 -07:00
Nikolaj Bjorner
a96fa0c555 remove deprecated maxsat solvers, adjust values inline 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-14 11:55:47 -07:00
Nikolaj Bjorner
67b802c9d9 fix scope accounting bug and documentation per Konrad's request 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-12 17:38:34 -07:00
Nikolaj Bjorner
c917c1c53d reset ast trail on context deletion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-12 15:54:42 -07:00
Nikolaj Bjorner
770d0d58fe bug fixes to sorting network 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-11 21:53:12 -07:00
Nikolaj Bjorner
e288b7795d add to unit test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-11 20:33:37 -07:00
Nikolaj Bjorner
019ff77613 fix sorting network bug, add network compilation,... 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-11 18:47:21 -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
Christoph M. Wintersteiger
f8861915d2 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-09-10 23:54:34 +01:00
Nikolaj Bjorner
72f09e4729 better verbose pretty printing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-09 16:57:43 -07:00
Nikolaj Bjorner
f151879c0b enable neat vs. less neat pretty priting as an option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-09 16:25:41 -07:00
Ken McMillan
13b61d894c adding recursion bounds to duality 2014-09-09 14:02:46 -07:00