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 \
#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"
#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;
#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"
#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;
#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"
#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;
--- /dev/null
+/********************* */
+/*! \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<Node> ExtTheory::collectVars(Node n)
+{
+ std::vector<Node> vars;
+ std::set<Node> visited;
+ std::vector<Node> 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<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;
+ }
+
+ 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<Node>& terms,
+ std::vector<Node>& sterms,
+ std::vector<std::vector<Node> >& 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<Node>());
+ 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 (const Node& n : terms)
+ {
+ // do substitution, rewrite
+ std::map<Node, ExtfInfo>::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<Node> 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 (const Node& v : iti->second.d_vars)
+ {
+ std::map<Node, std::vector<Node> >::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<Node>& terms,
+ std::vector<Node>& 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<Node> sterms;
+ std::vector<std::vector<Node> > exp;
+ getSubstitutedTerms(effort, terms, sterms, exp);
+ std::map<Node, unsigned> 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<Node, unsigned>::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<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 (const Node& n : terms)
+ {
+ std::vector<Node> 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<Node>& terms,
+ std::vector<Node>& nred,
+ bool batch)
+{
+ if (!terms.empty())
+ {
+ return doInferencesInternal(effort, terms, nred, batch, false);
+ }
+ 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<Node>& terms,
+ std::vector<Node>& nred,
+ bool batch)
+{
+ if (!terms.empty())
+ {
+ return doInferencesInternal(effort, terms, nred, batch, true);
+ }
+ return false;
+}
+
+bool ExtTheory::doReductions(int effort, std::vector<Node>& nred, bool batch)
+{
+ const std::vector<Node> 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<TNode, TNodeHashFunction> visited;
+ std::vector<TNode> 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<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() 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<Node> ExtTheory::getActive() const
+{
+ std::vector<Node> 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<Node> ExtTheory::getActive(Kind k) const
+{
+ std::vector<Node> 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 */
--- /dev/null
+/********************* */
+/*! \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 <map>
+#include <set>
+
+#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<Node, bool, NodeHashFunction> NodeBoolMap;
+ typedef context::CDHashSet<Node, NodeHashFunction> 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<Node>& terms,
+ std::vector<Node>& sterms,
+ std::vector<std::vector<Node> >& 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<Node>& 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<Node>& terms,
+ std::vector<Node>& nred,
+ bool batch = true);
+ /**
+ * Calls the above function, where terms is getActive(), the set of currently
+ * active terms.
+ */
+ bool doInferences(int effort, std::vector<Node>& 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<Node>& terms,
+ std::vector<Node>& nred,
+ bool batch = true);
+ bool doReductions(int effort, std::vector<Node>& nred, bool batch = true);
+
+ /** get the set of all extended function terms from d_ext_func_terms */
+ void getTerms(std::vector<Node>& 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<Node> getActive() const;
+ /** get the set of active terms from d_ext_func_terms of kind k */
+ std::vector<Node> getActive(Kind k) const;
+
+ private:
+ /** returns the set of variable subterms of n */
+ static std::vector<Node> collectVars(Node n);
+ /** is n context dependent inactive? */
+ bool isContextIndependentInactive(Node n) const;
+ /** do inferences internal */
+ bool doInferencesInternal(int effort,
+ const std::vector<Node>& terms,
+ std::vector<Node>& 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<Node> d_has_extf;
+ /** the set of kinds we are treated as extended functions */
+ 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;
+ /** 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<Node> 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<int, std::map<Node, SubsTermInfo> > d_gst_cache;
+};
+
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__EXT_THEORY_H */
#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;
#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;
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<Node> ExtTheory::collectVars(Node n) {
- std::vector<Node> vars;
- std::set<Node> visited;
- std::vector<Node> 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<Node>& terms,
- std::vector<Node>& sterms,
- std::vector<std::vector<Node> >& exp,
- bool useCache) {
- if (useCache) {
- for( unsigned i=0; i<terms.size(); i++ ){
- Node n = terms[i];
- 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< Node >() );
- 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<terms.size(); i++ ){
- //do substitution, rewrite
- Node n = terms[i];
- std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n );
- Assert( iti!=d_extf_info.end() );
- for( unsigned i=0; i<iti->second.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<terms.size(); i++ ){
- Node n = terms[i];
- Node ns = n;
- std::vector< Node > 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; j<iti->second.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; k<itx->second.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<Node>& terms,
- std::vector<Node>& nred, bool batch,
- bool isRed) {
- if (batch) {
- bool addedLemma = false;
- if( isRed ){
- for( unsigned i=0; i<terms.size(); i++ ){
- Node n = terms[i];
- Node nr;
- //TODO: reduction with substitution?
- 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( 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; i<terms.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< 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<terms.size(); i++ ){
- std::vector< Node > 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<Node>& terms,
- std::vector<Node>& 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<Node>& terms,
- std::vector<Node>& nred, bool batch) {
- if (!terms.empty()) {
- return doInferencesInternal( effort, terms, nred, batch, true );
- }else{
- return false;
- }
-}
-
-bool ExtTheory::doReductions(int effort, std::vector<Node>& nred, bool batch) {
- const std::vector<Node> 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<Node> visited;
- registerTermRec(n, &visited);
-}
-
-void ExtTheory::registerTermRec(Node n, std::set<Node>* 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<Node> ExtTheory::getActive() const {
- std::vector<Node> 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<Node> ExtTheory::getActive(Kind k) const {
- std::vector<Node> 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 */
virtual ~EntailmentCheckSideEffects();
};/* class EntailmentCheckSideEffects */
-
-class ExtTheory {
- typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
-private:
- // collect variables
- static std::vector<Node> collectVars(Node n);
- // is context dependent inactive
- bool isContextIndependentInactive( Node n ) const;
- //do inferences internal
- bool doInferencesInternal(int effort, const std::vector<Node>& terms,
- std::vector<Node>& nred, bool batch, bool isRed);
- // send lemma
- bool sendLemma( Node lem, bool preprocess = false );
- // register term (recursive)
- void registerTermRec(Node n, std::set<Node>* 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<Node>& terms,
- std::vector<Node>& sterms,
- std::vector<std::vector<Node> >& 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<Node>& terms,
- std::vector<Node>& nred, bool batch = true);
- bool doInferences(int effort, std::vector<Node>& 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<Node>& terms,
- std::vector<Node>& nred, bool batch = true);
- bool doReductions(int effort, std::vector<Node>& 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<Node> getActive() const;
- // get the set of active terms from d_ext_func_terms of kind k
- std::vector<Node> getActive(Kind k) const;
- //clear cache
- void clearCache();
-};
-
}/* CVC4::theory namespace */
}/* CVC4 namespace */
projects / cvc5.git / commitdiff