Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/booleans/proof_circuit_propagator.h	Lines:	2	2	100.0 %
Date:	2021-11-07	Branches:	0	0	0.0 %


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

#ifndef CVC5__THEORY__BOOLEANS__PROOF_CIRCUIT_PROPAGATOR_H
#define CVC5__THEORY__BOOLEANS__PROOF_CIRCUIT_PROPAGATOR_H

#include <memory>

#include "expr/node.h"
#include "proof/proof_rule.h"

namespace cvc5 {

class ProofNode;
class ProofNodeManager;

namespace theory {
namespace booleans {

/**
 * Base class for for CircuitPropagatorProofs.
 * This class collects common functionality for proofs of backward and forward
 * propagation.
 */
class ProofCircuitPropagator
{
 public:
  ProofCircuitPropagator(ProofNodeManager* pnm);

  /** Assuming the given node */
  std::shared_ptr<ProofNode> assume(Node n);
  /** Apply CONTRA rule. Takes care of switching a and b if necessary */
  std::shared_ptr<ProofNode> conflict(const std::shared_ptr<ProofNode>& a,
                                      const std::shared_ptr<ProofNode>& b);

  /** (and true ... holdout true ...)  -->  holdout */
  std::shared_ptr<ProofNode> andFalse(Node parent, TNode::iterator holdout);

  /** (or false ... holdout false ...)  ->  holdout */
  std::shared_ptr<ProofNode> orTrue(Node parent, TNode::iterator holdout);

  /** (not x) is true  -->  x is false (and vice versa) */
  std::shared_ptr<ProofNode> Not(bool negate, Node parent);

  /** (=> X false)  -->  (not X) */
  std::shared_ptr<ProofNode> impliesXFromY(Node parent);
  /** (=> true Y)  -->  Y */
  std::shared_ptr<ProofNode> impliesYFromX(Node parent);

  /** Derive X from (= X Y) */
  std::shared_ptr<ProofNode> eqXFromY(bool y, Node parent);
  /** Derive Y from (= X Y) */
  std::shared_ptr<ProofNode> eqYFromX(bool x, Node parent);
  /** Derive X from (not (= X Y)) */
  std::shared_ptr<ProofNode> neqXFromY(bool y, Node parent);
  /** Derive Y from (not (= X Y)) */
  std::shared_ptr<ProofNode> neqYFromX(bool x, Node parent);

  /**
   * Uses (xor X Y) to derive the value of X.
   * (xor X false)  -->  X
   * (xor X true)  -->  (not X)
   * (not (xor X false))  -->  (not X)
   * (not (xor X true))  -->  X
   */
  std::shared_ptr<ProofNode> xorXFromY(bool negated, bool y, Node parent);
  /**
   * Uses (xor X Y) to derive the value of Y.
   * (xor false Y)  -->  Y
   * (xor true Y)  -->  (not Y)
   * (not (xor false Y))  -->  (not Y)
   * (not (xor true Y))  -->  Y
   */
  std::shared_ptr<ProofNode> xorYFromX(bool negated, bool x, Node parent);

 protected:
  /** Shorthand to check whether proof generation is disabled */
  bool disabled() const;

  /** Construct proof using the given rule, children and args */
  std::shared_ptr<ProofNode> mkProof(
      PfRule rule,
      const std::vector<std::shared_ptr<ProofNode>>& children,
      const std::vector<Node>& args = {});
  /**
   * Apply CHAIN_RESOLUTION rule.
   * Constructs the args from the given literals and polarities (called ids in
   * the proof rule). Automatically adds the clauses to resolve with as
   * assumptions, depending on their polarity.
   */
  std::shared_ptr<ProofNode> mkCResolution(
      const std::shared_ptr<ProofNode>& clause,
      const std::vector<Node>& lits,
      const std::vector<bool>& polarity);
  /** Shorthand for mkCResolution(clause, lits, {polarity, ...}) */
  std::shared_ptr<ProofNode> mkCResolution(
      const std::shared_ptr<ProofNode>& clause,
      const std::vector<Node>& lits,
      bool polarity);
  /** Apply RESOLUTION rule */
  std::shared_ptr<ProofNode> mkResolution(
      const std::shared_ptr<ProofNode>& clause, const Node& lit, bool polarity);
  /** Apply NOT_NOT_ELIM rule if n.getResult() is a nested negation */
  std::shared_ptr<ProofNode> mkNot(const std::shared_ptr<ProofNode>& n);

  /** The proof node manager */
  ProofNodeManager* d_pnm;
};

/**
 * Proof generator for backward propagation
 * A backward propagation is triggered by the assignment of the parent node.
 */
class ProofCircuitPropagatorBackward : public ProofCircuitPropagator
{
 public:
  ProofCircuitPropagatorBackward(ProofNodeManager* pnm,
                                 TNode parent,
                                 bool parentAssignment);

  /** and true  -->  child is true */
  std::shared_ptr<ProofNode> andTrue(TNode::iterator i);

  /** or false  -->  child is false */
  std::shared_ptr<ProofNode> orFalse(TNode::iterator i);

  /**
   * Propagate on ite with evaluate condition
   * (ite true t e)  -->  t
   * (not (ite true t e))  -->  (not t)
   * (ite false t e)  -->  e
   * (not (ite false t e))  -->  (not e)
   */
  std::shared_ptr<ProofNode> iteC(bool c);
  /**
   * For (ite c t e), we can derive the value for c
   * c = 1: c = true
   * c = 0: c = false
   */
  std::shared_ptr<ProofNode> iteIsCase(unsigned c);

  /** (not (=> X Y))  -->  X */
  std::shared_ptr<ProofNode> impliesNegX();
  /** (not (=> X Y))  -->  (not Y) */
  std::shared_ptr<ProofNode> impliesNegY();

 private:
  /** The parent node */
  TNode d_parent;
  /** The assignment of d_parent */
  bool d_parentAssignment;
};

/**
 * Proof generator for forward propagation
 * A forward propagation is triggered by the assignment of a child node.
 */
class ProofCircuitPropagatorForward : public ProofCircuitPropagator
{
 public:
  ProofCircuitPropagatorForward(ProofNodeManager* pnm,
                                Node child,
                                bool childAssignment,
                                Node parent);

  /** All children are true  -->  and is true */
  std::shared_ptr<ProofNode> andAllTrue();
  /** One child is false  -->  and is false */
  std::shared_ptr<ProofNode> andOneFalse();

  /** One child is true  -->  or is true */
  std::shared_ptr<ProofNode> orOneTrue();
  /** or false  -->  all children are false */
  std::shared_ptr<ProofNode> orFalse();

  /** Evaluate (ite true X _) from X */
  std::shared_ptr<ProofNode> iteEvalThen(bool x);
  /** Evaluate (ite false _ Y) from Y */
  std::shared_ptr<ProofNode> iteEvalElse(bool y);

  /** Evaluate (= X Y) from X,Y */
  std::shared_ptr<ProofNode> eqEval(bool x, bool y);

  /** Evaluate (=> X Y) from X,Y */
  std::shared_ptr<ProofNode> impliesEval(bool premise, bool conclusion);
  /** Evaluate (xor X Y) from X,Y */
  std::shared_ptr<ProofNode> xorEval(bool x, bool y);

 private:
  /** The current child that triggered the propagations */
  Node d_child;
  /** The assignment of d_child */
  bool d_childAssignment;
  /** The parent node used for propagation */
  Node d_parent;
};

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

#endif


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 "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__BOOLEANS__PROOF_CIRCUIT_PROPAGATOR_H
19		#define CVC5__THEORY__BOOLEANS__PROOF_CIRCUIT_PROPAGATOR_H
20
21		#include <memory>
22
23		#include "expr/node.h"
24		#include "proof/proof_rule.h"
25
26		namespace cvc5 {
27
28		class ProofNode;
29		class ProofNodeManager;
30
31		namespace theory {
32		namespace booleans {
33
34		/**
35		* Base class for for CircuitPropagatorProofs.
36		* This class collects common functionality for proofs of backward and forward
37		* propagation.
38		*/
39		class ProofCircuitPropagator
40		{
41		public:
42		ProofCircuitPropagator(ProofNodeManager* pnm);
43
44		/** Assuming the given node */
45		std::shared_ptr<ProofNode> assume(Node n);
46		/** Apply CONTRA rule. Takes care of switching a and b if necessary */
47		std::shared_ptr<ProofNode> conflict(const std::shared_ptr<ProofNode>& a,
48		const std::shared_ptr<ProofNode>& b);
49
50		/** (and true ... holdout true ...) --> holdout */
51		std::shared_ptr<ProofNode> andFalse(Node parent, TNode::iterator holdout);
52
53		/** (or false ... holdout false ...) -> holdout */
54		std::shared_ptr<ProofNode> orTrue(Node parent, TNode::iterator holdout);
55
56		/** (not x) is true --> x is false (and vice versa) */
57		std::shared_ptr<ProofNode> Not(bool negate, Node parent);
58
59		/** (=> X false) --> (not X) */
60		std::shared_ptr<ProofNode> impliesXFromY(Node parent);
61		/** (=> true Y) --> Y */
62		std::shared_ptr<ProofNode> impliesYFromX(Node parent);
63
64		/** Derive X from (= X Y) */
65		std::shared_ptr<ProofNode> eqXFromY(bool y, Node parent);
66		/** Derive Y from (= X Y) */
67		std::shared_ptr<ProofNode> eqYFromX(bool x, Node parent);
68		/** Derive X from (not (= X Y)) */
69		std::shared_ptr<ProofNode> neqXFromY(bool y, Node parent);
70		/** Derive Y from (not (= X Y)) */
71		std::shared_ptr<ProofNode> neqYFromX(bool x, Node parent);
72
73		/**
74		* Uses (xor X Y) to derive the value of X.
75		* (xor X false) --> X
76		* (xor X true) --> (not X)
77		* (not (xor X false)) --> (not X)
78		* (not (xor X true)) --> X
79		*/
80		std::shared_ptr<ProofNode> xorXFromY(bool negated, bool y, Node parent);
81		/**
82		* Uses (xor X Y) to derive the value of Y.
83		* (xor false Y) --> Y
84		* (xor true Y) --> (not Y)
85		* (not (xor false Y)) --> (not Y)
86		* (not (xor true Y)) --> Y
87		*/
88		std::shared_ptr<ProofNode> xorYFromX(bool negated, bool x, Node parent);
89
90		protected:
91		/** Shorthand to check whether proof generation is disabled */
92		bool disabled() const;
93
94		/** Construct proof using the given rule, children and args */
95		std::shared_ptr<ProofNode> mkProof(
96		PfRule rule,
97		const std::vector<std::shared_ptr<ProofNode>>& children,
98		const std::vector<Node>& args = {});
99		/**
100		* Apply CHAIN_RESOLUTION rule.
101		* Constructs the args from the given literals and polarities (called ids in
102		* the proof rule). Automatically adds the clauses to resolve with as
103		* assumptions, depending on their polarity.
104		*/
105		std::shared_ptr<ProofNode> mkCResolution(
106		const std::shared_ptr<ProofNode>& clause,
107		const std::vector<Node>& lits,
108		const std::vector<bool>& polarity);
109		/** Shorthand for mkCResolution(clause, lits, {polarity, ...}) */
110		std::shared_ptr<ProofNode> mkCResolution(
111		const std::shared_ptr<ProofNode>& clause,
112		const std::vector<Node>& lits,
113		bool polarity);
114		/** Apply RESOLUTION rule */
115		std::shared_ptr<ProofNode> mkResolution(
116		const std::shared_ptr<ProofNode>& clause, const Node& lit, bool polarity);
117		/** Apply NOT_NOT_ELIM rule if n.getResult() is a nested negation */
118		std::shared_ptr<ProofNode> mkNot(const std::shared_ptr<ProofNode>& n);
119
120		/** The proof node manager */
121		ProofNodeManager* d_pnm;
122		};
123
124		/**
125		* Proof generator for backward propagation
126		* A backward propagation is triggered by the assignment of the parent node.
127		*/
128	180039	class ProofCircuitPropagatorBackward : public ProofCircuitPropagator
129		{
130		public:
131		ProofCircuitPropagatorBackward(ProofNodeManager* pnm,
132		TNode parent,
133		bool parentAssignment);
134
135		/** and true --> child is true */
136		std::shared_ptr<ProofNode> andTrue(TNode::iterator i);
137
138		/** or false --> child is false */
139		std::shared_ptr<ProofNode> orFalse(TNode::iterator i);
140
141		/**
142		* Propagate on ite with evaluate condition
143		* (ite true t e) --> t
144		* (not (ite true t e)) --> (not t)
145		* (ite false t e) --> e
146		* (not (ite false t e)) --> (not e)
147		*/
148		std::shared_ptr<ProofNode> iteC(bool c);
149		/**
150		* For (ite c t e), we can derive the value for c
151		* c = 1: c = true
152		* c = 0: c = false
153		*/
154		std::shared_ptr<ProofNode> iteIsCase(unsigned c);
155
156		/** (not (=> X Y)) --> X */
157		std::shared_ptr<ProofNode> impliesNegX();
158		/** (not (=> X Y)) --> (not Y) */
159		std::shared_ptr<ProofNode> impliesNegY();
160
161		private:
162		/** The parent node */
163		TNode d_parent;
164		/** The assignment of d_parent */
165		bool d_parentAssignment;
166		};
167
168		/**
169		* Proof generator for forward propagation
170		* A forward propagation is triggered by the assignment of a child node.
171		*/
172	197494	class ProofCircuitPropagatorForward : public ProofCircuitPropagator
173		{
174		public:
175		ProofCircuitPropagatorForward(ProofNodeManager* pnm,
176		Node child,
177		bool childAssignment,
178		Node parent);
179
180		/** All children are true --> and is true */
181		std::shared_ptr<ProofNode> andAllTrue();
182		/** One child is false --> and is false */
183		std::shared_ptr<ProofNode> andOneFalse();
184
185		/** One child is true --> or is true */
186		std::shared_ptr<ProofNode> orOneTrue();
187		/** or false --> all children are false */
188		std::shared_ptr<ProofNode> orFalse();
189
190		/** Evaluate (ite true X _) from X */
191		std::shared_ptr<ProofNode> iteEvalThen(bool x);
192		/** Evaluate (ite false _ Y) from Y */
193		std::shared_ptr<ProofNode> iteEvalElse(bool y);
194
195		/** Evaluate (= X Y) from X,Y */
196		std::shared_ptr<ProofNode> eqEval(bool x, bool y);
197
198		/** Evaluate (=> X Y) from X,Y */
199		std::shared_ptr<ProofNode> impliesEval(bool premise, bool conclusion);
200		/** Evaluate (xor X Y) from X,Y */
201		std::shared_ptr<ProofNode> xorEval(bool x, bool y);
202
203		private:
204		/** The current child that triggered the propagations */
205		Node d_child;
206		/** The assignment of d_child */
207		bool d_childAssignment;
208		/** The parent node used for propagation */
209		Node d_parent;
210		};
211
212		} // namespace booleans
213		} // namespace theory
214		} // namespace cvc5
215
216		#endif