scale.score.dependence.omega.omegaLib
Class Formula

java.lang.Object
  extended by 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 222n. 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()