z3 / src / front_end_params / cnf_params.h

/*++
Copyright (c) 2006 Microsoft Corporation

Module Name:

    cnf_params.h

Abstract:

    <abstract>

Author:

    Leonardo de Moura (leonardo) 2008-01-23.

Revision History:

--*/
#ifndef _CNF_PARAMS_H_
#define _CNF_PARAMS_H_

#include"ini_file.h"

/**
   \brief CNF translation mode.  The cheapest mode is CNF_QUANT, and
   the most expensive is CNF_FULL.
*/
enum cnf_mode {
    CNF_DISABLED, /* CNF translator is disabled. 
                     This mode is sufficient when using E-matching.
                  */
    CNF_QUANT, /* A subformula is put into CNF if it is inside of a
                  quantifier.
               
                  This mode is sufficient when using Superposition
                  Calculus.
               */
    CNF_OPPORTUNISTIC, /* a subformula is also put in CNF if it is cheap. */
    CNF_FULL /* Everything is put into CNF, new names are introduced
                if it is too expensive. */
};

struct cnf_params {
    cnf_mode m_cnf_mode;
    unsigned m_cnf_factor;
    cnf_params():
        m_cnf_mode(CNF_DISABLED),
        m_cnf_factor(4) {
    }
    
    void register_params(ini_params & p);
};


#endif /* _CNF_PARAMS_H_ */
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.