An implementation of DataLog using BDD data structures (devel list)

Ashley Sterritt | 3 May 2011 20:11

Basic install problem

Hey guys,
Just ran into a problem while trying to install bddbddb.

1. I downloaded the pre-built JavaBDD binaries for Linux
2. I downloaded (using 'web access' method) and compiled bddbddb, which 
created the .jar
3. I tried running it without setting classpaths explicitly, and it 
failed with:
BDD library is not in classpath!  Cannot find JavaBDD library!

4. I tried various ways of setting the classpath, though the javabdd jar 
is in the same directory, without success
e.g., java -classpath .:javabdd-1.0b2.jar -jar bddbddb.jar

5. I copied the libbuddy.so from the JavaBDD distribution itself into 
the current directory, with the same results.

Am I missing something obvious here?

Thanks,
Ashley

------------------------------------------------------------------------------
WhatsUp Gold - Download Free Network Management Software
The most intuitive, comprehensive, and cost-effective network 
management toolset available today.  Delivers lowest initial 
acquisition cost and overall TCO of any competing solution.
http://p.sf.net/sfu/whatsupgold-sd

headers

Su Zhang | 4 Apr 2011 18:10

where to find fielddomains.pa ?

Hi there,

I downloaded the bddbddb jar file and example datalog input at the official page. However, while I was running the tool, I got the following error script. It claims that fielddomains.pa couldn't be found. However, I couldn't find the file online. Could anyone help me out of this trouble?

$ java -jar bddbddb-full.jar input.P
Initializing BDD library (500000 nodes, cache size 125000, min free 0.2%)
buddy.dll is in use, linking temporary copy /var/folders/gZ/gZFalIWIGEuJUksAjy8KRU+++TM/-Tmp-/buddy2480215492501851966.dll
Could not load BDD package buddy: /private/var/folders/gZ/gZFalIWIGEuJUksAjy8KRU+++TM/-Tmp-/buddy2480215492501851966.dll: no suitable image found. Did find: /private/var/folders/gZ/gZFalIWIGEuJUksAjy8KRU+++TM/-Tmp-/buddy2480215492501851966.dll: mach-o, but wrong architecture
Using BDD library JFactory 1.20
No machine learning library found, learning disabled.
Opening Datalog program "input.P"
Exception in thread "main" java.io.FileNotFoundException: fielddomains.pa (No such file or directory)
    at java.io.FileInputStream.open(Native Method)
    at java.io.FileInputStream.<init>(FileInputStream.java:106)
    at java.io.FileInputStream.<init>(FileInputStream.java:66)
    at java.io.FileReader.<init>(FileReader.java:41)
    at net.sf.bddbddb.Solver.parseDirective(Solver.java:729)
    at net.sf.bddbddb.Solver.parseDatalogLine(Solver.java:631)
    at net.sf.bddbddb.Solver.readDatalogProgram(Solver.java:613)
    at net.sf.bddbddb.Solver.load(Solver.java:365)
    at net.sf.bddbddb.Solver.load(Solver.java:361)
    at net.sf.bddbddb.Solver.main2(Solver.java:448)
    at net.sf.bddbddb.Solver.main(Solver.java:1966)

thanks,

--
Su Zhang
Ph.D Candidate
Computing and Information Sciences
Kansas State University

------------------------------------------------------------------------------
Create and publish websites with WebMatrix
Use the most popular FREE web apps or write code yourself; 
WebMatrix provides all the features you need to develop and 
publish your website. http://p.sf.net/sfu/ms-webmatrix-sf

_______________________________________________
bddbddb-devel mailing list
bddbddb-devel <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/bddbddb-devel

headers

WALA Javascript | 29 Nov 2010 16:12

bddbddb usage query

Hi,
       I am planning to use bddbddb for dataflow analysis of Javascript program. I have already downloaded bddbddb but still not sure how to set it up and use even after going through the PLDI tutorial slides(however the demos were missing there).
      WALA already provide tools to parse the javascript program and express in its own intermediate format. What I intend to do is - spit out the fact/predicates such as pointsTo(v5, h1), heapPointsTo(h4, f9, h2) etc. by WALA say in a txt file and then feed these facts to bddbddb program containing the inference rules. As far as I understood I can define the inference rule according to my necessity. Given a query say pointsTo(v100, h50), the datalog program should decide whether it is true or false. Is this possible ?
        Or the java bytecode has to be provided directly to JOEq compiler and that would produce the facts/predicates from the input program bytecode?
        I would really appreciate if someone can provide a detailed explanation on how the bddbddb works and how should I set it up.

Thanks

------------------------------------------------------------------------------
Increase Visibility of Your 3D Game App & Earn a Chance To Win $500!
Tap into the largest installed PC base & get more eyes on your game by
optimizing for Intel(R) Graphics Technology. Get started today with the
Intel(R) Software Partner Program. Five $500 cash prizes are up for grabs.
http://p.sf.net/sfu/intelisp-dev2dev

_______________________________________________
bddbddb-devel mailing list
bddbddb-devel <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/bddbddb-devel

headers

ebuppies admin | 21 Dec 2009 23:28

eBuppies.com - Offers New Online Dating Site for Black Urban Professionals


 <http://www.ebuppies.com/tellafriend.php>

 December 18, 2009

 <http://www.ebuppies.com/signup.php>

 Dear Friend, <http://www.ebuppies.com>

 eBuppies.com (www.ebuppies.com <http://www.ebuppies.com/signup.php>
) is a new online dating site that is dedicated to providing singles
from all over with the opportunity to connect with other buppy singles
in their local area or anywhere of their choice. 

 More and more buppy singles are going online to connect with others
because going out week after week to nightclubs and bars can be
tiresome, as well as expensive. eBuppies.com makes dating easy by
hosting hundreds of profiles of different singles looking for love.
Buppies can join on a monthly basis for less than they would probably
pay for one night at a nightclub or bar.

 Buppies who are looking for love, romance or just friendship now have
a unique resource that can help them discover their future soul mate:
eBuppies.com. 

 Although high technology drives eBuppies.com, the online dating site
is simple and easy for buppies to navigate. Buppies can register,
browse, search and contact other singles
<http://www.ebuppies.com/signup.php>
at no charge. There is also no charge for buppies to upload a photo
with their profile. A control panel enables buppies to customize
preferences based on their individual requirements. The control panel
also blocks undesired contacts for buppies' convenience.

 The pricing for membership is quite cost effective especially for the
average buppy. By January 31 2010 visitors can sign up for 1 Month and
get 30 Days extra membership exclusively through our THIRTYPLUS
<http://www.ebuppies.com/signup.php>
 promo code.

 For more information, visit www.ebuppies.com.
<http://www.ebuppies.com/signup.php>

 About eBuppies.com:

 eBuppies.com is a new online dating service based in San Francisco.
Its goal is to provide easy and affordable online dating to Black
Urban Professionals by using state of the art chat systems, instant
messaging, and forum technology to satisfy today's evolving online
community demands.

 Terms of use <http://www.ebuppies.com/index.php?page=terms_of_use>

 Contact Info:

 Name: Mr. F. Jackson

 Address: 1230 Market Street, #252

 City: San Francisco

 State: California

 Country: United States

 Zip: 94102

 Web Address: www.ebuppies.com <http://www.ebuppies.com/signup.php>

 Phone: 510-575-4124

 /

 /

 / / <http://www.ebuppies.com/signup.php>

 Site Statistics

 Special Offer!

 			Members in Last Week: 		
 			1 		

 Total Male eBuppies:
 			10 		

 			Total Female eBuppies: 		
 15 		

 Pictures in Last Week: 		
 0 		

 Members online: 		
 0

 News

 Women More Likely to Snoop Than Men

 Nov 24, 2009

 In the new film, Little Black Book, Brittany Murphy's character
engages in some high-tech snooping on her new boyfriend. Based...

 				more <http://www.ebuppies.com/signup.php>

 Internet Dating More Successful than Thought

 Nov 24, 2009

 Internet dating is proving a much more successful way to find
long-term romance and friendship for thousands of people than...

 				more <http://www.ebuppies.com/signup.php>

 			All News <http://www.ebuppies.com/signup.php>

 Poll

 <http://www.ebuppies.com/signup.php>

 Success Stories

 A Sister's Story

 Sep 11, 2009

 by				 			Monique <javascript:popUpScrollWindow2(>

 What initially started out as something to relieve a little boredom
and to have some fun turned into one of...

 more <http://www.ebuppies.com/signup.php>

 All Stories <http://www.ebuppies.com/signup.php>

 <http://www.ebuppies.com/signup.php>

 Welcome to eBuppies.com

 See why eBuppies.com is the fastest growing Black Urban Professional
relationship site on the web. Create your eBuppies.com profile to
begin the exciting journey towards finding your match.

 Members online: 0 <http://www.ebuppies.com/onlineusers.php>

 Don't stay alone, Join Now for Free
<http://www.ebuppies.com/signup.php>

 Newest eBuppies

 							 						kldixson 			 			 <http://www.ebuppies.com/signup.php>

 							 						systemsthinking 			
<http://www.ebuppies.com/signup.php>

 Show full list <http://www.ebuppies.com/signup.php>

 Newest Profiles

 brotherX <http://www.ebuppies.com/signup.php>

 *Age:*
 40

 *Gender:*
 Man

 *Looking for:*
 Woman

 *Location:*
 Albany, 

 California, 

 United States

 <javascript:popUpScrollWindow2(>

 No Pictures

 *Active wihin 1 week*
 View Profile <http://www.ebuppies.com/signup.php>

 kldixon <http://www.ebuppies.com/signup.php>

 *Age:*
 40

 *Gender:*
 Man

 *Looking for:*
 Woman

 *Location:*
 Oakland, 

 California, 

 United States

 <javascript:popUpScrollWindow2(>

 No Pictures

 *Active wihin 1 week*
 View Profile <http://www.ebuppies.com/signup.php>

 Login <http://www.ebuppies.com/signup.php>
 | 				 Privacy <http://www.ebuppies.com/signup.php>
 | 		 Terms of Use <http://www.ebuppies.com/signup.php>
 | 		 Services <http://www.ebuppies.com/signup.php>
 | 		 FAQ's <http://www.ebuppies.com/signup.php>
 | 		 Articles <http://www.ebuppies.com/signup.php>
 | 		 Affiliate <http://www.ebuppies.com/signup.php>
 | 	 Invite a Friend <http://www.ebuppies.com/signup.php>
 | 		 Feedback <http://www.ebuppies.com/signup.php>

<table cellspacing="0" cellpadding="2" border="0" width="100%">
    <tbody>
        <tr>
            <td colspan=3 align=right ><font face="arial,verdana"
size="2">If you do not want to receive any more newsletters, 
http://ebuppies.com/emailserv/?p=unsubscribe&uid=fc949c5b17acfa952ec9ab3be4006bec
To update your preferences and to unsubscribe visit
http://ebuppies.com/emailserv/?p=preferences&uid=fc949c5b17acfa952ec9ab3be4006bec
Forward a Message to Someone
http://ebuppies.com/emailserv/?p=forward&uid=fc949c5b17acfa952ec9ab3be4006bec&mid=20</font></td>
</tr>
        <tr>
            <td><font face="arial,verdana" size="1">CUBEMEDIALAB<br><br />
            1230 Market Street<br>
            Suite 252<br>
            San Francisco, California 94102<br>
            USA<br />
             </font></td><br />
            <td align="right"><a href="http://www.cubemedialab.com"
target="_blank"><img border="0"
src="http://www.ebuppies.com/images/cube_logo.gif" alt="Try digital design
with cubemedialab.com!" /></a></td><br />
        </tr>
    </tbody>
</table>

--
Powered by PHPlist, www.phplist.com --

------------------------------------------------------------------------------
This SF.Net email is sponsored by the Verizon Developer Community
Take advantage of Verizon's best-in-class app development support
A streamlined, 14 day to market process makes app distribution fast and easy
Join now and get one step closer to millions of Verizon customers
http://p.sf.net/sfu/verizon-dev2dev

headers

李进辉 | 3 Mar 2009 09:52

Is there some Tutorial for Bddbddb?

Hi all,

I am so glad to find this open source project! We are building a Static Analysis tool, and after reading J. Whale’s papers, we decided to try points-to analysis and interprocedural analysis with Bddbddb.

But I can’t find something like Tutorial, even the demos in J. Whale’s “PLDITutorial.ppt”.

So, somebody please tell me how to start the analysis or the process of analysis using Bddbddb.

Some resources like tutorial will be great, because files in the cvs repository of sourceforge make no sense to me.

Thanks for your contribution and share.

Look forward for your replies!

------------------------------------------------------------------------------
Open Source Business Conference (OSBC), March 24-25, 2009, San Francisco, CA
-OSBC tackles the biggest issue in open source: Open Sourcing the Enterprise
-Strategies to boost innovation and cut costs with open source participation
-Receive a $600 discount off the registration fee with the source code: SFAD
http://p.sf.net/sfu/XcvMzF8H

_______________________________________________
bddbddb-devel mailing list
bddbddb-devel <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/bddbddb-devel

headers

Suman | 8 Nov 2008 19:25

Thread escape analysis

Hi all,

I am using thread escape analysis from Algorithm 7 in [1][3]. When I tried to run it, I found that the relations H_T and vP0_t are not generated by joeq anymore( I ran gen-relations with the -cs, -partial and -fly options). A little digging into joeq code showed that joeq doesn't generate those relations anymore.

I also found some remains of a datalog syntax experiment in the the BDD[2] directory of joeq cvs. It looked like it was performing an escape analysis[4]. Even this doesn't seem to work because, While all relations existed, it looks like the definition of vP0 has changed from
vP0 ( vc:C, v:V , h:H )
to
vP0 ( v:V , h:H ).

Here are the questions I have. I would be glad if anyone can answer them.

1) Is there a new version of thread escape escape analysis some where in the bddbddb examples? Or is there a version that works with current bddbddb?
2) What do the relations mC and mV mean?
3) What flags do I need to use to generate IEcs relation? ( -cs doesn't seem to work)
4) I am using java 6 to run bddbddb. This seems to work. Is there any reason I should be only using 1.5?

Thanks for your time,
-S-

[1] Cloning-based context-sensitive pointer alias analysis using binary decision diagrams
[2] /joeq_core/joeq/Compiler/Analysis/BDD/*escape* files
[3] Thread escape analysis from the paper.
### Thread escape analysis from Whaley's thesis.

.basedir "/home/suman/installs/joeq/bankExample/bin/results/"
.include "fielddomains.pa"

# Relations

# From algo 1
vP0        (variable: V, heap: H) input
S     (base : V, field : F, source: V) input
L     (base: V, field : F, dest : V) input
A    (dest : V, source : V) input
vP (variable : V, heap: H)
hP (base: H, field : H, target : H)

# From algo 2
vT (variable : V, type : T) input
hT (heap: H, type : T1) input
aT (supertype : T0, subtype:T1) input
vPfilter (variable : V, heap : H)

# From algo 7
HT (c:C, heap: H) input
vP0T (cv : C, variable: V, ch : C, heap : H) input
vPT (cv : C, variable : V, ch : C, heap : H) output
hPT (cb : C, base : H, field : F, ct : C, target : H) output

# Rules
#

# computing vP and hP
vP(v,h) :- vP0(v,h).
vP(v1,h) :- A(v1,v2),vP(v2,h).
hP(h1,f,h2) :- S(v1,f,v2), vP(v1,h1), vP(v2,h2).
vP(v2,h2) :- L(v1,f,v2), vP(v1,h1), hP(h1,f,h2).

# Computing vPT and hPT
vPfilter(v, h) :- vT(v,tv), hT(h,th), aT(tv,th).
vPT(c1,v,c2,h) :- vP0T(c1,v,c2,h).
vPT(c,v,c2,h)    :- vP0(v,h),HT(c,h), equal(c,c2).
vPT(c2,v1,ch,h) :- A(v1,v2), vPT(c2,v2,ch,h), vPfilter(v1,h).
hPT(c1,h1,f,c2,h2) :- S(v1,f,v2),vPT(c,v1,c1,h1),vPT(c,v2,c2,h2).
vPT(c,v2,c2,h2) :- L(v1,f,v2),vPT(c,v1,c2,h1),hPT(c1,h1,f,c2,h2), vPfilter(v2,h2).

[4] Thread escape analysis from joeq's cvs

### Thread escape analysis from joeq sources

.basedir "/home/suman/installs/joeq/bankExample/bin/results/"
.include "fielddomains.pa"

# Relations

# escape 1
mC (method:M, context:C) input
IE0 (ccaller:C, invoke:I, ccallee:C, target:M) input
mI (method:M, invoke:I, name:N) input
mV (method:M, var:V) input

mVc ( method:M , cmethod:C , var:V , cvar:C )

# escape 2

# This relation doesn't exist
vP0 ( vc:C, v:V , h:H ) input
#This may print too many tuples
escape ( h:H , ccaller:C, m:M ) outputtuples

### Rules

# escape 1
mVc(m,c1,v,c2) :- mV(m,v), mC(m,c1), c1 = c2.
mVc(m1,c1,v3,c3) :- IE0(c1,i1,c2,m2), mI(m1,i1,_), mVc(m2,c2,v3,c3). split

# escape 2
escape(h,c0,m) :- mV(m2,v), vP0(cv,v,h), mC(m2,cv), !mVc(m,c0,v,cv).

-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/

_______________________________________________
bddbddb-devel mailing list
bddbddb-devel <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/bddbddb-devel

headers

Taryn | 23 Sep 2008 03:22

[SPAM] Re: INTERNET PROMOTION SERVICE - 608307

Dear bddbddb-devel <at> lists.sourceforge.net:

We provide Marketing Support:

1. Provide email list on your required.

2. Customise email list for you, broadcast your message to the list.

3. Web-based email mailing system that allows you easily sending
    emails and manage the list.

* We offer also broadcast server for sending emails.

Please contact us for any question.


Motely <at> zj.com
Marketing Support
PL Marketing Support Center



This email message is for bddbddb-devel <at> lists.sourceforge.net.
For opt-out: 229099 <at> ZJ.com

headers

John Whaley | 30 Dec 2007 21:22

Re: Encoding FORALL quantificator (the universal quantificator) Re: Encoding Object-oriented relations in bddbddb

Hi,

You can accomplish FORALL in Datalog by using a double negation. For example, if you have predicates "student(s)" for the list of students and "took(s,c)" if student s took class c, and "required(c)" for the list of required classes, then you could write:

cantGraduate(s) :- student(s), required(c), !took(s,c).
canGraduate(s) :- student(s), !cantGraduate(s).

Basically you just use the fact that FORALL(P) is the same as NOT EXISTS(NOT P).

-John

On Dec 30, 2007 8:22 AM, Pengcheng Wu <wupc <at> ccs.neu.edu> wrote:

Hi Dr. Whaley,

Thanks for your time answering my questions. I really appreciate them.

I am having another question about how to encode the FORALL quantificator (the universal quantificator) in bddbddb, and am wondering if you can give me some help. I realize that it is more of a Datalog question, instead of a direct question about the bddbddb tool. But I will appreciate your thoughts/suggestions.

I want to implement a CHA (Class Hierarchy Analysis) algorithm in bddbddb, where I need to encode the FORALL quantificator, because to determine if a method in a subclass (Sub) overrides another method in a superclass (Sup), I need to specify the constraint that the method name has to match, and FORALL of the arguments, the static types have to match. The first of my attempt is to encode the method arguments signature to be something like:

   methodsignature(meth, argPosition, argName, argType)

But soon I realized that I could not write down the overriding determination algorithm this way, because as far as I know, there is no FORALL quantificator in Datalog (I could be wrong about this), which I believe is necessary for expressing this constraint.

Then I looked into your PLDI'04 paper, where you also needed to use the CHA algorithm. However, I found in your paper, the CHA relation was not actually computed from the bddbddb slover. Instead, it was given as an 'a priori' fact, possibly pre-computed by some Java program (this is just my guess). So was that a deliberate decision due to the lack of FORALL quantificator in Datalog, or was that just due to a performance consideration (probably computing that in Java was faster)? If it is the latter, could it have been computed in bddbddb rules directly?

Thanks again,

--Pengcheng

On Dec 26, 2007 4:20 PM, John Whaley <joewhaley <at> gmail.com> wrote:
Hi,

You can find an example in testMap.datalog in bddbddb_examples, here:
http://bddbddb.svn.sourceforge.net/viewvc/bddbddb/trunk/bddbddb_examples/testMap.datalog?revision=304&view=markup

-John

On Dec 26, 2007 12:43 PM, Pengcheng Wu <wupc <at> ccs.neu.edu > wrote:
I was not aware of the "=>" operator. Can you please elaborate it? Or if there is a link to a relevant doc/paper, please let me know.

Thanks for the info!
--Pengcheng

On Dec 26, 2007 3:15 PM, John Whaley <joewhaley <at> gmail.com> wrote:
Yes, the easiest way to accomplish that is to always use "IsRegionMem()" when using "size()". Basically instead of using a predicate "P(...,m:RegionMem,...)", use two predicates "P(...,m:Memory,...)" and "IsRegionMem(m:Memory)".

The other way to do it would be to separate the domains and use the "=>" operator to move between domains.

-John

On Dec 26, 2007 11:29 AM, Pengcheng Wu < wupc <at> ccs.neu.edu> wrote:
Sure we can do that. But I can see an issue of losing type precision when we cannot introduce separate domains for "HeapMem" and "RegionMem" respectively. Imagine there is a relation 'size' that only makes sense for "RegionMem' but not for "HeapMem", i.e., the following meta-model:

+----------+           +---------------+
    | Pointer | ---------------------------> | Memory | <|----+
    +-----------+              pointsTo   +--------------+        |
                                                                          |
                                                          -------------------------------
|    |
                     +---------------+           +-----------------+          +----------+
   | HeapMem |            | RegionMem| --------> | Size   |
   +---------------+           +-----------------+           +---------+

We would have to define the size relation to be:

size(m:Memory, s:Size)

And use this relation always conjunction with predicate IsRegionMem. I guess a relation like size(rm:RegionMem, s:Size) would have made this conjunction unnecessary and would have allowed us to exclude some ill-formed facts earlier by type-checking.

Do you agree?

Thanks,
--Pengcheng

On Dec 26, 2007 1:08 PM, John Whaley < joewhaley <at> gmail.com> wrote:
Sure, one easy way to do this is to partition your "Memory" domain into smaller parts, and add "IsHeapMem()" or "IsRegionMem()" predicates to distinguish between them for the rules that need to. You can partition the domain by e.g. saying elements 1-10000 are heap and 10001-20000 are region.

Example:

PointsTo(v1,h) :- Assign(v1,v2), PointsTo(v2,h).

PointsToNonRegionMem(v) :- PointsTo(v,h), !IsRegionMem(h).
PointsToOnlyRegionMem(v) :- PointsTo(v,_), !PointsToNonRegionMem(v).

-John

On Dec 26, 2007 9:21 AM, Pengcheng Wu <wupc <at> ccs.neu.edu > wrote:
Dear Dr. John Whaley,

How are you?

I am a PhD student with Northeastern University, Boston, trying to use your bddbddb tool to do some software analysis tasks. I have a question about the tool itself, and I would appreciate it very much if you can spend some time answering it.

My question is specific to how to encode object-oriented relations in bddbddb. I understand that when using bddbddb, one needs to firstly define domains and the relations (with relation signatures) over the domains. However, all the examples that I have seen (in your papers) only use pure relational relations, and it is not clear to me whether the tool directly supports inheritance paradigm that is common in O-O modeling. Let me use one specific example to get my point. Assume I have the following OO meta-model (using the UML notation), on which I want to run some query using bddbddb:

    +----------+                              +---------------+
    | Pointer | ---------------------------> | Memory | <|----+
    +-----------+              pointsTo   +--------------+        |
                                                                          |
                                                          -------------------------------
|    |
                     +---------------+           +-----------------+
   | HeapMem |            | RegionMem|
   +---------------+           +-----------------+

As hopefully can be seen in the diagram, a pointer can point to a memory object, which can be either a HeapMem object or a RegionMem object at run time. It is unclear to me how to encode the pointsTo relation. For example, I may encode it as:

pointsTo(p:Pointer, m:Memory)

but when I forms the ground rules (facts), I have to make a $p$ points to either a HeapMem object, or a RegionMem object, which is not in the domain of Memory.

Am I supposed to flatten this relation, such that we have the following?

   pointsToHeap(p:Pointer, hm:HeapMem)
   pointsToRegion(p:Pointer,rm:RegionMem)

But I can see many more rules will need to be made when the O-O meta-model gets bigger and more inheritances are used (or the inheritance chain gets deeper).

Or better, does bddbddb support the notion that a domain can be built up from other domains using primitive set operations, e.g., the domain of Memory could be got by doing union on the two disjoint domains from HeapMem and RegionMem? This way, I would not need to flatten the diagram. Maybe the tool already supports this, but I didn't find an example. So if that is the case, please let me know where I can find such an example.

Thanks a lot in advance!

Happy holiday!

--Pengcheng

-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2005.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/

_______________________________________________
bddbddb-devel mailing list
bddbddb-devel <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/bddbddb-devel

headers

John Whaley | 26 Dec 2007 19:08

Re: Encoding Object-oriented relations in bddbddb

Sure, one easy way to do this is to partition your "Memory" domain into smaller parts, and add "IsHeapMem()" or "IsRegionMem()" predicates to distinguish between them for the rules that need to. You can partition the domain by e.g. saying elements 1-10000 are heap and 10001-20000 are region.

Example:

PointsTo(v1,h) :- Assign(v1,v2), PointsTo(v2,h).

PointsToNonRegionMem(v) :- PointsTo(v,h), !IsRegionMem(h).
PointsToOnlyRegionMem(v) :- PointsTo(v,_), !PointsToNonRegionMem(v).

-John

On Dec 26, 2007 9:21 AM, Pengcheng Wu <wupc <at> ccs.neu.edu> wrote:

Dear Dr. John Whaley,

How are you?

I am a PhD student with Northeastern University, Boston, trying to use your bddbddb tool to do some software analysis tasks. I have a question about the tool itself, and I would appreciate it very much if you can spend some time answering it.

My question is specific to how to encode object-oriented relations in bddbddb. I understand that when using bddbddb, one needs to firstly define domains and the relations (with relation signatures) over the domains. However, all the examples that I have seen (in your papers) only use pure relational relations, and it is not clear to me whether the tool directly supports inheritance paradigm that is common in O-O modeling. Let me use one specific example to get my point. Assume I have the following OO meta-model (using the UML notation), on which I want to run some query using bddbddb:

    +----------+                              +---------------+
    | Pointer | ---------------------------> | Memory | <|----+
    +-----------+              pointsTo   +--------------+        |
                                                                          |
                                                          -------------------------------
|    |
                     +---------------+           +-----------------+
   | HeapMem |            | RegionMem|
   +---------------+           +-----------------+

As hopefully can be seen in the diagram, a pointer can point to a memory object, which can be either a HeapMem object or a RegionMem object at run time. It is unclear to me how to encode the pointsTo relation. For example, I may encode it as:

pointsTo(p:Pointer, m:Memory)

but when I forms the ground rules (facts), I have to make a $p$ points to either a HeapMem object, or a RegionMem object, which is not in the domain of Memory.

Am I supposed to flatten this relation, such that we have the following?

   pointsToHeap(p:Pointer, hm:HeapMem)
   pointsToRegion(p:Pointer,rm:RegionMem)

But I can see many more rules will need to be made when the O-O meta-model gets bigger and more inheritances are used (or the inheritance chain gets deeper).

Or better, does bddbddb support the notion that a domain can be built up from other domains using primitive set operations, e.g., the domain of Memory could be got by doing union on the two disjoint domains from HeapMem and RegionMem? This way, I would not need to flatten the diagram. Maybe the tool already supports this, but I didn't find an example. So if that is the case, please let me know where I can find such an example.

Thanks a lot in advance!

Happy holiday!

--Pengcheng

-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2005.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/

_______________________________________________
bddbddb-devel mailing list
bddbddb-devel <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/bddbddb-devel

headers

Alan Ryan | 27 Nov 2007 15:11

Repost: (Mangled Encoding) -findbestorder problem

Hi, this is a repost of last weeks topic, it seems to  have been
mangled on the SF page:

I am having trouble getting the solver to run the machine learning
algorithm.  I have taken a trivial app and run:

[alan <at> soma-dt resources]$ java -cp $CLASSPATH:resources/:.  -Xmx1024m -
Dpa.dumppath=results/ -Dpa.specialmapinfo=yes -Dpa.dumpunmunged=yes -
Dpa.signaturesinlocs=yes joeq.Main.GenRelations Driver

This produces the relations as expected.  I then want to take
pacs2.datalogsupplied in bddbdb_examples and run it.   I comment out
the .bddnodes &
.bddcache & .bddvarorder directives (same error if I don't do this) in
pacs2.datalog and then run:

[alan <at> soma-dt resources]$ java -cp $CLASSPATH:resources/:.  -Xmx1024m -
Dpa.dumppath=results/ -Dfindbestorder -Dfbotrials=700 -Dbddnodes=100000
-Dbddvarorder= net.sf.bddbddb.Solver pacs2.datalog

This gives me:
 (the entire output is attached, libbuddy.so is not loading for me, I get an
'unsatisifed link error : addRef' when I put in the directory I am executing
from.  I haven't tried to solve this.)

Exception in thread "main" java.lang.NullPointerException
        at net.sf.bddbddb.order.TrialData
Repository.buildAttribInstances(
TrialDataRepository.java:79)
        at net.sf.bddbddb.order.TrialDataRepository.getAttribDataGroup(
TrialDataRepository.java:153)
        at net.sf.bddbddb.FindBestDomainOrder.tryNewGoodOrder(
FindBestDomainOrder.java:777)
        at net.sf.bddbddb.FindBestDomainOrder.hasOrdersToTry(
FindBestDomainOrder.java:602)
        at net.sf.bddbddb.FindBestDomainOrder.findBestDomainOrder(
FindBestDomainOrder.java:2065)
        at net.sf.bddbddb.BDDInferenceRule.evalRelations(
BDDInferenceRule.java:480)
        at net.sf.bddbddb.BDDInferenceRule.update(BDDInferenceRule.java:373)
        at net.sf.bddbddb.ir.BDDInterpreter.interpret(BDDInterpreter.java
:70)
        at net.sf.bddbddb.ir.BDDInterpreter.interpret(BDDInterpreter.java
:50)
        at net.sf.bddbddb.BDDSolver.solve(BDDSolver.java:395)
        at net.sf.bddbddb.Solver.run(Solver.java:388)
        at net.sf.bddbddb.Solver.main2(Solver.java:441)
        at net.sf.bddbddb.Solver.main(Solver.java:1108)

What am I doing wrong here - I cannot seem to get the results that Luke was
getting in his email regarding the same?

Thanks,
Alan

--

-- 
T:  +353 91 512601

Dept. of Information Technology.
National University of Ireland, Galway

-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2005.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/

headers

Alan Ryan | 21 Nov 2007 13:58

Variable Ordering

Hi John,

I am having trouble getting the solver to run the machine learning algorithm. I have taken a trivial app and run:

[alan <at> soma-dt resources]$ java -cp $CLASSPATH:resources/:. -Xmx1024m -Dpa.dumppath=results/ -Dpa.specialmapinfo=yes -Dpa.dumpunmunged=yes -Dpa.signaturesinlocs=yes joeq.Main.GenRelations Driver

This produces the relations as expected. I then want to take pacs2.datalog supplied in bddbdb_examples and run it.   I comment out the .bddnodes & .bddcache & .bddvarorder directives (same error if I don't do this) in pacs2.datalog and then run:

[alan <at> soma-dt resources]$ java -cp $CLASSPATH:resources/:. -Xmx1024m -Dpa.dumppath=results/ -Dfindbestorder -Dfbotrials=700 -Dbddnodes=100000 -Dbddvarorder= net.sf.bddbddb.Solver pacs2.datalog

This gives me:
(the entire output is attached, libbuddy.so is not loading for me, I get an 'unsatisifed link error : addRef' when I put in the directory I am executing from. I haven't tried to solve this.)

Exception in thread "main" java.lang.NullPointerException
        at net.sf.bddbddb.order.TrialDataRepository.buildAttribInstances(TrialDataRepository.java:79)
        at net.sf.bddbddb.order.TrialDataRepository.getAttribDataGroup (TrialDataRepository.java:153)
        at net.sf.bddbddb.FindBestDomainOrder.tryNewGoodOrder(FindBestDomainOrder.java:777)
        at net.sf.bddbddb.FindBestDomainOrder.hasOrdersToTry(FindBestDomainOrder.java:602)
        at net.sf.bddbddb.FindBestDomainOrder.findBestDomainOrder(FindBestDomainOrder.java:2065)
        at net.sf.bddbddb.BDDInferenceRule.evalRelations(BDDInferenceRule.java:480)
        at net.sf.bddbddb.BDDInferenceRule.update (BDDInferenceRule.java:373)
        at net.sf.bddbddb.ir.BDDInterpreter.interpret(BDDInterpreter.java:70)
        at net.sf.bddbddb.ir.BDDInterpreter.interpret(BDDInterpreter.java:50)
        at net.sf.bddbddb.BDDSolver.solve (BDDSolver.java:395)
        at net.sf.bddbddb.Solver.run(Solver.java:388)
        at net.sf.bddbddb.Solver.main2(Solver.java:441)
        at net.sf.bddbddb.Solver.main(Solver.java:1108)

What am I doing wrong here - I cannot seem to get the results that Luke was getting in his email regarding the same?

Thanks,
Alan

--
T: +353 91 512601

Dept. of Information Technology.
National University of Ireland, Galway

[alan <at> soma-dt resources]$ java -cp $CLASSPATH:resources/:.  -Xmx1024m -Dpa.dumppath=results/
-Dfindbestorder -Dfbotrials=700 -Dbddnodes=100000 -Dbddvarorder= net.sf.bddbddb.Solver pacs2.datalog

Initializing BDD library (100000 nodes, cache size 25000, min free 0.2%)
Could not load BDD package buddy: Can't load library: /home/alan/phd/bddbddb/resources/libbuddy.so
Using BDD library JFactory 474
Opening Datalog program "pacs2.datalog"
WARNING: Cannot load mapfile "results/class.map", skipping.
12 field domains.
26 relations.
13 rules.
Splitting rules: done.
Initializing solver: Garbage collection #1: 1009 nodes / 107 free / 0.0030s / 0.0030s total
Resizing node table from 1009 to 2017
Adding missing domain "V0" to bddvarorder.
Adding missing domain "V1" to bddvarorder.
Adding missing domain "I0" to bddvarorder.
Adding missing domain "I1" to bddvarorder.
Adding missing domain "H0" to bddvarorder.
Adding missing domain "H1" to bddvarorder.
Adding missing domain "Z0" to bddvarorder.
Adding missing domain "F0" to bddvarorder.
Adding missing domain "T0" to bddvarorder.
Adding missing domain "T1" to bddvarorder.
Adding missing domain "N0" to bddvarorder.
Adding missing domain "M0" to bddvarorder.
Adding missing domain "C0" to bddvarorder.
Adding missing domain "M1" to bddvarorder.
Adding missing domain "STR0" to bddvarorder.
Adding missing domain "VC0" to bddvarorder.
Adding missing domain "VC1" to bddvarorder.
Setting variable ordering to VC1_VC0_STR0_C0_M1_M0_N0_T1_T0_F0_Z0_H1_H0_I1_I0_V1_V0_, Start reordering
Garbage collection #2: 2017 nodes / 1067 free / 0.0010s / 0.0040s total
End reordering. Went from 976 to 950 nodes, gain = 2% (0.072 sec)
done.
194,193,192,191,190,189,188,187,186,185,184,183,182,181,180,179,178,177,176,175,174,173,172,171,170,169,168,167,166,165,164,163,162,161,160,159,158,157,156,155,154,153,152,151,140,139,138,137,136,135,134,133,132,131,130,129,150,149,148,147,146,145,144,143,142,141,128,127,126,125,124,123,122,121,120,119,118,117,116,115,114,113,112,111,110,109,108,107,106,105,104,103,102,101,100,99,98,97,96,95,94,93,92,91,90,89,88,87,86,85,84,83,82,81,80,79,78,77,76,75,74,73,72,71,70,69,68,67,66,65,64,63,62,61,60,59,58,57,56,55,54,53,52,51,50,49,48,47,46,45,44,43,42,41,40,39,38,37,36,35,34,33,32,31,30,29,28,27,26,25,24,23,22,21,20,19,18,17,16,15,14,13,12,11,10,9,8,7,6,5,4,3,2,1,0,
Resizing node table from 2017 to 99991
Trials filename=trials_pacs2.xml
done.
Loading initial relations: Loading BDD from file: vP0.bdd 4897 nodes, 1468.0 elements.
Loading BDD from file: A.bdd 1187 nodes, 849.0 elements.
Loading BDD from file: S.bdd 4780 nodes, 644.0 elements.
Loading BDD from file: L.bdd 2272 nodes, 135.0 elements.
Loading BDD from file: actual.bdd 6899 nodes, 1881.0 elements.
Loading BDD from file: formal.bdd 4471 nodes, 612.0 elements.
Loading BDD from file: Mret.bdd 983 nodes, 146.0 elements.
Loading BDD from file: Mthr.bdd 3073 nodes, 1230.0 elements.
Loading BDD from file: Iret.bdd 2790 nodes, 407.0 elements.
Loading BDD from file: Ithr.bdd 5122 nodes, 1154.0 elements.
Loading BDD from file: mI.bdd Garbage collection #3: 99991 nodes / 62967 free / 0.0070s / 0.011s total
9282 nodes, 1154.0 elements.
Loading BDD from file: IE0.bdd 4060 nodes, 1127.0 elements.
Loading BDD from file: vT.bdd Garbage collection #4: 99991 nodes / 55576 free / 0.0080s / 0.019s total
3728 nodes, 3623.0 elements.
Loading BDD from file: hT.bdd 1269 nodes, 974.0 elements.
Loading BDD from file: aT.bdd 779 nodes, 746.0 elements.
Loading BDD from file: cha.bdd 2289 nodes, 617.0 elements.
Loading BDD from file: hP0.bdd WARNING: Cannot load bdd hP0: java.io.FileNotFoundException:
results/hP0.bdd (No such file or directory)
Loading BDD from file: roots.bdd 14 nodes, 45.0 elements.
done. (337 ms)
Stratifying: 
Note: the following relations are unused:
    [cha, hP0]
Note: the following rules are unused:
Discovering stratum, 0 SCCs visited so far
Finished discovery of 52 SCCs in 1 strata
done. (33 ms)
Solving: 
list1:
  list2:
    cvP(_,v:V0,h:H0) :- vP0(v:V0,h:H0).
    mI0(m:M0,i:I0) :- mI(m:M0,i:I0,_:N0).
    cA(_,v1:V0,_,v2:V1) :- A(v1:V0,v2:V1).
    vPfilter(v:V0,h:H0) :- vT(v:V0,tv:T0), aT(tv:T0,th:T1), hT(h:H0,th:T1).
    IEnum(i,m,vc2,vc1) :- roots(m), mI0(m,i), IE0(i,m).
    IEcs(vc2:VC1,i:I0,vc1:VC0,m:M0) :- IE0(i:I0,m:M0), IEnum(i:I0,m:M0,vc2:VC1,vc1:VC0).
    IE(i:I0,m:M0) :- IEcs(_:VC1,i:I0,_:VC0,m:M0).
    cA(vc2:VC1,v2:V0,vc1:VC0,v1:V1) :- Mthr(m:M0,v1:V1), IEcs(vc2:VC1,i:I0,vc1:VC0,m:M0), Ithr(i:I0,v2:V0).
    cA(vc2:VC1,v2:V0,vc1:VC0,v1:V1) :- Mret(m:M0,v1:V1), IEcs(vc2:VC1,i:I0,vc1:VC0,m:M0), Iret(i:I0,v2:V0).
    cA(vc1:VC0,v1:V0,vc2:VC1,v2:V1) :- formal(m:M0,z:Z0,v1:V0), IEcs(vc2:VC1,i:I0,vc1:VC0,m:M0), actual(i:I0,z:Z0,v2:V1).
    loop3:
      loop5:
        cvP(vc1:VC0,v1:V0,h:H0) :- cA(vc1:VC0,v1:V0,vc2:VC1,v2:V1), cvP(vc2:VC1,v2:V1,h:H0), vPfilter(v1:V0,h:H0).
      cvP_11_0(f:F0,v2:V1,vc1:VC0,h1:H0) :- L(v1:V0,f:F0,v2:V1), cvP(vc1:VC0,v1:V0,h1:H0).
      hP(h1:H0,f:F0,h2:H1) :- S(v1:V0,f:F0,v2:V1), cvP(vc1:VC0,v1:V0,h1:H0), cvP(vc1:VC0,v2:V1,h2:H1).
      cvP_11_1(v2:V1,vc1:VC0,h2:H1) :- cvP_11_0(f:F0,v2:V1,vc1:VC0,h1:H0), hP(h1:H0,f:F0,h2:H1).
      cvP(vc1:VC0,v2:V1,h2:H1) :- cvP_11_1(v2:V1,vc1:VC0,h2:H1), vPfilter(v2:V1,h2:H1).

Applying inference rule:
   cvP(_,v:V0,h:H0) :- vP0(v:V0,h:H0). (1)
Applying inference rule:
   mI0(m:M0,i:I0) :- mI(m:M0,i:I0,_:N0). (1)
Applying inference rule:
   cA(_,v1:V0,_,v2:V1) :- A(v1:V0,v2:V1). (1)
Applying inference rule:
   vPfilter(v:V0,h:H0) :- vT(v:V0,tv:T0), aT(tv:T0,th:T1), hT(h:H0,th:T1). (1)
Applying numbering rule:
   IEnum(i,m,vc2,vc1) :- roots(m), mI0(m,i), IE0(i,m).
Garbage collection #5: 99991 nodes / 41935 free / 0.01s / 0.029s total
Done counting paths (1242 ms, number of paths = 13196 (14 bits)          
Garbage collection #6: 99991 nodes / 4844 free / 0.013s / 0.042s total
Resizing node table from 99991 to 299969
Garbage collection #7: 299969 nodes / 192110 free / 0.023s / 0.065s total
Garbage collection #8: 299969 nodes / 186936 free / 0.024s / 0.089s total
Garbage collection #9: 299969 nodes / 185060 free / 0.024s / 0.113s total
Garbage collection #10: 299969 nodes / 185412 free / 0.024s / 0.137s total
Garbage collection #11: 299969 nodes / 180906 free / 0.025s / 0.162s total
Garbage collection #12: 299969 nodes / 148282 free / 0.03s / 0.192s total
Garbage collection #13: 299969 nodes / 165578 free / 0.027s / 0.219s total
Garbage collection #14: 299969 nodes / 140328 free / 0.03s / 0.249s total
Garbage collection #15: 299969 nodes / 127969 free / 0.032s / 0.281s total
Garbage collection #16: 299969 nodes / 155750 free / 0.029s / 0.31s total
Garbage collection #17: 299969 nodes / 142863 free / 0.031s / 0.341s total
Garbage collection #18: 299969 nodes / 141777 free / 0.031s / 0.372s total
Garbage collection #19: 299969 nodes / 143517 free / 0.031s / 0.403s total
Garbage collection #20: 299969 nodes / 131401 free / 0.032s / 0.435s total
Garbage collection #21: 299969 nodes / 150505 free / 0.029s / 0.464s total
Garbage collection #22: 299969 nodes / 144100 free / 0.031s / 0.495s total
Garbage collection #23: 299969 nodes / 139500 free / 0.031s / 0.526s total
Garbage collection #24: 299969 nodes / 141132 free / 0.031s / 0.557s total
Garbage collection #25: 299969 nodes / 141454 free / 0.031s / 0.588s total
Garbage collection #26: 299969 nodes / 130849 free / 0.032s / 0.62s total
Garbage collection #27: 299969 nodes / 136797 free / 0.031s / 0.651s total
Garbage collection #28: 299969 nodes / 147632 free / 0.031s / 0.682s total
Garbage collection #29: 299969 nodes / 124670 free / 0.037s / 0.719s total
Garbage collection #30: 299969 nodes / 143531 free / 0.031s / 0.75s total
Garbage collection #31: 299969 nodes / 136378 free / 0.032s / 0.782s total
Garbage collection #32: 299969 nodes / 107594 free / 0.036s / 0.818s total
Garbage collection #33: 299969 nodes / 110455 free / 0.035s / 0.853s total
Garbage collection #34: 299969 nodes / 97496 free / 0.038s / 0.891s total
Garbage collection #35: 299969 nodes / 115436 free / 0.035s / 0.926s total
Garbage collection #36: 299969 nodes / 96907 free / 0.038s / 0.964s total
Garbage collection #37: 299969 nodes / 104030 free / 0.037s / 1.001s total
Garbage collection #38: 299969 nodes / 118924 free / 0.035s / 1.036s total
Garbage collection #39: 299969 nodes / 118029 free / 0.035s / 1.071s total
Garbage collection #40: 299969 nodes / 112190 free / 0.036s / 1.107s total
Garbage collection #41: 299969 nodes / 106630 free / 0.037s / 1.144s total
Garbage collection #42: 299969 nodes / 115519 free / 0.035s / 1.179s total
Garbage collection #43: 299969 nodes / 107672 free / 0.037s / 1.216s total
Garbage collection #44: 299969 nodes / 115517 free / 0.035s / 1.251s total
Garbage collection #45: 299969 nodes / 119436 free / 0.035s / 1.286s total
Time spent: 15517 ms
Applying inference rule:
   IEcs(vc2:VC1,i:I0,vc1:VC0,m:M0) :- IE0(i:I0,m:M0), IEnum(i:I0,m:M0,vc2:VC1,vc1:VC0). (1)
Applying inference rule:
   IE(i:I0,m:M0) :- IEcs(_:VC1,i:I0,_:VC0,m:M0). (1)
Garbage collection #46: 299969 nodes / 120095 free / 0.035s / 1.321s total
Applying inference rule:
   cA(vc2:VC1,v2:V0,vc1:VC0,v1:V1) :- Mthr(m:M0,v1:V1), IEcs(vc2:VC1,i:I0,vc1:VC0,m:M0),
Ithr(i:I0,v2:V0). (1)
Garbage collection #47: 299969 nodes / 83603 free / 0.04s / 1.361s total
Garbage collection #48: 299969 nodes / 65480 free / 0.042s / 1.403s total
Garbage collection #49: 299969 nodes / 50922 free / 0.045s / 1.448s total
Resizing node table from 299969 to 899903
Applying inference rule:
   cA(vc2:VC1,v2:V0,vc1:VC0,v1:V1) :- Mret(m:M0,v1:V1), IEcs(vc2:VC1,i:I0,vc1:VC0,m:M0),
Iret(i:I0,v2:V0). (1)
Applying inference rule:
   cA(vc1:VC0,v1:V0,vc2:VC1,v2:V1) :- formal(m:M0,z:Z0,v1:V0), IEcs(vc2:VC1,i:I0,vc1:VC0,m:M0),
actual(i:I0,z:Z0,v2:V1). (1)
Garbage collection #50: 899903 nodes / 475464 free / 0.093s / 1.541s total
Variables: [vc2, vc1, m, z, i, v2, v1]
Exception in thread "main" java.lang.NullPointerException
        at net.sf.bddbddb.order.TrialDataRepository.buildAttribInstances(TrialDataRepository.java:79)
        at net.sf.bddbddb.order.TrialDataRepository.getAttribDataGroup(TrialDataRepository.java:153)
        at net.sf.bddbddb.FindBestDomainOrder.tryNewGoodOrder(FindBestDomainOrder.java:777)
        at net.sf.bddbddb.FindBestDomainOrder.hasOrdersToTry(FindBestDomainOrder.java:602)
        at net.sf.bddbddb.FindBestDomainOrder.findBestDomainOrder(FindBestDomainOrder.java:2065)
        at net.sf.bddbddb.BDDInferenceRule.evalRelations(BDDInferenceRule.java:480)
        at net.sf.bddbddb.BDDInferenceRule.update(BDDInferenceRule.java:373)
        at net.sf.bddbddb.ir.BDDInterpreter.interpret(BDDInterpreter.java:70)
        at net.sf.bddbddb.ir.BDDInterpreter.interpret(BDDInterpreter.java:50)
        at net.sf.bddbddb.BDDSolver.solve(BDDSolver.java:395)
        at net.sf.bddbddb.Solver.run(Solver.java:388)
        at net.sf.bddbddb.Solver.main2(Solver.java:441)
        at net.sf.bddbddb.Solver.main(Solver.java:1108)

-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2005.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/

_______________________________________________
bddbddb-devel mailing list
bddbddb-devel <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/bddbddb-devel

1	May 2011
1	April 2011
1	November 2010
1	December 2009
1	March 2009
1	November 2008
1	September 2008
2	December 2007
3	November 2007
2	September 2007
1	August 2007
12	June 2007
1	March 2007
1	February 2007
6	January 2007
2	November 2006
2	June 2006
1	March 2006
1	November 2005

Mon	Tue	Wed	Thu	Fri	Sat	Sun

		1	2	3	4	5
6	7	8	9	10	11	12
13	14	15	16	17	18	19
20	21	22	23	24	25	26
27	28	29	30	31