mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
15439 commits 49 branches 53 tags 182 MiB
Commit graph

15439 commits

This branch
This branch
All branches
Author SHA1 Message Date
Murphy Berzish
99f20c59e4
Merge pull request #4490 from mtrberzi/issue4486 
z3str3: construct proper cex for str.at model construction
 2020-06-01 20:06:51 -05:00
Nikolaj Bjorner
7343783efe finetune 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-01 15:40:02 -07:00
Nikolaj Bjorner
8849cef4b7 add stub for equality propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-01 15:33:52 -07:00
Murphy Berzish
f395c8643c z3str3: construct proper cex for str.at model construction 2020-06-01 14:55:44 -04:00
Nuno Lopes
e079af9d0d
add context::internalize() API that takes multiple expressions at once (#4488) 2020-06-01 11:51:39 -07:00
Andrew V. Jones
e634f2987c
Ensuring correct 'set' call is used when setting 'smtlib2_log' (#4487) 
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
 2020-06-01 10:55:48 -07:00
trinhmt
48a2d3d5b6
fix #4481 (#4484) 2020-06-01 09:02:50 -07:00
Lev Nachmanson
c967b4aead more efficient patching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
c355ee025a fix bugs in patching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
e7bb8e57cb fixes in patch blocking 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
4728a1fb0c fix in cautious remove_basis 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
a6040a1f3d cautious remove_basis 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
91d9b0319e toward full patching in nl 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
c58bd3105b adding more aggressive patching in nl 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
6a5579341d add restore_patched_values 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
47d5515b78 change try_patch to a template 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
4b76e213a5 move declarations closer to usage 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
9b7f97fab9 change try_patch to a template 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
a53ed5bddd change try_patch to a template 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
2de79be31b change try_patch to a template 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
b84585beeb more aggressive patching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
e5503cdc65 change try_patch to a template 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
2710afbea1 change try_patch to a template 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
18016a7100 rename 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Nikolaj Bjorner
c424165d94 block deep based on condition for internalization #4192 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-31 13:31:16 -07:00
Nikolaj Bjorner
7d4c9e6126 fix #4480 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-31 12:40:04 -07:00
Nikolaj Bjorner
084cd335eb add (disabled) stubs for decomposing re-membership on regex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-31 12:25:21 -07:00
Nikolaj Bjorner
7f7663a3b4 fix #4478 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-31 11:16:21 -07:00
Nuno Lopes
31e75d1401 minor simplifications 2020-05-31 13:26:27 +01:00
Nuno Lopes
07e5b228a2 try to fix nightly build by moving to python3. python2 isn't supported anymore by setuptools 2020-05-31 11:40:13 +01:00
Nikolaj Bjorner
d372af4782 add stub for cheap equality propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-30 15:36:27 -07:00
Nuno Lopes
6a45c5d17c fix build with prehistorical compilers because of pip/manylinux 2020-05-30 11:42:27 +01:00
Nikolaj Bjorner
ce4e1d3cbb fresh index 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-29 19:54:50 -07:00
Nikolaj Bjorner
c92a63690d enable parsing (_ char ..) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-29 17:47:24 -07:00
Nikolaj Bjorner
d41ecda03e skip non-overlap simplification in rewriter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-29 17:27:54 -07:00
Nikolaj Bjorner
e68c72755a fix leak 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-29 14:49:53 -07:00
Nikolaj Bjorner
f381d51c83 update badge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-29 14:04:12 -07:00
calebstanford-msr
c939195c10
add regex support for reverse and left/right derivative rewriting (#4477) 
* partial work on adding 'reverse' (broken code)

* new op codes for derivative and reverse + associated rewrite rules

* incorporate reverses and derivatives in rewriter + some fixes

* enable rewriting str.in_re constraints with right derivative
 2020-05-29 13:00:37 -07:00
Nikolaj Bjorner
3d9d52f742 add detection of string equalities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-29 10:40:47 -07:00
Nikolaj Bjorner
e0130f5cf4 remove Kleene naming as it is a misnomer in this context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-28 20:41:03 -07:00
Nikolaj Bjorner
0911a06d81 bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-28 20:05:32 -07:00
Nikolaj Bjorner
ea1f50b77e simplify extended contains patterns 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-28 19:11:29 -07:00
Nikolaj Bjorner
6a90072a98 bug in non-member disjunction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-28 12:03:40 -07:00
Nikolaj Bjorner
220b8afd97 m is now an attribute on theory_smt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-28 10:36:51 -07:00
Nikolaj Bjorner
6d17c656bd merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-28 10:32:38 -07:00
trinhmt
4aa1e60daa
fix branch_variable() (#4472) 
* fixed branch_variable()

* add docs
 2020-05-28 10:21:50 -07:00
Murphy Berzish
e9eec5349d
z3str3: improve vector handling in simplify_parent (#4413) 2020-05-28 09:59:42 -07:00
Murphy Berzish
882777fc1d
z3str3: track the scope of library-aware terms for axiom setup (#4420) 2020-05-28 09:59:28 -07:00
Murphy Berzish
3b0c8a7ff9
fix logic for disabling theory case split heuristic (#4397) 2020-05-28 09:57:44 -07:00
Murphy Berzish
71ea7287bb
z3str3: detect and give up when symbolic automaton construction fails (#4384) 
typically this will happen due to non-constant terms in a RegLan expression
 2020-05-28 09:57:33 -07:00