3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Commit graph

756 commits

Author SHA1 Message Date
Leonardo de Moura fa53b1eb92 added module descriptions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-02 13:15:56 -08:00
Leonardo de Moura 1871bef6e1 cleaned algebraic params
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-02 12:47:20 -08:00
Leonardo de Moura b7f636984e merged
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-02 12:24:45 -08:00
Leonardo de Moura 624115ea6d exposed pattern inference params
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-02 12:24:27 -08:00
Leonardo de Moura 32854c677c exposed old simplifier parameters
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-02 12:10:06 -08:00
Leonardo de Moura c82b8174d8 fixed win compilation bug
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-02 12:08:58 -08:00
Leonardo de Moura 8d62c95a54 fixed mk_make
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-02 11:31:38 -08:00
Leonardo de Moura 6a220c8b58 moved old params files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-02 11:27:39 -08:00
Leonardo de Moura 6107e8d9ce moved old params files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-02 10:47:04 -08:00
Leonardo de Moura ffb7e26c75 removed front-end-params
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-02 10:05:29 -08:00
Leonardo de Moura 288a96610f ported VCC trace streams
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-02 09:08:47 -08:00
Leonardo de Moura 80405dbd62 added context_params to API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-02 08:12:15 -08:00
Leonardo de Moura 1c15e078a4 cleanup
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-01 23:00:06 -08:00
Leonardo de Moura f15de18c4a context params
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-01 22:53:55 -08:00
Leonardo de Moura 02e763bb6b env params
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-01 20:56:40 -08:00
Leonardo de Moura 9bd4fd969a cleanning
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-01 18:50:26 -08:00
Leonardo de Moura 29ec68284b Added better error message when old parameter name is used
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-01 18:34:53 -08:00
Leonardo de Moura 92acd6d4ee removed front_end_params from cmd_context
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-01 18:19:02 -08:00
Leonardo de Moura 29cf179364 more reorg
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-01 17:03:14 -08:00
Leonardo de Moura 32791204e7 merged
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-01 16:36:24 -08:00
Leonardo de Moura 9374a4e20a removed ini_file
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-01 16:30:39 -08:00
Leonardo de Moura 823dd6ca47 missing file
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-01 15:54:53 -08:00
Leonardo de Moura 589f096e6e working on new parameter framework
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-01 15:54:34 -08:00
Christoph M. Wintersteiger f78e595b56 Added QF_FPABV logic, default tactic, and the asIEEEBV conversion function.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2012-12-01 15:51:33 +00:00
Leonardo de Moura be5f933201 removed dead module
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-30 18:20:07 -08:00
Leonardo de Moura 6195ed7c66 checkpoint
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-30 18:16:02 -08:00
Leonardo de Moura 3e6bddbad1 converted pp_params
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-30 17:20:45 -08:00
Nikolaj Bjorner 2d1a6bf270 fix regression for simplifying tails with quantifiers, add some more handling for quantified tails
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-11-30 15:58:06 -08:00
Leonardo de Moura 4f9442864a auto generation of parameter helper
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-30 15:31:40 -08:00
Christoph M. Wintersteiger 692593baaa Java API: 32-bit issues and bugfixes.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2012-11-30 22:31:07 +00:00
Leonardo de Moura 124c0339c1 merged
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-30 13:17:41 -08:00
Leonardo de Moura 9246a7a673 checkpoint
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-30 13:14:42 -08:00
Christoph M. Wintersteiger 9b2236361c Java API: bugfix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2012-11-30 19:50:57 +00:00
Christoph M. Wintersteiger d13d6fecbf Java API: added correct error handling.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2012-11-30 19:43:34 +00:00
Leonardo de Moura caf14b96d4 moving to gparams...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-30 11:30:20 -08:00
Christoph M. Wintersteiger e87e0991f3 Java API: multi-platform fixes 2012-11-30 19:17:05 +00:00
Christoph M. Wintersteiger 3544379f53 Java API: removed platform-dependency of Native.cpp
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2012-11-30 19:10:59 +00:00
Christoph M. Wintersteiger 0c1f2a8281 Java API: Added exception wrappers and build dependencies.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2012-11-30 15:39:25 +00:00
Nikolaj Bjorner 654c02701c pretty print rules with quoted symbols
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-11-29 19:17:01 -08:00
Leonardo de Moura 722cce0cff checkpoint
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-29 17:52:07 -08:00
Leonardo de Moura cf28cbab0a saved params work
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-29 17:19:12 -08:00
Nikolaj Bjorner 646ace6842 fix bugs uncovered from running non-Horn SDV samples
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-11-29 14:56:09 -08:00
Nikolaj Bjorner cefa2d7650 add option to print with variable declarations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-11-29 13:11:34 -08:00
Leonardo de Moura c3055207ed updated release notes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-29 10:30:16 -08:00
Leonardo de Moura c6bd31e01d working on new global parameter setting framework
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-29 10:05:13 -08:00
Leonardo de Moura 0733db382f updated release notes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-29 09:15:03 -08:00
Leonardo de Moura 001c8487e9 small change to be able to test java example on linux
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-29 09:13:24 -08:00
Leonardo de Moura 30905da58c fixed: make examples
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-29 08:14:06 -08:00
Leonardo de Moura 0c445cec57 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-11-28 16:47:36 -08:00
Leonardo de Moura 3ca41c6202 fixed recently introduced bug
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-28 16:46:19 -08:00