3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Commit graph

944 commits

Author SHA1 Message Date
Leonardo de Moura c011b05b61 exposing algebraic numbers in the API (working in progress)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-07 17:48:57 -08:00
Leonardo de Moura c350943c78 fixed bug introduced today
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-07 15:59:54 -08:00
Leonardo de Moura cba449b75e more parameter issues
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-07 15:16:46 -08:00
Leonardo de Moura a07b459fdf Added is_unique_value. Its semantics is equal to the old is_value method. The contract for is_value changed. See comments at ast.h for more information.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-07 12:53:51 -08:00
Leonardo de Moura bd0366eef7 Fixed problems in the new parameter setting. Many thanks to Nuno Lopes for sending a benchmark that exposed the problem, a noticing the discrepancy between unstable and master branches.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-07 11:09:14 -08:00
Leonardo de Moura e055e0b47c Fixed other parameter setting problems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-07 10:41:50 -08:00
Leonardo de Moura 0a1ba9a9e0 added openmp test, stopped using the compiler name to decide whether openmp will be used or not.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-07 09:27:19 -08:00
Leonardo de Moura ac03c9eff7 chasing parameter setting bug
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-07 08:27:17 -08:00
Leonardo de Moura 60ebc5c4dd added missing #ifndef to automatically generated hpp files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-07 06:59:54 -08:00
Leonardo de Moura 684f573c3c Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-07 06:08:25 -08:00
Leonardo de Moura 8d45de02c5 Fixed timer bug on freebsd
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-07 06:07:57 -08:00
Leonardo de Moura 1ad7458d9f missing space
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-06 18:38:18 -08:00
Leonardo de Moura 5b2dced157 merged 2012-12-06 16:09:54 -08:00
Leonardo de Moura 44ae1a2d70 fixed problem reported by Dejan
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-06 16:09:10 -08:00
Leonardo de Moura fc20eba945 another dir issue
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-06 15:46:36 -08:00
Leonardo de Moura 60b9207485 fixed more problems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-06 15:40:31 -08:00
Leonardo de Moura a430d53475 merged 2012-12-06 15:35:54 -08:00
Leonardo de Moura 26f616268e fixed warning in 32bit sys
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-06 15:35:28 -08:00
Leonardo de Moura 017176c720 fixed messy directory separator in mk_util
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-06 15:33:43 -08:00
Leonardo de Moura db6e20b2ea cleaning mk_make
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-06 14:57:07 -08:00
Leonardo de Moura fdb3e22560 fixed mk_make problem on Windows
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-06 13:57:35 -08:00
Leonardo de Moura 68b97024e2 added missing option
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-06 08:54:00 -08:00
Leonardo de Moura 75739fdf7b fixed memory smash
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-06 08:19:42 -08:00
Leonardo de Moura 294d40889f Merge branch 'nikolaj' into unstable 2012-12-06 07:42:50 -08:00
Nikolaj Bjorner dbde71c290 fixing unit tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-12-06 07:38:53 -08:00
Nikolaj Bjorner 6bdde9047a fixing unit tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-12-06 07:38:50 -08:00
Leonardo de Moura 3cefa0a1f7 making tests deterministic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-05 19:20:48 -08:00
Josh Berdine 2f3daf14b5 Regenerate ml api 2012-12-05 19:20:48 -08:00
Josh Berdine 6fad07e6e1 Update build system for ml api 2012-12-05 19:20:47 -08:00
Josh Berdine 949317ccfc Fixes for error handling in ml api 2012-12-05 19:20:47 -08:00
Josh Berdine ae5f96895d Change to avoid relying on sed supporting disjunction or escaped control characters 2012-12-05 19:20:47 -08:00
Josh Berdine 4ec4151e82 Change treatment of unsigned to avoid depending on unspecified behavior of recursive macros 2012-12-05 19:20:47 -08:00
Josh Berdine 6a5de3384c Regenerate ml api 2012-12-06 00:42:30 +00:00
Josh Berdine 79be6ee6c2 Update build system for ml api 2012-12-06 00:39:45 +00:00
Josh Berdine c9865606e6 Fixes for error handling in ml api 2012-12-06 00:34:34 +00:00
Josh Berdine 192f51e986 Change to avoid relying on sed supporting disjunction or escaped control characters 2012-12-06 00:34:34 +00:00
Josh Berdine 8cc695eb7f Change treatment of unsigned to avoid depending on unspecified behavior of recursive macros 2012-12-06 00:34:33 +00:00
Leonardo de Moura 3a5e71afef Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-05 16:22:16 -08:00
Leonardo de Moura 1a11196211 fixing bug introduced today
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-05 16:21:53 -08:00
Leonardo de Moura 2b66b50c75 making tests deterministic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-05 16:21:38 -08:00
Leonardo de Moura 5e4d1151eb fixing clang compilation problems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-05 15:20:16 -08:00
Nikolaj Bjorner 188aea3fb1 fix test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-12-05 13:48:27 -08:00
Nikolaj Bjorner 53cb389398 fixing unit tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-12-05 13:05:14 -08:00
Nikolaj Bjorner 3b51597dbe fixing unit tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-12-05 12:05:07 -08:00
Nikolaj Bjorner 3bf86e1a49 fixing unit tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-12-05 12:02:08 -08:00
Nikolaj Bjorner aeb3857391 fixing unit tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-12-05 12:01:03 -08:00
Leonardo de Moura 3736c5ea3b removed template specialization overkill
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-05 08:56:19 -08:00
Leonardo de Moura 5379130c8c eliminated m_proof_mode from smt_params, ast_manager has this information
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-05 08:35:03 -08:00
Leonardo de Moura f6a3ec58e5 allow --help, --version, etc as valid parameter names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-04 15:48:28 -08:00
Leonardo de Moura 89385b4e9a no need for / options 2012-12-04 15:38:16 -08:00