/*! \file quantifiers_engine.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Morgan Deters, Tim King
+ ** Andrew Reynolds, Morgan Deters, Haniel Barbosa
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS_ENGINE_H
-#define __CVC4__THEORY__QUANTIFIERS_ENGINE_H
+#ifndef CVC4__THEORY__QUANTIFIERS_ENGINE_H
+#define CVC4__THEORY__QUANTIFIERS_ENGINE_H
-#include <ext/hash_set>
-#include <iostream>
#include <map>
+#include <unordered_map>
-#include "context/cdchunk_list.h"
#include "context/cdhashset.h"
+#include "context/cdlist.h"
#include "expr/attribute.h"
-#include "options/quantifiers_modes.h"
-#include "theory/quantifiers/inst_match.h"
+#include "expr/term_canonize.h"
+#include "theory/quantifiers/ematching/trigger_trie.h"
+#include "theory/quantifiers/equality_query.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/fmf/model_builder.h"
+#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quant_util.h"
-#include "theory/theory.h"
-#include "util/hash.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/skolemize.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_enumeration.h"
+#include "theory/quantifiers/term_util.h"
#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
-class QuantifiersEngine;
+class DecisionManager;
namespace quantifiers {
- class TermDb;
- class TermDbSygus;
+class QuantifiersModules;
}
-class InstantiationNotify {
-public:
- InstantiationNotify(){}
- virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) = 0;
- virtual void filterInstantiations() = 0;
-};
-
-namespace quantifiers {
- class FirstOrderModel;
- //modules
- class InstantiationEngine;
- class ModelEngine;
- class BoundedIntegers;
- class QuantConflictFind;
- class RewriteEngine;
- class RelevantDomain;
- class QModelBuilder;
- class ConjectureGenerator;
- class CegInstantiation;
- class LtePartialInst;
- class AlphaEquivalence;
- class FunDefEngine;
- class QuantEqualityEngine;
- class FullSaturation;
- class InstStrategyCbqi;
- class InstStrategyCegqi;
- class QuantDSplit;
- class QuantAntiSkolem;
- class EqualityInference;
- class InstPropagator;
-}/* CVC4::theory::quantifiers */
-
-namespace inst {
- class TriggerTrie;
-}/* CVC4::theory::inst */
-
-//class EfficientEMatcher;
-class EqualityQueryQuantifiersEngine;
-
+// TODO: organize this more/review this, github issue #1163
class QuantifiersEngine {
- friend class quantifiers::InstantiationEngine;
- friend class quantifiers::InstStrategyCbqi;
- friend class quantifiers::InstStrategyCegqi;
- friend class quantifiers::ModelEngine;
- friend class quantifiers::RewriteEngine;
- friend class quantifiers::QuantConflictFind;
- friend class inst::InstMatch;
+ friend class ::CVC4::TheoryEngine;
typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
- typedef context::CDChunkList<Node> NodeList;
- typedef context::CDChunkList<bool> BoolList;
+ typedef context::CDList<Node> NodeList;
+ typedef context::CDList<bool> BoolList;
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
-private:
- /** reference to theory engine object */
- TheoryEngine* d_te;
- /** vector of utilities for quantifiers */
- std::vector< QuantifiersUtil* > d_util;
- /** vector of modules for quantifiers */
- std::vector< QuantifiersModule* > d_modules;
- /** instantiation notify */
- std::vector< InstantiationNotify* > d_inst_notify;
- /** equality query class */
- EqualityQueryQuantifiersEngine* d_eq_query;
- /** for computing relevance of quantifiers */
- QuantRelevance * d_quant_rel;
- /** relevant domain */
- quantifiers::RelevantDomain* d_rel_dom;
- /** alpha equivalence */
- quantifiers::AlphaEquivalence * d_alpha_equiv;
- /** model builder */
- quantifiers::QModelBuilder* d_builder;
- /** utility for effectively propositional logic */
- QuantEPR * d_qepr;
-private:
- /** instantiation engine */
- quantifiers::InstantiationEngine* d_inst_engine;
- /** model engine */
- quantifiers::ModelEngine* d_model_engine;
- /** bounded integers utility */
- quantifiers::BoundedIntegers * d_bint;
- /** Conflict find mechanism for quantifiers */
- quantifiers::QuantConflictFind* d_qcf;
- /** rewrite rules utility */
- quantifiers::RewriteEngine * d_rr_engine;
- /** subgoal generator */
- quantifiers::ConjectureGenerator * d_sg_gen;
- /** ceg instantiation */
- quantifiers::CegInstantiation * d_ceg_inst;
- /** lte partial instantiation */
- quantifiers::LtePartialInst * d_lte_part_inst;
- /** function definitions engine */
- quantifiers::FunDefEngine * d_fun_def_engine;
- /** quantifiers equality engine */
- quantifiers::QuantEqualityEngine * d_uee;
- /** full saturation */
- quantifiers::FullSaturation * d_fs;
- /** counterexample-based quantifier instantiation */
- quantifiers::InstStrategyCbqi * d_i_cbqi;
- /** quantifiers splitting */
- quantifiers::QuantDSplit * d_qsplit;
- /** quantifiers anti-skolemization */
- quantifiers::QuantAntiSkolem * d_anti_skolem;
- /** quantifiers instantiation propagtor */
- quantifiers::InstPropagator * d_inst_prop;
-private:
- /** whether we are tracking instantiation lemmas */
- bool d_trackInstLemmas;
-public: //effort levels
- enum {
- QEFFORT_CONFLICT,
- QEFFORT_STANDARD,
- QEFFORT_MODEL,
- QEFFORT_LAST_CALL,
- //none
- QEFFORT_NONE,
- };
-private: //this information is reset during check
- /** current effort level */
- unsigned d_curr_effort_level;
- /** are we in conflict */
- bool d_conflict;
- context::CDO< bool > d_conflict_c;
- /** has added lemma this round */
- bool d_hasAddedLemma;
-private:
- /** list of all quantifiers seen */
- std::map< Node, bool > d_quants;
- /** quantifiers reduced */
- BoolMap d_quants_red;
- std::map< Node, Node > d_quants_red_lem;
- /** list of all lemmas produced */
- //std::map< Node, bool > d_lemmas_produced;
- BoolMap d_lemmas_produced_c;
- /** lemmas waiting */
- std::vector< Node > d_lemmas_waiting;
- /** phase requirements waiting */
- std::map< Node, bool > d_phase_req_waiting;
- /** list of all instantiations produced for each quantifier */
- std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
- std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie;
- /** recorded instantiations */
- std::vector< std::pair< Node, std::vector< Node > > > d_recorded_inst;
- /** quantifiers that have been skolemized */
- BoolMap d_skolemized;
- /** term database */
- quantifiers::TermDb* d_term_db;
- /** all triggers will be stored in this trie */
- inst::TriggerTrie* d_tr_trie;
- /** extended model object */
- quantifiers::FirstOrderModel* d_model;
- /** statistics for debugging */
- std::map< Node, int > d_total_inst_debug;
- std::map< Node, int > d_temp_inst_debug;
- int d_total_inst_count_debug;
- /** inst round counters TODO: make context-dependent? */
- context::CDO< int > d_ierCounter_c;
- int d_ierCounter;
- int d_ierCounter_lc;
- int d_ierCounterLastLc;
- int d_inst_when_phase;
- /** has presolve been called */
- context::CDO< bool > d_presolve;
- /** presolve cache */
- NodeSet d_presolve_in;
- NodeList d_presolve_cache;
- BoolList d_presolve_cache_wq;
- BoolList d_presolve_cache_wic;
-public:
- QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te);
+ public:
+ QuantifiersEngine(quantifiers::QuantifiersState& qstate,
+ quantifiers::QuantifiersInferenceManager& qim,
+ ProofNodeManager* pnm);
~QuantifiersEngine();
+ //---------------------- external interface
/** get theory engine */
- TheoryEngine* getTheoryEngine() { return d_te; }
- /** get equality query */
- EqualityQueryQuantifiersEngine* getEqualityQuery();
- /** get default sat context for quantifiers engine */
- context::Context* getSatContext();
- /** get default sat context for quantifiers engine */
- context::UserContext* getUserContext();
+ TheoryEngine* getTheoryEngine() const;
+ /** Get the decision manager */
+ DecisionManager* getDecisionManager();
/** get default output channel for the quantifiers engine */
OutputChannel& getOutputChannel();
/** get default valuation for the quantifiers engine */
Valuation& getValuation();
- /** get relevant domain */
- quantifiers::RelevantDomain* getRelevantDomain() { return d_rel_dom; }
- /** get quantifier relevance */
- QuantRelevance* getQuantifierRelevance() { return d_quant_rel; }
+ /** get the logic info for the quantifiers engine */
+ const LogicInfo& getLogicInfo() const;
+ //---------------------- end external interface
+ //---------------------- utilities
+ /** get the master equality engine */
+ eq::EqualityEngine* getMasterEqualityEngine() const;
+ /** get equality query */
+ EqualityQuery* getEqualityQuery() const;
/** get the model builder */
- quantifiers::QModelBuilder* getModelBuilder() { return d_builder; }
- /** get utility for EPR */
- QuantEPR* getQuantEPR() { return d_qepr; }
-public: //modules
- /** get instantiation engine */
- quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
- /** get model engine */
- quantifiers::ModelEngine* getModelEngine() { return d_model_engine; }
- /** get bounded integers utility */
- quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; }
- /** Conflict find mechanism for quantifiers */
- quantifiers::QuantConflictFind* getConflictFind() { return d_qcf; }
- /** rewrite rules utility */
- quantifiers::RewriteEngine * getRewriteEngine() { return d_rr_engine; }
- /** subgoal generator */
- quantifiers::ConjectureGenerator * getConjectureGenerator() { return d_sg_gen; }
- /** ceg instantiation */
- quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; }
- /** local theory ext partial inst */
- quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; }
- /** function definition engine */
- quantifiers::FunDefEngine * getFunDefEngine() { return d_fun_def_engine; }
- /** quantifiers equality engine */
- quantifiers::QuantEqualityEngine * getQuantEqualityEngine() { return d_uee; }
- /** get full saturation */
- quantifiers::FullSaturation * getFullSaturation() { return d_fs; }
- /** get inst strategy cbqi */
- quantifiers::InstStrategyCbqi * getInstStrategyCbqi() { return d_i_cbqi; }
- /** get quantifiers splitting */
- quantifiers::QuantDSplit * getQuantDSplit() { return d_qsplit; }
- /** get quantifiers anti-skolemization */
- quantifiers::QuantAntiSkolem * getQuantAntiSkolem() { return d_anti_skolem; }
-private:
- /** owner of quantified formulas */
+ quantifiers::QModelBuilder* getModelBuilder() const;
+ /** get model */
+ quantifiers::FirstOrderModel* getModel() const;
+ /** get term database */
+ quantifiers::TermDb* getTermDatabase() const;
+ /** get term database sygus */
+ quantifiers::TermDbSygus* getTermDatabaseSygus() const;
+ /** get term utilities */
+ quantifiers::TermUtil* getTermUtil() const;
+ /** get term canonizer */
+ expr::TermCanonize* getTermCanonize() const;
+ /** get quantifiers attributes */
+ quantifiers::QuantAttributes* getQuantAttributes() const;
+ /** get instantiate utility */
+ quantifiers::Instantiate* getInstantiate() const;
+ /** get skolemize utility */
+ quantifiers::Skolemize* getSkolemize() const;
+ /** get term enumeration utility */
+ quantifiers::TermEnumeration* getTermEnumeration() const;
+ /** get trigger database */
+ inst::TriggerTrie* getTriggerDatabase() const;
+ //---------------------- end utilities
+ private:
+ //---------------------- private initialization
+ /**
+ * Finish initialize, which passes pointers to the objects that quantifiers
+ * engine needs but were not available when it was created. This is
+ * called after theories have been created but before they have finished
+ * initialization.
+ *
+ * @param te The theory engine
+ * @param dm The decision manager of the theory engine
+ * @param mee The master equality engine of the theory engine
+ */
+ void finishInit(TheoryEngine* te,
+ DecisionManager* dm,
+ eq::EqualityEngine* mee);
+ //---------------------- end private initialization
+ /**
+ * Maps quantified formulas to the module that owns them, if any module has
+ * specifically taken ownership of it.
+ */
std::map< Node, QuantifiersModule * > d_owner;
+ /**
+ * The priority value associated with the ownership of quantified formulas
+ * in the domain of the above map, where higher values take higher
+ * precendence.
+ */
std::map< Node, int > d_owner_priority;
-public:
+ public:
/** get owner */
QuantifiersModule * getOwner( Node q );
- /** set owner */
+ /**
+ * Set owner of quantified formula q to module m with given priority. If
+ * the quantified formula has previously been assigned an owner with
+ * lower priority, that owner is overwritten.
+ */
void setOwner( Node q, QuantifiersModule * m, int priority = 0 );
+ /** set owner of quantified formula q based on its attributes qa. */
+ void setOwner(Node q, quantifiers::QAttributes& qa);
/** considers */
bool hasOwnership( Node q, QuantifiersModule * m = NULL );
-public:
- /** initialize */
- void finishInit();
+ /** does variable v of quantified formula q have a finite bound? */
+ bool isFiniteBound(Node q, Node v) const;
+ /** get bound var type
+ *
+ * This returns the type of bound that was inferred for variable v of
+ * quantified formula q.
+ */
+ BoundVarType getBoundVarType(Node q, Node v) const;
+ /**
+ * Get the indices of bound variables, in the order they should be processed
+ * in a RepSetIterator.
+ *
+ * For details, see BoundedIntegers::getBoundVarIndices.
+ */
+ void getBoundVarIndices(Node q, std::vector<unsigned>& indices) const;
+ /**
+ * Get bound elements
+ *
+ * This gets the (finite) enumeration of the range of variable v of quantified
+ * formula q and adds it into the vector elements in the context of the
+ * iteration being performed by rsi. It returns true if it could successfully
+ * determine this range.
+ *
+ * For details, see BoundedIntegers::getBoundElements.
+ */
+ bool getBoundElements(RepSetIterator* rsi,
+ bool initial,
+ Node q,
+ Node v,
+ std::vector<Node>& elements) const;
+
+ public:
/** presolve */
void presolve();
/** notify preprocessed assertion */
- void ppNotifyAssertions( std::vector< Node >& assertions );
+ void ppNotifyAssertions(const std::vector<Node>& assertions);
/** check at level */
void check( Theory::Effort e );
/** notify that theories were combined */
void notifyCombineTheories();
- /** register quantifier */
- bool registerQuantifier( Node f );
+ /** preRegister quantifier
+ *
+ * This function is called after registerQuantifier for quantified formulas
+ * that are pre-registered to the quantifiers theory.
+ */
+ void preRegisterQuantifier(Node q);
/** register quantifier */
void registerPattern( std::vector<Node> & pattern);
/** assert universal quantifier */
void assertQuantifier( Node q, bool pol );
- /** propagate */
- void propagate( Theory::Effort level );
- /** get next decision request */
- Node getNextDecisionRequest( unsigned& priority );
private:
- /** reduceQuantifier, return true if reduced */
- bool reduceQuantifier( Node q );
- /** compute term vector */
- void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
- /** record instantiation, return true if it was non-duplicate */
- bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool addedLem = true );
- /** remove instantiation */
- bool removeInstantiationInternal( Node q, std::vector< Node >& terms );
- /** set instantiation level attr */
- static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level );
+ /** (context-indepentent) register quantifier internal
+ *
+ * This is called when a quantified formula q is pre-registered to the
+ * quantifiers theory, and updates the modules in this class with
+ * context-independent information about how to handle q. This includes basic
+ * information such as which module owns q.
+ */
+ void registerQuantifierInternal(Node q);
+ /** reduceQuantifier, return true if reduced */
+ bool reduceQuantifier(Node q);
+ /** flush lemmas */
+ void flushLemmas();
+
public:
- /** flush lemmas */
- void flushLemmas();
- /** get instantiation */
- Node getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false );
- /** get instantiation */
- Node getInstantiation( Node q, InstMatch& m, bool doVts = false );
- /** get instantiation */
- Node getInstantiation( Node q, std::vector< Node >& terms, bool doVts = false );
- /** do substitution */
- Node getSubstitute( Node n, std::vector< Node >& terms );
- /** add lemma lem */
- bool addLemma( Node lem, bool doCache = true, bool doRewrite = true );
- /** remove pending lemma */
- bool removeLemma( Node lem );
- /** add require phase */
- void addRequirePhase( Node lit, bool req );
- /** do instantiation specified by m */
- bool addInstantiation( Node q, InstMatch& m, bool mkRep = false, bool modEq = false, bool doVts = false );
- /** add instantiation */
- bool addInstantiation( Node q, std::vector< Node >& terms, bool mkRep = false, bool modEq = false, bool doVts = false );
- /** remove pending instantiation */
- bool removeInstantiation( Node q, Node lem, std::vector< Node >& terms );
- /** split on node n */
- bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true );
- /** add split equality */
- bool addSplitEquality( Node n1, Node n2, bool reqPhase = false, bool reqPhasePol = true );
- /** add EPR axiom */
- bool addEPRAxiom( TypeNode tn );
- /** mark relevant quantified formula, this will indicate it should be checked before the others */
- void markRelevant( Node q );
- /** has added lemma */
- bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
- /** is in conflict */
- bool inConflict() { return d_conflict; }
- /** get number of waiting lemmas */
- unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
- /** get needs check */
- bool getInstWhenNeedsCheck( Theory::Effort e );
- /** get user pat mode */
- quantifiers::UserPatMode getInstUserPatMode();
- /** set instantiation level attr */
- static void setInstantiationLevelAttr( Node n, uint64_t level );
+ /**
+ * Add lemma to the lemma buffer of this quantifiers engine.
+ * @param lem The lemma to send
+ * @param doCache Whether to cache the lemma (to check for duplicate lemmas)
+ * @param doRewrite Whether to rewrite the lemma
+ * @return true if the lemma was successfully added to the buffer
+ */
+ bool addLemma(Node lem, bool doCache = true, bool doRewrite = true);
+ /**
+ * Add trusted lemma lem, same as above, but where a proof generator may be
+ * provided along with the lemma.
+ */
+ bool addTrustedLemma(TrustNode tlem,
+ bool doCache = true,
+ bool doRewrite = true);
+ /** remove pending lemma */
+ bool removeLemma(Node lem);
+ /** add require phase */
+ void addRequirePhase(Node lit, bool req);
+ /** mark relevant quantified formula, this will indicate it should be checked
+ * before the others */
+ void markRelevant(Node q);
+ /** has added lemma */
+ bool hasAddedLemma() const;
+ /** theory engine needs check
+ *
+ * This is true if the theory engine has more constraints to process. When
+ * it is false, we are tentatively going to terminate solving with
+ * sat/unknown. For details, see TheoryEngine::needCheck.
+ */
+ bool theoryEngineNeedsCheck() const;
+ /** is in conflict */
+ bool inConflict() { return d_conflict; }
+ /** set conflict */
+ void setConflict();
+ /** get current q effort */
+ QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; }
+ /** get number of waiting lemmas */
+ unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
+ /** get needs check */
+ bool getInstWhenNeedsCheck(Theory::Effort e);
+ /** get user pat mode */
+ options::UserPatMode getInstUserPatMode();
+
public:
- /** get model */
- quantifiers::FirstOrderModel* getModel() { return d_model; }
- /** get term database */
- quantifiers::TermDb* getTermDatabase() { return d_term_db; }
- /** get term database sygus */
- quantifiers::TermDbSygus* getTermDatabaseSygus();
- /** get trigger database */
- inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
- /** add term to database */
- void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
- /** notification when master equality engine is updated */
- void eqNotifyNewClass(TNode t);
- void eqNotifyPreMerge(TNode t1, TNode t2);
- void eqNotifyPostMerge(TNode t1, TNode t2);
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
- /** get the master equality engine */
- eq::EqualityEngine* getMasterEqualityEngine() ;
- /** debug print equality engine */
- void debugPrintEqualityEngine( const char * c );
+ /** add term to database */
+ void addTermToDatabase(Node n,
+ bool withinQuant = false,
+ bool withinInstClosure = false);
+ /** notification when master equality engine is updated */
+ void eqNotifyNewClass(TNode t);
+ /** debug print equality engine */
+ void debugPrintEqualityEngine(const char* c);
+ /** get internal representative
+ *
+ * Choose a term that is equivalent to a in the current context that is the
+ * best term for instantiating the index^th variable of quantified formula q.
+ * If no legal term can be found, we return null. This can occur if:
+ * - a's type is not a subtype of the type of the index^th variable of q,
+ * - a is in an equivalent class with all terms that are restricted not to
+ * appear in instantiations of q, e.g. INST_CONSTANT terms for counterexample
+ * guided instantiation.
+ */
+ Node getInternalRepresentative(Node a, Node q, int index);
+
public:
- /** print instantiations */
- void printInstantiations( std::ostream& out );
- /** print solution for synthesis conjectures */
- void printSynthSolution( std::ostream& out );
- /** get list of quantified formulas that were instantiated */
- void getInstantiatedQuantifiedFormulas( std::vector< Node >& qs );
- /** get instantiations */
- void getInstantiations( Node q, std::vector< Node >& insts );
- void getInstantiations( std::map< Node, std::vector< Node > >& insts );
- /** get instantiation term vectors */
- void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs );
- void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts );
- /** get instantiated conjunction */
- Node getInstantiatedConjunction( Node q );
- /** get unsat core lemmas */
- bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas );
- bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp );
- /** get inst for lemmas */
- void getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec );
- /** statistics class */
- class Statistics {
+ //----------user interface for instantiations (see quantifiers/instantiate.h)
+ /** print instantiations */
+ void printInstantiations(std::ostream& out);
+ /** print solution for synthesis conjectures */
+ void printSynthSolution(std::ostream& out);
+ /** get list of quantified formulas that were instantiated */
+ void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
+ /** get instantiation term vectors */
+ void getInstantiationTermVectors(Node q,
+ std::vector<std::vector<Node> >& tvecs);
+ void getInstantiationTermVectors(
+ std::map<Node, std::vector<std::vector<Node> > >& insts);
+
+ /** get synth solutions
+ *
+ * This method returns true if there is a synthesis solution available. This
+ * is the case if the last call to check satisfiability originated in a
+ * check-synth call, and the synthesis engine module of this class
+ * successfully found a solution for all active synthesis conjectures.
+ *
+ * This method adds entries to sol_map that map functions-to-synthesize with
+ * their solutions, for all active conjectures. This should be called
+ * immediately after the solver answers unsat for sygus input.
+ *
+ * For details on what is added to sol_map, see
+ * SynthConjecture::getSynthSolutions.
+ */
+ bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map);
+
+ //----------end user interface for instantiations
+
+ /** statistics class */
+ class Statistics
+ {
public:
TimerStat d_time;
TimerStat d_qcf_time;
IntStat d_num_quant;
IntStat d_instantiation_rounds;
IntStat d_instantiation_rounds_lc;
- IntStat d_instantiations;
- IntStat d_inst_duplicate;
- IntStat d_inst_duplicate_eq;
- IntStat d_inst_duplicate_ent;
IntStat d_triggers;
IntStat d_simple_triggers;
IntStat d_multi_triggers;
~Statistics();
};/* class QuantifiersEngine::Statistics */
Statistics d_statistics;
-};/* class QuantifiersEngine */
-
-
-
-/** equality query object using theory engine */
-class EqualityQueryQuantifiersEngine : public EqualityQuery
-{
-private:
- /** pointer to theory engine */
- QuantifiersEngine* d_qe;
- /** quantifiers equality inference */
- quantifiers::EqualityInference * d_eq_inference;
- context::CDO< unsigned > d_eqi_counter;
- /** internal representatives */
- std::map< TypeNode, std::map< Node, Node > > d_int_rep;
- /** rep score */
- std::map< Node, int > d_rep_score;
- /** reset count */
- int d_reset_count;
- /** processInferences : will merge equivalence classes in master equality engine, if possible */
- bool processInferences( Theory::Effort e );
- /** node contains */
- Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache );
- /** get score */
- int getRepScore( Node n, Node f, int index, TypeNode v_tn );
- /** flatten representatives */
- void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
-public:
- EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe );
- virtual ~EqualityQueryQuantifiersEngine();
- /** reset */
- bool reset( Theory::Effort e );
- /** identify */
- std::string identify() const { return "EqualityQueryQE"; }
- /** general queries about equality */
- bool hasTerm( Node a );
- Node getRepresentative( Node a );
- bool areEqual( Node a, Node b );
- bool areDisequal( Node a, Node b );
- eq::EqualityEngine* getEngine();
- void getEquivalenceClass( Node a, std::vector< Node >& eqc );
- TNode getCongruentTerm( Node f, std::vector< TNode >& args );
- /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.
- If cbqi is active, this will return a term in the equivalence class of "a" that does
- not contain instantiation constants, if such a term exists.
+ private:
+ /** The quantifiers state object */
+ quantifiers::QuantifiersState& d_qstate;
+ /** The quantifiers inference manager */
+ quantifiers::QuantifiersInferenceManager& d_qim;
+ /** Pointer to theory engine object */
+ TheoryEngine* d_te;
+ /** Reference to the decision manager of the theory engine */
+ DecisionManager* d_decManager;
+ /** Pointer to the master equality engine */
+ eq::EqualityEngine* d_masterEqualityEngine;
+ /** vector of utilities for quantifiers */
+ std::vector<QuantifiersUtil*> d_util;
+ /** vector of modules for quantifiers */
+ std::vector<QuantifiersModule*> d_modules;
+ //------------- quantifiers utilities
+ /** equality query class */
+ std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query;
+ /** all triggers will be stored in this trie */
+ std::unique_ptr<inst::TriggerTrie> d_tr_trie;
+ /** extended model object */
+ std::unique_ptr<quantifiers::FirstOrderModel> d_model;
+ /** model builder */
+ std::unique_ptr<quantifiers::QModelBuilder> d_builder;
+ /** term utilities */
+ std::unique_ptr<quantifiers::TermUtil> d_term_util;
+ /** term utilities */
+ std::unique_ptr<expr::TermCanonize> d_term_canon;
+ /** term database */
+ std::unique_ptr<quantifiers::TermDb> d_term_db;
+ /** sygus term database */
+ std::unique_ptr<quantifiers::TermDbSygus> d_sygus_tdb;
+ /** quantifiers attributes */
+ std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr;
+ /** instantiate utility */
+ std::unique_ptr<quantifiers::Instantiate> d_instantiate;
+ /** skolemize utility */
+ std::unique_ptr<quantifiers::Skolemize> d_skolemize;
+ /** term enumeration utility */
+ std::unique_ptr<quantifiers::TermEnumeration> d_term_enum;
+ //------------- end quantifiers utilities
+ /**
+ * The modules utility, which contains all of the quantifiers modules.
*/
- Node getInternalRepresentative( Node a, Node f, int index );
- /** get quantifiers equality inference */
- quantifiers::EqualityInference * getEqualityInference() { return d_eq_inference; }
-}; /* EqualityQueryQuantifiersEngine */
+ std::unique_ptr<quantifiers::QuantifiersModules> d_qmodules;
+ //------------- temporary information during check
+ /** current effort level */
+ QuantifiersModule::QEffort d_curr_effort_level;
+ /** are we in conflict */
+ bool d_conflict;
+ context::CDO<bool> d_conflict_c;
+ /** has added lemma this round */
+ bool d_hasAddedLemma;
+ //------------- end temporary information during check
+ private:
+ /** list of all quantifiers seen */
+ std::map<Node, bool> d_quants;
+ /** quantifiers pre-registered */
+ NodeSet d_quants_prereg;
+ /** quantifiers reduced */
+ BoolMap d_quants_red;
+ std::map<Node, Node> d_quants_red_lem;
+ /** list of all lemmas produced */
+ // std::map< Node, bool > d_lemmas_produced;
+ BoolMap d_lemmas_produced_c;
+ /** lemmas waiting */
+ std::vector<Node> d_lemmas_waiting;
+ /** map from waiting lemmas to their proof generators */
+ std::map<Node, ProofGenerator*> d_lemmasWaitingPg;
+ /** phase requirements waiting */
+ std::map<Node, bool> d_phase_req_waiting;
+ /** inst round counters TODO: make context-dependent? */
+ context::CDO<int> d_ierCounter_c;
+ int d_ierCounter;
+ int d_ierCounter_lc;
+ int d_ierCounterLastLc;
+ int d_inst_when_phase;
+ /** has presolve been called */
+ context::CDO<bool> d_presolve;
+ /** presolve cache */
+ NodeSet d_presolve_in;
+ NodeList d_presolve_cache;
+ BoolList d_presolve_cache_wq;
+ BoolList d_presolve_cache_wic;
+};/* class QuantifiersEngine */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS_ENGINE_H */
+#endif /* CVC4__THEORY__QUANTIFIERS_ENGINE_H */
projects / cvc5.git / blobdiff