Thai Trinh
|
cd62017afd
|
fixed failures with regression tests
|
2018-06-30 15:52:20 +08:00 |
|
Lev Nachmanson
|
da44ad7e6f
|
added stubs for get_lower/get_upper required by theory_seq
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2018-06-29 13:43:23 -07:00 |
|
Thai Trinh
|
1892d31794
|
add parameter to enable splitting guided by length constraints
|
2018-06-27 18:10:40 +08:00 |
|
Thai Trinh
|
aacb7289be
|
merge with Z3Prover/master
|
2018-06-25 19:44:46 +08:00 |
|
Nikolaj Bjorner
|
eeba30a277
|
fix #1677
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-06-19 10:56:45 -07:00 |
|
Nikolaj Bjorner
|
b4aac1ab55
|
revert fix to #1677
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-06-18 21:23:13 -07:00 |
|
Nikolaj Bjorner
|
6a0b70ee5c
|
selective expansion of strings for canonizer to fix #1690 regression
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-06-18 20:42:53 -07:00 |
|
Nikolaj Bjorner
|
4634d1daed
|
selective expansion of strings for canonizer to fix #1690 regression
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-06-18 20:37:39 -07:00 |
|
Nikolaj Bjorner
|
c3b27903f8
|
fix #1677
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-06-18 11:22:01 -07:00 |
|
Nikolaj Bjorner
|
1e143971c3
|
tune for unit test, delay initialize re-solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-05-13 11:49:33 -07:00 |
|
Nikolaj Bjorner
|
b5f067bec5
|
fix #1592 #1587
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-04-25 11:18:24 +02:00 |
|
Nikolaj Bjorner
|
19bb883263
|
fix #1581
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-04-23 12:12:39 +02:00 |
|
Nikolaj Bjorner
|
279f1986a6
|
fix #1575, fix #1585
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-04-23 07:11:15 +02:00 |
|
Nikolaj Bjorner
|
72f8e408fc
|
fix #1538
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-17 11:25:07 -07:00 |
|
Nikolaj Bjorner
|
eb1122c5cb
|
delay updating parameters to ensure rewriting in asserted_formulas is applied using configuration overrides. Fixes build regression for tree_interpolation documentation test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-04 21:57:08 -08:00 |
|
Nikolaj Bjorner
|
ce1b135ec3
|
address accessor inconsistencies between - and from #1506
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-02-26 14:57:17 +09:00 |
|
Nikolaj Bjorner
|
7b68be75c9
|
fixes to #1500 and #1457
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-02-25 13:11:20 +09:00 |
|
Bruce Mitchener
|
76eb7b9ede
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
Bruce Mitchener
|
7167fda1dc
|
Use override rather than virtual.
|
2018-02-10 09:56:33 +07:00 |
|
Nikolaj Bjorner
|
61934d8106
|
align semantics of re.allchar with string proposal. #1475
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-02-07 20:08:15 -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 |
|
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 |
|
Thai Trinh
|
c07a63cf8e
|
coalesce seq.unit into string in mk_skolem
|
2017-12-12 05:00:34 +08: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
|
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 |
|
Thai Trinh
|
ff567412c1
|
Simplify code
|
2017-12-08 14:26:20 +08:00 |
|
Thai Trinh
|
b6806eb1c2
|
Add more splitting rules for string equations (including rules based on length constraints)
|
2017-12-08 04:34:50 +08:00 |
|
Nikolaj Bjorner
|
39d1ad3edb
|
fix #1390
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-12-07 05:15:53 +05:30 |
|
Nikolaj Bjorner
|
bfe6260c58
|
fix #1376
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-27 08:39:20 -08:00 |
|
Nikolaj Bjorner
|
7d693a5f9f
|
fix different bug reported on #1366
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-25 20:01:14 -08:00 |
|
Nikolaj Bjorner
|
841c48e04d
|
fix break
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-25 18:24:45 -08:00 |
|
Nikolaj Bjorner
|
77b74ddb88
|
fix #1366
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-25 17:55:20 -08:00 |
|
Nikolaj Bjorner
|
d520557ad9
|
fix #1233
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-21 11:52:15 -08:00 |
|
Nikolaj Bjorner
|
c5f231acdf
|
debugging #1233
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-21 08:16:41 -08:00 |
|
Nikolaj Bjorner
|
42fbe19814
|
fix #1316, segmentation fault when numeric value is not internalized
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-10-21 18:56:36 -04:00 |
|
Nikolaj Bjorner
|
4d8290ebc2
|
update to theory_seq following examples from PJLJ
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-30 14:04:02 -07:00 |
|
Nikolaj Bjorner
|
974eaab01c
|
complement regular expressions when used in negated membership constraints #1224
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-28 01:38:23 -07:00 |
|
Nikolaj Bjorner
|
ebe9db14d5
|
fix regression exposed by segfault2.smt2 crash
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-21 14:13:43 -07:00 |
|
Nikolaj Bjorner
|
276fdd0e97
|
register auxiliary constants from projection operation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-20 08:51:24 -07:00 |
|
Nikolaj Bjorner
|
ead704f52f
|
handle undefined constant cases for int.to.str
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-13 17:13:10 -07:00 |
|
Nikolaj Bjorner
|
19bb55e396
|
recognize theory_i_arith to fix #1200
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-13 10:22:36 -07:00 |
|