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

5531 commits

Author SHA1 Message Date
Doug Woos 89ba99918e reindent 2017-01-31 11:48:52 -08:00
Doug Woos c0bb6dd2be delete unused args 2017-01-31 11:48:51 -08:00
Doug Woos da63f6b0ff delete comment 2017-01-31 11:48:51 -08:00
Doug Woos b00c4d2e64 add name 2017-01-31 11:48:51 -08:00
Murphy Berzish 19779f1a9b fix string operators in theory_str, this breaks theory_seq temporarily 2017-01-31 11:49:10 -05:00
Nikolaj Bjorner 1d1949e395 ensure that parallel threads are only invoked when thread count > 1 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 18:30:06 -08:00
Doug Woos 8196173e29 Introduce and use labels_vec 2017-01-30 15:50:34 -08:00
Doug Woos 3791810920 add const & 2017-01-30 15:09:57 -08:00
Murphy Berzish ebcfa966c7 data structure refactor in theory_str 2017-01-30 16:07:32 -05:00
Nikolaj Bjorner 76bc4f0b38 refine parsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 11:30:42 -08:00
Nikolaj Bjorner dadcc6e8ff Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-30 02:09:26 -08:00
Nikolaj Bjorner 37ee4c95c3 adding parallel threads 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 02:09:08 -08:00
Murphy Berzish fa1ec0b80f smtlib25 draft standard in theory_str 2017-01-27 16:49:40 -05:00
Murphy Berzish a879b24011 add str.prefixof, str.suffixof in theory_str 2017-01-27 16:26:30 -05:00
Doug Woos a9d61d48ae Add basic Sine Qua Non filtering 2017-01-27 11:22:39 -08:00
Doug Woos 5796e15088 Thread labels through tactic system 2017-01-27 11:07:13 -08:00
Nikolaj Bjorner b70f1f0319 fix overflow exposed in #880 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-27 09:47:18 -08:00
Nikolaj Bjorner 962979b09c rework sat.mus to use restart count for bounded minimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-26 13:28:40 -08:00
Nikolaj Bjorner 7386e2f3e9 add warning for scearios of #876 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-25 18:29:30 -08:00
Nikolaj Bjorner 6e6c5935d7 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-25 18:09:37 -08:00
Nikolaj Bjorner 777091e653 fix part 1 of #875 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-25 18:09:27 -08:00
Nikolaj Bjorner 4782e19086 fix bug in sat-simplifier decreasing heap values of variables that are not in the heap 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-25 16:21:51 -08:00
Nikolaj Bjorner 60783e5696 fix regression for z3num 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-25 13:26:58 -08:00
Nikolaj Bjorner 4ec4abd7e3 fix test for int-value 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-23 13:31:43 -08:00
Murphy Berzish 09ac5645e4 parameterize theory-aware activity of overlap 2017-01-22 23:21:20 -05:00
Christoph M. Wintersteiger adf8072eaa Added option to limit the distance of unsat core extension through patterns. 2017-01-21 12:28:37 +00:00
Murphy Berzish 50e2273dbd substr bugfix 2017-01-20 17:39:32 -05:00
Nikolaj Bjorner 1bfd09e16b Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-19 19:31:24 -08:00
Nikolaj Bjorner e23509797a access parameters from Python API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-19 19:28:20 -08:00
Christoph M. Wintersteiger 5c1ffe13d1 x64 build fix for .NET 3.5 API 2017-01-18 13:06:28 +00:00
Christoph M. Wintersteiger 81c3a7dabd Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-18 12:32:10 +00:00
Christoph M. Wintersteiger a334020f2c Added .NET 3.5 solution/project files 2017-01-18 12:32:02 +00:00
Nikolaj Bjorner 16552d32cb Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-17 14:19:32 -08:00
Nikolaj Bjorner 0aa912371b Another fix for #847. Reset wmax theory solver state between lex calls, otherwise it uses stale constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-17 14:19:24 -08:00
Nikolaj Bjorner 735998c386 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-17 13:41:25 -08:00
Nikolaj Bjorner 873d975c77 fix bug in consequence extraction: the order of bcp is not fixed between restarts, so the order of unit literals may not be preserved. This is relatively rare, so we optimize for the case where we assume bcp preserves order (and maybe miss some consequences) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-17 13:41:15 -08:00
Murphy Berzish a570149b57 finite overlap models with binary search 2017-01-17 14:49:57 -05:00
Christoph M. Wintersteiger 6d34899c46 Bugfix for macro finder. Fixes #832. 2017-01-17 15:44:03 +00:00
Murphy Berzish 794e210958 finite model fix 2017-01-16 21:42:11 -05:00
Murphy Berzish 0af834421f finite model finding for other concat cases in theory_str 2017-01-16 18:24:47 -05:00
Murphy Berzish e459617c39 experimental finite model finding WIP, first successful run 2017-01-16 18:04:03 -05:00
Murphy Berzish 4e2847dea4 Revert "scale theory-aware priority by bvar_inc" 
This reverts commit aa8bf2668f.
 2017-01-16 15:46:28 -05:00
Murphy Berzish 4b6582b8f3 Revert "experimental z3str2 search order" 
This reverts commit 0dfaa30ae8.
 2017-01-16 15:46:17 -05:00
Murphy Berzish 0dfaa30ae8 experimental z3str2 search order 2017-01-16 14:46:04 -05:00
Christoph M. Wintersteiger e472a8d4cf Enabled filenames in error messages during inclusion of files. 2017-01-16 15:46:58 +00:00
Christoph M. Wintersteiger 090a331d79 Added filenames to error messages for when we have more than one file. 2017-01-16 15:43:13 +00:00
Christoph M. Wintersteiger 00a50eea7f Added (include ...) SMT2 command. 2017-01-16 15:05:58 +00:00
Nikolaj Bjorner dc543a7ee7 update macro_util logging to uniform format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 21:13:22 -08:00
Nikolaj Bjorner c4c9de0838 fix memory leaks from cancellations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 20:09:27 -08:00
Nikolaj Bjorner 24eae3f6e0 fix crash with unary xor #870 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 12:06:56 -08:00
Nikolaj Bjorner ee36662435 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-15 11:56:01 -08:00
Nikolaj Bjorner 7df803c131 Fix unsound handling of upper bounds in wmax, thanks to Patrick Trentin for report and careful repros #847 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 11:52:48 -08:00
Murphy Berzish aa8bf2668f scale theory-aware priority by bvar_inc 2017-01-14 15:28:58 -05:00
Murphy Berzish a9ec8666f0 add phase selection to theory-aware branching queue 2017-01-14 14:43:57 -05:00
Nikolaj Bjorner bc6b3007de remove unused features related to weighted check-sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-13 20:53:22 -08:00
Murphy Berzish dd03632f3d Merge branch 'develop' of github.com:mtrberzi/z3 into develop 2017-01-13 12:57:50 -05:00
Murphy Berzish f033a77fae modify theory-aware branching to manipulate activity instead of giving absolute priority 2017-01-13 12:57:48 -05:00
Murphy Berzish 677fcdcb41 concat overlap avoid in theory_str 2017-01-12 18:41:30 -05:00
Christoph M. Wintersteiger f1a4a48491 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-12 12:49:35 +00:00
Christoph M. Wintersteiger 2458db30cf Corner-case fix for smt::solver::pop_core 2017-01-12 12:49:26 +00:00
Murphy Berzish 6576dabd58 add tracing info to theory_str cut var map 2017-01-12 00:20:34 -05:00
Daniel Perelman 3370adcdff Mark void DummyContracts as Conditional to avoid compiling their arguments. 2017-01-11 17:02:26 -08:00
Christoph M. Wintersteiger 650ea7b9cc Bugfix for smt.core.extend_patterns 2017-01-11 18:40:11 +00:00
Murphy Berzish 20a8ad9b21 correctly reserve entries in theory aware branching queue heap 2017-01-10 22:15:46 -05:00
Murphy Berzish bc5af58734 additional theory-aware branches in theory_str 2017-01-10 20:08:35 -05:00
Murphy Berzish 1363f50e4f demonstration of theory-aware branching in theory_str, WIP 2017-01-10 19:50:46 -05:00
Christoph M. Wintersteiger 9f49905582 Formatting, whitespace, and Z3_API annotations. 2017-01-10 21:05:27 +00:00
Christoph M. Wintersteiger d8d869822f Cleaned up #include<iostream> in api* objects. 2017-01-10 21:04:44 +00:00
Murphy Berzish 3459c1993e experimental theory-aware branching code 2017-01-10 15:38:33 -05:00
Christoph M. Wintersteiger 384468bc99 Added option to extend unsat cores with literals that (potentially) provide quantifier instances. 2017-01-10 20:22:20 +00:00
Christoph M. Wintersteiger ba9d36605b Formatting, whitespace 2017-01-10 20:22:20 +00:00
Murphy Berzish 9004e1b23e disable length test/theory case split integration theory_str 2017-01-10 12:34:44 -05:00
Christoph M. Wintersteiger 8047f0d91a GCC compilation/keyword fix. Relates to #864 2017-01-10 14:06:56 +00:00
Christoph M. Wintersteiger 8f95ee01e1 Removed polynomial factorization test cases. Relates to #852 and fixes #865. 2017-01-10 14:02:59 +00:00
Nikolaj Bjorner 331658f208 remove polynomial factorization as suggested by issue #852 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-09 21:30:54 -08:00
Nikolaj Bjorner 8d09b6e4a8 add at-least and pbge to API, fix for issue #864 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-09 21:23:00 -08:00
Murphy Berzish 5f854c6689 experimental linear search theory case split in theory_str 2017-01-09 15:11:56 -05:00
Murphy Berzish 6f5c1942f0 theory_str length propagation 2017-01-08 20:15:45 -05:00
Nikolaj Bjorner c69a86e647 fix bug in antecedent collection for consequence finding: once an antecedent is set, it should not be cleared 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-06 19:34:50 -05:00
Nikolaj Bjorner e9edcdc6e6 moderate exception behavior for issue #861 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-05 16:09:16 -05:00
Nikolaj Bjorner f443bfed87 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-04 19:05:52 -08:00
Nikolaj Bjorner ddf4bc548f allow disabling exceptions from C++. Issue #861 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-04 19:04:43 -08:00
Murphy Berzish c190d45859 fix binary search string length axiom 2017-01-04 15:56:16 -05:00
Nikolaj Bjorner ae9a3bfc24 add operator for issue #860 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-04 09:14:09 -08:00
Murphy Berzish f9d7981c1e add theory case split to theory_str binary search 2017-01-03 15:45:04 -05:00
Christoph M. Wintersteiger cb75a55095 Fixed initialization order warning. 2017-01-03 13:41:08 +00:00
Nikolaj Bjorner 74d3de01b3 enable incremental consequence finding with restart timeout 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-02 10:07:02 -08:00
Murphy Berzish f3e064cb07 theory_str binary search crash avoidance when a negative length is reached 2016-12-31 13:28:32 -05:00
Nikolaj Bjorner a4d5c4a00a make get_consequence call skip check-sat if a model is already there 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-30 18:05:19 -08:00
Nikolaj Bjorner 8dde60f634 initialize watch in assign_eh 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-26 10:18:55 -08:00
Nikolaj Bjorner aaf6e67ec8 add restart.max parameter to control cancellation based on restart count 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-25 17:43:47 -08:00
Nikolaj Bjorner 2bd29548da improve parser error message over API, streamline names of statistics for arithmetic solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-25 17:27:56 -08:00
Nikolaj Bjorner c44dd01292 fix missing else reported in #855 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-22 20:56:14 -08:00
Nikolaj Bjorner 46df31babf Merge branch 'master' of https://github.com/Z3Prover/z3 2016-12-22 20:54:14 -08:00
Nikolaj Bjorner 1787fa8296 remove redundant disjunction in compilation of at-most-1 constraints, log mutexes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-22 20:54:09 -08:00
Nikolaj Bjorner a444a33c30 updated encodings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-22 17:45:21 -08:00
Murphy Berzish 0a6c23148f fix empty vector edge case in binary search 2016-12-22 19:33:38 -05:00
Murphy Berzish 2dc9b486d3 theory_str binary search heuristic WIP 2016-12-22 19:17:42 -05:00
Nikolaj Bjorner f52baf1e17 fix build again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-21 10:48:43 -08:00
Nikolaj Bjorner 4bcf1bf2f6 fix debug build, unused variable warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-21 10:44:49 -08:00
Nikolaj Bjorner df492e200f merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-21 10:04:02 -08:00
Nikolaj Bjorner 8d18fd075e remove sources for unused variable warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-21 09:54:45 -08:00
Murphy Berzish df63b62763 fix vector manip bug in theory case split 2016-12-20 17:32:51 -05:00
Murphy Berzish ab0fcc42f9 theory case split heuristic 2016-12-20 16:21:07 -05:00
Murphy Berzish a04bc9974b theory case split WIP 2016-12-20 11:14:42 -05:00
Dan Liew b5aa6d5eb5 Fix issue with bd1f07f864 pointed out by 
@nunolopes .

If `pthread_cond_signal()` is called while `m_mutex` is held then the
timing thread might be woken up twice due to waking up from
`pthread_cond_timeout()` (due to being signaled) but then being forced
to sleep again because the thread calling `~imp()` is still holding
`m_mutex` (which the timing thread needs to acquire).
 2016-12-19 22:36:42 +00:00
Nikolaj Bjorner 0c6c104f9a Merge pull request #841 from delcypher/scope_timer_spurious_wakes 
Make `scoped_timer` robust to spurious wakes under Linux.
 2016-12-19 08:22:03 -08:00
Murphy Berzish 94762d276d add string constant cache to theory_str and associated param 2016-12-18 18:47:38 -05:00
Nikolaj Bjorner 189d449cff fix generation of wcnf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-18 14:49:45 -08:00
Murphy Berzish e5d3e425f1 theory_str caching of all string constants 2016-12-18 15:23:05 -05:00
Nikolaj Bjorner 5083b1adee Merge branch 'master' of https://github.com/Z3Prover/z3 2016-12-17 16:03:02 -08:00
Nikolaj Bjorner 5cb21924ad ensure that FD logic understands pb from command context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-17 16:02:54 -08:00
Murphy Berzish e85f9d33c4 add "legacy" support for theory case splits 
this replicates what was done in theory_str to add axioms excluding each
pair of literals from being assigned True at the same time;
no new heuristics are being used in smt_context (yet)
 2016-12-16 15:50:03 -05:00
Christoph M. Wintersteiger 6ce903b1d6 Style, whitespace. 2016-12-16 20:04:29 +00:00
Murphy Berzish dd8cd8199b theory_str refcount debug messages and beginning theory case split 2016-12-16 14:37:34 -05:00
Murphy Berzish 67e7307777 add cut var debug info, wip 2016-12-14 15:00:17 -05:00
Murphy Berzish 27a2c20c1c add more parameters for theory_str 2016-12-13 19:38:40 -05:00
Murphy Berzish bced5828f7 theory_str parameters 2016-12-13 17:20:58 -05:00
Murphy Berzish f5bc17b864 theory_str params module, WIP 2016-12-13 16:12:57 -05:00
Nikolaj Bjorner c1480b4389 handle model generation from issue #748. Deal with warnings from #836 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-12 00:40:52 +01:00
Dan Liew bd1f07f864 Fix implementation of scoped_timer under Linux where it was 
incorrectly assumed that `pthread_cond_timedwait()` would exit
due to a condition variable being signaled or a timeout occuring.

According to the documentation `pthread_cond_timedwait()` might
spuriously wake so we introduce a new variable `m_signal_sent` (that is
guarded by an existing mutex) that is used as the variable to check that
the thread wake was not spurious.

This is intended to partially fix #839 .
 2016-12-11 23:12:36 +00:00
Nikolaj Bjorner 7cc093eee0 Add rewrite rule for property encoded in #812 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-11 11:05:12 +01:00
Nikolaj Bjorner 2307a7ffa7 fix bug in handling of repeated soft constraints. #815 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-11 10:19:57 +01:00
Nikolaj Bjorner 0765eea486 add suggestions from #835 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-11 05:45:40 +01:00
Nikolaj Bjorner 70bb92d016 remove nested booleans during pre-processing. issue #837 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-11 05:16:31 +01:00
Nikolaj Bjorner ff46a925a2 bail out on failure to properly project. issue #837 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-11 04:25:05 +01:00
Nikolaj Bjorner 20790c46ee bail out on failure to properly project 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-11 04:23:07 +01:00
Nikolaj Bjorner 32c63ce4cd address other warnings per input from delcypher 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-10 17:23:59 +01:00
Nikolaj Bjorner 6594c3a046 add virtual destructor to intermediary class in case this helps for #835 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-10 13:58:39 +01:00
Nikolaj Bjorner dea3b8ddf7 address warnings from #836 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-10 13:14:36 +01:00
Nikolaj Bjorner 8e078cf9e2 address #835 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-10 07:52:00 +01:00
Nikolaj Bjorner fe10f2d244 address #835 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-10 07:51:16 +01:00
Murphy Berzish 09053b831d enforce nonempty string constraint on refreshed nonempty string vars 2016-12-09 17:23:39 -05:00
Nikolaj Bjorner 0ef14ffa08 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-12-09 23:18:02 +01:00
Nikolaj Bjorner e092232f67 add virtual destructors, fix operator code for API methods complement and intersection per note by Loris d'Antoni 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 23:17:52 +01:00
Murphy Berzish e9411e5b8c explicitly re-introduce string axioms on refreshed string theory vars 
this fixes at least one case (kaluza/unsat/big/9650.smt2) where a string
could have a negative length value due to a constraint that went out of scope
 2016-12-09 17:12:29 -05:00
Murphy Berzish 737565180f disable stronger arrangements in theory_str for now 2016-12-09 16:55:34 -05:00
Christoph M. Wintersteiger 4c664f1c05 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-12-09 15:03:36 +00:00
Christoph M. Wintersteiger 16b32ecf12 Bugfix for special-case handling in fp.fma. 
Thanks to Florian Schanda for reporting this bug.

(+reversed accidental debug code commit).
 2016-12-09 15:03:31 +00:00
Nikolaj Bjorner a17e957362 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-12-09 15:32:26 +01:00
Nikolaj Bjorner acba529bce fix bug in encoding of axioms for indexof. Issue #806 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 15:32:15 +01:00
Christoph M. Wintersteiger 56b1a8b086 Bugfix for special-case handling in fp.fma. 
Thanks to Florian Schanda for reporting this bug.
 2016-12-09 13:43:05 +00:00
Christoph M. Wintersteiger 9df5c31485 Whitespace 2016-12-09 13:40:46 +00:00
Nikolaj Bjorner 0ab2067b69 produce error message for cores with optimization. Issue #825 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 13:15:40 +01:00
Nikolaj Bjorner 99b7c26e9f exposing regular expression features to address issue #831 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 13:05:02 +01:00
Nikolaj Bjorner 8e6600c6be add python API for newly exposed regex constructors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 09:09:03 +01:00
Nikolaj Bjorner 976fadf771 add missing complement 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 06:21:57 +01:00
Nikolaj Bjorner 0473d2ef56 add regular expression features to C# API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 06:17:13 +01:00
Nikolaj Bjorner a82b5e21fe add regular expression operations to C and C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 06:11:36 +01:00
Murphy Berzish 515cd4a3f3 add boolean case split in theory_str::solve_concat_eq_str 2016-12-08 14:49:38 -05:00
Nikolaj Bjorner 4e25bffab6 add range constructor to .NET API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-08 18:33:02 +01:00
Nikolaj Bjorner feb801564b adding range to C API. Issue #831 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-08 18:28:27 +01:00
Christoph M. Wintersteiger dc0d29a00c Bugfix for model construction. Fixes #828. 2016-12-08 16:14:54 +00:00
Murphy Berzish 7b0aaf8745 boolean case split theory_str concat_eq remaining cases 2016-12-06 16:22:42 -05:00
Murphy Berzish 225b527d58 boolean case split theory_str process_concat_eq_type2 2016-12-06 16:09:38 -05:00
Murphy Berzish b57f04e2d2 optimize generate_mutual_exclusion in theory_str to make only half as many subterms 2016-12-06 12:59:40 -05:00
Murphy Berzish da61c99f9e experimental boolean case split in theory_str process_concat_eq_type1 WIP 2016-12-06 12:52:48 -05:00
Murphy Berzish 938dcaa669 Merge branch 'develop' of github.com:/mtrberzi/z3 into develop 2016-12-05 20:17:44 -05:00
Murphy Berzish be9cb8db82 regex tracing theory_str 2016-12-05 20:17:43 -05:00
Murphy Berzish 35ad68d9b5 assert stronger arrangements theory_str 2016-12-05 15:13:48 -05:00
Christoph M. Wintersteiger f1a704484b Re-added context creation locks in the Java API. Relates to #819. 2016-12-01 23:16:15 +00:00
Murphy Berzish 406b622f59 Revert "testing term generation refactor in theory_str::check_length_const_string" 
This reverts commit edf151c9a0.
 2016-12-01 15:19:51 -05:00
Murphy Berzish b020c71f8a Revert "ref_vector refactoring in theory_str::check_length_concat_concat" 
This reverts commit 599cc1e75d.
 2016-12-01 15:19:51 -05:00
Murphy Berzish 548f635f7e Revert "experimental non-reuse of XOR vars in theory_str" 
This reverts commit fd1bf65b64.
 2016-12-01 15:19:50 -05:00
Murphy Berzish 10c0d94cf2 Revert "refactor theory_str::check_length_concat_var" 
This reverts commit 170e2b4e2a.
 2016-12-01 15:19:50 -05:00
Nuno Lopes dedae29300 add a few more statics to avoid symbol clashes 2016-12-01 17:37:07 +00:00
Nuno Lopes e697d3e810 remove 2 outdated comments 2016-12-01 14:10:31 +00:00
Nuno Lopes 42b26c63e5 make a few functions static 2016-12-01 14:01:20 +00:00
Murphy Berzish 170e2b4e2a refactor theory_str::check_length_concat_var 2016-11-30 19:41:00 -05:00
Murphy Berzish fd1bf65b64 experimental non-reuse of XOR vars in theory_str 2016-11-30 15:52:58 -05:00
Murphy Berzish 599cc1e75d ref_vector refactoring in theory_str::check_length_concat_concat 2016-11-30 13:08:42 -05:00
Nikolaj Bjorner 7ebc660b6d Merge branch 'master' of https://github.com/Z3Prover/z3 2016-11-30 09:52:15 -08:00
Nikolaj Bjorner 024082a45f adding preferred sat, currently disabled, to wmax. Fixing issue #815 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-30 09:52:05 -08:00
Murphy Berzish edf151c9a0 testing term generation refactor in theory_str::check_length_const_string 2016-11-29 21:46:00 -05:00
Murphy Berzish 947d443726 improved regex concat rewrite 2016-11-29 19:46:37 -05:00
Nikolaj Bjorner d9227b95ea blast distinct in incremental BV solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-29 15:45:23 -08:00
Murphy Berzish 361f02ef1d remove assignment refcount hack from theory_str::pop_scope_eh 2016-11-28 21:34:55 -05:00
Murphy Berzish f968f79d1c refactor solve_concat_eq_str to use expr_ref_vector 2016-11-28 18:47:42 -05:00
Murphy Berzish b77f6666dc refactor process_concat_eq_type_6 to use expr_ref_vector 2016-11-28 18:40:28 -05:00
Murphy Berzish 1e65511a3f save a few functions to trail in theory_str 2016-11-28 16:21:26 -05:00
Nuno Lopes 4b4365470d mam compiler: move reset of matched_exprs cache next to code reset 2016-11-28 15:40:25 +00:00
Nuno Lopes 2babd192b8 small optimization in compilation of multi-patterns 
also make the path faster for single patterns
 2016-11-28 14:43:47 +00:00
Nuno Lopes 4452ac0d6d optimize pattern matching code generator for DAG patterns 
generated code now uses COMPARE instructions to compare subtrees instead of diving into both subtrees. Code is thus smaller and fails faster.
 2016-11-28 13:48:15 +00:00
Murphy Berzish 8c33dfab39 fix escape character overflow print 2016-11-27 20:51:34 -05:00
Christoph M. Wintersteiger 1799310155 Fixed iterator invalidation bug in SAT probing. Relates to #798. 2016-11-26 14:07:05 +00:00
Murphy Berzish 1fa8129c8f pretty-printing of general escape sequences for string literals 2016-11-25 18:02:24 -05:00
Nikolaj Bjorner 441dbbb94b streamline logging in arithmetic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-24 13:08:50 -08:00
Murphy Berzish 889b6be2c3 fix smt-lib 2.5 double quotes in pp 2016-11-23 19:03:53 -05:00
Martin Nowack 762e5fd093 Do not request time stamp if not needed 
If no timeout is needed for solving queries, time stamps do not
need to be acquired.
 2016-11-23 16:38:21 +01:00
Murphy Berzish 8e962aa427 escape chars in smt2 printing of string constants 2016-11-22 18:32:03 -05:00
Murphy Berzish 11d8ffc4d4 escape characters in theory_str 2016-11-22 18:21:40 -05:00
Nikolaj Bjorner 7a4c20698f fix handling of AC operator ++ on regular expressions. Issue #804 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-22 13:02:17 -08:00
Christoph M. Wintersteiger 71ca355257 Fixed OpenMP problems in log synchronization. Relates to #798. 2016-11-22 13:26:29 +00:00
Christoph M. Wintersteiger dee7c29b19 Added optional synchronization for multi-thread API logs. Relates to #798. 2016-11-22 11:32:25 +00:00
Nikolaj Bjorner d3fe015ff5 Merge pull request #796 from rickyz/nondependent_name 
Fix GCC/Clang compilation.
 2016-11-20 06:29:37 -08:00
Nikolaj Bjorner 725e79e9eb re-enable ematching on recursive function definitions, disabling ematching breaks regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-20 06:24:47 -08:00
Nikolaj Bjorner 650a719298 fix crash in new clique code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-20 06:20:22 -08:00
Ricky Zhou 9939d07827 Fix GCC/Clang compilation. 
The calls to negate use a non-dependent name, so GCC and Clang do not
examine dependent base classes when looking up the name. Adds a using
declaration as suggested at
https://isocpp.org/wiki/faq/templates#nondependent-name-lookup-members.
 2016-11-20 05:09:30 -08:00
Nikolaj Bjorner 6a9b5ea3af fix unsoundness reported in issue #777, disable ematching on recursive function definition axioms exposed in #793 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-19 15:29:43 -08:00
Nikolaj Bjorner 2ff5af7d42 fix bug incorrect clearing of goals during node creation. Issue #777 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-19 10:06:16 -08:00
Nikolaj Bjorner a5bae72bdf Merge branch 'master' of https://github.com/Z3Prover/z3 2016-11-19 08:09:55 -08:00
Nikolaj Bjorner df0e3a100c tune initialization for wmax and sortmax 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-19 08:04:06 -08:00
Nikolaj Bjorner ea601dd403 fix and coallesce clique functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-19 03:55:48 -08:00
Murphy Berzish 5e37a21802 fix expr_ref in theory_str splits WIP 2016-11-18 16:07:20 -05:00
Murphy Berzish 855037eed7 refactor process_concat_eq_type2 in theory_str; fixes unsat/big/8558 2016-11-17 16:25:53 -05:00
Murphy Berzish d260218e2b tabs to spaces test 2016-11-17 15:28:26 -05:00
Murphy Berzish e2d05578d6 add extra trace message in smt_context for theory_str results change 2016-11-17 15:25:39 -05:00
Christoph M. Wintersteiger ad76e536b2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-11-17 16:36:44 +00:00
Christoph M. Wintersteiger b138a0f6d3 Cleaned up hacky rewriter cancelation fix in theory_fpa. 2016-11-17 16:36:39 +00:00
Christoph M. Wintersteiger a97358965b Fixed interruption/cancelation issue in rewriter. 2016-11-17 16:28:49 +00:00
Nikolaj Bjorner 1600823435 fix perf bug reported in #790 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-17 05:38:52 +02:00
Nikolaj Bjorner 123b50ed3c Merge branch 'master' of https://github.com/Z3Prover/z3 2016-11-17 04:26:36 +02:00
Nikolaj Bjorner e9db934f1a improving perf of mutex finding, revert semantics of 0 timeout to no-timeout. Issue #791 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-17 04:26:17 +02:00
Murphy Berzish 55ae83f47e Revert "experimental modification to simplify_parent call in theory_str, WIP" 
This reverts commit 9771428600.
 2016-11-16 13:00:05 -05:00
Christoph M. Wintersteiger 9053e6eba6 Resolved merge conflicts. Added FPA API input validity checks. 2016-11-15 20:19:40 +00:00
Murphy Berzish 9771428600 experimental modification to simplify_parent call in theory_str, WIP 2016-11-15 15:18:07 -05:00
Christoph M. Wintersteiger dcf643f711 Merge branch 'master' of https://github.com/Z3Prover/z3 into gh570-att-2 2016-11-15 19:59:54 +00:00
Christoph M. Wintersteiger c7787feebb Assertion fix for theory_fpa. Relates to #570. 2016-11-15 19:59:22 +00:00
Christoph M. Wintersteiger ee60ba824f Bugfix for rewriter exceptions in theory_fpa. Relates to #570. 2016-11-15 19:59:08 +00:00
Nikolaj Bjorner e65d80dedd make semantics of extract/substr deterministic. Issue #781 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-15 18:29:51 +02:00
Nikolaj Bjorner fa8427258a Merge branch 'master' of https://github.com/Z3Prover/z3 2016-11-15 15:07:15 +02:00
Nikolaj Bjorner e21bd8dacc fix lexicographic combinations for wmax: pb constrsaints were not interpreted in Boolean benchmarks. #782 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-15 15:07:05 +02:00
Christoph M. Wintersteiger bfaa9ddf63 Fixed potential SAT solver cleanup problem. Renamed functions for consistency. Relates to #570. 2016-11-14 17:42:21 +00:00
Christoph M. Wintersteiger 520e868add Fixed interruption cleanup bug in sat_solver. Relates to #570. 2016-11-14 17:42:20 +00:00
Christoph M. Wintersteiger d099e26342 Fixed compiler warning 2016-11-14 17:42:20 +00:00
Christoph M. Wintersteiger 890142ef96 Fix cleanup/initialization of sat::simplifier. Relates to #570. 2016-11-14 17:42:20 +00:00
Christoph M. Wintersteiger 6204f67d38 Fixed problems with aborted rewriters in theory_fpa. Relates to #570. 2016-11-14 17:40:09 +00:00
Murphy Berzish df6b461117 enhanced backpropagation in theory_str final_check for var=concat terms 
fixes kaluza sat/big/709.smt2
 2016-11-14 12:33:23 -05:00
Nikolaj Bjorner fc7a217cd0 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-11-12 08:58:09 -08:00
Nikolaj Bjorner e0613b6737 fix crash reported in #784 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-12 08:58:03 -08:00
Christoph M. Wintersteiger 2df5a4e3f9 typo 2016-11-12 15:01:54 +00:00
Murphy Berzish 02aacab04e add z3str2-style free variable check to theory_str 2016-11-11 17:52:18 -05:00
Murphy Berzish fbaee080b2 fix performance regression introduced with theory_str str.from-int 
more investigation is required to understand why this works.
 2016-11-11 00:32:50 -05:00
Christoph M. Wintersteiger ca81e803cb Bugfix for Z3_fpa_get_numeral_sign. Relates to #570. 2016-11-10 21:33:42 +00:00
Christoph M. Wintersteiger b47c67dee3 Bugfix for Z3_fpa_get_numeral_*_uint64. Relates to #570. 2016-11-10 21:16:05 +00:00
Murphy Berzish 5635016205 theory_str str.from-int very WIP 2016-11-09 18:06:02 -05:00
Murphy Berzish fff1fadf3b add str.from-int in theory_str rewriter 2016-11-09 15:54:22 -05:00
Murphy Berzish 4aa2d965b3 Merge branch 'develop' of github.com:mtrberzi/z3 into develop 2016-11-09 14:05:38 -05:00
Murphy Berzish 61d1d5e8b0 add cache for length terms to theory_str, but it seems to slow things down so I disabled it 2016-11-08 15:20:47 -05:00
Murphy Berzish 521e0e175b refresh reused split vars in theory_str 
this fixes kaluza/unsat/big/7907, now SAT in ~30s
 2016-11-08 14:23:10 -05:00
Christoph M. Wintersteiger 1188e6df47 Typo 2016-11-08 15:28:20 +00:00
Christoph M. Wintersteiger e22a67c12c Whitespace 2016-11-08 15:27:46 +00:00
Christoph M. Wintersteiger e0066df6a9 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-11-08 15:12:08 +00:00
Christoph M. Wintersteiger a3e4629996 fixed hard-coded version number in setup.py 2016-11-08 15:12:04 +00:00
Christoph M. Wintersteiger 7c308ca8c6 Merge pull request #779 from ddcc/master 
Standardize on __uint64 instead of unsigned __int64
 2016-11-08 12:21:34 +00:00
Christoph M. Wintersteiger 889e5e9388 Bumped version number. 2016-11-07 23:19:59 +00:00
Dominic Chen 00ada5305f Standardize on __uint64 instead of unsigned __int64 2016-11-07 17:42:44 -05:00
Christoph M. Wintersteiger d57a2a6dce Bumped version to 4.5.0 2016-11-07 22:02:30 +00:00
Nikolaj Bjorner ef9230d8f8 detect quantifiers in model expressions to quiet down failing model validation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-07 06:56:36 -08:00
Christoph M. Wintersteiger 75cfd14e5a bugfix for macro finder 2016-11-07 14:14:45 +00:00
Christoph M. Wintersteiger 80e136f090 build fix 2016-11-07 13:51:09 +00:00
Christoph M. Wintersteiger 4e7077db70 Bugfix for denormal numeral exponents 2016-11-07 12:38:12 +00:00
Christoph M. Wintersteiger 758a6d98fb FPA API clarification 2016-11-07 12:35:48 +00:00
Christoph M. Wintersteiger 9ebea09d05 added is_numeral_negative to ML API. 2016-11-07 10:28:39 +00:00
Christoph M. Wintersteiger 5ef7d38d72 Whitespace 2016-11-05 14:39:23 +00:00
Christoph M. Wintersteiger 50c323dc74 Whitespace 2016-11-05 14:35:56 +00:00
Nikolaj Bjorner 69853ba6fc Merge branch 'master' of https://github.com/Z3Prover/z3 2016-11-05 08:18:59 +00:00
Nikolaj Bjorner caf0a1e80d fix breaking change to theory-seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-05 07:22:27 +00:00
Christoph M. Wintersteiger b1f7c6ac97 eliminated unnecessary variable 2016-11-04 22:08:49 +00:00
Christoph M. Wintersteiger 696bbc7708 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-11-04 21:27:16 +00:00
Christoph M. Wintersteiger ac7e1b145c Whitespace, typo 2016-11-04 21:27:10 +00:00
Christoph M. Wintersteiger 81fce55d78 Updated optimization ML API. Addresses #776. 2016-11-04 21:22:01 +00:00
Nikolaj Bjorner 152321bce6 fix crash in poly normalizer exposed by qe. Issue #775 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-04 20:29:12 +00:00
Nikolaj Bjorner 856cf7d4f9 fix generation of fresh constants for uninterpreted sort in EPR, Issue #649 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-04 15:51:35 +00:00
Nikolaj Bjorner e700460645 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-11-04 15:19:19 +00:00
Nikolaj Bjorner 51a4085910 check for logic in solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-04 15:19:11 +00:00
Christoph M. Wintersteiger 824ba14977 Disabled some ITE rewrite rules that were applied by default, but too expensive. Added re-computation of subterm occurrences in ctx_simplify_tactic. (Performance fixes for QF_LIA benchmarks). 2016-11-04 13:39:53 +00:00
Christoph M. Wintersteiger a3e915fbea Whitespace 2016-11-04 13:37:14 +00:00
Nikolaj Bjorner c0fb2eafe5 remove recursive expansion of else-case 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-02 23:08:10 +00:00
Nikolaj Bjorner be9d5c7088 fix evaluator for array store expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-02 21:33:24 +00:00
Murphy Berzish 3ae336fa6f add experimental value tester caching to theory_str 2016-11-02 13:05:16 -04:00
Murphy Berzish a61e1f17e8 fix crash in gen_len_test_options when fast length testers are disabled 2016-11-02 12:35:14 -04:00
Nikolaj Bjorner 46a4bc6030 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-11-02 14:15:05 +00:00
Nikolaj Bjorner f61600d1d8 fixing unsat core extraction for tactics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-02 14:14:55 +00:00
Christoph M. Wintersteiger c8689ed796 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-11-02 13:36:38 +00:00
Christoph M. Wintersteiger c81ee05098 Fixes for .NET Core build 2016-11-02 13:36:29 +00:00
Murphy Berzish 3da78f9d80 experimental cached length testers in theory_str 2016-11-01 20:35:01 -04:00
Nikolaj Bjorner 46c4fdaae5 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-11-01 18:39:00 +01:00
Murphy Berzish a5b00641d8 Merge branch 'develop' of github.com:mtrberzi/z3 into develop 2016-11-01 13:02:59 -04:00
Nikolaj Bjorner 305e080239 enable unsat core extraction in nlsat_tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-01 17:57:28 +01:00
Christoph M. Wintersteiger 026309a325 bugfix for disequality propagation in smt_context 2016-11-01 14:21:06 +00:00
Christoph M. Wintersteiger ed5137ffd2 build fix 2016-11-01 11:23:42 +00:00
Nikolaj Bjorner 84172302a2 fix bug in mutex extraction, reported by Patrick Trentin 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-01 00:16:16 +01:00
Nikolaj Bjorner ba942af5a8 disable sat solver when proofs are turned on. Fixes issue #768 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-31 23:27:39 +01:00
Nikolaj Bjorner fa1a0aa7ba remove buggy and unused equivalence relation plugin. Github issue #770 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-31 22:59:56 +01:00
Nikolaj Bjorner ff75f88c4f fix memory abuse in internalization in inc-sat-solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-31 22:25:58 +01:00
Murphy Berzish 452eed6626 move get_std_regex_str to str_util 2016-10-29 12:19:24 -04:00
Nikolaj Bjorner 596f07e548 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-28 08:27:21 -07:00
Nikolaj Bjorner 3714e520be fix performance bottlnecks: gc of literals walk through potentially huge watch-lists, avoid user-push/pop around calls to solver2tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-28 08:27:11 -07:00
Nikolaj Bjorner 7764148dd3 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-28 07:42:27 -07:00
Nikolaj Bjorner 2475f3bff5 ensure that variables passed to consequence finding have bound constraints, if applicable. Even if those variables do not occur in the constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-28 07:41:27 -07:00
Nikolaj Bjorner 4d078dc0a9 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-28 07:17:49 -07:00
Christoph M. Wintersteiger f1412d3f32 Bugfix for bouned_int2bv_solver 2016-10-28 14:23:01 +01:00
Christoph M. Wintersteiger 02e1bae9cb whitespace 2016-10-28 14:22:27 +01:00
Christoph M. Wintersteiger 9c16d16bc8 removed debug output 2016-10-28 12:22:28 +01:00
Nikolaj Bjorner ca309341c3 fixing cancellation code paths for inc_sat_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-27 22:07:46 -07:00
Nikolaj Bjorner b1d673e3eb catch cancellation exceptions, return undef 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-27 16:34:26 -07:00
Nikolaj Bjorner 7d7e03e377 rewind qhead to ensure re-propagation after cancellation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-27 16:23:33 -07:00
Nikolaj Bjorner 41deae52c6 fix enum2bv to handle singleton enumeration types, differentiate disequality conflicts for theories that handle disequalities vs. theories that don't 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-27 13:35:53 -07:00
Nikolaj Bjorner 24fc19ed58 speed up consequence finding by avoiding local search whenver assumption level is reached during the initial phase 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-27 08:15:39 -07:00
Christoph M. Wintersteiger 253cfeb0af Added FPA numeral accessors/predicates to Python API 2016-10-27 15:07:34 +01:00
Christoph M. Wintersteiger 95d7b33ebb Added is_numeral_negative to .NET and Java APIs 2016-10-27 15:07:10 +01:00
Christoph M. Wintersteiger e4f7ff9881 Added Z3_fpa_is_numeral_negative to FPA API 2016-10-27 15:06:24 +01:00
Nikolaj Bjorner 485372ec2a Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-26 19:15:11 -07:00
Nikolaj Bjorner 4bd83724dd remove conflict on false disequality, introduced regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-26 19:15:05 -07:00
Christoph M. Wintersteiger 23c58a1ef6 Added FPA numeral predicates to ML API 2016-10-26 18:53:20 +01:00
Christoph M. Wintersteiger 903d962a3c Merge branch 'fpa_numeral_accessors' of https://github.com/wintersteiger/z3 into fpa_numeral_accessors 2016-10-26 18:44:49 +01:00
Christoph M. Wintersteiger 935c523ef8 Added FPA numeral predicates to Java API 2016-10-26 18:44:35 +01:00
Christoph M. Wintersteiger c573a7446b Added FPA numeral predicates to .NET API 2016-10-26 18:44:25 +01:00
Christoph M. Wintersteiger bea7bc5e30 Bugfix for bv2fpa_converter. Fixes #767. 2016-10-26 16:32:44 +01:00
Christoph M. Wintersteiger cf93e39666 Fixed FPA unbiased exponent accessors 2016-10-26 15:54:33 +01:00
Christoph M. Wintersteiger e381cef92c Marked .NET Z3Exception as serializable 2016-10-26 15:12:10 +01:00
Christoph M. Wintersteiger ead970b477 Bugfix for Python API. 
Thanks to John D. Ramsdell for reporting this issue (http://stackoverflow.com/questions/39584779/why-is-the-sort-of-a-bound-variable-forced-not-to-be-a-finite-domain-sort).
 2016-10-26 14:08:33 +01:00
Nikolaj Bjorner da4289fadc fix unit tests for pb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-25 20:47:48 -07:00
Nikolaj Bjorner d0c5b86a2a Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-25 20:32:20 -07:00
Nikolaj Bjorner 461e88e34c additional robustness check for incremental sat solver core when it recieves interpreted constants, added PB equality to interface and special handling of equalities to adddress performance gap documented in #755 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-25 20:32:13 -07:00
Christoph M. Wintersteiger c7fddf80c2 fixed unhandled case warning in test/qe_arith.cpp 2016-10-25 14:34:00 +01:00
Christoph M. Wintersteiger 8c5c564d6c fixed initialization order warning in pb2bv_rewriter 2016-10-25 14:31:29 +01:00
Christoph M. Wintersteiger 963dfad10e fix for biased flag on get_numeral_exponent_string 2016-10-25 14:17:23 +01:00
Christoph M. Wintersteiger dc78a04135 removed debug output 2016-10-25 12:20:45 +01:00
Nikolaj Bjorner fefd00aa49 fix sign of constant in pb constraint 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 20:28:56 -07:00
Nikolaj Bjorner b82b53dc34 add handling of pseudo-boolean inequalities that use if-expressions over Booleans and arihmetic instead of built-in PB predicates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 17:41:52 -07:00
Nikolaj Bjorner e4d2c5867a remove dead (and incorrect) code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 15:52:47 -07:00
Nikolaj Bjorner a880e5f49b fix incorrection assertion when checking signs of literals, exposed by miTLS regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 13:12:36 -07:00
Nikolaj Bjorner c68c56b0e7 fix incorrect assertion when checking signs of literals, exposed by mitls regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 13:09:27 -07:00
Nikolaj Bjorner 33e7dccd42 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 09:11:02 -07:00
Nikolaj Bjorner 0439b795b4 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-24 09:10:40 -07:00
Nikolaj Bjorner 99002aeffb Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-24 08:25:19 -07:00
Nikolaj Bjorner 6cf54a226e a more efficient encoding for pseudo-Boolean inequality constraints into bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 08:25:02 -07:00
Christoph M. Wintersteiger 79f1d7b4d4 fixed GCC build issue in tests 2016-10-24 15:27:47 +01:00
Christoph M. Wintersteiger 5fee1ea3c0 removed unused variables 2016-10-24 14:08:33 +01:00
Christoph M. Wintersteiger 7517cf485e ML API bugfixes for FPA numeral accessors 2016-10-24 13:32:37 +01:00
Christoph M. Wintersteiger df2a569d25 Replaced antiquated header with modern equivalent. 2016-10-24 13:29:17 +01:00
Christoph M. Wintersteiger abcb6040d4 Refactored FPA numeral accessors. 2016-10-24 12:53:57 +01:00
Christoph M. Wintersteiger 0a11e8f3c0 Resolved rebase conflicts 2016-10-24 12:53:57 +01:00
Christoph M. Wintersteiger 8926b3311d Fixed FP numeral special value sig/exp extraction functions. 2016-10-24 12:52:07 +01:00
Christoph M. Wintersteiger 89d38385db Added functions to test FP numerals for special values. 2016-10-24 12:50:05 +01:00
Christoph M. Wintersteiger 6b474adc8a Added accessors to extract sign/exponent/significand BV numerals from FP numerals. 2016-10-24 12:50:05 +01:00
Christoph M. Wintersteiger 5716eaafed whitespace 2016-10-24 12:50:05 +01:00
Nikolaj Bjorner 4f3f21bff1 disable local optimization in presence of non-linear constraints, addresses issue #758 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-23 21:45:35 -07:00
Nikolaj Bjorner a1b7e41d7f Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-23 20:53:14 -07:00
Nikolaj Bjorner b92bd89a45 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-23 20:53:10 -07:00
Nikolaj Bjorner b476784f23 add missing file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-23 20:52:44 -07:00
Nikolaj Bjorner 3778048eb4 add bounded-int and pb2bv solvers to fd_solver, use sorting networks for pb2bv rewriter when applicable, hoist to pb2bv_rewriter module and remove it from the pb2bv_tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-23 20:31:59 -07:00
Nikolaj Bjorner 6d3430c689 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-22 21:51:11 -07:00
Nikolaj Bjorner e32e0d460d fix at-most-1 constraint compiler bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-22 21:50:45 -07:00
Nikolaj Bjorner 23b9d3ef55 fix at-most-1 constraint compiler bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-22 18:50:16 -07:00
Murphy Berzish b06b9f9264 str.to-int WIP 2016-10-21 13:35:35 -04:00
Christoph M. Wintersteiger 5bd00d3f83 Bugfixes for the FPA API 2016-10-21 15:39:02 +01:00
Nikolaj Bjorner bb6d826908 use index j to avoid superficial, but typically flagged, name clash with internal index i 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-20 22:17:11 -07:00