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 |
|
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 |
|
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
|
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
|
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 |
|
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 |
|
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 |
|
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 |
|
Nikolaj Bjorner
|
2749e547cf
|
fix c example, remove more smtlib1 printing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-28 18:14:24 -08:00 |
|
Nikolaj Bjorner
|
d7042c234f
|
fix #1371
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-28 09:34:44 -08:00 |
|
Nikolaj Bjorner
|
2b3ee995ff
|
fix #1375
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-27 09:03:52 -08:00 |
|
Nikolaj Bjorner
|
bfe6260c58
|
fix #1376
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-27 08:39:20 -08:00 |
|
Nikolaj Bjorner
|
4520fafa8c
|
fix #1368
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-26 19:13:35 -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
|
441c0de3c8
|
Merge branch 'master' of https://github.com/z3prover/z3
|
2017-11-23 11:17:58 -08:00 |
|
Nikolaj Bjorner
|
357b4b20fd
|
fix #1365. Filter MBQI instantiations for as-array terms that lead the array theory to return unknown and therefore block further instantiations. as-array terms are at this point almost always created from internal model values so quantifier instantiations with these have little value, other than instantiations of other paraameters that may indepdendently help
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-23 11:17:41 -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
|
33e8113c9e
|
adding instrumentation to debug #1233
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-20 16:51:17 -08:00 |
|
Nikolaj Bjorner
|
2e6ae8cfd2
|
fix crash
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-15 23:06:05 -08:00 |
|
Nikolaj Bjorner
|
c3364f17fa
|
fix infinite loop in traversing equivalence class, #1274, still requires addressing MBQI
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-15 21:19:22 -08:00 |
|
Nikolaj Bjorner
|
c3f67f3b5f
|
fix infinite loop in traversing equivalence class, #1274, still requires addressing MBQI
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-15 21:17:00 -08:00 |
|
Nikolaj Bjorner
|
9d3518736b
|
fix #889
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-06 15:25:10 -08:00 |
|
Nikolaj Bjorner
|
53ed1bb862
|
fix segfault reported as part of #1241
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-06 02:05:00 -08:00 |
|
Murphy Berzish
|
2d25355611
|
Merge remote-tracking branch 'upstream/master' into issue1274-crash
|
2017-10-31 17:07:54 -04:00 |
|
Nikolaj Bjorner
|
24a44a0b29
|
Merge pull request #1336 from mtrberzi/clean-rewriter-patch
fix rewriter in theory_str
|
2017-10-31 08:45:14 -07:00 |
|
Nikolaj Bjorner
|
29d643cc23
|
Merge pull request #1337 from mtrberzi/fix-length-testing
Optimizations for length testing in theory_str
|
2017-10-30 12:00:47 -07:00 |
|