scale.score.dependence.omega.omegaLib
Class Formula

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

Direct Known Subclasses:

FAnd, FDeclaration, FNot, FOr, RelBody

public abstract class Formula
extends java.lang.Object

Presburger Formula base class.

$Id: Formula.java,v 1.14 2005-02-07 21:28:40 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

Presburger formulas are those formulas that can be constructed by combining affine constraints on integer variables with the logical operations not, and and or, and the quantifiers forall and there-exists. The affine constraints can be either equality constraints or inequality constraints (abbreviated as EQs and GEQs respectively). There are a number of algorithms for testing the satisfiability of arbitrary Presburger formulas.

The best known upper bound on the performance of an algorithm for verifying Presburger formulas is 2²²ⁿ. and we have no reason to believe that the omegaLib provides better worst-case performance. However, it may be more efficient for the many simple cases that arise in compiler applications.

Field Summary

protected Vector<Formula>	myChildren
protected Formula	myParent
protected RelBody	myRelation
protected OmegaLib	omegaLib
static int	OP_AND
static int	OP_CONJUNCT
static int	OP_EXISTS
static int	OP_FORALL
static int	OP_NOT
static int	OP_OR
static int	OP_RELATION

Constructor Summary

protected	Formula(OmegaLib omegaLib)
protected	Formula(OmegaLib omegaLib, Formula p, RelBody r)

Method Summary

FAnd	addAnd()
protected void	addChild(Formula kid) Add the formula as a child of this formula.
protected Conjunct	addConjunct()
FExists	addExists()
FExists	addExists(Vector<VarDecl> S)
FForall	addForall()
FNot	addNot()
FOr	addOr()
FAnd	andWith()
void	assertNotFinalized()
void	beautify()
boolean	canAddChild()
protected void	checkAndAddChild(Formula kid) If this formula can have children, add the formula as a child of this formula.
Vector<Formula>	children()
protected void	combineColumns()
abstract Formula	copy(Formula f, RelBody b)
void	delete()
abstract DNF	DNFize()
void	enforceLeadingInfo(int guaranteed, int possible, int dir)
abstract Conjunct	findAvailableConjunct()
Vector<Formula>	getChildren()
protected Formula	getFirstChild()
void	invalidateLeadingInfo(int changed)
abstract int	nodeType()
int	numberOfChildren()
protected void	olAssert(boolean t)
protected void	olAssert(boolean t, java.lang.String msg)
Formula	parent()
void	prefixPrint(boolean debug)
void	print()
void	printSeparator()
int	priority()
protected void	pushExists(Vector<VarDecl> vid) Push exists takes responsibility for the VarDecls.
Conjunct	reallyConjunct()
void	rearrange()
RelBody	relation()
void	remap() Remap mappedVars in all conjuncts of formula.
protected void	removeChild(Formula kid)
protected Formula	removeFirstChild()
void	reverseLeadingDirInfo()
void	setFinalized()
void	setParent(Formula p)
void	setParent(Formula parent, RelBody reln)
void	setRelation(RelBody r)
void	setupNames()
java.lang.String	toString()
java.lang.String	toStringClass() Convert the class name of this node to a string representation.
void	verifytree()

Methods inherited from class java.lang.Object

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

Field Detail

OP_RELATION

public static final int OP_RELATION

See Also:

Constant Field Values

OP_NOT

public static final int OP_NOT

See Also:

Constant Field Values

OP_AND

public static final int OP_AND

See Also:

Constant Field Values

OP_OR

public static final int OP_OR

See Also:

Constant Field Values

OP_CONJUNCT

public static final int OP_CONJUNCT

See Also:

Constant Field Values

OP_FORALL

public static final int OP_FORALL

See Also:

Constant Field Values

OP_EXISTS

public static final int OP_EXISTS

See Also:

Constant Field Values

omegaLib

protected OmegaLib omegaLib

myChildren

protected Vector<Formula> myChildren

myParent

protected Formula myParent

myRelation

protected RelBody myRelation

Constructor Detail

Formula

protected Formula(OmegaLib omegaLib,
                  Formula p,
                  RelBody r)

Formula

protected Formula(OmegaLib omegaLib)

Method Detail

delete

public void delete()

setFinalized

public void setFinalized()

toStringClass

public final java.lang.String toStringClass()

Convert the class name of this node to a string representation.

olAssert

protected void olAssert(boolean t)

olAssert

protected void olAssert(boolean t,
                        java.lang.String msg)

canAddChild

public boolean canAddChild()

nodeType

public abstract int nodeType()

addForall

public FForall addForall()

addExists

public FExists addExists()

addExists

public FExists addExists(Vector<VarDecl> S)

andWith

public FAnd andWith()

addAnd

public FAnd addAnd()

addOr

public FOr addOr()

addNot

public FNot addNot()

relation

public RelBody relation()

removeFirstChild

protected Formula removeFirstChild()

getFirstChild

protected Formula getFirstChild()

removeChild

protected void removeChild(Formula kid)

checkAndAddChild

protected void checkAndAddChild(Formula kid)

If this formula can have children, add the formula as a child of this formula. Abort oterwise. The parent of the child is set to this formula and the relation of the child is set to the relation of this formula.

addChild

protected void addChild(Formula kid)

Add the formula as a child of this formula. The parent and the relation of the child are assumed to be set already.

addConjunct

protected Conjunct addConjunct()

findAvailableConjunct

public abstract Conjunct findAvailableConjunct()

pushExists

protected void pushExists(Vector<VarDecl> vid)

Push exists takes responsibility for the VarDecls. It should: Re-use them, or Delete them.

children

public Vector<Formula> children()

numberOfChildren

public int numberOfChildren()

getChildren

public Vector<Formula> getChildren()

parent

public Formula parent()

setParent

public void setParent(Formula p)

verifytree

public void verifytree()

reverseLeadingDirInfo

public void reverseLeadingDirInfo()

invalidateLeadingInfo

public void invalidateLeadingInfo(int changed)

enforceLeadingInfo

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

remap

public void remap()

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

DNFize

public abstract DNF DNFize()

copy

public abstract Formula copy(Formula f,
                             RelBody b)

beautify

public void beautify()

rearrange

public void rearrange()

setupNames

public void setupNames()

combineColumns

protected void combineColumns()

setRelation

public void setRelation(RelBody r)

setParent

public void setParent(Formula parent,
                      RelBody reln)

assertNotFinalized

public void assertNotFinalized()

reallyConjunct

public Conjunct reallyConjunct()

priority

public int priority()

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

print

public void print()

prefixPrint

public void prefixPrint(boolean debug)

printSeparator

public void printSeparator()