This ensures that datatype selectors are properly handled as triggers in E-matching.
This is challenging since selectors in quantified formulas are of kind APPLY_SELECTOR but are theory-preprocessed to APPLY_SELECTOR_TOTAL/APPLY_UF. Hence, we must match on 2 possible operators, and ones that do not match the operator of the trigger. This adds a custom candidate generator for this case.
It also removes a deprecated option that is no longer used (in part due to our use of shared selectors).
This is in preparation for further work on optimizing cvc4 on benchmarks from Facebook.
Note that there is not a convienient way to call expandDefinitions currently (which is required to get the proper operators to match). This PR calls smt::getCurrentSmtEngine() to do this, although we should find a better solution soon, e.g. adding expandDefinitions to the rewriter.
FYI @barrettcw
default = "false"
help = "purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1"
-[[option]]
- name = "purifyDtTriggers"
- category = "regular"
- long = "purify-dt-triggers"
- type = "bool"
- default = "false"
- help = "purify dt triggers, match all constructors of correct form instead of selectors"
-
[[option]]
name = "pureThTriggers"
category = "regular"
return d_pp->simplify(ex);
}
-Node SmtEngine::expandDefinitions(const Node& ex)
+Node SmtEngine::expandDefinitions(const Node& ex, bool expandOnly)
{
d_resourceManager->spendResource(ResourceManager::Resource::PreprocessStep);
SmtScope smts(this);
finishInit();
d_state->doPendingPops();
- // set expandOnly flag to true
- return d_pp->expandDefinitions(ex, true);
+ return d_pp->expandDefinitions(ex, expandOnly);
}
// TODO(#1108): Simplify the error reporting of this method.
Node simplify(const Node& e);
/**
- * Expand the definitions in a term or formula. No other
- * simplification or normalization is done.
+ * Expand the definitions in a term or formula.
+ *
+ * @param n The node to expand
+ * @param expandOnly if true, then the expandDefinitions function of
+ * TheoryEngine is not called on subterms of n.
*
* @throw TypeCheckingException, LogicException, UnsafeInterruptException
*/
- Node expandDefinitions(const Node& e);
+ Node expandDefinitions(const Node& n, bool expandOnly = true);
/**
* Get the assigned value of an expr (only if immediately preceded by a SAT
#include "theory/quantifiers/ematching/candidate_generator.h"
#include "expr/dtype.h"
#include "options/quantifiers_options.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
#include "theory/quantifiers/inst_match.h"
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/term_database.h"
#include "theory/theory_engine.h"
#include "theory/uf/theory_uf.h"
-using namespace std;
-using namespace CVC4;
using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::inst;
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
bool CandidateGenerator::isLegalCandidate( Node n ){
return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(n) );
d_term_iter_limit = d_qe->getTermDatabase()->getNumGroundTerms( d_op );
}
-void CandidateGeneratorQE::reset( Node eqc ){
+void CandidateGeneratorQE::reset(Node eqc) { resetForOperator(eqc, d_op); }
+
+void CandidateGeneratorQE::resetForOperator(Node eqc, Node op)
+{
d_term_iter = 0;
+ d_eqc = eqc;
+ d_op = op;
if( eqc.isNull() ){
d_mode = cand_term_db;
}else{
}else{
eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine();
if( ee->hasTerm( eqc ) ){
- TNodeTrie* tat = d_qe->getTermDatabase()->getTermArgTrie(eqc, d_op);
+ TNodeTrie* tat = d_qe->getTermDatabase()->getTermArgTrie(eqc, op);
if( tat ){
//create an equivalence class iterator in eq class eqc
Node rep = ee->getRepresentative( eqc );
}
}else{
//the only match is this term itself
- d_eqc = eqc;
d_mode = cand_term_ident;
}
}
}
Node CandidateGeneratorQE::getNextCandidate(){
+ return getNextCandidateInternal();
+}
+
+Node CandidateGeneratorQE::getNextCandidateInternal()
+{
if( d_mode==cand_term_db ){
Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl;
//get next candidate term in the uf term database
Node CandidateGeneratorConsExpand::getNextCandidate()
{
// get the next term from the base class
- Node curr = CandidateGeneratorQE::getNextCandidate();
+ Node curr = getNextCandidateInternal();
if (curr.isNull() || (curr.hasOperator() && curr.getOperator() == d_op))
{
return curr;
{
return isLegalCandidate(n);
}
+
+CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersEngine* qe,
+ Node mpat)
+ : CandidateGeneratorQE(qe, mpat)
+{
+ Trace("sel-trigger") << "Selector trigger: " << mpat << std::endl;
+ Assert(mpat.getKind() == APPLY_SELECTOR);
+ Node mpatExp = smt::currentSmtEngine()->expandDefinitions(mpat, false);
+ Trace("sel-trigger") << "Expands to: " << mpatExp << std::endl;
+ if (mpatExp.getKind() == ITE)
+ {
+ Assert(mpatExp[1].getKind() == APPLY_SELECTOR_TOTAL);
+ Assert(mpatExp[2].getKind() == APPLY_UF);
+ d_selOp = qe->getTermDatabase()->getMatchOperator(mpatExp[1]);
+ d_ufOp = qe->getTermDatabase()->getMatchOperator(mpatExp[2]);
+ }
+ else
+ {
+ // corner case of datatype with one constructor
+ Assert(mpatExp.getKind() == APPLY_SELECTOR_TOTAL);
+ d_selOp = qe->getTermDatabase()->getMatchOperator(mpatExp);
+ }
+ Assert(d_selOp != d_ufOp);
+}
+
+void CandidateGeneratorSelector::reset(Node eqc)
+{
+ Trace("sel-trigger-debug") << "Reset in eqc=" << eqc << std::endl;
+ // start with d_selOp
+ resetForOperator(eqc, d_selOp);
+}
+
+Node CandidateGeneratorSelector::getNextCandidate()
+{
+ Node nextc = getNextCandidateInternal();
+ if (!nextc.isNull())
+ {
+ Trace("sel-trigger-debug") << "...next candidate is " << nextc << std::endl;
+ return nextc;
+ }
+ else if (d_op == d_selOp)
+ {
+ if (d_ufOp.isNull())
+ {
+ // corner case: selector cannot be wrongly applied (1-cons case)
+ d_op = Node::null();
+ }
+ else
+ {
+ // finished correctly applied selectors, now try incorrectly applied ones
+ resetForOperator(d_eqc, d_ufOp);
+ return getNextCandidate();
+ }
+ }
+ Trace("sel-trigger-debug") << "...finished" << std::endl;
+ // no more candidates
+ return Node::null();
+}
+
+} // namespace inst
+} // namespace theory
+} // namespace CVC4
}
protected:
+ /** reset this class for matching operator op in equivalence class eqc */
+ void resetForOperator(Node eqc, Node op);
+ /** the default implementation of getNextCandidate. */
+ Node getNextCandidateInternal();
/** operator you are looking for */
Node d_op;
/** the equality class iterator (for cand_term_eqc) */
int d_term_iter;
/** the TermDb index of the current ground term (for cand_term_db) */
int d_term_iter_limit;
- /** the term we are matching (for cand_term_ident) */
+ /** the current equivalence class */
Node d_eqc;
/** candidate generation modes */
enum {
bool isLegalOpCandidate(Node n) override;
};
+/**
+ * Candidate generator for selector applications, which considers both
+ * internal terms corresponding to correctly and incorrectly applied selectors.
+ */
+class CandidateGeneratorSelector : public CandidateGeneratorQE
+{
+ public:
+ CandidateGeneratorSelector(QuantifiersEngine* qe, Node mpat);
+ /** reset */
+ void reset(Node eqc) override;
+ /**
+ * Get next candidate, returns matching candidates that are ground terms
+ * of the selector operator, followed by those that are applications of the
+ * UF corresponding to an invocation of applying this selector to an
+ * application of the wrong constructor.
+ */
+ Node getNextCandidate() override;
+ protected:
+ /** the selector operator */
+ Node d_selOp;
+ /** the UF operator */
+ Node d_ufOp;
+};
+
}/* CVC4::theory::inst namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
break;
}
}
- }else if( d_match_pattern.getKind()==APPLY_SELECTOR_TOTAL && d_match_pattern[0].getKind()==INST_CONSTANT &&
- options::purifyDtTriggers() && !options::dtSharedSelectors() ){
- d_match_pattern = d_match_pattern[0];
}
d_match_pattern_type = d_match_pattern.getType();
Trace("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl;
d_match_pattern_op = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
//now, collect children of d_match_pattern
- if (d_match_pattern.getKind() == INST_CONSTANT)
+ Kind mpk = d_match_pattern.getKind();
+ if (mpk == INST_CONSTANT)
{
d_children_types.push_back(
d_match_pattern.getAttribute(InstVarNumAttribute()));
}
//create candidate generator
- if( Trigger::isAtomicTrigger( d_match_pattern ) ){
- if (d_match_pattern.getKind() == APPLY_CONSTRUCTOR)
+ if (mpk == APPLY_SELECTOR)
+ {
+ // candidates for apply selector are a union of correctly and incorrectly
+ // applied selectors
+ d_cg = new inst::CandidateGeneratorSelector(qe, d_match_pattern);
+ }
+ else if (Trigger::isAtomicTriggerKind(mpk))
+ {
+ if (mpk == APPLY_CONSTRUCTOR)
{
// 1-constructors have a trivial way of generating candidates in a
// given equivalence class
d_eq_class_rel = Node::null();
}
}
- }else if( d_match_pattern.getKind()==INST_CONSTANT ){
+ }
+ else if (mpk == INST_CONSTANT)
+ {
if( d_pattern.getKind()==APPLY_SELECTOR_TOTAL ){
Node selectorExpr = qe->getTermDatabase()->getMatchOperator(d_pattern);
size_t selectorIndex = datatypes::utils::cindexOf(selectorExpr);
d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern );
}
}
- else if (d_match_pattern.getKind() == EQUAL)
+ else if (mpk == EQUAL)
{
//we will be producing candidates via literal matching heuristics
if (d_pattern.getKind() == NOT)
//if t is null
Assert(!t.isNull());
Assert(!quantifiers::TermUtil::hasInstConstAttr(t));
- Assert(d_match_pattern.getKind() == INST_CONSTANT
- || t.getKind() == d_match_pattern.getKind());
- Assert(!Trigger::isAtomicTrigger(d_match_pattern)
- || t.getOperator() == d_match_pattern.getOperator());
+ // notice that t may have a different kind or operator from our match
+ // pattern, e.g. for APPLY_SELECTOR triggers.
//first, check if ground arguments are not equal, or a match is in conflict
Trace("matching-debug2") << "Setting immediate matches..." << std::endl;
for (unsigned i = 0, size = d_match_pattern.getNumChildren(); i < size; i++)
}
bool Trigger::isAtomicTriggerKind( Kind k ) {
+ // we use both APPLY_SELECTOR and APPLY_SELECTOR_TOTAL since this
+ // method is used both for trigger selection and for ground term registration,
+ // where these two things require those kinds respectively.
return k == APPLY_UF || k == SELECT || k == STORE || k == APPLY_CONSTRUCTOR
- || k == APPLY_SELECTOR_TOTAL || k == APPLY_TESTER || k == UNION
- || k == INTERSECTION || k == SUBSET || k == SETMINUS || k == MEMBER
- || k == SINGLETON || k == SEP_PTO || k == BITVECTOR_TO_NAT
- || k == INT_TO_BITVECTOR || k == HO_APPLY || k == SEQ_NTH;
+ || k == APPLY_SELECTOR || k == APPLY_SELECTOR_TOTAL
+ || k == APPLY_TESTER || k == UNION || k == INTERSECTION || k == SUBSET
+ || k == SETMINUS || k == MEMBER || k == SINGLETON || k == SEP_PTO
+ || k == BITVECTOR_TO_NAT || k == INT_TO_BITVECTOR || k == HO_APPLY
+ || k == SEQ_NTH;
}
bool Trigger::isRelationalTrigger( Node n ) {
return false;
}
}
- if( options::purifyDtTriggers() && t.getKind()==APPLY_SELECTOR_TOTAL ){
- return false;
- }
if (t.getKind() == HO_APPLY && t[0].getKind() == INST_CONSTANT)
{
return false;
}
return true;
- }else{
- return false;
}
+ return false;
}
//store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula
regress0/quantifiers/qcf-rel-dom-opt.smt2
regress0/quantifiers/quant-model-simplification.smt2
regress0/quantifiers/rew-to-scala.smt2
+ regress0/quantifiers/selector-trigger.smt2
regress0/quantifiers/simp-len.smt2
regress0/quantifiers/simp-typ-test.smt2
regress0/quantifiers/sygus-inst-nia-psyco-060.smt2
--- /dev/null
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatypes ((T 0)) (
+ ((Z) (Y (y Int)))))
+
+(declare-fun b () T)
+(declare-fun a () Int)
+
+(declare-fun P (Int) Bool)
+(assert (P (y b)))
+
+(assert (forall ((x T)) (not (P (y x)))))
+
+(check-sat)
projects / cvc5.git / commitdiff