mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
11550 commits 49 branches 53 tags 182 MiB
Commit graph

2530 commits

Author SHA1 Message Date
Murphy Berzish
09053b831d enforce nonempty string constraint on refreshed nonempty string vars 2016-12-09 17:23:39 -05: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
Murphy Berzish
515cd4a3f3 add boolean case split in theory_str::solve_concat_eq_str 2016-12-08 14:49:38 -05: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
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
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
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
Nikolaj Bjorner
441dbbb94b streamline logging in arithmetic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-24 13:08:50 -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
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
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
b138a0f6d3 Cleaned up hacky rewriter cancelation fix in theory_fpa. 2016-11-17 16:36:39 +00: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