Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
file stats: LOC: 62   Methods: 3
NCLOC: 17   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
FirstUIP.java - 100% 100% 100%
coverage
 1    /*
 2    * SAT4J: a SATisfiability library for Java
 3    * Copyright (C) 2004 Daniel Le Berre
 4    *
 5    * Based on the original minisat specification from:
 6    *
 7    * An extensible SAT solver. Niklas E?n and Niklas S?rensson.
 8    * Proceedings of the Sixth International Conference on Theory
 9    * and Applications of Satisfiability Testing, LNCS 2919,
 10    * pp 502-518, 2003.
 11    *
 12    * This library is free software; you can redistribute it and/or
 13    * modify it under the terms of the GNU Lesser General Public
 14    * License as published by the Free Software Foundation; either
 15    * version 2.1 of the License, or (at your option) any later version.
 16    *
 17    * This library is distributed in the hope that it will be useful,
 18    * but WITHOUT ANY WARRANTY; without even the implied warranty of
 19    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
 20    * Lesser General Public License for more details.
 21    *
 22    * You should have received a copy of the GNU Lesser General Public
 23    * License along with this library; if not, write to the Free Software
 24    * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
 25    *
 26    */
 27   
 28    package org.sat4j.minisat.uip;
 29   
 30    import java.io.Serializable;
 31   
 32    import org.sat4j.minisat.core.AssertingClauseGenerator;
 33    import org.sat4j.specs.IConstr;
 34   
 35    /**
 36    * FirstUIP scheme introduced in Chaff. Here the generator stops when a
 37    * syntactical criteria is met: only one literal in the current decision level
 38    * appears in the generated clause. The computation is done by counting the
 39    * literals appearing in the current decision level and decrementing that
 40    * counter when a resolution step is done.
 41    *
 42    * @author leberre
 43    */
 44    public class FirstUIP implements AssertingClauseGenerator, Serializable {
 45   
 46    private static final long serialVersionUID = 1L;
 47   
 48    private int counter;
 49   
 50  139151393 public void initAnalyze() {
 51  139151393 counter = 0;
 52    }
 53   
 54  1404897971 public void onCurrentDecisionLevelLiteral(int p) {
 55  1404897971 counter++;
 56    }
 57   
 58  1404897971 public boolean clauseNonAssertive(IConstr reason) {
 59  1404897971 return --counter > 0;
 60    }
 61   
 62    }