mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity
969 commits 23 branches 48 tags 157 MiB
Commit graph

969 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 0906fd9d9c Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-01-24 19:20:17 -08:00
Nikolaj Bjorner a6cf5281eb working on tab context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-24 19:20:08 -08:00
Leonardo de Moura 6dd4cb832b Fix problem reported by Alex Horn 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-24 16:42:34 -08:00
Leonardo de Moura 711abc75fb Fix issue reported at http://z3.codeplex.com/workitem/14 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-24 13:22:28 -08:00
Leonardo de Moura 7e7927052e Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-01-24 12:51:11 -08:00
Leonardo de Moura 7eaa5562d8 Fix http://z3.codeplex.com/workitem/19 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-24 12:51:03 -08:00
Nikolaj Bjorner 521382e37f working on tab-context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-24 12:50:19 -08:00
Nikolaj Bjorner d3025569c2 working on tab-context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-24 12:45:58 -08:00
Leonardo de Moura afaef63bfa Fix compilation error when using gcc. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-24 12:38:37 -08:00
Nikolaj Bjorner c89531bcf8 working on tab-context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-23 21:44:42 -08:00
Nikolaj Bjorner 0e02fcad60 merge 2013-01-23 19:37:59 -08:00
Nikolaj Bjorner 2d1afa7ba4 stash 2013-01-23 19:36:41 -08:00
Nikolaj Bjorner b61c1b0ded working on tab-context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-23 19:05:38 -08:00
Nikolaj Bjorner 085ccf5eff working on tab context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-21 22:28:25 -08:00
Nikolaj Bjorner af4c09c8d3 update substitution routines 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-21 21:59:20 -08:00
Nikolaj Bjorner b9cc7080e7 update substitution routines 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-21 21:47:43 -08:00
Leonardo de Moura 7cad0b4a1f Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-01-21 08:27:56 -08:00
Leonardo de Moura a3eb6d121f Merge branch 'cade24' into unstable 2013-01-21 08:27:32 -08:00
Nikolaj Bjorner 87e9015675 working on tab_context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-20 18:41:41 -08:00
Leonardo de Moura 5d938a5fe2 Fix bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-20 18:41:24 -08:00
Leonardo de Moura 3344151aca Replace # with x in the definition of algebraic elements 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-20 18:21:09 -08:00
Nikolaj Bjorner 99f5a5bddb working on tab_context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-18 17:36:42 -08:00
Nikolaj Bjorner cab908bfef working on horn tab solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-18 09:56:35 -08:00
Nikolaj Bjorner 8daf100c65 working on tab Horn solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-17 18:03:34 -08:00
Christoph M. Wintersteiger 79dafcea81 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-01-17 19:31:24 +00:00
Christoph M. Wintersteiger 4b18c8f9c4 Java API: syntactic adjustments, getters, setters, 
... convenience parameters, etc.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-01-17 19:31:02 +00:00
Christoph M. Wintersteiger 3abf397560 Added Solver.AssertAndTrack 
Convenience fixes.
Renamed Context.Const to Context.ConstProbe

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-01-17 19:30:00 +00:00
Nikolaj Bjorner c0f22039e4 add back cooperate.h include (not used now, but will be) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-17 08:23:09 -08:00
Nikolaj Bjorner b19a47176b working on tab 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-17 08:17:21 -08:00
Nikolaj Bjorner 50bf845b40 add tabulation/subsumption engine 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-16 17:16:44 -08:00
Leonardo de Moura bb386c0f18 Fix problem in inv_rf 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-16 11:19:11 -08:00
Leonardo de Moura c9b7ea35b6 Fix typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-16 08:39:24 -08:00
Leonardo de Moura be266bdd56 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-01-15 17:44:18 -08:00
Leonardo de Moura 53094c6173 Add gprof support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-15 17:43:22 -08:00
Leonardo de Moura eea3384106 Add lazy normalization for algebraic extension values. Increase default max_precision to 128. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-15 16:35:36 -08:00
Leonardo de Moura 217c8375ce Add new rational function normalization procedure. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-15 14:34:34 -08:00
Nikolaj Bjorner ca5eb5186d fix pretty printer for smt2 unary minus 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-01-15 09:24:12 -08:00
Christoph M. Wintersteiger 5f0cb28ca3 .NET and Java APIs: added functions for global parameter management. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-01-15 17:05:31 +00:00
Leonardo de Moura f0737bdf7f Replace expensive_eval_sign_at with version that does not generate rational numbers 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 18:30:36 -08:00
Leonardo de Moura 799fe073db Add API for extracting numerator/denominator of RCF numerals. Add field to store the original isolating interval before refinement. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 18:29:08 -08:00
Leonardo de Moura 991a1528cd Cache isolating interval for better pretty printing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 12:17:15 -08:00
Leonardo de Moura 025cb2a2a8 Avoid wasteful memory allocation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 12:03:22 -08:00
Leonardo de Moura 38e0b4a20a Fix bug. Add is_denominator_one macro. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 11:55:52 -08:00
Leonardo de Moura 742f2b07dd Add support for compact string representation in the RCF API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 11:08:32 -08:00
Leonardo de Moura 6c35e08e43 Make sure we do not use denominators != 1 when encoding values of algebraic extensions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 10:43:18 -08:00
Leonardo de Moura 39d5b850e8 Fix bug reported at http://stackoverflow.com/questions/14307692/unknown-when-using-defs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-13 12:59:39 -08:00
Leonardo de Moura 349c21d4de Add configure script that is just a wrapper for python 'src/mk_make.py'. It makes the build more user friendly for users familiar with ./configure + make idiom 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-13 11:34:05 -08:00
Leonardo de Moura 7312f49f88 Fix Visual Studio warnings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-13 09:06:07 -08:00
Leonardo de Moura 93f37bdf9f Merge branch 'realclosure' into unstable 2013-01-12 22:03:40 -08:00
Leonardo de Moura f747bde548 Add restore_interval for extensions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 21:59:41 -08:00