vallstAPI.h

Go to the documentation of this file.

/*!\file
  Vallst's API.
  Vallst is a boolean constraint solver.

  See \ref VallstApiFuncsGrouped for a list of all API functions grouped into
  categories.
*/
// (A comment marked with '!' is a doxygen comment and '\x' is a doxygen
//  command. This is for generating documentation.)



/*
    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.
*/



/*! \page VallstApiFuncsGrouped API functions grouped
    Here is a list of all API functions grouped into categories.


\section allocSec Allocation

 - vallst_deleteInstance()       -- Deletes a vallst instance.
 - vallst_extendNrOfVars()       -- Extends the number of variables ready to be
                                    used.
 - vallst_newInstance()          -- Creates a new vallst problem instance.
 - vallst_propagateNrOf3ClausesEstimate()
                                 -- Propagates value.
 - vallst_propagateNrOfLitOccsEstimate()
                                 -- Propagates value.
 - vallst_setFstNrOfLevelsAllocSize()
                                 -- Sets flag.
 - vallst_setMaxHashLoad()       -- Sets max load.
 - vallst_setNonAxChunkSizeAxDep()
                                 -- Sets value.
 - vallst_setNonAxChunkSizeConst()
                                 -- Sets value.
 - vallst_setNonAxChunkSizeVarDep()
                                 -- Sets value.
 - vallst_setNrOf3ClausesEstimate()
                                 -- Sets the number of ternary clauses
                                    estimate.
 - vallst_setNrOfFreeChunksCap() -- Sets cap.
 - vallst_setNrOfLitOccsEstimate()
                                 -- Sets estimate of the number of literal
                                    occurrences, modulo special accounting.


\section formulasSec Formulas and variables

 - vallst_addAxiom()             -- Adds an axiom.
 - vallst_addConsequence()       -- Adds a formula that should be a consequence
                                    of the axioms since the formula might be
                                    removed.
 - vallst_addNamedAxiom()        -- Adds a named axiom.
 - vallst_alterAxiomIncMT()      -- Adds to the constant in a more-than* axiom.
 - vallst_alterAxiomIncMTMKeepAboves()
                                 -- Adds to the constant in a <*-axiom keeping
                                    "aboves".
 - vallst_extendNrOfVars()       -- Extends the number of variables ready to be
                                    used.
 - vallst_formulaType()          -- Returns the type given a formula name.
 - vallst_getConst()             -- Returns the constant in a constraint.
 - vallst_getFullLitValue()      -- Returns the full status of a literal.
 - vallst_getKeepAboves()        -- Returns the keep-aboves flag.
 - vallst_getLitValue()          -- Returns the status of a literal.
 - vallst_getNrOfVarsAllocated() -- Returns the number of vars allocated for.
 - vallst_getTotalSum()          -- Returns the sum of the literal constants in
                                    a more-than-mult (<*) formula.
 - vallst_isConstraint()         -- Returns true iff a name is a constraint.
 - vallst_lessThanEqMultToMoreThanMult()
                                 -- Tranforms a >=*-formula into a <*-formula.
 - vallst_lessThanEqToMoreThan() -- Tranforms a >=-formula  into a <-formula.
 - vallst_neg()                  -- Returns the negation of a literal.
 - vallst_newVar()               -- Returns a new variable ready to be used.
 - vallst_setKeepAboves()        -- Sets flag.
 - vallst_setStartConst()        -- Sets value.
 - vallst_sumOpenTrue()          -- Sums up true and open lits in a constraint.
 - vallst_sumTrue()              -- Sums up true          lits in a constraint.


\section searchSec Search

 - vallst_getAbortThreshold()    -- Returns nr of vars set to abort value.
 - vallst_getLevel()             -- Returns the current search level.
 - vallst_getNoAbortTime()       -- Returns time limit for no aborts.
 - vallst_makeCurrentAssumptionsSuggestions()
                                 -- Sets suggestions.
 - vallst_makeSearchAssumption() -- Makes a search assumption.
 - vallst_moveToLevel0()         -- Moves the current search state to level 0.
 - vallst_removeAssumptions()    -- Removes all search assumptions.
 - vallst_removeLastAssumption() -- Removes the last search assumption.
 - vallst_search()               -- Searches for a proof of false or a model.
 - vallst_setAbortThreshold()    -- Sets nr of vars set to abort.
 - vallst_setBufferResetFrequency()
                                 -- Sets the frequency.
 - vallst_setBufferSizeConst()   -- Sets value.
 - vallst_setBufferSizeNonAxDep()
                                 -- Sets value.
 - vallst_setBufferSizeVarDep()  -- Sets value.
 - vallst_setCCLeeway()          -- Sets proof improvement leeway.
 - vallst_setCreatePhantomConflictClauses()
                                 -- Sets the create-phantom-conflict-clauses
                                    flag.
 - vallst_setFirstRestart()      -- Sets the base/initial restart size.
 - vallst_setFstNrOfLevelsAllocSize()
                                 -- Sets flag.
 - vallst_setGoodClauseSize()    -- Sets what's to be considered good.
 - vallst_setGoodLevel()         -- Sets what's to be considered good.
 - vallst_setHeurAxSize()        -- Sets size.
 - vallst_setImproveProofLevel() -- Sets level threshold.
 - vallst_setKeepCCMetaMetaThreshold()
                                 -- Sets threshold.
 - vallst_setKeepConflictClauseLengthThreshold()
                                 -- Sets threshold.
 - vallst_setLooseTheoryMetaSizeLeeway()
                                 -- Set meta leeway used in loose mode.
 - vallst_setLooseTheorySizeLeeway()
                                 -- Set meta meta leeway used in loose mode.
 - vallst_setLooseTheorySizeLeewayKeep()
                                 -- Set leeway used in loose mode.
 - vallst_setLooseTimeLimitBase()
                                 -- Sets mode limit parameter.
 - vallst_setLooseTimeLimitMod() -- Sets mode limit parameter.
 - vallst_setMaxSkippedSimps()   -- Sets max skipped search simplifications.
 - vallst_setMetaMetaPruneEnd()  -- Sets the value.
 - vallst_setMetaMetaPruneFrequency()
                                 -- Sets the frequency.
 - vallst_setMetaMetaPruneStart()
                                 -- Sets the value.
 - vallst_setMetaPruneEnd()      -- Sets the value.
 - vallst_setMetaPruneFrequency()
                                 -- Sets the frequency.
 - vallst_setMetaPruneStart()    -- Sets the value.
 - vallst_setNextBatchSizeConst()
                                 -- Sets value.
 - vallst_setNoAbortTime()       -- Sets time limit for no aborts.
 - vallst_setPositiveHeurAxSign()
                                 -- Sets value.
 - vallst_setPositiveSign()      -- Sets value.
 - vallst_setPruningFunction()   -- Sets the pruning function.
 - vallst_setRandomBranchSign()  -- Sets random sign choice likelihood.
 - vallst_setRandomFormulaLit()  -- Sets random formula lit choice likelihood.
 - vallst_setRemoveTmpCauses()   -- Sets this flag.
 - vallst_setResetBuffersBetweenSearches()
                                 -- Sets flag.
 - vallst_setRestartFunc()       -- Sets restart batch size function.
 - vallst_setRestartPredefFunc() -- Chooses a predef. restart batch size
                                    function.
 - vallst_setRestartProlongCap() -- Sets cap.
 - vallst_setRestartStart()      -- Sets the start phase size.
 - vallst_setStartWithBinFstBcp()
                                 -- Sets flag.
 - vallst_setStrengthLeeway()    -- Sets the heuristic strength leeway.
 - vallst_setStrengthLeewayFormula()
                                 -- Sets the heuristic strength leeway for
                                    formulas.
 - vallst_setStrengthLeewaySize()
                                 -- Sets a hard strength leeway space size cap.
 - vallst_setStrengthLeewaySizeFormula()
                                 -- Sets a hard strength leeway space size cap
                                    for formulas.
 - vallst_setTightCCLeeway()     -- Sets tight proof improvement leeway.
 - vallst_setTightKeepCCThreshold()
                                 -- Set value used in tight mode.
 - vallst_setTightMetaMetaPruneEnd()
                                 -- Set value used in tight mode.
 - vallst_setTightMetaMetaPruneStart()
                                 -- Set value used in tight mode.
 - vallst_setTightMetaPruneStart()
                                 -- Set value used in tight mode.
 - vallst_setTightTheoryMetaSizeLeeway()
                                 -- Set meta leeway used in tight mode.
 - vallst_setTightTheorySizeLeeway()
                                 -- Set meta meta leeway used in tight mode.
 - vallst_setTightTheorySizeLeewayKeep()
                                 -- Set leeway used in tight mode.
 - vallst_setTightTimeLimitBase()
                                 -- Sets mode limit parameter.
 - vallst_setTightTimeLimitMod() -- Sets mode limit parameter.
 - vallst_setUseDoppelganger()   -- Sets flag.


\section simpSec Simplification

 - vallst_compactifyVars()       -- Removes gaps in the variables.
 - vallst_getSubstEqus()         -- Returns flag.
 - vallst_permuteVars()          -- Permute the variables moving related
                                    variables closer together.
 - vallst_pruneTheory()          -- Prunes the theory.
 - vallst_setConvert3ClausesIntoEqus()
                                 -- Sets the convert-3-clauses flag.
 - vallst_setSimpTimeLimitFast() -- Sets time limit for fast simplifications.
 - vallst_setSimpTimeLimitSlow() -- Sets time limit for slow simplifications.
 - vallst_setSimpSetting()       -- Setting for main bcp based fast
                                    simplification.
 - vallst_setSimpSettingSlow()   -- Setting for main bcp based slow
                                    simplification.
 - vallst_setSubstEqus()         -- Sets flag.
 - vallst_simplify()             -- Simplifies the problem fast. BCP based.
 - vallst_simplifySlow()         -- Simplifies the problem slow. BCP based.
 - vallst_substEqus()            -- Substitutes vars p<->a in equivalences.


\section symSec Symmetry detection

 - vallst_symmetrySearch()       -- Searches for symmetries.


\section parsingSec Parsing

 - vallst_closeInTheoryFile()    -- Closes the in-theory file.
 - vallst_getInTheoryFile()      -- Returns the in-theory file.
 - vallst_getInTheoryFileName()  -- Returns the in-theory file name.
 - vallst_setPBVarPrefixChar()   -- Sets flag.
 - vallst_getProblemType         -- Returns the problem type.
 - vallst_parseCommandLineOptions()
                                 -- Parses options.
 - vallst_readInTheoryBody()     -- Reads the body of the in-theory.
 - vallst_readInTheoryHead()     -- Reads the head (i.e. the prologue) of the
                                    in-theory.
 - vallst_setIgnorePrologue()    -- Sets the ignore-prologue flag.
 - vallst_setInTheoryFile()      -- Sets the in-theory file.
 - vallst_setInTheoryFileName()  -- Sets the in-theory file name.
 - vallst_setProblemType         -- Sets the problem type.
 - vallst_setVarMapFile()        -- Sets the pb variable map file.
 - vallst_setVarMapFileName()    -- Sets the pb variable map file name.


\section printSec Printing

 - vallst_closeChangingSettingFile()
                                 -- Closes the changing-setting file.
 - vallst_closeOutTheoryFile()   -- Closes the out-theory file.
 - vallst_getChangingSettingFile()
                                 -- Returns the changing-setting file.
 - vallst_getChangingSettingFileName()
                                 -- Returns the changing-setting file name.
 - vallst_getCompleteModel()     -- Returns the complete-model flag.
 - vallst_getOutTheoryFile()     -- Returns the out-theory file.
 - vallst_getOutTheoryFileName() -- Returns the out-theory file name.
 - vallst_getPrintChangingSetting()
                                 -- Returns the print-changing-setting flag.
 - vallst_getPrintOutTheory()    -- Returns the print-out-theory flag.
 - vallst_getResultFile()        -- Returns the result file.
 - vallst_getResultFileName()    -- Returns the result file name.
 - vallst_getVerbosityVector()   -- Returns the verbosity vector.
 - vallst_hashStateCheck()       -- Prints detailed hash info.
 - vallst_printAllGgcditTours()  -- Prints all ggcdit tours.
 - vallst_printChangingSetting() -- Prints changing settings.
 - vallst_printChangingSettingToFile()
                                 -- Prints changing settings to supplied file.
 - vallst_printEstimatedPrologues()
                                 -- Prints estimated prologue values.
 - vallst_printGgcditTour()      -- Prints a tour.
 - vallst_printHashInfo()        -- Prints easily obtainable hash info.
 - vallst_printModel()           -- Prints the current value of variables.
 - vallst_printNrOfUncheckedVars()
                                 -- Prints nr of unchecked vars.
 - vallst_printNrOfVarsSet()     -- Prints nr of vars set.
 - vallst_printOpenTheory()      -- Prints the current theory but without the
                                    variable history.
 - vallst_printPrologues()       -- Prints hindsighted prologue values.
 - vallst_printSettings()        -- Prints option settings.
 - vallst_printTheory()          -- Prints the current theory.
 - vallst_printTheoryToFile()    -- Prints the theory to a supplied file.
 - vallst_printTimePassed()      -- Prints the cpu time used.
 - vallst_printVallstResult()    -- Prints a short string corresponding to a
                                    VallstResult.
 - vallst_printVarHistory()      -- Prints the variable history.
 - vallst_setChangingSettingFile()
                                 -- Sets the changing-setting file.
 - vallst_setChangingSettingFileName()
                                 -- Sets the changing-setting file name.
 - vallst_setCompleteModel()     -- Sets the complete-model flag.
 - vallst_setOutTheoryFile()     -- Sets the out-theory file.
 - vallst_setOutTheoryFileName() -- Sets the out-theory file name.
 - vallst_setPrintChangingSetting()
                                 -- Sets the print-changing-setting flag.
 - vallst_setPrintOutTheory()    -- Sets the print-out-theory flag.
 - vallst_setResultFile()        -- Sets the result file.
 - vallst_setResultFileName()    -- Sets the result file name.
 - vallst_setVerbosityLevel()    -- Sets the verbosity level.
 - vallst_setVerbosityVector()   -- Sets the verbosity vector.


\section callbackSec Callback

 - vallst_setCallback()          -- Sets the callback function.


\section nameAllocSec Formula name allocation

 - vallst_extendFormulaNameArray()
                                 -- Extends a name array.
 - vallst_newFormulaNameArray()  -- Returns a new formula name array.


\section graphCodingSec Graph coding

 - vallst_ggcditEdgeToLit()      -- Maps an (i,j) edge to a vallst literal.
 - vallst_ggcditLitToEdge()      -- Maps a literal to the corresponding edge.
 - vallst_ggcditLitToEdgeFst()   -- Maps a literal to first node of edge.


\section optimizationSec Optimization

 - vallst_getBreadthFstOptStrat()
                                 -- Returns the optimization strategy flag.
 - vallst_maxConstraints()       -- Maximizes constraint constants.
 - vallst_setBreadthFstOptStrat()
                                 -- Sets the optimization strategy flag.


\section seedSec Seed

 - vallst_getSeed()              -- Gets the seed used.
 - vallst_setSeed()              -- Sets the seed.


\section timerSec Timers

 - vallst_setTimeLimitInMilliSec()
                                 -- Sets the overall time limit in
                                    milliseconds.
 - vallst_setTimeLimitInSec()    -- Sets the overall time limit in seconds.


*/



#ifndef vallstAPI_H
#define vallstAPI_H


#ifdef __cplusplus
extern "C"
{
#endif


#include <stdint.h>
#include <stdbool.h>
#include <limits.h>
#include <stdio.h>
#include <time.h>



// Types. -------------------------------------------------------------


//! The main structure containing everything.
typedef struct VallstInstance_ VallstInstance;

/*! The type for literals. 2, 3, 4, ... are literals.

      (If you want you can change this to e.g. uint16_t. See note in
    vallstTypes.h.)
*/
typedef uint32_t VallstLiteral;

//! The maximum value of the type VallstLiteral
#define VallstLiteral_MAX UINT32_MAX

//! A type for counting literals.
typedef VallstLiteral VallstLiteralN;

//! A type for counting formulas.
typedef uint32_t VallstFormulaN;

//! The maximum value of the type VallstFormulaN
#define VallstFormulaN_MAX UINT32_MAX



// Some special values with special meaning.

//! No prologue nrOfVars was present. This is not treated as an error.
#define VallstLiteralN_noPrologueNrOfVars (VallstLiteral_MAX)

//! Parse error.
#define VallstLiteralN_parseError         (VallstLiteral_MAX-1)

//! File error.
#define VallstLiteralN_fileError          (VallstLiteral_MAX-2)

//! An undefined VallstFormulaN.
#define VallstFormulaN_undef VallstFormulaN_MAX



//! A result type used for various functions.
typedef enum
{
    VallstResult_proofOfFalse,       //!< A proof of false was found.
    VallstResult_model,              //!< A model was found.
    VallstResult_timeLimitExceeded,  //!< The time limit has been exceeded.
    VallstResult_interupt,           //!< An interupt signal was received.
    VallstResult_notEnoughMemory,    //!< Not enough memory could be allocated.
    VallstResult_fileError,          //!< Some file error occurred.
    VallstResult_parseError,         //!< A parse error occurred.
    //VallstResult_error,              // Other error. Not used.

    //! There is no model where the extra search assumptions are true as well.
    VallstResult_proofOfFalseGivenSearchAssumptions,

    //! Model where the extra search assumptions are true as well.
    VallstResult_modelOfSearchAssumptions,

    //! VallstResult_other* constants are for miscellaneous other results.
    VallstResult_other,
    // VallstResult_other1,
    // ...
    //! VallstResult_otherIntMax ensures that the VallstResult type is large.
    VallstResult_otherIntMax = INT_MAX

} VallstResult;



//! A type for formula formats.
typedef VallstLiteralN VallstFormulaType;

/*!\t
  For any formula a you can easily introduce a Tseitin name p for the
  formula such that p<=>a --- disregarding global types.

  Formulas of type >=* and >= aren't supported directly. Instead you have to
  transform them into <*- and <-formulas. See
  vallst_lessThanEqMultToMoreThanMult() and vallst_lessThanEqToMoreThan().

  (Negated) equivalences will be normalized so that all the literals in them
  are unnegated. E.g. <->{-p,-q,-r} will be turned into -<->{p,q,r} where
  p, q and r are variables.
*/ /*\{*/ /*!\u*/ //\{

//! Arbitrary long disjunction, \/{...}.
#define VallstFormulaType_clause          (VallstLiteral_MAX-1)


/*! Arbitrary long equivalence, <->{...} (i.e p1<->p2<->p3<->p4<->...<->pn
   (saying that an even number of the literals are true if n is even and saying
   that an odd number of the literals are true if n is odd)).
*/
#define VallstFormulaType_equivalence     (VallstLiteral_MAX-5)

//! Arbitrary long negated equivalence (xor), -<->{...}
//! (i.e -(p<->q<->r<->s<->...)).
#define VallstFormulaType_negEquivalence  (VallstLiteral_MAX-4)


/*! Arbitrary long constraint on the form c < p+q+r+..., where c is a constant.
    I.e. the formula says that at least c+1 of p,q,... should be true.

      With c=0, the formula is equivalent to a disjunction and it's slightly
    more efficient to use the clause form. Note though that there can be good
    reasons for using c=0, namely in cases where you later on might want to
    increase the constant.

      See vallst_lessThanEqToMoreThan() for transforming a >=-formula into a
    <-formula.
*/
#define VallstFormulaType_moreThan        (VallstLiteral_MAX-6)

/*!\v
    For formulas p\/a where a is of more-than type.
      With this type you can Tseitin name more-than formulas without using
    more-than-mult: Let a be c < q0 + .. + qn. Then p <=> a is equivalent to
    -p \/ a and p \/ -a where -a can be expressed as n-c < -q0 + ... + -qn.
      Having more-than-dis means that the more-than type isn't strictly
    necessary. However, using more-than rather than more-than-dis when
    possible is a little bit more efficient and transparent.
      Note that if you are looking for a p \/ /\{q0,...,qn} formula type
    you can use more-than-dis with c=n, i.e. p \/ n<q0+...+qn.\w
*/
#define VallstFormulaType_moreThanDis     (VallstLiteral_MAX-7)

/*! Arbitrary long constraint on the form c < d0*p0 + d1*p1 + ... where c and
    di are constants.

      A Tseitin name p for a more-than-mult formula a = c < +{di*pi} can be
    defined like this: q \/ a <=> c < +{di*pi} + (c+1)*q. Also,
    +{di} = +{di*pi} + +{di*-pi}. Hence, -a <=> c >= +{di*pi} <=>
    c >= +{di} - +{di*-pi} <=> +{di*-pi} >= +{di} - c <=>
    +{di}-c-1 < +{di*-pi}. Therefor p <=> a can be expressed by translating
    -p \/ a and p \/ -a. See vallst_lessThanEqMultToMoreThanMult() for
    transforming a >=*-formula into a <*-formula.

      Negative constants are not allowed. You can transform negative literal
    constants like this:  c < ... + -d*p + ...  <=>  c+d < ... + d*-p + ...

      If the formula is very long you might want to input d0, d1,... in
    increasing order since internally they will be sorted that way using an
    algorithm which is fast on already increasing formulas but which might be
    slow on non-increasing formulas.

      Excessive variable constants, as in e.g. 3 < 9*p + 7*q + 5*r + ..., are
    allowed and could be useful if you plan on incrementing the main constant,
    3, later on (see vallst_addNamedAxiom() and axiom altering functions).
    Though, rather than using excessive constants you might want to use
    vallst_alterAxiomIncMTMKeepAboves() instead.
    
*/
#define VallstFormulaType_moreThanMult    (VallstLiteral_MAX-8)


/*! \a0
    The meaning of the global axiom type VallstFormulaType_ggcdiTour is
    that any solution interpreted as nodes and edges in a complete directed
    irreflexive graph, assuming a canonical coding, must be a tour (i.e. a
    Hamiltonian cycle (visiting every node in the graph)).

      This formula type only covers the non-local part of formulas stating
    that the solution is a tour. Accompanying this formula must be the
    concluding local part. Otherwise the meaning and behaviour of the 
    solver is undefined.

      Here is an example that will clear things up:
    Suppose that you have a problem involving a complete directed irreflexive
    graph with n nodes 0,1...n-1. n is the dimension (dim) and the graph
    has n*(n-1) edges. Suppose that any solution to the problem must result
    in a tour of the graph; confer the asymmetric traveling salesperson
    problem, atsp. Let the graph be coded by variables p(i,j) with i!=j,
    i<n and j<n. p(i,j) will be true iff the edge (i,j) in the graph will be
    used in the solution. Assume that in actual fact p(i,j) will be
    represented by vallst literals q, q+2, q+4... where q is some offset 
    start vallst literal, e.g. 2. q may be odd. If q is 2 then let edge
    (0,1) be represented by vallst variable 2, (0,2) by 4, (0,3) by 6,
    (1,0) by 2*((n-1)+1), (1,2) by 2*((n-1)+2), (2,0) by 2*(2*(n-1)+1)... 
      The local part of formulas saying that a solution must be a tour says
    that each node has at most 1 in-edge and 1 out-edge, and at least
    1 in-edge and 1 out-edge:

        -     for all i<n,  n-3 < +{-p(i,j): j!=i, j<n}
        -     for all i<n,  n-3 < +{-p(j,i): j!=i, j<n}
        -     for all i<n,  \/{p(i,j): j!=i, j<n}
        -     for all i<n,  \/{p(j,i): j!=i, j<n}

    Then if you add a non-local tour axiom with vallst literal start q
    and with dimension n, you are ensured that any solution is a tour.
    The call to vallst_addAxiom() would be
    vallst_addAxiom( vi, [q,n], 2, VallstFormulaType_ggcdiTour ).

    As said, the tour type assumes the canonical coding of the graph
    described above. For a further definition of the canonical coding and
    utilities, see the macros vallst_ggcditEdgeToLit() and
    vallst_ggcditLitToEdge() (where dim is n above).
*/
#define VallstFormulaType_ggcdiTour       (VallstLiteral_MAX-9)


/*! Marks that the formula has been erased. 

      Although you can't use this type directly, you might still encounter
    this type because formulas can be erased by vallst. Say e.g. that you have
    named an axiom b which later gets erased by vallst (e.g. because it's
    simplified away or recognized to be subsumed). Then you have a name of an
    erased axiom and if you e.g. call vallst_formulaType() with the name you
    will get VallstFormulaType_erased back.
*/
#define VallstFormulaType_erased          (VallstLiteral_MAX-10)

/*\}*/ //\}



//! A result type used for callback functions.
typedef enum
{
    VallstCallbackResult_continue,   //!< Continue as normal.
    VallstCallbackResult_interupt,   //!< Interupt and possibly save what has 
                                     //!  been achieved so far.
    VallstCallbackResult_otherIntMax = INT_MAX

} VallstCallbackResult;



//! Each bit in a verbosity vector decides if some particular info should be
//! printed when appropriate. See \r2 below for what each bit means.
typedef uint64_t VallstVerbosityVector;

/*!\m Masks for the verbosity vector */
/*\{*/ /*!\o*/ //\{

//! Warns when space dependent on the number of variables needs to be extended.
#define VallstVerbosity_varExtensionWarning ( (VallstVerbosityVector)1 << 0 )

//! Warns when an empty (i.e. false) clause is added. Also warns about e.g.
//! -<->{} I think. Not sure if every case that one wants to catch is caught.
#define VallstVerbosity_emptyClauseWarning  ( (VallstVerbosityVector)1 << 1 )

//! Gives you notice if you miss to oversee the allocation of the theory
//! memory so that vallst will have to do it for you.
#define VallstVerbosity_theoryMemNotice     ( (VallstVerbosityVector)1 << 2 )

//! Prints info about a search when it's finished.
#define VallstVerbosity_searchDetails       ( (VallstVerbosityVector)1 << 3 )

//! Prints any model found.
#define VallstVerbosity_printModel          ( (VallstVerbosityVector)1 << 4 )

//! Prints parse error messages.
#define VallstVerbosity_parseError          ( (VallstVerbosityVector)1 << 5 )

//! Prints messages about other errors that the program will recover from and
//! then continue.
#define VallstVerbosity_lesserError         ( (VallstVerbosityVector)1 << 6 )

//! Prints a brief notice of the result of the proof search.
#define VallstVerbosity_printResult         ( (VallstVerbosityVector)1 << 7 )

//! Prints info about how many variables are set and unchecked.
#define VallstVerbosity_varsSet             ( (VallstVerbosityVector)1 << 8 )

//! Prints the seed.
#define VallstVerbosity_printSeed           ( (VallstVerbosityVector)1 << 9 )

//! Prints the cpu time used.
#define VallstVerbosity_time                ( (VallstVerbosityVector)1 << 10 )

//! Prints some, easily obtainable, info about the hash-table.
#define VallstVerbosity_hashInfo            ( (VallstVerbosityVector)1 << 11 )

//! Prints option settings.
#define VallstVerbosity_printSettings       ( (VallstVerbosityVector)1 << 12 )

//! Prints hindsighted prologue values. See \ref vallst.c for an example.
#define VallstVerbosity_printPrologues      ( (VallstVerbosityVector)1 << 13 )

//! Prints estimated prologue values. See \ref vallst.c for an example.
#define VallstVerbosity_printEstimatedPrologues  \
                                            ( (VallstVerbosityVector)1 << 14 )

//! Gives notice when clauses are converted to an equivalence.
#define VallstVerbosity_equConversionNotice ( (VallstVerbosityVector)1 << 15 )

//! Prints info about non-axioms.
#define VallstVerbosity_nonAxInfo           ( (VallstVerbosityVector)1 << 16 )

//! Prints info about optimization parts of a problem.
#define VallstVerbosity_optimizeInfo        ( (VallstVerbosityVector)1 << 17 )

//! Gives notice when an already existing clause is added.
#define VallstVerbosity_redundancyNotice    ( (VallstVerbosityVector)1 << 18 )

//! Prints message about failure to double the hash table size. The program
//! will recover from this error and then continue.
#define VallstVerbosity_lesserHashError     ( (VallstVerbosityVector)1 << 19 )


//! Prints progress info during the simplification process.
#define VallstVerbosity_simpProgressDetails ( (VallstVerbosityVector)1 << 22 )

//! Gives notice when a proof improvement attempt failed to prove false.
#define VallstVerbosity_failedProofImprovementNotice  \
                                            ( (VallstVerbosityVector)1 << 23 )

//! Prints info about proof improvements during search as they happen.
#define VallstVerbosity_proofImprovementDetails  \
                                            ( (VallstVerbosityVector)1 << 24 )

//! Prints detailed info about a the hash-table during consistency checks.
#define VallstVerbosity_hashDetails         ( (VallstVerbosityVector)1 << 25 )

//! Prints info about restarts during the search as they occur.
#define VallstVerbosity_restartDetails      ( (VallstVerbosityVector)1 << 26 )

//! Prints detailed progress info during the search.
#define VallstVerbosity_progressDetails     ( (VallstVerbosityVector)1 << 27 )

//! Prints detailed info about a the search branching heuristic.
#define VallstVerbosity_branchingDetails    ( (VallstVerbosityVector)1 << 28 )

//! Gives notice of a midair pruning.
#define VallstVerbosity_midairPruneNotice   ( (VallstVerbosityVector)1 << 29 )

//! Prints various not too interesting midair pruning details.
#define VallstVerbosity_midairPruneDetails  ( (VallstVerbosityVector)1 << 30 )

//! Gives notice when a contradiction is found but not acted on.
#define VallstVerbosity_ignoredContradictionNotice  \
                                            ( (VallstVerbosityVector)1 << 31 )

/*\}*/ //\}



//! The type for names for formulas.
typedef void * VallstFormulaName;


//! A dynamic array of type VallstFormulaName.
typedef struct VallstFormulaNames_ VallstFormulaNames;

//! A dynamic array of type VallstFormulaName.
struct VallstFormulaNames_
{
    VallstFormulaName * names;         //!< The start of the array.
    VallstFormulaN nrOfNames;          //!< The current number of active names.
    VallstFormulaN nrOfAllocatedNames; //!< The physical length of the array.

};



/*!\d4 Problem types */
/*\{*/ /*!\n1*/ //\{

//! For some general default settings.
#define VallstProblemType_default 0

//! Means that the type is undefined at the moment. If the undefined value
//! doesn't apply and something is needed, the same settings as for
//! VallstProblemType_default will be used.
#define VallstProblemType_undef   1

//! For asymmetric traveling salesperson problems.
#define VallstProblemType_atsp    2

//! For symmetric traveling salesperson problems.
#define VallstProblemType_tsp     3

//! For pseudo boolean, (o)pb, problems. Only meant for problems where the
//! input is on (restricted) (o)pb form.
#define VallstProblemType_pb      4

/*\}*/ //\}



/*!\j Allocation */ // -----------------------------------------------
//\{


// vallst_deleteInstance       -- Deletes a vallst instance.


/*! Returns a new vallst problem instance. NULL is returned iff a new instance
    couldn't be created, which can only happen due to insufficient memory.

      nrOfVars is meant to be a roughly minimal upper bound for the number of
    variables, like in the DIMACS cnf prologue. Any value including 0 will work
    though and if you don't have any good guess of a roughly minimal upper
    bound just use any value as long as it isn't much larger than the largest
    variable to be used.

      If nrOfVars is 0, no variable space will be allocated. Using nrOfVars=0
    is useful for memory efficiency reasons if you at first don't know how many
    variables that are used. If you later learn of a roughly minimal upper
    bound on the variables you can call vallst_extendNrOfVars().
    See vallst.c for an example.

      nrOf3ClausesEstimate is meant to be an estimate of the number of ternary
    clauses. It's not important that nrOf3Clauses is exactly accurate but any
    fairly accurate estimate might be helpful for memory efficiency reasons.

      You can use nrOf3ClausesEstimate=0, and then later, before adding
    ternary clauses, set an estimate with vallst_setNrOf3ClausesEstimate() and
    propagate the value by calling vallst_propagateNrOf3ClausesEstimate().
    See vallst.c for an example.

      If you know that there will be ternary clauses but have no idea of how
    many, just use any value not too large, e.g. 0. The only motive behind 
    this number of ternary clauses estimate is to improve efficiency a little;
    it's not very important.

      nrOfLitOccsEstimate is supposed to be a possibly rough estimate of the
    number of literal/constant occurrences in the input theory modulo "special
    accounting". The special accounting works like this: Occurrences in unit
    formulas or binary disjunctions don't count at all; add 1 for each
    formula (that isn't unit or a binary disjunction); add 1 for each formula
    that isn't a ternary disjunction (and not unit or a binary disjunction);
    add 2 for each <*-formula; the count for ggcdit is exactly 4. For example,
    the count for c < c1*p1 + ... + cn*pn  would be 1 + 2*n + 1 + 1 + 2.

      It's not important that the estimate is exactly accurate but any fairly
    accurate estimate might be helpful for memory efficiency reasons. Try to
    make it an upper bound. You could also set the value to some fraction of
    the "correct" value. Just try not to get a too low value.

      You can use nrOfLitOccsEstimate = VallstFormulaN_undef, and then later,
    before adding formulas, set an estimate with
    vallst_setNrOfLitOccsEstimate() and propagate the value by calling
    vallst_propagateNrOfLitOccsEstimate(). See vallst.c for an example.
*/
VallstInstance * vallst_newInstance( VallstLiteralN nrOfVars,
                                     VallstFormulaN nrOf3ClausesEstimate,
                                     VallstFormulaN nrOfLitOccsEstimate );


/*! See vallst_newInstance() for a description.
    Returns true iff not enough memory could be allocated.

      Nothing is done if the nrOf3ClausesEstimate in vi is undefined, i.e.
    equals VallstFormulaN_undef.
*/
bool vallst_propagateNrOf3ClausesEstimate( VallstInstance * vi );


/*! See vallst_newInstance() for a description.
    Returns true iff not enough memory could be allocated.

      Nothing is done if the theory memory is already set up somehow, i.e.
    the theory memory isn't NULL.

      If the nrOfLitOccsEstimate in vi is undefined, i.e. equals
    VallstFormulaN_undef, nrOfLitOccsEstimate in vi will be set to some
    value first before propagation.

      If it's possible, try to set the number of variables, explicitly or
    implicitly, before calling this function since some heuristic size value
    function will use that variable value. See e.g. vallst.c.
*/
bool vallst_propagateNrOfLitOccsEstimate( VallstInstance * vi );


/*! Sets the fstNrOfLevelsAlloc size.

      If no smaller value can be seen to be enough, like e.g. the number of
    variables, this value will be used as a first allocation size of
    nr-of-levels dependent arrays.

      This value can at most only have some minor memory allocation
    efficiency impact.
*/
void vallst_setFstNrOfLevelsAllocSize( VallstInstance * vi,
                                       VallstLiteralN size );


//! Sets max load. Decides how many hash entries are allowed before resizing.
//! Resizing is done when maxLoad < nrOfEntries/tableSize.
void vallst_setMaxHashLoad( VallstInstance * vi, double maxLoad );


//! Sets the value. It determines the size addition to the non-axiom chunk
//! size relative to the size of the axiom chunks.
void vallst_setNonAxChunkSizeAxDep( VallstInstance * vi, double value );

//! Sets the value. It determines the size of a constant addition to the
//! non-axiom chunk size.
void vallst_setNonAxChunkSizeConst( VallstInstance * vi,
                                    VallstFormulaN value );

//! Sets the value. It determines the size addition to the non-axiom chunk size
//! relative to the number of variables allocated for.
void vallst_setNonAxChunkSizeVarDep( VallstInstance * vi, double value );


/*! Sets the number of ternary clauses estimate.

      It's not important that the estimate is exactly accurate but any fairly
    accurate estimate might be helpful for memory efficiency reasons.
*/
void vallst_setNrOf3ClausesEstimate( VallstInstance * vi,
                                     VallstFormulaN pNrOf3Clauses );


/*! Sets cap.

      Only 'cap' number of free chunks are guaranteed to be kept.
    The rest are freed occasionally, handing the memory back to the system.
*/
void vallst_setNrOfFreeChunksCap( VallstInstance * vi, unsigned int cap );


/*! Sets the number of literal occurrences estimate, modulo special accounting.
    See vallst_newInstance().

      It's not important that the estimate is exactly accurate but any fairly
    accurate estimate might be helpful for memory efficiency reasons. Try to
    make it an upper bound.
*/
void vallst_setNrOfLitOccsEstimate( VallstInstance * vi,
                                    VallstFormulaN pNrOfLitOccs );


//\}



/*!\x Formulas and variables */ // -----------------------------------
//\{

/*! Adds an axiom. New unit clauses will be put as unchecked w.r.t bcp.

      Literals are represented by 2, 3, 4,... 2 is the first variable. 3 is
    the negation of the first variable. In general 2n is the nth variable and
    2n+1 is the negation of the nth variable.

      'size' is the size of the formula to add, i.e. the length of 'axiom'.

      E.g. if the formula is a ternary clause 3\/6\/8, 'size' should be 3,
    type should be VallstFormulaType_clause and axiom should be [3,6,8].

      E.g. 1 < p+q+r is represented as [1,p,q,r] (where p, q and r are numbers
    representing literals) and the size is 4.

      2 < 3*p + 2*q + r + s is represented as [2,3,p,2,q,1,r,1,s] with size 9.

      p \/ c<q+r+s is represented as [p,c,q,r,s] with size 5.

      The axiom array might be altered.

      VallstResult_other is returned if no other value is applicable.
    VallstResult_model is never returned. Neither is
    VallstResult_modelOfSearchAssumptions, nor
    VallstResult_proofOfFalseGivenSearchAssumptions.

      For <*-formulas a variable p is allowed to occur as many times as you
    like, both positively and negatively. I.e. the literal list may look like
    ...d*p...e*p...f*-p...g*p...h*-p...

      For more-than and more-than-dis formulas it's an error if a literal
    occurs twice with the same sign, i.e. if the literal list looks like
    ...p...p... or ...-p...-p... where p is a variable. ...p...-p... is allowed
    though.

      If the type is more-than-dis and the formula is p\/a, then p and -p are
    allowed to occur in a.

      Literal constants in <*-formulas may be 0, like e.g. in c < ...0*p....

      You may use 0 and 1 as false and true constants if you like. (This of
    course only works here and not for the file parser where 0 marks the end
    of formulas.)

      If you have unit-clauses to add it might be slightly more efficient to
    supply them first.

      You might want to add the more important axioms, like e.g. a conclusion
    if there is something like that, last. This is for efficiency reasons
    since some heuristics go through the axioms from the last one to the
    first one. There might also be some sort of sos-like strategy in use
    where only the last n axioms will be considered.

      It might be good to have strong (short) formulas before weak (long)
    ones. (Consider though also the above paragraph.)
*/
VallstResult vallst_addAxiom( VallstInstance * vi,
                              VallstLiteral * axiom,
                              VallstLiteralN size,
                              VallstFormulaType type );


/*! Adds a formula that should be a consequence of the axioms since the formula
    might be removed. (It's guaranteed though that formulas with less than 4(?)
    literals won't be removed.)

      The formula must be a cnf clause, otherwise VallstResult_parseError is
    return.

      Otherwise it works like vallst_addAxiom().
*/
VallstResult vallst_addConsequence( VallstInstance * vi,
                                    VallstLiteral * nonAxiom,
                                    VallstLiteralN size,
                                    VallstFormulaType type );


/*! Adds a named axiom.

      Works like vallst_addAxiom() except that a name of the axiom is placed in
    *namePtr for future reference. The return value might also be different,
    see below. If namePtr is NULL, nothing extra is done at all and
    vallst_addNamedAxiom() will work exactly like vallst_addAxiom().

      Note that even if you successfully called vallst_addNamedAxiom() creating
    a new axiom, the axiom might internally have been tranformed into something
    you might not have expected. E.g. even if you input a long more-than-dis
    axiom, this might be turned into a binary clause.

      If a new axiom b was created, and b isn't a binary disjunction, then
    VallstResult_other will be returned and namePtr will be updated if it isn't
    NULL.

      Important to note is that binary clauses are treated in a special way
    because it's not very convenient or feasible to give them names like for
    other formulas. Instead, if a new axiom b was created, and b is a binary
    disjunction, either because the input was a binary clause or the input was
    transformed into a binary clause internally, then when a name is requested
    for b, *namePtr will be assigned 'axiom' (*namePtr = axiom) and the two
    disjuncts in the binary clause will be placed at the first two positions,
    [0..1], in the *namePtr/axiom array. VallstResult_other is returned.

      If no axiom was created and no already existing formula was found to be
    equivalent to 'axiom', (e.g. because the axiom was found inconsistent
    and vallst_addNamedAxiom() therefor returned VallstResult_proofOfFalse),
    *namePtr will be assigned NULL.

      If no axiom was created because 'axiom' was found to already be true,
    *namePtr will be assigned NULL and VallstResult_other+1 will be returned.

      If no axiom was created but, or rather because, 'axiom' was found to be
    equivalent to a literal, p, *namePtr will be assigned 'axiom' (*namePtr =
    axiom), p will be placed in the first position ([0]) in the *namePtr/axiom
    array (axiom[0] = p) and VallstResult_other+2 will be returned (and p will
    of course be set to true).

      If no axiom was created because 'axiom' was found to be equivalent to an
    already existing axiom b, then *namePtr will be assigned 'axiom'
    (*namePtr = axiom) when b is a binary clause; *namePtr will be a name of b
    when b isn't a binary clause. The equivalent axiom b is a disjunction and
    the disjuncts in b are placed in the first positions, [0..k], in the
    *namePtr/axiom array. Also, vallst_addNamedAxiom() will return
    VallstResult_other+1+size where size is the number of literals in b so that
    e.g. VallstResult_other+1+2 will be returned when 'axiom' is found to be
    equivalent to a binary disjunction.

      Here is a summary:

       - VallstResult_other: new axiom created with name *namePtr.
                             For created bin clause p\/q, *namePtr = [p,q,...]
       - VallstResult_other+1: 'axiom' true;        *namePtr = NULL
       - VallstResult_other+2: 'axiom' <=> p;       *namePtr = [p,...]
       - VallstResult_other+3: 'axiom' <=> p\/q;    *namePtr = [p,q,...]
       - VallstResult_other+4: 'axiom' <=> b <=> p\/q\/r; *namePtr is a name of
                                                    b; array = [p,q,r,...]

    Note that in the above summary, [...] denotes the 'axiom' array provided
    as an argument to the function. Hence it is of a temporary nature and may
    very well be overwritten (by the owner of the axiom array; indeed,
    overwriting it is probably the natural and common thing to do eventually).

      As things are at the moment, no value greater than VallstResult_other+4
    will ever be returned; 'axiom' will not be found to be equivalent to e.g.
    a disjunction with 4 disjuncts.

      You can use vallst_formulaType() to find out the type of a formula name.

      Getting a name for an axiom is useful e.g. for axiom strengthening:
    Assume e.g. that you have got a model for a theory and want to make the
    theory stronger, e.g. by incrementing the constant in a more-than axiom, to
    see if the stronger theory has a model or not. To do that you can just call
    some alter-axiom function to make the theory stronger and keep everything
    else, including all derived consequences of the previous theory, as it is.
*/
VallstResult vallst_addNamedAxiom( VallstInstance * vi,
                                   VallstLiteral * axiom,
                                   VallstLiteralN size,
                                   VallstFormulaType type,
                                   VallstFormulaName * namePtr );


/*! Adds c to the constant in a more-than (<), more-than-mult (<*) or
    more-than-dis (<\/) axiom.

      Returns VallstResult_parseError if 'name' isn't a name of a formula of
    more-than* type or if the level isn't 0. VallstResult_notEnoughMemory is
    returned in case not enough memory could be allocated.
    VallstResult_proofOfFalse may also be returned. Otherwise, Vallst_other is
    returned.

      Note that only strengthening of axioms is supported. 
    As a consequence you can't keep Tseitin names of <*-axioms that you alter
    because the p\/-a part would get weaker when the constant is increased.
    (Intuitively, if you strengthen a and have p<->a and -p is used positively
    elsewhere, that would weaken the theory, which isn't supported.)
    (If you want to weaken/undo something you can either use search
    assumptions; or you can save the theory/state and then later revert back
    to the saved theory/state.)
*/
VallstResult vallst_alterAxiomIncMT( VallstInstance * vi,
                                     VallstFormulaName name,
                                     VallstLiteralN c );


/*! Like vallst_alterAxiomIncMT() but also adds c to any literal constant d in
    'name' that is greater than the current constraint constant. 'name' must
    be of <* type.
*/
VallstResult vallst_alterAxiomIncMTMKeepAboves( VallstInstance * vi,
                                                VallstFormulaName name,
                                                VallstLiteralN c );


/*! Extends the number of variables ready to be used. true is returned iff the
    extension failed --- which can only happen due to insufficient memory.

      nrOfVars is meant to be a roughly minimal upper bound for the number of
    variables, like in the DIMACS cnf prologue. Any value will work though and
    if you don't have any good guess of a roughly minimal upper bound don't use
    this function. This function only exists for memory efficiency purposes and
    you are never required to use it. If nrOfVars is less than or equal to the
    current value, nothing will be done.

      You should, for efficiency reasons, try to use this function if you have
    an already built theory (that you e.g. just have decided) and you now want
    to extend or change the theory with a known number of variables.
*/
bool vallst_extendNrOfVars( VallstInstance * vi, VallstLiteralN nrOfVars );


/*! Returns the type of the formula with name formulaName.

      To follow vallst_addNamedAxiom(), vallst_formulaType() will return 1,
    representing the true constant, if formulaName is NULL. It will return
    VallstFormulaType_clause if *formulaName isn't a type (refer to the
    vallst_addNamedAxiom() case where formulaName = axiom = [p,...] where p is
    a literal and not a type).
*/
VallstFormulaType vallst_formulaType( VallstFormulaName formulaName );


//! Returns the constant in a formula of type <, <\/ or <*. Returns
//! VallstLiteralN_parseError if the formula is of wrong type.
VallstLiteralN vallst_getConst( VallstFormulaName name );


/*! Returns the full status of literal p. 0 is returned iff p is held false
    (i.e. -p is true). 1 is returned iff p is held true. Otherwise p is open
    and 2 is returned.
*/
int vallst_getFullLitValue( VallstInstance * vi, VallstLiteral p );


//! Returns the keep-aboves flag. If true, constant-aboves will be kept aboves
//! e.g. in vallst standalone if constraint constants are to be increased.
//! See vallst_alterAxiomIncMTMKeepAboves() and vallst.c.
bool vallst_getKeepAboves( VallstInstance * vi );


/*! Returns the status of literal p. true is returned iff p is held true.
    Otherwise false is returned.
*/
bool vallst_getLitValue( VallstInstance * vi, VallstLiteral p );


//! Returns the number of variables that has been allocated for.
VallstLiteralN vallst_getNrOfVarsAllocated( VallstInstance * vi );


/*! Returns the sum of the literal constants in a more-than-mult (<*) formula.
    Takes constant time. Returns VallstLiteralN_parseError if the formula is
    of the wrong type.
*/
VallstLiteralN vallst_getTotalSum( VallstFormulaName name );


//! Returns true iff name is a constraint (i.e. of type <, <* or <\/).
//! If name is NULL, false will be returned.
bool vallst_isConstraint( VallstFormulaName name );


/*! Tranforms a >=*-formula into a <*-formula using
    c >= +{di*pi} <=> +{di}-c-1 < +{di*-pi}.

      For example, [3,2,p,3,q,1,r] (size=7) with type >=*, representing
    3 >= 2p+3q+1r, is transformed into the equivalent [2,2,-p,3,-q,1,-r] with
    type <*, representing 2 < 2*'-p'+3*'-q'+1*'-r', where p, q,... are numbers.

      Returns true iff +{di}-c-1 < 0, i.e. c >= +{di}, in which case a isn't
    altered. I.e. if true is returned, the formula a is a tautology and can
    be ignored.
*/
bool vallst_lessThanEqMultToMoreThanMult( VallstLiteral * a,
                                          VallstLiteralN size );


/*! Tranforms a >=-formula into a <-formula using
    c >= p1+...+pn <=> n-c-1 < +{-pi}.

      For example, [2,p,q,r] (size=4) with type >=, representing 2 >= p+q+r,
    is transformed into the equivalent [0,-p,-q,-r] with type <, representing
    0 < '-p'+'-q'+'-r', where p, q,... are numbers.

      Returns true iff n-c-1 < 0, i.e. c >= n, in which case a isn't altered.
    I.e. if true is returned, the formula a is a tautology and can be ignored.
*/
bool vallst_lessThanEqToMoreThan( VallstLiteral * a,
                                  VallstLiteralN size );


//! Returns -p, i.e. the negation of the literal p.
VallstLiteral vallst_neg( VallstLiteral p );



/*
  vallst_newVar               -- Returns a new variable ready to be used.
*/



//! Sets flag. If true, constant-aboves will be kept aboves
//! e.g. in vallst standalone if constraint constants are to be increased.
//! See vallst_alterAxiomIncMTMKeepAboves() and \ref vallst.c.
void vallst_setKeepAboves( VallstInstance * vi, bool b );


/*! Sets the main constant for an (a)tsp. This value will be used when the
    formula is parsed and nowhere else. The edge sum formula will be
    (min) c >= d0*p0 + ... + dn*pn. Any value