This modifies our treatment of purification Skolems in the internal proof calculus. In particular, we now use an "unpurified form" instead of "original form" for defining Skolems. SKOLEM_INTRO is modified to prove the equality between a skolem and its unpurified form.
For example:
k1 purifies (ite A B C)
k2 purifies (+ k1 1)
The unpurified form of k2 is (+ k1 1), its original form is (+ (ite A B C) 1).
As a consequence:
(1) Our global skolem sharing is now slightly weaker, for example a k3 could be constructed whose unpurified form is (+ (ite A B C) 1); previously this would guaranteed to be k1.
(2) We do not require recursively computing the original form of terms when constructing purification Skolems,
(3) The witness form proof generator requires a fix point.
(4) The LFSC signature is simplified, and does not require a side condition to recursively compute the original form of a Skolem.
Fixes cvc5/LFSC#81.
(! r (^ (sc_substitute body v s) bodyi)
(holds (exists v u body))))))))))
-(declare skolem_intro (! u term
- (! t term
- (! r (^ (sc_mk_skolem t) u)
- (holds (= u t))))))
+(declare skolem_intro (! t term
+ (holds (= (skolem t) t))))
(emptystr tt)
(default ff)))
+;;-------------------- Skolem terms
+; The following side conditions are used for computing terms that define
+; Skolems, which are used in reductions. Notice that Skolem terms may use
+; terms that are not in original form, meaning that the definitions of Skolems
+; may themselves contain Skolems. This is to avoid the use of a side condition
+; for computing the original form of a term in the LFSC signature, which
+; naively is exponential.
+
; Get the term corresponding to the prefix of term s of fixed length n.
(program sc_skolem_prefix ((s term) (n term)) term
(str.substr s (int 0) n)
; Get the term corresponding to the suffix of s after the first occurrence of
; t in s.
(program sc_skolem_first_ctn_post ((s term) (t term)) term
- (sc_skolem_suffix_rem s (a.+ (str.len (sc_skolem_first_ctn_pre s t)) (a.+ (str.len t) (int 0)))))
+ (sc_skolem_suffix_rem s (a.+ (str.len (skolem (sc_skolem_first_ctn_pre s t))) (a.+ (str.len t) (int 0)))))
+
+;;-------------------- Utilities
; Head and tail for string concatenation. Fails if not a concatentation term.
(program sc_string_head ((t term)) term (nary_head f_str.++ t))
; Convert t into a str.++ application, if it is not already in n-ary form.
(program sc_string_nary_intro ((t term) (u sort)) term (nary_intro f_str.++ t (sc_mk_emptystr u)))
+;;-------------------- Reductions
+
; In the following, a "reduction predicate" refers to a formula that is used
; to axiomatize an extended string function in terms of (simpler) functions.
; Compute the reduction predicate for (str.substr x n m) of sort s.
(program sc_string_reduction_substr ((x term) (n term) (m term) (u sort)) term
- (let k (sc_mk_skolem (str.substr x n m))
+ (let k (skolem (str.substr x n m))
(let npm (a.+ n (a.+ m (int 0)))
- (let k1 (sc_mk_skolem (sc_skolem_prefix x n))
- (let k2 (sc_mk_skolem (sc_skolem_suffix_rem x npm))
+ (let k1 (skolem (sc_skolem_prefix x n))
+ (let k2 (skolem (sc_skolem_suffix_rem x npm))
(ite
; condition
(and (a.>= n (int 0))
; Compute the reduction predicate for (str.indexof x y n) of sort s.
(program sc_string_reduction_indexof ((x term) (y term) (n term) (u sort)) term
- (let k (sc_mk_skolem (str.indexof x y n))
+ (let k (skolem (str.indexof x y n))
(let xn (str.substr x n (a.- (str.len x) n))
- (let k1 (sc_mk_skolem (sc_skolem_first_ctn_pre xn y))
- (let k2 (sc_mk_skolem (sc_skolem_first_ctn_post xn y))
+ (let k1 (skolem (sc_skolem_first_ctn_pre xn y))
+ (let k2 (skolem (sc_skolem_first_ctn_post xn y))
(ite
(or (not (str.contains xn y))
(or (a.> n (str.len x))
; Returns the reduction predicate and purification equality for term t
; of sort s.
(program sc_string_reduction ((t term) (u sort)) term
- (and (sc_string_reduction_pred t u) (and (= t (sc_mk_skolem t)) true))
+ (and (sc_string_reduction_pred t u) (and (= t (skolem t)) true))
)
; Compute the eager reduction predicate for (str.contains t r) where s
; This is the formula:
; (ite (str.contains t r) (= t (str.++ sk1 r sk2)) (not (= t r)))
(program sc_string_eager_reduction_contains ((t term) (r term) (u sort)) term
- (let k1 (sc_mk_skolem (sc_skolem_first_ctn_pre t r))
- (let k2 (sc_mk_skolem (sc_skolem_first_ctn_post t r))
+ (let k1 (skolem (sc_skolem_first_ctn_pre t r))
+ (let k2 (skolem (sc_skolem_first_ctn_post t r))
(ite
(str.contains t r)
(= t (str.++ k1 (str.++ r (str.++ k2 (sc_mk_emptystr u)))))
((char n)
(= thead
(ifequal rev ff
- (str.++ s12 (str.++ (sc_mk_skolem (sc_skolem_suffix_rem thead (int 1))) emptystr))
- (str.++ (sc_mk_skolem (sc_skolem_prefix thead (a.- (str.len thead) (int 1)))) (str.++ s12 emptystr)))))))))
+ (str.++ s12 (str.++ (skolem (sc_skolem_suffix_rem thead (int 1))) emptystr))
+ (str.++ (skolem (sc_skolem_prefix thead (a.- (str.len thead) (int 1)))) (str.++ s12 emptystr)))))))))
(fail term))))
)
(default t)
))
-; Make a skolem, which ensures that the given term is in original form. For
-; consistency, we require that the witness term for all Skolems are in
-; original form. Failure to use this side condition when introducing fresh
-; Skolems will result in proofs failing to check due to mismatched uses of
-; Skolem variables in conclusions.
-(program sc_mk_skolem ((t term)) term (skolem (sc_to_original t)))
-
;; ---- Proof rules
; "proof-let", which is used to introduce a variable corresponding to the
};
typedef expr::Attribute<OriginalFormAttributeId, Node> OriginalFormAttribute;
+struct UnpurifiedFormAttributeId
+{
+};
+typedef expr::Attribute<UnpurifiedFormAttributeId, Node> UnpurifiedFormAttribute;
+
struct AbstractValueId
{
};
const std::string& comment,
int flags)
{
- Node to = getOriginalForm(t);
- // We do not currently insist that to does not contain witness terms
-
- Node k = mkSkolemInternal(to, prefix, comment, flags);
- // set original form attribute for k
- OriginalFormAttribute ofa;
- k.setAttribute(ofa, to);
+ // We do not recursively compute the original form of t here
+ Node k = mkSkolemInternal(t, prefix, comment, flags);
+ // set unpurified form attribute for k
+ UnpurifiedFormAttribute ufa;
+ k.setAttribute(ufa, t);
+ // the original form of k can be computed by calling getOriginalForm, but
+ // it is not computed here
Trace("sk-manager-skolem")
- << "skolem: " << k << " purify " << to << std::endl;
+ << "skolem: " << k << " purify " << t << std::endl;
return k;
}
Trace("sk-manager-debug")
<< "SkolemManager::getOriginalForm " << n << std::endl;
OriginalFormAttribute ofa;
+ UnpurifiedFormAttribute ufa;
NodeManager* nm = NodeManager::currentNM();
std::unordered_map<TNode, Node> visited;
std::unordered_map<TNode, Node>::iterator it;
{
visited[cur] = cur.getAttribute(ofa);
}
+ else if (cur.hasAttribute(ufa))
+ {
+ // if it has an unpurified form, compute the original form of it
+ Node ucur = cur.getAttribute(ufa);
+ if (ucur.hasAttribute(ofa))
+ {
+ // Already computed, set. This always happens after cur is visited
+ // again after computing the original form of its unpurified form.
+ Node ucuro = ucur.getAttribute(ofa);
+ cur.setAttribute(ofa, ucuro);
+ visited[cur] = ucuro;
+ }
+ else
+ {
+ // visit ucur then visit cur again
+ visit.push_back(cur);
+ visit.push_back(ucur);
+ }
+ }
else
{
visited[cur] = Node::null();
return visited[n];
}
+Node SkolemManager::getUnpurifiedForm(Node k)
+{
+ UnpurifiedFormAttribute ufa;
+ if (k.hasAttribute(ufa))
+ {
+ return k.getAttribute(ufa);
+ }
+ return k;
+}
+
Node SkolemManager::mkSkolemInternal(Node w,
const std::string& prefix,
const std::string& comment,
int flags = SKOLEM_DEFAULT,
ProofGenerator* pg = nullptr);
/**
- * Same as above, but for special case of (witness ((x T)) (= x t))
- * where T is the type of t. This skolem is unique for each t, which we
+ * Make purification skolem. This skolem is unique for each t, which we
* implement via an attribute on t. This attribute is used to ensure to
* associate a unique skolem for each t.
*
- * Notice that a purification skolem is trivial to justify, and hence it
- * does not require a proof generator.
+ * Notice that a purification skolem is trivial to justify (via SKOLEM_INTRO),
+ * and hence it does not require a proof generator.
*
- * Notice that in very rare cases, two different terms may have the
- * same purification skolem. For example, let k be the skolem introduced to
- * eliminate (ite A B C). Then, the pair of terms:
+ * Notice that we do not convert t to original form in this call. Thus,
+ * in very rare cases, two Skolems may be introduced that have the same
+ * original form. For example, let k be the skolem introduced to eliminate
+ * (ite A B C). Then, asking for the purify skolem for:
* (ite (ite A B C) D E) and (ite k D E)
- * have the same purification skolem. In the implementation, this is a result
- * of the fact that the above terms have the same original form. It is sound
- * to use the same skolem to purify these two terms, since they are
- * definitionally equivalent.
+ * will return two different Skolems.
*/
Node mkPurifySkolem(Node t,
const std::string& prefix,
* @return n in original form.
*/
static Node getOriginalForm(Node n);
+ /**
+ * Convert to unpurified form, which returns the term that k purifies. This
+ * is literally the term that was passed as an argument to mkPurify on the
+ * call that created k. In contrast to getOriginalForm, this is not recursive
+ * w.r.t. skolems, so that the term purified by k may itself contain
+ * purification skolems that are not expanded.
+ *
+ * @param k The skolem to convert to unpurified form
+ * @return the unpurified form of k.
+ */
+ static Node getUnpurifiedForm(Node k);
private:
/** Cache of skolem functions for mkSkolemFunction above. */
}
// skolems v print as their witness forms
// v is (skolem W) where W is the original or witness form of v
- Node wi = SkolemManager::getOriginalForm(n);
+ Node wi = SkolemManager::getUnpurifiedForm(n);
if (wi == n)
{
// if it is not a purification skolem, maybe it is a witness skolem
// quantifiers
case PfRule::SKOLEM_INTRO:
{
- pf << h << d_tproc.convert(SkolemManager::getOriginalForm(args[0]));
+ pf << d_tproc.convert(SkolemManager::getUnpurifiedForm(args[0]));
}
break;
// ---------- arguments of non-translated rules go here
*
* \inferrule{-\mid k}{k = t}
*
- * where :math:`t` is the original form of skolem :math:`k`.
+ * where :math:`t` is the unpurified form of skolem :math:`k`.
* \endverbatim
*/
SKOLEM_INTRO,
{
d_visited.insert(cur);
curw = SkolemManager::getOriginalForm(cur);
- // if its witness form is different
+ // if its original form is different
if (cur != curw)
{
if (cur.isVar())
{
+ curw = SkolemManager::getUnpurifiedForm(cur);
Node eq = cur.eqNode(curw);
- // equality between a variable and its original form
+ // equality between a variable and its unpurified form
d_eqs.insert(eq);
// ------- SKOLEM_INTRO
// k = t
d_wintroPf.addStep(eq, PfRule::SKOLEM_INTRO, {}, {cur});
d_tcpg.addRewriteStep(
cur, curw, &d_wintroPf, true, PfRule::ASSUME, true);
+ // recursively transform
+ visit.push_back(curw);
}
else
{
- // A term whose witness form is different from itself, recurse.
- // It should be the case that cur has children, since the witness
+ // A term whose original form is different from itself, recurse.
+ // It should be the case that cur has children, since the original
// form of constants are themselves.
Assert(cur.getNumChildren() > 0);
if (cur.hasOperator())
{
Assert(children.empty());
Assert(args.size() == 1);
- Node t = SkolemManager::getOriginalForm(args[0]);
+ Node t = SkolemManager::getUnpurifiedForm(args[0]);
return args[0].eqNode(t);
}
else if (id == PfRule::SKOLEMIZE)
projects / cvc5.git / commitdiff