Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/booleans/proof_circuit_propagator.cpp	Lines:	228	249	91.6 %
Date:	2021-05-22	Branches:	544	1098	49.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Gereon Kremer
 *
 * 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.
 * ****************************************************************************
 *
 * Proofs for the non-clausal circuit propagator.
 */

#include "theory/booleans/proof_circuit_propagator.h"

#include <sstream>

#include "expr/proof_node.h"
#include "expr/proof_node_manager.h"

namespace cvc5 {
namespace theory {
namespace booleans {

namespace {

/** Shorthand to create a Node from a constant number */
template <typename T>
Node mkRat(T val)
{
  return NodeManager::currentNM()->mkConst<Rational>(val);
}

/**
 * Collect all children from parent except for one particular child (the
 * "holdout"). The holdout is given as iterator, and should be an iterator into
 * the [parent.begin(),parent.end()] range.
 */
inline std::vector<Node> collectButHoldout(TNode parent,
                                           TNode::iterator holdout)
{
  std::vector<Node> lits;
  for (TNode::iterator i = parent.begin(), i_end = parent.end(); i != i_end;
       ++i)
  {
    if (i != holdout)
    {
      lits.emplace_back(*i);
    }
  }
  return lits;
}

}  // namespace

ProofCircuitPropagator::ProofCircuitPropagator(ProofNodeManager* pnm)
    : d_pnm(pnm)
{
}

bool ProofCircuitPropagator::disabled() const { return d_pnm == nullptr; }

std::shared_ptr<ProofNode> ProofCircuitPropagator::assume(Node n)
{
  return d_pnm->mkAssume(n);
}

std::shared_ptr<ProofNode> ProofCircuitPropagator::conflict(
    const std::shared_ptr<ProofNode>& a, const std::shared_ptr<ProofNode>& b)
{
  if (a->getResult().notNode() == b->getResult())
  {
    return mkProof(PfRule::CONTRA, {a, b});
  }
  Assert(a->getResult() == b->getResult().notNode());
  return mkProof(PfRule::CONTRA, {b, a});
}

std::shared_ptr<ProofNode> ProofCircuitPropagator::andFalse(
    Node parent, TNode::iterator holdout)
{
  if (disabled())
  {
    return nullptr;
  }
  return mkNot(
      mkCResolution(mkProof(PfRule::NOT_AND, {assume(parent.notNode())}),
                    collectButHoldout(parent, holdout),
                    false));
}

std::shared_ptr<ProofNode> ProofCircuitPropagator::orTrue(
    Node parent, TNode::iterator holdout)
{
  if (disabled())
  {
    return nullptr;
  }
  return mkCResolution(
      assume(parent), collectButHoldout(parent, holdout), true);
}

std::shared_ptr<ProofNode> ProofCircuitPropagator::Not(bool negate, Node parent)
{
  if (disabled())
  {
    return nullptr;
  }
  return mkNot(assume(negate ? Node(parent[0]) : parent));
}

std::shared_ptr<ProofNode> ProofCircuitPropagator::impliesXFromY(Node parent)
{
  if (disabled())
  {
    return nullptr;
  }
  return mkNot(mkResolution(
      mkProof(PfRule::IMPLIES_ELIM, {assume(parent)}), parent[1], true));
}

std::shared_ptr<ProofNode> ProofCircuitPropagator::impliesYFromX(Node parent)
{
  if (disabled())
  {
    return nullptr;
  }
  return mkResolution(
      mkProof(PfRule::IMPLIES_ELIM, {assume(parent)}), parent[0], false);
}

std::shared_ptr<ProofNode> ProofCircuitPropagator::eqXFromY(bool y, Node parent)
{
  if (disabled())
  {
    return nullptr;
  }
  if (y)
  {
    return mkProof(
        PfRule::EQ_RESOLVE,
        {assume(parent[1]), mkProof(PfRule::SYMM, {assume(parent)})});
  }
  return mkNot(mkResolution(
      mkProof(PfRule::EQUIV_ELIM1, {assume(parent)}), parent[1], true));
}

std::shared_ptr<ProofNode> ProofCircuitPropagator::eqYFromX(bool x, Node parent)
{
  if (disabled())
  {
    return nullptr;
  }
  if (x)
  {
    return mkProof(PfRule::EQ_RESOLVE, {assume(parent[0]), assume(parent)});
  }
  return mkNot(mkResolution(
      mkProof(PfRule::EQUIV_ELIM2, {assume(parent)}), parent[0], true));
}

std::shared_ptr<ProofNode> ProofCircuitPropagator::neqXFromY(bool y,
                                                             Node parent)
{
  if (disabled())
  {
    return nullptr;
  }
  return mkResolution(
      mkProof(y ? PfRule::NOT_EQUIV_ELIM2 : PfRule::NOT_EQUIV_ELIM1,
              {assume(parent.notNode())}),
      parent[1],
      !y);
}

std::shared_ptr<ProofNode> ProofCircuitPropagator::neqYFromX(bool x,
                                                             Node parent)
{
  if (disabled())
  {
    return nullptr;
  }
  return mkResolution(
      mkProof(x ? PfRule::NOT_EQUIV_ELIM2 : PfRule::NOT_EQUIV_ELIM1,
              {assume(parent.notNode())}),
      parent[0],
      !x);
}

std::shared_ptr<ProofNode> ProofCircuitPropagator::xorXFromY(bool negated,
                                                             bool y,
                                                             Node parent)
{
  if (disabled())
  {
    return nullptr;
  }
  if (y)
  {
    return mkNot(mkResolution(
        mkProof(negated ? PfRule::NOT_XOR_ELIM1 : PfRule::XOR_ELIM2,
                {assume(negated ? parent.notNode() : Node(parent))}),
        parent[1],
        false));
  }
  return mkResolution(
      mkProof(negated ? PfRule::NOT_XOR_ELIM2 : PfRule::XOR_ELIM1,
              {assume(negated ? parent.notNode() : Node(parent))}),
      parent[1],
      true);
}

std::shared_ptr<ProofNode> ProofCircuitPropagator::xorYFromX(bool negated,
                                                             bool x,
                                                             Node parent)
{
  if (disabled())
  {
    return nullptr;
  }
  if (x)
  {
    return mkResolution(
        mkProof(negated ? PfRule::NOT_XOR_ELIM2 : PfRule::XOR_ELIM2,
                {assume(negated ? parent.notNode() : Node(parent))}),
        parent[0],
        false);
  }
  return mkNot(
      mkResolution(mkProof(negated ? PfRule::NOT_XOR_ELIM1 : PfRule::XOR_ELIM1,
                           {assume(negated ? parent.notNode() : Node(parent))}),
                   parent[0],
                   true));
}

std::shared_ptr<ProofNode> ProofCircuitPropagator::mkProof(
    PfRule rule,
    const std::vector<std::shared_ptr<ProofNode>>& children,
    const std::vector<Node>& args)
{
  if (Trace.isOn("circuit-prop"))
  {
    std::stringstream ss;
    ss << "Constructing (" << rule;
    for (const auto& c : children)
    {
      ss << " " << *c;
    }
    if (!args.empty())
    {
      ss << " :args";
      for (const auto& a : args)
      {
        ss << " " << a;
      }
    }
    ss << ")";
    Trace("circuit-prop") << ss.str() << std::endl;
  }
  return d_pnm->mkNode(rule, children, args);
}

std::shared_ptr<ProofNode> ProofCircuitPropagator::mkCResolution(
    const std::shared_ptr<ProofNode>& clause,
    const std::vector<Node>& lits,
    const std::vector<bool>& polarity)
{
  auto* nm = NodeManager::currentNM();
  std::vector<std::shared_ptr<ProofNode>> children = {clause};
  std::vector<Node> args;
  Assert(lits.size() == polarity.size());
  for (std::size_t i = 0, n = lits.size(); i < n; ++i)
  {
    bool pol = polarity[i];
    Node lit = lits[i];
    if (polarity[i])
    {
      if (lit.getKind() == Kind::NOT)
      {
        lit = lit[0];
        pol = !pol;
        children.emplace_back(assume(lit));
      }
      else
      {
        children.emplace_back(assume(lit.notNode()));
      }
    }
    else
    {
      children.emplace_back(assume(lit));
    }
    args.emplace_back(nm->mkConst(pol));
    args.emplace_back(lit);
  }
  return mkProof(PfRule::CHAIN_RESOLUTION, children, args);
}

std::shared_ptr<ProofNode> ProofCircuitPropagator::mkCResolution(
    const std::shared_ptr<ProofNode>& clause,
    const std::vector<Node>& lits,
    bool polarity)
{
  return mkCResolution(clause, lits, std::vector<bool>(lits.size(), polarity));
}

std::shared_ptr<ProofNode> ProofCircuitPropagator::mkResolution(
    const std::shared_ptr<ProofNode>& clause, const Node& lit, bool polarity)
{
  auto* nm = NodeManager::currentNM();
  if (polarity)
  {
    if (lit.getKind() == Kind::NOT)
    {
      return mkProof(PfRule::RESOLUTION,
                     {clause, assume(lit[0])},
                     {nm->mkConst(false), lit[0]});
    }
    return mkProof(PfRule::RESOLUTION,
                   {clause, assume(lit.notNode())},
                   {nm->mkConst(true), lit});
  }
  return mkProof(
      PfRule::RESOLUTION, {clause, assume(lit)}, {nm->mkConst(false), lit});
}

std::shared_ptr<ProofNode> ProofCircuitPropagator::mkNot(
    const std::shared_ptr<ProofNode>& n)
{
  Node m = n->getResult();
  if (m.getKind() == Kind::NOT && m[0].getKind() == Kind::NOT)
  {
    return mkProof(PfRule::NOT_NOT_ELIM, {n});
  }
  return n;
}

ProofCircuitPropagatorBackward::ProofCircuitPropagatorBackward(
    ProofNodeManager* pnm, TNode parent, bool parentAssignment)
    : ProofCircuitPropagator(pnm),
      d_parent(parent),
      d_parentAssignment(parentAssignment)
{
}

std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::andTrue(
    TNode::iterator i)
{
  if (disabled())
  {
    return nullptr;
  }
  return mkProof(
      PfRule::AND_ELIM, {assume(d_parent)}, {mkRat(i - d_parent.begin())});
}

std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::orFalse(
    TNode::iterator i)
{
  if (disabled())
  {
    return nullptr;
  }
  return mkNot(mkProof(PfRule::NOT_OR_ELIM,
                       {assume(d_parent.notNode())},
                       {mkRat(i - d_parent.begin())}));
}

std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::iteC(bool c)
{
  if (disabled())
  {
    return nullptr;
  }
  if (d_parentAssignment)
  {
    return mkResolution(
        mkProof(c ? PfRule::ITE_ELIM1 : PfRule::ITE_ELIM2, {assume(d_parent)}),
        d_parent[0],
        !c);
  }
  return mkResolution(mkProof(c ? PfRule::NOT_ITE_ELIM1 : PfRule::NOT_ITE_ELIM2,
                              {assume(d_parent.notNode())}),
                      d_parent[0],
                      !c);
}

std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::iteIsCase(unsigned c)
{
  if (disabled())
  {
    return nullptr;
  }
  if (d_parentAssignment)
  {
    return mkResolution(
        mkProof(PfRule::ITE_ELIM2, {assume(d_parent)}), d_parent[c + 1], false);
  }
  return mkResolution(
      mkProof(PfRule::NOT_ITE_ELIM2, {assume(d_parent.notNode())}),
      d_parent[c + 1],
      false);
}

std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::impliesNegX()
{
  if (disabled())
  {
    return nullptr;
  }
  return mkNot(
      mkProof(PfRule::NOT_IMPLIES_ELIM1, {assume(d_parent.notNode())}));
}

std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::impliesNegY()
{
  if (disabled())
  {
    return nullptr;
  }
  return mkNot(
      mkProof(PfRule::NOT_IMPLIES_ELIM2, {assume(d_parent.notNode())}));
}

ProofCircuitPropagatorForward::ProofCircuitPropagatorForward(
    ProofNodeManager* pnm, Node child, bool childAssignment, Node parent)
    : ProofCircuitPropagator{pnm},
      d_child(child),
      d_childAssignment(childAssignment),
      d_parent(parent)
{
}

std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::andAllTrue()
{
  if (disabled())
  {
    return nullptr;
  }
  std::vector<std::shared_ptr<ProofNode>> children;
  for (const auto& child : d_parent)
  {
    children.emplace_back(assume(child));
  }
  return mkProof(PfRule::AND_INTRO, children);
}

std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::andOneFalse()
{
  if (disabled())
  {
    return nullptr;
  }
  auto it = std::find(d_parent.begin(), d_parent.end(), d_child);
  return mkResolution(
      mkProof(
          PfRule::CNF_AND_POS, {}, {d_parent, mkRat(it - d_parent.begin())}),
      d_child,
      true);
}

std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::orOneTrue()
{
  if (disabled())
  {
    return nullptr;
  }
  auto it = std::find(d_parent.begin(), d_parent.end(), d_child);
  return mkNot(mkResolution(
      mkProof(PfRule::CNF_OR_NEG, {}, {d_parent, mkRat(it - d_parent.begin())}),
      d_child,
      false));
}

std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::orFalse()
{
  if (disabled())
  {
    return nullptr;
  }
  std::vector<Node> children(d_parent.begin(), d_parent.end());
  return mkCResolution(
      mkProof(PfRule::CNF_OR_POS, {}, {d_parent}), children, true);
}

std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::iteEvalThen(bool x)
{
  if (disabled())
  {
    return nullptr;
  }
  return mkCResolution(
      mkProof(x ? PfRule::CNF_ITE_NEG1 : PfRule::CNF_ITE_POS1, {}, {d_parent}),
      {d_parent[0], d_parent[1]},
      {false, !x});
}

std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::iteEvalElse(bool y)
{
  if (disabled())
  {
    return nullptr;
  }
  return mkCResolution(
      mkProof(y ? PfRule::CNF_ITE_NEG2 : PfRule::CNF_ITE_POS2, {}, {d_parent}),
      {d_parent[0], d_parent[2]},
      {true, !y});
}

std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::eqEval(bool x, bool y)
{
  if (disabled())
  {
    return nullptr;
  }
  if (x == y)
  {
    return mkCResolution(
        mkProof(x ? PfRule::CNF_EQUIV_NEG2 : PfRule::CNF_EQUIV_NEG1,
                {},
                {d_parent}),
        {d_parent[0], d_parent[1]},
        {!x, !y});
  }
  return mkCResolution(
      mkProof(
          x ? PfRule::CNF_EQUIV_POS1 : PfRule::CNF_EQUIV_POS2, {}, {d_parent}),
      {d_parent[0], d_parent[1]},
      {!x, !y});
}

std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::impliesEval(
    bool premise, bool conclusion)
{
  if (disabled())
  {
    return nullptr;
  }
  if (!premise)
  {
    return mkResolution(
        mkProof(PfRule::CNF_IMPLIES_NEG1, {}, {d_parent}), d_parent[0], true);
  }
  if (conclusion)
  {
    return mkResolution(
        mkProof(PfRule::CNF_IMPLIES_NEG2, {}, {d_parent}), d_parent[1], false);
  }
  return mkCResolution(mkProof(PfRule::CNF_IMPLIES_POS, {}, {d_parent}),
                       {d_parent[0], d_parent[1]},
                       {false, true});
}

std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::xorEval(bool x,
                                                                  bool y)
{
  if (disabled())
  {
    return nullptr;
  }
  if (x && y)
  {
    return mkCResolution(mkProof(PfRule::CNF_XOR_POS2, {}, {d_parent}),
                         {d_parent[0], d_parent[1]},
                         {false, false});
  }
  else if (x && !y)
  {
    return mkCResolution(mkProof(PfRule::CNF_XOR_NEG1, {}, {d_parent}),
                         {d_parent[0], d_parent[1]},
                         {false, true});
  }
  else if (!x && y)
  {
    return mkCResolution(mkProof(PfRule::CNF_XOR_NEG2, {}, {d_parent}),
                         {d_parent[0], d_parent[1]},
                         {true, false});
  }
  Assert(!x && !y);
  return mkCResolution(mkProof(PfRule::CNF_XOR_POS1, {}, {d_parent}),
                       {d_parent[0], d_parent[1]},
                       {true, true});
}

}  // namespace booleans
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Gereon Kremer
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		* Proofs for the non-clausal circuit propagator.
14		*/
15
16		#include "theory/booleans/proof_circuit_propagator.h"
17
18		#include <sstream>
19
20		#include "expr/proof_node.h"
21		#include "expr/proof_node_manager.h"
22
23		namespace cvc5 {
24		namespace theory {
25		namespace booleans {
26
27		namespace {
28
29		/** Shorthand to create a Node from a constant number */
30		template <typename T>
31	41066	Node mkRat(T val)
32		{
33	41066	return NodeManager::currentNM()->mkConst<Rational>(val);
34		}
35
36		/**
37		* Collect all children from parent except for one particular child (the
38		* "holdout"). The holdout is given as iterator, and should be an iterator into
39		* the [parent.begin(),parent.end()] range.
40		*/
41	665	inline std::vector<Node> collectButHoldout(TNode parent,
42		TNode::iterator holdout)
43		{
44	665	std::vector<Node> lits;
45	2248	for (TNode::iterator i = parent.begin(), i_end = parent.end(); i != i_end;
46		++i)
47		{
48	1583	if (i != holdout)
49		{
50	918	lits.emplace_back(*i);
51		}
52		}
53	665	return lits;
54		}
55
56		} // namespace
57
58	1095897	ProofCircuitPropagator::ProofCircuitPropagator(ProofNodeManager* pnm)
59	1095897	: d_pnm(pnm)
60		{
61	1095897	}
62
63	1022641	bool ProofCircuitPropagator::disabled() const { return d_pnm == nullptr; }
64
65	8978654	std::shared_ptr<ProofNode> ProofCircuitPropagator::assume(Node n)
66		{
67	8978654	return d_pnm->mkAssume(n);
68		}
69
70	103	std::shared_ptr<ProofNode> ProofCircuitPropagator::conflict(
71		const std::shared_ptr<ProofNode>& a, const std::shared_ptr<ProofNode>& b)
72		{
73	103	if (a->getResult().notNode() == b->getResult())
74		{
75	68	return mkProof(PfRule::CONTRA, {a, b});
76		}
77	35	Assert(a->getResult() == b->getResult().notNode());
78	35	return mkProof(PfRule::CONTRA, {b, a});
79		}
80
81	810	std::shared_ptr<ProofNode> ProofCircuitPropagator::andFalse(
82		Node parent, TNode::iterator holdout)
83		{
84	810	if (disabled())
85		{
86	560	return nullptr;
87		}
88		return mkNot(
89	500	mkCResolution(mkProof(PfRule::NOT_AND, {assume(parent.notNode())}),
90	500	collectButHoldout(parent, holdout),
91	250	false));
92		}
93
94	87937	std::shared_ptr<ProofNode> ProofCircuitPropagator::orTrue(
95		Node parent, TNode::iterator holdout)
96		{
97	87937	if (disabled())
98		{
99	87522	return nullptr;
100		}
101		return mkCResolution(
102	415	assume(parent), collectButHoldout(parent, holdout), true);
103		}
104
105	138076	std::shared_ptr<ProofNode> ProofCircuitPropagator::Not(bool negate, Node parent)
106		{
107	138076	if (disabled())
108		{
109	112326	return nullptr;
110		}
111	25750	return mkNot(assume(negate ? Node(parent[0]) : parent));
112		}
113
114	56	std::shared_ptr<ProofNode> ProofCircuitPropagator::impliesXFromY(Node parent)
115		{
116	56	if (disabled())
117		{
118	29	return nullptr;
119		}
120	108	return mkNot(mkResolution(
121	81	mkProof(PfRule::IMPLIES_ELIM, {assume(parent)}), parent[1], true));
122		}
123
124	674	std::shared_ptr<ProofNode> ProofCircuitPropagator::impliesYFromX(Node parent)
125		{
126	674	if (disabled())
127		{
128	449	return nullptr;
129		}
130		return mkResolution(
131	225	mkProof(PfRule::IMPLIES_ELIM, {assume(parent)}), parent[0], false);
132		}
133
134	116	std::shared_ptr<ProofNode> ProofCircuitPropagator::eqXFromY(bool y, Node parent)
135		{
136	116	if (disabled())
137		{
138	53	return nullptr;
139		}
140	63	if (y)
141		{
142		return mkProof(
143		PfRule::EQ_RESOLVE,
144	52	{assume(parent[1]), mkProof(PfRule::SYMM, {assume(parent)})});
145		}
146	44	return mkNot(mkResolution(
147	33	mkProof(PfRule::EQUIV_ELIM1, {assume(parent)}), parent[1], true));
148		}
149
150	766	std::shared_ptr<ProofNode> ProofCircuitPropagator::eqYFromX(bool x, Node parent)
151		{
152	766	if (disabled())
153		{
154	97	return nullptr;
155		}
156	669	if (x)
157		{
158	609	return mkProof(PfRule::EQ_RESOLVE, {assume(parent[0]), assume(parent)});
159		}
160	240	return mkNot(mkResolution(
161	180	mkProof(PfRule::EQUIV_ELIM2, {assume(parent)}), parent[0], true));
162		}
163
164	3	std::shared_ptr<ProofNode> ProofCircuitPropagator::neqXFromY(bool y,
165		Node parent)
166		{
167	3	if (disabled())
168		{
169	2	return nullptr;
170		}
171		return mkResolution(
172	5	mkProof(y ? PfRule::NOT_EQUIV_ELIM2 : PfRule::NOT_EQUIV_ELIM1,
173	3	{assume(parent.notNode())}),
174		parent[1],
175	3	!y);
176		}
177
178	7	std::shared_ptr<ProofNode> ProofCircuitPropagator::neqYFromX(bool x,
179		Node parent)
180		{
181	7	if (disabled())
182		{
183	6	return nullptr;
184		}
185		return mkResolution(
186	5	mkProof(x ? PfRule::NOT_EQUIV_ELIM2 : PfRule::NOT_EQUIV_ELIM1,
187	3	{assume(parent.notNode())}),
188		parent[0],
189	3	!x);
190		}
191
192	24	std::shared_ptr<ProofNode> ProofCircuitPropagator::xorXFromY(bool negated,
193		bool y,
194		Node parent)
195		{
196	24	if (disabled())
197		{
198	16	return nullptr;
199		}
200	8	if (y)
201		{
202	32	return mkNot(mkResolution(
203	40	mkProof(negated ? PfRule::NOT_XOR_ELIM1 : PfRule::XOR_ELIM2,
204	24	{assume(negated ? parent.notNode() : Node(parent))}),
205		parent[1],
206	8	false));
207		}
208		return mkResolution(
209		mkProof(negated ? PfRule::NOT_XOR_ELIM2 : PfRule::XOR_ELIM1,
210		{assume(negated ? parent.notNode() : Node(parent))}),
211		parent[1],
212		true);
213		}
214
215	25	std::shared_ptr<ProofNode> ProofCircuitPropagator::xorYFromX(bool negated,
216		bool x,
217		Node parent)
218		{
219	25	if (disabled())
220		{
221	16	return nullptr;
222		}
223	9	if (x)
224		{
225		return mkResolution(
226	20	mkProof(negated ? PfRule::NOT_XOR_ELIM2 : PfRule::XOR_ELIM2,
227	12	{assume(negated ? parent.notNode() : Node(parent))}),
228		parent[0],
229	12	false);
230		}
231		return mkNot(
232	25	mkResolution(mkProof(negated ? PfRule::NOT_XOR_ELIM1 : PfRule::XOR_ELIM1,
233	15	{assume(negated ? parent.notNode() : Node(parent))}),
234		parent[0],
235	5	true));
236		}
237
238	61202	std::shared_ptr<ProofNode> ProofCircuitPropagator::mkProof(
239		PfRule rule,
240		const std::vector<std::shared_ptr<ProofNode>>& children,
241		const std::vector<Node>& args)
242		{
243	61202	if (Trace.isOn("circuit-prop"))
244		{
245		std::stringstream ss;
246		ss << "Constructing (" << rule;
247		for (const auto& c : children)
248		{
249		ss << " " << *c;
250		}
251		if (!args.empty())
252		{
253		ss << " :args";
254		for (const auto& a : args)
255		{
256		ss << " " << a;
257		}
258		}
259		ss << ")";
260		Trace("circuit-prop") << ss.str() << std::endl;
261		}
262	61202	return d_pnm->mkNode(rule, children, args);
263		}
264
265	3842	std::shared_ptr<ProofNode> ProofCircuitPropagator::mkCResolution(
266		const std::shared_ptr<ProofNode>& clause,
267		const std::vector<Node>& lits,
268		const std::vector<bool>& polarity)
269		{
270	3842	auto* nm = NodeManager::currentNM();
271	7684	std::vector<std::shared_ptr<ProofNode>> children = {clause};
272	7684	std::vector<Node> args;
273	3842	Assert(lits.size() == polarity.size());
274	199106	for (std::size_t i = 0, n = lits.size(); i < n; ++i)
275		{
276	195264	bool pol = polarity[i];
277	390528	Node lit = lits[i];
278	195264	if (polarity[i])
279		{
280	192158	if (lit.getKind() == Kind::NOT)
281		{
282	173809	lit = lit[0];
283	173809	pol = !pol;
284	173809	children.emplace_back(assume(lit));
285		}
286		else
287		{
288	18349	children.emplace_back(assume(lit.notNode()));
289		}
290		}
291		else
292		{
293	3106	children.emplace_back(assume(lit));
294		}
295	195264	args.emplace_back(nm->mkConst(pol));
296	195264	args.emplace_back(lit);
297		}
298	7684	return mkProof(PfRule::CHAIN_RESOLUTION, children, args);
299		}
300
301	1986	std::shared_ptr<ProofNode> ProofCircuitPropagator::mkCResolution(
302		const std::shared_ptr<ProofNode>& clause,
303		const std::vector<Node>& lits,
304		bool polarity)
305		{
306	1986	return mkCResolution(clause, lits, std::vector<bool>(lits.size(), polarity));
307		}
308
309	3230	std::shared_ptr<ProofNode> ProofCircuitPropagator::mkResolution(
310		const std::shared_ptr<ProofNode>& clause, const Node& lit, bool polarity)
311		{
312	3230	auto* nm = NodeManager::currentNM();
313	3230	if (polarity)
314		{
315	1396	if (lit.getKind() == Kind::NOT)
316		{
317		return mkProof(PfRule::RESOLUTION,
318		{clause, assume(lit[0])},
319	323	{nm->mkConst(false), lit[0]});
320		}
321		return mkProof(PfRule::RESOLUTION,
322	2146	{clause, assume(lit.notNode())},
323	3219	{nm->mkConst(true), lit});
324		}
325		return mkProof(
326	1834	PfRule::RESOLUTION, {clause, assume(lit)}, {nm->mkConst(false), lit});
327		}
328
329	29277	std::shared_ptr<ProofNode> ProofCircuitPropagator::mkNot(
330		const std::shared_ptr<ProofNode>& n)
331		{
332	58554	Node m = n->getResult();
333	29277	if (m.getKind() == Kind::NOT && m[0].getKind() == Kind::NOT)
334		{
335	879	return mkProof(PfRule::NOT_NOT_ELIM, {n});
336		}
337	28398	return n;
338		}
339
340	567347	ProofCircuitPropagatorBackward::ProofCircuitPropagatorBackward(
341	567347	ProofNodeManager* pnm, TNode parent, bool parentAssignment)
342		: ProofCircuitPropagator(pnm),
343		d_parent(parent),
344	567347	d_parentAssignment(parentAssignment)
345		{
346	567347	}
347
348	515323	std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::andTrue(
349		TNode::iterator i)
350		{
351	515323	if (disabled())
352		{
353	478210	return nullptr;
354		}
355		return mkProof(
356	37113	PfRule::AND_ELIM, {assume(d_parent)}, {mkRat(i - d_parent.begin())});
357		}
358
359	4296	std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::orFalse(
360		TNode::iterator i)
361		{
362	4296	if (disabled())
363		{
364	2953	return nullptr;
365		}
366	8058	return mkNot(mkProof(PfRule::NOT_OR_ELIM,
367	2686	{assume(d_parent.notNode())},
368	5372	{mkRat(i - d_parent.begin())}));
369		}
370
371	14	std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::iteC(bool c)
372		{
373	14	if (disabled())
374		{
375	8	return nullptr;
376		}
377	6	if (d_parentAssignment)
378		{
379		return mkResolution(
380	8	mkProof(c ? PfRule::ITE_ELIM1 : PfRule::ITE_ELIM2, {assume(d_parent)}),
381		d_parent[0],
382	12	!c);
383		}
384	10	return mkResolution(mkProof(c ? PfRule::NOT_ITE_ELIM1 : PfRule::NOT_ITE_ELIM2,
385	6	{assume(d_parent.notNode())}),
386		d_parent[0],
387	6	!c);
388		}
389
390		std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::iteIsCase(unsigned c)
391		{
392		if (disabled())
393		{
394		return nullptr;
395		}
396		if (d_parentAssignment)
397		{
398		return mkResolution(
399		mkProof(PfRule::ITE_ELIM2, {assume(d_parent)}), d_parent[c + 1], false);
400		}
401		return mkResolution(
402		mkProof(PfRule::NOT_ITE_ELIM2, {assume(d_parent.notNode())}),
403		d_parent[c + 1],
404		false);
405		}
406
407	633	std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::impliesNegX()
408		{
409	633	if (disabled())
410		{
411	396	return nullptr;
412		}
413		return mkNot(
414	237	mkProof(PfRule::NOT_IMPLIES_ELIM1, {assume(d_parent.notNode())}));
415		}
416
417	633	std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::impliesNegY()
418		{
419	633	if (disabled())
420		{
421	396	return nullptr;
422		}
423		return mkNot(
424	237	mkProof(PfRule::NOT_IMPLIES_ELIM2, {assume(d_parent.notNode())}));
425		}
426
427	528232	ProofCircuitPropagatorForward::ProofCircuitPropagatorForward(
428	528232	ProofNodeManager* pnm, Node child, bool childAssignment, Node parent)
429		: ProofCircuitPropagator{pnm},
430		d_child(child),
431		d_childAssignment(childAssignment),
432	528232	d_parent(parent)
433		{
434	528232	}
435
436	17808	std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::andAllTrue()
437		{
438	17808	if (disabled())
439		{
440	10960	return nullptr;
441		}
442	13696	std::vector<std::shared_ptr<ProofNode>> children;
443	8718765	for (const auto& child : d_parent)
444		{
445	8711917	children.emplace_back(assume(child));
446		}
447	6848	return mkProof(PfRule::AND_INTRO, children);
448		}
449
450	4149	std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::andOneFalse()
451		{
452	4149	if (disabled())
453		{
454	2888	return nullptr;
455		}
456	1261	auto it = std::find(d_parent.begin(), d_parent.end(), d_child);
457		return mkResolution(
458	5044	mkProof(
459	2522	PfRule::CNF_AND_POS, {}, {d_parent, mkRat(it - d_parent.begin())}),
460		d_child,
461	2522	true);
462		}
463
464	243394	std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::orOneTrue()
465		{
466	243394	if (disabled())
467		{
468	242045	return nullptr;
469		}
470	1349	auto it = std::find(d_parent.begin(), d_parent.end(), d_child);
471	4047	return mkNot(mkResolution(
472	2698	mkProof(PfRule::CNF_OR_NEG, {}, {d_parent, mkRat(it - d_parent.begin())}),
473		d_child,
474	2698	false));
475		}
476
477	4223	std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::orFalse()
478		{
479	4223	if (disabled())
480		{
481	2902	return nullptr;
482		}
483	2642	std::vector<Node> children(d_parent.begin(), d_parent.end());
484		return mkCResolution(
485	1321	mkProof(PfRule::CNF_OR_POS, {}, {d_parent}), children, true);
486		}
487
488	17	std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::iteEvalThen(bool x)
489		{
490	17	if (disabled())
491		{
492	10	return nullptr;
493		}
494		return mkCResolution(
495	14	mkProof(x ? PfRule::CNF_ITE_NEG1 : PfRule::CNF_ITE_POS1, {}, {d_parent}),
496		{d_parent[0], d_parent[1]},
497	21	{false, !x});
498		}
499
500	11	std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::iteEvalElse(bool y)
501		{
502	11	if (disabled())
503		{
504	7	return nullptr;
505		}
506		return mkCResolution(
507	8	mkProof(y ? PfRule::CNF_ITE_NEG2 : PfRule::CNF_ITE_POS2, {}, {d_parent}),
508		{d_parent[0], d_parent[2]},
509	12	{true, !y});
510		}
511
512	1587	std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::eqEval(bool x, bool y)
513		{
514	1587	if (disabled())
515		{
516	213	return nullptr;
517		}
518	1374	if (x == y)
519		{
520		return mkCResolution(
521	4104	mkProof(x ? PfRule::CNF_EQUIV_NEG2 : PfRule::CNF_EQUIV_NEG1,
522		{},
523	1368	{d_parent}),
524		{d_parent[0], d_parent[1]},
525	4104	{!x, !y});
526		}
527		return mkCResolution(
528	18	mkProof(
529	6	x ? PfRule::CNF_EQUIV_POS1 : PfRule::CNF_EQUIV_POS2, {}, {d_parent}),
530		{d_parent[0], d_parent[1]},
531	18	{!x, !y});
532		}
533
534	2022	std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::impliesEval(
535		bool premise, bool conclusion)
536		{
537	2022	if (disabled())
538		{
539	1292	return nullptr;
540		}
541	730	if (!premise)
542		{
543		return mkResolution(
544	31	mkProof(PfRule::CNF_IMPLIES_NEG1, {}, {d_parent}), d_parent[0], true);
545		}
546	699	if (conclusion)
547		{
548		return mkResolution(
549	241	mkProof(PfRule::CNF_IMPLIES_NEG2, {}, {d_parent}), d_parent[1], false);
550		}
551	916	return mkCResolution(mkProof(PfRule::CNF_IMPLIES_POS, {}, {d_parent}),
552		{d_parent[0], d_parent[1]},
553	1374	{false, true});
554		}
555
556	37	std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::xorEval(bool x,
557		bool y)
558		{
559	37	if (disabled())
560		{
561	24	return nullptr;
562		}
563	13	if (x && y)
564		{
565	8	return mkCResolution(mkProof(PfRule::CNF_XOR_POS2, {}, {d_parent}),
566		{d_parent[0], d_parent[1]},
567	12	{false, false});
568		}
569	9	else if (x && !y)
570		{
571	2	return mkCResolution(mkProof(PfRule::CNF_XOR_NEG1, {}, {d_parent}),
572		{d_parent[0], d_parent[1]},
573	3	{false, true});
574		}
575	8	else if (!x && y)
576		{
577	12	return mkCResolution(mkProof(PfRule::CNF_XOR_NEG2, {}, {d_parent}),
578		{d_parent[0], d_parent[1]},
579	18	{true, false});
580		}
581	2	Assert(!x && !y);
582	4	return mkCResolution(mkProof(PfRule::CNF_XOR_POS1, {}, {d_parent}),
583		{d_parent[0], d_parent[1]},
584	6	{true, true});
585		}
586
587		} // namespace booleans
588		} // namespace theory
589	28191	} // namespace cvc5