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