GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/theory_quantifiers.cpp Lines: 81 85 95.3 %
Date: 2021-03-22 Branches: 110 212 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
8995
TheoryQuantifiers::TheoryQuantifiers(Context* c,
35
                                     context::UserContext* u,
36
                                     OutputChannel& out,
37
                                     Valuation valuation,
38
                                     const LogicInfo& logicInfo,
39
8995
                                     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
8995
      d_qim(*this, d_qstate, pnm)
45
{
46
  // Finish initializing the term registry by hooking it up to the inference
47
  // manager. This is required due to a cyclic dependency between the term
48
  // database and the instantiate module. Term database needs inference manager
49
  // since it sends out lemmas when term indexing is inconsistent, instantiate
50
  // needs term database for entailment checks.
51
8995
  d_treg.finishInit(&d_qim);
52
53
8995
  out.handleUserAttribute( "fun-def", this );
54
8995
  out.handleUserAttribute("qid", this);
55
8995
  out.handleUserAttribute( "quant-inst-max-level", this );
56
8995
  out.handleUserAttribute( "quant-elim", this );
57
8995
  out.handleUserAttribute( "quant-elim-partial", this );
58
59
8995
  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
60
8995
  if (pc != nullptr)
61
  {
62
    // add the proof rules
63
962
    d_qChecker.registerTo(pc);
64
  }
65
  // indicate we are using the quantifiers theory state object
66
8995
  d_theoryState = &d_qstate;
67
  // use the inference manager as the official inference manager
68
8995
  d_inferManager = &d_qim;
69
70
8995
  Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
71
17990
  Trace("quant-engine-debug")
72
8995
      << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
73
  // Finite model finding requires specialized ways of building the model.
74
  // We require constructing the model here, since it is required for
75
  // initializing the CombinationEngine and the rest of quantifiers engine.
76
8995
  if (options::finiteModelFind() || options::fmfBound())
77
  {
78
838
    if (QuantifiersModules::useFmcModel())
79
    {
80
1648
      d_qmodel.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
81
824
          d_qstate, d_qreg, d_treg, "FirstOrderModelFmc"));
82
    }
83
    else
84
    {
85
28
      d_qmodel.reset(new quantifiers::FirstOrderModel(
86
14
          d_qstate, d_qreg, d_treg, "FirstOrderModel"));
87
    }
88
  }
89
  else
90
  {
91
16314
    d_qmodel.reset(new quantifiers::FirstOrderModel(
92
8157
        d_qstate, d_qreg, d_treg, "FirstOrderModel"));
93
  }
94
95
  // construct the quantifiers engine
96
17990
  d_qengine.reset(new QuantifiersEngine(
97
8995
      d_qstate, d_qreg, d_treg, d_qim, d_qmodel.get(), pnm));
98
99
  //!!!!!!!!!!!!!! temporary (project #15)
100
8995
  d_qmodel->finishInit(d_qengine.get());
101
102
  // Set the pointer to the quantifiers engine, which this theory owns. This
103
  // pointer will be retreived by TheoryEngine and set to all theories
104
  // post-construction.
105
8995
  d_quantEngine = d_qengine.get();
106
8995
}
107
108
17984
TheoryQuantifiers::~TheoryQuantifiers() {
109
17984
}
110
111
8995
TheoryRewriter* TheoryQuantifiers::getTheoryRewriter() { return &d_rewriter; }
112
8995
void TheoryQuantifiers::finishInit()
113
{
114
  // quantifiers are not evaluated in getModelValue
115
8995
  d_valuation.setUnevaluatedKind(EXISTS);
116
8995
  d_valuation.setUnevaluatedKind(FORALL);
117
  // witness is used in several instantiation strategies
118
8995
  d_valuation.setUnevaluatedKind(WITNESS);
119
8995
}
120
121
8995
bool TheoryQuantifiers::needsEqualityEngine(EeSetupInfo& esi)
122
{
123
  // use the master equality engine
124
8995
  esi.d_useMaster = true;
125
8995
  return true;
126
}
127
128
27722
void TheoryQuantifiers::preRegisterTerm(TNode n)
129
{
130
27722
  if (n.getKind() != FORALL)
131
  {
132
    return;
133
  }
134
55444
  Debug("quantifiers-prereg")
135
27722
      << "TheoryQuantifiers::preRegisterTerm() " << n << std::endl;
136
  // Preregister the quantified formula.
137
  // This initializes the modules used for handling n in this user context.
138
27723
  getQuantifiersEngine()->preRegisterQuantifier(n);
139
55442
  Debug("quantifiers-prereg")
140
27721
      << "TheoryQuantifiers::preRegisterTerm() done " << n << std::endl;
141
}
142
143
144
12416
void TheoryQuantifiers::presolve() {
145
12416
  Debug("quantifiers-presolve") << "TheoryQuantifiers::presolve()" << std::endl;
146
12416
  if( getQuantifiersEngine() ){
147
6438
    getQuantifiersEngine()->presolve();
148
  }
149
12416
}
150
151
10348
void TheoryQuantifiers::ppNotifyAssertions(
152
    const std::vector<Node>& assertions) {
153
20696
  Trace("quantifiers-presolve")
154
10348
      << "TheoryQuantifiers::ppNotifyAssertions" << std::endl;
155
10348
  if (getQuantifiersEngine()) {
156
5907
    getQuantifiersEngine()->ppNotifyAssertions(assertions);
157
  }
158
10348
}
159
160
15457
bool TheoryQuantifiers::collectModelValues(TheoryModel* m,
161
                                           const std::set<Node>& termSet)
162
{
163
49447
  for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
164
33990
    if ((*i).d_assertion.getKind() == NOT)
165
    {
166
11268
      Debug("quantifiers::collectModelInfo")
167
5634
          << "got quant FALSE: " << (*i).d_assertion[0] << std::endl;
168
5634
      if (!m->assertPredicate((*i).d_assertion[0], false))
169
      {
170
        return false;
171
      }
172
    }
173
    else
174
    {
175
56712
      Debug("quantifiers::collectModelInfo")
176
28356
          << "got quant TRUE : " << *i << std::endl;
177
28356
      if (!m->assertPredicate(*i, true))
178
      {
179
        return false;
180
      }
181
    }
182
  }
183
15457
  return true;
184
}
185
186
69390
void TheoryQuantifiers::postCheck(Effort level)
187
{
188
  // call the quantifiers engine to check
189
69390
  getQuantifiersEngine()->check(level);
190
69390
}
191
192
67814
bool TheoryQuantifiers::preNotifyFact(
193
    TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal)
194
{
195
67814
  Kind k = atom.getKind();
196
67814
  if (k == FORALL)
197
  {
198
67814
    getQuantifiersEngine()->assertQuantifier(atom, polarity);
199
  }
200
  else
201
  {
202
    Unhandled() << "Unexpected fact " << fact;
203
  }
204
  // don't use equality engine, always return true
205
67814
  return true;
206
}
207
208
109
void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value){
209
109
  QuantAttributes::setUserAttribute( attr, n, node_values, str_value );
210
109
}
211
212
}  // namespace quantifiers
213
}  // namespace theory
214
26676
}  // namespace CVC4