Package kodkod.engine.fol2sat

Examples of kodkod.engine.fol2sat.RecordFilter

55
56
57
58
59
60
61
62
63
64
65
   * @return let formulas = (this.log.records[int] & literal.{i: int | abs(i) in coreVars}).formula |
   *       connected = {f: formulas  | some s: set coreNodes | f + this.log.formula in s and (s - this.log.formula).~components in s }
   */
  private Set<Formula>  connectedCore(final IntSet coreVars) {
    final Set<Formula> coreNodes = new IdentityHashSet<Formula>();
    final RecordFilter filter = new RecordFilter() {
      public boolean accept(Node node, Formula translated, int literal, Map<Variable,TupleSet> env) {
        return coreVars.contains(StrictMath.abs(literal));
      }
    };
    for(Iterator<TranslationRecord> itr = log().replay(filter); itr.hasNext(); ) {
View Full Code Here
95
96
97
98
99
100
101
102
103
104
105
   * {@inheritDoc}
   * @see kodkod.engine.Proof#core()
   */
  public final Iterator<TranslationRecord> core() {
    if (coreFilter == null) {
      coreFilter = new RecordFilter() {
        final IntSet coreVariables = StrategyUtils.coreVars(solver.proof());
        final Set<Formula> coreNodes = connectedCore(coreVariables);
        public boolean accept(Node node, Formula translated, int literal, Map<Variable,TupleSet> env) {
          return coreNodes.contains(translated) && coreVariables.contains(StrictMath.abs(literal));
        }
View Full Code Here
112
113
114
115
116
117
118
119
120
121
122
   * {@inheritDoc}
   * @see kodkod.engine.Proof#highLevelCore()
   */
  public final Map<Formula, Node> highLevelCore() {
    if (coreRoots == null) {
      final RecordFilter unitFilter = new RecordFilter() {
        final IntSet coreUnits = StrategyUtils.coreUnits(solver.proof());
        final Set<Formula> roots = log().roots();
        public boolean accept(Node node, Formula translated, int literal, Map<Variable, TupleSet> env) {
          return roots.contains(translated) && coreUnits.contains(Math.abs(literal));
        }
View Full Code Here
69
70
71
72
73
74
75
76
77
78
79
   */
  public static IntSet rootVars(TranslationLog log) {
    final IntSet rootVars = new IntTreeSet();
    final Set<Formula> roots = log.roots();
    final Map<Formula,int[]> maxRootVar = new LinkedHashMap<Formula,int[]>(roots.size());
    final RecordFilter filter = new RecordFilter() {
      public boolean accept(Node node, Formula translated, int literal, Map<Variable, TupleSet> env) {
        return roots.contains(translated) && env.isEmpty();
      }
    };
    for(Iterator<TranslationRecord> itr = log.replay(filter); itr.hasNext();) {
View Full Code Here
117
118
119
120
121
122
123
124
125
126
127
   */
  static SparseSequence<Formula> roots(TranslationLog log) {
    final SparseSequence<Formula> rootVars = new TreeSequence<Formula>();
    final Set<Formula> roots = log.roots();
    final Map<Formula,int[]> maxRootVar = new IdentityHashMap<Formula,int[]>(roots.size());
    final RecordFilter filter = new RecordFilter() {
      public boolean accept(Node node, Formula translated, int literal, Map<Variable, TupleSet> env) {
        return roots.contains(translated) && env.isEmpty();
      }
    };
    for(Iterator<TranslationRecord> itr = log.replay(filter); itr.hasNext();) {
View Full Code Here
56
57
58
59
60
61
62
63
64
65
66
   * {@inheritDoc}
   * @see kodkod.engine.Proof#core()
   */
  public final Iterator<TranslationRecord> core() {
    if (coreFilter==null) {
      coreFilter = new RecordFilter() {
        final Set<Node> coreNodes = NodePruner.relevantNodes(log(),  coreRoots==null ? log().roots() : coreRoots.keySet());
        public boolean accept(Node node, Formula translated, int literal, Map<Variable, TupleSet> env) {
          return coreNodes.contains(translated) ;
        }
      };
View Full Code Here
163
164
165
166
167
168
169
170
171
172
173
    @SuppressWarnings("unchecked")
    NodePruner(TranslationLog log) {
      visited = new IdentityHashSet<Node>();
      relevant = new IdentityHashSet<Node>();
           
      final RecordFilter filter = new RecordFilter() {
        public boolean accept(Node node, Formula translated, int literal, Map<Variable, TupleSet> env) {
          return env.isEmpty();
        } 
      };
     
View Full Code Here
TOP

Related Classes of kodkod.engine.fol2sat.RecordFilter

  • kodkod.engine.ResolutionBasedProof
  • kodkod.engine.TrivialProof
  • kodkod.engine.TrivialProof$NodePruner
  • kodkod.engine.ucore.StrategyUtils
    • Copyright © 2018 www.massapicom. All rights reserved.
    All source code are property of their respective owners. Java is a trademark of Sun Microsystems, Inc and owned by ORACLE Inc. Contact coftware#gmail.com.