theory/quantifiers/ceg_t_instantiator.h \
theory/quantifiers/conjecture_generator.cpp \
theory/quantifiers/conjecture_generator.h \
+ theory/quantifiers/dynamic_rewrite.cpp \
+ theory/quantifiers/dynamic_rewrite.h \
theory/quantifiers/equality_query.cpp \
theory/quantifiers/equality_query.h \
theory/quantifiers/equality_infer.cpp \
std::map<Node, SygusSamplerExt>::iterator its = d_sampler.find(prog);
if (its == d_sampler.end())
{
- d_sampler[prog].initializeSygus(
- sygusDb, prog, options::sygusSamples());
+ d_sampler[prog].initializeSygusExt(
+ d_qe, prog, options::sygusSamples());
its = d_sampler.find(prog);
}
Node solb = sygusDb->sygusToBuiltin(sol, prog.getType());
--- /dev/null
+/********************* */
+/*! \file dynamic_rewriter.cpp
+ ** \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 Implementation of dynamic_rewriter
+ **/
+
+#include "theory/quantifiers/dynamic_rewrite.h"
+
+#include "theory/rewriter.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+DynamicRewriter::DynamicRewriter(const std::string& name, QuantifiersEngine* qe)
+ : d_qe(qe),
+ d_equalityEngine(qe->getUserContext(), "DynamicRewriter::" + name, true)
+{
+ d_equalityEngine.addFunctionKind(kind::APPLY_UF);
+}
+
+bool DynamicRewriter::addRewrite(Node a, Node b)
+{
+ Trace("dyn-rewrite") << "Dyn-Rewriter : " << a << " == " << b << std::endl;
+ if (a == b)
+ {
+ Trace("dyn-rewrite") << "...fail, equal." << std::endl;
+ return false;
+ }
+
+ // add to the equality engine
+ Node ai = toInternal(a);
+ Node bi = toInternal(b);
+ d_equalityEngine.addTerm(ai);
+ d_equalityEngine.addTerm(bi);
+
+ // may already be equal by congruence
+ Node air = d_equalityEngine.getRepresentative(ai);
+ Node bir = d_equalityEngine.getRepresentative(bi);
+ if (air == bir)
+ {
+ Trace("dyn-rewrite") << "...fail, congruent." << std::endl;
+ return false;
+ }
+
+ Node eq = ai.eqNode(bi);
+ d_equalityEngine.assertEquality(eq, true, eq);
+ return true;
+}
+
+Node DynamicRewriter::toInternal(Node a)
+{
+ std::map<Node, Node>::iterator it = d_term_to_internal.find(a);
+ if (it != d_term_to_internal.end())
+ {
+ return it->second;
+ }
+ Node ret = a;
+
+ if (!a.isVar())
+ {
+ std::vector<Node> children;
+ if (a.hasOperator())
+ {
+ Node op = a.getOperator();
+ if (a.getKind() != APPLY_UF)
+ {
+ op = d_ois_trie[op].getSymbol(a);
+ }
+ children.push_back(op);
+ }
+ for (const Node& ca : a)
+ {
+ Node cai = toInternal(ca);
+ children.push_back(cai);
+ }
+ if (!children.empty())
+ {
+ if (children.size() == 1)
+ {
+ ret = children[0];
+ }
+ else
+ {
+ ret = NodeManager::currentNM()->mkNode(APPLY_UF, children);
+ }
+ }
+ }
+ d_term_to_internal[a] = ret;
+ return ret;
+}
+
+Node DynamicRewriter::OpInternalSymTrie::getSymbol(Node n)
+{
+ std::vector<TypeNode> ctypes;
+ for (const Node& cn : n)
+ {
+ ctypes.push_back(cn.getType());
+ }
+ ctypes.push_back(n.getType());
+
+ OpInternalSymTrie* curr = this;
+ for (unsigned i = 0, size = ctypes.size(); i < size; i++)
+ {
+ curr = &(curr->d_children[ctypes[i]]);
+ }
+ if (!curr->d_sym.isNull())
+ {
+ return curr->d_sym;
+ }
+ // make UF operator
+ TypeNode utype;
+ if (ctypes.size() == 1)
+ {
+ utype = ctypes[0];
+ }
+ else
+ {
+ utype = NodeManager::currentNM()->mkFunctionType(ctypes);
+ }
+ Node f = NodeManager::currentNM()->mkSkolem(
+ "ufd", utype, "internal op for dynamic_rewriter");
+ curr->d_sym = f;
+ return f;
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file dynamic_rewriter.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 dynamic_rewriter
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
+#define __CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
+
+#include <map>
+
+#include "theory/quantifiers_engine.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** DynamicRewriter
+ *
+ * This class is given a stream of equalities in calls to addRewrite(...).
+ * The goal is to show that a subset of these can be inferred from previously
+ * asserted equalities. For example, a possible set of return values for
+ * add rewrite on successive calls is the following:
+ *
+ * addRewrite( x, y ) ---> true
+ * addRewrite( f( x ), f( y ) ) ---> false, since we already know x=y
+ * addRewrite( x, z ) ---> true
+ * addRewrite( x+y, x+z ) ---> false, since we already know y=x=z.
+ *
+ * This class can be used to filter out redundant candidate rewrite rules
+ * when using the option sygusRewSynth().
+ *
+ * Currently, this class infers that an equality is redundant using
+ * an instance of the equality engine that does congruence over all
+ * operators by mapping all operators to uninterpreted ones and doing
+ * congruence on APPLY_UF.
+ *
+ * TODO (#1591): Add more advanced technique, e.g. by theory rewriting
+ * to show when terms can already be inferred equal.
+ */
+class DynamicRewriter
+{
+ public:
+ DynamicRewriter(const std::string& name, QuantifiersEngine* qe);
+ ~DynamicRewriter() {}
+ /** inform this class that the equality a = b holds.
+ *
+ * This function returns true if this class did not already know that
+ * a = b based on the previous equalities it has seen.
+ */
+ bool addRewrite(Node a, Node b);
+
+ private:
+ /** pointer to the quantifiers engine */
+ QuantifiersEngine* d_qe;
+ /** index over argument types to function skolems
+ *
+ * The purpose of this trie is to associate a class of interpreted operator
+ * with uninterpreted symbols. It is necessary to introduce multiple
+ * uninterpreted symbols per interpreted operator since they may be
+ * polymorphic. For example, for array select, its associate trie may look
+ * like this:
+ * d_children[array_type_1]
+ * d_children[index_type_1] : k1
+ * d_children[index_type_2] : k2
+ * d_children[array_type_2]
+ * d_children[index_type_1] : k3
+ */
+ class OpInternalSymTrie
+ {
+ public:
+ /**
+ * Get the uninterpreted function corresponding to the top-most symbol
+ * of the internal representation of term n. This will return a skolem
+ * of the same type as n.getOperator() if it has one, or of the same type
+ * as n itself otherwise.
+ */
+ Node getSymbol(Node n);
+
+ private:
+ /** the symbol at this node in the trie */
+ Node d_sym;
+ /** the children of this node in the trie */
+ std::map<TypeNode, OpInternalSymTrie> d_children;
+ };
+ /** the internal operator symbol trie for this class */
+ std::map<Node, OpInternalSymTrie> d_ois_trie;
+ /**
+ * Convert node a to its internal representation, which replaces all
+ * interpreted operators in a by a unique uninterpreted symbol.
+ */
+ Node toInternal(Node a);
+ /** cache of the above function */
+ std::map<Node, Node> d_term_to_internal;
+ /** stores congruence closure over terms given to this class. */
+ eq::EqualityEngine d_equalityEngine;
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
-#define __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H
#include <map>
#include "theory/quantifiers_engine.h"
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */
+#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H */
class SygusInvarianceTest
{
public:
- virtual ~SygusInvarianceTest(){}
+ virtual ~SygusInvarianceTest() {}
/** Is nvn invariant with respect to this test ?
*
}
}
+void SygusSamplerExt::initializeSygusExt(QuantifiersEngine* qe,
+ Node f,
+ unsigned nsamples)
+{
+ SygusSampler::initializeSygus(qe->getTermDatabaseSygus(), f, nsamples);
+
+ // initialize the dynamic rewriter
+ std::stringstream ss;
+ ss << f;
+ d_drewrite =
+ std::unique_ptr<DynamicRewriter>(new DynamicRewriter(ss.str(), qe));
+}
+
Node SygusSamplerExt::registerTerm(Node n, bool forceKeep)
{
Node eq_n = SygusSampler::registerTerm(n, forceKeep);
isUnique = containsFreeVariables(eq_n, n);
}
}
+ bool rewRedundant = false;
+ if (d_drewrite != nullptr)
+ {
+ if (!d_drewrite->addRewrite(n, eq_n))
+ {
+ rewRedundant = isUnique;
+ // must be unique according to the dynamic rewriter
+ isUnique = false;
+ }
+ }
if (isUnique)
{
}
return eq_n;
}
- else
+ else if (Trace.isOn("sygus-synth-rr"))
{
- Trace("sygus-synth-rr") << "Alpha equivalent candidate rewrite : " << eq_n
- << " " << n << std::endl;
+ Trace("sygus-synth-rr") << "Redundant rewrite : " << eq_n << " " << n;
+ if (rewRedundant)
+ {
+ Trace("sygus-synth-rr") << " (by rewriting)";
+ }
+ Trace("sygus-synth-rr") << std::endl;
}
return n;
}
#define __CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
#include <map>
+#include "theory/quantifiers/dynamic_rewrite.h"
#include "theory/quantifiers/term_database_sygus.h"
namespace CVC4 {
class SygusSamplerExt : public SygusSampler
{
public:
+ /** initialize extended */
+ void initializeSygusExt(QuantifiersEngine* qe, Node f, unsigned nsamples);
/** register term n with this sampler database
*
* This returns a term ret with the same guarantees as
* will not be input/output pairs of this function.
*/
virtual Node registerTerm(Node n, bool forceKeep = false) override;
+
+ private:
+ /** dynamic rewriter class */
+ std::unique_ptr<DynamicRewriter> d_drewrite;
};
} /* CVC4::theory::quantifiers namespace */
projects / cvc5.git / commitdiff