mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-21 16:16:38 +00:00
Code Activity
1067 commits 23 branches 48 tags 157 MiB
Commit graph

1067 commits

This branch
This branch
All branches
Author SHA1 Message Date
Ken McMillan 7cc6ff0a4c changed timeout behavior in duality 2013-06-25 12:25:41 -07:00
Ken McMillan 0f13ec6e42 adding timeout to duality 2013-06-18 12:28:20 -07:00
Ken McMillan 64acd9cac0 fixed some bugs with quantifiers in rule bodies 2013-06-17 18:04:23 -07:00
Ken McMillan a78564145b hooked up array.weak and array.extension params 2013-06-14 16:46:13 -07:00
Ken McMillan 886128c989 hooked up array.weak and array.extension params 2013-06-14 16:33:51 -07:00
Ken McMillan 30a4627a1e fixed problem with nullary background constants in duality 2013-06-10 14:46:15 -07:00
Ken McMillan c21cd6ffa5 fixed model completion problem in duality 2013-06-07 16:16:56 -07:00
Ken McMillan 40fe1f6e99 adjusting stratified inlining in duality 2013-06-07 11:50:01 -07:00
Ken McMillan 97a7ae1589 add profiling option 2013-06-05 18:01:05 -07:00
Ken McMillan c3eae9bf2a working on incremental stratified inlining in duality 2013-06-05 17:02:13 -07:00
Ken McMillan 418f148ecf working on incremental stratified inlining in duality 2013-06-04 18:22:54 -07:00
Ken McMillan 9890b3bb5c changing model format in duality to support boogie 2013-05-31 18:00:50 -07:00
Ken McMillan ca38158966 fix bug in getting decision count in duality 2013-05-31 17:52:51 -07:00
Ken McMillan dfae0c5109 output background model in duality counterexamples 2013-05-29 16:40:47 -07:00
Ken McMillan ee4b9d46f1 fix labels bug in duality 2013-05-27 19:22:47 -07:00
Ken McMillan b27abc501e set proof mode by default to avoid crash on pop if we set it later in duality 2013-05-27 19:22:19 -07:00
Ken McMillan 058c8d2083 fixing labels in duality 2013-05-22 15:42:25 -07:00
Ken McMillan 9d611997b3 fixing labels in duality 2013-05-22 15:18:50 -07:00
Ken McMillan 193e255387 Merge /home/mcmillan/pc/Code/z3_interp into interp 2013-05-22 13:31:24 -07:00
Ken McMillan 7905f48e88 status reporting issue 2013-05-22 13:23:37 -07:00
Ken McMillan 65fbef4133 fix for compiler weirdness 2013-05-10 12:16:24 -07:00
Ken McMillan 477754c386 fixed bug in label output in duality 2013-05-09 14:24:22 -07:00
Ken McMillan dc793907a5 added rule names to duality output 2013-05-09 13:31:17 -07:00
Ken McMillan b935e1e71a still adding labels to duality 2013-05-07 11:04:10 -07:00
Ken McMillan 389c2018df working on duality 2013-05-03 17:30:07 -07:00
Ken McMillan 2f8b7bfa18 adding labels to duality 2013-05-03 17:29:13 -07:00
Ken McMillan e939dd2bc5 still integrating duality 2013-04-30 13:07:49 -07:00
Ken McMillan feb5360999 integrating duality 2013-04-28 16:29:55 -07:00
Ken McMillan 8488ca24d2 first commit of duality 2013-04-20 18:18:45 -07:00
Ken McMillan 71275652a7 added simp of interpolants before print 2013-04-15 14:37:08 -07:00
Ken McMillan 6495d7b88c fixed so produce-interpolants option is not needed for compute-interpolant 2013-04-15 12:22:04 -07:00
Ken McMillan e651f45bc0 added sequences to get-interpolant and compute-interpolant 2013-04-09 15:52:30 -07:00
Ken McMillan bbe036bc03 adding build instructions 2013-03-28 11:38:11 -07:00
U-REDMOND\kenmcmil 7a0d49cb32 porting to windows 2013-03-28 11:18:20 -07:00
U-REDMOND\kenmcmil 28266786f3 porting to windows 2013-03-27 12:17:52 -07:00
Ken McMillan 78848f3ddd working on smt2 and api 2013-03-26 17:25:54 -07:00
Ken McMillan 2b93537366 debugging interpolation 2013-03-06 18:26:46 -08:00
Ken McMillan ae9276ad9b more work on interpolation 2013-03-05 21:56:09 -08:00
Kenneth McMillan d66211c007 working on interpolation API 2013-03-04 23:48:01 -08:00
Kenneth McMillan bc6b20d557 Merge branch 'interp' of https://git01.codeplex.com/z3 into interp 2013-03-04 19:53:53 -08:00
Kenneth McMillan 12d2d3beef minor fixes for OSX 2013-03-04 19:53:46 -08:00
Ken McMillan 9792f6dd33 more work on incorporating iz3 2013-03-04 18:41:30 -08:00
Kenneth McMillan e5f5e008aa fixing file heads to match z3 2013-03-03 21:22:50 -08:00
Ken McMillan 68fb01c206 initial commit for interpolation 2013-03-03 20:45:58 -08:00
Nikolaj Bjorner 197b2e8ddb fix bugs reported by Arie Gurfinkel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-03 13:55:41 -08:00
Nikolaj Bjorner 523dc0fb36 add slicing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-02 21:24:21 -08:00
Nikolaj Bjorner 352912c6b5 add default simplifications as tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-02 21:06:13 -08:00
Nikolaj Bjorner ed846a9ff3 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-03-02 21:03:15 -08:00
Nikolaj Bjorner 6c3e2e6764 add default simplifications as tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-03-02 21:03:08 -08:00
Christoph M. Wintersteiger 7822b86b53 FPA: multiple bugfixes for HWF, MPF and a bugfix for FPA2BV (many thanks to Gabriele Paganelli) 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-03-01 19:06:01 +00:00