scale.score.dependence.omega.omegaLib
Class Conjunct

java.lang.Object
  scale.score.dependence.omega.omegaLib.Formula
      scale.score.dependence.omega.omegaLib.FDeclaration
          scale.score.dependence.omega.omegaLib.Conjunct

public final class Conjunct
extends FDeclaration

Conjunct.

$Id: Conjunct.java,v 1.16 2007-10-04 19:58:25 burrill 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

About variables in Conjunct:

• All varaibles appear in exactly one declaration.
• All variables used in Conjunct are referenced in mappedVars.
• Wildcard variables are referenced both in mappedVars and in myLocals, since they are declared in the conjunct.
• All other variables are declared at the levels above.

Column number is:

• in forwardingAddress in Problem if variablesInitialized is set,
• equal to position of VarDecl in mappedVars list otherwise.

Field Summary

static int	ANY_NEGATION
static int	AvoidNegating
static int	CantBeNegated
static char[]	dirGlyphs
static int	EVAC_AFFINE
static int	EVAC_NASTY
static int	EVAC_OFFSET
static int	EVAC_OFFSET_subseq
static int	EVAC_SUBSEQ
static int	EVAC_TRIVIAL
int	id
static int	MERGE_COMPOSE
static int	MERGE_GIST
static int	MERGE_REGULAR
static int	ONE_GEQ_OR_EQ
static int	ONE_GEQ_OR_STRIDE

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

myLocals

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

Conjunct(Conjunct conj)

Conjunct(OmegaLib omegaLib)

Conjunct(OmegaLib omegaLib, Formula f, RelBody r)

Method Summary

EQHandle	addEQ(boolean preserves_level)
EQHandle	addEQ(ConstraintHandle c, boolean preserves_level)
GEQHandle	addGEQ(boolean preserves_level)
GEQHandle	addGEQ(ConstraintHandle c, boolean preserves_level)
EQHandle	addStride(int step, boolean preserves_level) Create new constraints with all co-efficients 0.
void	after(RelBody r, int preservedPositions)
void	assertLeadingInfo()
void	beautify()
boolean	canAddChild()
boolean	checkLeading0s(int level)
boolean	checkLeading0s(int direction, int level)
void	clearSubs()
protected void	combineColumns()
boolean	constraintIsEqual(Equation eq, Conjunct that, Equation eqt)
void	convertEQstoGEQs()
Conjunct	copy(Formula parent, RelBody rel_body)
void	copyConstraint(Equation eqns, Conjunct from, Equation eq)
int	cost() Cost = # of terms in DNF when negated.
void	countLeadingZeros()
static int	created()
VarDecl	declare()
VarDecl	declare(java.lang.String s)
VarDecl	declare(VarDecl v)
void	delete()
void	deltas()
int	difficulty()
DNF	DNFize()
void	DNFizeH(Vector<VarDecl> locals_copy)
void	domain(RelBody r, int a)
void	enforceLeadingInfo(int guaranteed, int possible, int dir)
void	extractNonWildVars(Vector<VarDecl> allVars)
void	farkas()
void	fastTightHull(HashSet<VarDecl> vars)
Conjunct	findAvailableConjunct()
int	findColumn(VarDecl D)
int	getColumn(VarDecl D) Return column for D in conjunct.
Equation[]	getEQs()
Equation[]	getGEQs()
int	getGuaranteedLeading0s()
int	getNumEQs()
int	getNumGEQs()
Problem	getProblem()
java.lang.String	getVarName(int col)
boolean	hasWildcards(Equation eq)
int	hull(Equation eq, Conjunct that, Equation eqt)
void	interpretUnknownAsTrue()
void	invalidateLeadingInfo(int changed)
boolean	isEmpty()
boolean	isExact()
boolean	isInexact()
boolean	isTrue()
boolean	isUnknown()
boolean	leadingDirValidAndKnown()
void	makeInexact()
void	makeLevelCarriedTo(DNF newstuff, int split_to, int level)
int	maxTuplePosition(Equation eq)
int	maxUfsArityOfIn()
int	maxUfsArityOfOut()
int	maxUfsArityOfSet()
Conjunct	mergeConjuncts(Conjunct conj2, int action, RelBody body) Merge CONJ1 & CONJ2 => CONJ.
DNF	negateConjunct() ~CONJ => DNF
int	nodeType()
int	numVars()
void	orderedElimination(int symLen)
boolean	parallel(Equation eq, Conjunct that, Equation eqt)
void	prefixPrint()
void	prefixPrint(boolean debug)
void	print()
java.lang.String	printEQtoString(Equation e)
java.lang.String	printGEQtoString(Equation e)
java.lang.String	printSubToString(int col)
java.lang.String	printTermToString(Equation e)
java.lang.String	printToString(boolean true_printed)
int	priority()
void	promiseThatUbSolutionsExist()
protected void	pushExists(Vector<VarDecl> S) Add given list of wildcards S to this Conjunct.
boolean	queryDifference(VarDecl v1, VarDecl v2, int[] bounds)
int	queryGuaranteedLeadingZeros()
int	queryLeadingDir()
int	queryPossibleLeadingZeros()
void	queryVariableBounds(VarDecl v, int[] bounds)
void	range(RelBody r, int a)
Conjunct	reallyConjunct()
void	recomputeMappedVars()
int	redSimplifyProblem(int effort, boolean computeGist)
void	remap() Remap mappedVars in all conjuncts of formula.
void	remapDNFVars(RelBody ref_rel)
void	removeColorConstraints()
void	reorderAndSimplify(RelBody r, boolean stridesAllowed)
void	reorderForPrint(boolean reverseOrder, int first_pass_input, int first_pass_output, boolean sort)
void	reverseLeadingDirInfo()
boolean	simplifyConjunct(boolean ver_sim, int simplificationEffort, int color) Simplify Conjunct.
boolean	simplifyProblem(boolean verify, int redundantElimination)
java.lang.String	toString()
java.lang.String	tryToPrintVarToStringWithDiv(VarDecl v)
Vector<VarDecl>	variables()
boolean	varIsConstant(VarDecl v, Equation eq)

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

declareTuple, doDeclare, locals, setupAnonymousWildcardNames, setupNames

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

addAnd, addChild, addConjunct, addExists, addExists, addForall, addNot, addOr, andWith, assertNotFinalized, checkAndAddChild, children, getChildren, getFirstChild, numberOfChildren, olAssert, olAssert, parent, printSeparator, rearrange, relation, removeChild, removeFirstChild, setFinalized, setParent, setParent, setRelation, toStringClass, verifytree

Methods inherited from class java.lang.Object

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

Field Detail

CantBeNegated

public static final int CantBeNegated

See Also:

Constant Field Values

AvoidNegating

public static final int AvoidNegating

See Also:

Constant Field Values

MERGE_REGULAR

public static final int MERGE_REGULAR

See Also:

Constant Field Values

MERGE_COMPOSE

public static final int MERGE_COMPOSE

See Also:

Constant Field Values

MERGE_GIST

public static final int MERGE_GIST

See Also:

Constant Field Values

dirGlyphs

public static final char[] dirGlyphs

EVAC_TRIVIAL

public static final int EVAC_TRIVIAL

See Also:

Constant Field Values

EVAC_OFFSET

public static final int EVAC_OFFSET

See Also:

Constant Field Values

EVAC_SUBSEQ

public static final int EVAC_SUBSEQ

See Also:

Constant Field Values

EVAC_OFFSET_subseq

public static final int EVAC_OFFSET_subseq

See Also:

Constant Field Values

EVAC_AFFINE

public static final int EVAC_AFFINE

See Also:

Constant Field Values

EVAC_NASTY

public static final int EVAC_NASTY

See Also:

Constant Field Values

ANY_NEGATION

public static final int ANY_NEGATION

See Also:

Constant Field Values

ONE_GEQ_OR_EQ

public static final int ONE_GEQ_OR_EQ

See Also:

Constant Field Values

ONE_GEQ_OR_STRIDE

public static final int ONE_GEQ_OR_STRIDE

See Also:

Constant Field Values

id

public int id

Constructor Detail

Conjunct

public Conjunct(OmegaLib omegaLib)

Conjunct

public Conjunct(OmegaLib omegaLib,
                Formula f,
                RelBody r)

Conjunct

public Conjunct(Conjunct conj)

Method Detail

created

public static int created()

copy

public Conjunct copy(Formula parent,
                     RelBody rel_body)

Specified by:

copy in class Formula

delete

public void delete()

Overrides:

delete in class Formula

toString

public java.lang.String toString()

Overrides:

toString in class Formula

leadingDirValidAndKnown

public boolean leadingDirValidAndKnown()

variables

public Vector<VarDecl> variables()

numVars

public int numVars()

getEQs

public Equation[] getEQs()

getNumEQs

public int getNumEQs()

getGEQs

public Equation[] getGEQs()

getNumGEQs

public int getNumGEQs()

getProblem

public Problem getProblem()

hasWildcards

public boolean hasWildcards(Equation eq)

maxTuplePosition

public int maxTuplePosition(Equation eq)

varIsConstant

public boolean varIsConstant(VarDecl v,
                             Equation eq)

promiseThatUbSolutionsExist

public void promiseThatUbSolutionsExist()

maxUfsArityOfSet

public int maxUfsArityOfSet()

maxUfsArityOfIn

public int maxUfsArityOfIn()

maxUfsArityOfOut

public int maxUfsArityOfOut()

nodeType

public int nodeType()

Specified by:

nodeType in class Formula

isTrue

public boolean isTrue()

isEmpty

public boolean isEmpty()

clearSubs

public void clearSubs()

queryDifference

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

queryVariableBounds

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

difficulty

public int difficulty()

queryGuaranteedLeadingZeros

public int queryGuaranteedLeadingZeros()

getGuaranteedLeading0s

public int getGuaranteedLeading0s()

queryPossibleLeadingZeros

public int queryPossibleLeadingZeros()

queryLeadingDir

public int queryLeadingDir()

isUnknown

public boolean isUnknown()

isExact

public boolean isExact()

isInexact

public boolean isInexact()

makeInexact

public void makeInexact()

simplifyConjunct

public boolean simplifyConjunct(boolean ver_sim,
                                int simplificationEffort,
                                int color)

Simplify Conjunct. Return true if there are solutions.

recomputeMappedVars

public void recomputeMappedVars()

assertLeadingInfo

public void assertLeadingInfo()

tryToPrintVarToStringWithDiv

public java.lang.String tryToPrintVarToStringWithDiv(VarDecl v)

print

public void print()

Overrides:

print in class FDeclaration

prefixPrint

public void prefixPrint()

prefixPrint

public void prefixPrint(boolean debug)

Overrides:

prefixPrint in class FDeclaration

printToString

public java.lang.String printToString(boolean true_printed)

printEQtoString

public java.lang.String printEQtoString(Equation e)

printGEQtoString

public java.lang.String printGEQtoString(Equation e)

printTermToString

public java.lang.String printTermToString(Equation e)

printSubToString

public java.lang.String printSubToString(int col)

interpretUnknownAsTrue

public void interpretUnknownAsTrue()

reallyConjunct

public Conjunct reallyConjunct()

Overrides:

reallyConjunct in class Formula

addStride

public EQHandle addStride(int step,
                          boolean preserves_level)

Create new constraints with all co-efficients 0. These are public in FAnd, use them from there.

addEQ

public EQHandle addEQ(boolean preserves_level)

addGEQ

public GEQHandle addGEQ(boolean preserves_level)

addEQ

public EQHandle addEQ(ConstraintHandle c,
                      boolean preserves_level)

addGEQ

public GEQHandle addGEQ(ConstraintHandle c,
                        boolean preserves_level)

copyConstraint

public void copyConstraint(Equation eqns,
                           Conjunct from,
                           Equation eq)

canAddChild

public boolean canAddChild()

Overrides:

canAddChild in class FDeclaration

remap

public void remap()

Description copied from class: Formula

Remap mappedVars in all conjuncts of formula. Uses the remap field of the VarDecl.

Overrides:

remap in class Formula

beautify

public void beautify()

Overrides:

beautify in class Formula

DNFize

public DNF DNFize()

Specified by:

DNFize in class Formula

DNFizeH

public void DNFizeH(Vector<VarDecl> locals_copy)

priority

public int priority()

Overrides:

priority in class FDeclaration

findAvailableConjunct

public Conjunct findAvailableConjunct()

Specified by:

findAvailableConjunct in class Formula

getVarName

public java.lang.String getVarName(int col)

declare

public VarDecl declare(java.lang.String s)

Overrides:

declare in class FDeclaration

declare

public VarDecl declare()

Specified by:

declare in class FDeclaration

declare

public VarDecl declare(VarDecl v)

Specified by:

declare in class FDeclaration

pushExists

protected void pushExists(Vector<VarDecl> S)

Add given list of wildcards S to this Conjunct. Clears argument. (That's very important, otherwise those var_id's get freed) Push_exists takes responsibility for reusing or deleting Var_ID's; here we reuse them. Must also empty out the Tuple when finished (joins).

Overrides:

pushExists in class Formula

getColumn

public int getColumn(VarDecl D)

Return column for D in conjunct.

findColumn

public int findColumn(VarDecl D)

combineColumns

protected void combineColumns()

Overrides:

combineColumns in class Formula

reorderForPrint

public void reorderForPrint(boolean reverseOrder,
                            int first_pass_input,
                            int first_pass_output,
                            boolean sort)

countLeadingZeros

public void countLeadingZeros()

enforceLeadingInfo

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

Overrides:

enforceLeadingInfo in class Formula

invalidateLeadingInfo

public void invalidateLeadingInfo(int changed)

Overrides:

invalidateLeadingInfo in class Formula

reverseLeadingDirInfo

public void reverseLeadingDirInfo()

Overrides:

reverseLeadingDirInfo in class Formula

removeColorConstraints

public void removeColorConstraints()

orderedElimination

public void orderedElimination(int symLen)

convertEQstoGEQs

public void convertEQstoGEQs()

cost

public int cost()

Cost = # of terms in DNF when negated. Cost = CantBeNegated if too bad (i.e. bad wildcards). Cost = AvoidNegating if it would be inexact. Also check presLegalNegations --

• If set to ANY_NEGATION, just return the number
• If set to ONE_GEQ_OR_STRIDE, return CantBeNegated if c > 1
• If set to ONE_GEQ_OR_EQ, return CantBeNegated if not a single geq or eq

simplifyProblem

public boolean simplifyProblem(boolean verify,
                               int redundantElimination)

redSimplifyProblem

public int redSimplifyProblem(int effort,
                              boolean computeGist)

mergeConjuncts

public Conjunct mergeConjuncts(Conjunct conj2,
                               int action,
                               RelBody body)

Merge CONJ1 & CONJ2 => CONJ. Action:

• MERGE_REGULAR or MERGE_COMPOSE: regular merge.
• MERGE_GIST make constraints from conj2 red, i.e. Gist Conj2 given Conj1 (T.S. comment).

Reorder columns as we go. Merge the columns for identical variables. We assume we know nothing about the ordering of conj1, conj2.

Does not consume its arguments

Optional 4th argument gives the relation for the result - if null, conj1 and conj2 must have the same relation, which will be used for the result

The only members of conj1 and conj2 that are used are: problem, mappedVars and declare(), and the leading_0s/leading_dir members and exact.

NOTE: variables that are shared between conjuncts are necessarily declared above, not here; so we can simply create columns for the locals of each conj after doing the protected vars.

negateConjunct

public DNF negateConjunct()

~CONJ => DNF

reorderAndSimplify

public void reorderAndSimplify(RelBody r,
                               boolean stridesAllowed)

domain

public void domain(RelBody r,
                   int a)

range

public void range(RelBody r,
                  int a)

after

public void after(RelBody r,
                  int preservedPositions)

deltas

public void deltas()

checkLeading0s

public boolean checkLeading0s(int direction,
                              int level)

checkLeading0s

public boolean checkLeading0s(int level)

remapDNFVars

public void remapDNFVars(RelBody ref_rel)

extractNonWildVars

public void extractNonWildVars(Vector<VarDecl> allVars)

makeLevelCarriedTo

public void makeLevelCarriedTo(DNF newstuff,
                               int split_to,
                               int level)

parallel

public boolean parallel(Equation eq,
                        Conjunct that,
                        Equation eqt)

hull

public int hull(Equation eq,
                Conjunct that,
                Equation eqt)

constraintIsEqual

public boolean constraintIsEqual(Equation eq,
                                 Conjunct that,
                                 Equation eqt)

farkas

public void farkas()

fastTightHull

public void fastTightHull(HashSet<VarDecl> vars)