scale.score.dependence.omega.omegaLib
Class DNF

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

public final class DNF
extends java.lang.Object

DNF.

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

Field Summary

int

id

Constructor Summary

DNF(OmegaLib omegaLib)

Method Summary

void	addConjunct(Conjunct conj)
void	after(RelBody r, int preserved_positions)
void	appendClausesToList(Vector<Relation> l, int depth, RelBody rel)
void	assertLeadingInfo()
void	clear()
DNF	conjAndNotDnf(Conjunct positive_conjunct, boolean weak) Compute C0 and not (C1 or C2 or ...
void	convertEQstoGEQs()
DNF	copy(OmegaLib omegaLib, RelBody rel_body)
void	countLeadingZeros()
static int	created()
void	delete()
void	deltas()
void	dimensions(RelBody r, int[] dims)
DNF	DNFandDNF(DNF dnf2) DNF1 & DNF2 => DNF.
void	DNFizeH(Vector<VarDecl> myLocals)
void	DNFtoFormula(Formula root) Convert DNF to Formula and add it root.
void	domain(RelBody r, int a)
void	farkas()
HashSet<VarDecl>	fastTightHull()
Vector<Conjunct>	getConjList()
Conjunct	getSingleConjunct()
DNF	gistSingleConjunct(Conjunct known, RelBody r1, int effort)
boolean	hasSingleConjunct()
void	interpretUnknownAsTrue()
boolean	isDefinitelyFalse()
boolean	isDefinitelyTrue()
boolean	isExact()
boolean	isLowerBoundSatisfiable() Check if there exist any exact conjuncts in the solution.
void	join_conjAndNotDnf(DNF pdnf, DNF neg_conjs)
void	joinDNF(DNF dnf)
int	length()
int	localStatus()
void	makeLevelCarriedTo(int level) Add level-carried DNF form out to level "level".
static int	maxSize()
int	minNumEQs()
void	prefixPrint()
void	prefixPrint(boolean debug, boolean parent_names_setup)
void	print()
java.lang.String	printToString()
boolean	queryDifference(VarDecl v1, VarDecl v2, int[] bounds)
int	queryGuaranteedLeadingZeros(int what_to_return_for_empty_dnf) Return x such that for all conjuncts c, c has >= x leading 0s.
int	queryLeadingDir()
int	queryPossibleLeadingZeros(int numberInputput_and_output) Return x such that for all conjuncts c, c has <= x leading 0s.
void	queryVariableBounds(VarDecl v, int[] bounds)
void	range(RelBody r, int a)
DNF	realNegConjs()
boolean	redSimplifyProblem(DNF dnf2)
void	remap()
void	remapDNFVars(RelBody ref_rel)
void	removeConjunct(Conjunct c)
Conjunct	removeFirstConjunct()
void	removeInexactConjunct()
void	reorderAndSimplify(RelBody r, boolean strides_allowed)
void	reverseLeadingDirInfo()
void	rmRedundantConjs(int effort) Remove redundant conjuncts from given DNF.
void	rmRedundantInexactConjs() Remove inexact conjuncts from given DNF if it contains UNKNOWN conjunct.
void	setParentRel(RelBody rel)
void	setupNames()
void	simplify(int sRdtConstraints) Simplify all conjuncts in a DNF
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

id

public int id

Constructor Detail

DNF

public DNF(OmegaLib omegaLib)

Method Detail

created

public static int created()

maxSize

public static int maxSize()

copy

public DNF copy(OmegaLib omegaLib,
                RelBody rel_body)

delete

public void delete()

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

print

public void print()

printToString

public java.lang.String printToString()

prefixPrint

public void prefixPrint()

prefixPrint

public void prefixPrint(boolean debug,
                        boolean parent_names_setup)

isDefinitelyFalse

public boolean isDefinitelyFalse()

isDefinitelyTrue

public boolean isDefinitelyTrue()

length

public int length()

getConjList

public Vector<Conjunct> getConjList()

getSingleConjunct

public Conjunct getSingleConjunct()

hasSingleConjunct

public boolean hasSingleConjunct()

removeFirstConjunct

public Conjunct removeFirstConjunct()

clear

public void clear()

queryGuaranteedLeadingZeros

public int queryGuaranteedLeadingZeros(int what_to_return_for_empty_dnf)

Return x such that for all conjuncts c, c has >= x leading 0s. If it is a set, always returns -1. The argument specifies if it is a set or relation.

queryPossibleLeadingZeros

public int queryPossibleLeadingZeros(int numberInputput_and_output)

Return x such that for all conjuncts c, c has <= x leading 0s. If no conjuncts, return the argument.

queryLeadingDir

public int queryLeadingDir()

simplify

public void simplify(int sRdtConstraints)

Simplify all conjuncts in a DNF

makeLevelCarriedTo

public void makeLevelCarriedTo(int level)

Add level-carried DNF form out to level "level".

countLeadingZeros

public void countLeadingZeros()

addConjunct

public void addConjunct(Conjunct conj)

joinDNF

public void joinDNF(DNF dnf)

removeConjunct

public void removeConjunct(Conjunct c)

rmRedundantConjs

public void rmRedundantConjs(int effort)

Remove redundant conjuncts from given DNF. If (C1 => C2), remove C1. C1 => C2 is TRUE: when problem where C1 is Black and C2 is Red Blk Red : has no red constraints. It means that C1 is a subset of C2 and therefore C1 is redundant. Exception: C1 => UNKNOWN - leave them as they are

rmRedundantInexactConjs

public void rmRedundantInexactConjs()

Remove inexact conjuncts from given DNF if it contains UNKNOWN conjunct.

DNFtoFormula

public void DNFtoFormula(Formula root)

Convert DNF to Formula and add it root.

remap

public void remap()

setupNames

public void setupNames()

removeInexactConjunct

public void removeInexactConjunct()

DNFandDNF

public DNF DNFandDNF(DNF dnf2)

DNF1 & DNF2 => DNF.

conjAndNotDnf

public DNF conjAndNotDnf(Conjunct positive_conjunct,
                         boolean weak)

Compute C0 and not (C1 or C2 or ... CN). Reuse/delete its arguments.

dimensions

public void dimensions(RelBody r,
                       int[] dims)

reverseLeadingDirInfo

public void reverseLeadingDirInfo()

interpretUnknownAsTrue

public void interpretUnknownAsTrue()

setParentRel

public void setParentRel(RelBody rel)

isLowerBoundSatisfiable

public boolean isLowerBoundSatisfiable()

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

queryDifference

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

queryVariableBounds

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

assertLeadingInfo

public void assertLeadingInfo()

domain

public void domain(RelBody r,
                   int a)

range

public void range(RelBody r,
                  int a)

reorderAndSimplify

public void reorderAndSimplify(RelBody r,
                               boolean strides_allowed)

redSimplifyProblem

public boolean redSimplifyProblem(DNF dnf2)

fastTightHull

public HashSet<VarDecl> fastTightHull()

deltas

public void deltas()

farkas

public void farkas()

appendClausesToList

public void appendClausesToList(Vector<Relation> l,
                                int depth,
                                RelBody rel)

convertEQstoGEQs

public void convertEQstoGEQs()

minNumEQs

public int minNumEQs()

DNFizeH

public void DNFizeH(Vector<VarDecl> myLocals)

realNegConjs

public DNF realNegConjs()

join_conjAndNotDnf

public void join_conjAndNotDnf(DNF pdnf,
                               DNF neg_conjs)

remapDNFVars

public void remapDNFVars(RelBody ref_rel)

gistSingleConjunct

public DNF gistSingleConjunct(Conjunct known,
                              RelBody r1,
                              int effort)

after

public void after(RelBody r,
                  int preserved_positions)

isExact

public boolean isExact()

localStatus

public int localStatus()