<commit_before>#include "GringoNumericFormat.h"

#include "../util/Constants.h"
#include "../util/ErrorMessage.h"
#include "../Clause.h"

#include <cassert>
#include <iostream>
#include <unordered_set>
using namespace std;

void
GringoNumericFormat::parse()
{
    this->parse( cin );
}

void
GringoNumericFormat::parse(
    istream& input )
{
    trace_msg( parser, 1, "Start parsing..." );
    bool loop = true;

    while( loop )
    {
        unsigned int type;
        input >> type;

        switch( type )
        {
        case GRINGO_NORMAL_RULE_ID:
            readNormalRule( input );
            break;

        case GRINGO_CHOICE_RULE_ID:
            readChoiceRule( input );
            break;

        case GRINGO_CONSTRAINT_RULE_ID:
//                readConstraintRule( input );
            ErrorMessage::errorDuringParsing( "Unsupported rule type." );
            break;

        case GRINGO_DISJUNCTIVE_RULE_ID:
//                readDisjunctiveRule( input );
            ErrorMessage::errorDuringParsing( "Unsupported rule type." );
            break;

        case GRINGO_LINE_SEPARATOR:
            loop = false;
            break;

        default:
            ErrorMessage::errorDuringParsing( "Unsupported rule type." );
            break;
        }

        if( solver.conflictDetected() )
            return;
            
        propagate();
    }

    readAtomsTable( input );
    readTrueAtoms( input );
    readFalseAtoms( input );
    readErrorNumber( input );

    simplify();

    if( solver.conflictDetected() )
        return;
        
//    cout << "cc" << endl;
    computeSCCs();
    if( !solver.tight() )
    {
        trace_msg( parser, 1, "Program is not tight" );
        computeGusStructures();
    } else
    {
        trace_msg( parser, 1, "Program is tight" );
    }
    computeCompletion();

    //TODO: remove
//    cout << solver.numberOfVariables() << endl;
//    unsigned c[1024] = {0};
//    for( unsigned i = 0; i < solver.numberOfClauses(); i++ )
//        c[solver.clauseAt( i )->size()]++;
//    cout << "occs\n";
//    for( unsigned i = 1; i < 10; i++)
//        cout << c[i] << endl;
    cout << "Solving..." << endl;
}

void
GringoNumericFormat::readChoiceRule(
    istream& input )
{
    int headSize, bodySize, negativeSize;
    input >> headSize;
    unsigned head[ headSize ];
    for( int i = 0; i < headSize; )
    {
        input >> head[ i ];
        createStructures( head[ i ] );
        if( solver.getVariable( head[ i ] )->isFalse() )
            --headSize;
        else
            ++i;
    }
    readBodySize( input, bodySize, negativeSize );
    if( headSize == 0)
    {
        skipLiterals( input, bodySize );
        return;
    }
    
    ++readNormalRule_numberOfCalls;
    NormalRule* rule = new NormalRule( head[ 0 ] );
    unsigned tmp;
    while( negativeSize-- > 0 )
    {
        --bodySize;
        input >> tmp;
        createStructures( tmp );
        
        if( atomData[ tmp ].readNormalRule_negativeLiterals == readNormalRule_numberOfCalls )
            continue;
        if( solver.getVariable( tmp )->isTrue() )
        {
            delete rule;
            skipLiterals( input, bodySize );
            return;
        }
        else if( solver.getVariable( tmp )->isUndefined() )
        {
            rule->addNegativeLiteral( tmp );
            atomData[ tmp ].readNormalRule_negativeLiterals = readNormalRule_numberOfCalls;
        }
    }
    while( bodySize-- > 0 )
    {
        input >> tmp;
        createStructures( tmp );

        if( atomData[ tmp ].readNormalRule_positiveLiterals == readNormalRule_numberOfCalls )
            continue;
        if( solver.getVariable( tmp )->isFalse() || tmp == head[ 0 ] || atomData[ tmp ].readNormalRule_negativeLiterals == readNormalRule_numberOfCalls )
        {
            delete rule;
            skipLiterals( input, bodySize );
            return;
        }
        else 
        {
            if( solver.getVariable( tmp )->isUndefined() )
                rule->addPositiveLiteral( tmp );
            else
                rule->addPositiveTrueLiteral( tmp );
            atomData[ tmp ].readNormalRule_positiveLiterals = readNormalRule_numberOfCalls;
        }
    }
    rule->addDoubleNegLiteral( head[ 0 ] );

    for( int i = 1; i < headSize; ++i )
    {
        if( atomData[ i ].readNormalRule_negativeLiterals == readNormalRule_numberOfCalls )
            continue;
        NormalRule* r = new NormalRule( *rule );
        r->head = head[ i ];
        r->doubleNegBody.back() = head[ i ];
        add( r );
    }

    if( atomData[ head[ 0 ] ].readNormalRule_negativeLiterals == readNormalRule_numberOfCalls )
        delete rule;
    else
        add( rule );
    
}

void
GringoNumericFormat::readNormalRule(
    istream& input )
{
    unsigned head;
    input >> head;

    createStructures( head );

    if( solver.getVariable( head )->isFalse() )
        readConstraint( input );
    else
    {
        int bodySize, negativeSize;
        readBodySize( input, bodySize, negativeSize );

        if( atomData[ head ].isSupported() )
            skipLiterals( input, bodySize );
        else if( bodySize == 0 )
            addFact( head );
        else
            readNormalRule( input, head, bodySize, negativeSize );
    }
}

void
GringoNumericFormat::readBodySize(
    istream& input,
    int& bodySize,
    int& negativeSize )
{
    input >> bodySize >> negativeSize;

    if( bodySize < negativeSize )
        ErrorMessage::errorDuringParsing( "Body size must be greater than or equal to negative size." );
}

void
GringoNumericFormat::skipLiterals(
    istream& input,
    unsigned howMany )
{
    unsigned tmp;
    while( howMany-- > 0 )
        input >> tmp;
}

void
GringoNumericFormat::readNormalRule(
    istream& input,
    unsigned head,
    int bodySize,
    int negativeSize )
{
    assert( !solver.getVariable( head )->isFalse() );
    assert( !atomData[ head ].isSupported() );
    assert( bodySize >= negativeSize );
    assert( negativeSize >= 0 );
    assert( bodySize >= 1 );

    readNormalRule_numberOfCalls++;
    assert( readNormalRule_numberOfCalls != 0 );

    NormalRule* rule = new NormalRule( head );
    unsigned tmp;
    while( negativeSize-- > 0 )
    {
        --bodySize;
        input >> tmp;
        createStructures( tmp );
        
        if( atomData[ tmp ].readNormalRule_negativeLiterals == readNormalRule_numberOfCalls )
            continue;
        if( solver.getVariable( tmp )->isTrue() )
        {
            delete rule;
            skipLiterals( input, bodySize );
            return;
        }
        else if( solver.getVariable( tmp )->isUndefined() )
        {
            rule->addNegativeLiteral( tmp );
            atomData[ tmp ].readNormalRule_negativeLiterals = readNormalRule_numberOfCalls;
        }
    }
    while( bodySize-- > 0 )
    {
        input >> tmp;
        createStructures( tmp );

        if( atomData[ tmp ].readNormalRule_positiveLiterals == readNormalRule_numberOfCalls )
            continue;
        if( solver.getVariable( tmp )->isFalse() || tmp == head || atomData[ tmp ].readNormalRule_negativeLiterals == readNormalRule_numberOfCalls )
        {
            delete rule;
            skipLiterals( input, bodySize );
            return;
        }
        else 
        {
            if( solver.getVariable( tmp )->isUndefined() )
                rule->addPositiveLiteral( tmp );
            else
                rule->addPositiveTrueLiteral( tmp );
            atomData[ tmp ].readNormalRule_positiveLiterals = readNormalRule_numberOfCalls;
        }
    }

    if( atomData[ head ].readNormalRule_negativeLiterals == readNormalRule_numberOfCalls )
    {
        bodyToConstraint( rule );
        delete rule;
    }
    else if( rule->isFact() )
    {
        delete rule;
        addFact( head );
    }
    else
    {
        if( rule->isFiring() )
            solver.addClause( Literal( solver.getVariable( head ), POSITIVE ) );
        add( rule );
    }
}

void
GringoNumericFormat::readConstraint(
    istream& input )
{
    unsigned  bodySize, negativeSize, tmp;
    input >> bodySize >> negativeSize;

    if( bodySize < negativeSize )
        ErrorMessage::errorDuringParsing( "Body size must be greater than or equal to negative size." );

    Clause* clause = solver.newClause( bodySize );
    while( negativeSize-- > 0 )
    {
        --bodySize;
        input >> tmp;
        if( !clause->addUndefinedLiteral( Literal( solver.getVariable( tmp ), POSITIVE ) ) )
        {
            solver.releaseClause( clause );
            skipLiterals( input, bodySize );
            return;
        }
    }
    while( bodySize-- > 0 )
    {
        input >> tmp;
        if( !clause->addUndefinedLiteral( Literal( solver.getVariable( tmp ), NEGATIVE ) ) )
        {
            solver.releaseClause( clause );
            skipLiterals( input, bodySize );
            return;
        }
    }

    solver.addClause( clause );
}

void
GringoNumericFormat::propagate()
{
    bool repeat;
    do {
        repeat = false;
        while( propagatedLiterals < solver.numberOfAssignedLiterals() )
        {
            repeat = true;
            Variable* var = solver.getAssignedVariable( propagatedLiterals++ );
            if( var->isTrue() )
                propagateTrue( var );
            else
                propagateFalse( var );
        }
        while( !facts.empty() )
        {
            repeat = true;
            Variable* var = solver.getVariable( facts.back() );
            facts.pop_back();
            propagateFact( var );
        }
    }while( repeat );
}

void
GringoNumericFormat::propagateTrue(
    Variable* var )
{
    assert( var != NULL );
    assert( var->isTrue() );

    assert( var->getId() < atomData.size() );
    AtomData& data = atomData[ var->getId() ];

    trace_msg( parser, 2, "Propagating " << *var << " as true" << ( data.isSupported() ? " (supported)" : "" ) );

    if( data.numberOfHeadOccurrences == 1 )
        atomsWithSupportInference.push_back( var->getId() );

    unsigned j = 0;
    for( unsigned i = 0; i < data.posOccurrences.size(); ++i )
    {
        NormalRule* rule = data.posOccurrences[ i ];
        assert( rule != NULL );
        if( !shrinkPos( rule, var->getId() ) )
            data.posOccurrences[ j++ ] = data.posOccurrences[ i ];
    }
    data.posOccurrences.resize( j );

    for( unsigned i = 0; i < data.negOccurrences.size(); ++i )
    {
        NormalRule* rule = data.negOccurrences[ i ];
        assert( rule != NULL );
        removeAndCheckSupport( rule );
    }
    data.negOccurrences.clear();
    
    for( unsigned i = 0; i < data.doubleNegOccurrences.size(); ++i )
    {
        NormalRule* rule = data.doubleNegOccurrences[ i ];
        assert( rule != NULL );
        shrinkDoubleNeg( rule, var->getId() );
    }
    data.doubleNegOccurrences.clear();
}

void
GringoNumericFormat::propagateFalse(
    Variable* var )
{
    assert( var != NULL );
    assert( var->isFalse() );

    assert( var->getId() < atomData.size() );
    AtomData& data = atomData[ var->getId() ];
    
    trace_msg( parser, 2, "Propagating " << *var << " as false" );

    for( unsigned i = 0; i < data.doubleNegOccurrences.size(); ++i )
    {
        NormalRule* rule = data.doubleNegOccurrences[ i ];
        assert( rule != NULL );
        removeAndCheckSupport( rule );
    }
    data.doubleNegOccurrences.clear();
    
    for( unsigned i = 0; i < data.headOccurrences.size(); ++i )
    {
        NormalRule* rule = data.headOccurrences[ i ];
        assert( rule != NULL );
        if( rule->isRemoved() )
            continue;
        bodyToConstraint( rule );
        rule->remove();
    }
    data.numberOfHeadOccurrences = 0;
    data.headOccurrences.clear();

    for( unsigned i = 0; i < data.posOccurrences.size(); ++i )
    {
        NormalRule* rule = data.posOccurrences[ i ];
        assert( rule != NULL );
        removeAndCheckSupport( rule );
    }
    data.posOccurrences.clear();

    for( unsigned i = 0; i < data.negOccurrences.size(); ++i )
    {
        NormalRule* rule = data.negOccurrences[ i ];
        assert( rule != NULL );
        shrinkNeg( rule, var->getId() );
    }
    data.negOccurrences.clear();
}

void
GringoNumericFormat::bodyToConstraint(
    NormalRule* rule )
{
    trace_msg( parser, 3, "Replacing " << *rule << " by a constraint" );
    Clause* clause = solver.newClause( rule->size() );
    for( unsigned j = 0; j < rule->negBody.size(); ++j )
        clause->addLiteral( Literal( solver.getVariable( rule->negBody[ j ] ), POSITIVE ) );
    for( unsigned j = 0; j < rule->posBody.size(); ++j )
        clause->addLiteral( Literal( solver.getVariable( rule->posBody[ j ] ), NEGATIVE ) );
    for( unsigned j = 0; j < rule->doubleNegBody.size(); ++j )
        clause->addLiteral( Literal( solver.getVariable( rule->doubleNegBody[ j ] ), NEGATIVE ) );
    solver.cleanAndAddClause( clause );
}

void
GringoNumericFormat::propagateFact(
    Variable* var )
{
    assert( var->getId() < atomData.size() );
    AtomData& data = atomData[ var->getId() ];
    
    trace_msg( parser, 2, "Propagating fact " << *var );

    for( unsigned i = 0; i < data.headOccurrences.size(); ++i )
    {
        NormalRule* rule = data.headOccurrences[ i ];
        assert( rule != NULL );
        if( rule->isRemoved() )
            continue;
        trace_msg( parser, 3, "Removing rule " << *rule );
        rule->remove();
    }
    data.numberOfHeadOccurrences = 0;
    data.headOccurrences.clear();
    
    for( unsigned i = 0; i < data.posOccurrences.size(); ++i )
    {
        NormalRule* rule = data.posOccurrences[ i ];
        assert( rule != NULL );
        shrinkPos( rule, var->getId() );
    }
    data.posOccurrences.clear();
}

void
GringoNumericFormat::addFact(
    unsigned head )
{
    if( atomData[ head ].isSupported() )
        return;

    trace_msg( parser, 3, "Adding fact " << head );
    atomData[ head ].setSupported();
    solver.addClause( Literal( solver.getVariable( head ), POSITIVE ) );
    facts.push_back( head );
}

void
GringoNumericFormat::readAtomsTable(
    istream& input )
{
    unsigned int nextAtom;
    input >> nextAtom;

    createStructures( nextAtom );

    char name[ 1024 ];
    while( nextAtom != 0 )
    {
//        assert_msg( nextAtom < inputVarId.size(), "nextAtom = " << nextAtom << "; size = " << inputVarId.size() );
//        assert( inputVarId[ nextAtom ] > 1 );

        input.getline( name, 1024 );
        VariableNames::setName( solver.getVariable( nextAtom ), name+1 );
        trace_msg( parser, 6, "Set name " << name+1 << " for atom " << nextAtom );
        input >> nextAtom;
    }

//    #ifdef TRACE_ON
//    for( unsigned i = 1; i < inputVarId.size(); ++i )
//    {
//        Variable* variable = solver.getVariable( inputVarId[ i ] );
//        if( VariableNames::isHidden( variable ) )
//        {
//            stringstream s;
//            s << "#hidden" << i;
//            string name = s.str();
//            VariableNames::setName( variable, name );
//        }
//    }
//    for( unsigned i = 1; i < auxVarId.size(); ++i )
//    {
//        Variable* variable = solver.getVariable( auxVarId[ i ] );
//        if( VariableNames::isHidden( variable ) )
//        {
//            stringstream s;
//            s << "#aux" << i;
//            string name = s.str();
//            VariableNames::setName( variable, name );
//        }
//    }
//    #endif
}

void
GringoNumericFormat::readTrueAtoms(
    istream& input )
{
    char b;

    input >> b;
    assert( b == 'B' );
    input >> b;
    assert( b == '+' );

    unsigned int nextAtom;
    input >> nextAtom;

    createStructures( nextAtom );

    while( nextAtom != 0 )
    {
        cout << nextAtom << endl;
        solver.addClause( Literal( solver.getVariable( nextAtom ), POSITIVE ) );
        input >> nextAtom;
    }
}

void
GringoNumericFormat::readFalseAtoms(
    istream& input )
{
    char b;

    input >> b;
    assert( b == 'B' );
    input >> b;
    assert( b == '-' );

    unsigned int nextAtom;
    input >> nextAtom;

    createStructures( nextAtom );

    while( nextAtom != 0 )
    {
        solver.addClause( Literal( solver.getVariable( nextAtom ), NEGATIVE ) );
        input >> nextAtom;
    }
}

void
GringoNumericFormat::readErrorNumber(
    istream& input )
{
    unsigned int errorNumber;
    input >> errorNumber;

    if( errorNumber != 1 ) {
        stringstream ss;
        ss << "read error message number " << errorNumber;
        ErrorMessage::errorDuringParsing( ss.str() );
        exit( 0 );
    }
    else
    {
    }
}

void
GringoNumericFormat::processRecursivePositiveCrule(
    Clause* crule )
{
    assert( crule != NULL );
    assert( crule->getAt( 0 ).isPositive() );
    Variable* variable = crule->getAt( 0 ).getVariable();
    assert( variable->isInCyclicComponent() );

    trace_msg( parser, 2, "Creating GUS data structures for variable " << *variable << " whose supporting rule has " << crule->size()-1 << " literals" );
    variable->setFrozen();

    Component* component = variable->getComponent();
    assert( component != NULL );
    component->setAuxVariable( variable->getId() );

    for( unsigned int j = 1; j < crule->size(); j++ )
    {
        crule->getAt( j ).getVariable()->setFrozen();
        if( crule->getAt( j ).isNegative() )
        {
            if( crule->getAt( j ).getVariable()->inTheSameComponent( variable ) )
            {
                Literal lit = crule->getAt( j ).getOppositeLiteral();
                trace_msg( parser, 3, "Adding " << lit << " to the supporting rule of " << *variable );
                component->addAuxVariableSupportedByLiteral( variable, lit );
                component->addInternalLiteralForVariable( variable->getId(), lit );
            }
        }
    }
}

void
GringoNumericFormat::processRecursiveNegativeCrule(
    Clause* crule )
{
    assert( crule != NULL );
    assert( crule->getAt( 0 ).isNegative() );
    Variable* variable = crule->getAt( 0 ).getVariable();
    assert( variable->isInCyclicComponent() );

    trace_msg( parser, 2, "Creating GUS data structures for variable " << *variable << ", which has " << crule->size()-1 << " supporting rules" );

    Component* component = variable->getComponent();
    assert( component != NULL );

    for( unsigned int j = 1; j < crule->size(); j++ )
    {
        Variable* ruleVar = crule->getAt( j ).getVariable();
        ruleVar->setFrozen();
        if( literalsPostPropagator[ crule->getAt( j ).getSign() ][ ruleVar ].insert( component ).second )
            Literal( ruleVar, crule->getAt( j ).getSign() ).addPostPropagator( component );

        if( crule->getAt( j ).isPositive() && variable->inTheSameComponent( ruleVar ) )
        {
            trace_msg( parser, 3, "Adding " << *ruleVar << " as internal rule for " << *variable );
            component->addInternalLiteralForVariable( variable->getId(), Literal( ruleVar, POSITIVE ) );
            component->addVariablePossiblySupportedByLiteral( variable, Literal( ruleVar, POSITIVE ) );
        }
        else
        {
            trace_msg( parser, 3, "Adding " << crule->getAt( j ) << " as external rule for " << *variable );
            component->addExternalLiteralForVariable( variable->getId(), crule->getAt( j ) );
        }
    }    
}

void
GringoNumericFormat::computeGusStructures()
{
    //Add two fake positions
    solver.addGUSData( NULL );
    solver.addGUSData( NULL );
    for( unsigned int i = 2; i <= solver.numberOfVariables(); i++ )
    {
        GUSData* gd = new GUSData();
        gd->variable = solver.getVariable( i );
        solver.addGUSData( gd );
    }

    trace_msg( parser, 2, "Program is not tight. Number of cyclic components " << solver.getNumberOfCyclicComponents() );
    for( unsigned int i = 0; i < solver.getNumberOfCyclicComponents(); i++ )
    {
        Component* component = solver.getCyclicComponent( i );

        for( unsigned int j = 0; j < component->size(); j++ )
        {
            unsigned int varId = component->getVariable( j );
            assert( varId <= solver.numberOfVariables() );
            trace_msg( parser, 2, "Variable " << *solver.getVariable( varId ) << " is in the cyclic component " << i );
            Variable* currentVariable = solver.getVariable( varId );
            currentVariable->setComponent( component );
            component->variableHasNoSourcePointer( currentVariable );
        }

        solver.addPostPropagator( component );
    }

    for( unsigned int i = 0; i < crules.size(); i++ )
    {
        Clause* crule = crules[ i ];
        assert( crule != NULL );

        // skip acyclic variables
        if( !crule->getAt( 0 ).getVariable()->isInCyclicComponent() )
            continue;

        if( crule->getAt( 0 ).isPositive() )
            processRecursivePositiveCrule( crule );
        else
            processRecursiveNegativeCrule( crule );
    }
    
//    unsigned count = 0;
//    for( unsigned int i = 0; i < solver.getNumberOfCyclicComponents(); i++ )
//    {
//        bool found = false;
//        Component* component = solver.getCyclicComponent( i );
//        for( unsigned int j = 0; j < component->size(); j++ )
//        {
//            unsigned int varId = component->getVariable( j );
//            if( !component->isAuxVariable( varId ) )
//            {
//                cout << varId << endl;
//                found = true;
//                break;
//            }
//        }
//        if( found ) count++;
//    }
//    cout << count << " " << solver.getNumberOfCyclicComponents() << endl;
}

void
GringoNumericFormat::createStructures(
    unsigned id )
{
    while( id >= atomData.size() ) {
        solver.addVariable();
        solver.addEdgeInDependencyGraph( solver.numberOfVariables(), 0 );
        atomData.push_back( AtomData( false ) );
    }
}

void
GringoNumericFormat::simplify()
{
    trace_msg( parser, 1, "Simplify" );
    atomsWithSupportInference.clear();
    for( unsigned i = 2; i < atomData.size(); ++i )
    {
        if( atomData[ i ].isSupported() || solver.getVariable( i )->isFalse() )
            continue;
        if( atomData[ i ].numberOfHeadOccurrences == 0 || ( atomData[ i ].numberOfHeadOccurrences == 1 && solver.getVariable( i )->isTrue() ) )
            atomsWithSupportInference.push_back( i );
    }
    
    while( !atomsWithSupportInference.empty() )
    {
        AtomData& data = atomData[ atomsWithSupportInference.back() ];
        if( !data.isSupported() && !solver.getVariable( atomsWithSupportInference.back() )->isFalse() )
        {
            if( data.numberOfHeadOccurrences == 0 )
            {
                trace_msg( parser, 2, "Infer falsity of variable " << *solver.getVariable( atomsWithSupportInference.back() ) << " with no support" );
                solver.addClause( Literal( solver.getVariable( atomsWithSupportInference.back() ), NEGATIVE ) );
                assert( solver.getVariable( atomsWithSupportInference.back() )->isFalse() || solver.conflictDetected() );
            }
            else
            {
                assert( data.numberOfHeadOccurrences == 1 );
                assert( solver.getVariable( atomsWithSupportInference.back() )->isTrue() );
                assert( !data.isSupported() );
                
                for( unsigned i = 0; i < data.headOccurrences.size(); ++i )
                {
                    if( !data.headOccurrences[ i ]->isRemoved() )
                    {
                        data.headOccurrences[ 0 ] = data.headOccurrences[ i ];
                        break;
                    }
                }
                data.headOccurrences.resize( 1 );
                NormalRule* rule = data.headOccurrences[ 0 ];
                assert( !rule->isRemoved() );
                trace_msg( parser, 2, "Infer truth of the body of " << *rule << " (unique support of true head)" );
                for( unsigned i = 0; i < rule->posBody.size(); ++i )
                    solver.addClause( Literal( solver.getVariable( rule->posBody[ i ] ), POSITIVE ) );
                for( unsigned i = 0; i < rule->negBody.size(); ++i )
                    solver.addClause( Literal( solver.getVariable( rule->negBody[ i ] ), NEGATIVE ) );
                for( unsigned i = 0; i < rule->doubleNegBody.size(); ++i )
                    solver.addClause( Literal( solver.getVariable( rule->doubleNegBody[ i ], POSITIVE ) ) );
            }
        }
        atomsWithSupportInference.pop_back();
        propagate();
        if( solver.conflictDetected() )
            return;
    }
}

void
GringoNumericFormat::createCrule(
    Literal head,
    NormalRule* rule )
{
    assert( head.isPositive() );
    Clause* crule = solver.newClause( rule->size() + 1 );
    crule->addLiteral( head );
    for( unsigned k = 0; k < rule->negBody.size(); ++k )
        crule->addLiteral( Literal( solver.getVariable( rule->negBody[ k ] ), POSITIVE ) );
    for( unsigned k = 0; k < rule->posBody.size(); ++k )
    {<commit_msg>Minor fix.<commit_after>#include "GringoNumericFormat.h"

#include "../util/Constants.h"
#include "../util/ErrorMessage.h"
#include "../Clause.h"

#include <cassert>
#include <iostream>
#include <unordered_set>
using namespace std;

void
GringoNumericFormat::parse()
{
    this->parse( cin );
}

void
GringoNumericFormat::parse(
    istream& input )
{
    trace_msg( parser, 1, "Start parsing..." );
    bool loop = true;

    while( loop )
    {
        unsigned int type;
        input >> type;

        switch( type )
        {
        case GRINGO_NORMAL_RULE_ID:
            readNormalRule( input );
            break;

        case GRINGO_CHOICE_RULE_ID:
            readChoiceRule( input );
            break;

        case GRINGO_CONSTRAINT_RULE_ID:
//                readConstraintRule( input );
            ErrorMessage::errorDuringParsing( "Unsupported rule type." );
            break;

        case GRINGO_DISJUNCTIVE_RULE_ID:
//                readDisjunctiveRule( input );
            ErrorMessage::errorDuringParsing( "Unsupported rule type." );
            break;

        case GRINGO_LINE_SEPARATOR:
            loop = false;
            break;

        default:
            ErrorMessage::errorDuringParsing( "Unsupported rule type." );
            break;
        }

        if( solver.conflictDetected() )
            return;
            
        propagate();
    }

    readAtomsTable( input );
    readTrueAtoms( input );
    readFalseAtoms( input );
    readErrorNumber( input );

    simplify();

    if( solver.conflictDetected() )
        return;
        
//    cout << "cc" << endl;
    computeSCCs();
    if( !solver.tight() )
    {
        trace_msg( parser, 1, "Program is not tight" );
        computeGusStructures();
    } else
    {
        trace_msg( parser, 1, "Program is tight" );
    }
    computeCompletion();

    //TODO: remove
//    cout << solver.numberOfVariables() << endl;
//    unsigned c[1024] = {0};
//    for( unsigned i = 0; i < solver.numberOfClauses(); i++ )
//        c[solver.clauseAt( i )->size()]++;
//    cout << "occs\n";
//    for( unsigned i = 1; i < 10; i++)
//        cout << c[i] << endl;
    cout << "Solving..." << endl;
}

void
GringoNumericFormat::readChoiceRule(
    istream& input )
{
    int headSize, bodySize, negativeSize;
    input >> headSize;
    unsigned head[ headSize ];
    for( int i = 0; i < headSize; )
    {
        input >> head[ i ];
        createStructures( head[ i ] );
        if( solver.getVariable( head[ i ] )->isFalse() )
            --headSize;
        else
            ++i;
    }
    readBodySize( input, bodySize, negativeSize );
    if( headSize == 0)
    {
        skipLiterals( input, bodySize );
        return;
    }
    
    ++readNormalRule_numberOfCalls;
    NormalRule* rule = new NormalRule( head[ 0 ] );
    unsigned tmp;
    while( negativeSize-- > 0 )
    {
        --bodySize;
        input >> tmp;
        createStructures( tmp );
        
        if( atomData[ tmp ].readNormalRule_negativeLiterals == readNormalRule_numberOfCalls )
            continue;
        if( solver.getVariable( tmp )->isTrue() )
        {
            delete rule;
            skipLiterals( input, bodySize );
            return;
        }
        else if( solver.getVariable( tmp )->isUndefined() )
        {
            rule->addNegativeLiteral( tmp );
            atomData[ tmp ].readNormalRule_negativeLiterals = readNormalRule_numberOfCalls;
        }
    }
    while( bodySize-- > 0 )
    {
        input >> tmp;
        createStructures( tmp );

        if( atomData[ tmp ].readNormalRule_positiveLiterals == readNormalRule_numberOfCalls )
            continue;
        if( solver.getVariable( tmp )->isFalse() || tmp == head[ 0 ] || atomData[ tmp ].readNormalRule_negativeLiterals == readNormalRule_numberOfCalls )
        {
            delete rule;
            skipLiterals( input, bodySize );
            return;
        }
        else 
        {
            if( solver.getVariable( tmp )->isUndefined() )
                rule->addPositiveLiteral( tmp );
            else
                rule->addPositiveTrueLiteral( tmp );
            atomData[ tmp ].readNormalRule_positiveLiterals = readNormalRule_numberOfCalls;
        }
    }
    rule->addDoubleNegLiteral( head[ 0 ] );

    for( int i = 1; i < headSize; ++i )
    {
        if( atomData[ i ].readNormalRule_negativeLiterals == readNormalRule_numberOfCalls )
            continue;
        NormalRule* r = new NormalRule( *rule );
        r->head = head[ i ];
        r->doubleNegBody.back() = head[ i ];
        add( r );
    }

    if( atomData[ head[ 0 ] ].readNormalRule_negativeLiterals == readNormalRule_numberOfCalls )
        delete rule;
    else
        add( rule );
    
}

void
GringoNumericFormat::readNormalRule(
    istream& input )
{
    unsigned head;
    input >> head;

    createStructures( head );

    if( solver.getVariable( head )->isFalse() )
        readConstraint( input );
    else
    {
        int bodySize, negativeSize;
        readBodySize( input, bodySize, negativeSize );

        if( atomData[ head ].isSupported() )
            skipLiterals( input, bodySize );
        else if( bodySize == 0 )
            addFact( head );
        else
            readNormalRule( input, head, bodySize, negativeSize );
    }
}

void
GringoNumericFormat::readBodySize(
    istream& input,
    int& bodySize,
    int& negativeSize )
{
    input >> bodySize >> negativeSize;

    if( bodySize < negativeSize )
        ErrorMessage::errorDuringParsing( "Body size must be greater than or equal to negative size." );
}

void
GringoNumericFormat::skipLiterals(
    istream& input,
    unsigned howMany )
{
    unsigned tmp;
    while( howMany-- > 0 )
        input >> tmp;
}

void
GringoNumericFormat::readNormalRule(
    istream& input,
    unsigned head,
    int bodySize,
    int negativeSize )
{
    assert( !solver.getVariable( head )->isFalse() );
    assert( !atomData[ head ].isSupported() );
    assert( bodySize >= negativeSize );
    assert( negativeSize >= 0 );
    assert( bodySize >= 1 );

    readNormalRule_numberOfCalls++;
    assert( readNormalRule_numberOfCalls != 0 );

    NormalRule* rule = new NormalRule( head );
    unsigned tmp;
    while( negativeSize-- > 0 )
    {
        --bodySize;
        input >> tmp;
        createStructures( tmp );
        
        if( atomData[ tmp ].readNormalRule_negativeLiterals == readNormalRule_numberOfCalls )
            continue;
        if( solver.getVariable( tmp )->isTrue() )
        {
            delete rule;
            skipLiterals( input, bodySize );
            return;
        }
        else if( solver.getVariable( tmp )->isUndefined() )
        {
            rule->addNegativeLiteral( tmp );
            atomData[ tmp ].readNormalRule_negativeLiterals = readNormalRule_numberOfCalls;
        }
    }
    while( bodySize-- > 0 )
    {
        input >> tmp;
        createStructures( tmp );

        if( atomData[ tmp ].readNormalRule_positiveLiterals == readNormalRule_numberOfCalls )
            continue;
        if( solver.getVariable( tmp )->isFalse() || tmp == head || atomData[ tmp ].readNormalRule_negativeLiterals == readNormalRule_numberOfCalls )
        {
            delete rule;
            skipLiterals( input, bodySize );
            return;
        }
        else 
        {
            if( solver.getVariable( tmp )->isUndefined() )
                rule->addPositiveLiteral( tmp );
            else
                rule->addPositiveTrueLiteral( tmp );
            atomData[ tmp ].readNormalRule_positiveLiterals = readNormalRule_numberOfCalls;
        }
    }

    if( atomData[ head ].readNormalRule_negativeLiterals == readNormalRule_numberOfCalls )
    {
        bodyToConstraint( rule );
        delete rule;
    }
    else if( rule->isFact() )
    {
        delete rule;
        addFact( head );
    }
    else
    {
        if( rule->isFiring() )
            solver.addClause( Literal( solver.getVariable( head ), POSITIVE ) );
        add( rule );
    }
}

void
GringoNumericFormat::readConstraint(
    istream& input )
{
    unsigned  bodySize, negativeSize, tmp;
    input >> bodySize >> negativeSize;

    if( bodySize < negativeSize )
        ErrorMessage::errorDuringParsing( "Body size must be greater than or equal to negative size." );

    Clause* clause = solver.newClause( bodySize );
    while( negativeSize-- > 0 )
    {
        --bodySize;
        input >> tmp;
        if( !clause->addUndefinedLiteral( Literal( solver.getVariable( tmp ), POSITIVE ) ) )
        {
            solver.releaseClause( clause );
            skipLiterals( input, bodySize );
            return;
        }
    }
    while( bodySize-- > 0 )
    {
        input >> tmp;
        if( !clause->addUndefinedLiteral( Literal( solver.getVariable( tmp ), NEGATIVE ) ) )
        {
            solver.releaseClause( clause );
            skipLiterals( input, bodySize );
            return;
        }
    }

    solver.addClause( clause );
}

void
GringoNumericFormat::propagate()
{
    bool repeat;
    do {
        repeat = false;
        while( propagatedLiterals < solver.numberOfAssignedLiterals() )
        {
            repeat = true;
            Variable* var = solver.getAssignedVariable( propagatedLiterals++ );
            if( var->isTrue() )
                propagateTrue( var );
            else
                propagateFalse( var );
        }
        while( !facts.empty() )
        {
            repeat = true;
            Variable* var = solver.getVariable( facts.back() );
            facts.pop_back();
            propagateFact( var );
        }
    }while( repeat );
}

void
GringoNumericFormat::propagateTrue(
    Variable* var )
{
    assert( var != NULL );
    assert( var->isTrue() );

    assert( var->getId() < atomData.size() );
    AtomData& data = atomData[ var->getId() ];

    trace_msg( parser, 2, "Propagating " << *var << " as true" << ( data.isSupported() ? " (supported)" : "" ) );

    if( data.numberOfHeadOccurrences == 1 )
        atomsWithSupportInference.push_back( var->getId() );

    unsigned j = 0;
    for( unsigned i = 0; i < data.posOccurrences.size(); ++i )
    {
        NormalRule* rule = data.posOccurrences[ i ];
        assert( rule != NULL );
        if( !shrinkPos( rule, var->getId() ) )
            data.posOccurrences[ j++ ] = data.posOccurrences[ i ];
    }
    data.posOccurrences.resize( j );

    for( unsigned i = 0; i < data.negOccurrences.size(); ++i )
    {
        NormalRule* rule = data.negOccurrences[ i ];
        assert( rule != NULL );
        removeAndCheckSupport( rule );
    }
    data.negOccurrences.clear();
    
    for( unsigned i = 0; i < data.doubleNegOccurrences.size(); ++i )
    {
        NormalRule* rule = data.doubleNegOccurrences[ i ];
        assert( rule != NULL );
        shrinkDoubleNeg( rule, var->getId() );
    }
    data.doubleNegOccurrences.clear();
}

void
GringoNumericFormat::propagateFalse(
    Variable* var )
{
    assert( var != NULL );
    assert( var->isFalse() );

    assert( var->getId() < atomData.size() );
    AtomData& data = atomData[ var->getId() ];
    
    trace_msg( parser, 2, "Propagating " << *var << " as false" );

    for( unsigned i = 0; i < data.doubleNegOccurrences.size(); ++i )
    {
        NormalRule* rule = data.doubleNegOccurrences[ i ];
        assert( rule != NULL );
        removeAndCheckSupport( rule );
    }
    data.doubleNegOccurrences.clear();
    
    for( unsigned i = 0; i < data.headOccurrences.size(); ++i )
    {
        NormalRule* rule = data.headOccurrences[ i ];
        assert( rule != NULL );
        if( rule->isRemoved() )
            continue;
        bodyToConstraint( rule );
        rule->remove();
    }
    data.numberOfHeadOccurrences = 0;
    data.headOccurrences.clear();

    for( unsigned i = 0; i < data.posOccurrences.size(); ++i )
    {
        NormalRule* rule = data.posOccurrences[ i ];
        assert( rule != NULL );
        removeAndCheckSupport( rule );
    }
    data.posOccurrences.clear();

    for( unsigned i = 0; i < data.negOccurrences.size(); ++i )
    {
        NormalRule* rule = data.negOccurrences[ i ];
        assert( rule != NULL );
        shrinkNeg( rule, var->getId() );
    }
    data.negOccurrences.clear();
}

void
GringoNumericFormat::bodyToConstraint(
    NormalRule* rule )
{
    trace_msg( parser, 3, "Replacing " << *rule << " by a constraint" );
    Clause* clause = solver.newClause( rule->size() );
    for( unsigned j = 0; j < rule->negBody.size(); ++j )
        clause->addLiteral( Literal( solver.getVariable( rule->negBody[ j ] ), POSITIVE ) );
    for( unsigned j = 0; j < rule->posBody.size(); ++j )
        clause->addLiteral( Literal( solver.getVariable( rule->posBody[ j ] ), NEGATIVE ) );
    for( unsigned j = 0; j < rule->doubleNegBody.size(); ++j )
        clause->addLiteral( Literal( solver.getVariable( rule->doubleNegBody[ j ] ), NEGATIVE ) );
    solver.cleanAndAddClause( clause );
}

void
GringoNumericFormat::propagateFact(
    Variable* var )
{
    assert( var->getId() < atomData.size() );
    AtomData& data = atomData[ var->getId() ];
    
    trace_msg( parser, 2, "Propagating fact " << *var );

    for( unsigned i = 0; i < data.headOccurrences.size(); ++i )
    {
        NormalRule* rule = data.headOccurrences[ i ];
        assert( rule != NULL );
        if( rule->isRemoved() )
            continue;
        trace_msg( parser, 3, "Removing rule " << *rule );
        rule->remove();
    }
    data.numberOfHeadOccurrences = 0;
    data.headOccurrences.clear();
    
    for( unsigned i = 0; i < data.posOccurrences.size(); ++i )
    {
        NormalRule* rule = data.posOccurrences[ i ];
        assert( rule != NULL );
        shrinkPos( rule, var->getId() );
    }
    data.posOccurrences.clear();
}

void
GringoNumericFormat::addFact(
    unsigned head )
{
    if( atomData[ head ].isSupported() )
        return;

    trace_msg( parser, 3, "Adding fact " << head );
    atomData[ head ].setSupported();
    solver.addClause( Literal( solver.getVariable( head ), POSITIVE ) );
    facts.push_back( head );
}

void
GringoNumericFormat::readAtomsTable(
    istream& input )
{
    unsigned int nextAtom;
    input >> nextAtom;

    createStructures( nextAtom );

    char name[ 1024 ];
    while( nextAtom != 0 )
    {
//        assert_msg( nextAtom < inputVarId.size(), "nextAtom = " << nextAtom << "; size = " << inputVarId.size() );
//        assert( inputVarId[ nextAtom ] > 1 );

        input.getline( name, 1024 );
        VariableNames::setName( solver.getVariable( nextAtom ), name+1 );
        trace_msg( parser, 6, "Set name " << name+1 << " for atom " << nextAtom );
        input >> nextAtom;
    }

//    #ifdef TRACE_ON
//    for( unsigned i = 1; i < inputVarId.size(); ++i )
//    {
//        Variable* variable = solver.getVariable( inputVarId[ i ] );
//        if( VariableNames::isHidden( variable ) )
//        {
//            stringstream s;
//            s << "#hidden" << i;
//            string name = s.str();
//            VariableNames::setName( variable, name );
//        }
//    }
//    for( unsigned i = 1; i < auxVarId.size(); ++i )
//    {
//        Variable* variable = solver.getVariable( auxVarId[ i ] );
//        if( VariableNames::isHidden( variable ) )
//        {
//            stringstream s;
//            s << "#aux" << i;
//            string name = s.str();
//            VariableNames::setName( variable, name );
//        }
//    }
//    #endif
}

void
GringoNumericFormat::readTrueAtoms(
    istream& input )
{
    char b;

    input >> b;
    assert( b == 'B' );
    input >> b;
    assert( b == '+' );

    unsigned int nextAtom;
    input >> nextAtom;

    createStructures( nextAtom );

    while( nextAtom != 0 )
    {
        cout << nextAtom << endl;
        solver.addClause( Literal( solver.getVariable( nextAtom ), POSITIVE ) );
        input >> nextAtom;
    }
}

void
GringoNumericFormat::readFalseAtoms(
    istream& input )
{
    char b;

    input >> b;
    assert( b == 'B' );
    input >> b;
    assert( b == '-' );

    unsigned int nextAtom;
    input >> nextAtom;

    createStructures( nextAtom );

    while( nextAtom != 0 )
    {
        solver.addClause( Literal( solver.getVariable( nextAtom ), NEGATIVE ) );
        input >> nextAtom;
    }
}

void
GringoNumericFormat::readErrorNumber(
    istream& input )
{
    unsigned int errorNumber;
    input >> errorNumber;

    if( errorNumber != 1 ) {
        stringstream ss;
        ss << "read error message number " << errorNumber;
        ErrorMessage::errorDuringParsing( ss.str() );
        exit( 0 );
    }
    else
    {
    }
}

void
GringoNumericFormat::processRecursivePositiveCrule(
    Clause* crule )
{
    assert( crule != NULL );
    assert( crule->getAt( 0 ).isPositive() );
    Variable* variable = crule->getAt( 0 ).getVariable();
    assert( variable->isInCyclicComponent() );

    trace_msg( parser, 2, "Creating GUS data structures for variable " << *variable << " whose supporting rule has " << crule->size()-1 << " literals" );
    variable->setFrozen();

    Component* component = variable->getComponent();
    assert( component != NULL );
    component->setAuxVariable( variable->getId() );

    for( unsigned int j = 1; j < crule->size(); j++ )
    {
        crule->getAt( j ).getVariable()->setFrozen();
        if( crule->getAt( j ).isNegative() )
        {
            if( crule->getAt( j ).getVariable()->inTheSameComponent( variable ) )
            {
                Literal lit = crule->getAt( j ).getOppositeLiteral();
                trace_msg( parser, 3, "Adding " << lit << " to the supporting rule of " << *variable );
                component->addAuxVariableSupportedByLiteral( variable, lit );
                component->addInternalLiteralForVariable( variable->getId(), lit );
            }
        }
    }
}

void
GringoNumericFormat::processRecursiveNegativeCrule(
    Clause* crule )
{
    assert( crule != NULL );
    assert( crule->getAt( 0 ).isNegative() );
    Variable* variable = crule->getAt( 0 ).getVariable();
    assert( variable->isInCyclicComponent() );

    trace_msg( parser, 2, "Creating GUS data structures for variable " << *variable << ", which has " << crule->size()-1 << " supporting rules" );

    Component* component = variable->getComponent();
    assert( component != NULL );

    for( unsigned int j = 1; j < crule->size(); j++ )
    {
        Variable* ruleVar = crule->getAt( j ).getVariable();
        ruleVar->setFrozen();
        if( literalsPostPropagator[ crule->getAt( j ).getSign() ][ ruleVar ].insert( component ).second )
            Literal( ruleVar, crule->getAt( j ).getSign() ).addPostPropagator( component );

        if( crule->getAt( j ).isPositive() && variable->inTheSameComponent( ruleVar ) )
        {
            trace_msg( parser, 3, "Adding " << *ruleVar << " as internal rule for " << *variable );
            component->addInternalLiteralForVariable( variable->getId(), Literal( ruleVar, POSITIVE ) );
            component->addVariablePossiblySupportedByLiteral( variable, Literal( ruleVar, POSITIVE ) );
        }
        else
        {
            trace_msg( parser, 3, "Adding " << crule->getAt( j ) << " as external rule for " << *variable );
            component->addExternalLiteralForVariable( variable->getId(), crule->getAt( j ) );
        }
    }    
}

void
GringoNumericFormat::computeGusStructures()
{
    //Add two fake positions
    solver.addGUSData( NULL );
    solver.addGUSData( NULL );
    for( unsigned int i = 2; i <= solver.numberOfVariables(); i++ )
    {
        GUSData* gd = new GUSData();
        gd->variable = solver.getVariable( i );
        solver.addGUSData( gd );
    }

    trace_msg( parser, 2, "Program is not tight. Number of cyclic components " << solver.getNumberOfCyclicComponents() );
    for( unsigned int i = 0; i < solver.getNumberOfCyclicComponents(); i++ )
    {
        Component* component = solver.getCyclicComponent( i );

        for( unsigned int j = 0; j < component->size(); j++ )
        {
            unsigned int varId = component->getVariable( j );
            assert( varId <= solver.numberOfVariables() );
            trace_msg( parser, 2, "Variable " << *solver.getVariable( varId ) << " is in the cyclic component " << i );
            Variable* currentVariable = solver.getVariable( varId );
            currentVariable->setComponent( component );
            component->variableHasNoSourcePointer( currentVariable );
        }

        solver.addPostPropagator( component );
    }

    for( unsigned int i = 0; i < crules.size(); i++ )
    {
        Clause* crule = crules[ i ];
        assert( crule != NULL );

        // skip acyclic variables
        if( !crule->getAt( 0 ).getVariable()->isInCyclicComponent() )
            continue;

        if( crule->getAt( 0 ).isPositive() )
            processRecursivePositiveCrule( crule );
        else
            processRecursiveNegativeCrule( crule );
    }
    
//    unsigned count = 0;
//    for( unsigned int i = 0; i < solver.getNumberOfCyclicComponents(); i++ )
//    {
//        bool found = false;
//        Component* component = solver.getCyclicComponent( i );
//        for( unsigned int j = 0; j < component->size(); j++ )
//        {
//            unsigned int varId = component->getVariable( j );
//            if( !component->isAuxVariable( varId ) )
//            {
//                cout << varId << endl;
//                found = true;
//                break;
//            }
//        }
//        if( found ) count++;
//    }
//    cout << count << " " << solver.getNumberOfCyclicComponents() << endl;
}

void
GringoNumericFormat::createStructures(
    unsigned id )
{
    while( id >= atomData.size() ) {
        solver.addVariable();
        solver.addEdgeInDependencyGraph( solver.numberOfVariables(), 0 );
        atomData.push_back( AtomData( false ) );
    }
}

void
GringoNumericFormat::simplify()
{
    trace_msg( parser, 1, "Simplify" );
    atomsWithSupportInference.clear();
    for( unsigned i = 2; i < atomData.size(); ++i )
    {
        if( atomData[ i ].isSupported() || solver.getVariable( i )->isFalse() )
            continue;
        if( atomData[ i ].numberOfHeadOccurrences == 0 || ( atomData[ i ].numberOfHeadOccurrences == 1 && solver.getVariable( i )->isTrue() ) )
            atomsWithSupportInference.push_back( i );
    }
    
    while( !atomsWithSupportInference.empty() )
    {
        AtomData& data = atomData[ atomsWithSupportInference.back() ];
        if( !data.isSupported() && !solver.getVariable( atomsWithSupportInference.back() )->isFalse() )
        {
            if( data.numberOfHeadOccurrences == 0 )
            {
                trace_msg( parser, 2, "Infer falsity of variable " << *solver.getVariable( atomsWithSupportInference.back() ) << " with no support" );
                solver.addClause( Literal( solver.getVariable( atomsWithSupportInference.back() ), NEGATIVE ) );
                assert( solver.getVariable( atomsWithSupportInference.back() )->isFalse() || solver.conflictDetected() );
            }
            else
            {
                assert( data.numberOfHeadOccurrences == 1 );
                assert( solver.getVariable( atomsWithSupportInference.back() )->isTrue() );
                assert( !data.isSupported() );
                
                for( unsigned i = 0; i < data.headOccurrences.size(); ++i )
                {
                    if( !data.headOccurrences[ i ]->isRemoved() )
                    {
                        data.headOccurrences[ 0 ] = data.headOccurrences[ i ];
                        break;
                    }
                }
                data.headOccurrences.resize( 1 );
                NormalRule* rule = data.headOccurrences[ 0 ];
                assert( !rule->isRemoved() );
                trace_msg( parser, 2, "Infer truth of the body of " << *rule << " (unique support of true head)" );
                for( unsigned i = 0; i < rule->posBody.size(); ++i )
                    solver.addClause( Literal( solver.getVariable( rule->posBody[ i ] ), POSITIVE ) );
                for( unsigned i = 0; i < rule->negBody.size(); ++i )
                    solver.addClause( Literal( solver.getVariable( rule->negBody[ i ] ), NEGATIVE ) );
                for( unsigned i = 0; i < rule->doubleNegBody.size(); ++i )
                    solver.addClause( Literal( solver.getVariable( rule->doubleNegBody[ i ] ), POSITIVE ) );
            }
        }
        atomsWithSupportInference.pop_back();
        propagate();
        if( solver.conflictDetected() )
            return;
    }
}

void
GringoNumericFormat::createCrule(
    Literal head,
    NormalRule* rule )
{
    assert( head.isPositive() );
    Clause* crule = solver.newClause( rule->size() + 1 );
    crule->addLiteral( head );
    for( unsigned k = 0; k < rule->negBody.size(); ++k )
        crule->addLiteral( Literal( solver.getVariable( rule->negBody[ k ] ), POSITIVE ) );
    for( unsigned k = 0; k < rule->posBody.size(); ++k )
    {
{'fraction_non_alphanumeric': 0.13489578139024633, 'fraction_numerical': 0.004547721152887205, 'mean_word_length': 2.1011319354240117, 'pattern_counts': {'":': 0, '<': 347, '<?xml version=': 0, '>': 379, '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': '3498004', 'n_tokens_mistral': 15881, 'n_tokens_neox': 15100, 'n_words': 3513}