///////////////////////////////////////////////////////////////////////////////
version="$Id: digimult.lib,v 1.6 2006-07-18 15:48:11 Singular Exp $";
category="Logic";
info="
LIBRARY: digimult.lib   Satisfiability of prop. logical expressions
AUTHORS: Michael Brickenstein, bricken@mathematik.uni-kl.de

OVERVIEW:
        Various algorithms for verifiying digital circuits, including SAT-Solvers

PROCEDURES:
         satisfiable(I);   returns 1, if system is satisfiable
";
proc gen_integer_poly(ideal var_i){
  poly erg=0;
  number two=2;
  int i;
  for(i=1;i<=ncols(var_i);i++){

    erg=erg+two^(i-1)*var_i[i];
  }
  return(erg);
}

proc gen_var_ideal(int start, int last){
  ideal erg;
  int i;
  for(i=0;i<=last-start;i++){
    erg[i+1]=var(i+start);
  }
  return(erg);
}

proc poly_cancel_mod_number(poly f, number n){
  if (f==0){
    return(0);
  }
  poly l=lead(f);
  if ((leadcoef(l) mod n)==0){
    return(poly_cancel_mod_number(f-l,n));
  }

  return(l+poly_cancel_mod_number(f-l,n));
}

proc gen_poly_mod2(poly f){
  number max=0;
  number min=0;
  //matrix M=coeffs(M);
  int i=0;
  poly terms=f;
  number c;
  while(terms!=0){
    c=leadcoef(terms);
    if (c>0) {max=max+c;}else{min=min+c;}
    terms=terms-lead(terms);
  }
  number n=min;
  list constr;
  int z=0;
  for(n=min;n<=max;n=n+1){
    z++;
    constr[z]=list(n,n % 2);
  }
  poly u=uni_poly_on_values(constr);
  return(system("bit_subst",u,f)); //subst(u,var(1),f));
  }
proc uni_poly_on_values(list l){
  poly summand;
  poly erg=0;
  int i,j;
  for(i=1;i<=size(l);i++){
    summand=1;
    for(j=1;j<=size(l);j++){
      if(i!=j){
        summand=summand*(var(1)-l[j][1]);
      }
    }
    summand=summand/subst(summand,var(1),l[i][1]);
    summand=summand*l[i][2];
    erg=erg+summand;
  }
  return(erg);
}


proc zero_one_comb(int n){
  list l;
  if (n==1){
    list erg=list(0),list(1);
    return(erg);
  }
  list rec= zero_one_comb(n-1);
  int i=0;
  list l0;
  for(i=1;i<=size(rec);i++){
    l0[i]=list(0)+rec[i];
  }
  list l1;
  for(i=1;i<=size(rec);i++){
    l1[i]=list(1)+rec[i];
  }
  return(l1+l0);
}

proc gen_min_term(list point)
"RETURN: poly function, which is 1 on point, 0 else"
{
  int n=size(point);
  def oldring=basering;
  ring helperring=char(basering),x(1..n),dp;
  list comb=zero_one_comb(n);
  int i,j;
  poly erg=0;
  poly m;
  for(i=1;i<=size(comb);i++){
    m=1;
    for(j=1;j<=n;j++){
      m=m*(var(j))^comb[i][j];
    }
    erg=erg+m;
  }
  list erg_l=helperring,erg;
  setring oldring;
  //return(erg_l);
}

proc satisfiable(ideal i)
"USAGE: use with x(x-1) polys"
{
   ideal bit_ideal=gen_var_ideal(1,nvars(basering));
   int it;
   list var_order;
   for(it=1;it<=nvars(basering);it++){
     var_order[it]=it;
   }
   int step=0;
   return(simple_gps(i,var_order,0));
}

static proc simple_gps(ideal i, list var_order, int step){
  if ((size(i)==0)){~;}
  step=step+1;
  degBound=step+1;
  ideal j;
  if (size(var_order)==0){
    ~;
    degBound=0;
    j=std(i);
    if (reduce(1,j)==0){
      //whole ring
      return(0);
    }
    else {
      return(1);
    }
  }

  j=std(i);
  if (reduce(1,j)==0){
    //whole ring
    return(0);
  }
  j=simplify(j,2);
  //j=simplify(j,8);

  poly v=var(var_order[1]);
  var_order=delete(var_order,1);
  ideal j0=subst(j,v,0);
  "setting", v, "to",0;
  j0=simplify(j0,2);

  j0=simplify(j0,8);
  if (simple_gps(j0,var_order,step)==1){
    return(1);
  } else{
    "setting", v, "to",1;
    ideal j1=subst(j,v,1);
    j1=simplify(j1,2);
    //j0=simplify(j1,8);
    return(simple_gps(j1,var_order, step));
  }

}