###############
# ThreeCNF data structure
# Updated by Mark Goadrich 2/16/2008
#
# ThreeCNF is a conjunction of disjunctive clauses, otherwise
# known as conjunctive normal form.  Each clause in ThreeCNF 
# consists of three literals.  Both the clauses and propositional
# symbols are stored in arrays.  I have included what I believe
# to be the necessary methods for this assignment.  Feel free to 
# change and rewrite any part of this code.  

import random

class ThreeCNF:
   
    # the constructor initializes our lists of PropSymbols and Clauses
    def __init__(self, numberOfPropSymbols, numberOfClauses):

	# first create enough space based on input
	self.clauses = []
	self.propSymbols = []

	# randomly create new Propositional symbols and place 
	# them in the array propSymbols
	for i in range(numberOfPropSymbols):
	    self.propSymbols.append(PropSymbol(True, i))
	self.generateTruths()

	# for as many clauses as you need, randomly select three
	# propositional symbols with replacement to be included
	# in the Clause
	for i in range(numberOfClauses):
	    
	    # Make space for three literals
	    lits = []
	    for j in range(3):

		# select the index for a PropSymbol
		temp = random.randrange(numberOfPropSymbols)
		
		# randomly determine the negation status of each literal
		neg = False
		if (random.random() > 0.5):
		    neg = True

		# create the Literal
		lits.append(Literal(self.propSymbols[temp], neg))
	    
	    # place newly formed Clauses in the array of clauses
	    self.clauses.append(Clause(lits[0], lits[1], lits[2]))

    # this method randomly assigns truth values to the Propositional
    # Symbols in our ThreeCNF.
    def generateTruths(self):
	for i in range(len(self.propSymbols)):
	    if (random.random() > 0.5):
		self.propSymbols[i].putValue(True)
	    else:
		self.propSymbols[i].putValue(False)

    # returns true if all of the Clauses in this ThreeCNF are satisfied
    # if we ever find a false clause, return false, otherwise it's true.
    def isSatisfied(self) :
	for i in range(len(self.clauses)):
	    if (not self.clauses[i].findTValue()):
		return False
	return True

    # flips the given PropSymbol i to its negation.  If you try to flip
    # a nonexistant PropSymbol, it will print "Out of Bounds"
    def flipPropSymbol(self, i):
	if (i > len(self.propSymbols) - 1):
	    print "Out of Bounds"
	else:
	    self.propSymbols[i].flip()
    
    # returns the number of true clauses in this ThreeCNF.
    # This is useful in evaluating whether or not to choose a certain
    # truth value assignment.
    def numberOfTrueClauses(self):
	numTrue = 0;
	for i in range(len(self.clauses)):
	    if (self.clauses[i].findTValue()):
		numTrue += 1
	return numTrue
    
    # prints out the clauses in a conjunctive notation for human
    # readability.  ie. (A v ~B v C) ^ (~B v ~D v A) ^ etc...
    def printClauses(self):
	print "Clauses:"
	for i in range(len(self.clauses)):
	    print self.clauses[i]
	    if (i != len(self.clauses) - 1):
		print " ^ ",
	print
    
    # prints the array of PropSymbols, with names followed by their
    # truth value.
    def printPropSymbols(self):
	print "PropSymbols:"
	for i in range(len(self.propSymbols)):
	    print str(i) + ": " + str(self.propSymbols[i].booleanValue())

#######################
# Clause data structre 
# Updated by Mark Goadrich 2/16/2008
#
# The Clause class holds three literals, A, B, C, and 
# three booleans denoting the status of their negation.  
# Clauses consist of a disjunction of literals.  The clause
# is true when at least one of its literals is true.
# In logic, clauses are written as (A v ~B v C)

class Clause:

    # the constructor initializes all the data members
    def __init__(self, A, B, C):
	self.lits = []
	self.lits.append(A)
	self.lits.append(B)
	self.lits.append(C)

    # returns the truth value of the clause. (disjunction of literals)
    def findTValue(self):
	for i in range(len(self.lits)):
	    if (self.lits[i].findTValue()):
		return True
	return False

    # prints out the clause in a human-readable form...(A v B v ~C)
    def __str__(self):
	return "(" + str(self.lits[0]) + " v " + str(self.lits[1]) + \
	       " v " + str(self.lits[2]) + ")"

#################
# Literal data structure
# Updated by Mark Goadrich 2/16/2008
#
# This class contains a Propositional Symbol and a boolean
# value for the status of negation.  Literals are a slight extention
# over PropSymbol, in that they allow the symbol to be negated.

class Literal:

    # the constructor initializes the values for prop and negation
    def __init__(self, prop, negation):
	self.prop = prop;
	self.negation = negation;

    # returns the truth value for the Literal.  If negation is true,
    # then return the negation of the PropSymbol, otherwise return 
    # the value of the PropSymbol.
    def findTValue(self):
	if (self.negation):
	    return not self.prop.booleanValue()
	else:
	    return self.prop.booleanValue()

    # returns a String for easy printing of the literal.  This sticks
    # a squiggle on the front of the PropSymbol to denote negation.
    def __str__(self):
	temp = ""
	if (self.negation):
	    temp = "~"
	temp += str(self.prop.getIndex())
	return temp

##############
# PropSymbol data structure
# Updated by Mark Goadrich 2/16/2008
#
# This class contains a boolean value and an integer index.
# The index can be thought of as its name; rather than using
# P, Q, and R as traditional in Propositional logic, it is 
# easier and helpful in Java to use numbers.

class PropSymbol:

    # The constructor initializes value and index
    def __init__(self, value, index):
	self.value = value;
	self.index = index;

    # flip switches the value of the PropSymbol from true to false
    # and vice versa.  This is helpful in finding a clauses "neighbors"
    def flip(self):
	self.value = not self.value

    # returns the value of this PropSymbol
    def booleanValue(self):
	return self.value

    # returns the "name" of the PropSymbol
    def getIndex(self):
	return self.index

    # assigns a new value to the PropSymbol
    def putValue(self, value):
	self.value = value    
    
########################
# A method for unit testing the ThreeCNF class
def main():
    ps = input("How many propSymbols? ")
    cs = input("How many clauses? ")
    
    testing = ThreeCNF(ps, cs)
    testing.printClauses()
    testing.printPropSymbols()
    print "Is Satisfied? " + str(testing.isSatisfied())
    print "How Many Satisfied out of " + str(cs) + "? " + \
	  str(testing.numberOfTrueClauses())
    symb = random.randrange(ps)
    testing.flipPropSymbol(symb)
    print "Flipped Symbol " + str(symb)
    print "Is Satisfied? " + str(testing.isSatisfied())
    print "How Many Satisfied out of " + str(cs) + "? " + \
	  str(testing.numberOfTrueClauses())