Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bv_solver.h	Lines:	16	26	61.5 %
Date:	2021-05-24	Branches:	0	8	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Mathias Preiner, Andrew Reynolds, Andres Noetzli
 *
 * 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-vector solver interface.
 *
 * Describes the interface for the internal bit-vector solver of TheoryBV.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__BV__BV_SOLVER_H
#define CVC5__THEORY__BV__BV_SOLVER_H

#include "theory/theory.h"

namespace cvc5 {
namespace theory {
namespace bv {

class BVSolver
{
 public:
  BVSolver(TheoryState& state, TheoryInferenceManager& inferMgr)
      : d_state(state), d_im(inferMgr){};

  virtual ~BVSolver(){};

  /**
   * Returns true if we need an equality engine. If so, we initialize the
   * information regarding how it should be setup. For details, see the
   * documentation in Theory::needsEqualityEngine.
   */
  virtual bool needsEqualityEngine(EeSetupInfo& esi) { return false; }

  virtual void finishInit(){};

  virtual void preRegisterTerm(TNode n) = 0;

  /**
   * Forwarded from TheoryBV::preCheck().
   */
  virtual bool preCheck(Theory::Effort level = Theory::Effort::EFFORT_FULL)
  {
    return false;
  }
  /**
   * Forwarded from TheoryBV::postCheck().
   */
  virtual void postCheck(Theory::Effort level = Theory::Effort::EFFORT_FULL){};
  /**
   * Forwarded from TheoryBV:preNotifyFact().
   */
  virtual bool preNotifyFact(
      TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
  {
    return false;
  }
  /**
   * Forwarded from TheoryBV::notifyFact().
   */
  virtual void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) {}

  virtual bool needsCheckLastEffort() { return false; }

  virtual void propagate(Theory::Effort e){};

  virtual TrustNode explain(TNode n)
  {
    Unimplemented() << "BVSolver propagated a node but doesn't implement the "
                       "BVSolver::explain() interface!";
    return TrustNode::null();
  }

  /** Collect model values in m based on the relevant terms given by termSet */
  virtual bool collectModelValues(TheoryModel* m,
                                  const std::set<Node>& termSet) = 0;

  virtual std::string identify() const = 0;

  virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); };

  virtual void ppStaticLearn(TNode in, NodeBuilder& learned){};

  virtual void presolve(){};

  virtual void notifySharedTerm(TNode t) {}

  virtual EqualityStatus getEqualityStatus(TNode a, TNode b)
  {
    return EqualityStatus::EQUALITY_UNKNOWN;
  }

  /** Called by abstraction preprocessing pass. */
  virtual bool applyAbstraction(const std::vector<Node>& assertions,
                                std::vector<Node>& new_assertions)
  {
    new_assertions.insert(
        new_assertions.end(), assertions.begin(), assertions.end());
    return false;
  };

 protected:
  TheoryState& d_state;
  TheoryInferenceManager& d_im;
};

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

#endif /* CVC5__THEORY__BV__BV_SOLVER_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Mathias Preiner, Andrew Reynolds, Andres Noetzli
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-vector solver interface.
14		*
15		* Describes the interface for the internal bit-vector solver of TheoryBV.
16		*/
17
18		#include "cvc5_private.h"
19
20		#ifndef CVC5__THEORY__BV__BV_SOLVER_H
21		#define CVC5__THEORY__BV__BV_SOLVER_H
22
23		#include "theory/theory.h"
24
25		namespace cvc5 {
26		namespace theory {
27		namespace bv {
28
29		class BVSolver
30		{
31		public:
32	9459	BVSolver(TheoryState& state, TheoryInferenceManager& inferMgr)
33	9459	: d_state(state), d_im(inferMgr){};
34
35	9459	virtual ~BVSolver(){};
36
37		/**
38		* Returns true if we need an equality engine. If so, we initialize the
39		* information regarding how it should be setup. For details, see the
40		* documentation in Theory::needsEqualityEngine.
41		*/
42	15	virtual bool needsEqualityEngine(EeSetupInfo& esi) { return false; }
43
44	15	virtual void finishInit(){};
45
46		virtual void preRegisterTerm(TNode n) = 0;
47
48		/**
49		* Forwarded from TheoryBV::preCheck().
50		*/
51	211	virtual bool preCheck(Theory::Effort level = Theory::Effort::EFFORT_FULL)
52		{
53	211	return false;
54		}
55		/**
56		* Forwarded from TheoryBV::postCheck().
57		*/
58	211	virtual void postCheck(Theory::Effort level = Theory::Effort::EFFORT_FULL){};
59		/**
60		* Forwarded from TheoryBV:preNotifyFact().
61		*/
62		virtual bool preNotifyFact(
63		TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
64		{
65		return false;
66		}
67		/**
68		* Forwarded from TheoryBV::notifyFact().
69		*/
70		virtual void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) {}
71
72	15	virtual bool needsCheckLastEffort() { return false; }
73
74	289	virtual void propagate(Theory::Effort e){};
75
76		virtual TrustNode explain(TNode n)
77		{
78		Unimplemented() << "BVSolver propagated a node but doesn't implement the "
79		"BVSolver::explain() interface!";
80		return TrustNode::null();
81		}
82
83		/** Collect model values in m based on the relevant terms given by termSet */
84		virtual bool collectModelValues(TheoryModel* m,
85		const std::set<Node>& termSet) = 0;
86
87		virtual std::string identify() const = 0;
88
89	628	virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); };
90
91	38	virtual void ppStaticLearn(TNode in, NodeBuilder& learned){};
92
93	19	virtual void presolve(){};
94
95	90	virtual void notifySharedTerm(TNode t) {}
96
97	64	virtual EqualityStatus getEqualityStatus(TNode a, TNode b)
98		{
99	64	return EqualityStatus::EQUALITY_UNKNOWN;
100		}
101
102		/** Called by abstraction preprocessing pass. */
103		virtual bool applyAbstraction(const std::vector<Node>& assertions,
104		std::vector<Node>& new_assertions)
105		{
106		new_assertions.insert(
107		new_assertions.end(), assertions.begin(), assertions.end());
108		return false;
109		};
110
111		protected:
112		TheoryState& d_state;
113		TheoryInferenceManager& d_im;
114		};
115
116		} // namespace bv
117		} // namespace theory
118		} // namespace cvc5
119
120		#endif /* CVC5__THEORY__BV__BV_SOLVER_H */