// Path: 3-sat-core/src/main/java/com/anjlab/sat3/Helper.java
// public static ITabularFormula createRandomFormula(Random random, int varCount, int clausesCount)
// {
//     int mMax = getMaxNumberOfUniqueTriplets(varCount);
//         
//     if (clausesCount > mMax) { 
//         throw new IllegalArgumentException(MessageFormat
//             .format("3-SAT formula of {0} variables may have at most {1} valuable clauses, but requested to create formula with " + clausesCount + " clauses",
//                     varCount, mMax));
//     }
// 
//     ITabularFormula formula = new SimpleFormula();
//     for (int i = 0; i < clausesCount && formula.getPermutation().size() < varCount; i++)
//     {
//         formula.add(createRandomTriplet(random, varCount));
//     }
//         
//     return formula;
// }
// 
// Path: 3-sat-core/src/main/java/com/anjlab/sat3/Helper.java
// public static ITabularFormula loadFromFile(String filename) throws IOException
// {
//     String fileExt = filename.substring(filename.lastIndexOf('.'), filename.length());
//         
//     IFormulaReader formulaReader;
//     if (".skt".equals(fileExt))
//     {
//         formulaReader = new RomanovSKTFormulaReader();
//     }
//     else
//     {
//         formulaReader = new GenericFormulaReader();
//     }
//         
//     FileInputStream is = null;
//     try
//     {
//         is = new FileInputStream(new File(filename));
//             
//         ITabularFormula formula = formulaReader.readFormula(is);
//             
//         //  Clear SimpleFormula's tierHash3 after formula loaded
//             
//         ((SimpleFormula) formula).clearTierHash3();
//             
//         return formula;
//     }
//     finally
//     {
//         if (is != null)
//         {
//             is.close();
//         }
//     }
// }
// 
// Path: 3-sat-core/src/main/java/com/anjlab/sat3/Helper.java
// public static void prettyPrint(ITabularFormula formula)
// {
//     printLine('-', 50);
// 
//     StringBuilder builder = buildPrettyOutput(formula);
//     builder.insert(0, '\n');
// 
//     LOGGER.info(builder.toString());
// }
// 
// Path: 3-sat-core/src/main/java/com/anjlab/sat3/Helper.java
// public static void saveToDIMACSFileFormat(ITabularFormula formula, String filename) throws IOException
// {
//     BufferedWriter writer = null;
//     try {
//         writer = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(new File(filename)), "ascii"));
//     
//         StringBuilder builder = new StringBuilder();
//         builder.append("p cnf ");
//         builder.append(formula.getVarCount());
//         builder.append(" ");
//         builder.append(formula.getClausesCount());
//         builder.append('\n');
//         ObjectArrayList tiers = formula.getTiers();
//         for (int i = 0; i < tiers.size(); i++)
//         {
//             ITier tier = (ITier) tiers.get(i);
//             for (ITripletValue tripletValue : tier)
//             {
//                 if (tripletValue.isNotA()) builder.append('-');
//                 builder.append(tier.getAName());
//                 builder.append(' ');
//                 if (tripletValue.isNotB()) builder.append('-');
//                 builder.append(tier.getBName());
//                 builder.append(' ');
//                 if (tripletValue.isNotC()) builder.append('-');
//                 builder.append(tier.getCName());
//                 builder.append(" 0\n");
//             }
//         }
//             
//         writer.write(builder.toString());
//     } 
//     finally 
//     {
//         if (writer != null)
//         {
//             writer.close();
//         }
//     }
// }


import java.io.IOException;
import java.util.Random;
import org.junit.BeforeClass;
import org.junit.Test;
import cern.colt.list.ObjectArrayList;
import static com.anjlab.sat3.Helper.createRandomFormula;
import static com.anjlab.sat3.Helper.loadFromFile;
import static com.anjlab.sat3.Helper.prettyPrint;
import static com.anjlab.sat3.Helper.saveToDIMACSFileFormat;
import static junit.framework.Assert.assertEquals;
import static junit.framework.Assert.assertNotNull;
import static junit.framework.Assert.assertTrue;

/*
 * Copyright (c) 2010 AnjLab
 * 
 * This file is part of 
 * Reference Implementation of Romanov's Polynomial Algorithm for 3-SAT Problem.
 * 
 * Reference Implementation of Romanov's Polynomial Algorithm for 3-SAT Problem 
 * is free software: you can redistribute it and/or modify
 * it under the terms of the GNU Lesser General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 * 
 * Reference Implementation of Romanov's Polynomial Algorithm for 3-SAT Problem
 * is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU Lesser General Public License for more details.
 * 
 * You should have received a copy of the GNU Lesser General Public License
 * along with
 * Reference Implementation of Romanov's Polynomial Algorithm for 3-SAT Problem.
 * If not, see <http://www.gnu.org/licenses/>.
 */
package com.anjlab.sat3;





public class TestLoadSave
{
    @BeforeClass
    public static void setup()
    {
        Helper.UsePrettyPrint = true;
        Helper.EnableAssertions = true;
        System.out.println(TestLoadSave.class.getName());
    }
    
    @Test
    public void testLoadFromDIMACS() throws IOException
    {

// Path: 3-sat-core/src/main/java/com/anjlab/sat3/Helper.java
// public static ITabularFormula createRandomFormula(Random random, int varCount, int clausesCount)
// {
//     int mMax = getMaxNumberOfUniqueTriplets(varCount);
//         
//     if (clausesCount > mMax) { 
//         throw new IllegalArgumentException(MessageFormat
//             .format("3-SAT formula of {0} variables may have at most {1} valuable clauses, but requested to create formula with " + clausesCount + " clauses",
//                     varCount, mMax));
//     }
// 
//     ITabularFormula formula = new SimpleFormula();
//     for (int i = 0; i < clausesCount && formula.getPermutation().size() < varCount; i++)
//     {
//         formula.add(createRandomTriplet(random, varCount));
//     }
//         
//     return formula;
// }
// 
// Path: 3-sat-core/src/main/java/com/anjlab/sat3/Helper.java
// public static ITabularFormula loadFromFile(String filename) throws IOException
// {
//     String fileExt = filename.substring(filename.lastIndexOf('.'), filename.length());
//         
//     IFormulaReader formulaReader;
//     if (".skt".equals(fileExt))
//     {
//         formulaReader = new RomanovSKTFormulaReader();
//     }
//     else
//     {
//         formulaReader = new GenericFormulaReader();
//     }
//         
//     FileInputStream is = null;
//     try
//     {
//         is = new FileInputStream(new File(filename));
//             
//         ITabularFormula formula = formulaReader.readFormula(is);
//             
//         //  Clear SimpleFormula's tierHash3 after formula loaded
//             
//         ((SimpleFormula) formula).clearTierHash3();
//             
//         return formula;
//     }
//     finally
//     {
//         if (is != null)
//         {
//             is.close();
//         }
//     }
// }
// 
// Path: 3-sat-core/src/main/java/com/anjlab/sat3/Helper.java
// public static void prettyPrint(ITabularFormula formula)
// {
//     printLine('-', 50);
// 
//     StringBuilder builder = buildPrettyOutput(formula);
//     builder.insert(0, '\n');
// 
//     LOGGER.info(builder.toString());
// }
// 
// Path: 3-sat-core/src/main/java/com/anjlab/sat3/Helper.java
// public static void saveToDIMACSFileFormat(ITabularFormula formula, String filename) throws IOException
// {
//     BufferedWriter writer = null;
//     try {
//         writer = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(new File(filename)), "ascii"));
//     
//         StringBuilder builder = new StringBuilder();
//         builder.append("p cnf ");
//         builder.append(formula.getVarCount());
//         builder.append(" ");
//         builder.append(formula.getClausesCount());
//         builder.append('\n');
//         ObjectArrayList tiers = formula.getTiers();
//         for (int i = 0; i < tiers.size(); i++)
//         {
//             ITier tier = (ITier) tiers.get(i);
//             for (ITripletValue tripletValue : tier)
//             {
//                 if (tripletValue.isNotA()) builder.append('-');
//                 builder.append(tier.getAName());
//                 builder.append(' ');
//                 if (tripletValue.isNotB()) builder.append('-');
//                 builder.append(tier.getBName());
//                 builder.append(' ');
//                 if (tripletValue.isNotC()) builder.append('-');
//                 builder.append(tier.getCName());
//                 builder.append(" 0\n");
//             }
//         }
//             
//         writer.write(builder.toString());
//     } 
//     finally 
//     {
//         if (writer != null)
//         {
//             writer.close();
//         }
//     }
// }


// Path: 3-sat-core/src/test/java/com/anjlab/sat3/TestLoadSave.java
import java.io.IOException;
import java.util.Random;
import org.junit.BeforeClass;
import org.junit.Test;
import cern.colt.list.ObjectArrayList;
import static com.anjlab.sat3.Helper.createRandomFormula;
import static com.anjlab.sat3.Helper.loadFromFile;
import static com.anjlab.sat3.Helper.prettyPrint;
import static com.anjlab.sat3.Helper.saveToDIMACSFileFormat;
import static junit.framework.Assert.assertEquals;
import static junit.framework.Assert.assertNotNull;
import static junit.framework.Assert.assertTrue;

/*
 * Copyright (c) 2010 AnjLab
 * 
 * This file is part of 
 * Reference Implementation of Romanov's Polynomial Algorithm for 3-SAT Problem.
 * 
 * Reference Implementation of Romanov's Polynomial Algorithm for 3-SAT Problem 
 * is free software: you can redistribute it and/or modify
 * it under the terms of the GNU Lesser General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 * 
 * Reference Implementation of Romanov's Polynomial Algorithm for 3-SAT Problem
 * is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU Lesser General Public License for more details.
 * 
 * You should have received a copy of the GNU Lesser General Public License
 * along with
 * Reference Implementation of Romanov's Polynomial Algorithm for 3-SAT Problem.
 * If not, see <http://www.gnu.org/licenses/>.
 */
package com.anjlab.sat3;





public class TestLoadSave
{
    @BeforeClass
    public static void setup()
    {
        Helper.UsePrettyPrint = true;
        Helper.EnableAssertions = true;
        System.out.println(TestLoadSave.class.getName());
    }
    
    @Test
    public void testLoadFromDIMACS() throws IOException
    {

        ITabularFormula formula = loadFromFile("target/test-classes/article-example.cnf");
