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 larger than or equal to the
    total sum s = d0+...+dn will reduce to s-1.
*/
void vallst_setStartConst( VallstInstance * vi, VallstLiteralN c );


/*! Evaluates the summation side in a more-than* formula given the current
    state. Open literals will count as true. Returns the sum. Returns
    VallstLiteralN_parseError if the formula isn't a more-than* formula.

      See vallst_sumTrue() for the intended use.
*/
VallstLiteralN 
vallst_sumOpenTrue( VallstInstance * vi, VallstFormulaName name );


/*! Evaluates the summation side in a more-than* formula given the current
    state. Open literals will count as false. Returns the sum. Returns
    VallstLiteralN_parseError if the formula isn't a more-than* formula.

      The intended use of this function is like this: Assume that you have
    found a model to a problem which contains constraint formulas
    a_k := c_k < +{d_i*p_i}. Then you can call this function for all a_k to
    know of a lower bound of how high you can raise the c_k constants and still
    have a model. Then you can carry out the increase of the constants ---
    possible after that you have moved up to level 0 --- and then maybe
    strengthen the theory further to see if the constants found were optimal.
    (See the various axiom altering functions on how to increase constants in
    constraints.)

      Since open variables can be interpreted either way you can use 
    vallst_sumOpenTrue() instead if you know that the variables in the formulas
    you are interested in are disjoint. If the variables aren't disjoint, some
    caution is of course needed. Assume e.g. a_0 := c_0 < ...d_j*p_j... and
    a_1 := c_m < ...d_k*-p_j... where p_j is open. Then you can't of course
    count both p_j and -p_j as true. But you can always use
    vallst_sumOpenTrue() on at least one formula a_i.
*/
VallstLiteralN vallst_sumTrue( VallstInstance * vi, VallstFormulaName name );


//\}



/*!\h Search */ // ---------------------------------------------------
//\{

/*! Returns value.

      Search will be aborted after this many new variables have been set, to
    a truth value or to an other equ class. (Aborted that is provided that
    enough time has passed. See vallst_getNoAbortTime().) Search will also
    be aborted if fewer vars are set but more time has passed.
*/
VallstLiteralN vallst_getAbortThreshold( VallstInstance * vi );


//! Returns the current search level.
VallstLiteralN vallst_getLevel( VallstInstance * vi );


/*! Returns limit.

      Given that enough vars are set, search will not abort until no-abort-time
    seconds have passed. See vallst_getAbortThreshold().
*/
unsigned int vallst_getNoAbortTime( VallstInstance * vi );


/*! Makes all search assumptions into onetime search suggestions. Used for
    suggesting a model/state.

      Suggestions will be chosen as assumptions at the lowest levels in a
    search. The suggestions will be emptied/reset as soon as one literal
    suggestion is false.

      Search assumptions take precedence over search suggestions.

      Returns true iff not enough memory could be allocated.

      Any previous suggestions will be emptied/reset.
*/
bool vallst_makeCurrentAssumptionsSuggestions( VallstInstance * vi );


/*! Makes a search assumption that will affect vallst_search().

      If p is already true, VallstResult_other is returned.

      If p is already false, VallstResult_proofOfFalseGivenSearchAssumptions is
    returned.

      If not enough memory could be allocated, VallstResult_notEnoughMemory is
    returned.

      Otherwise VallstResult_other+1 is returned.

      If p is already true or false, a call to vallst_makeSearchAssumption()
    will have no effect.
*/
VallstResult vallst_makeSearchAssumption( VallstInstance * vi,
                                          VallstLiteral p );


/*! Moves the current search state to level 0.

      Also resets the buffers if the level isn't 0 already.
*/
void vallst_moveToLevel0( VallstInstance * vi );


//! Removes all search assumptions.
void vallst_removeAssumptions( VallstInstance * vi );

//! Removes the last search assumption.
void vallst_removeLastAssumption( VallstInstance * vi );


/*! Searches for a proof of false or a model. Returns the result of the search.

      VallstResult_other will be returned if the level isn't 0.

      If there are search assumptions,
    VallstResult_proofOfFalseGivenSearchAssumptions and
    VallstResult_modelOfSearchAssumptions may be returned. If it's determined
    that there is no model where the extra search assumptions are true as well
    as the axioms, VallstResult_proofOfFalseGivenSearchAssumptions is returned,
    except that if a proof of false was found not using the extra search
    assumptions, VallstResult_proofOfFalse will be returned rather than
    VallstResult_proofOfFalseGivenSearchAssumptions. Note also that 
    VallstResult_model may be returned instead
    VallstResult_proofOfFalseGivenSearchAssumptions if it's proved that there
    is no model satisfying the extra search assumptions but a model to the
    axioms was in fact found.
*/
VallstResult vallst_search( VallstInstance * vi );


/*! Sets value.

      Search will be aborted after this many new variables have been set, to
    a truth value or to an other equ class. (Aborted that is provided that
    enough time has passed. See vallst_getNoAbortTime().) Search will also
    be aborted if fewer vars are set but more time has passed.
*/
void vallst_setAbortThreshold( VallstInstance * vi, VallstLiteralN n );


/*! Sets the frequency.

      The buffers will be emptied every bufferResetFrequency-th time the
    search is restarted. You might want to synchronize this value with
    metaPruneFrequency and perhaps with metaMetaPruneFrequency too
    so that metaPruneFrequency is a multiple of bufferResetFrequency and
    metaMetaPruneFrequency is a multiple of metaPruneFrequency.
*/
void vallst_setBufferResetFrequency( VallstInstance * vi,
                                     VallstFormulaN freq );


//! Sets the value. It determines the size of a constant addition to the
//! buffer size.
void vallst_setBufferSizeConst( VallstInstance * vi, VallstFormulaN value );

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

//! Sets the value. It determines the size addition to the buffer size 
//! relative to the number of variables allocated for.
void vallst_setBufferSizeVarDep( VallstInstance * vi, double value );


/*! Sets the proof improvement leeway.

      Conflict clause size ccSize1 is considered as good as ccSize2 if
    ccSize1/ccSize2 <= ccLeeway. Used when the 1-uips are the same. Should
    probably be 1.0 or slightly greater.
*/
void vallst_setCCLeeway( VallstInstance * vi, double ccLeeway );


/*! Sets the create-phantom-conflict-clauses flag. Conflict clauses will be
    marked as deleted iff createPhantomConflictClauses is true and they aren't
    short. False by default.

      If you change this flag from false to true after a search has been made
    the buffers will also reset.

      This flag, if set to true, might interact with the improveProofLevel
    and keepConflictClauseLengthThreshold options to affect proof improvement
    in a perhaps subtle way. See the note on vallst_setImproveProofLevel().
*/
void vallst_setCreatePhantomConflictClauses( VallstInstance * vi, bool b );


/*! Sets the base/initial restart size. Typically used as the initial number of
    end nodes until the first restart is made. Restarts may be postponed for
    other reasons during the search batch. The value is supposed to be the
    least size that is sensible to have as a search batch size and is used as
    a base for restart strategies.

      If the Luby-Sinclair-Zuckerman restart strategy is used, all batch sizes
    will be multiples of this value. See vallst_setRestartPredefFunc().
*/
void vallst_setFirstRestart( VallstInstance * vi, VallstFormulaN n );


/*! Sets what's to be considered good.

      Clause sizes <= goodClauseSize are considered good. If a conflict
    clause size is good the next restart will be postponed.
*/
void vallst_setGoodClauseSize( VallstInstance * vi, VallstFormulaN size );


/*! Sets what's to be considered good.

      Levels <= goodLevel are considered good. If the search backtracks to
    a good level the next restart will be postponed.
*/
void vallst_setGoodLevel( VallstInstance * vi, VallstFormulaN size );


//! Sets how many axioms, starting from the last one, that should be checked
//! to see if they are open, in some branching heuristics. Binary clauses
//! don't count!
void vallst_setHeurAxSize( VallstInstance * vi, VallstFormulaN size );


/*! Sets the level threshold.

      The solver will try to improve proofs if the current level is less
    than improveProofLevel. Hence, setting it to 0 will turn off proof
    improvements.

      There are situations where the algorithm won't make an effort to
    improve proofs even if the level is less than improveProofLevel.

      Note that trying to improve proofs while createPhantomConflictClauses is
    true might give rise to a situation where the prover during a proof
    improvement attempt can't re-prove what it just proved:
    Let |-0 stand for closure under bcp. Assume that improveProofLevel is large
    enough and keepConflictClauseLengthThreshold is small enough. Assume that
    ...+p+q+r|-0 0, where 0 stands for a contradiction. Then ...+p+q proves -r
    with reason c_r and say that c_r is a phantom clause. Assume that
    ...+p+q+-r|-0 0. Then ...+p|- -q but this proof depends on c_r and it's not
    necessarily the case that we now have ...+p+q|-0 0. In this situation,
    i.e. when the proof improvement attempt fails to even find a proof of
    false, the proof path is aborted and the state is reverted back to the
    first proof before proof improvement was last attempted.
      Hence, if you want to try to improve proofs while creating phantom
    conflict clauses, you still might want to lower the improve-proof-level
    in order to get the proof improvement to work more effectively. Ideally
    one might want to somehow synchronize improveProofLevel and
    vallst_setKeepConflictClauseLengthThreshold().
*/
void vallst_setImproveProofLevel( VallstInstance * vi, VallstLiteralN lvl );



/*! Sets the keep-conflict-clause-length meta meta threshold.

      keepCCMetaMetaThreshold functions as a lower bound for various
    non-axiom pruning thresholds. Non-axioms of size less than or equal to
    keepCCMetaMetaThreshold will be kept.

      The intended use is to have:

     -   keepCCMetaMetaThreshold <= metaPruneStart <= metaPruneEnd
     -   keepCCMetaMetaThreshold <= metaMetaPruneStart <= metaMetaPruneEnd
     -   metaMetaPruneStart <= metaPruneStart
     -   metaMetaPruneEnd <= metaPruneEnd
     -   keepCCMetaMetaThreshold <= tightMetaPruneStart <= tightMetaPruneEnd
     -   keepCCMetaMetaThreshold <= tightMetaMetaPruneStart <=
         tightMetaMetaPruneEnd
     -   tightMetaMetaPruneStart <= tightMetaPruneStart
     -   tightMetaMetaPruneEnd <= tightMetaPruneEnd

      Furthermore, the tight thresholds are intended to be less than or equal
    to the loose ones (where it makes sense):

     -   tightMetaPruneStart <= metaPruneStart
     -   tightMetaMetaPruneStart <= metaMetaPruneStart
     -   tightMetaMetaPruneEnd <= metaMetaPruneEnd
     -   tightKeepCCThreshold <= keepConflictClauseLengthThreshold
     -   tightTheorySizeLeeway <= looseTheorySizeLeeway

      It is also the intention that the below meta-meta, meta, object relations
    hold:
     -   tightTheorySizeLeeway <= tightTheoryMetaSizeLeeway <=
         tightTheorySizeLeewayKeep
     -   looseTheorySizeLeeway <= looseTheoryMetaSizeLeeway <=
         looseTheorySizeLeewayKeep
*/
void vallst_setKeepCCMetaMetaThreshold( VallstInstance * vi,
                                        VallstLiteralN threshold );


/*! Sets the keep-conflict-clause-length threshold.

      Conflict clauses less than or equal to keepConflictClauseLengthThreshold
    will be fully added even if the createPhantomConflictClauses flag is 
    true.

      Also, when using conflict clause buffers, if the conflict clause is
    less than or equal to keepConflictClauseLengthThreshold the clause
    will be added, to the non-axioms, as a proper first class clause.
    Note though that a doppelganger may be created too.

      A threshold of less than 2 will have the same effects as a threshold of
    2. Therefore any value lower than 2 will be raised to 2.

      This flag might interact with the improveProofLevel and
    createPhantomConflictClauses options, if the latter is set to true, to
    affect proof improvement in a perhaps subtle way. See the note on
    vallst_setImproveProofLevel().

      The intention is to have
    tightKeepCCThreshold <= keepConflictClauseLengthThreshold.
*/
void vallst_setKeepConflictClauseLengthThreshold( VallstInstance * vi,
                                                  VallstLiteralN threshold );


/*! Sets the function defining the strength of literal pairs (p,-p) given
    the strength of the literals p and -p.

      The litPairStrFunc function should return a measure of the combined
    strength of p and -p given the individual strength of p and -p.
    varStrPtr[0] will be the strength of the unnegated variable (p),
    varStrPtr[1] will be the strength of the   negated variable (-p).

      The default function looks something like this:\v
        static Strength litPairStrF( Strength * varStrPtr )
        {
            return varStrPtr[0] * varStrPtr[1];
        } \w

      Unfortunately, because the Strength type isn't (for various reasons) part
    of the interface/library, you have to provide two versions of the function:
        1) a version with type      double as the Strength type,
        2) a version with type long double as the Strength type.
*/
void vallst_setLitPairStrFunc
                 ( VallstInstance * vi,
                   double (*litPairStrFunc)( double * varStrPtr ),
                   long double (*litPairStrFuncl)( long double * varStrPtr ) );



/*! Sets meta meta leeway.

      The nr of non-axioms is allowed to grow in loose mode to at most
    nrOf(non-erased)Axioms * looseTheorySizeLeeway before relevant parameters
    are tightened in order to bring the size of the theory back down again.
    Used after meta meta pruning.

      The intention is to have tightTheorySizeLeeway <= looseTheorySizeLeeway.
    See also vallst_setKeepCCMetaMetaThreshold().
*/
void vallst_setLooseTheorySizeLeeway( VallstInstance * vi, double leeway );


/*! Sets value.

      Given that enough vars are set, search will not abort until secs
    seconds have passed. See vallst_getAbortThreshold().
*/
void vallst_setNoAbortTime( VallstInstance * vi, unsigned int secs );


/*! Sets meta meta leeway.

      The nr of non-axioms is allowed to grow in tight mode to at most
    nrOf(non-erased)Axioms * tightTheorySizeLeeway before relevant parameters
    are tightened in order to bring the size of the theory back down again.
    Used after meta meta pruning.

      The intention is to have tightTheorySizeLeeway <= looseTheorySizeLeeway.
    See also vallst_setKeepCCMetaMetaThreshold().
*/
void vallst_setTightTheorySizeLeeway( VallstInstance * vi, double leeway );


/*! Sets meta leeway.

      Like vallst_setLooseTheorySizeLeeway() but used after meta pruning.

      The intention is to have tightTheoryMetaSizeLeeway <=
    looseTheoryMetaSizeLeeway.
*/
void vallst_setLooseTheoryMetaSizeLeeway( VallstInstance * vi, double leeway );


/*! Sets meta leeway.

      Like vallst_setTightTheorySizeLeeway() but used after meta pruning.

      The intention is to have tightTheoryMetaSizeLeeway <=
    looseTheoryMetaSizeLeeway.
*/
void vallst_setTightTheoryMetaSizeLeeway( VallstInstance * vi, double leeway );


/*! Sets leeway.

      Like vallst_setLooseTheorySizeLeeway() but used before meta meta pruning.

      The intention is to have tightTheorySizeLeewayKeep <=
    looseTheorySizeLeewayKeep.
*/
void vallst_setLooseTheorySizeLeewayKeep( VallstInstance * vi, double leeway );


/*! Sets leeway.

      Like vallst_setTightTheorySizeLeeway() but used before meta meta pruning.

      The intention is to have tightTheorySizeLeewayKeep <=
    looseTheorySizeLeewayKeep.
*/
void vallst_setTightTheorySizeLeewayKeep( VallstInstance * vi, double leeway );



/*! Sets the looseTimeLimitBase parameter to k. The heuristic mode timers will
    be something like
    looseTimeLimitBase * looseBias + nrOfRestarts * looseTimeLimitMod.
*/
void vallst_setLooseTimeLimitBase( VallstInstance * vi, unsigned int k );

/*! Sets the looseTimeLimitMod parameter to k. The heuristic mode timers will
    be something like
    looseTimeLimitBase * looseBias + nrOfRestarts * looseTimeLimitMod.
*/
void vallst_setLooseTimeLimitMod( VallstInstance * vi, unsigned int k );

/*! Sets the tightTimeLimitBase parameter to k. The heuristic mode timers will
    be something like
    tightTimeLimitBase * tightBias + nrOfRestarts * tightTimeLimitMod.
*/
void vallst_setTightTimeLimitBase( VallstInstance * vi, unsigned int k );

/*! Sets the tightTimeLimitMod parameter to k. The heuristic mode timers will
    be something like
    tightTimeLimitBase * tightBias + nrOfRestarts * tightTimeLimitMod.
*/
void vallst_setTightTimeLimitMod( VallstInstance * vi, unsigned int k );


/*! Sets the value.

      The value determines the maximal number of times the simplify call
    during search can be skipped (because the theory didn't become sufficently
    much stronger from the last time simplification was made).
*/
void vallst_setMaxSkippedSimps( VallstInstance * vi, VallstFormulaN size );


/*! Sets the value.

      These start and end values determine which clauses are kept during
    pruning. A clause is kept iff it's on or below the line starting at the
    start value and ending at the end value. The actual end point used will be
    the minimum of meta(Meta)PruneEnd and (tight) keep-cc-length-threshold.

      The idea is to keep the meta meta pruning more restrictive and rarer
    than the meta pruning although that's not required.

      See vallst_setKeepCCMetaMetaThreshold() for more on the intended
    relation between different thresholds.
*/
void vallst_setMetaMetaPruneEnd( VallstInstance * vi, VallstLiteralN end );


/*! Sets the frequency.

      The proper non-axioms will be meta meta pruned, using
    metaMetaPruneStart and metaMetaPruneEnd, every metaMetaPruneFrequency-th
    time the search is restarted. You might want to synchronize this value
    with bufferResetFrequency and perhaps also with metaPruneFrequency so
    that metaPruneFrequency is a multiple of bufferResetFrequency and
    metaMetaPruneFrequency is a multiple of metaPruneFrequency.
*/
void vallst_setMetaMetaPruneFrequency( VallstInstance * vi,
                                       VallstFormulaN freq );


//! Sets the value. See vallst_setMetaMetaPruneEnd().
void vallst_setMetaMetaPruneStart( VallstInstance * vi, VallstLiteralN start );


/*! Sets the value. See vallst_setMetaMetaPruneEnd().

      Not that relevant since tightKeepCCThreshold and
    keepConflictClauseLengthThreshold are used as endpoints instead of
    this metaPruneEnd value if metaPruneEnd is larger. Hence you might
    want to leave metaPruneEnd at the default infinite value.
*/
void vallst_setMetaPruneEnd( VallstInstance * vi, VallstLiteralN end );


/*! Sets the frequency.

      The proper non-axioms will be (meta) pruned, using
    metaPruneStart and metaPruneEnd, every metaPruneFrequency-th
    time the search is restarted provided that it's not time for a
    meta meta pruning. You might want to synchronize this 
    value with bufferResetFrequency and perhaps also metaMetaPruneFrequency
    so that metaPruneFrequency is a multiple of bufferResetFrequency and
    metaMetaPruneFrequency is a multiple of metaPruneFrequency.
*/
void vallst_setMetaPruneFrequency( VallstInstance * vi,
                                   VallstFormulaN freq );


//! Sets the value. See vallst_setMetaMetaPruneEnd().
void vallst_setMetaPruneStart( VallstInstance * vi, VallstLiteralN start );


/*! Sets the next-batch-size-const value.

      The restart batch size will possibly increase with nextBatchSizeConst,
    depending on the restart strategy. (The restart batch size may depend
    on other things too.)
*/
void vallst_setNextBatchSizeConst( VallstInstance * vi, double value );


/*! If positiveHeurAxSign is true, the sign of the branching literal will be
    the sign it has in the formula from where it was derived, if it is
    derived from an axiom in the sos-like heuristic set (i.e. if the axiom
    comes late) (see vallst_setHeurAxSize()).

      This can be useful e.g. if you don't want to set the positiveSign to
    true but still want the literals picked from the last axiom to be true,
    e.g. when solving an optimization problem with a large driving last
    axiom to optimize.
*/
void vallst_setPositiveHeurAxSign( VallstInstance * vi, bool b );


/*! Depending on other settings as well, if positiveSign is true, the sign
    of the branching literal will be the sign it has in the formula from
    where it was derived.
*/
void vallst_setPositiveSign( VallstInstance * vi, bool b );



// vallst_setPruningFunction   -- Sets the pruning function.



/*! With prob/1000 probability the sign of the literal to branch on will be
    chosen randomly.

      (This will not affect any added search assumptions of course.)
*/
void vallst_setRandomBranchSign( VallstInstance * vi, unsigned int prob );

/*! With prob/1000 probability the open literal to branch on in a formula
    will be chosen randomly.
*/
void vallst_setRandomFormulaLit( VallstInstance * vi, unsigned int prob );


//! Moved temporary causes no longer active will be removed iff the
//! removeTmpCauses flag is true. This flag will have no very large impact but
//! left-over causes no longer active might screw up some heuristics.(???)
void vallst_setRemoveTmpCauses( VallstInstance * vi, bool b );


//! The flag tells whether buffers should be reset when moving up to level 0
//! between searches.
void vallst_setResetBuffersBetweenSearches( VallstInstance * vi, bool b );


/*! Sets restart batch size function.

      The restart batch size function should return the next batch size,
    which should be greater than 0.

      lastSize is the last batch size. At the very first invocation of each
    search, the value provided will be taken to be firstRestart.

       nrOfRestarts is the number of restarts made so far. Is 0 at each
    search start.
*/
void
vallst_setRestartFunc
( VallstInstance * vi,
  VallstFormulaN (*restartSizeFunc)( VallstInstance * vi,
                                     VallstFormulaN lastSize,
                                     VallstFormulaN nrOfRestarts ) );


/*! Sets the restart batch size function used to the fth function below:

        0: Luby-Sinclair-Zuckerman restart strategy (1,1,2,1,1,2,4,1,1,2,1...)
           with firstRestart used as a base size.

        1: Starting at firstRestart size, the sizes will be incremented using
           nextBatchSizeConst.

      Returns true iff f doesn't designate a legitimate function, i.e. iff f>1.

      To set firstRestart, see vallst_setFirstRestart().
*/
bool vallst_setRestartPredefFunc( VallstInstance * vi, unsigned char f );


/*! Sets the restart batch prolong cap.

      A restart batch won't be prolonged to be (much) more than the value at
    the start of the batch times restartProlongCap.
*/
void vallst_setRestartProlongCap( VallstInstance * vi, double cap );


/*! Sets the start phase size.

      A restart time strictly less than restartStart belongs to the
    start phase of a restart search batch which will possibly imply a
    different branching heuristic from the main phase.
*/
void vallst_setRestartStart( VallstInstance * vi, VallstFormulaN size );


/*! Sets flag.

      Decides which bcp function should be applied first. The other bcp
    function will then be used if a proof improvement is attempted.
*/
void vallst_setStartWithBinFstBcp( VallstInstance * vi, bool b );


/*! Will be greater than or equal to 1. Heuristic strength str is
    considered to be maximal iff leeway * str >= maxStr where maxStr
    is the real maximal strength.

      The Formula variant of leeway (see vallst_setStrengthLeewayFormula()
    below) is used for formula based heuristics. This non-formula variant is
    used elsewhere for absolute heuristics.
*/
void vallst_setStrengthLeeway( VallstInstance * vi, double leeway );

/*! Will be greater than or equal to 1. Heuristic strength str is
    considered to be maximal iff leeway * str >= maxStr where maxStr
    is the real maximal strength.

      This Formula variant of leeway is used for formula based heuristics.
    The non-formula variant (see vallst_setStrengthLeeway() above) is used
    elsewhere for absolute heuristics.
*/
void vallst_setStrengthLeewayFormula( VallstInstance * vi, double leeway );

//! Sets a hard cap of the maximal number of strengths to be considered maximal
//! by the strength-leeway construction (see vallst_setStrengthLeeway()). Will
//! be greater than or equal to 1.
void vallst_setStrengthLeewaySize( VallstInstance * vi,
                                   VallstFormulaN leewaySize );

//! Sets a hard cap of the maximal number of strengths to be considered maximal
//! by the strength-leeway-formula construction (see
//! vallst_setStrengthLeewayFormula()). Will be greater than or equal to 1.
void vallst_setStrengthLeewaySizeFormula( VallstInstance * vi,
                                          VallstFormulaN leewaySize );

//! Sets the tight proof improvement leeway. Like the normal ccLeeway but used
//! when the 1-uips differ. Should probably be 1.0 or slightly greater.
void vallst_setTightCCLeeway( VallstInstance * vi, double leeway );


/*! Like vallst_setKeepConflictClauseLengthThreshold() but for when the
    search heuristic is in tight mode. The intention is to have
    tightKeepCCThreshold <= keepConflictClauseLengthThreshold.
*/
void vallst_setTightKeepCCThreshold( VallstInstance * vi,
                                     VallstLiteralN threshold );

/*! Like vallst_setMetaMetaPruneEnd() but for when the
    search heuristic is in tight mode.
*/
void vallst_setTightMetaMetaPruneEnd( VallstInstance * vi,
                                      VallstLiteralN end );

/*! Like vallst_setMetaMetaPruneStart() but for when the
    search heuristic is in tight mode.
*/
void vallst_setTightMetaMetaPruneStart( VallstInstance * vi,
                                        VallstLiteralN start );

/*! Like vallst_setMetaPruneStart() but for when the
    search heuristic is in tight mode.
*/
void vallst_setTightMetaPruneStart( VallstInstance * vi,
                                    VallstLiteralN start );


/*! Sets the useDoppelganger flag.

      Determines if, when the conflict clause is saved in a non-buffer as a 
    proper non-axiom, an extra copy phantom clause should be added to a
    buffer in order to preserve clause order for branching heuristics.
*/
void vallst_setUseDoppelganger( VallstInstance * vi, bool b );


//\}



/*!\y Simplification */ // -------------------------------------------
//\{


/*
  vallst_compactifyVars       -- Removes gaps in the variables.
*/



//! Returns flag. See vallst_setSubstEqus() and vallst_substEqus().
bool vallst_getSubstEqus( VallstInstance * vi );



/*
  vallst_permuteVars          -- Permute the variables moving related
                                 variables closer together.
  vallst_pruneTheory          -- Prunes the theory.
*/



/*!\v
    Sets the convert-3-clauses flag. 3-clauses on the form:
       p \/  q \/  r
       p \/ -q \/ -r
      -p \/ -q \/  r
      -p \/  q \/ -r
    will be converted into an equivalence <->{p,q,r} iff the convert-3-clauses
    flag is true. p, q and r stand for literals rather than just variables and
    the clauses and the literals in the clauses may be permuted in any way,
    clauses representing an equivalence will still be detected and converted 
    if the 3-clause flag is true. The conversion happens at input, when the 
    fourth clause is added. There may be other formulas added in between the 
    four clauses.\w
*/
void vallst_setConvert3ClausesIntoEqus( VallstInstance * vi, bool b );



//! Sets the time limit in millisecs for fast simplification calls,
//! vallst_simplify().
void vallst_setSimpTimeLimitFast( VallstInstance * vi, unsigned int ms );


//! Sets the time limit in millisecs for slow simplification calls,
//! vallst_simplifySlow().
void vallst_setSimpTimeLimitSlow( VallstInstance * vi, unsigned int ms );



/*! Sets setting for the main, bcp based, simplification, vallst_simplify().

      'level' determines which simplification case the sublevel, nrOfVars and
    nrOfIterations arguments pertain to. 'level' start at 1 so having
    level = 0 is pointless. Having nrOfIterations = 0 will traverse once,
    which might very well be the best strategy.

      The time complexity for vallst_simplify() for a level n typically is
    2^n times the product of the nrOfVars values for that level, not
    counting iterations (nrOfIterations). Hence be mindful of the complexity
    explosion! However, there is a time limit in effect too. See
    vallst_setSimpTimeLimitFast().

      'sublevel' must be less than or equal to level. (Having sublevel=0 makes
    no sense.)

      Return true iff not enough memory could be allocated.

      The default setting for level 1 is a very large nrOfVars value, in
    effect infinite. The default nrOfIterations value for level 1 is 0.
    Other lower levels, especially level 2, might also have some default
    values that imply that simplification will be done on that level.
    Levels not covered thus far get default values like this:
    the default setting for nrOfIterations is 0; the default for nrOfVars
    is 0 if the sublevel is 1, otherwise it is 1.
*/
bool vallst_setSimpSetting( VallstInstance * vi, VallstLiteralN level,
                            VallstLiteralN sublevel,
                            VallstLiteralN nrOfVars,
                            VallstLiteralN nrOfIterations );


/*! Like vallst_setSimpSetting() but used for the slower and stronger
    vallst_simplifySlow(). See also vallst_setSimpTimeLimitSlow().
*/
bool vallst_setSimpSettingSlow( VallstInstance * vi, VallstLiteralN level,
                                VallstLiteralN sublevel,
                                VallstLiteralN nrOfVars,
                                VallstLiteralN nrOfIterations );


/*! Simplifies the problem. BCP based.

      For each level k>0 and each sublevel i, 0<i<=k, in the simplification
    settings, the m=nrOfVars strongest variables and their negations will be
    assumed so that there are k nested assumptions. Then bcp will be applied
    and the cut inferred. This is iterated n=nrOfIterations times.

      See vallst_setSimpSetting() to define how much simplification is done.
    The default setting entails *no* simplification (for the API version; the
    standalone solver will do some simplifications)!

      VallstResult_other will be returned if no other value is applicable.

      VallstResult_other+1 will be returned iff the function couldn't even
    try to do simplifications. This can only happen if certain default
    compiling options are changed (in particular undefining StrHeur).

      Uses the simp-time-limit-fast time limit as time limit (or the overall
    time limit if at the time the overall time limit is smaller). See
    vallst_setSimpTimeLimitFast().

      The fast and weak version. Uses the fast
    simplification settings (confer vallst_setSimpSetting()) in contrast to
    the slow and strong vallst_simplifySlow(), which uses the slow
    simplification settings (confer vallst_setSimpSettingSlow()).
*/
VallstResult vallst_simplify( VallstInstance * vi );


/*! Like vallst_simplify() but slower and stronger. Uses the slow
    simplification settings, confer vallst_setSimpSettingSlow(), and the
    slow time limit, confer vallst_setSimpTimeLimitSlow().
*/
VallstResult vallst_simplifySlow( VallstInstance * vi );


/*! Sets flag. If true, then at least for standalone vallst, variables p
    equivalent to an equivalence a (e.g. p<->a, a:=-q<->r), will be
    substituted in other equivalences. (Equivalences here include xors (-<->).)
*/
void vallst_setSubstEqus( VallstInstance * vi, bool b );


/*! Variables p equivalent to an equivalence a (e.g. p<->a, a:=-q<->r), will be
    substituted in other equivalences. (Equivalences here include xors (-<->).)

      Returns 1 iff a proof of false was found; 2 iff not enough memory could
    be allocated; 0 otherwise.
*/
unsigned char vallst_substEqus( VallstInstance * vi );


//\}



/*!\k Symmetry detection */ // ---------------------------------------
//\{

/*
  vallst_symmetrySearch       -- Searches for symmetries.
*/

//\}



/*!\g Parsing */ // --------------------------------------------------
//\{


//! Closes the in-theory file, if it isn't stdin. Will however *not* reset
//! the in-theory file *name*. Returns true iff fclose returned an error
//! (EOF). Also sets the in-theory file to NULL.
bool vallst_closeInTheoryFile( VallstInstance * vi );

//! Returns the in-theory file.
FILE * vallst_getInTheoryFile( VallstInstance * vi );

//! Returns the in-theory file name.
char * vallst_getInTheoryFileName( VallstInstance * vi );

//! Returns the problem type (see \r3 description above).
unsigned char vallst_getProblemType( VallstInstance * vi );


/*! Parses command line options. vi will be updated according to the
    options. argC and argV work like C's 'main' function arguments.
    VallstResult_other is returned if a help or version flag is encountered.
    VallstResult_other + 1 is returned iff no other VallstResult value is
    applicable, which is usually the case.

      You are free to free the argV memory after the call; vallst won't
    store and use any argV pointer.
*/
VallstResult vallst_parseCommandLineOptions( VallstInstance * vi,
                                             int argC, char * * argV );


/*! Reads the body of an in-theory. At invocation it's assumed that the
    in-theory file pointer is between the head and the body.

      VallstLiteralN_parseError is returned on parse error.
    VallstResult_notEnoughMemory might also be returned.
    VallstResult_other+1 is returned if the newNamePtrFunc returned an error.
    VallstResult_other is returned if no other value is applicable.

      A name of each min/max formula will be saved to a name pointer provided
    by newNamePtrFunc. What is stated for vallst_addNamedAxiom() relating to
    names also holds here. A difference though is that here, the name will be
    assigned NULL if it doesn't point to a vallst axiom (confer *namePtr being
    NULL or pointing to the provided 'axiom' array parameter in the
    vallst_addNamedAxiom() case). If nothing else applies, the name will be
    set to NULL.

      newNamePtrFunc should return a name pointer when called. newNamePtrFunc
    will be called when a name pointer is needed for giving a name to a min/max
    formula. The name pointer returned by newNamePtrFunc will be used to store
    the name of the formula to be named.

    newNamePtrFuncArg is a fixed pointer argument that will be supplied to
    newNamePtrFunc each call.

    If newNamePtrFunc returns NULL, the formula wont be given a name.

    You may set newNamePtrFunc to NULL in which case no formulas will be given
    names.

    If newNamePtrFunc sets *errorFlag to true, the parsing will be aborted and
    VallstResult_other+1 will be returned. *errorFlag is false by default so
    you don't need to set *errorFlag to false in newNamePtrFunc each time.

    The pNrOfVars argument is supposed to be the value returned from the
    preceding vallst_readInTheoryHead() call. (It's currently used only
    for tsp problems.)

    See vallst.c for an example.
*/
VallstResult
vallst_readInTheoryBody
( VallstInstance * vi, VallstLiteralN pNrOfVars,
  VallstFormulaName * (*newNamePtrFunc)( void * newNamePtrFuncArg,
                                         VallstInstance * vi,
                                         bool * errorFlag ),
  void * newNamePtrFuncArg );

//\}


/*!\d
 \v
    A vallst prologue, which is different from the ordinary prologue beginning
    with a 'p', is a line whose first non-white characters are "cv". If numbers
    follow the vallst prologue start, like this:
    "cv [<nrOf3Clauses> [<nrOfLitOccs>]]", the number <nrOf3Clauses> will be
    taken to be the number of ternary clauses and <nrOfLitOccs> will be taken
    to be the number of literal occurrences, modulo some special accounting (do
    a search on "special accounting"). It's not important that nrOf3Clauses is
    exactly accurate but any fairly accurate estimate might be helpful for
    memory efficiency reasons. Try to make nrOfLitOccs an upper bound.
      A vallst prologue must come before the ordinary 'p'-prologue.
      If there are many vallst prologues defining <nrOf3Clauses>, it's the last
    one (containing a <nrOf3Clauses> number) that counts. The same goes for
    <nrOfLitOccs>.\w
*/

/*!\i*/ //\{

/*!
    Reads the head (i.e. any optional prologue) of the in-theory file, placing
    the file pointer just after any optional prologue but before any character
    in the body (i.e. before any character in any formula definition) --- no
    matter what is returned except for file error i.e. when
    VallstLiteralN_fileError is returned.

      Returns the prologue's nrOfVars. If no such prologue nrOfVars can be
    found or vi's ignorePrologue flag is true, the maximal variable occurring
    in the file is returned provided that the file can be reread. If there is
    no prologue nrOfVars and the file can't be reread,
    VallstLiteralN_noPrologueNrOfVars is returned.

      The nrOf3Clauses and nrOfLitOccs values from the vallst prologue, see \r
    description above, will, if present, be read and saved in vi. If the
    whole file is read twice (because of reasons related to nrOfVars; see
    above) *and* no vallst prologue nrOf3Clauses was found and it hasn't been
    set before in some other way, an estimate of the number of ternary
    clauses will be saved in vi; and similar for nrOfLitOccs.

      VallstLiteralN_parseError is returned on parse error.
    VallstLiteralN_fileError is returned on file error.
*/
VallstLiteralN vallst_readInTheoryHead( VallstInstance * vi );


//! Sets the ignore-prologue flag. The prologue nrOfVars, in any in-theory file
//! read, will be ignored, if possible, iff the ignore-prologue flag is true.
void vallst_setIgnorePrologue( VallstInstance * vi, bool b );

//! Sets the in-theory file.
void vallst_setInTheoryFile( VallstInstance * vi, FILE * f );


/*! Sets the in-theory file name. There is no need really to supply a name for
    the in-theory file, if there even is one, since it is only used for error
    messages. NULL is the default.

      The string will *not* be copied and the pointer (fileName) will be saved.
*/
void vallst_setInTheoryFileName( VallstInstance * vi, char * fileName );


/*! Sets flag. If true, it is assumed that pb variables are on the form
    <char><positive_integer>. Otherwise the variables can be any string of
    characters.
*/
void vallst_setPBVarPrefixChar( VallstInstance * vi, bool b );


//! Sets the problem type (see \r3 description above).
void vallst_setProblemType( VallstInstance * vi, unsigned char type );


/*! Sets the pb variable map file.

      The file will be used for any variable mapping. Used for pb problems
    where variables can be arbitrary character strings. The file will contain
    a list of string variable names. The first variable in the file is mapped
    to the first internal variable name (1 or 2), and so on.

      May also be used for holding the prefix character for pb problems if
    the single prefix character mode is used. See vallst_setPBVarPrefixChar().
*/
void vallst_setVarMapFile( VallstInstance * vi, FILE * f );


/*! Sets the pb variable map file name.

      The string will *not* be copied and the pointer (fileName) will be saved.
*/
void vallst_setVarMapFileName( VallstInstance * vi, char * fileName );


//\}



/*!\d0 Printing */ // ------------------------------------------------
//\{

//! Closes the changing-setting file, if it isn't stdout. Will however *not*
//! reset the changing-setting file *name*. Returns true iff fclose returned
//! an error (EOF). Also sets the changing-setting file to NULL.
bool vallst_closeChangingSettingFile( VallstInstance * vi );

//! Closes the out-theory file, if it isn't stdout. Will however *not* reset
//! the out-theory file *name*. Returns true iff fclose returned an error
//! (EOF). Also sets the out-theory file to NULL.
bool vallst_closeOutTheoryFile( VallstInstance * vi );


/*! Returns the changing-setting file.

      If the changing setting is printed it goes to this file. See
    vallst_printChangingSetting().
*/
FILE * vallst_getChangingSettingFile( VallstInstance * vi );


//! Returns the changing-setting file name.
char * vallst_getChangingSettingFileName( VallstInstance * vi );


/*! Returns the complete-model flag determining if partial models will be
    printed as non-partial. See vallst_printModel().
*/
bool vallst_getCompleteModel( VallstInstance * vi );


/*! Returns the out-theory file.

      If the theory is printed it goes to this file. See vallst_printTheory().
*/
FILE * vallst_getOutTheoryFile( VallstInstance * vi );


//! Returns the out-theory file name.
char * vallst_getOutTheoryFileName( VallstInstance * vi );


/*! Returns the print-changing-setting flag.

      If the flag is true, the changing setting will be printed at time-out
    and at interupt. See vallst_printChangingSetting().
*/
bool vallst_getPrintChangingSetting( VallstInstance * vi );


/*! Returns the print-out-theory flag.

      If the flag is true, the theory will be printed at time-out and at
    interupt.
*/
bool vallst_getPrintOutTheory( VallstInstance * vi );


//! Returns the result file, to which any model is printed.
FILE * vallst_getResultFile( VallstInstance * vi );

//! Returns the result file name.
char * vallst_getResultFileName( VallstInstance * vi );

//! Returns the verbosity vector.
//! See \r1 VallstVerbosityVector for what each bit means.
VallstVerbosityVector vallst_getVerbosityVector( VallstInstance * vi );


/*! Prints detailed info about a the hash-table, if the
    VallstVerbosity_hashDetails flag is set.

      If NDEBUG is defined, things will be printed only if forcePrint is true
    (and the VallstVerbosity_hashDetails flag is set).
*/
void vallst_hashStateCheck( FILE * f, VallstInstance * vi, bool forcePrint );


/*! Prints all ggcdit tours. See vallst_printGgcditTour().
*/
bool vallst_printAllGgcditTours( FILE * f, VallstInstance * vi );


/*! Prints changing settings.

      Will print a subset of the settings that typically change during a
    search. Something like this is what will be printed, on a single line
    without a newline character ending the line:
      "  --tight-meta-meta-prune-start=5  --tight-meta-meta-prune-end=7
         --tight-meta-prune-start=9  --tight-keep-cc-threshold=18
         --meta-meta-prune-start=8  --meta-meta-prune-end=12
         --meta-prune-start=30  --keep-conflict-clause-length-threshold=47  "

      The file printed to will be changing-setting-file-name. If
    changing-setting-file-name is NULL, the file used will be
    changing-setting-file. Any previous contents of the file will be
    discarded if changing-setting-file-name isn't NULL. See
    vallst_setChangingSettingFile() and vallst_setChangingSettingFileName().

      If changing-setting-file-name isn't NULL, that file will be assigned to
    changing-setting-file. If the file couldn't be opened, true is returned.
    Otherwise false is returned.


      False is returned iff the destination file couldn't be opened.
*/
bool vallst_printChangingSetting( VallstInstance * vi );


//! Prints the changing setting to file.
void vallst_printChangingSettingToFile( VallstInstance * vi, FILE * file );


/*! Prints estimated prologue values.

    See vallst.c for an example.
*/
void vallst_printEstimatedPrologues( FILE * f,
                                     VallstInstance * vi,
                                     VallstLiteralN pNrOfVars );


/*! Prints the current tour corresponding to the formula 'a', where 'a' should
    be of type VallstFormulaType_ggcdiTour. For example, if the current
    state corresponds to the tour 0->3->1->2->0, "0 3 1 2 0" will be printed.

      Takes linear time in the number of nodes in the graph.

      Returns true iff something went wrong, like e.g. if 'a' isn't of the
    ggcdit type or it's detected that the literals representing the graph
    don't correspond to a tour.

      Note that there is no guarantee that the current state does in fact
    constitute a tour and no exhaustive check of that fact will be done.
    The edge state is just printed as it is without any double checks.
    If you have a model, and everything else is as it should be, then
    what's printed will be a tour. But if something is askew there is no
    guarantee that what's printed is correct or a tour and there is no
    guarantee that the function returns true if there is something wrong.
*/
bool vallst_printGgcditTour( FILE * f, VallstInstance * vi,
                             VallstFormulaName a );


//! Prints some, easily obtainable, info about the hash-table.
void vallst_printHashInfo( FILE * f, VallstInstance * vi );


/*! Prints the current value of the variables to 'file'. The notation 
    used will be DIMACS so that e.g. if the negated variable 7 is
    true it will be printed as -3. Only true literals are printed.

      If 'file' is NULL, the default output result file will be used
    except when that also is NULL in which case stdout is used.

      Open variables, who is not in an equ-class with more than one member,
    will be printed (as true) if the complete-model flag is true. See
    vallst_setCompleteModel().

      Members of an open equivalence class with more than one member will be
    printed as having a truth value.
*/
void vallst_printModel( FILE * file, VallstInstance * vi );


//! Prints the number of unchecked variables.
void vallst_printNrOfUncheckedVars( FILE * f, VallstInstance * vi );

//! Prints the number of variables that have been given a truth-value.
void vallst_printNrOfVarsSet(  FILE * f, VallstInstance * vi );



/*
  vallst_printOpenTheory      -- Prints the current theory but without the
                                 variable history.
*/



/*! Prints hindsighted prologue values.

    See vallst.c for an example.
*/
void vallst_printPrologues( FILE * f, VallstInstance * vi );

//! Prints option settings. sep is used as a separator between options and can
//! e.g. be ' ' (space) or '\\n' (newline).
void vallst_printSettings( FILE * f, VallstInstance * vi, char sep );


/*! Prints the current theory.

      The file printed to will be out-theory-file-name. If out-theory-file-name
    is NULL, the file used will be out-theory-file. Any previous contents of
    the file will be discarded if out-theory-file-name isn't NULL.
    See vallst_setOutTheoryFile() and vallst_setOutTheoryFileName().

      If out-theory-file-name isn't NULL, that file will be assigned to
    out-theory-file. If the file couldn't be opened, true is returned.
    Otherwise false is returned.

      "max" will be augmented to the prints of constraint formulas of type <,
    <* and <\/ in optMax. This doesn't affect other types of formulas. If
    optMax is NULL, no "max" will be printed. (Note that a "max" for <\/ might
    not make much sense.)
*/
bool vallst_printTheory( VallstInstance * vi, VallstFormulaNames * optMax );


/*! Prints the current theory to file.

      "max" will be augmented to the prints of constraint formulas of type <,
    <* and <\/ in optMax. This doesn't affect other types of formulas. If
    optMax is NULL, no "max" will be printed. (Note that a "max" for <\/ might
    not make much sense.)
*/
void vallst_printTheoryToFile( VallstInstance * vi, FILE * file,
                               VallstFormulaNames * optMax );

//! Prints the cpu time used.
void vallst_printTimePassed( FILE * f, VallstInstance * vi );

//! Prints to f a short string corresponding to a VallstResult.
void vallst_printVallstResult( FILE * f, VallstResult result );



/*
  vallst_printVarHistory      -- Prints the variable history.
*/



/*! Sets the changing-setting file. See vallst_printChangingSetting().
*/
void vallst_setChangingSettingFile( VallstInstance * vi, FILE * f );

//! Sets the changing-setting file name. See vallst_printChangingSetting().
//! The string will *not* be copied and the pointer (fileName) will be saved.
void vallst_setChangingSettingFileName( VallstInstance * vi, char * fileName );


/*! Sets the complete-model flag determining if partial models will be
    printed as non-partial. See vallst_printModel().
*/
void vallst_setCompleteModel( VallstInstance * vi, bool b );


/*! Sets the out-theory file. See vallst_printTheory().
*/
void vallst_setOutTheoryFile( VallstInstance * vi, FILE * f );

//! Sets the out-theory file name. See vallst_printTheory().
//! The string will *not* be copied and the pointer (fileName) will be saved.
void vallst_setOutTheoryFileName( VallstInstance * vi, char * fileName );


/*! Sets the print-changing-setting flag.

      If the flag is true, the changing setting will be printed at time-out
    and at interupt.
*/
void vallst_setPrintChangingSetting( VallstInstance * vi, bool b );


/*! Sets the print-out-theory flag.

      If the flag is true, the theory will be printed at time-out and at
    interupt.
*/
void vallst_setPrintOutTheory( VallstInstance * vi, bool b );


//! Sets the result file, to which any model is printed.
void vallst_setResultFile( VallstInstance * vi, FILE * f );

//! Sets the result file name. The string will *not* be copied and the pointer
//! (fileName) will be saved.
void vallst_setResultFileName( VallstInstance * vi, char * fileName );


/*! Sets the verbosity level. 0 is quiet; only some error messages are printed.
    99 is maximally verbose. What this function does is to set the verbosity
    vector to something seemingly appropriate. If you want to fine-tune, use
    vallst_setVerbosityVector().
*/
void vallst_setVerbosityLevel( VallstInstance * vi, unsigned int vl );


//! Sets the verbosity vector to vv. 0 is quiet; only some error messages is
//! printed. See \r1 VallstVerbosityVector for what each bit means.
void vallst_setVerbosityVector( VallstInstance * vi,
                                VallstVerbosityVector vv );


//\}



/*!\d3 Callback */ // ------------------------------------------------
//\{

/*! Sets the callback function. callbackArg is an argument that will be used on
    every call to callbackFunc. callbackFunc will be called regularly e.g. in
    vallst_search().

      The default callback function is a function that always returns
    VallstCallbackResult_continue. In vallst standalone the callback function
    is one that handles interupt signals (see vallst.c).
*/
void
vallst_setCallback( VallstInstance * vi,
                    VallstCallbackResult (*callbackFunc)(void * callbackArg),
                    void * callbackArg );


//\}



/*!\d1 Formula name allocation */ // ---------------------------------
//\{

//! Extends the name array. Returns true iff it fails.
bool vallst_extendFormulaNameArray( VallstFormulaNames * names );

//! Returns a new formula name array with n elements. Returns NULL if it fails.
//! If n is 0, a size 1 array will be allocated.
VallstFormulaNames * vallst_newFormulaNameArray( VallstFormulaN n );


//\}



/*!\d5 Graph coding */ // --------------------------------------------
//\{

/*! The intended meaning of this macro is a mapping from graph edge (i,j)
    to the corresponding vallst literal representing the edge.

    vallst_ggcditEdgeToLit defines a canonical mapping between the edges
    (i,j) in a complete directed irreflexive graph with dim many nodes, and
    vallst literals representing the edges, with i!=j, 0<=i<dim and 0<=j<dim.

    Here the first vallst literal representing an edge is assumed to be 2.
    If that's not the case but instead the coding starts with literal q,
    just adjust the returned values accordingly. E.g. if q=5 starts the
    representation, just add 3 (5-2 (q-2)) to values returned by
    vallst_ggcditEdgeToLit.

    VallstFormulaType_ggcdiTour assumes the coding defined by
    vallst_ggcditEdgeToLit (except possibly for some other vallst start
    literal q). See \ref VallstFormulaType_ggcdiTour for more.
*/
#define vallst_ggcditEdgeToLit(i,j,dim)  \
    ( 2 * ( ((dim)-1) * (i) + (j) + ((j)<(i)) ) )


/*! The inverse of vallst_ggcditEdgeToLit(), mapping the literals p and -p
    representing (i,j) to (i,j), assigning i and j. See
    vallst_ggcditEdgeToLit() and \ref VallstFormulaType_ggcdiTour. If e.g.
    your edge representation starts with q=5 instead of the default 2,
    subtract 2 to the representing p when calling vallst_ggcditLitToEdge
    (i.e. subtract q-2+"q is odd" (i.e. subtract (q-2+q%2))).
*/
#define vallst_ggcditLitToEdge(p,dim,i,j)  \
do                                         \
{                                          \
    (j) = (p)/2 - 1;                       \
    (i) = (j) / ((dim)-1);                 \
    (j) = (j) % ((dim)-1);                 \
    (j) += (i) <= (j);                     \
}                                          \
while (0)


/*! The first part of the inverse of vallst_ggcditEdgeToLit(), mapping the
    literals p and -p representing (i,j) to i. See vallst_ggcditEdgeToLit()
    and \ref VallstFormulaType_ggcdiTour.
*/
#define vallst_ggcditLitToEdgeFst(p,dim)  ( ( (p)/2 - 1 )  /  ((dim)-1) )


//\}



/*!\s Optimization */ // ---------------------------------------------
//\{

/*! Returns the optimization strategy flag.

    If true, min/max formulas will be optimized in a breadth first fashion
    e.g. in vallst standalone. Otherwise the last min/max axiom will be the
    one pushed. See vallst.c.
*/
bool vallst_getBreadthFstOptStrat( VallstInstance * vi );


/*! Calculates the maximum amount the constraint constants in 'names' can be
    raised while still maintaining the model. The calculated max amounts
    will be placed in constraintIncs like this: pushedConstraintPos will
    correspond to constraintIncs+0; prev(pushedConstraintPos) to
    constraintIncs+1; ...

      Semi-completes the model for open literals in the constraints. The
    literals will all be set on one level greater than the
    current one. Note that that is a bit of a hack since all the literals on
    that level will really be assumptions and not consequences. However,
    since the open literals set could be very many and there shouldn't be any
    problem with this hack, they are collected to one level. You can undo the
    semi-completion by moving up one level (i.e. undoing one level,
    moving to a lesser level). See vallst_undoLevel().

      However, if no literal was set, no new level will be created. If
    levelCreated isn't NULL, *levelCreated will be set to true iff a new level
    was created; otherwise it is set to false.

      Returns true iff an out of memory error occurred.

      pushedConstraintPos must be the position of a constraint in 'names'.
    pushedConstraintPos will be the first position processed. Then
    prev(pushedConstraintPos) will be processed, and so on.

      The state should be a model (i.e. all axioms should be satisfied).

      The raise for formulas of type <\/ where the left disjunct is true will
    be set to 0.

      See vallst.c for an example.
*/
bool vallst_maxConstraints( VallstInstance * vi,
                            VallstFormulaNames * names,
                            VallstFormulaN pushedConstraintPos,
                            VallstLiteralN * constraintIncs,
                            bool * levelCreated );


/*! Sets the optimization strategy flag.

    If true, min/max formulas will be optimized in a breadth first fashion
    e.g. in vallst standalone. Otherwise the last min/max axiom will be the
    one pushed. See \ref vallst.c.
*/
void vallst_setBreadthFstOptStrat( VallstInstance * vi, bool b );


//\}



/*!\z Seed */ // -----------------------------------------------------
//\{

//! Returns the seed used.
unsigned int vallst_getSeed( VallstInstance * vi );


/*! Sets the seed.

      Before you start all over on a completely new problem you might want to
    call this function (e.g. with seed=time(NULL)) in order to know what the
    seed value is for the new problem.
*/
void vallst_setSeed( VallstInstance * vi, unsigned int seed );


//\}



/*!\d2 Timers */ // --------------------------------------------------
//\{


// The sub-time limit isn't included in the api any longer.
#if 0
/*! Sets the time limit in milliseconds for sub-processes. See
    vallst_setTimeLimitInMilliSec(). The sub-processes affected are those that 
    can take a lot of time: vallst_symmetrySearch(), vallst_search() and
    vallst_simplify().

      Note that all vi's time limits will decrease as time passes so if you
    e.g. set a time limit to 242 ms, do a vallst_search() and then want to do
    another vallst_search() with 242 ms time limit you will have to set the
    time timit again.
*/
void vallst_setTimeLimitForSubProcInMilliSec( VallstInstance * vi,
                                              long long int milliSec,
                                              bool startFromCurrentClock );


//! Sets time limit in seconds for sub-processes. See
//! vallst_setTimeLimitForSubProcInMilliSec().
void vallst_setTimeLimitForSubProcInSec( VallstInstance * vi,
                                         unsigned int sec,
                                         bool startFromCurrentClock );
#endif


/*! Sets the overall time limit in milliseconds.

      If startFromCurrentClock is true, the timer will start counting toward
    the time limit from the current clock. Otherwise the counting is from when
    the main program was started. With startFromCurrentClock=false the timer
    is only guaranteed to be accurate if vallst_setTimeLimitInMilliSec()
    (or vallst_setTimeLimitInSec()) was called within 35 min from when the
    main program was started.
*/
void vallst_setTimeLimitInMilliSec( VallstInstance * vi,
                                    long long int milliSec,
                                    bool startFromCurrentClock );


//! Sets the overall time limit in seconds. See
//! vallst_setTimeLimitInMilliSec().
void vallst_setTimeLimitInSec( VallstInstance * vi, unsigned int sec,
                               bool startFromCurrentClock );


//\}



// Misc:

// There is only standalone support for this yet, sort of.
void vallst_setNrOfVarsSetAtStartIs0( VallstInstance * vi, bool b );



#ifdef __cplusplus
}
#endif

#endif // vallstAPI_H

---