3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-13 06:30:54 +00:00

Commit graph

  • a33913979d moved bit_blaster_tactic to bv_tactics Leonardo de Moura 2012-10-21 22:37:34 -07:00
  • 59fc7acc48 checkpoint Leonardo de Moura 2012-10-21 22:21:33 -07:00
  • 9359ab7ce5 checkpoint Leonardo de Moura 2012-10-21 22:16:58 -07:00
  • 142bf71b35 checkpoint Leonardo de Moura 2012-10-21 22:04:19 -07:00
  • 63154b99c5 checkpoint Leonardo de Moura 2012-10-21 21:52:11 -07:00
  • 78b11ccd8e checkpoint Leonardo de Moura 2012-10-21 21:50:58 -07:00
  • 80b2df3621 checkpoint Leonardo de Moura 2012-10-21 20:46:41 -07:00
  • 6fd63cd05a checkpoint Leonardo de Moura 2012-10-21 20:04:34 -07:00
  • d71595fc1c regenerated ml api Josh Berdine 2012-10-22 03:37:57 +01:00
  • 8231d1cbcf updated Debug dir name Josh Berdine 2012-10-22 03:35:52 +01:00
  • cd8618f90d updated ml api test regressions (due to new printing?) Josh Berdine 2012-10-22 03:34:56 +01:00
  • 53e22f308b made .cmd scripts executable Josh Berdine 2012-10-22 03:20:00 +01:00
  • f6c89ba1d3 checkpoint Leonardo de Moura 2012-10-21 18:32:35 -07:00
  • 39d6628be9 checkpoint Leonardo de Moura 2012-10-21 18:23:20 -07:00
  • 56ab7a7495 checkpoint Leonardo de Moura 2012-10-21 18:12:34 -07:00
  • ffaf88798d preparing to split framework Leonardo de Moura 2012-10-21 17:31:45 -07:00
  • 83e92c2dd7 added build and test scripts and READMEs to distribute Josh Berdine 2012-10-07 02:26:27 +01:00
  • 6e1eb7044b removed files specific to source depot and SDV Josh Berdine 2012-10-07 02:21:57 +01:00
  • 27b8eefa67 updated ml api test expected output following recent formatting changes Josh Berdine 2012-10-07 00:33:22 +01:00
  • 4c8044176d clean .z3-trace Josh Berdine 2012-10-07 00:31:55 +01:00
  • aec36146ab updated ml build scripts to assume required tools are already set up, and added comments specifying which tools are required Josh Berdine 2012-10-07 00:27:00 +01:00
  • c4711ac472 checkpoint Leonardo de Moura 2012-10-21 16:03:12 -07:00
  • 00e94e1653 Moved scripts to scripts dir Leonardo de Moura 2012-10-21 15:35:30 -07:00
  • 6d25a3bd2b Added Visual Solution Generation Leonardo de Moura 2012-10-21 15:33:49 -07:00
  • ae400c4b2a checkpoint Leonardo de Moura 2012-10-21 14:39:59 -07:00
  • cf47f6ce60 renamed user_ext => user_plugin Leonardo de Moura 2012-10-21 14:19:00 -07:00
  • dcf778a287 Reorganizing the code Leonardo de Moura 2012-10-21 14:16:35 -07:00
  • 3003ee5cb6 Integrating Nikolaj's Saturday changes (at unstable branch) Leonardo de Moura 2012-10-21 13:40:22 -07:00
  • add684d8e9 checkpoint Leonardo de Moura 2012-10-21 13:32:12 -07:00
  • 4722fdfca5 Reorganizing the code Leonardo de Moura 2012-10-21 08:12:38 -07:00
  • 6bc591c67e Reorganizing the code Leonardo de Moura 2012-10-20 22:44:27 -07:00
  • aa949693d4 Reorganizing the code Leonardo de Moura 2012-10-20 22:28:22 -07:00
  • 492484c5aa Reorganizing the code Leonardo de Moura 2012-10-20 22:03:58 -07:00
  • 2b8fb6c718 Reorganizing the code Leonardo de Moura 2012-10-20 20:53:33 -07:00
  • 6bdb009c3e Reorganizing the code Leonardo de Moura 2012-10-20 20:42:28 -07:00
  • d8cd3fc3ab Reorganizing the code Leonardo de Moura 2012-10-20 19:54:08 -07:00
  • 8b70f0b833 Reorganizing the code Leonardo de Moura 2012-10-20 19:30:14 -07:00
  • 452ea65189 move to z3.dll instead of z3_dbg.dll Nikolaj Bjorner 2012-10-20 19:26:31 -07:00
  • 61de6433c0 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Nikolaj Bjorner 2012-10-20 19:11:50 -07:00
  • 1cae83183a add missing /** so that OCaml can build Nikolaj Bjorner 2012-10-20 19:10:25 -07:00
  • ded42feeb6 Reorganizing code base Leonardo de Moura 2012-10-20 16:33:01 -07:00
  • 9a84cba6c9 Reorganizing the code. Moved nlsat to its own directory. Leonardo de Moura 2012-10-20 15:48:18 -07:00
  • c66b9ab615 Reorganizing the code Leonardo de Moura 2012-10-20 15:30:42 -07:00
  • 8a6997960a Reorganizing code. Added script for generating VS project files Leonardo de Moura 2012-10-20 15:16:37 -07:00
  • 090ca2e46c refined difference logic check, consolidate scoped modes Nikolaj Bjorner 2012-10-20 10:47:30 -07:00
  • 2c464d413d Reorganizing source code. Created util dir Leonardo de Moura 2012-10-20 10:19:38 -07:00
  • 14aff67684 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Nikolaj Bjorner 2012-10-20 06:36:30 -07:00
  • 630ba0c675 use a more liberal static feature for difference logic Nikolaj Bjorner 2012-10-20 06:33:14 -07:00
  • c2f9f2e9cd Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Nikolaj Bjorner 2012-10-20 04:27:42 -07:00
  • 4e94fa7d37 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Nikolaj Bjorner 2012-10-20 04:26:46 -07:00
  • 2e73957f97 enable proof production with difference logic, integrate with PDR engine Nikolaj Bjorner 2012-10-20 04:25:58 -07:00
  • 472b8caa41 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Leonardo de Moura 2012-10-19 18:39:01 -07:00
  • b505fe13cd updated release notes Leonardo de Moura 2012-10-19 18:38:34 -07:00
  • 36f7bad1da Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable Nikolaj Bjorner 2012-10-19 08:33:57 -07:00
  • ccb50f5d8a updated comments to create_children Nikolaj Bjorner 2012-10-19 08:33:43 -07:00
  • 28a4f51ea5 qe-lite Nikolaj Bjorner 2012-10-19 08:30:23 -07:00
  • cadfb804c5 remove dead code Nikolaj Bjorner 2012-10-19 08:22:31 -07:00
  • b22fb74c5c working on symbolic execution for PDR Nikolaj Bjorner 2012-10-18 21:09:32 -07:00
  • 8f5fc3716e working on symbolic execution for PDR Nikolaj Bjorner 2012-10-18 21:01:28 -07:00
  • 8cde0c0672 fixed update_api.py Leonardo de Moura 2012-10-18 12:55:28 -07:00
  • 5fa96ccb0b Renamed z3_dbg.dll to z3.dll Leonardo de Moura 2012-10-18 12:52:33 -07:00
  • fae9a1b760 Fixed bug in DLL .def generation Leonardo de Moura 2012-10-18 04:51:41 -07:00
  • 2a4e6d03f3 Extending public API with internal objects Leonardo de Moura 2012-10-18 04:47:46 -07:00
  • 9cb29777e2 fixed update_api.py Leonardo de Moura 2012-10-17 23:13:43 -07:00
  • 15fb18c65d Simplified binding and logging support generation. Now, everything is generated by update_api.py script. The binding commands can be included in the .h files (e.g., z3_api.h Leonardo de Moura 2012-10-17 23:00:21 -07:00
  • 8459401b6e working on expansion Nikolaj Bjorner 2012-10-17 08:34:42 -07:00
  • 3a837037d4 working on symbolic execution trace unfolding Nikolaj Bjorner 2012-10-16 16:54:03 -07:00
  • 6b414ba5cf Add coalesce transformer Nikolaj Bjorner 2012-10-16 08:21:32 -07:00
  • d16db63e56 add rule unfolding transformation Nikolaj Bjorner 2012-10-15 15:34:29 -07:00
  • 2c24f25050 finish (inefficient) BMC for non-linear Horn Nikolaj Bjorner 2012-10-15 10:49:19 -07:00
  • b6e7d4ecc6 finish (inefficient) BMC for non-linear Horn Nikolaj Bjorner 2012-10-15 10:48:42 -07:00
  • f7f2a77504 Merge branch 'working' of //z3-1/z3 into working Leonardo de Moura 2012-10-15 10:08:02 -07:00
  • 4efe38a71d Added support for parsing negative numerals in the SMT 2.0 frontend Leonardo de Moura 2012-10-15 10:02:52 -07:00
  • bdad4e3bcb optimize model pruning Nikolaj Bjorner 2012-10-14 11:19:02 -07:00
  • f27c9b9d3d optimize model pruning Nikolaj Bjorner 2012-10-14 11:17:05 -07:00
  • bf0481c4d0 working on pdr Nikolaj Bjorner 2012-10-14 11:13:36 -07:00
  • 990b93c2fd working on pdr Nikolaj Bjorner 2012-10-14 00:24:17 -07:00
  • 16cfb3895d optimize model pruning Nikolaj Bjorner 2012-10-13 20:09:12 -07:00
  • 95fbf073f8 Merge branch 'working' of https://z3-1/gw/git/z3 into working Nikolaj Bjorner 2012-10-13 20:09:04 -07:00
  • 6a7d180e69 goodies for gdb Leonardo de Moura 2012-10-13 18:13:39 -07:00
  • 72809843d5 Merge branch 'working' of https://z3-1/gw/git/z3 into working Nikolaj Bjorner 2012-10-13 17:55:12 -07:00
  • 148416122f optimize model pruning Nikolaj Bjorner 2012-10-13 17:52:37 -07:00
  • 0a8be25149 optimize model pruning Nikolaj Bjorner 2012-10-13 16:15:42 -07:00
  • a159943669 cygwin support Leonardo de Moura 2012-10-13 14:07:39 -07:00
  • 3cf96f7475 Merge branch 'working' of ssh://localhost:22/home/leo/projects-bare/z3 into working Leonardo de Moura 2012-10-13 14:03:44 -07:00
  • 42572ec93a added missing script Leonardo de Moura 2012-10-13 14:03:03 -07:00
  • 9828a29b68 better proof mining for Farkas Nikolaj Bjorner 2012-10-13 10:13:14 -07:00
  • 8121386d5e Merge branch 'working' of https://z3-1/gw/git/z3 into working Nikolaj Bjorner 2012-10-13 10:13:02 -07:00
  • bccf07be0b fixed bug in unsat core generation Leonardo de Moura 2012-10-13 09:11:54 -07:00
  • 6145ccc077 Added tactic for qfnra purely based on nlsat Leonardo de Moura 2012-10-12 17:34:23 -07:00
  • af469f82ec better proof mining for Farkas Nikolaj Bjorner 2012-10-12 17:20:55 -07:00
  • 9ad4b5bc0f Merge branch 'working' of https://z3-1/gw/git/z3 into working Nikolaj Bjorner 2012-10-12 17:15:53 -07:00
  • 2087c59084 better proof mining for Farkas Nikolaj Bjorner 2012-10-12 17:12:43 -07:00
  • 5c0d82d555 Updated Release notes Leonardo de Moura 2012-10-12 16:42:28 -07:00
  • af13e22f99 Merge branch 'working' of //z3-1/z3 into working Leonardo de Moura 2012-10-12 16:38:06 -07:00
  • 75457e1393 int<->real coercions. Leonardo de Moura 2012-10-12 16:34:54 -07:00
  • c2623e15c3 Switched ParamDescrs.ToString to native implementation Christoph M. Wintersteiger 2012-10-12 21:05:32 +01:00
  • c48bd1e8de updated release notes Leonardo de Moura 2012-10-12 12:16:20 -07:00
  • 44db8c083d exposed solver object param descrs Leonardo de Moura 2012-10-12 09:42:45 -07:00
  • f7bcd40137 Added API Z3_param_descrs_to_string Leonardo de Moura 2012-10-12 09:13:04 -07:00