diff --git a/o-CNFpolymer/izda.py b/o-CNFpolymer/izda.py index fd6a4c60582a90568307503216524ead87f73723..a1bee29fc7cea632867fc687809e1f0366ab0eac 100644 --- a/o-CNFpolymer/izda.py +++ b/o-CNFpolymer/izda.py @@ -13,15 +13,20 @@ def valueOf(var, assignment): else: return invert(val) - -def ORop(valA, valB): - """ OR operator """ +def parseVar(operation, assignment): + """ parsing a single var """ + assert len(operation)==1 + var= operation[0] + return valueOf(var, assignment) + +def OR2op(valA, valB): + """ OR operator arity 2 """ assert valA=='0' or valA=='1' assert valB=='0' or valB=='1' return '0' if valA=='0' and valB=='0' else '1' def OR3op(valA, valB, valC): - """ OR operator """ + """ OR operator arity 3 """ assert valA=='0' or valA=='1' assert valB=='0' or valB=='1' assert valC=='0' or valC=='1' @@ -33,7 +38,7 @@ def parseOR2(operation, assignment): argA, argB= operation[0], operation[4] valA=valueOf(argA,assignment) valB=valueOf(argB,assignment) - return ORop(valA,valB) + return OR2op(valA,valB) def parseOR3(operation, assignment): """ parsing x v y v z""" @@ -46,45 +51,87 @@ def parseOR3(operation, assignment): -def evaluate(operation,assignment): - arity=1+operation.count('v') - assert arity==2 or arity==3, print("oulala:"+operation) +def evaluateClause(clause, assignment): + """ evaluates """ + arity=1 + clause.count('v') + assert arity==1 or arity==2 or arity==3, print("oulala:"+clause) if arity==2: - val=parseOR2(operation, assignment) - else: - val=parseOR3(operation, assignment) + val=parseOR2(clause, assignment) + elif arity==3: + val=parseOR3(clause, assignment) + else: + val=parseVar(clause, assignment) #print("evaluating %s on assignment:%s >> %s"%(operation,assignment,val)) return val +def evaluateFormula(formula, assignment): + clauselist=formula.split(', ') # splitting chars =' '+ ','!! + resformula='1' + for clause in clauselist: + res=evaluateClause(clause, assignment) + if res=='0': # one clause is evaluated to "false" + resformula='0' + break + return resformula + def assign(a,b,c): return "%s%s%s"%(a,b,c) def scanTab(clause): + """ builds the transition table of a clause """ transtab="" for i in range(8): a,b,c,=i//4,(i//2)%2,i%2 #print ( "i:%d %d %d %d"%(i,a,b,c) ) assi=assign(a,b,c) - res= evaluate(clause, assi) + res= evaluateFormula(clause, assi) transtab+=res W=int(transtab[::-1],2) print("clause:%s W:%d transtab:%s"%(clause, W, transtab)) -listf0=['a v b','b v c','a v c'] -listf1=['A v b','a v B', 'B v c', 'b v C', 'A v c','a v C'] - -listf2=['a v b v c','A v b v c','a v B v c', 'a v b v C', 'A v B v c', 'A v b v C', 'a v B v C', 'A v B v C'] - def evalFormulae(listFormulae): print("-"*30) for form in listFormulae: scanTab(form) print("-"*30) -evalFormulae(listf0) -evalFormulae(listf1) -evalFormulae(listf2) \ No newline at end of file +def testClauses(): + """ test the 26 clauses""" + evalFormulae(listf1) + evalFormulae(listf2a) + evalFormulae(listf2b) + evalFormulae(listf2c) + evalFormulae(listf3) + + +NC=7 + +def combineClauses(): + for i in range(NC): + for j in range(i+1,NC): + print(i,j) + + +# TESTS +############################# + +listf1=['a','b','c','A','B','C'] +listf2a=['a v b','b v c','a v c'] +listf2b=['A v b','a v B', 'B v c', 'b v C', 'A v c','a v C'] +listf2c=['A v B','B v C','A v C'] +listf3=['a v b v c','A v b v c','a v B v c', 'a v b v C', 'A v B v c', 'A v b v C', 'a v B v C', 'A v B v C'] + +#testClauses() + +#formula1=['a, b v c', 'a v b, A v B'] +#evalFormulae(formula1) + +clauses=listf1+listf2a+listf2b+listf2c+listf3 +print (len(clauses), clauses) + +combineClauses() +