GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/strings_fmf.cpp Lines: 40 43 93.0 %
Date: 2021-03-22 Branches: 48 90 53.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file strings_fmf.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tianyi Liang
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 a finite model finding decision strategy for
13
 ** strings.
14
 **/
15
16
#include "theory/strings/strings_fmf.h"
17
18
using namespace std;
19
using namespace CVC4::context;
20
using namespace CVC4::kind;
21
22
namespace CVC4 {
23
namespace theory {
24
namespace strings {
25
26
8995
StringsFmf::StringsFmf(context::Context* c,
27
                       context::UserContext* u,
28
                       Valuation valuation,
29
8995
                       TermRegistry& tr)
30
    : d_sslds(nullptr),
31
      d_satContext(c),
32
      d_userContext(u),
33
      d_valuation(valuation),
34
8995
      d_termReg(tr)
35
{
36
8995
}
37
38
8992
StringsFmf::~StringsFmf() {}
39
40
61
void StringsFmf::presolve()
41
{
42
122
  d_sslds.reset(new StringSumLengthDecisionStrategy(
43
122
      d_satContext, d_userContext, d_valuation));
44
122
  Trace("strings-dstrat-reg")
45
61
      << "presolve: register decision strategy." << std::endl;
46
61
  const NodeSet& ivars = d_termReg.getInputVars();
47
122
  std::vector<Node> inputVars;
48
187
  for (NodeSet::const_iterator itr = ivars.begin(); itr != ivars.end(); ++itr)
49
  {
50
126
    inputVars.push_back(*itr);
51
  }
52
61
  d_sslds->initialize(inputVars);
53
61
}
54
55
61
DecisionStrategy* StringsFmf::getDecisionStrategy() const
56
{
57
61
  return d_sslds.get();
58
}
59
60
61
StringsFmf::StringSumLengthDecisionStrategy::StringSumLengthDecisionStrategy(
61
61
    context::Context* c, context::UserContext* u, Valuation valuation)
62
61
    : DecisionStrategyFmf(c, valuation), d_inputVarLsum(u)
63
{
64
61
}
65
66
bool StringsFmf::StringSumLengthDecisionStrategy::isInitialized()
67
{
68
  return !d_inputVarLsum.get().isNull();
69
}
70
71
61
void StringsFmf::StringSumLengthDecisionStrategy::initialize(
72
    const std::vector<Node>& vars)
73
{
74
61
  if (d_inputVarLsum.get().isNull() && !vars.empty())
75
  {
76
56
    NodeManager* nm = NodeManager::currentNM();
77
112
    std::vector<Node> sum;
78
182
    for (const Node& v : vars)
79
    {
80
126
      sum.push_back(nm->mkNode(STRING_LENGTH, v));
81
    }
82
112
    Node sumn = sum.size() == 1 ? sum[0] : nm->mkNode(PLUS, sum);
83
56
    d_inputVarLsum.set(sumn);
84
  }
85
61
}
86
87
270
Node StringsFmf::StringSumLengthDecisionStrategy::mkLiteral(unsigned i)
88
{
89
270
  if (d_inputVarLsum.get().isNull())
90
  {
91
    return Node::null();
92
  }
93
270
  NodeManager* nm = NodeManager::currentNM();
94
540
  Node lit = nm->mkNode(LEQ, d_inputVarLsum.get(), nm->mkConst(Rational(i)));
95
270
  Trace("strings-fmf") << "StringsFMF::mkLiteral: " << lit << std::endl;
96
270
  return lit;
97
}
98
63147
std::string StringsFmf::StringSumLengthDecisionStrategy::identify() const
99
{
100
63147
  return std::string("string_sum_len");
101
}
102
103
}  // namespace strings
104
}  // namespace theory
105
26676
}  // namespace CVC4