Account Options

  1. Sign in
The old Google Groups will be going away soon, but your browser is incompatible with the new version.
Google Groups Home
« Groups Home
stp-users
Home
About this group
Apply for group membership
Non terminating STP
Options
There are currently too many topics in this group that display first. To make this topic appear first, remove this option from another topic.
There was an error processing your request. Please try again.
flag
   4 messages - Collapse all  -  Translate all to Translated (View all originals)
The group you are posting to is a Usenet group. Messages posted to this group will make your email address visible to anyone on the Internet.
Your reply message has not been sent.
Your post was successful
 
From:
To:
Cc:
Followup To:
Add Cc | Add Followup-to | Edit Subject
Subject:
Validation:
For verification purposes please type the characters you see in the picture below or the numbers you hear by clicking the accessibility icon. Listen and type the numbers you hear
 
Guancio  
View profile  
 More options May 15 2012, 4:30 am
From: Guancio <guan...@gmail.com>
Date: Tue, 15 May 2012 01:30:13 -0700 (PDT)
Local: Tues, May 15 2012 4:30 am
Subject: Non terminating STP
Print | Individual message | Show original | Report this message | Find messages by this author
Dear all,
I'm starting to experimenting the usage of STP as component for
assembly verification.
I'm running STP with the following input file, but it not terminates.
There is some problem in my input program?

Regards

Roberto Guanciale

% free variables:
R_EBP_0 : BITVECTOR(32);
mem_296 : ARRAY BITVECTOR(32) OF BITVECTOR(8);
% end free variables.

ASSERT(
(LET yvalue =((((0bin000000000000000000000000 @ mem_296[BVPLUS(32,

BVPLUS(32,

R_EBP_0,

0hexfffffff8),

0hex00000000)])|
                     (((0bin000000000000000000000000 @ mem_296[
                                                       BVPLUS(32,
BVPLUS(32,

R_EBP_0,

0hexfffffff8),
                                                       0hex00000001)])
<< 8)[31:0]))|
                    (((0bin000000000000000000000000 @
mem_296[BVPLUS(32,

BVPLUS(32,

R_EBP_0,

0hexfffffff8),

0hex00000002)]) << 16)[31:0]))|
                   (((0bin000000000000000000000000 @
mem_296[BVPLUS(32,

BVPLUS(32,

R_EBP_0,

0hexfffffff8),

0hex00000003)]) << 24)[31:0])) IN
(LET xvalue =((((0bin000000000000000000000000 @ mem_296[BVPLUS(32,

BVPLUS(32,

R_EBP_0,

0hex00000010),

0hex00000000)])|
                     (((0bin000000000000000000000000 @ mem_296[
                                                       BVPLUS(32,
BVPLUS(32,

R_EBP_0,

0hex00000010),
                                                       0hex00000001)])
<< 8)[31:0]))|
                    (((0bin000000000000000000000000 @
mem_296[BVPLUS(32,

BVPLUS(32,

R_EBP_0,

0hex00000010),

0hex00000002)]) << 16)[31:0]))|
                   (((0bin000000000000000000000000 @
mem_296[BVPLUS(32,

BVPLUS(32,

R_EBP_0,

0hex00000010),

0hex00000003)]) << 24)[31:0])) IN
(LET sqvalue =((((0bin000000000000000000000000 @ mem_296[BVPLUS(32,

BVPLUS(32,

R_EBP_0,

~0hex00000003),

0hex00000000)])|
                     (((0bin000000000000000000000000 @ mem_296[
                                                       BVPLUS(32,
BVPLUS(32,

R_EBP_0,

~0hex00000003),
                                                       0hex00000001)])
<< 8)[31:0]))|
                    (((0bin000000000000000000000000 @
mem_296[BVPLUS(32,

BVPLUS(32,

R_EBP_0,

~0hex00000003),

0hex00000002)]) << 16)[31:0]))|
                   (((0bin000000000000000000000000 @
mem_296[BVPLUS(32,

BVPLUS(32,

R_EBP_0,

~0hex00000003),

0hex00000003)]) << 24)[31:0])) IN
(LET y1 = BVPLUS(32, yvalue, 0hex00000001) IN
        BVSLE(sqvalue, xvalue)
         AND
         sqvalue = BVMULT(32, y1, y1)
        AND
        BVSLE(BVMULT(32, yvalue, yvalue), xvalue)
)
))));

QUERY(
0bin1 =
(LET temp_82_0 = BVPLUS(32, R_EBP_0,0hexfffffff8) IN
(LET t_78_83_1 =
                  (LET loadnorm_297_2 = mem_296 IN
                  ((((0bin000000000000000000000000 @
loadnorm_297_2[BVPLUS(32,

temp_82_0,

0hex00000000)])|
                    (((0bin000000000000000000000000 @ loadnorm_297_2[
                                                      BVPLUS(32,
temp_82_0,
                                                      0hex00000001)])
<< 8)[31:0]))|
                   (((0bin000000000000000000000000 @
loadnorm_297_2[BVPLUS(32,

temp_82_0,

0hex00000002)]) << 16)[31:0]))|
                  (((0bin000000000000000000000000 @
loadnorm_297_2[BVPLUS(32,

temp_82_0,

0hex00000003)]) << 24)[31:0])))
                  IN
(LET mem_300_3 =
                  (LET tempval_299_4 = BVPLUS(32,
t_78_83_1,0hex00000001) IN
                  (LET tempmem_298_5 =
                                        (mem_296 WITH [BVPLUS(32,
temp_82_0,

0hex00000003)] :=
                                        (tempval_299_4 >> 24)[7:0]) IN
                  (LET tempmem_298_6 =
                                        (tempmem_298_5 WITH
[BVPLUS(32,

temp_82_0,

0hex00000002)] :=
                                        (tempval_299_4 >> 16)[7:0]) IN
                  (LET tempmem_298_7 =
                                        (tempmem_298_6 WITH
[BVPLUS(32,

temp_82_0,

0hex00000001)] :=
                                        (tempval_299_4 >> 8)[7:0]) IN
                  (LET tempmem_298_8 =
                                        (tempmem_298_7 WITH
[BVPLUS(32,

temp_82_0,

0hex00000000)] :=
                                        tempval_299_4[7:0]) IN
                  tempmem_298_8))))) IN
(LET R_EDX_161_9 =
                    BVPLUS(32, (LET loadnorm_301_10 = mem_300_3 IN
                               ((((0bin000000000000000000000000 @
loadnorm_301_10[

BVPLUS(32,

temp_82_0,

0hex00000000)])|
                                 (((0bin000000000000000000000000 @
loadnorm_301_10[

BVPLUS(32,

temp_82_0,

0hex00000001)]) << 8)[31:0]))|
                                (((0bin000000000000000000000000 @
loadnorm_301_10[

BVPLUS(32,

temp_82_0,

0hex00000002)]) << 16)[31:0]))|
                               (((0bin000000000000000000000000 @
loadnorm_301_10[

BVPLUS(32,

temp_82_0,

0hex00000003)]) << 24)[31:0]))),
                    0hex00000001) IN
(LET T_32t2_82_197_11 = BVMULT(32, R_EDX_161_9,R_EDX_161_9) IN
(LET temp_231_12 = BVPLUS(32, R_EBP_0,0hexfffffffc) IN
(LET mem_304_13 =
                   (LET tempval_303_14 = T_32t2_82_197_11 IN
                   (LET tempmem_302_15 =
                                          (mem_300_3 WITH [BVPLUS(32,

temp_231_12,

0hex00000003)] :=
                                          (tempval_303_14 >> 24)[7:0])
IN
                   (LET tempmem_302_16 =
                                          (tempmem_302_15 WITH
[BVPLUS(32,

temp_231_12,

0hex00000002)] :=
                                          (tempval_303_14 >> 16)[7:0])
IN
                   (LET tempmem_302_17 =
                                          (tempmem_302_16 WITH
[BVPLUS(32,

temp_231_12,

0hex00000001)] :=
                                          (tempval_303_14 >> 8)[7:0])
IN
                   (LET tempmem_302_18 =
                                          (tempmem_302_17 WITH
[BVPLUS(32,

temp_231_12,

0hex00000000)] :=
                                          tempval_303_14[7:0]) IN
                   tempmem_302_18))))) IN
(LET R_EAX_235_19 =
                     (LET loadnorm_305_20 = mem_304_13 IN
                     ((((0bin000000000000000000000000 @
loadnorm_305_20[
                                                        BVPLUS(32,
temp_231_12,

0hex00000000)])|
                       (((0bin000000000000000000000000 @
loadnorm_305_20[
                                                         BVPLUS(32,
temp_231_12,

0hex00000001)]) << 8)[31:0]))|
                      (((0bin000000000000000000000000 @
loadnorm_305_20[
                                                        BVPLUS(32,
temp_231_12,

0hex00000002)]) << 16)[31:0]))|
                     (((0bin000000000000000000000000 @
loadnorm_305_20[
                                                       BVPLUS(32,
temp_231_12,
                                                       0hex00000003)])
<< 24)[31:0])))
                     IN
(LET temp_277_21 =
                    (LET loadnorm_306_22 = mem_304_13 IN
                    ((((0bin000000000000000000000000 @
loadnorm_306_22[
                                                       BVPLUS(32,
temp_82_0,

0hex00000000)])|
                      (((0bin000000000000000000000000 @
loadnorm_306_22[
                                                        BVPLUS(32,
temp_82_0,

0hex00000001)]) << 8)[31:0]))|
                     (((0bin000000000000000000000000 @
loadnorm_306_22[
                                                       BVPLUS(32,
temp_82_0,
                                                       0hex00000002)])
<< 16)[31:0]))|
                    (((0bin000000000000000000000000 @ loadnorm_306_22[
                                                      BVPLUS(32,
temp_82_0,
                                                      0hex00000003)])
<< 24)[31:0])))
                    IN
(LET temp_278_23 = BVPLUS(32, temp_277_21,0hex00000001) IN
(LET goal_295_24 =
                    (IF (R_EAX_235_19=
                     BVMULT(32, temp_278_23,temp_278_23)) THEN 0bin1
ELSE 0bin0 ENDIF&
                    IF (BVSLE(BVMULT(32, temp_277_21,temp_277_21),
                    (LET loadnorm_307_25 = mem_304_13 IN
                    ((((0bin000000000000000000000000 @
loadnorm_307_25[
                                                       BVPLUS(32,
BVPLUS(32,

R_EBP_0,

0hex00000010),

0hex00000000)])|
                      (((0bin000000000000000000000000 @
loadnorm_307_25[
                                                        BVPLUS(32,
BVPLUS(32,

R_EBP_0,

0hex00000010),

0hex00000001)]) << 8)[31:0]))|
                     (((0bin000000000000000000000000 @
loadnorm_307_25[
                                                       BVPLUS(32,
BVPLUS(32,

R_EBP_0,

0hex00000010),
                                                       0hex00000002)])
<< 16)[31:0]))|
                    (((0bin000000000000000000000000 @ loadnorm_307_25[
                                                      BVPLUS(32,
BVPLUS(32,

R_EBP_0,

0hex00000010),
                                                      0hex00000003)])
<< 24)[31:0]))))) THEN 0bin1 ELSE 0bin0 ENDIF)
                    IN
goal_295_24)))))))))))
);
COUNTEREXAMPLE;


 
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.
Trevor Hansen  
View profile  
 More options May 15 2012, 8:40 am
From: Trevor Hansen <trev_abr...@yahoo.com>
Date: Tue, 15 May 2012 05:40:35 -0700 (PDT)
Local: Tues, May 15 2012 8:40 am
Subject: Re: Non terminating STP
Print | Individual message | Show original | Report this message | Find messages by this author

Hi Guancio,

To find out if STP is spending its time doing nothing, or working hard, run it with the command line: -s -t

If nothing happens it's probably trying to parse from the STDIN.

I hope your experiments go well,

Trevor

...

read more »


 
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.
Guancio  
View profile  
 More options May 15 2012, 10:59 am
From: Guancio <guan...@gmail.com>
Date: Tue, 15 May 2012 07:59:45 -0700 (PDT)
Local: Tues, May 15 2012 10:59 am
Subject: Re: Non terminating STP
Print | Individual message | Show original | Report this message | Find messages by this author
Dear Trevor,
STP is not waiting from STDIN, it consume 100% of one of my cores. I
tried the option you suggested and
I attach the corresponding output.

Roberto

[3ms:12M]Printing: input asserts and query: Node size is: 195
Difficulty Initially:28848
[1ms:12M]Printing: After Removing Unconstrained: Node size is: 195
[1ms:12M]Printing: After Establishing Intervals: Node size is: 195
[2ms:12M]Printing: After Constant Bit Propagation: Node size is: 195
[1ms:12M]Printing: after solving: Node size is: 193
Difficulty After Size reducing:28846
[0ms:12M]Printing: after pure substitution: Node size is: 193
[3ms:12M]Printing: after simplification: Node size is: 136
[0ms:12M]Printing: after solving: Node size is: 136
[1ms:12M]Printing: after pure substitution: Node size is: 136
[0ms:12M]Printing: after simplification: Node size is: 136
[0ms:12M]Printing: after solving: Node size is: 136
[1ms:12M]Printing: After Constant Bit Propagation begins: Node size
is: 136
[0ms:12M]Printing: After Establishing Intervals: Node size is: 136
[0ms:12M]Printing: Before SimplifyWrites_Inplace begins: Node size is:
136
[0ms:12M]Printing: after pure substitution: Node size is: 136
[0ms:12M]Printing: after simplification: Node size is: 136
[0ms:12M]Printing: after solving: Node size is: 136
[1ms:12M]Printing: After SimplifyWrites_Inplace: Node size is: 136
[0ms:12M]Printing: After Unconstrained Remove begins: Node size is:
136
Initial Difficulty Score:28846
Final Difficulty Score:32086
Array Sizes:12 :
[0ms:12M]Printing: after transformation: Node size is: 160
SimplifyMap:0:193
SimplifyNegMap:0:193
AlwaysTrueFormSet0:193
MultInverseMap0:193
ReadOverWrite_NewName_Map0:193
NewName_ReadOverWrite_Map0:193
substn_map0:193
[0ms:12M]Printing: Before Constant Bit Propagation begins: Node size
is: 160
Nodes before AIG rewrite:26005
advanced CNF
============================[ Search
Statistics ]==============================
| Conflicts |          ORIGINAL         |          LEARNT          |
Progress |
|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl
|          |
=========================================================================== ====
|       100 |   20555    64688   157959 |    23718      100     31 |
1.358 % |
|       250 |   20555    64688   157959 |    26090      250     26 |
1.358 % |
|       475 |   20555    64688   157959 |    28699      475     76 |
1.358 % |
|       812 |   20555    64688   157959 |    31569      812    108 |
1.358 % |
|      1318 |   20555    64688   157959 |    34726     1318     95 |
1.358 % |
|      2077 |   20555    64688   157959 |    38199     2077     99 |
1.358 % |
|      3216 |   20555    64688   157959 |    42019     3216    119 |
1.358 % |
|      4924 |   20555    64688   157959 |    46221     4924    123 |
1.358 % |
|      7486 |   20555    64688   157959 |    50843     7486    121 |
1.358 % |
|     11330 |   20555    64688   157959 |    55928    11330    129 |
1.358 % |
|     17096 |   20555    64688   157959 |    61520    17096    126 |
1.358 % |

On May 15, 2:40 pm, Trevor Hansen <trev_abr...@yahoo.com> wrote:

...

read more »


 
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.
Guancio  
View profile  
 More options May 15 2012, 3:21 pm
From: Guancio <guan...@gmail.com>
Date: Tue, 15 May 2012 12:21:53 -0700 (PDT)
Local: Tues, May 15 2012 3:21 pm
Subject: Re: Non terminating STP
Print | Individual message | Show original | Report this message | Find messages by this author
Dear Trevor,
I was using the binary version of STP.
After reading the message http://www.mail-archive.com/klee-...@keeda.stanford.edu/msg00154.html
I decided to compile the svn sources. The problem is now solved.

Roberto

On May 15, 4:59 pm, Guancio <guan...@gmail.com> wrote:

...

read more »


 
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.
End of messages
« Back to Discussions « Newer topic     Older topic »

Create a group - Google Groups - Google Home - Terms of Service - Privacy Policy
©2013 Google