Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/callbacks.h	Lines:	13	13	100.0 %
Date:	2021-05-24	Branches:	2	8	25.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Mathias Preiner, Clark Barrett
 *
 * 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
 */

#pragma once

#include "expr/node.h"
#include "theory/arith/arithvar.h"
#include "theory/arith/bound_counts.h"
#include "theory/arith/constraint_forward.h"
#include "theory/inference_id.h"
#include "util/rational.h"

namespace cvc5 {

class ProofNode;

namespace theory {
namespace arith {

class TheoryArithPrivate;

/**
 * ArithVarCallBack provides a mechanism for agreeing on callbacks while
 * breaking mutual recursion inclusion order problems.
 */
class ArithVarCallBack {
public:
  virtual ~ArithVarCallBack() {}
  virtual void operator()(ArithVar x) = 0;
};

/**
 * Requests arithmetic variables for internal use,
 * and releases arithmetic variables that are no longer being used.
 */
class ArithVarMalloc {
public:
  virtual ~ArithVarMalloc() {}
  virtual ArithVar request() = 0;
  virtual void release(ArithVar v) = 0;
};

class TNodeCallBack {
public:
  virtual ~TNodeCallBack() {}
  virtual void operator()(TNode n) = 0;
};

class NodeCallBack {
public:
  virtual ~NodeCallBack() {}
  virtual void operator()(Node n) = 0;
};

class RationalCallBack {
public:
  virtual ~RationalCallBack() {}
  virtual Rational operator()() const = 0;
};

class SetupLiteralCallBack : public TNodeCallBack {
private:
  TheoryArithPrivate& d_arith;
public:
  SetupLiteralCallBack(TheoryArithPrivate& ta);
  void operator()(TNode lit) override;
};

class DeltaComputeCallback : public RationalCallBack {
private:
  const TheoryArithPrivate& d_ta;
public:
  DeltaComputeCallback(const TheoryArithPrivate& ta);
  Rational operator()() const override;
};

class BasicVarModelUpdateCallBack : public ArithVarCallBack{
private:
  TheoryArithPrivate& d_ta;
public:
  BasicVarModelUpdateCallBack(TheoryArithPrivate& ta);
  void operator()(ArithVar x) override;
};

class TempVarMalloc : public ArithVarMalloc {
private:
  TheoryArithPrivate& d_ta;
public:
  TempVarMalloc(TheoryArithPrivate& ta);
  ArithVar request() override;
  void release(ArithVar v) override;
};

class RaiseConflict {
private:
  TheoryArithPrivate& d_ta;
public:
  RaiseConflict(TheoryArithPrivate& ta);

  /** Calls d_ta.raiseConflict(c) */
  void raiseConflict(ConstraintCP c, InferenceId id) const;
};

class FarkasConflictBuilder {
private:
  RationalVector d_farkas;
  ConstraintCPVec d_constraints;
  ConstraintCP d_consequent;
  bool d_consequentSet;
public:

  /**
   * Constructs a new FarkasConflictBuilder.
   */
  FarkasConflictBuilder();

  /**
   * Adds an antecedent constraint to the conflict under construction
   * with the farkas coefficient fc * mult.
   *
   * The value mult is either 1 or -1.
   */
  void addConstraint(ConstraintCP c, const Rational& fc, const Rational& mult);

  /**
   * Adds an antecedent constraint to the conflict under construction
   * with the farkas coefficient fc.
   */
  void addConstraint(ConstraintCP c, const Rational& fc);

  /**
   * Makes the last constraint added the consequent.
   * Can be done exactly once per reset().
   */
  void makeLastConsequent();

  /**
   * Turns the antecendents into a proof of the negation of one of the
   * antecedents.
   *
   * The buffer is no longer underConstruction afterwards.
   *
   * precondition:
   * - At least two constraints have been asserted.
   * - makeLastConsequent() has been called.
   *
   * postcondition: The returned constraint is in conflict.
   */
  ConstraintCP commitConflict();

  /** Returns true if a conflict has been pushed back since the last reset. */
  bool underConstruction() const;

  /** Returns true if the consequent has been set since the last reset. */
  bool consequentIsSet() const;

  /** Resets the state of the buffer. */
  void reset();
};


class RaiseEqualityEngineConflict {
private:
  TheoryArithPrivate& d_ta;

public:
  RaiseEqualityEngineConflict(TheoryArithPrivate& ta);

  /* If you are not an equality engine, don't use this!
   *
   * The proof should prove that `n` is a conflict.
   * */
  void raiseEEConflict(Node n, std::shared_ptr<ProofNode> pf) const;
};

class BoundCountingLookup {
private:
  TheoryArithPrivate& d_ta;
public:
  BoundCountingLookup(TheoryArithPrivate& ta);
  const BoundsInfo& boundsInfo(ArithVar basic) const;
  BoundCounts atBounds(ArithVar basic) const;
  BoundCounts hasBounds(ArithVar basic) const;
};

}  // namespace arith
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Tim King, Mathias Preiner, Clark Barrett
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		#pragma once
20
21		#include "expr/node.h"
22		#include "theory/arith/arithvar.h"
23		#include "theory/arith/bound_counts.h"
24		#include "theory/arith/constraint_forward.h"
25		#include "theory/inference_id.h"
26		#include "util/rational.h"
27
28		namespace cvc5 {
29
30		class ProofNode;
31
32		namespace theory {
33		namespace arith {
34
35		class TheoryArithPrivate;
36
37		/**
38		* ArithVarCallBack provides a mechanism for agreeing on callbacks while
39		* breaking mutual recursion inclusion order problems.
40		*/
41	18918	class ArithVarCallBack {
42		public:
43	18918	virtual ~ArithVarCallBack() {}
44		virtual void operator()(ArithVar x) = 0;
45		};
46
47		/**
48		* Requests arithmetic variables for internal use,
49		* and releases arithmetic variables that are no longer being used.
50		*/
51	113508	class ArithVarMalloc {
52		public:
53	113508	virtual ~ArithVarMalloc() {}
54		virtual ArithVar request() = 0;
55		virtual void release(ArithVar v) = 0;
56		};
57
58	18918	class TNodeCallBack {
59		public:
60	18918	virtual ~TNodeCallBack() {}
61		virtual void operator()(TNode n) = 0;
62		};
63
64		class NodeCallBack {
65		public:
66		virtual ~NodeCallBack() {}
67		virtual void operator()(Node n) = 0;
68		};
69
70	18918	class RationalCallBack {
71		public:
72	18918	virtual ~RationalCallBack() {}
73		virtual Rational operator()() const = 0;
74		};
75
76	28377	class SetupLiteralCallBack : public TNodeCallBack {
77		private:
78		TheoryArithPrivate& d_arith;
79		public:
80		SetupLiteralCallBack(TheoryArithPrivate& ta);
81		void operator()(TNode lit) override;
82		};
83
84	28377	class DeltaComputeCallback : public RationalCallBack {
85		private:
86		const TheoryArithPrivate& d_ta;
87		public:
88		DeltaComputeCallback(const TheoryArithPrivate& ta);
89		Rational operator()() const override;
90		};
91
92	28377	class BasicVarModelUpdateCallBack : public ArithVarCallBack{
93		private:
94		TheoryArithPrivate& d_ta;
95		public:
96		BasicVarModelUpdateCallBack(TheoryArithPrivate& ta);
97		void operator()(ArithVar x) override;
98		};
99
100	311290	class TempVarMalloc : public ArithVarMalloc {
101		private:
102		TheoryArithPrivate& d_ta;
103		public:
104		TempVarMalloc(TheoryArithPrivate& ta);
105		ArithVar request() override;
106		void release(ArithVar v) override;
107		};
108
109		class RaiseConflict {
110		private:
111		TheoryArithPrivate& d_ta;
112		public:
113		RaiseConflict(TheoryArithPrivate& ta);
114
115		/** Calls d_ta.raiseConflict(c) */
116		void raiseConflict(ConstraintCP c, InferenceId id) const;
117		};
118
119	37836	class FarkasConflictBuilder {
120		private:
121		RationalVector d_farkas;
122		ConstraintCPVec d_constraints;
123		ConstraintCP d_consequent;
124		bool d_consequentSet;
125		public:
126
127		/**
128		* Constructs a new FarkasConflictBuilder.
129		*/
130		FarkasConflictBuilder();
131
132		/**
133		* Adds an antecedent constraint to the conflict under construction
134		* with the farkas coefficient fc * mult.
135		*
136		* The value mult is either 1 or -1.
137		*/
138		void addConstraint(ConstraintCP c, const Rational& fc, const Rational& mult);
139
140		/**
141		* Adds an antecedent constraint to the conflict under construction
142		* with the farkas coefficient fc.
143		*/
144		void addConstraint(ConstraintCP c, const Rational& fc);
145
146		/**
147		* Makes the last constraint added the consequent.
148		* Can be done exactly once per reset().
149		*/
150		void makeLastConsequent();
151
152		/**
153		* Turns the antecendents into a proof of the negation of one of the
154		* antecedents.
155		*
156		* The buffer is no longer underConstruction afterwards.
157		*
158		* precondition:
159		* - At least two constraints have been asserted.
160		* - makeLastConsequent() has been called.
161		*
162		* postcondition: The returned constraint is in conflict.
163		*/
164		ConstraintCP commitConflict();
165
166		/** Returns true if a conflict has been pushed back since the last reset. */
167		bool underConstruction() const;
168
169		/** Returns true if the consequent has been set since the last reset. */
170		bool consequentIsSet() const;
171
172		/** Resets the state of the buffer. */
173		void reset();
174		};
175
176
177		class RaiseEqualityEngineConflict {
178		private:
179		TheoryArithPrivate& d_ta;
180
181		public:
182		RaiseEqualityEngineConflict(TheoryArithPrivate& ta);
183
184		/* If you are not an equality engine, don't use this!
185		*
186		* The proof should prove that `n` is a conflict.
187		* */
188		void raiseEEConflict(Node n, std::shared_ptr<ProofNode> pf) const;
189		};
190
191		class BoundCountingLookup {
192		private:
193		TheoryArithPrivate& d_ta;
194		public:
195		BoundCountingLookup(TheoryArithPrivate& ta);
196		const BoundsInfo& boundsInfo(ArithVar basic) const;
197		BoundCounts atBounds(ArithVar basic) const;
198		BoundCounts hasBounds(ArithVar basic) const;
199		};
200
201		} // namespace arith
202		} // namespace theory
203		} // namespace cvc5