Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/booleans/proof_circuit_propagator.cpp	Lines:	230	251	91.6 %
Date:	2021-09-13	Branches:	547	1100	49.7 %


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