src/theory/quantifiers_engine.h

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