It makes the skolem definition manager more robust so that skolem definitions can be added for skolems that have already appeared in asserted literals. This was the initial motivation for the change in ordering. As a result, fixes #8347 and fixes cvc5/cvc5-projects#512. It also optimizes this class in a few ways.
It also comments more on the change to PropEngine introduced here: #8301 which led to performance degradation on a set of string benchmarks of interest.
const std::vector<theory::SkolemLemma>& ppLemmas,
bool removable)
{
- // Assert to decision engine. Notice this must come before the calls to
- // assertTrustedLemmaInternal below, since the decision engine requires
- // setting up information about the relevance of skolems before literals
- // are potentially asserted to the theory engine, which it listens to for
- // tracking active skolem definitions.
+ // Assert to decision engine first.
+ // Note that this order is important for theories that send lemmas during
+ // preregistration, as it impacts the order in which lemmas are processed
+ // by default by the decision engine. In particular, sending to the SAT
+ // solver first means that lemmas sent during preregistration in response to
+ // the current lemma are processed after that lemma. This makes a difference
+ // e.g. for string reduction lemmas, where preregistration lemmas are
+ // introduced for skolems that appear in reductions. Moving this
+ // block after the one below has mixed (trending negative) performance on
+ // SMT-LIB strings logics.
if (!removable)
{
// also add to the decision engine, where notice we don't need proofs
// equivalent up to purification
if (d_skDefs.find(skolem) == d_skDefs.end())
{
- // should not have already computed whether the skolem has skolems, or else
- // our computation of hasSkolems is wrong after adding this definition
- Assert(d_hasSkolems.find(skolem) == d_hasSkolems.end());
d_skDefs.insert(skolem, def);
}
}
}
void SkolemDefManager::notifyAsserted(TNode literal,
- std::vector<TNode>& activatedSkolems,
- bool useDefs)
+ std::vector<TNode>& activatedSkolems)
{
- std::unordered_set<Node> skolems;
- getSkolems(literal, skolems);
- Trace("sk-defs") << "notifyAsserted: " << literal << " has skolems "
- << skolems << std::endl;
- for (const Node& k : skolems)
+ if (d_skActive.size() == d_skDefs.size())
{
- if (d_skActive.find(k) != d_skActive.end())
+ // already activated all skolems
+ return;
+ }
+ std::unordered_set<Node> defs;
+ getSkolems(literal, defs, true);
+ Trace("sk-defs") << "notifyAsserted: " << literal << " has skolems " << defs
+ << std::endl;
+ for (const Node& d : defs)
+ {
+ if (d_skActive.find(d) != d_skActive.end())
{
// already active
continue;
}
- d_skActive.insert(k);
- Trace("sk-defs") << "...activate " << k << std::endl;
- if (useDefs)
- {
- // add its definition to the activated list
- NodeNodeMap::const_iterator it = d_skDefs.find(k);
- Assert(it != d_skDefs.end());
- activatedSkolems.push_back(it->second);
- }
- else
- {
- // add to the activated list
- activatedSkolems.push_back(k);
- }
+ d_skActive.insert(d);
+ Trace("sk-defs") << "...activate " << d << std::endl;
+ // add its definition to the activated list
+ activatedSkolems.push_back(d);
}
}
if (cur.getNumChildren() == 0)
{
visit.pop_back();
- bool hasSkolem = false;
- if (cur.isVar())
+ Kind ck = cur.getKind();
+ // We have skolems if we are a skolem that has a definition, or
+ // we are a Boolean term variable. For Boolean term variables, we do
+ // not make this test depend on whether the skolem has a definition,
+ // since that is prone to change if the Boolean term variable was
+ // introduced in a lemma prior to its definition being introduced.
+ // This is for example the case in strings reduction for Booleans,
+ // ground term purification for E-matching, etc.
+ if (ck == kind::SKOLEM)
+ {
+ d_hasSkolems[cur] = (d_skDefs.find(cur) != d_skDefs.end());
+ }
+ else
{
- hasSkolem = (d_skDefs.find(cur) != d_skDefs.end());
+ d_hasSkolems[cur] = (ck == kind::BOOLEAN_TERM_VARIABLE);
}
- d_hasSkolems[cur] = hasSkolem;
}
else
{
return d_hasSkolems[n];
}
-void SkolemDefManager::getSkolems(TNode n, std::unordered_set<Node>& skolems)
+void SkolemDefManager::getSkolems(TNode n,
+ std::unordered_set<Node>& skolems,
+ bool useDefs)
{
+ NodeNodeMap::const_iterator itd;
std::unordered_set<TNode> visited;
std::unordered_set<TNode>::iterator it;
std::vector<TNode> visit;
visited.insert(cur);
if (cur.isVar())
{
- if (d_skDefs.find(cur) != d_skDefs.end())
+ itd = d_skDefs.find(cur);
+ if (itd != d_skDefs.end())
{
- skolems.insert(cur);
+ skolems.insert(useDefs ? itd->second : Node(cur));
}
continue;
}
* is active in the SAT context if it appears in an asserted literal.
*
* @param literal The literal that became asserted
- * @param activatedSkolems The list to add skolems to
- * @param useDefs If this flag is true, we add the skolem definition for
- * skolems to activatedSkolems instead of the skolem itself.
+ * @param activatedDefs The list to add skolem definitions to
*/
- void notifyAsserted(TNode literal,
- std::vector<TNode>& activatedSkolems,
- bool useDefs = false);
+ void notifyAsserted(TNode literal, std::vector<TNode>& activatedDefs);
/**
* Get the set of skolems maintained by this class that occur in node n,
*
* @param n The node to traverse
* @param skolems The set where the skolems are added
+ * @param useDefs Whether to add definitions for the skolems instead of the
+ * skolems
*/
- void getSkolems(TNode n, std::unordered_set<Node>& skolems);
+ void getSkolems(TNode n,
+ std::unordered_set<Node>& skolems,
+ bool useDefs = false);
/**
* Does n have skolems having definitions managed by this class? Should call
* this method *after* notifying skolem definitions for all potential
private:
/** skolems to definitions (user-context dependent) */
NodeNodeMap d_skDefs;
- /** set of active skolems (SAT-context dependent) */
+ /** set of active skolem definitions (SAT-context dependent) */
NodeSet d_skActive;
/** Cache for hasSkolems */
NodeBoolMap d_hasSkolems;
// Assertion makes all skolems in assertion active,
// which triggers their definitions to becoming active.
std::vector<TNode> activeSkolemDefs;
- d_skdm->notifyAsserted(assertion, activeSkolemDefs, true);
- // notify the decision engine of the skolem definitions that have become
- // active due to the assertion.
- d_decisionEngine->notifyActiveSkolemDefs(activeSkolemDefs);
+ d_skdm->notifyAsserted(assertion, activeSkolemDefs);
+ if (!activeSkolemDefs.empty())
+ {
+ // notify the decision engine of the skolem definitions that have become
+ // active due to the assertion.
+ d_decisionEngine->notifyActiveSkolemDefs(activeSkolemDefs);
+ }
}
}
if (!d_stopSearch.get())
regress0/quantifiers/nested-inf.smt2
regress0/quantifiers/partial-trigger.smt2
regress0/quantifiers/proj-issue152-2-non-std-nterm-ext-rew.smt2
+ regress0/quantifiers/proj-issue512-has-skolem.smt2
regress0/quantifiers/pure_dt_cbqi.smt2
regress0/quantifiers/qarray-sel-over-store.smt2
regress0/quantifiers/qbv-inequality2.smt2
regress1/strings/issue7677-test-const-rv.smt2
regress1/strings/issue7918-learned-rewrite.smt2
regress1/strings/issue8094-witness-model.smt2
+ regress1/strings/issue8347-has-skolem.smt2
regress1/strings/issue8434-nterm-str-rw.smt2
regress1/strings/kaluza-fl.smt2
regress1/strings/loop002.smt2
--- /dev/null
+; EXPECT: sat
+(set-logic ALL)
+(set-option :fmf-bound true)
+(declare-fun x (Bool Bool) Bool)
+(assert (forall ((x4 Bool)) (x x4 (x false false))))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --strings-exp -i
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun uf6_2 (Bool Bool Bool Bool Bool Bool) Bool)
+(declare-fun str2 () String)
+(declare-fun str6 () String)
+(assert (str.in_re str2 re.allchar))
+(assert (str.<= str2 str6))
+(check-sat)
+(assert (uf6_2 true false true false false (str.<= str2 str6)))
+(push)
projects / cvc5.git / commitdiff