kodkod.engine.satlab

Interface ReductionStrategy

All Known Implementing Classes:

AdaptiveRCEStrategy, CRRStrategy, DynamicRCEStrategy, ECFPStrategy, HybridStrategy, NCEStrategy, RCEStrategy, SCEStrategy

public interface ReductionStrategy

Strategy for reducing the unsatisfiable core of a SATProver.

Author:

Emina Torlak

Specfields:

traces: ResolutionTrace[]

nexts: IntSet[]

Invariants:

#traces = #nexts

no disj i,j: [0..#nexts) | traces[i] = traces[j] && nexts[i] = nexts[j]

See Also:

SATProver.reduce(ReductionStrategy)

Method Summary

Modifier and Type	Method and Description
IntSet	next(ResolutionTrace trace) Returns the next subtrace of the specified trace to be analyzed, given as a set of indices into the trace.

Method Detail

next

IntSet next(ResolutionTrace trace)

Returns the next subtrace of the specified trace to be analyzed, given as a set of indices into the trace. If there are no more subtraces to be analyzed (i.e. the given trace is minimal according to the minimality measure used by this strategy), returns the empty set.

Requires:

 let t = this.traces[#this.traces-1], n = this.nexts[#this.nexts-1] | 
  unsat(t.elts[n].literals) => 
   (all i: n.ints | let j = #{k: n.ints | k < i} | t.elts[i].equals(trace.elts[j])) 
  else
   trace = t
 

Ensures:

 
  let next = { i: int | 0 <= i < trace.size()-1 } |
   trace.elts[next].antecedents in trace.elts[next] and 
   (some i: [0..#trace) | i !in next and no trace[i].antecedents) and  
   this.nexts' = this.nexts + #this.nexts->next and
   this.traces' = this.traces + #this.traces->trace 
 

Returns:

this.nexts'[#this.nexts-1]