src/theory/arith/proof_checker.cpp

   1 /*********************                                                        */
   2 /*! \file proof_checker.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Alex Ozdemir
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 arithmetic proof checker
  13  **/
  14
  15 #include "theory/arith/proof_checker.h"
  16
  17 #include <iostream>
  18 #include <set>
  19
  20 #include "expr/skolem_manager.h"
  21 #include "theory/arith/arith_utilities.h"
  22 #include "theory/arith/constraint.h"
  23 #include "theory/arith/normal_form.h"
  24 #include "theory/arith/operator_elim.h"
  25
  26 namespace CVC4 {
  27 namespace theory {
  28 namespace arith {
  29
  30 void ArithProofRuleChecker::registerTo(ProofChecker* pc)
  31 {
  32   pc->registerChecker(PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS, this);
  33   pc->registerChecker(PfRule::ARITH_TRICHOTOMY, this);
  34   pc->registerChecker(PfRule::INT_TIGHT_UB, this);
  35   pc->registerChecker(PfRule::INT_TIGHT_LB, this);
  36   pc->registerChecker(PfRule::INT_TRUST, this);
  37   pc->registerChecker(PfRule::ARITH_OP_ELIM_AXIOM, this);
  38 }
  39
  40 Node ArithProofRuleChecker::checkInternal(PfRule id,
  41                                           const std::vector<Node>& children,
  42                                           const std::vector<Node>& args)
  43 {
  44   if (Debug.isOn("arith::pf::check"))
  45   {
  46     Debug("arith::pf::check") << "Arith PfRule:" << id << std::endl;
  47     Debug("arith::pf::check") << "  children: " << std::endl;
  48     for (const auto& c : children)
  49     {
  50       Debug("arith::pf::check") << "  * " << c << std::endl;
  51     }
  52     Debug("arith::pf::check") << "  args:" << std::endl;
  53     for (const auto& c : args)
  54     {
  55       Debug("arith::pf::check") << "  * " << c << std::endl;
  56     }
  57   }
  58   switch (id)
  59   {
  60     case PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS:
  61     {
  62       // Children: (P1:l1, ..., Pn:ln)
  63       //           where each li is an ArithLiteral
  64       //           not(= ...) is dis-allowed!
  65       //
  66       // Arguments: (k1, ..., kn), non-zero reals
  67       // ---------------------
  68       // Conclusion: (>< (* k t1) (* k t2))
  69       //    where >< is the fusion of the combination of the ><i, (flipping each
  70       //    it its ki is negative). >< is always one of <, <= NB: this implies
  71       //    that lower bounds must have negative ki,
  72       //                      and upper bounds must have positive ki.
  73       //    t1 is the sum of the polynomials.
  74       //    t2 is the sum of the constants.
  75       Assert(children.size() == args.size());
  76       if (children.size() < 2)
  77       {
  78         return Node::null();
  79       }
  80
  81       // Whether a strict inequality is in the sum.
  82       auto nm = NodeManager::currentNM();
  83       bool strict = false;
  84       NodeBuilder<> leftSum(Kind::PLUS);
  85       NodeBuilder<> rightSum(Kind::PLUS);
  86       for (size_t i = 0; i < children.size(); ++i)
  87       {
  88         Rational scalar = args[i].getConst<Rational>();
  89         if (scalar == 0)
  90         {
  91           Debug("arith::pf::check") << "Error: zero scalar" << std::endl;
  92           return Node::null();
  93         }
  94
  95         // Adjust strictness
  96         switch (children[i].getKind())
  97         {
  98           case Kind::GT:
  99           case Kind::LT:
 100           {
 101             strict = true;
 102             break;
 103           }
 104           case Kind::GEQ:
 105           case Kind::LEQ:
 106           case Kind::EQUAL:
 107           {
 108             break;
 109           }
 110           default:
 111           {
 112             Debug("arith::pf::check")
 113                 << "Bad kind: " << children[i].getKind() << std::endl;
 114           }
 115         }
 116         // Check sign
 117         switch (children[i].getKind())
 118         {
 119           case Kind::GT:
 120           case Kind::GEQ:
 121           {
 122             if (scalar > 0)
 123             {
 124               Debug("arith::pf::check")
 125                   << "Positive scalar for lower bound: " << scalar << " for "
 126                   << children[i] << std::endl;
 127               return Node::null();
 128             }
 129             break;
 130           }
 131           case Kind::LEQ:
 132           case Kind::LT:
 133           {
 134             if (scalar < 0)
 135             {
 136               Debug("arith::pf::check")
 137                   << "Negative scalar for upper bound: " << scalar << " for "
 138                   << children[i] << std::endl;
 139               return Node::null();
 140             }
 141             break;
 142           }
 143           case Kind::EQUAL:
 144           {
 145             break;
 146           }
 147           default:
 148           {
 149             Debug("arith::pf::check")
 150                 << "Bad kind: " << children[i].getKind() << std::endl;
 151           }
 152         }
 153         leftSum << nm->mkNode(
 154             Kind::MULT, children[i][0], nm->mkConst<Rational>(scalar));
 155         rightSum << nm->mkNode(
 156             Kind::MULT, children[i][1], nm->mkConst<Rational>(scalar));
 157       }
 158       Node r = nm->mkNode(strict ? Kind::LT : Kind::LEQ,
 159                           leftSum.constructNode(),
 160                           rightSum.constructNode());
 161       return r;
 162     }
 163     case PfRule::INT_TIGHT_LB:
 164     {
 165       // Children: (P:(> i c))
 166       //         where i has integer type.
 167       // Arguments: none
 168       // ---------------------
 169       // Conclusion: (>= i leastIntGreaterThan(c)})
 170       if (children.size() != 1
 171           || (children[0].getKind() != Kind::GT
 172               && children[0].getKind() != Kind::GEQ)
 173           || !children[0][0].getType().isInteger()
 174           || children[0][1].getKind() != Kind::CONST_RATIONAL)
 175       {
 176         Debug("arith::pf::check") << "Illformed input: " << children;
 177         return Node::null();
 178       }
 179       else
 180       {
 181         Rational originalBound = children[0][1].getConst<Rational>();
 182         Rational newBound = leastIntGreaterThan(originalBound);
 183         auto nm = NodeManager::currentNM();
 184         Node rational = nm->mkConst<Rational>(newBound);
 185         return nm->mkNode(kind::GEQ, children[0][0], rational);
 186       }
 187     }
 188     case PfRule::INT_TIGHT_UB:
 189     {
 190       // ======== Tightening Strict Integer Upper Bounds
 191       // Children: (P:(< i c))
 192       //         where i has integer type.
 193       // Arguments: none
 194       // ---------------------
 195       // Conclusion: (<= i greatestIntLessThan(c)})
 196       if (children.size() != 1
 197           || (children[0].getKind() != Kind::LT
 198               && children[0].getKind() != Kind::LEQ)
 199           || !children[0][0].getType().isInteger()
 200           || children[0][1].getKind() != Kind::CONST_RATIONAL)
 201       {
 202         Debug("arith::pf::check") << "Illformed input: " << children;
 203         return Node::null();
 204       }
 205       else
 206       {
 207         Rational originalBound = children[0][1].getConst<Rational>();
 208         Rational newBound = greatestIntLessThan(originalBound);
 209         auto nm = NodeManager::currentNM();
 210         Node rational = nm->mkConst<Rational>(newBound);
 211         return nm->mkNode(kind::LEQ, children[0][0], rational);
 212       }
 213     }
 214     case PfRule::ARITH_TRICHOTOMY:
 215     {
 216       Node a = negateProofLiteral(children[0]);
 217       Node b = negateProofLiteral(children[1]);
 218       Node c = args[0];
 219       if (a[0] == b[0] && b[0] == c[0] && a[1] == b[1] && b[1] == c[1])
 220       {
 221         std::set<Kind> cmps;
 222         cmps.insert(a.getKind());
 223         cmps.insert(b.getKind());
 224         cmps.insert(c.getKind());
 225         if (cmps.count(Kind::EQUAL) == 0)
 226         {
 227           Debug("arith::pf::check") << "Error: No = " << std::endl;
 228           return Node::null();
 229         }
 230         if (cmps.count(Kind::GT) == 0)
 231         {
 232           Debug("arith::pf::check") << "Error: No > " << std::endl;
 233           return Node::null();
 234         }
 235         if (cmps.count(Kind::LT) == 0)
 236         {
 237           Debug("arith::pf::check") << "Error: No < " << std::endl;
 238           return Node::null();
 239         }
 240         return args[0];
 241       }
 242       else
 243       {
 244         Debug("arith::pf::check")
 245             << "Error: Different polynomials / values" << std::endl;
 246         Debug("arith::pf::check") << "  a: " << a << std::endl;
 247         Debug("arith::pf::check") << "  b: " << b << std::endl;
 248         Debug("arith::pf::check") << "  c: " << c << std::endl;
 249         return Node::null();
 250       }
 251       // Check that all have the same constant:
 252     }
 253     case PfRule::INT_TRUST:
 254     {
 255       Assert(args.size() == 1);
 256       return args[0];
 257     }
 258     case PfRule::ARITH_OP_ELIM_AXIOM:
 259     {
 260       Assert(children.empty());
 261       Assert(args.size() == 1);
 262       return OperatorElim::getAxiomFor(args[0]);
 263     }
 264     default: return Node::null();
 265   }
 266 }
 267 }  // namespace arith
 268 }  // namespace theory
 269 }  // namespace CVC4