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

13015 commits

Author SHA1 Message Date
Graydon Hoare 957d7bfe35
Adjust imports so z3.z3 is still available in python3 (#5079) 2021-03-04 17:18:39 -08:00
Nikolaj Bjorner 38737db802 fixes and more porting seq_eq_solver to self-contained module 2021-03-04 16:23:22 -08:00
Nikolaj Bjorner 847724fb21 added rewrite for itos 2021-03-04 10:47:47 -08:00
Nikolaj Bjorner e398959732 move eq solver functionality to common place, fixes to goal2sat 2021-03-04 07:57:31 -08:00
Nikolaj Bjorner cf3002c293 fix #5071 2021-03-03 23:13:56 -08:00
Nikolaj Bjorner 79ababb00a force push 2021-03-03 11:38:33 -08:00
Nikolaj Bjorner 69070a7486 align translation cache with scopes and variable elimination 2021-03-03 11:22:17 -08:00
Nikolaj Bjorner 11efe33aa0 fix #5061 2021-03-03 11:19:03 -08:00
Nikolaj Bjorner 8c66691e6d disable propagation in proof mode as it produces ill-formed proof objects. Fixes #5063 2021-03-03 09:51:56 -08:00
Nikolaj Bjorner bef6f1a729 fix build 2021-03-02 13:51:58 -08:00
Nikolaj Bjorner a66362a933 missing new files 2021-03-02 13:00:17 -08:00
Nikolaj Bjorner 0ce1c34d81 fix #5065 - regression solving str.from_int equations now that it isn't injective any longer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-02 12:59:48 -08:00
Nuno Lopes 4c9fed21e2
increase starting size of ast's hash table to 512k entries (instead of 8) (#5040) 2021-03-02 11:45:07 -08:00
Nikolaj Bjorner 56478f917b enable sat.euf in opt, enable smt legacy for lns 2021-03-02 06:21:20 -08:00
Nuno Lopes db04ccb137 scoped_timer: skip extra unneded heap allocation 2021-03-01 14:36:22 +00:00
Nuno Lopes fc558d3946 fix #5059: exit straight away on hard timeout 
dont run atexit handlers as its not safe to do so with multiple threads
code might be inside malloc, for example, and glibc tries to cleanup its heap
state with an atexit handler
 2021-03-01 14:34:41 +00:00
Nikolaj Bjorner 484c83e6c0 revert enum split for legacy solver 2021-03-01 04:13:17 -08:00
Nuno Lopes ff1429413d Z3_subst: avoid unneded cache lookups 2021-03-01 11:14:24 +00:00
Nikolaj Bjorner f725989225 optimize for enumeration datatypes 2021-02-28 21:31:21 -08:00
Nikolaj Bjorner caae0ba569 rename statistics to pb 2021-02-28 21:31:21 -08:00
Nuno Lopes 5b24396ecd Z3_subst: add fast path for quantifier subst 
when replace patterns are ground
 2021-02-28 23:09:52 +00:00
Nikolaj Bjorner 026065ff71 streamline pb solver interface and naming after removal of xor 2021-02-28 12:32:04 -08:00
Nikolaj Bjorner 13f05ae9dc enable wcnf output for weighted maxsat problems 2021-02-28 09:59:36 -08:00
Nikolaj Bjorner b02cba6106 rename propagation to explain 2021-02-27 17:25:11 -08:00
Nikolaj Bjorner fb8e2e444e remove xor solver, tune dt_solver for enumeration case 2021-02-27 17:17:39 -08:00
Nikolaj Bjorner 830f314a3f fixes to dt_solver and related 2021-02-27 11:03:20 -08:00
Nikolaj Bjorner f7b1469462 Try freeing context in dispose method and not wait for finalizer #5043 2021-02-27 11:02:58 -08:00
Nikolaj Bjorner c6eb55537a Throttle nra solver when progress is being made by linearization 2021-02-26 11:14:24 -08:00
Nikolaj Bjorner 08f55f9d1f start wcnf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-26 11:13:44 -08:00
Nikolaj Bjorner be68456c06 java compilation? 2021-02-26 05:04:46 -08:00
Nikolaj Bjorner 06caf57a86 fix #5033 2021-02-26 03:42:13 -08:00
Nikolaj Bjorner 5c47f244e9 fix #5047 2021-02-26 03:37:14 -08:00
Nikolaj Bjorner ea1089e980 fix #4938 2021-02-26 02:06:28 -08:00
Murphy Berzish 56e4ee3273
z3str3: use assert_axiom_rw more consistently (#5055) 2021-02-25 19:50:18 -06:00
Nikolaj Bjorner 64ba0b631a fixes to seq solver 2021-02-25 10:35:14 -08:00
Nikolaj Bjorner 080c9c6893 fixes to dt solver 2021-02-25 10:35:02 -08:00
Nikolaj Bjorner 04edfc9fdb out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-23 18:14:20 -08:00
Nikolaj Bjorner 377d060036 move to separate axiom management 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-23 18:09:45 -08:00
Murphy Berzish 9bde93f812
z3str3: check whether rewritten axioms rewrite to TRUE (#5039) 2021-02-23 10:36:14 -06:00
Murphy Berzish 5599387a34
z3str3: add str.is_digit support (#5038) 2021-02-23 10:36:01 -06:00
Nikolaj Bjorner c3b7fa941a fix #5048 2021-02-22 10:56:19 -08:00
Nikolaj Bjorner d9fb40602e use theory agnostic axioms in more cases 2021-02-21 18:36:53 -08:00
Nuno Lopes 977082e2bd travis: disable LTO build; its just too slow 2021-02-21 20:18:48 +00:00
Nuno Lopes 4a3d63f9e4 NNF: dont allocate act_cache separately 2021-02-21 16:34:28 +00:00
Nuno Lopes 7b6eff6967 fix user-after-free in smt_ctx test 2021-02-20 16:20:32 +00:00
Nuno Lopes e773e1e78d fix a few more warnings 2021-02-19 12:16:05 +00:00
Nuno Lopes d6ce9cce95 fix clang warnings 2021-02-19 10:59:22 +00:00
Nuno Lopes 5e034e495f fix compiler warnings 2021-02-19 10:33:41 +00:00
Nikolaj Bjorner a22fb8a96e revert unit propagation of equality literals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-18 23:11:03 -08:00
Nikolaj Bjorner 27584d68db more rewrite rules 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-18 22:14:53 -08:00
Nikolaj Bjorner b2eb248bad fixes, fix #5034 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-18 16:47:44 -08:00
Nikolaj Bjorner 180015a529 fix #5035 2021-02-18 16:47:36 -08:00
Murphy Berzish 27db97c269
Z3str3: add str.to_code and str.from_code (#5015) 2021-02-18 16:51:34 -06:00
Nikolaj Bjorner ca9fcbd1df na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-18 13:46:59 -08:00
Nikolaj Bjorner 00dab30ea0 remove binary_function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-18 13:18:58 -08:00
Nikolaj Bjorner 9ae3339c33 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-18 12:33:17 -08:00
Nuno Lopes 14de590566 fix MSVC build 2021-02-18 19:05:20 +00:00
Nuno Lopes d396d46bd1 let's test if all the buildbots are happy with C++17 
it's stil a bit too early for C++20
 2021-02-18 18:13:10 +00:00
Nikolaj Bjorner e63dc7efc2 more rewrite rules 2021-02-17 17:32:00 -08:00
Nuno Lopes bcad4d9435 revert my mess with the ast hashtable 
will share results form the experiments later
 2021-02-17 14:29:07 +00:00
Nikolaj Bjorner 4f9117a921 Move seq axioms to theory independent module 2021-02-16 05:13:52 -08:00
Nikolaj Bjorner 823830181b butterfly effect with relevancy marking 
bail out of infinite instantiation loop
 2021-02-15 16:37:23 -08:00
Nikolaj Bjorner a6dce246f6 fix #5031 2021-02-15 14:36:01 -08:00
Nikolaj Bjorner 96e7b811f9 fix #5029 2021-02-15 14:17:05 -08:00
Nikolaj Bjorner c387863da1 fix #5032, reset substitution during fold transformation 2021-02-15 14:14:25 -08:00
Nikolaj Bjorner 6bd02e122b parse according to http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-15 09:32:31 -08:00
Nikolaj Bjorner 1da7522893 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-14 17:47:19 -08:00
Nikolaj Bjorner 70b4822571 patch seq theory using purification to avoid unsoundness caused by interaction with canonization and rewriting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-14 17:41:06 -08:00
Nuno Lopes 2db2767e7a remove unused method 
in preparation for a bigger storm :)
 2021-02-14 23:31:24 +00:00
Nikolaj Bjorner eac69c5504 incorrect axiomatization 
Fixes repro in https://github.com/Z3Prover/z3/issues/4866#issuecomment-778706682
 2021-02-14 15:29:10 -08:00
Nikolaj Bjorner 45af1bd243 fix build, move seq_skolem 2021-02-14 14:40:29 -08:00
Nikolaj Bjorner 083d09aa81 fix #5016 2021-02-14 13:52:10 -08:00
Nikolaj Bjorner 04a1d4245c fix #4801 2021-02-12 20:20:00 -08:00
Nikolaj Bjorner 83f4a006c6 wreckfun 2021-02-12 19:46:47 -08:00
Nikolaj Bjorner 612cc5cfba fix #5014 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-12 16:01:33 -08:00
Nikolaj Bjorner 4991c6c2c6 fix #5002 
Avoid code path that uses qe_tactic as it isn't protected against parameter abuse
 2021-02-12 13:20:51 -08:00
Nikolaj Bjorner 998cf4c726 fix #5020 
comparison for strict neighbor relation seemed reversed.
Alas, this could introduce additional regressions
 2021-02-12 12:24:27 -08:00
Nikolaj Bjorner c808f74591 fix multiplier base for #5022 
add also some C++ API shorthands for retrieving numerals
 2021-02-12 11:53:40 -08:00
Nikolaj Bjorner 1d12b72bbc log classificaiton 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-11 14:43:05 -08:00
Nikolaj Bjorner 25f53c0467 deal with warnings reported in https://launchpadlibrarian.net/522361319/buildlog_ubuntu-groovy-s390x.z3_4.8.10-1ubuntu4ppa1_BUILDING.txt.gz 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-11 13:49:47 -08:00
Nikolaj Bjorner 2e648e2f02 glibc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-11 13:19:23 -08:00
Nikolaj Bjorner 98eae28fca try to update setup.py to libc naming 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-11 11:52:05 -08:00
Nikolaj Bjorner 5d46ac0aca is glibc the new centos? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-11 11:14:39 -08:00
Nikolaj Bjorner 53e98a27db adding stubs 2021-02-11 09:36:47 -08:00
Nikolaj Bjorner 4c3c15c015 Propagate reason for undef as exception to improve error reporting in scenarios such as #5009 2021-02-09 16:58:01 -08:00
Nikolaj Bjorner 5c04b9eee2 fix #5012 
teething stage for from/to code axiomatization
 2021-02-09 16:38:03 -08:00
Nikolaj Bjorner 692f159af8 try without format 2021-02-09 12:49:55 -08:00
Nikolaj Bjorner e722589810 address some of the ugliness pointed out by abandoned pull request #5008 2021-02-09 11:23:16 -08:00
Nikolaj Bjorner 8b5094fe73 provide additional diagnostics for #5009 2021-02-09 10:14:38 -08:00
Nikolaj Bjorner 8ca2de41db turn on from/to code handling #5007 samples 2021-02-09 10:00:08 -08:00
Nikolaj Bjorner cbb570051c #5007 - wrong recognizer function definitions 2021-02-09 09:54:24 -08:00
Nikolaj Bjorner 55cb12e233 build fix 2021-02-08 16:53:30 -08:00
Nikolaj Bjorner a152bb1e80 remove template Context dependency in every trail object 2021-02-08 15:41:57 -08:00
Nikolaj Bjorner df0a449f70 fix some build warnings exposed in #5005 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-08 10:58:42 -08:00
Nikolaj Bjorner b56372fe76 fix some build warnings exposed in #5005 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-08 10:57:50 -08:00
Nikolaj Bjorner 8fffc03263 remove bv dependencies 2021-02-08 10:57:50 -08:00
Nikolaj Bjorner 0f29fff836 remove bit-vector dependencies in seq theory 2021-02-08 10:57:50 -08:00
Nikolaj Bjorner 43d1ef2fee iterable is a Python 3 thingy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-07 18:22:57 -08:00
Nuno Lopes 52e67b0d3e
switch expr_safe_replace to std::unordered_map (#5003) 
* switch expr_safe_replace to std::unordered_map

* further tweaks to expr_safe_replace for an overall speedup of 1.x in Z3_substitute
 2021-02-07 18:20:48 -08:00
Nuno Lopes 615cafe39b remove unneded pragma once 2021-02-07 12:54:17 +00:00
Nuno Lopes 682b947ad3 the documentation of Z3_model_get_func_interp() says it returns NULL if there's no interpretation 
so let's honour that instead of throwing an exception
 2021-02-07 12:46:36 +00:00
Nuno Lopes e1572096ca delete some dead code 2021-02-07 12:14:52 +00:00
Julius Marozas 01d5f3259c
Fix show parameter in prove, solve, and solve_using (#5001) 
* Fix show parameter in prove function

* Fix show in solve & solve_using

* Use Python 2 compatible syntax

* Add default value for show
 2021-02-06 16:42:15 -08:00
Nikolaj Bjorner e856cfc458 coercions 2021-02-06 10:35:28 -08:00
Nikolaj Bjorner 16448104eb add new model event handler for incremental optimization 2021-02-05 17:11:04 -08:00
Nikolaj Bjorner 2c472aaa10 #4999 
use typing Iterable
 2021-02-05 12:09:24 -08:00
Nikolaj Bjorner a582014854 #4999 2021-02-05 12:01:30 -08:00
Nikolaj Bjorner 0a9ee6c640 build break 2021-02-04 16:58:32 -08:00
Malte Mues 5d8d42b1fa
Update the mkConstant parameter type (#4996) 2021-02-04 16:17:49 -08:00
Nikolaj Bjorner 0ec567fe15 integrate v2 of lns 2021-02-04 15:47:40 -08:00
Nikolaj Bjorner dfb7c87448 #4997 2021-02-04 15:46:34 -08:00
Nikolaj Bjorner cc39cf037e build again 2021-02-04 12:36:44 -08:00
Nikolaj Bjorner b3144a534d remove string conversion causing regression 2021-02-03 21:40:45 -08:00
Nikolaj Bjorner abcabba9fe fix python build 2021-02-03 09:57:16 -08:00
Nikolaj Bjorner fb1509d011 expose internal API for set_phase 2021-02-02 14:29:06 -08:00
Nikolaj Bjorner 8f577d3943 remove ast_manager get_sort method entirely 2021-02-02 13:57:01 -08:00
Nikolaj Bjorner 489df0760f experiments with LNS 2021-02-02 13:03:54 -08:00
Nikolaj Bjorner 4ad95939b6 fix build 2021-02-02 06:40:31 -08:00
Nikolaj Bjorner cc001ad682 fix regression 2021-02-02 06:16:06 -08:00
Nikolaj Bjorner 937b61fc88 fix build, refactor 2021-02-02 05:26:57 -08:00
Nikolaj Bjorner 3ae4c6e9de refactor get_sort 2021-02-02 04:45:54 -08:00
Nikolaj Bjorner 4455f6caf8 move to get_sort as method, add opt_lns pass, disable xor simplification unless configured, fix perf bug in model converter update trail 2021-02-02 03:58:19 -08:00
Nikolaj Bjorner 6f346bf804 fix build break 2021-01-31 22:56:42 -08:00
Nikolaj Bjorner 33525007ab try #4984 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-31 22:15:00 -08:00
Nikolaj Bjorner 20870c43ec build test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-31 20:49:53 -08:00
Nikolaj Bjorner 4dfdabc80f na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-31 16:36:55 -08:00
Nikolaj Bjorner 46f754c43d add priority queue to instantiation 2021-01-31 16:17:52 -08:00
Nikolaj Bjorner 22b0c3aa70 add priority queue to instantiation 2021-01-31 16:17:36 -08:00
Nikolaj Bjorner 942706e271 equality simplification 2021-01-31 15:44:43 -08:00
Nikolaj Bjorner 6d99a8f0cc fixes for unicode 2021-01-31 14:55:52 -08:00
Nikolaj Bjorner 60cc9d8182 set unicode by default 2021-01-31 11:32:33 -08:00
Nikolaj Bjorner 8fde6c207d set unicode to default 2021-01-31 07:22:51 -08:00
Nikolaj Bjorner 3f93cc3f0b use unicode by default 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-30 16:39:31 -08:00
Nikolaj Bjorner a1f46392aa na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-30 16:00:38 -08:00
Nikolaj Bjorner 657ed4db7a fix relevancy bug for recfun 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-30 07:19:57 -08:00
Nikolaj Bjorner 520b24aab4 string escaping 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-30 04:58:58 -08:00
Nikolaj Bjorner c99b805c14 mld 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-29 18:37:38 -08:00
Nikolaj Bjorner ff475cbd5f include rewriter_def 2021-01-29 17:17:22 -08:00
Nikolaj Bjorner 34c34b68ee one more nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-29 16:40:59 -08:00
Nikolaj Bjorner ec1e3cc14a encoding disaster 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-29 16:25:24 -08:00
Nikolaj Bjorner 4af9132f2e more ematching 2021-01-29 13:39:14 -08:00
Nikolaj Bjorner 4857446cf6 change handling of escapes for #4708 2021-01-29 13:36:47 -08:00
Nikolaj Bjorner b402268d35 fix #4982 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-29 06:43:33 -08:00
Nikolaj Bjorner c0c314d1ae build fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-29 06:23:27 -08:00
Nikolaj Bjorner 4e98a39d60 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-29 06:15:00 -08:00
Murphy Berzish da68c3213c
Unicode for Z3str3 (#4981) 
* z3str3: remove hard-coded char set

* z3str3: remove hard-coded char set

* z3str3: use char abstraction

* z3str3: scope management for unicode chars

* add QF_CHAR for z3str3

* z3str3: remove hard-coded char set

* z3str3: use char abstraction

* z3str3: scope management for unicode chars

* add QF_CHAR for z3str3

* z3str3: add 'char' string solver case

* z3str3: fix mk_char using the wrong ast manager

* z3str3: fix refcounted character vectors
 2021-01-29 06:14:38 -08:00
Nikolaj Bjorner cfcd7f18a9 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-28 17:09:12 -08:00
Nikolaj Bjorner afc4c700b1 move directory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-28 14:49:15 -08:00
Nikolaj Bjorner 42e601483d add selected updates #4981 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-28 13:43:30 -08:00
Nikolaj Bjorner e3d634807b move common routines for quantifiers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-28 13:23:40 -08:00
Nikolaj Bjorner 5414030875 #4939 escape character 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-28 11:57:00 -08:00
Nikolaj Bjorner f48fb8d3e8 it just works 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-28 11:12:05 -08:00
Nikolaj Bjorner 8a229bf684 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 22:39:02 -08:00
Nikolaj Bjorner 49aebdbb02 adding unicode fixup base on #4939 discussion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 20:21:46 -08:00
Nikolaj Bjorner e61949059d compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 19:50:34 -08:00
Nikolaj Bjorner 579caab025 na 2021-01-27 19:35:34 -08:00
Nikolaj Bjorner 909257f856 remove family id externals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 06:48:24 -08:00
Nikolaj Bjorner d3564f5b50 move unicode toggle to char-plugin 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 06:42:19 -08:00
Nikolaj Bjorner 0c770e25df na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 06:29:38 -08:00
Nikolaj Bjorner e969bd1c97 fully remove seq-based characters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 06:26:44 -08:00
Nikolaj Bjorner 8d8fe872ad remove plugin status to theory_seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 06:22:25 -08:00
Nikolaj Bjorner 696b3c79b9 fixes to self-contained character unicode 2021-01-27 06:13:37 -08:00
Nikolaj Bjorner d0f1d8f59e move to unicode as stand-alone theory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 05:46:45 -08:00
Nikolaj Bjorner ecba26beae missing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-26 17:07:46 -08:00
Nikolaj Bjorner 32058d9c68 add char_decl_plugin 2021-01-26 16:43:03 -08:00
Nikolaj Bjorner 20332c6d3e adding char decl plugin for separate theory treatment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-26 16:28:44 -08:00
Nikolaj Bjorner 33714ceb40 use _ 2021-01-26 14:56:48 -08:00
Nikolaj Bjorner e26e38b654 add error generation for #4977 2021-01-26 14:55:42 -08:00
Nikolaj Bjorner 8ed1992029 char value 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-26 11:29:40 -08:00
Nikolaj Bjorner a0b7879dd9 handle signed characters convertions into unsigned numbers 2021-01-26 11:20:28 -08:00
Nikolaj Bjorner 7dd7d83a36 make it easier to use string literals 2021-01-26 11:01:03 -08:00
Nikolaj Bjorner 31b7ad3012 prepare char utilities as a stand-alone theory 2021-01-26 10:34:10 -08:00
Nikolaj Bjorner dccfecb488 generator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-25 19:18:55 -08:00
Nikolaj Bjorner 4b6d7ca097 working on mam 2021-01-25 17:54:53 -08:00
Nikolaj Bjorner f33d6f89b9 fix #4973 2021-01-25 12:20:27 -08:00
Nikolaj Bjorner 2646e0a1c0 have add_soft accept an interable of Booleans. 2021-01-25 12:17:35 -08:00
Nikolaj Bjorner 7d60d8462d patch for Sturm sequence bug #4961 2021-01-24 12:58:25 -08:00
Nikolaj Bjorner 47cb1d1207 remove bit-vector dependencies in theory_str_mc. See discussion #4939 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-23 13:03:06 -08:00
Nikolaj Bjorner e4cec19f03 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-23 12:16:00 -08:00
Nikolaj Bjorner 96f1f4a567 rename to seq_char instead of seq_unicode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-23 12:12:06 -08:00
Artem Alekseev 7e668e9a1f
Fix build (#4960) 2021-01-23 11:13:10 -08:00
Nikolaj Bjorner 03fd251ccb streamline unicode/ascii toggling. Fix bit-width for unicode to 18 2021-01-23 11:11:44 -08:00
Nikolaj Bjorner 90eb4de526 track reference counts of allocated characters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-23 10:42:43 -08:00
Nikolaj Bjorner 6edabd6c03 egraph 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-22 18:11:27 -08:00
Nikolaj Bjorner 680b185872 adding ematching engine, fixing seq_unicode 2021-01-22 17:10:45 -08:00
Nikolaj Bjorner db17ae03c6 early return, statistics, remove unused field 2021-01-21 23:53:34 -08:00
Nikolaj Bjorner 4c82350ca4 na 2021-01-21 23:35:04 -08:00
Nikolaj Bjorner 2051cac3a3 tidy 2021-01-21 23:34:47 -08:00
Nikolaj Bjorner 4e8ba8b160 regression fix, fix unicode mode 2021-01-21 22:06:15 -08:00
Nikolaj Bjorner 64ba44d2ac fix underflow bug when subtracting unsigned numbers 2021-01-21 21:01:02 -08:00
Nikolaj Bjorner dafee71500 reshuffle unicode support to use global parameter, and use bit-vectors on demand 2021-01-21 14:24:26 -08:00
Nikolaj Bjorner c5432dbd88 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-20 09:12:09 -08:00
Nuno Lopes 3a572edb9c fix build 2021-01-20 10:42:29 +00:00
Nikolaj Bjorner 48058e706f fix #4951 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-20 02:21:42 -08:00
Nikolaj Bjorner fa4869e400 fix #4949 - and/or get rewritten depending on parameters for rewriter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-20 01:08:54 -08:00
Nikolaj Bjorner 3a2ed691f8 fix #4952 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-20 00:49:28 -08:00
Nikolaj Bjorner 27ea23289e fix #4955 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-20 00:30:11 -08:00
Nikolaj Bjorner dc4382604b fix #4955 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-20 00:29:09 -08:00
Nikolaj Bjorner 80033a5527 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-19 23:21:47 -08:00
Nikolaj Bjorner 95d98ea8ce throttle equality propagation to shared expressions 2021-01-19 04:51:00 -08:00
Nikolaj Bjorner 7c34a54e8a try different command-line 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-19 04:28:22 -08:00
Nikolaj Bjorner 64ba2a9fc9 fix gc of pb constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-19 03:38:00 -08:00
Nikolaj Bjorner 01418a06a3 better staging of mbi based on generation 2021-01-18 16:55:58 -08:00
Nikolaj Bjorner 990aecceb7 change gc strategy for user-push/pop 2021-01-18 16:55:29 -08:00
Nikolaj Bjorner b87405cc92 tune user-pop 2021-01-18 16:51:34 -08:00
Nikolaj Bjorner 3ed490d4ed tune backtracking 2021-01-18 16:51:01 -08:00
Nikolaj Bjorner 91c54f6c39 na 2021-01-12 14:03:55 -08:00
Nikolaj Bjorner d1dab327cd fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-11 23:51:40 -08:00
Nikolaj Bjorner fc3a642876 fix #4948 2021-01-11 19:26:16 -08:00
Nikolaj Bjorner 0aac7e54a9 fix #4942 
Patching model update. Could use a more thorough revision.
 2021-01-11 15:48:49 -08:00
Nikolaj Bjorner 0e429cab33 enable new core for incremental mode 2021-01-11 14:55:31 -08:00
Nikolaj Bjorner 2ead209d40 indentation and updated links to default landing pages 2021-01-11 13:21:52 -08:00
Nikolaj Bjorner bcbda45298 updates to doc 2021-01-11 13:03:55 -08:00
Nikolaj Bjorner 396bfa05f3 fix grouping error 2021-01-11 12:25:53 -08:00
Nikolaj Bjorner 223bffd035 fix #4920 2021-01-09 02:02:50 -08:00
Nikolaj Bjorner 1a71dfac6f play nicebox #4918 2021-01-09 01:39:29 -08:00
Nikolaj Bjorner 96ab9edbfd fix #4923 2021-01-09 01:21:50 -08:00
Nikolaj Bjorner ffd57bef24 #4923 - eq2bv 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-08 16:38:07 -08:00
Nikolaj Bjorner 690bc51b7f fix #4927 2021-01-08 15:40:15 -08:00
Nikolaj Bjorner bb56443e71 more #4932 2021-01-08 15:24:12 -08:00
Nikolaj Bjorner 43eb862374 fix #4932 2021-01-08 12:50:36 -08:00
Nikolaj Bjorner 3d39f37e63 fix #4930 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-08 12:15:02 -08:00
Nikolaj Bjorner e902e1ef13 fix #4931 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-08 12:02:53 -08:00
Nikolaj Bjorner c36355c1e5 fix #4933 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-08 10:57:55 -08:00
Nikolaj Bjorner 0173359a50 debugging/testing mbi 2021-01-07 17:32:05 -08:00
Nikolaj Bjorner 4ca6d6951f use updated C++ features 2021-01-07 17:32:05 -08:00
Nikolaj Bjorner ac7d07ca58 fix #4937 2021-01-07 17:32:05 -08:00
Nikolaj Bjorner 60ef60dff8 euf solver updates 2021-01-07 17:32:04 -08:00
Nikolaj Bjorner 7bf691e1f9 fix bug in tracking qhead 2021-01-07 17:32:04 -08:00
Nuno Lopes 4db41c02cc remove some dead code from fpa2bv converter 2021-01-04 17:06:35 +00:00
Nikolaj Bjorner 5da71dc847 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-30 16:10:11 -08:00
Nikolaj Bjorner 523578e3f6 working on new solver core 2020-12-30 14:38:41 -08:00
Nikolaj Bjorner f519c58ace Add groovy R.U.Stan option to retrieve models even when they don't exist #4924 
Usage:
z3 4924.smt2 smt.candidate_models=true
 2020-12-30 14:38:41 -08:00
Nuno Lopes 799de71a9f
limit recursion depth of push_not() to 8 (#4917) 2020-12-28 19:55:43 -08:00
Nikolaj Bjorner 374ae52d70 testing mbi 2020-12-26 13:49:59 -08:00
Nikolaj Bjorner 372e5ca569 fixes in new solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-25 11:19:31 -08:00
Nikolaj Bjorner 21c626e3ee fix bound miss-computation, include sporadic nra check for #4913 2020-12-24 03:22:43 -08:00
Nikolaj Bjorner 8546cf97d7 on #4702 
Add weighting function to cycle more fairly through nla solvers.
Handles anomaly from https://github.com/Z3Prover/z3/files/5361721/pero.txt
 2020-12-24 03:07:25 -08:00
Nikolaj Bjorner 2679ae517b fix #4912 2020-12-23 15:04:25 -08:00
Nikolaj Bjorner 021bd8a994 sym file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-21 17:08:38 -08:00
Nikolaj Bjorner a72856111b add destination to custom command 2020-12-21 11:42:04 -08:00
Nikolaj Bjorner a164087384 remove cheap-eqs option as there is already propagate_eqs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-21 11:04:04 -08:00
Nikolaj Bjorner cd77a4d9a5 fix #4909 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-20 11:53:19 -08:00
Nikolaj Bjorner 8e0a2c9e77 fix #4910 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-20 11:29:13 -08:00
Nikolaj Bjorner 259a8ff786 fix #4907 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-20 11:02:19 -08:00
Nikolaj Bjorner c022a3e573 fix reset break 2020-12-19 16:32:54 -08:00
Nikolaj Bjorner 28a6da4532 fix #4902 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-18 14:43:00 -08:00
Nikolaj Bjorner 8521d2caaa check engine configuration for unsupported engines #4898 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-18 14:38:42 -08:00
Nikolaj Bjorner 7ce1c38544 'na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-18 14:33:06 -08:00
Nikolaj Bjorner e1f71d4932 fix #4904 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-18 14:32:16 -08:00
Nikolaj Bjorner 26af694d2c add overloads to != and == based on #4906 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-18 14:04:01 -08:00
Nikolaj Bjorner fa5567fa1f fix #4905 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-18 14:00:05 -08:00
Nikolaj Bjorner 727095c563 fix #4899 2020-12-17 23:03:01 -08:00
Nikolaj Bjorner 11477f1ed1 fixes in new solver 
fix logging and lemma signs in arith_solver, move logging of drat equalities to euf
 2020-12-16 10:40:17 -08:00
Nikolaj Bjorner 692bed7991 fix sign bug in internalization of literals 2020-12-14 17:33:14 -08:00
Nikolaj Bjorner 0ef8ebe89f fix #4895 2020-12-14 15:05:51 -08:00
Nikolaj Bjorner 7fe8298479 fix #4873 2020-12-12 16:03:48 -08:00
Nikolaj Bjorner f71204c222 fix #4879 2020-12-12 13:37:25 -08:00
Nikolaj Bjorner 0643e7c0fc fix #4886 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-12 12:40:14 -08:00
Nikolaj Bjorner dda4d66325 fix #4888 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-12 12:33:48 -08:00
Nikolaj Bjorner 8cb30d0505 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-12 12:21:34 -08:00
Nikolaj Bjorner 89fb55a864 fix #4890 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-12 12:20:53 -08:00
Nikolaj Bjorner 89a6c7a349 fix #4883 2020-12-10 07:30:19 -08:00
Lev Nachmanson 4d7062d2a1 fix in nla_ordered_lemma 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-12-09 06:48:58 -08:00
Nikolaj Bjorner 621e99284b fix arith_solver=6 regression over solver=2 
https://github.com/Z3Prover/z3/issues/4613#issuecomment-668047545
 2020-12-08 16:36:43 -08:00
Nikolaj Bjorner fae9481308 fix #4875 
remove unsound rewrite, regression
 2020-12-08 12:17:41 -08:00
Nikolaj Bjorner 97683bd48a fix #4876 2020-12-08 12:12:16 -08:00
Nikolaj Bjorner 8ce08d57a0 na 2020-12-08 12:08:15 -08:00
Nikolaj Bjorner 43ddb08332 fix #4874 2020-12-08 12:08:07 -08:00
Nikolaj Bjorner 9b9d906702 fix #4871 2020-12-07 22:07:30 -08:00
Nikolaj Bjorner c49d39af81 perf for #4655 2020-12-07 21:34:57 -08:00
Nikolaj Bjorner f5f980fa38 add rewrite rule 2020-12-07 21:28:23 -08:00
Nikolaj Bjorner 430b4ea252 fix #4870 2020-12-07 17:52:56 -08:00
Nikolaj Bjorner 9f6a0a868a fix #4389 fix #4859 
The bugs are duplicates
 2020-12-07 14:57:50 -08:00
Nikolaj Bjorner 409414c5b3 #4655 
rewrite replace using distributivity rule.
 2020-12-07 13:12:26 -08:00
Nikolaj Bjorner 289cc9de79 add rewrites for replace_all 2020-12-07 13:02:28 -08:00
Lev Nachmanson 7089610bbd set arith.cheap_eqsTO True 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-12-07 12:02:57 -08:00
Nikolaj Bjorner 982da8db05 fix #4868 2020-12-07 10:27:00 -08:00
Nikolaj Bjorner 6c9bdc949e fix #4848 2020-12-07 05:59:55 -08:00
Nikolaj Bjorner 27dac3e1a0 fix #4844 2020-12-07 05:54:50 -08:00
Lev Nachmanson b90143cc0e set the defalt for cheap_eqs=False, do not run 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-12-06 18:26:26 -08:00
Nikolaj Bjorner 4c1fcbaa62 fix #4865 2020-12-06 14:13:46 -08:00
Nikolaj Bjorner 746dd745ad fix #4856 2020-12-06 14:06:08 -08:00
Nikolaj Bjorner c3c7aad1a8 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-06 11:18:37 -08:00
Lev Nachmanson 2e5eb2dde2
Tree fix (#4864) 
* simplify cheap equality tree

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* simplify cheap equality tree

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* more fixes

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-12-06 11:18:27 -08:00
Addison Crump b0cecf7747
Make multi-index arrays not so bad (#4857) 2020-12-05 15:45:46 -08:00
Nikolaj Bjorner 4d55f83654 misc 2020-12-04 16:59:13 -08:00
Murphy Berzish b0fd25f041
z3str3: don't compute intersection difficulty against a null automaton (#4846) 2020-12-04 10:40:03 -06:00
Nikolaj Bjorner 6d427d9dae fix #4839 2020-12-02 12:46:24 -08:00
Nikolaj Bjorner 12198d13ac fix #4794 2020-12-02 12:24:35 -08:00
Nikolaj Bjorner 9156e355d8 log 2020-11-30 11:57:25 -08:00
Addison Crump 3bca1fbcd8
Java type generics (#4832) 
* Generify, needs some testing and review

* Remove unnecessary change

* Whoops, ? capture that type

* Misread the docs, whoops

* More permissible arithmetic operations

* Implement believed Optimize generics

* Missed a few generics

* More permissible expr for arrays in parameters

* More permissible expr for bitvecs in parameters

* More permissible expr for bools in parameters

* More permissible expr for fps in parameters

* More permissible expr for fprms in parameters

* More permissible expr for ints in parameters

* More permissible expr for reals in parameters

* Undo breaking name conflict due to type erasure; see notes

* Whoops, fix typing of ReExpr

* Sort corrections for Re, Seq

* More permissible expr for regular expressions in parameters

* Fix name conflict between sequences and regular expressions; see notes

* Minor typo, big implications!

* Make Constructor consistent, associate captured types with other unknown capture types for datatype consistency

* More expressive; outputs of multiple datatype definitions are only known to be sort, not capture, and Constructor.of should make a capture

* Be less dumb and just type it a little differently

* Update examples, make sure to type Expr and FuncDecl sort returns

* General fixups

* Downgrade java version, make it only for the generic support, remove var and Expr[]::new construction

* Turns out Java 8 hadn't figured out how to do stream generics yet. Didn't even show up in my IDE, weird
 2020-11-30 10:04:54 -08:00
Nikolaj Bjorner bb24b3f2be fix #4836 2020-11-29 21:08:28 -08:00
Nikolaj Bjorner 260f759177 fix #4835 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-29 20:06:32 -08:00
Nikolaj Bjorner 67bbdc7524 fix initialization order 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-29 19:48:42 -08:00
Nikolaj Bjorner 64af8981ba fix #4834, regression after delay-propagating disequality axioms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-29 19:43:46 -08:00
John Regehr b7e1b1e118
get rid of threads in the scoped_timer thread pool prior to forking, on non-Windows (#4833) 
* on POSIX systems, fork() is dangerous in the presence of a thread
pool, because the child process inherits only the thread from the
parent that actually called fork().

this patch winds down the scoped_timer thread pool in preparation for
forking; workers will get freshly created again following the fork
call.
 2020-11-29 21:26:53 +00:00
Nikolaj Bjorner 05c5f72ca1 fix #4829 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-28 11:25:36 -08:00
Nikolaj Bjorner 17f04099a5 fix #4831 2020-11-28 11:01:07 -08:00
Nikolaj Bjorner 6e14d3fbd3 fix #4795 2020-11-27 18:00:36 -08:00
Nikolaj Bjorner df09cb7c95 fix relevancy test 2020-11-27 14:49:05 -08:00
Nikolaj Bjorner 35900ee8ea avoid crash from #4772 
To take care of "When I use options fp.xform.slice=false fp.xform.inline_eager=false Z3 actually seg-faults."
 2020-11-27 14:41:28 -08:00
Nikolaj Bjorner 67a8492bd0 more graceful proof checks 2020-11-27 14:40:46 -08:00
Nikolaj Bjorner 6771e44d93 fix #4825 #4824 2020-11-27 13:39:33 -08:00
Nikolaj Bjorner 1619311ff7 fix #4826 2020-11-27 10:42:13 -08:00
Nikolaj Bjorner f58618aa04 fix java compile 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-26 08:09:48 -08:00
Nikolaj Bjorner b5a6c6bc66 attempt at more graceful timeout handling #4821 2020-11-26 06:33:44 -08:00
Nikolaj Bjorner d6a5ef4343 add recfuns to Java #4820 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-25 12:25:20 -08:00
Murphy Berzish 6aba325cea
z3str3: reject certain unhandled expressions (#4818) 2020-11-25 12:15:35 -08:00
Nikolaj Bjorner c27a325017 na 2020-11-23 10:22:21 -08:00
Nikolaj Bjorner b769c0054b fix error messages for #4816 2020-11-23 10:20:52 -08:00
Nikolaj Bjorner 291502f8e4 this-> 2020-11-22 21:20:13 -08:00
Nikolaj Bjorner 1008b2d4cb fix #4812 2020-11-22 16:21:19 -08:00
Nikolaj Bjorner 193ca57444 fix #4811 2020-11-22 16:05:44 -08:00
Nikolaj Bjorner 65464f5944 include order 2020-11-22 15:39:09 -08:00
Nikolaj Bjorner 797f50e699 DRAT debugging updates 2020-11-22 15:38:57 -08:00
Nikolaj Bjorner 6d0b89a989 fix #4810 2020-11-22 15:37:55 -08:00
Nikolaj Bjorner 065e0652a3 fix crash when parsing datalog format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-21 15:15:28 -08:00
Nikolaj Bjorner 299e1788b8 fix #4808 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-21 15:03:17 -08:00
Nikolaj Bjorner d6106f26ff disable gcd test 2020-11-20 12:18:19 -08:00
Nikolaj Bjorner 1b768c9b3a fix #4805 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-20 12:11:38 -08:00
Nikolaj Bjorner 1269776777 remove experimental option. Fix #4806 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-20 11:46:19 -08:00
Nikolaj Bjorner ac1b3fc6f2 fix delay blasting and relevancy 2020-11-20 11:12:55 -08:00
Nikolaj Bjorner 9f34af5e18 update justifications only at level 0 2020-11-20 11:12:55 -08:00
Nikolaj Bjorner ee04bfd174 fix equality propagation 2020-11-20 11:12:55 -08:00
Nikolaj Bjorner a475e7cf5a Add gcd test to bv-rewriter 2020-11-20 11:12:54 -08:00
Nikolaj Bjorner 6506d33b35 Add GCD test 2020-11-20 11:12:54 -08:00
Nikolaj Bjorner b7b7970c4a guard table erasure for representative 2020-11-20 11:12:54 -08:00
Nuno Lopes 40159a3a96 fix single-thread build 2020-11-19 21:46:32 +00:00
John Regehr 0fa88efc2b
scoped_timer: wait for timer thread before main thread continues (#4803) 2020-11-19 21:42:55 +00:00
Nikolaj Bjorner e16acd0965 move std::function initializer to beginning of class 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-16 17:02:15 -08:00
Nikolaj Bjorner f6f594e21d fix missing equality propagation in new bv solver 2020-11-16 16:22:56 -08:00
Nikolaj Bjorner 36e40a296f add logging for rewriter.flat 2020-11-16 11:20:33 -08:00
Nikolaj Bjorner 85a20791db fix relevancy tracking in new solver 2020-11-16 11:20:17 -08:00
Nikolaj Bjorner 36e9412252 fix #4796 2020-11-16 11:19:54 -08:00
Nikolaj Bjorner 98db260a93 relax unhandled condition 2020-11-14 14:58:43 -08:00
Nikolaj Bjorner 49a0266c6a na 2020-11-13 17:05:56 -08:00
Nikolaj Bjorner 9fa17a432a bug fixes in nullability check 
@veanes @cdstanford
 2020-11-13 17:05:10 -08:00
Nikolaj Bjorner c15001bf69 #4532 
https://github.com/Z3Prover/z3/issues/4532#issuecomment-726867868
 2020-11-13 11:45:59 -08:00
Nikolaj Bjorner 71ac40ca23 fix #4793 2020-11-13 11:45:05 -08:00
Nikolaj Bjorner cb4e5197fa #4740 
Fix https://github.com/Z3Prover/z3/issues/4740#issuecomment-712092917
 2020-11-12 16:55:07 -08:00
Nikolaj Bjorner 7f869e513b fix #4792 2020-11-12 13:23:34 -08:00
Nikolaj Bjorner d61f30fdc6 force flat for solver 2, fix #4789 2020-11-12 13:01:38 -08:00
Nikolaj Bjorner 5d10cb7af4 fix #4791 - diff is left associative 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-11 18:07:05 -08:00
Nikolaj Bjorner 7e68d546ba na 2020-11-11 17:37:07 -08:00
Nikolaj Bjorner aced115b70 model validation 2020-11-11 17:37:07 -08:00
Nikolaj Bjorner 16db8bf49e add model validation 2020-11-11 17:37:07 -08:00
Nikolaj Bjorner b5aab7ec2a fix clone 2020-11-11 17:37:06 -08:00
Nikolaj Bjorner 9704733693 fix #4790 2020-11-11 17:37:06 -08:00
Lev Nachmanson 4810b4cac2 add a comment in nla_order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-11-10 11:12:28 -08:00