GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/ext/proof_checker.cpp Lines: 81 87 93.1 %
Date: 2021-03-22 Branches: 219 718 30.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_checker.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Gereon Kremer, Tim King
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 NlExt proof checker
13
 **/
14
15
#include "theory/arith/nl/ext/proof_checker.h"
16
17
#include "expr/sequence.h"
18
#include "theory/arith/arith_utilities.h"
19
#include "theory/rewriter.h"
20
21
using namespace CVC4::kind;
22
23
namespace CVC4 {
24
namespace theory {
25
namespace arith {
26
namespace nl {
27
28
401
void ExtProofRuleChecker::registerTo(ProofChecker* pc)
29
{
30
401
  pc->registerChecker(PfRule::ARITH_MULT_SIGN, this);
31
401
  pc->registerChecker(PfRule::ARITH_MULT_TANGENT, this);
32
401
}
33
34
188
Node ExtProofRuleChecker::checkInternal(PfRule id,
35
                                        const std::vector<Node>& children,
36
                                        const std::vector<Node>& args)
37
{
38
188
  NodeManager* nm = NodeManager::currentNM();
39
376
  auto zero = nm->mkConst<Rational>(0);
40
376
  auto one = nm->mkConst<Rational>(1);
41
376
  auto mone = nm->mkConst<Rational>(-1);
42
376
  auto pi = nm->mkNullaryOperator(nm->realType(), Kind::PI);
43
376
  auto mpi = nm->mkNode(Kind::MULT, mone, pi);
44
188
  Trace("nl-ext-checker") << "Checking " << id << std::endl;
45
188
  for (const auto& c : children)
46
  {
47
    Trace("nl-ext-checker") << "\t" << c << std::endl;
48
  }
49
188
  if (id == PfRule::ARITH_MULT_SIGN)
50
  {
51
174
    Assert(children.empty());
52
174
    Assert(args.size() > 1);
53
348
    Node mon = args.back();
54
348
    std::map<Node, int> exps;
55
348
    std::vector<Node> premise = args;
56
174
    premise.pop_back();
57
174
    Assert(mon.getKind() == Kind::MULT
58
           || mon.getKind() == Kind::NONLINEAR_MULT);
59
643
    for (const auto& v : mon)
60
    {
61
469
      exps[v]++;
62
    }
63
348
    std::map<Node, int> signs;
64
576
    for (const auto& f : premise)
65
    {
66
433
      if (f.getKind() == Kind::NOT)
67
      {
68
31
        Assert(f[0].getKind() == Kind::EQUAL);
69
31
        Assert(f[0][1].isConst() && f[0][1].getConst<Rational>().isZero());
70
31
        Assert(signs.find(f[0][0]) == signs.end());
71
31
        signs.emplace(f[0][0], 0);
72
31
        continue;
73
      }
74
371
      Assert(f.getKind() == Kind::LT || f.getKind() == Kind::GT);
75
371
      Assert(f[1].isConst() && f[1].getConst<Rational>().isZero());
76
371
      Assert(signs.find(f[0]) == signs.end());
77
371
      signs.emplace(f[0], f.getKind() == Kind::LT ? -1 : 1);
78
    }
79
174
    int sign = 0;
80
576
    for (const auto& ve : exps)
81
    {
82
402
      auto sit = signs.find(ve.first);
83
402
      Assert(sit != signs.end());
84
402
      if (ve.second % 2 == 0)
85
      {
86
31
        Assert(sit->second == 0);
87
31
        if (sign == 0)
88
        {
89
26
          sign = 1;
90
        }
91
      }
92
      else
93
      {
94
371
        Assert(sit->second != 0);
95
371
        if (sign == 0)
96
        {
97
148
          sign = sit->second;
98
        }
99
        else
100
        {
101
223
          sign *= sit->second;
102
        }
103
      }
104
    }
105
174
    switch (sign)
106
    {
107
67
      case -1:
108
        return nm->mkNode(
109
67
            Kind::IMPLIES, nm->mkAnd(premise), nm->mkNode(Kind::GT, zero, mon));
110
      case 0:
111
        return nm->mkNode(Kind::IMPLIES,
112
                          nm->mkAnd(premise),
113
                          nm->mkNode(Kind::DISTINCT, mon, zero));
114
107
      case 1:
115
        return nm->mkNode(
116
107
            Kind::IMPLIES, nm->mkAnd(premise), nm->mkNode(Kind::GT, mon, zero));
117
      default: Assert(false); return Node();
118
    }
119
  }
120
14
  else if (id == PfRule::ARITH_MULT_TANGENT)
121
  {
122
14
    Assert(children.empty());
123
14
    Assert(args.size() == 6);
124
14
    Assert(args[0].getType().isReal());
125
14
    Assert(args[1].getType().isReal());
126
14
    Assert(args[2].getType().isReal());
127
14
    Assert(args[3].getType().isReal());
128
14
    Assert(args[4].getType().isReal());
129
14
    Assert(args[5].isConst() && args[5].getKind() == Kind::CONST_RATIONAL
130
           && args[5].getConst<Rational>().isIntegral());
131
28
    Node t = args[0];
132
28
    Node x = args[1];
133
28
    Node y = args[2];
134
28
    Node a = args[3];
135
28
    Node b = args[4];
136
14
    int sgn = args[5].getConst<Rational>().getNumerator().sgn();
137
14
    Assert(sgn == -1 || sgn == 1);
138
    Node tplane = nm->mkNode(Kind::MINUS,
139
56
                             nm->mkNode(Kind::PLUS,
140
28
                                        nm->mkNode(Kind::MULT, b, x),
141
28
                                        nm->mkNode(Kind::MULT, a, y)),
142
56
                             nm->mkNode(Kind::MULT, a, b));
143
    return nm->mkNode(
144
        Kind::EQUAL,
145
28
        nm->mkNode(sgn == -1 ? Kind::LEQ : Kind::GEQ, t, tplane),
146
56
        nm->mkNode(
147
            Kind::OR,
148
56
            nm->mkNode(Kind::AND,
149
28
                       nm->mkNode(Kind::LEQ, x, a),
150
28
                       nm->mkNode(sgn == -1 ? Kind::GEQ : Kind::LEQ, y, b)),
151
56
            nm->mkNode(Kind::AND,
152
28
                       nm->mkNode(Kind::GEQ, x, a),
153
70
                       nm->mkNode(sgn == -1 ? Kind::LEQ : Kind::GEQ, y, b))));
154
  }
155
  return Node::null();
156
}
157
158
}  // namespace nl
159
}  // namespace arith
160
}  // namespace theory
161
26676
}  // namespace CVC4