d_theoryEngine(nullptr),
d_propEngine(nullptr),
d_proofManager(nullptr),
+ d_rewriter(new theory::Rewriter()),
d_definedFunctions(nullptr),
d_fmfRecFunctionsDefined(nullptr),
d_assertionList(nullptr),
namespace theory {
class TheoryModel;
+ class Rewriter;
}/* CVC4::theory namespace */
// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
friend class ::CVC4::LogicRequest;
friend class ::CVC4::Model; // to access d_modelCommands
friend class ::CVC4::theory::TheoryModel;
+ friend class ::CVC4::theory::Rewriter;
/* ....................................................................... */
public:
/** Get a pointer to the ProofManager owned by this SmtEngine. */
ProofManager* getProofManager() { return d_proofManager.get(); };
+ /** Get a pointer to the Rewriter owned by this SmtEngine. */
+ theory::Rewriter* getRewriter() { return d_rewriter.get(); }
+
/** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */
StatisticsRegistry* getStatisticsRegistry()
{
/** The proof manager */
std::unique_ptr<ProofManager> d_proofManager;
+ /**
+ * The rewriter associated with this SmtEngine. We have a different instance
+ * of the rewriter for each SmtEngine instance. This is because rewriters may
+ * hold references to objects that belong to theory solvers, which are
+ * specific to an SmtEngine/TheoryEngine instance.
+ */
+ std::unique_ptr<theory::Rewriter> d_rewriter;
+
/** An index of our defined functions */
DefinedFunctionMap* d_definedFunctions;
delete d_internal;
}
-std::unique_ptr<TheoryRewriter> TheoryArith::mkTheoryRewriter()
+TheoryRewriter* TheoryArith::getTheoryRewriter()
{
- return std::unique_ptr<TheoryRewriter>(new ArithRewriter());
+ return d_internal->getTheoryRewriter();
}
void TheoryArith::preRegisterTerm(TNode n){
Valuation valuation, const LogicInfo& logicInfo);
virtual ~TheoryArith();
- std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+ TheoryRewriter* getTheoryRewriter() override;
/**
* Does non-context dependent setup for a node connected to a theory.
TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
~TheoryArithPrivate();
+ TheoryRewriter* getTheoryRewriter() { return &d_rewriter; }
+
/**
* Does non-context dependent setup for a node connected to a theory.
*/
NodeMap d_int_div_skolem;
NodeMap d_nlin_inverse_skolem;
+ /** The theory rewriter for this theory. */
+ ArithRewriter d_rewriter;
};/* class TheoryArithPrivate */
}/* CVC4::theory::arith namespace */
smtStatisticsRegistry()->unregisterStat(&d_numSetModelValConflicts);
}
-std::unique_ptr<TheoryRewriter> TheoryArrays::mkTheoryRewriter()
-{
- return std::unique_ptr<TheoryRewriter>(new TheoryArraysRewriter());
-}
-
void TheoryArrays::setMasterEqualityEngine(eq::EqualityEngine* eq) {
d_equalityEngine.setMasterEqualityEngine(eq);
}
#include "context/cdqueue.h"
#include "theory/arrays/array_info.h"
#include "theory/arrays/array_proof_reconstruction.h"
+#include "theory/arrays/theory_arrays_rewriter.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
#include "util/statistics_registry.h"
std::string name = "");
~TheoryArrays();
- std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+ TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
bool ppDisequal(TNode a, TNode b);
Node solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck);
+ /** The theory rewriter for this theory. */
+ TheoryArraysRewriter d_rewriter;
+
public:
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
Node ppRewrite(TNode atom) override;
namespace theory {
namespace booleans {
-std::unique_ptr<TheoryRewriter> TheoryBool::mkTheoryRewriter()
+TheoryBool::TheoryBool(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo)
+ : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo)
{
- return std::unique_ptr<TheoryRewriter>(new TheoryBoolRewriter());
}
Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
#ifndef CVC4__THEORY__BOOLEANS__THEORY_BOOL_H
#define CVC4__THEORY__BOOLEANS__THEORY_BOOL_H
-#include "theory/theory.h"
#include "context/context.h"
+#include "theory/booleans/theory_bool_rewriter.h"
+#include "theory/theory.h"
namespace CVC4 {
namespace theory {
namespace booleans {
class TheoryBool : public Theory {
-public:
- TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out,
- Valuation valuation, const LogicInfo& logicInfo)
- : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo)
- {}
+ public:
+ TheoryBool(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo);
- std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+ TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
//void check(Effort);
std::string identify() const override { return std::string("TheoryBool"); }
+
+ private:
+ /** The theory rewriter for this theory. */
+ TheoryBoolRewriter d_rewriter;
};/* class TheoryBool */
}/* CVC4::theory::booleans namespace */
{
}
-std::unique_ptr<TheoryRewriter> TheoryBuiltin::mkTheoryRewriter()
-{
- return std::unique_ptr<TheoryRewriter>(new TheoryBuiltinRewriter());
-}
-
std::string TheoryBuiltin::identify() const
{
return std::string("TheoryBuiltin");
#ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H
#define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H
+#include "theory/builtin/theory_builtin_rewriter.h"
#include "theory/theory.h"
namespace CVC4 {
Valuation valuation,
const LogicInfo& logicInfo);
- std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+ TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
std::string identify() const override;
/** finish initialization */
void finishInit() override;
+
+ private:
+ /** The theory rewriter for this theory. */
+ TheoryBuiltinRewriter d_rewriter;
}; /* class TheoryBuiltin */
} // namespace builtin
Assert(retNode.getType() == node.getType());
Assert(expr::hasFreeVar(node) == expr::hasFreeVar(retNode));
return RewriteResponse(REWRITE_DONE, retNode);
- }
- }else{
+ }
+ }
+ else
+ {
Trace("builtin-rewrite-debug") << "...failed to get array representation." << std::endl;
}
return RewriteResponse(REWRITE_DONE, node);
TheoryBV::~TheoryBV() {}
-std::unique_ptr<TheoryRewriter> TheoryBV::mkTheoryRewriter()
-{
- return std::unique_ptr<TheoryRewriter>(new TheoryBVRewriter());
-}
-
void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
if (options::bitblastMode() == options::BitblastMode::EAGER)
{
#include "context/cdlist.h"
#include "context/context.h"
#include "theory/bv/bv_subtheory.h"
+#include "theory/bv/theory_bv_rewriter.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/theory.h"
#include "util/hash.h"
~TheoryBV();
- std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+ TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
void checkForLemma(TNode node);
+ /** The theory rewriter for this theory. */
+ TheoryBVRewriter d_rewriter;
+
friend class LazyBitblaster;
friend class TLazyBitblaster;
friend class EagerBitblaster;
}
}
-std::unique_ptr<TheoryRewriter> TheoryDatatypes::mkTheoryRewriter()
-{
- return std::unique_ptr<TheoryRewriter>(new DatatypesRewriter());
-}
-
void TheoryDatatypes::setMasterEqualityEngine(eq::EqualityEngine* eq) {
d_equalityEngine.setMasterEqualityEngine(eq);
}
#include "expr/attribute.h"
#include "expr/datatype.h"
#include "expr/node_trie.h"
+#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/datatypes/sygus_extension.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
const LogicInfo& logicInfo);
~TheoryDatatypes();
- std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+ TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
bool areDisequal( TNode a, TNode b );
bool areCareDisequal( TNode x, TNode y );
TNode getRepresentative( TNode a );
-private:
- /** sygus symmetry breaking utility */
- std::unique_ptr<SygusExtension> d_sygusExtension;
+ private:
+ /** sygus symmetry breaking utility */
+ std::unique_ptr<SygusExtension> d_sygusExtension;
+
+ /** The theory rewriter for this theory. */
+ DatatypesRewriter d_rewriter;
};/* class TheoryDatatypes */
}/* CVC4::theory::datatypes namespace */
d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_COMPONENT_EXPONENT);
d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND);
d_equalityEngine.addFunctionKind(kind::ROUNDINGMODE_BITBLAST);
-
} /* TheoryFp::TheoryFp() */
-std::unique_ptr<TheoryRewriter> TheoryFp::mkTheoryRewriter()
-{
- return std::unique_ptr<TheoryRewriter>(new TheoryFpRewriter());
-}
-
Node TheoryFp::minUF(Node node) {
Assert(node.getKind() == kind::FLOATINGPOINT_MIN);
TypeNode t(node.getType());
#include "context/cdo.h"
#include "theory/fp/fp_converter.h"
+#include "theory/fp/theory_fp_rewriter.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
TheoryFp(context::Context* c, context::UserContext* u, OutputChannel& out,
Valuation valuation, const LogicInfo& logicInfo);
- std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+ TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
Node expandDefinition(LogicRequest& lr, Node node) override;
bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete);
+ /** The theory rewriter for this theory. */
+ TheoryFpRewriter d_rewriter;
}; /* class TheoryFp */
} // namespace fp
d_ext_rewrite = er;
}
-CandidateRewriteDatabaseGen::CandidateRewriteDatabaseGen(
- std::vector<Node>& vars, unsigned nsamples)
- : d_qe(nullptr), d_vars(vars.begin(), vars.end()), d_nsamples(nsamples)
-{
-}
-
-bool CandidateRewriteDatabaseGen::addTerm(Node n, std::ostream& out)
-{
- ExtendedRewriter* er = &d_ext_rewrite;
- Node nr;
- if (er == nullptr)
- {
- nr = Rewriter::rewrite(n);
- }
- else
- {
- nr = er->extendedRewrite(n);
- }
- TypeNode tn = nr.getType();
- std::map<TypeNode, CandidateRewriteDatabase>::iterator itc = d_cdbs.find(tn);
- if (itc == d_cdbs.end())
- {
- Trace("synth-rr-dbg") << "Initialize database for " << tn << std::endl;
- // initialize with the extended rewriter owned by this class
- d_cdbs[tn].initialize(d_vars, &d_sampler[tn]);
- d_cdbs[tn].setExtendedRewriter(er);
- itc = d_cdbs.find(tn);
- Trace("synth-rr-dbg") << "...finish." << std::endl;
- }
- Trace("synth-rr-dbg") << "Add term " << nr << " for " << tn << std::endl;
- return itc->second.addTerm(nr, false, out);
-}
-
} /* CVC4::theory::quantifiers namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
bool d_silent;
};
-/**
- * This class generates and stores candidate rewrite databases for multiple
- * types as needed.
- */
-class CandidateRewriteDatabaseGen
-{
- public:
- /** constructor
- *
- * vars : the variables we are testing substitutions for, for all types,
- * nsamples : number of sample points this class will test for all types.
- */
- CandidateRewriteDatabaseGen(std::vector<Node>& vars, unsigned nsamples);
- /** add term
- *
- * This registers term n with this class. We generate the candidate rewrite
- * database of the appropriate type (if not allocated already), and register
- * n with this database. This may result in "candidate-rewrite" being
- * printed on the output stream out. We return true if the term sol is
- * distinct (up to equivalence) with all previous terms added to this class.
- */
- bool addTerm(Node n, std::ostream& out);
-
- private:
- /** reference to quantifier engine */
- QuantifiersEngine* d_qe;
- /** the variables */
- std::vector<Node> d_vars;
- /** sygus sampler object for each type */
- std::map<TypeNode, SygusSampler> d_sampler;
- /** the number of samples */
- unsigned d_nsamples;
- /** candidate rewrite databases for each type */
- std::map<TypeNode, CandidateRewriteDatabase> d_cdbs;
- /** an extended rewriter object */
- ExtendedRewriter d_ext_rewrite;
-};
-
} /* CVC4::theory::quantifiers namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
if (ret.getKind() == EQUAL)
{
- new_ret = strings::SequencesRewriter::rewriteEqualityExt(ret);
+ new_ret = strings::SequencesRewriter(nullptr).rewriteEqualityExt(ret);
}
return new_ret;
TheoryQuantifiers::~TheoryQuantifiers() {
}
-std::unique_ptr<TheoryRewriter> TheoryQuantifiers::mkTheoryRewriter()
-{
- return std::unique_ptr<TheoryRewriter>(new QuantifiersRewriter());
-}
-
void TheoryQuantifiers::finishInit()
{
// quantifiers are not evaluated in getModelValue
#include "context/context.h"
#include "expr/node.h"
#include "theory/output_channel.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/theory.h"
#include "theory/theory_engine.h"
#include "theory/valuation.h"
const LogicInfo& logicInfo);
~TheoryQuantifiers();
- std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+ TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
/** finish initialization */
void finishInit() override;
std::vector<Node> node_values,
std::string str_value) override;
+ private:
+ /** The theory rewriter for this theory. */
+ QuantifiersRewriter d_rewriter;
};/* class TheoryQuantifiers */
}/* CVC4::theory::quantifiers namespace */
#include "theory/rewriter.h"
#include "options/theory_options.h"
+#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "smt/smt_statistics_registry.h"
#include "theory/rewriter_tables.h"
// eagerly for the sake of efficiency here.
return node;
}
- return getInstance().rewriteTo(theoryOf(node), node);
+ return getInstance()->rewriteTo(theoryOf(node), node);
}
void Rewriter::registerTheoryRewriter(theory::TheoryId tid,
- std::unique_ptr<TheoryRewriter> trew)
+ TheoryRewriter* trew)
{
- getInstance().d_theoryRewriters[tid] = std::move(trew);
+ getInstance()->d_theoryRewriters[tid] = trew;
}
void Rewriter::registerPreRewrite(
d_postRewritersEqual[tid] = fn;
}
-Rewriter& Rewriter::getInstance()
+Rewriter* Rewriter::getInstance()
{
- thread_local static Rewriter rewriter;
- return rewriter;
+ return smt::currentSmtEngine()->getRewriter();
}
Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
}
void Rewriter::clearCaches() {
- Rewriter& rewriter = getInstance();
+ Rewriter* rewriter = getInstance();
#ifdef CVC4_ASSERTIONS
- rewriter.d_rewriteStack.reset(nullptr);
+ rewriter->d_rewriteStack.reset(nullptr);
#endif
- rewriter.clearCachesInternal();
+ rewriter->clearCachesInternal();
}
}/* CVC4::theory namespace */
static void clearCaches();
/**
- * Registers a theory rewriter with this rewriter. This transfers the
- * ownership of the theory rewriter to the rewriter.
+ * Registers a theory rewriter with this rewriter. The rewriter does not own
+ * the theory rewriters.
*
* @param tid The theory that the theory rewriter should be associated with.
* @param trew The theory rewriter to register.
*/
static void registerTheoryRewriter(theory::TheoryId tid,
- std::unique_ptr<TheoryRewriter> trew);
+ TheoryRewriter* trew);
/**
* Register a prerewrite for a given kind.
private:
/**
- * Get the (singleton) instance of the rewriter.
+ * Get the rewriter associated with the SmtEngine in scope.
*
- * TODO(#3468): Get rid of this singleton
+ * TODO(#3468): Get rid of this function (it relies on there being an
+ * singleton with the current SmtEngine in scope)
*/
- static Rewriter& getInstance();
+ static Rewriter* getInstance();
/** Returns the appropriate cache for a node */
Node getPreRewriteCache(theory::TheoryId theoryId, TNode node);
void clearCachesInternal();
- /** Theory rewriters managed by this rewriter instance */
- std::unique_ptr<TheoryRewriter> d_theoryRewriters[theory::THEORY_LAST];
+ /** Theory rewriters used by this rewriter instance */
+ TheoryRewriter* d_theoryRewriters[theory::THEORY_LAST];
unsigned long d_iterationCount = 0;
}
}
-std::unique_ptr<TheoryRewriter> TheorySep::mkTheoryRewriter()
-{
- return std::unique_ptr<TheoryRewriter>(new TheorySepRewriter());
-}
-
void TheorySep::setMasterEqualityEngine(eq::EqualityEngine* eq) {
d_equalityEngine.setMasterEqualityEngine(eq);
}
#include "context/cdhashset.h"
#include "context/cdlist.h"
#include "context/cdqueue.h"
+#include "theory/sep/theory_sep_rewriter.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
#include "util/statistics_registry.h"
//whether bounds have been initialized
bool d_bounds_init;
+ TheorySepRewriter d_rewriter;
+
Node mkAnd( std::vector< TNode >& assumptions );
int processAssertion( Node n, std::map< int, std::map< Node, int > >& visited,
TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
~TheorySep();
- std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+ TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
// Do not move me to the header. See explanation in the constructor.
}
-std::unique_ptr<TheoryRewriter> TheorySets::mkTheoryRewriter()
+TheoryRewriter* TheorySets::getTheoryRewriter()
{
- return std::unique_ptr<TheoryRewriter>(new TheorySetsRewriter());
+ return d_internal->getTheoryRewriter();
}
void TheorySets::finishInit()
const LogicInfo& logicInfo);
~TheorySets() override;
- std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+ TheoryRewriter* getTheoryRewriter() override;
/** finish initialization */
void finishInit() override;
#include "theory/sets/inference_manager.h"
#include "theory/sets/solver_state.h"
#include "theory/sets/theory_sets_rels.h"
+#include "theory/sets/theory_sets_rewriter.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
~TheorySetsPrivate();
+ TheoryRewriter* getTheoryRewriter() { return &d_rewriter; }
+
void setMasterEqualityEngine(eq::EqualityEngine* eq);
void addSharedTerm(TNode);
* involving cardinality constraints is asserted to this theory.
*/
bool d_card_enabled;
+
+ /** The theory rewriter for this theory. */
+ TheorySetsRewriter d_rewriter;
};/* class TheorySetsPrivate */
return a.getConst<Rational>().sgn() >= (strict ? 1 : 0);
}
- Node ar =
- strict
- ? NodeManager::currentNM()->mkNode(
+ Node ar = strict ? NodeManager::currentNM()->mkNode(
kind::MINUS, a, NodeManager::currentNM()->mkConst(Rational(1)))
- : a;
+ : a;
ar = Rewriter::rewrite(ar);
if (ar.getAttribute(StrCheckEntailArithComputedAttr()))
SolverState& s,
InferenceManager& im,
SkolemCache& skc,
+ StringsRewriter& rewriter,
BaseSolver& bs,
CoreSolver& cs,
ExtTheory* et,
- SequencesStatistics& stats)
+ SequencesStatistics& statistics)
: d_state(s),
d_im(im),
d_skCache(skc),
+ d_rewriter(rewriter),
d_bsolver(bs),
d_csolver(cs),
d_extt(et),
- d_statistics(stats),
- d_preproc(&skc, u, stats),
+ d_statistics(statistics),
+ d_preproc(&skc, u, statistics),
d_hasExtf(c, false),
d_extfInferCache(c)
{
if (inferEqr.getKind() == EQUAL)
{
// try to use the extended rewriter for equalities
- inferEqrr = SequencesRewriter::rewriteEqualityExt(inferEqr);
+ inferEqrr = d_rewriter.rewriteEqualityExt(inferEqr);
}
if (inferEqrr != inferEqr)
{
#ifndef CVC4__THEORY__STRINGS__EXTF_SOLVER_H
#define CVC4__THEORY__STRINGS__EXTF_SOLVER_H
-#include <vector>
#include <map>
+#include <vector>
#include "context/cdo.h"
#include "expr/node.h"
#include "theory/strings/sequences_stats.h"
#include "theory/strings/skolem_cache.h"
#include "theory/strings/solver_state.h"
+#include "theory/strings/strings_rewriter.h"
#include "theory/strings/theory_strings_preprocess.h"
namespace CVC4 {
SolverState& s,
InferenceManager& im,
SkolemCache& skc,
+ StringsRewriter& rewriter,
BaseSolver& bs,
CoreSolver& cs,
ExtTheory* et,
- SequencesStatistics& stats);
+ SequencesStatistics& statistics);
~ExtfSolver();
/** check extended functions evaluation
InferenceManager& d_im;
/** cache of all skolems */
SkolemCache& d_skCache;
+ /** The theory rewriter for this theory. */
+ StringsRewriter& d_rewriter;
/** reference to the base solver, used for certain queries */
BaseSolver& d_bsolver;
/** reference to the core solver, used for certain queries */
return true;
}
}
- case REGEXP_EMPTY: { return false;
+ case REGEXP_EMPTY:
+ {
+ return false;
}
case REGEXP_SIGMA:
{
#include "theory/rewriter.h"
#include "theory/strings/arith_entail.h"
#include "theory/strings/regexp_entail.h"
-#include "theory/strings/strings_entail.h"
#include "theory/strings/strings_rewriter.h"
#include "theory/strings/theory_strings_utils.h"
#include "theory/strings/word.h"
namespace theory {
namespace strings {
+SequencesRewriter::SequencesRewriter(HistogramStat<Rewrite>* statistics)
+ : d_statistics(statistics), d_stringsEntail(*this)
+{
+}
+
Node SequencesRewriter::rewriteEquality(Node node)
{
Assert(node.getKind() == kind::EQUAL);
// must call rewrite contains directly to avoid infinite loop
// we do a fix point since we may rewrite contains terms to simpler
// contains terms.
- Node ctn = StringsEntail::checkContains(node[r], node[1 - r], false);
+ Node ctn = d_stringsEntail.checkContains(node[r], node[1 - r], false);
if (!ctn.isNull())
{
if (!ctn.getConst<bool>())
// e.g. this ensures we rewrite (a)* ++ (_)* ---> (_)*
while (!cvec.empty() && RegExpEntail::isConstRegExp(cvec.back())
&& RegExpEntail::testConstStringInRegExp(
- emptyStr, 0, cvec.back()))
+ emptyStr, 0, cvec.back()))
{
cvec.pop_back();
}
RewriteResponse SequencesRewriter::postRewrite(TNode node)
{
- Trace("strings-postrewrite")
- << "Strings::postRewrite start " << node << std::endl;
+ Trace("sequences-postrewrite")
+ << "Strings::SequencesRewriter::postRewrite start " << node << std::endl;
Node retNode = node;
Kind nk = node.getKind();
if (nk == kind::STRING_CONCAT)
{
retNode = rewriteContains(node);
}
- else if (nk == kind::STRING_LT)
- {
- retNode = StringsRewriter::rewriteStringLt(node);
- }
- else if (nk == kind::STRING_LEQ)
- {
- retNode = StringsRewriter::rewriteStringLeq(node);
- }
else if (nk == kind::STRING_STRIDOF)
{
retNode = rewriteIndexof(node);
{
retNode = rewriteReplaceAll(node);
}
- else if (nk == STRING_TOLOWER || nk == STRING_TOUPPER)
- {
- retNode = StringsRewriter::rewriteStrConvert(node);
- }
else if (nk == STRING_REV)
{
retNode = rewriteStrReverse(node);
{
retNode = rewritePrefixSuffix(node);
}
- else if (nk == STRING_IS_DIGIT)
- {
- retNode = StringsRewriter::rewriteStringIsDigit(node);
- }
- else if (nk == kind::STRING_ITOS)
- {
- retNode = StringsRewriter::rewriteIntToStr(node);
- }
- else if (nk == kind::STRING_STOI)
- {
- retNode = StringsRewriter::rewriteStrToInt(node);
- }
else if (nk == kind::STRING_IN_REGEXP)
{
retNode = rewriteMembership(node);
}
- else if (nk == STRING_TO_CODE)
- {
- retNode = StringsRewriter::rewriteStringToCode(node);
- }
- else if (nk == STRING_FROM_CODE)
- {
- retNode = StringsRewriter::rewriteStringFromCode(node);
- }
else if (nk == REGEXP_CONCAT)
{
retNode = rewriteConcatRegExp(node);
retNode = rewriteRepeatRegExp(node);
}
- Trace("strings-postrewrite")
- << "Strings::postRewrite returning " << retNode << std::endl;
+ Trace("sequences-postrewrite")
+ << "Strings::SequencesRewriter::postRewrite returning " << retNode
+ << std::endl;
if (node != retNode)
{
- Trace("strings-rewrite-debug")
- << "Strings: post-rewrite " << node << " to " << retNode << std::endl;
+ Trace("strings-rewrite-debug") << "Strings::SequencesRewriter::postRewrite "
+ << node << " to " << retNode << std::endl;
return RewriteResponse(REWRITE_AGAIN_FULL, retNode);
}
return RewriteResponse(REWRITE_DONE, retNode);
}
else if (node[0].getKind() == STRING_STRREPL)
{
- Node rplDomain = StringsEntail::checkContains(node[0][1], node[1]);
+ Node rplDomain = d_stringsEntail.checkContains(node[0][1], node[1]);
if (!rplDomain.isNull() && !rplDomain.getConst<bool>())
{
Node d1 = nm->mkNode(STRING_STRCTN, node[0][0], node[1]);
// component-wise containment
std::vector<Node> nc1rb;
std::vector<Node> nc1re;
- if (StringsEntail::componentContains(nc1, nc2, nc1rb, nc1re) != -1)
+ if (d_stringsEntail.componentContains(nc1, nc2, nc1rb, nc1re) != -1)
{
Node ret = NodeManager::currentNM()->mkConst(true);
return returnRewrite(node, ret, Rewrite::CTN_COMPONENT);
// replacement does not change y. (str.contains x w) checks that if the
// replacement changes anything in y, the w makes it impossible for it to
// occur in x.
- Node ctnConst = StringsEntail::checkContains(node[0], n[0]);
+ Node ctnConst = d_stringsEntail.checkContains(node[0], n[0]);
if (!ctnConst.isNull() && !ctnConst.getConst<bool>())
{
- Node ctnConst2 = StringsEntail::checkContains(node[0], n[2]);
+ Node ctnConst2 = d_stringsEntail.checkContains(node[0], n[2]);
if (!ctnConst2.isNull() && !ctnConst2.getConst<bool>())
{
Node res = nm->mkConst(false);
// if (str.contains z w) ---> false and (str.len w) = 1
if (StringsEntail::checkLengthOne(node[1]))
{
- Node ctn = StringsEntail::checkContains(node[1], node[0][2]);
+ Node ctn = d_stringsEntail.checkContains(node[1], node[0][2]);
if (!ctn.isNull() && !ctn.getConst<bool>())
{
Node empty = nm->mkConst(String(""));
fstr = Rewriter::rewrite(fstr);
}
- Node cmp_conr = StringsEntail::checkContains(fstr, node[1]);
+ Node cmp_conr = d_stringsEntail.checkContains(fstr, node[1]);
Trace("strings-rewrite-debug") << "For " << node << ", check contains("
<< fstr << ", " << node[1] << ")" << std::endl;
Trace("strings-rewrite-debug") << "...got " << cmp_conr << std::endl;
// past the first position in node[0] that contains node[1], we can drop
std::vector<Node> nb;
std::vector<Node> ne;
- int cc = StringsEntail::componentContains(
+ int cc = d_stringsEntail.componentContains(
children0, children1, nb, ne, true, 1);
if (cc != -1 && !ne.empty())
{
// check if contains definitely does (or does not) hold
Node cmp_con = nm->mkNode(kind::STRING_STRCTN, node[0], node[1]);
Node cmp_conr = Rewriter::rewrite(cmp_con);
- if (!StringsEntail::checkContains(node[0], node[1]).isNull())
+ if (!d_stringsEntail.checkContains(node[0], node[1]).isNull())
{
if (cmp_conr.getConst<bool>())
{
// component-wise containment
std::vector<Node> cb;
std::vector<Node> ce;
- int cc = StringsEntail::componentContains(
+ int cc = d_stringsEntail.componentContains(
children0, children1, cb, ce, true, 1);
if (cc != -1)
{
return returnRewrite(node, node[0], Rewrite::REPL_REPL2_INV_ID);
}
bool dualReplIteSuccess = false;
- Node cmp_con2 = StringsEntail::checkContains(node[1][0], node[1][2]);
+ Node cmp_con2 = d_stringsEntail.checkContains(node[1][0], node[1][2]);
if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>())
{
// str.contains( x, z ) ---> false
// implies
// str.replace( x, str.replace( x, y, z ), w ) --->
// ite( str.contains( x, y ), x, w )
- cmp_con2 = StringsEntail::checkContains(node[1][1], node[1][2]);
+ cmp_con2 = d_stringsEntail.checkContains(node[1][1], node[1][2]);
if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>())
{
- cmp_con2 = StringsEntail::checkContains(node[1][2], node[1][1]);
+ cmp_con2 = d_stringsEntail.checkContains(node[1][2], node[1][1]);
if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>())
{
dualReplIteSuccess = true;
// str.contains(y, z) ----> false and ( y == w or x == w ) implies
// implies
// str.replace(x, str.replace(y, x, z), w) ---> str.replace(x, y, w)
- Node cmp_con2 = StringsEntail::checkContains(node[1][0], node[1][2]);
+ Node cmp_con2 = d_stringsEntail.checkContains(node[1][0], node[1][2]);
invSuccess = !cmp_con2.isNull() && !cmp_con2.getConst<bool>();
}
}
// str.contains(x, z) ----> false and str.contains(x, w) ----> false
// implies
// str.replace(x, str.replace(y, z, w), u) ---> str.replace(x, y, u)
- Node cmp_con2 = StringsEntail::checkContains(node[0], node[1][1]);
+ Node cmp_con2 = d_stringsEntail.checkContains(node[0], node[1][1]);
if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>())
{
- cmp_con2 = StringsEntail::checkContains(node[0], node[1][2]);
+ cmp_con2 = d_stringsEntail.checkContains(node[0], node[1][2]);
invSuccess = !cmp_con2.isNull() && !cmp_con2.getConst<bool>();
}
}
{
// str.contains( z, w ) ----> false implies
// str.replace( x, w, str.replace( z, x, y ) ) ---> str.replace( x, w, z )
- Node cmp_con2 = StringsEntail::checkContains(node[1], node[2][0]);
+ Node cmp_con2 = d_stringsEntail.checkContains(node[1], node[2][0]);
if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>())
{
Node res =
{
// str.contains( x, z ) ----> false implies
// str.replace( x, y, str.replace( y, z, w ) ) ---> x
- cmp_con = StringsEntail::checkContains(node[0], node[2][1]);
+ cmp_con = d_stringsEntail.checkContains(node[0], node[2][1]);
success = !cmp_con.isNull() && !cmp_con.getConst<bool>();
}
if (success)
checkLhs.end(), children0.begin(), children0.begin() + checkIndex);
Node lhs = utils::mkConcat(checkLhs, stype);
Node rhs = children0[checkIndex];
- Node ctn = StringsEntail::checkContains(lhs, rhs);
+ Node ctn = d_stringsEntail.checkContains(lhs, rhs);
if (!ctn.isNull() && ctn.getConst<bool>())
{
lastLhs = lhs;
NodeManager* nm = NodeManager::currentNM();
+ if (d_statistics != nullptr)
+ {
+ (*d_statistics) << r;
+ }
+
// standard post-processing
// We rewrite (string) equalities immediately here. This allows us to forego
// the standard invariant on equality rewrites (that s=t must rewrite to one
#include "expr/node.h"
#include "theory/strings/rewrites.h"
+#include "theory/strings/sequences_stats.h"
+#include "theory/strings/strings_entail.h"
#include "theory/theory_rewriter.h"
namespace CVC4 {
class SequencesRewriter : public TheoryRewriter
{
+ public:
+ SequencesRewriter(HistogramStat<Rewrite>* statistics);
+
protected:
/** rewrite regular expression concatenation
*
* This is the entry point for post-rewriting applications of re.++.
* Returns the rewritten form of node.
*/
- static Node rewriteConcatRegExp(TNode node);
+ Node rewriteConcatRegExp(TNode node);
/** rewrite regular expression star
*
* This is the entry point for post-rewriting applications of re.*.
* Returns the rewritten form of node.
*/
- static Node rewriteStarRegExp(TNode node);
+ Node rewriteStarRegExp(TNode node);
/** rewrite regular expression intersection/union
*
* This is the entry point for post-rewriting applications of re.inter and
* re.union. Returns the rewritten form of node.
*/
- static Node rewriteAndOrRegExp(TNode node);
+ Node rewriteAndOrRegExp(TNode node);
/** rewrite regular expression loop
*
* This is the entry point for post-rewriting applications of re.loop.
* Returns the rewritten form of node.
*/
- static Node rewriteLoopRegExp(TNode node);
+ Node rewriteLoopRegExp(TNode node);
/** rewrite regular expression repeat
*
* This is the entry point for post-rewriting applications of re.repeat.
* Returns the rewritten form of node.
*/
- static Node rewriteRepeatRegExp(TNode node);
+ Node rewriteRepeatRegExp(TNode node);
/** rewrite regular expression option
*
* This is the entry point for post-rewriting applications of re.opt.
* Returns the rewritten form of node.
*/
- static Node rewriteOptionRegExp(TNode node);
+ Node rewriteOptionRegExp(TNode node);
/** rewrite regular expression plus
*
* This is the entry point for post-rewriting applications of re.+.
* Returns the rewritten form of node.
*/
- static Node rewritePlusRegExp(TNode node);
+ Node rewritePlusRegExp(TNode node);
/** rewrite regular expression difference
*
* This is the entry point for post-rewriting applications of re.diff.
* Returns the rewritten form of node.
*/
- static Node rewriteDifferenceRegExp(TNode node);
+ Node rewriteDifferenceRegExp(TNode node);
/** rewrite regular expression range
*
* This is the entry point for post-rewriting applications of re.range.
* Returns the rewritten form of node.
*/
- static Node rewriteRangeRegExp(TNode node);
+ Node rewriteRangeRegExp(TNode node);
/** rewrite regular expression membership
*
* This is the entry point for post-rewriting applications of str.in.re
* Returns the rewritten form of node.
*/
- static Node rewriteMembership(TNode node);
+ Node rewriteMembership(TNode node);
/** rewrite string equality extended
*
* This method returns a formula that is equivalent to the equality between
* two strings s = t, given by node. It is called by rewriteEqualityExt.
*/
- static Node rewriteStrEqualityExt(Node node);
+ Node rewriteStrEqualityExt(Node node);
/** rewrite arithmetic equality extended
*
* This method returns a formula that is equivalent to the equality between
* two arithmetic string terms s = t, given by node. t is called by
* rewriteEqualityExt.
*/
- static Node rewriteArithEqualityExt(Node node);
+ Node rewriteArithEqualityExt(Node node);
/**
* Called when node rewrites to ret.
*
* additional rewrites on ret, after which we return the result of this call.
* Otherwise, this method simply returns ret.
*/
- static Node returnRewrite(Node node, Node ret, Rewrite r);
+ Node returnRewrite(Node node, Node ret, Rewrite r);
public:
RewriteResponse postRewrite(TNode node) override;
* two strings s = t, given by node. The result of rewrite is one of
* { s = t, t = s, true, false }.
*/
- static Node rewriteEquality(Node node);
+ Node rewriteEquality(Node node);
/** rewrite equality extended
*
* This method returns a formula that is equivalent to the equality between
* Specifically, this function performs rewrites whose conclusion is not
* necessarily one of { s = t, t = s, true, false }.
*/
- static Node rewriteEqualityExt(Node node);
+ Node rewriteEqualityExt(Node node);
/** rewrite string length
* This is the entry point for post-rewriting terms node of the form
* str.len( t )
* Returns the rewritten form of node.
*/
- static Node rewriteLength(Node node);
+ Node rewriteLength(Node node);
/** rewrite concat
* This is the entry point for post-rewriting terms node of the form
* str.++( t1, .., tn )
* Returns the rewritten form of node.
*/
- static Node rewriteConcat(Node node);
+ Node rewriteConcat(Node node);
/** rewrite character at
* This is the entry point for post-rewriting terms node of the form
* str.charat( s, i1 )
* Returns the rewritten form of node.
*/
- static Node rewriteCharAt(Node node);
+ Node rewriteCharAt(Node node);
/** rewrite substr
* This is the entry point for post-rewriting terms node of the form
* str.substr( s, i1, i2 )
* Returns the rewritten form of node.
*/
- static Node rewriteSubstr(Node node);
+ Node rewriteSubstr(Node node);
/** rewrite contains
* This is the entry point for post-rewriting terms node of the form
* str.contains( t, s )
* 7 of Reynolds et al "Scaling Up DPLL(T) String Solvers Using
* Context-Dependent Rewriting", CAV 2017.
*/
- static Node rewriteContains(Node node);
+ Node rewriteContains(Node node);
/** rewrite indexof
* This is the entry point for post-rewriting terms n of the form
* str.indexof( s, t, n )
* Returns the rewritten form of node.
*/
- static Node rewriteIndexof(Node node);
+ Node rewriteIndexof(Node node);
/** rewrite replace
* This is the entry point for post-rewriting terms n of the form
* str.replace( s, t, r )
* Returns the rewritten form of node.
*/
- static Node rewriteReplace(Node node);
+ Node rewriteReplace(Node node);
/** rewrite replace all
* This is the entry point for post-rewriting terms n of the form
* str.replaceall( s, t, r )
* Returns the rewritten form of node.
*/
- static Node rewriteReplaceAll(Node node);
+ Node rewriteReplaceAll(Node node);
/** rewrite replace internal
*
* This method implements rewrite rules that apply to both str.replace and
* str.replaceall. If it returns a non-null ret, then node rewrites to ret.
*/
- static Node rewriteReplaceInternal(Node node);
+ Node rewriteReplaceInternal(Node node);
/** rewrite string reverse
*
* This is the entry point for post-rewriting terms n of the form
* str.rev( s )
* Returns the rewritten form of node.
*/
- static Node rewriteStrReverse(Node node);
+ Node rewriteStrReverse(Node node);
/** rewrite prefix/suffix
* This is the entry point for post-rewriting terms n of the form
* str.prefixof( s, t ) / str.suffixof( s, t )
* Returns the rewritten form of node.
*/
- static Node rewritePrefixSuffix(Node node);
+ Node rewritePrefixSuffix(Node node);
/** rewrite str.to_code
* This is the entry point for post-rewriting terms n of the form
* str.to_code( t )
* Returns the rewritten form of node.
*/
- static Node rewriteStringToCode(Node node);
+ Node rewriteStringToCode(Node node);
/** length preserving rewrite
*
* string exists.
*/
static Node canonicalStrForSymbolicLength(Node n, TypeNode stype);
+
+ /** Reference to the rewriter statistics. */
+ HistogramStat<Rewrite>* d_statistics;
+
+ /** Instance of the entailment checker for strings. */
+ StringsEntail d_stringsEntail;
}; /* class SequencesRewriter */
} // namespace strings
d_reductions("theory::strings::reductions"),
d_regexpUnfoldingsPos("theory::strings::regexpUnfoldingsPos"),
d_regexpUnfoldingsNeg("theory::strings::regexpUnfoldingsNeg"),
+ d_rewrites("theory::strings::rewrites"),
d_conflictsEqEngine("theory::strings::conflictsEqEngine", 0),
d_conflictsEagerPrefix("theory::strings::conflictsEagerPrefix", 0),
d_conflictsInfer("theory::strings::conflictsInfer", 0),
smtStatisticsRegistry()->registerStat(&d_reductions);
smtStatisticsRegistry()->registerStat(&d_regexpUnfoldingsPos);
smtStatisticsRegistry()->registerStat(&d_regexpUnfoldingsNeg);
+ smtStatisticsRegistry()->registerStat(&d_rewrites);
smtStatisticsRegistry()->registerStat(&d_conflictsEqEngine);
smtStatisticsRegistry()->registerStat(&d_conflictsEagerPrefix);
smtStatisticsRegistry()->registerStat(&d_conflictsInfer);
smtStatisticsRegistry()->unregisterStat(&d_reductions);
smtStatisticsRegistry()->unregisterStat(&d_regexpUnfoldingsPos);
smtStatisticsRegistry()->unregisterStat(&d_regexpUnfoldingsNeg);
+ smtStatisticsRegistry()->unregisterStat(&d_rewrites);
smtStatisticsRegistry()->unregisterStat(&d_conflictsEqEngine);
smtStatisticsRegistry()->unregisterStat(&d_conflictsEagerPrefix);
smtStatisticsRegistry()->unregisterStat(&d_conflictsInfer);
#include "expr/kind.h"
#include "theory/strings/infer_info.h"
+#include "theory/strings/rewrites.h"
#include "util/statistics_registry.h"
namespace CVC4 {
HistogramStat<Kind> d_regexpUnfoldingsPos;
HistogramStat<Kind> d_regexpUnfoldingsNeg;
//--------------- end of inferences
+ /** Counts the number of applications of each type of rewrite rule */
+ HistogramStat<Rewrite> d_rewrites;
//--------------- conflicts, partition of calls to OutputChannel::conflict
/** Number of equality engine conflicts */
IntStat d_conflictsEqEngine;
namespace theory {
namespace strings {
+StringsEntail::StringsEntail(SequencesRewriter& rewriter) : d_rewriter(rewriter)
+{
+}
+
bool StringsEntail::canConstantContainConcat(Node c,
Node n,
int& firstc,
{
// (str.contains (str.replace x y z) w) ---> true
// if (str.contains x w) --> true and (str.contains z w) ---> true
- Node xCtnW = StringsEntail::checkContains(n1[0], n2);
+ Node xCtnW = checkContains(n1[0], n2);
if (!xCtnW.isNull() && xCtnW.getConst<bool>())
{
- Node zCtnW = StringsEntail::checkContains(n1[2], n2);
+ Node zCtnW = checkContains(n1[2], n2);
if (!zCtnW.isNull() && zCtnW.getConst<bool>())
{
return true;
do
{
prev = ctn;
- ctn = SequencesRewriter::rewriteContains(ctn);
+ ctn = d_rewriter.rewriteContains(ctn);
} while (prev != ctn && ctn.getKind() == STRING_STRCTN);
}
namespace theory {
namespace strings {
+class SequencesRewriter;
+
/**
* Entailment tests involving strings.
* Some of these techniques are described in Reynolds et al, "High Level
class StringsEntail
{
public:
+ StringsEntail(SequencesRewriter& rewriter);
+
/** can constant contain list
* return true if constant c can contain the list l in order
* firstc/lastc store which indices in l were used to determine the return
* n1 is updated to { "c", x, "def" },
* nb is updated to { y, "ab" }
*/
- static int componentContains(std::vector<Node>& n1,
- std::vector<Node>& n2,
- std::vector<Node>& nb,
- std::vector<Node>& ne,
- bool computeRemainder = false,
- int remainderDir = 0);
+ int componentContains(std::vector<Node>& n1,
+ std::vector<Node>& n2,
+ std::vector<Node>& nb,
+ std::vector<Node>& ne,
+ bool computeRemainder = false,
+ int remainderDir = 0);
/** strip constant endpoints
* This function is used when rewriting str.contains( t1, t2 ), where
* n1 is the vector form of t1
* @return true node if it can be shown that `a` contains `b`, false node if
* it can be shown that `a` does not contain `b`, null node otherwise
*/
- static Node checkContains(Node a, Node b, bool fullRewriter = true);
+ Node checkContains(Node a, Node b, bool fullRewriter = true);
/** entail non-empty
*
* Since we do not wish to introduce ITE terms in the rewriter, we instead
* return false, indicating that we cannot compute the remainder.
*/
- static bool componentContainsBase(
+ bool componentContainsBase(
Node n1, Node n2, Node& n1rb, Node& n1re, int dir, bool computeRemainder);
/**
* Simplifies a given node `a` s.t. the result is a concatenation of string
* @return A concatenation that can be interpreted as a multiset
*/
static Node getMultisetApproximation(Node a);
+
+ private:
+ /**
+ * Reference to the sequences rewriter that owns this `StringsEntail`
+ * instance.
+ */
+ SequencesRewriter& d_rewriter;
};
} // namespace strings
namespace theory {
namespace strings {
+StringsRewriter::StringsRewriter(HistogramStat<Rewrite>* statistics)
+ : SequencesRewriter(statistics)
+{
+}
+
+RewriteResponse StringsRewriter::postRewrite(TNode node)
+{
+ Trace("strings-postrewrite")
+ << "Strings::StringsRewriter::postRewrite start " << node << std::endl;
+
+ Node retNode = node;
+ Kind nk = node.getKind();
+ if (nk == kind::STRING_LT)
+ {
+ retNode = rewriteStringLt(node);
+ }
+ else if (nk == kind::STRING_LEQ)
+ {
+ retNode = rewriteStringLeq(node);
+ }
+ else if (nk == STRING_TOLOWER || nk == STRING_TOUPPER)
+ {
+ retNode = rewriteStrConvert(node);
+ }
+ else if (nk == STRING_IS_DIGIT)
+ {
+ retNode = rewriteStringIsDigit(node);
+ }
+ else if (nk == kind::STRING_ITOS)
+ {
+ retNode = rewriteIntToStr(node);
+ }
+ else if (nk == kind::STRING_STOI)
+ {
+ retNode = rewriteStrToInt(node);
+ }
+ else if (nk == STRING_TO_CODE)
+ {
+ retNode = rewriteStringToCode(node);
+ }
+ else if (nk == STRING_FROM_CODE)
+ {
+ retNode = rewriteStringFromCode(node);
+ }
+ else
+ {
+ return SequencesRewriter::postRewrite(node);
+ }
+
+ Trace("strings-postrewrite")
+ << "Strings::StringsRewriter::postRewrite returning " << retNode
+ << std::endl;
+ if (node != retNode)
+ {
+ Trace("strings-rewrite-debug") << "Strings::StringsRewriter::postRewrite "
+ << node << " to " << retNode << std::endl;
+ return RewriteResponse(REWRITE_AGAIN_FULL, retNode);
+ }
+ return RewriteResponse(REWRITE_DONE, retNode);
+}
+
Node StringsRewriter::rewriteStrToInt(Node node)
{
Assert(node.getKind() == STRING_STOI);
class StringsRewriter : public SequencesRewriter
{
public:
+ StringsRewriter(HistogramStat<Rewrite>* statistics);
+
+ RewriteResponse postRewrite(TNode node) override;
+
/** rewrite string to integer
*
* This is the entry point for post-rewriting terms n of the form
* str.to_int( s )
* Returns the rewritten form of n.
*/
- static Node rewriteStrToInt(Node n);
+ Node rewriteStrToInt(Node n);
/** rewrite integer to string
*
* str.from_int( i )
* Returns the rewritten form of n.
*/
- static Node rewriteIntToStr(Node n);
+ Node rewriteIntToStr(Node n);
/** rewrite string convert
*
* str.tolower( s ) and str.toupper( s )
* Returns the rewritten form of n.
*/
- static Node rewriteStrConvert(Node n);
+ Node rewriteStrConvert(Node n);
/** rewrite string less than
*
* str.<( t, s )
* Returns the rewritten form of n.
*/
- static Node rewriteStringLt(Node n);
+ Node rewriteStringLt(Node n);
/** rewrite string less than or equal
*
* str.<=( t, s )
* Returns the rewritten form of n.
*/
- static Node rewriteStringLeq(Node n);
+ Node rewriteStringLeq(Node n);
/** rewrite str.from_code
*
* str.from_code( t )
* Returns the rewritten form of n.
*/
- static Node rewriteStringFromCode(Node n);
+ Node rewriteStringFromCode(Node n);
/** rewrite str.to_code
*
* str.to_code( t )
* Returns the rewritten form of n.
*/
- static Node rewriteStringToCode(Node n);
+ Node rewriteStringToCode(Node n);
/** rewrite is digit
*
* str.is_digit( t )
* Returns the rewritten form of n.
*/
- static Node rewriteStringIsDigit(Node n);
+ Node rewriteStringIsDigit(Node n);
};
} // namespace strings
#include "smt/smt_statistics_registry.h"
#include "theory/ext_theory.h"
#include "theory/rewriter.h"
-#include "theory/strings/sequences_rewriter.h"
#include "theory/strings/theory_strings_utils.h"
#include "theory/strings/type_enumerator.h"
#include "theory/strings/word.h"
const LogicInfo& logicInfo)
: Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
d_notify(*this),
+ d_statistics(),
d_equalityEngine(d_notify, c, "theory::strings::ee", true),
d_state(c, d_equalityEngine, d_valuation),
d_im(*this, c, u, d_state, d_sk_cache, out, d_statistics),
d_registered_terms_cache(u),
d_functionsTerms(c),
d_has_str_code(false),
+ d_rewriter(&d_statistics.d_rewrites),
d_bsolver(c, u, d_state, d_im),
d_csolver(c, u, d_state, d_im, d_sk_cache, d_bsolver),
d_esolver(nullptr),
d_state,
d_im,
d_sk_cache,
+ d_rewriter,
d_bsolver,
d_csolver,
extt,
}
-std::unique_ptr<TheoryRewriter> TheoryStrings::mkTheoryRewriter()
-{
- return std::unique_ptr<TheoryRewriter>(new SequencesRewriter());
-}
-
bool TheoryStrings::areCareDisequal( TNode x, TNode y ) {
Assert(d_equalityEngine.hasTerm(x));
Assert(d_equalityEngine.hasTerm(y));
#include "theory/strings/skolem_cache.h"
#include "theory/strings/solver_state.h"
#include "theory/strings/strings_fmf.h"
+#include "theory/strings/strings_rewriter.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
const LogicInfo& logicInfo);
~TheoryStrings();
- std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+ TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
// Symbolic Regular Expression
private:
+ /** The theory rewriter for this theory. */
+ StringsRewriter d_rewriter;
+
/**
* The base solver, responsible for reasoning about congruent terms and
* inferring constants for equivalence classes.
Node sk2 = ArithEntail::check(t12, lt0)
? emp
: d_sc->mkSkolemCached(
- s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr");
+ s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr");
Node b11 = s.eqNode(nm->mkNode(STRING_CONCAT, sk1, skt, sk2));
//length of first skolem is second argument
Node b12 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n);
#include "theory/ext_theory.h"
#include "theory/quantifiers_engine.h"
#include "theory/substitutions.h"
+#include "theory/theory_rewriter.h"
using namespace std;
class TheoryModel;
class SubstitutionMap;
class ExtTheory;
+class TheoryRewriter;
class EntailmentCheckParameters;
class EntailmentCheckSideEffects;
* all calls to them.)
*/
class Theory {
-
-private:
-
+ private:
friend class ::CVC4::TheoryEngine;
// Disallow default construction, copy, assignment.
protected:
-
// === STATISTICS ===
/** time spent in check calls */
TimerStat d_checkTime;
virtual ~Theory();
/**
- * Creates a new theory rewriter for the theory.
+ * @return The theory rewriter associated with this theory.
*/
- virtual std::unique_ptr<TheoryRewriter> mkTheoryRewriter() = 0;
+ virtual TheoryRewriter* getTheoryRewriter() = 0;
/**
* Subclasses of Theory may add additional efforts. DO NOT CHECK
theory::Valuation(this),
d_logicInfo);
theory::Rewriter::registerTheoryRewriter(
- theoryId, d_theoryTable[theoryId]->mkTheoryRewriter());
+ theoryId, d_theoryTable[theoryId]->getTheoryRewriter());
}
void setPropEngine(prop::PropEngine* propEngine)
TheoryUF::~TheoryUF() {
}
-std::unique_ptr<TheoryRewriter> TheoryUF::mkTheoryRewriter()
-{
- return std::unique_ptr<TheoryRewriter>(new TheoryUfRewriter());
-}
-
void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) {
d_equalityEngine.setMasterEqualityEngine(eq);
}
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
#include "theory/uf/symmetry_breaker.h"
+#include "theory/uf/theory_uf_rewriter.h"
namespace CVC4 {
namespace theory {
~TheoryUF();
- std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+ TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
void finishInit() override;
TNodeTrie* t2,
unsigned arity,
unsigned depth);
+
+ TheoryUfRewriter d_rewriter;
};/* class TheoryUF */
}/* CVC4::theory::uf namespace */
** Unit tests for the strings/sequences rewriter.
**/
+#include <cxxtest/TestSuite.h>
+
+#include <iostream>
+#include <memory>
+#include <vector>
+
#include "expr/node.h"
#include "expr/node_manager.h"
#include "smt/smt_engine.h"
#include "theory/strings/arith_entail.h"
#include "theory/strings/sequences_rewriter.h"
#include "theory/strings/strings_entail.h"
-
-#include <cxxtest/TestSuite.h>
-#include <iostream>
-#include <memory>
-#include <vector>
+#include "theory/strings/strings_rewriter.h"
using namespace CVC4;
using namespace CVC4::smt;
// (str.substr "A" x x) --> ""
Node n = d_nm->mkNode(kind::STRING_SUBSTR, a, x, x);
- Node res = SequencesRewriter::rewriteSubstr(n);
+ Node res = StringsRewriter(nullptr).rewriteSubstr(n);
TS_ASSERT_EQUALS(res, empty);
// (str.substr "A" (+ x 1) x) -> ""
a,
d_nm->mkNode(kind::PLUS, x, d_nm->mkConst(Rational(1))),
x);
- res = SequencesRewriter::rewriteSubstr(n);
+ res = StringsRewriter(nullptr).rewriteSubstr(n);
TS_ASSERT_EQUALS(res, empty);
// (str.substr "A" (+ x (str.len s2)) x) -> ""
a,
d_nm->mkNode(kind::PLUS, x, d_nm->mkNode(kind::STRING_LENGTH, s)),
x);
- res = SequencesRewriter::rewriteSubstr(n);
+ res = StringsRewriter(nullptr).rewriteSubstr(n);
TS_ASSERT_EQUALS(res, empty);
// (str.substr "A" x y) -> (str.substr "A" x y)
n = d_nm->mkNode(kind::STRING_SUBSTR, a, x, y);
- res = SequencesRewriter::rewriteSubstr(n);
+ res = StringsRewriter(nullptr).rewriteSubstr(n);
TS_ASSERT_EQUALS(res, n);
// (str.substr "ABCD" (+ x 3) x) -> ""
n = d_nm->mkNode(
kind::STRING_SUBSTR, abcd, d_nm->mkNode(kind::PLUS, x, three), x);
- res = SequencesRewriter::rewriteSubstr(n);
+ res = StringsRewriter(nullptr).rewriteSubstr(n);
TS_ASSERT_EQUALS(res, empty);
// (str.substr "ABCD" (+ x 2) x) -> (str.substr "ABCD" (+ x 2) x)
n = d_nm->mkNode(
kind::STRING_SUBSTR, abcd, d_nm->mkNode(kind::PLUS, x, two), x);
- res = SequencesRewriter::rewriteSubstr(n);
+ res = StringsRewriter(nullptr).rewriteSubstr(n);
TS_ASSERT_EQUALS(res, n);
// (str.substr (str.substr s x x) x x) -> ""
template <TheoryId theoryId>
class FakeTheory : public Theory
{
- /**
- * This fake theory class is equally useful for bool, uf, arith, etc. It
- * keeps an identifier to identify itself.
- */
- std::string d_id;
-
- /**
- * The expected sequence of rewrite calls. Filled by FakeTheory::expect() and
- * consumed by FakeTheory::preRewrite() and FakeTheory::postRewrite().
- */
- // static std::deque<RewriteItem> s_expected;
-
public:
FakeTheory(context::Context* ctxt,
context::UserContext* uctxt,
{
}
- std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override
- {
- return std::unique_ptr<TheoryRewriter>(new FakeTheoryRewriter());
- }
+ TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
/** Register an expected rewrite call */
static void expect(RewriteType type,
return Node::null();
}
Node getValue(TNode n) { return Node::null(); }
+
+ private:
+ /**
+ * This fake theory class is equally useful for bool, uf, arith, etc. It
+ * keeps an identifier to identify itself.
+ */
+ std::string d_id;
+
+ /** The theory rewriter for this theory. */
+ FakeTheoryRewriter d_rewriter;
}; /* class FakeTheory */
/* definition of the s_expected static field in FakeTheory; see above */
: Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo)
{}
- std::unique_ptr<TheoryRewriter> mkTheoryRewriter()
- {
- return std::unique_ptr<TheoryRewriter>();
- }
+ TheoryRewriter* getTheoryRewriter() { return nullptr; }
void registerTerm(TNode n) {
// check that we registerTerm() a term only once
projects / cvc5.git / commitdiff