FALSE=-1
UNDEF=0
TRUE =1

# Il True e False di Python. Aggiungiamo il prefisso "Py" per non confonderli con
# TRUE e FALSE
PyTrue=True
PyFalse=False

class GV:
        '''Variabil globali di data.py'''
        vars = {}       # dizionario { nome_variabile : istanza_variabile }
        vars_N = 0      # numero di variabili

def sgn(z): return 1 if z>= 0 else -1
def val(l, v): return v if l>=0 else -v

from misc import unique, append_if_new
from debug import DEBUG
class Unsatisfable(Exception): pass
class Conflict(Exception): pass
class TrueClause(Exception): pass

class Clause(object):
        __slots__ = ['undefs', 'ones', 'lit']
        def __init__(self, lit):
                '''lit e' un vettore che rappresenta la clausola. E' del tipo [Z1, Z2, ...]
                   Ogni Zi rappresenta un letterale ed e' un intero (positivo
                   o negativo, diverso da zero). Zi e' negativo se il letterale contiene il 
                   simbolo NOT. In particolare,  1 verra' interpretato come TRUE e -1 come FALSE.
        
                   Nota: per "valutare" una letterale, basta moltiplicare la variabile per il
                   segno del letterale, cioe' sgn(l)*v, dove l e' un letterale che contiene la variabile v. Ad
                   esempio, se l e' "NOT v", con v.value=TRUE, e 15 e' il numero della variabile v, avremo:  
                       l=-15
                       sgn(l)=-1
                       v.value=TRUE=1
                       sgn(l)*v.value=-1=FALSE

                   Questa funzione (__init__) fa una raise di TrueClause se la clausola deve essere scartata.
                '''

                if type(lit) != type([]):
                        raise Exception, 'lit  deve essere un array'

                # rimuovi i duplicati e tutti i FALSE
                self.lit=unique([l for l in lit if l != FALSE])
                
                if self.lit == []:
                        raise Unsatisfable, 'Clausola vuota'

                if TRUE in self.lit:
                        # La clausola contiene TRUE, e' inutile considerarla
                        raise TrueClause
                
                # Controlla se sono presenti letterali del tipo A, NOT A
                if len(self.lit) > len(unique([abs(l) for l in self.lit])):
                        raise TrueClause

                # Aggiorna le clause_list 
                for l in self.lit:
                        GV.vars[abs(l)].clause_list[self]=sgn(l)

                # Il numero di letterali non assegnati
                self.undefs=len(self.lit)

                # Il numero di letterali posti a TRUE
                self.ones = 0

        def adjust_undefs(self):
                '''Resetta il contatore self.undefs, conta il numero di
                   letterali non assegnati correnti e reimposta il contatore'''
                self.undefs=0
                for l in self.lit:
                        if GV.vars[abs(l)].value == UNDEF:
                                self.undefs+=1
        def __str__(self):
                return str(self.lit)+' undefs: '+str(self.undefs)+' ones: '+str(self.ones)

class Var(object):
        __slots__ = ['name', 'value', 'impliedby', 'level', 'clause_list', 'activity']

        def __init__(self, name=0):
                self.name =name        # Il numero che identifica la variabile
                self.value=UNDEF       # Il valore assegnato alla variabile,
                                       # puo' essere: TRUE, FALSE, UNDEF
                self.impliedby=None    # La clausola che ha implicato il
                                       # valore attuale di self.value

                self.level=float("infinity")  # Il livello di decisione
                # Nota: level=0 se la variabile e' stata
                # assegnata durante una decisione "forzata", derivata da clausole 
                # formate da un solo elemento. Una tale variabile non puo'
                # essere modificata durante la procedura di risoluzione.
                
                self.clause_list={}    # Dizionario delle clausole in cui self e'
                                       # un letterale. Formato: { Clausola : segno }
                                       # dove `segno' e' -1 se il letterale e'
                                       # in forma negativa, 1 altrimenti

                self.activity=0        # contatore di attivita'

        def set_value(self, val, impliedby=None, level=None):
                '''Assegna un valore alla variabile.
                   Ritorna la lista delle clausole unitarie generate dall'assegnamento.
                   Se entriamo in conflitto fa il raise dell'errore Conflict'''
                
                if self.value != UNDEF:
                        if self.value != val:
                                raise Conflict  # conflitto
                        if DEBUG: raise Exception, 'Non dovremmo riassegnare lo stesso valore ad una variabile!'
                        return [] # il valore non e' cambiato, e' inutile proseguire

                implied=[]
                self.value=val
                if impliedby!=None:
                        self.impliedby=impliedby
                if level!=None:
                        self.level=level

                # Cerchiamo le clausole che vengono valutate come TRUE e le
                # disabilitiamo aumentando il contatore C.ones.
                # Aggiorniamo anche il contatore C.undefs, cercando clausole
                # che diventano unitarie. In tal caso, le aggiungiamo nella
                # lista `implied' che verra' ritornata in seguito.
                for C, sign in self.clause_list.iteritems():
                        if self.value == sign:
                                # La variabile e' valutata a TRUE in C
                                C.ones+=1
                        C.undefs-=1
                        if C.undefs == 0 and len(C.lit)==1 and sgn(C.lit[0])!=self.value:
                                # C e' una clausola con un solo elemento.
                                # L'elemento deve necessariamente essere `self'. Controlliamo se abbiamo un
                                # conflitto, e in tal caso aggiungiamo C in `implied'.
                                if DEBUG: assert abs(C.lit[0])==self.name
                                implied.append((C, C.lit[0], self))
                        elif C.undefs == 1:
                                # Tutti i letterali, tranne uno, sono assegnati.
                                # Abbiamo quindi trovato una clausola unitaria.
                                found=0
                                for l in C.lit:
                                        v=GV.vars[abs(l)]
                                        if v.value==UNDEF:
                                                implied.append((C, l, v))
                                                found=1
                                                break
                                if DEBUG: assert found == 1
                return implied

        def unset(self):
                '''Azzeriamo il valore di `self', aggiornando tutti i relativi
                   contatori.
                   Nota: Supponiamo che self.value!=UNDEF.'''
                
                oldvalue  = self.value
                self.value=UNDEF

                #Il contrario di quello che e' stato fatto da set_value()
                for C, sgn in self.clause_list.iteritems():
                        if oldvalue == sgn:
                                # La variabile era valutata a TRUE in C
                                C.ones-=1
                        C.undefs+=1

        def reset(self):
                '''Resettiamo la variabile `self', ripristinandola alla
                   condizione di inizio programma. Aggiorniamo pero' il suo
                   contatore di attivita'.  '''
                self.impliedby=None
                self.level=0
                self.activity+=1
                self.unset()

        def get_root_implications(self, alreadyseen=[]):
                '''Ritorna la lista di tutte le variabili decisionali che
                hanno contribuito ad implicare l'attuale valore di `self'.
                Nota: le variabili decisionali sono quelle il cui valore e'
                stato assegnato a seguito di una decisione.'''
                if not self.impliedby:
                        # `self' e' stata assegnata come decisione e non
                        # e' stata implicata.
                        return [self]
                L=[]
                alreadyseen.append(self)
                for l in self.impliedby.lit:
                        l=abs(l)
                        if l == self.name: continue
                        if GV.vars[l] in alreadyseen: continue
                        # Ricursivamente prendiamo le variabili decisionali di `l'
                        L+=GV.vars[l].get_root_implications(alreadyseen+[abs(il) for il in self.impliedby.lit[:]])
                return L

        def __str__(self):
                return 'v:%d val=%d lvl=%d'%(self.name, self.value, self.level)

def adjust_activity():
        '''Ammortizza il contatore di attivita' di ogni variabile, in modo da
           favorire quelle con attivita' piu' recente'''
        for v in GV.vars.itervalues():
                v.activity=float(v.activity)/1.1