Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/proof/theory_proof_step_buffer.cpp	Lines:	90	100	90.0 %
Date:	2021-09-15	Branches:	150	340	44.1 %


/******************************************************************************
 * 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 "proof/theory_proof_step_buffer.h"

#include "proof/proof.h"

using namespace cvc5::kind;

namespace cvc5 {

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);
  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);
  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);
  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;
  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 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 "proof/theory_proof_step_buffer.h"
17
18		#include "proof/proof.h"
19
20		using namespace cvc5::kind;
21
22		namespace cvc5 {
23
24	9653	TheoryProofStepBuffer::TheoryProofStepBuffer(ProofChecker* pc)
25	9653	: ProofStepBuffer(pc)
26		{
27	9653	}
28
29	11798	bool TheoryProofStepBuffer::applyEqIntro(Node src,
30		Node tgt,
31		const std::vector<Node>& exp,
32		MethodId ids,
33		MethodId ida,
34		MethodId idr)
35		{
36	23596	std::vector<Node> args;
37	11798	args.push_back(src);
38	11798	addMethodIds(args, ids, ida, idr);
39	23596	Node res = tryStep(PfRule::MACRO_SR_EQ_INTRO, exp, args);
40	11798	if (res.isNull())
41		{
42		// failed to apply
43		return false;
44		}
45		// should have concluded the expected equality
46	23596	Node expected = src.eqNode(tgt);
47	11798	if (res != expected)
48		{
49		// did not provide the correct target
50		popStep();
51		return false;
52		}
53		// successfully proved src == tgt.
54	11798	return true;
55		}
56
57	2261	bool TheoryProofStepBuffer::applyPredTransform(Node src,
58		Node tgt,
59		const std::vector<Node>& exp,
60		MethodId ids,
61		MethodId ida,
62		MethodId idr)
63		{
64		// symmetric equalities
65	2261	if (CDProof::isSame(src, tgt))
66		{
67	561	return true;
68		}
69	3400	std::vector<Node> children;
70	1700	children.push_back(src);
71	3400	std::vector<Node> args;
72		// try to prove that tgt rewrites to src
73	1700	children.insert(children.end(), exp.begin(), exp.end());
74	1700	args.push_back(tgt);
75	1700	addMethodIds(args, ids, ida, idr);
76	3400	Node res = tryStep(PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
77	1700	if (res.isNull())
78		{
79		// failed to apply
80	218	return false;
81		}
82		// should definitely have concluded tgt
83	1482	Assert(res == tgt);
84	1482	return true;
85		}
86
87	95	bool TheoryProofStepBuffer::applyPredIntro(Node tgt,
88		const std::vector<Node>& exp,
89		MethodId ids,
90		MethodId ida,
91		MethodId idr)
92		{
93	190	std::vector<Node> args;
94	95	args.push_back(tgt);
95	95	addMethodIds(args, ids, ida, idr);
96	190	Node res = tryStep(PfRule::MACRO_SR_PRED_INTRO, exp, args);
97	95	if (res.isNull())
98		{
99	2	return false;
100		}
101	93	Assert(res == tgt);
102	93	return true;
103		}
104
105	59	Node TheoryProofStepBuffer::applyPredElim(Node src,
106		const std::vector<Node>& exp,
107		MethodId ids,
108		MethodId ida,
109		MethodId idr)
110		{
111	118	std::vector<Node> children;
112	59	children.push_back(src);
113	59	children.insert(children.end(), exp.begin(), exp.end());
114	118	std::vector<Node> args;
115	59	addMethodIds(args, ids, ida, idr);
116	59	Node srcRew = tryStep(PfRule::MACRO_SR_PRED_ELIM, children, args);
117	59	if (CDProof::isSame(src, srcRew))
118		{
119	30	popStep();
120		}
121	118	return srcRew;
122		}
123
124	585439	Node TheoryProofStepBuffer::factorReorderElimDoubleNeg(Node n)
125		{
126	585439	if (n.getKind() != kind::OR)
127		{
128		return elimDoubleNegLit(n);
129		}
130	585439	NodeManager* nm = NodeManager::currentNM();
131	1170878	std::vector<Node> children{n.begin(), n.end()};
132	1170878	std::vector<Node> childrenEqs;
133		// eliminate double neg for each lit. Do it first because it may expose
134		// duplicates
135	585439	bool hasDoubleNeg = false;
136	2394073	for (unsigned i = 0; i < children.size(); ++i)
137		{
138	3617268	if (children[i].getKind() == kind::NOT
139	3617268	&& children[i][0].getKind() == kind::NOT)
140		{
141	105602	hasDoubleNeg = true;
142	105602	childrenEqs.push_back(children[i].eqNode(children[i][0][0]));
143	422408	addStep(PfRule::MACRO_SR_PRED_INTRO,
144		{},
145	105602	{childrenEqs.back()},
146	211204	childrenEqs.back());
147		// update child
148	105602	children[i] = children[i][0][0];
149		}
150		else
151		{
152	1703032	childrenEqs.push_back(children[i].eqNode(children[i]));
153	1703032	addStep(PfRule::REFL, {}, {children[i]}, childrenEqs.back());
154		}
155		}
156	585439	if (hasDoubleNeg)
157		{
158	127270	Node oldn = n;
159	63635	n = nm->mkNode(kind::OR, children);
160		// Create a congruence step to justify replacement of each doubly negated
161		// literal. This is done to avoid having to use MACRO_SR_PRED_TRANSFORM
162		// from the old clause to the new one, which, under the standard rewriter,
163		// may not hold. An example is
164		//
165		// ---------------------------------------------------------------------
166		// (or (or (not x2) x1 x2) (not (not x2))) = (or (or (not x2) x1 x2) x2)
167		//
168		// which fails due to factoring not happening after flattening.
169		//
170		// Using congruence only the
171		//
172		// ------------------ MACRO_SR_PRED_INTRO
173		// (not (not t)) = t
174		//
175		// steps are added, which, since double negation is eliminated in a
176		// pre-rewrite in the Boolean rewriter, will always hold under the
177		// standard rewriter.
178	127270	Node congEq = oldn.eqNode(n);
179	127270	addStep(PfRule::CONG,
180		childrenEqs,
181		{ProofRuleChecker::mkKindNode(kind::OR)},
182	63635	congEq);
183		// add an equality resolution step to derive normalize clause
184	63635	addStep(PfRule::EQ_RESOLVE, {oldn, congEq}, {}, n);
185		}
186	585439	children.clear();
187		// remove duplicates while keeping the order of children
188	1170878	std::unordered_set<TNode> clauseSet;
189	585439	unsigned size = n.getNumChildren();
190	2394073	for (unsigned i = 0; i < size; ++i)
191		{
192	1808634	if (clauseSet.count(n[i]))
193		{
194	854	continue;
195		}
196	1807780	children.push_back(n[i]);
197	1807780	clauseSet.insert(n[i]);
198		}
199		// if factoring changed
200	585439	if (children.size() < size)
201		{
202	662	Node factored = children.empty()
203		? nm->mkConst<bool>(false)
204	662	: children.size() == 1 ? children[0]
205	1986	: nm->mkNode(kind::OR, children);
206		// don't overwrite what already has a proof step to avoid cycles
207	662	addStep(PfRule::FACTORING, {n}, {}, factored);
208	662	n = factored;
209		}
210		// nothing to order
211	585439	if (children.size() < 2)
212		{
213		return n;
214		}
215		// order
216	585439	std::sort(children.begin(), children.end());
217	1170878	Node ordered = nm->mkNode(kind::OR, children);
218		// if ordering changed
219	585439	if (ordered != n)
220		{
221		// don't overwrite what already has a proof step to avoid cycles
222	470612	addStep(PfRule::REORDERING, {n}, {ordered}, ordered);
223		}
224	585439	return ordered;
225		}
226
227		Node TheoryProofStepBuffer::elimDoubleNegLit(Node n)
228		{
229		// eliminate double neg
230		if (n.getKind() == kind::NOT && n[0].getKind() == kind::NOT)
231		{
232		addStep(PfRule::NOT_NOT_ELIM, {n}, {}, n[0][0]);
233		return n[0][0];
234		}
235		return n;
236		}
237
238	29577	} // namespace cvc5