Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/uf/cardinality_extension.h	Lines:	53	55	96.4 %
Date:	2021-09-14	Branches:	38	104	36.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Morgan Deters, 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.
 * ****************************************************************************
 *
 * Theory of UF with cardinality.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY_UF_STRONG_SOLVER_H
#define CVC5__THEORY_UF_STRONG_SOLVER_H

#include "context/cdhashmap.h"
#include "context/context.h"
#include "smt/env_obj.h"
#include "theory/decision_strategy.h"
#include "theory/theory.h"
#include "util/statistics_stats.h"

namespace cvc5 {
namespace theory {
namespace uf {

class TheoryUF;

/**
 * This module implements a theory solver for UF with cardinality constraints.
 * For high level details, see Reynolds et al "Finite Model Finding in SMT",
 * CAV 2013, or Reynolds dissertation "Finite Model Finding in Satisfiability
 * Modulo Theories".
 */
class CardinalityExtension : protected EnvObj
{
 protected:
  typedef context::CDHashMap<Node, bool> NodeBoolMap;
  typedef context::CDHashMap<Node, int> NodeIntMap;

 public:
  /**
   * Information for incremental conflict/clique finding for a
   * particular sort.
   */
  class SortModel
  {
   private:
    std::map< Node, std::vector< int > > d_totality_lems;
    std::map< TypeNode, std::map< int, std::vector< Node > > > d_sym_break_terms;
    std::map< Node, int > d_sym_break_index;

   public:
    /**
     * A partition of the current equality graph for which cliques
     * can occur internally.
     */
    class Region
    {
     public:
      /** information stored about each node in region */
      class RegionNodeInfo {
      public:
        /** disequality list for node */
        class DiseqList {
        public:
          DiseqList( context::Context* c )
            : d_size( c, 0 ), d_disequalities( c ) {}
          ~DiseqList(){}

          void setDisequal( Node n, bool valid ){
            Assert((!isSet(n)) || getDisequalityValue(n) != valid);
            d_disequalities[ n ] = valid;
            d_size = d_size + ( valid ? 1 : -1 );
          }
          bool isSet(Node n) const {
            return d_disequalities.find(n) != d_disequalities.end();
          }
          bool getDisequalityValue(Node n) const {
            Assert(isSet(n));
            return (*(d_disequalities.find(n))).second;
          }

          int size() const { return d_size; }

          typedef NodeBoolMap::iterator iterator;
          iterator begin() { return d_disequalities.begin(); }
          iterator end() { return d_disequalities.end(); }

        private:
          context::CDO< int > d_size;
          NodeBoolMap d_disequalities;
        }; /* class DiseqList */
       public:
        /** constructor */
        RegionNodeInfo( context::Context* c )
          : d_internal(c), d_external(c), d_valid(c, true) {
          d_disequalities[0] = &d_internal;
          d_disequalities[1] = &d_external;
        }
        ~RegionNodeInfo(){}

        int getNumDisequalities() const {
          return d_disequalities[0]->size() + d_disequalities[1]->size();
        }
        int getNumExternalDisequalities() const {
          return d_disequalities[0]->size();
        }
        int getNumInternalDisequalities() const {
          return d_disequalities[1]->size();
        }

        bool valid() const { return d_valid; }
        void setValid(bool valid) { d_valid = valid; }

        DiseqList* get(unsigned i) { return d_disequalities[i]; }

       private:
        DiseqList d_internal;
        DiseqList d_external;
        context::CDO< bool > d_valid;
        DiseqList* d_disequalities[2];
      }; /* class RegionNodeInfo */

    private:
      /** conflict find pointer */
      SortModel* d_cf;

      context::CDO<size_t> d_testCliqueSize;
      context::CDO< unsigned > d_splitsSize;
      //a postulated clique
      NodeBoolMap d_testClique;
      //disequalities needed for this clique to happen
      NodeBoolMap d_splits;
      //number of valid representatives in this region
      context::CDO<size_t> d_reps_size;
      //total disequality size (external)
      context::CDO< unsigned > d_total_diseq_external;
      //total disequality size (internal)
      context::CDO< unsigned > d_total_diseq_internal;
      /** set rep */
      void setRep( Node n, bool valid );
      //region node infomation
      std::map< Node, RegionNodeInfo* > d_nodes;
      //whether region is valid
      context::CDO< bool > d_valid;

     public:
      //constructor
      Region( SortModel* cf, context::Context* c );
      virtual ~Region();

      typedef std::map< Node, RegionNodeInfo* >::iterator iterator;
      iterator begin() { return d_nodes.begin(); }
      iterator end() { return d_nodes.end(); }

      typedef NodeBoolMap::iterator split_iterator;
      split_iterator begin_splits() { return d_splits.begin(); }
      split_iterator end_splits() { return d_splits.end(); }

      /** Returns a RegionInfo. */
      RegionNodeInfo* getRegionInfo(Node n) {
        Assert(d_nodes.find(n) != d_nodes.end());
        return (* (d_nodes.find(n))).second;
      }

      /** Returns whether or not d_valid is set in current context. */
      bool valid() const { return d_valid; }

      /** Sets d_valid to the value valid in the current context.*/
      void setValid(bool valid) { d_valid = valid; }

      /** add rep */
      void addRep( Node n );
      //take node from region
      void takeNode( Region* r, Node n );
      //merge with other region
      void combine( Region* r );
      /** merge */
      void setEqual( Node a, Node b );
      //set n1 != n2 to value 'valid', type is whether it is internal/external
      void setDisequal( Node n1, Node n2, int type, bool valid );
      //get num reps
      size_t getNumReps() const { return d_reps_size; }
      //get test clique size
      size_t getTestCliqueSize() const { return d_testCliqueSize; }
      // has representative
      bool hasRep( Node n ) {
        return d_nodes.find(n) != d_nodes.end() && d_nodes[n]->valid();
      }
      // is disequal
      bool isDisequal( Node n1, Node n2, int type );
      /** get must merge */
      bool getMustCombine( int cardinality );
      /** has splits */
      bool hasSplits() { return d_splitsSize>0; }
      /** get external disequalities */
      void getNumExternalDisequalities(std::map< Node, int >& num_ext_disequalities );
      /** check for cliques */
      bool check( Theory::Effort level, int cardinality, std::vector< Node >& clique );
      //print debug
      void debugPrint( const char* c, bool incClique = false );

      // Returns the first key in d_nodes.
      Node frontKey() const { return d_nodes.begin()->first; }
    }; /* class Region */

   private:
    /** the type this model is for */
    TypeNode d_type;
    /** Reference to the state object */
    TheoryState& d_state;
    /** Reference to the inference manager */
    TheoryInferenceManager& d_im;
    /** Pointer to the cardinality extension that owns this. */
    CardinalityExtension* d_thss;
    /** regions used to d_region_index */
    context::CDO<size_t> d_regions_index;
    /** vector of regions */
    std::vector< Region* > d_regions;
    /** map from Nodes to index of d_regions they exist in, -1 means invalid */
    NodeIntMap d_regions_map;
    /** the score for each node for splitting */
    NodeIntMap d_split_score;
    /** number of valid disequalities in d_disequalities */
    context::CDO< unsigned > d_disequalities_index;
    /** list of all disequalities */
    std::vector< Node > d_disequalities;
    /** number of representatives in all regions */
    context::CDO< unsigned > d_reps;

    /** get number of disequalities from node n to region ri */
    int getNumDisequalitiesToRegion( Node n, int ri );
    /** get number of disequalities from Region r to other regions */
    void getDisequalitiesToRegions( int ri, std::map< int, int >& regions_diseq );
    /** is valid */
    bool isValid( int ri ) {
      return ri>=0 && ri<(int)d_regions_index && d_regions[ ri ]->valid();
    }
    /** set split score */
    void setSplitScore( Node n, int s );
    /** check if we need to combine region ri */
    void checkRegion( int ri, bool checkCombine = true );
    /** force combine region */
    int forceCombineRegion( int ri, bool useDensity = true );
    /** merge regions */
    int combineRegions( int ai, int bi );
    /** move node n to region ri */
    void moveNode( Node n, int ri );
    /** allocate cardinality */
    void allocateCardinality();
    /**
     * Add splits. Returns
     *   0 = no split,
     *  -1 = entailed disequality added, or
     *   1 = split added.
     */
    int addSplit(Region* r);
    /** add clique lemma */
    void addCliqueLemma(std::vector<Node>& clique);
    /** cardinality */
    context::CDO<uint32_t> d_cardinality;
    /** cardinality lemma term */
    Node d_cardinality_term;
    /** cardinality literals */
    std::map<uint32_t, Node> d_cardinality_literal;
    /** whether a positive cardinality constraint has been asserted */
    context::CDO< bool > d_hasCard;
    /** clique lemmas that have been asserted */
    std::map< int, std::vector< std::vector< Node > > > d_cliques;
    /** maximum negatively asserted cardinality */
    context::CDO<uint32_t> d_maxNegCard;
    /** list of fresh representatives allocated */
    std::vector< Node > d_fresh_aloc_reps;
    /** whether we are initialized */
    context::CDO< bool > d_initialized;
    /** simple check cardinality */
    void simpleCheckCardinality();

   public:
    SortModel(Node n,
              TheoryState& state,
              TheoryInferenceManager& im,
              CardinalityExtension* thss);
    virtual ~SortModel();
    /** initialize */
    void initialize();
    /** new node */
    void newEqClass( Node n );
    /** merge */
    void merge( Node a, Node b );
    /** assert terms are disequal */
    void assertDisequal( Node a, Node b, Node reason );
    /** are disequal */
    bool areDisequal( Node a, Node b );
    /** check */
    void check(Theory::Effort level);
    /** presolve */
    void presolve();
    /** assert cardinality */
    void assertCardinality(uint32_t c, bool val);
    /** get cardinality */
    uint32_t getCardinality() const { return d_cardinality; }
    /** has cardinality */
    bool hasCardinalityAsserted() const { return d_hasCard; }
    /** get cardinality term */
    Node getCardinalityTerm() const { return d_cardinality_term; }
    /** get cardinality literal */
    Node getCardinalityLiteral(uint32_t c);
    /** get maximum negative cardinality */
    uint32_t getMaximumNegativeCardinality() const
    {
      return d_maxNegCard.get();
    }
    //print debug
    void debugPrint( const char* c );
    /**
     * Check at last call effort. This will verify that the model is minimal.
     * This return lemmas if there are terms in the model that the cardinality
     * extension was not notified of.
     *
     * @return false if current model is not minimal. In this case, lemmas are
     * sent on the output channel of the UF theory.
     */
    bool checkLastCall();
    /** get number of regions (for debugging) */
    int getNumRegions();

   private:
    /**
     * Decision strategy for cardinality constraints. This asserts
     * the minimal constraint positively in the SAT context. For details, see
     * Section 6.3 of Reynolds et al, "Constraint Solving for Finite Model
     * Finding in SMT Solvers", TPLP 2017.
     */
    class CardinalityDecisionStrategy : public DecisionStrategyFmf
    {
     public:
      CardinalityDecisionStrategy(Env& env, Node t, Valuation valuation);
      /** make literal (the i^th combined cardinality literal) */
      Node mkLiteral(unsigned i) override;
      /** identify */
      std::string identify() const override;

     private:
      /** the cardinality term */
      Node d_cardinality_term;
    };
    /** cardinality decision strategy */
    std::unique_ptr<CardinalityDecisionStrategy> d_c_dec_strat;
  }; /** class SortModel */

 public:
  CardinalityExtension(Env& env,
                       TheoryState& state,
                       TheoryInferenceManager& im,
                       TheoryUF* th);
  ~CardinalityExtension();
  /** get theory */
  TheoryUF* getTheory() { return d_th; }
  /** new node */
  void newEqClass( Node n );
  /** merge */
  void merge( Node a, Node b );
  /** assert terms are disequal */
  void assertDisequal( Node a, Node b, Node reason );
  /** assert node */
  void assertNode( Node n, bool isDecision );
  /** are disequal */
  bool areDisequal( Node a, Node b );
  /** check */
  void check( Theory::Effort level );
  /** presolve */
  void presolve();
  /** preregister a term */
  void preRegisterTerm( TNode n );
  /** identify */
  std::string identify() const { return std::string("CardinalityExtension"); }
  //print debug
  void debugPrint( const char* c );
  /** get cardinality for node */
  int getCardinality( Node n );
  /** get cardinality for type */
  int getCardinality( TypeNode tn );
  /** has eqc */
  bool hasEqc(Node a);

  class Statistics {
   public:
    IntStat d_clique_conflicts;
    IntStat d_clique_lemmas;
    IntStat d_split_lemmas;
    IntStat d_max_model_size;
    Statistics();
  };
  /** statistics class */
  Statistics d_statistics;

 private:
  /** get sort model */
  SortModel* getSortModel(Node n);
  /** initialize */
  void initializeCombinedCardinality();
  /** check */
  void checkCombinedCardinality();
  /** ensure eqc */
  void ensureEqc(SortModel* c, Node a);
  /** ensure eqc for all subterms of n */
  void ensureEqcRec(Node n);

  /** Reference to the state object */
  TheoryState& d_state;
  /** Reference to the inference manager */
  TheoryInferenceManager& d_im;
  /** theory uf pointer */
  TheoryUF* d_th;
  /** rep model structure, one for each type */
  std::map<TypeNode, SortModel*> d_rep_model;

  /** minimum positive combined cardinality */
  context::CDO<uint32_t> d_min_pos_com_card;
  /** Whether the field above has been set */
  context::CDO<bool> d_min_pos_com_card_set;
  /**
   * Decision strategy for combined cardinality constraints. This asserts
   * the minimal combined cardinality constraint positively in the SAT
   * context. It is enabled by options::ufssFairness(). For details, see
   * the extension to multiple sorts in Section 6.3 of Reynolds et al,
   * "Constraint Solving for Finite Model Finding in SMT Solvers", TPLP 2017.
   */
  class CombinedCardinalityDecisionStrategy : public DecisionStrategyFmf
  {
   public:
    CombinedCardinalityDecisionStrategy(Env& env, Valuation valuation);
    /** make literal (the i^th combined cardinality literal) */
    Node mkLiteral(unsigned i) override;
    /** identify */
    std::string identify() const override;
  };
  /** combined cardinality decision strategy */
  std::unique_ptr<CombinedCardinalityDecisionStrategy> d_cc_dec_strat;
  /** Have we initialized combined cardinality? */
  context::CDO<bool> d_initializedCombinedCardinality;

  /** cardinality literals for which we have added */
  NodeBoolMap d_card_assertions_eqv_lemma;
  /** the master monotone type (if ufssFairnessMonotone enabled) */
  TypeNode d_tn_mono_master;
  std::map<TypeNode, bool> d_tn_mono_slave;
  /** The minimum positive asserted master cardinality */
  context::CDO<uint32_t> d_min_pos_tn_master_card;
  /** Whether the field above has been set */
  context::CDO<bool> d_min_pos_tn_master_card_set;
  /** relevant eqc */
  NodeBoolMap d_rel_eqc;
}; /* class CardinalityExtension */

}  // namespace uf
}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY_UF_STRONG_SOLVER_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Morgan Deters, 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		* Theory of UF with cardinality.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY_UF_STRONG_SOLVER_H
19		#define CVC5__THEORY_UF_STRONG_SOLVER_H
20
21		#include "context/cdhashmap.h"
22		#include "context/context.h"
23		#include "smt/env_obj.h"
24		#include "theory/decision_strategy.h"
25		#include "theory/theory.h"
26		#include "util/statistics_stats.h"
27
28		namespace cvc5 {
29		namespace theory {
30		namespace uf {
31
32		class TheoryUF;
33
34		/**
35		* This module implements a theory solver for UF with cardinality constraints.
36		* For high level details, see Reynolds et al "Finite Model Finding in SMT",
37		* CAV 2013, or Reynolds dissertation "Finite Model Finding in Satisfiability
38		* Modulo Theories".
39		*/
40		class CardinalityExtension : protected EnvObj
41		{
42		protected:
43		typedef context::CDHashMap<Node, bool> NodeBoolMap;
44		typedef context::CDHashMap<Node, int> NodeIntMap;
45
46		public:
47		/**
48		* Information for incremental conflict/clique finding for a
49		* particular sort.
50		*/
51		class SortModel
52		{
53		private:
54		std::map< Node, std::vector< int > > d_totality_lems;
55		std::map< TypeNode, std::map< int, std::vector< Node > > > d_sym_break_terms;
56		std::map< Node, int > d_sym_break_index;
57
58		public:
59		/**
60		* A partition of the current equality graph for which cliques
61		* can occur internally.
62		*/
63		class Region
64		{
65		public:
66		/** information stored about each node in region */
67		class RegionNodeInfo {
68		public:
69		/** disequality list for node */
70		class DiseqList {
71		public:
72	19308	DiseqList( context::Context* c )
73	19308	: d_size( c, 0 ), d_disequalities( c ) {}
74	19308	~DiseqList(){}
75
76	373151	void setDisequal( Node n, bool valid ){
77	373151	Assert((!isSet(n)) \|\| getDisequalityValue(n) != valid);
78	373151	d_disequalities[ n ] = valid;
79	373151	d_size = d_size + ( valid ? 1 : -1 );
80	373151	}
81	1146915	bool isSet(Node n) const {
82	1146915	return d_disequalities.find(n) != d_disequalities.end();
83		}
84	316209	bool getDisequalityValue(Node n) const {
85	316209	Assert(isSet(n));
86	316209	return (*(d_disequalities.find(n))).second;
87		}
88
89	199980	int size() const { return d_size; }
90
91		typedef NodeBoolMap::iterator iterator;
92	176534	iterator begin() { return d_disequalities.begin(); }
93	409193	iterator end() { return d_disequalities.end(); }
94
95		private:
96		context::CDO< int > d_size;
97		NodeBoolMap d_disequalities;
98		}; /* class DiseqList */
99		public:
100		/** constructor */
101	9654	RegionNodeInfo( context::Context* c )
102	9654	: d_internal(c), d_external(c), d_valid(c, true) {
103	9654	d_disequalities[0] = &d_internal;
104	9654	d_disequalities[1] = &d_external;
105	9654	}
106	9654	~RegionNodeInfo(){}
107
108	60620	int getNumDisequalities() const {
109	60620	return d_disequalities[0]->size() + d_disequalities[1]->size();
110		}
111	46846	int getNumExternalDisequalities() const {
112	46846	return d_disequalities[0]->size();
113		}
114	31894	int getNumInternalDisequalities() const {
115	31894	return d_disequalities[1]->size();
116		}
117
118	1031268	bool valid() const { return d_valid; }
119	80905	void setValid(bool valid) { d_valid = valid; }
120
121	1007240	DiseqList* get(unsigned i) { return d_disequalities[i]; }
122
123		private:
124		DiseqList d_internal;
125		DiseqList d_external;
126		context::CDO< bool > d_valid;
127		DiseqList* d_disequalities[2];
128		}; /* class RegionNodeInfo */
129
130		private:
131		/** conflict find pointer */
132		SortModel* d_cf;
133
134		context::CDO<size_t> d_testCliqueSize;
135		context::CDO< unsigned > d_splitsSize;
136		//a postulated clique
137		NodeBoolMap d_testClique;
138		//disequalities needed for this clique to happen
139		NodeBoolMap d_splits;
140		//number of valid representatives in this region
141		context::CDO<size_t> d_reps_size;
142		//total disequality size (external)
143		context::CDO< unsigned > d_total_diseq_external;
144		//total disequality size (internal)
145		context::CDO< unsigned > d_total_diseq_internal;
146		/** set rep */
147		void setRep( Node n, bool valid );
148		//region node infomation
149		std::map< Node, RegionNodeInfo* > d_nodes;
150		//whether region is valid
151		context::CDO< bool > d_valid;
152
153		public:
154		//constructor
155		Region( SortModel* cf, context::Context* c );
156		virtual ~Region();
157
158		typedef std::map< Node, RegionNodeInfo* >::iterator iterator;
159	74865	iterator begin() { return d_nodes.begin(); }
160	516636	iterator end() { return d_nodes.end(); }
161
162		typedef NodeBoolMap::iterator split_iterator;
163	3578	split_iterator begin_splits() { return d_splits.begin(); }
164	23373	split_iterator end_splits() { return d_splits.end(); }
165
166		/** Returns a RegionInfo. */
167	32176	RegionNodeInfo* getRegionInfo(Node n) {
168	32176	Assert(d_nodes.find(n) != d_nodes.end());
169	32176	return (* (d_nodes.find(n))).second;
170		}
171
172		/** Returns whether or not d_valid is set in current context. */
173	3000227	bool valid() const { return d_valid; }
174
175		/** Sets d_valid to the value valid in the current context.*/
176	42828	void setValid(bool valid) { d_valid = valid; }
177
178		/** add rep */
179		void addRep( Node n );
180		//take node from region
181		void takeNode( Region* r, Node n );
182		//merge with other region
183		void combine( Region* r );
184		/** merge */
185		void setEqual( Node a, Node b );
186		//set n1 != n2 to value 'valid', type is whether it is internal/external
187		void setDisequal( Node n1, Node n2, int type, bool valid );
188		//get num reps
189	164721	size_t getNumReps() const { return d_reps_size; }
190		//get test clique size
191		size_t getTestCliqueSize() const { return d_testCliqueSize; }
192		// has representative
193	251460	bool hasRep( Node n ) {
194	251460	return d_nodes.find(n) != d_nodes.end() && d_nodes[n]->valid();
195		}
196		// is disequal
197		bool isDisequal( Node n1, Node n2, int type );
198		/** get must merge */
199		bool getMustCombine( int cardinality );
200		/** has splits */
201	2016	bool hasSplits() { return d_splitsSize>0; }
202		/** get external disequalities */
203		void getNumExternalDisequalities(std::map< Node, int >& num_ext_disequalities );
204		/** check for cliques */
205		bool check( Theory::Effort level, int cardinality, std::vector< Node >& clique );
206		//print debug
207		void debugPrint( const char* c, bool incClique = false );
208
209		// Returns the first key in d_nodes.
210	108	Node frontKey() const { return d_nodes.begin()->first; }
211		}; /* class Region */
212
213		private:
214		/** the type this model is for */
215		TypeNode d_type;
216		/** Reference to the state object */
217		TheoryState& d_state;
218		/** Reference to the inference manager */
219		TheoryInferenceManager& d_im;
220		/** Pointer to the cardinality extension that owns this. */
221		CardinalityExtension* d_thss;
222		/** regions used to d_region_index */
223		context::CDO<size_t> d_regions_index;
224		/** vector of regions */
225		std::vector< Region* > d_regions;
226		/** map from Nodes to index of d_regions they exist in, -1 means invalid */
227		NodeIntMap d_regions_map;
228		/** the score for each node for splitting */
229		NodeIntMap d_split_score;
230		/** number of valid disequalities in d_disequalities */
231		context::CDO< unsigned > d_disequalities_index;
232		/** list of all disequalities */
233		std::vector< Node > d_disequalities;
234		/** number of representatives in all regions */
235		context::CDO< unsigned > d_reps;
236
237		/** get number of disequalities from node n to region ri */
238		int getNumDisequalitiesToRegion( Node n, int ri );
239		/** get number of disequalities from Region r to other regions */
240		void getDisequalitiesToRegions( int ri, std::map< int, int >& regions_diseq );
241		/** is valid */
242	351612	bool isValid( int ri ) {
243	351612	return ri>=0 && ri<(int)d_regions_index && d_regions[ ri ]->valid();
244		}
245		/** set split score */
246		void setSplitScore( Node n, int s );
247		/** check if we need to combine region ri */
248		void checkRegion( int ri, bool checkCombine = true );
249		/** force combine region */
250		int forceCombineRegion( int ri, bool useDensity = true );
251		/** merge regions */
252		int combineRegions( int ai, int bi );
253		/** move node n to region ri */
254		void moveNode( Node n, int ri );
255		/** allocate cardinality */
256		void allocateCardinality();
257		/**
258		* Add splits. Returns
259		* 0 = no split,
260		* -1 = entailed disequality added, or
261		* 1 = split added.
262		*/
263		int addSplit(Region* r);
264		/** add clique lemma */
265		void addCliqueLemma(std::vector<Node>& clique);
266		/** cardinality */
267		context::CDO<uint32_t> d_cardinality;
268		/** cardinality lemma term */
269		Node d_cardinality_term;
270		/** cardinality literals */
271		std::map<uint32_t, Node> d_cardinality_literal;
272		/** whether a positive cardinality constraint has been asserted */
273		context::CDO< bool > d_hasCard;
274		/** clique lemmas that have been asserted */
275		std::map< int, std::vector< std::vector< Node > > > d_cliques;
276		/** maximum negatively asserted cardinality */
277		context::CDO<uint32_t> d_maxNegCard;
278		/** list of fresh representatives allocated */
279		std::vector< Node > d_fresh_aloc_reps;
280		/** whether we are initialized */
281		context::CDO< bool > d_initialized;
282		/** simple check cardinality */
283		void simpleCheckCardinality();
284
285		public:
286		SortModel(Node n,
287		TheoryState& state,
288		TheoryInferenceManager& im,
289		CardinalityExtension* thss);
290		virtual ~SortModel();
291		/** initialize */
292		void initialize();
293		/** new node */
294		void newEqClass( Node n );
295		/** merge */
296		void merge( Node a, Node b );
297		/** assert terms are disequal */
298		void assertDisequal( Node a, Node b, Node reason );
299		/** are disequal */
300		bool areDisequal( Node a, Node b );
301		/** check */
302		void check(Theory::Effort level);
303		/** presolve */
304		void presolve();
305		/** assert cardinality */
306		void assertCardinality(uint32_t c, bool val);
307		/** get cardinality */
308		uint32_t getCardinality() const { return d_cardinality; }
309		/** has cardinality */
310		bool hasCardinalityAsserted() const { return d_hasCard; }
311		/** get cardinality term */
312	9082	Node getCardinalityTerm() const { return d_cardinality_term; }
313		/** get cardinality literal */
314		Node getCardinalityLiteral(uint32_t c);
315		/** get maximum negative cardinality */
316	64831	uint32_t getMaximumNegativeCardinality() const
317		{
318	64831	return d_maxNegCard.get();
319		}
320		//print debug
321		void debugPrint( const char* c );
322		/**
323		* Check at last call effort. This will verify that the model is minimal.
324		* This return lemmas if there are terms in the model that the cardinality
325		* extension was not notified of.
326		*
327		* @return false if current model is not minimal. In this case, lemmas are
328		* sent on the output channel of the UF theory.
329		*/
330		bool checkLastCall();
331		/** get number of regions (for debugging) */
332		int getNumRegions();
333
334		private:
335		/**
336		* Decision strategy for cardinality constraints. This asserts
337		* the minimal constraint positively in the SAT context. For details, see
338		* Section 6.3 of Reynolds et al, "Constraint Solving for Finite Model
339		* Finding in SMT Solvers", TPLP 2017.
340		*/
341	920	class CardinalityDecisionStrategy : public DecisionStrategyFmf
342		{
343		public:
344		CardinalityDecisionStrategy(Env& env, Node t, Valuation valuation);
345		/** make literal (the i^th combined cardinality literal) */
346		Node mkLiteral(unsigned i) override;
347		/** identify */
348		std::string identify() const override;
349
350		private:
351		/** the cardinality term */
352		Node d_cardinality_term;
353		};
354		/** cardinality decision strategy */
355		std::unique_ptr<CardinalityDecisionStrategy> d_c_dec_strat;
356		}; /** class SortModel */
357
358		public:
359		CardinalityExtension(Env& env,
360		TheoryState& state,
361		TheoryInferenceManager& im,
362		TheoryUF* th);
363		~CardinalityExtension();
364		/** get theory */
365	22248	TheoryUF* getTheory() { return d_th; }
366		/** new node */
367		void newEqClass( Node n );
368		/** merge */
369		void merge( Node a, Node b );
370		/** assert terms are disequal */
371		void assertDisequal( Node a, Node b, Node reason );
372		/** assert node */
373		void assertNode( Node n, bool isDecision );
374		/** are disequal */
375		bool areDisequal( Node a, Node b );
376		/** check */
377		void check( Theory::Effort level );
378		/** presolve */
379		void presolve();
380		/** preregister a term */
381		void preRegisterTerm( TNode n );
382		/** identify */
383		std::string identify() const { return std::string("CardinalityExtension"); }
384		//print debug
385		void debugPrint( const char* c );
386		/** get cardinality for node */
387		int getCardinality( Node n );
388		/** get cardinality for type */
389		int getCardinality( TypeNode tn );
390		/** has eqc */
391		bool hasEqc(Node a);
392
393		class Statistics {
394		public:
395		IntStat d_clique_conflicts;
396		IntStat d_clique_lemmas;
397		IntStat d_split_lemmas;
398		IntStat d_max_model_size;
399		Statistics();
400		};
401		/** statistics class */
402		Statistics d_statistics;
403
404		private:
405		/** get sort model */
406		SortModel* getSortModel(Node n);
407		/** initialize */
408		void initializeCombinedCardinality();
409		/** check */
410		void checkCombinedCardinality();
411		/** ensure eqc */
412		void ensureEqc(SortModel* c, Node a);
413		/** ensure eqc for all subterms of n */
414		void ensureEqcRec(Node n);
415
416		/** Reference to the state object */
417		TheoryState& d_state;
418		/** Reference to the inference manager */
419		TheoryInferenceManager& d_im;
420		/** theory uf pointer */
421		TheoryUF* d_th;
422		/** rep model structure, one for each type */
423		std::map<TypeNode, SortModel*> d_rep_model;
424
425		/** minimum positive combined cardinality */
426		context::CDO<uint32_t> d_min_pos_com_card;
427		/** Whether the field above has been set */
428		context::CDO<bool> d_min_pos_com_card_set;
429		/**
430		* Decision strategy for combined cardinality constraints. This asserts
431		* the minimal combined cardinality constraint positively in the SAT
432		* context. It is enabled by options::ufssFairness(). For details, see
433		* the extension to multiple sorts in Section 6.3 of Reynolds et al,
434		* "Constraint Solving for Finite Model Finding in SMT Solvers", TPLP 2017.
435		*/
436	560	class CombinedCardinalityDecisionStrategy : public DecisionStrategyFmf
437		{
438		public:
439		CombinedCardinalityDecisionStrategy(Env& env, Valuation valuation);
440		/** make literal (the i^th combined cardinality literal) */
441		Node mkLiteral(unsigned i) override;
442		/** identify */
443		std::string identify() const override;
444		};
445		/** combined cardinality decision strategy */
446		std::unique_ptr<CombinedCardinalityDecisionStrategy> d_cc_dec_strat;
447		/** Have we initialized combined cardinality? */
448		context::CDO<bool> d_initializedCombinedCardinality;
449
450		/** cardinality literals for which we have added */
451		NodeBoolMap d_card_assertions_eqv_lemma;
452		/** the master monotone type (if ufssFairnessMonotone enabled) */
453		TypeNode d_tn_mono_master;
454		std::map<TypeNode, bool> d_tn_mono_slave;
455		/** The minimum positive asserted master cardinality */
456		context::CDO<uint32_t> d_min_pos_tn_master_card;
457		/** Whether the field above has been set */
458		context::CDO<bool> d_min_pos_tn_master_card_set;
459		/** relevant eqc */
460		NodeBoolMap d_rel_eqc;
461		}; /* class CardinalityExtension */
462
463		} // namespace uf
464		} // namespace theory
465		} // namespace cvc5
466
467		#endif /* CVC5__THEORY_UF_STRONG_SOLVER_H */