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-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 */
  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 */
 217   bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
 218   /** is in conflict */
 219   bool inConflict() { return d_conflict; }
 220   /** set conflict */
 221   void setConflict();
 222   /** get current q effort */
 223   QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; }
 224   /** get number of waiting lemmas */
 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 */
 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 */