projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
f416c88
)
Minor changes to E-matching utilities (#7062)
author
Andrew Reynolds
<andrew.j.reynolds@gmail.com>
Wed, 15 Sep 2021 18:08:27 +0000
(13:08 -0500)
committer
GitHub
<noreply@github.com>
Wed, 15 Sep 2021 18:08:27 +0000
(15:08 -0300)
src/theory/quantifiers/ematching/candidate_generator.h
patch
|
blob
|
history
src/theory/quantifiers/ematching/inst_match_generator.cpp
patch
|
blob
|
history
src/theory/quantifiers/ematching/pattern_term_selector.cpp
patch
|
blob
|
history
diff --git
a/src/theory/quantifiers/ematching/candidate_generator.h
b/src/theory/quantifiers/ematching/candidate_generator.h
index 12c667fb56823a4636429422e8cf46474d2dc327..4272c048466dfc88b2850564159e5eee14821578 100644
(file)
--- a/
src/theory/quantifiers/ematching/candidate_generator.h
+++ b/
src/theory/quantifiers/ematching/candidate_generator.h
@@
-73,6
+73,8
@@
class CandidateGenerator {
virtual Node getNextCandidate() = 0;
/** is n a legal candidate? */
bool isLegalCandidate(Node n);
virtual Node getNextCandidate() = 0;
/** is n a legal candidate? */
bool isLegalCandidate(Node n);
+ /** Identify this generator (for debugging, etc..) */
+ virtual std::string identify() const = 0;
protected:
/** Reference to the quantifiers state */
protected:
/** Reference to the quantifiers state */
@@
-106,6
+108,9
@@
class CandidateGeneratorQE : public CandidateGenerator
{
return d_exclude_eqc.find(r) != d_exclude_eqc.end();
}
{
return d_exclude_eqc.find(r) != d_exclude_eqc.end();
}
+ /** Identify this generator (for debugging, etc..) */
+ std::string identify() const override { return "CandidateGeneratorQE"; }
+
protected:
/** reset this class for matching operator op in equivalence class eqc */
void resetForOperator(Node eqc, Node op);
protected:
/** reset this class for matching operator op in equivalence class eqc */
void resetForOperator(Node eqc, Node op);
@@
-153,6
+158,8
@@
class CandidateGeneratorQELitDeq : public CandidateGenerator
void reset(Node eqc) override;
/** get next candidate */
Node getNextCandidate() override;
void reset(Node eqc) override;
/** get next candidate */
Node getNextCandidate() override;
+ /** Identify this generator (for debugging, etc..) */
+ std::string identify() const override { return "CandidateGeneratorQELitDeq"; }
private:
/** the equality class iterator for false */
private:
/** the equality class iterator for false */
@@
-182,6
+189,8
@@
class CandidateGeneratorQEAll : public CandidateGenerator
unsigned d_index;
//first time
bool d_firstTime;
unsigned d_index;
//first time
bool d_firstTime;
+ /** Identify this generator (for debugging, etc..) */
+ std::string identify() const override { return "CandidateGeneratorQEAll"; }
public:
CandidateGeneratorQEAll(QuantifiersState& qs, TermRegistry& tr, Node mpat);
public:
CandidateGeneratorQEAll(QuantifiersState& qs, TermRegistry& tr, Node mpat);
@@
-209,6
+218,11
@@
class CandidateGeneratorConsExpand : public CandidateGeneratorQE
void reset(Node eqc) override;
/** get next candidate */
Node getNextCandidate() override;
void reset(Node eqc) override;
/** get next candidate */
Node getNextCandidate() override;
+ /** Identify this generator (for debugging, etc..) */
+ std::string identify() const override
+ {
+ return "CandidateGeneratorConsExpand";
+ }
protected:
/** the (datatype) type of the input match pattern */
protected:
/** the (datatype) type of the input match pattern */
@@
-234,6
+248,9
@@
class CandidateGeneratorSelector : public CandidateGeneratorQE
* application of the wrong constructor.
*/
Node getNextCandidate() override;
* application of the wrong constructor.
*/
Node getNextCandidate() override;
+ /** Identify this generator (for debugging, etc..) */
+ std::string identify() const override { return "CandidateGeneratorSelector"; }
+
protected:
/** the selector operator */
Node d_selOp;
protected:
/** the selector operator */
Node d_selOp;
diff --git
a/src/theory/quantifiers/ematching/inst_match_generator.cpp
b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 5f76d5289cdb13d9644dfa1b3371b76b69bdeffe..5380fc7d5f21b32afb6753625c13ba292159e7ec 100644
(file)
--- a/
src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/
src/theory/quantifiers/ematching/inst_match_generator.cpp
@@
-271,6
+271,9
@@
void InstMatchGenerator::initialize(Node q,
Trace("inst-match-gen-warn")
<< "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
}
Trace("inst-match-gen-warn")
<< "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
}
+ Trace("inst-match-gen") << "Candidate generator is "
+ << (d_cg != nullptr ? d_cg->identify() : "null")
+ << std::endl;
gens.insert( gens.end(), d_children.begin(), d_children.end() );
}
gens.insert( gens.end(), d_children.begin(), d_children.end() );
}
diff --git
a/src/theory/quantifiers/ematching/pattern_term_selector.cpp
b/src/theory/quantifiers/ematching/pattern_term_selector.cpp
index 83234d1153a8d2db96c05e76d1e610b86a2138de..332346f3fea699389f3b5dd0d4f2d36fbb22d250 100644
(file)
--- a/
src/theory/quantifiers/ematching/pattern_term_selector.cpp
+++ b/
src/theory/quantifiers/ematching/pattern_term_selector.cpp
@@
-60,7
+60,6
@@
bool PatternTermSelector::isUsable(Node n, Node q)
{
return true;
}
{
return true;
}
- std::map<Node, Node> coeffs;
if (options::purifyTriggers())
{
Node x = getInversionVariable(n);
if (options::purifyTriggers())
{
Node x = getInversionVariable(n);
@@
-82,7
+81,7
@@
Node PatternTermSelector::getIsUsableEq(Node q, Node n)
if (i == 1 && n.getKind() == EQUAL
&& !quantifiers::TermUtil::hasInstConstAttr(n[0]))
{
if (i == 1 && n.getKind() == EQUAL
&& !quantifiers::TermUtil::hasInstConstAttr(n[0]))
{
- return NodeManager::currentNM()->mkNode(
n.getKind()
, n[1], n[0]);
+ return NodeManager::currentNM()->mkNode(
EQUAL
, n[1], n[0]);
}
else
{
}
else
{