Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/theory_proof_step_buffer.cpp	Lines:	81	100	81.0 %
Date:	2021-05-22	Branches:	140	342	40.9 %


/******************************************************************************
 * Top contributors (to current version):
 *   Haniel Barbosa, Andrew Reynolds, Aina Niemetz
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Implementation of theory proof step buffer utility.
 */

#include "theory/theory_proof_step_buffer.h"

#include "expr/proof.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {

TheoryProofStepBuffer::TheoryProofStepBuffer(ProofChecker* pc)
    : ProofStepBuffer(pc)
{
}

bool TheoryProofStepBuffer::applyEqIntro(Node src,
                                         Node tgt,
                                         const std::vector<Node>& exp,
                                         MethodId ids,
                                         MethodId ida,
                                         MethodId idr)
{
  std::vector<Node> args;
  args.push_back(src);
  builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr);
  Node res = tryStep(PfRule::MACRO_SR_EQ_INTRO, exp, args);
  if (res.isNull())
  {
    // failed to apply
    return false;
  }
  // should have concluded the expected equality
  Node expected = src.eqNode(tgt);
  if (res != expected)
  {
    // did not provide the correct target
    popStep();
    return false;
  }
  // successfully proved src == tgt.
  return true;
}

bool TheoryProofStepBuffer::applyPredTransform(Node src,
                                               Node tgt,
                                               const std::vector<Node>& exp,
                                               MethodId ids,
                                               MethodId ida,
                                               MethodId idr)
{
  // symmetric equalities
  if (CDProof::isSame(src, tgt))
  {
    return true;
  }
  std::vector<Node> children;
  children.push_back(src);
  std::vector<Node> args;
  // try to prove that tgt rewrites to src
  children.insert(children.end(), exp.begin(), exp.end());
  args.push_back(tgt);
  builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr);
  Node res = tryStep(PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
  if (res.isNull())
  {
    // failed to apply
    return false;
  }
  // should definitely have concluded tgt
  Assert(res == tgt);
  return true;
}

bool TheoryProofStepBuffer::applyPredIntro(Node tgt,
                                           const std::vector<Node>& exp,
                                           MethodId ids,
                                           MethodId ida,
                                           MethodId idr)
{
  std::vector<Node> args;
  args.push_back(tgt);
  builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr);
  Node res = tryStep(PfRule::MACRO_SR_PRED_INTRO, exp, args);
  if (res.isNull())
  {
    return false;
  }
  Assert(res == tgt);
  return true;
}

Node TheoryProofStepBuffer::applyPredElim(Node src,
                                          const std::vector<Node>& exp,
                                          MethodId ids,
                                          MethodId ida,
                                          MethodId idr)
{
  std::vector<Node> children;
  children.push_back(src);
  children.insert(children.end(), exp.begin(), exp.end());
  std::vector<Node> args;
  builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr);
  Node srcRew = tryStep(PfRule::MACRO_SR_PRED_ELIM, children, args);
  if (CDProof::isSame(src, srcRew))
  {
    popStep();
  }
  return srcRew;
}

Node TheoryProofStepBuffer::factorReorderElimDoubleNeg(Node n)
{
  if (n.getKind() != kind::OR)
  {
    return elimDoubleNegLit(n);
  }
  NodeManager* nm = NodeManager::currentNM();
  std::vector<Node> children{n.begin(), n.end()};
  std::vector<Node> childrenEqs;
  // eliminate double neg for each lit. Do it first because it may expose
  // duplicates
  bool hasDoubleNeg = false;
  for (unsigned i = 0; i < children.size(); ++i)
  {
    if (children[i].getKind() == kind::NOT
        && children[i][0].getKind() == kind::NOT)
    {
      hasDoubleNeg = true;
      childrenEqs.push_back(children[i].eqNode(children[i][0][0]));
      addStep(PfRule::MACRO_SR_PRED_INTRO,
              {},
              {childrenEqs.back()},
              childrenEqs.back());
      // update child
      children[i] = children[i][0][0];
    }
    else
    {
      childrenEqs.push_back(children[i].eqNode(children[i]));
      addStep(PfRule::REFL, {}, {children[i]}, childrenEqs.back());
    }
  }
  if (hasDoubleNeg)
  {
    Node oldn = n;
    n = nm->mkNode(kind::OR, children);
    // Create a congruence step to justify replacement of each doubly negated
    // literal. This is done to avoid having to use MACRO_SR_PRED_TRANSFORM
    // from the old clause to the new one, which, under the standard rewriter,
    // may not hold. An example is
    //
    //   ---------------------------------------------------------------------
    //   (or (or (not x2) x1 x2) (not (not x2))) = (or (or (not x2) x1 x2) x2)
    //
    // which fails due to factoring not happening after flattening.
    //
    // Using congruence only the
    //
    //  ------------------ MACRO_SR_PRED_INTRO
    //  (not (not t)) = t
    //
    // steps are added, which, since double negation is eliminated in a
    // pre-rewrite in the Boolean rewriter, will always hold under the
    // standard rewriter.
    Node congEq = oldn.eqNode(n);
    addStep(PfRule::CONG,
            childrenEqs,
            {ProofRuleChecker::mkKindNode(kind::OR)},
            congEq);
    // add an equality resolution step to derive normalize clause
    addStep(PfRule::EQ_RESOLVE, {oldn, congEq}, {}, n);
  }
  children.clear();
  // remove duplicates while keeping the order of children
  std::unordered_set<TNode> clauseSet;
  unsigned size = n.getNumChildren();
  for (unsigned i = 0; i < size; ++i)
  {
    if (clauseSet.count(n[i]))
    {
      continue;
    }
    children.push_back(n[i]);
    clauseSet.insert(n[i]);
  }
  // if factoring changed
  if (children.size() < size)
  {
    Node factored = children.empty()
                        ? nm->mkConst<bool>(false)
                        : children.size() == 1 ? children[0]
                                               : nm->mkNode(kind::OR, children);
    // don't overwrite what already has a proof step to avoid cycles
    addStep(PfRule::FACTORING, {n}, {}, factored);
    n = factored;
  }
  // nothing to order
  if (children.size() < 2)
  {
    return n;
  }
  // order
  std::sort(children.begin(), children.end());
  Node ordered = nm->mkNode(kind::OR, children);
  // if ordering changed
  if (ordered != n)
  {
    // don't overwrite what already has a proof step to avoid cycles
    addStep(PfRule::REORDERING, {n}, {ordered}, ordered);
  }
  return ordered;
}

Node TheoryProofStepBuffer::elimDoubleNegLit(Node n)
{
  // eliminate double neg
  if (n.getKind() == kind::NOT && n[0].getKind() == kind::NOT)
  {
    addStep(PfRule::NOT_NOT_ELIM, {n}, {}, n[0][0]);
    return n[0][0];
  }
  return n;
}

}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Haniel Barbosa, Andrew Reynolds, Aina Niemetz
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Implementation of theory proof step buffer utility.
14		*/
15
16		#include "theory/theory_proof_step_buffer.h"
17
18		#include "expr/proof.h"
19
20		using namespace cvc5::kind;
21
22		namespace cvc5 {
23		namespace theory {
24
25	9749	TheoryProofStepBuffer::TheoryProofStepBuffer(ProofChecker* pc)
26	9749	: ProofStepBuffer(pc)
27		{
28	9749	}
29
30	10761	bool TheoryProofStepBuffer::applyEqIntro(Node src,
31		Node tgt,
32		const std::vector<Node>& exp,
33		MethodId ids,
34		MethodId ida,
35		MethodId idr)
36		{
37	21522	std::vector<Node> args;
38	10761	args.push_back(src);
39	10761	builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr);
40	21522	Node res = tryStep(PfRule::MACRO_SR_EQ_INTRO, exp, args);
41	10761	if (res.isNull())
42		{
43		// failed to apply
44		return false;
45		}
46		// should have concluded the expected equality
47	21522	Node expected = src.eqNode(tgt);
48	10761	if (res != expected)
49		{
50		// did not provide the correct target
51		popStep();
52		return false;
53		}
54		// successfully proved src == tgt.
55	10761	return true;
56		}
57
58	2031	bool TheoryProofStepBuffer::applyPredTransform(Node src,
59		Node tgt,
60		const std::vector<Node>& exp,
61		MethodId ids,
62		MethodId ida,
63		MethodId idr)
64		{
65		// symmetric equalities
66	2031	if (CDProof::isSame(src, tgt))
67		{
68	578	return true;
69		}
70	2906	std::vector<Node> children;
71	1453	children.push_back(src);
72	2906	std::vector<Node> args;
73		// try to prove that tgt rewrites to src
74	1453	children.insert(children.end(), exp.begin(), exp.end());
75	1453	args.push_back(tgt);
76	1453	builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr);
77	2906	Node res = tryStep(PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
78	1453	if (res.isNull())
79		{
80		// failed to apply
81	108	return false;
82		}
83		// should definitely have concluded tgt
84	1345	Assert(res == tgt);
85	1345	return true;
86		}
87
88		bool TheoryProofStepBuffer::applyPredIntro(Node tgt,
89		const std::vector<Node>& exp,
90		MethodId ids,
91		MethodId ida,
92		MethodId idr)
93		{
94		std::vector<Node> args;
95		args.push_back(tgt);
96		builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr);
97		Node res = tryStep(PfRule::MACRO_SR_PRED_INTRO, exp, args);
98		if (res.isNull())
99		{
100		return false;
101		}
102		Assert(res == tgt);
103		return true;
104		}
105
106	89	Node TheoryProofStepBuffer::applyPredElim(Node src,
107		const std::vector<Node>& exp,
108		MethodId ids,
109		MethodId ida,
110		MethodId idr)
111		{
112	178	std::vector<Node> children;
113	89	children.push_back(src);
114	89	children.insert(children.end(), exp.begin(), exp.end());
115	178	std::vector<Node> args;
116	89	builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr);
117	89	Node srcRew = tryStep(PfRule::MACRO_SR_PRED_ELIM, children, args);
118	89	if (CDProof::isSame(src, srcRew))
119		{
120	21	popStep();
121		}
122	178	return srcRew;
123		}
124
125	377534	Node TheoryProofStepBuffer::factorReorderElimDoubleNeg(Node n)
126		{
127	377534	if (n.getKind() != kind::OR)
128		{
129		return elimDoubleNegLit(n);
130		}
131	377534	NodeManager* nm = NodeManager::currentNM();
132	755068	std::vector<Node> children{n.begin(), n.end()};
133	755068	std::vector<Node> childrenEqs;
134		// eliminate double neg for each lit. Do it first because it may expose
135		// duplicates
136	377534	bool hasDoubleNeg = false;
137	1662452	for (unsigned i = 0; i < children.size(); ++i)
138		{
139	2569836	if (children[i].getKind() == kind::NOT
140	2569836	&& children[i][0].getKind() == kind::NOT)
141		{
142	157363	hasDoubleNeg = true;
143	157363	childrenEqs.push_back(children[i].eqNode(children[i][0][0]));
144	629452	addStep(PfRule::MACRO_SR_PRED_INTRO,
145		{},
146	157363	{childrenEqs.back()},
147	314726	childrenEqs.back());
148		// update child
149	157363	children[i] = children[i][0][0];
150		}
151		else
152		{
153	1127555	childrenEqs.push_back(children[i].eqNode(children[i]));
154	1127555	addStep(PfRule::REFL, {}, {children[i]}, childrenEqs.back());
155		}
156		}
157	377534	if (hasDoubleNeg)
158		{
159	94172	Node oldn = n;
160	47086	n = nm->mkNode(kind::OR, children);
161		// Create a congruence step to justify replacement of each doubly negated
162		// literal. This is done to avoid having to use MACRO_SR_PRED_TRANSFORM
163		// from the old clause to the new one, which, under the standard rewriter,
164		// may not hold. An example is
165		//
166		// ---------------------------------------------------------------------
167		// (or (or (not x2) x1 x2) (not (not x2))) = (or (or (not x2) x1 x2) x2)
168		//
169		// which fails due to factoring not happening after flattening.
170		//
171		// Using congruence only the
172		//
173		// ------------------ MACRO_SR_PRED_INTRO
174		// (not (not t)) = t
175		//
176		// steps are added, which, since double negation is eliminated in a
177		// pre-rewrite in the Boolean rewriter, will always hold under the
178		// standard rewriter.
179	94172	Node congEq = oldn.eqNode(n);
180	94172	addStep(PfRule::CONG,
181		childrenEqs,
182		{ProofRuleChecker::mkKindNode(kind::OR)},
183	47086	congEq);
184		// add an equality resolution step to derive normalize clause
185	47086	addStep(PfRule::EQ_RESOLVE, {oldn, congEq}, {}, n);
186		}
187	377534	children.clear();
188		// remove duplicates while keeping the order of children
189	755068	std::unordered_set<TNode> clauseSet;
190	377534	unsigned size = n.getNumChildren();
191	1662452	for (unsigned i = 0; i < size; ++i)
192		{
193	1284918	if (clauseSet.count(n[i]))
194		{
195	603	continue;
196		}
197	1284315	children.push_back(n[i]);
198	1284315	clauseSet.insert(n[i]);
199		}
200		// if factoring changed
201	377534	if (children.size() < size)
202		{
203	474	Node factored = children.empty()
204		? nm->mkConst<bool>(false)
205	474	: children.size() == 1 ? children[0]
206	1422	: nm->mkNode(kind::OR, children);
207		// don't overwrite what already has a proof step to avoid cycles
208	474	addStep(PfRule::FACTORING, {n}, {}, factored);
209	474	n = factored;
210		}
211		// nothing to order
212	377534	if (children.size() < 2)
213		{
214		return n;
215		}
216		// order
217	377534	std::sort(children.begin(), children.end());
218	755068	Node ordered = nm->mkNode(kind::OR, children);
219		// if ordering changed
220	377534	if (ordered != n)
221		{
222		// don't overwrite what already has a proof step to avoid cycles
223	302551	addStep(PfRule::REORDERING, {n}, {ordered}, ordered);
224		}
225	377534	return ordered;
226		}
227
228		Node TheoryProofStepBuffer::elimDoubleNegLit(Node n)
229		{
230		// eliminate double neg
231		if (n.getKind() == kind::NOT && n[0].getKind() == kind::NOT)
232		{
233		addStep(PfRule::NOT_NOT_ELIM, {n}, {}, n[0][0]);
234		return n[0][0];
235		}
236		return n;
237		}
238
239		} // namespace theory
240	28194	} // namespace cvc5