#Today was such a nice day, so most of the class was outside. In the first 20 minutes we discussed the class project
#and below (see Help) are some very rudimentary Maple procedures that may be useful for the porject.
#It relies on the stuff we did in C22.txt and C23.txt that is also included in this file

Help:=proc(): print(`EvalB(f,n,v), EvalBT(L,n,v), FP(L,n), BtoA(f,x), RandTF(n,r,K),  gFP(L,n), `): end:

###stuff from C23.txt
Help23:=proc(): print(`IsTa(D1,n), Inter1(S1,S2), Inter(S), Wt(S) , Wtr(S,r), NuPts(D1,n)`) :
print(`IsTb(D1,n) `): end:

 with(combinat):

##stuff from C22.txt

#C22.txt, April 11, 2016
#"Tautologically" of Disjunctive normal form DNF
Help22:=proc(): print(`RC(n,r), RDNF(n,r,K)  ,SubCube(C,n), TF(D1,n) `): end:

#Group Class assignment:
#Producer: Andrew Lohr
#Associate Producer for real Math: Anthony
#Associate Producer for human interface: Alejandro
#Actors for real math: {John C., Keith, Bryan, Jinyoung};
#Actors for stories (under Alejandro): {Ali,Xukai, Emily, Mingjia} 
#Sanitation engineer: Richard V.
#Becky: can pick what she wants

#RC(n,r): a random disjunction in n veriables with r terms
#Data structre for a single conjunction is a susbet of {1,2,..,n,-1, ..., -n}
#such that i and -i can't be together. For example 
#not x3 AND x7 AND not x9= {-3,7,-9}.
RC:=proc(n,r) local S,a,b,ra1,ra2:

ra1:=rand(1..n):
ra2:=rand(0..1):

S:={}:

 while nops(S)<r do

 a:=ra1():
 
  if not (member(a,S) or member(-a,S)) then
    b:=(-1)^ra2():
    S:=S union {a*b}:
  fi:
od:
S:
end:

 #RDNF(n,r,K):  a random DNF with K clauses each being a conjunction of exactly r terms
 RDNF:=proc(n,r,K)  local i: { seq(RC(n,r),i=1..K)}:  end:
 
 #SubCube(C,n): all the vectors in [0,1]^n that belong to the clause C
 SubCube:=proc(C,n) local C1,S1, a:

 if n=0 then
    RETURN({[]}):
 fi:

  C1:=C minus {n,-n}:

  S1:=SubCube(C1,n-1):

  if member(n,C) then
   RETURN({seq([op(a),1], a in S1)}):
  elif member(-n,C) then
   RETURN({seq([op(a),0], a in S1)}):
  elif not member(n,C) and not member(-n,C) then

RETURN({seq([op(a),0], a in S1),seq([op(a),1], a in S1)}):

  else  
    RETURN(FAIL):
fi:


  end:

#TF(D1,n): inputs a DNF in n variables (as above) and outputs the
#set of vectors in [0,1]^n that belong to the union of the subcubes
TF:=proc(D1,n) local C:
 {seq( op(SubCube(C,n)), C in D1)}:
end:

#end C22.txt
  #IsTa(D1,n): inputs a DNF (Disjunctive Normal Form) Boolean Function in
  #our data structure SetOfSets, and a positive integer n (the number of variables), outputs
  #true iff it is a Tautology
 IsTa:=proc(D1,n)  evalb(nops(TF(D1,n))=2^n): end:
 
 #Inter1(S1,S2): The interesection of clause S1 and S2, if empty then returns FAIL
 Inter1:=proc(S1,S2) local i:

  for i in S1 do
    if member(-i,S2) then
      RETURN(FAIL):
    fi:
  od:
   S1 union S2:

 end:

 #Inter(S): Inputs a set of sets (indicating k-dim subcubes) outoputs the subcube that is their
 #intersection , and FAIL if it is emtpy
 Inter:=proc(S) local i,T:

 T:=S[1]:

  for i from 2 to nops(S) do
   T:=Inter1(T,S[i]):
    if T=FAIL then
        RETURN(FAIL):
    fi:
 od:
 T:
 end:
 
   #Wt(S):The weight (proportion) of the clause (wall) S, namely 2^(-nops(S))
   #and 0 if S=FAIL
   Wt:=proc(S)
    if S=FAIL then
      0:
    else
       2^(-nops(S)):
    fi:
   end:

  #Wtr(D1,r): inputs a DNF D1 and a positive integer  r, outputs the
  #sum of the densities of these clauses taken r-at-a-time
  Wtr:=proc(D1,r) local T,t: T:=choose(D1,r):  add(Wt(Inter(t)),t in T):   end:

 
  

#NuPts(D1,n): A counting approach (using the famous Principle of Inclusion-Exclusion)
 #for finding the number of true-false vectors contained in D1
NuPts:=proc(D1,n) local r: 

2^n*add((-1)^(r-1)*Wtr(D1,r),r=1..nops(D1)):

end:






#Added after class by Dr. Z.
#IsTb(f,n): Is f a tautology, using Inclusion and Exclusion and Bonferroni
#as soon as you know for sure. It also outputs the exit k
#(indicating how soon it knew for sure that it was a tautology or not)
IsTb:=proc(f,n) local su,r:
su:=0:

for r from 1 to nops(f) do
su:=su+(-1)^(r-1)*Wtr(f,r):
if r mod 2=1 and su<1 then
 RETURN(false,r):
elif r mod 2=0 and su>=1 then
  RETURN(true,r):
fi:
od:
FAIL:

end:

###stuff from C23.txt

##New stuff done by Dr. Z.
#EvalB(f,n,v) Evaluates the Boolean function f (in DNF) of variables at truth vector v
EvalB:=proc(f,n,v)

if member(v,TF(f,n)) then
 1:
else
0:
fi:

end:
#EvalBT(L,n,v) Evaluates the Boolean transformation(in DNF) of variables at truth vector v
EvalBT:=proc(L,n,v) local i:
[seq(EvalB(L[i],n,v),i=1..nops(L))]:
end:

#FP(L,n): the fixed points of the Boolean transformation
FP:=proc(L,n) local C,v,S:

C:=TF({{}},n):

S:={}:

for v  in C do

if EvalBT(L,n,v)=v then
  S:=S union {v}:
fi:

od:

S:

end:

#BtoAand(C,x): algebraic rendition of clause C
BtoAand:=proc(C,x) local i,gu:

gu:=1:

for i in C do
 if i>0 then
  gu:=gu*x[i]:
 elif i<0 then
   gu:=gu*(1-x[-i]):
 fi:
od:
gu:
end: 


#BtoA(f,x): 
BtoA:=proc(f,x) local f1,la,a,b:

la:=f[nops(f)]:

if nops(f)=1 then
RETURN( BtoAand(f[1],x)):
fi:
f1:=f minus {la}:
a:=BtoAand(la,x):
b:=BtoA(f1,x):
expand(a+b-a*b):
end:



#RandTF(n,r,K): a random Boolean transformation in n verables where each comoponent is a random DNF with n variables, and K clauses, each with r terms
RandTF:=proc(n,r,K)  local i:
[seq(RDNF(n,r,K),i=1..n)]:
end:


#gFP(L,n): the fixed points of the Probability-generalization of a Boolean transformation
gFP:=proc(L,n) local x,L1,G,g,i:

L1:= [seq(BtoA(L[i],x),i=1..nops(L))]:

G:={solve({seq(x[i]=L1[i],i=1..nops(L1))},{seq(x[i],i=1..n)})}:

{seq(evalf(subs(g,[seq(x[i],i=1..n)])),g in G)}:

end: