Andrew V. Jones
d0515dca50
Circular seq axioms node ( #5104 )
...
* Dealing with ambiguity when calling 'find_file' #5089
Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
* Correcting ambiguity when calling 'find_file' if the file is in the current src dir #5089
Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
* Ensuring consistency when obtaining the original include #5089
Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
2021-03-16 06:58:54 -07:00
Nikolaj Bjorner
648568489c
internalize only terms not atoms
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-03-16 06:53:14 -07:00
Nikolaj Bjorner
cb8c6ffafc
a pending issue from #4866
...
https://github.com/Z3Prover/z3/issues/4866#issuecomment-748658905
2021-03-16 05:26:13 -07:00
Alexander Kreuzer
dc5fa89de3
Mixing Integers and Rational in the new Java API #5085 ( #5098 )
...
* Added covariance to arithmetic operations
* Added distillSort
* Update JavaGenericExample.java
Co-authored-by: Alexander Kreuzer <alexander.kreuzer@sap.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-03-16 05:24:23 -07:00
Nikolaj Bjorner
ee614c2e46
fix #5090
2021-03-15 17:02:38 -07:00
Nikolaj Bjorner
ff0de59a70
more streamlined diagnostics to prepare for #5106
2021-03-15 16:23:35 -07:00
Nikolaj Bjorner
d03fdf5fed
more descriptive naming convention
2021-03-15 15:48:33 -07:00
Nikolaj Bjorner
4b3fecc35e
remove dependency on ast from params
2021-03-15 15:40:41 -07:00
Nikolaj Bjorner
f00db08221
unused, thanks to AVJ
2021-03-15 13:49:17 -07:00
Nikolaj Bjorner
9098084217
reduce overhead of creating seq-plugin, enable parameter cleanup for #5095
2021-03-15 11:54:44 -07:00
Nikolaj Bjorner
d62f6c62b5
fix #5096 fix #5099
2021-03-15 09:43:34 -07:00
Nikolaj Bjorner
18143d8932
fix #5102
2021-03-15 01:01:33 -07:00
Nikolaj Bjorner
1cb0dbae51
missing dependency for python build
2021-03-14 20:45:30 -07:00
Nikolaj Bjorner
845ba7a11e
use a large delay for nlsat
2021-03-14 19:14:44 -07:00
Nikolaj Bjorner
155738088f
fix internalization on post-visit, increase delay to 100
2021-03-14 17:20:39 -07:00
Nikolaj Bjorner
8412ecbdbf
fixes to new solver, add mode for using nlsat solver eagerly from nla_core
2021-03-14 13:57:04 -07:00
Nikolaj Bjorner
9a975a4523
array solver fixes
2021-03-13 06:19:32 -08:00
Nikolaj Bjorner
78f4513441
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-03-13 06:19:31 -08:00
Murphy Berzish
04ac5f03f7
z3str3: use improved substr axioms from seq_axioms ( #5097 )
2021-03-12 14:51:16 -06:00
Andrew V. Jones
e8917a1a9f
Correcting 'String' to 'STRING' to resolve CMake warning ( #5091 )
...
Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
2021-03-09 15:14:57 -08:00
Nikolaj Bjorner
e08ceee424
compiler
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-03-08 20:41:10 -08:00
Nikolaj Bjorner
857557ad93
deal with compiler warnings
2021-03-08 20:39:19 -08:00
Nikolaj Bjorner
88fbf6510f
updates to theory_lra
2021-03-08 17:19:07 -08:00
Nikolaj Bjorner
f29a596070
deal with compiler warnings, from MacOS CI build
2021-03-08 17:14:09 -08:00
Nikolaj Bjorner
7eceeff349
move branch of unit variable
2021-03-08 10:09:04 -08:00
Nikolaj Bjorner
3c26a965e1
updated script, add comment to mk_eq_empty
2021-03-07 06:59:58 -08:00
Nikolaj Bjorner
7edc99f807
na
2021-03-06 12:36:19 -08:00
Nikolaj Bjorner
8de96009cd
na
2021-03-06 12:36:19 -08:00
Nikolaj Bjorner
e83f31949e
fix #5074 , add rewrite rules to simplify indexof special cases
2021-03-06 12:36:19 -08:00
Graydon Hoare
e8b3c90e14
Fix unintentional re-import of package z3 in z3printer, in python3. ( #5082 )
2021-03-06 10:44:07 -08:00
Nikolaj Bjorner
8d54e83567
updated hitting set sample
2021-03-06 10:18:52 -08:00
Nikolaj Bjorner
e804f7743a
Revert "Adjust imports so z3.z3 is still available in python3 ( #5079 )" ( #5081 )
...
This reverts commit 957d7bfe35
.
2021-03-05 15:26:00 -08:00
Nikolaj Bjorner
ea181fe8b2
more useful trace
2021-03-05 15:01:40 -08:00
Nikolaj Bjorner
5f0ec936e4
count final checks
2021-03-05 15:01:39 -08:00
Nikolaj Bjorner
022a1fd3dd
fix #5080 assertion is violated on legal input, add an example
2021-03-05 15:01:39 -08:00
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