mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 22:59:02 +00:00
Code Activity
4945 commits 23 branches 48 tags 157 MiB
Commit graph

4033 commits

Author SHA1 Message Date
Nikolaj Bjorner 660eff0b9e Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-12 18:59:05 +00:00
Nikolaj Bjorner 45999b254c hoist simplifier functionality out of context loop to allow plugging in other contextual simplification methods 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-12 18:58:37 +00:00
Christoph M. Wintersteiger 6319861e26 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-12 18:32:46 +00:00
Christoph M. Wintersteiger f399fe5e1d resolved conflicts 2016-02-12 18:29:46 +00:00
Christoph M. Wintersteiger 3356f36b8f Merge pull request #446 from msullivan/arm-build 
Fix gcc build failure on ARM caused by including <emmintrin.h>
 2016-02-12 18:27:14 +00:00
Nikolaj Bjorner e2dc7c6f64 add note that current re.complement is non-standard 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-12 17:12:43 +00:00
Nikolaj Bjorner 94453033b6 add partial support for complementation of regular expressions. Handles case of complementing character ranges 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-12 15:59:33 +00:00
Christoph M. Wintersteiger 9dbb8057ca Merge pull request #449 from kenmcmil/issue243 
fixed logging on return of Z3_compute_interpolant...
 2016-02-12 12:40:01 +00:00
Nikolaj Bjorner 8d61d36c3f add documentation methods to param_descrs, add C++ API and example for param_descrs. Issue #443 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-12 11:45:00 +00:00
Ken McMillan 8b90bc9e91 fixed logginf on return of Z3_compute_interpolant and added interpolation example to test_capi.c 2016-02-11 16:09:54 -08:00
Michael Sullivan fa598edf43 Fix gcc build failure on ARM caused by including <emmintrin.h> 
src/util/hwf.cpp tries to use <emmintrin.h> to directly use SSE
intrinsics. Make sure to only use those when actually on x86 or
x86_64.
 2016-02-10 20:47:08 +00:00
Nikolaj Bjorner 9ed7dadc02 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-10 15:02:28 +00:00
Nikolaj Bjorner a6e1c70eab fix documentation/default bug. #445 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-10 15:02:22 +00:00
Christoph M. Wintersteiger fa68b00563 Cleanliness 2016-02-10 14:39:33 +00:00
Christoph M. Wintersteiger c01f0323c3 Merge branch 'lackr' of https://github.com/MikolasJanota/z3 into MikolasJanota-lackr 2016-02-10 14:26:04 +00:00
Nikolaj Bjorner 84cf208d5f Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-10 12:02:51 +00:00
Nikolaj Bjorner 535fb39313 add documentation comments as raised in #443 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-10 12:02:40 +00:00
Nikolaj Bjorner 56f15e98b5 Merge pull request #444 from delcypher/explicit_solver_timeout_units 
Explicitly state what the units of the timeout parameter for the "smt" module are.
 2016-02-10 11:43:31 +00:00
Dan Liew ea900db337 Explicitly state what the units of the timeout parameter for the "smt" 
module are.
 2016-02-10 11:35:15 +00:00
Nikolaj Bjorner 5285a795ac handle configuration passed in as null, deal with crash in logs attached to issue #243 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-10 01:20:16 +00:00
Nikolaj Bjorner cacfa0cb98 fix build, likely addressing issue #420 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-09 22:58:08 +00:00
Nikolaj Bjorner a0503ba6a1 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-09 22:24:48 +00:00
Nikolaj Bjorner 5ce85aba40 removing const qualifiers, perhaps this helps for #420 and adding assert to enable Clang analysis earlier for issue #440 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-09 22:23:37 +00:00
Mikolas Janota 73ef125171 Merge remote-tracking branch 'upstream/master' into lackr 2016-02-09 17:28:24 +00:00
Christoph M. Wintersteiger 4ba744987d Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-09 16:38:42 +00:00
Christoph M. Wintersteiger 3df9fea54c removed unused variables 2016-02-09 16:38:35 +00:00
Nuno Lopes 564343c39c remove unused methods in ast.cpp 2016-02-09 15:30:05 +00:00
Nikolaj Bjorner 60c0e73b2f Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-09 11:08:52 +00:00
Nikolaj Bjorner 133e3693de fix bug in replace built-in and move length-equality propagation to branch final check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-09 11:08:33 +00:00
Christoph M. Wintersteiger a2f376f9d6 Fixed memory leak in theory_fpa. Relates to #436 2016-02-08 17:17:49 +00:00
Christoph M. Wintersteiger 7e2783c6a2 Fixed javadoc links in comments. 
Relates to #401.
 2016-02-08 15:25:53 +00:00
Mikolas Janota b614e7732b Merge remote-tracking branch 'upstream/master' into lackr 2016-02-08 12:54:22 +00:00
Christoph M. Wintersteiger 92b6a3e134 Fixed exponent cap for fp.add in fpa2bv_converter (was unsound for combinations of many sbits but few ebits). 
Fixes #439.
 2016-02-07 17:33:33 +00:00
Christoph M. Wintersteiger e9d94e53f6 Improved FPA simplifier plugin 2016-02-07 15:01:22 +00:00
Christoph M. Wintersteiger 37b11cdc74 Comments, whitespace. 2016-02-07 15:01:09 +00:00
Nikolaj Bjorner 3ef6d91038 fix #434: repeat documentation remarks about reference counting for disambiguation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-07 14:46:53 +00:00
Nikolaj Bjorner 677b4bf4fe fix #436, adding more length-based propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-07 14:43:53 +00:00
Nikolaj Bjorner fc1f37efc9 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-06 16:14:07 +00:00
Nikolaj Bjorner 5b50d98b89 ensure that seq rewriter gets invoked during pre-processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-06 16:13:31 +00:00
Christoph M. Wintersteiger b61376e8c2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-05 15:22:42 +00:00
Christoph M. Wintersteiger 7ddd2856c8 Added is_considered_uninterpreted() to decl_plugins. 2016-02-05 15:22:37 +00:00
Christoph M. Wintersteiger 3d37c25bcc whitespace 2016-02-05 15:16:54 +00:00
Christoph M. Wintersteiger c11b6d90ce whitespace 2016-02-05 15:16:19 +00:00
Christoph M. Wintersteiger 757585d96f Merge pull request #427 from jwakely/patch-1 
Convert stream to bool explicitly
 2016-02-05 15:08:33 +00:00
Christoph M. Wintersteiger ac19bfb032 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-05 13:53:41 +00:00
Christoph M. Wintersteiger bb5118acbb Bugfix for bv*div0 model construction. 2016-02-05 13:53:35 +00:00
Christoph M. Wintersteiger 88f007e9da whitespace 2016-02-05 13:48:47 +00:00
Christoph M. Wintersteiger b87f4ca677 whitespace 2016-02-05 13:48:05 +00:00
Christoph M. Wintersteiger 21b85c27e1 whitespace 2016-02-05 13:47:14 +00:00
Nikolaj Bjorner eae17a43a2 Fix #430: disable rewriting of concatentations with constants because it breaks equality propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-05 11:00:17 +00:00
Nikolaj Bjorner cf970fd76a Fix #430: disable rewriting of concatentations with constants because it breaks equality propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-05 10:59:24 +00:00
Nikolaj Bjorner 2a65503235 fix #425 and report from Patrick Trentin of same bug in preprocessing soft constraints that are simplified to true/false 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-04 22:35:02 +00:00
Christoph M. Wintersteiger 808eb664cb Merge branch 'master' of https://github.com/Z3Prover/z3 into lackr 2016-02-04 18:27:19 +00:00
Nikolaj Bjorner 768bb84798 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-04 08:12:56 -08:00
Nikolaj Bjorner 9c7e5c37d1 add equality propagation based on partial length information to sequence theory. Fix issue #429 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-04 08:12:46 -08:00
Mikolas Janota 8547a965ab changing preamble for qfufbv_ackr_tactic. 2016-02-04 14:05:40 +00:00
Christoph M. Wintersteiger 4e37821dde "canceled" -> Z3_CANCELED_MSG 
Relates to #431
 2016-02-04 13:52:43 +00:00
mikolas faa620f673 Further refactoring ackermannization. 2016-02-03 17:31:19 +00:00
mikolas f3240024e7 Further refactoring ackermannization. 2016-02-03 17:26:58 +00:00
mikolas 2679b74543 refactoring 2016-02-03 13:53:52 +00:00
Mikolas Janota 6f12c0e6f9 bugfix in refactoring 2016-02-03 11:52:11 +00:00
Jonathan Wakely f02d273ee3 Convert stream to bool explicitly 
In C++11 there is no implicit conversion from iostream classes to `void*`, just an explicit conversion to bool.
 2016-02-02 23:39:11 +00:00
mikolas 0f0d3e55dc refactoring 2016-02-02 17:58:23 +00:00
mikolas 21b332235a Merge branch 'lackr' of github.com:MikolasJanota/z3 into lackr 2016-02-02 15:04:32 +00:00
mikolas bcab9a3600 re-factoring 2016-02-02 15:04:20 +00:00
Christoph M. Wintersteiger 3f6a1eb8c5 Fix for QF_BV core theory detection. 2016-02-02 13:01:32 +00:00
Christoph M. Wintersteiger 35c21779e3 Merge branch 'master' of https://github.com/Z3Prover/z3 into lackr 2016-02-02 11:29:35 +00:00
Nikolaj Bjorner 9b979b6e1e more string optimizations based on Chris' examples 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-01 17:08:11 -08:00
Christoph M. Wintersteiger 0b298b4df9 Minor fixes for QF_BV div0 ackermannization 2016-02-01 18:04:19 +00:00
Nuno Lopes 16a69e750a fix break in configure 2016-02-01 17:38:14 +00:00
Nuno Lopes ea55bd495f add new API function Z3_get_estimated_alloc_size() that returns *estimated* allocated memory size by Z3 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2016-02-01 17:19:55 +00:00
Nuno Lopes b9c0578eea fix build on C++98 compilers 2016-02-01 17:12:22 +00:00
Nikolaj Bjorner fe6799699c Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-01 07:51:26 -08:00
Nikolaj Bjorner 995a2e1a29 perf tuning based on Chris's examples 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-01 07:51:05 -08:00
Nuno Lopes cc6769c866 improve bit-blasting for the case (bvsrem var power-of-two) 
We will now transform bvsrem into an extract + zero extend
Gives ~40% speedup in selected benchmarks

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2016-02-01 13:46:55 +00:00
mikolas de28e57dee Adding parameters to Ackermannization in qfbv_tactic. 2016-01-29 17:21:21 +00:00
mikolas c9799b143d Adding parameters to Ackermannization in qfbv_tactic. 2016-01-29 17:18:21 +00:00
Mikolas Janota 470b5c20fe Small modifs in ackermannization. 2016-01-29 16:43:18 +00:00
mikolas 2ce7dc68ad Adding a probe for estimating the number of Ackermann congruence lemas. 2016-01-29 15:37:10 +00:00
Nikolaj Bjorner 2115111dac update display method for datalog to use predicates, throttle use of extensionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-28 20:23:06 -08:00
Mikolas Janota 3e94a44540 Refactoring ackermannization functionality. 2016-01-28 18:18:42 +00:00
Nikolaj Bjorner 847607bda7 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-28 08:51:40 -08:00
Nikolaj Bjorner 30f8110488 fix bugs exposed by Chris' sequence unit tests. Improve diagnostics for reason-unknown in combined solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-28 08:51:04 -08:00
Nikolaj Bjorner b352d43e50 fix bugs exposed by Chris' sequence unit tests. Improve diagnostics for reason-unknown in combined solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-28 08:50:13 -08:00
Mikolas Janota 53c187671f Merge branch 'lackr' of github.com:MikolasJanota/z3 into lackr 2016-01-28 11:48:20 +00:00
mikolas acd01c7778 Adding a probe for qf_ufbv and applying it in the qfufbv_ackr_tactic. 2016-01-28 11:46:31 +00:00
Christoph M. Wintersteiger 20df9e1cd1 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-28 11:14:11 +00:00
Christoph M. Wintersteiger 5f0ea74e89 Made ufbv-rewriter tactic public 2016-01-28 11:14:01 +00:00
Nikolaj Bjorner 512aa0e8d3 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-27 14:47:24 -08:00
Nikolaj Bjorner 87228b6a9d add a little more verbiage to description of simplify. Issue #424 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-27 14:47:15 -08:00
Nuno Lopes ac2e8f8b57 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-27 18:09:36 +00:00
Nuno Lopes ee2bae898a remove unused exceeded_memory_allocations class 2016-01-27 18:09:24 +00:00
Mikolas Janota 28a5c27e33 Merge branch 'lackr' of github.com:MikolasJanota/z3 into lackr 2016-01-27 16:27:35 +00:00
Mikolas Janota e318d460d7 dbg printing 2016-01-27 16:27:31 +00:00
mikolas 956d774299 Detecting OP_BSDIV0, etc. as uninterpreted functions in ackermannization. 2016-01-27 16:22:28 +00:00
Mikolas Janota 4b37140780 small fix 2016-01-26 18:11:33 +00:00
Nikolaj Bjorner 6529d43fb1 fix bugs exposed by unit tests from Pierre 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-26 09:50:14 -08:00
Mikolas Janota 0dc8dc4d8e Moving things around. Adding tactic just for ackermannization. 2016-01-26 17:02:30 +00:00
Mikolas Janota 470f8bca73 Merge remote-tracking branch 'upstream/master' into lackr 2016-01-26 16:51:57 +00:00
Mikolas Janota c63f9f4912 Moving things around. Adding tactic just for ackermannization. 2016-01-26 16:50:00 +00:00
Nikolaj Bjorner 8e378062e2 add get-some-value to seq API, expose quantifier tactics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-26 08:05:44 -08:00
Nikolaj Bjorner 345f6e87bd seq bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-26 07:21:31 -08:00
Mikolas Janota 3978410fcb Merge branch 'lackr' of github.com:MikolasJanota/z3 into lackr 2016-01-26 14:23:50 +00:00
mikolas d32c9449b2 Editing some comments and also enabling to export the ackermannized formula as a gole. 2016-01-26 11:53:47 +00:00
Mikolas Janota c2edf2c5bf Merge remote-tracking branch 'upstream/master' into lackr 2016-01-25 13:04:46 +00:00
Nikolaj Bjorner 924f03c6de fixing bugs in seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-23 10:38:49 -05:00
Nikolaj Bjorner 993a0434b4 fix warning message for unused variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-19 23:47:35 -05:00
Nikolaj Bjorner 099e572a26 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-19 19:10:08 +01:00
Nikolaj Bjorner a021e51a9c make parse error a bit more informative 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-19 19:09:41 +01:00
Nuno Lopes 23cc8258fe remove m_ast_lim from API context since that one isn't used either 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2016-01-19 15:37:58 +00:00
Nuno Lopes 1f872e720d remove m_replay_stack from API context since it's never used 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2016-01-19 15:19:00 +00:00
Nikolaj Bjorner d9e4648d8d Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-19 13:57:59 +01:00
Nikolaj Bjorner cccd502a4d bug-fixes to sequence theory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-19 13:57:47 +01:00
Christoph M. Wintersteiger 4dba5270ad Efficiency fix for fp.div. 2016-01-18 18:09:29 +00:00
Christoph M. Wintersteiger 99176cca60 Bugfix for FP model converter. 2016-01-18 18:00:04 +00:00
Nikolaj Bjorner c9373ebc9f fix axiomatization for at 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-18 12:01:15 +05:30
Nikolaj Bjorner 6aed3c3a44 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-18 11:09:52 +05:30
Nikolaj Bjorner 85d44c5d66 fix axioms for extract, add extensionality checking for shared variables, convert exceptions to unknown status per #419 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-18 11:09:41 +05:30
Christoph M. Wintersteiger 99d2ab4e8e Undid previous update of SMT2 scanner to support the new SMT2.5 string escaping. 2016-01-17 14:24:02 +00:00
Christoph M. Wintersteiger 01cb20e098 Fix for escape sequences in SMT2 scanner 2016-01-16 13:53:29 +00:00
Nikolaj Bjorner 88362a1c3a fix bugs in sequence extraction from NFA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-15 16:32:43 +05:30
Nikolaj Bjorner 14c19fe928 add parameter validation to sequence expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-15 10:39:21 +05:30
Nikolaj Bjorner 150c5c283d update re simplification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-15 10:11:39 +05:30
Nikolaj Bjorner a295dd48dc add seq_rewriter to model_evaluator, remove th_rewriter additional step in validator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-15 04:02:48 +05:30
Nikolaj Bjorner 7cbd59bf06 enhance model validation to invoke rewriter if result isn't true using the simplify-based model evaluator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-15 03:40:33 +05:30
Nikolaj Bjorner 01fd3c919b fix tout -> out. Tune generation of automata transitions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-15 03:32:27 +05:30
Nikolaj Bjorner 2d41b0e29b fix tout -> out. Tune generation of automata transitions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-15 03:31:30 +05:30
Mikolas Janota c6df8b3128 Merge remote-tracking branch 'upstream/master' into lackr 2016-01-14 15:25:04 +00:00
Mikolas Janota 7ec13166b1 Merge branch 'lackr' of github.com:MikolasJanota/z3 into lackr 2016-01-14 14:21:28 +00:00
mikolas d97e2b432c Ackermann run on separate assertions rather than an AND thereof. 2016-01-14 14:11:11 +00:00
Christoph M. Wintersteiger 0f082578cb Debug-fix for theory_seq. Fixes #418. 2016-01-14 13:07:48 +00:00
Nikolaj Bjorner 3ff97357a3 fix back rewriting for concat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-14 11:22:11 +01:00
Nikolaj Bjorner de9c959241 add support for re.nostr, re.all, fix bug in disequality handling of sequences, update signature of loop to handle integer arguments and variable arguments 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-14 10:56:03 +01:00
Nikolaj Bjorner a81c7c48d0 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-14 00:56:52 +01:00
Nikolaj Bjorner 2f0a049df8 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-13 20:13:29 +01:00
Nikolaj Bjorner e0215400e2 add empty/full regular languages, escape sequence fixes, check cancellation inside simplifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-13 20:13:17 +01:00
Mikolas Janota a5ea17f1e3 Merge remote-tracking branch 'upstream/master' into lackr 2016-01-13 18:22:58 +00:00
Christoph M. Wintersteiger 357ec9e7d1 Changed FP significand/exponent functions to return non-normalized results. Clarified function remarks. Relates to #383. 2016-01-13 16:32:32 +00:00
Mikolas Janota 094d357b07 Merge remote-tracking branch 'upstream/master' into lackr 2016-01-13 12:10:36 +00:00
Nikolaj Bjorner 57e1d4dc1f model generation with strings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-13 10:39:38 +01:00
Nikolaj Bjorner 9909c056f0 add range / loop handling for re. Fix regression reading mixed numerals reported by Trentin 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-13 00:49:31 -08:00
Nikolaj Bjorner 9a6fe93e6c re-enable feature that lets Z3 solver mixed integer/real constraints with additional information tha texpressions with sort real can only take integer values. Fixes regression on epsilon.smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-12 12:42:18 -08:00
Nikolaj Bjorner e2d54940b4 revert mixed integer/real handling pending fix to equality propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-12 12:11:27 -08:00
Nikolaj Bjorner f8971362c8 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-12 11:19:04 -08:00
Nikolaj Bjorner 22fbed18cc fix regressions exposed by build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-12 11:18:52 -08:00
Christoph M. Wintersteiger f093ebe44c Optimization for initialization of mpf's from tiny reals. 2016-01-12 19:06:53 +00:00
Nikolaj Bjorner db746e0c2f fix more unused variable warning messages 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-12 09:52:16 -08:00
Nikolaj Bjorner 985fc50961 breaking regression tests: ensure that model values are of the sort of the original expression. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-12 09:48:43 -08:00
Nikolaj Bjorner db71563478 fix build compiler warnings on OSX 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-12 09:36:01 -08:00
Nikolaj Bjorner 01c3e02e99 fix query for non-relational engines 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-12 07:57:10 -08:00