src/theory/quantifiers_engine.h

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