Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/logic_info.h	Lines:	23	23	100.0 %
Date:	2021-09-12	Branches:	15	18	83.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Andrew Reynolds, Tim King
 *
 * 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.
 * ****************************************************************************
 *
 * A class giving information about a logic (group of theory modules and
 * configuration information).
 */

#include "cvc5_public.h"

#ifndef CVC5__LOGIC_INFO_H
#define CVC5__LOGIC_INFO_H

#include <string>
#include <vector>

#include "cvc5_export.h"
#include "theory/theory_id.h"

namespace cvc5 {

/**
 * A LogicInfo instance describes a collection of theory modules and some
 * basic configuration about them.  Conceptually, it provides a background
 * context for all operations in cvc5.  Typically, when cvc5's SmtEngine
 * is created, it is issued a setLogic() command indicating features of the
 * assertions and queries to follow---for example, whether quantifiers are
 * used, whether integers or reals (or both) will be used, etc.
 *
 * Most places in cvc5 will only ever need to access a const reference to an
 * instance of this class.  Such an instance is generally set by the SmtEngine
 * when setLogic() is called.  However, mutating member functions are also
 * provided by this class so that it can be used as a more general mechanism
 * (e.g., for communicating to the SmtEngine which theories should be used,
 * rather than having to provide an SMT-LIB string).
 */
class CVC5_EXPORT LogicInfo
{
  mutable std::string d_logicString; /**< an SMT-LIB-like logic string */
  std::vector<bool> d_theories; /**< set of active theories */
  size_t d_sharingTheories; /**< count of theories that need sharing */

  /** are integers used in this logic? */
  bool d_integers;
  /** are reals used in this logic? */
  bool d_reals;
  /** transcendentals in this logic? */
  bool d_transcendentals;
  /** linear-only arithmetic in this logic? */
  bool d_linear;
  /** difference-only arithmetic in this logic? */
  bool d_differenceLogic;
  /** cardinality constraints in this logic? */
  bool d_cardinalityConstraints;
  /** higher-order constraints in this logic? */
  bool d_higherOrder;

  bool d_locked; /**< is this LogicInfo instance locked (and thus immutable)? */

  /**
   * Returns true iff this is a "true" theory (one that must be worried
   * about for sharing
   */
  static inline bool isTrueTheory(theory::TheoryId theory) {
    switch(theory) {
    case theory::THEORY_BUILTIN:
    case theory::THEORY_BOOL:
    case theory::THEORY_QUANTIFIERS:
      return false;
    default:
      return true;
    }
  }

public:

  /**
   * Constructs a LogicInfo for the most general logic (quantifiers, all
   * background theory modules, ...).
   */
  LogicInfo();

  /**
   * Construct a LogicInfo from an SMT-LIB-like logic string.
   * Throws an IllegalArgumentException if the logic string cannot
   * be interpreted.
   */
  LogicInfo(std::string logicString);

  /**
   * Construct a LogicInfo from an SMT-LIB-like logic string.
   * Throws an IllegalArgumentException if the logic string cannot
   * be interpreted.
   */
  LogicInfo(const char* logicString);

  // ACCESSORS

  /**
   * Get an SMT-LIB-like logic string.  These are only guaranteed to
   * be SMT-LIB-compliant if an SMT-LIB-compliant string was used in
   * the constructor and no mutating functions were called.
   */
  std::string getLogicString() const;

  /** Is sharing enabled for this logic? */
  bool isSharingEnabled() const;

  /** Is the given theory module active in this logic? */
  bool isTheoryEnabled(theory::TheoryId theory) const;

  /** Is this a quantified logic? */
  bool isQuantified() const;

  /** Is this a logic that includes the all-inclusive logic?
   *
   * @return Yields true if the logic corresponds to "ALL" or its super
   * set including , such as "HO_ALL".
   */
  bool hasEverything() const;

  /** Is this the all-exclusive logic?  (Here, that means propositional logic) */
  bool hasNothing() const;

  /**
   * Is this a pure logic (only one "true" background theory).  Quantifiers
   * can exist in such logics though; to test for quantifier-free purity,
   * use "isPure(theory) && !isQuantified()".
   */
  bool isPure(theory::TheoryId theory) const;

  // these are for arithmetic

  /** Are integers in this logic? */
  bool areIntegersUsed() const;

  /** Are reals in this logic? */
  bool areRealsUsed() const;

  /** Are transcendentals in this logic? */
  bool areTranscendentalsUsed() const;

  /** Does this logic only linear arithmetic? */
  bool isLinear() const;

  /** Does this logic only permit difference reasoning? (implies linear) */
  bool isDifferenceLogic() const;

  /** Does this logic allow cardinality constraints? */
  bool hasCardinalityConstraints() const;

  /** Is this a higher order logic? */
  bool isHigherOrder() const;

  // MUTATORS

  /**
   * Initialize the LogicInfo with an SMT-LIB-like logic string.
   * Throws an IllegalArgumentException if the string can't be
   * interpreted.
   */
  void setLogicString(std::string logicString);

  /**
   * Enable all functionality.  All theories, plus quantifiers, will be
   * enabled.
   *
   * @param enableHigherOrder Whether HOL should be enable together with the
   * above.
   */
  void enableEverything(bool enableHigherOrder = false);

  /**
   * Disable all functionality.  The result will be a LogicInfo with
   * the BUILTIN and BOOLEAN theories enabled only ("QF_SAT").
   */
  void disableEverything();

  /**
   * Enable the given theory module.
   */
  void enableTheory(theory::TheoryId theory);

  /**
   * Disable the given theory module.  THEORY_BUILTIN and THEORY_BOOL cannot
   * be disabled (and if given here, the request will be silently ignored).
   */
  void disableTheory(theory::TheoryId theory);

  /**
   * Quantifiers are a special case, since two theory modules handle them.
   */
  void enableQuantifiers() {
    enableTheory(theory::THEORY_QUANTIFIERS);
  }

  /**
   * Quantifiers are a special case, since two theory modules handle them.
   */
  void disableQuantifiers() {
    disableTheory(theory::THEORY_QUANTIFIERS);
  }

  /**
   * Enable everything that is needed for sygus with respect to this logic info.
   * This means enabling quantifiers, datatypes, UF, integers, and higher order.
   */
  void enableSygus();
  /**
   * Enable everything that is needed for separation logic. This means enabling
   * the theories of separation logic, UF and sets.
   */
  void enableSeparationLogic();

  // these are for arithmetic

  /** Enable the use of integers in this logic. */
  void enableIntegers();
  /** Disable the use of integers in this logic. */
  void disableIntegers();
  /** Enable the use of reals in this logic. */
  void enableReals();
  /** Disable the use of reals in this logic. */
  void disableReals();
  /** Enable the use of transcendentals in this logic. */
  void arithTranscendentals();
  /** Only permit difference arithmetic in this logic. */
  void arithOnlyDifference();
  /** Only permit linear arithmetic in this logic. */
  void arithOnlyLinear();
  /** Permit nonlinear arithmetic in this logic. */
  void arithNonLinear();

  // for cardinality constraints

  /** Enable the use of cardinality constraints in this logic. */
  void enableCardinalityConstraints();
  /** Disable the use of cardinality constraints in this logic. */
  void disableCardinalityConstraints();

  // for higher-order

  /** Enable the use of higher-order in this logic. */
  void enableHigherOrder();
  /** Disable the use of higher-order in this logic. */
  void disableHigherOrder();

  // LOCKING FUNCTIONALITY

  /** Lock this LogicInfo, disabling further mutation and allowing queries */
  void lock() { d_locked = true; }
  /** Check whether this LogicInfo is locked, disallowing further mutation */
  bool isLocked() const { return d_locked; }
  /** Get a copy of this LogicInfo that is identical, but unlocked */
  LogicInfo getUnlockedCopy() const;

  // COMPARISON

  /** Are these two LogicInfos equal? */
  bool operator==(const LogicInfo& other) const;

  /** Are these two LogicInfos disequal? */
  bool operator!=(const LogicInfo& other) const {
    return !(*this == other);
  }

  /** Is this LogicInfo "greater than" (does it contain everything and more) the other? */
  bool operator>(const LogicInfo& other) const {
    return *this >= other && *this != other;
  }

  /** Is this LogicInfo "less than" (does it contain strictly less) the other? */
  bool operator<(const LogicInfo& other) const {
    return *this <= other && *this != other;
  }
  /** Is this LogicInfo "less than or equal" the other? */
  bool operator<=(const LogicInfo& other) const;

  /** Is this LogicInfo "greater than or equal" the other? */
  bool operator>=(const LogicInfo& other) const;

  /** Are two LogicInfos comparable?  That is, is one of <= or > true? */
  bool isComparableTo(const LogicInfo& other) const {
    return *this <= other || *this >= other;
  }

}; /* class LogicInfo */

std::ostream& operator<<(std::ostream& out, const LogicInfo& logic);

}  // namespace cvc5

#endif /* CVC5__LOGIC_INFO_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Morgan Deters, Andrew Reynolds, Tim King
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		* A class giving information about a logic (group of theory modules and
14		* configuration information).
15		*/
16
17		#include "cvc5_public.h"
18
19		#ifndef CVC5__LOGIC_INFO_H
20		#define CVC5__LOGIC_INFO_H
21
22		#include <string>
23		#include <vector>
24
25		#include "cvc5_export.h"
26		#include "theory/theory_id.h"
27
28		namespace cvc5 {
29
30		/**
31		* A LogicInfo instance describes a collection of theory modules and some
32		* basic configuration about them. Conceptually, it provides a background
33		* context for all operations in cvc5. Typically, when cvc5's SmtEngine
34		* is created, it is issued a setLogic() command indicating features of the
35		* assertions and queries to follow---for example, whether quantifiers are
36		* used, whether integers or reals (or both) will be used, etc.
37		*
38		* Most places in cvc5 will only ever need to access a const reference to an
39		* instance of this class. Such an instance is generally set by the SmtEngine
40		* when setLogic() is called. However, mutating member functions are also
41		* provided by this class so that it can be used as a more general mechanism
42		* (e.g., for communicating to the SmtEngine which theories should be used,
43		* rather than having to provide an SMT-LIB string).
44		*/
45	234860	class CVC5_EXPORT LogicInfo
46		{
47		mutable std::string d_logicString; /*< an SMT-LIB-like logic string /
48		std::vector<bool> d_theories; /*< set of active theories /
49		size_t d_sharingTheories; /*< count of theories that need sharing /
50
51		/** are integers used in this logic? */
52		bool d_integers;
53		/** are reals used in this logic? */
54		bool d_reals;
55		/** transcendentals in this logic? */
56		bool d_transcendentals;
57		/** linear-only arithmetic in this logic? */
58		bool d_linear;
59		/** difference-only arithmetic in this logic? */
60		bool d_differenceLogic;
61		/** cardinality constraints in this logic? */
62		bool d_cardinalityConstraints;
63		/** higher-order constraints in this logic? */
64		bool d_higherOrder;
65
66		bool d_locked; /*< is this LogicInfo instance locked (and thus immutable)? /
67
68		/**
69		* Returns true iff this is a "true" theory (one that must be worried
70		* about for sharing
71		*/
72	1444325	static inline bool isTrueTheory(theory::TheoryId theory) {
73	1444325	switch(theory) {
74	364474	case theory::THEORY_BUILTIN:
75		case theory::THEORY_BOOL:
76		case theory::THEORY_QUANTIFIERS:
77	364474	return false;
78	1079851	default:
79	1079851	return true;
80		}
81		}
82
83		public:
84
85		/**
86		* Constructs a LogicInfo for the most general logic (quantifiers, all
87		* background theory modules, ...).
88		*/
89		LogicInfo();
90
91		/**
92		* Construct a LogicInfo from an SMT-LIB-like logic string.
93		* Throws an IllegalArgumentException if the logic string cannot
94		* be interpreted.
95		*/
96		LogicInfo(std::string logicString);
97
98		/**
99		* Construct a LogicInfo from an SMT-LIB-like logic string.
100		* Throws an IllegalArgumentException if the logic string cannot
101		* be interpreted.
102		*/
103		LogicInfo(const char* logicString);
104
105		// ACCESSORS
106
107		/**
108		* Get an SMT-LIB-like logic string. These are only guaranteed to
109		* be SMT-LIB-compliant if an SMT-LIB-compliant string was used in
110		* the constructor and no mutating functions were called.
111		*/
112		std::string getLogicString() const;
113
114		/** Is sharing enabled for this logic? */
115		bool isSharingEnabled() const;
116
117		/** Is the given theory module active in this logic? */
118		bool isTheoryEnabled(theory::TheoryId theory) const;
119
120		/** Is this a quantified logic? */
121		bool isQuantified() const;
122
123		/** Is this a logic that includes the all-inclusive logic?
124		*
125		* @return Yields true if the logic corresponds to "ALL" or its super
126		* set including , such as "HO_ALL".
127		*/
128		bool hasEverything() const;
129
130		/** Is this the all-exclusive logic? (Here, that means propositional logic) */
131		bool hasNothing() const;
132
133		/**
134		* Is this a pure logic (only one "true" background theory). Quantifiers
135		* can exist in such logics though; to test for quantifier-free purity,
136		* use "isPure(theory) && !isQuantified()".
137		*/
138		bool isPure(theory::TheoryId theory) const;
139
140		// these are for arithmetic
141
142		/** Are integers in this logic? */
143		bool areIntegersUsed() const;
144
145		/** Are reals in this logic? */
146		bool areRealsUsed() const;
147
148		/** Are transcendentals in this logic? */
149		bool areTranscendentalsUsed() const;
150
151		/** Does this logic only linear arithmetic? */
152		bool isLinear() const;
153
154		/** Does this logic only permit difference reasoning? (implies linear) */
155		bool isDifferenceLogic() const;
156
157		/** Does this logic allow cardinality constraints? */
158		bool hasCardinalityConstraints() const;
159
160		/** Is this a higher order logic? */
161		bool isHigherOrder() const;
162
163		// MUTATORS
164
165		/**
166		* Initialize the LogicInfo with an SMT-LIB-like logic string.
167		* Throws an IllegalArgumentException if the string can't be
168		* interpreted.
169		*/
170		void setLogicString(std::string logicString);
171
172		/**
173		* Enable all functionality. All theories, plus quantifiers, will be
174		* enabled.
175		*
176		* @param enableHigherOrder Whether HOL should be enable together with the
177		* above.
178		*/
179		void enableEverything(bool enableHigherOrder = false);
180
181		/**
182		* Disable all functionality. The result will be a LogicInfo with
183		* the BUILTIN and BOOLEAN theories enabled only ("QF_SAT").
184		*/
185		void disableEverything();
186
187		/**
188		* Enable the given theory module.
189		*/
190		void enableTheory(theory::TheoryId theory);
191
192		/**
193		* Disable the given theory module. THEORY_BUILTIN and THEORY_BOOL cannot
194		* be disabled (and if given here, the request will be silently ignored).
195		*/
196		void disableTheory(theory::TheoryId theory);
197
198		/**
199		* Quantifiers are a special case, since two theory modules handle them.
200		*/
201	7034	void enableQuantifiers() {
202	7034	enableTheory(theory::THEORY_QUANTIFIERS);
203	7034	}
204
205		/**
206		* Quantifiers are a special case, since two theory modules handle them.
207		*/
208	20861	void disableQuantifiers() {
209	20861	disableTheory(theory::THEORY_QUANTIFIERS);
210	20859	}
211
212		/**
213		* Enable everything that is needed for sygus with respect to this logic info.
214		* This means enabling quantifiers, datatypes, UF, integers, and higher order.
215		*/
216		void enableSygus();
217		/**
218		* Enable everything that is needed for separation logic. This means enabling
219		* the theories of separation logic, UF and sets.
220		*/
221		void enableSeparationLogic();
222
223		// these are for arithmetic
224
225		/** Enable the use of integers in this logic. */
226		void enableIntegers();
227		/** Disable the use of integers in this logic. */
228		void disableIntegers();
229		/** Enable the use of reals in this logic. */
230		void enableReals();
231		/** Disable the use of reals in this logic. */
232		void disableReals();
233		/** Enable the use of transcendentals in this logic. */
234		void arithTranscendentals();
235		/** Only permit difference arithmetic in this logic. */
236		void arithOnlyDifference();
237		/** Only permit linear arithmetic in this logic. */
238		void arithOnlyLinear();
239		/** Permit nonlinear arithmetic in this logic. */
240		void arithNonLinear();
241
242		// for cardinality constraints
243
244		/** Enable the use of cardinality constraints in this logic. */
245		void enableCardinalityConstraints();
246		/** Disable the use of cardinality constraints in this logic. */
247		void disableCardinalityConstraints();
248
249		// for higher-order
250
251		/** Enable the use of higher-order in this logic. */
252		void enableHigherOrder();
253		/** Disable the use of higher-order in this logic. */
254		void disableHigherOrder();
255
256		// LOCKING FUNCTIONALITY
257
258		/** Lock this LogicInfo, disabling further mutation and allowing queries */
259	86332	void lock() { d_locked = true; }
260		/** Check whether this LogicInfo is locked, disallowing further mutation */
261	149071	bool isLocked() const { return d_locked; }
262		/** Get a copy of this LogicInfo that is identical, but unlocked */
263		LogicInfo getUnlockedCopy() const;
264
265		// COMPARISON
266
267		/** Are these two LogicInfos equal? */
268		bool operator==(const LogicInfo& other) const;
269
270		/** Are these two LogicInfos disequal? */
271	3416	bool operator!=(const LogicInfo& other) const {
272	3416	return !(*this == other);
273		}
274
275		/** Is this LogicInfo "greater than" (does it contain everything and more) the other? */
276	2348	bool operator>(const LogicInfo& other) const {
277	2348	return this >= other && this != other;
278		}
279
280		/** Is this LogicInfo "less than" (does it contain strictly less) the other? */
281	2348	bool operator<(const LogicInfo& other) const {
282	2348	return this <= other && this != other;
283		}
284		/** Is this LogicInfo "less than or equal" the other? */
285		bool operator<=(const LogicInfo& other) const;
286
287		/** Is this LogicInfo "greater than or equal" the other? */
288		bool operator>=(const LogicInfo& other) const;
289
290		/** Are two LogicInfos comparable? That is, is one of <= or > true? */
291	2348	bool isComparableTo(const LogicInfo& other) const {
292	2348	return this <= other \|\| this >= other;
293		}
294
295		}; /* class LogicInfo */
296
297		std::ostream& operator<<(std::ostream& out, const LogicInfo& logic);
298
299		} // namespace cvc5
300
301		#endif /* CVC5__LOGIC_INFO_H */