1 /********************* */
2 /*! \file model_builder.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters, Tim King
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 Implementation of model builder class
13 **/
14
15 #include "theory/quantifiers/fmf/model_builder.h"
16
17 #include "options/quantifiers_options.h"
18 #include "theory/quantifiers/first_order_model.h"
19 #include "theory/quantifiers/instantiate.h"
20 #include "theory/quantifiers/fmf/model_engine.h"
21 #include "theory/quantifiers/quantifiers_attributes.h"
22 #include "theory/quantifiers/term_database.h"
23 #include "theory/quantifiers/term_util.h"
24 #include "theory/quantifiers/ematching/trigger.h"
25 #include "theory/theory_engine.h"
26 #include "theory/uf/equality_engine.h"
27 #include "theory/uf/theory_uf.h"
28 #include "theory/uf/theory_uf_model.h"
29 #include "theory/uf/theory_uf_strong_solver.h"
30
31 using namespace std;
32 using namespace CVC4;
33 using namespace CVC4::kind;
34 using namespace CVC4::context;
35 using namespace CVC4::theory;
36 using namespace CVC4::theory::quantifiers;
37
QModelBuilder(context::Context * c,QuantifiersEngine * qe)38 QModelBuilder::QModelBuilder(context::Context* c, QuantifiersEngine* qe)
39 : TheoryEngineModelBuilder(qe->getTheoryEngine()),
40 d_qe(qe),
41 d_addedLemmas(0),
42 d_triedLemmas(0) {}
43
optUseModel()44 bool QModelBuilder::optUseModel() {
45 return options::mbqiMode()!=MBQI_NONE || options::fmfBound();
46 }
47
preProcessBuildModel(TheoryModel * m)48 bool QModelBuilder::preProcessBuildModel(TheoryModel* m) {
49 return preProcessBuildModelStd( m );
50 }
51
preProcessBuildModelStd(TheoryModel * m)52 bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) {
53 d_addedLemmas = 0;
54 d_triedLemmas = 0;
55 if( options::fmfEmptySorts() || options::fmfFunWellDefinedRelevant() ){
56 FirstOrderModel * fm = (FirstOrderModel*)m;
57 //traverse equality engine
58 std::map< TypeNode, bool > eqc_usort;
59 eq::EqClassesIterator eqcs_i =
60 eq::EqClassesIterator(fm->getEqualityEngine());
61 while( !eqcs_i.isFinished() ){
62 TypeNode tr = (*eqcs_i).getType();
63 eqc_usort[tr] = true;
64 ++eqcs_i;
65 }
66 //look at quantified formulas
67 for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
68 Node q = fm->getAssertedQuantifier( i, true );
69 if( fm->isQuantifierActive( q ) ){
70 //check if any of these quantified formulas can be set inactive
71 if( options::fmfEmptySorts() ){
72 for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
73 TypeNode tn = q[0][i].getType();
74 //we are allowed to assume the type is empty
75 if( tn.isSort() && eqc_usort.find( tn )==eqc_usort.end() ){
76 Trace("model-engine-debug") << "Empty domain quantified formula : " << q << std::endl;
77 fm->setQuantifierActive( q, false );
78 }
79 }
80 }else if( options::fmfFunWellDefinedRelevant() ){
81 if( q[0].getNumChildren()==1 ){
82 TypeNode tn = q[0][0].getType();
83 if( tn.getAttribute(AbsTypeFunDefAttribute()) ){
84 //Trace("model-engine-debug2") << "...possible irrelevant function def : " << q << ", #rr = " << d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn ) << std::endl;
85 //we are allowed to assume the introduced type is empty
86 if( eqc_usort.find( tn )==eqc_usort.end() ){
87 Trace("model-engine-debug") << "Irrelevant function definition : " << q << std::endl;
88 fm->setQuantifierActive( q, false );
89 }
90 }
91 }
92 }
93 }
94 }
95 }
96 return true;
97 }
98
debugModel(TheoryModel * m)99 void QModelBuilder::debugModel( TheoryModel* m ){
100 //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
101 if( Trace.isOn("quant-check-model") ){
102 FirstOrderModel* fm = (FirstOrderModel*)m;
103 Trace("quant-check-model") << "Testing quantifier instantiations..." << std::endl;
104 int tests = 0;
105 int bad = 0;
106 for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
107 Node f = fm->getAssertedQuantifier( i );
108 std::vector< Node > vars;
109 for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
110 vars.push_back( f[0][j] );
111 }
112 QRepBoundExt qrbe(d_qe);
113 RepSetIterator riter(d_qe->getModel()->getRepSet(), &qrbe);
114 if( riter.setQuantifier( f ) ){
115 while( !riter.isFinished() ){
116 tests++;
117 std::vector< Node > terms;
118 for (unsigned k = 0; k < riter.getNumTerms(); k++)
119 {
120 terms.push_back( riter.getCurrentTerm( k ) );
121 }
122 Node n = d_qe->getInstantiate()->getInstantiation(f, vars, terms);
123 Node val = fm->getValue( n );
124 if (val != d_qe->getTermUtil()->d_true)
125 {
126 Trace("quant-check-model") << "******* Instantiation " << n << " for " << std::endl;
127 Trace("quant-check-model") << " " << f << std::endl;
128 Trace("quant-check-model") << " Evaluates to " << val << std::endl;
129 bad++;
130 }
131 riter.increment();
132 }
133 Trace("quant-check-model") << "Tested " << tests << " instantiations";
134 if( bad>0 ){
135 Trace("quant-check-model") << ", " << bad << " failed" << std::endl;
136 }
137 Trace("quant-check-model") << "." << std::endl;
138 }else{
139 if( riter.isIncomplete() ){
140 Trace("quant-check-model") << "Warning: Could not test quantifier " << f << std::endl;
141 }
142 }
143 }
144 }
145 }
146