scale.score.dependence.omega.omegaLib
Class RelBody

java.lang.Object
  scale.score.dependence.omega.omegaLib.Formula
      scale.score.dependence.omega.omegaLib.RelBody

public final class RelBody
extends Formula

RelBody.

$Id: RelBody.java,v 1.22 2007-10-31 04:28:28 asmith Exp $

Copyright 2008 by the Scale Compiler Group,
Department of Computer Science
University of Massachusetts,
Amherst MA. 01003, USA
All Rights Reserved.

This version of the Omega Libray is a translation from C++ to Java of the Omega Library developed at the University of Maryland.

Copyright (C) 1994-1996 by the Omega Project

All rights reserved.

NOTICE: This software is provided ``as is'', without any warranty, including any implied warranty for merchantability or fitness for a particular purpose. Under no circumstances shall the Omega Project or its agents be liable for any use of, misuse of, or inability to use this software, including incidental and consequential damages.

License is hereby given to use, modify, and redistribute this software, in whole or in part, for any purpose, commercial or non-commercial, provided that the user agrees to the terms of this copyright notice, including disclaimer of warranty, and provided that this copyright notice, including disclaimer of warranty, is preserved in the source code and documentation of anything derived from this software. Any redistributor of this software or anything derived from this software assumes responsibility for ensuring that any parties to whom such a redistribution is made are fully aware of the terms of this license and disclaimer.

The Omega project can be contacted at omega@cs.umd.edu or http://www.cs.umd.edu/projects/omega

Field Summary

Fields inherited from class scale.score.dependence.omega.omegaLib.Formula

myChildren, myParent, myRelation, omegaLib, OP_AND, OP_CONJUNCT, OP_EXISTS, OP_FORALL, OP_NOT, OP_OR, OP_RELATION

Constructor Summary

RelBody(OmegaLib omegaLib, int number_input, int number_output)

RelBody(RelBody r)

RelBody(RelBody r, Conjunct c)

Method Summary

void	addInputVar(java.lang.String name)
void	addOutputVar(java.lang.String name)
void	addSetVar(java.lang.String name)
RelBody	affineHull()
RelBody	after(int carried_by, int new_output, int dir)
boolean	align(RelBody newr, FExists fe, Formula f, Mapping mapping) Build lists of variables that need to be replaced in the given Formula.
FAnd	andWithAnd()
EQHandle	andWithEQ()
EQHandle	andWithEQ(Conjunct c, Equation eq)
GEQHandle	andWithGEQ()
GEQHandle	andWithGEQ(Conjunct c, Equation eq)
RelBody	approximate(boolean strides_allowed)
void	beautify()
void	calculateDimensions(Conjunct c, int[] dims)
boolean	canAddChild()
RelBody	checkForConvexPairs()
RelBody	checkForConvexRepresentation()
void	clearGlobalDecls()
RelBody	complement() complement.
RelBody	composition(RelBody r2) Composition(F, G) = F o G, where F o G (x) = F(G(x)) That is, if F = { [i] .
RelBody	conicClosure()
RelBody	conicHull()
RelBody	convexHull()
Formula	copy(Formula f, RelBody b)
Vector<CName>	copyCNames(Vector<CName> vars)
void	copyNames(RelBody r)
Vector<VarDecl>	copyVars(Vector<VarDecl> vars)
static int	created()
RelBody	crossProduct(RelBody r2) Cross Product.
RelBody	decoupledConvexHull()
void	decrementRefCount()
void	delete()
RelBody	deltas() Deltas(F) Return a set such that the ith variable is old Out_i - In_i Delta variables are created as input variables.
RelBody	deltas(int eq_no)
RelBody	deltasToRelation(int n_inputs, int n_outputs)
RelBody	difference(RelBody r2) F minus G.
DNF	DNFize()
void	DNFtoFormula()
RelBody	domain() Domain and Range.
boolean	doSubsetCheck(RelBody r2)
RelBody	emptyRelation()
void	enforceLeadingInfo(int guaranteed, int possible, int dir)
boolean	equal(RelBody r2)
RelBody	extractDNFByCarriedLevel(int level, int direction) If direction==0, move all conjuncts with >= level leading 0's to return else move all conjuncts with level-1 0's followed by the appropriate signed difference to returned Relation.
RelBody	falseRelation()
static RelBody	falseRelation(OmegaLib omegaLib, int setvars)
static RelBody	falseRelation(OmegaLib omegaLib, int in, int out)
Conjunct	findAvailableConjunct()
Vector<VarDecl>	getGlobalDecls()
VarDecl	getLocal(GlobalVarDecl G)
VarDecl	getLocal(GlobalVarDecl G, int of)
VarDecl	getLocal(VarDecl v)
int	getRefCount()
Conjunct	getSingleConjunct()
RelBody	gist(RelBody R2, int effort) Compute gist(r1) given r2.
RelBody	gistSingleConjunct(RelBody R2, int effort) Compute (gist r1 given r2).
boolean	hasLocal(GlobalVarDecl G)
boolean	hasLocal(GlobalVarDecl G, int of)
boolean	hasSingleConjunct()
RelBody	hull(boolean stridesAllowed, int effort, RelBody knownHull)
RelBody	identity()
static RelBody	identity(OmegaLib omegaLib, int numberInputp) Identity.
void	incrementRefCount()
VarDecl	inputVar(int nth)
void	interpretUnknownAsFalse()
void	interpretUnknownAsTrue()
RelBody	intersection(RelBody r2) F intersection G.
void	invalidateLeadingInfo(int changed)
RelBody	inverse() Inverse F -reverse the input and output tuples.
boolean	isDOK(RelBody D, RelBody AxA) Check if we can use D instead of R.
boolean	isExact()
boolean	isFinalized()
boolean	isLowerBoundSatisfiable() Check if there exist any exact conjuncts in the solution.
boolean	isNotSatisfiable()
boolean	isObviousTautology() Check if we can easily determine if the formula evaluates to true.
boolean	isSatisfiable()
boolean	isSet()
boolean	isShared()
boolean	isSimplified()
boolean	isUnknown()
boolean	isUpperBoundDefinitelyNotSatisfiable() Check if the formula simplifies to FALSE.
boolean	isUpperBoundSatisfiable() Check if the formula simplifies to FALSE, since the library will never say that if the *known* constraints are unsatisfiable by themselves.
RelBody	join(RelBody G)
RelBody	linearHull()
RelBody	makeLevelCarriedTo(int level)
void	nameInputVar(int nth, java.lang.String s)
void	nameOutputVar(int nth, java.lang.String s)
void	nameSetVar(int nth, java.lang.String s)
int	nodeType()
int	numberInput()
int	numberOfConjuncts()
int	numberOutput()
int	numberSet()
VarDecl	outputVar(int nth)
void	prefixPrint()
void	prefixPrint(boolean debug)
void	print()
java.lang.String	printFormulaToString()
java.lang.String	printOutputsWithSubsToString()
java.lang.String	printOutputsWithSubsToString(int i)
java.lang.String	printSubsToString(Conjunct conj, boolean printSym)
void	printWithSubs()
void	printWithSubs(boolean printSym, boolean newline)
java.lang.String	printWithSubsToString(boolean printSym, boolean newline)
RelBody	project(GlobalVarDecl g) Project out global variable g from RelBody r.
RelBody	project(int pos, int vkind) Project an input, output or set variable, leaving a variable in that position with no constraints.
RelBody	project(Vector<VarDecl> s)
RelBody	projectOnSym(RelBody input_context) Project away all input and output variables.
RelBody	projectOntoJust(VarDecl v)
RelBody	projectSym() Project all symbolic variables from RelBody r.
boolean	queryDifference(VarDecl v1, VarDecl v2, int[] bounds)
DNF	queryDNF()
DNF	queryDNF(int rdt_conjs, int rdt_constrs)
int	queryGuaranteedLeadingZeros() Return x such that for all conjuncts c, c has >= x leading 0s.
int	queryLeadingDir() Return +-1 according to sign of leading dir, or 0 if we don't know.
int	queryPossibleLeadingZeros() Return x such that for all conjuncts c, c has <= x leading 0s.
void	queryVariableBounds(VarDecl v, int[] bounds)
RelBody	range()
void	rearrange()
void	remapDNFVars(RelBody ref_rel) Variables in DNF of map_rel reference declarations of map_rel (or not).
Conjunct	removeFirstConjunct()
boolean	removeGlobalDecl(VarDecl v) Return true if the variable was removed from the list of globals.
RelBody	restrictDomain(RelBody r2) F \ G (the relation F restricted to domain G).
RelBody	restrictRange(RelBody r2) F / G (the relation F restricted to range G) align the output tuples for F and G match named variables in F and G formula is f & g
void	reverseLeadingDirInfo()
void	setFinalized()
void	setIsSet(boolean flg)
void	setupNames()
VarDecl	setVar(int nth)
DNF	simplifiedDNF()
void	simplify()
void	simplify(int rdt_conjs, int rdt_constrs)
java.lang.String	toString()
RelBody	transitiveClosure(int maxExpansion, RelBody iterationSpace)
RelBody	transitiveClosure0(int maxExpansion, RelBody iterationSpace) Transitive closure of the RelBody containing multiple conjuncts.
RelBody	trueRelation()
static RelBody	trueRelation(OmegaLib omegaLib, int setvars)
static RelBody	trueRelation(OmegaLib omegaLib, int in, int out)
RelBody	tryConjunctTransitiveClosure(RelBody iterationSpace, RelBody rPlus) Try to get conjunct transitive closure.
RelBody	union(RelBody r2) r1 Union r2.
RelBody	unknownRelation()
static RelBody	unknownRelation(OmegaLib omegaLib, int setvars)
static RelBody	unknownRelation(OmegaLib omegaLib, int in, int out)
int	unknownUses()
RelBody	vennDiagramForm(RelBody context)

Methods inherited from class scale.score.dependence.omega.omegaLib.Formula

addAnd, addChild, addConjunct, addExists, addExists, addForall, addNot, addOr, andWith, assertNotFinalized, checkAndAddChild, children, combineColumns, getChildren, getFirstChild, numberOfChildren, olAssert, olAssert, parent, printSeparator, priority, pushExists, reallyConjunct, relation, remap, removeChild, removeFirstChild, setParent, setParent, setRelation, toStringClass, verifytree

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

RelBody

public RelBody(OmegaLib omegaLib,
               int number_input,
               int number_output)

Parameters:

number_input - is the number of input variables

number_output - is the number of output variables

RelBody

public RelBody(RelBody r)

RelBody

public RelBody(RelBody r,
               Conjunct c)

Method Detail

created

public static int created()

copyVars

public Vector<VarDecl> copyVars(Vector<VarDecl> vars)

copyCNames

public Vector<CName> copyCNames(Vector<CName> vars)

delete

public void delete()

Overrides:

delete in class Formula

incrementRefCount

public void incrementRefCount()

decrementRefCount

public void decrementRefCount()

getRefCount

public int getRefCount()

setFinalized

public void setFinalized()

Overrides:

setFinalized in class Formula

simplifiedDNF

public DNF simplifiedDNF()

queryGuaranteedLeadingZeros

public int queryGuaranteedLeadingZeros()

Return x such that for all conjuncts c, c has >= x leading 0s. For a set, return -1.

queryPossibleLeadingZeros

public int queryPossibleLeadingZeros()

Return x such that for all conjuncts c, c has <= x leading 0s. If no conjuncts, return min of input and output tuple sizes, or -1 if relation is a set.

queryLeadingDir

public int queryLeadingDir()

Return +-1 according to sign of leading dir, or 0 if we don't know.

numberOfConjuncts

public int numberOfConjuncts()

toString

public java.lang.String toString()

Overrides:

toString in class Formula

copy

public Formula copy(Formula f,
                    RelBody b)

Specified by:

copy in class Formula

nodeType

public int nodeType()

Specified by:

nodeType in class Formula

isSet

public boolean isSet()

setIsSet

public void setIsSet(boolean flg)

numberInput

public int numberInput()

numberOutput

public int numberOutput()

numberSet

public int numberSet()

getGlobalDecls

public Vector<VarDecl> getGlobalDecls()

clearGlobalDecls

public void clearGlobalDecls()

removeGlobalDecl

public boolean removeGlobalDecl(VarDecl v)

Return true if the variable was removed from the list of globals.

inputVar

public VarDecl inputVar(int nth)

outputVar

public VarDecl outputVar(int nth)

setVar

public VarDecl setVar(int nth)

getLocal

public VarDecl getLocal(VarDecl v)

getLocal

public VarDecl getLocal(GlobalVarDecl G)

getLocal

public VarDecl getLocal(GlobalVarDecl G,
                        int of)

hasLocal

public boolean hasLocal(GlobalVarDecl G)

hasLocal

public boolean hasLocal(GlobalVarDecl G,
                        int of)

nameInputVar

public void nameInputVar(int nth,
                         java.lang.String s)

nameOutputVar

public void nameOutputVar(int nth,
                          java.lang.String s)

addInputVar

public void addInputVar(java.lang.String name)

addSetVar

public void addSetVar(java.lang.String name)

addOutputVar

public void addOutputVar(java.lang.String name)

nameSetVar

public void nameSetVar(int nth,
                       java.lang.String s)

andWithAnd

public FAnd andWithAnd()

andWithEQ

public EQHandle andWithEQ()

andWithEQ

public EQHandle andWithEQ(Conjunct c,
                          Equation eq)

andWithGEQ

public GEQHandle andWithGEQ()

andWithGEQ

public GEQHandle andWithGEQ(Conjunct c,
                            Equation eq)

print

public void print()

Overrides:

print in class Formula

printWithSubs

public void printWithSubs(boolean printSym,
                          boolean newline)

printWithSubs

public void printWithSubs()

printWithSubsToString

public java.lang.String printWithSubsToString(boolean printSym,
                                              boolean newline)

printSubsToString

public java.lang.String printSubsToString(Conjunct conj,
                                          boolean printSym)

printOutputsWithSubsToString

public java.lang.String printOutputsWithSubsToString()

printOutputsWithSubsToString

public java.lang.String printOutputsWithSubsToString(int i)

printFormulaToString

public java.lang.String printFormulaToString()

prefixPrint

public void prefixPrint()

prefixPrint

public void prefixPrint(boolean debug)

Overrides:

prefixPrint in class Formula

isSatisfiable

public boolean isSatisfiable()

isNotSatisfiable

public boolean isNotSatisfiable()

isLowerBoundSatisfiable

public boolean isLowerBoundSatisfiable()

Check if there exist any exact conjuncts in the solution. Interpret UNKNOWN as false, then check satisfiability.

isUpperBoundSatisfiable

public boolean isUpperBoundSatisfiable()

Check if the formula simplifies to FALSE, since the library will never say that if the *known* constraints are unsatisfiable by themselves. Interpret UNKNOWN as true, then check satisfiability.

isUpperBoundDefinitelyNotSatisfiable

public boolean isUpperBoundDefinitelyNotSatisfiable()

Check if the formula simplifies to FALSE.

isObviousTautology

public boolean isObviousTautology()

Check if we can easily determine if the formula evaluates to true.

isUnknown

public boolean isUnknown()

queryDNF

public DNF queryDNF()

queryDNF

public DNF queryDNF(int rdt_conjs,
                    int rdt_constrs)

simplify

public void simplify()

simplify

public void simplify(int rdt_conjs,
                     int rdt_constrs)

isFinalized

public boolean isFinalized()

isShared

public boolean isShared()

queryDifference

public boolean queryDifference(VarDecl v1,
                               VarDecl v2,
                               int[] bounds)

queryVariableBounds

public void queryVariableBounds(VarDecl v,
                                int[] bounds)

copyNames

public void copyNames(RelBody r)

extractDNFByCarriedLevel

public RelBody extractDNFByCarriedLevel(int level,
                                        int direction)

If direction==0, move all conjuncts with >= level leading 0's to return else move all conjuncts with level-1 0's followed by the appropriate signed difference to returned Relation.

makeLevelCarriedTo

public RelBody makeLevelCarriedTo(int level)

setupNames

public void setupNames()

Overrides:

setupNames in class Formula

unknownUses

public int unknownUses()

isExact

public boolean isExact()

isSimplified

public boolean isSimplified()

removeFirstConjunct

public Conjunct removeFirstConjunct()

getSingleConjunct

public Conjunct getSingleConjunct()

hasSingleConjunct

public boolean hasSingleConjunct()

beautify

public void beautify()

Overrides:

beautify in class Formula

rearrange

public void rearrange()

Overrides:

rearrange in class Formula

interpretUnknownAsTrue

public void interpretUnknownAsTrue()

interpretUnknownAsFalse

public void interpretUnknownAsFalse()

canAddChild

public boolean canAddChild()

Overrides:

canAddChild in class Formula

reverseLeadingDirInfo

public void reverseLeadingDirInfo()

Overrides:

reverseLeadingDirInfo in class Formula

invalidateLeadingInfo

public void invalidateLeadingInfo(int changed)

Overrides:

invalidateLeadingInfo in class Formula

enforceLeadingInfo

public void enforceLeadingInfo(int guaranteed,
                               int possible,
                               int dir)

Overrides:

enforceLeadingInfo in class Formula

DNFize

public DNF DNFize()

Specified by:

DNFize in class Formula

DNFtoFormula

public void DNFtoFormula()

findAvailableConjunct

public Conjunct findAvailableConjunct()

Specified by:

findAvailableConjunct in class Formula

align

public boolean align(RelBody newr,
                     FExists fe,
                     Formula f,
                     Mapping mapping)

Build lists of variables that need to be replaced in the given Formula. Declare globals in new relation. Then call map_vars to do the replacements.

Obnoxiously many arguments here: Relation arguments contain declarations of symbolic and in/out vars. FExists argument is where needed existentially quant. vars can be decl.

Mapping specifies how in/out vars are mapped Two lists are required to be able to map in/out variables from the first and second relations to the same existentially quantified variable.

approximate

public RelBody approximate(boolean strides_allowed)

remapDNFVars

public void remapDNFVars(RelBody ref_rel)

Variables in DNF of map_rel reference declarations of map_rel (or not). remapDNFVars makes them to reference declarations of ref_rel. Ref_rel can get new global variable declarations in the process.

after

public RelBody after(int carried_by,
                     int new_output,
                     int dir)

projectOnSym

public RelBody projectOnSym(RelBody input_context)

Project away all input and output variables.

domain

public RelBody domain()

Domain and Range. Make output (input) variables wildcards and simplify. Move all UFS's to have have the remaining tuple as an argument, and maprel will move them to the set tuple RESET all leading 0's

range

public RelBody range()

inverse

public RelBody inverse()

Inverse F -reverse the input and output tuples.

deltas

public RelBody deltas()

Deltas(F) Return a set such that the ith variable is old Out_i - In_i Delta variables are created as input variables. Then input and output variables are projected out.

deltas

public RelBody deltas(int eq_no)

deltasToRelation

public RelBody deltasToRelation(int n_inputs,
                                int n_outputs)

complement

public RelBody complement()

complement. not F

projectOntoJust

public RelBody projectOntoJust(VarDecl v)

union

public RelBody union(RelBody r2)

r1 Union r2. align the input tuples (if any) for F and G align the output tuples (if any) for F and G match named variables in F and G formula is f | g

intersection

public RelBody intersection(RelBody r2)

F intersection G. align the input tuples (if any) for F and G align the output tuples (if any) for F and G match named variables in F and G formula is f & g

restrictDomain

public RelBody restrictDomain(RelBody r2)

F \ G (the relation F restricted to domain G). align the input tuples for F and G match named variables in F and G formula is f & g

restrictRange

public RelBody restrictRange(RelBody r2)

F / G (the relation F restricted to range G) align the output tuples for F and G match named variables in F and G formula is f & g

crossProduct

public RelBody crossProduct(RelBody r2)

Cross Product. Give two sets, A and B, create a RelBody whose domain is A and whose range is B.

composition

public RelBody composition(RelBody r2)

Composition(F, G) = F o G, where F o G (x) = F(G(x)) That is, if F = { [i] . [j] : ... } and G = { [x] . [y] : ... } then Composition(F, G) = { [x] . [j] : ... } align the output tuple for G and the input tuple for F, these become existensially quantified variables use the output tuple from F and the input tuple from G for the result match named variables in G and F formula is g & f If there are function symbols of arity > 0, we call special case code to handle them. This is not set up for the r2.isSet case yet.

difference

public RelBody difference(RelBody r2)

F minus G.

doSubsetCheck

public boolean doSubsetCheck(RelBody r2)

project

public RelBody project(GlobalVarDecl g)

Project out global variable g from RelBody r.

projectSym

public RelBody projectSym()

Project all symbolic variables from RelBody r.

project

public RelBody project(int pos,
                       int vkind)

Project an input, output or set variable, leaving a variable in that position with no constraints.

project

public RelBody project(Vector<VarDecl> s)

calculateDimensions

public void calculateDimensions(Conjunct c,
                                int[] dims)

trueRelation

public RelBody trueRelation()

trueRelation

public static RelBody trueRelation(OmegaLib omegaLib,
                                   int setvars)

trueRelation

public static RelBody trueRelation(OmegaLib omegaLib,
                                   int in,
                                   int out)

falseRelation

public RelBody falseRelation()

falseRelation

public static RelBody falseRelation(OmegaLib omegaLib,
                                    int setvars)

falseRelation

public static RelBody falseRelation(OmegaLib omegaLib,
                                    int in,
                                    int out)

emptyRelation

public RelBody emptyRelation()

unknownRelation

public RelBody unknownRelation()

unknownRelation

public static RelBody unknownRelation(OmegaLib omegaLib,
                                      int setvars)

unknownRelation

public static RelBody unknownRelation(OmegaLib omegaLib,
                                      int in,
                                      int out)

hull

public RelBody hull(boolean stridesAllowed,
                    int effort,
                    RelBody knownHull)

checkForConvexPairs

public RelBody checkForConvexPairs()

vennDiagramForm

public RelBody vennDiagramForm(RelBody context)

checkForConvexRepresentation

public RelBody checkForConvexRepresentation()

gistSingleConjunct

public RelBody gistSingleConjunct(RelBody R2,
                                  int effort)

Compute (gist r1 given r2). Currently we assume that r2 has only one conjunct. r2 may have zero input and output OR may have # in/out vars equal to r1.

gist

public RelBody gist(RelBody R2,
                    int effort)

Compute gist(r1) given r2. Relation r2 can have multiple conjuncts.

isDOK

public boolean isDOK(RelBody D,
                     RelBody AxA)

Check if we can use D instead of R. i.e. D intersection (A cross A) is mustBeSubset of R

identity

public static RelBody identity(OmegaLib omegaLib,
                               int numberInputp)

Identity.

identity

public RelBody identity()

tryConjunctTransitiveClosure

public RelBody tryConjunctTransitiveClosure(RelBody iterationSpace,
                                            RelBody rPlus)

Try to get conjunct transitive closure. it we can get it easy get it, return true. if not - return false

equal

public boolean equal(RelBody r2)

decoupledConvexHull

public RelBody decoupledConvexHull()

convexHull

public RelBody convexHull()

affineHull

public RelBody affineHull()

linearHull

public RelBody linearHull()

conicHull

public RelBody conicHull()

conicClosure

public RelBody conicClosure()

join

public RelBody join(RelBody G)

transitiveClosure0

public RelBody transitiveClosure0(int maxExpansion,
                                  RelBody iterationSpace)

Transitive closure of the RelBody containing multiple conjuncts.

transitiveClosure

public RelBody transitiveClosure(int maxExpansion,
                                 RelBody iterationSpace)