#!/usr/bin/env python3

from util import randomSAT as rdSAT
import matplotlib.pyplot as plt
import seaborn as sns

import numpy as np

def test1():
    kSATInstance = rdSAT.generateRandomKSAT(5, 4, 3)

    print(kSATInstance.toString())

    print("conflicts:")

    for conflict in kSATInstance.getConflicts():
        conflictVerified = False
        
        clause1 = kSATInstance.getClause(conflict[0][0])
        clause2 = kSATInstance.getClause(conflict[1][0])
        
        for binding in clause2:
            if binding == conflict[0][1] * -1:
                conflictVerified = True
                
        print(conflict[0], conflict[1], conflictVerified)
    
def test2():
    data = {}
    
    data["clause"] = []
    data["num"] = []
    data["labels"] = []
    
    for i in range(10000):
        sat = rdSAT.generateRandomKSAT(7, 6, 3)
        
        for ci in range(sat.getNumberOfClauses()):
            clause = sat.getClause(ci)
            clause = list(np.sort(clause))
            
            if clause in data["clause"]:
                clauseIndex = data["clause"].index(clause)
                data["num"][clauseIndex] += 1
            else:
                data["clause"].append(clause)
                data["labels"].append("[{}, {}, {}]".format(clause[0], clause[1], clause[2]))
                data["num"].append(1)
        
    
    print("done ({}) unique clauses".format(len(data["clause"])))
    
    sns.set()
    
    sns.barplot(x=data["labels"], y=data["num"])
    
    plt.show()
    
test2()