mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity
10783 commits 23 branches 48 tags 157 MiB
Commit graph

8929 commits

Author SHA1 Message Date
Nikolaj Bjorner 598fc810b5 adding FP 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-20 15:34:47 +01:00
Nikolaj Bjorner 3548057bd1 fix detection of arithmetic operations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-20 14:00:05 +01:00
Nikolaj Bjorner cc216f8cc3 fix regressions breaking build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-19 21:24:44 +01:00
Nikolaj Bjorner c022d47d60 Merge branch 'master' of https://github.com/z3prover/z3 2019-02-19 18:17:17 +01:00
Nikolaj Bjorner caa15ea04d enable cardinality constraints in nla2bv 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-19 18:17:07 +01:00
Nuno Lopes 61272fdc0c remove a few more inc/dec refs 2019-02-19 13:36:39 +00:00
Nuno Lopes edf0df634d simplifications to refs 2019-02-19 13:18:20 +00:00
Nuno Lopes 8e4ef19f45 fix debug build 2019-02-19 10:54:41 +00:00
Nuno Lopes 8c2584bcf7 eliminate a few ref incs/decs plus remove unused variable 2019-02-19 10:52:12 +00:00
Nikolaj Bjorner 2138a5232f fix #2142 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-19 10:16:50 +01:00
Nikolaj Bjorner 7fb2c6a908 turn off model validation unless specified by parameter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-18 15:55:24 +01:00
Nikolaj Bjorner 0aafa8b7ce optimize binary output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-18 15:52:42 +01:00
Nikolaj Bjorner 5b57c6b780 unused variable warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-17 01:30:26 -08:00
Nikolaj Bjorner 8c085f1a18 removing unused and fixing suspect optimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-16 21:26:29 -08:00
Nikolaj Bjorner ea778eefb2 skip optimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-16 20:58:30 -08:00
Nikolaj Bjorner c1402ad70f tone down verbosity of integrity checking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-16 20:39:15 -08:00
Nikolaj Bjorner 7f51cc7931 fix #2140 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-16 09:54:05 -08:00
Nikolaj Bjorner 4f223542ac fix #2129 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-16 09:38:47 -08:00
Nikolaj Bjorner f84de9400e also deal with initializing boolean variables in smt context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-15 17:58:26 -08:00
Nikolaj Bjorner 39f73fa595 ensure that activity works for sat solver from cold state 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-15 16:56:55 -08:00
Nikolaj Bjorner 89bf2d4368 add API for setting variable activity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-15 12:05:24 -08:00
Nikolaj Bjorner e4c6dcd84c import csp progress 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-14 17:09:18 -08:00
Nikolaj Bjorner 45aa8dd39a remove more references 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-14 17:06:38 -08:00
Nikolaj Bjorner 96c05b0289 remove reference to deprecated code in cmd_context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-14 17:00:02 -08:00
Nikolaj Bjorner 5cdfa7cd1c variations on unit-walk 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-13 17:43:15 -08:00
Nikolaj Bjorner 83f0fd5cc2 Merge branch 'master' of https://github.com/z3prover/z3 2019-02-12 15:49:20 -08:00
Nikolaj Bjorner eec1da5a15 move restart test to after propagation, clean up drat generation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-12 15:49:12 -08:00
Christoph M. Wintersteiger 64d085c188
Fix bug in fpa2bv_converter, fixes #2136. 2019-02-12 14:02:30 +00:00
Nikolaj Bjorner d9a51f8f8a fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-11 14:44:12 -08:00
Nikolaj Bjorner 72b220e84a import improvements to lookahead 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-11 13:28:13 -08:00
Nikolaj Bjorner 6d893e0599 revise unit walk 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-11 13:16:17 -08:00
Nikolaj Bjorner 5fe40a25dc revise local search 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-11 13:14:20 -08:00
Nikolaj Bjorner 22783a4bcb import more from csp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-11 13:09:28 -08:00
Nikolaj Bjorner 93ee05648e add shortcuts for unit assertions, conflicts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-11 10:56:36 -08:00
Nikolaj Bjorner d73b7267e3 Merge branch 'master' of https://github.com/z3prover/z3 2019-02-10 18:11:08 -08:00
Nikolaj Bjorner 6cfe66c3c2 re-enabling model evaluation of as-array after tuning normalization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-10 18:11:01 -08:00
Audrey Dutcher 4e687671a5 Tweak python setup.py clean to properly clean the native build 2019-02-10 14:32:02 -08:00
Audrey Dutcher b702cad81e Append std=c++11 instead of replacing CXXFLAGS; see #2130 2019-02-10 14:12:27 -08:00
Nikolaj Bjorner 81d322b79f fix bug in model compression that skips dependencies in function entries. Exposed in t171.smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-10 11:12:26 -08:00
Nikolaj Bjorner c5df6ce96e fix #2131 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-10 10:07:24 -08:00
Nikolaj Bjorner 24dfdfe9bc disable fixes for #2128 and related as it breaks model evaluation time in regressions, set longer delay for inprocessing in sat solver, report stats 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-09 16:06:02 -08:00
Nikolaj Bjorner c7bd985fac remove asserts for ground defs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-09 08:50:02 -08:00
Nikolaj Bjorner 0fd4c4fb06 tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-09 08:24:14 -08:00
Nikolaj Bjorner d2d42f9810 fix #2127 fix #2128 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-09 08:23:22 -08:00
Nikolaj Bjorner b17c946acb fix bug in hoist module, tune num2bits for large bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-08 14:40:06 -08:00
Nikolaj Bjorner d2a3b53d92 fix remaining incorrect uses of new BoolExpr related to #2125 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-07 12:28:17 -08:00
Nikolaj Bjorner 77942a35dc fix #2125 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-07 11:20:53 -08:00
Nikolaj Bjorner d21fc642b4 refactor watch_diseq, disable it completely 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-07 09:57:24 -08:00
Nikolaj Bjorner 6f9082598c tuning relevancy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-07 08:05:40 -08:00
Nikolaj Bjorner e22f713b19 tune QF_UFBV 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-07 12:02:48 +01:00
Nikolaj Bjorner c9ffe7417c mark destructors virtual 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-07 07:55:17 +01:00
Nikolaj Bjorner 064c9faf11 fix test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-06 20:13:21 +01:00
Nikolaj Bjorner c6a7dc7b44 formatting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-06 20:05:45 +01:00
Nikolaj Bjorner 6c10e27bd5 Merge branch 'master' of https://github.com/z3prover/z3 2019-02-06 19:43:56 +01:00
Nikolaj Bjorner 56598037b6 new rewriter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-06 19:42:40 +01:00
Nikolaj Bjorner d04e72819a abstract solver API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-06 19:42:01 +01:00
Nuno Lopes 904bc34139 remove some debug leftover 2019-02-05 10:02:58 +00:00
Nuno Lopes 73f6806371 rewrite scoped_timer in C++11 way 
the code is much smaller and reused across platforms
I see a small speedup on linux as well
 2019-02-04 17:42:27 +00:00
Nikolaj Bjorner 9cf99e26a6 fix #2123 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-03 19:54:08 +01:00
Nikolaj Bjorner 0acc042bf7 fix #2120 fix #2122 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-03 17:15:38 +01:00
Nikolaj Bjorner 9fde9fe3a2 fix #2122 for code that isn't exception safe 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-02 19:49:16 +01:00
Nikolaj Bjorner a76107e50d fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-01 18:44:52 -08:00
Nikolaj Bjorner 6c464f8aec add assert_and_track to optimize for #2116 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-01 14:59:36 -08:00
Nikolaj Bjorner d1877f58a5 Merge branch 'master' of https://github.com/z3prover/z3 2019-02-01 13:36:02 -08:00
Nikolaj Bjorner e07f0c0284 tune generation of drat files, add helpful binary clause in lookahead simplification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-01 13:35:54 -08:00
Daniel Selsam df73c58195 array resize must m_size 2019-02-01 09:36:03 -08:00
Daniel Selsam cca280ac47 do not echo dimacs while parsing 2019-02-01 09:36:03 -08:00
Nikolaj Bjorner 7fa9768c36 improving drat output perf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-01 09:16:46 -08:00
Nikolaj Bjorner 1e90be62bc fix drat for lookahead, fixes for binary drat format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-31 14:58:51 -08:00
Nikolaj Bjorner cda78d8d0b #2117 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-30 09:34:45 -08:00
Nikolaj Bjorner cb94f82f37 fix #2118 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-30 09:31:05 -08:00
Nikolaj Bjorner e004986e99 fix z3++.h 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-30 09:20:38 -08:00
Nikolaj Bjorner 35eb21bc35 fix extraction of trail 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-30 09:06:41 -08:00
Nikolaj Bjorner 08ce6f7ac1 working on binary drat format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-30 08:54:59 -08:00
Nikolaj Bjorner 8d20310758 adding trail/levels 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-29 14:45:51 -08:00
Nikolaj Bjorner e22c657811 Merge branch 'master' of https://github.com/z3prover/z3 2019-01-29 10:50:28 -08:00
Nikolaj Bjorner 58f5531cff fix #2114 introduced while working on #2095 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-29 08:18:03 -08:00
Nikolaj Bjorner 4f988595c7 fix #2107 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-27 19:45:19 -08:00
Nikolaj Bjorner 94dae2da3a fix fourth bug produced by repros by Mark Dunlop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-27 18:11:18 -08:00
Nikolaj Bjorner d0b2f73c0c change opt.maxlen.enable default to true to prefer this over all other heuristics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-26 13:02:25 -08:00
Nikolaj Bjorner 1297eeb817 fix #2104 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-26 11:55:32 -08:00
Nikolaj Bjorner cf6119cdfd fix #2102 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-25 21:02:25 -08:00
Nikolaj Bjorner e7cabf3e44
Merge pull request #2103 from alcides/master 
Deepcopy works with Python 3.7
 2019-01-25 20:07:40 -08:00
Nikolaj Bjorner 121211a51c maxlexN 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-25 20:01:38 -08:00
Nikolaj Bjorner 1ed68906fa fix debug assertion code, make maxlex optional 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-25 08:23:41 -08:00
Alcides Fonseca 83717a9c86 Merge branch 'master' of https://github.com/Z3Prover/z3 2019-01-25 14:45:22 +00:00
Alcides Fonseca a785ffe0ba Updated deepcopy to the latest Python API 2019-01-25 14:42:22 +00:00
Nikolaj Bjorner d3d392da41 adding maxlex, delay mk_true() calls in goal2sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 21:36:40 -08:00
Nikolaj Bjorner b4f4a1f316 adding maxlex, throttle use of asymmetric literal addition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 19:47:50 -08:00
Nikolaj Bjorner ad81fee118 adding maxlex, throttle use of asymmetric literal addition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 19:26:44 -08:00
Nikolaj Bjorner 8da1d6070b throttle big-reductions #2101 #2098 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 14:00:56 -08:00
Nikolaj Bjorner 498864c582 adding dump facility for cancelation #2095, easing dimacs in/out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 12:21:23 -08:00
Nikolaj Bjorner f7746e2284 address perf #2098 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-23 16:58:00 -08:00
Nikolaj Bjorner 9c07167ff8 add new pyg file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-23 16:06:44 -08:00
Nikolaj Bjorner 8e5c1fcfd1 make context_solve configurable and exposed as top-level tactic parameter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-23 16:06:25 -08:00
Nikolaj Bjorner 412eee0dac throttle number of rounds of ba simplification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-22 18:12:39 -08:00
Nikolaj Bjorner f9195c77a7 remove not-handled clause from mod with non-numerals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-22 09:46:04 -08:00
Nikolaj Bjorner 49a51a0757 fix #2096, introduced when fixing #2082 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-22 07:06:40 -08:00
Nikolaj Bjorner 6bd87f837a fix Boolean argument 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 14:14:26 -08:00
Nikolaj Bjorner 8566d88b99 remove validation assert 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 12:49:04 -08:00
Nikolaj Bjorner 785fe2f6f7 add main remaining updates from #1815 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 12:43:05 -08:00
Nikolaj Bjorner 5cdbb1f7be this is still used 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 11:25:34 -08:00
Nikolaj Bjorner 9dd41ba554 remove offending assert, disable assembly-info for dotnet core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 11:13:03 -08:00
Nikolaj Bjorner cabe0ee447 integrating additional changes from @yatli pull request #1815 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-20 10:51:44 -08:00
Nikolaj Bjorner 1efbc25b3b Merge branch 'master' of https://github.com/z3prover/z3 2019-01-18 18:09:22 -08:00
Nikolaj Bjorner 0b7021d2c8 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-18 18:09:19 -08:00
Nikolaj Bjorner c45ab6efed add setting to dump intermediary models #2087 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-18 15:12:08 -08:00
Nikolaj Bjorner 947fe2ff9c fix datatype occurs check bug reported by Gerhard Schellhorn 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-17 16:35:07 -08:00
Nikolaj Bjorner 442e47dfce fix datatype occurs check bug reported by Gerhard Schellhorn 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-17 16:34:26 -08:00
Nikolaj Bjorner f2e636c598 record simplified input clauses as lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-16 16:37:21 -08:00
Nikolaj Bjorner 247980c5a2 don't assign already assigned literals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-16 11:41:32 -08:00
Nikolaj Bjorner 038971c029
Revert "api: dotnet: switch to multi-targeting project and modern cmake-dotnet integration." 2019-01-16 10:21:56 -08:00
Nikolaj Bjorner 16c15d53a9
Merge pull request #1815 from yatli/master 
api: dotnet: switch to multi-targeting project and modern cmake-dotnet integration.
 2019-01-16 10:16:26 -08:00
Nikolaj Bjorner e01a668da0 coordinate drat with clause removal 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-16 02:29:33 -08:00
Nikolaj Bjorner b33f5f879e fix another bug reported by Mark Dunlop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-15 17:57:11 -08:00
Nikolaj Bjorner 3298486136 don't reach max conflicts if state is inconsistent 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-15 08:40:38 -08:00
Nikolaj Bjorner 5328454c77 const 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-15 08:37:23 -08:00
Nikolaj Bjorner 161c83795f remember inconsistent states when cloning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-15 08:34:55 -08:00
Nikolaj Bjorner 65bd427e46 neatify statistics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 16:48:48 -08:00
Nikolaj Bjorner f238460597 neatify statistics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 16:45:04 -08:00
Nikolaj Bjorner ed7cac8cc0 neatify logging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 16:42:13 -08:00
nilsbecker 279413412d preventing operations during MBQI search from being logged 2019-01-15 01:09:44 +01:00
Nikolaj Bjorner b11ec3bfbf merge sat_tactic from csp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 15:17:42 -08:00
Nikolaj Bjorner ee07008fb9 import files from csp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 15:04:46 -08:00
Nikolaj Bjorner 54a125063b remove produce interpolants 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 15:00:25 -08:00
Nikolaj Bjorner e954f59052 ensure that solver objects have timeout/rlimit/ctrl-c exposed as possible parameters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 13:50:17 -08:00
nilsbecker bfb554c0b8 logging sorts of quantified variables 
logging proof objects seperately form regular terms
renaming inst-possible -> inst-discovered
 2019-01-14 21:28:06 +01:00
Nikolaj Bjorner a686aa7f56 produce binary clauses for DRAT for units produced by probing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 10:56:10 -08:00
Yatao Li 43ee345f01 dotnet deps hack for test 2019-01-15 03:06:36 +09:00
Nikolaj Bjorner 0b84c60886 fix another bug uncovered by Dunlop, prepare grounds for equality solving within NNFs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 01:25:25 -08:00
Nikolaj Bjorner eaa80d5b02 fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-13 11:33:23 -08:00
Yatao Li 8ebde41f35 dotnet: example: copy to binary dir before build 2019-01-13 22:45:05 +08:00
Nikolaj Bjorner 46bfcbd4f8 fix #2082 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-13 03:46:11 -08:00
Nikolaj Bjorner 4159b987ce purge unused code from theory_pb, fix bug reported by Mark Dunlop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-13 03:23:57 -08:00
Nikolaj Bjorner 4b35ef29c9 fix #2081 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-13 01:18:03 -08:00
Nikolaj Bjorner dc5e4ca1c5 fix drat generation in asymmetric branch simplification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-12 13:19:09 -08:00
Nikolaj Bjorner f835a3c2b2 revert assumption tracking choice in unit literals inferred from binary clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-12 11:08:35 -08:00
Nikolaj Bjorner e4d6aa07dc use vectors instead of hash-tables in dimacs serialization to avoid hash-table contention 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-12 11:05:00 -08:00
Yatao Li 5e79dba3d6 dotnet: move example project build to cmake 2019-01-13 00:03:37 +08:00
Yatao Li 55f92f3658 dotnet: remove stale packages before pack; relay cmake config generator expression into msbuild property.. 2019-01-12 21:33:09 +08:00
Yatao Li 4b3189f3e2 dotnet: identifies arch-specific native libraries 2019-01-12 20:04:44 +08:00
Yatao Li e5f65263bb dotnet: reigster local repo for nupkg 2019-01-12 19:22:38 +08:00
Yatao Li 53eaab4709 dotnet: update build scripts 2019-01-12 17:38:24 +08:00
Nikolaj Bjorner e623f1e9c9 restoring clause sizes after deletion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-12 01:01:49 -08:00
Nikolaj Bjorner 3c96b51e97 lvl -> _lvl 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-12 00:40:36 -08:00
Nikolaj Bjorner 0b8dbf2854 fixing drat proofs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-12 00:30:21 -08:00
Nikolaj Bjorner 836f156d54 fix drat for units learned from binary clause resolution 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-12 00:12:20 -08:00
Yatao Li 17596fcc17 Merge remote-tracking branch 'upstream/master' 2019-01-12 15:01:28 +08:00
Yatao Li ffd26e5a56 .net: remove net35 related build props; drop src/api/dotnet/core 2019-01-12 15:01:05 +08:00
Nikolaj Bjorner 63d480fd92 fix cnf check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-11 21:17:39 -08:00
Nikolaj Bjorner b8d18c6c6d speed-up handling of cnf input to inc_sat_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-11 20:52:19 -08:00
Nikolaj Bjorner 9bd4050e0c use ref-vector for shared occurrences to avoid hash-table overhead 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-11 13:43:39 -08:00
Nikolaj Bjorner f8f3549c1c Merge branch 'master' of https://github.com/z3prover/z3 2019-01-11 10:13:14 -08:00
Nikolaj Bjorner 1a4636518c Merge branch 'master' of https://github.com/z3prover/z3 2019-01-11 04:58:47 -08:00
Nikolaj Bjorner f1c3e1aa77 fix #2077 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-11 04:58:40 -08:00
Nikolaj Bjorner 434eb25004 add useful div lemma for case #2079 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-10 17:20:01 -08:00
Nikolaj Bjorner 6e60926cc3 fix drat output for elim_eqs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-10 15:25:10 -08:00
Nikolaj Bjorner b12c1b1cba set a throttle on ala 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-10 13:38:45 -08:00
Nikolaj Bjorner 7fc349b622 Merge branch 'master' of https://github.com/z3prover/z3 2019-01-10 12:08:44 -08:00
Nikolaj Bjorner 59b0b56b42 add checkpoints to blocked clause elimination to handle timeouts, #2080 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-10 12:08:38 -08:00
Nikolaj Bjorner 1e4662e0bc
Merge pull request #2073 from waywardmonkeys/emscripten-no-debug 
Define NO_Z3_DEBUGGER for emscripten builds.
 2019-01-10 11:39:19 -08:00
Nikolaj Bjorner efaab6d8fd have sat cleaner use a fixed-point 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-10 11:38:35 -08:00
Nikolaj Bjorner 9c318ed304 fix #2076, add option to handle .cnf files into dimacs parser 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-09 15:43:45 -08:00
nilsbecker 3620dfee5e logging names of quantified variables and updating inst-possible line 2019-01-08 22:09:32 +01:00
Nikolaj Bjorner b63a0e31d3 fix regression from #2061 breaking #2074 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-07 16:30:04 -08:00
Nikolaj Bjorner 14f3ff0b63 Merge branch 'master' of https://github.com/z3prover/z3 2019-01-07 09:00:21 -08:00
Nikolaj Bjorner cec34c745a defer blocking propagation until all properties of literal have been axiomatized. Deals with seq part of #2071 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-07 09:00:11 -08:00
Bruce Mitchener d757c342d5 Define NO_Z3_DEBUGGER for emscripten builds. 2019-01-07 23:13:09 +07:00
Nikolaj Bjorner bde4ddd861 Merge branch 'master' of https://github.com/z3prover/z3 2019-01-06 20:20:55 -08:00
Nikolaj Bjorner 6113149138 fix #2060. Code comment was right, code wasn't. Code comment and code could also be tuned 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-06 20:20:34 -08:00
Nikolaj Bjorner 2486971094
Merge pull request #2065 from waywardmonkeys/improve-ios-support 
Define NO_Z3_DEBUGGER for iOS builds.
 2019-01-06 18:56:03 -08:00
Nikolaj Bjorner 8ad2f70aaa
Merge pull request #2066 from waywardmonkeys/const-str-hashtable 
Let str_hashtable store `const char*`.
 2019-01-06 18:55:32 -08:00
Nikolaj Bjorner ea48d0a95a add set method to iterator, #2068, a set method to the vector template was also added 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-06 18:55:00 -08:00
Nikolaj Bjorner a87f7a14d3 ever so gentle slap over the fingers for not using real regular expressions, #2058 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-06 13:46:04 -08:00
Nikolaj Bjorner 71e239c08e fix #2061 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-06 11:49:47 -08:00
Bruce Mitchener 7e1ce2a16c Define NO_Z3_DEBUGGER for iOS builds. 
This is defined because we can't call `system` (via `invoke_gdb`)
on iOS and related platforms.
 2019-01-06 12:16:33 +07:00
Bruce Mitchener a06bc49710 Let str_hashtable store const char*. 
This removes some boilerplate const casting.
 2019-01-06 12:15:31 +07:00
nilsbecker 58def55796 mbqi support 2019-01-05 14:44:06 +01:00
Nikolaj Bjorner fb397cbe25 remove incorrect assertion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-04 08:18:40 -08:00
Nikolaj Bjorner 0d400a5ad6 fix bit2bool bug reported by Jianying Li 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-04 07:46:53 -08:00
Nikolaj Bjorner b533ba39d6 use private rewriter to avoid surprises 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-29 17:13:32 +08:00
Nikolaj Bjorner 815faa96d9 remove dotnet35 support 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-29 16:44:03 +08:00
Yatao Li b72cb96ee3 update dotnet cmake module 2018-12-29 16:43:08 +08:00
Yatao Li f5b874e0a3 Merge branch 'master' of https://github.com/Z3Prover/z3 2018-12-29 16:27:00 +08:00
Nikolaj Bjorner f8a3300026 introduce proxies to differentiate from arithmetical variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-29 11:13:15 +08:00
Nikolaj Bjorner e40884725b remove unused euf-mbi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-28 19:47:48 +08:00
Nikolaj Bjorner 64103038a7 simplify 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-28 12:20:53 +08:00
Nikolaj Bjorner 0628711c4a simplify 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-28 12:18:29 +08:00
Nikolaj Bjorner 6a2d54b31e cleanup and doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-28 11:59:17 +08:00
Nikolaj Bjorner da95fd7d83 fixing get-arith-vars and extraction of private variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-28 11:23:52 +08:00
Nikolaj Bjorner 2cc3918027 Merge branch 'master' of https://github.com/z3prover/z3 2018-12-28 09:38:31 +08:00
Nikolaj Bjorner 8829fa96de change projection function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-28 09:38:17 +08:00
Nikolaj Bjorner d879e2732a
Merge pull request #2050 from waywardmonkeys/allow-disabling-invoking-debugger 
If NO_Z3_DEBUGGER, also drop defining invoke_gdb.
 2018-12-27 17:23:31 -08:00
Bruce Mitchener 877df0f1cc If NO_Z3_DEBUGGER, also drop defining invoke_gdb. 2018-12-27 09:21:45 -05:00
Nikolaj Bjorner 8b3abe120c Merge branch 'master' of https://github.com/z3prover/z3 2018-12-26 21:04:44 +08:00
Nikolaj Bjorner 076cfa5813 working on revising project0 to project 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-26 21:04:35 +08:00
Bruce Mitchener 44bc00f13d Fix typos. 2018-12-23 21:58:57 -05:00
Nikolaj Bjorner 9379ec3a68 add back pre_visit, which does get called from rewriter_def/rewriter.h 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-21 18:52:09 -08:00
Nikolaj Bjorner 99cc4747c5 fixing #1971 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-21 17:21:04 -08:00
Nikolaj Bjorner 95db37d105 Merge branch 'master' of https://github.com/z3prover/z3 2018-12-21 17:10:41 -08:00
Nikolaj Bjorner b0b6394c6c fixing #1971 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-21 17:10:37 -08:00
Nuno Lopes 3104291b80 spread a few anonymous namespaces and remove some m_imp idioms 2018-12-21 23:02:15 +00:00
Nuno Lopes 178e5b31e8 spread a few anonymous namespaces and remove some m_imp idioms 2018-12-21 22:49:06 +00:00
Nuno Lopes 52f960a7c8 elim_uncnstr_tactic: remove m_imp idiom to reduce mem alloc 2018-12-21 19:48:18 +00:00
Nikolaj Bjorner a63d1b1848 update doctest 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-18 11:57:20 -08:00
Nikolaj Bjorner 35e8decdb1 for #2039 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-18 11:27:04 -08:00
Nikolaj Bjorner b6bf299b8b update upolynmial test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-17 17:41:50 -08:00
Nikolaj Bjorner 360d6f963e reduce output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-17 17:05:48 -08:00
Nikolaj Bjorner bd96eaff47 axiomatize pb-eq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-17 08:26:59 -08:00
Nikolaj Bjorner f4d03edf22 remove unreachable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-16 15:54:30 -08:00
Nikolaj Bjorner 2dcf36e96c fix #2044 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-16 15:32:38 -08:00
Nikolaj Bjorner 82a89120b0 fix #2042 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-16 15:26:40 -08:00
Nikolaj Bjorner f56749a241 fix #2041, fix #2043 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-16 15:18:49 -08:00
Nikolaj Bjorner 58b9fc437d add sin/cos axiom regardless of whether sin/cos can be eliminated. fix #2037 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-13 16:09:08 -06:00
Nikolaj Bjorner db3e5ce070
Merge pull request #1997 from waywardmonkeys/change-64-bit-configuration-strategy 
Change how 64 bit builds are detected.
 2018-12-12 09:55:13 -08:00
Nikolaj Bjorner b3d0ed6143 fix #2035 regression. correct axiom is |extract(s,i,l)| <= l or l < 0, but it is subsumed by encoding of extract, so new axiom is not useful 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-11 20:27:28 -08:00
Nikolaj Bjorner c1b03e8ca6 Merge branch 'master' of https://github.com/z3prover/z3 2018-12-11 09:38:44 -08:00
Nikolaj Bjorner bfcea7a819 perf improvements by reordering variable branching #1676 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-11 09:38:36 -08:00
Nikolaj Bjorner 271e86020a Merge branch 'master' of https://github.com/z3prover/z3 2018-12-11 09:35:34 -08:00
Nikolaj Bjorner 045fef35ed fix build break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-11 09:35:27 -08:00
Nikolaj Bjorner 021c5315a7
Merge pull request #2034 from Bronsa/patch-1 
Change error message from "internal failure" to "Object allocation failed"
 2018-12-11 09:32:32 -08:00
Nikolaj Bjorner a3f9e3168d simplify ~context #1948 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-11 09:29:59 -08:00
Nikolaj Bjorner 796689f708 #1948 remove memory allocation in nlsat::solver::~solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-11 09:08:53 -08:00
Nicola Mometto 06fc94818f
Change error message from "internal failure" to "Object allocation failed" 
For consistency with ad49c3269a and Java/dotNet APIs
 2018-12-11 12:09:22 +00:00
Nikolaj Bjorner da5486563d Merge branch 'master' of https://github.com/z3prover/z3 2018-12-10 18:38:15 -08:00
Nikolaj Bjorner 092c25d596 fix #2007 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-10 18:37:30 -08:00
Nikolaj Bjorner b40c2b2926 fix #876 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-10 14:11:00 -08:00
nilsbecker 6d2cf4f464 smt-like logging of theory specific meaning of constants 2018-12-10 22:49:08 +01:00
Nikolaj Bjorner 68ace83893 remove enable trace 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-10 07:34:56 -08:00
Nikolaj Bjorner f2a7bcaf5d remove prints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-09 14:38:45 -08:00
Nikolaj Bjorner bb69aa88fb Merge branch 'master' of https://github.com/z3prover/z3 2018-12-09 12:56:26 -08:00
Nikolaj Bjorner 604e5dd0bb fixing #2030 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-09 12:56:21 -08:00
Bruce Mitchener 1b91694d9b Enable dl_table tests on non-Windows/Cygwin. 2018-12-09 21:02:06 +07:00
Bruce Mitchener 51a947b73d Change how 64 bit builds are detected. 
Instead of doing this at configure time, we look at the actual
compile time status. This also avoids hardcoding checks based on
what CPU architecture is present, which doesn't work when Z3 is
being built on non-x86_64 platforms.
 2018-12-09 16:16:20 +07:00
Nikolaj Bjorner 559f57470e fix #2031 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-09 08:21:48 +01:00
Nikolaj Bjorner 2ca83d0095 Merge branch 'master' of https://github.com/z3prover/z3 2018-12-08 15:42:13 +01:00
Nikolaj Bjorner 38b5e6de56 fix #2019 - insufficient axioms for special cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-08 13:57:35 +01:00
Nikolaj Bjorner a20e68facc throttel extract/ite rewriting to avoid perf-bug exposed in example from Lucas Cordeiro and Alessandro Trindade 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-07 17:54:49 +00:00
Bruce Mitchener 0231bc44bc Simplify boolean code. 
Now that the C API is using bool, this can be simplified.
 2018-12-07 22:06:51 +07:00
Sebastian Buchwald 5690dbcbfd Fix enum type of case labels 2018-12-06 00:08:29 +01:00
Nikolaj Bjorner f2c263001c
Merge pull request #2020 from waywardmonkeys/fix-typos 
Fix typos.
 2018-12-05 13:16:23 -08:00
Bruce Mitchener 4bc1b0b8c8 Fix typos. 2018-12-05 21:07:34 +07:00
Nikolaj Bjorner 9635ddd8fc fix #2018 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-05 00:54:10 -08:00
Nikolaj Bjorner dc77579707 delta faction to control double lookahead eagerness 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-04 23:41:03 -08:00
Nikolaj Bjorner 3b54575340
Revert "Use nullptr, not 0 in the C++ API impl." 2018-12-04 12:06:44 -08:00
Nikolaj Bjorner 0223846b4f
Merge pull request #2015 from waywardmonkeys/c++-api-use-nullptr 
Use nullptr, not 0 in the C++ API impl.
 2018-12-04 10:18:23 -08:00
Nikolaj Bjorner 7aaacbfc62
Merge pull request #2014 from waywardmonkeys/simplify-boolean-returns 
Simplify some boolean returns.
 2018-12-04 10:17:53 -08:00
Nikolaj Bjorner 4b94ea112d
Merge pull request #2013 from waywardmonkeys/remove-get-manager 
Remove Z3_get_manager.
 2018-12-04 10:17:29 -08:00
Nikolaj Bjorner 3551d12168
Merge pull request #2011 from waywardmonkeys/missing-Z3_API 
Z3_fixedpoint_add_constraint: decl missing Z3_API.
 2018-12-04 10:17:12 -08:00
Nikolaj Bjorner 2372d1bdeb
Merge pull request #2012 from waywardmonkeys/doc-fixups 
Fix up more documentation formatting.
 2018-12-04 10:16:27 -08:00