GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/strings_fmf.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file strings_fmf.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, 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 A finite model finding decision strategy for strings.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__STRINGS__STRINGS_FMF_H
18
#define CVC4__THEORY__STRINGS__STRINGS_FMF_H
19
20
#include "context/cdhashset.h"
21
#include "context/cdo.h"
22
#include "context/context.h"
23
#include "expr/node.h"
24
#include "theory/decision_strategy.h"
25
#include "theory/strings/term_registry.h"
26
#include "theory/valuation.h"
27
28
namespace CVC4 {
29
namespace theory {
30
namespace strings {
31
32
/** Strings finite model finding
33
 *
34
 * This class manages the creation of a decision strategy that bounds the
35
 * sum of lengths of terms of type string.
36
 */
37
class StringsFmf
38
{
39
  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
40
41
 public:
42
  StringsFmf(context::Context* c,
43
             context::UserContext* u,
44
             Valuation valuation,
45
             TermRegistry& tr);
46
  ~StringsFmf();
47
  /** presolve
48
   *
49
   * This initializes a (new copy) of the decision strategy d_sslds.
50
   */
51
  void presolve();
52
  /**
53
   * Get the decision strategy, valid after a call to presolve in the duration
54
   * of a check-sat call.
55
   */
56
  DecisionStrategy* getDecisionStrategy() const;
57
58
 private:
59
  /** String sum of lengths decision strategy
60
   *
61
   * This decision strategy enforces that len(x_1) + ... + len(x_k) <= n
62
   * for a minimal natural number n, where x_1, ..., x_n is the list of
63
   * input variables of the problem of type String.
64
   *
65
   * This decision strategy is enabled by option::stringsFmf().
66
   */
67
122
  class StringSumLengthDecisionStrategy : public DecisionStrategyFmf
68
  {
69
   public:
70
    StringSumLengthDecisionStrategy(context::Context* c,
71
                                    context::UserContext* u,
72
                                    Valuation valuation);
73
    /** make literal */
74
    Node mkLiteral(unsigned i) override;
75
    /** identify */
76
    std::string identify() const override;
77
    /** is initialized */
78
    bool isInitialized();
79
    /** initialize */
80
    void initialize(const std::vector<Node>& vars);
81
82
    /*
83
     * Do not hide the zero-argument version of initialize() inherited from the
84
     * base class
85
     */
86
    using DecisionStrategyFmf::initialize;
87
88
   private:
89
    /**
90
     * User-context-dependent node corresponding to the sum of the lengths of
91
     * input variables of type string
92
     */
93
    context::CDO<Node> d_inputVarLsum;
94
  };
95
  /** an instance of the above class */
96
  std::unique_ptr<StringSumLengthDecisionStrategy> d_sslds;
97
  /** The SAT search context for the theory of strings. */
98
  context::Context* d_satContext;
99
  /** The user level assertion context for the theory of strings. */
100
  context::UserContext* d_userContext;
101
  /** The valuation object of theory of strings */
102
  Valuation d_valuation;
103
  /** The term registry of theory of strings */
104
  TermRegistry& d_termReg;
105
};
106
107
}  // namespace strings
108
}  // namespace theory
109
}  // namespace CVC4
110
111
#endif /* CVC4__THEORY__STRINGS__STRINGS_FMF_H */