3102 commits

Author	SHA1	Message	Date
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
Nikolaj Bjorner	82c26509ae	Merge pull request #1396 from mtrberzi/substr-bug ... Fix incorrect term in theory_str str.substr reduction	2017-12-11 12:36:07 -08:00
Murphy Berzish	9d2c86f214	fix incorrect clause in argumentsValid subterm of substr reduction	2017-12-08 20:31:22 -05:00
Thai Trinh	8bf4a15c27	update "seq.align" skolem function	2017-12-09 00:47:48 +08:00
Thai Trinh	a2641909d0	initialize pointers	2017-12-08 19:40:20 +08:00
Thai Trinh	b819b368f1	minor	2017-12-08 19:29:07 +08:00
Thai Trinh	b8ce5509b0	change to "auto"	2017-12-08 19:16:28 +08:00
Thai Trinh	c33dfc80e0	Merge branch 'master' of https://github.com/Z3Prover/z3 into Z3Prover-master ... Conflicts: src/smt/theory_seq.cpp	2017-12-08 19:02:24 +08:00
Nikolaj Bjorner	faebbc5384	add shortcuts for concatenation and equality propagation ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-12-08 16:17:04 +05:30
Thai Trinh	b181d9d5fa	fix set-up	2017-12-08 18:45:56 +08:00
Thai Trinh	3a5c30bd9b	use obj_ref_map	2017-12-08 18:36:20 +08:00
Thai Trinh	6253faece7	fixed redundant check	2017-12-08 17:20:30 +08:00
Thai Trinh	7ece37f9a1	added assertions	2017-12-08 17:10:28 +08:00
trinhmt	034e72572f	Merge pull request #1 from Z3Prover/master	2017-12-08 14:42:34 +08:00
Thai Trinh	ff567412c1	Simplify code	2017-12-08 14:26:20 +08:00
Thai Trinh	2c48ffe7a7	Fixed setup_QF_S(): using configuration to choose the corresponding string solver	2017-12-08 13:41:18 +08:00
Nikolaj Bjorner	a5d5dfdf86	fix setup for non-linear real arithmetic per QF_UFNRA regresssions ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-12-08 09:23:57 +05:30
Thai Trinh	b6806eb1c2	Add more splitting rules for string equations (including rules based on length constraints)	2017-12-08 04:34:50 +08:00
Murphy Berzish	9554723b44	use safer mk_and in extended indexof	2017-12-06 20:50:03 -05:00
Nikolaj Bjorner	39d1ad3edb	fix #1390 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-12-07 05:15:53 +05:30
Murphy Berzish	a5c828f6f2	length estimation	2017-12-06 18:32:11 -05:00
Murphy Berzish	fbe8d1577e	new regex automata start; add complexity estimation	2017-12-04 18:05:00 -05:00
Murphy Berzish	b3ebcfe558	correctly check third argument of str.indexof in theory_str	2017-11-29 18:20:59 -05:00