1/****************************************** 2Copyright (c) 2016, Mate Soos 3 4Permission is hereby granted, free of charge, to any person obtaining a copy 5of this software and associated documentation files (the "Software"), to deal 6in the Software without restriction, including without limitation the rights 7to use, copy, modify, merge, publish, distribute, sublicense, and/or sell 8copies of the Software, and to permit persons to whom the Software is 9furnished to do so, subject to the following conditions: 10 11The above copyright notice and this permission notice shall be included in 12all copies or substantial portions of the Software. 13 14THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR 15IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, 16FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE 17AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER 18LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, 19OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN 20THE SOFTWARE. 21***********************************************/ 22 23#ifndef __CRYPTOMINISAT5_H__ 24#define __CRYPTOMINISAT5_H__ 25 26#define CRYPTOMINISAT_VERSION_MAJOR @PROJECT_VERSION_MAJOR@ 27#define CRYPTOMINISAT_VERSION_MINOR @PROJECT_VERSION_MINOR@ 28#define CRYPTOMINISAT_VERSION_PATCH @PROJECT_VERSION_PATCH@ 29 30#include <atomic> 31#include <vector> 32#include <iostream> 33#include <utility> 34#include <string> 35#include "cryptominisat5/solvertypesmini.h" 36 37namespace CMSat { 38 struct CMSatPrivateData; 39 #ifdef _WIN32 40 class __declspec(dllexport) SATSolver 41 #else 42 class SATSolver 43 #endif 44 { 45 public: 46 //////////////////////////// 47 // You can pass in a variable that if set to TRUE, will abort the 48 // solver as soon as possible. This bool can be set through a timer, 49 // or through a thread, etc. This gives you the possiblity to abort 50 // the solver any time you like, depending on some external factor 51 // such as time, or your own code's inner workings. 52 SATSolver(void* config = NULL 53 , std::atomic<bool>* interrupt_asap = NULL 54 ); 55 ~SATSolver(); 56 57 //////////////////////////// 58 // Adding variables and clauses 59 //////////////////////////// 60 61 void new_var(); //add a new variable to the solver 62 void new_vars(const size_t n); //and many new variables to the solver -- much faster 63 unsigned nVars() const; //get number of variables inside the solver 64 bool add_clause(const std::vector<Lit>& lits); 65 bool add_xor_clause(const std::vector<unsigned>& vars, bool rhs); 66 void set_var_weight(Lit lit, double weight); 67 68 //////////////////////////// 69 // Solving and simplifying 70 // You can call solve() multiple times: incremental mode is supported! 71 //////////////////////////// 72 73 lbool solve(const std::vector<Lit>* assumptions = 0, bool only_indep_solution = false); //solve the problem, optionally with assumptions. If only_indep_solution is set, only the independent variables set with set_independent_vars() are returned in the solution 74 lbool simplify(const std::vector<Lit>* assumptions = 0); //simplify the problem, optionally with assumptions 75 const std::vector<lbool>& get_model() const; //get model that satisfies the problem. Only makes sense if previous solve()/simplify() call was l_True 76 const std::vector<Lit>& get_conflict() const; //get conflict in terms of the assumptions given in case the previous call to solve() was l_False 77 bool okay() const; //the problem is still solveable, i.e. the empty clause hasn't been derived 78 const std::vector<Lit>& get_decisions_reaching_model() const; //get decisions that lead to model. may NOT work, in case the decisions needed were internal, extended variables. exit(-1)'s in case of such a case. you MUST check decisions_reaching_computed(). 79 80 //////////////////////////// 81 // Debug all calls for later replay with --debuglit FILENAME 82 //////////////////////////// 83 void log_to_file(std::string filename); 84 85 //////////////////////////// 86 // SQLite for statistics gathering 87 //////////////////////////// 88 void set_sqlite(std::string filename); 89 void add_sql_tag(const std::string& tagname, const std::string& tag); 90 unsigned long get_sql_id() const; 91 92 //////////////////////////// 93 // Configuration 94 // -- Note that nothing else can be changed, only these. 95 // -- The main.cpp has access to the internal config, but it changes 96 // -- all the time and hence exposing it to the outside world would 97 // -- be very brittle. 98 //////////////////////////// 99 100 void set_num_threads(unsigned n); //Number of threads to use. Must be set before any vars/clauses are added 101 void set_allow_otf_gauss(); //allow on-the-fly gaussian elimination 102 /** 103 * CPU time (in seconds) that can be consumed before the next call to solve() must return 104 * 105 * Because the elapsed CPU time depends on both the number of 106 * threads, and the activity of these threads, the elapsed time 107 * can wildly differ from wall clock time. 108 * 109 * \pre max_time >= 0 110 */ 111 void set_max_time(double max_time); 112 /** 113 * Conflicts that can be consumed before the next call to solve() must return 114 * 115 * \pre max_confl >= 0 116 */ 117 void set_max_confl(int64_t max_confl); 118 void set_verbosity(unsigned verbosity = 0); //default is 0, silent 119 void set_verbosity_detach_warning(bool verb); //default is 0, silent 120 void set_default_polarity(bool polarity); //default polarity when branching for all vars 121 void set_no_simplify(); //never simplify 122 void set_no_simplify_at_startup(); //doesn't simplify at start, faster startup time 123 void set_no_equivalent_lit_replacement(); //don't replace equivalent literals 124 void set_no_bva(); //No bounded variable addition 125 void set_no_bve(); //No bounded variable elimination 126 void set_yes_comphandler(); //Allow component handler to work 127 void set_greedy_undef(); //Try to set variables to l_Undef in solution 128 void set_sampling_vars(std::vector<uint32_t>* sampl_vars); 129 void set_timeout_all_calls(double secs); //max timeout on all subsequent solve() or simplify 130 void set_up_for_scalmc(); //used to set the solver up for ScalMC configuration 131 void set_single_run(); //we promise to call solve() EXACTLY once 132 void set_intree_probe(int val); 133 void set_sls(int val); 134 void set_full_bve(int val); 135 void set_full_bve_iter_ratio(double val); 136 void set_scc(int val); 137 void set_bva(int val); 138 void set_distill(int val); 139 void reset_vsids(); 140 void set_no_confl_needed(); //assumptions-based conflict will NOT be calculated for next solve run 141 void set_xor_detach(bool val); 142 143 144 //////////////////////////// 145 // Get generic info 146 //////////////////////////// 147 static const char* get_version(); //get solver version in string format 148 static const char* get_version_sha1(); //get SHA1 version string of the solver 149 static const char* get_compilation_env(); //get compilation environment string 150 std::string get_text_version_info(); //get printable version and copyright text 151 152 153 //////////////////////////// 154 // Get info about only the last solve() OR simplify() call 155 // summed for all threads 156 //////////////////////////// 157 uint64_t get_last_conflicts(); //get total number of conflicts of last solve() or simplify() call of all threads 158 uint64_t get_last_propagations(); //get total number of propagations of last solve() or simplify() call made by all threads 159 uint64_t get_last_decisions(); //get total number of decisions of last solve() or simplify() call made by all threads 160 161 162 //////////////////////////// 163 //Get info about total sum of all time of all threads 164 //////////////////////////// 165 166 uint64_t get_sum_conflicts(); //get total number of conflicts of all time of all threads 167 uint64_t get_sum_conflicts() const; //!< Return sum of all conflicts since construction across all the threads 168 uint64_t get_sum_propagations(); //get total number of propagations of all time made by all threads 169 uint64_t get_sum_propagations() const; //!< Returns sum of all propagations since construction across all the threads 170 uint64_t get_sum_decisions(); //get total number of decisions of all time made by all threads 171 uint64_t get_sum_decisions() const; //!< Returns sum of all decisions since construction across all the threads 172 173 void print_stats() const; //print solving stats. Call after solve()/simplify() 174 void set_drat(std::ostream* os, bool set_ID); //set drat to ostream, e.g. stdout or a file 175 void add_empty_cl_to_drat(); // allows to treat SAT as UNSAT and perform learning 176 void interrupt_asap(); //call this asynchronously, and the solver will try to cleanly abort asap 177 void dump_irred_clauses(std::ostream *out) const; //dump irredundant clauses to this stream when solving finishes 178 void dump_red_clauses(std::ostream *out) const; //dump redundant ("learnt") clauses to this stream when solving finishes 179 void open_file_and_dump_irred_clauses(std::string fname) const; //dump irredundant clauses to this file when solving finishes 180 void open_file_and_dump_red_clauses(std::string fname) const; //dump redundant ("learnt") clauses to this file when solving finishes 181 void add_in_partial_solving_stats(); //used only by Ctrl+C handler. Ignore. 182 183 //////////////////////////// 184 // Extract useful information from the solver 185 // This can be used in the theory solver 186 187 //////////////////////////// 188 std::vector<Lit> get_zero_assigned_lits() const; //get literals of fixed value 189 std::vector<std::pair<Lit, Lit> > get_all_binary_xors() const; //get all binary XORs that are = 0 190 191 ////////////////////// 192 // EXPERIMENTAL 193 std::vector<std::pair<std::vector<uint32_t>, bool> > get_recovered_xors(bool xor_together_xors) const; //get XORs recovered. If "xor_together_xors" is TRUE, then xors that share a variable (and ONLY they share them) will be XORed together 194 std::vector<uint32_t> get_var_incidence(); 195 std::vector<uint32_t> get_var_incidence_also_red(); 196 std::vector<double> get_vsids_scores(); 197 198 //Given a set of literals to enqueue, returns: 199 // 1) Whether they imply SAT/UNSAT. If "true": SAT. If "false": UNSAT 200 // 2) into "out_implied" the set of literals they imply, including the literals themselves 201 // NOTES: 202 // * You may get back some of the literals you gave 203 // * Order is not guaranteed: literals you gave as input may end up at the end or may not end up at all 204 // * It only returns literals that are newly implied. So you must call get_zero_assigned_lits() before to be sure you know what literals are implied at decision level 0 205 206 bool implied_by( 207 const std::vector<Lit>& lits, std::vector<Lit>& out_implied); 208 209 ////////////////////// 210 //Below must be done in-order. Multi-threading not allowed. 211 void start_getting_small_clauses(uint32_t max_len, uint32_t max_glue); 212 bool get_next_small_clause(std::vector<Lit>& ret); //returns FALSE if no more 213 void end_getting_small_clauses(); 214 215 private: 216 217 //////////////////////////// 218 // Do not bother with this, it's private 219 //////////////////////////// 220 221 CMSatPrivateData *data; 222 }; 223} 224 225#endif //__CRYPTOMINISAT5_H__ 226