hflmc2's People
Forkers
kamocychflmc2's Issues
Fpat cannot solve HCCS
Input
%HES
S n =v Twice n Neg (Eq n).
Twice m f k =v f m (F m f k).
F m f k l =v f l k.
Neg a h =v h (- a).
Eq c d =v c = d.
Output:
Fpat.BwIPHCCSSolver.solve
- Raise
Unknown
- Raise
Fpat.(GenHCCSSolver.solve (CHGenInterpProver.interpolate b))
- Raise
NoSolution
- Raise
Fpat.FwHCCSSolver.solve_simp
gives me a solution but this solver is not so good at finding proper predicates.
Following HCCS is generated by hflmc2
:
_|_
<= P[S:0](n), n = n
P[S:0](n)
<= P[Twice](m), m = n
P[Twice](m)
<= P[f1](m, x1), x1 = m
P[f1](m, x1)
<= P[Neg1](a1), m = n, x1 = m, a1 = x1
P[Neg1](a1)
<= P[h1:0](a1, b1), b1 = 0 - a1
P[h1:0](a1, b1)
<= P[g1:0](m, x1, y1),
a1 = x1, m = n, x1 = m, b1 = 0 - a1, y1 = b1
P[g1:0](m, x1, y1)
<= P[F](m_, l_),
x1 = m, x1 = m && y1 = 0 - x1, m_ = m, l_ = y1
P[F](m_, l_)
<= P[f_:0](m_, x_), x_ = l_
P[f_:0](m_, x_)
<= P[f2](m, x2),
m_ = m, x1 = m, x1 = m && y1 = 0 - x1, x2 = x_
P[f2](m, x2)
<= P[Neg2](a2), m = n, a2 = x2
P[Neg2](a2)
<= P[h2:0](a2, b2), b2 = 0 - a2
P[h2:0](a2, b2)
<= P[g2:0](m, x2, y2),
a2 = x2, m = n, b2 = 0 - a2, y2 = b2
P[g2:0](m, x2, y2)
<= P[g_:0](m_, x_, y_),
x2 = x_, m_ = m, x1 = m, x1 = m && y1 = 0 - x1, y2 = 0 - x2, y_ = y2
P[g_:0](m_, x_, y_)
<= P[k_:0](m_, z_), x_ = l_, z_ = y_
P[k_:0](m_, z_)
<= P[k:0](m, z),
m_ = m, x1 = m, x1 = m && y1 = 0 - x1, z = z_
P[k:0](m, z)
<= P[Eq](c, d), m = n, c = n, d = z
P[Eq](c, d)
<= c /= d
Assert failure in hflmc2_refine.ml
Input:
%HES
Sentry =ν exi_x196 < 1 || Exists exi_x196.
Exists exi_x217 =ν
(exi_r278 < 1
|| exi_r278 < 1 * exi_x217 || exi_r278 < -1 * exi_x217 || F_0_ff_ap_ exi_x217 exi_r278
|| exi_r279 < 1
|| exi_r279 < 1 * -exi_x217 || exi_r279 < -1 * -exi_x217 || F_0_ff_ap_ (-exi_x217) exi_r279
|| Exists (exi_x217 - 1))
&& exi_x217 >= 0.
F_0_tt x2210 =ν
exi_r2311 < 1 || exi_r2311 < 1 * x2210 || exi_r2311 < -1 * x2210 || F_0_tt_ap_ x2210 exi_r2311.
F_0_tt_ap_ x2412 exi_r2513 =ν
((x2412 >= 0
&& rec_G_1_ff_13214 < 1 + 1 * exi_r2513
|| rec_G_1_ff_13214 < 1 + -1 * exi_r2513
|| rec_G_1_ff_13214 < 1 + 1 * (x2412 - 1)
|| rec_G_1_ff_13214 < 1 + -1 * (x2412 - 1)
|| rec_G_1_ff_13214 < 1 || G_1_ff_1 rec_G_1_ff_13214 (x2412 - 1) exi_r2513
|| x2412 < 0 && exi_r2513 = 5)
&& F_0_tt exi_r2513
|| (x2412 >= 0
&& rec_G_1_ff_13215 < 1 + 1 * -exi_r2513
|| rec_G_1_ff_13215 < 1 + -1 * -exi_r2513
|| rec_G_1_ff_13215 < 1 + 1 * (x2412 - 1)
|| rec_G_1_ff_13215 < 1 + -1 * (x2412 - 1)
|| rec_G_1_ff_13215 < 1 || G_1_ff_1 rec_G_1_ff_13215 (x2412 - 1) (-exi_r2513)
|| x2412 < 0 && -exi_r2513 = 5)
&& F_0_tt (-exi_r2513)
|| F_0_tt_ap_ x2412 (exi_r2513 - 1))
&& exi_r2513 >= 0.
F_0_ff_ap_ x2816 exi_r2917 =ν
((x2816 >= 0
&& rec_G_1_ff_13218 < 1 + 1 * exi_r2917
|| rec_G_1_ff_13218 < 1 + -1 * exi_r2917
|| rec_G_1_ff_13218 < 1 + 1 * (x2816 - 1)
|| rec_G_1_ff_13218 < 1 + -1 * (x2816 - 1)
|| rec_G_1_ff_13218 < 1 || G_1_ff_1 rec_G_1_ff_13218 (x2816 - 1) exi_r2917
|| x2816 < 0 && exi_r2917 = 5)
&& F_0_tt exi_r2917
|| (x2816 >= 0
&& rec_G_1_ff_13219 < 1 + 1 * -exi_r2917
|| rec_G_1_ff_13219 < 1 + -1 * -exi_r2917
|| rec_G_1_ff_13219 < 1 + 1 * (x2816 - 1)
|| rec_G_1_ff_13219 < 1 + -1 * (x2816 - 1)
|| rec_G_1_ff_13219 < 1 || G_1_ff_1 rec_G_1_ff_13219 (x2816 - 1) (-exi_r2917)
|| x2816 < 0 && -exi_r2917 = 5)
&& F_0_tt (-exi_r2917)
|| F_0_ff_ap_ x2816 (exi_r2917 - 1))
&& exi_r2917 >= 0.
G_1_ff_1 rec_G_1_ff_13320 x3421 r3522 =ν
rec_G_1_ff_13320 > 0
&& (x3421 >= 0 && G_1_ff_1 (rec_G_1_ff_13320 - 1) (x3421 - 1) r3522 || x3421 < 0 && r3522 = 5).
Running hflmc2 input.hes
gives me the error below:
Uncaught exception:
"Assert_failure lib/refine/hflmc2_refine.ml:408:34"
Raised at file "lib/refine/hflmc2_refine.ml", line 408, characters 34-46
Called from file "src/list.ml", line 325, characters 13-17
Called from file "src/list.ml", line 557, characters 34-40
Called from file "lib/refine/hflmc2_refine.ml", line 405, characters 22-275
Called from file "lib/refine/hflmc2_refine.ml", line 340, characters 16-46
Called from file "lib/refine/hflmc2_refine.ml", line 340, characters 16-46
Called from file "lib/refine/hflmc2_refine.ml", line 340, characters 16-46
Called from file "lib/refine/hflmc2_refine.ml", line 353, characters 51-81
Called from file "lib/refine/hflmc2_refine.ml", line 369, characters 31-44
Called from file "lib/refine/hflmc2_refine.ml", line 12, characters 10-14
Called from file "lib/refine/traceVar.ml", line 67, characters 10-14
Called from file "lib/refine/hflmc2_refine.ml", line 350, characters 20-1023
Called from file "lib/refine/hflmc2_refine.ml", line 340, characters 16-46
Called from file "lib/refine/hflmc2_refine.ml", line 340, characters 16-46
Called from file "lib/refine/hflmc2_refine.ml", line 340, characters 16-46
Called from file "lib/refine/hflmc2_refine.ml", line 568, characters 18-76
Called from file "lib/refine/hflmc2_refine.ml", line 340, characters 16-46
Called from file "lib/refine/hflmc2_refine.ml", line 568, characters 18-76
Called from file "lib/refine/hflmc2_refine.ml", line 590, characters 11-58
Called from file "lib/refine/hflmc2_refine.ml", line 606, characters 39-57
Called from file "lib/hflmc2.ml", line 28, characters 15-19
Called from file "lib/hflmc2.ml", line 40, characters 16-30
Called from file "lib/hflmc2.ml", line 146, characters 24-101
Called from file "lib/hflmc2.ml", line 177, characters 4-52
Called from file "bin/main.ml", line 14, characters 16-32
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.