Skip to content

Commit

Permalink
Simplify ProofRule::SKOLEMIZE (cvc5#10898)
Browse files Browse the repository at this point in the history
Changes:
- ProofRule::SKOLEMIZE only expects negated universals as premises.
- Skolems of id `QUANTIFIERS_SKOLEMIZE` take a universal instead of an
existential.

After doing this change, several BV invertibility condition benchmarks
became "unknown", since the witness term elimination introduced in
cvc5#10848 was not quite optimal: in
particular, the skolems introduced when eliminating witness for BV
invertibility condition instantiations would in rare cases not align
with the quantified formulas since we did not run theory preprocessing
on them. This fixes the issue by making the witness elimination take
this into account via a new callback in this utility.

---------

Co-authored-by: Abdalrhman Mohamed <[email protected]>
ajreynol and abdoo8080 authored Jul 17, 2024
1 parent 2cb0e95 commit 90eeba9
Showing 8 changed files with 66 additions and 60 deletions.
12 changes: 3 additions & 9 deletions include/cvc5/cvc5_proof_rule.h
Original file line number Diff line number Diff line change
@@ -1308,18 +1308,12 @@ enum ENUM(ProofRule)
*
* .. math::
*
* \inferrule{\exists x_1\dots x_n.\> F\mid -}{F\sigma}
*
* or
*
* .. math::
*
* \inferrule{\neg (\forall x_1\dots x_n.\> F)\mid -}{\neg F\sigma}
*
* where :math:`\sigma` maps :math:`x_1,\dots,x_n` to their representative
* skolems obtained by ``SkolemManager::mkSkolemize``, returned in the skolems
* argument of that method. The witness terms for the returned skolems can be
* obtained by ``SkolemManager::getWitnessForm``.
* skolems, which are skolems :math:`k_1,\dots,k_n`. For each :math:`k_i`,
* its skolem identifier is :cpp:enumerator:`QUANTIFIERS_SKOLEMIZE <cvc5::SkolemId::QUANTIFIERS_SKOLEMIZE>`,
* and its indices are :math:`(\forall x_1\dots x_n.\> F)` and :math:`x_i`.
* \endverbatim
*/
EVALUE(SKOLEMIZE),
2 changes: 1 addition & 1 deletion include/cvc5/cvc5_skolem_id.h
Original file line number Diff line number Diff line change
@@ -175,7 +175,7 @@ enum ENUM(SkolemId)
*/
EVALUE(SHARED_SELECTOR),
/**
* The n^th skolem for quantified formula Q.
* The n^th skolem for the negation of universally quantified formula Q.
*
* - Number of skolem indices: ``2``
* - ``1:`` The quantified formula Q.
14 changes: 4 additions & 10 deletions proofs/alf/cvc5/rules/Quantifiers.smt3
Original file line number Diff line number Diff line change
@@ -35,16 +35,10 @@
; - Q Bool: The quantified formula to skolemize. This is either an existential or a negated universal.
; conclusion: >
; The skolemized body of Q, where its variables are replaced by skolems
; introduced via $mk_skolems,
(declare-rule skolemize ((F Bool))
:premises (F)
:conclusion
(alf.match ((T Type) (x @List) (G Bool))
F
(
((exists x G) ($substitute_list x ($mk_skolems x F) G))
((not (forall x G)) ($substitute_list x ($mk_skolems x (exists x (not G))) (not G)))
))
; introduced via $mk_skolems.
(declare-rule skolemize ((x @List) (G Bool))
:premises ((not (forall x G)))
:conclusion ($substitute_list x ($mk_skolems x (forall x G)) (not G))
)

; rule: skolem_intro
13 changes: 9 additions & 4 deletions src/expr/elim_witness_converter.cpp
Original file line number Diff line number Diff line change
@@ -32,14 +32,19 @@ Node ElimWitnessNodeConverter::postConvert(Node n)
NodeManager* nm = nodeManager();
SkolemManager* skm = nm->getSkolemManager();
std::vector<Node> nchildren(n.begin(), n.end());
Node exists = nm->mkNode(Kind::EXISTS, nchildren);
Node k = skm->mkSkolemFunction(SkolemId::QUANTIFIERS_SKOLEMIZE,
{exists, n[0][0]});
d_exists.push_back(exists);
nchildren[1] = nchildren[1].notNode();
Node q = nm->mkNode(Kind::FORALL, nchildren);
Node qn = getNormalFormFor(q);
Node k =
skm->mkSkolemFunction(SkolemId::QUANTIFIERS_SKOLEMIZE, {qn, n[0][0]});
d_exists.push_back(qn.notNode());
return k;
}
return n;
}

Node ElimWitnessNodeConverter::getNormalFormFor(const Node& q) { return q; }

const std::vector<Node>& ElimWitnessNodeConverter::getExistentials() const
{
return d_exists;
6 changes: 6 additions & 0 deletions src/expr/elim_witness_converter.h
Original file line number Diff line number Diff line change
@@ -45,6 +45,12 @@ class ElimWitnessNodeConverter : protected EnvObj, public NodeConverter
*/
const std::vector<Node>& getExistentials() const;

/**
* Get the normal form of a quantified formula for which we are introducing
* a skolem variable based on eliminating a witness term.
*/
virtual Node getNormalFormFor(const Node& q);

private:
/** The list of existentials introduced by eliminating witness */
std::vector<Node> d_exists;
30 changes: 29 additions & 1 deletion src/theory/quantifiers/cegqi/ceg_instantiator.cpp
Original file line number Diff line number Diff line change
@@ -941,6 +941,34 @@ bool CegInstantiator::constructInstantiationInc(Node pv,
}
}

/**
* A class for eliminating witness terms. We require overriding the method of
* the base class to ensure that quantified formulas have been run through
* theory preprocessing. This ensures that the skolem variables introduced
* align exactly with the quantified formula we will assert in the corresponding
* QUANTIFIERS_CEGQI_WITNESS lemma.
*/
class PreprocessElimWitnessNodeConverter : public ElimWitnessNodeConverter
{
public:
PreprocessElimWitnessNodeConverter(Env& env, Valuation& val)
: ElimWitnessNodeConverter(env), d_val(val)
{
}
/**
* Get the normal form for quantified formula q, which must perform theory
* preprocessing.
*/
Node getNormalFormFor(const Node& q) override
{
return d_val.getPreprocessedTerm(q);
}

private:
/** Reference to a valuation */
Valuation& d_val;
};

bool CegInstantiator::doAddInstantiation(std::vector<Node>& vars,
std::vector<Node>& subs)
{
@@ -983,7 +1011,7 @@ bool CegInstantiator::doAddInstantiation(std::vector<Node>& vars,
{
if (expr::hasSubtermKind(Kind::WITNESS, s))
{
ElimWitnessNodeConverter ewc(d_env);
PreprocessElimWitnessNodeConverter ewc(d_env, d_qstate.getValuation());
Node sc = ewc.convert(s);
const std::vector<Node>& wexists = ewc.getExistentials();
exists.insert(exists.end(), wexists.begin(), wexists.end());
27 changes: 8 additions & 19 deletions src/theory/quantifiers/proof_checker.cpp
Original file line number Diff line number Diff line change
@@ -45,7 +45,6 @@ Node QuantifiersProofRuleChecker::checkInternal(
const std::vector<Node>& children,
const std::vector<Node>& args)
{
NodeManager* nm = nodeManager();
if (id == ProofRule::SKOLEM_INTRO)
{
Assert(children.empty());
@@ -57,28 +56,18 @@ Node QuantifiersProofRuleChecker::checkInternal(
{
Assert(children.size() == 1);
Assert(args.empty());
// can use either negated FORALL or EXISTS
if (children[0].getKind() != Kind::EXISTS
&& (children[0].getKind() != Kind::NOT
|| children[0][0].getKind() != Kind::FORALL))
// must use negated FORALL
if (children[0].getKind() != Kind::NOT
|| children[0][0].getKind() != Kind::FORALL)
{
return Node::null();
}
Node exists;
if (children[0].getKind() == Kind::EXISTS)
{
exists = children[0];
}
else
{
std::vector<Node> echildren(children[0][0].begin(), children[0][0].end());
echildren[1] = echildren[1].notNode();
exists = nm->mkNode(Kind::EXISTS, echildren);
}
std::vector<Node> vars(exists[0].begin(), exists[0].end());
std::vector<Node> skolems = Skolemize::getSkolemConstants(exists);
Node res = exists[1].substitute(
Node q = children[0][0];
std::vector<Node> vars(q[0].begin(), q[0].end());
std::vector<Node> skolems = Skolemize::getSkolemConstants(q);
Node res = q[1].substitute(
vars.begin(), vars.end(), skolems.begin(), skolems.end());
res = res.notNode();
return res;
}
else if (id == ProofRule::INSTANTIATE)
22 changes: 6 additions & 16 deletions src/theory/quantifiers/skolemize.cpp
Original file line number Diff line number Diff line change
@@ -64,17 +64,15 @@ TrustNode Skolemize::process(Node q)
// if using proofs and not using induction, we use the justified
// skolemization
NodeManager* nm = NodeManager::currentNM();
std::vector<Node> echildren(q.begin(), q.end());
echildren[1] = echildren[1].notNode();
Node existsq = nm->mkNode(Kind::EXISTS, echildren);
std::vector<Node> vars(existsq[0].begin(), existsq[0].end());
// cache the skolems in d_skolem_constants[q]
std::vector<Node>& skolems = d_skolem_constants[q];
skolems = getSkolemConstants(existsq);
Node res = existsq[1].substitute(
skolems = getSkolemConstants(q);
std::vector<Node> vars(q[0].begin(), q[0].end());
Node res = q[1].substitute(
vars.begin(), vars.end(), skolems.begin(), skolems.end());
Node qnot = q.notNode();
CDProof cdp(d_env);
res = res.notNode();
cdp.addStep(res, ProofRule::SKOLEMIZE, {qnot}, {});
std::shared_ptr<ProofNode> pf = cdp.getProofFor(res);
std::vector<Node> assumps;
@@ -106,15 +104,7 @@ TrustNode Skolemize::process(Node q)

std::vector<Node> Skolemize::getSkolemConstants(const Node& q)
{
if (q.getKind()==Kind::FORALL)
{
std::vector<Node> echildren(q.begin(), q.end());
echildren[1] = echildren[1].notNode();
NodeManager* nm = NodeManager::currentNM();
Node existsq = nm->mkNode(Kind::EXISTS, echildren);
return getSkolemConstants(existsq);
}
Assert(q.getKind() == Kind::EXISTS);
Assert(q.getKind() == Kind::FORALL);
std::vector<Node> skolems;
for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
{
@@ -125,7 +115,7 @@ std::vector<Node> Skolemize::getSkolemConstants(const Node& q)

Node Skolemize::getSkolemConstant(const Node& q, size_t i)
{
Assert(q.getKind() == Kind::EXISTS);
Assert(q.getKind() == Kind::FORALL);
Assert(i < q[0].getNumChildren());
NodeManager* nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();

0 comments on commit 90eeba9

Please sign in to comment.