diff options
| -rw-r--r-- | src/Makefile.am | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/ce_guided_conjecture.cpp | 4 | ||||
| -rw-r--r-- | src/theory/quantifiers/dynamic_rewrite.cpp | 140 | ||||
| -rw-r--r-- | src/theory/quantifiers/dynamic_rewrite.h | 114 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus_grammar_red.h | 6 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus_invariance.h | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus_sampler.cpp | 33 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus_sampler.h | 7 |
8 files changed, 299 insertions, 9 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 0006a8521..bcbe15192 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -387,6 +387,8 @@ libcvc4_la_SOURCES = \ 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 \ diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp index d325f3f36..b8f016a79 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/ce_guided_conjecture.cpp @@ -629,8 +629,8 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation 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()); diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp new file mode 100644 index 000000000..a19695770 --- /dev/null +++ b/src/theory/quantifiers/dynamic_rewrite.cpp @@ -0,0 +1,140 @@ +/********************* */ +/*! \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 */ diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h new file mode 100644 index 000000000..be2ff4c78 --- /dev/null +++ b/src/theory/quantifiers/dynamic_rewrite.h @@ -0,0 +1,114 @@ +/********************* */ +/*! \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 */ diff --git a/src/theory/quantifiers/sygus_grammar_red.h b/src/theory/quantifiers/sygus_grammar_red.h index b65a12da2..d0484aa57 100644 --- a/src/theory/quantifiers/sygus_grammar_red.h +++ b/src/theory/quantifiers/sygus_grammar_red.h @@ -14,8 +14,8 @@ #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" @@ -116,4 +116,4 @@ class SygusRedundantCons } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */ +#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H */ diff --git a/src/theory/quantifiers/sygus_invariance.h b/src/theory/quantifiers/sygus_invariance.h index 1cc43fb7d..a43e38719 100644 --- a/src/theory/quantifiers/sygus_invariance.h +++ b/src/theory/quantifiers/sygus_invariance.h @@ -43,7 +43,7 @@ class CegConjecture; class SygusInvarianceTest { public: - virtual ~SygusInvarianceTest(){} + virtual ~SygusInvarianceTest() {} /** Is nvn invariant with respect to this test ? * diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index c7c322132..757b8e44f 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -640,6 +640,19 @@ void SygusSampler::registerSygusType(TypeNode tn) } } +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); @@ -665,6 +678,16 @@ Node SygusSamplerExt::registerTerm(Node n, bool 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) { @@ -677,10 +700,14 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep) } 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; } diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index 8ed4bc783..48ddddbc6 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -18,6 +18,7 @@ #define __CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H #include <map> +#include "theory/quantifiers/dynamic_rewrite.h" #include "theory/quantifiers/term_database_sygus.h" namespace CVC4 { @@ -327,6 +328,8 @@ class SygusSampler : public LazyTrieEvaluator 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 @@ -338,6 +341,10 @@ class SygusSamplerExt : public SygusSampler * 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 */ |