VariableState Class Reference

Represents the state of propositional variables and clauses. More...

#include <variablestate.h>

List of all members.

Public Member Functions
	VariableState (GroundPredicateHashArray *const &unknownQueries, GroundPredicateHashArray *const &knownQueries, Array< TruthValue > *const &knownQueryValues, const Array< int > *const &allPredGndingsAreQueries, const bool &markHardGndClauses, const bool &trackParentClauseWts, const MLN *const &mln, const Domain *const &domain, const bool &lazy)
	Constructor for a VariableState.
	~VariableState ()
	Destructor.
void	addNewClauses (bool initial)
	New clauses are added to the state.
void	init ()
	Information about the state is reset and initialized.
void	reinit ()
	State is re-initialized with all new clauses and atoms.
void	initRandom ()
	Makes a random truth assigment to all (active) atoms.
void	initBlocksRandom ()
	Sets one atom in each block to true and the rest to false.
void	resetMakeBreakCostWatch ()
	Resets the makeCost, breakCost and watch arrays.
void	initMakeBreakCostWatch ()
	Re-initializes the makeCost, breakCost and watch arrays based on the current variable assignment.
void	initMakeBreakCostWatch (const int &startClause)
	Initialize makeCost and breakCost and watch arrays based on the current variable assignment.
int	getNumAtoms ()
int	getNumClauses ()
int	getNumDeadClauses ()
int	getIndexOfRandomAtom ()
	Returns the absolute index of a random atom.
int	getIndexOfAtomInRandomFalseClause ()
	Returns the absolute index of a random atom in a random unsatisfied pos.
int	getRandomFalseClauseIndex ()
	Returns the index of a random unsatisfied pos.
long double	getCostOfFalseClauses ()
	Returns the cost of the unsatisfied positive and satisfied negative clauses.
int	getNumFalseClauses ()
	Returns the number of the unsatisfied positive and satisfied negative clauses.
bool	getValueOfAtom (const int &atomIdx)
	Returns the truth value of an atom.
bool	getValueOfLowAtom (const int &atomIdx)
	Returns the truth value of an atom in the best state.
void	setValueOfAtom (const int &atomIdx, const bool &value, const bool &activate, const int &blockIdx)
	Sets the truth value of an atom.
Array< int > &	getNegOccurenceArray (const int &atomIdx)
	Retrieves the negative occurence array of an atom.
Array< int > &	getPosOccurenceArray (const int &atomIdx)
	Retrieves the positive occurence array of an atom.
void	flipAtom (const int &toFlip, const int &blockIdx)
	Flip the truth value of an atom and update info arrays.
void	flipAtomValue (const int &atomIdx, const int &blockIdx)
	Flips the truth value of an atom.
long double	getImprovementByFlipping (const int &atomIdx)
	Calculates the improvement achieved by flipping an atom.
void	setActive (const int &atomIdx)
	Set the active status of an atom to true in the database if in lazy mode.
bool	activateAtom (const int &atomIdx, const bool &ignoreActivePreds, const bool &groundOnly)
	If in lazy mode, an atom is activated and all clauses activated by this atom are added to the state.
void	setInferenceMode (int mode)
	Set the inference mode currently being used.
bool	isFixedAtom (int atomIdx)
	Returns true, if an atom is fixed to true or false.
bool	isSatisfiedClause (const int &clauseIdx)
void	setSatisfiedClause (const int &clauseIdx)
void	updatePrevSatisfied ()
void	unitPropagation ()
	Perform unit propagation on the current clauses.
void	addNewClauses (int addType, Array< GroundClause * > &clauses)
	Adds new clauses to the state.
void	updateSatisfiedClauses (const int &toFix)
	Updates isSatisfiedClause after an atom is fixed.
void	updateMakeBreakCostAfterFlip (const int &toFlip)
	Updates cost after flip.
bool	isActive (const int &atomIdx)
	Checks if an atom is active.
bool	isActive (const Predicate *pred)
	Checks if an atom is active.
Array< int > &	getOccurenceArray (const int &idx)
	Retrieves the occurence array of an atom.
int	incrementNumTrueLits (const int &clauseIdx)
	Increments the number of true literals in a clause.
int	decrementNumTrueLits (const int &clauseIdx)
	Decrements the number of true literals in a clause.
int	getNumTrueLits (const int &clauseIdx)
	Retrieves the number of true literals in a clause.
long double	getClauseCost (const int &clauseIdx)
	Retrieves the cost associated with a clause.
Array< int > &	getAtomsInClause (const int &clauseIdx)
	Retrieves the atoms in a clauses as an Array of ints.
void	addFalseClause (const int &clauseIdx)
	Marks a clause as false in the state.
void	removeFalseClause (const int &clauseIdx)
	Unmarks a clause as false in the state.
void	addBreakCost (const int &atomIdx, const long double &cost)
	Increases the breakcost of an atom.
void	subtractBreakCost (const int &atomIdx, const long double &cost)
	Decreases the breakcost of an atom.
void	addBreakCostToAtomsInClause (const int &clauseIdx, const long double &cost)
	Increases breakCost of all atoms in a given clause.
void	subtractBreakCostFromAtomsInClause (const int &clauseIdx, const long double &cost)
	Decreases breakCost of all atoms in a given clause.
void	addMakeCost (const int &atomIdx, const long double &cost)
	Increases makeCost of an atom.
void	subtractMakeCost (const int &atomIdx, const long double &cost)
	Decreases makeCost of an atom.
void	addMakeCostToAtomsInClause (const int &clauseIdx, const long double &cost)
	Increases makeCost of all atoms in a given clause.
void	subtractMakeCostFromAtomsInClause (const int &clauseIdx, const long double &cost)
	Decreases makeCost of all atoms in a given clause.
const int	getTrueLiteralOtherThan (const int &clauseIdx, const int &atomIdx1, const int &atomIdx2)
	Retrieves a true literal in a clause other than the two given.
const bool	isTrueLiteral (const int &literal)
	Checks if a literal is true (Negated and false or non-negated an true).
const int	getAtomInClause (const int &atomIdxInClause, const int &clauseIdx)
	Retrieves the absolute index of the nth atom in a clause.
const int	getRandomAtomInClause (const int &clauseIdx)
	Retrieves the absolute index of a random atom in a clause.
const int	getRandomTrueLitInClause (const int &clauseIdx)
	Retrieves the index of a random true literal in a clause.
const double	getMaxClauseWeight ()
const long double	getMakeCost (const int &atomIdx)
const long double	getBreakCost (const int &atomIdx)
const int	getClauseSize (const int &clauseIdx)
const int	getWatch1 (const int &clauseIdx)
void	setWatch1 (const int &clauseIdx, const int &atomIdx)
const int	getWatch2 (const int &clauseIdx)
void	setWatch2 (const int &clauseIdx, const int &atomIdx)
const int	getBlockIndex (const int &atomIdx)
	Returns the index of the block which the atom with index atomIdx is in.
const long double	getLowCost ()
	Returns the cost of bad clauses in the optimum state.
const int	getLowBad ()
	Returns the number of bad clauses in the optimum state.
void	makeUnitCosts ()
	Turns all costs into units.
void	saveLowState ()
	Save current assignment as an optimum state.
int	getTrueFixedAtomInBlock (const int &blockIdx)
	Returns index of an atom if it is true and fixed in block, otherwise -1.
const GroundPredicateHashArray *	getGndPredHashArrayPtr () const
const GroundPredicateHashArray *	getUnePreds () const
const GroundPredicateHashArray *	getKnePreds () const
const Array< TruthValue > *	getKnePredValues () const
void	setGndClausesWtsToSumOfParentWts ()
	Sets the weight of a ground clause to the sum of its parents' weights.
void	getNumClauseGndings (Array< double > *const &numGndings, bool tv)
	Gets the number of (true or false) clause groundings in this state.
void	getNumClauseGndingsWithUnknown (double numGndings[], int clauseCnt, bool tv, const Array< bool > *const &unknownPred)
	Gets the number of (true or false) clause groundings in this state.
void	setOthersInBlockToFalse (const int &atomIdx, const int &blockIdx)
	Sets the truth values of all atoms in a block except for the one given.
void	fixAtom (const int &atomIdx, const bool &value)
	Fixes an atom to a truth value.
Array< int > *	simplifyClauseFromFixedAtoms (const int &clauseIdx)
	Simplifies a clause using atoms which have been fixed.
const bool	isDeadClause (const int &clauseIdx)
	Checks if a clause is dead.
void	eliminateSoftClauses ()
	Marks soft clauses as dead.
void	LoadDisEviValuesFromRst (const char *szDisEvi)
void	killClauses (const int &startClause)
	Marks clauses as dead which were not good in the previous iteration of inference or are not picked according to a weighted coin flip.
const bool	clauseGoodInPrevious (const int &clauseIdx)
	Checks if a clause was good in the previous iteration of inference, i.e.
void	resetDeadClauses ()
	Resets all dead clauses to be alive again.
void	resetFixedAtoms ()
	Resets all fixed atoms to be not fixed again.
void	setLazy (const bool &l)
const bool	getLazy ()
void	setUseThreshold (const bool &t)
const bool	getUseThreshold ()
long double	getHardWt ()
const Domain *	getDomain ()
const MLN *	getMLN ()
void	printLowState (ostream &out)
	Prints the best state found to a stream.
void	printGndPred (const int &predIndex, ostream &out)
	Prints a ground predicate to a stream.
int	getIndexOfGroundPredicate (GroundPredicate *const &gndPred)
	Finds and returns the index of a ground predicate.
void	setAsEvidence (const GroundPredicate *const &predicate, const bool &trueEvidence)
	Sets a GroundPredicate to be evidence and sets its truth value.
void	setAsQuery (const GroundPredicate *const &predicate)
	Sets a GroundPredicate to be query.
GroundPredicate *	getGndPred (const int &index)
	Gets a pointer to a GroundPredicate.
GroundClause *	getGndClause (const int &index)
	Gets a pointer to a GroundClause.
void	saveLowStateToGndPreds ()
	The atom assignment in the best state is saved to the ground predicates.
void	saveLowStateToDB ()
	The atom assignment in the best state is saved to the database.
const int	getGndPredIndex (GroundPredicate *const &gndPred)
	Gets the index of a GroundPredicate in this state.
void	getActiveClauses (Predicate *inputPred, Array< GroundClause * > &activeClauses, bool const &active, bool const &ignoreActivePreds)
	Gets clauses and weights activated by the predicate inputPred, if active is true.
void	getActiveClauses (Array< GroundClause * > &allClauses, bool const &ignoreActivePreds)
	Get all the active clauses in the database.
int	getNumActiveAtoms ()
const void	setBreakHardClauses (const bool &breakHardClauses)
Static Public Attributes
static const int	MODE_MWS = 0
static const int	MODE_HARD = 1
static const int	MODE_SAMPLESAT = 2
static const int	ADD_CLAUSE_INITIAL = 0
static const int	ADD_CLAUSE_REGULAR = 1
static const int	ADD_CLAUSE_DEAD = 2
static const int	ADD_CLAUSE_SAT = 3

---

Detailed Description

Represents the state of propositional variables and clauses.

Some of this code is based on the MaxWalkSat package of Kautz et al.

All inference algorithms should have a VariableState to access the information needed in its predicates and clauses.

Each atom has its own index starting at 1. The negation of an atom with index a is represented by -a (this is why the indices do not start at 0). Each clause has its own index starting at 0.

A VariableState is either eager or lazy. Eager states build an MRF upfront based on an MLN and a domain. Thus, all ground clauses and predicates are in memory after building the MRF. Lazy states activate atoms and clauses as they are needed from the MLN and domain. An atom is activated if it is in an unsatisfied clause with the assumption of all atoms being false or if it is looked at during inference (it is flipped or the cost of flipping it is computed). Active clauses are those which contain active atoms.

Definition at line 97 of file variablestate.h.

---

Constructor & Destructor Documentation

VariableState::VariableState	(	GroundPredicateHashArray *const &	unknownQueries,
		GroundPredicateHashArray *const &	knownQueries,
		Array< TruthValue > *const &	knownQueryValues,
		const Array< int > *const &	allPredGndingsAreQueries,
		const bool &	markHardGndClauses,
		const bool &	trackParentClauseWts,
		const MLN *const &	mln,
		const Domain *const &	domain,
		const bool &	lazy
	)			[inline]

Constructor for a VariableState.

The hard clause weight is set. In lazy mode, the initial active atoms and clauses are retrieved and in eager mode, the MRF is built and the atoms and clauses are retrieved from it. In addition, all information arrays are filled with information.

Parameters:

	unknownQueries	Query predicates with unknown values used to build MRF in eager mode.
	knownQueries	Query predicates with known values used to build MRF in eager mode.
	knownQueryValues	Truth values of the known query predicates.
	allPredGndingsAreQueries	Array used to build MRF in eager mode.
	mln	mln and domain are used to build MRF in eager state and to retrieve active atoms in lazy state.
	domain	mln and domain are used to build MRF in eager state and to retrieve active atoms in lazy state.
	lazy	Flag stating whether lazy mode is used or not.

Definition at line 119 of file variablestate.h.

References addNewClauses(), HashArray< Type, HashFn, EqualFn >::append(), Array< Type >::clear(), Domain::computeNumNonEvidAtoms(), MRF::deleteGndPredsGndClauseSets(), getActiveClauses(), Domain::getDB(), MRF::getGndClauses(), MRF::getGndPreds(), getNumClauses(), Domain::getNumNonEvidenceAtoms(), initBlocksRandom(), MODE_MWS, Timer::printTime(), Database::setActiveStatus(), Database::setPerformingInference(), HashArray< Type, HashFn, EqualFn >::size(), Array< Type >::size(), and Timer::time().

  {
    stillActivating_ = true;
    breakHardClauses_ = false;
      // By default MaxWalkSAT mode
    inferenceMode_ = MODE_MWS;
    Timer timer;
    double startTime = timer.time();

    this->mln_ = (MLN*)mln;
    this->domain_ = (Domain*)domain;
    this->lazy_ = lazy;

      // Instantiate information
    baseNumAtoms_ = 0;
    activeAtoms_ = 0;
    numFalseClauses_ = 0;
    costOfFalseClauses_ = 0.0;
    lowCost_ = LDBL_MAX;
    lowBad_ = INT_MAX;

      // Clauses and preds are stored in gndClauses_ and gndPreds_
    gndClauses_ = new GroundClauseHashArray;
    gndPreds_ = new Array<GroundPredicate*>;

      // Set the hard clause weight
    setHardClauseWeight();

      // Lazy version: Produce state with initial active atoms and clauses
    if (lazy_)
    {
        // Set number of non-evidence atoms from domain
      domain_->computeNumNonEvidAtoms();
      numNonEvAtoms_ = domain_->getNumNonEvidenceAtoms();
        // Unknown preds are treated as false
      domain_->getDB()->setPerformingInference(true);
      clauseLimit_ = INT_MAX;
      noApprox_ = false;
      haveDeactivated_ = false;

        // Get initial set of active atoms (atoms in unsat. clauses)
        // Assumption is: all atoms are initially false except those in blocks

        // One atom in each block is set to true and activated
      initBlocksRandom();

      //bool ignoreActivePreds = false;
      bool ignoreActivePreds = true;
      cout << "Getting initial active atoms ... " << endl;
      getActiveClauses(newClauses_, ignoreActivePreds);
      cout << "done." << endl;
      int defaultCnt = newClauses_.size();
      long double defaultCost = 0;

      for (int i = 0; i < defaultCnt; i++)
      {
        if (newClauses_[i]->isHardClause())
          defaultCost += hardWt_;
        else
          defaultCost += abs(newClauses_[i]->getWt());
      }

        // Clear ground clauses in the ground preds
      for (int i = 0; i < gndPredHashArray_.size(); i++)
        gndPredHashArray_[i]->removeGndClauses();

        // Delete new clauses
      for (int i = 0; i < newClauses_.size(); i++)
        delete newClauses_[i];
      newClauses_.clear();

      baseNumAtoms_ = gndPredHashArray_.size();
      cout << "Number of Baseatoms = " << baseNumAtoms_ << endl;
      cout << "Default => Cost\t" << "******\t" << " Clause Cnt\t" << endl;
      cout << "           " << defaultCost << "\t" << "******\t" << defaultCnt
           << "\t" << endl << endl;

        // Set base atoms as active in DB
      for (int i = 0; i < baseNumAtoms_; i++)
      {
        domain_->getDB()->setActiveStatus(gndPredHashArray_[i], true);
        activeAtoms_++;     
      }

        // Get the initial set of active clauses
      ignoreActivePreds = false;
      cout << "Getting initial active clauses ... ";
      getActiveClauses(newClauses_, ignoreActivePreds);      
      cout << "done." << endl;
        } // End lazy version
      // Eager version: Use KBMC to produce the state
    else
    {
      unePreds_ = unknownQueries;
      knePreds_ = knownQueries;
      knePredValues_ = knownQueryValues;

        // MRF is built on known and unknown queries
      int size = 0;
      if (unknownQueries) size += unknownQueries->size();
      if (knownQueries) size += knownQueries->size();
      GroundPredicateHashArray* queries = new GroundPredicateHashArray(size);
      if (unknownQueries) queries->append(unknownQueries);
      if (knownQueries) queries->append(knownQueries);
      mrf_ = new MRF(queries, allPredGndingsAreQueries, domain_,
                     domain_->getDB(), mln_, markHardGndClauses,
                     trackParentClauseWts, -1);

        //delete to save space. Can be deleted because no more gndClauses are
        //appended to gndPreds beyond this point
      mrf_->deleteGndPredsGndClauseSets();
        //do not delete the intArrRep in gndPreds_;
      delete queries;

        // Put ground clauses in newClauses_
      newClauses_ = *(Array<GroundClause*>*)mrf_->getGndClauses();
        // Put ground preds in the hash array
      //const Array<GroundPredicate*>* gndPreds = mrf_->getGndPreds();
      const GroundPredicateHashArray* gndPreds = mrf_->getGndPreds();
      for (int i = 0; i < gndPreds->size(); i++)
        gndPredHashArray_.append((*gndPreds)[i]);
    
        // baseNumAtoms_ are all atoms in eager version
      baseNumAtoms_ = gndPredHashArray_.size();        
    } // End eager version
    
      // At this point, ground clauses are held in newClauses_
      // and ground predicates are held in gndPredHashArray_
      // for both versions
    
      // Add the clauses and preds and fill info arrays
    bool initial = true;
    addNewClauses(initial);
    
        cout << "[VS] ";
        Timer::printTime(cout,timer.time()-startTime);
        cout << endl;
        cout << ">>> DONE: Initial num. of clauses: " << getNumClauses() << endl;
  }

VariableState::~VariableState

(

)

[inline]

Destructor.

MRF is deleted in eager version.

Definition at line 270 of file variablestate.h.

References HashArray< Type, HashFn, EqualFn >::size().

  {
    if (lazy_)
    {
      if (gndClauses_)
        for (int i = 0; i < gndClauses_->size(); i++)
          delete (*gndClauses_)[i];

      for (int i = 0; i < gndPredHashArray_.size(); i++)
      {
        gndPredHashArray_[i]->removeGndClauses();
        delete gndPredHashArray_[i];
      }
    }
    else
    {
        // MRF from eager version is deleted
      if (mrf_)
      {
        delete mrf_;
        mrf_ = NULL;
      }
      //if (unePreds_) delete unePreds_;
      //if (knePreds_) delete knePreds_;
      //if (knePredValues_) delete knePredValues_;
    }
    //delete gndClauses_;
    //delete gndPreds_;
    //delete mln_;
  }

---

Member Function Documentation

void VariableState::addNewClauses

(

bool

initial

)

[inline]

New clauses are added to the state.

If not the initialization, then makecost and breakcost are updated for the new atoms.

Parameters:

initial

If true, this is the first time new clauses have been added.

Definition at line 309 of file variablestate.h.

References ADD_CLAUSE_INITIAL, and ADD_CLAUSE_REGULAR.

Referenced by activateAtom(), fixAtom(), getIndexOfRandomAtom(), initBlocksRandom(), reinit(), and VariableState().

  {
    if (initial) addNewClauses(ADD_CLAUSE_INITIAL, newClauses_);
    else addNewClauses(ADD_CLAUSE_REGULAR, newClauses_);
  }

void VariableState::initRandom

(

)

[inline]

Makes a random truth assigment to all (active) atoms.

Blocks are taken into account: exactly one atom in the block is set to true and the others are set to false.

Definition at line 362 of file variablestate.h.

References activateAtom(), getBlockIndex(), getNegOccurenceArray(), getPosOccurenceArray(), init(), initBlocksRandom(), isActive(), MODE_SAMPLESAT, setValueOfAtom(), Array< Type >::size(), and unitPropagation().

Referenced by MaxWalkSat::init().

  {
      // If performing SampleSat, do a run of UP
        if (inferenceMode_ == MODE_SAMPLESAT)
        {
      unitPropagation();
    }

      // Set one in each block to true randomly
    initBlocksRandom();

    for (int i = 1; i <= gndPreds_->size(); i++)
    {
      if (fixedAtom_[i] != 0)
      {
        continue;
      }

        // Blocks are initialized above
      if (getBlockIndex(i - 1) >= 0)
      {
        if (vsdebug) cout << "Atom " << i << " in block" << endl;
        continue;
      }
        // Not fixed and not in block
      else
      {
        if (vsdebug) cout << "Atom " << i << " not in block" << endl;
                        
          // only need to activate inactive true atoms
        if (!lazy_ || isActive(i))
        {
          bool isTrue = random() % 2;
          bool activate = false;
          setValueOfAtom(i, isTrue, activate, -1);
        }
        else if (inferenceMode_ == MODE_SAMPLESAT)
        {
          bool isInPrevUnsat = false;
          Array<int> oca = getPosOccurenceArray(i);
          for (int k = 0; k < oca.size(); k++)
            if (!prevSatisfiedClause_[oca[k]])
            {
              isInPrevUnsat = true;
              break;
            }
            
          if (!isInPrevUnsat)
          {
            oca = getNegOccurenceArray(i);
            for (int k = 0; k < oca.size(); k++)
              if (!prevSatisfiedClause_[oca[k]])
              {
                isInPrevUnsat = true;
                break;
              }
          }
          if (isInPrevUnsat)
          {
            bool isTrue = random() % 2;
            if (isTrue)
            {
              if (activateAtom(i, false, false))
                setValueOfAtom(i, true, false, -1);
            }
          }
        }
      }
    }

    init();     
  }

void VariableState::initMakeBreakCostWatch

(

const int &

startClause

)

[inline]

Initialize makeCost and breakCost and watch arrays based on the current variable assignment.

Parameters:

startClause

All clauses with index of this or greater are initialized.

Definition at line 553 of file variablestate.h.

References getClauseSize(), getNumClauses(), and isTrueLiteral().

  {
    int theTrueLit = -1;
      // Initialize breakCost and makeCost in the following:
    for (int i = startClause; i < getNumClauses(); i++)
    {
        // Don't look at dead or satisfied clauses
      if (deadClause_[i] || isSatisfied_[i]) continue;

      int trueLit1 = 0;
      int trueLit2 = 0;
      long double cost = clauseCost_[i];
      numTrueLits_[i] = 0;
      for (int j = 0; j < getClauseSize(i); j++)
      {
        if (isTrueLiteral(clause_[i][j]))
        { // ij is true lit
          numTrueLits_[i]++;
          theTrueLit = abs(clause_[i][j]);
          if (!trueLit1) trueLit1 = theTrueLit;
          else if (trueLit1 && !trueLit2) trueLit2 = theTrueLit;
        }
      }

        // Unsatisfied positive-weighted clauses or
        // Satisfied negative-weighted clauses
      if ((numTrueLits_[i] == 0 && cost >= 0) ||
          (numTrueLits_[i] > 0 && cost < 0))
      {
        whereFalse_[i] = numFalseClauses_;
        falseClause_[numFalseClauses_] = i;
        numFalseClauses_++;
        costOfFalseClauses_ += abs(cost);
        if (highestCost_ == abs(cost)) {eqHighest_ = true; numHighest_++;}

          // Unsat. pos. clause: increase makeCost_ of all atoms
        if (numTrueLits_[i] == 0)
          for (int j = 0; j < getClauseSize(i); j++)
          {
            makeCost_[abs(clause_[i][j])] += cost;
          }

          // Sat. neg. clause: increase makeCost_ if one true literal
        if (numTrueLits_[i] == 1)
        {
            // Subtract neg. cost
          makeCost_[theTrueLit] -= cost;
          watch1_[i] = theTrueLit;
        }
        else if (numTrueLits_[i] > 1)
        {
          watch1_[i] = trueLit1;
          watch2_[i] = trueLit2;
        }
      }
        // Pos. clauses satisfied by one true literal
      else if (numTrueLits_[i] == 1 && cost >= 0)
      {
        breakCost_[theTrueLit] += cost;
        watch1_[i] = theTrueLit;
      }
        // Pos. clauses satisfied by 2 or more true literals
      else if (cost >= 0)
      { /*if (numtruelit[i] == 2)*/
        watch1_[i] = trueLit1;
        watch2_[i] = trueLit2;
      }
        // Unsat. neg. clauses: increase breakCost of all atoms
      else if (numTrueLits_[i] == 0 && cost < 0)
      {
        for (int j = 0; j < getClauseSize(i); j++)
          breakCost_[abs(clause_[i][j])] -= cost;
      }
    } // for all clauses
  }

int VariableState::getIndexOfRandomAtom

(

)

[inline]

Returns the absolute index of a random atom.

If in lazy mode, a non-evidence atom which is not in memory could be picked. In this case, the atom is added to the set in memory and its index is returned.

Definition at line 646 of file variablestate.h.

References addNewClauses(), HashArray< Type, HashFn, EqualFn >::append(), HashArray< Type, HashFn, EqualFn >::find(), Domain::getNonEvidenceAtom(), getNumAtoms(), GroundPredicate::print(), and HashArray< Type, HashFn, EqualFn >::size().

Referenced by MaxWalkSat::pickSS().

  {
      // Lazy: pick a random non-evidence atom from domain
    if (lazy_)
    {
      Predicate* pred = domain_->getNonEvidenceAtom(random() % numNonEvAtoms_);
      GroundPredicate* gndPred = new GroundPredicate(pred);
      delete pred;

      int idx = gndPredHashArray_.find(gndPred);
        // Already present, then return index
      if (idx >= 0)
      {
        delete gndPred;
        return idx + 1;
      }
        // Not present, add it to the state
      else
      {
        if (vsdebug)
        {
          cout << "Adding randomly ";
          gndPred->print(cout, domain_);
          cout << " to the state" << endl; 
        }
        gndPredHashArray_.append(gndPred);
        bool initial = false;
        addNewClauses(initial);
          // index to return is the last element
        return gndPredHashArray_.size();
      }
    }
      // Eager: pick an atom from the state
    else
    {
      int numAtoms = getNumAtoms();
      if (numAtoms == 0) return NOVALUE;
      return random()%numAtoms + 1;
    }
  }

int VariableState::getIndexOfAtomInRandomFalseClause

(

)

[inline]

Returns the absolute index of a random atom in a random unsatisfied pos.

clause or the absolute index of a random true literal in a random satisfied clause.

Definition at line 692 of file variablestate.h.

References getClauseSize(), and getRandomTrueLitInClause().

Referenced by MaxWalkSat::pickRandom().

  {
    if (numFalseClauses_ == 0) return NOVALUE;
    int clauseIdx = falseClause_[random()%numFalseClauses_];

      // Pos. clause: return index of random atom
    if (clauseCost_[clauseIdx] >= 0)
    {
        // Q: Can all atoms in a clause be fixed?
      while (true)
      {
        int i = random()%getClauseSize(clauseIdx);
        if (!fixedAtom_[abs(clause_[clauseIdx][i])])
          return abs(clause_[clauseIdx][i]);
      }
    }
      // Neg. clause: find random true lit
    else
      return getRandomTrueLitInClause(clauseIdx);
  }

int VariableState::getRandomFalseClauseIndex

(

)

[inline]

Returns the index of a random unsatisfied pos.

clause or a random satisfied neg. clause.

Definition at line 717 of file variablestate.h.

Referenced by MaxWalkSat::pickBest(), and MaxWalkSat::pickTabu().

  {
    if (numFalseClauses_ == 0) return NOVALUE;
    return falseClause_[random()%numFalseClauses_];
  }

bool VariableState::getValueOfAtom

(

const int &

atomIdx

)

[inline]

Returns the truth value of an atom.

Index of atom whose truth value is returned.

Returns:

Truth value of atom.

Definition at line 747 of file variablestate.h.

Referenced by MaxWalkSat::calculateImprovement(), flipAtom(), MaxWalkSat::pickRandom(), updateMakeBreakCostAfterFlip(), and updateSatisfiedClauses().

  {
    return atom_[atomIdx];
  }

bool VariableState::getValueOfLowAtom

(

const int &

atomIdx

)

[inline]

Returns the truth value of an atom in the best state.

Index of atom whose truth value is returned.

Returns:

Truth value of atom.

Definition at line 758 of file variablestate.h.

Referenced by UnitPropagation::getChangedPreds(), SAT::getChangedPreds(), UnitPropagation::getProbability(), SAT::getProbability(), SAT::getProbabilityH(), UnitPropagation::printProbabilities(), SAT::printProbabilities(), UnitPropagation::printTruePreds(), SAT::printTruePreds(), SAT::printTruePredsH(), and MCMC::saveLowStateToChain().

  {
    return lowAtom_[atomIdx];
  }

void VariableState::setValueOfAtom	(	const int &	atomIdx,
		const bool &	value,
		const bool &	activate,
		const int &	blockIdx
	)			[inline]

Sets the truth value of an atom.

The truth value is propagated to the database.

Parameters:

	atomIdx	Index of atom whose value is to be set.
	value	Truth value being set.
	activate	If true, atom is activated if not active.
	blockIdx	Indicates which block the atom being flipped is in. If not in one, this is -1.

Definition at line 773 of file variablestate.h.

References activateAtom(), Domain::getDB(), isActive(), Predicate::printWithStrVar(), Domain::setTruePredInBlock(), and Database::setValue().

Referenced by activateAtom(), fixAtom(), flipAtomValue(), initBlocksRandom(), initRandom(), and setOthersInBlockToFalse().

  {
      // If atom already has this value, then do nothing
    if (atom_[atomIdx] == value) return;
    if (vsdebug) cout << "Setting value of atom " << atomIdx 
                      << " to " << value << endl;
      // Propagate assignment to DB
    GroundPredicate* p = gndPredHashArray_[atomIdx - 1];
    if (value)
      domain_->getDB()->setValue(p, TRUE);
    else
      domain_->getDB()->setValue(p, FALSE);

      // If not active, then activate it
    if (activate && lazy_ && !isActive(atomIdx))
    {
      bool ignoreActivePreds = false;
      bool groundOnly = false;
      activateAtom(atomIdx, ignoreActivePreds, groundOnly);
    }
    atom_[atomIdx] = value;

      // If in block and setting to true, tell the domain
    if (blockIdx > -1 && value)
    {
      Predicate* pred = p->createEquivalentPredicate(domain_);
      domain_->setTruePredInBlock(blockIdx, pred);
      if (vsdebug)
      {
        cout << "Set true pred in block " << blockIdx << " to ";
        pred->printWithStrVar(cout, domain_);
        cout << endl;
      }
    }
  }

void VariableState::flipAtom	(	const int &	toFlip,
		const int &	blockIdx
	)			[inline]

Flip the truth value of an atom and update info arrays.

Parameters:

	toFlip	Index of atom to be flipped.
	blockIdx	Index of block in which atom is, or -1 if not in one.

Definition at line 834 of file variablestate.h.

References addBreakCost(), addBreakCostToAtomsInClause(), addFalseClause(), addMakeCost(), addMakeCostToAtomsInClause(), decrementNumTrueLits(), flipAtomValue(), getClauseCost(), getOccurenceArray(), getTrueLiteralOtherThan(), getValueOfAtom(), getWatch1(), getWatch2(), incrementNumTrueLits(), removeFalseClause(), setWatch1(), setWatch2(), and Array< Type >::size().

Referenced by MaxWalkSat::flipAtom().

  {
    bool toFlipValue = getValueOfAtom(toFlip);
    register int clauseIdx;
    int sign;
    int oppSign;
    int litIdx;
    if (toFlipValue)
      sign = 1;
    else
      sign = 0;
    oppSign = sign ^ 1;

    flipAtomValue(toFlip, blockIdx);
      // Update all clauses in which the atom occurs as a true literal
    litIdx = 2*toFlip - sign;
    Array<int>& posOccArray = getOccurenceArray(litIdx);
    for (int i = 0; i < posOccArray.size(); i++)
    {
      clauseIdx = posOccArray[i];
        // Don't look at dead or satisfied clauses
      if (deadClause_[clauseIdx] || isSatisfied_[clauseIdx]) continue;

          // The true lit became a false lit
          int numTrueLits = decrementNumTrueLits(clauseIdx);
      long double cost = getClauseCost(clauseIdx);
      int watch1 = getWatch1(clauseIdx);
      int watch2 = getWatch2(clauseIdx);
        // 1. If last true lit was flipped, then we have to update
        // the makecost / breakcost info accordingly        
      if (numTrueLits == 0)
      {
          // Pos. clause
        if (cost >= 0)
        {
            // Add this clause as false in the state
          addFalseClause(clauseIdx);
            // Decrease toFlip's breakcost (add neg. cost)
          addBreakCost(toFlip, -cost);
            // Increase makecost of all vars in clause (add pos. cost)
          addMakeCostToAtomsInClause(clauseIdx, cost);
        }
          // Neg. clause
        else
        {
          assert(cost < 0);
            // Remove this clause as false in the state
          removeFalseClause(clauseIdx);
            // Increase breakcost of all vars in clause (add pos. cost)
          addBreakCostToAtomsInClause(clauseIdx, -cost);        
            // Decrease toFlip's makecost (add neg. cost)
          addMakeCost(toFlip, cost);
        }
      }
        // 2. If there is now one true lit left, then move watch2
        // up to watch1 and increase the breakcost / makecost of watch1
      else if (numTrueLits == 1)
      {
        if (watch1 == toFlip)
        {
          assert(watch1 != watch2);
          setWatch1(clauseIdx, watch2);
          watch1 = getWatch1(clauseIdx);
        }

          // Pos. clause: Increase toFlip's breakcost (add pos. cost)
        if (cost >= 0)
        {
          addBreakCost(watch1, cost);
        }
          // Neg. clause: Increase toFlip's makecost (add pos. cost)
        else
        {
          assert(cost < 0);
          addMakeCost(watch1, -cost);
        }
      }
        // 3. If there are 2 or more true lits left, then we have to
        // find a new true lit to watch if one was flipped
      else
      { /* numtruelit[clauseIdx] >= 2 */
          // If watch1[clauseIdx] has been flipped
        if (watch1 == toFlip)
        {
            // find a different true literal to watch
          int diffTrueLit = getTrueLiteralOtherThan(clauseIdx, watch1, watch2);
          setWatch1(clauseIdx, diffTrueLit);
        }
          // If watch2[clauseIdx] has been flipped
        else if (watch2 == toFlip)
        {
            // find a different true literal to watch
          int diffTrueLit = getTrueLiteralOtherThan(clauseIdx, watch1, watch2);
          setWatch2(clauseIdx, diffTrueLit);
        }
      }
    }
        
      // Update all clauses in which the atom occurs as a false literal
    litIdx = 2*toFlip - oppSign;
    Array<int>& negOccArray = getOccurenceArray(litIdx);
    for (int i = 0; i < negOccArray.size(); i++)
    {
      clauseIdx = negOccArray[i];
        // Don't look at dead or satisfied clauses
      if (deadClause_[clauseIdx] || isSatisfied_[clauseIdx]) continue;

        // The false lit became a true lit
      int numTrueLits = incrementNumTrueLits(clauseIdx);
      long double cost = getClauseCost(clauseIdx);
      int watch1 = getWatch1(clauseIdx);

        // 1. If this is the only true lit, then we have to update
        // the makecost / breakcost info accordingly        
      if (numTrueLits == 1)
      {
          // Pos. clause
        if (cost >= 0)
        {
            // Remove this clause as false in the state
          removeFalseClause(clauseIdx);
            // Increase toFlip's breakcost (add pos. cost)
          addBreakCost(toFlip, cost);        
            // Decrease makecost of all vars in clause (add neg. cost)
          addMakeCostToAtomsInClause(clauseIdx, -cost);
        }
          // Neg. clause
        else
        {
          assert(cost < 0);
            // Add this clause as false in the state
          addFalseClause(clauseIdx);
            // Decrease breakcost of all vars in clause (add neg. cost)
          addBreakCostToAtomsInClause(clauseIdx, cost);
            // Increase toFlip's makecost (add pos. cost)
          addMakeCost(toFlip, -cost);
        }
          // Watch this atom
        setWatch1(clauseIdx, toFlip);
      }
        // 2. If there are now exactly 2 true lits, then watch second atom
        // and update breakcost
      else
      if (numTrueLits == 2)
      {
        if (cost >= 0)
        {
            // Pos. clause
            // Decrease breakcost of first atom being watched (add neg. cost)
          addBreakCost(watch1, -cost);
        }
        else
        {
            // Neg. clause
          assert(cost < 0);
            // Decrease makecost of first atom being watched (add neg. cost)
          addMakeCost(watch1, cost);
        }
        
          // Watch second atom
        setWatch2(clauseIdx, toFlip);
      }
    }
  }

void VariableState::flipAtomValue	(	const int &	atomIdx,
		const int &	blockIdx
	)			[inline]

Flips the truth value of an atom.

If in lazy mode, the truth value is propagated to the database.

Parameters:

	atomIdx	Index of atom to be flipped.
	blockIdx	Index of block in which the atom is in, or -1 if not in one.

Definition at line 1006 of file variablestate.h.

References setValueOfAtom().

Referenced by flipAtom(), and MaxWalkSat::reconstructLowState().

  {
    bool opposite = !atom_[atomIdx];
    bool activate = true;
    setValueOfAtom(atomIdx, opposite, activate, blockIdx);
  }

long double VariableState::getImprovementByFlipping

(

const int &

atomIdx

)

[inline]

Calculates the improvement achieved by flipping an atom.

This is the cost of clauses which flipping the atom makes good minus the cost of clauses which flipping the atom makes bad. In lazy mode, if the atom is not active, then the atom is activated and the makecost and breakcost are updated.

Parameters:

atomIdx

Index of atom to flip.

Returns:

Improvement achieved by flipping the atom.

Definition at line 1024 of file variablestate.h.

Referenced by MaxWalkSat::calculateImprovement(), and MaxWalkSat::pickRandom().

  {
    if (!breakHardClauses_ && breakCost_[atomIdx] >= hardWt_)
      return -LDBL_MAX;
    long double improvement = makeCost_[atomIdx] - breakCost_[atomIdx];
    return improvement;
  }

void VariableState::setActive

(

const int &

atomIdx

)

[inline]

Set the active status of an atom to true in the database if in lazy mode.

Index of the atom to be set to active.

Definition at line 1037 of file variablestate.h.

References Domain::getDB(), and Database::setActiveStatus().

Referenced by MaxWalkSat::pickSS().

  {
    if (lazy_)
    {
      Predicate* p =
        gndPredHashArray_[atomIdx - 1]->createEquivalentPredicate(domain_);
      domain_->getDB()->setActiveStatus(p, true);
      activeAtoms_++;
      delete p;
    }
  }

bool VariableState::activateAtom	(	const int &	atomIdx,
		const bool &	ignoreActivePreds,
		const bool &	groundOnly
	)			[inline]

If in lazy mode, an atom is activated and all clauses activated by this atom are added to the state.

If in eager mode, nothing happens.

Parameters:

	atomIdx	Index of atom to be activated.
	ignoreActivePreds	If true, active atoms are ignored when getting active clauses (just gets unsatisfied clauses).
	groundOnly	If true, atom itself is not activated, just its active clauses are retrieved.

Definition at line 1059 of file variablestate.h.

References ADD_CLAUSE_DEAD, ADD_CLAUSE_REGULAR, ADD_CLAUSE_SAT, addNewClauses(), Array< Type >::append(), Array< Type >::clear(), fixAtom(), getActiveClauses(), Database::getActiveStatus(), Domain::getDB(), isActive(), Database::setActiveStatus(), setValueOfAtom(), Array< Type >::size(), and updateMakeBreakCostAfterFlip().

Referenced by initRandom(), MaxWalkSat::pickBest(), MaxWalkSat::pickRandom(), MaxWalkSat::pickSS(), MaxWalkSat::pickTabu(), and setValueOfAtom().

  {
    /***
     * . [IF MCSAT] 
     * - check neg-wt clauses
     * . if alive, fix
     * . else mark dead
     * - if not fixed, add all pos-wt, killClauses
     * - else add dead
     * . [ELSE] add all
     ***/
    if (lazy_ && !isActive(atomIdx))
    {
      if (vsdebug)
      {
        cout << "\tActivating ";
        gndPredHashArray_[atomIdx-1]->print(cout,domain_);
        cout << " " <<
        domain_->getDB()->getActiveStatus(gndPredHashArray_[atomIdx-1]) << endl;
      }

        // Set atom to true first, see if avoid getting clauses already active
      bool needToFlipBack = false;
      if (!atom_[atomIdx])
      {
        bool activate = false;
        setValueOfAtom(atomIdx, true, activate, -1);
        updateMakeBreakCostAfterFlip(atomIdx);
        needToFlipBack = true;
      } 

        // gather active clauses
      Predicate* p =
        gndPredHashArray_[atomIdx - 1]->createEquivalentPredicate(domain_);

      bool isFixed = false;
      Array<GroundClause*> unsatClauses;
      Array<GroundClause*> deadClauses;
      Array<GroundClause*> toAddClauses;

        // Using newClauses_ causes problem since it's shared across the board
      getActiveClauses(p, unsatClauses, true, ignoreActivePreds);

        // if MC-SAT: check neg-wt or unit clauses and see if can fix             
      if (useThreshold_)
      {
          // first append deadClauses, then pos-wt
        for (int ni = 0; ni < unsatClauses.size(); ni++)
        {
          GroundClause* c = unsatClauses[ni];
          if (c->getWt() < 0)
          {  // Neg. weighted clause
              // since newClauses_ excludes clauses in memory, c must be
              // goodInPrevious
            double threshold = RAND_MAX*(1 - exp(c->getWt()));
            if (random() <= threshold)
            {
                // fix
              isFixed = true;

                // append dead and fixed clauses first, so fixed atoms do not
                // activate them unnecessarily
              if (deadClauses.size() > 0)
                addNewClauses(ADD_CLAUSE_DEAD, deadClauses);

              Array<GroundClause*> fixedClauses;
              fixedClauses.append(c);
              addNewClauses(ADD_CLAUSE_SAT, fixedClauses);

                // --- fix the atoms
              for (int pi = 0; pi < c->getNumGroundPredicates(); pi++)
              {
                int lit = c->getGroundPredicateIndex(pi);
                fixAtom(abs(lit), (lit < 0));
              }

                // - can quit now
              break;
            }
            else
            {
                // dead
              deadClauses.append(c);
            }
          }
          else if (c->getNumGroundPredicates() == 1)
          {  // Unit clause
            double threshold = RAND_MAX*(1 - exp(-c->getWt()));
            if (random() <= threshold)
            {
                // fix
              isFixed = true;

                // append dead and fixed clauses first, so fixed atoms do not
                // activate them unnecessarily
              if (deadClauses.size() > 0)
                addNewClauses(ADD_CLAUSE_DEAD, deadClauses);

              Array<GroundClause*> fixedClauses;
              fixedClauses.append(c);
              addNewClauses(ADD_CLAUSE_SAT, fixedClauses);

                // --- fix the atoms
              int lit = c->getGroundPredicateIndex(0);
              fixAtom(abs(lit), (lit > 0)); // this is positive wt

                // - can quit now
              break;
            }
            else
            {
                // dead
              deadClauses.append(c);
            }
          }
          else toAddClauses.append(c);
        }
      }

        // Add the clauses and preds and fill info arrays
      if (!isFixed)
      {
        if (deadClauses.size() > 0)
          addNewClauses(ADD_CLAUSE_DEAD, deadClauses);

        if (useThreshold_)
          addNewClauses(ADD_CLAUSE_REGULAR, toAddClauses);
        else // lazy-sat
          addNewClauses(ADD_CLAUSE_REGULAR, unsatClauses);

          // To avoid append already-active: if not fixed, might need to
          // flip back
        if (needToFlipBack)
        {
          bool activate = false;
          setValueOfAtom(atomIdx, false, activate, -1);
          updateMakeBreakCostAfterFlip(atomIdx);
        }

        if (!groundOnly)
        {
            // Set active status in db
          domain_->getDB()->setActiveStatus(p, true);
          activeAtoms_++;
        }
      }

      delete p;
      unsatClauses.clear();
      deadClauses.clear();
      toAddClauses.clear();

      return !isFixed; // if !isFixed, then activated
    }
    return true;
  }

void VariableState::addNewClauses	(	int	addType,
		Array< GroundClause * > &	clauses
	)			[inline]

Adds new clauses to the state.

Parameters:

	addType	How the clauses are being added (see ADD_CLAUSE_*)
	clauses	Array of ground clauses to be added to the state.

Definition at line 1367 of file variablestate.h.

References ADD_CLAUSE_DEAD, ADD_CLAUSE_REGULAR, ADD_CLAUSE_SAT, Array< Type >::append(), HashArray< Type, HashFn, EqualFn >::append(), Array< Type >::clear(), Domain::getDB(), getNumAtoms(), getNumClauses(), Database::getValue(), Array< Type >::growToSize(), initMakeBreakCostWatch(), killClauses(), MODE_HARD, MODE_SAMPLESAT, HashArray< Type, HashFn, EqualFn >::size(), and Array< Type >::size().

  {
    if (vsdebug)
      cout << "Adding " << clauses.size() << " new clauses.." << endl;

      // Must be in mc-sat to add dead or sat
    if (!useThreshold_ &&
        (addType == ADD_CLAUSE_DEAD || addType == ADD_CLAUSE_SAT))
    {
      cout << ">>> [ERR] add_dead/sat but useThreshold_ is false" << endl;
      exit(0);
    }

      // Store the old number of clauses and atoms
    int oldNumClauses = getNumClauses();
    int oldNumAtoms = getNumAtoms();

      //gndClauses_->append(clauses);
    for (int i = 0; i < clauses.size(); i++)
    {
      gndClauses_->append(clauses[i]);
      clauses[i]->appendToGndPreds(&gndPredHashArray_);
    }

    gndPreds_->growToSize(gndPredHashArray_.size());

    int numAtoms = getNumAtoms();
    int numClauses = getNumClauses();
      // If no new atoms or clauses have been added, then do nothing
    if (numAtoms == oldNumAtoms && numClauses == oldNumClauses) return;

    if (vsdebug) cout << "Clauses: " << numClauses << endl;
      // atomIdx starts at 1
    atom_.growToSize(numAtoms + 1, false);

    makeCost_.growToSize(numAtoms + 1, 0.0);
    breakCost_.growToSize(numAtoms + 1, 0.0);
    lowAtom_.growToSize(numAtoms + 1, false);
    fixedAtom_.growToSize(numAtoms + 1, 0);

          // Copy ground preds to gndPreds_ and set values in atom and lowAtom
    for (int i = oldNumAtoms; i < gndPredHashArray_.size(); i++)
    {
      (*gndPreds_)[i] = gndPredHashArray_[i];

      if (vsdebug)
      {
        cout << "New pred " << i + 1 << ": ";
        (*gndPreds_)[i]->print(cout, domain_);
        cout << endl;
      }

      lowAtom_[i + 1] = atom_[i + 1] = 
        (domain_->getDB()->getValue((*gndPreds_)[i]) == TRUE) ? true : false;
    }
    clauses.clear();

    clause_.growToSize(numClauses);
    clauseCost_.growToSize(numClauses);
    falseClause_.growToSize(numClauses);
    whereFalse_.growToSize(numClauses);
    numTrueLits_.growToSize(numClauses);
    watch1_.growToSize(numClauses);
    watch2_.growToSize(numClauses);
    isSatisfied_.growToSize(numClauses, false);
    deadClause_.growToSize(numClauses, false);
    threshold_.growToSize(numClauses, false);
  
    occurence_.growToSize(2*numAtoms + 1);

    for (int i = oldNumClauses; i < numClauses; i++)
    {
      GroundClause* gndClause = (*gndClauses_)[i];

      if (vsdebug)
      {
        cout << "New clause " << i << ": ";
        gndClause->print(cout, domain_, &gndPredHashArray_);
        cout << endl;
      }

        // Set thresholds for clause selection
      if (gndClause->isHardClause()) threshold_[i] = RAND_MAX;
      else
      {
        double w = gndClause->getWt();
        threshold_[i] = RAND_MAX*(1 - exp(-abs(w)));
        if (vsdebug)
        {
          cout << "Weight: " << w << endl;            
        }
      }
      if (vsdebug)
        cout << "Threshold: " << threshold_[i] << endl;            

      int numGndPreds = gndClause->getNumGroundPredicates();
      clause_[i].growToSize(numGndPreds);
      for (int j = 0; j < numGndPreds; j++) 
      {
        int lit = gndClause->getGroundPredicateIndex(j);
        clause_[i][j] = lit;
        int litIdx = 2*abs(lit) - (lit > 0);
        occurence_[litIdx].append(i);
      }

        // Hard clause weight has been previously determined
      if (inferenceMode_==MODE_SAMPLESAT)
      {
        if (gndClause->getWt()>0) clauseCost_[i] = 1;
        else clauseCost_[i] = -1;
      }
      else if (gndClause->isHardClause())
        clauseCost_[i] = hardWt_;
      else
        clauseCost_[i] = gndClause->getWt();

        // filter hard clauses
      if (inferenceMode_ == MODE_HARD && !gndClause->isHardClause())
      {
          // mark dead
        deadClause_[i] = true;
      }
    }

    if (addType == ADD_CLAUSE_DEAD)
    {
        // set to dead: no need for initMakeBreakCost, won't impact anyone
      for (int i = oldNumClauses; i < numClauses; i++)
      {
        deadClause_[i] = true;
      }
    }
    else if (addType == ADD_CLAUSE_SAT)
    {
        // set to dead: no need for initMakeBreakCost, won't impact anyone
      for (int i = oldNumClauses; i < numClauses; i++)
      {
        isSatisfied_[i]=true;
      }
    }
    else if (addType == ADD_CLAUSE_REGULAR)
    {
      if (useThreshold_)
        killClauses(oldNumClauses);
      else
        initMakeBreakCostWatch(oldNumClauses);
    }

    if (vsdebug) 
      cout << "Done adding new clauses.." << endl;
  }

void VariableState::updateSatisfiedClauses

(

const int &

toFix

)

[inline]

Updates isSatisfiedClause after an atom is fixed.

ASSUME: fixed val already applied, and updateMakeBreakCost called

Parameters:

toFix

Index of atom fixed

Definition at line 1525 of file variablestate.h.

References getClauseCost(), getOccurenceArray(), getValueOfAtom(), and Array< Type >::size().

Referenced by fixAtom().

  {
      // Already flipped
    bool toFlipValue = getValueOfAtom(toFix);
      
    register int clauseIdx;
    int sign;
    int litIdx;
    if (toFlipValue)
      sign = 1;
    else
      sign = 0;

      // Set isSatisfied: all clauses in which the atom occurs as a true literal
    litIdx = 2*toFix - sign;
    Array<int>& posOccArray = getOccurenceArray(litIdx);
    for (int i = 0; i < posOccArray.size(); i++)
    {
      clauseIdx = posOccArray[i];
        // Don't look at dead clauses
        // ignore already sat
      if (deadClause_[clauseIdx] || isSatisfied_[clauseIdx]) continue;

      if (getClauseCost(clauseIdx) < 0) 
      {
        cout << "ERR: in MC-SAT, active neg-wt clause (" << clauseIdx
             << ") is sat by fixed "<<endl;
        exit(0);
      }
      isSatisfied_[clauseIdx] = true;  
    }
  }

void VariableState::updateMakeBreakCostAfterFlip

(

const int &

toFlip

)

[inline]

Updates cost after flip.

Assume: already activated and flipped. Called by flipAtom and fixAtom (if fixed to the opposite val)

Definition at line 1563 of file variablestate.h.

References addBreakCost(), addBreakCostToAtomsInClause(), addFalseClause(), addMakeCost(), addMakeCostToAtomsInClause(), decrementNumTrueLits(), getClauseCost(), getOccurenceArray(), getTrueLiteralOtherThan(), getValueOfAtom(), getWatch1(), getWatch2(), incrementNumTrueLits(), removeFalseClause(), setWatch1(), setWatch2(), and Array< Type >::size().

Referenced by activateAtom(), and fixAtom().

  {       
      // Already flipped
    bool toFlipValue = !getValueOfAtom(toFlip);

    register int clauseIdx;
    int sign;
    int oppSign;
    int litIdx;
    if (toFlipValue)
      sign = 1;
    else
      sign = 0;
    oppSign = sign ^ 1;

      // Update all clauses in which the atom occurs as a true literal
    litIdx = 2*toFlip - sign;
    Array<int>& posOccArray = getOccurenceArray(litIdx);

    for (int i = 0; i < posOccArray.size(); i++)
    {
      clauseIdx = posOccArray[i];
        // Don't look at dead clauses and sat clauses
      if (deadClause_[clauseIdx] || isSatisfied_[clauseIdx]) continue;

        // The true lit became a false lit
      int numTrueLits = decrementNumTrueLits(clauseIdx);
      long double cost = getClauseCost(clauseIdx);
      int watch1 = getWatch1(clauseIdx);
      int watch2 = getWatch2(clauseIdx);

        // 1. If last true lit was flipped, then we have to update
        // the makecost / breakcost info accordingly        
      if (numTrueLits == 0)
      {
          // Pos. clause
        if (cost >= 0)
        {
            // Add this clause as false in the state
          addFalseClause(clauseIdx);
            // Decrease toFlip's breakcost (add neg. cost)
          addBreakCost(toFlip, -cost);
            // Increase makecost of all vars in clause (add pos. cost)
          addMakeCostToAtomsInClause(clauseIdx, cost);
        }
          // Neg. clause
        else
        {
          assert(cost < 0);
            // Remove this clause as false in the state
          removeFalseClause(clauseIdx);
            // Increase breakcost of all vars in clause (add pos. cost)
          addBreakCostToAtomsInClause(clauseIdx, -cost);        
            // Decrease toFlip's makecost (add neg. cost)
          addMakeCost(toFlip, cost);
        }
      }
        // 2. If there is now one true lit left, then move watch2
        // up to watch1 and increase the breakcost / makecost of watch1
      else if (numTrueLits == 1)
      {
        if (watch1 == toFlip)
        {
          assert(watch1 != watch2);
          setWatch1(clauseIdx, watch2);
          watch1 = getWatch1(clauseIdx);
        }
          // Pos. clause: Increase toFlip's breakcost (add pos. cost)
        if (cost >= 0)
        {
          addBreakCost(watch1, cost);
        }
            // Neg. clause: Increase toFlip's makecost (add pos. cost)
        else
        {
          assert(cost < 0);
          addMakeCost(watch1, -cost);
        }
      }
        // 3. If there are 2 or more true lits left, then we have to
        // find a new true lit to watch if one was flipped
      else
      {
          /* numtruelit[clauseIdx] >= 2 */
          // If watch1[clauseIdx] has been flipped
        if (watch1 == toFlip)
        {
            // find a different true literal to watch
          int diffTrueLit = getTrueLiteralOtherThan(clauseIdx, watch1, watch2);
          setWatch1(clauseIdx, diffTrueLit);
        }
          // If watch2[clauseIdx] has been flipped
        else if (watch2 == toFlip)
        {
            // find a different true literal to watch
          int diffTrueLit = getTrueLiteralOtherThan(clauseIdx, watch1, watch2);
          setWatch2(clauseIdx, diffTrueLit);
        }
      }
    }

      // Update all clauses in which the atom occurs as a false literal
    litIdx = 2*toFlip - oppSign;
    Array<int>& negOccArray = getOccurenceArray(litIdx);
    for (int i = 0; i < negOccArray.size(); i++)
    {
      clauseIdx = negOccArray[i];
        // Don't look at dead clauses or satisfied clauses
      if (deadClause_[clauseIdx] || isSatisfied_[clauseIdx]) continue;

        // The false lit became a true lit
      int numTrueLits = incrementNumTrueLits(clauseIdx);
      long double cost = getClauseCost(clauseIdx);
      int watch1 = getWatch1(clauseIdx);

        // 1. If this is the only true lit, then we have to update
        // the makecost / breakcost info accordingly        
      if (numTrueLits == 1)
      {
          // Pos. clause
        if (cost >= 0)
        {
            // Remove this clause as false in the state
          removeFalseClause(clauseIdx);
            // Increase toFlip's breakcost (add pos. cost)
          addBreakCost(toFlip, cost);        
            // Decrease makecost of all vars in clause (add neg. cost)
          addMakeCostToAtomsInClause(clauseIdx, -cost);
        }
          // Neg. clause
        else
        {
          assert(cost < 0);
            // Add this clause as false in the state
          addFalseClause(clauseIdx);
            // Decrease breakcost of all vars in clause (add neg. cost)
          addBreakCostToAtomsInClause(clauseIdx, cost);
            // Increase toFlip's makecost (add pos. cost)
          addMakeCost(toFlip, -cost);
        }
          // Watch this atom
        setWatch1(clauseIdx, toFlip);
      }
        // 2. If there are now exactly 2 true lits, then watch second atom
        // and update breakcost
      else if (numTrueLits == 2)
      {
        if (cost >= 0)
        {
            // Pos. clause
            // Decrease breakcost of first atom being watched (add neg. cost)
          addBreakCost(watch1, -cost);
        }
        else
        {
            // Neg. clause
          assert(cost < 0);
            // Decrease makecost of first atom being watched (add neg. cost)
          addMakeCost(watch1, cost);
        }
          // Watch second atom
        setWatch2(clauseIdx, toFlip);
      }
    }
  }

bool VariableState::isActive

(

const int &

atomIdx

)

[inline]

Checks if an atom is active.

Parameters:

atomIdx

Index of atom to be checked.

Returns:

true, if atom is active, otherwise false.

Definition at line 1736 of file variablestate.h.

References Database::getActiveStatus(), and Domain::getDB().

Referenced by activateAtom(), fixAtom(), initRandom(), and setValueOfAtom().

  {
    return domain_->getDB()->getActiveStatus(gndPredHashArray_[atomIdx-1]);
  }

bool VariableState::isActive

(

const Predicate *

pred

)

[inline]

Checks if an atom is active.

Parameters:

pred

Predicate to be checked.

Returns:

true, if atom is active, otherwise false.

Definition at line 1747 of file variablestate.h.

References Database::getActiveStatus(), and Domain::getDB().

  {
    return domain_->getDB()->getActiveStatus(pred);
  }

void VariableState::addBreakCostToAtomsInClause	(	const int &	clauseIdx,
		const long double &	cost
	)			[inline]

Increases breakCost of all atoms in a given clause.

Parameters:

	clauseIdx	Index of clause whose atoms' breakCost is altered.
	cost	Cost to be added to atoms' breakCost.

Definition at line 1844 of file variablestate.h.

References getClauseSize().

Referenced by flipAtom(), and updateMakeBreakCostAfterFlip().

  {
    register int size = getClauseSize(clauseIdx);
    for (int i = 0; i < size; i++)
    {
      register int lit = clause_[clauseIdx][i];
      breakCost_[abs(lit)] += cost;
    }
  }

void VariableState::subtractBreakCostFromAtomsInClause	(	const int &	clauseIdx,
		const long double &	cost
	)			[inline]

Decreases breakCost of all atoms in a given clause.

Parameters:

	clauseIdx	Index of clause whose atoms' breakCost is altered.
	cost	Cost to be subtracted from atoms' breakCost.

Definition at line 1861 of file variablestate.h.

References getClauseSize().

  {
    register int size = getClauseSize(clauseIdx);
    for (int i = 0; i < size; i++)
    {
      register int lit = clause_[clauseIdx][i];
      breakCost_[abs(lit)] -= cost;
    }
  }

void VariableState::addMakeCost	(	const int &	atomIdx,
		const long double &	cost
	)			[inline]

Increases makeCost of an atom.

Parameters:

	atomIdx	Index of atom whose makeCost is altered.
	cost	Cost to be added to atom's makeCost.

Definition at line 1878 of file variablestate.h.

Referenced by flipAtom(), and updateMakeBreakCostAfterFlip().

  {
    makeCost_[atomIdx] += cost;
  }

void VariableState::subtractMakeCost	(	const int &	atomIdx,
		const long double &	cost
	)			[inline]

Decreases makeCost of an atom.

Parameters:

	atomIdx	Index of atom whose makeCost is altered.
	cost	Cost to be subtracted from atom's makeCost.

Definition at line 1889 of file variablestate.h.

  {
    makeCost_[atomIdx] -= cost;
  }

void VariableState::addMakeCostToAtomsInClause	(	const int &	clauseIdx,
		const long double &	cost
	)			[inline]

Increases makeCost of all atoms in a given clause.

Parameters:

	clauseIdx	Index of clause whose atoms' makeCost is altered.
	cost	Cost to be added to atoms' makeCost.

Definition at line 1900 of file variablestate.h.

References getClauseSize().

Referenced by flipAtom(), and updateMakeBreakCostAfterFlip().

  {
    register int size = getClauseSize(clauseIdx);
    for (int i = 0; i < size; i++)
    {
      register int lit = clause_[clauseIdx][i];
      makeCost_[abs(lit)] += cost;
    }
  }

void VariableState::subtractMakeCostFromAtomsInClause	(	const int &	clauseIdx,
		const long double &	cost
	)			[inline]

Decreases makeCost of all atoms in a given clause.

Parameters:

	clauseIdx	Index of clause whose atoms' makeCost is altered.
	cost	Cost to be subtracted from atoms' makeCost.

Definition at line 1917 of file variablestate.h.

References getClauseSize().

  {
    register int size = getClauseSize(clauseIdx);
    for (int i = 0; i < size; i++)
    {
      register int lit = clause_[clauseIdx][i];
      makeCost_[abs(lit)] -= cost;
    }
  }

const int VariableState::getTrueLiteralOtherThan	(	const int &	clauseIdx,
		const int &	atomIdx1,
		const int &	atomIdx2
	)			[inline]

Retrieves a true literal in a clause other than the two given.

Parameters:

	clauseIdx	Index of clause from which literal is retrieved.
	atomIdx1	Index of first atom excluded from search.
	atomIdx2	Index of second atom excluded from search.

Returns:

Index of atom found.

Definition at line 1937 of file variablestate.h.

References getClauseSize(), and isTrueLiteral().

Referenced by flipAtom(), and updateMakeBreakCostAfterFlip().

  {
    register int size = getClauseSize(clauseIdx);
    for (int i = 0; i < size; i++)
    {
      register int lit = clause_[clauseIdx][i];
      register int v = abs(lit);
      if (isTrueLiteral(lit) && v != atomIdx1 && v != atomIdx2)
        return v;
    }
      // If we're here, then no other true lit exists
    assert(false);
    return -1;
  }

const int VariableState::getRandomTrueLitInClause

(

const int &

clauseIdx

)

[inline]

Retrieves the index of a random true literal in a clause.

Parameters:

clauseIdx

Index of clause from which the literal is retrieved.

Returns:

Index of the atom retrieved.

Definition at line 1984 of file variablestate.h.

References getClauseSize(), and isTrueLiteral().

Referenced by getIndexOfAtomInRandomFalseClause().

  {
    assert(numTrueLits_[clauseIdx] > 0);
    int trueLit = random()%numTrueLits_[clauseIdx];
    int whichTrueLit = 0;
    for (int i = 0; i < getClauseSize(clauseIdx); i++)
    {
      int lit = clause_[clauseIdx][i];
      int atm = abs(lit);
        // True literal
      if (isTrueLiteral(lit))
        if (trueLit == whichTrueLit++)
          return atm;
    }
      // If we're here, then no other true lit exists
    assert(false);
    return -1;
  }

const int VariableState::getBlockIndex

(

const int &

atomIdx

)

[inline]

Returns the index of the block which the atom with index atomIdx is in.

If not in any, returns -1.

Definition at line 2053 of file variablestate.h.

References Domain::getBlock().

Referenced by MaxWalkSat::calculateImprovement(), fixAtom(), SimulatedTempering::infer(), initRandom(), MCMC::performGibbsStep(), MaxWalkSat::pickRandom(), and MCMC::randomInitGndPredsTruthValues().

  {
    const GroundPredicate* gndPred = (*gndPreds_)[atomIdx];
    return domain_->getBlock(gndPred);
  }

void VariableState::makeUnitCosts

(

)

[inline]

Turns all costs into units.

Positive costs are converted to 1, negative costs are converted to -1

Definition at line 2079 of file variablestate.h.

References initMakeBreakCostWatch(), and Array< Type >::size().

Referenced by setInferenceMode().

  {
    for (int i = 0; i < clauseCost_.size(); i++)
    {
      if (clauseCost_[i] >= 0) clauseCost_[i] = 1.0;
      else
      {
        assert(clauseCost_[i] < 0);
        clauseCost_[i] = -1.0;
      }
    }
    if (vsdebug) cout << "Made unit costs" << endl;
    initMakeBreakCostWatch();
  }

void VariableState::getNumClauseGndings	(	Array< double > *const &	numGndings,
		bool	tv
	)			[inline]

Gets the number of (true or false) clause groundings in this state.

If eager, the first order clause frequencies in the mrf are used. If lazy, the f.o. clause frequencies computed when activating are used.

Parameters:

	numGndings	Array being filled with values.
	clauseCnt	Number of first-order clauses (size of numGndings)
	tv	If true, number of true groundings are retrieved, otherwise false groundings are retrieved.

Definition at line 2197 of file variablestate.h.

References MLN::getClause(), MLN::getNumClauses(), Domain::getNumNonEvidGroundings(), isTrueLiteral(), HashArray< Type, HashFn, EqualFn >::size(), and Array< Type >::size().

Referenced by SimulatedTempering::infer(), MCMC::performGibbsStep(), and Inference::tallyCntsFromState().

  {
      // If lazy, then all groundings of pos. clauses not materialized in this
      // state are true (non-materialized groundings of neg. clauses are false),
      // so if tv is false and clause is pos. (or tv is true and clause is
      // neg.), then eager and lazy counts are equivalent. If tv is
      // true and clause is pos. (or tv is false and clause is neg.), then we
      // need to keep track of true *and* false groundings and
      // then subtract from total groundings of the f.o. clause.
      
      // This holds the false groundings when tv is true and lazy.
    Array<double> lazyFalseGndings(numGndings->size(), 0);
    Array<double> lazyTrueGndings(numGndings->size(), 0);

    IntBoolPairItr itr;
    IntBoolPair *clauseFrequencies;
    
      // numGndings should have been initialized with non-negative values
    int clauseCnt = numGndings->size();
    assert(clauseCnt == mln_->getNumClauses());
    for (int clauseno = 0; clauseno < clauseCnt; clauseno++)
      assert ((*numGndings)[clauseno] >= 0);
    
    for (int i = 0; i < gndClauses_->size(); i++)
    {
      GroundClause *gndClause = (*gndClauses_)[i];
      int satLitcnt = 0;
      for (int j = 0; j < gndClause->getNumGroundPredicates(); j++)
      {
        int lit = gndClause->getGroundPredicateIndex(j);
        if (isTrueLiteral(lit)) satLitcnt++;
      }

      clauseFrequencies = gndClause->getClauseFrequencies();
      for (itr = clauseFrequencies->begin();
           itr != clauseFrequencies->end(); itr++)
      {
        int clauseno = itr->first;
        int frequency = itr->second.first;
        bool invertWt = itr->second.second;
          // If flipped unit clause, then we want opposite kind of grounding
        if (invertWt)
        {
            // Want true and is true => don't count it
          if (tv && satLitcnt > 0)
          {
              // Lazy: We need to keep track of false groundings also
            if (lazy_) lazyFalseGndings[clauseno] += frequency;
            continue;
          }
            // Want false and is false => don't count it
          if (!tv && satLitcnt == 0)
          {
              // Lazy: We need to keep track of false groundings also
            if (lazy_) lazyTrueGndings[clauseno] += frequency;
            continue;
          }
        }
        else
        {
            // Want true and is false => don't count it
          if (tv && satLitcnt == 0)
          {
              // Lazy: We need to keep track of false groundings also
            if (lazy_) lazyFalseGndings[clauseno] += frequency;
            continue;
          }
            // Want false and is true => don't count it
          if (!tv && satLitcnt > 0)
          {
              // Lazy: We need to keep track of false groundings also
            if (lazy_) lazyTrueGndings[clauseno] += frequency;
            continue;
          }
        }
        (*numGndings)[clauseno] += frequency;
      }
    }
    
      // Getting true counts in lazy: we have to add the remaining groundings
      // not materialized (they are by definition true groundings if clause is
      // positive, or false groundings if clause is negative)
    if (lazy_)
    {
      for (int c = 0; c < mln_->getNumClauses(); c++)
      {
        const Clause* clause = mln_->getClause(c);
          // Getting true counts and positive clause
        if (tv && clause->getWt() >= 0)
        {
          double totalGndings = domain_->getNumNonEvidGroundings(c);
          assert(totalGndings >= (*numGndings)[c] + lazyFalseGndings[c]);
          double remainingTrueGndings = totalGndings - lazyFalseGndings[c] -
                                        (*numGndings)[c];
          (*numGndings)[c] += remainingTrueGndings;
        }
          // Getting false counts and negative clause
        else if (!tv && clause->getWt() < 0)
        {
          double totalGndings = domain_->getNumNonEvidGroundings(c);
          assert(totalGndings >= (*numGndings)[c] + lazyTrueGndings[c]);
          double remainingFalseGndings = totalGndings - lazyTrueGndings[c] -
                                        (*numGndings)[c];
          (*numGndings)[c] += remainingFalseGndings;
        }
      }
    }

  }

void VariableState::getNumClauseGndingsWithUnknown	(	double	numGndings[],
		int	clauseCnt,
		bool	tv,
		const Array< bool > *const &	unknownPred
	)			[inline]

Gets the number of (true or false) clause groundings in this state.

If eager, the first order clause frequencies in the mrf are used.

Parameters:

	numGndings	Will hold the number of groundings for each first-order clause.
	clauseCnt	Number of first-order clauses whose groundings are being counted.
	tv	If true, true groundings are counted, otherwise false groundings.
	unknownPred	If pred is marked as unknown, it is ignored in the count

Definition at line 2318 of file variablestate.h.

References getNumAtoms(), isTrueLiteral(), HashArray< Type, HashFn, EqualFn >::size(), and Array< Type >::size().

  {
    // TODO: lazy version
    assert(unknownPred->size() == getNumAtoms());
    IntBoolPairItr itr;
    IntBoolPair *clauseFrequencies;
    
    for (int clauseno = 0; clauseno < clauseCnt; clauseno++)
      numGndings[clauseno] = 0;
    
    for (int i = 0; i < gndClauses_->size(); i++)
    {
      GroundClause *gndClause = (*gndClauses_)[i];
      int satLitcnt = 0;
      bool unknown = false;
      for (int j = 0; j < gndClause->getNumGroundPredicates(); j++)
      {
        int lit = gndClause->getGroundPredicateIndex(j);
        if ((*unknownPred)[abs(lit) - 1])
        {
          unknown = true;
          continue;
        }
        if (isTrueLiteral(lit)) satLitcnt++;
      }

      clauseFrequencies = gndClause->getClauseFrequencies();
      for (itr = clauseFrequencies->begin();
           itr != clauseFrequencies->end(); itr++)
      {
        int clauseno = itr->first;
        int frequency = itr->second.first;
        bool invertWt = itr->second.second;
          // If flipped unit clause, then we want opposite kind of grounding
        if (invertWt)
        {
            // Want true and is true or unknown => don't count it
          if (tv && (satLitcnt > 0 || unknown))
            continue;
            // Want false and is false => don't count it
          if (!tv && satLitcnt == 0)
            continue;
        }
        else
        {
            // Want true and is false => don't count it
          if (tv && satLitcnt == 0)
            continue;
            // Want false and is true => don't count it
          if (!tv && (satLitcnt > 0 || unknown))
            continue;
        }
        numGndings[clauseno] += frequency;
      }
    }
  }

void VariableState::setOthersInBlockToFalse	(	const int &	atomIdx,
		const int &	blockIdx
	)			[inline]

Sets the truth values of all atoms in a block except for the one given.

Parameters:

	atomIdx	Absolute index of atom in block exempt from being set to false.
	blockIdx	Index of block whose atoms are set to false.

Definition at line 2384 of file variablestate.h.

References HashArray< Type, HashFn, EqualFn >::find(), Domain::getBlockSize(), Domain::getPredInBlock(), GroundPredicate::print(), and setValueOfAtom().

Referenced by initBlocksRandom().

  {
    if (vsdebug)
    {
      cout << "Set all in block " << blockIdx << " to false except "
           << atomIdx << endl;
    }
    int blockSize = domain_->getBlockSize(blockIdx);
    for (int i = 0; i < blockSize; i++)
    {
      const Predicate* pred = domain_->getPredInBlock(i, blockIdx);
      GroundPredicate* gndPred = new GroundPredicate((Predicate*)pred);      
      int idx = gndPredHashArray_.find(gndPred);

      if (vsdebug)
      {
        cout << "Gnd pred in block ";
        gndPred->print(cout, domain_);
        cout << " (idx " << idx << ")" << endl;
      }

      delete gndPred;
      delete pred;
      
        // Pred already present: check that it's not fixed
      if (idx >= 0)
      {
          // Atom not the one specified and not fixed
        if (idx != atomIdx && fixedAtom_[idx + 1] == 0)
        {
          if (vsdebug)
            cout << "Set " << idx + 1 << " to false" << endl;

          bool activate = true;
          setValueOfAtom(idx + 1, false, activate, -1);
        }
      }
    }
  }

void VariableState::fixAtom	(	const int &	atomIdx,
		const bool &	value
	)			[inline]

Fixes an atom to a truth value.

This means the atom can not change its truth value again. If the atom has already been fixed to the opposite value, then we have a contradiction and the program terminates.

Parameters:

	atomIdx	Index of atom to be fixed.
	value	Truth value to which the atom is fixed.

Definition at line 2433 of file variablestate.h.

References ADD_CLAUSE_REGULAR, addNewClauses(), HashArray< Type, HashFn, EqualFn >::find(), getActiveClauses(), getBlockIndex(), Domain::getBlockSize(), Domain::getDB(), Domain::getPredInBlock(), isActive(), Database::setActiveStatus(), setValueOfAtom(), updateMakeBreakCostAfterFlip(), and updateSatisfiedClauses().

Referenced by activateAtom(), UnitPropagation::infer(), and unitPropagation().

  {
    assert(atomIdx > 0);
    if (vsdebug)
    {
      cout << "Fixing ";
      (*gndPreds_)[atomIdx - 1]->print(cout, domain_);
      cout << " to " << value << endl;    
    }

      // Must be in mc-sat
    if (!useThreshold_)
    {
      cout << ">>> [ERR] useThreshold_ is false" << endl;
      exit(0);
    }

      // If already fixed to opp. sense, then contradiction
    if ((fixedAtom_[atomIdx] == 1 && value == false) ||
        (fixedAtom_[atomIdx] == -1 && value == true))
    {
      cout << "Contradiction: Tried to fix atom " << atomIdx <<
      " to true and false ... exiting." << endl;
      exit(0);
    }

      // already fixed
    if (fixedAtom_[atomIdx] != 0) return;

    fixedAtom_[atomIdx] = (value) ? 1 : -1;     
    if (atom_[atomIdx] != value) 
    {
      bool activate = false;
      int blockIdx =  getBlockIndex(atomIdx - 1);
      setValueOfAtom(atomIdx, value, activate, blockIdx);
      updateMakeBreakCostAfterFlip(atomIdx);
    }
    
      // update isSat
    updateSatisfiedClauses(atomIdx);

      // If in a block and fixing to true, fix all others to false
    if (value)
    {
      int blockIdx = getBlockIndex(atomIdx - 1);
      if (blockIdx > -1)
      {
        int blockSize = domain_->getBlockSize(blockIdx);
        for (int i = 0; i < blockSize; i++)
        {
          const Predicate* pred = domain_->getPredInBlock(i, blockIdx);
          GroundPredicate* gndPred = new GroundPredicate((Predicate*)pred);      
          int idx = gndPredHashArray_.find(gndPred);
          delete gndPred;
          delete pred;
      
            // Pred already present: check that it's not fixed
          if (idx >= 0)
          {
              // Atom not the one specified
            if (idx != (atomIdx - 1))
            {
                // If already fixed to true, then contradiction
              if (fixedAtom_[idx + 1] == 1)
              {
                cout << "Contradiction: Tried to fix atom " << idx + 1 <<
                " to true and false ... exiting." << endl;
                exit(0);
              }
                // already fixed
              if (fixedAtom_[idx + 1] == -1) continue;
              if (vsdebug)
              {
                cout << "Fixing ";
                (*gndPreds_)[idx]->print(cout, domain_);
                cout << " to 0" << endl;
              }
              fixedAtom_[idx + 1] = -1; 
              if (atom_[idx + 1] != false) 
              {
                bool activate = false;
                setValueOfAtom(idx + 1, value, activate, blockIdx);
                updateMakeBreakCostAfterFlip(idx + 1);
              }
                // update isSat
              updateSatisfiedClauses(idx + 1);
            }
          }
        }
      }
    }

      // activate clauses falsified
      // need to updateMakeBreakCost for new clauses only, which aren't sat
    if (lazy_ && !isActive(atomIdx) && value)
    {
        // if inactive fixed to true, need to activate falsified
        // inactive clauses gather active clauses
      Predicate* p =
        gndPredHashArray_[atomIdx - 1]->createEquivalentPredicate(domain_);
                
      bool ignoreActivePreds = false; // only get currently unsat ones
      Array<GroundClause*> unsatClauses;
      getActiveClauses(p, unsatClauses, true, ignoreActivePreds);               
                
        // filter out clauses already added (can also add directly, but
        // will elicit warning)
      addNewClauses(ADD_CLAUSE_REGULAR, unsatClauses);

        // Set active status in db
      domain_->getDB()->setActiveStatus(p, true);
      activeAtoms_++;

      delete p;
    }
  }

Array<int>* VariableState::simplifyClauseFromFixedAtoms

(

const int &

clauseIdx

)

[inline]

Simplifies a clause using atoms which have been fixed.

If clause is satisfied from the fixed atoms, this is marked in isSatisfied_ and an empty array is returned. If clause is empty and not satisfied, then a contradiction has occured. Otherwise, the simplified clause is returned.

Returned array should be deleted.

Parameters:

clauseIdx

Index of the clause to be simplified

Returns:

Simplified clause

Definition at line 2561 of file variablestate.h.

References Array< Type >::append(), Array< Type >::clear(), and getClauseSize().

Referenced by UnitPropagation::infer().

  {
    Array<int>* returnArray = new Array<int>;
      // If already satisfied from fixed atoms, then return empty array
    if (isSatisfied_[clauseIdx]) return returnArray;

      // Keeps track of pos. clause being satisfied or 
      // neg. clause being unsatisfied due to fixed atoms
    bool isGood = (clauseCost_[clauseIdx] >= 0) ? false : true;
      // Keeps track of all atoms being fixed to false in a pos. clause
    bool allFalseAtoms = (clauseCost_[clauseIdx] >= 0) ? true : false;
      // Check each literal in clause
    for (int i = 0; i < getClauseSize(clauseIdx); i++)
    {
      int lit = clause_[clauseIdx][i];
      int fixedValue = fixedAtom_[abs(lit)];

      if (clauseCost_[clauseIdx] >= 0)
      { // Pos. clause: check if clause is satisfied
        if ((fixedValue == 1 && lit > 0) ||
            (fixedValue == -1 && lit < 0))
        { // True fixed lit
          isGood = true;
          allFalseAtoms = false;
          returnArray->clear();
          break;
        }
        else if (fixedValue == 0)
        { // Lit not fixed
          allFalseAtoms = false;
          returnArray->append(lit);
        }
      }
      else
      { // Neg. clause:
        assert(clauseCost_[clauseIdx] < 0);
        if ((fixedValue == 1 && lit > 0) ||
            (fixedValue == -1 && lit < 0))
        { // True fixed lit
          cout << "Contradiction: Tried to fix atom " << abs(lit) <<
          " to true in a negative clause ... exiting." << endl;
          exit(0);
        }
        else
        { // False fixed lit or non-fixed lit
          returnArray->append(lit);
            // Non-fixed lit
          if (fixedValue == 0) isGood = false;          
        }
      }
    }
    if (allFalseAtoms)
    {
      cout << "Contradiction: All atoms in clause " << clauseIdx <<
      " fixed to false ... exiting." << endl;
      exit(0);
    }
    if (isGood) isSatisfied_[clauseIdx] = true;
    return returnArray;
  }

const bool VariableState::isDeadClause

(

const int &

clauseIdx

)

[inline]

Checks if a clause is dead.

Parameters:

clauseIdx

Index of clause being checked.

Returns:

True, if clause is dead, otherwise false.

Definition at line 2628 of file variablestate.h.

Referenced by UnitPropagation::infer(), and unitPropagation().

  {
    return deadClause_[clauseIdx];
  }

void VariableState::killClauses

(

const int &

startClause

)

[inline]

Marks clauses as dead which were not good in the previous iteration of inference or are not picked according to a weighted coin flip.

Parameters:

startClause

All clauses with index of this or greater are looked at to be killed.

Definition at line 2704 of file variablestate.h.

References clauseGoodInPrevious(), getNumClauses(), initMakeBreakCostWatch(), and MODE_HARD.

Referenced by addNewClauses().

  {
      // for hard init, no need to killClauses
    if (inferenceMode_ != MODE_HARD)
    {
      for (int i = startClause; i < getNumClauses(); i++)
      {
        GroundClause* clause = (*gndClauses_)[i];
        if ((clauseGoodInPrevious(i)) &&
            (clause->isHardClause() || random() <= threshold_[i]))
        {
          if (vsdebug)
          {
            cout << "Keeping clause "<< i << " ";
            clause->print(cout, domain_, &gndPredHashArray_);
            cout << endl;
          }
          deadClause_[i] = false;
        }
        else
        {
          deadClause_[i] = true;
        }
      }
    }
    
    initMakeBreakCostWatch(startClause);
  }

const bool VariableState::clauseGoodInPrevious

(

const int &

clauseIdx

)

[inline]

Checks if a clause was good in the previous iteration of inference, i.e.

if it is positive and satisfied or negative and unsatisfied.

Parameters:

clauseIdx

Index of clause being checked.

Returns:

true, if clause was good, otherwise false.

Definition at line 2741 of file variablestate.h.

References Array< Type >::size().

Referenced by killClauses().

  {
      // satisfied: wt-sat
    return (clauseIdx >= prevSatisfiedClause_.size() ||
            prevSatisfiedClause_[clauseIdx]);
  }

void VariableState::printLowState

(

ostream &

out

)

[inline]

Prints the best state found to a stream.

Parameters:

out

Stream to which the state is printed.

Definition at line 2786 of file variablestate.h.

References getNumAtoms().

Referenced by MCSAT::init().

  {
    for (int i = 0; i < getNumAtoms(); i++)
    {
      (*gndPreds_)[i]->print(out, domain_);
      out << " " << lowAtom_[i + 1] << endl;
    }
  }

void VariableState::printGndPred	(	const int &	predIndex,
		ostream &	out
	)			[inline]

Prints a ground predicate to a stream.

Parameters:

	predIndex	Index of predicate to be printed.
	out	Stream to which predicate is printed.

Definition at line 2801 of file variablestate.h.

Referenced by UnitPropagation::getChangedPreds(), SAT::getChangedPreds(), MCMC::getChangedPreds(), UnitPropagation::printProbabilities(), SAT::printProbabilities(), MCMC::printProbabilities(), UnitPropagation::printTruePreds(), SAT::printTruePreds(), MCMC::printTruePreds(), and SAT::printTruePredsH().

  {
    (*gndPreds_)[predIndex]->print(out, domain_);
  }

int VariableState::getIndexOfGroundPredicate

(

GroundPredicate *const &

gndPred

)

[inline]

Finds and returns the index of a ground predicate.

Parameters:

gndPred

GroundPredicate to be found.

Returns:

Index of the ground predicate, if present; otherwise, -1.

Definition at line 2812 of file variablestate.h.

References HashArray< Type, HashFn, EqualFn >::find().

Referenced by MaxWalkSat::calculateImprovement(), MCMC::gibbsSampleFromBlock(), SimulatedTempering::infer(), MCMC::performGibbsStep(), MaxWalkSat::pickRandom(), MCMC::randomInitGndPredsTruthValues(), and MCMC::setOthersInBlockToFalse().

  {
    return gndPredHashArray_.find(gndPred);
  }
  

void VariableState::setAsEvidence	(	const GroundPredicate *const &	predicate,
		const bool &	trueEvidence
	)			[inline]

Sets a GroundPredicate to be evidence and sets its truth value.

If it is already present as evidence with the given truth value, then nothing happens. If the predicate was a query, then additional clauses may be eliminated. reinit() should be called after this in order to ensure that the clause and atom information is correct.

Parameters:

	predicate	GroundPredicate to be set as evidence.
	trueEvidence	The truth value of the predicate is set to this.

Definition at line 2827 of file variablestate.h.

References Array< Type >::bubbleSort(), Array< Type >::compress(), HashArray< Type, HashFn, EqualFn >::compress(), HashArray< Type, HashFn, EqualFn >::find(), Domain::getDB(), getNegOccurenceArray(), getPosOccurenceArray(), Database::getValue(), GroundPredicate::print(), HashArray< Type, HashFn, EqualFn >::removeItem(), Array< Type >::removeItemFastDisorder(), HashArray< Type, HashFn, EqualFn >::removeItemFastDisorder(), Database::setValue(), HashArray< Type, HashFn, EqualFn >::size(), and Array< Type >::size().

  {
    if (vsdebug)
    {
      cout << "Setting to evidence " ;
      predicate->print(cout, domain_);
      cout << endl;
    }
    Database* db = domain_->getDB();
    int atomIdx = gndPredHashArray_.find((GroundPredicate*)predicate);
      // If already evidence, then check its truth value
    if (atomIdx <= 0)
    {
        // If predicate already evidence with same truth value, then do nothing
      if (db->getValue(predicate) == trueEvidence)
        return;
        
        // Changing truth value of evidence
      if (trueEvidence)
        db->setValue(predicate, TRUE);
      else
        db->setValue(predicate, FALSE);
    }
    else
    {
      Array<int> gndClauseIndexes;      
      int deleted;
      gndClauseIndexes = getNegOccurenceArray(atomIdx + 1);
      gndClauseIndexes.bubbleSort();
        // Keep track of how many clauses deleted, because the indices are
        // are adjusted when we remove an element from HashArray
      deleted = 0;
      for (int i = 0; i < gndClauseIndexes.size(); i++)
      {
          // Atom appears neg. in these clauses, so remove the atom from
          // these clauses if true evidence, or remove clause if false evidence
          // or a unit clause
        if (!trueEvidence ||
            (*gndClauses_)[gndClauseIndexes[i]]->getNumGroundPredicates() == 1)
        {          
          if (vsdebug)
            cout << "Deleting ground clause " << gndClauseIndexes[i] << endl;
            // Real index is old index adjusted one lower for every element
            // deleted up until now
          delete (*gndClauses_)[gndClauseIndexes[i] - deleted];
          gndClauses_->removeItem(gndClauseIndexes[i] - deleted);
          deleted++;
        }
        else
        {
          if (vsdebug)
          {
            cout << "Removing gnd pred " << -(atomIdx + 1)
                 << " from ground clause " << gndClauseIndexes[i] << endl;
          }
          (*gndClauses_)[gndClauseIndexes[i]]->removeGndPred(-(atomIdx + 1));
        }
      }

      gndClauseIndexes = getPosOccurenceArray(atomIdx + 1);
      gndClauseIndexes.bubbleSort();
        // Keep track of how many clauses deleted, because the indices are
        // are adjusted when we remove an element from HashArray
      deleted = 0;
      for (int i = 0; i < gndClauseIndexes.size(); i++)
      {
          // Atom appears pos. in these clauses, so remove the atom from
          // these clauses if false evidence, or remove clause if true evidence
          // or a unit clause
        if (trueEvidence ||
            (*gndClauses_)[gndClauseIndexes[i]]->getNumGroundPredicates() == 1)
        {
          if (vsdebug)
            cout << "Deleting ground clause " << gndClauseIndexes[i] << endl;
            // Real index is old index adjusted one lower for every element
            // deleted up until now
          delete (*gndClauses_)[gndClauseIndexes[i] - deleted];
          gndClauses_->removeItem(gndClauseIndexes[i] - deleted);
          deleted++;
        }
        else
        {
          if (vsdebug)
          {
            cout << "Removing gnd pred " << -(atomIdx + 1)
                 << " from ground clause " << gndClauseIndexes[i] << endl;
          }
          (*gndClauses_)[gndClauseIndexes[i]]->removeGndPred(atomIdx + 1);
        }
      }
      
      gndPredHashArray_.removeItemFastDisorder(atomIdx);
      gndPredHashArray_.compress();
      gndPreds_->removeItemFastDisorder(atomIdx);
      gndPreds_->compress();
        // By removing a pred, the pred at the end of the array gets the
        // index of the pred deleted, so we have to update to the new index
        // in all clauses
      int oldIdx = gndPredHashArray_.size();
      replaceAtomIndexInAllClauses(oldIdx, atomIdx);      
    }
  }

void VariableState::setAsQuery

(

const GroundPredicate *const &

predicate

)

[inline]

Sets a GroundPredicate to be query.

If it is already present as query, then nothing happens. If the predicate was evidence, then additional clauses may be added. reinit() should be called after this in order to ensure that the clause and atom information is correct.

Parameters:

predicate

GroundPredicate to be set as a query.

Definition at line 2939 of file variablestate.h.

References HashArray< Type, HashFn, EqualFn >::append(), HashArray< Type, HashFn, EqualFn >::contains(), getActiveClauses(), Domain::getDB(), GroundPredicate::print(), and Database::setEvidenceStatus().

  {
    if (vsdebug)
    {
      cout << "Setting to query " ;
      predicate->print(cout, domain_);
      cout << endl;
    }
    Database* db = domain_->getDB();
      // If already non-evidence, then do nothing
    if (gndPredHashArray_.contains((GroundPredicate*)predicate))
      return;
    else
    {
        // Evidence -> query
        // Add predicate to query set and get clauses
      gndPredHashArray_.append((GroundPredicate*)predicate);
      Predicate* p = predicate->createEquivalentPredicate(domain_);
      db->setEvidenceStatus(p, false);
      bool ignoreActivePreds = true;
      getActiveClauses(p, newClauses_, true, ignoreActivePreds);
    }
  }

GroundPredicate* VariableState::getGndPred

(

const int &

index

)

[inline]

Gets a pointer to a GroundPredicate.

Parameters:

index

Index of the GroundPredicate to be retrieved.

Returns:

Pointer to the GroundPredicate

Definition at line 2971 of file variablestate.h.

Referenced by MCMC::getProbabilityOfPred(), MCMC::gndPredFlippedUpdates(), SimulatedTempering::infer(), MCSAT::infer(), GibbsSampler::infer(), MCMC::initNumTrueLits(), MCMC::performGibbsStep(), and MCMC::randomInitGndPredsTruthValues().

  {
    return (*gndPreds_)[index];
  }

GroundClause* VariableState::getGndClause

(

const int &

index

)

[inline]

Gets a pointer to a GroundClause.

Parameters:

index

Index of the GroundClause to be retrieved.

Returns:

Pointer to the GroundClause

Definition at line 2982 of file variablestate.h.

Referenced by MCMC::gndPredFlippedUpdates(), MCMC::initNumTrueLits(), and MCMC::updateWtsForGndPreds().

  {
    return (*gndClauses_)[index];
  }

const int VariableState::getGndPredIndex

(

GroundPredicate *const &

gndPred

)

[inline]

Gets the index of a GroundPredicate in this state.

Parameters:

gndPred

GroundPredicate whose index is being found.

Returns:

Index of the GroundPredicate, if found; otherwise -1.

Definition at line 3022 of file variablestate.h.

References Array< Type >::find().

Referenced by UnitPropagation::getProbability(), SAT::getProbability(), MCMC::getProbability(), and SAT::getProbabilityH().

  {
    return gndPreds_->find(gndPred);
  }

void VariableState::getActiveClauses	(	Predicate *	inputPred,
		Array< GroundClause * > &	activeClauses,
		bool const &	active,
		bool const &	ignoreActivePreds
	)			[inline]

Gets clauses and weights activated by the predicate inputPred, if active is true.

If false, inactive clauses (and their weights) containing inputPred are retrieved. If inputPred is NULL, then all active (or inactive) clauses and their weights are retrieved.

Parameters:

	inputPred	Only clauses containing this Predicate are looked at. If NULL, then all active clauses are retrieved.
	activeClauses	New active clauses are put here.
	active	If true, active clauses are retrieved, otherwise inactive.
	ignoreActivePreds	If true, active preds are not taken into account. This results in the retrieval of all unsatisfied clauses.

Definition at line 3046 of file variablestate.h.

References Array< Type >::append(), HashArray< Type, HashFn, EqualFn >::append(), HashArray< Type, HashFn, EqualFn >::clear(), Array< Type >::clear(), HashArray< Type, HashFn, EqualFn >::find(), MLN::findClauseIdx(), Clause::getActiveClauses(), MLN::getClause(), MLN::getClausesContainingPred(), Domain::getDB(), Database::getDeactivatedStatus(), GroundClause::getGroundPredicateSense(), Predicate::getId(), MLN::getNumClauses(), GroundClause::getNumGroundPredicates(), GroundClause::getWt(), Clause::getWt(), Clause::getWtPtr(), GroundClause::incrementClauseFrequency(), Clause::isHardClause(), GroundClause::print(), Clause::print(), GroundClause::setGroundPredicateSense(), GroundClause::setWt(), HashArray< Type, HashFn, EqualFn >::size(), Array< Type >::size(), and Timer::time().

Referenced by activateAtom(), fixAtom(), getActiveClauses(), setAsQuery(), and VariableState().

  {
    Timer timer;
    double currTime;

    Clause *fclause;
    GroundClause* newClause;
    int clauseCnt;
    GroundClauseHashArray clauseHashArray;

    Array<GroundClause*>* newClauses = new Array<GroundClause*>; 
  
    const Array<IndexClause*>* indexClauses = NULL;
      
      // inputPred is null: all active clauses should be retrieved
    if (inputPred == NULL)
    {
      clauseCnt = mln_->getNumClauses();
    }
      // Otherwise, look at all first order clauses containing the pred
    else
    {
      if (domain_->getDB()->getDeactivatedStatus(inputPred)) return;
      int predId = inputPred->getId();
      indexClauses = mln_->getClausesContainingPred(predId);
      clauseCnt = indexClauses->size();
    }

      // Look at each first-order clause and get active groundings
    int clauseno = 0;

    while (clauseno < clauseCnt)
    {
      if (inputPred)
        fclause = (Clause *) (*indexClauses)[clauseno]->clause;           
      else
        fclause = (Clause *) mln_->getClause(clauseno);

      if (vsdebug)
      {
        cout << "Getting active clauses for FO clause: ";
        fclause->print(cout, domain_);
        cout << endl;
      }

      currTime = timer.time();

      const double* parentWtPtr = NULL;
      if (!fclause->isHardClause()) parentWtPtr = fclause->getWtPtr();
      const int clauseId = mln_->findClauseIdx(fclause);
      newClauses->clear();

      if (stillActivating_)
        stillActivating_ = fclause->getActiveClauses(inputPred, domain_,
                                                     newClauses,
                                                     &gndPredHashArray_,
                                                     ignoreActivePreds);

      for (int i = 0; i < newClauses->size(); i++)
      {
        long double wt = fclause->getWt();
        newClause = (*newClauses)[i];

          // If already active, ignore; assume all gndClauses_ are active
        if (gndClauses_->find(newClause) >= 0)
        {
          delete newClause;
          continue;
        }

        bool invertWt = false;
          // We want to normalize soft unit clauses to all be positives
        if (!fclause->isHardClause() &&
            newClause->getNumGroundPredicates() == 1 &&
            !newClause->getGroundPredicateSense(0))
        {
          newClause->setGroundPredicateSense(0, true);
          newClause->setWt(-newClause->getWt());
          wt = -wt;
          invertWt = true;
          int addToIndex = gndClauses_->find(newClause);
          if (addToIndex >= 0)
          {
            (*gndClauses_)[addToIndex]->addWt(wt);
            if (parentWtPtr)
              (*gndClauses_)[addToIndex]->incrementClauseFrequency(clauseId, 1,
                                                                   invertWt);
            delete newClause;
            continue;
          }
        }
        
        int pos = clauseHashArray.find(newClause);
          // If clause already present, then just add weight
        if (pos >= 0)
        {
            // Check if already added from this f.o. clause. If so, don't add
            // again
          if (clauseHashArray[pos]->getClauseFrequency(clauseId) > 0)
          {
            delete newClause;
            continue;
          }
          if (vsdebug)
          {
            cout << "Adding weight " << wt << " to clause ";
            clauseHashArray[pos]->print(cout, domain_, &gndPredHashArray_);
            cout << endl;
          }
          clauseHashArray[pos]->addWt(wt);
          if (parentWtPtr)
            clauseHashArray[pos]->incrementClauseFrequency(clauseId, 1,
                                                           invertWt);
          delete newClause;
          continue;
        }

          // If here, then clause is not yet present        
        newClause->setWt(wt);
        if (parentWtPtr)
          newClause->incrementClauseFrequency(clauseId, 1, invertWt);

        if (vsdebug)
        {
          cout << "Appending clause ";
          newClause->print(cout, domain_, &gndPredHashArray_);
          cout << endl;
        }
        clauseHashArray.append(newClause);
      }
      clauseno++; 

    } //while (clauseno < clauseCnt)

    for (int i = 0; i < clauseHashArray.size(); i++)
    {
      newClause = clauseHashArray[i];
      activeClauses.append(newClause);
    }

    newClauses->clear();
    delete newClauses;

    clauseHashArray.clear();
  }

void VariableState::getActiveClauses	(	Array< GroundClause * > &	allClauses,
		bool const &	ignoreActivePreds
	)			[inline]

Get all the active clauses in the database.

Parameters:

	allClauses	Active clauses are retrieved into this Array.
	ignoreActivePreds	If true, active preds are ignored; this means all unsatisfied clauses are retrieved.

Definition at line 3202 of file variablestate.h.

References getActiveClauses().

  {
    getActiveClauses(NULL, allClauses, true, ignoreActivePreds);
  }
  

---

The documentation for this class was generated from the following file:

• src/logic/variablestate.h

---