<commit_before>package leo.modules.encoding

import leo.LeoTestSuite
import leo.datastructures.{Term, Type, Signature}
import leo.modules.Parsing

/**
  * Checks whether the [[leo.modules.encoding.Monotonicity]] inference rules work as expected.
  *
  * @see [[leo.modules.encoding.BBPS]] -- the calculus tested here.
  */
class MonotonicityTest extends LeoTestSuite {
  test("Monkey Village (Ex. 1)") {
    implicit val sig: Signature = getFreshSignature
    import leo.modules.HOLSignature.o
    import leo.modules.calculus.{FullCNF => CNF, freshVarGenFromBlank => vargen}
    import leo.modules.Utility.termToClause

    // New types
    val monkey = Type.mkType(sig.addBaseType("monkey"))
    val banana = Type.mkType(sig.addBaseType("banana"))

    // Introduced symbols to signature
    sig.addUninterpreted("owns", Type.mkFunType(Seq(monkey, banana, o)))
    sig.addUninterpreted("b1", Type.mkFunType(monkey, banana))
    sig.addUninterpreted("b2", Type.mkFunType(monkey, banana))

    // create formulae
    val f1 = Parsing.parseThf("! [M: monkey]: ((owns @ M @ (b1 @ M)) & (owns @ M @ (b2 @ M)))")
    val f2 = Parsing.parseThf("! [M: monkey]: ((b1 @ M) != (b2 @ M))")
    val f3 = Parsing.parseThf("! [M1: monkey, M2: monkey, B: banana]:" +
      " (((owns @ M1 @ B) & (owns @ M2 @ B)) => (M1 = M2))")

    assert(Term.wellTyped(f1))
    assert(Term.wellTyped(f2))
    assert(Term.wellTyped(f3))

    // calculate CNF
    val cnf = CNF(vargen, termToClause(f1)).toSet union CNF(vargen, termToClause(f2)).toSet union CNF(vargen, termToClause(f3)).toSet

    // infinite types
    val infTypes: Set[Type] = Set.empty // none known

    // test monotonicity check
    assert(BBPS.monotone(banana ,cnf, infTypes))
    assert(!BBPS.monotone(monkey ,cnf, infTypes))
    assert(!BBPS.monotone(cnf, infTypes))
  }
}<commit_msg>adde monotonicity check to checked tests<commit_after>package leo.modules.encoding

import leo.{Checked, LeoTestSuite}
import leo.datastructures.{Signature, Term, Type}
import leo.modules.Parsing

/**
  * Checks whether the [[leo.modules.encoding.Monotonicity]] inference rules work as expected.
  *
  * @see [[leo.modules.encoding.BBPS]] -- the calculus tested here.
  */
class MonotonicityTest extends LeoTestSuite {
  test("Monkey Village (Ex. 1)", Checked) {
    implicit val sig: Signature = getFreshSignature
    import leo.modules.HOLSignature.o
    import leo.modules.calculus.{FullCNF => CNF, freshVarGenFromBlank => vargen}
    import leo.modules.Utility.termToClause

    // New types
    val monkey = Type.mkType(sig.addBaseType("monkey"))
    val banana = Type.mkType(sig.addBaseType("banana"))

    // Introduced symbols to signature
    sig.addUninterpreted("owns", Type.mkFunType(Seq(monkey, banana, o)))
    sig.addUninterpreted("b1", Type.mkFunType(monkey, banana))
    sig.addUninterpreted("b2", Type.mkFunType(monkey, banana))

    // create formulae
    val f1 = Parsing.parseThf("! [M: monkey]: ((owns @ M @ (b1 @ M)) & (owns @ M @ (b2 @ M)))")
    val f2 = Parsing.parseThf("! [M: monkey]: ((b1 @ M) != (b2 @ M))")
    val f3 = Parsing.parseThf("! [M1: monkey, M2: monkey, B: banana]:" +
      " (((owns @ M1 @ B) & (owns @ M2 @ B)) => (M1 = M2))")

    assert(Term.wellTyped(f1))
    assert(Term.wellTyped(f2))
    assert(Term.wellTyped(f3))

    // calculate CNF
    val cnf = CNF(vargen, termToClause(f1)).toSet union CNF(vargen, termToClause(f2)).toSet union CNF(vargen, termToClause(f3)).toSet

    // infinite types
    val infTypes: Set[Type] = Set.empty // none known

    // test monotonicity check
    assert(BBPS.monotone(banana, cnf, infTypes))
    assert(!BBPS.monotone(monkey, cnf, infTypes))
    assert(!BBPS.monotone(cnf, infTypes))
  }
}
{'fraction_non_alphanumeric': 0.15268411114108443, 'fraction_numerical': 0.011869436201780416, 'mean_word_length': 3.753846153846154, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 9, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2766358', 'n_tokens_mistral': 1388, 'n_tokens_neox': 1337, 'n_words': 295}