Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/first_order_model.h	Lines:	4	6	66.7 %
Date:	2021-09-29	Branches:	9	22	40.9 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Paul Meng, Morgan Deters
 *
 * 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 extended classes.
 */

#include "cvc5_private.h"

#ifndef CVC5__FIRST_ORDER_MODEL_H
#define CVC5__FIRST_ORDER_MODEL_H

#include "context/cdlist.h"
#include "smt/env_obj.h"
#include "theory/quantifiers/equality_query.h"
#include "theory/theory_model.h"
#include "theory/uf/theory_uf_model.h"

namespace cvc5 {
namespace theory {

class TheoryModel;
class RepSet;

namespace quantifiers {

class QuantifiersState;
class TermRegistry;
class QuantifiersRegistry;

// TODO (#1301) : document and refactor this class
class FirstOrderModel : protected EnvObj
{
 public:
  FirstOrderModel(Env& env,
                  QuantifiersState& qs,
                  QuantifiersRegistry& qr,
                  TermRegistry& tr);
  virtual ~FirstOrderModel() {}

  /** finish init */
  void finishInit(TheoryModel* m);
  //---------------------------------- access functions for underlying model
  /** Get value in the underlying theory model */
  Node getValue(TNode n) const;
  /** does the equality engine of this model have term a? */
  bool hasTerm(TNode a);
  /** get the representative of a in the equality engine of this model */
  Node getRepresentative(TNode a);
  /** are a and b equal in the equality engine of this model? */
  bool areEqual(TNode a, TNode b);
  /** are a and b disequal in the equality engine of this model? */
  bool areDisequal(TNode a, TNode b);
  /** get the equality engine for this model */
  eq::EqualityEngine* getEqualityEngine();
  /** get the representative set object */
  const RepSet* getRepSet() const;
  /** get the representative set object */
  RepSet* getRepSetPtr();
  /** get the entire theory model */
  TheoryModel* getTheoryModel();
  //---------------------------------- end access functions for underlying model
  /** get internal representative
   *
   * Choose a term that is equivalent to a in the current context that is the
   * best term for instantiating the index^th variable of quantified formula q.
   * If no legal term can be found, we return null. This can occur if:
   * - a's type is not a subtype of the type of the index^th variable of q,
   * - a is in an equivalent class with all terms that are restricted not to
   * appear in instantiations of q, e.g. INST_CONSTANT terms for counterexample
   * guided instantiation.
   */
  Node getInternalRepresentative(Node a, Node q, size_t index);

  /** assert quantifier */
  void assertQuantifier( Node n );
  /** get number of asserted quantifiers */
  size_t getNumAssertedQuantifiers() const;
  /** get asserted quantifier */
  Node getAssertedQuantifier( unsigned i, bool ordered = false );
  /** initialize model for term */
  void initializeModelForTerm( Node n, std::map< Node, bool >& visited );
  // initialize the model
  void initialize();
  /** get variable id */
  int getVariableId(TNode q, TNode n) {
    return d_quant_var_id.find( q )!=d_quant_var_id.end() ? d_quant_var_id[q][n] : -1;
  }
  /** do we need to do any work? */
  bool checkNeeded();
  /** reset round */
  void reset_round();
  /** mark quantified formula relevant */
  void markRelevant( Node q );
  /** set quantified formula active/inactive
   *
   * This indicates that quantified formula is "inactive", that is, it need
   * not be considered during this instantiation round.
   *
   * A quantified formula may be set inactive if for instance:
   *   - It is entailed by other quantified formulas, or
   *   - All of its instances are known to be true in the current model.
   *
   * This method should be called after a call to FirstOrderModel::reset_round,
   * and before calls to QuantifiersModule check calls. A common place to call
   * this method is during QuantifiersModule reset_round calls.
   */
  void setQuantifierActive( TNode q, bool active );
  /** is quantified formula active?
   *
   * Returns false if there has been a call to setQuantifierActive( q, false )
   * during this instantiation round.
   */
  bool isQuantifierActive(TNode q) const;
  /** is quantified formula asserted */
  bool isQuantifierAsserted(TNode q) const;
  /** get model basis term */
  Node getModelBasisTerm(TypeNode tn);
  /** is model basis term */
  bool isModelBasisTerm(Node n);
  /** get model basis term for op */
  Node getModelBasisOpTerm(Node op);
  /** get model basis */
  Node getModelBasis(Node q, Node n);
  /** get model basis arg */
  unsigned getModelBasisArg(Node n);
  /** get some domain element */
  Node getSomeDomainElement(TypeNode tn);
  /** initialize representative set for type
   *
   * This ensures that TheoryModel::d_rep_set
   * is initialized for type tn. In particular:
   * (1) If tn is an uninitialized (unconstrained)
   * uninterpreted sort, then we interpret it
   * as a set of size one,
   * (2) If tn is a "small" enumerable finite type,
   * then we ensure that all its values are in
   * TheoryModel::d_rep_set.
   *
   * Returns true if the initialization was complete,
   * in that the set for tn in TheoryModel::d_rep_set
   * has all representatives of type tn.
   */
  bool initializeRepresentativesForType(TypeNode tn);
  /**
   * Has the term been marked as a model basis term?
   */
  static bool isModelBasis(TNode n);
  /** Get the equality query */
  EqualityQuery* getEqualityQuery();

 protected:
  /** Pointer to the underyling theory model */
  TheoryModel* d_model;
  /** The quantifiers registry */
  QuantifiersRegistry& d_qreg;
  /** Reference to the term registry */
  TermRegistry& d_treg;
  /** equality query class */
  EqualityQuery d_eq_query;
  /** list of quantifiers asserted in the current context */
  context::CDList<Node> d_forall_asserts;
  /**
   * The (ordered) list of quantified formulas marked as relevant using
   * markRelevant, where the quantified formula q in the most recent
   * call to markRelevant comes last in the list.
   */
  std::vector<Node> d_forall_rlv_vec;
  /** The last quantified formula marked as relevant, if one exists. */
  Node d_last_forall_rlv;
  /**
   * The list of asserted quantified formulas, ordered by relevance.
   * Relevance is a dynamic partial ordering where q1 < q2 if there has been
   * a call to markRelevant( q1 ) after the last call to markRelevant( q2 )
   * (or no call to markRelevant( q2 ) has been made).
   *
   * This list is used primarily as an optimization for conflict-based
   * instantiation so that quantifed formulas that have been instantiated
   * most recently are processed first, since these are (statistically) more
   * likely to have conflicting instantiations.
   */
  std::vector<Node> d_forall_rlv_assert;
  /**
   * Whether the above list has been computed. This flag is updated during
   * reset_round and is valid within a full effort check.
   */
  bool d_forallRlvComputed;
  /** get variable id */
  std::map<Node, std::map<Node, int> > d_quant_var_id;
  /** process initialize model for term */
  virtual void processInitializeModelForTerm(Node n) {}
  /** process initialize quantifier */
  virtual void processInitializeQuantifier(Node q) {}
  /** process initialize */
  virtual void processInitialize(bool ispre) {}

 private:
  // list of inactive quantified formulas
  std::map<TNode, bool> d_quant_active;
  /** map from types to model basis terms */
  std::map<TypeNode, Node> d_model_basis_term;
  /** map from ops to model basis terms */
  std::map<Node, Node> d_model_basis_op_term;
  /** map from instantiation terms to their model basis equivalent */
  std::map<Node, Node> d_model_basis_body;
  /** map from universal quantifiers to model basis terms */
  std::map<Node, std::vector<Node> > d_model_basis_terms;
  /** compute model basis arg */
  void computeModelBasisArgAttribute(Node n);
};/* class FirstOrderModel */

}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__FIRST_ORDER_MODEL_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Paul Meng, Morgan Deters
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 extended classes.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__FIRST_ORDER_MODEL_H
19		#define CVC5__FIRST_ORDER_MODEL_H
20
21		#include "context/cdlist.h"
22		#include "smt/env_obj.h"
23		#include "theory/quantifiers/equality_query.h"
24		#include "theory/theory_model.h"
25		#include "theory/uf/theory_uf_model.h"
26
27		namespace cvc5 {
28		namespace theory {
29
30		class TheoryModel;
31		class RepSet;
32
33		namespace quantifiers {
34
35		class QuantifiersState;
36		class TermRegistry;
37		class QuantifiersRegistry;
38
39		// TODO (#1301) : document and refactor this class
40		class FirstOrderModel : protected EnvObj
41		{
42		public:
43		FirstOrderModel(Env& env,
44		QuantifiersState& qs,
45		QuantifiersRegistry& qr,
46		TermRegistry& tr);
47	11645	virtual ~FirstOrderModel() {}
48
49		/** finish init */
50		void finishInit(TheoryModel* m);
51		//---------------------------------- access functions for underlying model
52		/** Get value in the underlying theory model */
53		Node getValue(TNode n) const;
54		/** does the equality engine of this model have term a? */
55		bool hasTerm(TNode a);
56		/** get the representative of a in the equality engine of this model */
57		Node getRepresentative(TNode a);
58		/** are a and b equal in the equality engine of this model? */
59		bool areEqual(TNode a, TNode b);
60		/** are a and b disequal in the equality engine of this model? */
61		bool areDisequal(TNode a, TNode b);
62		/** get the equality engine for this model */
63		eq::EqualityEngine* getEqualityEngine();
64		/** get the representative set object */
65		const RepSet* getRepSet() const;
66		/** get the representative set object */
67		RepSet* getRepSetPtr();
68		/** get the entire theory model */
69		TheoryModel* getTheoryModel();
70		//---------------------------------- end access functions for underlying model
71		/** get internal representative
72		*
73		* Choose a term that is equivalent to a in the current context that is the
74		* best term for instantiating the index^th variable of quantified formula q.
75		* If no legal term can be found, we return null. This can occur if:
76		* - a's type is not a subtype of the type of the index^th variable of q,
77		* - a is in an equivalent class with all terms that are restricted not to
78		* appear in instantiations of q, e.g. INST_CONSTANT terms for counterexample
79		* guided instantiation.
80		*/
81		Node getInternalRepresentative(Node a, Node q, size_t index);
82
83		/** assert quantifier */
84		void assertQuantifier( Node n );
85		/** get number of asserted quantifiers */
86		size_t getNumAssertedQuantifiers() const;
87		/** get asserted quantifier */
88		Node getAssertedQuantifier( unsigned i, bool ordered = false );
89		/** initialize model for term */
90		void initializeModelForTerm( Node n, std::map< Node, bool >& visited );
91		// initialize the model
92		void initialize();
93		/** get variable id */
94	43042	int getVariableId(TNode q, TNode n) {
95	43042	return d_quant_var_id.find( q )!=d_quant_var_id.end() ? d_quant_var_id[q][n] : -1;
96		}
97		/** do we need to do any work? */
98		bool checkNeeded();
99		/** reset round */
100		void reset_round();
101		/** mark quantified formula relevant */
102		void markRelevant( Node q );
103		/** set quantified formula active/inactive
104		*
105		* This indicates that quantified formula is "inactive", that is, it need
106		* not be considered during this instantiation round.
107		*
108		* A quantified formula may be set inactive if for instance:
109		* - It is entailed by other quantified formulas, or
110		* - All of its instances are known to be true in the current model.
111		*
112		* This method should be called after a call to FirstOrderModel::reset_round,
113		* and before calls to QuantifiersModule check calls. A common place to call
114		* this method is during QuantifiersModule reset_round calls.
115		*/
116		void setQuantifierActive( TNode q, bool active );
117		/** is quantified formula active?
118		*
119		* Returns false if there has been a call to setQuantifierActive( q, false )
120		* during this instantiation round.
121		*/
122		bool isQuantifierActive(TNode q) const;
123		/** is quantified formula asserted */
124		bool isQuantifierAsserted(TNode q) const;
125		/** get model basis term */
126		Node getModelBasisTerm(TypeNode tn);
127		/** is model basis term */
128		bool isModelBasisTerm(Node n);
129		/** get model basis term for op */
130		Node getModelBasisOpTerm(Node op);
131		/** get model basis */
132		Node getModelBasis(Node q, Node n);
133		/** get model basis arg */
134		unsigned getModelBasisArg(Node n);
135		/** get some domain element */
136		Node getSomeDomainElement(TypeNode tn);
137		/** initialize representative set for type
138		*
139		* This ensures that TheoryModel::d_rep_set
140		* is initialized for type tn. In particular:
141		* (1) If tn is an uninitialized (unconstrained)
142		* uninterpreted sort, then we interpret it
143		* as a set of size one,
144		* (2) If tn is a "small" enumerable finite type,
145		* then we ensure that all its values are in
146		* TheoryModel::d_rep_set.
147		*
148		* Returns true if the initialization was complete,
149		* in that the set for tn in TheoryModel::d_rep_set
150		* has all representatives of type tn.
151		*/
152		bool initializeRepresentativesForType(TypeNode tn);
153		/**
154		* Has the term been marked as a model basis term?
155		*/
156		static bool isModelBasis(TNode n);
157		/** Get the equality query */
158		EqualityQuery* getEqualityQuery();
159
160		protected:
161		/** Pointer to the underyling theory model */
162		TheoryModel* d_model;
163		/** The quantifiers registry */
164		QuantifiersRegistry& d_qreg;
165		/** Reference to the term registry */
166		TermRegistry& d_treg;
167		/** equality query class */
168		EqualityQuery d_eq_query;
169		/** list of quantifiers asserted in the current context */
170		context::CDList<Node> d_forall_asserts;
171		/**
172		* The (ordered) list of quantified formulas marked as relevant using
173		* markRelevant, where the quantified formula q in the most recent
174		* call to markRelevant comes last in the list.
175		*/
176		std::vector<Node> d_forall_rlv_vec;
177		/** The last quantified formula marked as relevant, if one exists. */
178		Node d_last_forall_rlv;
179		/**
180		* The list of asserted quantified formulas, ordered by relevance.
181		* Relevance is a dynamic partial ordering where q1 < q2 if there has been
182		* a call to markRelevant( q1 ) after the last call to markRelevant( q2 )
183		* (or no call to markRelevant( q2 ) has been made).
184		*
185		* This list is used primarily as an optimization for conflict-based
186		* instantiation so that quantifed formulas that have been instantiated
187		* most recently are processed first, since these are (statistically) more
188		* likely to have conflicting instantiations.
189		*/
190		std::vector<Node> d_forall_rlv_assert;
191		/**
192		* Whether the above list has been computed. This flag is updated during
193		* reset_round and is valid within a full effort check.
194		*/
195		bool d_forallRlvComputed;
196		/** get variable id */
197		std::map<Node, std::map<Node, int> > d_quant_var_id;
198		/** process initialize model for term */
199		virtual void processInitializeModelForTerm(Node n) {}
200		/** process initialize quantifier */
201	7789	virtual void processInitializeQuantifier(Node q) {}
202		/** process initialize */
203		virtual void processInitialize(bool ispre) {}
204
205		private:
206		// list of inactive quantified formulas
207		std::map<TNode, bool> d_quant_active;
208		/** map from types to model basis terms */
209		std::map<TypeNode, Node> d_model_basis_term;
210		/** map from ops to model basis terms */
211		std::map<Node, Node> d_model_basis_op_term;
212		/** map from instantiation terms to their model basis equivalent */
213		std::map<Node, Node> d_model_basis_body;
214		/** map from universal quantifiers to model basis terms */
215		std::map<Node, std::vector<Node> > d_model_basis_terms;
216		/** compute model basis arg */
217		void computeModelBasisArgAttribute(Node n);
218		};/* class FirstOrderModel */
219
220		} // namespace quantifiers
221		} // namespace theory
222		} // namespace cvc5
223
224		#endif /* CVC5__FIRST_ORDER_MODEL_H */