1 /********************* */ 2 /*! \file quantifiers_engine.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Andrew Reynolds, Morgan Deters, Haniel Barbosa 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 Theory instantiator, Instantiation Engine classes 13 **/ 14 15 #include "cvc4_private.h" 16 17 #ifndef __CVC4__THEORY__QUANTIFIERS_ENGINE_H 18 #define __CVC4__THEORY__QUANTIFIERS_ENGINE_H 19 20 #include <iostream> 21 #include <map> 22 #include <memory> 23 #include <unordered_map> 24 25 #include "context/cdhashset.h" 26 #include "context/cdlist.h" 27 #include "expr/attribute.h" 28 #include "options/quantifiers_modes.h" 29 #include "theory/quantifiers/inst_match.h" 30 #include "theory/quantifiers/quant_util.h" 31 #include "theory/theory.h" 32 #include "util/hash.h" 33 #include "util/statistics_registry.h" 34 35 namespace CVC4 { 36 37 class TheoryEngine; 38 39 namespace theory { 40 41 class QuantifiersEngine; 42 43 namespace quantifiers { 44 //TODO: organize this more/review this, github issue #1163 45 //TODO: include these instead of doing forward declarations? #1307 46 //utilities 47 class TermDb; 48 class TermDbSygus; 49 class TermUtil; 50 class TermCanonize; 51 class Instantiate; 52 class Skolemize; 53 class TermEnumeration; 54 class FirstOrderModel; 55 class QuantAttributes; 56 class QuantEPR; 57 class QuantRelevance; 58 class RelevantDomain; 59 class BvInverter; 60 class InstPropagator; 61 class EqualityInference; 62 class EqualityQueryQuantifiersEngine; 63 //modules, these are "subsolvers" of the quantifiers theory. 64 class InstantiationEngine; 65 class ModelEngine; 66 class BoundedIntegers; 67 class QuantConflictFind; 68 class RewriteEngine; 69 class QModelBuilder; 70 class ConjectureGenerator; 71 class SynthEngine; 72 class LtePartialInst; 73 class AlphaEquivalence; 74 class InstStrategyEnum; 75 class InstStrategyCegqi; 76 class QuantDSplit; 77 class QuantAntiSkolem; 78 class EqualityInference; 79 }/* CVC4::theory::quantifiers */ 80 81 namespace inst { 82 class TriggerTrie; 83 }/* CVC4::theory::inst */ 84 85 86 class QuantifiersEngine { 87 typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; 88 typedef context::CDList<Node> NodeList; 89 typedef context::CDList<bool> BoolList; 90 typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; 91 92 public: 93 QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te); 94 ~QuantifiersEngine(); 95 //---------------------- external interface 96 /** get theory engine */ getTheoryEngine()97 TheoryEngine* getTheoryEngine() const { return d_te; } 98 /** get default sat context for quantifiers engine */ 99 context::Context* getSatContext(); 100 /** get default sat context for quantifiers engine */ 101 context::UserContext* getUserContext(); 102 /** get default output channel for the quantifiers engine */ 103 OutputChannel& getOutputChannel(); 104 /** get default valuation for the quantifiers engine */ 105 Valuation& getValuation(); 106 /** get the logic info for the quantifiers engine */ 107 const LogicInfo& getLogicInfo() const; 108 //---------------------- end external interface 109 //---------------------- utilities 110 /** get equality query */ 111 EqualityQuery* getEqualityQuery() const; 112 /** get the equality inference */ 113 quantifiers::EqualityInference* getEqualityInference() const; 114 /** get relevant domain */ 115 quantifiers::RelevantDomain* getRelevantDomain() const; 116 /** get the BV inverter utility */ 117 quantifiers::BvInverter* getBvInverter() const; 118 /** get quantifier relevance */ 119 quantifiers::QuantRelevance* getQuantifierRelevance() const; 120 /** get the model builder */ 121 quantifiers::QModelBuilder* getModelBuilder() const; 122 /** get utility for EPR */ 123 quantifiers::QuantEPR* getQuantEPR() const; 124 /** get model */ 125 quantifiers::FirstOrderModel* getModel() const; 126 /** get term database */ 127 quantifiers::TermDb* getTermDatabase() const; 128 /** get term database sygus */ 129 quantifiers::TermDbSygus* getTermDatabaseSygus() const; 130 /** get term utilities */ 131 quantifiers::TermUtil* getTermUtil() const; 132 /** get term canonizer */ 133 quantifiers::TermCanonize* getTermCanonize() const; 134 /** get quantifiers attributes */ 135 quantifiers::QuantAttributes* getQuantAttributes() const; 136 /** get instantiate utility */ 137 quantifiers::Instantiate* getInstantiate() const; 138 /** get skolemize utility */ 139 quantifiers::Skolemize* getSkolemize() const; 140 /** get term enumeration utility */ 141 quantifiers::TermEnumeration* getTermEnumeration() const; 142 /** get trigger database */ 143 inst::TriggerTrie* getTriggerDatabase() const; 144 //---------------------- end utilities 145 //---------------------- modules 146 /** get bounded integers utility */ 147 quantifiers::BoundedIntegers* getBoundedIntegers() const; 148 /** Conflict find mechanism for quantifiers */ 149 quantifiers::QuantConflictFind* getConflictFind() const; 150 /** rewrite rules utility */ 151 quantifiers::RewriteEngine* getRewriteEngine() const; 152 /** ceg instantiation */ 153 quantifiers::SynthEngine* getSynthEngine() const; 154 /** get full saturation */ 155 quantifiers::InstStrategyEnum* getInstStrategyEnum() const; 156 /** get inst strategy cbqi */ 157 quantifiers::InstStrategyCegqi* getInstStrategyCegqi() const; 158 //---------------------- end modules 159 private: 160 /** owner of quantified formulas */ 161 std::map< Node, QuantifiersModule * > d_owner; 162 std::map< Node, int > d_owner_priority; 163 public: 164 /** get owner */ 165 QuantifiersModule * getOwner( Node q ); 166 /** set owner */ 167 void setOwner( Node q, QuantifiersModule * m, int priority = 0 ); 168 /** considers */ 169 bool hasOwnership( Node q, QuantifiersModule * m = NULL ); 170 /** is finite bound */ 171 bool isFiniteBound( Node q, Node v ); 172 public: 173 /** presolve */ 174 void presolve(); 175 /** notify preprocessed assertion */ 176 void ppNotifyAssertions(const std::vector<Node>& assertions); 177 /** check at level */ 178 void check( Theory::Effort e ); 179 /** notify that theories were combined */ 180 void notifyCombineTheories(); 181 /** preRegister quantifier 182 * 183 * This function is called after registerQuantifier for quantified formulas 184 * that are pre-registered to the quantifiers theory. 185 */ 186 void preRegisterQuantifier(Node q); 187 /** register quantifier */ 188 void registerPattern( std::vector<Node> & pattern); 189 /** assert universal quantifier */ 190 void assertQuantifier( Node q, bool pol ); 191 private: 192 /** (context-indepentent) register quantifier internal 193 * 194 * This is called when a quantified formula q is pre-registered to the 195 * quantifiers theory, and updates the modules in this class with 196 * context-independent information about how to handle q. This includes basic 197 * information such as which module owns q. 198 */ 199 void registerQuantifierInternal(Node q); 200 /** reduceQuantifier, return true if reduced */ 201 bool reduceQuantifier(Node q); 202 /** flush lemmas */ 203 void flushLemmas(); 204 205 public: 206 /** add lemma lem */ 207 bool addLemma( Node lem, bool doCache = true, bool doRewrite = true ); 208 /** remove pending lemma */ 209 bool removeLemma( Node lem ); 210 /** add require phase */ 211 void addRequirePhase( Node lit, bool req ); 212 /** add EPR axiom */ 213 bool addEPRAxiom( TypeNode tn ); 214 /** mark relevant quantified formula, this will indicate it should be checked before the others */ 215 void markRelevant( Node q ); 216 /** has added lemma */ hasAddedLemma()217 bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; } 218 /** is in conflict */ inConflict()219 bool inConflict() { return d_conflict; } 220 /** set conflict */ 221 void setConflict(); 222 /** get current q effort */ getCurrentQEffort()223 QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; } 224 /** get number of waiting lemmas */ getNumLemmasWaiting()225 unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); } 226 /** get needs check */ 227 bool getInstWhenNeedsCheck( Theory::Effort e ); 228 /** get user pat mode */ 229 quantifiers::UserPatMode getInstUserPatMode(); 230 public: 231 /** add term to database */ 232 void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false ); 233 /** notification when master equality engine is updated */ 234 void eqNotifyNewClass(TNode t); 235 void eqNotifyPreMerge(TNode t1, TNode t2); 236 void eqNotifyPostMerge(TNode t1, TNode t2); 237 void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); 238 /** get the master equality engine */ 239 eq::EqualityEngine* getMasterEqualityEngine(); 240 /** get the active equality engine */ 241 eq::EqualityEngine* getActiveEqualityEngine(); 242 /** use model equality engine */ usingModelEqualityEngine()243 bool usingModelEqualityEngine() const { return d_useModelEe; } 244 /** debug print equality engine */ 245 void debugPrintEqualityEngine( const char * c ); 246 /** get internal representative */ 247 Node getInternalRepresentative( Node a, Node q, int index ); 248 249 public: 250 //----------user interface for instantiations (see quantifiers/instantiate.h) 251 /** print instantiations */ 252 void printInstantiations(std::ostream& out); 253 /** print solution for synthesis conjectures */ 254 void printSynthSolution(std::ostream& out); 255 /** get list of quantified formulas that were instantiated */ 256 void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs); 257 /** get instantiations */ 258 void getInstantiations(Node q, std::vector<Node>& insts); 259 void getInstantiations(std::map<Node, std::vector<Node> >& insts); 260 /** get instantiation term vectors */ 261 void getInstantiationTermVectors(Node q, 262 std::vector<std::vector<Node> >& tvecs); 263 void getInstantiationTermVectors( 264 std::map<Node, std::vector<std::vector<Node> > >& insts); 265 /** get instantiated conjunction */ 266 Node getInstantiatedConjunction(Node q); 267 /** get unsat core lemmas */ 268 bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas); 269 bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas, 270 std::map<Node, Node>& weak_imp); 271 /** get explanation for instantiation lemmas */ 272 void getExplanationForInstLemmas(const std::vector<Node>& lems, 273 std::map<Node, Node>& quant, 274 std::map<Node, std::vector<Node> >& tvec); 275 276 /** get synth solutions 277 * 278 * This function adds entries to sol_map that map functions-to-synthesize with 279 * their solutions, for all active conjectures. This should be called 280 * immediately after the solver answers unsat for sygus input. 281 * 282 * For details on what is added to sol_map, see 283 * CegConjecture::getSynthSolutions. 284 */ 285 void getSynthSolutions(std::map<Node, Node>& sol_map); 286 287 //----------end user interface for instantiations 288 289 /** statistics class */ 290 class Statistics { 291 public: 292 TimerStat d_time; 293 TimerStat d_qcf_time; 294 TimerStat d_ematching_time; 295 IntStat d_num_quant; 296 IntStat d_instantiation_rounds; 297 IntStat d_instantiation_rounds_lc; 298 IntStat d_triggers; 299 IntStat d_simple_triggers; 300 IntStat d_multi_triggers; 301 IntStat d_multi_trigger_instantiations; 302 IntStat d_red_alpha_equiv; 303 IntStat d_instantiations_user_patterns; 304 IntStat d_instantiations_auto_gen; 305 IntStat d_instantiations_guess; 306 IntStat d_instantiations_qcf; 307 IntStat d_instantiations_qcf_prop; 308 IntStat d_instantiations_fmf_exh; 309 IntStat d_instantiations_fmf_mbqi; 310 IntStat d_instantiations_cbqi; 311 IntStat d_instantiations_rr; 312 Statistics(); 313 ~Statistics(); 314 };/* class QuantifiersEngine::Statistics */ 315 Statistics d_statistics; 316 317 private: 318 /** reference to theory engine object */ 319 TheoryEngine* d_te; 320 /** vector of utilities for quantifiers */ 321 std::vector<QuantifiersUtil*> d_util; 322 /** vector of modules for quantifiers */ 323 std::vector<QuantifiersModule*> d_modules; 324 //------------- quantifiers utilities 325 /** equality query class */ 326 std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query; 327 /** equality inference class */ 328 std::unique_ptr<quantifiers::EqualityInference> d_eq_inference; 329 /** quantifiers instantiation propagtor */ 330 std::unique_ptr<quantifiers::InstPropagator> d_inst_prop; 331 /** all triggers will be stored in this trie */ 332 std::unique_ptr<inst::TriggerTrie> d_tr_trie; 333 /** extended model object */ 334 std::unique_ptr<quantifiers::FirstOrderModel> d_model; 335 /** for computing relevance of quantifiers */ 336 std::unique_ptr<quantifiers::QuantRelevance> d_quant_rel; 337 /** relevant domain */ 338 std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom; 339 /** inversion utility for BV instantiation */ 340 std::unique_ptr<quantifiers::BvInverter> d_bv_invert; 341 /** model builder */ 342 std::unique_ptr<quantifiers::QModelBuilder> d_builder; 343 /** utility for effectively propositional logic */ 344 std::unique_ptr<quantifiers::QuantEPR> d_qepr; 345 /** term utilities */ 346 std::unique_ptr<quantifiers::TermUtil> d_term_util; 347 /** term utilities */ 348 std::unique_ptr<quantifiers::TermCanonize> d_term_canon; 349 /** term database */ 350 std::unique_ptr<quantifiers::TermDb> d_term_db; 351 /** sygus term database */ 352 std::unique_ptr<quantifiers::TermDbSygus> d_sygus_tdb; 353 /** quantifiers attributes */ 354 std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr; 355 /** instantiate utility */ 356 std::unique_ptr<quantifiers::Instantiate> d_instantiate; 357 /** skolemize utility */ 358 std::unique_ptr<quantifiers::Skolemize> d_skolemize; 359 /** term enumeration utility */ 360 std::unique_ptr<quantifiers::TermEnumeration> d_term_enum; 361 //------------- end quantifiers utilities 362 //------------- quantifiers modules 363 /** alpha equivalence */ 364 std::unique_ptr<quantifiers::AlphaEquivalence> d_alpha_equiv; 365 /** instantiation engine */ 366 std::unique_ptr<quantifiers::InstantiationEngine> d_inst_engine; 367 /** model engine */ 368 std::unique_ptr<quantifiers::ModelEngine> d_model_engine; 369 /** bounded integers utility */ 370 std::unique_ptr<quantifiers::BoundedIntegers> d_bint; 371 /** Conflict find mechanism for quantifiers */ 372 std::unique_ptr<quantifiers::QuantConflictFind> d_qcf; 373 /** rewrite rules utility */ 374 std::unique_ptr<quantifiers::RewriteEngine> d_rr_engine; 375 /** subgoal generator */ 376 std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen; 377 /** ceg instantiation */ 378 std::unique_ptr<quantifiers::SynthEngine> d_synth_e; 379 /** lte partial instantiation */ 380 std::unique_ptr<quantifiers::LtePartialInst> d_lte_part_inst; 381 /** full saturation */ 382 std::unique_ptr<quantifiers::InstStrategyEnum> d_fs; 383 /** counterexample-based quantifier instantiation */ 384 std::unique_ptr<quantifiers::InstStrategyCegqi> d_i_cbqi; 385 /** quantifiers splitting */ 386 std::unique_ptr<quantifiers::QuantDSplit> d_qsplit; 387 /** quantifiers anti-skolemization */ 388 std::unique_ptr<quantifiers::QuantAntiSkolem> d_anti_skolem; 389 //------------- end quantifiers modules 390 //------------- temporary information during check 391 /** current effort level */ 392 QuantifiersModule::QEffort d_curr_effort_level; 393 /** are we in conflict */ 394 bool d_conflict; 395 context::CDO<bool> d_conflict_c; 396 /** has added lemma this round */ 397 bool d_hasAddedLemma; 398 /** whether to use model equality engine */ 399 bool d_useModelEe; 400 //------------- end temporary information during check 401 private: 402 /** list of all quantifiers seen */ 403 std::map<Node, bool> d_quants; 404 /** quantifiers pre-registered */ 405 NodeSet d_quants_prereg; 406 /** quantifiers reduced */ 407 BoolMap d_quants_red; 408 std::map<Node, Node> d_quants_red_lem; 409 /** list of all lemmas produced */ 410 // std::map< Node, bool > d_lemmas_produced; 411 BoolMap d_lemmas_produced_c; 412 /** lemmas waiting */ 413 std::vector<Node> d_lemmas_waiting; 414 /** phase requirements waiting */ 415 std::map<Node, bool> d_phase_req_waiting; 416 /** inst round counters TODO: make context-dependent? */ 417 context::CDO<int> d_ierCounter_c; 418 int d_ierCounter; 419 int d_ierCounter_lc; 420 int d_ierCounterLastLc; 421 int d_inst_when_phase; 422 /** has presolve been called */ 423 context::CDO<bool> d_presolve; 424 /** presolve cache */ 425 NodeSet d_presolve_in; 426 NodeList d_presolve_cache; 427 BoolList d_presolve_cache_wq; 428 BoolList d_presolve_cache_wic; 429 };/* class QuantifiersEngine */ 430 431 }/* CVC4::theory namespace */ 432 }/* CVC4 namespace */ 433 434 #endif /* __CVC4__THEORY__QUANTIFIERS_ENGINE_H */ 435