/*-----------------------------------------------------------------------

File  : ccl_splitting.c

Author: Stephan Schulz

Contents
 
  Implements functions for destructive splitting of clauses with at
  least two non-propositional variable disjoint subsets of literals.

  Copyright 1998, 1999 by the author.
  This code is released under the GNU General Public Licence and
  the GNU Lesser General Public License.
  See the file COPYING in the main E directory for details..
  Run "eprover -h" for contact information.

Changes

<1> Wed Apr 18 18:24:18 MET DST 2001
    New

-----------------------------------------------------------------------*/

#include "ccl_splitting.h"



/*---------------------------------------------------------------------*/
/*                        Global Variables                             */
/*---------------------------------------------------------------------*/


/*---------------------------------------------------------------------*/
/*                      Forward Declarations                           */
/*---------------------------------------------------------------------*/


/*---------------------------------------------------------------------*/
/*                         Internal Functions                          */
/*---------------------------------------------------------------------*/


/*-----------------------------------------------------------------------
//
// Function: initialize_lit_table()
//
//   Initialize the literal table.
//
// Global Variables: 
//
// Side Effects    : 
//
/----------------------------------------------------------------------*/

static void initialize_lit_table(LitSplitDesc_p lit_table,Clause_p
				 clause, SplitType how, TermProperties
				 var_filter)
{
   int i, lit_no = ClauseLiteralNumber(clause);
   Eqn_p handle = clause->literals;

   for(i=0; i<lit_no; i++)
   {
      assert(handle);
      lit_table[i].literal = handle;
      lit_table[i].part    = 0;
      lit_table[i].varset  = NULL;
      (void)EqnCollectPropVariables(handle, &(lit_table[i].varset),
				  var_filter);
      /* We are only calling EqnCollectVariables for the side
	 effect here */
      if(how == SplitGroundOne || how == SplitGroundNone)
      {
	 if(!lit_table[i].varset)
	 {
	    lit_table[i].part = 1;
	 }
      }
      handle = handle->next;
   }
}


/*-----------------------------------------------------------------------
//
// Function: find_free_literal()
//
//   Find the first entry in lit_table that corresponds to a literal
//   not yet assigned to any clause part and return its index. If none
//   exists, return -1.
//
// Global Variables: -
//
// Side Effects    : -
//
/----------------------------------------------------------------------*/

static int find_free_literal(LitSplitDesc_p lit_table, int lit_no)
{
   int res = -1,i;

   for(i=0; i<lit_no; i++)
   {
      if(!lit_table[i].part)
      {
	 res = i;
	 break;
      }
   }
   return res;
}


/*-----------------------------------------------------------------------
//
// Function: build_part()
//
//   Given the index of the first unassigned literal in lit_table and
//   a part number, assign this number to all literals that are
//   transitively variable-linked to this first literal.
//
// Global Variables: -
//
// Side Effects    : Accumulates all part variables in
//                   lit_table[lit_index].varset 
//
/----------------------------------------------------------------------*/

static void build_part(LitSplitDesc_p lit_table, int lit_no, int
		       lit_index, int part)
{
   bool new_vars = true;
   int  i;

   lit_table[lit_index].part = part;
   while(new_vars)
   {
      new_vars = false;
      for(i=lit_index+1; i< lit_no; i++)
      {
	 if(!lit_table[i].part)
	 {
	    if(PTreeSharedElement(&(lit_table[lit_index].varset),
				  lit_table[i].varset))
	    {
	       lit_table[i].part = part;
	       new_vars = PTreeMerge(&(lit_table[lit_index].varset),
				     lit_table[i].varset)||new_vars;
	       lit_table[i].varset = NULL;
	    }
	 }
      }
   }
}


/*-----------------------------------------------------------------------
//
// Function: clause_split_general()
//
//   Try to split clause into different clauses according to the
//   inference rule below. If successful,
//   deposit split clauses into set and return number of clauses
//   created. Otherwise return 0.
//
//   L1(X) v L2(X) v L3(X) ...
//   ----------------------------------------------------
//   T1(X) v T2(X) v T3(X) ...., 
//   ~T1(X) v L1(X), ~T2(X) v L2(X), ~T3(X) v L3(X), ...
//
//   if the Li are subsets of the clause that do not share any
//   variables but those in the set X and the Ti
//   are _new_ predicate symbols. X is a parameter to the function!
//
//   If fresh_defs is false (and split_vars is empty), try if an
//   existing definition already covers any of the parts and reuse it,
//   otherwise always use fresh definitions.
//
// Global Variables: -
//
// Side Effects    : Memory allocation, if successful, destroys
//                   clause!
//
/----------------------------------------------------------------------*/

int clause_split_general(DefStore_p store, Clause_p clause, 
                         ClauseSet_p set, SplitType how, 
                         bool fresh_defs, PStack_p split_vars)
{
   int              res = 0, part = 0,i,j,size, lit_no, split_var_no;
   LitSplitDesc_p   lit_table;
   Eqn_p            handle,tmp, join;
   FunCode          new_pred;
   long             def_id;
   TB_p             bank;
   Clause_p         new_clause;
   ClauseProperties props;

   assert(clause);
   assert(!clause->children);
   assert(!clause->set);
   assert(set);

   props = ClauseGiveProps(clause, CPTypeMask|CPIsSOS);
   lit_no = ClauseLiteralNumber(clause);

   if(lit_no<=1 || ClauseHasSplitLiteral(clause))
   {
      return 0;
   }
   bank = clause->literals->bank;
   size = lit_no*sizeof(LitSplitDescCell);
   lit_table = SizeMalloc(size);
      
   split_var_no = PStackGetSP(split_vars);
   
   if(!split_var_no)
   {
      initialize_lit_table(lit_table, clause, how, TPIgnoreProps);
   }
   else
   {
      PStackPointer sp;
      Term_p var;

      ClauseTermSetProp(clause, TPCheckFlag);
      for(sp=0; sp<split_var_no; sp++)
      {
	 var = PStackElementP(split_vars,sp);
	 assert(TermCellQueryProp(var, TPCheckFlag));
	 TermCellDelProp(var,TPCheckFlag);	 
      }
      initialize_lit_table(lit_table, clause, how, TPCheckFlag);
   }
   
   if((how == SplitGroundOne) && find_free_literal(lit_table, lit_no))
   {
      part++;
   }
   /* Find the variable disjoint parts of the clause */
   while((i=find_free_literal(lit_table, lit_no))!=-1)
   {
      part++;
      build_part(lit_table, lit_no, i, part);
   }
   if(part>1)
   {
      Clause_p parent1 = clause->parent1;
      Clause_p parent2 = clause->parent2;
      PStack_p def_stack = PStackAlloc();

      ClauseDetachParents(clause);
      
      
      /* Build split clauses from original literals */
      join = NULL;
      clause->literals = NULL; /* Literals are recycled in new
				  clauses, clause skeleton is
				  deallocated below */
      for(i=1; i<=part; i++)
      {   
         if(split_var_no)
         {
            /* Get new predicate code */
            new_pred = SigGetNewPredicateCode(bank->sig,
                                              split_var_no); 
            SigSetFuncProp(bank->sig, new_pred, FPClSplitDef);
            
            /* Create definition clause (for maintaining completeness) */
            handle = GenDefLit(bank, new_pred, true, split_vars);
            assert(!handle->next);

            for(j=0; j<lit_no; j++)
            {
               if(lit_table[j].part == i)
               {
                  tmp = lit_table[j].literal;
                  tmp->next = handle; 
                  handle = tmp;
               }
            }
            new_clause = ClauseAlloc(handle);
            assert(new_clause);

            def_id = new_clause->ident;
            assert(def_id);
            assert(new_pred);
         }
         else            
         {
            /* Create definition clause (for maintaining completeness) */
            handle = NULL;
            for(j=0; j<lit_no; j++)
            {
               if(lit_table[j].part == i)
               {
                  tmp = lit_table[j].literal;
                  tmp->next = handle; 
                  handle = tmp;
               }
            }
            new_clause = GetDefinition(store, handle, 
                                       &new_pred, fresh_defs, &def_id);
            assert(def_id);
            assert(new_pred);            
         }
         PStackPushInt(def_stack, def_id);

         if(new_clause)
         {
            /* Fix clause properties */

            new_clause->properties = props;
            /* Note: Potentially recycled definitions have no real
               parents, as they are conceptually introduced ad-hoc and
               can be reused for many other clauses. */
            if(parent1 && fresh_defs)
            {
               new_clause->parent1 = parent1;
               ClauseRegisterChild(parent1, new_clause);
            }
            if(parent2 && fresh_defs)
            {
               new_clause->parent2 = parent2;
               ClauseRegisterChild(parent2, new_clause);
            }
            
            /* Insert result clause */
            ClauseSetInsert(set, new_clause);

            /* Document creation -> Now done in ccl_def_handling.c*/
            /* DocClauseCreationDefault(new_clause, inf_split, clause,
               NULL); */
         }
         /* Extend remainder clause (after application of definition) */
	 tmp       = GenDefLit(bank, new_pred, false, split_vars);
	 tmp->next = join;
	 join = tmp;
      }
      new_clause = ClauseAlloc(join);
      new_clause->properties = props;
      if(parent1)
      {
	 new_clause->parent1 = parent1;
	 ClauseRegisterChild(parent1, new_clause);
      }
      if(parent2)
      {
	 new_clause->parent2 = parent2;
	 ClauseRegisterChild(parent2, new_clause);
      }
      ClauseSetInsert(set, new_clause);
      /* DocClauseCreationDefault(new_clause, inf_split, clause, NULL); */
      DocClauseApplyDefsDefault(new_clause, clause, def_stack);
      ClauseFree(clause);      /* We still retain the literals in the
				  split clauses! */
      res = part+1;
      PStackFree(def_stack);
   }
   for(i=0; i<lit_no; i++)
   {
      PTreeFree(lit_table[i].varset);
   }
   SizeFree(lit_table, size);
   
   return res;
}


/*-----------------------------------------------------------------------
//
// Function: initialize_permute_stack()
//
//   We want to generate unordered n-tuples from k elements. This
//   initializes a stack to contain the first valid sample (1, 2,
//   ...n) of size n.
//
// Global Variables: -
//
// Side Effects    : -
//
/----------------------------------------------------------------------*/

static void initialize_permute_stack(PStack_p stack, int size)
{
   int i;
   
   PStackReset(stack);
   for(i=0; i<size; i++)
   {
      PStackPushInt(stack, i);
   }
}

/*-----------------------------------------------------------------------
//
// Function: permute_stack_next()
//
//   Generate the next valid permutation and return true if it exists,
//   otherwise return false.
//
// Global Variables: -
//
// Side Effects    : -
//
/----------------------------------------------------------------------*/

static bool permute_stack_next(PStack_p permute_stack, int var_no)
{
   PStackPointer limit = PStackGetSP(permute_stack), i;
   long tmp;
   
   i = 0;
   while(i < limit)
   {
      tmp = PStackPopInt(permute_stack);
      tmp++;
      if((tmp) < (var_no-i))
      {	 
	 while(i>=0)
	 {
	    PStackPushInt(permute_stack, tmp);
	    tmp++;
	    i--;
	 }
	 return true;
      }
      i++;
   }
   return false;
}

/*---------------------------------------------------------------------*/
/*                         Exported Functions                          */
/*---------------------------------------------------------------------*/


/*-----------------------------------------------------------------------
//
// Function: ClauseHasSplitLiteral()
//
//   Return true if a literal in the clause is a split literal.
//
// Global Variables: -
//
// Side Effects    : -
//
/----------------------------------------------------------------------*/

bool ClauseHasSplitLiteral(Clause_p clause)
{
   Eqn_p handle;

   for(handle = clause->literals; handle; handle = handle->next)
   {
      if(EqnQueryProp(handle, EPIsSplitLit))
      {
	 return true;
      }
   }
   return false;   
}



/*-----------------------------------------------------------------------
//
// Function: ClauseSplit()
//
//   Try to split clause into different clauses according to the
//   inference rule below. If successful,
//   deposit split clauses into set and return number of clauses
//   created. Otherwise return 0.
//
//   L1 v L2 v L3 ...
//   ----------------------------------------------------
//   T1 v T2 v T3 ...., ~T1 v L1, ~T2 v L2, ~T3 v L3, ...
//
//   if the Li are variable-disjoint subsets of the clause and the Ti
//   are _new_ propositional variables.
//
// Global Variables: -
//
// Side Effects    : Memory allocation, if successful, destroys
//                   clause!
//
/----------------------------------------------------------------------*/

int ClauseSplit(DefStore_p store, Clause_p clause, ClauseSet_p set, 
                SplitType how, bool fresh_defs)
{
   int res ;
   PStack_p dummy = PStackAlloc();
   
   res = clause_split_general(store, clause, set, how, fresh_defs, dummy);
   PStackFree(dummy);
   return res;
}


/*-----------------------------------------------------------------------
//
// Function: ClauseSplitGeneral()
//
//   Wrapper for clause_split_general(). Tries tries different
//   variable subsets (partially ordered by cardinality) to find a
//   subset that splits the clause. Only used for eground, so I skimp
//   on options.
//
// Global Variables: -
//
// Side Effects    : Memory allocation, if successful, destroys
//                   clause!
//
/----------------------------------------------------------------------*/

int ClauseSplitGeneral(DefStore_p store, bool fresh_defs, 
                       Clause_p clause, ClauseSet_p set, long tries)
{
   int res, var_no, set_size;
   PStackPointer i;
   PStack_p vars, split_vars, permute_stack;
   PTree_p  vars_tree = NULL;

   res =  ClauseSplit(store, clause, set, SplitGroundOne, fresh_defs);
   if(res)
   {
      return res;
   }
   
   var_no = ClauseCollectVariables(clause, &vars_tree);
   if(var_no<=2) /* Non-ground splitting is useless here */
   {
      PTreeFree(vars_tree);
      return 0;
   }
   vars = PStackAlloc();
   split_vars = PStackAlloc();
   permute_stack = PStackAlloc();

   PTreeToPStack(vars, vars_tree);
   PTreeFree(vars_tree);   

   set_size = 1;
   
   initialize_permute_stack(permute_stack, set_size);
   
   while(tries)
   {      
      PStackReset(split_vars);
      for(i=0; i<set_size; i++)
      {
	 PStackPushP(split_vars, 
		     PStackElementP(vars,
				    PStackElementInt(permute_stack, i)));	 
      }
      res = clause_split_general(store, clause, set, SplitGroundNone, 
                                 fresh_defs, split_vars);
      if(res)
      {
	 break;
      }
      if(!permute_stack_next(permute_stack, var_no))
      {
	 if(set_size == var_no-2)
	 {
	    break;
	 }
	 set_size++;
	 initialize_permute_stack(permute_stack, set_size);
      }
      tries--;
   }
   PStackFree(permute_stack);
   PStackFree(split_vars);
   PStackFree(vars);
   return res;
}


/*-----------------------------------------------------------------------
//
// Function: ClauseSetSplitClauses()
//
//   Split all clauses in from_set and put the result into to_set.
//
// Global Variables: -
//
// Side Effects    : -
//
/----------------------------------------------------------------------*/

long ClauseSetSplitClauses(DefStore_p store, ClauseSet_p from_set, 
                           ClauseSet_p to_set, SplitType how, bool fresh_defs)
{
   long res=0, tmp;
   Clause_p handle;

   assert(from_set&&to_set);

   while(!ClauseSetEmpty(from_set))
   {
      handle = ClauseSetExtractFirst(from_set);
      tmp = ClauseSplit(store, handle, to_set, how, fresh_defs);
      if(!tmp)
      {
	 ClauseSetInsert(to_set, handle);
      }
      res += tmp;
   }
   return res;
}



/*-----------------------------------------------------------------------
//
// Function: ClauseSetSplitClausesGeneral()
//
//   Split all clauses in from_set and put the result into to_set.
//
// Global Variables: -
//
// Side Effects    : -
//
/----------------------------------------------------------------------*/

long ClauseSetSplitClausesGeneral(DefStore_p store, bool fresh_defs, 
                                  ClauseSet_p from_set, 
                                  ClauseSet_p to_set, long tries)
{
   long res=0, tmp;
   Clause_p handle;

   assert(from_set&&to_set);

   while(!ClauseSetEmpty(from_set))
   {
      handle = ClauseSetExtractFirst(from_set);
      tmp = ClauseSplitGeneral(store, fresh_defs, handle, to_set, tries);
      if(!tmp)
      {
	 ClauseSetInsert(to_set, handle);
      }
      res += tmp;
   }
   return res;
}




/*---------------------------------------------------------------------*/
/*                        End of File                                  */
/*---------------------------------------------------------------------*/