/* \section{Test harness}                                                   */
/* To test the operation of [[LocalSearch()]] we need to construct an       */
/* instance and feed it to the function.  This code must be linked with     */
/* [[cnf.o]] and [[hill.o]]  (See the Makefile).                            */
/*                                                                          */
/*                                                                          */
/* <testhill.c>=                                                            */
/* \title{hill.nw - Hill climbing routines for solving satisfiabilty problems.} */
   /* \author{}                                                                */
   /* \maketitle                                                               */
   /*                                                                          */
   /* <Copyright notice>= */
   /* 
  Copyright (C) 1993 by Fred Annexstein, John Franco, Humberto
   Ortiz-Zuazaga, Manian Swaminathan.

   This program is free software; you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2 of the License, or (at
   your option) any later version.

   This program 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
   General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with this program; if not, write to the Free Software
   Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. */
#include <assert.h>
#include <stdio.h>
#include <stdlib.h>
#include "cnfparse.h"
#include "cnf.h"
#include "hill.h"

int main (int, char**);

int main (int argc, char *argv[]) {
  FILE *infile;
  CNFInstance *instance;

  if (2 != argc) {
    fprintf (stderr,
"    Testhill version 0.1, Copyright (C) 1993 Fred Annexstein,\n\
    John Franco, Humberto Ortiz-Zuazaga, and Manian Swaminathan.\n\
    Testhill comes with ABSOLUTELY NO WARRANTY; for details see\n\
    the file COPYING.\n\
    This is free software, and you are welcome to redistribute it\n\
    under certain conditions; see the file COPYING for details.\n\
\n\
Usage: testhill {inputfile}\n");
    exit (1);
  }

  printf ("    Testhill version 0.1, Copyright (C) 1993 Fred Annexstein,\n\
    John Franco, Humberto Ortiz-Zuazaga, and Manian Swaminathan.\n\n");

  if (NULL == (infile = fopen (argv[1], "r"))) {
    fprintf (stderr, "Cannot open file %s\n", argv[1]);
    exit (1);
  }
  
  instance = BuildInstance (infile);
  assert (NULL != instance);

  fclose (infile);

  printf ("Clauses:  %d, Variables:  %d, Longest:  %d\n",
          instance->clause_cnt, instance->var_cnt, instance->longest_clause);

  if (TRUE == LocalSearch (instance)) {
    if (TRUE == TestInstance (instance)) {
      printf ("Solved!.\n");
    }
    else {
      printf ("Error: LocalSearch returned true for unsatisfied instance.\n");
    }
  }

  DeleteCNFInstance (instance);
  FreeCnf ();

  exit (0);
}