GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/fmf/model_builder.cpp Lines: 32 64 50.0 %
Date: 2021-03-22 Branches: 44 232 19.0 %

Line Exec Source
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-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.\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/fmf/model_engine.h"
20
#include "theory/quantifiers/instantiate.h"
21
#include "theory/quantifiers/quant_rep_bound_ext.h"
22
#include "theory/quantifiers/quantifiers_state.h"
23
#include "theory/quantifiers_engine.h"
24
#include "theory/uf/equality_engine.h"
25
26
using namespace std;
27
using namespace CVC4;
28
using namespace CVC4::kind;
29
using namespace CVC4::context;
30
using namespace CVC4::theory;
31
using namespace CVC4::theory::quantifiers;
32
33
822
QModelBuilder::QModelBuilder(QuantifiersState& qs, QuantifiersRegistry& qr)
34
    : TheoryEngineModelBuilder(),
35
      d_addedLemmas(0),
36
      d_triedLemmas(0),
37
      d_qe(nullptr),
38
      d_qstate(qs),
39
822
      d_qreg(qr)
40
{
41
822
}
42
43
11036
bool QModelBuilder::optUseModel() {
44
11036
  return options::mbqiMode() != options::MbqiMode::NONE || options::fmfBound();
45
}
46
47
28
bool QModelBuilder::preProcessBuildModel(TheoryModel* m) {
48
28
  return preProcessBuildModelStd( m );
49
}
50
51
1616
bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) {
52
1616
  d_addedLemmas = 0;
53
1616
  d_triedLemmas = 0;
54
1616
  if (options::fmfFunWellDefinedRelevant())
55
  {
56
85
    FirstOrderModel * fm = (FirstOrderModel*)m;
57
    //traverse equality engine
58
170
    std::map< TypeNode, bool > eqc_usort;
59
    eq::EqClassesIterator eqcs_i =
60
85
        eq::EqClassesIterator(fm->getEqualityEngine());
61
5297
    while( !eqcs_i.isFinished() ){
62
5212
      TypeNode tr = (*eqcs_i).getType();
63
2606
      eqc_usort[tr] = true;
64
2606
      ++eqcs_i;
65
    }
66
    //look at quantified formulas
67
611
    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
68
1052
      Node q = fm->getAssertedQuantifier( i, true );
69
526
      if( fm->isQuantifierActive( q ) ){
70
        //check if any of these quantified formulas can be set inactive
71
526
        if (q[0].getNumChildren() == 1)
72
        {
73
1052
          TypeNode tn = q[0][0].getType();
74
526
          if (tn.getAttribute(AbsTypeFunDefAttribute()))
75
          {
76
            // we are allowed to assume the introduced type is empty
77
505
            if (eqc_usort.find(tn) == eqc_usort.end())
78
            {
79
78
              Trace("model-engine-debug")
80
39
                  << "Irrelevant function definition : " << q << std::endl;
81
39
              fm->setQuantifierActive( q, false );
82
            }
83
          }
84
        }
85
      }
86
    }
87
  }
88
1616
  return true;
89
}
90
91
109
void QModelBuilder::debugModel( TheoryModel* m ){
92
  //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
93
109
  if( Trace.isOn("quant-check-model") ){
94
    FirstOrderModel* fm = (FirstOrderModel*)m;
95
    Trace("quant-check-model") << "Testing quantifier instantiations..." << std::endl;
96
    int tests = 0;
97
    int bad = 0;
98
    QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
99
    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
100
      Node f = fm->getAssertedQuantifier( i );
101
      std::vector< Node > vars;
102
      for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
103
        vars.push_back( f[0][j] );
104
      }
105
      QRepBoundExt qrbe(qbi, fm);
106
      RepSetIterator riter(fm->getRepSet(), &qrbe);
107
      if( riter.setQuantifier( f ) ){
108
        while( !riter.isFinished() ){
109
          tests++;
110
          std::vector< Node > terms;
111
          for (unsigned k = 0; k < riter.getNumTerms(); k++)
112
          {
113
            terms.push_back( riter.getCurrentTerm( k ) );
114
          }
115
          Node n = d_qe->getInstantiate()->getInstantiation(f, vars, terms);
116
          Node val = fm->getValue( n );
117
          if (!val.isConst() || !val.getConst<bool>())
118
          {
119
            Trace("quant-check-model") << "*******  Instantiation " << n << " for " << std::endl;
120
            Trace("quant-check-model") << "         " << f << std::endl;
121
            Trace("quant-check-model") << "         Evaluates to " << val << std::endl;
122
            bad++;
123
          }
124
          riter.increment();
125
        }
126
        Trace("quant-check-model") << "Tested " << tests << " instantiations";
127
        if( bad>0 ){
128
          Trace("quant-check-model") << ", " << bad << " failed" << std::endl;
129
        }
130
        Trace("quant-check-model") << "." << std::endl;
131
      }else{
132
        if( riter.isIncomplete() ){
133
          Trace("quant-check-model") << "Warning: Could not test quantifier " << f << std::endl;
134
        }
135
      }
136
    }
137
  }
138
26785
}