GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/abduction_solver.cpp Lines: 83 99 83.8 %
Date: 2021-03-22 Branches: 163 438 37.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file abduction_solver.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Mathias Preiner
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 abduction queries
13
 **/
14
15
#include "smt/abduction_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_abduct.h"
23
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
24
#include "theory/smt_engine_subsolver.h"
25
26
using namespace CVC4::theory;
27
28
namespace CVC4 {
29
namespace smt {
30
31
596
AbductionSolver::AbductionSolver(SmtEngine* parent) : d_parent(parent) {}
32
33
596
AbductionSolver::~AbductionSolver() {}
34
22
bool AbductionSolver::getAbduct(const Node& goal,
35
                                const TypeNode& grammarType,
36
                                Node& abd)
37
{
38
24219
  if (!options::produceAbducts())
39
  {
40
    const char* msg = "Cannot get abduct when produce-abducts options is off.";
41
    throw ModalException(msg);
42
  }
43
22
  Trace("sygus-abduct") << "SmtEngine::getAbduct: goal " << goal << std::endl;
44
44
  std::vector<Node> axioms = d_parent->getExpandedAssertions();
45
44
  std::vector<Node> asserts(axioms.begin(), axioms.end());
46
  // must expand definitions
47
44
  Node conjn = d_parent->expandDefinitions(goal);
48
  // now negate
49
22
  conjn = conjn.negate();
50
22
  d_abdConj = conjn;
51
22
  asserts.push_back(conjn);
52
44
  std::string name("A");
53
  Node aconj = quantifiers::SygusAbduct::mkAbductionConjecture(
54
44
      name, asserts, axioms, grammarType);
55
  // should be a quantified conjecture with one function-to-synthesize
56
22
  Assert(aconj.getKind() == kind::FORALL && aconj[0].getNumChildren() == 1);
57
  // remember the abduct-to-synthesize
58
22
  d_sssf = aconj[0][0];
59
44
  Trace("sygus-abduct") << "SmtEngine::getAbduct: made conjecture : " << aconj
60
22
                        << ", solving for " << d_sssf << std::endl;
61
  // we generate a new smt engine to do the abduction query
62
22
  initializeSubsolver(d_subsolver);
63
  // get the logic
64
44
  LogicInfo l = d_subsolver->getLogicInfo().getUnlockedCopy();
65
  // enable everything needed for sygus
66
22
  l.enableSygus();
67
22
  d_subsolver->setLogic(l);
68
  // assert the abduction query
69
22
  d_subsolver->assertFormula(aconj);
70
40
  return getAbductInternal(abd);
71
}
72
73
bool AbductionSolver::getAbduct(const Node& goal, Node& abd)
74
{
75
  TypeNode grammarType;
76
  return getAbduct(goal, grammarType, abd);
77
}
78
79
22
bool AbductionSolver::getAbductInternal(Node& abd)
80
{
81
  // should have initialized the subsolver by now
82
22
  Assert(d_subsolver != nullptr);
83
22
  Trace("sygus-abduct") << "  SmtEngine::getAbduct check sat..." << std::endl;
84
40
  Result r = d_subsolver->checkSat();
85
18
  Trace("sygus-abduct") << "  SmtEngine::getAbduct result: " << r << std::endl;
86
18
  if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
87
  {
88
    // get the synthesis solution
89
36
    std::map<Node, Node> sols;
90
18
    d_subsolver->getSynthSolutions(sols);
91
18
    Assert(sols.size() == 1);
92
18
    std::map<Node, Node>::iterator its = sols.find(d_sssf);
93
18
    if (its != sols.end())
94
    {
95
36
      Trace("sygus-abduct")
96
18
          << "SmtEngine::getAbduct: solution is " << its->second << std::endl;
97
18
      abd = its->second;
98
18
      if (abd.getKind() == kind::LAMBDA)
99
      {
100
18
        abd = abd[1];
101
      }
102
      // get the grammar type for the abduct
103
36
      Node agdtbv = d_sssf.getAttribute(SygusSynthFunVarListAttribute());
104
18
      Assert(!agdtbv.isNull());
105
18
      Assert(agdtbv.getKind() == kind::BOUND_VAR_LIST);
106
      // convert back to original
107
      // must replace formal arguments of abd with the free variables in the
108
      // input problem that they correspond to.
109
36
      std::vector<Node> vars;
110
36
      std::vector<Node> syms;
111
      SygusVarToTermAttribute sta;
112
132
      for (const Node& bv : agdtbv)
113
      {
114
114
        vars.push_back(bv);
115
114
        syms.push_back(bv.hasAttribute(sta) ? bv.getAttribute(sta) : bv);
116
      }
117
18
      abd = abd.substitute(vars.begin(), vars.end(), syms.begin(), syms.end());
118
119
      // if check abducts option is set, we check the correctness
120
60
      if (options::checkAbducts())
121
      {
122
9
        checkAbduct(abd);
123
      }
124
18
      return true;
125
    }
126
    Trace("sygus-abduct") << "SmtEngine::getAbduct: could not find solution!"
127
                          << std::endl;
128
    throw RecoverableModalException("Could not find solution for get-abduct.");
129
  }
130
  return false;
131
}
132
133
9
void AbductionSolver::checkAbduct(Node a)
134
{
135
9
  Assert(a.getType().isBoolean());
136
18
  Trace("check-abduct") << "SmtEngine::checkAbduct: get expanded assertions"
137
9
                        << std::endl;
138
139
18
  std::vector<Node> asserts = d_parent->getExpandedAssertions();
140
9
  asserts.push_back(a);
141
142
  // two checks: first, consistent with assertions, second, implies negated goal
143
  // is unsatisfiable.
144
27
  for (unsigned j = 0; j < 2; j++)
145
  {
146
36
    Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
147
18
                          << ": make new SMT engine" << std::endl;
148
    // Start new SMT engine to check solution
149
36
    std::unique_ptr<SmtEngine> abdChecker;
150
18
    initializeSubsolver(abdChecker);
151
36
    Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
152
18
                          << ": asserting formulas" << std::endl;
153
173
    for (const Node& e : asserts)
154
    {
155
155
      abdChecker->assertFormula(e);
156
    }
157
36
    Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
158
18
                          << ": check the assertions" << std::endl;
159
36
    Result r = abdChecker->checkSat();
160
36
    Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
161
18
                          << ": result is " << r << std::endl;
162
36
    std::stringstream serr;
163
18
    bool isError = false;
164
18
    if (j == 0)
165
    {
166
9
      if (r.asSatisfiabilityResult().isSat() != Result::SAT)
167
      {
168
        isError = true;
169
        serr << "SmtEngine::checkAbduct(): produced solution cannot be shown "
170
                "to be consisconsistenttent with assertions, result was "
171
             << r;
172
      }
173
18
      Trace("check-abduct")
174
9
          << "SmtEngine::checkAbduct: goal is " << d_abdConj << std::endl;
175
      // add the goal to the set of assertions
176
9
      Assert(!d_abdConj.isNull());
177
9
      asserts.push_back(d_abdConj);
178
    }
179
    else
180
    {
181
9
      if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
182
      {
183
        isError = true;
184
        serr << "SmtEngine::checkAbduct(): negated goal cannot be shown "
185
                "unsatisfiable with produced solution, result was "
186
             << r;
187
      }
188
    }
189
    // did we get an unexpected result?
190
18
    if (isError)
191
    {
192
      InternalError() << serr.str();
193
    }
194
  }
195
9
}
196
197
}  // namespace smt
198
50915
}  // namespace CVC4