Main.h 4.77 KB
Newer Older
Masahiko Sakai's avatar
Masahiko Sakai committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
/******************************************************************************************[Main.h]
Copyright (c) 2005-2010, Niklas Een, Niklas Sorensson

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
including without limitation the rights to use, copy, modify, merge, publish, distribute,
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/

#ifndef Main_h
#define Main_h

#include "Int.h"
Masahiko Sakai's avatar
Masahiko Sakai committed
24 25
#include "Version.h"
#include "FEnv.h"
Masahiko Sakai's avatar
Masahiko Sakai committed
26 27 28 29 30 31 32 33 34

//=================================================================================================


enum SolverT  { st_MiniSat, st_SatELite, st_GlueMiniSat, st_MiniSat22, st_Glucose10, st_ES1Sat, st_CCMiniSat};
enum ConvertT { ct_Sorters, ct_Adders, ct_BDDs, ct_Mixed, ct_Mixed2, ct_Undef };
enum Command  { cmd_Minimize, cmd_FirstSolution, cmd_AllSolutions, cmd_InterestSolutions, cmd_Soft };
enum GpwT     { gt_none, gt_positive, gt_negative, gt_low, gt_high, gt_both };

Masahiko Sakai's avatar
Masahiko Sakai committed
35 36 37 38 39
// Controlling optimization
extern bool    minimization_mode;     // turned on after first SAT-solver execution
extern std::map<Pair< int, Pair< Interval<Int> , Interval<Int> > >, Pair<Pair< Interval<Int> , Interval<Int> >, Formula> > memo_bdd_conv_int_in_min_mode;
extern Map<Pair<int,Int>, Formula>  memo_bdd_conv_in_min_mode;      

Masahiko Sakai's avatar
Masahiko Sakai committed
40 41 42 43 44 45 46
// -- output options:
extern bool     opt_satlive;
extern bool     opt_ansi;
extern char*    opt_cnf;
extern int      opt_verbosity;
extern bool     opt_try;
extern bool     opt_model_out;
Masahiko Sakai's avatar
Masahiko Sakai committed
47 48
extern bool     opt_dimacs;
extern bool     opt_eager_cl;
Masahiko Sakai's avatar
Masahiko Sakai committed
49 50 51

// -- solver options:
extern SolverT  opt_solver;
Masahiko Sakai's avatar
Masahiko Sakai committed
52
extern bool	opt_simp_solver;
Masahiko Sakai's avatar
Masahiko Sakai committed
53 54
extern ConvertT opt_convert;
extern ConvertT opt_convert_goal;
Masahiko Sakai's avatar
Masahiko Sakai committed
55
extern bool     opt_convert_goal_reusing;
Masahiko Sakai's avatar
Masahiko Sakai committed
56 57 58 59 60 61 62
extern GpwT     opt_convert_gpw;
extern bool     opt_convert_bdd_monotonic;
//extern bool     opt_convert_bdd_binary_decomposition;
extern int      opt_convert_bdd_decomposition;
extern bool     opt_convert_bdd_interval;
extern bool     opt_convert_bdd_increasing_order;
extern bool     opt_convert_weak;
Masahiko Sakai's avatar
Masahiko Sakai committed
63
extern int      opt_opt_base_method;
Masahiko Sakai's avatar
Masahiko Sakai committed
64 65 66 67 68 69 70 71 72 73
extern bool     opt_or_detection;
extern bool     opt_es1_detection;
extern bool     opt_cc_detection;
extern bool     opt_cc_sort;
extern int      opt_avoid_band_constraint;
extern bool     opt_split;
extern int      opt_cc_thres;
extern double   opt_bdd_thres;
extern double   opt_sort_thres;
extern double   opt_goal_bias;
Masahiko Sakai's avatar
Masahiko Sakai committed
74
extern int      opt_bdd_max_const;
Masahiko Sakai's avatar
Masahiko Sakai committed
75 76 77 78
extern Int      opt_goal;
extern Command  opt_command;
//extern bool     opt_binary_minimization;
extern int      opt_minimization;
Masahiko Sakai's avatar
Masahiko Sakai committed
79 80
extern int      opt_bin_coeff;
extern int      opt_seq_thres;
Masahiko Sakai's avatar
Masahiko Sakai committed
81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
extern bool     opt_band_for_goal;
extern bool     opt_goal_gcd;
extern bool     opt_branch_pbvars;
extern bool     opt_branch_goal_vars;
extern int      opt_polarity_sug;
extern bool     opt_extract_ucore;
extern int      opt_ucore_mode;

// -- extra stats
extern int      stats_bdd_cost;
extern int      stats_sort_cost;
extern int      stats_adder_cost;
extern int      stats_bdd_raw_constraints;
extern int      stats_bdd_bin_constraints;
extern int      stats_bdd_mul_constraints;
extern int      stats_sort_constraints;
extern int      stats_adder_constraints;
extern int      stats_monotonic_coding,stats_non_monotonic_coding;
extern int      stats_std_form,stats_band_form;
extern int      stats_sat_calls,stats_unsat_calls;
extern int      stats_bdd_nodes;
extern int      stats_es1_detection;
extern int      stats_cc_detection;
extern double   stats_cnf_coding_time;
Masahiko Sakai's avatar
Masahiko Sakai committed
105
extern double   stats_opt_base_calc_time;
Masahiko Sakai's avatar
Masahiko Sakai committed
106 107 108 109 110 111 112 113 114 115 116 117 118 119 120

// -- debug:
extern bool     opt_model_check;
// -- files:
extern char*    opt_input;
extern char*    opt_result;

//- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

void reportf(const char* format, ...);      // 'printf()' replacer -- will put "c " first at each line if 'opt_satlive' is TRUE.


//=================================================================================================

#endif