{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Init Plugin\n",
      "Init Graph Optimizer\n",
      "Init Kernel\n"
     ]
    }
   ],
   "source": [
    "import logging; logging.basicConfig(level=logging.INFO)\n",
    "import tensorflow as tf\n",
    "import numpy as np\n",
    "import ltn"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [],
   "source": [
    "a = ltn.Proposition(0.2,trainable=True)\n",
    "b = ltn.Proposition(0.5,trainable=True)\n",
    "c = ltn.Proposition(0.5,trainable=True)\n",
    "d = ltn.Proposition(0.3, trainable=False)\n",
    "e = ltn.Proposition(0.9, trainable=False)\n",
    "\n",
    "x = ltn.Variable(\"x\", np.array([[1,2],[3,4],[5,6]]))\n",
    "P = ltn.Predicate.MLP(input_shapes=[(2)])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [],
   "source": [
    "Not = ltn.Wrapper_Connective(ltn.fuzzy_ops.Not_Std())\n",
    "And = ltn.Wrapper_Connective(ltn.fuzzy_ops.And_Prod())\n",
    "Or = ltn.Wrapper_Connective(ltn.fuzzy_ops.Or_ProbSum())\n",
    "Implies = ltn.Wrapper_Connective(ltn.fuzzy_ops.Implies_Reichenbach())\n",
    "Forall = ltn.Wrapper_Quantifier(ltn.fuzzy_ops.Aggreg_pMeanError(p=5),semantics=\"forall\")\n",
    "Exists = ltn.Wrapper_Quantifier(ltn.fuzzy_ops.Aggreg_pMean(p=10),semantics=\"exists\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [],
   "source": [
    "formula_aggregator = ltn.Wrapper_Formula_Aggregator(ltn.fuzzy_ops.Aggreg_Mean())\n",
    "\n",
    "@tf.function\n",
    "def axioms():\n",
    "    axioms = [\n",
    "        # [ (A and B and (forall x: P(x))) -> Not C ] and C\n",
    "        And(\n",
    "            Implies(And(And(a,b),Forall(x,P(x))),\n",
    "                    Not(c)),\n",
    "            c\n",
    "        ),\n",
    "        # w1 -> (forall x: P(x))\n",
    "        Implies(w1, Forall(x,P(x))),\n",
    "        # w2 -> (Exists x: P(x))\n",
    "        Implies(w2, Exists(x,P(x)))\n",
    "    ]\n",
    "    sat_level = formula_aggregator(axioms).tensor\n",
    "    return sat_level"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "2021-08-30 16:52:58.075369: I tensorflow/compiler/mlir/mlir_graph_optimization_pass.cc:176] None of the MLIR Optimization Passes are enabled (registered 2)\n",
      "2021-08-30 16:52:58.076456: W tensorflow/core/platform/profile_utils/cpu_utils.cc:128] Failed to get CPU frequency: 0 Hz\n",
      "2021-08-30 16:52:58.076523: I tensorflow/core/grappler/optimizers/custom_graph_optimizer_registry.cc:112] Plugin optimizer for device_type GPU is enabled.\n",
      "2021-08-30 16:52:58.139682: I tensorflow/core/grappler/optimizers/custom_graph_optimizer_registry.cc:112] Plugin optimizer for device_type GPU is enabled.\n",
      "2021-08-30 16:52:58.307572: I tensorflow/core/grappler/optimizers/custom_graph_optimizer_registry.cc:112] Plugin optimizer for device_type GPU is enabled.\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Epoch 0: Sat Level 0.783\n",
      "Epoch 100: Sat Level 0.879\n",
      "Epoch 200: Sat Level 0.952\n",
      "Epoch 300: Sat Level 0.956\n",
      "Epoch 400: Sat Level 0.956\n",
      "Epoch 500: Sat Level 0.956\n",
      "Epoch 600: Sat Level 0.956\n",
      "Epoch 700: Sat Level 0.956\n",
      "Epoch 800: Sat Level 0.956\n",
      "Epoch 900: Sat Level 0.956\n",
      "Training finished at Epoch 999 with Sat Level 0.956\n"
     ]
    }
   ],
   "source": [
    "trainable_variables = ltn.as_tensors([a,b,c])\n",
    "optimizer = tf.keras.optimizers.SGD(learning_rate=0.01)\n",
    "\n",
    "for epoch in range(1000):\n",
    "    with tf.GradientTape() as tape:\n",
    "        loss_value = 1. - axioms()\n",
    "    grads = tape.gradient(loss_value, trainable_variables)\n",
    "    optimizer.apply_gradients(zip(grads, trainable_variables))\n",
    "    if epoch%100 == 0:\n",
    "        print(\"Epoch %d: Sat Level %.3f\"%(epoch, axioms()))\n",
    "print(\"Training finished at Epoch %d with Sat Level %.3f\"%(epoch, axioms()))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "interpreter": {
   "hash": "889985fd10eb245a43f2ae5f5aa0c555254f5b898fe16071f1c89d06fa8d76a2"
  },
  "kernelspec": {
   "display_name": "Python 3.9.6 64-bit ('tf-py39': conda)",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.9.6"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}