/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Mudathir Mohamed, Andrew Reynolds
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Black box testing of the guards of the Java API functions.
 */

package tests;
import static io.github.cvc5.Kind.*;
import static org.junit.jupiter.api.Assertions.*;

import io.github.cvc5.*;
import java.util.Arrays;
import org.junit.jupiter.api.AfterEach;
import org.junit.jupiter.api.BeforeEach;
import org.junit.jupiter.api.Test;

class GrammarTest
{
  private TermManager d_tm;
  private Solver d_solver;

  @BeforeEach
  void setUp()
  {
    d_tm = new TermManager();
    d_solver = new Solver(d_tm);
  }

  @AfterEach
  void tearDown()
  {
    Context.deletePointers();
  }

  @Test
  void testToString()
  {
    d_solver.setOption("sygus", "true");
    Sort bool = d_tm.getBooleanSort();
    Term start = d_tm.mkVar(bool);
    Grammar g = d_solver.mkGrammar(new Term[] {}, new Term[] {start});
    assertFalse(g.isNull());
    g.addRule(start, d_tm.mkBoolean(false));
    g.toString();
  }

  @Test
  void addRule()
  {
    d_solver.setOption("sygus", "true");
    Sort bool = d_tm.getBooleanSort();
    Sort integer = d_tm.getIntegerSort();

    Term nullTerm = new Term();
    Term start = d_tm.mkVar(bool);
    Term nts = d_tm.mkVar(bool);

    Grammar g = d_solver.mkGrammar(new Term[] {}, new Term[] {start});

    assertDoesNotThrow(() -> g.addRule(start, d_tm.mkBoolean(false)));

    assertThrows(CVC5ApiException.class, () -> g.addRule(nullTerm, d_tm.mkBoolean(false)));
    assertThrows(CVC5ApiException.class, () -> g.addRule(start, nullTerm));
    assertThrows(CVC5ApiException.class, () -> g.addRule(nts, d_tm.mkBoolean(false)));
    assertThrows(CVC5ApiException.class, () -> g.addRule(start, d_tm.mkInteger(0)));

    d_solver.synthFun("f", new Term[] {}, bool, g);

    assertThrows(CVC5ApiException.class, () -> g.addRule(start, d_tm.mkBoolean(false)));
  }

  @Test
  void addRules()
  {
    d_solver.setOption("sygus", "true");
    Sort bool = d_tm.getBooleanSort();
    Sort integer = d_tm.getIntegerSort();

    Term nullTerm = new Term();
    Term start = d_tm.mkVar(bool);
    Term nts = d_tm.mkVar(bool);

    Grammar g = d_solver.mkGrammar(new Term[] {}, new Term[] {start});

    assertDoesNotThrow(() -> g.addRules(start, new Term[] {d_tm.mkBoolean(false)}));

    assertThrows(
        CVC5ApiException.class, () -> g.addRules(nullTerm, new Term[] {d_tm.mkBoolean(false)}));
    assertThrows(CVC5ApiException.class, () -> g.addRules(start, new Term[] {nullTerm}));
    assertThrows(CVC5ApiException.class, () -> g.addRules(nts, new Term[] {d_tm.mkBoolean(false)}));
    assertThrows(CVC5ApiException.class, () -> g.addRules(start, new Term[] {d_tm.mkInteger(0)}));

    d_solver.synthFun("f", new Term[] {}, bool, g);

    assertThrows(
        CVC5ApiException.class, () -> g.addRules(start, new Term[] {d_tm.mkBoolean(false)}));
  }

  @Test
  void addAnyConstant()
  {
    d_solver.setOption("sygus", "true");
    Sort bool = d_tm.getBooleanSort();

    Term nullTerm = new Term();
    Term start = d_tm.mkVar(bool);
    Term nts = d_tm.mkVar(bool);

    Grammar g = d_solver.mkGrammar(new Term[] {}, new Term[] {start});

    assertDoesNotThrow(() -> g.addAnyConstant(start));
    assertDoesNotThrow(() -> g.addAnyConstant(start));

    assertThrows(CVC5ApiException.class, () -> g.addAnyConstant(nullTerm));
    assertThrows(CVC5ApiException.class, () -> g.addAnyConstant(nts));

    d_solver.synthFun("f", new Term[] {}, bool, g);

    assertThrows(CVC5ApiException.class, () -> g.addAnyConstant(start));
  }

  @Test
  void addAnyVariable()
  {
    d_solver.setOption("sygus", "true");
    Sort bool = d_tm.getBooleanSort();

    Term nullTerm = new Term();
    Term x = d_tm.mkVar(bool);
    Term start = d_tm.mkVar(bool);
    Term nts = d_tm.mkVar(bool);

    Grammar g1 = d_solver.mkGrammar(new Term[] {x}, new Term[] {start});
    Grammar g2 = d_solver.mkGrammar(new Term[] {}, new Term[] {start});

    assertDoesNotThrow(() -> g1.addAnyVariable(start));
    assertDoesNotThrow(() -> g1.addAnyVariable(start));
    assertDoesNotThrow(() -> g2.addAnyVariable(start));

    assertThrows(CVC5ApiException.class, () -> g1.addAnyVariable(nullTerm));
    assertThrows(CVC5ApiException.class, () -> g1.addAnyVariable(nts));

    d_solver.synthFun("f", new Term[] {}, bool, g1);

    assertThrows(CVC5ApiException.class, () -> g1.addAnyVariable(start));
  }

  @Test
  void equalHash()
  {
    d_solver.setOption("sygus", "true");

    Sort bool = d_tm.getBooleanSort();
    Term x = d_tm.mkVar(bool, "x");
    Term start1 = d_tm.mkVar(bool, "start");
    Term start2 = d_tm.mkVar(bool, "start");
    Grammar g1, g2;

    {
      g1 = d_solver.mkGrammar(new Term[] {}, new Term[] {start1});
      g2 = d_solver.mkGrammar(new Term[] {}, new Term[] {start1});
      assertEquals(g1.hashCode(), g1.hashCode());
      assertEquals(g1.hashCode(), g2.hashCode());
      assertTrue(g1.equals(g1));
      assertFalse(g1.equals(g2));
    }

    {
      g1 = d_solver.mkGrammar(new Term[] {}, new Term[] {start1});
      g2 = d_solver.mkGrammar(new Term[] {x}, new Term[] {start1});
      assertNotEquals(g1.hashCode(), g2.hashCode());
      assertTrue(g1.equals(g1));
      assertFalse(g1.equals(g2));
    }

    {
      g1 = d_solver.mkGrammar(new Term[] {x}, new Term[] {start1});
      g2 = d_solver.mkGrammar(new Term[] {x}, new Term[] {start2});
      assertNotEquals(g1.hashCode(), g2.hashCode());
      assertTrue(g1.equals(g1));
      assertFalse(g1.equals(g2));
    }

    {
      g1 = d_solver.mkGrammar(new Term[] {x}, new Term[] {start1});
      g2 = d_solver.mkGrammar(new Term[] {x}, new Term[] {start1});
      g2.addAnyVariable(start1);
      assertNotEquals(g1.hashCode(), g2.hashCode());
      assertTrue(g1.equals(g1));
      assertFalse(g1.equals(g2));
    }

    {
      g1 = d_solver.mkGrammar(new Term[] {x}, new Term[] {start1});
      g2 = d_solver.mkGrammar(new Term[] {x}, new Term[] {start1});
      Term[] rules = new Term[] {d_tm.mkFalse()};
      g1.addRules(start1, rules);
      g2.addRules(start1, rules);
      assertEquals(g1.hashCode(), g2.hashCode());
      assertTrue(g1.equals(g1));
      assertFalse(g1.equals(g2));
    }

    {
      g1 = d_solver.mkGrammar(new Term[] {x}, new Term[] {start1});
      g2 = d_solver.mkGrammar(new Term[] {x}, new Term[] {start1});
      Term[] rules2 = new Term[] {d_tm.mkFalse()};
      g2.addRules(start1, rules2);
      assertNotEquals(g1.hashCode(), g2.hashCode());
      assertTrue(g1.equals(g1));
      assertFalse(g1.equals(g2));
    }

    {
      g1 = d_solver.mkGrammar(new Term[] {x}, new Term[] {start1});
      g2 = d_solver.mkGrammar(new Term[] {x}, new Term[] {start1});
      Term[] rules1 = new Term[] {d_tm.mkTrue()};
      Term[] rules2 = new Term[] {d_tm.mkFalse()};
      g1.addRules(start1, rules1);
      g2.addRules(start1, rules2);
      assertNotEquals(g1.hashCode(), g2.hashCode());
      assertTrue(g1.equals(g1));
      assertFalse(g1.equals(g2));
    }
  }
}