z3 / src / front_end_params / cnf_params.h

Copyright (c) 2006 Microsoft Corporation

Module Name:





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

Revision History:

#ifndef _CNF_PARAMS_H_
#define _CNF_PARAMS_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
                  This mode is sufficient when using Superposition
    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;
        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.