<commit_before>// Copyright 2015 <NAME>. Subject to the MIT License.

#include "sentence.hpp"

#include <algorithm>
#include <cassert>

// =============================================================================
//            Logical
// =============================================================================

std::ostream& operator<<(std::ostream& stream, const Sentence& s) {
	return s.print(stream);
}

// =============================================================================
//            Logical
// =============================================================================

Sentence* Logical::clone() const {
	return new Logical(_type, _a->clone(), _b->clone());
}

Sentence::Value Logical::value() const {
	Value va = _a->value();
	Value vb = _b->value();
	if (va == MU || vb == MU) {
		return MU;
	}
	switch(_type) {
	case AND:
		return static_cast<Value>(va && vb);
	case OR:
		return static_cast<Value>(va || vb);
	case IMPLIES:
		return static_cast<Value>(!va || vb);
	case IFF:
		return static_cast<Value>(va == vb);
	}
}

void Logical::negate() {
	switch (_type) {
	case AND:
		_type = OR;
		_a->negate();
		_b->negate();
		break;
	case OR:
		_type = AND;
		_a->negate();
		_b->negate();
		break;
	case IMPLIES:
		_type = AND;
		_b->negate();
		break;
	case IFF:
		expandIff();
		negate();
		break;
	}
}

std::ostream& Logical::print(std::ostream& s) const {
	s << '(';
	switch (_type) {
	case AND: s << "and"; break;
	case OR: s << "or"; break;
	case IMPLIES: s << "=>"; break;
	case IFF: s << "iff"; break;
	}
	s << ' ';
	_a->print(s);
	s << ' ';
	_b->print(s);
	return s << ')';
}

void Logical::converse() {
	assert(_type == IMPLIES);
	std::swap(_a, _b);
}

void Logical::contrapositive() {
	converse();
	_a->negate();
	_b->negate();
}

void Logical::expandIff() {
	assert(_type == IFF);
	_type = AND;
	Logical* fwd = new Logical(IMPLIES, _a, _b);
	Logical* bwd = new Logical(IMPLIES, _a->clone(), _b->clone());
	_a = fwd;
	_b = bwd;
}

int Logical::getType(const std::string& s) {
	if (s == "and") return AND;
	if (s == "or") return OR;
	if (s == "=>") return IMPLIES;
	if (s == "iff") return IFF;
	return -1;
}

// =============================================================================
//            Relation
// =============================================================================

Sentence* Relation::clone() const {
	return new Relation(_type, _a->clone(), _b->clone());
}

Sentence::Value Relation::value() const {
	return Sentence::MU;
}

void Relation::negate() {
	switch (_type) {
	case EQ: _type = NEQ; break;
	case NEQ: _type = EQ; break;
	case LT: _type = GTE; break;
	case GT: _type = LTE; break;
	case LTE: _type = GT; break;
	case GTE: _type = LT; break;
	case IN: _type = NOTIN; break;
	case NOTIN: _type = IN; break;
	case SUBSET:
		expandSubset();
		negate();
		break;
	}
}

std::ostream& Relation::print(std::ostream& s) const {
	s << '(';
	switch (_type) {
	case EQ: s << '='; break;
	case NEQ: s << "!="; break;
	case LT: s << '<'; break;
	case GT: s << '>'; break;
	case LTE: s << "<="; break;
	case GTE: s << ">="; break;
	case IN: s << "in"; break;
	case NOTIN: s << "notin"; break;
	case SUBSET: s << "subset"; break;
	}
	s << ' ';
	_a->print(s);
	s << ' ';
	_b->print(s);
	return s << ')';
}

Sentence* Relation::expandSubset() {
	assert(_type == SUBSET);
	Symbol* var = new Symbol('x');
	return new Quantified(
		Quantified::FORALL,
		var,
		dynamic_cast<Set*>(_a->clone()),
		new Relation(Relation::IN, var->cloneSelf(), _b->clone())
	);
}

int Relation::getType(const std::string& s) {
	if (s == "=") return EQ;
	if (s == "!=") return NEQ;
	if (s == "<") return LT;
	if (s == ">") return GT;
	if (s == "<=") return LTE;
	if (s == ">=") return GTE;
	if (s == "in") return IN;
	if (s == "notin") return NOTIN;
	if (s == "subset") return SUBSET;
	return -1;
}

// =============================================================================
//            Quantified
// =============================================================================

Quantified::Quantified(Type t, Symbol* var, Set* domain, Sentence* body)
	: _type(t), _var(var) {
	_body = new Logical(
		Logical::IMPLIES,
		new Relation(Relation::IN, var->clone(), domain),
		body
	);
}

Sentence* Quantified::clone() const {
	return new Quantified(_type, _var->cloneSelf(), _body->clone());
}

Sentence::Value Quantified::value() const {
	return Sentence::MU;
}

void Quantified::negate() {
	_type = static_cast<Type>(!_type);
	_body->negate();
}

std::ostream& Quantified::print(std::ostream& s) const {
	s << '(';
	switch (_type) {
	case FORALL: s << "forall"; break;
	case EXISTS: s << "exists"; break;
	}
	s << ' ';
	_var->print(s);
	s << ' ';
	_body->print(s);
	return s << ')';
}
<commit_msg>Fix quantified constructor (use AND for exists)<commit_after>// Copyright 2015 <NAME>. Subject to the MIT License.

#include "sentence.hpp"

#include <algorithm>
#include <cassert>

// =============================================================================
//            Logical
// =============================================================================

std::ostream& operator<<(std::ostream& stream, const Sentence& s) {
	return s.print(stream);
}

// =============================================================================
//            Logical
// =============================================================================

Sentence* Logical::clone() const {
	return new Logical(_type, _a->clone(), _b->clone());
}

Sentence::Value Logical::value() const {
	Value va = _a->value();
	Value vb = _b->value();
	if (va == MU || vb == MU) {
		return MU;
	}
	switch(_type) {
	case AND:
		return static_cast<Value>(va && vb);
	case OR:
		return static_cast<Value>(va || vb);
	case IMPLIES:
		return static_cast<Value>(!va || vb);
	case IFF:
		return static_cast<Value>(va == vb);
	}
}

void Logical::negate() {
	switch (_type) {
	case AND:
		_type = OR;
		_a->negate();
		_b->negate();
		break;
	case OR:
		_type = AND;
		_a->negate();
		_b->negate();
		break;
	case IMPLIES:
		_type = AND;
		_b->negate();
		break;
	case IFF:
		expandIff();
		negate();
		break;
	}
}

std::ostream& Logical::print(std::ostream& s) const {
	s << '(';
	switch (_type) {
	case AND: s << "and"; break;
	case OR: s << "or"; break;
	case IMPLIES: s << "=>"; break;
	case IFF: s << "iff"; break;
	}
	s << ' ';
	_a->print(s);
	s << ' ';
	_b->print(s);
	return s << ')';
}

void Logical::converse() {
	assert(_type == IMPLIES);
	std::swap(_a, _b);
}

void Logical::contrapositive() {
	converse();
	_a->negate();
	_b->negate();
}

void Logical::expandIff() {
	assert(_type == IFF);
	_type = AND;
	Logical* fwd = new Logical(IMPLIES, _a, _b);
	Logical* bwd = new Logical(IMPLIES, _a->clone(), _b->clone());
	_a = fwd;
	_b = bwd;
}

int Logical::getType(const std::string& s) {
	if (s == "and") return AND;
	if (s == "or") return OR;
	if (s == "=>") return IMPLIES;
	if (s == "iff") return IFF;
	return -1;
}

// =============================================================================
//            Relation
// =============================================================================

Sentence* Relation::clone() const {
	return new Relation(_type, _a->clone(), _b->clone());
}

Sentence::Value Relation::value() const {
	return Sentence::MU;
}

void Relation::negate() {
	switch (_type) {
	case EQ: _type = NEQ; break;
	case NEQ: _type = EQ; break;
	case LT: _type = GTE; break;
	case GT: _type = LTE; break;
	case LTE: _type = GT; break;
	case GTE: _type = LT; break;
	case IN: _type = NOTIN; break;
	case NOTIN: _type = IN; break;
	case SUBSET:
		expandSubset();
		negate();
		break;
	}
}

std::ostream& Relation::print(std::ostream& s) const {
	s << '(';
	switch (_type) {
	case EQ: s << '='; break;
	case NEQ: s << "!="; break;
	case LT: s << '<'; break;
	case GT: s << '>'; break;
	case LTE: s << "<="; break;
	case GTE: s << ">="; break;
	case IN: s << "in"; break;
	case NOTIN: s << "notin"; break;
	case SUBSET: s << "subset"; break;
	}
	s << ' ';
	_a->print(s);
	s << ' ';
	_b->print(s);
	return s << ')';
}

Sentence* Relation::expandSubset() {
	assert(_type == SUBSET);
	Symbol* var = new Symbol('x');
	return new Quantified(
		Quantified::FORALL,
		var,
		dynamic_cast<Set*>(_a->clone()),
		new Relation(Relation::IN, var->cloneSelf(), _b->clone())
	);
}

int Relation::getType(const std::string& s) {
	if (s == "=") return EQ;
	if (s == "!=") return NEQ;
	if (s == "<") return LT;
	if (s == ">") return GT;
	if (s == "<=") return LTE;
	if (s == ">=") return GTE;
	if (s == "in") return IN;
	if (s == "notin") return NOTIN;
	if (s == "subset") return SUBSET;
	return -1;
}

// =============================================================================
//            Quantified
// =============================================================================

Quantified::Quantified(Type t, Symbol* var, Set* domain, Sentence* body)
	: _type(t), _var(var) {
	_body = new Logical(
		(_type == FORALL) ? Logical::IMPLIES : Logical::AND,
		new Relation(Relation::IN, var->clone(), domain),
		body
	);
}

Sentence* Quantified::clone() const {
	return new Quantified(_type, _var->cloneSelf(), _body->clone());
}

Sentence::Value Quantified::value() const {
	return Sentence::MU;
}

void Quantified::negate() {
	_type = static_cast<Type>(!_type);
	_body->negate();
}

std::ostream& Quantified::print(std::ostream& s) const {
	s << '(';
	switch (_type) {
	case FORALL: s << "forall"; break;
	case EXISTS: s << "exists"; break;
	}
	s << ' ';
	_var->print(s);
	s << ' ';
	_body->print(s);
	return s << ')';
}

{'fraction_non_alphanumeric': 0.3137747097583935, 'fraction_numerical': 0.0012550988390335738, 'mean_word_length': 4.25673446948873, 'pattern_counts': {'":': 0, '<': 141, '<?xml version=': 0, '>': 89, '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': '6296468', 'n_tokens_mistral': 3606, 'n_tokens_neox': 3431, 'n_words': 865}