GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/bv_inverter.h Lines: 6 6 100.0 %
Date: 2021-03-23 Branches: 4 8 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bv_inverter.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Aina Niemetz
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 inverse rules for bit-vector operators
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__BV_INVERTER_H
18
#define CVC4__BV_INVERTER_H
19
20
#include <map>
21
#include <unordered_map>
22
#include <unordered_set>
23
#include <vector>
24
25
#include "expr/node.h"
26
27
namespace CVC4 {
28
namespace theory {
29
namespace quantifiers {
30
31
/** BvInverterQuery
32
 *
33
 * This is a virtual class for queries
34
 * required by the BvInverter class.
35
 */
36
class BvInverterQuery
37
{
38
 public:
39
2913
  BvInverterQuery() {}
40
2913
  virtual ~BvInverterQuery() {}
41
  /** returns the current model value of n */
42
  virtual Node getModelValue(Node n) = 0;
43
  /** returns a bound variable of type tn */
44
  virtual Node getBoundVariable(TypeNode tn) = 0;
45
};
46
47
// inverter class
48
// TODO : move to theory/bv/ if generally useful?
49
class BvInverter
50
{
51
 public:
52
4499
  BvInverter() {}
53
4498
  ~BvInverter() {}
54
  /** get dummy fresh variable of type tn, used as argument for sv */
55
  Node getSolveVariable(TypeNode tn);
56
57
  /**
58
   * Get path to pv in lit, replace that occurrence by sv and all others by
59
   * pvs (if pvs is non-null). If return value R is non-null, then :
60
   *   lit.path = pv R.path = sv
61
   *   R.path' = pvs for all lit.path' = pv, where path' != path
62
   *
63
   * If the flag projectNl is false, we return the null node if the
64
   * literal lit is non-linear with respect to pv.
65
   */
66
  Node getPathToPv(Node lit,
67
                   Node pv,
68
                   Node sv,
69
                   Node pvs,
70
                   std::vector<unsigned>& path,
71
                   bool projectNl);
72
73
  /**
74
   * Same as above, but does not linearize lit for pv.
75
   * Use this version if we know lit is linear wrt pv.
76
   */
77
845
  Node getPathToPv(Node lit, Node pv, std::vector<unsigned>& path)
78
  {
79
845
    return getPathToPv(lit, pv, pv, Node::null(), path, false);
80
  }
81
82
  /** solveBvLit
83
   *
84
   * Solve for sv in lit, where lit.path = sv. If this function returns a
85
   * non-null node t, then sv = t is the solved form of lit.
86
   *
87
   * If the BvInverterQuery provided to this function call is null, then
88
   * the solution returned by this call will not contain WITNESS expressions.
89
   * If the solved form for lit requires introducing a WITNESS expression,
90
   * then this call will return null.
91
   */
92
  Node solveBvLit(Node sv,
93
                  Node lit,
94
                  std::vector<unsigned>& path,
95
                  BvInverterQuery* m);
96
97
 private:
98
  /** Dummy variables for each type */
99
  std::map<TypeNode, Node> d_solve_var;
100
101
  /** Helper function for getPathToPv */
102
  Node getPathToPv(Node lit,
103
                   Node pv,
104
                   Node sv,
105
                   std::vector<unsigned>& path,
106
                   std::unordered_set<TNode, TNodeHashFunction>& visited);
107
108
  /** Helper function for getInv.
109
   *
110
   * This expects a condition cond where:
111
   *   (exists x. cond)
112
   * is a BV tautology where x is getSolveVariable( tn ).
113
   *
114
   * It returns a term of the form:
115
   *   (witness y. cond { x -> y })
116
   * where y is a bound variable and x is getSolveVariable( tn ).
117
   *
118
   * In some cases, we may return a term t if cond implies an equality on
119
   * the solve variable. For example, if cond is x = t where x is
120
   * getSolveVariable(tn), then we return t instead of introducing the choice
121
   * function.
122
   *
123
   * This function will return the null node if the BvInverterQuery m provided
124
   * to this call is null.
125
   */
126
  Node getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m);
127
};
128
129
}  // namespace quantifiers
130
}  // namespace theory
131
}  // namespace CVC4
132
133
#endif /* CVC4__BV_INVERTER_H */