/*---------------------------------------------------------
 *
 * Satisfiability problem - brute force search (Uniprocessor)
 *
 */

#include<stdlib.h>
#include<iostream.h>
#include"satisf.h"

#define inp(num) ((testNumber>>num)&1)

typedef unsigned char boolean;

static int testNumber;

/* generic one output gate */
/* with initialization to 0 */
class gate
{
    public:
    boolean output;

            gate()
    {
        output = 0;
    }

    boolean &update(const boolean &newval)
    {
        output = newval;
        return (output);
    }

};

/* two input nand gate */
class nand2:public gate
{
    public:
    boolean &e(const boolean &in1, const boolean &in2)
    {
        return update(!(in1 && in2));
    }
};



nand2 ga, gb, gc, g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10,
      g11, g12, g13, g14, g15;

/* a self-evaluating netlist */
boolean &net(boolean in0, boolean in1, boolean in2, boolean in3, boolean in4, boolean in5, boolean in6, boolean in7, boolean in8, boolean in9, boolean in10, boolean in11, boolean in12, boolean in13, boolean in14, boolean in15, boolean in16)
{
// tree of combinational logic followed a non-satisfiable circuit
    (void) g0.e(g1.e(g2.e(g3.e(in0, in1), g4.e(in2, in3))
                     ,g5.e(g6.e(in4, in5), g7.e(in6, in7)))
                ,g8.e(g9.e(g10.e(in8, in9), g11.e(in10, in11))
        ,g12.e(g13.e(in12, in13), g14.e(in14, g15.e(in15, in16)))));

    return (gc.e(gb.e(ga.e(g0.output, g0.output), g0.output), gb.output));
}


/* Determine if there exists a set of inputs for which the value is true */
boolean satisfiability()
{
    boolean satisfied;
    int testCases;

    testCases = 1 << INPUTCOUNT;

    for (testNumber = 0; testNumber < testCases; testNumber++)
      {
          satisfied = net(inp(0), inp(1), inp(2), inp(3), inp(4), inp(5), inp(6), inp(7), inp(8), inp(9), inp(10), inp(11), inp(12), inp(13), inp(14), inp(15), inp(16));

          if (satisfied)
              break;            // found a solution

      }
    return (satisfied);
}