/*---------------------------------------------------------
 *
 * Satisfiability problem - brute force search (C-RAM)
 *
 */

#include<cram.h>
#include"satisf.h"

#define inp(num) (PEid.extractBit(num))

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

             gate()
    {
        output.zero();
    }

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

};

/* two input nand gate */
class nand2:public gate
{
    public:
    // evaluate
    cboolean &e(const cboolean &in1, const cboolean &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 */
cboolean &net(cboolean in0, cboolean in1, cboolean in2, cboolean in3, cboolean in4, cboolean in5, cboolean in6, cboolean in7, cboolean in8, cboolean in9, cboolean in10, cboolean in11, cboolean in12, cboolean in13, cboolean in14, cboolean in15, cboolean 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()
{

    // satisfied IFF OR over all inputs of net is TRUE
    return (!candScalar(!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))));
}