GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/smt_engine_subsolver.cpp Lines: 39 48 81.3 %
Date: 2021-03-23 Branches: 45 132 34.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file smt_engine_subsolver.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, 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 utilities for initializing subsolvers (copies of
13
 ** SmtEngine) during solving.
14
 **/
15
16
#include "theory/smt_engine_subsolver.h"
17
18
#include "api/cvc4cpp.h"
19
#include "smt/smt_engine.h"
20
#include "smt/smt_engine_scope.h"
21
#include "theory/rewriter.h"
22
23
namespace CVC4 {
24
namespace theory {
25
26
// optimization: try to rewrite to constant
27
1200
Result quickCheck(Node& query)
28
{
29
1200
  query = theory::Rewriter::rewrite(query);
30
1200
  if (query.isConst())
31
  {
32
400
    if (!query.getConst<bool>())
33
    {
34
56
      return Result(Result::UNSAT);
35
    }
36
    else
37
    {
38
344
      return Result(Result::SAT);
39
    }
40
  }
41
800
  return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK);
42
}
43
44
2566
void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
45
                         bool needsTimeout,
46
                         unsigned long timeout)
47
{
48
2566
  NodeManager* nm = NodeManager::currentNM();
49
2566
  SmtEngine* smtCurr = smt::currentSmtEngine();
50
  // must copy the options
51
2566
  smte.reset(new SmtEngine(nm, &smtCurr->getOptions()));
52
2566
  smte->setIsInternalSubsolver();
53
2566
  smte->setLogic(smtCurr->getLogicInfo());
54
  // set the options
55
2566
  if (needsTimeout)
56
  {
57
    smte->setTimeLimit(timeout);
58
  }
59
2566
}
60
61
Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
62
                          Node query,
63
                          bool needsTimeout,
64
                          unsigned long timeout)
65
{
66
  Assert(query.getType().isBoolean());
67
  Result r = quickCheck(query);
68
  if (!r.isUnknown())
69
  {
70
    return r;
71
  }
72
  initializeSubsolver(smte, needsTimeout, timeout);
73
  smte->assertFormula(query);
74
  return smte->checkSat();
75
}
76
77
296
Result checkWithSubsolver(Node query, bool needsTimeout, unsigned long timeout)
78
{
79
592
  std::vector<Node> vars;
80
592
  std::vector<Node> modelVals;
81
592
  return checkWithSubsolver(query, vars, modelVals, needsTimeout, timeout);
82
}
83
84
1200
Result checkWithSubsolver(Node query,
85
                          const std::vector<Node>& vars,
86
                          std::vector<Node>& modelVals,
87
                          bool needsTimeout,
88
                          unsigned long timeout)
89
{
90
1200
  Assert(query.getType().isBoolean());
91
1200
  Assert(modelVals.empty());
92
  // ensure clear
93
1200
  modelVals.clear();
94
1200
  Result r = quickCheck(query);
95
1200
  if (!r.isUnknown())
96
  {
97
400
    if (r.asSatisfiabilityResult().isSat() == Result::SAT)
98
    {
99
      // default model
100
360
      for (const Node& v : vars)
101
      {
102
16
        modelVals.push_back(v.getType().mkGroundTerm());
103
      }
104
    }
105
400
    return r;
106
  }
107
1600
  std::unique_ptr<SmtEngine> smte;
108
800
  initializeSubsolver(smte, needsTimeout, timeout);
109
800
  smte->assertFormula(query);
110
800
  r = smte->checkSat();
111
800
  if (r.asSatisfiabilityResult().isSat() == Result::SAT)
112
  {
113
3643
    for (const Node& v : vars)
114
    {
115
6308
      Node val = smte->getValue(v);
116
3154
      modelVals.push_back(val);
117
    }
118
  }
119
800
  return r;
120
}
121
122
}  // namespace theory
123
26685
}  // namespace CVC4