zhengqunkoo / hipsleek Goto Github PK
View Code? Open in Web Editor NEWThis project forked from hipsleek/hipsleek
hipsleek's Issues
Analysis of entailments with issues
The following table shows results of ./sleek -dre="compute_pretty_actions\|isFailCtx" --pnum <pnum> <filename> | ./remove-aliases.py | less, at commit 5edb3fc.
If table is too wide, please scroll horizontally.
<pnum> |
checkentail | search | comments | <filename> |
issue | function@call | entailment | pretty entailment | simplified pretty entailment |
|---|---|---|---|---|---|---|---|---|---|
15 |
checkentail x::arr_seg<5> & y=x+1 |- x::arr_seg<1> * y::int_arr_seg<1>. |
SEARCH =>[COND =>[BaseCaseFold, UnmatchedRHSData]] |
Unable to instantiate q_293=1+x, b_291=4, a_292=1. Unable to either indirectly fold int_arr_seg<1> into arr_seg<4>, or do so directly via lemma "int2char". |
testcases/ex5c.slk |
Expecting(3)Valid BUT got : Fail_May | compute_pretty_actions@14 |
q_293::arr_seg<b_291>@M & flted_156_270=b_291+a_292 & a_292+x=q_293 & Univ(b_291) & Univ(a_292) & Univ(q_293) & y=1+x & flted_156_270=5 |- y::int_arr_seg<flted_157_288>@M & flted_157_289=1 & flted_157_288=1 |
q_293::arr_seg<b_291>@M & a_292+x=q_293 & Univ(b_291) & Univ(a_292) &Univ(q_293) & b_291+a_292=5 |- 1+x::int_arr_seg<1>@M |
1+x::arr_seg<4>@M & Univ(1+x) |- 1+x::int_arr_seg<1>@M |
16 |
checkentail x::arr_seg<4*n+1> & y=x+4*n |- x::arr_seg<4*n> * y::arr_seg<1>. |
SEARCH =>[SEARCH =>[COND =>[Match, COND =>[BaseCaseFold, BaseCaseUnfold]], (Lemma 0==> splitchar_left), (Lemma 0<== splitchar_left_right)]] |
Entailment is due to function@call compute_pretty_actions@7 with action (Lemma 0<== int2char_left_right) on LHS: x::arr_seg<1+(4*n)>@M and RHS: x::int_arr_seg<n_289>@M, which should give x::arr_seg<1+(4*n)>@M |- x::arr_seg<4*n>@M * (4*n)+x::arr_seg<1>@M, but (4*n)+x::arr_seg<1>@M is missing from the pretty entailment. This missing heap state appears to be a cosmetic error, since function@call compute_pretty_actions@32 attempts to prove (4*n)+x::arr_seg<1>@M. |
testcases/ex5c.slk |
NA | compute_pretty_actions@10 |
x::arr_seg<flted_166_270>@M & flted_166_270=1+(4*n) & y=(4*n)+x |- x::arr_seg<flted_16_296>@M & flted_16_296=4*n_289 |
x::arr_seg<1+(4*n)>@M |- x::arr_seg<4*n_289>@M |
NA |
16 |
checkentail x::arr_seg<4*n+1> & y=x+4*n |- x::arr_seg<4*n> * y::arr_seg<1>. |
SEARCH =>[SEARCH =>[COND =>[Match, COND =>[BaseCaseFold, BaseCaseUnfold]], (Lemma 0==> splitchar_left), (Lemma 0<== splitchar_left_right)]] |
Unable to instantiate q_302=(4*n)+x, b_300=1, n_289=n. Fails since n_289=n is unprovable, since the antecedent does not have Univ(n_289). It is likely that isFailCtx@33 explains exactly why n_289=n cannot be proved. |
testcases/ex5c.slk |
Expecting(3)Valid BUT got : Fail_May | compute_pretty_actions@32 |
q_302::arr_seg<b_300>@M & a_301=4*n_289 & y=(4*n)+x & flted_166_270=1+(4*n) & Univ(q_302) & Univ(a_301) & Univ(b_300) & a_301+x=q_302 & flted_166_270=b_300+a_301 |- y::arr_seg<flted_167_290>@M & flted_167_290=1 & n_289=n |
q_302::arr_seg<b_300>@M & 4*n_289=4*n & Univ(q_302) &Univ(4*n_289) & Univ(b_300) & 4*n_289+x=q_302 & 1+(4*n)=b_300+4*n_289 |- (4*n)+x::arr_seg<1>@M |
4*n+x::arr_seg<1>@M |- (4*n)+x::arr_seg<1>@M |
17 |
checkentail x::arr_seg<4*n+1> & y=x+1 |- x::arr_seg<1> * y::int_arr_seg<n>. |
SEARCH =>[COND =>[BaseCaseFold, UnmatchedRHSData]] |
Unable to instantiate q_293=1+x, b_291=4*n, a_292=1. Fails since n_288=n is unprovable, since the antecedent does not have Univ(n_288). Unable to either indirectly fold int_arr_seg<n> into arr_seg<4*n>, or do so directly via lemma "int2char". |
testcases/ex5c.slk |
Expecting(3)Valid BUT got : Fail_May | compute_pretty_actions@14 |
q_293::arr_seg<b_291>@M & flted_178_270=b_291+a_292 & a_292+x=q_293 & Univ(b_291) & Univ(a_292) & Univ(q_293) & y=1+x & flted_178_270=1+(4*n) |- y::int_arr_seg<n_288>@M & flted_179_289=1 & n_288=n |
q_293::arr_seg<b_291>@M & a_292+x=q_293 & Univ(b_291) & Univ(a_292) &Univ(q_293) & b_291+a_292=1+(4*n) |- 1+x::int_arr_seg<n>@M |
1+x::arr_seg<4*n>@M |- 1+x::int_arr_seg<n>@M |
19 |
checkentail x::arr_seg<6> & y=x+1 & z=y+4 |- x::arr_seg<1> * y::int_arr_seg<1> * z::arr_seg<1>. |
SEARCH =>[COND =>[BaseCaseFold, UnmatchedRHSData]] |
Unable to instantiate q_301=1+x, b_299=5, a_300=1. Instantiation of b_299=5 could be helped if information that a_300=1 were provided. Missing information that a_300=1, which hipsleek should have derived and kept in the pretty entailment due to function@call compute_pretty_actions@13 with action Match on LHS: x::arr_seg<a_300> and RHS: x::arr_seg<1>. |
testcases/ex5c.slk |
Expecting(3)Valid BUT got : Fail_May | compute_pretty_actions@14 |
q_301::arr_seg<b_299>@M & flted_196_270=b_299+a_300 & a_300+x=q_301 & Univ(b_299) & Univ(a_300) & Univ(q_301) & z=4+y & y=1+x & flted_196_270=6 |- y::int_arr_seg<flted_197_296>@M * z::arr_seg<flted_197_295>@M & flted_197_297=1 & flted_197_296=1 & flted_197_295=1 |
q_301::arr_seg<b_299>@M & a_300+x=q_301 & Univ(b_299) & Univ(a_300) &Univ(q_301) & 4+y=4+1+x & b_299+a_300=6 |- 1+x::int_arr_seg<1>@M * 4+y::arr_seg<1>@M |
1+x::arr_seg<5>@M |- 1+x::int_arr_seg<1>@M * 4+1+x::arr_seg<1>@M |
20 |
checkentail x::arr_seg<6> & y=x+2 |- x::arr_seg<2> * y::int_arr_seg<1>. |
SEARCH =>[COND =>[BaseCaseFold, UnmatchedRHSData]] |
Unable to instantiate q_293=2+x, b_291=4, a_292=2. Instantiation of b_291=4 could be helped if information that a_292=2 were provided. Missing information that a_292=2, which hipsleek should have derived and kept in the pretty entailment due to function@call compute_pretty_actions@13 with action Match on LHS: x::arr_seg<a_292> and RHS: x::arr_seg<2>. Unable to either indirectly fold int_arr_seg<1> into arr_seg<4>, or do so directly via lemma "int2char". |
testcases/ex5c.slk |
Expecting(3)Valid BUT got : Fail_May | compute_pretty_actions@14 |
q_293::arr_seg<b_291>@M & flted_204_270=b_291+a_292 & a_292+x=q_293 & Univ(b_291) & Univ(a_292) & Univ(q_293) & y=2+x & flted_204_270=6 |- y::int_arr_seg<flted_205_288>@M & flted_205_289=2 & flted_205_288=1 |
q_293::arr_seg<b_291>@M & a_292+x=q_293 & Univ(b_291) & Univ(a_292) &Univ(q_293) & b_291+a_292=6 |- 2+x::int_arr_seg<1>@M |
2+x::arr_seg<4>@M |- 2+x::int_arr_seg<1>@M |
22 |
checkentail x::arr_seg<4*n+2> & y=x+1 & z=y+4*n |- x::arr_seg<1> * y::int_arr_seg<n> * z::arr_seg<1>. |
SEARCH =>[COND =>[Match, BaseCaseFold, BaseCaseUnfold]] |
Entailment is due to function@call compute_pretty_actions@14 with action (Lemma 0<== int2char_left_right) on LHS: q_302::arr_seg<b_300>@M and RHS: y::int_arr_seg<n_296>@M, which should give 1+x::arr_seg<(4*n)+1>@M & (4*n)+y=(4*n)+1+x |- 1+x::arr_seg<4*n_296>@M * (4*n)+y::arr_seg<1>@M, but (4*n)+y::arr_seg<1>@M is missing from the pretty entailment. |
testcases/ex5c.slk |
Expecting(3)Valid BUT got : Fail_May | compute_pretty_actions@17 |
q_302::arr_seg<b_300>@M & a_301=1 & flted_222_270=2+(4*n) & y=1+x & z=(4*n)+y & Univ(q_302) & Univ(a_301) & Univ(b_300) & a_301+x=q_302 & flted_222_270=b_300+a_301 |- y::arr_seg<flted_16_311>@M & flted_16_311=4*n_296 |
q_302::arr_seg<b_300>@M & (4*n)+y=(4*n)+1+x & Univ(q_302) &Univ(1) & Univ(b_300) & 1+x=q_302 & 2+(4*n)=b_300+1 |- 1+x::arr_seg<4*n_296>@M |
1+x::arr_seg<(4*n)+1>@M & (4*n)+y=(4*n)+1+x |- 1+x::arr_seg<4*n_296>@M |
23 |
checkentail x::arr_seg<4*n+2> & y=x+2 |- x::arr_seg<2> * y::int_arr_seg<n>. |
SEARCH =>[COND =>[BaseCaseFold, UnmatchedRHSData]] |
Unable to instantiate q_293=2+x, b_291=4*n, a_292=2. Instantiation of b_291=4*n could be helped if information that a_292=2 were provided. Missing information that a_292=2, which hipsleek should have derived and kept in the pretty entailment due to function@call compute_pretty_actions@13 with action Match on LHS: x::arr_seg<a_292> and RHS: x::arr_seg<2>. Unable to either indirectly fold int_arr_seg<n> into arr_seg<4*n>, or do so directly via lemma "int2char". Fails since n_288=n is unprovable, since the antecedent does not have Univ(n_288). |
testcases/ex5c.slk |
Expecting(3)Valid BUT got : Fail_May | compute_pretty_actions@14 |
q_293::arr_seg<b_291>@M & flted_230_270=b_291+a_292 & a_292+x=q_293 & Univ(b_291) & Univ(a_292) & Univ(q_293) & y=2+x & flted_230_270=2+(4*n) |- y::int_arr_seg<n_288>@M & flted_231_289=2 & n_288=n |
q_293::arr_seg<b_291>@M & a_292+x=q_293 & Univ(b_291) & Univ(a_292) &Univ(q_293) & b_291+a_292=2+(4*n) |- 2+x::int_arr_seg<n>@M |
2+x::arr_seg<4*n>@M |- 2+x::int_arr_seg<n>@M |
13 |
checkentail a::aseg<a+3> & b=a+1 & c=b+1 |- a::aseg<b> * b::int_star<v> * c::aseg<a+3>. |
SEARCH =>[UnmatchedRHSData] |
Either unable to instantiate k_268=1 or unable to instantiate v_278=v. Claims 1+a::int_star<v>@M is UnmatchedRHSData when it is not. |
testcases/exist-arrays.slk |
satisfiable state became hfalse | compute_pretty_actions@90 |
b_269::int_star<v_270>@M * c_268::aseg<flted_17_275>@M & flted_17_275=n_266+a & flted_123_105=n_266+a & b_269=k_267+a & c_268=1+b_269 & Univ(v_270) & Univ(n_266) & Univ(k_267) & Univ(c_268) & Univ(b_269) & Univ(v_270) & c=1+b & b=1+a & flted_123_105=3+a |- b::int_star<v>@M * c::aseg<flted_123_126>@M & flted_123_126=3+a & b_125=b |
k_268+a::int_star<v_278>@M * 1+b_270::aseg<n_267+a>@M &1+b_270=1+k_268+a & Univ(v_278) & Univ(n_267) & Univ(k_268) & Univ(1+b_270) & Univ(k_268+a) & n_267+a=3+a |- 1+a::int_star<v>@M * 1+1+a::aseg<3+a>@M |
1+a::int_star<v_278>@M * 1+1+a::aseg<3+a>@M & Univ(v_278) |- 1+a::int_star<v>@M * 1+1+a::aseg<3+a>@M |
16 |
checkentail a::aseg<a+4> & b=a+1 & c=b+1 |- a::aseg<b> * b::int_star<v> * c::aseg<a+4>. |
SEARCH =>[UnmatchedRHSData] |
Either unable to instantiate k_270=1 or unable to instantiate v_280=v. Claims 1+a::int_star<v>@M is UnmatchedRHSData when it is not. |
testcases/exist-arrays.slk |
satisfiable state became hfalse | compute_pretty_actions@92 |
b_270::int_star<v_271>@M * c_269::aseg<flted_17_276>@M & flted_17_276=n_267+a & flted_144_105=n_267+a & b_270=k_268+a & c_269=1+b_270 & Univ(v_271) & Univ(n_267) & Univ(k_268) & Univ(c_269) & Univ(b_270) & Univ(v_271) & c=1+b & b=1+a & flted_144_105=4+a |- b::int_star<v>@M * c::aseg<flted_144_126>@M & flted_144_126=4+a & b_125=b |
k_270+a::int_star<v_280>@M * 1+b_272::aseg<n_269+a>@M & Univ(v_280) &1+b_272=1+k_270+a & Univ(n_269) & Univ(k_270) & Univ(1+b_272) & Univ(k_270+a) & n_269+a=4+a |- 1+a::int_star<v>@M * 1+1+a::aseg<4+a>@M |
1+a::int_star<v_280>@M * 1+1+a::aseg<4+a>@M & Univ(v_280) |- 1+a::int_star<v>@M * 1+1+a::aseg<4+a>@M |
17 |
checkentail a::aseg<a+4> & b=a+2 & c=b+1 |- a::aseg<b> * b::int_star<v> * c::aseg<a+4>. |
SEARCH =>[UnmatchedRHSData] |
Either unable to instantiate k_157=2 or unable to instantiate v_142=v. Claims 3+a::int_star<v>@M is UnmatchedRHSData when it is not. |
testcases/exist-arrays.slk |
satisfiable state became hfalse | compute_pretty_actions@24 |
b_163::int_star<v_164>@M * c_162::aseg<flted_17_169>@M & flted_17_169=n_160+a & flted_151_105=n_160+a & b_163=k_161+a & c_162=1+b_163 & Univ(v_164) & Univ(n_160) & Univ(k_161) & Univ(c_162) & Univ(b_163) & Univ(v_164) & c=1+b & b=2+a & flted_151_105=4+a |- b::int_star<v>@M * c::aseg<flted_151_126>@M & flted_151_126=4+a & b_125=b |
k_157+a::int_star<v_160>@M * 1+b_159::aseg<n_156+a>@M &1+b_159=1+k_157+a & Univ(v_160) & Univ(n_156) & Univ(k_157) & Univ(1+b_159) &Univ(k_157+a) & Univ(v_160) & n_156+a=4+a |- 2+a::int_star<v>@M * 1+2+a::aseg<4+a>@M |
2+a::int_star<v_160>@M * 1+2+a::aseg<4+a>@M & Univ(v_160) |- 2+a::int_star<v>@M * 1+2+a::aseg<4+a>@M |
18 |
checkentail a::aseg<a+4> & b=a+3 |- a::aseg<b> * b::int_star<v>. |
SEARCH =>[UnmatchedRHSData] |
Either unable to instantiate k_132=3 or unable to instantiate v_142=v. Claims 3+a::int_star<v>@M is UnmatchedRHSData when it is not. |
testcases/exist-arrays.slk |
Expecting(3)Valid BUT got : Fail_May | compute_pretty_actions@15 |
b_143::int_star<v_144>@M * c_142::aseg<flted_17_149>@M & flted_17_149=n_140+a & flted_158_105=n_140+a & b_143=k_141+a & c_142=1+b_143 & Univ(v_144) & Univ(n_140) & Univ(k_141) & Univ(c_142) & Univ(b_143) & Univ(v_144) & b=3+a & flted_158_105=4+a |- b::int_star<v>@M & b_118=b |
k_132+a::int_star<v_142>@M * 1+b_134::aseg<n_131+a>@M &1+b_134=1+k_132+a & Univ(v_142) & Univ(n_131) & Univ(k_132) & Univ(1+b_134) & Univ(k_132+a) & n_131+a=4+a |- 3+a::int_star<v>@M |
3+a::int_star<v_142>@M * 1+3+a::aseg<4+a>@M & Univ(v_142) |- 3+a::int_star<v>@M |
Fix of #1 is incomplete
issues-1.slk.iget_answer.rec at commit c937a7f probably has the correct ouput by chance, because 2e37560 has a bug that is not manifested: when (reset) is used, the input to Z3 is, given by new_f at line
Line 751 in 2e37560
(push)
(reset)
;Variables declarations
(declare-fun n () Int)
(declare-fun f () Int)
;Relations declarations
;Axioms assertions
;Antecedent
(assert (< 1 n))
(assert (= (+ (+ 1 f) 1) (+ n n)))
(assert (<= 2 f))
;Negation of Consequence
(assert (not (exists ((alpha_134 Int)) (= (* 2 alpha_134) f))))
(check-sat)(pop)
on which running z3 -smt2 gives:
unsat
(error "line 14 column 15: invalid pop command, argument is greater than the current stack depth")
which could have unintended consequences. The solution is to remove (push) and (pop) from new_f whenever (reset) is used. A similar problem likely manifests at new_f at line
Line 1313 in 2e37560
Check if wrapper in koo/wrap_remove_univ_rhs is invoked in hip
Wrapper is known to work in sleek, but it is yet unknown if it works in hip.
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.