mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity
890 commits 23 branches 48 tags 157 MiB
Commit graph

890 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
026c81ba29 Simplified asserted_formulas. From now on, we should use tactics for qe, der, solve, etc. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-22 16:20:02 -08:00
Nikolaj Bjorner
dcbf1f9fbb Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-22 15:52:00 -08:00
Nikolaj Bjorner
141236e975 fix seg-fault bugs reported by Arie 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-22 15:51:47 -08:00
Leonardo de Moura
4237ac0dbf Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-22 15:22:28 -08:00
Leonardo de Moura
e0c79c06bc removed class 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-22 15:21:57 -08:00
Leonardo de Moura
ce2fbd559e removed dead file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-22 15:07:05 -08:00
Nikolaj Bjorner
d27997aa1b Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-22 13:46:26 -08:00
Nikolaj Bjorner
7d9254f122 fix multiple bugs in interfacing with fixedpoint context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-22 13:46:12 -08:00
Christoph M. Wintersteiger
985145d810 Beginnings of a Java API. This is under heavy construction. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-22 20:38:05 +00:00
Christoph M. Wintersteiger
e37a347b33 Formatting 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-22 20:37:24 +00:00
Leonardo de Moura
0111918aff mk_doc.py --> mk_api_doc.py 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-22 10:21:49 -08:00
Leonardo de Moura
badb81998d updated .gitignore 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-22 10:11:39 -08:00
Leonardo de Moura
bffa941616 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-22 10:06:45 -08:00
Leonardo de Moura
5e7436cb50 Removed (some) dead parameters. Added doxygen documentation for the whole code base. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-22 10:06:24 -08:00
Nikolaj Bjorner
fcdde59438 add missing files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-22 09:48:08 -08:00
Nikolaj Bjorner
8540b379ad add missing files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-22 09:47:11 -08:00
Leonardo de Moura
66b02eb88d Temporary fix for the build 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-22 07:44:03 -08:00
Leonardo de Moura
9e453664ce Making sure the bindings compile even when C++ compiler is used 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-21 23:05:49 -08:00
unknown
10d01a8379 Compiling java bindings on Windows 2012-11-21 22:53:31 -08:00
Leonardo de Moura
4b9e85bcd7 improving mk_make 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-21 21:20:55 -08:00
Leonardo de Moura
28dabd2441 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-21 18:32:48 -08:00
Leonardo de Moura
59b95a54e6 working on JNI bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-21 18:14:25 -08:00
Nikolaj Bjorner
ec21c7bbc5 rewrite quantifier module 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-21 16:54:41 -08:00
Leonardo de Moura
2a9014ff57 Added directory for future Java bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-21 12:51:07 -08:00
Leonardo de Moura
bfbd309419 Added checks for Java at mk_make. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-21 12:20:01 -08:00
Christoph M. Wintersteiger
a103f0e288 Made macro-finder and quasi-macros tactics public. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-21 14:39:39 +00:00
Leonardo de Moura
d9a48870db Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-20 22:38:16 -08:00
Leonardo de Moura
9c579565d4 Starting automatic generation of JNI bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 22:37:42 -08:00
Nikolaj Bjorner
ec8b7948bf Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-20 21:52:00 -08:00
Nikolaj Bjorner
21eca20b9e fix slice bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-20 21:51:41 -08:00
Nikolaj Bjorner
a935c64e15 expose assertions that are pushed to the context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-20 21:00:02 -08:00
Nikolaj Bjorner
93dfafb6d4 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-20 15:30:44 -08:00
Nikolaj Bjorner
a38a7ab506 delay rule flushing so that pretty printing retains original format of rules 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-20 15:30:22 -08:00
Leonardo de Moura
e22805c139 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-20 23:28:05 +00:00
Leonardo de Moura
ee0f0d231b Fixed missing space for OSX 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 23:27:41 +00:00
Leonardo de Moura
8f4518d28b updated RELEASE_NOTES 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 15:24:38 -08:00
Leonardo de Moura
d21cd210ed Fixed new mk_make for OSX 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 23:21:39 +00:00
Leonardo de Moura
2adbc61f1b Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-20 15:13:54 -08:00
Leonardo de Moura
bd021815b1 eliminated autoconf dependency 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 15:13:37 -08:00
Nikolaj Bjorner
2c54bbba5f more general predicate recognizer for quantified Horn clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-20 11:16:54 -08:00
Nikolaj Bjorner
6a18015622 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-20 10:43:05 -08:00
Nikolaj Bjorner
01ddb20441 recognize array and bv theories in HORN format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-20 10:42:59 -08:00
Leonardo de Moura
4d3a653309 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-20 09:38:47 -08:00
Leonardo de Moura
f9c9d5e342 updated website 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 09:38:28 -08:00
Leonardo de Moura
b3e048782c Updated RELEASE_NOTES 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 08:48:19 -08:00
Leonardo de Moura
c097b5620d fixed release notes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 08:46:48 -08:00
Leonardo de Moura
557cda70b0 Set :global-decls to false 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 08:45:31 -08:00
Leonardo de Moura
6c11a78e61 fixed .gitignore 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 08:41:45 -08:00
Leonardo de Moura
051e84de20 Updated .gitignore 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-20 08:40:05 -08:00
Leonardo de Moura
c769c683a7 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-20 08:38:07 -08:00