1 /*********************                                                        */
2 /*! \file full_model_check.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Andrew Reynolds, Morgan Deters, Mathias Preiner
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 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.\endverbatim
11  **
12  ** \brief Full model check class
13  **/
14 
15 #include "cvc4_private.h"
16 
17 #ifndef __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
18 #define __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
19 
20 #include "theory/quantifiers/fmf/model_builder.h"
21 #include "theory/quantifiers/first_order_model.h"
22 
23 namespace CVC4 {
24 namespace theory {
25 namespace quantifiers {
26 namespace fmcheck {
27 
28 
29 class FirstOrderModelFmc;
30 class FullModelChecker;
31 
32 class EntryTrie
33 {
34 private:
35   int d_complete;
36 public:
EntryTrie()37   EntryTrie() : d_complete(-1), d_data(-1){}
38   std::map<Node,EntryTrie> d_child;
39   int d_data;
reset()40   void reset() { d_data = -1; d_child.clear(); d_complete = -1; }
41   void addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int index = 0 );
42   bool hasGeneralization( FirstOrderModelFmc * m, Node c, int index = 0 );
43   int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index = 0 );
44   void getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index = 0, bool is_gen = true );
45 };/* class EntryTrie */
46 
47 
48 class Def
49 {
50 public:
51   EntryTrie d_et;
52   //cond is APPLY_UF whose arguments are returned by FullModelChecker::getRepresentative
53   std::vector< Node > d_cond;
54   //value is returned by FullModelChecker::getRepresentative
55   std::vector< Node > d_value;
56   void basic_simplify( FirstOrderModelFmc * m );
57 private:
58   enum {
59     status_unk,
60     status_redundant,
61     status_non_redundant
62   };
63   std::vector< int > d_status;
64   bool d_has_simplified;
65 public:
Def()66   Def() : d_has_simplified(false){}
reset()67   void reset() {
68     d_et.reset();
69     d_cond.clear();
70     d_value.clear();
71     d_status.clear();
72     d_has_simplified = false;
73   }
74   bool addEntry( FirstOrderModelFmc * m, Node c, Node v);
75   Node evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst );
76   int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& inst );
77   void simplify( FullModelChecker * mc, FirstOrderModelFmc * m );
78   void debugPrint(const char * tr, Node op, FullModelChecker * m);
79 };/* class Def */
80 
81 
82 class FullModelChecker : public QModelBuilder
83 {
84 protected:
85   Node d_true;
86   Node d_false;
87   std::map<TypeNode, std::map< Node, int > > d_rep_ids;
88   std::map<Node, Def > d_quant_models;
89   std::map<Node, Node > d_quant_cond;
90   std::map< TypeNode, Node > d_array_cond;
91   std::map< Node, Node > d_array_term_cond;
92   std::map< Node, std::vector< int > > d_star_insts;
93   //--------------------for preinitialization
94   /** preInitializeType
95    *
96    * This function ensures that the model fm is properly initialized with
97    * respect to type tn.
98    *
99    * In particular, this class relies on the use of "model basis" terms, which
100    * are distinguished terms that are used to specify default values for
101    * uninterpreted functions. This method enforces that the model basis term
102    * occurs in the model for each relevant type T, where a type T is relevant
103    * if a bound variable is of type T, or an uninterpreted function has an
104    * argument or a return value of type T.
105    */
106   void preInitializeType( FirstOrderModelFmc * fm, TypeNode tn );
107   /** for each type, an equivalence class of that type from the model */
108   std::map<TypeNode, Node> d_preinitialized_eqc;
109   /** map from types to whether we have called the method above */
110   std::map<TypeNode, bool> d_preinitialized_types;
111   //--------------------end for preinitialization
112   Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);
113   bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index);
114 private:
115   void doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n );
116 
117   void doNegate( Def & dc );
118   void doVariableEquality( FirstOrderModelFmc * fm, Node f, Def & d, Node eq );
119   void doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v);
120   void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n, std::vector< Def > & dc );
121 
122   void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d,
123                                Def & df, std::vector< Def > & dc, int index,
124                                std::vector< Node > & cond, std::vector<Node> & val );
125   void doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
126                                 std::map< int, Node > & entries, int index,
127                                 std::vector< Node > & cond, std::vector< Node > & val,
128                                 EntryTrie & curr);
129 
130   void doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n,
131                              std::vector< Def > & dc, int index,
132                              std::vector< Node > & cond, std::vector<Node> & val );
133   int isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c );
134   bool doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c );
135   Node mkCond( std::vector< Node > & cond );
136   Node mkCondDefault( FirstOrderModelFmc * fm, Node f );
137   void mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond );
138   void mkCondVec( Node n, std::vector< Node > & cond );
139   Node evaluateInterpreted( Node n, std::vector< Node > & vals );
140   Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
141 public:
142   FullModelChecker( context::Context* c, QuantifiersEngine* qe );
143 
144   void debugPrintCond(const char * tr, Node n, bool dispStar = false);
145   void debugPrint(const char * tr, Node n, bool dispStar = false);
146 
147   int doExhaustiveInstantiation(FirstOrderModel* fm,
148                                 Node f,
149                                 int effort) override;
150 
151   Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix );
152 
153   /** process build model */
154   bool preProcessBuildModel(TheoryModel* m) override;
155   bool processBuildModel(TheoryModel* m) override;
156 
157   bool useSimpleModels();
158 };/* class FullModelChecker */
159 
160 }/* CVC4::theory::quantifiers::fmcheck namespace */
161 }/* CVC4::theory::quantifiers namespace */
162 }/* CVC4::theory namespace */
163 }/* CVC4 namespace */
164 
165 #endif /* __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H */
166