<commit_before>// vim:filetype=cpp:textwidth=80:shiftwidth=2:softtabstop=2:expandtab
// Copyright 2014 <EMAIL>

#include <gtest/gtest.h>
#include <./ecai2014.h>
#include <./kr2014.h>
#include <./formula.h>

using namespace esbl;
using namespace bats;

TEST(formula, gl) {
  Kr2014 bat;
  auto& s = bat.setup();
  auto close = Formula::Or(Formula::Lit(Literal({}, true, bat.d0, {})),
                           Formula::Lit(Literal({}, true, bat.d1, {})));
  auto maybe_close = Formula::Or(Formula::Lit(Literal({}, true, bat.d1, {})),
                                 Formula::Lit(Literal({}, true, bat.d2, {})));

  // Property 1
  EXPECT_TRUE(Formula::Neg(close->Copy())->EntailedBy(&bat.tf(), &s, 0));

  s.AddSensingResult({}, bat.forward, true);

  // Property 2
  EXPECT_FALSE(Formula::Act(bat.forward, maybe_close->Copy())->EntailedBy(&bat.tf(), &s, 0));

  // Property 3
  EXPECT_TRUE(Formula::Act(bat.forward, maybe_close->Copy())->EntailedBy(&bat.tf(), &s, 1));

  s.AddSensingResult({bat.forward}, bat.sonar, true);

  // Property 4
  EXPECT_TRUE(Formula::Act({bat.forward, bat.sonar}, close->Copy())->EntailedBy(&bat.tf(), &s, 1));
}

TEST(formula, gl_regression) {
  Kr2014 bat;
  auto& s = bat.setup();
  auto close = Formula::Or(Formula::Lit(Literal({}, true, bat.d0, {})),
                           Formula::Lit(Literal({}, true, bat.d1, {})));
  auto maybe_close = Formula::Or(Formula::Lit(Literal({}, true, bat.d1, {})),
                                 Formula::Lit(Literal({}, true, bat.d2, {})));

  // Property 1
  Maybe<Formula::Ptr> reg1 = Formula::Neg(close->Copy())->Regress(&bat.tf(), bat);
  EXPECT_TRUE(reg1);
  EXPECT_TRUE(reg1.val->EntailedBy(&bat.tf(), &s, 0));

  s.AddSensingResult({}, bat.forward, true);

  // Property 2
  Maybe<Formula::Ptr> reg2 = Formula::Act(bat.forward, maybe_close->Copy())->Regress(&bat.tf(), bat);
  EXPECT_TRUE(reg2);
  //EXPECT_FALSE(reg2.val->EntailedBy(&bat.tf(), &s, 0)); // here regression differs from ESL
  EXPECT_TRUE(reg2.val->EntailedBy(&bat.tf(), &s, 0));

  // Property 3
  Maybe<Formula::Ptr> reg3 = Formula::Act(bat.forward, maybe_close->Copy())->Regress(&bat.tf(), bat);
  EXPECT_TRUE(reg3);
  EXPECT_TRUE(reg3.val->EntailedBy(&bat.tf(), &s, 1));

  s.AddSensingResult({bat.forward}, bat.sonar, true);

  // Property 4
  Maybe<Formula::Ptr> reg4 = Formula::Act({bat.forward, bat.sonar}, close->Copy())->Regress(&bat.tf(), bat);
  EXPECT_TRUE(reg4);
  EXPECT_TRUE(reg4.val->EntailedBy(&bat.tf(), &s, 1));
}

TEST(formula, morri) {
  constexpr Setups::split_level k = 2;
  Ecai2014 bat(k);
  auto& s = bat.setups();

  // Property 1
  EXPECT_TRUE(Formula::Lit(Literal({}, false, bat.L1, {}))->EntailedBy(&bat.tf(), &s, 2));

  // Property 2
  s.AddSensingResult({}, bat.SL, true);
  EXPECT_TRUE(Formula::Act(bat.SL, Formula::And(Formula::Lit(Literal({}, true, bat.L1, {})),
                                                Formula::Lit(Literal({}, true, bat.R1, {}))))->EntailedBy(&bat.tf(), &s, 2));

  // Property 3
  s.AddSensingResult({bat.SL}, bat.SR1, false);
  EXPECT_TRUE(Formula::Act({bat.SL, bat.SR1}, Formula::Neg(Formula::Lit(Literal({}, true, bat.R1, {}))))->EntailedBy(&bat.tf(), &s, 2));

  // Property 5
  EXPECT_FALSE(Formula::Act({bat.SL, bat.SR1}, Formula::Lit(Literal({}, true, bat.L1, {})))->EntailedBy(&bat.tf(), &s, 2));
  EXPECT_FALSE(Formula::Neg(Formula::Act({bat.SL, bat.SR1}, Formula::Lit(Literal({}, true, bat.L1, {}))))->EntailedBy(&bat.tf(), &s, 2));

  // Property 6
  EXPECT_TRUE(Formula::Act({bat.SL, bat.SR1, bat.LV}, Formula::Lit(Literal({}, true, bat.R1, {})))->EntailedBy(&bat.tf(), &s, 2));

  // Property 6
  s.AddSensingResult({bat.SL,bat.SR1,bat.LV}, bat.SL, true);
  EXPECT_TRUE(Formula::Act({bat.SL, bat.SR1, bat.LV, bat.SL}, Formula::Lit(Literal({}, true, bat.L1, {})))->EntailedBy(&bat.tf(), &s, 2));
}

TEST(formula, fol_incompleteness_positive1) {<commit_msg>Added second unit test for regression.<commit_after>// vim:filetype=cpp:textwidth=80:shiftwidth=2:softtabstop=2:expandtab
// Copyright 2014 <EMAIL>

#include <gtest/gtest.h>
#include <./ecai2014.h>
#include <./kr2014.h>
#include <./formula.h>

using namespace esbl;
using namespace bats;

TEST(formula, gl) {
  Kr2014 bat;
  auto& s = bat.setup();
  auto close = Formula::Or(Formula::Lit(Literal({}, true, bat.d0, {})),
                           Formula::Lit(Literal({}, true, bat.d1, {})));
  auto maybe_close = Formula::Or(Formula::Lit(Literal({}, true, bat.d1, {})),
                                 Formula::Lit(Literal({}, true, bat.d2, {})));

  // Property 1
  EXPECT_TRUE(Formula::Neg(close->Copy())->EntailedBy(&bat.tf(), &s, 0));

  s.AddSensingResult({}, bat.forward, true);

  // Property 2
  EXPECT_FALSE(Formula::Act(bat.forward, maybe_close->Copy())->EntailedBy(&bat.tf(), &s, 0));

  // Property 3
  EXPECT_TRUE(Formula::Act(bat.forward, maybe_close->Copy())->EntailedBy(&bat.tf(), &s, 1));

  s.AddSensingResult({bat.forward}, bat.sonar, true);

  // Property 4
  EXPECT_TRUE(Formula::Act({bat.forward, bat.sonar}, close->Copy())->EntailedBy(&bat.tf(), &s, 1));
}

TEST(formula, gl_regression) {
  Kr2014 bat;
  auto& s = bat.setup();
  auto close = Formula::Or(Formula::Lit(Literal({}, true, bat.d0, {})),
                           Formula::Lit(Literal({}, true, bat.d1, {})));
  auto maybe_close = Formula::Or(Formula::Lit(Literal({}, true, bat.d1, {})),
                                 Formula::Lit(Literal({}, true, bat.d2, {})));

  // Property 1
  Maybe<Formula::Ptr> reg1 = Formula::Neg(close->Copy())->Regress(&bat.tf(), bat);
  EXPECT_TRUE(reg1);
  EXPECT_TRUE(reg1.val->EntailedBy(&bat.tf(), &s, 0));

  s.AddSensingResult({}, bat.forward, true);

  // Property 2
  Maybe<Formula::Ptr> reg2 = Formula::Act(bat.forward, maybe_close->Copy())->Regress(&bat.tf(), bat);
  EXPECT_TRUE(reg2);
  //EXPECT_FALSE(reg2.val->EntailedBy(&bat.tf(), &s, 0)); // here regression differs from ESL
  EXPECT_TRUE(reg2.val->EntailedBy(&bat.tf(), &s, 0));

  // Property 3
  Maybe<Formula::Ptr> reg3 = Formula::Act(bat.forward, maybe_close->Copy())->Regress(&bat.tf(), bat);
  EXPECT_TRUE(reg3);
  EXPECT_TRUE(reg3.val->EntailedBy(&bat.tf(), &s, 1));

  s.AddSensingResult({bat.forward}, bat.sonar, true);

  // Property 4
  Maybe<Formula::Ptr> reg4 = Formula::Act({bat.forward, bat.sonar}, close->Copy())->Regress(&bat.tf(), bat);
  EXPECT_TRUE(reg4);
  EXPECT_TRUE(reg4.val->EntailedBy(&bat.tf(), &s, 1));
}

TEST(formula, morri) {
  constexpr Setups::split_level k = 2;
  Ecai2014 bat(k);
  auto& s = bat.setups();

  // Property 1
  EXPECT_TRUE(Formula::Lit(Literal({}, false, bat.L1, {}))->EntailedBy(&bat.tf(), &s, 2));

  // Property 2
  s.AddSensingResult({}, bat.SL, true);
  EXPECT_TRUE(Formula::Act(bat.SL, Formula::And(Formula::Lit(Literal({}, true, bat.L1, {})),
                                                Formula::Lit(Literal({}, true, bat.R1, {}))))->EntailedBy(&bat.tf(), &s, 2));

  // Property 3
  s.AddSensingResult({bat.SL}, bat.SR1, false);
  EXPECT_TRUE(Formula::Act({bat.SL, bat.SR1}, Formula::Neg(Formula::Lit(Literal({}, true, bat.R1, {}))))->EntailedBy(&bat.tf(), &s, 2));

  // Property 5
  EXPECT_FALSE(Formula::Act({bat.SL, bat.SR1}, Formula::Lit(Literal({}, true, bat.L1, {})))->EntailedBy(&bat.tf(), &s, 2));
  EXPECT_FALSE(Formula::Neg(Formula::Act({bat.SL, bat.SR1}, Formula::Lit(Literal({}, true, bat.L1, {}))))->EntailedBy(&bat.tf(), &s, 2));

  // Property 6
  EXPECT_TRUE(Formula::Act({bat.SL, bat.SR1, bat.LV}, Formula::Lit(Literal({}, true, bat.R1, {})))->EntailedBy(&bat.tf(), &s, 2));

  // Property 6
  s.AddSensingResult({bat.SL,bat.SR1,bat.LV}, bat.SL, true);
  EXPECT_TRUE(Formula::Act({bat.SL, bat.SR1, bat.LV, bat.SL}, Formula::Lit(Literal({}, true, bat.L1, {})))->EntailedBy(&bat.tf(), &s, 2));
}

TEST(formula, morri_regression) {
  constexpr Setups::split_level k = 2;
  Ecai2014 bat(k);
  auto& s = bat.setups();

  // Property 1
  Maybe<Formula::Ptr> reg1 = Formula::Lit(Literal({}, false, bat.L1, {}))->Regress(&bat.tf(), bat);
  EXPECT_TRUE(reg1);
  EXPECT_TRUE(reg1.val->EntailedBy(&bat.tf(), &s, 2));

  // Property 2
  s.AddSensingResult({}, bat.SL, true);
  Maybe<Formula::Ptr> reg2 = Formula::Act(bat.SL, Formula::And(Formula::Lit(Literal({}, true, bat.L1, {})),
                                                               Formula::Lit(Literal({}, true, bat.R1, {}))))->Regress(&bat.tf(), bat);
  EXPECT_TRUE(reg2);
  EXPECT_TRUE(reg2.val->EntailedBy(&bat.tf(), &s, 2));

  // Property 3
  s.AddSensingResult({bat.SL}, bat.SR1, false);
  Maybe<Formula::Ptr> reg3 = Formula::Act({bat.SL, bat.SR1}, Formula::Neg(Formula::Lit(Literal({}, true, bat.R1, {}))))->Regress(&bat.tf(), bat);
  EXPECT_TRUE(reg3);
  EXPECT_TRUE(reg3.val->EntailedBy(&bat.tf(), &s, 2));

  // Property 5
  Maybe<Formula::Ptr> reg4 = Formula::Act({bat.SL, bat.SR1}, Formula::Lit(Literal({}, true, bat.L1, {})))->Regress(&bat.tf(), bat);
  EXPECT_TRUE(reg4);
  EXPECT_FALSE(reg4.val->EntailedBy(&bat.tf(), &s, 2));
  Maybe<Formula::Ptr> reg5 = Formula::Neg(Formula::Act({bat.SL, bat.SR1}, Formula::Lit(Literal({}, true, bat.L1, {}))))->Regress(&bat.tf(), bat);
  EXPECT_TRUE(reg5);
  EXPECT_FALSE(reg5.val->EntailedBy(&bat.tf(), &s, 2));

  // Property 6
  Maybe<Formula::Ptr> reg6 = Formula::Act({bat.SL, bat.SR1, bat.LV}, Formula::Lit(Literal({}, true, bat.R1, {})))->Regress(&bat.tf(), bat);
  EXPECT_TRUE(reg6);
  EXPECT_TRUE(reg6.val->EntailedBy(&bat.tf(), &s, 2));

  // Property 6
  s.AddSensingResult({bat.SL,bat.SR1,bat.LV}, bat.SL, true);
  Maybe<Formula::Ptr> reg7 = Formula::Act({bat.SL, bat.SR1, bat.LV, bat.SL}, Formula::Lit(Literal({}, true, bat.L1, {})))->Regress(&bat.tf(), bat);
  EXPECT_TRUE(reg7);
  EXPECT_TRUE(reg7.val->EntailedBy(&bat.tf(), &s, 2));
}

TEST(formula, fol_incompleteness_positive1) {
{'fraction_non_alphanumeric': 0.2349199835863767, 'fraction_numerical': 0.025235945835043086, 'mean_word_length': 4.199466666666667, 'pattern_counts': {'":': 0, '<': 28, '<?xml version=': 0, '>': 98, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 10, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2720355', 'n_tokens_mistral': 3845, 'n_tokens_neox': 3689, 'n_words': 623}