mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity
6448 commits 23 branches 48 tags 157 MiB
Commit graph

6448 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner
e7f36a2d35 remove special characters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-14 10:32:17 -07:00
Nikolaj Bjorner
01eafdf68e Merge pull request #736 from MathieuRoger/patch-1 
Create socrates.py
 2016-09-14 10:29:21 -07:00
Mathieu Roger
a7e3a9df5a Create socrates.py 
Classical syllogism in Z3.
Many samples talks about integer, reals. Not much sample available on non integer things.
 2016-09-14 19:10:49 +02:00
Andrew Dutcher
02783d0bfb Minor tweaks to make things more reliable/less obnoxious 2016-09-14 01:49:37 -07:00
Andrew Dutcher
cb83c42100 Make python stuff live in a python directory in the build tree 2016-09-14 01:49:16 -07:00
Andrew Dutcher
704105306c FINISH IT 2016-09-14 01:40:01 -07:00
Andrew Dutcher
0bbd172af3 First steps to a sane python build 2016-09-14 01:37:04 -07:00
Andrew Dutcher
fa6cc19184 Moved python bindings into package 2016-09-14 01:33:07 -07:00
Murphy Berzish
34dc655150 z3str2 eqc semantics for theory_str unroll checks 2016-09-13 18:24:59 -04:00
Murphy Berzish
8f636e1f57 fix typo'ed set reference in handle_equality 2016-09-13 18:16:21 -04:00
Murphy Berzish
aea0032aa7 manage our own union-find structure in theory_str 
concat-086.smt2 passes with this, for the first time ever
 2016-09-13 18:01:45 -04:00
Nikolaj Bjorner
9f77759cd6 ensure that status is displayed in SMT-LIB2 compliant way. Issue #734 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-13 10:34:34 -07:00
Murphy Berzish
ca71a20ab7 add caching to theory_str::mk_concat, WIP 2016-09-12 17:17:17 -04:00
Murphy Berzish
015016c92b disable variable scope check if not tracing in theory_str 2016-09-12 16:57:05 -04:00
Murphy Berzish
b3fddf4707 performance optimization in theory_str::classify_ast_by_type 2016-09-12 16:41:35 -04:00