mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-16 01:16:39 +00:00
Code Activity
15480 commits 43 branches 51 tags 169 MiB
Commit graph

224 commits

Author SHA1 Message Date
Nikolaj Bjorner
20a67e47ca remove symbol -> zstring -> symbol round-trips 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-22 13:12:49 -07:00
Murphy Berzish
466269ee13
theory_str iterator refactoring and dead code removal (#5222) 
* z3str3: iterator refactoring

* z3str3: remove old nfa dead code

* z3str3: continued iterator refactoring

* z3str3: remove unroll dead code

* z3str3: ctx_dep_analysis iterator refactoring

* z3str3: continued iterator refactoring

* z3str3: final iterator refactoring
 2021-05-05 10:06:03 -05:00
Nikolaj Bjorner
15a7621e27 remove template dependency for trail objects 2021-03-19 11:15:05 -07:00
Murphy Berzish
5599387a34
z3str3: add str.is_digit support (#5038) 2021-02-23 10:36:01 -06:00
Murphy Berzish
27db97c269
Z3str3: add str.to_code and str.from_code (#5015) 2021-02-18 16:51:34 -06:00
Nikolaj Bjorner
a152bb1e80 remove template Context dependency in every trail object 2021-02-08 15:41:57 -08:00
Murphy Berzish
da68c3213c
Unicode for Z3str3 (#4981) 
* z3str3: remove hard-coded char set

* z3str3: remove hard-coded char set

* z3str3: use char abstraction

* z3str3: scope management for unicode chars

* add QF_CHAR for z3str3

* z3str3: remove hard-coded char set

* z3str3: use char abstraction

* z3str3: scope management for unicode chars

* add QF_CHAR for z3str3

* z3str3: add 'char' string solver case

* z3str3: fix mk_char using the wrong ast manager

* z3str3: fix refcounted character vectors
 2021-01-29 06:14:38 -08:00
Nikolaj Bjorner
42e601483d add selected updates #4981 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-28 13:43:30 -08:00
Nuno Lopes
bb26f219fe remove unneeded constructors (last round) 2020-07-12 17:41:57 +01:00
Nuno Lopes
23e6adcad3 fix a couple hundred deref-after-free bugs due to .c_str() on a temporary string 2020-07-11 20:24:45 +01:00
Nikolaj Bjorner
d0e20e44ff booyah 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 15:56:30 -07:00
Murphy Berzish
fce1252145
Z3str3: Add consistency checks for string-integer conversion terms in model construction (#4551) 
* z3str3: check consistency of str.to_int in fixed length solver

* z3str3: add similar check for int.to_str as well

* z3str3: refactor string-integer conversion check and add post checks for model construction
 2020-06-30 11:20:44 -05:00
Federico Mora Rocha
8d16a9a034
z3str3: fix Issues 4349, 4354, and 4310 (#4529) 
* regex needs lesson; m.mk_eq not ctx.mk_eq

* when unsat core is of size 0, then do naive learning

* remove two extra comments, and correct positive regex learning

* replace magic numbers for fixed-length lessons with constants
 2020-06-24 15:46:32 -05: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
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
Murphy Berzish
fcbcad6c10
Merge pull request #4320 from mtrberzi/mc-rational 
z3str3: use rational in place of unsigned during model construction
 2020-05-15 20:42:19 -05:00
Murphy Berzish
5e7806c4a4 z3str3: use rational in place of unsigned during model construction 2020-05-13 14:32:44 -04:00
Murphy Berzish
51beeec92f z3str3: heuristics for predicates over int-to-string terms 2020-05-12 21:35:24 -04:00
Nikolaj Bjorner
becf423c77
remove level of indirection for context and ast_manager in smt_theory (#4253) 
* remove level of indirection for context and ast_manager in smt_theory

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add request by #4252

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* move to def

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* int

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-08 16:46:03 -07:00
Murphy Berzish
1f15033ca2
z3str3: remove legacy code (#4215) 
* z3str3: remove legacy fixed-length overlap testing

parameter smt.str.fixed_length_overlap_models has been deprecated

* z3str3: remove legacy length/value testing algorithm and binary search heuristic

the following parameters are deprecated:
smt.str.use_binary_search
smt.str.binary_search_start
smt.str.fixed_length_models (the fixed-length model construction is now always used)

* z3str3: remove legacy regex unroll methods

* z3str3: remove unused methods and member variables
 2020-05-06 13:07:04 -07:00
Murphy Berzish
c1a0ce0862
Z3str3: reset internal data structures in init_search_eh() (#3818) 
* z3str3: fixes to solver state between check-sat calls, wip

* z3str3: reset many internal data structures during init_search_eh() to clean up state
 2020-04-11 12:36:30 -07:00
Nikolaj Bjorner
54d981e88f fix #3757 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 11:25:29 -07:00
Murphy Berzish
b4acd44d5e z3str3: fix crash in model construction when a variable has an impossible length assignment 2020-02-18 08:57:06 -10:00
Murphy Berzish
883c5df109 z3str3: regex automata in bitvector model construction 2020-02-06 21:43:23 -08:00
Murphy Berzish
237adbf40c z3str3: ensure top-level free variables always participate in model construction 2020-02-06 21:43:23 -08:00
Murphy Berzish
faf3934749 z3str3: add bitvector model construction algorithm 2020-02-06 21:43:23 -08:00
Murphy Berzish
e5ca451a02 z3str3: remove unused str_eq_todo worklist 2019-12-05 01:51:16 +03:00
Murphy Berzish
bf28b815fa z3str3: add a method to rewrite-and-assert an axiom to reduce boilerplate 2019-11-29 09:37:22 -08:00
Murphy Berzish
415260b93d z3str3: refactor app* to app_ref 2019-11-22 16:07:50 -08:00
Murphy Berzish
f91af02675 z3str3: set up axioms on string terms that are added during the search 2019-10-24 15:20:07 -07:00
Nikolaj Bjorner
ca498e20d1 move value factories to model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-16 19:48:35 -07:00
Murphy Berzish
f29b033253 z3str3: add is_var() similar to theory_seq's implementation 2019-09-28 17:45:49 -07:00
Murphy Berzish
b2f0051114 Merge remote-tracking branch 'upstream/master' into refactoring-arith 2018-10-02 12:38:40 -04:00
Bruce Mitchener
cdfc19a885 Use nullptr. 2018-10-02 09:11:19 +07:00
Murphy Berzish
144b72244e clean up pragmas, Z3str3 refactoring 2018-09-18 16:11:47 -04:00
Murphy Berzish
7e419137b1 Z3str3: refactor regex automata to subroutine, use arith_value 2018-09-17 16:13:34 -04:00
Murphy Berzish
3cfb32cd2d fix regex automata leaked memory 2018-04-12 14:35:29 -04:00
Murphy Berzish
6a3ce301b7 fix collection error 2018-04-03 12:51:03 -04:00
Murphy Berzish
41703a4254 Merge branch 'develop' into regex-develop 2018-04-03 12:31:27 -04:00
Murphy Berzish
d26eddf776 re-add indexof-contains heuristic 2018-03-19 18:31:26 -04:00
Murphy Berzish
d569485170 Merge remote-tracking branch 'upstream/master' into refactoring 2018-03-19 01:43:18 -04:00
Nikolaj Bjorner
aa913c564c moving more std::map std::set to obj_*, #1529 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-17 04:21:28 -07:00
Nikolaj Bjorner
86d3bbe6cb added TODO markers in theory_str.h for moving to obj_map, remove include of stdbool for now 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-16 07:46:27 -07:00
Murphy Berzish
6bb9a82425 experimental axiom-persist for regex conflict clauses 2018-03-15 13:56:44 -04:00
Murphy Berzish
73f7e301c3 preliminary refactoring to use obj_map 2018-03-12 17:09:55 -04:00
Nikolaj Bjorner
5651d00751 fix #1534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-12 13:21:31 -07:00
Murphy Berzish
49b810e00f Merge branch 'master' into regex-develop 2018-03-11 23:18:55 -04:00
Murphy Berzish
f43a027447 Merge branch 'develop' into issue1379 2018-03-06 22:14:18 -05:00
Murphy Berzish
762129d4c7 fixups to theory_str for regex 2018-02-12 17:45:07 -05:00
Murphy Berzish
54206e3674 Merge branch 'develop' into regex-develop 
Conflicts:
	src/smt/theory_str.h
 2018-02-12 17:25:50 -05:00