2324 commits

Author	SHA1	Message	Date
Murphy Berzish	852e0e0892	fix regex difficulty overflow bug; fix final check on regex terms that don't get path constraints	2018-01-25 15:25:36 -05:00
Murphy Berzish	8d5065d35d	fix constant eqc bug in mk_concat	2018-01-24 22:02:00 -05:00
Murphy Berzish	d648f95f63	fix setup of path constraints when the path constraint is False	2018-01-24 21:25:45 -05:00
Murphy Berzish	d9d3ef78d2	temporarily disable final check progress checking ... it is interfering with regex automata solving	2018-01-19 16:14:56 -05:00
Murphy Berzish	2065ea88ee	fix null pointer dereference	2018-01-19 14:56:06 -05:00
Murphy Berzish	a9fda81d03	check polarity	2018-01-18 17:53:42 -05:00
Murphy Berzish	5727950a3c	zero-length automaton solution fix	2018-01-18 17:52:55 -05:00
Murphy Berzish	dbb15f65b5	correct generation of linear length constraints for regex star terms	2018-01-17 19:26:42 -05:00
Murphy Berzish	c2b268c645	short path for length-0 regex terms	2018-01-17 18:26:31 -05:00
Murphy Berzish	c0ed683882	disable regex length constraint generation as it currently makes unsound axioms	2018-01-17 13:32:44 -05:00
Murphy Berzish	26ab91a448	check duplicate bounds info for regex terms	2018-01-17 13:02:32 -05:00
Murphy Berzish	e5585ecf4c	regex fail count and automaton fallback	2018-01-16 18:15:29 -05:00
Murphy Berzish	153701eabe	regex length term assertion WIP	2018-01-16 13:56:01 -05:00
Murphy Berzish	6c4c9a10e4	regex length linearity check WIP	2018-01-16 13:16:31 -05:00
Murphy Berzish	191cc30e2a	intersection of regex constraints produces a conflict clause	2018-01-15 15:30:12 -05:00
Murphy Berzish	058d24fd09	reuse regex character constraints for the same string	2018-01-15 14:30:12 -05:00
Murphy Berzish	6f889ab699	intersection WIP; fix polarity of generated path constraint LHS	2018-01-15 14:08:15 -05:00
Murphy Berzish	ca3784449f	regex failsafe and intersect WIP	2018-01-12 13:53:02 -05:00
Murphy Berzish	6b799706b5	add path constraint generation for regex terms	2018-01-10 17:24:47 -05:00
Murphy Berzish	bac5a648d9	regex path constraint generation (WIP)	2018-01-09 20:20:04 -05:00
Murphy Berzish	98691a2c49	lower bound refinement	2018-01-08 15:56:21 -05:00
Murphy Berzish	09dc5cd0f8	Merge branch 'develop' into regex-develop	2018-01-03 16:12:33 -05:00
Murphy Berzish	a5180edc76	make linear search the default for theory_str	2018-01-03 16:05:34 -05:00
Murphy Berzish	0f20944aeb	regex lower bound (WIP)	2018-01-03 13:54:18 -05:00
Murphy Berzish	0917af7c56	full upper bound refinement	2018-01-03 12:02:11 -05:00
Bruce Mitchener	5a0f5a778f	Remove unnecessary copy of coeff in iteration.	2018-01-02 23:14:29 +07:00
Bruce Mitchener	73b3da37d8	Typo fixes.	2018-01-02 22:48:06 +07:00
Nikolaj Bjorner	e8a9e1a58b	set default rewriter behavior in incremental mode to distribute multiplication over addition #1373 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-01-01 20:04:55 -08:00
Nikolaj Bjorner	c1c1b7378c	removing axiom exposing unsoundness, replace by weaker axiom ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-01-01 19:44:16 -08:00
Nikolaj Bjorner	f0a30ded7d	add shorthand for translating models #1407 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-01-01 19:25:09 -08:00
Simon Cruanes	cfcff78754	validate unsat cores in recfun	2017-12-25 23:35:54 +01:00
Simon Cruanes	f7e5977b9e	fix memleak	2017-12-25 22:51:40 +01:00
Simon Cruanes	35c802d869	simplify and strenghten some code	2017-12-25 22:51:39 +01:00
Simon Cruanes	0c753aa86a	fix bugs related to backtracking and restarts	2017-12-25 22:51:39 +01:00
Simon Cruanes	b877bd8286	debug messages and gating	2017-12-25 22:51:39 +01:00
Simon Cruanes	3b4718b99a	simpler conflicts when reaching unrolling limit (just add a clause)	2017-12-25 22:51:39 +01:00
Simon Cruanes	7b1e1d52e7	wip: conflicts for pruning branches with too many unrollings ... use the local assumption on depth to ensure the conflict clause is valid	2017-12-25 22:51:39 +01:00
Simon Cruanes	06e0b12700	add a predicate for depth limit assumptions	2017-12-25 22:51:39 +01:00
Simon Cruanes	d5e134dd94	wip: add recursive functions	2017-12-25 22:51:39 +01:00
Nikolaj Bjorner	5bc4c9809e	initialize additional assumptions after setup_context is called the first time ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-12-25 12:50:11 -08:00
Murphy Berzish	0ac7082c80	add upper bound refinement (WIP)	2017-12-21 17:13:39 -05:00
trinhmt	57845d4809	Merge pull request #4 from Z3Prover/master ... merge from z3prover/z3	2017-12-16 20:46:42 +08:00
Thai Trinh	07afce6a64	pass vectors by reference	2017-12-16 20:44:07 +08:00
Thai Trinh	fe503d95ec	simplify code	2017-12-15 20:01:03 +08:00
Nikolaj Bjorner	58c6cb87c3	small improvements to QF_NIA tactic ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-12-14 11:48:22 -08:00
Nikolaj Bjorner	a74d18a695	prepare for variable scoping and autarkies ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-12-13 20:11:16 -08:00
Nikolaj Bjorner	387e984bd3	Merge branch 'master' of https://github.com/z3prover/z3	2017-12-13 13:48:34 -08:00
Nikolaj Bjorner	5a479fca76	generalize model finder code to be independent of conjunction elimination ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-12-13 13:48:24 -08:00
Nikolaj Bjorner	7afbf8165e	snapshot ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-12-12 01:36:44 -08:00
Thai Trinh	c07a63cf8e	coalesce seq.unit into string in mk_skolem	2017-12-12 05:00:34 +08:00