JSHOP2
Class PreconditionForAll

java.lang.Object
  extended by JSHOP2.Precondition
      extended by JSHOP2.PreconditionForAll

public class PreconditionForAll
extends Precondition

This class represents an iterator over all the possible bindings that can satisfy a ForAll logical expression at run time. Note that in this case there is at most one such binding, and that is the empty binding.

Version:
1.0.3
Author:
Okhtay Ilghami, http://www.cs.umd.edu/~okhtay

Field Summary
private  Precondition consequence
          The consequence of the ForAll logical expression this object represents.
private  Term[] currentBinding
          To keep track of the bindings seen so far.
private  Precondition premise
          The premise of the ForAll logical expression this object represents.
private  Term[] retVal
          The array this object will return as its next binding.
 
Fields inherited from class JSHOP2.Precondition
bindings, bindingsIdx
 
Constructor Summary
PreconditionForAll(Precondition premiseIn, Precondition consequenceIn, int vars)
          To initialize this ForAll logical expression.
 
Method Summary
 void bind(Term[] binding)
          To bind the ForAll logical expression to some binding.
protected  Term[] nextBindingHelper()
          To return the next satisfier for this ForAll logical expression, which is either null or an empty binding.
protected  void resetHelper()
          To reset this ForAll logical expression.
 
Methods inherited from class JSHOP2.Precondition
nextBinding, reset, setComparator, setFirst
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

consequence

private Precondition consequence
The consequence of the ForAll logical expression this object represents.


currentBinding

private Term[] currentBinding
To keep track of the bindings seen so far.


premise

private Precondition premise
The premise of the ForAll logical expression this object represents.


retVal

private Term[] retVal
The array this object will return as its next binding.

Constructor Detail

PreconditionForAll

public PreconditionForAll(Precondition premiseIn,
                          Precondition consequenceIn,
                          int vars)
To initialize this ForAll logical expression.

Parameters:
premiseIn - the premise of the ForAll logical expression this object represents.
consequenceIn - the consequence of the ForAll logical expression this object represents.
vars - the number of variables this logical expression has. This is used to return a binding of the appropriate size.
Method Detail

bind

public void bind(Term[] binding)
To bind the ForAll logical expression to some binding.

Specified by:
bind in class Precondition
Parameters:
binding - the given binding.

nextBindingHelper

protected Term[] nextBindingHelper()
To return the next satisfier for this ForAll logical expression, which is either null or an empty binding.

Specified by:
nextBindingHelper in class Precondition

resetHelper

protected void resetHelper()
To reset this ForAll logical expression.

Specified by:
resetHelper in class Precondition