|
Data Structures |
| struct | VallstFormulaNames_ |
| | A dynamic array of type VallstFormulaName. More...
|
Formula types |
| #define | VallstFormulaType_clause (VallstLiteral_MAX-1) |
| #define | VallstFormulaType_equivalence (VallstLiteral_MAX-5) |
| #define | VallstFormulaType_negEquivalence (VallstLiteral_MAX-4) |
| #define | VallstFormulaType_moreThan (VallstLiteral_MAX-6) |
| #define | VallstFormulaType_moreThanDis (VallstLiteral_MAX-7) |
| #define | VallstFormulaType_moreThanMult (VallstLiteral_MAX-8) |
| #define | VallstFormulaType_ggcdiTour (VallstLiteral_MAX-9) |
| #define | VallstFormulaType_erased (VallstLiteral_MAX-10) |
Verbosity masks |
| #define | VallstVerbosity_varExtensionWarning ( (VallstVerbosityVector)1 << 0 ) |
| #define | VallstVerbosity_emptyClauseWarning ( (VallstVerbosityVector)1 << 1 ) |
| #define | VallstVerbosity_theoryMemNotice ( (VallstVerbosityVector)1 << 2 ) |
| #define | VallstVerbosity_searchDetails ( (VallstVerbosityVector)1 << 3 ) |
| #define | VallstVerbosity_printModel ( (VallstVerbosityVector)1 << 4 ) |
| #define | VallstVerbosity_parseError ( (VallstVerbosityVector)1 << 5 ) |
| #define | VallstVerbosity_lesserError ( (VallstVerbosityVector)1 << 6 ) |
| #define | VallstVerbosity_printResult ( (VallstVerbosityVector)1 << 7 ) |
| #define | VallstVerbosity_varsSet ( (VallstVerbosityVector)1 << 8 ) |
| #define | VallstVerbosity_printSeed ( (VallstVerbosityVector)1 << 9 ) |
| #define | VallstVerbosity_time ( (VallstVerbosityVector)1 << 10 ) |
| #define | VallstVerbosity_hashInfo ( (VallstVerbosityVector)1 << 11 ) |
| #define | VallstVerbosity_printSettings ( (VallstVerbosityVector)1 << 12 ) |
| #define | VallstVerbosity_printPrologues ( (VallstVerbosityVector)1 << 13 ) |
| #define | VallstVerbosity_printEstimatedPrologues ( (VallstVerbosityVector)1 << 14 ) |
| #define | VallstVerbosity_equConversionNotice ( (VallstVerbosityVector)1 << 15 ) |
| #define | VallstVerbosity_nonAxInfo ( (VallstVerbosityVector)1 << 16 ) |
| #define | VallstVerbosity_optimizeInfo ( (VallstVerbosityVector)1 << 17 ) |
| #define | VallstVerbosity_redundancyNotice ( (VallstVerbosityVector)1 << 18 ) |
| #define | VallstVerbosity_lesserHashError ( (VallstVerbosityVector)1 << 19 ) |
| #define | VallstVerbosity_simpProgressDetails ( (VallstVerbosityVector)1 << 22 ) |
| #define | VallstVerbosity_failedProofImprovementNotice ( (VallstVerbosityVector)1 << 23 ) |
| #define | VallstVerbosity_proofImprovementDetails ( (VallstVerbosityVector)1 << 24 ) |
| #define | VallstVerbosity_hashDetails ( (VallstVerbosityVector)1 << 25 ) |
| #define | VallstVerbosity_restartDetails ( (VallstVerbosityVector)1 << 26 ) |
| #define | VallstVerbosity_progressDetails ( (VallstVerbosityVector)1 << 27 ) |
| #define | VallstVerbosity_branchingDetails ( (VallstVerbosityVector)1 << 28 ) |
| #define | VallstVerbosity_midairPruneNotice ( (VallstVerbosityVector)1 << 29 ) |
| #define | VallstVerbosity_midairPruneDetails ( (VallstVerbosityVector)1 << 30 ) |
| #define | VallstVerbosity_ignoredContradictionNotice ( (VallstVerbosityVector)1 << 31 ) |
Problem types |
| #define | VallstProblemType_default 0 |
| #define | VallstProblemType_undef 1 |
| #define | VallstProblemType_atsp 2 |
| #define | VallstProblemType_tsp 3 |
| #define | VallstProblemType_pb 4 |
Defines |
| #define | VallstLiteral_MAX UINT32_MAX |
| #define | VallstFormulaN_MAX UINT32_MAX |
| #define | VallstLiteralN_noPrologueNrOfVars (VallstLiteral_MAX) |
| #define | VallstLiteralN_parseError (VallstLiteral_MAX-1) |
| #define | VallstLiteralN_fileError (VallstLiteral_MAX-2) |
| #define | VallstFormulaN_undef VallstFormulaN_MAX |
| #define | vallst_ggcditEdgeToLit(i, j, dim) ( 2 * ( ((dim)-1) * (i) + (j) + ((j)<(i)) ) ) |
| #define | vallst_ggcditLitToEdge(p, dim, i, j) |
| #define | vallst_ggcditLitToEdgeFst(p, dim) ( ( (p)/2 - 1 ) / ((dim)-1) ) |
Typedefs |
| typedef VallstInstance_ | VallstInstance |
| typedef uint32_t | VallstLiteral |
| typedef VallstLiteral | VallstLiteralN |
| typedef uint32_t | VallstFormulaN |
| typedef VallstLiteralN | VallstFormulaType |
| typedef uint64_t | VallstVerbosityVector |
| typedef void * | VallstFormulaName |
| typedef VallstFormulaNames_ | VallstFormulaNames |
Enumerations |
| enum | VallstResult {
VallstResult_proofOfFalse,
VallstResult_model,
VallstResult_timeLimitExceeded,
VallstResult_interupt,
VallstResult_notEnoughMemory,
VallstResult_fileError,
VallstResult_parseError,
VallstResult_proofOfFalseGivenSearchAssumptions,
VallstResult_modelOfSearchAssumptions,
VallstResult_other,
VallstResult_otherIntMax = INT_MAX
} |
| enum | VallstCallbackResult {
VallstCallbackResult_continue,
VallstCallbackResult_interupt
} |
Functions |
| VallstInstance * | vallst_newInstance (VallstLiteralN nrOfVars, VallstFormulaN nrOf3ClausesEstimate, VallstFormulaN nrOfLitOccsEstimate) |
| bool | vallst_propagateNrOf3ClausesEstimate (VallstInstance *vi) |
| bool | vallst_propagateNrOfLitOccsEstimate (VallstInstance *vi) |
| void | vallst_setFstNrOfLevelsAllocSize (VallstInstance *vi, VallstLiteralN size) |
| void | vallst_setMaxHashLoad (VallstInstance *vi, double maxLoad) |
| void | vallst_setNonAxChunkSizeAxDep (VallstInstance *vi, double value) |
| void | vallst_setNonAxChunkSizeConst (VallstInstance *vi, VallstFormulaN value) |
| void | vallst_setNonAxChunkSizeVarDep (VallstInstance *vi, double value) |
| void | vallst_setNrOf3ClausesEstimate (VallstInstance *vi, VallstFormulaN pNrOf3Clauses) |
| void | vallst_setNrOfFreeChunksCap (VallstInstance *vi, unsigned int cap) |
| void | vallst_setNrOfLitOccsEstimate (VallstInstance *vi, VallstFormulaN pNrOfLitOccs) |
| VallstResult | vallst_addAxiom (VallstInstance *vi, VallstLiteral *axiom, VallstLiteralN size, VallstFormulaType type) |
| VallstResult | vallst_addConsequence (VallstInstance *vi, VallstLiteral *nonAxiom, VallstLiteralN size, VallstFormulaType type) |
| VallstResult | vallst_addNamedAxiom (VallstInstance *vi, VallstLiteral *axiom, VallstLiteralN size, VallstFormulaType type, VallstFormulaName *namePtr) |
| VallstResult | vallst_alterAxiomIncMT (VallstInstance *vi, VallstFormulaName name, VallstLiteralN c) |
| VallstResult | vallst_alterAxiomIncMTMKeepAboves (VallstInstance *vi, VallstFormulaName name, VallstLiteralN c) |
| bool | vallst_extendNrOfVars (VallstInstance *vi, VallstLiteralN nrOfVars) |
| VallstFormulaType | vallst_formulaType (VallstFormulaName formulaName) |
| VallstLiteralN | vallst_getConst (VallstFormulaName name) |
| int | vallst_getFullLitValue (VallstInstance *vi, VallstLiteral p) |
| bool | vallst_getKeepAboves (VallstInstance *vi) |
| bool | vallst_getLitValue (VallstInstance *vi, VallstLiteral p) |
| VallstLiteralN | vallst_getNrOfVarsAllocated (VallstInstance *vi) |
| VallstLiteralN | vallst_getTotalSum (VallstFormulaName name) |
| bool | vallst_isConstraint (VallstFormulaName name) |
| bool | vallst_lessThanEqMultToMoreThanMult (VallstLiteral *a, VallstLiteralN size) |
| bool | vallst_lessThanEqToMoreThan (VallstLiteral *a, VallstLiteralN size) |
| VallstLiteral | vallst_neg (VallstLiteral p) |
| void | vallst_setKeepAboves (VallstInstance *vi, bool b) |
| void | vallst_setStartConst (VallstInstance *vi, VallstLiteralN c) |
| VallstLiteralN | vallst_sumOpenTrue (VallstInstance *vi, VallstFormulaName name) |
| VallstLiteralN | vallst_sumTrue (VallstInstance *vi, VallstFormulaName name) |
| VallstLiteralN | vallst_getAbortThreshold (VallstInstance *vi) |
| VallstLiteralN | vallst_getLevel (VallstInstance *vi) |
| unsigned int | vallst_getNoAbortTime (VallstInstance *vi) |
| bool | vallst_makeCurrentAssumptionsSuggestions (VallstInstance *vi) |
| VallstResult | vallst_makeSearchAssumption (VallstInstance *vi, VallstLiteral p) |
| void | vallst_moveToLevel0 (VallstInstance *vi) |
| void | vallst_removeAssumptions (VallstInstance *vi) |
| void | vallst_removeLastAssumption (VallstInstance *vi) |
| VallstResult | vallst_search (VallstInstance *vi) |
| void | vallst_setAbortThreshold (VallstInstance *vi, VallstLiteralN n) |
| void | vallst_setBufferResetFrequency (VallstInstance *vi, VallstFormulaN freq) |
| void | vallst_setBufferSizeConst (VallstInstance *vi, VallstFormulaN value) |
| void | vallst_setBufferSizeNonAxDep (VallstInstance *vi, double value) |
| void | vallst_setBufferSizeVarDep (VallstInstance *vi, double value) |
| void | vallst_setCCLeeway (VallstInstance *vi, double ccLeeway) |
| void | vallst_setCreatePhantomConflictClauses (VallstInstance *vi, bool b) |
| void | vallst_setFirstRestart (VallstInstance *vi, VallstFormulaN n) |
| void | vallst_setGoodClauseSize (VallstInstance *vi, VallstFormulaN size) |
| void | vallst_setGoodLevel (VallstInstance *vi, VallstFormulaN size) |
| void | vallst_setHeurAxSize (VallstInstance *vi, VallstFormulaN size) |
| void | vallst_setImproveProofLevel (VallstInstance *vi, VallstLiteralN lvl) |
| void | vallst_setKeepCCMetaMetaThreshold (VallstInstance *vi, VallstLiteralN threshold) |
| void | vallst_setKeepConflictClauseLengthThreshold (VallstInstance *vi, VallstLiteralN threshold) |
| void | vallst_setLitPairStrFunc (VallstInstance *vi, double(*litPairStrFunc)(double *varStrPtr), long double(*litPairStrFuncl)(long double *varStrPtr)) |
| void | vallst_setLooseTheorySizeLeeway (VallstInstance *vi, double leeway) |
| void | vallst_setNoAbortTime (VallstInstance *vi, unsigned int secs) |
| void | vallst_setTightTheorySizeLeeway (VallstInstance *vi, double leeway) |
| void | vallst_setLooseTheoryMetaSizeLeeway (VallstInstance *vi, double leeway) |
| void | vallst_setTightTheoryMetaSizeLeeway (VallstInstance *vi, double leeway) |
| void | vallst_setLooseTheorySizeLeewayKeep (VallstInstance *vi, double leeway) |
| void | vallst_setTightTheorySizeLeewayKeep (VallstInstance *vi, double leeway) |
| void | vallst_setLooseTimeLimitBase (VallstInstance *vi, unsigned int k) |
| void | vallst_setLooseTimeLimitMod (VallstInstance *vi, unsigned int k) |
| void | vallst_setTightTimeLimitBase (VallstInstance *vi, unsigned int k) |
| void | vallst_setTightTimeLimitMod (VallstInstance *vi, unsigned int k) |
| void | vallst_setMaxSkippedSimps (VallstInstance *vi, VallstFormulaN size) |
| void | vallst_setMetaMetaPruneEnd (VallstInstance *vi, VallstLiteralN end) |
| void | vallst_setMetaMetaPruneFrequency (VallstInstance *vi, VallstFormulaN freq) |
| void | vallst_setMetaMetaPruneStart (VallstInstance *vi, VallstLiteralN start) |
| void | vallst_setMetaPruneEnd (VallstInstance *vi, VallstLiteralN end) |
| void | vallst_setMetaPruneFrequency (VallstInstance *vi, VallstFormulaN freq) |
| void | vallst_setMetaPruneStart (VallstInstance *vi, VallstLiteralN start) |
| void | vallst_setNextBatchSizeConst (VallstInstance *vi, double value) |
| void | vallst_setPositiveHeurAxSign (VallstInstance *vi, bool b) |
| void | vallst_setPositiveSign (VallstInstance *vi, bool b) |
| void | vallst_setRandomBranchSign (VallstInstance *vi, unsigned int prob) |
| void | vallst_setRandomFormulaLit (VallstInstance *vi, unsigned int prob) |
| void | vallst_setRemoveTmpCauses (VallstInstance *vi, bool b) |
| void | vallst_setResetBuffersBetweenSearches (VallstInstance *vi, bool b) |
| void | vallst_setRestartFunc (VallstInstance *vi, VallstFormulaN(*restartSizeFunc)(VallstInstance *vi, VallstFormulaN lastSize, VallstFormulaN nrOfRestarts)) |
| bool | vallst_setRestartPredefFunc (VallstInstance *vi, unsigned char f) |
| void | vallst_setRestartProlongCap (VallstInstance *vi, double cap) |
| void | vallst_setRestartStart (VallstInstance *vi, VallstFormulaN size) |
| void | vallst_setStartWithBinFstBcp (VallstInstance *vi, bool b) |
| void | vallst_setStrengthLeeway (VallstInstance *vi, double leeway) |
| void | vallst_setStrengthLeewayFormula (VallstInstance *vi, double leeway) |
| void | vallst_setStrengthLeewaySize (VallstInstance *vi, VallstFormulaN leewaySize) |
| void | vallst_setStrengthLeewaySizeFormula (VallstInstance *vi, VallstFormulaN leewaySize) |
| void | vallst_setTightCCLeeway (VallstInstance *vi, double leeway) |
| void | vallst_setTightKeepCCThreshold (VallstInstance *vi, VallstLiteralN threshold) |
| void | vallst_setTightMetaMetaPruneEnd (VallstInstance *vi, VallstLiteralN end) |
| void | vallst_setTightMetaMetaPruneStart (VallstInstance *vi, VallstLiteralN start) |
| void | vallst_setTightMetaPruneStart (VallstInstance *vi, VallstLiteralN start) |
| void | vallst_setUseDoppelganger (VallstInstance *vi, bool b) |
| bool | vallst_getSubstEqus (VallstInstance *vi) |
| void | vallst_setConvert3ClausesIntoEqus (VallstInstance *vi, bool b) |
| void | vallst_setSimpTimeLimitFast (VallstInstance *vi, unsigned int ms) |
| void | vallst_setSimpTimeLimitSlow (VallstInstance *vi, unsigned int ms) |
| bool | vallst_setSimpSetting (VallstInstance *vi, VallstLiteralN level, VallstLiteralN sublevel, VallstLiteralN nrOfVars, VallstLiteralN nrOfIterations) |
| bool | vallst_setSimpSettingSlow (VallstInstance *vi, VallstLiteralN level, VallstLiteralN sublevel, VallstLiteralN nrOfVars, VallstLiteralN nrOfIterations) |
| VallstResult | vallst_simplify (VallstInstance *vi) |
| VallstResult | vallst_simplifySlow (VallstInstance *vi) |
| void | vallst_setSubstEqus (VallstInstance *vi, bool b) |
| unsigned char | vallst_substEqus (VallstInstance *vi) |
| bool | vallst_closeInTheoryFile (VallstInstance *vi) |
| FILE * | vallst_getInTheoryFile (VallstInstance *vi) |
| char * | vallst_getInTheoryFileName (VallstInstance *vi) |
| unsigned char | vallst_getProblemType (VallstInstance *vi) |
| VallstResult | vallst_parseCommandLineOptions (VallstInstance *vi, int argC, char **argV) |
| VallstResult | vallst_readInTheoryBody (VallstInstance *vi, VallstLiteralN pNrOfVars, VallstFormulaName *(*newNamePtrFunc)(void *newNamePtrFuncArg, VallstInstance *vi, bool *errorFlag), void *newNamePtrFuncArg) |
| VallstLiteralN | vallst_readInTheoryHead (VallstInstance *vi) |
| void | vallst_setIgnorePrologue (VallstInstance *vi, bool b) |
| void | vallst_setInTheoryFile (VallstInstance *vi, FILE *f) |
| void | vallst_setInTheoryFileName (VallstInstance *vi, char *fileName) |
| void | vallst_setPBVarPrefixChar (VallstInstance *vi, bool b) |
| void | vallst_setProblemType (VallstInstance *vi, unsigned char type) |
| void | vallst_setVarMapFile (VallstInstance *vi, FILE *f) |
| void | vallst_setVarMapFileName (VallstInstance *vi, char *fileName) |
| bool | vallst_closeChangingSettingFile (VallstInstance *vi) |
| bool | vallst_closeOutTheoryFile (VallstInstance *vi) |
| FILE * | vallst_getChangingSettingFile (VallstInstance *vi) |
| char * | vallst_getChangingSettingFileName (VallstInstance *vi) |
| bool | vallst_getCompleteModel (VallstInstance *vi) |
| FILE * | vallst_getOutTheoryFile (VallstInstance *vi) |
| char * | vallst_getOutTheoryFileName (VallstInstance *vi) |
| bool | vallst_getPrintChangingSetting (VallstInstance *vi) |
| bool | vallst_getPrintOutTheory (VallstInstance *vi) |
| FILE * | vallst_getResultFile (VallstInstance *vi) |
| char * | vallst_getResultFileName (VallstInstance *vi) |
| VallstVerbosityVector | vallst_getVerbosityVector (VallstInstance *vi) |
| void | vallst_hashStateCheck (FILE *f, VallstInstance *vi, bool forcePrint) |
| bool | vallst_printAllGgcditTours (FILE *f, VallstInstance *vi) |
| bool | vallst_printChangingSetting (VallstInstance *vi) |
| void | vallst_printChangingSettingToFile (VallstInstance *vi, FILE *file) |
| void | vallst_printEstimatedPrologues (FILE *f, VallstInstance *vi, VallstLiteralN pNrOfVars) |
| bool | vallst_printGgcditTour (FILE *f, VallstInstance *vi, VallstFormulaName a) |
| void | vallst_printHashInfo (FILE *f, VallstInstance *vi) |
| void | vallst_printModel (FILE *file, VallstInstance *vi) |
| void | vallst_printNrOfUncheckedVars (FILE *f, VallstInstance *vi) |
| void | vallst_printNrOfVarsSet (FILE *f, VallstInstance *vi) |
| void | vallst_printPrologues (FILE *f, VallstInstance *vi) |
| void | vallst_printSettings (FILE *f, VallstInstance *vi, char sep) |
| bool | vallst_printTheory (VallstInstance *vi, VallstFormulaNames *optMax) |
| void | vallst_printTheoryToFile (VallstInstance *vi, FILE *file, VallstFormulaNames *optMax) |
| void | vallst_printTimePassed (FILE *f, VallstInstance *vi) |
| void | vallst_printVallstResult (FILE *f, VallstResult result) |
| void | vallst_setChangingSettingFile (VallstInstance *vi, FILE *f) |
| void | vallst_setChangingSettingFileName (VallstInstance *vi, char *fileName) |
| void | vallst_setCompleteModel (VallstInstance *vi, bool b) |
| void | vallst_setOutTheoryFile (VallstInstance *vi, FILE *f) |
| void | vallst_setOutTheoryFileName (VallstInstance *vi, char *fileName) |
| void | vallst_setPrintChangingSetting (VallstInstance *vi, bool b) |
| void | vallst_setPrintOutTheory (VallstInstance *vi, bool b) |
| void | vallst_setResultFile (VallstInstance *vi, FILE *f) |
| void | vallst_setResultFileName (VallstInstance *vi, char *fileName) |
| void | vallst_setVerbosityLevel (VallstInstance *vi, unsigned int vl) |
| void | vallst_setVerbosityVector (VallstInstance *vi, VallstVerbosityVector vv) |
| void | vallst_setCallback (VallstInstance *vi, VallstCallbackResult(*callbackFunc)(void *callbackArg), void *callbackArg) |
| bool | vallst_extendFormulaNameArray (VallstFormulaNames *names) |
| VallstFormulaNames * | vallst_newFormulaNameArray (VallstFormulaN n) |
| bool | vallst_getBreadthFstOptStrat (VallstInstance *vi) |
| bool | vallst_maxConstraints (VallstInstance *vi, VallstFormulaNames *names, VallstFormulaN pushedConstraintPos, VallstLiteralN *constraintIncs, bool *levelCreated) |
| void | vallst_setBreadthFstOptStrat (VallstInstance *vi, bool b) |
| unsigned int | vallst_getSeed (VallstInstance *vi) |
| void | vallst_setSeed (VallstInstance *vi, unsigned int seed) |
| void | vallst_setTimeLimitInMilliSec (VallstInstance *vi, long long int milliSec, bool startFromCurrentClock) |
| void | vallst_setTimeLimitInSec (VallstInstance *vi, unsigned int sec, bool startFromCurrentClock) |