// Module containing the main-function for standalone vallst. Vallst is a // boolean constraint solver. /* Copyright (C) 2004-2005 Daniel Vallstrom. All rights reserved. Unless explicitly acquired and licensed from Licensor under a license other than the Reciprocal Public License ("RPL"), the contents of this file are subject to the RPL Version 1.1, or subsequent versions as allowed by the RPL, and You may not copy or use this file in either source code or executable form, except in compliance with the terms and conditions of the RPL. You should be able to find a copy of the RPL (the "License") in a file named LICENSE that should come along with this file; if not, write to vallst@gmail.com. All software distributed under the License is provided in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the License for more details. */ #include "vallstAPI.h" #include "compilerMacros.h" #include <signal.h> #include <assert.h> #include <stdlib.h> // Sets up interupt handling. static void setupInteruptCallback( VallstInstance * vi ); static void printResult( VallstInstance * vi, VallstResult result ) { if ( vallst_getVerbosityVector(vi) & VallstVerbosity_printResult ) { fprintf( stdout, "result: " ); vallst_printVallstResult( stdout, result ); fprintf( stdout, "\n" ); } } // Used as a callback function for vallst_readInTheoryBody. static VallstFormulaName * newNamePtr( void * formulaNames, VallstInstance * vi attribute__(unused), bool * errorFlag ) { VallstFormulaNames * names = formulaNames; if ( names->nrOfNames == names->nrOfAllocatedNames ) { if ( vallst_extendFormulaNameArray(names) ) { *errorFlag = true; return NULL; } } assert( names->nrOfNames < names->nrOfAllocatedNames ); names->names[names->nrOfNames] = NULL; names->nrOfNames++; return names->names + names->nrOfNames - 1; } // Returns the position of the last constraint in 'names', or // VallstFormulaN_undef if there isn't any. static VallstFormulaN lastConstraintPos( VallstFormulaNames * names ) { for ( VallstFormulaN k = names->nrOfNames; k != 0; ) { k--; if ( vallst_isConstraint( names->names[k] ) ) { return k; } } return VallstFormulaN_undef; } // Returns the position of the previous constraint, modulo wraparounds. static VallstFormulaN prevConstraintPos( VallstFormulaNames * names, VallstFormulaN pos ) { assert( names->nrOfNames > 0 ); do { if ( pos == 0 ) { pos = names->nrOfNames - 1; } else { pos--; } } while ( ! vallst_isConstraint( names->names[pos] ) ); return pos; } // Returns the position of the next constraint, modulo wraparounds. static VallstFormulaN nextConstraintPos( VallstFormulaNames * names, VallstFormulaN pos ) { assert( names->nrOfNames > 0 ); do { pos = (pos+1) % names->nrOfNames; } while ( ! vallst_isConstraint( names->names[pos] ) ); return pos; } // Returns the number of constraint formulas in 'names'. static VallstFormulaN nrOfConstraints( VallstFormulaNames * names ) { VallstFormulaN nrOfCs = 0; // Accumulated number of constraints. for ( VallstFormulaN k = 0; k != names->nrOfNames; k++ ) { if ( vallst_isConstraint( names->names[k] ) ) { nrOfCs++; } } return nrOfCs; } // Returns the first constraint position. static VallstFormulaN fstConstraintPos( VallstFormulaNames * names ) { VallstFormulaN fstPos = 0; while ( ! vallst_isConstraint( names->names[fstPos] ) ) { fstPos++; } return fstPos; } // For each contraint constant c in names, prints c+i, where i is the // corresponding entry to c in incs. Position pos in names corresponds to // incs, prevConstraintPos( names, pos ) corresponds to incs+1 and so on. // nrOfCs is the number of constraints in names. static void printConsts( FILE * f, VallstFormulaNames * names, VallstLiteralN * incs, VallstFormulaN pos, VallstFormulaN nrOfCs ) { assert( nrOfCs >= 1 ); // The first contraint position in names. VallstFormulaN fstPos = fstConstraintPos(names); // Loop until the first position in names while keeping (indexes of) // names (k) and incs (j) synced. VallstFormulaN k = pos; // Position in names. VallstFormulaN j = 0; // Loop counter/corresponding incs position. while ( k != fstPos ) { j++; k = prevConstraintPos( names, k ); } // Print. if ( nrOfCs == 1 ) { fprintf( f, "Model found with constant:" ); } else { fprintf( f, "Model found with the following constants:\n" ); } do { assert( k != pos || j == 0 ); if ( vallst_formulaType( names->names[k] ) == VallstFormulaType_moreThanMult ) { VallstLiteralN c = vallst_getConst( names->names[k] ) + incs[j]; VallstLiteralN s = vallst_getTotalSum( names->names[k] ); fprintf( stdout, " %lu (%lu:>=*);", (unsigned long int) c, (unsigned long int) ( s - c - 1 ) ); } else { fprintf( f, " %lu;", (unsigned long int) ( vallst_getConst( names->names[k] ) + incs[j] ) ); } k = nextConstraintPos( names, k ); j = (j+1) % nrOfCs; } while ( k != fstPos ); putc( '\n', f ); } // Prints the constraint constant. static void printConst( VallstFormulaName a ) { if ( vallst_formulaType(a) == VallstFormulaType_moreThanMult ) { VallstLiteralN c = vallst_getConst(a); VallstLiteralN totalSum = vallst_getTotalSum(a); fprintf( stdout, " %lu (%lu:>=*);", (unsigned long int) c, (unsigned long int) ( totalSum - c - 1 ) ); } else { fprintf( stdout, " %lu;", (unsigned long int) vallst_getConst(a) ); } } int main( int argc, char * * argv ) { VallstInstance * vi = vallst_newInstance( 0, 0, VallstFormulaN_undef ); if ( vi == NULL ) { fprintf( stdout, "result: not enough memory (%u)\n", VallstResult_notEnoughMemory ); return VallstResult_notEnoughMemory; } // Set up the handling of interupt signals. setupInteruptCallback(vi); // Read the command line options. { VallstResult parseResult = vallst_parseCommandLineOptions( vi, argc, argv ); if ( parseResult <= VallstResult_other ) { if ( parseResult < VallstResult_other ) { printResult( vi, parseResult ); } return parseResult; } } // Read the head of the in-theory. VallstLiteralN pNrOfVars = vallst_readInTheoryHead(vi); if ( pNrOfVars == VallstLiteralN_parseError ) { printResult( vi, VallstResult_parseError ); return VallstResult_parseError; } if ( pNrOfVars == VallstLiteralN_fileError ) { printResult( vi, VallstResult_fileError ); return VallstResult_fileError; } if ( pNrOfVars == VallstLiteralN_noPrologueNrOfVars ) { if ( vallst_getNrOfVarsAllocated(vi) == 0 ) { // Set pNrOfVars to something arbitrary not too large. pNrOfVars = 40; } else { pNrOfVars = 0; } } if ( vallst_getVerbosityVector(vi) & VallstVerbosity_printEstimatedPrologues ) { vallst_printEstimatedPrologues( stdout, vi, pNrOfVars ); } // Allocate nrOfVars space. if ( vallst_extendNrOfVars( vi, pNrOfVars ) ) { printResult( vi, VallstResult_notEnoughMemory ); return VallstResult_notEnoughMemory; } if ( vallst_propagateNrOfLitOccsEstimate(vi) ) { printResult( vi, VallstResult_notEnoughMemory ); return VallstResult_notEnoughMemory; } if ( vallst_propagateNrOf3ClausesEstimate(vi) ) { printResult( vi, VallstResult_notEnoughMemory ); return VallstResult_notEnoughMemory; } // Names for min/max axioms. VallstFormulaNames * formulaNames = vallst_newFormulaNameArray(1); if ( formulaNames == NULL ) { printResult( vi, VallstResult_notEnoughMemory ); return VallstResult_notEnoughMemory; } // Read the body of the in-theory. { VallstResult result = vallst_readInTheoryBody( vi, pNrOfVars, newNamePtr, formulaNames ); switch ( result ) { case VallstResult_other: break; case VallstResult_other+1: if ( vallst_getVerbosityVector(vi) & VallstVerbosity_printResult || vallst_getVerbosityVector(vi) & VallstVerbosity_parseError ) { fprintf( stderr, "vallst error: the callback function " "supplied to\n" "vallst_readInTheoryBody returned an error.\n" "Aborting and returning " "VallstResult_notEnoughMemory.\n" ); } return VallstResult_notEnoughMemory; default: printResult( vi, result ); return result; } } // Close the in-theory file. vallst_closeInTheoryFile(vi); // Print various info. if ( vallst_getVerbosityVector(vi) & VallstVerbosity_printPrologues ) { vallst_printPrologues( stdout, vi ); } if ( vallst_getVerbosityVector(vi) & VallstVerbosity_printSettings ) { vallst_printSettings( stdout, vi, ' ' ); } if ( vallst_getVerbosityVector(vi) & VallstVerbosity_hashInfo ) { vallst_printHashInfo( stdout, vi ); } if ( vallst_getVerbosityVector(vi) & VallstVerbosity_hashDetails ) { // Note that this will only print things if NDEBUG isn't defined. vallst_hashStateCheck( stdout, vi, false ); } if ( vallst_getVerbosityVector(vi) & VallstVerbosity_printSeed ) { fprintf( stdout, "seed: %u\n", vallst_getSeed(vi) ); } if ( vallst_getVerbosityVector(vi) & VallstVerbosity_varsSet ) { vallst_printNrOfVarsSet( stdout, vi ); //vallst_printNrOfUncheckedVars( stdout, vi ); } #ifdef SaveSeedToFile // Save the seed. FILE * seedFile = fopen( "test/seedsUsed", "a" ); if ( seedFile == NULL ) { fprintf( stderr, "Warning: couldn't open or create file " "test/seedsUsed for saving the seed.\nContinuing...\n" ); } else { if ( fprintf( seedFile, "%u ", vallst_getSeed(vi) ) < 0 ) { fprintf( stderr, "Warning: couldn't write to file " "test/seedsUsed in order to save the seed.\n" "Continuing...\n" ); } fclose( seedFile ); } #endif // Do equ simplifications/substitutions. if ( vallst_getSubstEqus(vi) ) { unsigned char equSubstResult = vallst_substEqus(vi); if ( Unlikely( equSubstResult == 2 ) ) { printResult( vi, VallstResult_notEnoughMemory ); return VallstResult_notEnoughMemory; } if ( Unlikely( equSubstResult == 1 ) ) { printResult( vi, VallstResult_proofOfFalse ); return VallstResult_proofOfFalse; } } // Used for various calls returning VallstResult. VallstResult result; // Do general bcp based simplifications. result = vallst_simplifySlow(vi); if ( vallst_getVerbosityVector(vi) & VallstVerbosity_varsSet ) { vallst_printNrOfVarsSet( stdout, vi ); } if ( result == VallstResult_other || result == VallstResult_other+1 || result == VallstResult_timeLimitExceeded ) { result = vallst_search(vi); } printResult( vi, result ); // If the problem is to optimize something, do that. if ( lastConstraintPos(formulaNames) != VallstFormulaN_undef ) { VallstFormulaN pushedConstraintPos; // The constraint being pushed. if ( vallst_getBreadthFstOptStrat(vi) ) { pushedConstraintPos = 0; } else { pushedConstraintPos = lastConstraintPos(formulaNames); } VallstFormulaN nrOfNamedConstraints = nrOfConstraints(formulaNames); // Used for holding the amount to increase the constraint constants // with. VallstLiteralN * incs = malloc( sizeof(VallstLiteralN) * nrOfNamedConstraints ); if ( incs == NULL ) { printResult( vi, VallstResult_notEnoughMemory ); return VallstResult_notEnoughMemory; } if ( result != VallstResult_model && result != VallstResult_modelOfSearchAssumptions ) { if ( vallst_getVerbosityVector(vi) & VallstVerbosity_printResult || vallst_getVerbosityVector(vi) & VallstVerbosity_optimizeInfo ) { fprintf( stdout, "No model found at all.\n" ); if ( result == VallstResult_proofOfFalse || result == VallstResult_proofOfFalseGivenSearchAssumptions ) { fprintf( stdout, "Proof of false found with initial constants.\n" ); } } } else { while ( result == VallstResult_model || result == VallstResult_modelOfSearchAssumptions ) { // Suggest the current model to the next search in the hope // that a state close to the current one will be satisfying. // We do this suggestion here before any completion of the // model to avoid making the completion a suggestion. The // below vallst_maxConstraints call can cause completion. if ( vallst_makeCurrentAssumptionsSuggestions(vi) ) { printResult( vi, VallstResult_notEnoughMemory ); return VallstResult_notEnoughMemory; } if ( vallst_getBreadthFstOptStrat(vi) ) { // Switch the pushed constraint. pushedConstraintPos = prevConstraintPos( formulaNames, pushedConstraintPos ); } // Calculate the maximal constraint constants the current model // entails. if ( vallst_maxConstraints( vi, formulaNames, pushedConstraintPos, incs, NULL ) ) { printResult( vi, VallstResult_notEnoughMemory ); return VallstResult_notEnoughMemory; } // Print the current model in case we don't find any better. if ( vallst_getVerbosityVector(vi) & VallstVerbosity_printModel ) { vallst_printModel( vallst_getResultFile(vi), vi ); vallst_printAllGgcditTours( vallst_getResultFile(vi), vi ); } // Print constraint constant info. if ( vallst_getVerbosityVector(vi) & VallstVerbosity_optimizeInfo ) { printConsts( stdout, formulaNames, incs, pushedConstraintPos, nrOfNamedConstraints ); } vallst_moveToLevel0(vi); // Increment constraints. VallstFormulaName a; // Increment all non-pushed constants. { VallstLiteralN * cIncs = incs+1; for ( VallstFormulaN k = prevConstraintPos( formulaNames, pushedConstraintPos ); k != pushedConstraintPos; k = prevConstraintPos( formulaNames, k ), cIncs++ ) { if ( *cIncs != 0 ) { a = formulaNames->names[k]; if ( vallst_formulaType(a) == VallstFormulaType_moreThanMult && vallst_getKeepAboves(vi) ) { result = vallst_alterAxiomIncMTMKeepAboves ( vi, a, *cIncs ); } else { result = vallst_alterAxiomIncMT( vi, a, *cIncs ); } assert( result != VallstResult_parseError ); assert( result != VallstResult_proofOfFalse ); assert( result == VallstResult_other ); } } } // Increment the formula being pushed. a = formulaNames->names[pushedConstraintPos]; if ( vallst_formulaType(a) == VallstFormulaType_moreThanMult && vallst_getKeepAboves(vi) ) { result = vallst_alterAxiomIncMTMKeepAboves( vi, a, incs[0] + 1 ); } else { result = vallst_alterAxiomIncMT( vi, a, incs[0] + 1 ); } assert( result != VallstResult_parseError ); if ( result == VallstResult_proofOfFalse ) { break; } // Is this a good assertion? In the future, VallstResult_model // might be added to the possible return values? assert( result == VallstResult_other ); result = vallst_search(vi); } // while ( result == VallstResult_model || ... ) { ... // Print optimization results. if ( vallst_getVerbosityVector(vi) & VallstVerbosity_printResult || vallst_getVerbosityVector(vi) & VallstVerbosity_optimizeInfo ) { assert( nrOfNamedConstraints >= 1 ); if ( nrOfNamedConstraints == 1 ) { fprintf( stdout, "Model found with constant:" ); } else { fprintf( stdout, "Model found with the following " "constants:\n" ); } // The first contraint position in names. VallstFormulaN fstPos = fstConstraintPos(formulaNames); for ( VallstFormulaN k = fstPos; k != pushedConstraintPos; k = nextConstraintPos( formulaNames, k ) ) { printConst( formulaNames->names[k] ); } { VallstFormulaName a = formulaNames->names[pushedConstraintPos]; VallstLiteralN c = vallst_getConst( a ); assert( c >= 1 ); if ( vallst_formulaType(a) == VallstFormulaType_moreThanMult ) { VallstLiteralN totalSum = vallst_getTotalSum( a ); fprintf( stdout, "\n (pushed:) %lu (%lu:>=*)\n", (unsigned long int) ( c - 1 ), (unsigned long int) ( totalSum - c ) ); } else { fprintf( stdout, "\n (pushed:) %lu\n", (unsigned long int) ( c - 1 ) ); } } for ( VallstFormulaN k = nextConstraintPos( formulaNames, pushedConstraintPos ); k != fstPos; k = nextConstraintPos( formulaNames, k ) ) { printConst( formulaNames->names[k] ); } putc( '\n', stdout ); if ( result == VallstResult_proofOfFalse || result == VallstResult_proofOfFalseGivenSearchAssumptions ) { fprintf( stdout, "With an increment of the last pushed " "constant, a proof of false was found.\n" ); } else { fprintf( stdout, "No proof was found though that an " "increment of the\n" "last pushed constraint doesn't have a model.\n" ); } } // if ( vallst_getVerbosityVector(vi) & ... ) { ... } // if ( result != VallstResult_model && ... ) {...} else { ... printResult( vi, result ); } // if ( lastConstraintPos(formulaNames) != VallstFormulaN_undef ) {... else { if ( ( result == VallstResult_model || result == VallstResult_modelOfSearchAssumptions ) && vallst_getVerbosityVector(vi) & VallstVerbosity_printModel ) { vallst_printModel( vallst_getResultFile(vi), vi ); vallst_printAllGgcditTours( vallst_getResultFile(vi), vi ); } } if ( vallst_getVerbosityVector(vi) & VallstVerbosity_printSeed ) { fprintf( stdout, "seed: %u\n", vallst_getSeed(vi) ); } if ( vallst_getVerbosityVector(vi) & VallstVerbosity_varsSet ) { vallst_printNrOfVarsSet( stdout, vi ); //vallst_printNrOfUncheckedVars( stdout, vi ); } if ( vallst_getVerbosityVector(vi) & VallstVerbosity_time ) { vallst_printTimePassed( stdout, vi ); } // Possibly print the theory. if ( vallst_getPrintOutTheory(vi) && ( result == VallstResult_timeLimitExceeded || result == VallstResult_interupt ) ) { vallst_moveToLevel0(vi); vallst_printTheory( vi, formulaNames ); vallst_closeOutTheoryFile(vi); } // Possibly print the setting that might have changed. if ( vallst_getPrintChangingSetting(vi) && ( result == VallstResult_timeLimitExceeded || result == VallstResult_interupt ) ) { vallst_printChangingSetting(vi); vallst_closeChangingSettingFile(vi); } #ifdef SaveSeedToFile // Mark the end of the run in the seed file. seedFile = fopen( "test/seedsUsed", "a" ); if ( seedFile == NULL ) { fprintf( stderr, "Warning: couldn't open or create file " "test/seedsUsed for marking end of run.\nContinuing...\n" ); } else { if ( fprintf( seedFile, "end\n" ) < 0 ) { fprintf( stderr, "Warning: couldn't write to file test/seedsUsed " "in order to end-of-run mark it.\nContinuing...\n" ); } fclose( seedFile ); } #endif return result; } // Interupt handling. ---------------- // Is 0 iff an interupt signal hasn't been received. static volatile sig_atomic_t vallstStandAloneGlobalVariable_interuptSigReceived = 0; // Returns VallstCallbackResult_continue iff an interupt signal hasn't been // received and VallstCallbackResult_interupt iff an interupt signal has been // received. static VallstCallbackResult checkInteruptSignal( void * dummyArg attribute__(unused) ) { if ( vallstStandAloneGlobalVariable_interuptSigReceived == 0 ) { return VallstCallbackResult_continue; } else { return VallstCallbackResult_interupt; } } // Records that an interupt signal has been received. static void recordInterupt( int sig attribute__(unused) ) { vallstStandAloneGlobalVariable_interuptSigReceived = 1; } // Sets up interupt handling. static void setupInteruptCallback( VallstInstance * vi ) { signal( SIGINT, recordInterupt ); signal( SIGTERM, recordInterupt ); signal( SIGXCPU, recordInterupt ); vallst_setCallback( vi, checkInteruptSignal, NULL ); }
Generated on Mon Jul 18 11:34:15 2005 for Vallst by doxygen 1.4.3.