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

6913 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
b758a7a508 disable smt-lib success printing when locally parsing database of common pattern rules. Issue #743 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-22 19:53:48 -07:00
Nikolaj Bjorner
092c52e5b7 fix for package directory. issue #744 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-22 18:29:26 -07:00
Murphy Berzish
dc8062ba67 patch out contains check for substr reduction 
fixes all regressions in release build, we may want to revisit this later
 2016-09-22 20:14:42 -04:00
Murphy Berzish
1061cdf58a fix value tester theory var reuse in theory_str 
fixes release regression in charAt-007
 2016-09-22 15:40:43 -04:00
Nikolaj Bjorner
9746794962 Merge pull request #742 from angr/fix-tests 
Fix z3test for build rearrangement
 2016-09-21 18:41:57 -07:00
Andrew Dutcher
4801a27c2d Fix up z3test to a) exist and b) work 2016-09-21 17:18:10 -07:00
Nikolaj Bjorner
cf56da8482 add z3test to cmakelists.txt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-21 16:33:30 -07:00
Nikolaj Bjorner
ef0dd74c53 try copy instead of cp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-21 16:14:27 -07:00
Nikolaj Bjorner
14668b4d44 Merge pull request #735 from angr/new-build 
New packaging for and ability to distribute python bindings
 2016-09-21 15:55:22 -07:00
Andrew Dutcher
f451363a8f use copy instead of create_symlink when not on unix 2016-09-21 15:15:21 -07:00
Nikolaj Bjorner
516dba52ce Merge branch 'master' of https://github.com/Z3Prover/z3 2016-09-21 12:24:34 -07:00
Nikolaj Bjorner
527c5191a6 Add C++ functions for set operations per stackoverflow post, set relevancy = 2 for quantified maxsmt per example from Aaron Gember, fix conversion of default weights based on bug report from Patrick Trentin on maxsat. Annotating soft constraints with weight=0 caused the weight to be adjusted to 1 and therefore produce wrong results 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-21 12:24:24 -07:00
Murphy Berzish
4433417b6e faster push_scope in theory_str 2016-09-20 16:25:28 -04:00
Murphy Berzish
feef85c129 override scope check in theory_str::solve_concat_eq_str 
fixes indexof2-009.smt2
 2016-09-20 15:37:29 -04:00
Murphy Berzish
48eaa6159c disable aggressive unroll testing in theory_str, it may be doing more harm than good 2016-09-20 01:10:27 -04:00
Murphy Berzish
447c6e4ce3 refresh length tester in theory_str::gen_len_val_options_for_free_var 
fixes charAt-007.smt2
 2016-09-20 00:28:29 -04:00
Murphy Berzish
f1d7ffcdce fix regression regex-020 2016-09-20 00:14:38 -04:00
Murphy Berzish
9615b191de theory_str hacking for theory var stuff WIP 2016-09-19 23:40:17 -04:00
Murphy Berzish
c38f63dd2a fix eqc management and unroll test var gen in theory_str::final_check 2016-09-19 19:42:16 -04:00
Nikolaj Bjorner
e8f4dd76c2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-09-17 17:29:33 -07:00
Nikolaj Bjorner
77b245b3d8 fix proof production to avoid crash. Issue #733 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-17 17:29:19 -07:00
Nikolaj Bjorner
cda967ead2 guard verbose output by verbosity level for datalog command-line tool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-16 15:36:40 -07:00
Nikolaj Bjorner
7f29674842 add option to bypass compression of unbound tails, issue #738 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-16 14:56:10 -07:00
Christoph M. Wintersteiger
7a3308110c Merge pull request #722 from wintersteiger/i715 
x64 clause allocator bug fix
 2016-09-16 19:53:08 +01:00
Christoph M. Wintersteiger
d922ee6a08 Merge pull request #741 from wintersteiger/master 
Adding bv preprocessing techniques (was #729).
 2016-09-16 19:52:46 +01:00
Mikolas Janota
147c0f8152 Removing an unused method from bv_rewriter. 2016-09-16 19:44:37 +01:00
Mikolas Janota
ec47a1df50 Adding bv preprocessing techniques. 2016-09-16 19:44:37 +01:00
Christoph M. Wintersteiger
27ea7d8e9d style/formatting 2016-09-16 19:34:48 +01:00
Christoph M. Wintersteiger
b70cc47a9d x64 clause allocator fix for del_clause 2016-09-16 19:25:41 +01:00
Christoph M. Wintersteiger
5b1cb49973 x64 clause allocator bug fix 2016-09-16 19:25:41 +01:00
Murphy Berzish
91b625768c fix tracing in theory_str 2016-09-15 17:01:59 -04:00
Murphy Berzish
e7c0c29ae5 potentially fix out-of-scope infinite loop bug in theory_str gen_unroll_conditional_options 2016-09-15 15:59:56 -04:00
Andrew Dutcher
9e498536b6 Fix cmake build to work with the new system 2016-09-15 02:19:20 -07:00
Murphy Berzish
8776b97841 variable scope correctness hack in theory_str 2016-09-14 22:08:40 -04:00
Murphy Berzish
bed40c45b8 cleanup 2016-09-14 21:48:27 -04:00
Murphy Berzish
ad7247df51 make calls to theory_str::dump_assignments depend on the correct trace flags 2016-09-14 19:32:14 -04:00
Murphy Berzish
15055c8041 use mk_int_var to make xor terms 2016-09-14 19:01:14 -04:00
Murphy Berzish
d334403720 remove relevancy testing experiment 2016-09-14 17:42:40 -04:00
Murphy Berzish
f22f4da023 remove unused variable 2016-09-14 17:33:47 -04:00
Murphy Berzish
9ee7326a19 tweaks to process_concat_eq_type_3 2016-09-14 17:26:52 -04:00
Andrew Dutcher
02217d048b replace all non-portable filepath slashes with os.path.join 2016-09-14 14:19:10 -07:00
Murphy Berzish
a294c145dc add theory_str::try_eval_concat to work around rewriter behaviour 
this fixes a regression in concat-013.smt2
 2016-09-14 16:18:03 -04:00
Murphy Berzish
e46fc7b0b6 fix expr-app conversion 2016-09-14 15:51:33 -04:00
Nikolaj Bjorner
5290cd1ff5 Merge pull request #737 from MathieuRoger/patch-1 
Update socrates.py
 2016-09-14 12:42:36 -07:00
Murphy Berzish
804009a757 use z3str2 eqc semantics for get_eqc_value 2016-09-14 15:37:48 -04:00
Mathieu Roger
9245e61775 Update socrates.py 2016-09-14 21:36:39 +02:00
Murphy Berzish
50353168ef fix semantics of get_concats_in_eqc and get_var_in_eqc 2016-09-14 15:36:36 -04:00
Murphy Berzish
87d61d6d6e fix semantics of in_same_eqc 2016-09-14 15:35:37 -04:00
Murphy Berzish
ec9e1686f7 fix semantics of collect_eq_nodes and simplify_parent 2016-09-14 15:32:49 -04:00
Murphy Berzish
9481601b4b restore z3str2 eqc semantics in theory_str::new_eq_check 2016-09-14 15:15:47 -04:00