/****************************************************************************** * Top contributors (to current version): * Andrew Reynolds, Mathias Preiner, Morgan Deters * * This file is part of the cvc5 project. * * Copyright (c) 2009-2021 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. * **************************************************************************** * * instantiate */ #include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INSTANTIATE_H #define CVC5__THEORY__QUANTIFIERS__INSTANTIATE_H #include #include "context/cdhashset.h" #include "expr/node.h" #include "proof/proof.h" #include "theory/inference_id.h" #include "theory/quantifiers/inst_match_trie.h" #include "theory/quantifiers/quant_util.h" #include "util/statistics_stats.h" namespace cvc5 { class LazyCDProof; namespace theory { namespace quantifiers { class TermRegistry; class QuantifiersState; class QuantifiersInferenceManager; class QuantifiersRegistry; class FirstOrderModel; /** Instantiation rewriter * * This class is used for cases where instantiation lemmas can be rewritten by * external utilities. Examples of this include virtual term substitution and * nested quantifier elimination techniques. */ class InstantiationRewriter { public: InstantiationRewriter() {} virtual ~InstantiationRewriter() {} /** rewrite instantiation * * The node inst is the instantiation of quantified formula q for terms. * This method returns the rewritten form of the instantiation. * * The flag doVts is whether we must apply virtual term substitution to the * instantiation. * * Returns a TrustNode of kind REWRITE, corresponding to the rewrite of inst * and its proof generator. */ virtual TrustNode rewriteInstantiation(Node q, std::vector& terms, Node inst, bool doVts) = 0; }; /** Context-dependent list of nodes */ class InstLemmaList { public: InstLemmaList(context::Context* c) : d_list(c) {} /** The list */ context::CDList d_list; }; /** Instantiate * * This class is used for generating instantiation lemmas. It maintains an * instantiation trie, which is represented by a different data structure * depending on whether incremental solving is enabled (see d_inst_match_trie * and d_c_inst_match_trie). * * Below, we say an instantiation lemma for q = forall x. F under substitution * { x -> t } is the formula: * ( ~forall x. F V F * { x -> t } ) * where * is application of substitution. * * Its main interface is ::addInstantiation(...), which is called by many of * the quantifiers modules, which enqueues instantiation lemmas in quantifiers * engine via calls to QuantifiersInferenceManager::addPendingLemma. * * It also has utilities for constructing instantiations, and interfaces for * getting the results of the instantiations produced during check-sat calls. */ class Instantiate : public QuantifiersUtil { using NodeInstListMap = context::CDHashMap>; public: Instantiate(Env& env, QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, ProofNodeManager* pnm = nullptr); ~Instantiate(); /** reset */ bool reset(Theory::Effort e) override; /** register quantifier */ void registerQuantifier(Node q) override; /** identify */ std::string identify() const override { return "Instantiate"; } /** check incomplete */ bool checkComplete(IncompleteId& incId) override; //--------------------------------------rewrite objects /** add instantiation rewriter */ void addRewriter(InstantiationRewriter* ir); /** notify flush lemmas * * This is called just before the quantifiers engine flushes its lemmas to * the output channel. */ void notifyFlushLemmas(); //--------------------------------------end rewrite objects /** do instantiation specified by m * * This function returns true if the instantiation lemma for quantified * formula q for the substitution specified by terms is successfully enqueued * via a call to QuantifiersInferenceManager::addPendingLemma. * @param q the quantified formula to instantiate * @param terms the terms to instantiate with * @param id the identifier of the instantiation lemma sent via the inference * manager * @param pfArg an additional node to add to the arguments of the INSTANTIATE * step * @param mkRep whether to take the representatives of the terms in the * range of the substitution m, * @param doVts whether we must apply virtual term substitution to the * instantiation lemma. * * This call may fail if it can be determined that the instantiation is not * relevant or legal in the current context. This happens if: * (1) The substitution is not well-typed, * (2) The substitution involves terms whose instantiation level is above the * allowed limit, * (3) The resulting instantiation is entailed in the current context using a * fast entailment check (see TermDb::isEntailed), * (4) The range of the substitution is a duplicate of that of a previously * added instantiation, * (5) The instantiation lemma is a duplicate of previously added lemma. * */ bool addInstantiation(Node q, std::vector& terms, InferenceId id, Node pfArg = Node::null(), bool mkRep = false, bool doVts = false); /** * Same as above, but we also compute a vector failMask indicating which * values in terms led to the instantiation not being added when this method * returns false. For example, if q is the formula * forall xy. x>5 => P(x,y) * If terms = { 4, 0 }, then this method will return false since * 4>5 => P(4,0) * is entailed true based on rewriting. This method may additionally set * failMask to "10", indicating that x's value was critical, but y's value * was not. In other words, all instantiations including { x -> 4 } will also * lead to this method returning false. * * The bits of failMask are computed in a greedy fashion, in reverse order. * That is, we check whether each variable is critical one at a time, starting * from the end. * * The parameter expFull is whether try to set all bits of the fail mask to * 0. If this argument is true, then we only try to set a suffix of the * bits in failMask to false. The motivation for expFull=false is for callers * of this method that are enumerating tuples in lexiocographic order. The * number of false bits in the suffix of failMask tells the caller how many * "decimal" places to increment their iterator. */ bool addInstantiationExpFail(Node q, std::vector& terms, std::vector& failMask, InferenceId id, Node pfArg = Node::null(), bool mkRep = false, bool doVts = false, bool expFull = true); /** record instantiation * * Explicitly record that q has been instantiated with terms, with virtual * term substitution if doVts is true. This is the same as addInstantiation, * but does not enqueue an instantiation lemma. */ void recordInstantiation(Node q, std::vector& terms, bool doVts = false); /** exists instantiation * * Returns true if and only if the instantiation already was added or * recorded by this class. * modEq : whether to check for duplication modulo equality */ bool existsInstantiation(Node q, std::vector& terms, bool modEq = false); //--------------------------------------general utilities /** get instantiation * * Returns the instantiation lemma for q under substitution { vars -> terms }. * doVts is whether to apply virtual term substitution to its body. * * If provided, pf is a lazy proof for which we store a proof of the * returned formula with free assumption q. This typically stores a * single INSTANTIATE step concluding the instantiated body of q from q. */ Node getInstantiation(Node q, std::vector& vars, std::vector& terms, InferenceId id = InferenceId::UNKNOWN, Node pfArg = Node::null(), bool doVts = false, LazyCDProof* pf = nullptr); /** get instantiation * * Same as above but with vars equal to the bound variables of q. */ Node getInstantiation(Node q, std::vector& terms, bool doVts = false); //--------------------------------------end general utilities /** * Called once at the end of each instantiation round. This prints * instantiations added this round to trace inst-per-quant-round, if * applicable, and prints to out if the option debug-inst is enabled. */ void notifyEndRound(); /** debug print model, called once, before we terminate with sat/unknown. */ void debugPrintModel(); //--------------------------------------user-level interface utilities /** get instantiated quantified formulas * * Get the list of quantified formulas that were instantiated in the current * user context, store them in qs. */ void getInstantiatedQuantifiedFormulas(std::vector& qs) const; /** get instantiation term vectors * * Get term vectors corresponding to for all instantiations lemmas added in * the current user context for quantified formula q, store them in tvecs. */ void getInstantiationTermVectors(Node q, std::vector >& tvecs); /** get instantiation term vectors * * Get term vectors for all instantiations lemmas added in the current user * context for quantified formula q, store them in tvecs. */ void getInstantiationTermVectors( std::map > >& insts); /** * Get instantiations for quantified formula q. If q is (forall ((x T)) (P * x)), this is a list of the form (P t1) ... (P tn) for ground terms ti. */ void getInstantiations(Node q, std::vector& insts); //--------------------------------------end user-level interface utilities /** Are proofs enabled for this object? */ bool isProofEnabled() const; /** statistics class * * This tracks statistics on the number of instantiations successfully * enqueued on the quantifiers output channel, and the number of redundant * instantiations encountered by various criteria. */ class Statistics { public: IntStat d_instantiations; IntStat d_inst_duplicate; IntStat d_inst_duplicate_eq; IntStat d_inst_duplicate_ent; Statistics(); }; /* class Instantiate::Statistics */ Statistics d_statistics; private: /** record instantiation, return true if it was not a duplicate */ bool recordInstantiationInternal(Node q, std::vector& terms); /** remove instantiation from the cache */ bool removeInstantiationInternal(Node q, std::vector& terms); /** * Ensure that n has type tn, return a term equivalent to it for that type * if possible. */ static Node ensureType(Node n, TypeNode tn); /** Get or make the instantiation list for quantified formula q */ InstLemmaList* getOrMkInstLemmaList(TNode q); /** Reference to the quantifiers state */ QuantifiersState& d_qstate; /** Reference to the quantifiers inference manager */ QuantifiersInferenceManager& d_qim; /** The quantifiers registry */ QuantifiersRegistry& d_qreg; /** Reference to the term registry */ TermRegistry& d_treg; /** pointer to the proof node manager */ ProofNodeManager* d_pnm; /** instantiation rewriter classes */ std::vector d_instRewrite; /** * The list of all instantiation lemma bodies per quantifier. This is used * for debugging and for quantifier elimination. */ NodeInstListMap d_insts; /** explicitly recorded instantiations * * Sometimes an instantiation is recorded internally but not sent out as a * lemma, for instance, for partial quantifier elimination. This is a map * of these instantiations, for each quantified formula. This map is cleared * on presolve, e.g. it is local to a check-sat call. */ std::map > d_recordedInst; /** statistics for debugging total instantiations per quantifier per round */ std::map d_instDebugTemp; /** list of all instantiations produced for each quantifier * * We store context (dependent, independent) versions. If incremental solving * is disabled, we use d_inst_match_trie for performance reasons. */ std::map d_inst_match_trie; std::map d_c_inst_match_trie; /** * The list of quantified formulas for which the domain of d_c_inst_match_trie * is valid. */ context::CDHashSet d_c_inst_match_trie_dom; /** * A CDProof storing instantiation steps. */ std::unique_ptr d_pfInst; }; } // namespace quantifiers } // namespace theory } // namespace cvc5 #endif /* CVC5__THEORY__QUANTIFIERS__INSTANTIATE_H */