Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/callbacks.h	Lines:	13	13	100.0 %
Date:	2021-09-29	Branches:	0	0	0.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;
  bool d_produceProofs;

 public:

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

  /**
   * 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	12542	class ArithVarCallBack {
42		public:
43	12539	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	75252	class ArithVarMalloc {
52		public:
53	75240	virtual ~ArithVarMalloc() {}
54		virtual ArithVar request() = 0;
55		virtual void release(ArithVar v) = 0;
56		};
57
58	12542	class TNodeCallBack {
59		public:
60	12539	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	12542	class RationalCallBack {
71		public:
72	12539	virtual ~RationalCallBack() {}
73		virtual Rational operator()() const = 0;
74		};
75
76	18810	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	18810	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	18810	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	125408	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	25072	class FarkasConflictBuilder {
120		private:
121		RationalVector d_farkas;
122		ConstraintCPVec d_constraints;
123		ConstraintCP d_consequent;
124		bool d_consequentSet;
125		bool d_produceProofs;
126
127		public:
128
129		/**
130		* Constructs a new FarkasConflictBuilder.
131		*/
132		FarkasConflictBuilder(bool produceProofs);
133
134		/**
135		* Adds an antecedent constraint to the conflict under construction
136		* with the farkas coefficient fc * mult.
137		*
138		* The value mult is either 1 or -1.
139		*/
140		void addConstraint(ConstraintCP c, const Rational& fc, const Rational& mult);
141
142		/**
143		* Adds an antecedent constraint to the conflict under construction
144		* with the farkas coefficient fc.
145		*/
146		void addConstraint(ConstraintCP c, const Rational& fc);
147
148		/**
149		* Makes the last constraint added the consequent.
150		* Can be done exactly once per reset().
151		*/
152		void makeLastConsequent();
153
154		/**
155		* Turns the antecendents into a proof of the negation of one of the
156		* antecedents.
157		*
158		* The buffer is no longer underConstruction afterwards.
159		*
160		* precondition:
161		* - At least two constraints have been asserted.
162		* - makeLastConsequent() has been called.
163		*
164		* postcondition: The returned constraint is in conflict.
165		*/
166		ConstraintCP commitConflict();
167
168		/** Returns true if a conflict has been pushed back since the last reset. */
169		bool underConstruction() const;
170
171		/** Returns true if the consequent has been set since the last reset. */
172		bool consequentIsSet() const;
173
174		/** Resets the state of the buffer. */
175		void reset();
176		};
177
178
179		class RaiseEqualityEngineConflict {
180		private:
181		TheoryArithPrivate& d_ta;
182
183		public:
184		RaiseEqualityEngineConflict(TheoryArithPrivate& ta);
185
186		/* If you are not an equality engine, don't use this!
187		*
188		* The proof should prove that `n` is a conflict.
189		* */
190		void raiseEEConflict(Node n, std::shared_ptr<ProofNode> pf) const;
191		};
192
193		class BoundCountingLookup {
194		private:
195		TheoryArithPrivate& d_ta;
196		public:
197		BoundCountingLookup(TheoryArithPrivate& ta);
198		const BoundsInfo& boundsInfo(ArithVar basic) const;
199		BoundCounts atBounds(ArithVar basic) const;
200		BoundCounts hasBounds(ArithVar basic) const;
201		};
202
203		} // namespace arith
204		} // namespace theory
205		} // namespace cvc5