Thesis.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<h2>Term Implementations</h2>\n",
    "\n",
    "<p>Also contains recursive reduceSize() code to compute s<sub>dag</sub>.</p>\n",
    "<p>Sorry everything isnt completely cleaned up yet.</p>\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "#deepcopy used to create repeated terms while keeping the original (that is possibly used elsewhere) intact.\n",
    "from copy import deepcopy\n",
    "\n",
    "#Assumtions:\n",
    "#All symbols are unique.\n",
    "#Integers can NOT be used as symbols, as they are used for internal variable use."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Constant structure loaded.\n"
     ]
    }
   ],
   "source": [
    "#Implementation of contsant. Overrides str, len, eq, and hash.\n",
    "class Constant:\n",
    "    registry = set()\n",
    "    \n",
    "    def __init__(self, s):\n",
    "        self.sym = s\n",
    "        self.arity = 0\n",
    "        self.length = 1\n",
    "        Constant.registry.add(self)\n",
    "        \n",
    "    def __str__(self):\n",
    "        return self.sym\n",
    "        \n",
    "    def __len__(self):\n",
    "        return self.length\n",
    "    \n",
    "    #def __eq__(self, other):\n",
    "    #    return isinstance(other, Constant) and self.sym == other.sym\n",
    "    \n",
    "    def __eq__(self, other):\n",
    "        return str(self) == str(other)\n",
    "\n",
    "    def __hash__(self):\n",
    "        return hash(str(self))\n",
    "    \n",
    "    #Tested different naming scheme. Not currently in use.\n",
    "    def name(self,s):\n",
    "        if sum([1 if i.sym==s else 0 for i in Constant.registry])>0:\n",
    "            return self.name(s + \".\")\n",
    "        else: return s\n",
    "    \n",
    "    #Constant size can not be reduced. Higher-level structures can determine if it is a repeat.\n",
    "    def reduceSize(self):\n",
    "        pass\n",
    "    \n",
    "    def reducedSize(self):\n",
    "        return self.length\n",
    "    \n",
    "    #Will always be a ground term. Base of higher level isGround recursion.\n",
    "    def isGround(self):\n",
    "        return True\n",
    "    \n",
    "    #No variables. Returns empty list to conform with other structures use of list concacts.\n",
    "    def findVariables(self):\n",
    "        return []\n",
    "    \n",
    "    #Is a constants. Returns object wrapped in list to conform with other structures use of list concacts.\n",
    "    #Base of higher level findConstants recursion.\n",
    "    def findConstants(self):\n",
    "        return [self]\n",
    "    \n",
    "    #Is Inherently a repeated term once found. Base of higher level findRepeats recursion.\n",
    "    def findRepeats(self):\n",
    "        return [self]\n",
    "    \n",
    "    #No functions. Returns empty list to conform with other structures use of list concacts.\n",
    "    def findFunctions(self):\n",
    "        return []\n",
    "    \n",
    "    #Nothing to replace. Base of higher level replace recursion.\n",
    "    def replace(self, var, rpt):\n",
    "        return self\n",
    "    \n",
    "print \"Constant structure loaded.\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Repeat structure loaded.\n"
     ]
    }
   ],
   "source": [
    "#Implementation of repeat. Encapsulates replaced object in case the information is needed. Length is always 0.\n",
    "#Overrides str, len, eq, and hash\n",
    "class Repeat:\n",
    "    \n",
    "    def __init__(self, original):\n",
    "        self.sym = '*'\n",
    "        self.origin = original\n",
    "        self.length = 0\n",
    "    \n",
    "    #Currently shows just a star. Switch commented line for more informative printed information.\n",
    "    def __str__(self):\n",
    "        return self.sym + str(self.origin) + self.sym\n",
    "        #return self.origin.sym\n",
    "        \n",
    "    def __len__(self):\n",
    "        return self.length\n",
    "    \n",
    "    #Checks encapsulated object of equality beyond just being a repeat.\n",
    "    #def __eq__(self, other):\n",
    "    #    return isinstance(other, type(self.origin)) and \\\n",
    "    #    self.origin.sym == other.sym and self.origin.params == other.params\n",
    "    \n",
    "    def __eq__(self, other):\n",
    "        return (str(self) == str(other)) or (str(self.origin) == str(other))\n",
    "        \n",
    "    def __hash__(self):\n",
    "        return hash(str(self.origin))\n",
    "    \n",
    "    #Size already reduced. Implemented so that reduceSize still works if accidentally called multiple times.\n",
    "    def reduceSize(self):\n",
    "        pass\n",
    "    \n",
    "    def reducedSize(self):\n",
    "        return self.length\n",
    "    \n",
    "    #Ground determined by encapsulated object. Passed on to that function.\n",
    "    def isGround(self):\n",
    "        return self.origin.isGround()\n",
    "    \n",
    "    #Variables determined by encapsulated object. Passed on to that function.\n",
    "    def findVariables(self):\n",
    "        return self.origin.findVariables()\n",
    "    \n",
    "    #Constants determined by encapsulated object. Passed on to that function.\n",
    "    def findConstants(self):\n",
    "        return self.origin.findConstants()\n",
    "    \n",
    "    #First instance of this repeat already included in search. \n",
    "    #Empty list used to conform with higher level findRepeat.\n",
    "    def findRepeats(self):\n",
    "        return []\n",
    "    \n",
    "    #Functions determined by encapsulated object. Passed on to that function.\n",
    "    def findFunctions(self):\n",
    "        return self.origin.findFunctions()\n",
    "    \n",
    "    \n",
    "    #No variable to replace. Should not replace underlying object (if possible) \n",
    "    #because there is some clause that does not have this as a repeat.\n",
    "    def replace(self, var, rpt):\n",
    "        return self\n",
    "\n",
    "print \"Repeat structure loaded.\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Variable structure loaded.\n"
     ]
    }
   ],
   "source": [
    "#Implementaion of variable. Frequently replaced with other objects in enumerate algorithm.\n",
    "#Overrides str, len, eq, and hash.\n",
    "class Variable:\n",
    "    \n",
    "    tally = 0\n",
    "    \n",
    "    def __init__(self, s=0):\n",
    "        if s==0:\n",
    "            self.sym = self.name()\n",
    "        else:\n",
    "            self.sym = s\n",
    "        #self.length = 1 #Use minimal possible size.\n",
    "        self.length = 0\n",
    "        \n",
    "    def __str__(self):\n",
    "        return self.sym\n",
    "    \n",
    "    def __len__(self):\n",
    "        return self.length\n",
    "    \n",
    "    #def __eq__(self, other):\n",
    "    #    return (isinstance(other, Variable) and self.sym == other.sym)\n",
    "    \n",
    "    def __eq__(self, other):\n",
    "        return str(self) == str(other)\n",
    "    \n",
    "    def __hash__(self):\n",
    "        return id(str(self))\n",
    "    \n",
    "    def name(self):\n",
    "        Variable.tally+=1\n",
    "        return str(Variable.tally)\n",
    "    \n",
    "    #Variable size can not be reduced. Higher-level structures can determine if it is a repeat.\n",
    "    def reduceSize(self):\n",
    "        pass\n",
    "    \n",
    "    def reducedSize(self):\n",
    "        return self.length\n",
    "    \n",
    "    #Will never be a ground term. Base of higher level isGround recursion.\n",
    "    def isGround(self):\n",
    "        return False\n",
    "    \n",
    "    #Is a variable. Returns object wrapped in list to conform with other structures use of list concacts.\n",
    "    #Base of higher level findVariables recursion.\n",
    "    def findVariables(self):\n",
    "        return [self]\n",
    "    \n",
    "    #No variables. Returns empty list to conform with other structures use of list concacts.\n",
    "    def findConstants(self):\n",
    "        return []\n",
    "    \n",
    "    #Is Inherently a repeated term once found. Base of higher level findRepeats recursion.\n",
    "    def findRepeats(self):\n",
    "        return []\n",
    "    \n",
    "    #No functions. Returns empty list to conform with other structures use of list concacts.\n",
    "    def findFunctions(self):\n",
    "        return []\n",
    "    \n",
    "    #Returns a copy of the predicate with 'var' replaced with 'rpt'.\n",
    "    #Should not need to copy, because it was done by the clause.\n",
    "    def replace(self, var, rpt):\n",
    "        #variable = deepcopy(self)\n",
    "        variable = self\n",
    "        if self==var:\n",
    "                return rpt\n",
    "        else:\n",
    "                return variable\n",
    "\n",
    "print \"Variable structure loaded.\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Function structure loaded.\n"
     ]
    }
   ],
   "source": [
    "#Implementation of function. Includes symbol (must be unique) and list of paramaters.\n",
    "#Registry containts copies of all functions that may be altered in enumerate algorithm.\n",
    "#Consider including arity parameter.\n",
    "#Overrides str, len, eq, and hash\n",
    "class Function:\n",
    "    \n",
    "    #Length calculated by definition: 1 + length of each parameter.\n",
    "    def __init__(self, s, *args):\n",
    "        self.sym = s\n",
    "        self.params = list(args)\n",
    "        self.arity = len(args)\n",
    "        self.length = 1+sum([len(i) for i in self.params])\n",
    "\n",
    "    def __str__(self):\n",
    "        toReturn = self.sym + \"(\"\n",
    "        for i in self.params:\n",
    "            toReturn += str(i) + \",\"\n",
    "        toReturn = toReturn[:-1] + \")\"\n",
    "        return toReturn\n",
    "    \n",
    "    def __len__(self):\n",
    "        return 1+sum([len(i) for i in self.params])\n",
    "                     \n",
    "    #def __eq__(self, other):\n",
    "    #    return isinstance(other, Function) and self.sym == other.sym and self.params == other.params\n",
    "    \n",
    "    def __eq__(self, other):\n",
    "        return str(self) == str(other)\n",
    "    \n",
    "    def __hash__(self):\n",
    "        return hash(str(self))\n",
    "    \n",
    "    #Previous naming scheme testing. Not in use.\n",
    "    def name(self,s):\n",
    "        if sum([1 if i.sym==s else 0 for i in Function.registry])>0:\n",
    "            return self.name(s + \".\")\n",
    "        else: return s\n",
    "    \n",
    "    #For each parameter (0 to arity), scans forward for repeated terms. Any repeats are replaced by Repeats.\n",
    "    #Then reduces size of each parameter.\n",
    "    def reduceSize(self):\n",
    "        for i in xrange(len(self.params)):\n",
    "            for j in xrange(i+1, len(self.params)):\n",
    "                if not isinstance(self.params[j], Repeat) and self.params[i] == self.params[j]:\n",
    "                    self.params[j] = Repeat(self.params[j])\n",
    "        for i in self.params:\n",
    "            i.reduceSize()\n",
    "    \n",
    "    #Scans each parameter. If any are not ground, the entire instance of the function is not ground.\n",
    "    def isGround(self):\n",
    "        for i in self.params:\n",
    "            if not i.isGround():\n",
    "                return False\n",
    "        return True\n",
    "    \n",
    "    #Scans each parameter. Finds variables in each parameter and adds all of them to the list.\n",
    "    def findVariables(self):\n",
    "        variables = []\n",
    "        for i in self.params:\n",
    "            variables = variables + i.findVariables()\n",
    "        return variables\n",
    "    \n",
    "    #Scans each parameter. Finds constants in each parameter and adds all of them to the list.\n",
    "    def findConstants(self):\n",
    "        constants = []\n",
    "        for i in self.params:\n",
    "            constants = constants + i.findConstants()\n",
    "        return constants\n",
    "    \n",
    "    #Scans each parameter. Finds repeats in each parameter and adds all of them to the list.\n",
    "    def findRepeats(self):\n",
    "        repeats = []\n",
    "        for i in self.params:\n",
    "            repeats = repeats + i.findRepeats()\n",
    "        if self.isGround():\n",
    "            repeats.append(self)\n",
    "        return repeats\n",
    "    \n",
    "    #Is inherently a function. Finds functions in each parameter and adds all of them to the list.\n",
    "    def findFunctions(self):\n",
    "        functions = [self]\n",
    "        for i in self.params:\n",
    "            functions = functions + i.findFunctions()\n",
    "        return functions\n",
    "    \n",
    "    #Returns a copy of the predicate with 'var' replaced with 'rpt'.\n",
    "    #Should not need to copy, because it was done by the clause.\n",
    "    def replace(self, var, rpt):\n",
    "        #function = deepcopy(self)\n",
    "        function = self\n",
    "        for i in xrange(len(function.params)):\n",
    "            term = function.params[i]\n",
    "            if term==var:\n",
    "                function.params[i] = rpt\n",
    "            else:\n",
    "                function.params[i] = term.replace(var, rpt)\n",
    "        return function\n",
    "\n",
    "print \"Function structure loaded.\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Predicate structure loaded.\n"
     ]
    }
   ],
   "source": [
    "#Implementation of predicate (very similar implementation to function). \n",
    "#Includes symbol (must be unique) and list of paramaters.\n",
    "#Registry containts copies of all functions that may be altered in enumerate algorithm.\n",
    "#Overrides str, len, eq, and hash\n",
    "class Predicate:\n",
    "    \n",
    "    #Length calculated by definition: 1 + length of each parameter.\n",
    "    def __init__(self, s, *args):\n",
    "        self.sym = s\n",
    "        self.params = list(args)\n",
    "        self.length = 1+sum([len(i) for i in self.params])\n",
    "       \n",
    "    def __str__(self):\n",
    "        toReturn = self.sym + \"(\"\n",
    "        for i in self.params:\n",
    "            toReturn += str(i) + \",\"\n",
    "        toReturn = toReturn[:-1] + \")\"\n",
    "        return toReturn\n",
    "    \n",
    "    def __len__(self):\n",
    "        return 1+sum([len(i) for i in self.params])\n",
    "    \n",
    "    #def __eq__(self, other):\n",
    "    #    return isinstance(other, Predicate) and self.params == other.params\n",
    " \n",
    "    def __eq__(self, other):\n",
    "        return str(self) == str(other)\n",
    "    \n",
    "    def __hash__(self):\n",
    "        return hash(str(self))\n",
    "    \n",
    "    #Previous naming scheme testing. Not in use.\n",
    "    def name(self,s):\n",
    "        if sum([1 if i.sym==s else 0 for i in Function.registry])>0:\n",
    "            return self.name(s + \".\")\n",
    "        else: return s\n",
    "    \n",
    "    #For each parameter (0 to arity), scans forward for repeated terms. Any repeats are replaced by Repeats.\n",
    "    #Then reduces size of each parameter.\n",
    "    def reduceSize(self):\n",
    "        for i in xrange(len(self.params)):\n",
    "            for j in xrange(i+1, len(self.params)):\n",
    "                if not isinstance(self.params[j], Repeat) and self.params[i] == self.params[j]:\n",
    "                    self.params[j] = Repeat(self.params[j])\n",
    "        for i in self.params:\n",
    "            i.reduceSize()\n",
    "            \n",
    "    #Scans each parameter. If any are not ground, the entire instance of the function is not ground.\n",
    "    def isGround(self):\n",
    "        for i in self.params:\n",
    "            if not i.isGround():\n",
    "                return False\n",
    "        return True\n",
    "    \n",
    "    #Scans each parameter. Finds variables in each parameter and adds all of them to the list.\n",
    "    def findVariables(self):\n",
    "        variables = []\n",
    "        for i in self.params:\n",
    "            variables = variables + i.findVariables()\n",
    "        return variables\n",
    "    \n",
    "    #Scans each parameter. Finds constants in each parameter and adds all of them to the list.\n",
    "    def findConstants(self):\n",
    "        constants = []\n",
    "        for i in self.params:\n",
    "            constants = constants + i.findConstants()\n",
    "        return constants\n",
    "    \n",
    "    #Scans each parameter. Finds repeats in each parameter and adds all of them to the list.\n",
    "    def findRepeats(self):\n",
    "        repeats = []\n",
    "        for i in self.params:\n",
    "            repeats = repeats + i.findRepeats()\n",
    "        if self.isGround():\n",
    "            repeats.append(self)\n",
    "        return repeats\n",
    "    \n",
    "    #Scans each parameter. Finds functions in each parameter and adds all of them to the list.\n",
    "    def findFunctions(self):\n",
    "        functions = []\n",
    "        for i in self.params:\n",
    "            functions = functions + i.findFunctions()\n",
    "        return functions\n",
    "\n",
    "    #Returns a copy of the predicate with 'var' replaced with 'rpt'.\n",
    "    #Should not need to copy, because it was done by the clause.\n",
    "    def replace(self, var, rpt):\n",
    "        #predicate = deepcopy(self)\n",
    "        predicate = self\n",
    "        for i in xrange(len(predicate.params)):\n",
    "            term = predicate.params[i]\n",
    "            if term==var:\n",
    "                predicate.params[i] = rpt\n",
    "            else:\n",
    "                predicate.params[i] = term.replace(var, rpt)\n",
    "        return predicate\n",
    "    \n",
    "print \"Predicate structure loaded.\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Clause structure loaded.\n"
     ]
    }
   ],
   "source": [
    "#Implementation of clause (very similar implementation to function and predicate). \n",
    "#Includes list of paramaters.\n",
    "#Registry containts copies of all functions that may be altered in enumerate algorithm.\n",
    "#Overrides str, len, eq, and hash\n",
    "class Clause: \n",
    "    \n",
    "    #Length calculated by definition: sum of length of each parameter.\n",
    "    def __init__(self, *args):\n",
    "        self.params = list(args)\n",
    "        self.length = sum([len(i) for i in self.params])\n",
    "        \n",
    "    def __str__(self):\n",
    "        toReturn = \"{\"\n",
    "        for i in self.params:\n",
    "            toReturn += str(i) + \",\"\n",
    "        toReturn = toReturn[:-1] + \"}\"\n",
    "        return toReturn\n",
    "    \n",
    "    def __len__(self):\n",
    "        return sum([len(i) for i in self.params])\n",
    "    \n",
    "    #def __eq__(self, other):\n",
    "    #    return isinstance(other, Clause) and self.params == other.params\n",
    "    \n",
    "    def __eq__(self, other):\n",
    "        return str(self) == str(other)\n",
    "\n",
    "    def __hash__(self):\n",
    "        return hash(str(self))\n",
    "    \n",
    "    #For each parameter (0 to arity), scans forward for repeated terms. Any repeats are replaced by Repeats.\n",
    "    #Then reduces size of each parameter. Returns new modified clause.\n",
    "    def reduceSize(self):\n",
    "        copy = deepcopy(self)\n",
    "        for i in xrange(len(copy.params)):\n",
    "            for j in xrange(i+1, len(copy.params)):\n",
    "                if not isinstance(copy.params[j], Repeat) and copy.params[i] == copy.params[j]:\n",
    "                    copy.params[j] = Repeat(copy.params[j])\n",
    "        for i in copy.params:\n",
    "            i.reduceSize()    \n",
    "        return copy\n",
    "    \n",
    "    #Scans each parameter. If any are not ground, the entire instance of the function is not ground.\n",
    "    def isGround(self):\n",
    "        for i in self.params:\n",
    "            if not i.isGround():\n",
    "                return False\n",
    "        return True\n",
    "    \n",
    "    #Scans each parameter. Finds variables in each parameter and adds all of them to the list.\n",
    "    def findVariables(self):\n",
    "        variables = []\n",
    "        for i in self.params:\n",
    "            variables = variables + i.findVariables()\n",
    "        return variables\n",
    "    \n",
    "    #Scans each parameter. Finds constants in each parameter and adds all of them to the list.\n",
    "    #Herbrand structures require at least one constant. If there are no constants, one arbitrary constant 'C' is added.\n",
    "    def findConstants(self):\n",
    "        constants = []\n",
    "        for i in self.params:\n",
    "            constants = constants + i.findConstants()\n",
    "        if not constants:\n",
    "            constants.append(Constant('C'))\n",
    "        return constants\n",
    "    \n",
    "    #Scans each parameter. Finds repeats in each parameter and adds all of them to the list.\n",
    "    #Unlike other structures, does not include itself.\n",
    "    def findRepeats(self):\n",
    "        repeats = []\n",
    "        for i in self.params:\n",
    "            repeats = repeats + i.findRepeats()\n",
    "        return repeats\n",
    "    \n",
    "    #Scans each parameter. Finds functions in each parameter and adds all of them to the list.\n",
    "    def findFunctions(self):\n",
    "        functions = []\n",
    "        for i in self.params:\n",
    "            functions = functions + i.findFunctions()\n",
    "        return functions\n",
    "    \n",
    "    #Returns a copy of the clause with 'var' replaced with 'rpt' to be used in deeper levels of recursion.\n",
    "    def replace(self, var, rpt):\n",
    "        clause = deepcopy(self)\n",
    "        for i in xrange(len(clause.params)):\n",
    "            term = clause.params[i]\n",
    "            if term==var:\n",
    "                clause.params[i] = rpt\n",
    "            else:\n",
    "                clause.params[i] = term.replace(var, rpt)\n",
    "        return clause\n",
    "    \n",
    "print \"Clause structure loaded.\""
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<h2>The Algorithm</h2>\n",
    "<p>Given a clause, enumerates all ground clauses whose size is less than some size bound.</p>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "\"\"\"\n",
    "Function:\n",
    "    enumerateClauses\n",
    "    \n",
    "Use:\n",
    "    Given a clause and sizebound, enumerates all ground clauses whose s_dag - calculated by len(reduceSize()) -\n",
    "    is less than the desired sizebound These results can then be fed into a DPLL implementation to determine\n",
    "    satisfiability. \n",
    "\n",
    "Inputs:\n",
    "    clause (Clause): The desired clause for ground instances under a sizebound to be enumerated from.\n",
    "    size (int): The sizebound. Conventionally compared to s_lin. Compared to s_dag here.\n",
    "    rpts (set): The set of repeats. Is empty to start, used within algorithm. Do not pass anything here.\n",
    "    clauseSet (set): The set of clauses that are both ground and under the sizebound. \n",
    "                     Is empty to start, used within algorithm. Do not pass anything here.\n",
    "    \n",
    "Output:\n",
    "    clauseSet (set): The set of clauses that are both ground and under the sizebound after the terminating condition.\n",
    "    \n",
    "Helper Functions:\n",
    "    hyperizefunctions: \n",
    "                        Returns a copy of a function with all terms replaced by new variables.\n",
    "                        Inputs: \n",
    "                            functions (set): a set of functions.\n",
    "                        Outputs:\n",
    "                            hyfunctions (set): the same set of functions with all terms replaced with variables.\n",
    "    \n",
    "\"\"\"\n",
    "       \n",
    "def enumerateClauses(clause, size, rpts = set(), clauseSet = set()):\n",
    "    \n",
    "    #Reduced clause length. Calculation often, so we'll store it once.\n",
    "    clauseReducedSize = len(clause.reduceSize())\n",
    "    \n",
    "    #Create an effective closure around repeats, (potentially) growing and shrinking with recursion depth.\n",
    "    repeats = rpts.union(set(clause.findRepeats()))\n",
    "    \n",
    "    #Base Case: Clause size is larger than size bound. Does nothing to clauseSet and returns.\n",
    "    if clauseReducedSize>size:\n",
    "        return clauseSet\n",
    "    \n",
    "    #Base Case: The clause is ground. Add it to clauseSet and return.\n",
    "    elif clause.isGround():\n",
    "        clauseSet.add(clause)\n",
    "\n",
    "    #Case 1: The clause has reached the sizebound, but is not ground. Recursively call enumerateClauses with only\n",
    "    #terms of size 0 - repeats.\n",
    "    elif clauseReducedSize==size:\n",
    "        for x in clause.findVariables():\n",
    "            for i in repeats:\n",
    "                enumerateClauses(clause.replace(x,i), size, repeats, clauseSet)\n",
    "                \n",
    "    #Case 2: The clause has not reached the sizebound and is not ground. Recursively call enumerateClauses with\n",
    "    #any possible goal-oriented term - constants, functions, or repeats.\n",
    "    else:\n",
    "        constants = set(clause.findConstants())\n",
    "        variables = set(clause.findVariables())\n",
    "        functions = hyperizefunctions(clause.findFunctions())\n",
    "        for x in variables:\n",
    "            for i in constants.union(repeats).union(functions):\n",
    "                #Branch-and-bound approach to cut unnecessary enumerateClauses calls.\n",
    "                #If the size of the term to be replaced is larger than the available space left, don't bother checking.\n",
    "                if (size-clauseReducedSize-len(i))>=0:\n",
    "                    enumerateClauses(clause.replace(x,i), size, repeats, clauseSet)\n",
    "\n",
    "    return clauseSet\n",
    "    \n",
    "def hyperizefunctions(functions):\n",
    "    hyfunctions = set()\n",
    "    for fn in functions:\n",
    "        hyperfn = deepcopy(fn)\n",
    "        for i in xrange(len(hyperfn.params)):\n",
    "            hyperfn.params[i] = Variable()\n",
    "        hyfunctions.add(hyperfn)\n",
    "    return hyfunctions"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<h2>Testing Zone</h2>\n",
    "<p>Instantiates some structures then runs the algorithm.</p>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {
    "collapsed": false,
    "scrolled": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{f(a,a,a,a,b)}\n",
      "{f(a,b,a,a,b)}\n",
      "{f(a,b,b,a,b)}\n",
      "{f(a,a,a,b,b)}\n",
      "{f(a,a,b,b,b)}\n",
      "{f(a,b,b,b,b)}\n",
      "{f(a,b,a,b,b)}\n",
      "{f(a,a,b,a,b)}\n"
     ]
    }
   ],
   "source": [
    "a = Constant('a')\n",
    "b = Constant('b')\n",
    "c = Constant('c')\n",
    "x = Variable('x')\n",
    "y = Variable('y')\n",
    "z = Variable('z')\n",
    "f1 = Function('f', a, z, x, y, b)\n",
    "f2 = Function('f', a, x)\n",
    "g1 = Function('g', b, x)\n",
    "g2 = Function('g', b, f1)\n",
    "g3 = Function('g', c, f1)\n",
    "p1 = Predicate('P',f1, f2, g2, g3)\n",
    "p2 = Predicate('Q', f1)\n",
    "p3 = Predicate('R', f1, g3)\n",
    "c1 = Clause(p1, p2, p3)\n",
    "c2 = Clause(f1)\n",
    "\n",
    "for i in enumerateClauses(c2, 4):\n",
    "    print i\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true
   },
   "source": [
    "Todo: \n",
    "    Comment everything, \n",
    "    Follow FOL statement through steps before DPLL, \n",
    "    Test on some problems (pelletier), \n",
    "    Look for efficiency improvements??"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 2",
   "language": "python",
   "name": "python2"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 2
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython2",
   "version": "2.7.12"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 0
}