mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-16 17:36:39 +00:00
Code Activity
485 commits 43 branches 51 tags 169 MiB
Commit graph

72 commits

Author SHA1 Message Date
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
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
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
Nikolaj Bjorner
ec21c7bbc5 rewrite quantifier module 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-21 16:54:41 -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
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
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
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
Nikolaj Bjorner
62c713129a rename pdr_tactic to horn_tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-19 09:24:19 -08:00
Nikolaj Bjorner
b30fc79bf1 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-19 05:21:15 -08:00
Nikolaj Bjorner
5bf20f9125 fix bug in qe-lite when substituting inside quantifiers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-19 05:20:45 -08:00
Nikolaj Bjorner
57c4ce4082 bit-blast equalities before checking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-19 04:39:18 -08:00
Nikolaj Bjorner
f98e107d0e insert fresh name 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-18 20:11:48 -08:00
Nikolaj Bjorner
f014ab9598 use different symbols for named rules 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-18 19:00:01 -08:00
Nikolaj Bjorner
3ce0e900ff register also head predicate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-18 18:31:35 -08:00
Nikolaj Bjorner
f9f303e934 add pdr tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-17 18:18:58 -08:00
Nikolaj Bjorner
39e6453f4a Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-17 18:03:46 -08:00
Nikolaj Bjorner
8592f5cef4 make verbose model only use simplified rules 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-17 15:27:51 -08:00
Nikolaj Bjorner
29a45e34a2 fixing bugs in model evaluator. remove wrong assertions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-17 22:09:15 +01:00
Nikolaj Bjorner
50385e7e29 add option to validate result of PDR. Add PDR tactic. Add fixedpoint parsing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-17 20:47:49 +01:00
Leonardo de Moura
93bfcaa404 Making ast_smt2_pp the default pretty printer. Now, mk_pp is just an alias for mk_ismt2_pp 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-17 10:20:08 -08:00
Leonardo de Moura
3e8d3db290 fixed gcc compilation error 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-13 09:26:01 -08:00
Nikolaj Bjorner
68ae5d434c fix cover retrieval for slicing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-13 17:00:01 +01:00
Nikolaj Bjorner
108bbb0597 add missing check for difference logic fragment for clause heads 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-10 11:50:17 +01:00
Nikolaj Bjorner
cec851440e fix model completion bug in PDR, addhoc handling of reals for arithmetic realizers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-06 15:38:07 +02:00
Nikolaj Bjorner
5ef505c357 set model completion to force value computation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-04 14:22:56 +02:00
Nikolaj Bjorner
37a13b1d09 update slicing to fix unbound variables. test datatype realizer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-04 14:15:24 +02:00
Nikolaj Bjorner
bfbdad3ce6 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-04 08:40:23 +02:00
Nikolaj Bjorner
927dc2e490 fix if-lifting, added light-weight FM to qe_lite 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-04 08:40:16 +02:00
Leonardo de Moura
c1587dc37d fixed some warnings reported by clang++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-02 17:28:27 -07:00
Leonardo de Moura
cadd35bf7a checkpoint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-01 21:44:35 -07:00
Nikolaj Bjorner
4f2b7049ab Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-01 13:06:16 -07:00
Nikolaj Bjorner
1c17e40fe5 optmizing DL 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-11-01 13:06:10 -07:00
Leonardo de Moura
4c98b567e1 old_params ==> front_end_params. Isolated abstract solver interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-01 11:28:14 -07:00
Nikolaj Bjorner
8f7494cb04 disable buggy code in slicer: it removes conjuncts for non-sliced variables. It should use the same criteria as the slice recognizer. reported by Arie Gurfinkel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-31 20:29:28 -07:00
Nikolaj Bjorner
9748b6ed11 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-10-31 13:25:42 -07:00
Nikolaj Bjorner
c4cb66bbfa fix bugs in inliner and usage of unbound variable fix, reported by Arie Gurfinkel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-31 13:23:24 -07:00
Leonardo de Moura
92eb2ec802 missing update 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-31 11:02:14 -07:00
Leonardo de Moura
683687b153 more cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-31 10:54:59 -07:00
Nikolaj Bjorner
bdc28762d3 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-10-31 10:37:10 -07:00
Nikolaj Bjorner
832ade3ac8 local changes 2012-10-31 10:37:05 -07:00
Leonardo de Moura
ffcb9741dc Fixed warnings reported by gcc 4.7.1 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-31 00:05:38 -07:00
Leonardo de Moura
d8f627c6c8 Fixed warnings produced by gcc 4.6.3 when compiling in debug mode 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-10-30 23:43:00 -07:00
Nikolaj Bjorner
f44631ce73 fix bugs encountered by regression tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-30 16:13:27 -07:00
Nikolaj Bjorner
7553c3c86e fix bugs in model generation reported by Ken 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-29 14:53:42 -07:00
Nikolaj Bjorner
3bf6af44bf expose additional external options for muz 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2012-10-29 09:00:38 -07:00