diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-05 03:01:17 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-05 03:01:17 +0100 |
commit | 858a8d518da98113edd6f32190fff837871bb542 (patch) | |
tree | c2b506532fcc73eb6e0c675d22555e4da3c1f99c | |
parent | 31944046f098066d852abcb947aa477a908caf11 (diff) | |
parent | 8494e02bf31a08a686e1cf990e512250a9210acc (diff) |
Merge branch 'master' into sygus2018stringsRewsygus2018stringsRew
-rw-r--r-- | src/Makefile.am | 3 | ||||
-rw-r--r-- | src/api/cvc4cpp.cpp | 112 | ||||
-rw-r--r-- | src/context/cdvector.h | 162 | ||||
-rw-r--r-- | src/theory/quantifiers/candidate_rewrite_database.cpp | 22 | ||||
-rw-r--r-- | src/theory/quantifiers/candidate_rewrite_database.h | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/candidate_rewrite_filter.cpp | 413 | ||||
-rw-r--r-- | src/theory/quantifiers/candidate_rewrite_filter.h | 218 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.cpp | 372 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.h | 166 | ||||
-rw-r--r-- | src/theory/strings/kinds | 11 | ||||
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 8 | ||||
-rw-r--r-- | src/theory/strings/regexp_operation.h | 1 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 309 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.h | 4 | ||||
-rw-r--r-- | src/util/regexp.cpp | 17 | ||||
-rw-r--r-- | src/util/regexp.h | 9 | ||||
-rw-r--r-- | test/unit/Makefile.am | 1 | ||||
-rw-r--r-- | test/unit/context/cdvector_black.h | 140 |
18 files changed, 772 insertions, 1205 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index b4a083b0a..917fc6ef3 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -54,7 +54,6 @@ libcvc4_la_SOURCES = \ context/cdtrail_hashmap.h \ context/cdtrail_hashmap_forward.h \ context/cdtrail_queue.h \ - context/cdvector.h \ context/context.cpp \ context/context.h \ context/context_mm.cpp \ @@ -394,6 +393,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/bv_inverter.h \ theory/quantifiers/candidate_rewrite_database.cpp \ theory/quantifiers/candidate_rewrite_database.h \ + theory/quantifiers/candidate_rewrite_filter.cpp \ + theory/quantifiers/candidate_rewrite_filter.h \ theory/quantifiers/cegqi/ceg_instantiator.cpp \ theory/quantifiers/cegqi/ceg_instantiator.h \ theory/quantifiers/cegqi/ceg_arith_instantiator.cpp \ diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 703c298d3..6d5a423e4 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1092,5 +1092,117 @@ size_t OpTermHashFunction::operator()(const OpTerm& t) const return ExprHashFunction()(*t.d_expr); } +/* -------------------------------------------------------------------------- */ +/* Datatypes */ +/* -------------------------------------------------------------------------- */ + +/* DatatypeSelectorDecl ----------------------------------------------------- */ + +DatatypeSelectorDecl::DatatypeSelectorDecl(const std::string& name, Sort sort) + : d_name(name), d_sort(sort) +{ +} + +DatatypeSelectorDecl::DatatypeSelectorDecl(const std::string& name, + DatatypeDeclSelfSort sort) + : d_name(name), d_sort(Sort(CVC4::Type())) +{ +} + +std::string DatatypeSelectorDecl::toString() const +{ + std::stringstream ss; + ss << d_name << ": " << d_sort; + return ss.str(); +} + +std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl) +{ + out << dtdecl.toString(); + return out; +} + +/* DatatypeConstructorDecl -------------------------------------------------- */ + +DatatypeConstructorDecl::DatatypeConstructorDecl(const std::string& name) + : d_ctor(new CVC4::DatatypeConstructor(name)) +{ +} + +void DatatypeConstructorDecl::addSelector(const DatatypeSelectorDecl& stor) +{ + CVC4::Type t = *stor.d_sort.d_type; + if (t.isNull()) + { + d_ctor->addArg(stor.d_name, DatatypeSelfType()); + } + else + { + d_ctor->addArg(stor.d_name, t); + } +} + +std::string DatatypeConstructorDecl::toString() const +{ + std::stringstream ss; + ss << *d_ctor; + return ss.str(); +} + +std::ostream& operator<<(std::ostream& out, + const DatatypeConstructorDecl& ctordecl) +{ + out << ctordecl.toString(); + return out; +} + +/* DatatypeDecl ------------------------------------------------------------- */ + +DatatypeDecl::DatatypeDecl(const std::string& name, bool isCoDatatype) + : d_dtype(new CVC4::Datatype(name, isCoDatatype)) +{ +} + +DatatypeDecl::DatatypeDecl(const std::string& name, + Sort param, + bool isCoDatatype) + : d_dtype(new CVC4::Datatype( + name, std::vector<Type>{*param.d_type}, isCoDatatype)) +{ +} + +DatatypeDecl::DatatypeDecl(const std::string& name, + const std::vector<Sort>& params, + bool isCoDatatype) +{ + std::vector<Type> tparams; + for (const Sort& s : params) { tparams.push_back(*s.d_type); } + d_dtype = std::shared_ptr<CVC4::Datatype>( + new CVC4::Datatype(name, tparams, isCoDatatype)); +} + +DatatypeDecl::~DatatypeDecl() +{ +} + +void DatatypeDecl::addConstructor(const DatatypeConstructorDecl& ctor) +{ + d_dtype->addConstructor(*ctor.d_ctor); +} + +std::string DatatypeDecl::toString() const +{ + std::stringstream ss; + ss << *d_dtype; + return ss.str(); +} + +std::ostream& operator<<(std::ostream& out, + const DatatypeSelectorDecl& stordecl) +{ + out << stordecl.toString(); + return out; +} + } // namespace api } // namespace CVC4 diff --git a/src/context/cdvector.h b/src/context/cdvector.h deleted file mode 100644 index 2622ccdd2..000000000 --- a/src/context/cdvector.h +++ /dev/null @@ -1,162 +0,0 @@ -/********************* */ -/*! \file cdvector.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__CONTEXT__CDVECTOR_H -#define __CVC4__CONTEXT__CDVECTOR_H - -#include <vector> - -#include "base/cvc4_assert.h" -#include "context/context.h" -#include "context/cdlist.h" - -namespace CVC4 { -namespace context { - - -/** - * Generic context-dependent dynamic vector. - * This is quite different than CDList<T>. - * It provides the ability to destructively update the i'th item. - * - * The back of the vector may only be popped if there have been no updates to it - * at this context level. - */ -template <class T> -class CDVector { -private: - static const int ImpossibleLevel = -1; - - struct UpdatableElement { - public: - T d_data; - int d_contextLevelOfLastUpdate; - - UpdatableElement(const T& data) : - d_data(data), - d_contextLevelOfLastUpdate(ImpossibleLevel) { - } - };/* struct CDVector<T>::UpdatableElement */ - - struct HistoryElement { - public: - UpdatableElement d_cached; - size_t d_index; - HistoryElement(const UpdatableElement& cache, size_t index) : - d_cached(cache), d_index(index) { - } - };/* struct CDVector<T>::HistoryElement */ - - typedef std::vector< UpdatableElement > CurrentVector; - CurrentVector d_current; - - - - class HistoryListCleanUp{ - private: - CurrentVector& d_current; - public: - HistoryListCleanUp(CurrentVector& current) - : d_current(current) - {} - - void operator()(HistoryElement* back){ - d_current[back->d_index] = back->d_cached; - } - };/* class CDVector<T>::HistoryListCleanUp */ - - typedef CDList< HistoryElement, HistoryListCleanUp > HistoryVector; - HistoryVector d_history; - - Context* d_context; - - // no copy or assignment - CDVector(const CDVector&) CVC4_UNDEFINED; - CDVector& operator=(const CDVector&) CVC4_UNDEFINED; - -public: - CDVector(Context* c) : - d_current(), - d_history(c, true, HistoryListCleanUp(d_current)), - d_context(c) - {} - - size_t size() const { - return d_current.size(); - } - - /** - * Return true iff there are no valid objects in the list. - */ - bool empty() const { - return d_current.empty(); - } - - /** - * Add an item to the end of the list. - * Assigns its state at level 0 to be equal to data. - */ - void push_back(const T& data) { - d_current.push_back(UpdatableElement(data)); - } - - /** - * Access to the ith item in the list. - */ - const T& operator[](size_t i) const { - return get(i); - } - - const T& get(size_t i) const { - Assert(i < size(), "index out of bounds in CDVector::get()"); - //makeConsistent(); - return d_current[i].d_data; - } - - void set(size_t index, const T& data) { - Assert(index < size(), "index out of bounds in CDVector::set()"); - //makeConsistent(); - - if(d_current[index].d_contextLevelOfLastUpdate == d_context->getLevel()) { - d_current[index].d_data = data; - }else{ - d_history.push_back(HistoryElement(d_current[index], index)); - - d_current[index].d_data = data; - d_current[index].d_contextLevelOfLastUpdate = d_context->getLevel(); - } - } - - bool hasUpdates(size_t index) const { - Assert(index < size(), "index out of bounds in CDVector::hasUpdates()"); - return d_current[index].d_contextLevelOfLastUpdate == ImpossibleLevel; - } - - void pop_back() { - Assert(!empty(), "pop_back() on an empty CDVector"); - Assert(!hasUpdates(size() - 1), "popping an element with updates."); - d_current.pop_back(); - } - -};/* class CDVector<T> */ - -}/* CVC4::context namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__CONTEXT__CDVECTOR_H */ diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 9bbb88699..a5a35f89d 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -32,25 +32,12 @@ namespace CVC4 { namespace theory { namespace quantifiers { -// the number of d_drewrite objects we have allocated (to avoid name conflicts) -static unsigned drewrite_counter = 0; - CandidateRewriteDatabase::CandidateRewriteDatabase() : d_qe(nullptr), d_tds(nullptr), d_ext_rewrite(nullptr), d_using_sygus(false) { - if (options::sygusRewSynthFilterCong()) - { - // initialize the dynamic rewriter - std::stringstream ss; - ss << "_dyn_rewriter_" << drewrite_counter; - drewrite_counter++; - d_drewrite = std::unique_ptr<DynamicRewriter>( - new DynamicRewriter(ss.str(), &d_fake_context)); - d_sampler.setDynamicRewriter(d_drewrite.get()); - } } void CandidateRewriteDatabase::initialize(ExtendedRewriter* er, TypeNode tn, @@ -65,6 +52,7 @@ void CandidateRewriteDatabase::initialize(ExtendedRewriter* er, d_tds = nullptr; d_ext_rewrite = er; d_sampler.initialize(tn, vars, nsamples, unique_type_ids); + d_crewrite_filter.initialize(&d_sampler, nullptr, false); } void CandidateRewriteDatabase::initializeSygus(QuantifiersEngine* qe, @@ -81,6 +69,7 @@ void CandidateRewriteDatabase::initializeSygus(QuantifiersEngine* qe, d_tds = d_qe->getTermDatabaseSygus(); d_ext_rewrite = d_tds->getExtRewriter(); d_sampler.initializeSygus(d_tds, f, nsamples, useSygusType); + d_crewrite_filter.initialize(&d_sampler, d_tds, true); } bool CandidateRewriteDatabase::addTerm(Node sol, @@ -93,9 +82,8 @@ bool CandidateRewriteDatabase::addTerm(Node sol, if (eq_sol != sol) { is_unique_term = false; - // if eq_sol is null, then we have an uninteresting candidate rewrite, - // e.g. one that is alpha-equivalent to another. - if (!eq_sol.isNull()) + // should we filter the pair? + if (!d_crewrite_filter.filterPair(sol, eq_sol)) { // get the actual term Node solb = sol; @@ -215,7 +203,7 @@ bool CandidateRewriteDatabase::addTerm(Node sol, if (!is_unique_term) { // register this as a relevant pair (helps filtering) - d_sampler.registerRelevantPair(sol, eq_sol); + d_crewrite_filter.registerRelevantPair(sol, eq_sol); // The analog of terms sol and eq_sol are equivalent under // sample points but do not rewrite to the same term. Hence, // this indicates a candidate rewrite. diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index a2a6c5745..7f51043e2 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -21,6 +21,7 @@ #include <memory> #include <unordered_set> #include <vector> +#include "theory/quantifiers/candidate_rewrite_filter.h" #include "theory/quantifiers/sygus_sampler.h" namespace CVC4 { @@ -116,11 +117,9 @@ class CandidateRewriteDatabase * This is used for the sygusRewSynth() option to synthesize new candidate * rewrite rules. */ - SygusSamplerExt d_sampler; - /** a (dummy) user context, used for d_drewrite */ - context::UserContext d_fake_context; - /** dynamic rewriter class */ - std::unique_ptr<DynamicRewriter> d_drewrite; + SygusSampler d_sampler; + /** candidate rewrite filter */ + CandidateRewriteFilter d_crewrite_filter; /** * Cache of skolems for each free variable that appears in a synthesis check * (for --sygus-rr-synth-check). diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp new file mode 100644 index 000000000..68a3abe37 --- /dev/null +++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp @@ -0,0 +1,413 @@ +/********************* */ +/*! \file candidate_rewrite_filter.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 Implements techniques for candidate rewrite rule filtering, which + ** filters the output of --sygus-rr-synth. The classes in this file implement + ** filtering based on congruence, variable ordering, and matching. + **/ + +#include "theory/quantifiers/candidate_rewrite_filter.h" + +#include "options/base_options.h" +#include "options/quantifiers_options.h" +#include "printer/printer.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +bool MatchTrie::getMatches(Node n, NotifyMatch* ntm) +{ + std::vector<Node> vars; + std::vector<Node> subs; + std::map<Node, Node> smap; + + std::vector<std::vector<Node> > visit; + std::vector<MatchTrie*> visit_trie; + std::vector<int> visit_var_index; + std::vector<bool> visit_bound_var; + + visit.push_back(std::vector<Node>{n}); + visit_trie.push_back(this); + visit_var_index.push_back(-1); + visit_bound_var.push_back(false); + while (!visit.empty()) + { + std::vector<Node> cvisit = visit.back(); + MatchTrie* curr = visit_trie.back(); + if (cvisit.empty()) + { + Assert(n + == curr->d_data.substitute( + vars.begin(), vars.end(), subs.begin(), subs.end())); + Trace("crf-match-debug") << "notify : " << curr->d_data << std::endl; + if (!ntm->notify(n, curr->d_data, vars, subs)) + { + return false; + } + visit.pop_back(); + visit_trie.pop_back(); + visit_var_index.pop_back(); + visit_bound_var.pop_back(); + } + else + { + Node cn = cvisit.back(); + Trace("crf-match-debug") << "traverse : " << cn << " at depth " + << visit.size() << std::endl; + unsigned index = visit.size() - 1; + int vindex = visit_var_index[index]; + if (vindex == -1) + { + if (!cn.isVar()) + { + Node op = cn.hasOperator() ? cn.getOperator() : cn; + unsigned nchild = cn.hasOperator() ? cn.getNumChildren() : 0; + std::map<unsigned, MatchTrie>::iterator itu = + curr->d_children[op].find(nchild); + if (itu != curr->d_children[op].end()) + { + // recurse on the operator or self + cvisit.pop_back(); + if (cn.hasOperator()) + { + for (const Node& cnc : cn) + { + cvisit.push_back(cnc); + } + } + Trace("crf-match-debug") << "recurse op : " << op << std::endl; + visit.push_back(cvisit); + visit_trie.push_back(&itu->second); + visit_var_index.push_back(-1); + visit_bound_var.push_back(false); + } + } + visit_var_index[index]++; + } + else + { + // clean up if we previously bound a variable + if (visit_bound_var[index]) + { + Assert(!vars.empty()); + smap.erase(vars.back()); + vars.pop_back(); + subs.pop_back(); + visit_bound_var[index] = false; + } + + if (vindex == static_cast<int>(curr->d_vars.size())) + { + Trace("crf-match-debug") + << "finished checking " << curr->d_vars.size() + << " variables at depth " << visit.size() << std::endl; + // finished + visit.pop_back(); + visit_trie.pop_back(); + visit_var_index.pop_back(); + visit_bound_var.pop_back(); + } + else + { + Trace("crf-match-debug") << "check variable #" << vindex + << " at depth " << visit.size() << std::endl; + Assert(vindex < static_cast<int>(curr->d_vars.size())); + // recurse on variable? + Node var = curr->d_vars[vindex]; + bool recurse = true; + // check if it is already bound + std::map<Node, Node>::iterator its = smap.find(var); + if (its != smap.end()) + { + if (its->second != cn) + { + recurse = false; + } + } + else + { + vars.push_back(var); + subs.push_back(cn); + smap[var] = cn; + visit_bound_var[index] = true; + } + if (recurse) + { + Trace("crf-match-debug") << "recurse var : " << var << std::endl; + cvisit.pop_back(); + visit.push_back(cvisit); + visit_trie.push_back(&curr->d_children[var][0]); + visit_var_index.push_back(-1); + visit_bound_var.push_back(false); + } + visit_var_index[index]++; + } + } + } + } + return true; +} + +void MatchTrie::addTerm(Node n) +{ + std::vector<Node> visit; + visit.push_back(n); + MatchTrie* curr = this; + while (!visit.empty()) + { + Node cn = visit.back(); + visit.pop_back(); + if (cn.hasOperator()) + { + curr = &(curr->d_children[cn.getOperator()][cn.getNumChildren()]); + for (const Node& cnc : cn) + { + visit.push_back(cnc); + } + } + else + { + if (cn.isVar() + && std::find(curr->d_vars.begin(), curr->d_vars.end(), cn) + == curr->d_vars.end()) + { + curr->d_vars.push_back(cn); + } + curr = &(curr->d_children[cn][0]); + } + } + curr->d_data = n; +} + +void MatchTrie::clear() +{ + d_children.clear(); + d_vars.clear(); + d_data = Node::null(); +} + +// the number of d_drewrite objects we have allocated (to avoid name conflicts) +static unsigned drewrite_counter = 0; + +CandidateRewriteFilter::CandidateRewriteFilter() + : d_ss(nullptr), + d_tds(nullptr), + d_use_sygus_type(false), + d_drewrite(nullptr), + d_ssenm(*this) +{ +} + +void CandidateRewriteFilter::initialize(SygusSampler* ss, + TermDbSygus* tds, + bool useSygusType) +{ + d_ss = ss; + d_use_sygus_type = false; + d_tds = tds; + // initialize members of this class + d_match_trie.clear(); + d_pairs.clear(); + if (options::sygusRewSynthFilterCong()) + { + // initialize the dynamic rewriter + std::stringstream ss; + ss << "_dyn_rewriter_" << drewrite_counter; + drewrite_counter++; + d_drewrite = std::unique_ptr<DynamicRewriter>( + new DynamicRewriter(ss.str(), &d_fake_context)); + } +} + +bool CandidateRewriteFilter::filterPair(Node n, Node eq_n) +{ + Node bn = n; + Node beq_n = eq_n; + if (d_use_sygus_type) + { + bn = d_tds->sygusToBuiltin(n); + beq_n = d_tds->sygusToBuiltin(eq_n); + } + Trace("cr-filter") << "crewriteFilter : " << bn << "..." << beq_n + << std::endl; + // whether we will keep this pair + bool keep = true; + + // ----- check ordering redundancy + if (options::sygusRewSynthFilterOrder()) + { + bool nor = d_ss->isOrdered(bn); + bool eqor = d_ss->isOrdered(beq_n); + Trace("cr-filter-debug") << "Ordered? : " << nor << " " << eqor + << std::endl; + if (eqor || nor) + { + // if only one is ordered, then we require that the ordered one's + // variables cannot be a strict subset of the variables of the other. + if (!eqor) + { + if (d_ss->containsFreeVariables(beq_n, bn, true)) + { + keep = false; + } + else + { + // if the previous value stored was unordered, but n is + // ordered, we prefer n. Thus, we force its addition to the + // sampler database. + d_ss->registerTerm(n, true); + } + } + else if (!nor) + { + keep = !d_ss->containsFreeVariables(bn, beq_n, true); + } + } + else + { + keep = false; + } + if (!keep) + { + Trace("cr-filter") << "...redundant (unordered)" << std::endl; + } + } + + // ----- check rewriting redundancy + if (keep && d_drewrite != nullptr) + { + Trace("cr-filter-debug") << "Check equal rewrite pair..." << std::endl; + if (d_drewrite->areEqual(bn, beq_n)) + { + // must be unique according to the dynamic rewriter + Trace("cr-filter") << "...redundant (rewritable)" << std::endl; + keep = false; + } + } + + if (options::sygusRewSynthFilterMatch()) + { + // ----- check matchable + // check whether the pair is matchable with a previous one + d_curr_pair_rhs = beq_n; + Trace("crf-match") << "CRF check matches : " << bn << " [rhs = " << beq_n + << "]..." << std::endl; + if (!d_match_trie.getMatches(bn, &d_ssenm)) + { + keep = false; + Trace("cr-filter") << "...redundant (matchable)" << std::endl; + // regardless, would help to remember it + registerRelevantPair(n, eq_n); + } + } + + if (keep) + { + return false; + } + if (Trace.isOn("sygus-rr-filter")) + { + Printer* p = Printer::getPrinter(options::outputLanguage()); + std::stringstream ss; + ss << "(redundant-rewrite "; + p->toStreamSygus(ss, n); + ss << " "; + p->toStreamSygus(ss, eq_n); + ss << ")"; + Trace("sygus-rr-filter") << ss.str() << std::endl; + } + return true; +} + +void CandidateRewriteFilter::registerRelevantPair(Node n, Node eq_n) +{ + Node bn = n; + Node beq_n = eq_n; + if (d_use_sygus_type) + { + bn = d_tds->sygusToBuiltin(n); + beq_n = d_tds->sygusToBuiltin(eq_n); + } + // ----- check rewriting redundancy + if (d_drewrite != nullptr) + { + Trace("cr-filter-debug") << "Add rewrite pair..." << std::endl; + Assert(!d_drewrite->areEqual(bn, beq_n)); + d_drewrite->addRewrite(bn, beq_n); + } + if (options::sygusRewSynthFilterMatch()) + { + // add to match information + for (unsigned r = 0; r < 2; r++) + { + Node t = r == 0 ? bn : beq_n; + Node to = r == 0 ? beq_n : bn; + // insert in match trie if first time + if (d_pairs.find(t) == d_pairs.end()) + { + Trace("crf-match") << "CRF add term : " << t << std::endl; + d_match_trie.addTerm(t); + } + d_pairs[t].insert(to); + } + } +} + +bool CandidateRewriteFilter::notify(Node s, + Node n, + std::vector<Node>& vars, + std::vector<Node>& subs) +{ + Assert(!d_curr_pair_rhs.isNull()); + std::map<Node, std::unordered_set<Node, NodeHashFunction> >::iterator it = + d_pairs.find(n); + if (Trace.isOn("crf-match")) + { + Trace("crf-match") << " " << s << " matches " << n + << " under:" << std::endl; + for (unsigned i = 0, size = vars.size(); i < size; i++) + { + Trace("crf-match") << " " << vars[i] << " -> " << subs[i] << std::endl; + // TODO (#1923) ensure that we use an internal representation to + // ensure polymorphism is handled correctly + Assert(vars[i].getType().isComparableTo(subs[i].getType())); + } + } + Assert(it != d_pairs.end()); + for (const Node& nr : it->second) + { + Node nrs = + nr.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); + bool areEqual = (nrs == d_curr_pair_rhs); + if (!areEqual && d_drewrite != nullptr) + { + // if dynamic rewriter is available, consult it + areEqual = d_drewrite->areEqual(nrs, d_curr_pair_rhs); + } + if (areEqual) + { + Trace("crf-match") << "*** Match, current pair: " << std::endl; + Trace("crf-match") << " (" << s << ", " << d_curr_pair_rhs << ")" + << std::endl; + Trace("crf-match") << "is an instance of previous pair:" << std::endl; + Trace("crf-match") << " (" << n << ", " << nr << ")" << std::endl; + return false; + } + } + return true; +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/candidate_rewrite_filter.h b/src/theory/quantifiers/candidate_rewrite_filter.h new file mode 100644 index 000000000..9a09680cc --- /dev/null +++ b/src/theory/quantifiers/candidate_rewrite_filter.h @@ -0,0 +1,218 @@ +/********************* */ +/*! \file candidate_rewrite_filter.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 Implements techniques for candidate rewrite rule filtering, which + ** filters the output of --sygus-rr-synth. The classes in this file implement + ** filtering based on congruence, variable ordering, and matching. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H +#define __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H + +#include <map> +#include "theory/quantifiers/dynamic_rewrite.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" +#include "theory/quantifiers/sygus_sampler.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** A virtual class for notifications regarding matches. */ +class NotifyMatch +{ + public: + virtual ~NotifyMatch() {} + /** + * A notification that s is equal to n * { vars -> subs }. This function + * should return false if we do not wish to be notified of further matches. + */ + virtual bool notify(Node s, + Node n, + std::vector<Node>& vars, + std::vector<Node>& subs) = 0; +}; + +/** + * A trie (discrimination tree) storing a set of terms S, that can be used to + * query, for a given term t, all terms s from S that are matchable with t, + * that is s*sigma = t for some substitution sigma. + */ +class MatchTrie +{ + public: + /** Get matches + * + * This calls ntm->notify( n, s, vars, subs ) for each term s stored in this + * trie that is matchable with n where s = n * { vars -> subs } for some + * vars, subs. This function returns false if one of these calls to notify + * returns false. + */ + bool getMatches(Node n, NotifyMatch* ntm); + /** Adds node n to this trie */ + void addTerm(Node n); + /** Clear this trie */ + void clear(); + + private: + /** + * The children of this node in the trie. Terms t are indexed by a + * depth-first (right to left) traversal on its subterms, where the + * top-symbol of t is indexed by: + * - (operator, #children) if t has an operator, or + * - (t, 0) if t does not have an operator. + */ + std::map<Node, std::map<unsigned, MatchTrie> > d_children; + /** The set of variables in the domain of d_children */ + std::vector<Node> d_vars; + /** The data of this node in the trie */ + Node d_data; +}; + +/** candidate rewrite filter + * + * This class is responsible for various filtering techniques for candidate + * rewrite rules, including: + * (1) filtering based on variable ordering, + * (2) filtering based on congruence, + * (3) filtering based on matching. + * For details, see Reynolds et al "Rewrites for SMT Solvers using Syntax-Guided + * Enumeration", SMT 2018. + * + * In the following, we assume that the registerRelevantPair method of this + * class been called for some pairs of terms. For each such call to + * registerRelevantPair( t, s ), we say that (t,s) and (s,t) are "relevant + * pairs". A relevant pair ( t, s ) typically corresponds to a (candidate) + * rewrite t = s. + */ +class CandidateRewriteFilter +{ + public: + CandidateRewriteFilter(); + + /** initialize + * + * Initializes this class, ss is the sygus sampler that this class is + * filtering rewrite rule pairs for, and tds is a point to the sygus term + * database utility class. + * + * If useSygusType is false, this means that the terms in filterPair and + * registerRelevantPair calls should be interpreted as themselves. Otherwise, + * if useSygusType is true, these terms should be interpreted as their + * analog according to the deep embedding. + */ + void initialize(SygusSampler* ss, TermDbSygus* tds, bool useSygusType); + /** filter pair + * + * This method returns true if the pair (n, eq_n) should be filtered. If it + * is not filtered, then the caller may choose to call + * registerRelevantPair(n, eq_n) below, although it may not, say if it finds + * another reason to discard the pair. + * + * If this method returns false, then for all previous relevant pairs + * ( a, eq_a ), we have that n = eq_n is not an instance of a = eq_a + * modulo symmetry of equality, nor is n = eq_n derivable from the set of + * all previous relevant pairs. The latter is determined by the d_drewrite + * utility. For example: + * [1] ( t+0, t ) and ( x+0, x ) + * will not both be relevant pairs of this function since t+0=t is + * an instance of x+0=x. + * [2] ( s, t ) and ( s+0, t+0 ) + * will not both be relevant pairs of this function since s+0=t+0 is + * derivable from s=t. + * These two criteria may be combined, for example: + * [3] ( t+0, s ) is not a relevant pair if both ( x+0, x+s ) and ( t+s, s ) + * are relevant pairs, since t+0 is an instance of x+0 where + * { x |-> t }, and x+s { x |-> t } = s is derivable, via the third pair + * above (t+s = s). + */ + bool filterPair(Node n, Node eq_n); + /** register relevant pair + * + * This should be called after filterPair( n, eq_n ) returns false. + * This registers ( n, eq_n ) as a relevant pair with this class. + */ + void registerRelevantPair(Node n, Node eq_n); + + private: + /** pointer to the sygus sampler that this class is filtering rewrites for */ + SygusSampler* d_ss; + /** pointer to the sygus term database, used if d_use_sygus_type is true */ + TermDbSygus* d_tds; + /** whether we are registering sygus terms with this class */ + bool d_use_sygus_type; + + //----------------------------congruence filtering + /** a (dummy) user context, used for d_drewrite */ + context::UserContext d_fake_context; + /** dynamic rewriter class */ + std::unique_ptr<DynamicRewriter> d_drewrite; + //----------------------------end congruence filtering + + //----------------------------match filtering + /** + * Stores all relevant pairs returned by this sampler (see registerTerm). In + * detail, if (t,s) is a relevant pair, then t in d_pairs[s]. + */ + std::map<Node, std::unordered_set<Node, NodeHashFunction> > d_pairs; + /** Match trie storing all terms in the domain of d_pairs. */ + MatchTrie d_match_trie; + /** Notify class */ + class CandidateRewriteFilterNotifyMatch : public NotifyMatch + { + CandidateRewriteFilter& d_sse; + + public: + CandidateRewriteFilterNotifyMatch(CandidateRewriteFilter& sse) : d_sse(sse) + { + } + /** notify match */ + bool notify(Node n, + Node s, + std::vector<Node>& vars, + std::vector<Node>& subs) override + { + return d_sse.notify(n, s, vars, subs); + } + }; + /** Notify object used for reporting matches from d_match_trie */ + CandidateRewriteFilterNotifyMatch d_ssenm; + /** + * Stores the current right hand side of a pair we are considering. + * + * In more detail, in registerTerm, we are interested in whether a pair (s,t) + * is a relevant pair. We do this by: + * (1) Setting the node d_curr_pair_rhs to t, + * (2) Using d_match_trie, compute all terms s1...sn that match s. + * For each si, where s = si * sigma for some substitution sigma, we check + * whether t = ti * sigma for some previously relevant pair (si,ti), in + * which case (s,t) is an instance of (si,ti). + */ + Node d_curr_pair_rhs; + /** + * Called by the above class during d_match_trie.getMatches( s ), when we + * find that si = s * sigma, where si is a term that is stored in + * d_match_trie. + * + * This function returns false if ( s, d_curr_pair_rhs ) is an instance of + * previously relevant pair. + */ + bool notify(Node s, Node n, std::vector<Node>& vars, std::vector<Node>& subs); + //----------------------------end match filtering +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */ diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index e07f73540..ebd10c585 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -746,378 +746,6 @@ void SygusSampler::registerSygusType(TypeNode tn) } } -SygusSamplerExt::SygusSamplerExt() : d_drewrite(nullptr), d_ssenm(*this) {} - -void SygusSamplerExt::initializeSygus(TermDbSygus* tds, - Node f, - unsigned nsamples, - bool useSygusType) -{ - SygusSampler::initializeSygus(tds, f, nsamples, useSygusType); - d_pairs.clear(); - d_match_trie.clear(); -} - -void SygusSamplerExt::setDynamicRewriter(DynamicRewriter* dr) -{ - d_drewrite = dr; -} - -Node SygusSamplerExt::registerTerm(Node n, bool forceKeep) -{ - Node eq_n = SygusSampler::registerTerm(n, forceKeep); - if (eq_n == n) - { - // this is a unique term - return n; - } - Node bn = n; - Node beq_n = eq_n; - if (d_use_sygus_type) - { - bn = d_tds->sygusToBuiltin(n); - beq_n = d_tds->sygusToBuiltin(eq_n); - } - Trace("sygus-synth-rr") << "sygusSampleExt : " << bn << "..." << beq_n - << std::endl; - // whether we will keep this pair - bool keep = true; - - // ----- check ordering redundancy - if (options::sygusRewSynthFilterOrder()) - { - bool nor = isOrdered(bn); - bool eqor = isOrdered(beq_n); - Trace("sygus-synth-rr-debug") << "Ordered? : " << nor << " " << eqor - << std::endl; - if (eqor || nor) - { - // if only one is ordered, then we require that the ordered one's - // variables cannot be a strict subset of the variables of the other. - if (!eqor) - { - if (containsFreeVariables(beq_n, bn, true)) - { - keep = false; - } - else - { - // if the previous value stored was unordered, but n is - // ordered, we prefer n. Thus, we force its addition to the - // sampler database. - SygusSampler::registerTerm(n, true); - } - } - else if (!nor) - { - keep = !containsFreeVariables(bn, beq_n, true); - } - } - else - { - keep = false; - } - if (!keep) - { - Trace("sygus-synth-rr") << "...redundant (unordered)" << std::endl; - } - } - - // ----- check rewriting redundancy - if (keep && d_drewrite != nullptr) - { - Trace("sygus-synth-rr-debug") << "Check equal rewrite pair..." << std::endl; - if (d_drewrite->areEqual(bn, beq_n)) - { - // must be unique according to the dynamic rewriter - Trace("sygus-synth-rr") << "...redundant (rewritable)" << std::endl; - keep = false; - } - } - - if (options::sygusRewSynthFilterMatch()) - { - // ----- check matchable - // check whether the pair is matchable with a previous one - d_curr_pair_rhs = beq_n; - Trace("sse-match") << "SSE check matches : " << bn << " [rhs = " << beq_n - << "]..." << std::endl; - if (!d_match_trie.getMatches(bn, &d_ssenm)) - { - keep = false; - Trace("sygus-synth-rr") << "...redundant (matchable)" << std::endl; - // regardless, would help to remember it - registerRelevantPair(n, eq_n); - } - } - - if (keep) - { - return eq_n; - } - if (Trace.isOn("sygus-rr-filter")) - { - Printer* p = Printer::getPrinter(options::outputLanguage()); - std::stringstream ss; - ss << "(redundant-rewrite "; - p->toStreamSygus(ss, n); - ss << " "; - p->toStreamSygus(ss, eq_n); - ss << ")"; - Trace("sygus-rr-filter") << ss.str() << std::endl; - } - return Node::null(); -} - -void SygusSamplerExt::registerRelevantPair(Node n, Node eq_n) -{ - Node bn = n; - Node beq_n = eq_n; - if (d_use_sygus_type) - { - bn = d_tds->sygusToBuiltin(n); - beq_n = d_tds->sygusToBuiltin(eq_n); - } - // ----- check rewriting redundancy - if (d_drewrite != nullptr) - { - Trace("sygus-synth-rr-debug") << "Add rewrite pair..." << std::endl; - Assert(!d_drewrite->areEqual(bn, beq_n)); - d_drewrite->addRewrite(bn, beq_n); - } - if (options::sygusRewSynthFilterMatch()) - { - // add to match information - for (unsigned r = 0; r < 2; r++) - { - Node t = r == 0 ? bn : beq_n; - Node to = r == 0 ? beq_n : bn; - // insert in match trie if first time - if (d_pairs.find(t) == d_pairs.end()) - { - Trace("sse-match") << "SSE add term : " << t << std::endl; - d_match_trie.addTerm(t); - } - d_pairs[t].insert(to); - } - } -} - -bool SygusSamplerExt::notify(Node s, - Node n, - std::vector<Node>& vars, - std::vector<Node>& subs) -{ - Assert(!d_curr_pair_rhs.isNull()); - std::map<Node, std::unordered_set<Node, NodeHashFunction> >::iterator it = - d_pairs.find(n); - if (Trace.isOn("sse-match")) - { - Trace("sse-match") << " " << s << " matches " << n - << " under:" << std::endl; - for (unsigned i = 0, size = vars.size(); i < size; i++) - { - Trace("sse-match") << " " << vars[i] << " -> " << subs[i] << std::endl; - // TODO (#1923) ensure that we use an internal representation to - // ensure polymorphism is handled correctly - Assert(vars[i].getType().isComparableTo(subs[i].getType())); - } - } - Assert(it != d_pairs.end()); - for (const Node& nr : it->second) - { - Node nrs = - nr.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); - bool areEqual = (nrs == d_curr_pair_rhs); - if (!areEqual && d_drewrite != nullptr) - { - // if dynamic rewriter is available, consult it - areEqual = d_drewrite->areEqual(nrs, d_curr_pair_rhs); - } - if (areEqual) - { - Trace("sse-match") << "*** Match, current pair: " << std::endl; - Trace("sse-match") << " (" << s << ", " << d_curr_pair_rhs << ")" - << std::endl; - Trace("sse-match") << "is an instance of previous pair:" << std::endl; - Trace("sse-match") << " (" << n << ", " << nr << ")" << std::endl; - return false; - } - } - return true; -} - -bool MatchTrie::getMatches(Node n, NotifyMatch* ntm) -{ - std::vector<Node> vars; - std::vector<Node> subs; - std::map<Node, Node> smap; - - std::vector<std::vector<Node> > visit; - std::vector<MatchTrie*> visit_trie; - std::vector<int> visit_var_index; - std::vector<bool> visit_bound_var; - - visit.push_back(std::vector<Node>{n}); - visit_trie.push_back(this); - visit_var_index.push_back(-1); - visit_bound_var.push_back(false); - while (!visit.empty()) - { - std::vector<Node> cvisit = visit.back(); - MatchTrie* curr = visit_trie.back(); - if (cvisit.empty()) - { - Assert(n - == curr->d_data.substitute( - vars.begin(), vars.end(), subs.begin(), subs.end())); - Trace("sse-match-debug") << "notify : " << curr->d_data << std::endl; - if (!ntm->notify(n, curr->d_data, vars, subs)) - { - return false; - } - visit.pop_back(); - visit_trie.pop_back(); - visit_var_index.pop_back(); - visit_bound_var.pop_back(); - } - else - { - Node cn = cvisit.back(); - Trace("sse-match-debug") - << "traverse : " << cn << " at depth " << visit.size() << std::endl; - unsigned index = visit.size() - 1; - int vindex = visit_var_index[index]; - if (vindex == -1) - { - if (!cn.isVar()) - { - Node op = cn.hasOperator() ? cn.getOperator() : cn; - unsigned nchild = cn.hasOperator() ? cn.getNumChildren() : 0; - std::map<unsigned, MatchTrie>::iterator itu = - curr->d_children[op].find(nchild); - if (itu != curr->d_children[op].end()) - { - // recurse on the operator or self - cvisit.pop_back(); - if (cn.hasOperator()) - { - for (const Node& cnc : cn) - { - cvisit.push_back(cnc); - } - } - Trace("sse-match-debug") << "recurse op : " << op << std::endl; - visit.push_back(cvisit); - visit_trie.push_back(&itu->second); - visit_var_index.push_back(-1); - visit_bound_var.push_back(false); - } - } - visit_var_index[index]++; - } - else - { - // clean up if we previously bound a variable - if (visit_bound_var[index]) - { - Assert(!vars.empty()); - smap.erase(vars.back()); - vars.pop_back(); - subs.pop_back(); - visit_bound_var[index] = false; - } - - if (vindex == static_cast<int>(curr->d_vars.size())) - { - Trace("sse-match-debug") - << "finished checking " << curr->d_vars.size() - << " variables at depth " << visit.size() << std::endl; - // finished - visit.pop_back(); - visit_trie.pop_back(); - visit_var_index.pop_back(); - visit_bound_var.pop_back(); - } - else - { - Trace("sse-match-debug") << "check variable #" << vindex - << " at depth " << visit.size() << std::endl; - Assert(vindex < static_cast<int>(curr->d_vars.size())); - // recurse on variable? - Node var = curr->d_vars[vindex]; - bool recurse = true; - // check if it is already bound - std::map<Node, Node>::iterator its = smap.find(var); - if (its != smap.end()) - { - if (its->second != cn) - { - recurse = false; - } - } - else - { - vars.push_back(var); - subs.push_back(cn); - smap[var] = cn; - visit_bound_var[index] = true; - } - if (recurse) - { - Trace("sse-match-debug") << "recurse var : " << var << std::endl; - cvisit.pop_back(); - visit.push_back(cvisit); - visit_trie.push_back(&curr->d_children[var][0]); - visit_var_index.push_back(-1); - visit_bound_var.push_back(false); - } - visit_var_index[index]++; - } - } - } - } - return true; -} - -void MatchTrie::addTerm(Node n) -{ - std::vector<Node> visit; - visit.push_back(n); - MatchTrie* curr = this; - while (!visit.empty()) - { - Node cn = visit.back(); - visit.pop_back(); - if (cn.hasOperator()) - { - curr = &(curr->d_children[cn.getOperator()][cn.getNumChildren()]); - for (const Node& cnc : cn) - { - visit.push_back(cnc); - } - } - else - { - if (cn.isVar() - && std::find(curr->d_vars.begin(), curr->d_vars.end(), cn) - == curr->d_vars.end()) - { - curr->d_vars.push_back(cn); - } - curr = &(curr->d_children[cn][0]); - } - } - curr->d_data = n; -} - -void MatchTrie::clear() -{ - d_children.clear(); - d_vars.clear(); - d_data = Node::null(); -} - } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index 290a8b17d..0134b3a86 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -19,7 +19,6 @@ #include <map> #include "theory/evaluator.h" -#include "theory/quantifiers/dynamic_rewrite.h" #include "theory/quantifiers/lazy_trie.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_enumeration.h" @@ -28,7 +27,6 @@ namespace CVC4 { namespace theory { namespace quantifiers { - /** SygusSampler * * This class can be used to test whether two expressions are equivalent @@ -124,7 +122,7 @@ class SygusSampler : public LazyTrieEvaluator */ int getDiffSamplePointIndex(Node a, Node b); - protected: + //--------------------------queries about terms /** is contiguous * * This returns whether n's free variables (terms occurring in the range of @@ -149,6 +147,7 @@ class SygusSampler : public LazyTrieEvaluator * occur in the range d_type_vars. */ bool containsFreeVariables(Node a, Node b, bool strict = false); + //--------------------------end queries about terms protected: /** sygus term database of d_qe */ @@ -286,167 +285,6 @@ class SygusSampler : public LazyTrieEvaluator void registerSygusType(TypeNode tn); }; -/** A virtual class for notifications regarding matches. */ -class NotifyMatch -{ - public: - virtual ~NotifyMatch() {} - - /** - * A notification that s is equal to n * { vars -> subs }. This function - * should return false if we do not wish to be notified of further matches. - */ - virtual bool notify(Node s, - Node n, - std::vector<Node>& vars, - std::vector<Node>& subs) = 0; -}; - -/** - * A trie (discrimination tree) storing a set of terms S, that can be used to - * query, for a given term t, all terms from S that are matchable with t. - */ -class MatchTrie -{ - public: - /** Get matches - * - * This calls ntm->notify( n, s, vars, subs ) for each term s stored in this - * trie that is matchable with n where s = n * { vars -> subs } for some - * vars, subs. This function returns false if one of these calls to notify - * returns false. - */ - bool getMatches(Node n, NotifyMatch* ntm); - /** Adds node n to this trie */ - void addTerm(Node n); - /** Clear this trie */ - void clear(); - - private: - /** - * The children of this node in the trie. Terms t are indexed by a - * depth-first (right to left) traversal on its subterms, where the - * top-symbol of t is indexed by: - * - (operator, #children) if t has an operator, or - * - (t, 0) if t does not have an operator. - */ - std::map<Node, std::map<unsigned, MatchTrie> > d_children; - /** The set of variables in the domain of d_children */ - std::vector<Node> d_vars; - /** The data of this node in the trie */ - Node d_data; -}; - -/** Version of the above class with some additional features */ -class SygusSamplerExt : public SygusSampler -{ - public: - SygusSamplerExt(); - /** initialize */ - void initializeSygus(TermDbSygus* tds, - Node f, - unsigned nsamples, - bool useSygusType) override; - /** set dynamic rewriter - * - * This tells this class to use the dynamic rewriter object dr. This utility - * is used to query whether pairs of terms are already entailed to be - * equal based on previous rewrite rules. - */ - void setDynamicRewriter(DynamicRewriter* dr); - - /** register term n with this sampler database - * - * For each call to registerTerm( t, ... ) that returns s, we say that - * (t,s) and (s,t) are "relevant pairs". - * - * This returns either null, or a term ret with the same guarantees as - * SygusSampler::registerTerm with the additional guarantee - * that for all previous relevant pairs ( n', nret' ), - * we have that n = ret is not an instance of n' = ret' - * modulo symmetry of equality, nor is n = ret derivable from the set of - * all previous relevant pairs. The latter is determined by the d_drewrite - * utility. For example: - * [1] ( t+0, t ) and ( x+0, x ) - * will not both be relevant pairs of this function since t+0=t is - * an instance of x+0=x. - * [2] ( s, t ) and ( s+0, t+0 ) - * will not both be relevant pairs of this function since s+0=t+0 is - * derivable from s=t. - * These two criteria may be combined, for example: - * [3] ( t+0, s ) is not a relevant pair if both ( x+0, x+s ) and ( t+s, s ) - * are relevant pairs, since t+0 is an instance of x+0 where - * { x |-> t }, and x+s { x |-> t } = s is derivable, via the third pair - * above (t+s = s). - * - * If this function returns null, then n is equivalent to a previously - * registered term ret, and the equality ( n, ret ) is either an instance - * of a previous relevant pair ( n', ret' ), or n = ret is derivable - * from the set of all previous relevant pairs based on the - * d_drewrite utility, or is an instance of a previous pair - */ - Node registerTerm(Node n, bool forceKeep = false) override; - /** register relevant pair - * - * This should be called after registerTerm( n ) returns eq_n. - * This registers ( n, eq_n ) as a relevant pair with this class. - */ - void registerRelevantPair(Node n, Node eq_n); - - private: - /** pointer to the dynamic rewriter class */ - DynamicRewriter* d_drewrite; - - //----------------------------match filtering - /** - * Stores all relevant pairs returned by this sampler (see registerTerm). In - * detail, if (t,s) is a relevant pair, then t in d_pairs[s]. - */ - std::map<Node, std::unordered_set<Node, NodeHashFunction> > d_pairs; - /** Match trie storing all terms in the domain of d_pairs. */ - MatchTrie d_match_trie; - /** Notify class */ - class SygusSamplerExtNotifyMatch : public NotifyMatch - { - SygusSamplerExt& d_sse; - - public: - SygusSamplerExtNotifyMatch(SygusSamplerExt& sse) : d_sse(sse) {} - /** notify match */ - bool notify(Node n, - Node s, - std::vector<Node>& vars, - std::vector<Node>& subs) override - { - return d_sse.notify(n, s, vars, subs); - } - }; - /** Notify object used for reporting matches from d_match_trie */ - SygusSamplerExtNotifyMatch d_ssenm; - /** - * Stores the current right hand side of a pair we are considering. - * - * In more detail, in registerTerm, we are interested in whether a pair (s,t) - * is a relevant pair. We do this by: - * (1) Setting the node d_curr_pair_rhs to t, - * (2) Using d_match_trie, compute all terms s1...sn that match s. - * For each si, where s = si * sigma for some substitution sigma, we check - * whether t = ti * sigma for some previously relevant pair (si,ti), in - * which case (s,t) is an instance of (si,ti). - */ - Node d_curr_pair_rhs; - /** - * Called by the above class during d_match_trie.getMatches( s ), when we - * find that si = s * sigma, where si is a term that is stored in - * d_match_trie. - * - * This function returns false if ( s, d_curr_pair_rhs ) is an instance of - * previously relevant pair. - */ - bool notify(Node s, Node n, std::vector<Node>& vars, std::vector<Node>& subs); - //----------------------------end match filtering -}; - } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index d931e99bc..de4a013cd 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -28,13 +28,6 @@ operator STRING_ITOS 1 "integer to string" operator STRING_STOI 1 "string to integer (total function)" operator STRING_CODE 1 "string to code, returns the code of the first character of the string if it has length one, -1 otherwise" -#sort CHAR_TYPE \ -# Cardinality::INTEGERS \ -# well-founded \ -# "NodeManager::currentNM()->mkConst(::CVC4::String())" \ -# "util/regexp.h" \ -# "String type" - sort STRING_TYPE \ Cardinality::INTEGERS \ well-founded \ @@ -53,10 +46,6 @@ enumerator STRING_TYPE \ "::CVC4::theory::strings::StringEnumerator" \ "theory/strings/type_enumerator.h" -#enumerator REGEXP_TYPE \ -# "::CVC4::theory::strings::RegExpEnumerator" \ -# "theory/strings/type_enumerator.h" - constant CONST_STRING \ ::CVC4::String \ ::CVC4::strings::StringHashFunction \ diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index e130d5e4b..d17e42ede 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -45,14 +45,6 @@ RegExpOpr::RegExpOpr() RegExpOpr::~RegExpOpr() {} -int RegExpOpr::gcd ( int a, int b ) { - int c; - while ( a != 0 ) { - c = a; a = b%a; b = c; - } - return b; -} - bool RegExpOpr::checkConstRegExp( Node r ) { Trace("strings-regexp-cstre") << "RegExp-CheckConstRegExp starts with /" << mkString( r ) << "/" << std::endl; bool ret = true; diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index d33a2b70c..ecf294fc6 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -71,7 +71,6 @@ private: void simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes ); void simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes ); std::string niceChar( Node r ); - int gcd ( int a, int b ); Node mkAllExceptOne( unsigned char c ); bool isPairNodesInSet(std::set< PairNodes > &s, Node n1, Node n2); diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index c070b88f2..cd7c6eeb4 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -385,302 +385,6 @@ Node TheoryStringsRewriter::rewriteConcat(Node node) return retNode; } - -void TheoryStringsRewriter::mergeInto(std::vector<Node> &t, const std::vector<Node> &s) { - for(std::vector<Node>::const_iterator itr=s.begin(); itr!=s.end(); itr++) { - if(std::find(t.begin(), t.end(), (*itr)) == t.end()) { - t.push_back( *itr ); - } - } -} - -void TheoryStringsRewriter::shrinkConVec(std::vector<Node> &vec) { - unsigned i = 0; - Node emptysingleton = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( CVC4::String("") ) ); - while(i < vec.size()) { - if( vec[i] == emptysingleton ) { - vec.erase(vec.begin() + i); - } else if(vec[i].getKind()==kind::STRING_TO_REGEXP && i<vec.size()-1 && vec[i+1].getKind()==kind::STRING_TO_REGEXP) { - Node tmp = NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, vec[i][0], vec[i+1][0]); - tmp = rewriteConcat(tmp); - vec[i] = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, tmp); - vec.erase(vec.begin() + i + 1); - } else { - i++; - } - } -} - -Node TheoryStringsRewriter::applyAX( TNode node ) { - Trace("regexp-ax") << "Regexp::AX start " << node << std::endl; - Node retNode = node; - - int k = node.getKind(); - switch( k ) { - case kind::REGEXP_UNION: { - std::vector<Node> vec_nodes; - for(unsigned i=0; i<node.getNumChildren(); i++) { - Node tmp = applyAX(node[i]); - if(tmp.getKind() == kind::REGEXP_UNION) { - for(unsigned j=0; j<tmp.getNumChildren(); j++) { - if(std::find(vec_nodes.begin(), vec_nodes.end(), tmp[j]) == vec_nodes.end()) { - vec_nodes.push_back(tmp[j]); - } - } - } else if(tmp.getKind() == kind::REGEXP_EMPTY) { - // do nothing - } else { - if(std::find(vec_nodes.begin(), vec_nodes.end(), tmp) == vec_nodes.end()) { - vec_nodes.push_back(tmp); - } - } - } - if(vec_nodes.empty()) { - std::vector< Node > nvec; - retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec ); - } else { - retNode = vec_nodes.size() == 1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vec_nodes ); - } - break; - } - case kind::REGEXP_CONCAT: { - std::vector< std::vector<Node> > vec_nodes; - bool emptyflag = false; - Node emptysingleton = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( CVC4::String("") ) ); - for(unsigned i=0; i<node.getNumChildren(); i++) { - Node tmp = applyAX(node[i]); - if(tmp.getKind() == kind::REGEXP_EMPTY) { - emptyflag = true; - break; - } else if(tmp == emptysingleton) { - //do nothing - } else if(vec_nodes.empty()) { - if(tmp.getKind() == kind::REGEXP_UNION) { - for(unsigned j=0; j<tmp.getNumChildren(); j++) { - std::vector<Node> vtmp; - if(tmp[j].getKind() == kind::REGEXP_CONCAT) { - for(unsigned j2=0; j2<tmp[j].getNumChildren(); j2++) { - vtmp.push_back(tmp[j][j2]); - } - } else { - vtmp.push_back(tmp[j]); - } - vec_nodes.push_back(vtmp); - } - } else if(tmp.getKind() == kind::REGEXP_CONCAT) { - std::vector<Node> vtmp; - for(unsigned j=0; j<tmp.getNumChildren(); j++) { - vtmp.push_back(tmp[j]); - } - vec_nodes.push_back(vtmp); - } else { - std::vector<Node> vtmp; - vtmp.push_back(tmp); - vec_nodes.push_back(vtmp); - } - } else { - //non-empty vec - if(tmp.getKind() == kind::REGEXP_UNION) { - unsigned cnt = vec_nodes.size(); - for(unsigned i2=0; i2<cnt; i2++) { - //std::vector<Node> vleft( vec_nodes[i2] ); - for(unsigned j=0; j<tmp.getNumChildren(); j++) { - if(tmp[j] == emptysingleton) { - vec_nodes.push_back( vec_nodes[i2] ); - } else { - std::vector<Node> vt( vec_nodes[i2] ); - if(tmp[j].getKind() != kind::REGEXP_CONCAT) { - vt.push_back( tmp[j] ); - } else { - for(unsigned j2=0; j2<tmp[j].getNumChildren(); j2++) { - vt.push_back(tmp[j][j2]); - } - } - vec_nodes.push_back(vt); - } - } - } - vec_nodes.erase(vec_nodes.begin(), vec_nodes.begin() + cnt); - } else if(tmp.getKind() == kind::REGEXP_CONCAT) { - for(unsigned i2=0; i2<vec_nodes.size(); i2++) { - for(unsigned j=0; j<tmp.getNumChildren(); j++) { - vec_nodes[i2].push_back(tmp[j]); - } - } - } else { - for(unsigned i2=0; i2<vec_nodes.size(); i2++) { - vec_nodes[i2].push_back(tmp); - } - } - } - } - if(emptyflag) { - std::vector< Node > nvec; - retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec ); - } else if(vec_nodes.empty()) { - retNode = emptysingleton; - } else if(vec_nodes.size() == 1) { - shrinkConVec(vec_nodes[0]); - retNode = vec_nodes[0].empty()? emptysingleton - : vec_nodes[0].size()==1? vec_nodes[0][0] - : NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_nodes[0]); - } else { - std::vector<Node> vtmp; - for(unsigned i=0; i<vec_nodes.size(); i++) { - shrinkConVec(vec_nodes[i]); - if(!vec_nodes[i].empty()) { - Node ntmp = vec_nodes[i].size()==1? vec_nodes[i][0] - : NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_nodes[i]); - vtmp.push_back(ntmp); - } - } - retNode = vtmp.empty()? emptysingleton - : vtmp.size()==1? vtmp[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vtmp); - } - break; - } - case kind::REGEXP_STAR: { - Node tmp = applyAX(node[0]); - Node emptysingleton = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( CVC4::String("") ) ); - if(tmp.getKind() == kind::REGEXP_EMPTY || tmp == emptysingleton) { - retNode = emptysingleton; - } else { - if(tmp.getKind() == kind::REGEXP_UNION) { - std::vector<Node> vec; - for(unsigned i=0; i<tmp.getNumChildren(); i++) { - if(tmp[i] != emptysingleton) { - vec.push_back(tmp[i]); - } - } - if(vec.size() != tmp.getNumChildren()) { - tmp = vec.size()==1? vec[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vec) ; - } - } else if(tmp.getKind() == kind::REGEXP_STAR) { - tmp = tmp[0]; - } - if(tmp != node[0]) { - retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, tmp ); - } - } - break; - } - case kind::REGEXP_INTER: { - std::vector< std::vector<Node> > vec_nodes; - bool emptyflag = false; - bool epsflag = false; - Node emptysingleton = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( CVC4::String("") ) ); - for(unsigned i=0; i<node.getNumChildren(); i++) { - Node tmp = applyAX(node[i]); - if(tmp.getKind() == kind::REGEXP_EMPTY) { - emptyflag = true; - break; - } else if(vec_nodes.empty()) { - if(tmp.getKind() == kind::REGEXP_INTER) { - std::vector<Node> vtmp; - for(unsigned j=0; j<tmp.getNumChildren(); j++) { - vtmp.push_back(tmp[j]); - } - vec_nodes.push_back(vtmp); - } else if(tmp.getKind() == kind::REGEXP_UNION) { - for(unsigned j=0; j<tmp.getNumChildren(); j++) { - std::vector<Node> vtmp; - if(tmp[j].getKind() == kind::REGEXP_INTER) { - for(unsigned j2=0; j2<tmp[j].getNumChildren(); j2++) { - vtmp.push_back(tmp[j][j2]); - } - } else { - vtmp.push_back(tmp[j]); - } - vec_nodes.push_back(vtmp); - } - } else { - if(tmp == emptysingleton) { - epsflag = true; - } - std::vector<Node> vtmp; - vtmp.push_back(tmp); - vec_nodes.push_back(vtmp); - } - } else { - //non-empty vec - if(tmp.getKind() == kind::REGEXP_INTER) { - for(unsigned j=0; j<tmp.getNumChildren(); j++) { - for(unsigned i2=0; i2<vec_nodes.size(); i2++) { - if(std::find(vec_nodes[i2].begin(), vec_nodes[i2].end(), tmp[j]) == vec_nodes[i2].end()) { - vec_nodes[i2].push_back(tmp[j]); - } - } - } - } else if(tmp == emptysingleton) { - if(!epsflag) { - epsflag = true; - for(unsigned j=0; j<vec_nodes.size(); j++) { - vec_nodes[j].insert(vec_nodes[j].begin(), emptysingleton); - } - } - } else if(tmp.getKind() == kind::REGEXP_UNION) { - unsigned cnt = vec_nodes.size(); - for(unsigned i2=0; i2<cnt; i2++) { - //std::vector<Node> vleft( vec_nodes[i2] ); - for(unsigned j=0; j<tmp.getNumChildren(); j++) { - std::vector<Node> vt(vec_nodes[i2]); - if(tmp[j].getKind() != kind::REGEXP_INTER) { - if(std::find(vt.begin(), vt.end(), tmp[j]) == vt.end()) { - vt.push_back(tmp[j]); - } - } else { - std::vector<Node> vtmp; - for(unsigned j2=0; j2<tmp[j].getNumChildren(); j2++) { - vtmp.push_back(tmp[j][j2]); - } - mergeInto(vt, vtmp); - } - vec_nodes.push_back(vt); - } - } - vec_nodes.erase(vec_nodes.begin(), vec_nodes.begin() + cnt); - } else { - for(unsigned j=0; j<vec_nodes.size(); j++) { - if(std::find(vec_nodes[j].begin(), vec_nodes[j].end(), tmp) == vec_nodes[j].end()) { - vec_nodes[j].push_back(tmp); - } - } - } - } - } - if(emptyflag) { - std::vector< Node > nvec; - retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec ); - } else if(vec_nodes.empty()) { - //to check? - retNode = emptysingleton; - } else if(vec_nodes.size() == 1) { - retNode = vec_nodes[0].empty() ? emptysingleton : vec_nodes[0].size() == 1 ? vec_nodes[0][0] : NodeManager::currentNM()->mkNode( kind::REGEXP_INTER, vec_nodes[0] ); - } else { - std::vector<Node> vtmp; - for(unsigned i=0; i<vec_nodes.size(); i++) { - Node tmp = vec_nodes[i].empty()? emptysingleton : vec_nodes[i].size() == 1 ? vec_nodes[i][0] : NodeManager::currentNM()->mkNode( kind::REGEXP_INTER, vec_nodes[i] ); - vtmp.push_back(tmp); - } - retNode = vtmp.size() == 1? vtmp[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vtmp ); - } - break; - } - case kind::REGEXP_SIGMA: { - break; - } - case kind::REGEXP_EMPTY: { - break; - } - //default: { - //to check? - //} - } - - Trace("regexp-ax") << "Regexp::AX end " << node << " to\n " << retNode << std::endl; - return retNode; -} - Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) { Assert( node.getKind() == kind::REGEXP_CONCAT ); Trace("strings-prerewrite") << "Strings::prerewriteConcatRegExp start " << node << std::endl; @@ -1026,7 +730,7 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i Node TheoryStringsRewriter::rewriteMembership(TNode node) { Node retNode = node; Node x = node[0]; - Node r = node[1];//applyAX(node[1]); + Node r = node[1]; if(r.getKind() == kind::REGEXP_EMPTY) { retNode = NodeManager::currentNM()->mkConst( false ); @@ -1215,16 +919,9 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { if(node[0].isConst()) { CVC4::String s = node[0].getConst<String>(); if(s.isNumber()) { - std::string stmp = s.toString(); - //TODO: leading zeros : when smt2 standard for strings is set, uncomment this if applicable - //if(stmp[0] == '0' && stmp.size() != 1) { - //retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(-1)); - //} else { - CVC4::Rational r2(stmp.c_str()); - retNode = NodeManager::currentNM()->mkConst( r2 ); - //} + retNode = nm->mkConst(s.toNumber()); } else { - retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(-1)); + retNode = nm->mkConst(::CVC4::Rational(-1)); } } else if(node[0].getKind() == kind::STRING_CONCAT) { for(unsigned i=0; i<node[0].getNumChildren(); ++i) { diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index 74d219e50..732d64095 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -61,10 +61,6 @@ class TheoryStringsRewriter { static bool isConstRegExp( TNode t ); static bool testConstStringInRegExp( CVC4::String &s, unsigned int index_start, TNode r ); - static void mergeInto(std::vector<Node> &t, const std::vector<Node> &s); - static void shrinkConVec(std::vector<Node> &vec); - static Node applyAX( TNode node ); - static Node prerewriteConcatRegExp(TNode node); static Node prerewriteOrRegExp(TNode node); static Node prerewriteAndRegExp(TNode node); diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp index 8589c6993..93178b948 100644 --- a/src/util/regexp.cpp +++ b/src/util/regexp.cpp @@ -421,18 +421,11 @@ size_t String::maxSize() { return std::numeric_limits<size_t>::max(); } - -int String::toNumber() const { - if (isNumber()) { - int ret = 0; - for (unsigned int i = 0; i < size(); ++i) { - unsigned char c = convertUnsignedIntToChar(d_str[i]); - ret = ret * 10 + (int)c - (int)'0'; - } - return ret; - } else { - return -1; - } +Rational String::toNumber() const +{ + // when smt2 standard for strings is set, this may change, based on the + // semantics of str.from.int for leading zeros + return Rational(toString()); } unsigned char String::hexToDec(unsigned char c) { diff --git a/src/util/regexp.h b/src/util/regexp.h index e2d07111d..e91ca61e2 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -25,6 +25,7 @@ #include <ostream> #include <string> #include <vector> +#include "util/rational.h" namespace CVC4 { @@ -178,8 +179,14 @@ class CVC4_PUBLIC String { */ std::size_t roverlap(const String& y) const; + /** + * Returns true if this string corresponds in text to a number, for example + * this returns true for strings "7", "12", "004", "0" and false for strings + * "abc", "4a", "-4", "". + */ bool isNumber() const; - int toNumber() const; + /** Returns the corresponding rational for the text of this string. */ + Rational toNumber() const; const std::vector<unsigned>& getVec() const { return d_str; } /** is the unsigned a digit? diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 0ab305039..d58ee411f 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -40,7 +40,6 @@ UNIT_TESTS += \ context/cdlist_black \ context/cdmap_black \ context/cdmap_white \ - context/cdvector_black \ util/array_store_all_black \ util/assert_white \ util/check_white \ diff --git a/test/unit/context/cdvector_black.h b/test/unit/context/cdvector_black.h deleted file mode 100644 index 3769b2cce..000000000 --- a/test/unit/context/cdvector_black.h +++ /dev/null @@ -1,140 +0,0 @@ -/********************* */ -/*! \file cdvector_black.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include <cxxtest/TestSuite.h> - -#include <vector> -#include <iostream> - -#include <limits.h> - -#include "context/context.h" -#include "context/cdvector.h" - -using namespace std; -using namespace CVC4::context; - -struct DtorSensitiveObject { - bool& d_dtorCalled; - DtorSensitiveObject(bool& dtorCalled) : d_dtorCalled(dtorCalled) {} - ~DtorSensitiveObject() { d_dtorCalled = true; } -}; - - - -class CDListBlack : public CxxTest::TestSuite { -private: - - Context* d_context; - -public: - - void setUp() { - d_context = new Context(); - } - - void tearDown() { - delete d_context; - } - - void testCDVector17() { vectorTest(17); } - void testCDVector31() { vectorTest(31); } - void testCDVector191() { vectorTest(113); } - - void vectorTest(unsigned P){ - vectorTest(P, 2); - vectorTest(P, 5); - vectorTest(P, P/3 + 1); - } - - void vectorTest(unsigned P, unsigned m){ - for(unsigned g=2; g< P; g++){ - vectorTest(P, g, m, 1); - vectorTest(P, g, m, 3); - } - } - vector<unsigned> copy(CDVector<unsigned>& v){ - vector<unsigned> ret; - for(unsigned i=0; i < v.size(); ++i){ - ret.push_back(v[i]); - } - return ret; - } - - void equal(vector<unsigned>& copy, CDVector<unsigned>& v){ - TS_ASSERT_EQUALS(copy.size(), v.size()); - for(unsigned i = 0; i < v.size(); ++i){ - TS_ASSERT_EQUALS(copy[i], v[i]); - } - } - - void vectorTest(unsigned P, unsigned g, unsigned m, unsigned r) { - CDVector<unsigned> vec(d_context); - vector< vector<unsigned> > copies; - - copies.push_back( copy(vec) ); - d_context->push(); - - TS_ASSERT(vec.empty()); - for(unsigned i = 0; i < P; ++i){ - vec.push_back(i); - TS_ASSERT_EQUALS(vec.size(), i+1); - } - TS_ASSERT(!vec.empty()); - TS_ASSERT_EQUALS(vec.size(), P); - - copies.push_back( copy(vec) ); - d_context->push(); - - for(unsigned i = 0, g_i = 1; i < r*P; ++i, g_i = (g_i * g)% P){ - if(i % m == 0){ - copies.push_back( copy(vec) ); - d_context->push(); - } - - vec.set(g_i, i); - - TS_ASSERT_EQUALS(vec.get(g_i), i); - } - TS_ASSERT_EQUALS(vec.size(), P); - - copies.push_back( copy(vec) ); - - while(d_context->getLevel() >= 1){ - TS_ASSERT_EQUALS(vec.size(), P); - equal(copies[d_context->getLevel()], vec); - d_context->pop(); - } - } - - void testTreeUpdate() { - CDVector<int> vec(d_context); - vec.push_back(-1); - - vec.set(0, 0); - d_context->push(); - d_context->push(); - vec.set(0, 1); - d_context->pop(); - d_context->pop(); - - d_context->push(); - d_context->push(); - TS_ASSERT_EQUALS(vec.get(0), 0); - } - -}; |