GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/cad_solver.cpp Lines: 10 30 33.3 %
Date: 2021-03-23 Branches: 9 44 20.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cad_solver.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Gereon Kremer
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 new non-linear solver
13
 **/
14
15
#include "theory/arith/nl/cad_solver.h"
16
17
#include "theory/inference_id.h"
18
#include "theory/arith/inference_manager.h"
19
#include "theory/arith/nl/cad/cdcac.h"
20
#include "theory/arith/nl/nl_model.h"
21
#include "theory/arith/nl/poly_conversion.h"
22
23
namespace CVC4 {
24
namespace theory {
25
namespace arith {
26
namespace nl {
27
28
4391
CadSolver::CadSolver(InferenceManager& im,
29
                     NlModel& model,
30
                     context::Context* ctx,
31
4391
                     ProofNodeManager* pnm)
32
    :
33
#ifdef CVC4_POLY_IMP
34
      d_CAC(ctx, pnm),
35
#endif
36
      d_foundSatisfiability(false),
37
      d_im(im),
38
4391
      d_model(model)
39
{
40
4391
  d_ranVariable =
41
17564
      NodeManager::currentNM()->mkSkolem("__z",
42
8782
                                         NodeManager::currentNM()->realType(),
43
                                         "",
44
4391
                                         NodeManager::SKOLEM_EXACT_NAME);
45
#ifdef CVC4_POLY_IMP
46
  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
47
  if (pc != nullptr)
48
  {
49
    // add checkers
50
    d_proofChecker.registerTo(pc);
51
  }
52
#endif
53
4391
}
54
55
4388
CadSolver::~CadSolver() {}
56
57
void CadSolver::initLastCall(const std::vector<Node>& assertions)
58
{
59
#ifdef CVC4_POLY_IMP
60
  if (Trace.isOn("nl-cad"))
61
  {
62
    Trace("nl-cad") << "CadSolver::initLastCall" << std::endl;
63
    Trace("nl-cad") << "* Assertions: " << std::endl;
64
    for (const Node& a : assertions)
65
    {
66
      Trace("nl-cad") << "  " << a << std::endl;
67
    }
68
  }
69
  // store or process assertions
70
  d_CAC.reset();
71
  for (const Node& a : assertions)
72
  {
73
    d_CAC.getConstraints().addConstraint(a);
74
  }
75
  d_CAC.computeVariableOrdering();
76
  d_CAC.retrieveInitialAssignment(d_model, d_ranVariable);
77
#else
78
  Warning() << "Tried to use CadSolver but libpoly is not available. Compile "
79
               "with --poly."
80
            << std::endl;
81
#endif
82
}
83
84
void CadSolver::checkFull()
85
{
86
#ifdef CVC4_POLY_IMP
87
  if (d_CAC.getConstraints().getConstraints().empty()) {
88
    Trace("nl-cad") << "No constraints. Return." << std::endl;
89
    return;
90
  }
91
  d_CAC.startNewProof();
92
  auto covering = d_CAC.getUnsatCover();
93
  if (covering.empty())
94
  {
95
    d_foundSatisfiability = true;
96
    Trace("nl-cad") << "SAT: " << d_CAC.getModel() << std::endl;
97
  }
98
  else
99
  {
100
    d_foundSatisfiability = false;
101
    auto mis = collectConstraints(covering);
102
    Trace("nl-cad") << "Collected MIS: " << mis << std::endl;
103
    Assert(!mis.empty()) << "Infeasible subset can not be empty";
104
    Trace("nl-cad") << "UNSAT with MIS: " << mis << std::endl;
105
    Node lem = NodeManager::currentNM()->mkAnd(mis).negate();
106
    ProofGenerator* proof = d_CAC.closeProof(mis);
107
    d_im.addPendingLemma(lem, InferenceId::ARITH_NL_CAD_CONFLICT, proof);
108
  }
109
#else
110
  Warning() << "Tried to use CadSolver but libpoly is not available. Compile "
111
               "with --poly."
112
            << std::endl;
113
#endif
114
}
115
116
void CadSolver::checkPartial()
117
{
118
#ifdef CVC4_POLY_IMP
119
  if (d_CAC.getConstraints().getConstraints().empty()) {
120
    Trace("nl-cad") << "No constraints. Return." << std::endl;
121
    return;
122
  }
123
  auto covering = d_CAC.getUnsatCover(0, true);
124
  if (covering.empty())
125
  {
126
    d_foundSatisfiability = true;
127
    Trace("nl-cad") << "SAT: " << d_CAC.getModel() << std::endl;
128
  }
129
  else
130
  {
131
    auto* nm = NodeManager::currentNM();
132
    Node first_var =
133
        d_CAC.getConstraints().varMapper()(d_CAC.getVariableOrdering()[0]);
134
    for (const auto& interval : covering)
135
    {
136
      Node premise;
137
      Assert(!interval.d_origins.empty());
138
      if (interval.d_origins.size() == 1)
139
      {
140
        premise = interval.d_origins[0];
141
      }
142
      else
143
      {
144
        premise = nm->mkNode(Kind::AND, interval.d_origins);
145
      }
146
      Node conclusion =
147
          excluding_interval_to_lemma(first_var, interval.d_interval, false);
148
      if (!conclusion.isNull())
149
      {
150
        Node lemma = nm->mkNode(Kind::IMPLIES, premise, conclusion);
151
        Trace("nl-cad") << "Excluding " << first_var << " -> "
152
                        << interval.d_interval << " using " << lemma
153
                        << std::endl;
154
        d_im.addPendingLemma(lemma,
155
                             InferenceId::ARITH_NL_CAD_EXCLUDED_INTERVAL);
156
      }
157
    }
158
  }
159
#else
160
  Warning() << "Tried to use CadSolver but libpoly is not available. Compile "
161
               "with --poly."
162
            << std::endl;
163
#endif
164
}
165
166
bool CadSolver::constructModelIfAvailable(std::vector<Node>& assertions)
167
{
168
#ifdef CVC4_POLY_IMP
169
  if (!d_foundSatisfiability)
170
  {
171
    return false;
172
  }
173
  bool foundNonVariable = false;
174
  for (const auto& v : d_CAC.getVariableOrdering())
175
  {
176
    Node variable = d_CAC.getConstraints().varMapper()(v);
177
    if (!variable.isVar())
178
    {
179
      Trace("nl-cad") << "Not a variable: " << variable << std::endl;
180
      foundNonVariable = true;
181
    }
182
    Node value = value_to_node(d_CAC.getModel().get(v), d_ranVariable);
183
    if (value.isConst())
184
    {
185
      d_model.addCheckModelSubstitution(variable, value);
186
    }
187
    else
188
    {
189
      d_model.addCheckModelWitness(variable, value);
190
    }
191
    Trace("nl-cad") << "-> " << v << " = " << value << std::endl;
192
  }
193
  if (foundNonVariable)
194
  {
195
    Trace("nl-cad")
196
        << "Some variable was an extended term, don't clear list of assertions."
197
        << std::endl;
198
    return false;
199
  }
200
  Trace("nl-cad") << "Constructed a full assignment, clear list of assertions."
201
                  << std::endl;
202
  assertions.clear();
203
  return true;
204
#else
205
  Warning() << "Tried to use CadSolver but libpoly is not available. Compile "
206
               "with --poly."
207
            << std::endl;
208
  return false;
209
#endif
210
}
211
212
}  // namespace nl
213
}  // namespace arith
214
}  // namespace theory
215
26685
}  // namespace CVC4