Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/theory_model_builder.h	Lines:	4	4	100.0 %
Date:	2021-05-24	Branches:	0	0	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner, 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.
 * ****************************************************************************
 *
 * Model class.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__THEORY_MODEL_BUILDER_H
#define CVC5__THEORY__THEORY_MODEL_BUILDER_H

#include <unordered_map>
#include <unordered_set>

#include "theory/theory_model.h"

namespace cvc5 {

class TheoryEngine;

namespace theory {

/** TheoryEngineModelBuilder class
 *
 * This is the class used by TheoryEngine
 * for constructing TheoryModel objects, which is the class
 * that represents models for a set of assertions.
 *
 * A call to TheoryEngineModelBuilder::buildModel(...) is made
 * after a full effort check passes with no theory solvers
 * adding lemmas or conflicts, and theory combination passes
 * with no splits on shared terms. If buildModel is successful,
 * this will set up the data structures in TheoryModel to represent
 * a model for the current set of assertions.
 */
class TheoryEngineModelBuilder
{
  typedef std::unordered_map<Node, Node> NodeMap;
  typedef std::unordered_set<Node> NodeSet;

 public:
  TheoryEngineModelBuilder();
  virtual ~TheoryEngineModelBuilder() {}
  /**
   * Should be called only on models m after they have been prepared
   * (e.g. using ModelManager). In other words, the equality engine of model
   * m contains all relevant information from each theory that is needed
   * for building a model. This class is responsible simply for ensuring
   * that all equivalence classes of the equality engine of m are assigned
   * constants.
   *
   * This constructs the model m, via the following steps:
   * (1) builder-specified pre-processing,
   * (2) find the equivalence classes of m's
   *     equality engine that initially contain constants,
   * (3) assign constants to all equivalence classes
   *     of m's equality engine, through alternating
   *     iterations of evaluation and enumeration,
   * (4) builder-specific processing, which includes assigning total
   *     interpretations to uninterpreted functions.
   *
   * This function returns false if any of the above
   * steps results in a lemma sent on an output channel.
   * Lemmas may be sent on an output channel by this
   * builder in steps (2) or (5), for instance, if the model we
   * are building fails to satisfy a quantified formula.
   *
   * @param m The model to build
   * @return true if the model was successfully built.
   */
  bool buildModel(TheoryModel* m);

  /** postprocess model
   *
   * This is called when m is a model that will be returned to the user. This
   * method checks the internal consistency of the model if we are in a debug
   * build.
   */
  void postProcessModel(bool incomplete, TheoryModel* m);

 protected:

  //-----------------------------------virtual functions
  /** pre-process build model
   * Do pre-processing specific to this model builder.
   * Called in step (2) of the build construction,
   * described above.
   */
  virtual bool preProcessBuildModel(TheoryModel* m);
  /** process build model
   * Do processing specific to this model builder.
   * Called in step (5) of the build construction,
   * described above.
   * By default, this assigns values to each function
   * that appears in m's equality engine.
   */
  virtual bool processBuildModel(TheoryModel* m);
  /** debug the model
   * Check assertions and printing debug information for the model.
   * Calls after step (5) described above is complete.
   */
  virtual void debugModel(TheoryModel* m) {}
  //-----------------------------------end virtual functions

  /** Debug check model.
   *
   * This throws an assertion failure if the model contains an equivalence
   * class with two terms t1 and t2 such that t1^M != t2^M.
   */
  void debugCheckModel(TheoryModel* m);

  /** Evaluate equivalence class
   *
   * If this method returns a non-null node c, then c is a constant and some
   * term in the equivalence class of r evaluates to c based on the current
   * state of the model m.
   */
  Node evaluateEqc(TheoryModel* m, TNode r);
  /** is n an assignable expression?
   *
   * A term n is an assignable expression if its value is unconstrained by a
   * standard model. Examples of assignable terms are:
   * - variables,
   * - applications of array select,
   * - applications of datatype selectors,
   * - applications of uninterpreted functions.
   * Assignable terms must be first-order, that is, all instances of the above
   * terms are not assignable if they have a higher-order (function) type.
   */
  bool isAssignable(TNode n);
  /** add assignable subterms
   * Adds all assignable subterms of n to tm's equality engine.
   */
  void addAssignableSubterms(TNode n, TheoryModel* tm, NodeSet& cache);
  /** normalize representative r
   *
   * This returns a term that is equivalent to r's
   * interpretation in the model m. It may do so
   * by rewriting the application of r's operator to the
   * result of normalizing each of r's children, if
   * each child is constant.
   */
  Node normalize(TheoryModel* m, TNode r, bool evalOnly);
  /** assign constant representative
   *
   * Called when equivalence class eqc is assigned a constant
   * representative const_rep.
   *
   * eqc should be a representative of tm's equality engine.
   */
  void assignConstantRep(TheoryModel* tm, Node eqc, Node const_rep);
  /** add to type list
   *
   * This adds to type_list the list of types that tn is built from.
   * For example, if tn is (Array Int Bool) and type_list is empty,
   * then we append ( Int, Bool, (Array Int Bool) ) to type_list.
   */
  void addToTypeList(TypeNode tn,
                     std::vector<TypeNode>& type_list,
                     std::unordered_set<TypeNode>& visiting);
  /** assign function f based on the model m.
  * This construction is based on "table form". For example:
  * (f 0 1) = 1
  * (f 0 2) = 2
  * (f 1 1) = 3
  * ...
  * becomes:
  * f = (lambda xy. (ite (and (= x 0) (= y 1)) 1
  *                 (ite (and (= x 0) (= y 2)) 2
  *                 (ite (and (= x 1) (= y 1)) 3 ...)))
  */
  void assignFunction(TheoryModel* m, Node f);
  /** assign function f based on the model m.
  * This construction is based on "dag form". For example:
  * (f 0 1) = 1
  * (f 0 2) = 2
  * (f 1 1) = 3
  * ...
  * becomes:
  * f = (lambda xy. (ite (= x 0) (ite (= y 1) 1
  *                              (ite (= y 2) 2 ...))
  *                 (ite (= x 1) (ite (= y 1) 3 ...)
  *                              ...))
  *
  * where the above is represented as a directed acyclic graph (dag).
  * This construction is accomplished by assigning values to (f c)
  * terms before f, e.g.
  * (f 0) = (lambda y. (ite (= y 1) 1
  *                    (ite (= y 2) 2 ...))
  * (f 1) = (lambda y. (ite (= y 1) 3 ...))
  * where
  * f = (lambda xy. (ite (= x 0) ((f 0) y)
  *                 (ite (= x 1) ((f 1) y) ...))
  */
  void assignHoFunction(TheoryModel* m, Node f);
  /** assign functions
   *
   * Assign all unassigned functions in the model m (those returned by
   * TheoryModel::getFunctionsToAssign),
   * using the two functions above. Currently:
   * If ufHo is disabled, we call assignFunction for all functions.
   * If ufHo is enabled, we call assignHoFunction.
   */
  void assignFunctions(TheoryModel* m);

 private:
  /** normalized cache
   * A temporary cache mapping terms to their
   * normalized form, used during buildModel.
   */
  NodeMap d_normalizedCache;
  /** mapping from terms to the constant associated with their equivalence class
   */
  std::map<Node, Node> d_constantReps;

  /** Theory engine model builder assigner class
   *
   * This manages the assignment of values to terms of a given type.
   * In particular, it is a wrapper around a type enumerator that is restricted
   * by a set of values that it cannot generate, called an "assignment exclusion
   * set".
   */
  class Assigner
  {
   public:
    Assigner() : d_te(nullptr), d_isActive(false) {}
    /**
     * Initialize this assigner to generate values of type tn, with properties
     * tep and assignment exclusion set aes.
     */
    void initialize(TypeNode tn,
                    TypeEnumeratorProperties* tep,
                    const std::vector<Node>& aes);
    /** get the next term in the enumeration
     *
     * This method returns the next legal term based on type enumeration, where
     * a term is legal it does not belong to the assignment exclusion set of
     * this assigner. If no more terms exist, this method returns null. This
     * should never be the case due to the conditions ensured by theory solvers
     * for finite types. If it is the case, we give an assertion failure.
     */
    Node getNextAssignment();
    /** The type enumerator */
    std::unique_ptr<TypeEnumerator> d_te;
    /** The assignment exclusion set of this Assigner */
    std::vector<Node> d_assignExcSet;
    /**
     * Is active, flag set to true when all values in d_assignExcSet are
     * constant.
     */
    bool d_isActive;
  };
  /** Is the given Assigner ready to assign values?
   *
   * This returns true if all values in the assignment exclusion set of a have
   * a known value according to the state of this model builder (via a lookup
   * in d_constantReps). It updates the assignment exclusion vector of a to
   * these values whenever possible.
   */
  bool isAssignerActive(TheoryModel* tm, Assigner& a);
  //------------------------------------for codatatypes
  /** is v an excluded codatatype value?
   *
   * If this returns true, then v is a value
   * that cannot be used during enumeration in step (4)
   * of model construction.
   *
   * repSet is the set of representatives of the same type as v,
   * assertedReps is a map from representatives t,
   * eqc is the equivalence class that v reside.
   *
   * This function is used to avoid alpha-equivalent
   * assignments for codatatype terms, described in
   * Reynolds/Blanchette CADE 2015. In particular,
   * this function returns true if v is in
   * the set V^{x}_I from page 9, where x is eqc
   * and I is the model we are building.
   */
  bool isExcludedCdtValue(Node v,
                          std::set<Node>* repSet,
                          std::map<Node, Node>& assertedReps,
                          Node eqc);
  /** is codatatype value match
   *
   * This returns true if v is r{ eqc -> t } for some t.
   * If this function returns true, then t above is
   * stored in eqc_m.
   */
  bool isCdtValueMatch(Node v, Node r, Node eqc, Node& eqc_m);
  //------------------------------------end for codatatypes

  /**
   * Is the given type constrained to be finite? This depends on whether
   * finite model finding is enabled.
   */
  bool isFiniteType(TypeNode tn) const;
  //---------------------------------for debugging finite model finding
  /** does type tn involve an uninterpreted sort? */
  bool involvesUSort(TypeNode tn) const;
  /** is v an excluded value based on uninterpreted sorts?
   * This gives an assertion failure in the case that v contains
   * an uninterpreted constant whose index is out of the bounds
   * specified by eqc_usort_count.
   */
  bool isExcludedUSortValue(std::map<TypeNode, unsigned>& eqc_usort_count,
                            Node v,
                            std::map<Node, bool>& visited);
  //---------------------------------end for debugging finite model finding

}; /* class TheoryEngineModelBuilder */

}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY__THEORY_MODEL_BUILDER_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Mathias Preiner, 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		* Model class.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__THEORY_MODEL_BUILDER_H
19		#define CVC5__THEORY__THEORY_MODEL_BUILDER_H
20
21		#include <unordered_map>
22		#include <unordered_set>
23
24		#include "theory/theory_model.h"
25
26		namespace cvc5 {
27
28		class TheoryEngine;
29
30		namespace theory {
31
32		/** TheoryEngineModelBuilder class
33		*
34		* This is the class used by TheoryEngine
35		* for constructing TheoryModel objects, which is the class
36		* that represents models for a set of assertions.
37		*
38		* A call to TheoryEngineModelBuilder::buildModel(...) is made
39		* after a full effort check passes with no theory solvers
40		* adding lemmas or conflicts, and theory combination passes
41		* with no splits on shared terms. If buildModel is successful,
42		* this will set up the data structures in TheoryModel to represent
43		* a model for the current set of assertions.
44		*/
45		class TheoryEngineModelBuilder
46		{
47		typedef std::unordered_map<Node, Node> NodeMap;
48		typedef std::unordered_set<Node> NodeSet;
49
50		public:
51		TheoryEngineModelBuilder();
52	15551	virtual ~TheoryEngineModelBuilder() {}
53		/**
54		* Should be called only on models m after they have been prepared
55		* (e.g. using ModelManager). In other words, the equality engine of model
56		* m contains all relevant information from each theory that is needed
57		* for building a model. This class is responsible simply for ensuring
58		* that all equivalence classes of the equality engine of m are assigned
59		* constants.
60		*
61		* This constructs the model m, via the following steps:
62		* (1) builder-specified pre-processing,
63		* (2) find the equivalence classes of m's
64		* equality engine that initially contain constants,
65		* (3) assign constants to all equivalence classes
66		* of m's equality engine, through alternating
67		* iterations of evaluation and enumeration,
68		* (4) builder-specific processing, which includes assigning total
69		* interpretations to uninterpreted functions.
70		*
71		* This function returns false if any of the above
72		* steps results in a lemma sent on an output channel.
73		* Lemmas may be sent on an output channel by this
74		* builder in steps (2) or (5), for instance, if the model we
75		* are building fails to satisfy a quantified formula.
76		*
77		* @param m The model to build
78		* @return true if the model was successfully built.
79		*/
80		bool buildModel(TheoryModel* m);
81
82		/** postprocess model
83		*
84		* This is called when m is a model that will be returned to the user. This
85		* method checks the internal consistency of the model if we are in a debug
86		* build.
87		*/
88		void postProcessModel(bool incomplete, TheoryModel* m);
89
90		protected:
91
92		//-----------------------------------virtual functions
93		/** pre-process build model
94		* Do pre-processing specific to this model builder.
95		* Called in step (2) of the build construction,
96		* described above.
97		*/
98		virtual bool preProcessBuildModel(TheoryModel* m);
99		/** process build model
100		* Do processing specific to this model builder.
101		* Called in step (5) of the build construction,
102		* described above.
103		* By default, this assigns values to each function
104		* that appears in m's equality engine.
105		*/
106		virtual bool processBuildModel(TheoryModel* m);
107		/** debug the model
108		* Check assertions and printing debug information for the model.
109		* Calls after step (5) described above is complete.
110		*/
111	39	virtual void debugModel(TheoryModel* m) {}
112		//-----------------------------------end virtual functions
113
114		/** Debug check model.
115		*
116		* This throws an assertion failure if the model contains an equivalence
117		* class with two terms t1 and t2 such that t1^M != t2^M.
118		*/
119		void debugCheckModel(TheoryModel* m);
120
121		/** Evaluate equivalence class
122		*
123		* If this method returns a non-null node c, then c is a constant and some
124		* term in the equivalence class of r evaluates to c based on the current
125		* state of the model m.
126		*/
127		Node evaluateEqc(TheoryModel* m, TNode r);
128		/** is n an assignable expression?
129		*
130		* A term n is an assignable expression if its value is unconstrained by a
131		* standard model. Examples of assignable terms are:
132		* - variables,
133		* - applications of array select,
134		* - applications of datatype selectors,
135		* - applications of uninterpreted functions.
136		* Assignable terms must be first-order, that is, all instances of the above
137		* terms are not assignable if they have a higher-order (function) type.
138		*/
139		bool isAssignable(TNode n);
140		/** add assignable subterms
141		* Adds all assignable subterms of n to tm's equality engine.
142		*/
143		void addAssignableSubterms(TNode n, TheoryModel* tm, NodeSet& cache);
144		/** normalize representative r
145		*
146		* This returns a term that is equivalent to r's
147		* interpretation in the model m. It may do so
148		* by rewriting the application of r's operator to the
149		* result of normalizing each of r's children, if
150		* each child is constant.
151		*/
152		Node normalize(TheoryModel* m, TNode r, bool evalOnly);
153		/** assign constant representative
154		*
155		* Called when equivalence class eqc is assigned a constant
156		* representative const_rep.
157		*
158		* eqc should be a representative of tm's equality engine.
159		*/
160		void assignConstantRep(TheoryModel* tm, Node eqc, Node const_rep);
161		/** add to type list
162		*
163		* This adds to type_list the list of types that tn is built from.
164		* For example, if tn is (Array Int Bool) and type_list is empty,
165		* then we append ( Int, Bool, (Array Int Bool) ) to type_list.
166		*/
167		void addToTypeList(TypeNode tn,
168		std::vector<TypeNode>& type_list,
169		std::unordered_set<TypeNode>& visiting);
170		/** assign function f based on the model m.
171		* This construction is based on "table form". For example:
172		* (f 0 1) = 1
173		* (f 0 2) = 2
174		* (f 1 1) = 3
175		* ...
176		* becomes:
177		* f = (lambda xy. (ite (and (= x 0) (= y 1)) 1
178		* (ite (and (= x 0) (= y 2)) 2
179		* (ite (and (= x 1) (= y 1)) 3 ...)))
180		*/
181		void assignFunction(TheoryModel* m, Node f);
182		/** assign function f based on the model m.
183		* This construction is based on "dag form". For example:
184		* (f 0 1) = 1
185		* (f 0 2) = 2
186		* (f 1 1) = 3
187		* ...
188		* becomes:
189		* f = (lambda xy. (ite (= x 0) (ite (= y 1) 1
190		* (ite (= y 2) 2 ...))
191		* (ite (= x 1) (ite (= y 1) 3 ...)
192		* ...))
193		*
194		* where the above is represented as a directed acyclic graph (dag).
195		* This construction is accomplished by assigning values to (f c)
196		* terms before f, e.g.
197		* (f 0) = (lambda y. (ite (= y 1) 1
198		* (ite (= y 2) 2 ...))
199		* (f 1) = (lambda y. (ite (= y 1) 3 ...))
200		* where
201		* f = (lambda xy. (ite (= x 0) ((f 0) y)
202		* (ite (= x 1) ((f 1) y) ...))
203		*/
204		void assignHoFunction(TheoryModel* m, Node f);
205		/** assign functions
206		*
207		* Assign all unassigned functions in the model m (those returned by
208		* TheoryModel::getFunctionsToAssign),
209		* using the two functions above. Currently:
210		* If ufHo is disabled, we call assignFunction for all functions.
211		* If ufHo is enabled, we call assignHoFunction.
212		*/
213		void assignFunctions(TheoryModel* m);
214
215		private:
216		/** normalized cache
217		* A temporary cache mapping terms to their
218		* normalized form, used during buildModel.
219		*/
220		NodeMap d_normalizedCache;
221		/** mapping from terms to the constant associated with their equivalence class
222		*/
223		std::map<Node, Node> d_constantReps;
224
225		/** Theory engine model builder assigner class
226		*
227		* This manages the assignment of values to terms of a given type.
228		* In particular, it is a wrapper around a type enumerator that is restricted
229		* by a set of values that it cannot generate, called an "assignment exclusion
230		* set".
231		*/
232	8	class Assigner
233		{
234		public:
235	8	Assigner() : d_te(nullptr), d_isActive(false) {}
236		/**
237		* Initialize this assigner to generate values of type tn, with properties
238		* tep and assignment exclusion set aes.
239		*/
240		void initialize(TypeNode tn,
241		TypeEnumeratorProperties* tep,
242		const std::vector<Node>& aes);
243		/** get the next term in the enumeration
244		*
245		* This method returns the next legal term based on type enumeration, where
246		* a term is legal it does not belong to the assignment exclusion set of
247		* this assigner. If no more terms exist, this method returns null. This
248		* should never be the case due to the conditions ensured by theory solvers
249		* for finite types. If it is the case, we give an assertion failure.
250		*/
251		Node getNextAssignment();
252		/** The type enumerator */
253		std::unique_ptr<TypeEnumerator> d_te;
254		/** The assignment exclusion set of this Assigner */
255		std::vector<Node> d_assignExcSet;
256		/**
257		* Is active, flag set to true when all values in d_assignExcSet are
258		* constant.
259		*/
260		bool d_isActive;
261		};
262		/** Is the given Assigner ready to assign values?
263		*
264		* This returns true if all values in the assignment exclusion set of a have
265		* a known value according to the state of this model builder (via a lookup
266		* in d_constantReps). It updates the assignment exclusion vector of a to
267		* these values whenever possible.
268		*/
269		bool isAssignerActive(TheoryModel* tm, Assigner& a);
270		//------------------------------------for codatatypes
271		/** is v an excluded codatatype value?
272		*
273		* If this returns true, then v is a value
274		* that cannot be used during enumeration in step (4)
275		* of model construction.
276		*
277		* repSet is the set of representatives of the same type as v,
278		* assertedReps is a map from representatives t,
279		* eqc is the equivalence class that v reside.
280		*
281		* This function is used to avoid alpha-equivalent
282		* assignments for codatatype terms, described in
283		* Reynolds/Blanchette CADE 2015. In particular,
284		* this function returns true if v is in
285		* the set V^{x}_I from page 9, where x is eqc
286		* and I is the model we are building.
287		*/
288		bool isExcludedCdtValue(Node v,
289		std::set<Node>* repSet,
290		std::map<Node, Node>& assertedReps,
291		Node eqc);
292		/** is codatatype value match
293		*
294		* This returns true if v is r{ eqc -> t } for some t.
295		* If this function returns true, then t above is
296		* stored in eqc_m.
297		*/
298		bool isCdtValueMatch(Node v, Node r, Node eqc, Node& eqc_m);
299		//------------------------------------end for codatatypes
300
301		/**
302		* Is the given type constrained to be finite? This depends on whether
303		* finite model finding is enabled.
304		*/
305		bool isFiniteType(TypeNode tn) const;
306		//---------------------------------for debugging finite model finding
307		/** does type tn involve an uninterpreted sort? */
308		bool involvesUSort(TypeNode tn) const;
309		/** is v an excluded value based on uninterpreted sorts?
310		* This gives an assertion failure in the case that v contains
311		* an uninterpreted constant whose index is out of the bounds
312		* specified by eqc_usort_count.
313		*/
314		bool isExcludedUSortValue(std::map<TypeNode, unsigned>& eqc_usort_count,
315		Node v,
316		std::map<Node, bool>& visited);
317		//---------------------------------end for debugging finite model finding
318
319		}; /* class TheoryEngineModelBuilder */
320
321		} // namespace theory
322		} // namespace cvc5
323
324		#endif /* CVC5__THEORY__THEORY_MODEL_BUILDER_H */