GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/theory_quantifiers.cpp Lines: 81 85 95.3 %
Date: 2021-03-23 Branches: 108 208 51.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_quantifiers.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 the theory of quantifiers
13
 **
14
 ** Implementation of the theory of quantifiers.
15
 **/
16
17
#include "theory/quantifiers/theory_quantifiers.h"
18
19
#include "expr/proof_node_manager.h"
20
#include "options/quantifiers_options.h"
21
#include "theory/quantifiers/first_order_model.h"
22
#include "theory/quantifiers/fmf/first_order_model_fmc.h"
23
#include "theory/quantifiers/quantifiers_modules.h"
24
#include "theory/quantifiers/quantifiers_rewriter.h"
25
#include "theory/valuation.h"
26
27
using namespace CVC4::kind;
28
using namespace CVC4::context;
29
30
namespace CVC4 {
31
namespace theory {
32
namespace quantifiers {
33
34
8997
TheoryQuantifiers::TheoryQuantifiers(Context* c,
35
                                     context::UserContext* u,
36
                                     OutputChannel& out,
37
                                     Valuation valuation,
38
                                     const LogicInfo& logicInfo,
39
8997
                                     ProofNodeManager* pnm)
40
    : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm),
41
      d_qstate(c, u, valuation, logicInfo),
42
      d_qreg(),
43
      d_treg(d_qstate, d_qreg),
44
      d_qim(nullptr),
45
8997
      d_qengine(nullptr)
46
{
47
8997
  out.handleUserAttribute( "fun-def", this );
48
8997
  out.handleUserAttribute("qid", this);
49
8997
  out.handleUserAttribute( "quant-inst-max-level", this );
50
8997
  out.handleUserAttribute( "quant-elim", this );
51
8997
  out.handleUserAttribute( "quant-elim-partial", this );
52
53
8997
  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
54
8997
  if (pc != nullptr)
55
  {
56
    // add the proof rules
57
962
    d_qChecker.registerTo(pc);
58
  }
59
60
8997
  Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
61
17994
  Trace("quant-engine-debug")
62
8997
      << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
63
  // Finite model finding requires specialized ways of building the model.
64
  // We require constructing the model here, since it is required for
65
  // initializing the CombinationEngine and the rest of quantifiers engine.
66
26741
  if ((options::finiteModelFind() || options::fmfBound())
67
9837
      && QuantifiersModules::useFmcModel())
68
  {
69
1652
    d_qmodel.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
70
826
        d_qstate, d_qreg, d_treg, "FirstOrderModelFmc"));
71
  }
72
  else
73
  {
74
16342
    d_qmodel.reset(new quantifiers::FirstOrderModel(
75
8171
        d_qstate, d_qreg, d_treg, "FirstOrderModel"));
76
  }
77
78
17994
  d_qim.reset(new QuantifiersInferenceManager(
79
8997
      *this, d_qstate, d_qreg, d_treg, d_qmodel.get(), pnm));
80
81
  // Finish initializing the term registry by hooking it up to the inference
82
  // manager. This is required due to a cyclic dependency between the term
83
  // database and the instantiate module. Term database needs inference manager
84
  // since it sends out lemmas when term indexing is inconsistent, instantiate
85
  // needs term database for entailment checks.
86
8997
  d_treg.finishInit(d_qim.get());
87
88
  // construct the quantifiers engine
89
17994
  d_qengine.reset(new QuantifiersEngine(
90
8997
      d_qstate, d_qreg, d_treg, *d_qim.get(), d_qmodel.get(), pnm));
91
92
  //!!!!!!!!!!!!!! temporary (project #15)
93
8997
  d_qmodel->finishInit(d_qengine.get());
94
95
  // indicate we are using the quantifiers theory state object
96
8997
  d_theoryState = &d_qstate;
97
  // use the inference manager as the official inference manager
98
8997
  d_inferManager = d_qim.get();
99
  // Set the pointer to the quantifiers engine, which this theory owns. This
100
  // pointer will be retreived by TheoryEngine and set to all theories
101
  // post-construction.
102
8997
  d_quantEngine = d_qengine.get();
103
8997
}
104
105
17988
TheoryQuantifiers::~TheoryQuantifiers() {
106
17988
}
107
108
8997
TheoryRewriter* TheoryQuantifiers::getTheoryRewriter() { return &d_rewriter; }
109
8997
void TheoryQuantifiers::finishInit()
110
{
111
  // quantifiers are not evaluated in getModelValue
112
8997
  d_valuation.setUnevaluatedKind(EXISTS);
113
8997
  d_valuation.setUnevaluatedKind(FORALL);
114
  // witness is used in several instantiation strategies
115
8997
  d_valuation.setUnevaluatedKind(WITNESS);
116
8997
}
117
118
8997
bool TheoryQuantifiers::needsEqualityEngine(EeSetupInfo& esi)
119
{
120
  // use the master equality engine
121
8997
  esi.d_useMaster = true;
122
8997
  return true;
123
}
124
125
27726
void TheoryQuantifiers::preRegisterTerm(TNode n)
126
{
127
27726
  if (n.getKind() != FORALL)
128
  {
129
    return;
130
  }
131
55452
  Debug("quantifiers-prereg")
132
27726
      << "TheoryQuantifiers::preRegisterTerm() " << n << std::endl;
133
  // Preregister the quantified formula.
134
  // This initializes the modules used for handling n in this user context.
135
27727
  getQuantifiersEngine()->preRegisterQuantifier(n);
136
55450
  Debug("quantifiers-prereg")
137
27725
      << "TheoryQuantifiers::preRegisterTerm() done " << n << std::endl;
138
}
139
140
141
12418
void TheoryQuantifiers::presolve() {
142
12418
  Debug("quantifiers-presolve") << "TheoryQuantifiers::presolve()" << std::endl;
143
12418
  if( getQuantifiersEngine() ){
144
6440
    getQuantifiersEngine()->presolve();
145
  }
146
12418
}
147
148
10350
void TheoryQuantifiers::ppNotifyAssertions(
149
    const std::vector<Node>& assertions) {
150
20700
  Trace("quantifiers-presolve")
151
10350
      << "TheoryQuantifiers::ppNotifyAssertions" << std::endl;
152
10350
  if (getQuantifiersEngine()) {
153
5909
    getQuantifiersEngine()->ppNotifyAssertions(assertions);
154
  }
155
10350
}
156
157
15465
bool TheoryQuantifiers::collectModelValues(TheoryModel* m,
158
                                           const std::set<Node>& termSet)
159
{
160
49463
  for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
161
33998
    if ((*i).d_assertion.getKind() == NOT)
162
    {
163
11268
      Debug("quantifiers::collectModelInfo")
164
5634
          << "got quant FALSE: " << (*i).d_assertion[0] << std::endl;
165
5634
      if (!m->assertPredicate((*i).d_assertion[0], false))
166
      {
167
        return false;
168
      }
169
    }
170
    else
171
    {
172
56728
      Debug("quantifiers::collectModelInfo")
173
28364
          << "got quant TRUE : " << *i << std::endl;
174
28364
      if (!m->assertPredicate(*i, true))
175
      {
176
        return false;
177
      }
178
    }
179
  }
180
15465
  return true;
181
}
182
183
69420
void TheoryQuantifiers::postCheck(Effort level)
184
{
185
  // call the quantifiers engine to check
186
69420
  getQuantifiersEngine()->check(level);
187
69420
}
188
189
67818
bool TheoryQuantifiers::preNotifyFact(
190
    TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal)
191
{
192
67818
  Kind k = atom.getKind();
193
67818
  if (k == FORALL)
194
  {
195
67818
    getQuantifiersEngine()->assertQuantifier(atom, polarity);
196
  }
197
  else
198
  {
199
    Unhandled() << "Unexpected fact " << fact;
200
  }
201
  // don't use equality engine, always return true
202
67818
  return true;
203
}
204
205
109
void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value){
206
109
  QuantAttributes::setUserAttribute( attr, n, node_values, str_value );
207
109
}
208
209
}  // namespace quantifiers
210
}  // namespace theory
211
26685
}  // namespace CVC4