** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Haniel Barbosa
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 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 "context/cdlist.h"
#include "expr/attribute.h"
#include "expr/term_canonize.h"
-#include "theory/quantifiers/ematching/trigger.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_epr.h"
#include "theory/quantifiers/quant_util.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"
namespace theory {
-class QuantifiersEnginePrivate;
+class DecisionManager;
+
+namespace quantifiers {
+class QuantifiersModules;
+}
// TODO: organize this more/review this, github issue #1163
class QuantifiersEngine {
+ friend class ::CVC4::TheoryEngine;
typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
typedef context::CDList<Node> NodeList;
typedef context::CDList<bool> BoolList;
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
-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() const { return d_te; }
- /** 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 */
//---------------------- utilities
/** get the master equality engine */
eq::EqualityEngine* getMasterEqualityEngine() const;
- /** get the active equality engine */
- eq::EqualityEngine* getActiveEqualityEngine() const;
/** get equality query */
EqualityQuery* getEqualityQuery() const;
/** get the model builder */
quantifiers::QModelBuilder* getModelBuilder() const;
- /** get utility for EPR */
- quantifiers::QuantEPR* getQuantEPR() const;
/** get model */
quantifiers::FirstOrderModel* getModel() const;
/** get term 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.
* precendence.
*/
std::map< Node, int > d_owner_priority;
-public:
+ public:
/** get owner */
QuantifiersModule * getOwner( Node q );
/**
void flushLemmas();
public:
- /** 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 );
- /** 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; }
- /** 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 */
- quantifiers::UserPatMode getInstUserPatMode();
+ /**
+ * 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:
- /** 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);
- /** use model equality engine */
- bool usingModelEqualityEngine() const { return d_useModelEe; }
- /** debug print equality engine */
- void debugPrintEqualityEngine( const char * c );
- /** get internal representative */
- Node getInternalRepresentative( Node a, Node q, int index );
+ /** 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:
- //----------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 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 explanation for instantiation lemmas */
- void getExplanationForInstLemmas(const std::vector<Node>& lems,
- std::map<Node, Node>& quant,
- std::map<Node, std::vector<Node> >& tvec);
+public:
+ //----------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);
+ /** 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
+ //----------end user interface for instantiations
- /** statistics class */
- class Statistics {
+ /** statistics class */
+ class Statistics
+ {
public:
TimerStat d_time;
TimerStat d_qcf_time;
~Statistics();
};/* class QuantifiersEngine::Statistics */
Statistics d_statistics;
-
+
private:
- /** reference to theory engine object */
+ /** 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::unique_ptr<quantifiers::FirstOrderModel> d_model;
/** model builder */
std::unique_ptr<quantifiers::QModelBuilder> d_builder;
- /** utility for effectively propositional logic */
- std::unique_ptr<quantifiers::QuantEPR> d_qepr;
/** term utilities */
std::unique_ptr<quantifiers::TermUtil> d_term_util;
/** term utilities */
std::unique_ptr<quantifiers::TermEnumeration> d_term_enum;
//------------- end quantifiers utilities
/**
- * The private utility, which contains all of the quantifiers modules.
+ * The modules utility, which contains all of the quantifiers modules.
*/
- std::unique_ptr<QuantifiersEnginePrivate> d_private;
+ std::unique_ptr<quantifiers::QuantifiersModules> d_qmodules;
//------------- temporary information during check
/** current effort level */
QuantifiersModule::QEffort d_curr_effort_level;
context::CDO<bool> d_conflict_c;
/** has added lemma this round */
bool d_hasAddedLemma;
- /** whether to use model equality engine */
- bool d_useModelEe;
//------------- end temporary information during check
private:
/** list of all quantifiers seen */
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? */
projects / cvc5.git / blobdiff