namespace theory {
namespace quantifiers {
+InstRewriterCegqi::InstRewriterCegqi(InstStrategyCegqi* p)
+ : InstantiationRewriter(), d_parent(p)
+{
+}
+
+Node InstRewriterCegqi::rewriteInstantiation(Node q,
+ std::vector<Node>& terms,
+ Node inst,
+ bool doVts)
+{
+ return d_parent->rewriteInstantiation(q, terms, inst, doVts);
+}
+
InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe)
: QuantifiersModule(qe),
+ d_irew(new InstRewriterCegqi(this)),
d_cbqi_set_quant_inactive(false),
d_incomplete_check(false),
d_added_cbqi_lemma(qe->getUserContext()),
}
}
}
+Node InstStrategyCegqi::rewriteInstantiation(Node q,
+ std::vector<Node>& terms,
+ Node inst,
+ bool doVts)
+{
+ if (doVts)
+ {
+ // do virtual term substitution
+ inst = Rewriter::rewrite(inst);
+ Trace("quant-vts-debug") << "Rewrite vts symbols in " << inst << std::endl;
+ inst = d_quantEngine->getTermUtil()->rewriteVtsSymbols(inst);
+ Trace("quant-vts-debug") << "...got " << inst << std::endl;
+ }
+ if (options::cbqiNestedQE())
+ {
+ inst = doNestedQE(q, terms, inst, doVts);
+ }
+ return inst;
+}
+
+InstantiationRewriter* InstStrategyCegqi::getInstRewriter() const
+{
+ return d_irew.get();
+}
Node InstStrategyCegqi::doNestedQENode(
Node q, Node ceq, Node n, std::vector<Node>& inst_terms, bool doVts)
#include "theory/decision_manager.h"
#include "theory/quantifiers/bv_inverter.h"
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
+#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quant_util.h"
#include "util/statistics_registry.h"
namespace theory {
namespace quantifiers {
+class InstStrategyCegqi;
+
+/**
+ * An instantiation rewriter based on the counterexample-guided instantiation
+ * quantifiers module below.
+ */
+class InstRewriterCegqi : public InstantiationRewriter
+{
+ public:
+ InstRewriterCegqi(InstStrategyCegqi* p);
+ ~InstRewriterCegqi() {}
+ /**
+ * Rewrite the instantiation via d_parent, based on virtual term substitution
+ * and nested quantifier elimination.
+ */
+ Node rewriteInstantiation(Node q,
+ std::vector<Node>& terms,
+ Node inst,
+ bool doVts) override;
+
+ private:
+ /** pointer to the parent of this class */
+ InstStrategyCegqi* d_parent;
+};
+
/**
* Counterexample-guided quantifier instantiation module.
*
void preRegisterQuantifier(Node q) override;
// presolve
void presolve() override;
- /** Do nested quantifier elimination. */
- Node doNestedQE(Node q, std::vector<Node>& inst_terms, Node lem, bool doVts);
+
+ /**
+ * Rewrite the instantiation inst of quantified formula q for terms; return
+ * the result.
+ *
+ * We rewrite inst based on virtual term substitution and nested quantifier
+ * elimination. For details, see "Solving Quantified Linear Arithmetic via
+ * Counterexample-Guided Instantiation" FMSD 2017, Reynolds et al.
+ */
+ Node rewriteInstantiation(Node q,
+ std::vector<Node>& terms,
+ Node inst,
+ bool doVts);
+ /** get the instantiation rewriter object */
+ InstantiationRewriter* getInstRewriter() const;
//------------------- interface for CegqiOutputInstStrategy
/** Instantiate the current quantified formula forall x. Q with x -> subs. */
//------------------- end interface for CegqiOutputInstStrategy
protected:
+ /** The instantiation rewriter object */
+ std::unique_ptr<InstRewriterCegqi> d_irew;
/** set quantified formula inactive
*
* This flag is set to true during a full effort check if at least one
NodeIntMap d_nested_qe_waitlist_proc;
std::map< Node, std::vector< Node > > d_nested_qe_waitlist;
+ /** Do nested quantifier elimination.
+ *
+ * This rewrites the quantified formulas in inst based on nested quantifier
+ * elimination. In this method, inst is the instantiation of quantified
+ * formula q for the vector terms. The flag doVts indicates whether we must
+ * apply virtual term substitution (if terms contains virtual terms).
+ */
+ Node doNestedQE(Node q, std::vector<Node>& terms, Node inst, bool doVts);
};
d_inst_notify.push_back(in);
}
+void Instantiate::addRewriter(InstantiationRewriter* ir)
+{
+ d_instRewrite.push_back(ir);
+}
+
void Instantiate::notifyFlushLemmas()
{
for (InstantiationNotify*& in : d_inst_notify)
// get the instantiation
Node body = getInstantiation(q, d_term_util->d_vars[q], terms, doVts);
Node orig_body = body;
- if (options::cbqiNestedQE())
- {
- InstStrategyCegqi* icegqi = d_qe->getInstStrategyCegqi();
- if (icegqi)
- {
- body = icegqi->doNestedQE(q, terms, body, doVts);
- }
- }
+ // now preprocess
body = quantifiers::QuantifiersRewriter::preprocess(body, true);
Trace("inst-debug") << "...preprocess to " << body << std::endl;
Node body;
Assert(vars.size() == terms.size());
Assert(q[0].getNumChildren() == vars.size());
- // TODO (#1386) : optimize this
+ // Notice that this could be optimized, but no significant performance
+ // improvements were observed with alternative implementations (see #1386).
body = q[1].substitute(vars.begin(), vars.end(), terms.begin(), terms.end());
- if (doVts)
+ // run rewriters to rewrite the instantiation in sequence.
+ for (InstantiationRewriter*& ir : d_instRewrite)
{
- // do virtual term substitution
- body = Rewriter::rewrite(body);
- Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl;
- Node body_r = d_term_util->rewriteVtsSymbols(body);
- Trace("quant-vts-debug") << " ...result: " << body_r
- << std::endl;
- body = body_r;
+ body = ir->rewriteInstantiation(q, terms, body, doVts);
}
return body;
}
virtual void filterInstantiations() = 0;
};
+/** Instantiation rewriter
+ *
+ * This class is used for cases where instantiation lemmas can be rewritten by
+ * external utilities. Examples of this include virtual term substitution and
+ * nested quantifier elimination techniques.
+ */
+class InstantiationRewriter
+{
+ public:
+ InstantiationRewriter() {}
+ virtual ~InstantiationRewriter() {}
+
+ /** rewrite instantiation
+ *
+ * The node inst is the instantiation of quantified formula q for terms.
+ * This method returns the rewritten form of the instantiation.
+ *
+ * The flag doVts is whether we must apply virtual term substitution to the
+ * instantiation.
+ */
+ virtual Node rewriteInstantiation(Node q,
+ std::vector<Node>& terms,
+ Node inst,
+ bool doVts) = 0;
+};
+
/** Instantiate
*
* This class is used for generating instantiation lemmas. It maintains an
/** check incomplete */
bool checkComplete() override;
- //--------------------------------------notify objects
+ //--------------------------------------notify/rewrite objects
/** add instantiation notify
*
* Adds an instantiation notify class to listen to the instantiations reported
void addNotify(InstantiationNotify* in);
/** get number of instantiation notify added to this class */
bool hasNotify() const { return !d_inst_notify.empty(); }
+ /** add instantiation rewriter */
+ void addRewriter(InstantiationRewriter* ir);
/** notify flush lemmas
*
* This is called just before the quantifiers engine flushes its lemmas to
TermUtil* d_term_util;
/** instantiation notify classes */
std::vector<InstantiationNotify*> d_inst_notify;
+ /** instantiation rewriter classes */
+ std::vector<InstantiationRewriter*> d_instRewrite;
/** statistics for debugging total instantiation */
int d_total_inst_count_debug;
{
d_i_cbqi.reset(new quantifiers::InstStrategyCegqi(qe));
modules.push_back(d_i_cbqi.get());
+ qe->getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter());
}
if (options::ceGuidedInst())
{
{
return d_private->d_synth_e.get();
}
-quantifiers::InstStrategyCegqi* QuantifiersEngine::getInstStrategyCegqi() const
-{
- return d_private->d_i_cbqi.get();
-}
QuantifiersModule * QuantifiersEngine::getOwner( Node q ) {
std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q );
#include "context/cdlist.h"
#include "expr/attribute.h"
#include "expr/term_canonize.h"
-#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
#include "theory/quantifiers/ematching/trigger.h"
#include "theory/quantifiers/equality_infer.h"
#include "theory/quantifiers/equality_query.h"
quantifiers::BoundedIntegers* getBoundedIntegers() const;
/** ceg instantiation */
quantifiers::SynthEngine* getSynthEngine() const;
- /** get inst strategy cbqi */
- quantifiers::InstStrategyCegqi* getInstStrategyCegqi() const;
//---------------------- end modules
private:
/**
projects / cvc5.git / commitdiff