#include <sstream>
#include "expr/skolem_manager.h"
-#include "theory/rewriter.h"
namespace cvc5 {
add(s.d_vars, s.d_subs);
}
-Node Subs::apply(Node n, bool doRewrite) const
+Node Subs::apply(Node n) const
{
if (d_vars.empty())
{
}
Node ns =
n.substitute(d_vars.begin(), d_vars.end(), d_subs.begin(), d_subs.end());
- if (doRewrite)
- {
- ns = theory::Rewriter::rewrite(ns);
- }
return ns;
}
-Node Subs::rapply(Node n, bool doRewrite) const
+Node Subs::rapply(Node n) const
{
if (d_vars.empty())
{
}
Node ns =
n.substitute(d_subs.begin(), d_subs.end(), d_vars.begin(), d_vars.end());
- if (doRewrite)
- {
- ns = theory::Rewriter::rewrite(ns);
- }
return ns;
}
-void Subs::applyToRange(Subs& s, bool doRewrite) const
+void Subs::applyToRange(Subs& s) const
{
if (d_vars.empty())
{
}
for (size_t i = 0, ns = s.d_subs.size(); i < ns; i++)
{
- s.d_subs[i] = apply(s.d_subs[i], doRewrite);
+ s.d_subs[i] = apply(s.d_subs[i]);
}
}
-void Subs::rapplyToRange(Subs& s, bool doRewrite) const
+void Subs::rapplyToRange(Subs& s) const
{
if (d_vars.empty())
{
}
for (size_t i = 0, ns = s.d_subs.size(); i < ns; i++)
{
- s.d_subs[i] = rapply(s.d_subs[i], doRewrite);
+ s.d_subs[i] = rapply(s.d_subs[i]);
}
}
/** Append the substitution s to this */
void append(Subs& s);
/** Return the result of this substitution on n */
- Node apply(Node n, bool doRewrite = false) const;
+ Node apply(Node n) const;
/** Return the result of the reverse of this substitution on n */
- Node rapply(Node n, bool doRewrite = false) const;
+ Node rapply(Node n) const;
/** Apply this substitution to all nodes in the range of s */
- void applyToRange(Subs& s, bool doRewrite = false) const;
+ void applyToRange(Subs& s) const;
/** Apply the reverse of this substitution to all nodes in the range of s */
- void rapplyToRange(Subs& s, bool doRewrite = false) const;
+ void rapplyToRange(Subs& s) const;
/** Get equality (= v s) where v -> s is the i^th position in the vectors */
Node getEquality(size_t i) const;
/** Convert substitution to map */
#include "expr/node_algorithm.h"
#include "expr/subs.h"
#include "smt/env.h"
+#include "theory/rewriter.h"
#include "theory/smt_engine_subsolver.h"
namespace cvc5 {
Node qeBody = sk.apply(q[1]);
qeBody = snqe.apply(qeBody);
// undo the skolemization
- qeBody = sk.rapply(qeBody, true);
+ qeBody = sk.rapply(qeBody);
+ qeBody = env.getRewriter()->rewrite(qeBody);
// reconstruct the body
std::vector<Node> qargs;
qargs.push_back(q[0]);
namespace quantifiers {
namespace inst {
-IMGenerator::IMGenerator(Trigger* tparent)
- : d_tparent(tparent), d_qstate(tparent->d_qstate), d_treg(tparent->d_treg)
+IMGenerator::IMGenerator(Env& env, Trigger* tparent)
+ : EnvObj(env),
+ d_tparent(tparent),
+ d_qstate(tparent->d_qstate),
+ d_treg(tparent->d_treg)
{
}
#define CVC5__THEORY__QUANTIFIERS__IM_GENERATOR_H
#include <map>
+
#include "expr/node.h"
+#include "smt/env_obj.h"
#include "theory/inference_id.h"
#include "theory/quantifiers/inst_match.h"
* point in which instantiate lemmas are enqueued to be sent on the output
* channel.
*/
-class IMGenerator {
-public:
- IMGenerator(Trigger* tparent);
- virtual ~IMGenerator() {}
- /** Reset instantiation round.
- *
- * Called once at beginning of an instantiation round.
- */
- virtual void resetInstantiationRound() {}
- /** Reset.
- *
- * eqc is the equivalence class to search in (any if eqc=null).
- * Returns true if this generator can produce instantiations, and false
- * otherwise. An example of when it returns false is if it can be determined
- * that no appropriate matchable terms occur based on eqc.
- */
- virtual bool reset(Node eqc) { return true; }
- /** Get the next match.
- *
- * Must call reset( eqc ) before this function. This constructs an
- * instantiation, which it populates in data structure m,
- * based on the current context using the implemented matching algorithm.
- *
- * q is the quantified formula we are adding instantiations for
- * m is the InstMatch object we are generating
- *
- * Returns a value >0 if an instantiation was successfully generated
- */
- virtual int getNextMatch(Node q, InstMatch& m) { return 0; }
- /** add instantiations
- *
- * This adds all available instantiations for q based on the current context
- * using the implemented matching algorithm. It typically is implemented as a
- * fixed point of getNextMatch above.
- *
- * It returns the number of instantiations added using calls to
- * Instantiate::addInstantiation(...).
- */
- virtual uint64_t addInstantiations(Node q) { return 0; }
- /** get active score
- *
- * A heuristic value indicating how active this generator is.
- */
- virtual int getActiveScore() { return 0; }
+class IMGenerator : protected EnvObj
+{
+ public:
+ IMGenerator(Env& env, Trigger* tparent);
+ virtual ~IMGenerator() {}
+ /** Reset instantiation round.
+ *
+ * Called once at beginning of an instantiation round.
+ */
+ virtual void resetInstantiationRound() {}
+ /** Reset.
+ *
+ * eqc is the equivalence class to search in (any if eqc=null).
+ * Returns true if this generator can produce instantiations, and false
+ * otherwise. An example of when it returns false is if it can be determined
+ * that no appropriate matchable terms occur based on eqc.
+ */
+ virtual bool reset(Node eqc) { return true; }
+ /** Get the next match.
+ *
+ * Must call reset( eqc ) before this function. This constructs an
+ * instantiation, which it populates in data structure m,
+ * based on the current context using the implemented matching algorithm.
+ *
+ * q is the quantified formula we are adding instantiations for
+ * m is the InstMatch object we are generating
+ *
+ * Returns a value >0 if an instantiation was successfully generated
+ */
+ virtual int getNextMatch(Node q, InstMatch& m) { return 0; }
+ /** add instantiations
+ *
+ * This adds all available instantiations for q based on the current context
+ * using the implemented matching algorithm. It typically is implemented as a
+ * fixed point of getNextMatch above.
+ *
+ * It returns the number of instantiations added using calls to
+ * Instantiate::addInstantiation(...).
+ */
+ virtual uint64_t addInstantiations(Node q) { return 0; }
+ /** get active score
+ *
+ * A heuristic value indicating how active this generator is.
+ */
+ virtual int getActiveScore() { return 0; }
-protected:
- /** send instantiation
- *
- * This method sends instantiation, specified by m, to the parent trigger
- * object, which will in turn make a call to
- * Instantiate::addInstantiation(...). This method returns true if a
- * call to Instantiate::addInstantiation(...) was successfully made,
- * indicating that an instantiation was enqueued in the quantifier engine's
- * lemma cache.
- */
- bool sendInstantiation(InstMatch& m, InferenceId id);
- /** The parent trigger that owns this */
- Trigger* d_tparent;
- /** Reference to the state of the quantifiers engine */
- QuantifiersState& d_qstate;
- /** Reference to the term registry */
- TermRegistry& d_treg;
-};/* class IMGenerator */
+ protected:
+ /** send instantiation
+ *
+ * This method sends instantiation, specified by m, to the parent trigger
+ * object, which will in turn make a call to
+ * Instantiate::addInstantiation(...). This method returns true if a
+ * call to Instantiate::addInstantiation(...) was successfully made,
+ * indicating that an instantiation was enqueued in the quantifier engine's
+ * lemma cache.
+ */
+ bool sendInstantiation(InstMatch& m, InferenceId id);
+ /** The parent trigger that owns this */
+ Trigger* d_tparent;
+ /** Reference to the state of the quantifiers engine */
+ QuantifiersState& d_qstate;
+ /** Reference to the term registry */
+ TermRegistry& d_treg;
+}; /* class IMGenerator */
} // namespace inst
}
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_registry.h"
#include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
#include "util/rational.h"
using namespace cvc5::kind;
namespace quantifiers {
namespace inst {
-InstMatchGenerator::InstMatchGenerator(Trigger* tparent, Node pat)
- : IMGenerator(tparent)
+InstMatchGenerator::InstMatchGenerator(Env& env, Trigger* tparent, Node pat)
+ : IMGenerator(env, tparent)
{
d_cg = nullptr;
d_needsReset = true;
}
else
{
- InstMatchGenerator* cimg = getInstMatchGenerator(d_tparent, q, pat);
+ InstMatchGenerator* cimg =
+ getInstMatchGenerator(d_env, d_tparent, q, pat);
if (cimg)
{
d_children.push_back(cimg);
return addedLemmas;
}
-InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator(Trigger* tparent,
+InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator(Env& env,
+ Trigger* tparent,
Node q,
Node pat)
{
std::vector< Node > pats;
pats.push_back( pat );
std::map< Node, InstMatchGenerator * > pat_map_init;
- return mkInstMatchGenerator(tparent, q, pats, pat_map_init);
+ return mkInstMatchGenerator(env, tparent, q, pats, pat_map_init);
}
InstMatchGenerator* InstMatchGenerator::mkInstMatchGeneratorMulti(
- Trigger* tparent, Node q, std::vector<Node>& pats)
+ Env& env, Trigger* tparent, Node q, std::vector<Node>& pats)
{
Assert(pats.size() > 1);
InstMatchGeneratorMultiLinear* imgm =
- new InstMatchGeneratorMultiLinear(tparent, q, pats);
+ new InstMatchGeneratorMultiLinear(env, tparent, q, pats);
std::vector< InstMatchGenerator* > gens;
imgm->initialize(q, gens);
Assert(gens.size() == pats.size());
patsn.push_back( pn );
pat_map_init[pn] = g;
}
- imgm->d_next = mkInstMatchGenerator(tparent, q, patsn, pat_map_init);
+ imgm->d_next = mkInstMatchGenerator(env, tparent, q, patsn, pat_map_init);
return imgm;
}
InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator(
+ Env& env,
Trigger* tparent,
Node q,
std::vector<Node>& pats,
InstMatchGenerator* init;
std::map< Node, InstMatchGenerator * >::iterator iti = pat_map_init.find( pats[pCounter] );
if( iti==pat_map_init.end() ){
- init = getInstMatchGenerator(tparent, q, pats[pCounter]);
+ init = getInstMatchGenerator(env, tparent, q, pats[pCounter]);
}else{
init = iti->second;
}
return oinit;
}
-InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent,
+InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Env& env,
+ Trigger* tparent,
Node q,
Node n)
{
if (!x.isNull())
{
Node s = PatternTermSelector::getInversion(n, x);
+ s = env.getRewriter()->rewrite(s);
VarMatchGeneratorTermSubs* vmg =
- new VarMatchGeneratorTermSubs(tparent, x, s);
+ new VarMatchGeneratorTermSubs(env, tparent, x, s);
Trace("var-trigger") << "Term substitution trigger : " << n
<< ", var = " << x << ", subs = " << s << std::endl;
return vmg;
if (TriggerTermInfo::isUsableRelationTrigger(n, hasPol, pol, lit))
{
Trace("relational-trigger") << "...yes, for literal " << lit << std::endl;
- return new RelationalMatchGenerator(tparent, lit, hasPol, pol);
+ return new RelationalMatchGenerator(env, tparent, lit, hasPol, pol);
}
- return new InstMatchGenerator(tparent, n);
+ return new InstMatchGenerator(env, tparent, n);
}
} // namespace inst
void setIndependent() { d_independent_gen = true; }
//-------------------------------construction of inst match generators
/** mkInstMatchGenerator for single triggers, calls the method below */
- static InstMatchGenerator* mkInstMatchGenerator(Trigger* tparent,
+ static InstMatchGenerator* mkInstMatchGenerator(Env& env,
+ Trigger* tparent,
Node q,
Node pat);
/** mkInstMatchGenerator for the multi trigger case
* InstMatchGenerators corresponding to each unique subterm of pats with
* free variables.
*/
- static InstMatchGenerator* mkInstMatchGeneratorMulti(Trigger* tparent,
+ static InstMatchGenerator* mkInstMatchGeneratorMulti(Env& env,
+ Trigger* tparent,
Node q,
std::vector<Node>& pats);
/** mkInstMatchGenerator
* It calls initialize(...) for all InstMatchGenerators generated by this call.
*/
static InstMatchGenerator* mkInstMatchGenerator(
+ Env& env,
Trigger* tparent,
Node q,
std::vector<Node>& pats,
* These are intentionally private, and are called during linked list
* construction in mkInstMatchGenerator.
*/
- InstMatchGenerator(Trigger* tparent, Node pat);
+ InstMatchGenerator(Env& env, Trigger* tparent, Node pat);
/** The pattern we are producing matches for.
*
* This term and d_match_pattern can be different since this
* appropriate matching algorithm for n within q
* within a linked list of InstMatchGenerators.
*/
- static InstMatchGenerator* getInstMatchGenerator(Trigger* tparent,
+ static InstMatchGenerator* getInstMatchGenerator(Env& env,
+ Trigger* tparent,
Node q,
Node n);
};/* class InstMatchGenerator */
namespace quantifiers {
namespace inst {
-InstMatchGeneratorMulti::InstMatchGeneratorMulti(Trigger* tparent,
+InstMatchGeneratorMulti::InstMatchGeneratorMulti(Env& env,
+ Trigger* tparent,
Node q,
std::vector<Node>& pats)
- : IMGenerator(tparent), d_quant(q)
+ : IMGenerator(env, tparent), d_quant(q)
{
Trace("multi-trigger-cache")
<< "Making smart multi-trigger for " << q << std::endl;
Node n = pats[i];
// make the match generator
InstMatchGenerator* img =
- InstMatchGenerator::mkInstMatchGenerator(tparent, q, n);
+ InstMatchGenerator::mkInstMatchGenerator(env, tparent, q, n);
img->setActiveAdd(false);
d_children.push_back(img);
// compute unique/shared variables
{
public:
/** constructors */
- InstMatchGeneratorMulti(Trigger* tparent, Node q, std::vector<Node>& pats);
+ InstMatchGeneratorMulti(Env& env,
+ Trigger* tparent,
+ Node q,
+ std::vector<Node>& pats);
/** destructor */
~InstMatchGeneratorMulti() override;
namespace inst {
InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear(
- Trigger* tparent, Node q, std::vector<Node>& pats)
- : InstMatchGenerator(tparent, Node::null())
+ Env& env, Trigger* tparent, Node q, std::vector<Node>& pats)
+ : InstMatchGenerator(env, tparent, Node::null())
{
// order patterns to maximize eager matching failures
std::map<Node, std::vector<Node> > var_contains;
{
Node po = pats_ordered[i];
Trace("multi-trigger-linear") << "...make for " << po << std::endl;
- InstMatchGenerator* cimg = getInstMatchGenerator(tparent, q, po);
+ InstMatchGenerator* cimg = getInstMatchGenerator(env, tparent, q, po);
Assert(cimg != nullptr);
d_children.push_back(cimg);
// this could be improved
/** reset the children of this generator */
int resetChildren();
/** constructor */
- InstMatchGeneratorMultiLinear(Trigger* tparent,
+ InstMatchGeneratorMultiLinear(Env& env,
+ Trigger* tparent,
Node q,
std::vector<Node>& pats);
};
namespace quantifiers {
namespace inst {
-InstMatchGeneratorSimple::InstMatchGeneratorSimple(Trigger* tparent,
+InstMatchGeneratorSimple::InstMatchGeneratorSimple(Env& env,
+ Trigger* tparent,
Node q,
Node pat)
- : IMGenerator(tparent), d_quant(q), d_match_pattern(pat)
+ : IMGenerator(env, tparent), d_quant(q), d_match_pattern(pat)
{
if (d_match_pattern.getKind() == NOT)
{
{
public:
/** constructors */
- InstMatchGeneratorSimple(Trigger* tparent, Node q, Node pat);
+ InstMatchGeneratorSimple(Env& env, Trigger* tparent, Node q, Node pat);
/** Reset instantiation round. */
void resetInstantiationRound() override;
x = nm->mkNode(MULT, x, coeff);
}
}
- x = Rewriter::rewrite(x);
}
else
{
namespace quantifiers {
namespace inst {
-RelationalMatchGenerator::RelationalMatchGenerator(Trigger* tparent,
- Node rtrigger,
- bool hasPol,
- bool pol)
- : InstMatchGenerator(tparent, Node::null()),
+RelationalMatchGenerator::RelationalMatchGenerator(
+ Env& env, Trigger* tparent, Node rtrigger, bool hasPol, bool pol)
+ : InstMatchGenerator(env, tparent, Node::null()),
d_vindex(-1),
d_hasPol(hasPol),
d_pol(pol),
* @param hasPol Whether the trigger has an entailed polarity
* @param pol The entailed polarity of the relational trigger.
*/
- RelationalMatchGenerator(Trigger* tparent,
- Node rtrigger,
- bool hasPol,
- bool pol);
+ RelationalMatchGenerator(
+ Env& env, Trigger* tparent, Node rtrigger, bool hasPol, bool pol);
/** Reset */
bool reset(Node eqc) override;
if( d_nodes.size()==1 ){
if (TriggerTermInfo::isSimpleTrigger(d_nodes[0]))
{
- d_mg = new InstMatchGeneratorSimple(this, q, d_nodes[0]);
+ d_mg = new InstMatchGeneratorSimple(env, this, q, d_nodes[0]);
++(stats.d_triggers);
}else{
- d_mg = InstMatchGenerator::mkInstMatchGenerator(this, q, d_nodes[0]);
+ d_mg = InstMatchGenerator::mkInstMatchGenerator(env, this, q, d_nodes[0]);
++(stats.d_simple_triggers);
}
}else{
if (options().quantifiers.multiTriggerCache)
{
- d_mg = new InstMatchGeneratorMulti(this, q, d_nodes);
+ d_mg = new InstMatchGeneratorMulti(env, this, q, d_nodes);
}
else
{
- d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti(this, q, d_nodes);
+ d_mg =
+ InstMatchGenerator::mkInstMatchGeneratorMulti(env, this, q, d_nodes);
}
if (Trace.isOn("multi-trigger"))
{
namespace quantifiers {
namespace inst {
-VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs(Trigger* tparent,
+VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs(Env& env,
+ Trigger* tparent,
Node var,
Node subs)
- : InstMatchGenerator(tparent, Node::null()),
+ : InstMatchGenerator(env, tparent, Node::null()),
d_var(var),
d_subs(subs),
d_rm_prev(false)
<< d_var << " in " << d_subs << std::endl;
TNode tvar = d_var;
Node s = d_subs.substitute(tvar, d_eq_class);
- s = Rewriter::rewrite(s);
+ s = rewrite(s);
Trace("var-trigger-matching")
<< "...got " << s << ", " << s.getKind() << std::endl;
d_eq_class = Node::null();
class VarMatchGeneratorTermSubs : public InstMatchGenerator
{
public:
- VarMatchGeneratorTermSubs(Trigger* tparent, Node var, Node subs);
+ VarMatchGeneratorTermSubs(Env& env, Trigger* tparent, Node var, Node subs);
/** Reset */
bool reset(Node eqc) override;
if (!d_solvedf.empty())
{
// replace the final solution into the solved functions
- finalSol.applyToRange(d_solvedf, true);
+ finalSol.applyToRange(d_solvedf);
+ // rewrite the solution
+ for (Node& n : d_solvedf.d_subs)
+ {
+ n = rewrite(n);
+ }
}
}
projects / cvc5.git / commitdiff