From: Andrew Reynolds Date: Fri, 6 Jul 2018 19:58:31 +0000 (+0100) Subject: Split ext theory to own file and document (#1809) X-Git-Tag: cvc5-1.0.0~4905 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=97ab81d20887f58c90365ba622c7c84148ca8033;p=cvc5.git Split ext theory to own file and document (#1809) --- diff --git a/src/Makefile.am b/src/Makefile.am index 917fc6ef3..71a66db59 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -369,6 +369,8 @@ libcvc4_la_SOURCES = \ theory/datatypes/theory_datatypes_type_rules.h \ theory/datatypes/type_enumerator.cpp \ theory/datatypes/type_enumerator.h \ + theory/ext_theory.cpp \ + theory/ext_theory.h \ theory/fp/theory_fp.cpp \ theory/fp/theory_fp.h \ theory/fp/theory_fp_rewriter.cpp \ diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 98c426339..8380014f3 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -25,6 +25,7 @@ #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/theory_arith.h" +#include "theory/ext_theory.h" #include "theory/quantifiers/quant_util.h" #include "theory/theory_model.h" diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 9a36f5eab..d7113b17d 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -21,6 +21,7 @@ #include "smt/smt_statistics_registry.h" #include "theory/arith/infer_bounds.h" #include "theory/arith/theory_arith_private.h" +#include "theory/ext_theory.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 81bf91992..ad0ce2e86 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -43,26 +43,22 @@ #include "theory/arith/approx_simplex.h" #include "theory/arith/arith_ite_utils.h" #include "theory/arith/arith_rewriter.h" -#include "theory/arith/arith_rewriter.h" #include "theory/arith/arith_static_learner.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/arithvar.h" #include "theory/arith/congruence_manager.h" #include "theory/arith/constraint.h" -#include "theory/arith/constraint.h" #include "theory/arith/cut_log.h" #include "theory/arith/delta_rational.h" -#include "theory/arith/delta_rational.h" #include "theory/arith/dio_solver.h" #include "theory/arith/linear_equality.h" #include "theory/arith/matrix.h" -#include "theory/arith/matrix.h" #include "theory/arith/nonlinear_extension.h" #include "theory/arith/normal_form.h" #include "theory/arith/partial_model.h" -#include "theory/arith/partial_model.h" #include "theory/arith/simplex.h" #include "theory/arith/theory_arith.h" +#include "theory/ext_theory.h" #include "theory/ite_utilities.h" #include "theory/quantifiers/fmf/bounded_integers.h" #include "theory/rewriter.h" diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index d648997cb..b3c3f73f3 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -22,6 +22,7 @@ #include "theory/bv/slicer.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" +#include "theory/ext_theory.h" #include "theory/theory_model.h" using namespace std; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 3b434f143..7dc6d3710 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -17,6 +17,8 @@ #include "options/bv_options.h" #include "options/smt_options.h" +#include "proof/proof_manager.h" +#include "proof/theory_proof.h" #include "smt/smt_statistics_registry.h" #include "theory/bv/abstraction.h" #include "theory/bv/bv_eager_solver.h" @@ -29,9 +31,8 @@ #include "theory/bv/theory_bv_rewrite_rules_simplification.h" #include "theory/bv/theory_bv_rewriter.h" #include "theory/bv/theory_bv_utils.h" +#include "theory/ext_theory.h" #include "theory/theory_model.h" -#include "proof/theory_proof.h" -#include "proof/proof_manager.h" #include "theory/valuation.h" using namespace CVC4::context; diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp new file mode 100644 index 000000000..7cc8627eb --- /dev/null +++ b/src/theory/ext_theory.cpp @@ -0,0 +1,544 @@ +/********************* */ +/*! \file ext_theory.cpp + ** \verbatim + ** Top contributors (to current version): + ** Tim King, Andrew Reynolds, Dejan Jovanovic + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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. + **/ + +#include "theory/ext_theory.h" + +#include "base/cvc4_assert.h" +#include "smt/smt_statistics_registry.h" +#include "theory/quantifiers_engine.h" +#include "theory/substitutions.h" + +using namespace std; + +namespace CVC4 { +namespace theory { + +ExtTheory::ExtTheory(Theory* p, bool cacheEnabled) + : d_parent(p), + d_ext_func_terms(p->getSatContext()), + d_ci_inactive(p->getUserContext()), + d_has_extf(p->getSatContext()), + d_lemmas(p->getUserContext()), + d_pp_lemmas(p->getUserContext()), + d_cacheEnabled(cacheEnabled) +{ + d_true = NodeManager::currentNM()->mkConst(true); +} + +// Gets all leaf terms in n. +std::vector ExtTheory::collectVars(Node n) +{ + std::vector vars; + std::set visited; + std::vector worklist; + worklist.push_back(n); + while (!worklist.empty()) + { + Node current = worklist.back(); + worklist.pop_back(); + if (current.isConst() || visited.count(current) > 0) + { + continue; + } + visited.insert(current); + // Treat terms not belonging to this theory as leaf + // note : chould include terms not belonging to this theory + // (commented below) + if (current.getNumChildren() > 0) + { + //&& Theory::theoryOf(n)==d_parent->getId() ){ + worklist.insert(worklist.end(), current.begin(), current.end()); + } + else + { + vars.push_back(current); + } + } + return vars; +} + +Node ExtTheory::getSubstitutedTerm(int effort, + Node term, + std::vector& exp, + bool useCache) +{ + if (useCache) + { + Assert(d_gst_cache[effort].find(term) != d_gst_cache[effort].end()); + exp.insert(exp.end(), + d_gst_cache[effort][term].d_exp.begin(), + d_gst_cache[effort][term].d_exp.end()); + return d_gst_cache[effort][term].d_sterm; + } + + std::vector terms; + terms.push_back(term); + std::vector sterms; + std::vector > exps; + getSubstitutedTerms(effort, terms, sterms, exps, useCache); + Assert(sterms.size() == 1); + Assert(exps.size() == 1); + exp.insert(exp.end(), exps[0].begin(), exps[0].end()); + return sterms[0]; +} + +// do inferences +void ExtTheory::getSubstitutedTerms(int effort, + const std::vector& terms, + std::vector& sterms, + std::vector >& exp, + bool useCache) +{ + if (useCache) + { + for (const Node& n : terms) + { + Assert(d_gst_cache[effort].find(n) != d_gst_cache[effort].end()); + sterms.push_back(d_gst_cache[effort][n].d_sterm); + exp.push_back(std::vector()); + exp[0].insert(exp[0].end(), + d_gst_cache[effort][n].d_exp.begin(), + d_gst_cache[effort][n].d_exp.end()); + } + } + else + { + Trace("extt-debug") << "getSubstitutedTerms for " << terms.size() << " / " + << d_ext_func_terms.size() << " extended functions." + << std::endl; + if (!terms.empty()) + { + // all variables we need to find a substitution for + std::vector vars; + std::vector sub; + std::map > expc; + for (const Node& n : terms) + { + // do substitution, rewrite + std::map::iterator iti = d_extf_info.find(n); + Assert(iti != d_extf_info.end()); + for (const Node& v : iti->second.d_vars) + { + if (std::find(vars.begin(), vars.end(), v) == vars.end()) + { + vars.push_back(v); + } + } + } + bool useSubs = d_parent->getCurrentSubstitution(effort, vars, sub, expc); + // get the current substitution for all variables + Assert(!useSubs || vars.size() == sub.size()); + for (const Node& n : terms) + { + Node ns = n; + std::vector expn; + if (useSubs) + { + // do substitution + ns = n.substitute(vars.begin(), vars.end(), sub.begin(), sub.end()); + if (ns != n) + { + // build explanation: explanation vars = sub for each vars in FV(n) + std::map::iterator iti = d_extf_info.find(n); + Assert(iti != d_extf_info.end()); + for (const Node& v : iti->second.d_vars) + { + std::map >::iterator itx = expc.find(v); + if (itx != expc.end()) + { + for (const Node& e : itx->second) + { + if (std::find(expn.begin(), expn.end(), e) == expn.end()) + { + expn.push_back(e); + } + } + } + } + } + Trace("extt-debug") + << " have " << n << " == " << ns << ", exp size=" << expn.size() + << "." << std::endl; + } + // add to vector + sterms.push_back(ns); + exp.push_back(expn); + // add to cache + if (d_cacheEnabled) + { + d_gst_cache[effort][n].d_sterm = ns; + d_gst_cache[effort][n].d_exp.clear(); + d_gst_cache[effort][n].d_exp.insert( + d_gst_cache[effort][n].d_exp.end(), expn.begin(), expn.end()); + } + } + } + } +} + +bool ExtTheory::doInferencesInternal(int effort, + const std::vector& terms, + std::vector& nred, + bool batch, + bool isRed) +{ + if (batch) + { + bool addedLemma = false; + if (isRed) + { + for (const Node& n : terms) + { + Node nr; + // note: could do reduction with substitution here + int ret = d_parent->getReduction(effort, n, nr); + if (ret == 0) + { + nred.push_back(n); + } + else + { + if (!nr.isNull() && n != nr) + { + Node lem = NodeManager::currentNM()->mkNode(kind::EQUAL, n, nr); + if (sendLemma(lem, true)) + { + Trace("extt-lemma") + << "ExtTheory : reduction lemma : " << lem << std::endl; + addedLemma = true; + } + } + markReduced(n, ret < 0); + } + } + } + else + { + std::vector sterms; + std::vector > exp; + getSubstitutedTerms(effort, terms, sterms, exp); + std::map sterm_index; + for (unsigned i = 0, size = terms.size(); i < size; i++) + { + bool processed = false; + if (sterms[i] != terms[i]) + { + Node sr = Rewriter::rewrite(sterms[i]); + // ask the theory if this term is reduced, e.g. is it constant or it + // is a non-extf term. + if (d_parent->isExtfReduced(effort, sr, terms[i], exp[i])) + { + processed = true; + markReduced(terms[i]); + Node eq = terms[i].eqNode(sr); + Node expn = + exp[i].size() > 1 + ? NodeManager::currentNM()->mkNode(kind::AND, exp[i]) + : (exp[i].size() == 1 ? exp[i][0] : d_true); + Trace("extt-debug") << "ExtTheory::doInferences : infer : " << eq + << " by " << expn << std::endl; + Node lem = + NodeManager::currentNM()->mkNode(kind::IMPLIES, expn, eq); + Trace("extt-debug") << "...send lemma " << lem << std::endl; + if (sendLemma(lem)) + { + Trace("extt-lemma") + << "ExtTheory : substitution + rewrite lemma : " << lem + << std::endl; + addedLemma = true; + } + } + else + { + // check if we have already reduced this + std::map::iterator itsi = sterm_index.find(sr); + if (itsi == sterm_index.end()) + { + sterm_index[sr] = i; + } + else + { + // unsigned j = itsi->second; + // note : can add (non-reducing) lemma : + // exp[j] ^ exp[i] => sterms[i] = sterms[j] + } + + Trace("extt-nred") << "Non-reduced term : " << sr << std::endl; + } + } + else + { + Trace("extt-nred") << "Non-reduced term : " << sterms[i] << std::endl; + } + if (!processed) + { + nred.push_back(terms[i]); + } + } + } + return addedLemma; + } + // non-batch + std::vector nnred; + if (terms.empty()) + { + for (NodeBoolMap::iterator it = d_ext_func_terms.begin(); + it != d_ext_func_terms.end(); + ++it) + { + if ((*it).second && !isContextIndependentInactive((*it).first)) + { + std::vector nterms; + nterms.push_back((*it).first); + if (doInferencesInternal(effort, nterms, nnred, true, isRed)) + { + return true; + } + } + } + } + else + { + for (const Node& n : terms) + { + std::vector nterms; + nterms.push_back(n); + if (doInferencesInternal(effort, nterms, nnred, true, isRed)) + { + return true; + } + } + } + return false; +} + +bool ExtTheory::sendLemma(Node lem, bool preprocess) +{ + if (preprocess) + { + if (d_pp_lemmas.find(lem) == d_pp_lemmas.end()) + { + d_pp_lemmas.insert(lem); + d_parent->getOutputChannel().lemma(lem, false, true); + return true; + } + } + else + { + if (d_lemmas.find(lem) == d_lemmas.end()) + { + d_lemmas.insert(lem); + d_parent->getOutputChannel().lemma(lem); + return true; + } + } + return false; +} + +bool ExtTheory::doInferences(int effort, + const std::vector& terms, + std::vector& nred, + bool batch) +{ + if (!terms.empty()) + { + return doInferencesInternal(effort, terms, nred, batch, false); + } + return false; +} + +bool ExtTheory::doInferences(int effort, std::vector& nred, bool batch) +{ + std::vector terms = getActive(); + return doInferencesInternal(effort, terms, nred, batch, false); +} + +bool ExtTheory::doReductions(int effort, + const std::vector& terms, + std::vector& nred, + bool batch) +{ + if (!terms.empty()) + { + return doInferencesInternal(effort, terms, nred, batch, true); + } + return false; +} + +bool ExtTheory::doReductions(int effort, std::vector& nred, bool batch) +{ + const std::vector terms = getActive(); + return doInferencesInternal(effort, terms, nred, batch, true); +} + +// Register term. +void ExtTheory::registerTerm(Node n) +{ + if (d_extf_kind.find(n.getKind()) != d_extf_kind.end()) + { + if (d_ext_func_terms.find(n) == d_ext_func_terms.end()) + { + Trace("extt-debug") << "Found extended function : " << n << " in " + << d_parent->getId() << std::endl; + d_ext_func_terms[n] = true; + d_has_extf = n; + d_extf_info[n].d_vars = collectVars(n); + } + } +} + +void ExtTheory::registerTermRec(Node n) +{ + std::unordered_set visited; + std::vector visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + registerTerm(cur); + for (const Node& cc : cur) + { + visit.push_back(cc); + } + } + } while (!visit.empty()); +} + +// mark reduced +void ExtTheory::markReduced(Node n, bool contextDepend) +{ + registerTerm(n); + Assert(d_ext_func_terms.find(n) != d_ext_func_terms.end()); + d_ext_func_terms[n] = false; + if (!contextDepend) + { + d_ci_inactive.insert(n); + } + + // update has_extf + if (d_has_extf.get() == n) + { + for (NodeBoolMap::iterator it = d_ext_func_terms.begin(); + it != d_ext_func_terms.end(); + ++it) + { + // if not already reduced + if ((*it).second && !isContextIndependentInactive((*it).first)) + { + d_has_extf = (*it).first; + } + } + } +} + +// mark congruent +void ExtTheory::markCongruent(Node a, Node b) +{ + Trace("extt-debug") << "Mark congruent : " << a << " " << b << std::endl; + registerTerm(a); + registerTerm(b); + NodeBoolMap::const_iterator it = d_ext_func_terms.find(b); + if (it != d_ext_func_terms.end()) + { + if (d_ext_func_terms.find(a) != d_ext_func_terms.end()) + { + d_ext_func_terms[a] = d_ext_func_terms[a] && (*it).second; + } + else + { + Assert(false); + } + d_ext_func_terms[b] = false; + } + else + { + Assert(false); + } +} + +bool ExtTheory::isContextIndependentInactive(Node n) const +{ + return d_ci_inactive.find(n) != d_ci_inactive.end(); +} + +void ExtTheory::getTerms(std::vector& terms) +{ + for (NodeBoolMap::iterator it = d_ext_func_terms.begin(); + it != d_ext_func_terms.end(); + ++it) + { + terms.push_back((*it).first); + } +} + +bool ExtTheory::hasActiveTerm() const { return !d_has_extf.get().isNull(); } + +// is active +bool ExtTheory::isActive(Node n) const +{ + NodeBoolMap::const_iterator it = d_ext_func_terms.find(n); + if (it != d_ext_func_terms.end()) + { + return (*it).second && !isContextIndependentInactive(n); + } + return false; +} + +// get active +std::vector ExtTheory::getActive() const +{ + std::vector active; + for (NodeBoolMap::iterator it = d_ext_func_terms.begin(); + it != d_ext_func_terms.end(); + ++it) + { + // if not already reduced + if ((*it).second && !isContextIndependentInactive((*it).first)) + { + active.push_back((*it).first); + } + } + return active; +} + +std::vector ExtTheory::getActive(Kind k) const +{ + std::vector active; + for (NodeBoolMap::iterator it = d_ext_func_terms.begin(); + it != d_ext_func_terms.end(); + ++it) + { + // if not already reduced + if ((*it).first.getKind() == k && (*it).second + && !isContextIndependentInactive((*it).first)) + { + active.push_back((*it).first); + } + } + return active; +} + +void ExtTheory::clearCache() { d_gst_cache.clear(); } + +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/ext_theory.h b/src/theory/ext_theory.h new file mode 100644 index 000000000..8657d0fb8 --- /dev/null +++ b/src/theory/ext_theory.h @@ -0,0 +1,250 @@ +/********************* */ +/*! \file ext_theory.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 928df298c..cb1f006b3 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -20,15 +20,16 @@ #include "expr/kind.h" #include "options/strings_options.h" +#include "smt/command.h" #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" -#include "smt/command.h" +#include "theory/ext_theory.h" +#include "theory/quantifiers/term_database.h" #include "theory/rewriter.h" #include "theory/strings/theory_strings_rewriter.h" #include "theory/strings/type_enumerator.h" #include "theory/theory_model.h" #include "theory/valuation.h" -#include "theory/quantifiers/term_database.h" using namespace std; using namespace CVC4::context; diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index a08ac2da3..10504b487 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -23,9 +23,9 @@ #include "base/cvc4_assert.h" #include "smt/smt_statistics_registry.h" -#include "theory/substitutions.h" +#include "theory/ext_theory.h" #include "theory/quantifiers_engine.h" - +#include "theory/substitutions.h" using namespace std; @@ -355,391 +355,5 @@ TheoryId EntailmentCheckSideEffects::getTheoryId() const { EntailmentCheckSideEffects::~EntailmentCheckSideEffects() { } - - -ExtTheory::ExtTheory( Theory * p, bool cacheEnabled ) : d_parent( p ), -d_ext_func_terms( p->getSatContext() ), d_ci_inactive( p->getUserContext() ), d_has_extf( p->getSatContext() ), -d_lemmas( p->getUserContext() ), d_pp_lemmas( p->getUserContext() ), d_cacheEnabled( cacheEnabled ){ - d_true = NodeManager::currentNM()->mkConst( true ); -} - -// Gets all leaf terms in n. -std::vector ExtTheory::collectVars(Node n) { - std::vector vars; - std::set visited; - std::vector worklist; - worklist.push_back(n); - while (!worklist.empty()) { - Node current = worklist.back(); - worklist.pop_back(); - if (current.isConst() || visited.count(current) > 0) { - continue; - } - visited.insert(current); - // Treat terms not belonging to this theory as leaf - // AJR TODO : should include terms not belonging to this theory - // (commented below) - if (current.getNumChildren() > 0) { - //&& Theory::theoryOf(n)==d_parent->getId() ){ - worklist.insert(worklist.end(), current.begin(), current.end()); - } else { - vars.push_back(current); - } - } - return vars; -} - -Node ExtTheory::getSubstitutedTerm( int effort, Node term, std::vector< Node >& exp, bool useCache ) { - if( useCache ){ - Assert( d_gst_cache[effort].find( term )!=d_gst_cache[effort].end() ); - exp.insert( exp.end(), d_gst_cache[effort][term].d_exp.begin(), d_gst_cache[effort][term].d_exp.end() ); - return d_gst_cache[effort][term].d_sterm; - }else{ - std::vector< Node > terms; - terms.push_back( term ); - std::vector< Node > sterms; - std::vector< std::vector< Node > > exps; - getSubstitutedTerms( effort, terms, sterms, exps, useCache ); - Assert( sterms.size()==1 ); - Assert( exps.size()==1 ); - exp.insert( exp.end(), exps[0].begin(), exps[0].end() ); - return sterms[0]; - } -} - -//do inferences -void ExtTheory::getSubstitutedTerms(int effort, const std::vector& terms, - std::vector& sterms, - std::vector >& exp, - bool useCache) { - if (useCache) { - for( unsigned i=0; i() ); - exp[0].insert( exp[0].end(), d_gst_cache[effort][n].d_exp.begin(), d_gst_cache[effort][n].d_exp.end() ); - } - }else{ - Trace("extt-debug") << "getSubstitutedTerms for " << terms.size() << " / " << d_ext_func_terms.size() << " extended functions." << std::endl; - if( !terms.empty() ){ - //all variables we need to find a substitution for - std::vector< Node > vars; - std::vector< Node > sub; - std::map< Node, std::vector< Node > > expc; - for( unsigned i=0; i::iterator iti = d_extf_info.find( n ); - Assert( iti!=d_extf_info.end() ); - for( unsigned i=0; isecond.d_vars.size(); i++ ){ - if( std::find( vars.begin(), vars.end(), iti->second.d_vars[i] )==vars.end() ){ - vars.push_back( iti->second.d_vars[i] ); - } - } - } - bool useSubs = d_parent->getCurrentSubstitution( effort, vars, sub, expc ); - //get the current substitution for all variables - Assert( !useSubs || vars.size()==sub.size() ); - for( unsigned i=0; i expn; - if( useSubs ){ - //do substitution - ns = n.substitute( vars.begin(), vars.end(), sub.begin(), sub.end() ); - if( ns!=n ){ - //build explanation: explanation vars = sub for each vars in FV( n ) - std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n ); - Assert( iti!=d_extf_info.end() ); - for( unsigned j=0; jsecond.d_vars.size(); j++ ){ - Node v = iti->second.d_vars[j]; - std::map< Node, std::vector< Node > >::iterator itx = expc.find( v ); - if( itx!=expc.end() ){ - for( unsigned k=0; ksecond.size(); k++ ){ - if( std::find( expn.begin(), expn.end(), itx->second[k] )==expn.end() ){ - expn.push_back( itx->second[k] ); - } - } - } - } - } - Trace("extt-debug") << " have " << n << " == " << ns << ", exp size=" << expn.size() << "." << std::endl; - } - //add to vector - sterms.push_back( ns ); - exp.push_back( expn ); - //add to cache - if( d_cacheEnabled ){ - d_gst_cache[effort][n].d_sterm = ns; - d_gst_cache[effort][n].d_exp.clear(); - d_gst_cache[effort][n].d_exp.insert( d_gst_cache[effort][n].d_exp.end(), expn.begin(), expn.end() ); - } - } - } - } -} - -bool ExtTheory::doInferencesInternal(int effort, const std::vector& terms, - std::vector& nred, bool batch, - bool isRed) { - if (batch) { - bool addedLemma = false; - if( isRed ){ - for( unsigned i=0; igetReduction( effort, n, nr ); - if( ret==0 ){ - nred.push_back( n ); - }else{ - if( !nr.isNull() && n!=nr ){ - Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, n, nr ); - if( sendLemma( lem, true ) ){ - Trace("extt-lemma") << "ExtTheory : reduction lemma : " << lem << std::endl; - addedLemma = true; - } - } - markReduced( terms[i], ret<0 ); - } - } - }else{ - std::vector< Node > sterms; - std::vector< std::vector< Node > > exp; - getSubstitutedTerms( effort, terms, sterms, exp ); - std::map< Node, unsigned > sterm_index; - for( unsigned i=0; iisExtfReduced( effort, sr, terms[i], exp[i] ) ){ - processed = true; - markReduced( terms[i] ); - Node eq = terms[i].eqNode( sr ); - Node expn = exp[i].size()>1 ? NodeManager::currentNM()->mkNode( kind::AND, exp[i] ) : ( exp[i].size()==1 ? exp[i][0] : d_true ); - Trace("extt-debug") << "ExtTheory::doInferences : infer : " << eq << " by " << expn << std::endl; - Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, expn, eq ); - Trace("extt-debug") << "...send lemma " << lem << std::endl; - if( sendLemma( lem ) ){ - Trace("extt-lemma") << "ExtTheory : substitution + rewrite lemma : " << lem << std::endl; - addedLemma = true; - } - }else{ - //check if we have already reduced this - std::map< Node, unsigned >::iterator itsi = sterm_index.find( sr ); - if( itsi!=sterm_index.end() ){ - //unsigned j = itsi->second; - //can add (non-reducing) lemma : exp[j] ^ exp[i] => sterms[i] = sterms[j] - //TODO - }else{ - sterm_index[sr] = i; - } - //check if we reduce to another active term? - - Trace("extt-nred") << "Non-reduced term : " << sr << std::endl; - } - }else{ - Trace("extt-nred") << "Non-reduced term : " << sterms[i] << std::endl; - } - if( !processed ){ - nred.push_back( terms[i] ); - } - } - } - return addedLemma; - }else{ - std::vector< Node > nnred; - if( terms.empty() ){ - for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ - if( (*it).second && !isContextIndependentInactive( (*it).first ) ){ - std::vector< Node > nterms; - nterms.push_back( (*it).first ); - if( doInferencesInternal( effort, nterms, nnred, true, isRed ) ){ - return true; - } - } - } - }else{ - for( unsigned i=0; i nterms; - nterms.push_back( terms[i] ); - if( doInferencesInternal( effort, nterms, nnred, true, isRed ) ){ - return true; - } - } - } - return false; - } -} - -bool ExtTheory::sendLemma( Node lem, bool preprocess ) { - if( preprocess ){ - if( d_pp_lemmas.find( lem )==d_pp_lemmas.end() ){ - d_pp_lemmas.insert( lem ); - d_parent->getOutputChannel().lemma( lem, false, true ); - return true; - } - }else{ - if( d_lemmas.find( lem )==d_lemmas.end() ){ - d_lemmas.insert( lem ); - d_parent->getOutputChannel().lemma( lem ); - return true; - } - } - return false; -} - -bool ExtTheory::doInferences(int effort, const std::vector& terms, - std::vector& nred, bool batch) { - if (!terms.empty()) { - return doInferencesInternal( effort, terms, nred, batch, false ); - }else{ - return false; - } -} - -bool ExtTheory::doInferences( int effort, std::vector< Node >& nred, bool batch ) { - std::vector< Node > terms = getActive(); - return doInferencesInternal( effort, terms, nred, batch, false ); -} - -bool ExtTheory::doReductions(int effort, const std::vector& terms, - std::vector& nred, bool batch) { - if (!terms.empty()) { - return doInferencesInternal( effort, terms, nred, batch, true ); - }else{ - return false; - } -} - -bool ExtTheory::doReductions(int effort, std::vector& nred, bool batch) { - const std::vector terms = getActive(); - return doInferencesInternal(effort, terms, nred, batch, true); -} - -// Register term. -void ExtTheory::registerTerm(Node n) { - if (d_extf_kind.find(n.getKind()) != d_extf_kind.end()) { - if (d_ext_func_terms.find(n) == d_ext_func_terms.end()) { - Trace("extt-debug") << "Found extended function : " << n << " in " - << d_parent->getId() << std::endl; - d_ext_func_terms[n] = true; - d_has_extf = n; - d_extf_info[n].d_vars = collectVars(n); - } - } -} - -void ExtTheory::registerTermRec(Node n) { - std::set visited; - registerTermRec(n, &visited); -} - -void ExtTheory::registerTermRec(Node n, std::set* visited) { - if (visited->find(n) == visited->end()) { - visited->insert(n); - registerTerm(n); - for (unsigned i = 0; i < n.getNumChildren(); i++) { - registerTermRec(n[i], visited); - } - } -} - -//mark reduced -void ExtTheory::markReduced( Node n, bool contextDepend ) { - registerTerm( n ); - Assert( d_ext_func_terms.find( n )!=d_ext_func_terms.end() ); - d_ext_func_terms[n] = false; - if( !contextDepend ){ - d_ci_inactive.insert( n ); - } - - //update has_extf - if( d_has_extf.get()==n ){ - for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ - //if not already reduced - if( (*it).second && !isContextIndependentInactive( (*it).first ) ){ - d_has_extf = (*it).first; - } - } - - } -} - -//mark congruent -void ExtTheory::markCongruent( Node a, Node b ) { - Trace("extt-debug") << "Mark congruent : " << a << " " << b << std::endl; - registerTerm( a ); - registerTerm( b ); - NodeBoolMap::const_iterator it = d_ext_func_terms.find( b ); - if( it!=d_ext_func_terms.end() ){ - if( d_ext_func_terms.find( a )!=d_ext_func_terms.end() ){ - d_ext_func_terms[a] = d_ext_func_terms[a] && (*it).second; - }else{ - Assert( false ); - } - d_ext_func_terms[b] = false; - }else{ - Assert( false ); - } -} - -bool ExtTheory::isContextIndependentInactive(Node n) const { - return d_ci_inactive.find(n) != d_ci_inactive.end(); -} - - -void ExtTheory::getTerms( std::vector< Node >& terms ) { - for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ - terms.push_back( (*it).first ); - } -} - -bool ExtTheory::hasActiveTerm() { - return !d_has_extf.get().isNull(); -} - -//is active -bool ExtTheory::isActive( Node n ) { - NodeBoolMap::const_iterator it = d_ext_func_terms.find( n ); - if( it!=d_ext_func_terms.end() ){ - return (*it).second && !isContextIndependentInactive( n ); - }else{ - return false; - } -} - -// get active -std::vector ExtTheory::getActive() const { - std::vector active; - for (NodeBoolMap::iterator it = d_ext_func_terms.begin(); - it != d_ext_func_terms.end(); ++it) { - // if not already reduced - if ((*it).second && !isContextIndependentInactive((*it).first)) { - active.push_back((*it).first); - } - } - return active; -} - -std::vector ExtTheory::getActive(Kind k) const { - std::vector active; - for (NodeBoolMap::iterator it = d_ext_func_terms.begin(); - it != d_ext_func_terms.end(); ++it) { - // if not already reduced - if ((*it).first.getKind() == k && (*it).second && - !isContextIndependentInactive((*it).first)) { - active.push_back((*it).first); - } - } - return active; -} - -void ExtTheory::clearCache() { - d_gst_cache.clear(); -} - }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/theory.h b/src/theory/theory.h index 231a56967..3721806ad 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -900,110 +900,6 @@ public: virtual ~EntailmentCheckSideEffects(); };/* class EntailmentCheckSideEffects */ - -class ExtTheory { - typedef context::CDHashMap NodeBoolMap; - typedef context::CDHashSet NodeSet; -private: - // collect variables - static std::vector collectVars(Node n); - // is 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 - bool sendLemma( Node lem, bool preprocess = false ); - // register term (recursive) - void registerTermRec(Node n, std::set* visited); - - Theory * d_parent; - Node d_true; - //extended string terms, map to whether they are active - NodeBoolMap d_ext_func_terms; - //set of terms from d_ext_func_terms that are SAT-context-independently inactive - // (e.g. term t when a reduction lemma of the form t = t' was added) - NodeSet d_ci_inactive; - //watched term for checking if any non-reduced extended functions exist - context::CDO< Node > d_has_extf; - //extf kind - std::map< Kind, bool > d_extf_kind; - //information for each term in d_ext_func_terms - class ExtfInfo { - public: - //all variables in this term - std::vector< Node > d_vars; - }; - std::map< Node, ExtfInfo > d_extf_info; - - //cache of all lemmas sent - NodeSet d_lemmas; - NodeSet d_pp_lemmas; - bool d_cacheEnabled; - // if d_cacheEnabled=true : - //cache for getSubstitutedTerms - class SubsTermInfo { - public: - Node d_sterm; - std::vector< Node > d_exp; - }; - std::map< int, std::map< Node, SubsTermInfo > > d_gst_cache; - - public: - ExtTheory(Theory* p, bool cacheEnabled = false ); - virtual ~ExtTheory() {} - // add extf kind - void addFunctionKind(Kind k) { d_extf_kind[k] = true; } - bool hasFunctionKind(Kind k) const { - return d_extf_kind.find(k) != d_extf_kind.end(); - } - // register term - // adds n to d_ext_func_terms if addFunctionKind( n.getKind() ) was called - void registerTerm( Node n ); - 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: set b inactive, set 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 - Node getSubstitutedTerm( int effort, Node term, std::vector< Node >& exp, bool useCache = false ); - void getSubstitutedTerms(int effort, const std::vector& terms, - std::vector& sterms, - std::vector >& exp, bool useCache = false); - // doInferences - // * input : effort, terms, batch (whether to send one lemma or lemmas for - // all terms) - // * 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 - // * output : nred (the terms that are still active) - // * return : true iff lemma is sent - bool doInferences(int effort, const std::vector& terms, - std::vector& nred, bool batch = true); - bool doInferences(int effort, std::vector& nred, bool batch = true); - //doReductions - // same as doInferences, but will send reduction lemmas of the form ( t = t' ) - // where t is in terms, t' is 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 terms from d_ext_func_terms - void getTerms( std::vector< Node >& terms ); - // has active term - bool hasActiveTerm(); - // is n active - bool isActive(Node n); - // 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; - //clear cache - void clearCache(); -}; - }/* CVC4::theory namespace */ }/* CVC4 namespace */