GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/interpolation_solver.cpp Lines: 46 58 79.3 %
Date: 2021-03-23 Branches: 83 210 39.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file interpolation_solver.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Ying Sheng, Andrew Reynolds, Abdalrhman Mohamed
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 The solver for interpolation queries
13
 **/
14
15
#include "smt/interpolation_solver.h"
16
17
#include <sstream>
18
19
#include "options/smt_options.h"
20
#include "smt/smt_engine.h"
21
#include "theory/quantifiers/quantifiers_attributes.h"
22
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
23
#include "theory/quantifiers/sygus/sygus_interpol.h"
24
#include "theory/smt_engine_subsolver.h"
25
26
using namespace CVC4::theory;
27
28
namespace CVC4 {
29
namespace smt {
30
31
73
InterpolationSolver::InterpolationSolver(SmtEngine* parent) : d_parent(parent)
32
{
33
73
}
34
35
73
InterpolationSolver::~InterpolationSolver() {}
36
37
10
bool InterpolationSolver::getInterpol(const Node& conj,
38
                                      const TypeNode& grammarType,
39
                                      Node& interpol)
40
{
41
22259
  if (options::produceInterpols() == options::ProduceInterpols::NONE)
42
  {
43
    const char* msg =
44
        "Cannot get interpolation when produce-interpol options is off.";
45
    throw ModalException(msg);
46
  }
47
20
  Trace("sygus-interpol") << "SmtEngine::getInterpol: conjecture " << conj
48
10
                          << std::endl;
49
20
  std::vector<Node> axioms = d_parent->getExpandedAssertions();
50
  // must expand definitions
51
20
  Node conjn = d_parent->expandDefinitions(conj);
52
20
  std::string name("A");
53
54
20
  quantifiers::SygusInterpol interpolSolver;
55
10
  if (interpolSolver.solveInterpolation(
56
          name, axioms, conjn, grammarType, interpol))
57
  {
58
36
    if (options::checkInterpols())
59
    {
60
8
      checkInterpol(interpol, axioms, conj);
61
    }
62
10
    return true;
63
  }
64
  return false;
65
}
66
67
bool InterpolationSolver::getInterpol(const Node& conj, Node& interpol)
68
{
69
  TypeNode grammarType;
70
  return getInterpol(conj, grammarType, interpol);
71
}
72
73
8
void InterpolationSolver::checkInterpol(Node interpol,
74
                                        const std::vector<Node>& easserts,
75
                                        const Node& conj)
76
{
77
8
  Assert(interpol.getType().isBoolean());
78
16
  Trace("check-interpol") << "SmtEngine::checkInterpol: get expanded assertions"
79
8
                          << std::endl;
80
81
  // two checks: first, axioms imply interpol, second, interpol implies conj.
82
24
  for (unsigned j = 0; j < 2; j++)
83
  {
84
16
    if (j == 1)
85
    {
86
16
      Trace("check-interpol")
87
8
          << "SmtEngine::checkInterpol: conjecture is " << conj << std::endl;
88
    }
89
32
    Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
90
16
                            << ": make new SMT engine" << std::endl;
91
    // Start new SMT engine to check solution
92
32
    std::unique_ptr<SmtEngine> itpChecker;
93
16
    initializeSubsolver(itpChecker);
94
32
    Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
95
16
                            << ": asserting formulas" << std::endl;
96
16
    if (j == 0)
97
    {
98
19
      for (const Node& e : easserts)
99
      {
100
11
        itpChecker->assertFormula(e);
101
      }
102
16
      Node negitp = interpol.notNode();
103
8
      itpChecker->assertFormula(negitp);
104
    }
105
    else
106
    {
107
8
      itpChecker->assertFormula(interpol);
108
8
      Assert(!conj.isNull());
109
8
      itpChecker->assertFormula(conj.notNode());
110
    }
111
32
    Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
112
16
                            << ": check the assertions" << std::endl;
113
32
    Result r = itpChecker->checkSat();
114
32
    Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
115
16
                            << ": result is " << r << std::endl;
116
32
    std::stringstream serr;
117
16
    if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
118
    {
119
      if (j == 0)
120
      {
121
        serr << "SmtEngine::checkInterpol(): negated produced solution cannot "
122
                "be shown "
123
                "satisfiable with assertions, result was "
124
             << r;
125
      }
126
      else
127
      {
128
        serr
129
            << "SmtEngine::checkInterpol(): negated conjecture cannot be shown "
130
               "satisfiable with produced solution, result was "
131
            << r;
132
      }
133
      InternalError() << serr.str();
134
    }
135
  }
136
8
}
137
138
}  // namespace smt
139
48960
}  // namespace CVC4