1 /********************* */ 2 /*! \file quantifiers_modes.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Andrew Reynolds, Tim King, Morgan Deters 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS 8 ** in the top-level source directory) and their institutional affiliations. 9 ** All rights reserved. See the file COPYING in the top-level source 10 ** directory for licensing information.\endverbatim 11 ** 12 ** \brief [[ Add one-line brief description here ]] 13 ** 14 ** [[ Add lengthier description here ]] 15 ** \todo document this file 16 **/ 17 18 #include "cvc4_public.h" 19 20 #ifndef __CVC4__BASE__QUANTIFIERS_MODES_H 21 #define __CVC4__BASE__QUANTIFIERS_MODES_H 22 23 #include <iostream> 24 25 namespace CVC4 { 26 namespace theory { 27 namespace quantifiers { 28 29 enum InstWhenMode { 30 /** Apply instantiation round before full effort (possibly at standard effort) */ 31 INST_WHEN_PRE_FULL, 32 /** Apply instantiation round at full effort or above */ 33 INST_WHEN_FULL, 34 /** Apply instantiation round at full effort, after all other theories finish, or above */ 35 INST_WHEN_FULL_DELAY, 36 /** Apply instantiation round at full effort half the time, and last call always */ 37 INST_WHEN_FULL_LAST_CALL, 38 /** Apply instantiation round at full effort after all other theories finish half the time, and last call always */ 39 INST_WHEN_FULL_DELAY_LAST_CALL, 40 /** Apply instantiation round at last call only */ 41 INST_WHEN_LAST_CALL, 42 }; 43 44 enum LiteralMatchMode { 45 /** Do not consider polarity of patterns */ 46 LITERAL_MATCH_NONE, 47 /** Conservatively consider polarity of patterns */ 48 LITERAL_MATCH_USE, 49 /** Aggressively consider polarity of Boolean predicates */ 50 LITERAL_MATCH_AGG_PREDICATE, 51 /** Aggressively consider polarity of all terms */ 52 LITERAL_MATCH_AGG, 53 }; 54 55 enum MbqiMode { 56 /** no mbqi */ 57 MBQI_NONE, 58 /** default, mbqi from Section 5.4.2 of AJR thesis */ 59 MBQI_FMC, 60 /** mbqi trust (produce no instantiations) */ 61 MBQI_TRUST, 62 }; 63 64 enum QcfWhenMode { 65 /** default, apply at full effort */ 66 QCF_WHEN_MODE_DEFAULT, 67 /** apply at last call */ 68 QCF_WHEN_MODE_LAST_CALL, 69 /** apply at standard effort */ 70 QCF_WHEN_MODE_STD, 71 /** apply based on heuristics */ 72 QCF_WHEN_MODE_STD_H, 73 }; 74 75 enum QcfMode { 76 /** default, use qcf for conflicts only */ 77 QCF_CONFLICT_ONLY, 78 /** use qcf for conflicts and propagations */ 79 QCF_PROP_EQ, 80 /** use qcf for conflicts, propagations and heuristic instantiations */ 81 QCF_PARTIAL, 82 }; 83 84 /** User pattern mode. 85 * 86 * These modes determine how user provided patterns (triggers) are 87 * used during E-matching. The modes vary on when instantiation based on 88 * user-provided triggers is combined with instantiation based on 89 * automatically selected triggers. 90 */ 91 enum UserPatMode 92 { 93 /** First instantiate based on user-provided triggers. If no instantiations 94 * are produced, use automatically selected triggers. 95 */ 96 USER_PAT_MODE_USE, 97 /** Default, if triggers are supplied for a quantifier, use only those. */ 98 USER_PAT_MODE_TRUST, 99 /** Resort to user triggers only when no instantiations are 100 * produced by automatically selected triggers 101 */ 102 USER_PAT_MODE_RESORT, 103 /** Ignore user patterns. */ 104 USER_PAT_MODE_IGNORE, 105 /** Interleave use/resort modes for quantified formulas with user patterns. */ 106 USER_PAT_MODE_INTERLEAVE, 107 }; 108 109 /** Trigger selection mode. 110 * 111 * These modes are used for determining which terms to select 112 * as triggers for quantified formulas, when necessary, during E-matching. 113 * In the following, note the following terminology. A trigger is a set of terms, 114 * where a single trigger is a singleton set and a multi-trigger is a set of more 115 * than one term. 116 * 117 * TRIGGER_SEL_MIN selects single triggers of minimal term size. 118 * TRIGGER_SEL_MAX selects single triggers of maximal term size. 119 * 120 * For example, consider the quantified formula : 121 * forall xy. P( f( g( x, y ) ) ) V Q( f( x ), y ) 122 * 123 * TRIGGER_SEL_MIN will select g( x, y ) and Q( f( x ), y ). 124 * TRIGGER_SEL_MAX will select P( f( g( x ) ) ) and Q( f( x ), y ). 125 * 126 * The remaining three trigger selections make a difference for multi-triggers 127 * only. For quantified formulas that require multi-triggers, we build a set of 128 * partial triggers that don't contain all variables, call this set S. Then, 129 * multi-triggers are built by taking a random subset of S that collectively 130 * contains all variables. 131 * 132 * Consider the quantified formula : 133 * forall xyz. P( h( x ), y ) V Q( y, z ) 134 * 135 * For TRIGGER_SEL_ALL and TRIGGER_SEL_MIN_SINGLE_ALL, 136 * S = { h( x ), P( h( x ), y ), Q( y, z ) }. 137 * For TRIGGER_SEL_MIN_SINGLE_MAX, 138 * S = { P( h( x ), y ), Q( y, z ) }. 139 * 140 * Furthermore, TRIGGER_SEL_MIN_SINGLE_ALL and TRIGGER_SEL_MIN_SINGLE_MAX, when 141 * selecting single triggers, only select terms of minimal size. 142 */ 143 enum TriggerSelMode { 144 /** only consider minimal terms for triggers */ 145 TRIGGER_SEL_MIN, 146 /** only consider maximal terms for triggers */ 147 TRIGGER_SEL_MAX, 148 /** consider minimal terms for single triggers, maximal for non-single */ 149 TRIGGER_SEL_MIN_SINGLE_MAX, 150 /** consider minimal terms for single triggers, all for non-single */ 151 TRIGGER_SEL_MIN_SINGLE_ALL, 152 /** consider all terms for triggers */ 153 TRIGGER_SEL_ALL, 154 }; 155 156 enum TriggerActiveSelMode { 157 /** always use all triggers */ 158 TRIGGER_ACTIVE_SEL_ALL, 159 /** only use triggers with minimal # of ground terms */ 160 TRIGGER_ACTIVE_SEL_MIN, 161 /** only use triggers with maximal # of ground terms */ 162 TRIGGER_ACTIVE_SEL_MAX, 163 }; 164 165 enum CVC4_PUBLIC PrenexQuantMode { 166 /** do not prenex */ 167 PRENEX_QUANT_NONE, 168 /** prenex same sign quantifiers */ 169 PRENEX_QUANT_SIMPLE, 170 /** aggressive prenex, disjunctive prenex normal form */ 171 PRENEX_QUANT_DISJ_NORMAL, 172 /** prenex normal form */ 173 PRENEX_QUANT_NORMAL, 174 }; 175 176 enum TermDbMode { 177 /** consider all terms in master equality engine */ 178 TERM_DB_ALL, 179 /** consider only relevant terms */ 180 TERM_DB_RELEVANT, 181 }; 182 183 enum IteLiftQuantMode { 184 /** do not lift ITEs in quantified formulas */ 185 ITE_LIFT_QUANT_MODE_NONE, 186 /** only lift ITEs in quantified formulas if reduces the term size */ 187 ITE_LIFT_QUANT_MODE_SIMPLE, 188 /** lift ITEs */ 189 ITE_LIFT_QUANT_MODE_ALL, 190 }; 191 192 enum CbqiBvIneqMode 193 { 194 /** solve for inequalities using slack values in model */ 195 CBQI_BV_INEQ_EQ_SLACK, 196 /** solve for inequalities using boundary points */ 197 CBQI_BV_INEQ_EQ_BOUNDARY, 198 /** solve for inequalities directly, using side conditions */ 199 CBQI_BV_INEQ_KEEP, 200 }; 201 202 enum CegqiSingleInvMode { 203 /** do not use single invocation techniques */ 204 CEGQI_SI_MODE_NONE, 205 /** use single invocation techniques */ 206 CEGQI_SI_MODE_USE, 207 /** always use single invocation techniques */ 208 CEGQI_SI_MODE_ALL, 209 }; 210 211 /** Solution reconstruction modes for single invocation conjectures 212 * 213 * These modes indicate the policy when CVC4 solves a synthesis conjecture using 214 * single invocation techniques for a sygus problem with a user-specified 215 * grammar. 216 */ 217 enum CegqiSingleInvRconsMode 218 { 219 /** 220 * Do not try to reconstruct solutions to single invocation conjectures. With 221 * this mode, solutions produced by CVC4 may violate grammar restrictions. 222 */ 223 CEGQI_SI_RCONS_MODE_NONE, 224 /** 225 * Try to reconstruct solution to single invocation conjectures in an 226 * incomplete (fail fast) way. 227 */ 228 CEGQI_SI_RCONS_MODE_TRY, 229 /** 230 * Reconstruct solutions to single invocation conjectures, but fail if we 231 * reach an upper limit on number of iterations in the enumeration 232 */ 233 CEGQI_SI_RCONS_MODE_ALL_LIMIT, 234 /** 235 * Reconstruct solutions to single invocation conjectures. This method 236 * relies on an expensive enumeration technique which only terminates when 237 * we succesfully reconstruct the solution, although it may not terminate. 238 */ 239 CEGQI_SI_RCONS_MODE_ALL, 240 }; 241 242 enum CegisSampleMode 243 { 244 /** do not use samples for CEGIS */ 245 CEGIS_SAMPLE_NONE, 246 /** use samples for CEGIS */ 247 CEGIS_SAMPLE_USE, 248 /** trust samples for CEGQI */ 249 CEGIS_SAMPLE_TRUST, 250 }; 251 252 enum SygusInvTemplMode { 253 /** synthesize I( x ) */ 254 SYGUS_INV_TEMPL_MODE_NONE, 255 /** synthesize ( pre( x ) V I( x ) ) */ 256 SYGUS_INV_TEMPL_MODE_PRE, 257 /** synthesize ( post( x ) ^ I( x ) ) */ 258 SYGUS_INV_TEMPL_MODE_POST, 259 }; 260 261 enum SygusActiveGenMode 262 { 263 /** do not use actively-generated enumerators */ 264 SYGUS_ACTIVE_GEN_NONE, 265 /** use basic enumeration for actively-generated enumerators */ 266 SYGUS_ACTIVE_GEN_ENUM_BASIC, 267 /** use optimized enumeration actively-generated enumerators */ 268 SYGUS_ACTIVE_GEN_ENUM, 269 /** use variable-agnostic enumerators */ 270 SYGUS_ACTIVE_GEN_VAR_AGNOSTIC, 271 /** internally decide the best policy for each enumerator */ 272 SYGUS_ACTIVE_GEN_AUTO, 273 }; 274 275 enum SygusFilterSolMode 276 { 277 /** do not filter solutions */ 278 SYGUS_FILTER_SOL_NONE, 279 /** filter logically stronger solutions */ 280 SYGUS_FILTER_SOL_STRONG, 281 /** filter logically weaker solutions */ 282 SYGUS_FILTER_SOL_WEAK, 283 }; 284 285 enum MacrosQuantMode { 286 /** infer all definitions */ 287 MACROS_QUANT_MODE_ALL, 288 /** infer ground definitions */ 289 MACROS_QUANT_MODE_GROUND, 290 /** infer ground uf definitions */ 291 MACROS_QUANT_MODE_GROUND_UF, 292 }; 293 294 enum QuantDSplitMode { 295 /** never do quantifiers splitting */ 296 QUANT_DSPLIT_MODE_NONE, 297 /** default */ 298 QUANT_DSPLIT_MODE_DEFAULT, 299 /** do quantifiers splitting aggressively */ 300 QUANT_DSPLIT_MODE_AGG, 301 }; 302 303 enum QuantRepMode { 304 /** let equality engine choose representatives */ 305 QUANT_REP_MODE_EE, 306 /** default, choose representatives that appear first */ 307 QUANT_REP_MODE_FIRST, 308 /** choose representatives that have minimal depth */ 309 QUANT_REP_MODE_DEPTH, 310 }; 311 312 }/* CVC4::theory::quantifiers namespace */ 313 }/* CVC4::theory namespace */ 314 315 std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mode) CVC4_PUBLIC; 316 317 }/* CVC4 namespace */ 318 319 #endif /* __CVC4__BASE__QUANTIFIERS_MODES_H */ 320