Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bv_solver_bitblast.h	Lines:	0	4	0.0 %
Date:	2021-05-22	Branches:	0	2	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Mathias Preiner, Andrew Reynolds
 *
 * 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.
 * ****************************************************************************
 *
 * Bit-blasting solver that supports multiple SAT back ends.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__BV__BV_SOLVER_BITBLAST_H
#define CVC5__THEORY__BV__BV_SOLVER_BITBLAST_H

#include <unordered_map>

#include "context/cdqueue.h"
#include "prop/cnf_stream.h"
#include "prop/sat_solver.h"
#include "theory/bv/bitblast/simple_bitblaster.h"
#include "theory/bv/bv_solver.h"
#include "theory/bv/proof_checker.h"
#include "theory/eager_proof_generator.h"

namespace cvc5 {

namespace theory {
namespace bv {

class BBRegistrar;

/**
 * Bit-blasting solver with support for different SAT back ends.
 */
class BVSolverBitblast : public BVSolver
{
 public:
  BVSolverBitblast(TheoryState* state,
                   TheoryInferenceManager& inferMgr,
                   ProofNodeManager* pnm);
  ~BVSolverBitblast() = default;

  bool needsEqualityEngine(EeSetupInfo& esi) override { return true; }

  void preRegisterTerm(TNode n) override {}

  void postCheck(Theory::Effort level) override;

  bool preNotifyFact(TNode atom,
                     bool pol,
                     TNode fact,
                     bool isPrereg,
                     bool isInternal) override;

  TrustNode explain(TNode n) override;

  std::string identify() const override { return "BVSolverBitblast"; };

  EqualityStatus getEqualityStatus(TNode a, TNode b) override;

  bool collectModelValues(TheoryModel* m,
                          const std::set<Node>& termSet) override;

 private:
  /**
   * Get value of `node` from SAT solver.
   *
   * The `initialize` flag indicates whether bits should be zero-initialized
   * if they were not bit-blasted yet.
   */
  Node getValueFromSatSolver(TNode node, bool initialize);

  /**
   * Get the current value of `node`.
   *
   * Computes the value if `node` was not yet bit-blasted.
   */
  Node getValue(TNode node);

  /**
   * Handle BITVECTOR_EAGER_ATOM atoms and assert/assume to CnfStream.
   *
   * @param assertFact: Indicates whether the fact should be asserted (true) or
   * assumed (false).
   */
  void handleEagerAtom(TNode fact, bool assertFact);

  /**
   * Cache for getValue() calls.
   *
   * Is cleared at the beginning of a getValue() call if the
   * `d_invalidateModelCache` flag is set to true.
   */
  std::unordered_map<Node, Node> d_modelCache;

  /** Bit-blaster used to bit-blast atoms/terms. */
  std::unique_ptr<BBSimple> d_bitblaster;

  /** Used for initializing `d_cnfStream`. */
  std::unique_ptr<BBRegistrar> d_bbRegistrar;
  std::unique_ptr<context::Context> d_nullContext;

  /** SAT solver back end (configured via options::bvSatSolver. */
  std::unique_ptr<prop::SatSolver> d_satSolver;
  /** CNF stream. */
  std::unique_ptr<prop::CnfStream> d_cnfStream;

  /**
   * Bit-blast queue for facts sent to this solver.
   *
   * Get populated on preNotifyFact().
   */
  context::CDQueue<Node> d_bbFacts;

  /**
   * Bit-blast queue for user-level 0 input facts sent to this solver.
   *
   * Get populated on preNotifyFact().
   */
  context::CDQueue<Node> d_bbInputFacts;

  /** Corresponds to the SAT literals of the currently asserted facts. */
  context::CDList<prop::SatLiteral> d_assumptions;

  /** Stores the current input assertions. */
  context::CDList<Node> d_assertions;

  /** Flag indicating whether `d_modelCache` should be invalidated. */
  context::CDO<bool> d_invalidateModelCache;

  /** Indicates whether the last check() call was satisfiable. */
  context::CDO<bool> d_inSatMode;

  /** Proof generator that manages proofs for lemmas generated by this class. */
  std::unique_ptr<EagerProofGenerator> d_epg;

  BVProofRuleChecker d_bvProofChecker;

  /** Stores the SatLiteral for a given fact. */
  context::CDHashMap<Node, prop::SatLiteral> d_factLiteralCache;

  /** Reverse map of `d_factLiteralCache`. */
  context::CDHashMap<prop::SatLiteral, Node, prop::SatLiteralHashFunction>
      d_literalFactCache;

  /** Option to enable/disable bit-level propagation. */
  bool d_propagate;
};

}  // namespace bv
}  // namespace theory
}  // namespace cvc5

#endif


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Mathias Preiner, Andrew Reynolds
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		* Bit-blasting solver that supports multiple SAT back ends.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__BV__BV_SOLVER_BITBLAST_H
19		#define CVC5__THEORY__BV__BV_SOLVER_BITBLAST_H
20
21		#include <unordered_map>
22
23		#include "context/cdqueue.h"
24		#include "prop/cnf_stream.h"
25		#include "prop/sat_solver.h"
26		#include "theory/bv/bitblast/simple_bitblaster.h"
27		#include "theory/bv/bv_solver.h"
28		#include "theory/bv/proof_checker.h"
29		#include "theory/eager_proof_generator.h"
30
31		namespace cvc5 {
32
33		namespace theory {
34		namespace bv {
35
36		class BBRegistrar;
37
38		/**
39		* Bit-blasting solver with support for different SAT back ends.
40		*/
41		class BVSolverBitblast : public BVSolver
42		{
43		public:
44		BVSolverBitblast(TheoryState* state,
45		TheoryInferenceManager& inferMgr,
46		ProofNodeManager* pnm);
47		~BVSolverBitblast() = default;
48
49		bool needsEqualityEngine(EeSetupInfo& esi) override { return true; }
50
51		void preRegisterTerm(TNode n) override {}
52
53		void postCheck(Theory::Effort level) override;
54
55		bool preNotifyFact(TNode atom,
56		bool pol,
57		TNode fact,
58		bool isPrereg,
59		bool isInternal) override;
60
61		TrustNode explain(TNode n) override;
62
63		std::string identify() const override { return "BVSolverBitblast"; };
64
65		EqualityStatus getEqualityStatus(TNode a, TNode b) override;
66
67		bool collectModelValues(TheoryModel* m,
68		const std::set<Node>& termSet) override;
69
70		private:
71		/**
72		* Get value of `node` from SAT solver.
73		*
74		* The `initialize` flag indicates whether bits should be zero-initialized
75		* if they were not bit-blasted yet.
76		*/
77		Node getValueFromSatSolver(TNode node, bool initialize);
78
79		/**
80		* Get the current value of `node`.
81		*
82		* Computes the value if `node` was not yet bit-blasted.
83		*/
84		Node getValue(TNode node);
85
86		/**
87		* Handle BITVECTOR_EAGER_ATOM atoms and assert/assume to CnfStream.
88		*
89		* @param assertFact: Indicates whether the fact should be asserted (true) or
90		* assumed (false).
91		*/
92		void handleEagerAtom(TNode fact, bool assertFact);
93
94		/**
95		* Cache for getValue() calls.
96		*
97		* Is cleared at the beginning of a getValue() call if the
98		* `d_invalidateModelCache` flag is set to true.
99		*/
100		std::unordered_map<Node, Node> d_modelCache;
101
102		/** Bit-blaster used to bit-blast atoms/terms. */
103		std::unique_ptr<BBSimple> d_bitblaster;
104
105		/** Used for initializing `d_cnfStream`. */
106		std::unique_ptr<BBRegistrar> d_bbRegistrar;
107		std::unique_ptr<context::Context> d_nullContext;
108
109		/** SAT solver back end (configured via options::bvSatSolver. */
110		std::unique_ptr<prop::SatSolver> d_satSolver;
111		/** CNF stream. */
112		std::unique_ptr<prop::CnfStream> d_cnfStream;
113
114		/**
115		* Bit-blast queue for facts sent to this solver.
116		*
117		* Get populated on preNotifyFact().
118		*/
119		context::CDQueue<Node> d_bbFacts;
120
121		/**
122		* Bit-blast queue for user-level 0 input facts sent to this solver.
123		*
124		* Get populated on preNotifyFact().
125		*/
126		context::CDQueue<Node> d_bbInputFacts;
127
128		/** Corresponds to the SAT literals of the currently asserted facts. */
129		context::CDList<prop::SatLiteral> d_assumptions;
130
131		/** Stores the current input assertions. */
132		context::CDList<Node> d_assertions;
133
134		/** Flag indicating whether `d_modelCache` should be invalidated. */
135		context::CDO<bool> d_invalidateModelCache;
136
137		/** Indicates whether the last check() call was satisfiable. */
138		context::CDO<bool> d_inSatMode;
139
140		/** Proof generator that manages proofs for lemmas generated by this class. */
141		std::unique_ptr<EagerProofGenerator> d_epg;
142
143		BVProofRuleChecker d_bvProofChecker;
144
145		/** Stores the SatLiteral for a given fact. */
146		context::CDHashMap<Node, prop::SatLiteral> d_factLiteralCache;
147
148		/** Reverse map of `d_factLiteralCache`. */
149		context::CDHashMap<prop::SatLiteral, Node, prop::SatLiteralHashFunction>
150		d_literalFactCache;
151
152		/** Option to enable/disable bit-level propagation. */
153		bool d_propagate;
154		};
155
156		} // namespace bv
157		} // namespace theory
158		} // namespace cvc5
159
160		#endif