Examples of kodkod.engine.satlab.SATSolver.addClause()

kodkod.engine.satlab.SATSolver.addClause()

Ensures that this solver logically contains the given clause, and returns true if this.clauses changed as a result of the call. No reference to the specified array is kept, so it can be reused. The contents of the array may, however, be modified. It is the client's responsibility to ensure that no literals in the given array are repeated, or that both a literal and its negation are present. The behavior of this method is undefined if it is called after this.solve() has returned false. @requires all i: [0..lits.length) | abs(lits[i]) in this.variables @requires all disj i,j: [0..lits.length) | abs(lits[i]) != abs(lits[j]) @effects [[this.clauses']] = ([[this.clauses]] and [[lits]]) @return #this.clauses' > #this.clauses @throws NullPointerException - lits = null

          final int primary = translation.numPrimaryVariables();
          final int[] notModel = new int[primary];
          for(int i = 1; i <= primary; i++) {
            notModel[i-1] = cnf.valueOf(i) ? -i : i;
          }
          cnf.addClause(notModel);
          return sol;
        } else {
          formula = null; bounds = null; // unsat, no more solutions, free up some space
          return unsat(translation, stats);
        }

//        solver.addClause(input.accept(translator,null));
        input.accept(translator, null);
      }
      for(BooleanFormula input : circuit) { 
        translator.unaryClause[0] = input.label();
        solver.addClause(translator.unaryClause);
      }
    } else {
      solver.addClause(circuit.accept(translator,null));
    }
    return solver;

      for(BooleanFormula input : circuit) { 
        translator.unaryClause[0] = input.label();
        solver.addClause(translator.unaryClause);
      }
    } else {
      solver.addClause(circuit.accept(translator,null));
    }
    return solver;
  }


  /**

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.