/********************* */ /*! \file ext_theory.h ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Mathias Preiner ** This file is part of the CVC4 project. ** 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 ** ** \brief Extended theory interface. ** ** This implements a generic module, used by theory solvers, for performing ** "context-dependent simplification", as described in Reynolds et al ** "Designing Theory Solvers with Extensions", FroCoS 2017. ** ** At a high level, this technique implements a generic inference scheme based ** on the combination of SAT-context-dependent equality reasoning and ** SAT-context-indepedent rewriting. ** ** As a simple example, say ** (1) TheoryStrings tells us that the following facts hold in the SAT context: ** x = "A" ^ str.contains( str.++( x, z ), "B" ) = true. ** (2) The Rewriter tells us that: ** str.contains( str.++( "A", z ), "B" ) ----> str.contains( z, "B" ). ** From this, this class may infer that the following lemma is T-valid: ** x = "A" ^ str.contains( str.++( x, z ), "B" ) => str.contains( z, "B" ) **/ #include "cvc4_private.h" #ifndef CVC4__THEORY__EXT_THEORY_H #define CVC4__THEORY__EXT_THEORY_H #include #include #include "context/cdhashset.h" #include "context/context.h" #include "expr/node.h" #include "theory/theory.h" namespace CVC4 { namespace theory { /** Extended theory class * * This class is used for constructing generic extensions to theory solvers. * In particular, it provides methods for "context-dependent simplification" * and "model-based refinement". For details, see Reynolds et al "Design * Theory Solvers with Extensions", FroCoS 2017. * * It maintains: * (1) A set of "extended function" kinds (d_extf_kind), * (2) A database of active/inactive extended function terms (d_ext_func_terms) * that have been registered to the class. * * This class has methods doInferences/doReductions, which send out lemmas * based on the current set of active extended function terms. The former * is based on context-dependent simplification, where this class asks the * underlying theory for a "derivable substitution", whereby extended functions * may be reducable. */ class ExtTheory { typedef context::CDHashMap NodeBoolMap; typedef context::CDHashSet NodeSet; public: /** constructor * * If cacheEnabled is false, we do not cache results of getSubstitutedTerm. */ ExtTheory(Theory* p, bool cacheEnabled = false); virtual ~ExtTheory() {} /** Tells this class to treat terms with Kind k as extended functions */ void addFunctionKind(Kind k) { d_extf_kind[k] = true; } /** Is kind k treated as an extended function by this class? */ bool hasFunctionKind(Kind k) const { return d_extf_kind.find(k) != d_extf_kind.end(); } /** register term * * Registers term n with this class. Adds n to the set of extended function * terms known by this class (d_ext_func_terms) if n is an extended function, * that is, if addFunctionKind( n.getKind() ) was called. */ void registerTerm(Node n); /** register all subterms of n with this class */ void registerTermRec(Node n); /** set n as reduced/inactive * * If contextDepend = false, then n remains inactive in the duration of this * user-context level */ void markReduced(Node n, bool contextDepend = true); /** * Mark that a and b are congruent terms. This sets b inactive, and sets a to * inactive if b was inactive. */ void markCongruent(Node a, Node b); /** getSubstitutedTerms * * input : effort, terms * output : sterms, exp, where ( exp[i] => terms[i] = sterms[i] ) for all i. * * For each i, sterms[i] = term[i] * sigma for some "derivable substitution" * sigma. We obtain derivable substitutions and their explanations via calls * to the underlying theory's Theory::getCurrentSubstitution method. This * also * * If useCache is true, we cache the result in d_gst_cache. This is a context * independent cache that can be cleared using clearCache() below. */ void getSubstitutedTerms(int effort, const std::vector& terms, std::vector& sterms, std::vector >& exp, bool useCache = false); /** * Same as above, but for a single term. We return the substituted form of * term and add its explanation to exp. */ Node getSubstitutedTerm(int effort, Node term, std::vector& exp, bool useCache = false); /** clear the cache for getSubstitutedTerm */ void clearCache(); /** doInferences * * This function performs "context-dependent simplification". The method takes * as input: * effort: an identifier used to determine which terms we reduce and the * form of the derivable substitution we will use, * terms: the set of terms to simplify, * batch: if this flag is true, we send lemmas for all terms; if it is false * we send a lemma for the first applicable term. * * Sends rewriting lemmas of the form ( exp => t = c ) where t is in terms * and c is a constant, c = rewrite( t*sigma ) where exp |= sigma. These * lemmas are determined by asking the underlying theory for a derivable * substitution (through getCurrentSubstitution with getSubstitutedTerm) * above, applying this substitution to terms in terms, rewriting * the result and checking with the theory whether the resulting term is * in reduced form (isExtfReduced). * * This method adds the extended terms that are still active to nred, and * returns true if and only if a lemma of the above form was sent. */ bool doInferences(int effort, const std::vector& terms, std::vector& nred, bool batch = true); /** * Calls the above function, where terms is getActive(), the set of currently * active terms. */ bool doInferences(int effort, std::vector& nred, bool batch = true); /** doReductions * * This method has the same interface as doInferences. In contrast to * doInfereces, this method will send reduction lemmas of the form ( t = t' ) * where t is in terms and t' is an equivalent reduced term. */ bool doReductions(int effort, const std::vector& terms, std::vector& nred, bool batch = true); bool doReductions(int effort, std::vector& nred, bool batch = true); /** get the set of all extended function terms from d_ext_func_terms */ void getTerms(std::vector& terms); /** is there at least one active extended function term? */ bool hasActiveTerm() const; /** is n an active extended function term? */ bool isActive(Node n) const; /** get the set of active terms from d_ext_func_terms */ std::vector getActive() const; /** get the set of active terms from d_ext_func_terms of kind k */ std::vector getActive(Kind k) const; private: /** returns the set of variable subterms of n */ static std::vector collectVars(Node n); /** is n context dependent inactive? */ bool isContextIndependentInactive(Node n) const; /** do inferences internal */ bool doInferencesInternal(int effort, const std::vector& terms, std::vector& nred, bool batch, bool isRed); /** send lemma on the output channel of d_parent */ bool sendLemma(Node lem, bool preprocess = false); /** reference to the underlying theory */ Theory* d_parent; /** the true node */ Node d_true; /** extended function terms, map to whether they are active */ NodeBoolMap d_ext_func_terms; /** * The set of terms from d_ext_func_terms that are SAT-context-independent * inactive. For instance, a term t is SAT-context-independent inactive if * a reduction lemma of the form t = t' was added in this user-context level. */ NodeSet d_ci_inactive; /** * Watched term for checking if any non-reduced extended functions exist. * This is an arbitrary active member of d_ext_func_terms. */ context::CDO d_has_extf; /** the set of kinds we are treated as extended functions */ std::map d_extf_kind; /** information for each term in d_ext_func_terms */ class ExtfInfo { public: /** all variables in this term */ std::vector d_vars; }; std::map d_extf_info; // cache of all lemmas sent NodeSet d_lemmas; NodeSet d_pp_lemmas; /** whether we enable caching for getSubstitutedTerm */ bool d_cacheEnabled; /** Substituted term info */ class SubsTermInfo { public: /** the substituted term */ Node d_sterm; /** an explanation */ std::vector d_exp; }; /** * This maps an (effort, term) to the information above. It is used as a * cache for getSubstitutedTerm when d_cacheEnabled is true. */ std::map > d_gst_cache; }; } /* CVC4::theory namespace */ } /* CVC4 namespace */ #endif /* CVC4__THEORY__EXT_THEORY_H */