This changes the attribute on internally generated bounded quantified formulas from `isInternal` to `isQuantBounded`. This makes it clear that bounded integers is the module that should process them. It also moves the utility for constructing these quantified formulas from strings to BoundedIntegers itself. This is to accommodate other theories, e.g. bags, that may make use of reductions to bounded quantifiers.
}
// also ignore internal quantifiers
QuantAttributes& qattr = d_qreg.getQuantAttributes();
- if (qattr.isInternal(q))
+ if (qattr.isQuantBounded(q))
{
return false;
}
#include "theory/rewriter.h"
#include "util/rational.h"
-using namespace cvc5;
-using namespace std;
-using namespace cvc5::theory;
-using namespace cvc5::theory::quantifiers;
using namespace cvc5::kind;
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic(
Env& env, Node r, Valuation valuation, bool isProxy)
: DecisionStrategyFmf(env, valuation),
{
// only applying it to internal quantifiers
QuantAttributes& qattr = d_qreg.getQuantAttributes();
- if (!qattr.isInternal(f))
+ if (!qattr.isQuantBounded(f))
{
- Trace("bound-int") << "...not internal, skip" << std::endl;
+ Trace("bound-int") << "...not bounded, skip" << std::endl;
return;
}
}
return true;
}
}
+
+/**
+ * Attribute true for quantifiers that have been internally generated and
+ * should be processed with the bounded integers module, e.g. quantified
+ * formulas from reductions of string operators.
+ *
+ * Currently, this attribute is used for indicating that E-matching should
+ * not be applied, as E-matching should not be applied to quantifiers
+ * generated internally.
+ *
+ * This attribute can potentially be generalized to an identifier indicating
+ * the internal source of the quantified formula (of which strings reduction
+ * is one possibility).
+ */
+struct BoundedQuantAttributeId
+{
+};
+typedef expr::Attribute<BoundedQuantAttributeId, bool> BoundedQuantAttribute;
+/**
+ * Mapping to a dummy node for marking an attribute on internal quantified
+ * formulas. This ensures that reductions are deterministic.
+ */
+struct QInternalVarAttributeId
+{
+};
+typedef expr::Attribute<QInternalVarAttributeId, Node> QInternalVarAttribute;
+
+Node BoundedIntegers::mkBoundedForall(Node bvl, Node body)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ QInternalVarAttribute qiva;
+ Node qvar;
+ if (bvl.hasAttribute(qiva))
+ {
+ qvar = bvl.getAttribute(qiva);
+ }
+ else
+ {
+ SkolemManager* sm = nm->getSkolemManager();
+ qvar = sm->mkDummySkolem("qinternal", nm->booleanType());
+ // this dummy variable marks that the quantified formula is internal
+ qvar.setAttribute(BoundedQuantAttribute(), true);
+ // remember the dummy variable
+ bvl.setAttribute(qiva, qvar);
+ }
+ // make the internal attribute, and put it in a singleton list
+ Node ip = nm->mkNode(INST_ATTRIBUTE, qvar);
+ Node ipl = nm->mkNode(INST_PATTERN_LIST, ip);
+ // make the overall formula
+ return nm->mkNode(FORALL, bvl, body, ipl);
+}
+
+bool BoundedIntegers::isBoundedForallAttribute(Node var)
+{
+ return var.getAttribute(BoundedQuantAttribute());
+}
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace cvc5
/** Identify this module */
std::string identify() const override { return "BoundedIntegers"; }
+ /**
+ * Make internal quantified formula with bound variable list bvl and body.
+ * Internally, we get a node corresponding to marking a quantified formula as
+ * a "bounded quantified formula". This node is provided as the third argument
+ * of the FORALL returned by this method. This ensures that E-matching is not
+ * applied to the quantified formula, and that this module is the one that
+ * handles it.
+ */
+ static Node mkBoundedForall(Node bvl, Node body);
+ /**
+ * Has this node been marked as an annotation for a bounded quantified
+ * formula? This is true for the annotation in the formula returned by the
+ * above method.
+ */
+ static bool isBoundedForallAttribute(Node var);
+
private:
/**
* Set that variable v of quantified formula q has a finite bound, where
{
if (!d_qreg.hasOwnership(q, this))
{
+ // if we don't have ownership, another module has taken responsibility
+ // for processing q.
return false;
}
// if finite model finding or fmf bound is on, we process everything
{
return true;
}
- // otherwise, we are only using model-based instantiation for internal
- // quantified formulas
+ // otherwise, we are only using model-based instantiation for internally
+ // generated bounded quantified formulas
QuantAttributes& qattr = d_qreg.getQuantAttributes();
- return qattr.isInternal(q);
+ return qattr.isQuantBounded(q);
}
} // namespace quantifiers
#include "options/quantifiers_options.h"
#include "theory/arith/arith_msum.h"
+#include "theory/quantifiers/fmf/bounded_integers.h"
#include "theory/quantifiers/sygus/synth_engine.h"
#include "theory/quantifiers/term_util.h"
#include "util/rational.h"
bool QAttributes::isStandard() const
{
- return !d_sygus && !d_quant_elim && !isFunDef() && !d_isInternal;
+ return !d_sygus && !d_quant_elim && !isFunDef() && !d_isQuantBounded;
}
QuantAttributes::QuantAttributes() {}
qa.d_quant_elim_partial = true;
//don't set owner, should happen naturally
}
- if (avar.getAttribute(InternalQuantAttribute()))
+ if (BoundedIntegers::isBoundedForallAttribute(avar))
{
- Trace("quant-attr") << "Attribute : internal : " << q << std::endl;
- qa.d_isInternal = true;
+ Trace("quant-attr")
+ << "Attribute : bounded quantifiers : " << q << std::endl;
+ qa.d_isQuantBounded = true;
}
if( avar.hasAttribute(QuantIdNumAttribute()) ){
qa.d_qid_num = avar;
}
}
-bool QuantAttributes::isInternal(Node q) const
+bool QuantAttributes::isQuantBounded(Node q) const
{
std::map<Node, QAttributes>::const_iterator it = d_qattr.find(q);
if (it != d_qattr.end())
{
- return it->second.d_isInternal;
+ return it->second.d_isQuantBounded;
}
return false;
}
};
typedef expr::Attribute<AbsTypeFunDefAttributeId, bool> AbsTypeFunDefAttribute;
-/**
- * Attribute true for quantifiers that have been internally generated, e.g.
- * for reductions of string operators.
- *
- * Currently, this attribute is used for indicating that E-matching should
- * not be applied, as E-matching should not be applied to quantifiers
- * generated for strings reductions.
- *
- * This attribute can potentially be generalized to an identifier indicating
- * the internal source of the quantified formula (of which strings reduction
- * is one possibility).
- */
-struct InternalQuantAttributeId
-{
-};
-typedef expr::Attribute<InternalQuantAttributeId, bool> InternalQuantAttribute;
-
namespace quantifiers {
/** This struct stores attributes for a single quantified formula */
d_qinstLevel(-1),
d_quant_elim(false),
d_quant_elim_partial(false),
- d_isInternal(false)
+ d_isQuantBounded(false)
{
}
~QAttributes(){}
bool d_quant_elim;
/** is this formula marked for partial quantifier elimination? */
bool d_quant_elim_partial;
- /** Is this formula internally generated? */
- bool d_isInternal;
+ /** Is this formula internally generated and belonging to bounded integers? */
+ bool d_isQuantBounded;
/** the instantiation pattern list for this quantified formula (its 3rd child)
*/
Node d_ipl;
/** is quant elim partial */
bool isQuantElimPartial( Node q );
/** is internal quantifier */
- bool isInternal(Node q) const;
+ bool isQuantBounded(Node q) const;
/** get quant name, which is used for :qid */
Node getQuantName(Node q) const;
/** Print quantified formula q, possibly using its name, if it has one */
#include "expr/attribute.h"
#include "expr/skolem_manager.h"
#include "options/strings_options.h"
+#include "theory/quantifiers/fmf/bounded_integers.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/rewriter.h"
#include "theory/strings/arith_entail.h"
return node.getOperator().getConst<RegExpLoop>().d_loopMinOcc;
}
-/**
- * Mapping to a dummy node for marking an attribute on internal quantified
- * formulas. This ensures that reductions are deterministic.
- */
-struct QInternalVarAttributeId
-{
-};
-typedef expr::Attribute<QInternalVarAttributeId, Node> QInternalVarAttribute;
-
Node mkForallInternal(Node bvl, Node body)
{
- NodeManager* nm = NodeManager::currentNM();
- QInternalVarAttribute qiva;
- Node qvar;
- if (bvl.hasAttribute(qiva))
- {
- qvar = bvl.getAttribute(qiva);
- }
- else
- {
- SkolemManager* sm = nm->getSkolemManager();
- qvar = sm->mkDummySkolem("qinternal", nm->booleanType());
- // this dummy variable marks that the quantified formula is internal
- qvar.setAttribute(InternalQuantAttribute(), true);
- // remember the dummy variable
- bvl.setAttribute(qiva, qvar);
- }
- // make the internal attribute, and put it in a singleton list
- Node ip = nm->mkNode(INST_ATTRIBUTE, qvar);
- Node ipl = nm->mkNode(INST_PATTERN_LIST, ip);
- // make the overall formula
- return nm->mkNode(FORALL, bvl, body, ipl);
+ return quantifiers::BoundedIntegers::mkBoundedForall(bvl, body);
}
} // namespace utils
projects / cvc5.git / commitdiff