Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/preprocessing/passes/pseudo_boolean_processor.h	Lines:	3	3	100.0 %
Date:	2021-05-22	Branches:	8	14	57.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Andres Noetzli, Mathias Preiner
 *
 * 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.
 * ****************************************************************************
 *
 * [[ Add one-line brief description here ]]
 *
 * [[ Add lengthier description here ]]
 * \todo document this file
 */

#include "cvc5_private.h"

#ifndef CVC5__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
#define CVC5__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H

#include <unordered_set>
#include <vector>

#include "context/cdhashmap.h"
#include "context/cdo.h"
#include "expr/node.h"
#include "preprocessing/preprocessing_pass.h"
#include "theory/substitutions.h"
#include "util/maybe.h"
#include "util/rational.h"

namespace cvc5 {
namespace preprocessing {
namespace passes {

class PseudoBooleanProcessor : public PreprocessingPass
{
 public:
  PseudoBooleanProcessor(PreprocessingPassContext* preprocContext);

 protected:
  PreprocessingPassResult applyInternal(
      AssertionPipeline* assertionsToPreprocess) override;

 private:
  /** Assumes that the assertions have been rewritten. */
  void learn(const std::vector<Node>& assertions);

  /** Assumes that the assertions have been rewritten. */
  void applyReplacements(AssertionPipeline* assertionsToPreprocess);

  bool likelyToHelp() const;

  bool isPseudoBoolean(Node v) const;

  // Adds the fact the that integert typed variable v
  //   must be >= 0 to the context.
  // This is explained by the explanation exp.
  // exp cannot be null.
  void addGeqZero(Node v, Node exp);

  // Adds the fact the that integert typed variable v
  //   must be <= 1 to the context.
  // This is explained by the explanation exp.
  // exp cannot be null.
  void addLeqOne(Node v, Node exp);

  static inline bool isIntVar(Node v)
  {
    return v.isVar() && v.getType().isInteger();
  }

  void clear();

  /** Assumes that the assertion has been rewritten. */
  void learn(Node assertion);

  /** Rewrites a node  */
  Node applyReplacements(Node pre);

  void learnInternal(Node assertion, bool negated, Node orig);
  void learnRewrittenGeq(Node assertion, bool negated, Node orig);

  void addSub(Node from, Node to);
  void learnGeqSub(Node geq);

  static Node mkGeqOne(Node v);

  // x ->  <geqZero, leqOne>
  typedef context::CDHashMap<Node, std::pair<Node, Node>> CDNode2PairMap;
  CDNode2PairMap d_pbBounds;
  theory::SubstitutionMap d_subCache;

  typedef std::unordered_set<Node> NodeSet;
  NodeSet d_learningCache;

  context::CDO<unsigned> d_pbs;

  // decompose into \sum pos >= neg + off
  Maybe<Rational> d_off;
  std::vector<Node> d_pos;
  std::vector<Node> d_neg;

  /** Returns true if successful. */
  bool decomposeAssertion(Node assertion, bool negated);
};

}  // namespace passes
}  // namespace preprocessing
}  // namespace cvc5

#endif  // CVC5__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Tim King, Andres Noetzli, Mathias Preiner
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		* [[ Add one-line brief description here ]]
14		*
15		* [[ Add lengthier description here ]]
16		* \todo document this file
17		*/
18
19		#include "cvc5_private.h"
20
21		#ifndef CVC5__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
22		#define CVC5__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
23
24		#include <unordered_set>
25		#include <vector>
26
27		#include "context/cdhashmap.h"
28		#include "context/cdo.h"
29		#include "expr/node.h"
30		#include "preprocessing/preprocessing_pass.h"
31		#include "theory/substitutions.h"
32		#include "util/maybe.h"
33		#include "util/rational.h"
34
35		namespace cvc5 {
36		namespace preprocessing {
37		namespace passes {
38
39	18918	class PseudoBooleanProcessor : public PreprocessingPass
40		{
41		public:
42		PseudoBooleanProcessor(PreprocessingPassContext* preprocContext);
43
44		protected:
45		PreprocessingPassResult applyInternal(
46		AssertionPipeline* assertionsToPreprocess) override;
47
48		private:
49		/** Assumes that the assertions have been rewritten. */
50		void learn(const std::vector<Node>& assertions);
51
52		/** Assumes that the assertions have been rewritten. */
53		void applyReplacements(AssertionPipeline* assertionsToPreprocess);
54
55		bool likelyToHelp() const;
56
57		bool isPseudoBoolean(Node v) const;
58
59		// Adds the fact the that integert typed variable v
60		// must be >= 0 to the context.
61		// This is explained by the explanation exp.
62		// exp cannot be null.
63		void addGeqZero(Node v, Node exp);
64
65		// Adds the fact the that integert typed variable v
66		// must be <= 1 to the context.
67		// This is explained by the explanation exp.
68		// exp cannot be null.
69		void addLeqOne(Node v, Node exp);
70
71	802	static inline bool isIntVar(Node v)
72		{
73	802	return v.isVar() && v.getType().isInteger();
74		}
75
76		void clear();
77
78		/** Assumes that the assertion has been rewritten. */
79		void learn(Node assertion);
80
81		/** Rewrites a node */
82		Node applyReplacements(Node pre);
83
84		void learnInternal(Node assertion, bool negated, Node orig);
85		void learnRewrittenGeq(Node assertion, bool negated, Node orig);
86
87		void addSub(Node from, Node to);
88		void learnGeqSub(Node geq);
89
90		static Node mkGeqOne(Node v);
91
92		// x -> <geqZero, leqOne>
93		typedef context::CDHashMap<Node, std::pair<Node, Node>> CDNode2PairMap;
94		CDNode2PairMap d_pbBounds;
95		theory::SubstitutionMap d_subCache;
96
97		typedef std::unordered_set<Node> NodeSet;
98		NodeSet d_learningCache;
99
100		context::CDO<unsigned> d_pbs;
101
102		// decompose into \sum pos >= neg + off
103		Maybe<Rational> d_off;
104		std::vector<Node> d_pos;
105		std::vector<Node> d_neg;
106
107		/** Returns true if successful. */
108		bool decomposeAssertion(Node assertion, bool negated);
109		};
110
111		} // namespace passes
112		} // namespace preprocessing
113		} // namespace cvc5
114
115		#endif // CVC5__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H