GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/ext/constraint.h Lines: 2 2 100.0 %
Date: 2021-03-22 Branches: 1 2 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file constraint.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, 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 Utilities for non-linear constraints
13
 **/
14
15
#ifndef CVC4__THEORY__ARITH__NL__EXT__CONSTRAINT_H
16
#define CVC4__THEORY__ARITH__NL__EXT__CONSTRAINT_H
17
18
#include <map>
19
#include <vector>
20
21
#include "expr/kind.h"
22
#include "expr/node.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace arith {
27
namespace nl {
28
29
class MonomialDb;
30
31
/** constraint information
32
 *
33
 * The struct ( d_rhs, d_coeff, d_type ) represents that a literal is of the
34
 * form (d_coeff * x) <d_type> d_rhs.
35
 */
36
39224
struct ConstraintInfo
37
{
38
 public:
39
  /** The term on the right hand side of the constraint */
40
  Node d_rhs;
41
  /** The coefficent */
42
  Node d_coeff;
43
  /** The type (relation) of the constraint */
44
  Kind d_type;
45
}; /* struct ConstraintInfo */
46
47
/** A database for constraints */
48
class ConstraintDb
49
{
50
 public:
51
  ConstraintDb(MonomialDb& mdb);
52
4386
  ~ConstraintDb() {}
53
  /** register constraint
54
   *
55
   * This ensures that atom is in the domain of the constraints maintained by
56
   * this database.
57
   */
58
  void registerConstraint(Node atom);
59
  /** get constraints
60
   *
61
   * Returns a map m such that whenever
62
   * m[lit][x] = ( r, coeff, k ), then
63
   * ( lit <=>  (coeff * x) <k> r )
64
   */
65
  const std::map<Node, std::map<Node, ConstraintInfo> >& getConstraints();
66
  /** Returns true if m is of maximal degree in atom
67
   *
68
   * For example, for atom x^2 + x*y + y >=0, the monomials x^2 and x*y
69
   * are of maximal degree (2).
70
   */
71
  bool isMaximal(Node atom, Node m) const;
72
73
 private:
74
  /** Reference to a monomial database */
75
  MonomialDb& d_mdb;
76
  /** List of all constraints */
77
  std::vector<Node> d_constraints;
78
  /** Is maximal degree */
79
  std::map<Node, std::map<Node, bool> > d_c_info_maxm;
80
  /** Constraint information */
81
  std::map<Node, std::map<Node, ConstraintInfo> > d_c_info;
82
};
83
84
}  // namespace nl
85
}  // namespace arith
86
}  // namespace theory
87
}  // namespace CVC4
88
89
#endif /* CVC4__THEORY__ARITH__NL_SOLVER_H */