summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Makefile.am3
-rw-r--r--src/api/cvc4cpp.cpp112
-rw-r--r--src/context/cdvector.h162
-rw-r--r--src/theory/quantifiers/candidate_rewrite_database.cpp22
-rw-r--r--src/theory/quantifiers/candidate_rewrite_database.h9
-rw-r--r--src/theory/quantifiers/candidate_rewrite_filter.cpp413
-rw-r--r--src/theory/quantifiers/candidate_rewrite_filter.h218
-rw-r--r--src/theory/quantifiers/sygus_sampler.cpp372
-rw-r--r--src/theory/quantifiers/sygus_sampler.h166
-rw-r--r--src/theory/strings/kinds11
-rw-r--r--src/theory/strings/regexp_operation.cpp8
-rw-r--r--src/theory/strings/regexp_operation.h1
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp309
-rw-r--r--src/theory/strings/theory_strings_rewriter.h4
-rw-r--r--src/util/regexp.cpp17
-rw-r--r--src/util/regexp.h9
-rw-r--r--test/unit/Makefile.am1
-rw-r--r--test/unit/context/cdvector_black.h140
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);
- }
-
-};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback