src/proof/arith_proof.h

   1 /*********************                                                        */
   2 /*! \file arith_proof.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Alex Ozdemir, Guy Katz, Mathias Preiner
   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 Arith proof
  13  **
  14  ** Arith proof
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef CVC4__ARITH__PROOF_H
  20 #define CVC4__ARITH__PROOF_H
  21
  22 #include <memory>
  23 #include <unordered_set>
  24
  25 #include "expr/expr.h"
  26 #include "proof/arith_proof_recorder.h"
  27 #include "proof/proof_manager.h"
  28 #include "proof/theory_proof.h"
  29 #include "theory/uf/equality_engine.h"
  30
  31 namespace CVC4 {
  32
  33 //proof object outputted by TheoryArith
  34 class ProofArith : public Proof {
  35  public:
  36   ProofArith(std::shared_ptr<theory::eq::EqProof> pf) : d_proof(pf) {}
  37   void toStream(std::ostream& out) const override;
  38
  39  private:
  40   static void toStreamLFSC(std::ostream& out, TheoryProof* tp,
  41                            const theory::eq::EqProof& pf,
  42                            const ProofLetMap& map);
  43   static Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp,
  44                               const theory::eq::EqProof& pf,
  45                               unsigned tb, const ProofLetMap& map);
  46   // it is simply an equality engine proof
  47   std::shared_ptr<theory::eq::EqProof> d_proof;
  48 };
  49
  50 namespace theory {
  51 namespace arith {
  52 class TheoryArith;
  53 }
  54 }
  55
  56 typedef std::unordered_set<Type, TypeHashFunction > TypeSet;
  57
  58
  59 class ArithProof : public TheoryProof {
  60 protected:
  61   // std::map<Expr, std::string> d_constRationalString; // all the variable/function declarations
  62
  63   //   TypeSet d_sorts;        // all the uninterpreted sorts in this theory
  64   ExprSet d_declarations; // all the variable/function declarations
  65
  66   /**
  67    * Where farkas proofs of lemmas are stored.
  68    */
  69   proof::ArithProofRecorder d_recorder;
  70
  71   theory::TheoryId getTheoryId() override;
  72
  73  public:
  74   ArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine);
  75
  76   void registerTerm(Expr term) override;
  77 };
  78
  79 class LFSCArithProof : public ArithProof {
  80 public:
  81   LFSCArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine)
  82     : ArithProof(arith, proofEngine)
  83   {}
  84   void printOwnedTermAsType(Expr term,
  85                             std::ostream& os,
  86                             const ProofLetMap& map,
  87                             TypeNode expectedType) override;
  88   void printOwnedSort(Type type, std::ostream& os) override;
  89
  90   /**
  91    * Returns the LFSC identifier for the operator of this node.
  92    *
  93    * e.g. "+_Real".
  94    *
  95    * Does not include any parens.
  96    *
  97    * Even if the operator is a comparison (e.g. >=) on integers, will not
  98    * return a purely `Int` predicate like ">=_Int". Instead this treats the
  99    * right hand side as a real.
 100    */
 101   static std::string getLfscFunction(const Node& n);
 102
 103   /**
 104    * Print a rational number in LFSC format.
 105    *        e.g. 5/8 or (~ 1/1)
 106    *
 107    * @param o ostream to print to.
 108    * @param r the rational to print
 109    */
 110   static void printRational(std::ostream& o, const Rational& r);
 111
 112   /**
 113    * Print an integer in LFSC format.
 114    *        e.g. 5 or (~ 1)
 115    *
 116    * @param o ostream to print to.
 117    * @param i the integer to print
 118    */
 119   static void printInteger(std::ostream& o, const Integer& i);
 120
 121   /**
 122    * Print a value of type poly_formula_norm
 123    *
 124    * @param o ostream to print to
 125    * @param n node (asserted to be of the form [linear polynomial >= constant])
 126    */
 127   static void printLinearPolynomialPredicateNormalizer(std::ostream& o,
 128                                                        const Node& n);
 129
 130   /**
 131    * Print a value of type poly_norm
 132    *
 133    * @param o ostream to print to
 134    * @param n node (asserted to be a linear polynomial)
 135    */
 136   static void printLinearPolynomialNormalizer(std::ostream& o, const Node& n);
 137
 138   /**
 139    * Print a value of type poly_norm
 140    *
 141    * @param o ostream to print to
 142    * @param n node (asserted to be a linear monomial)
 143    */
 144   static void printLinearMonomialNormalizer(std::ostream& o, const Node& n);
 145
 146   /**
 147    * Print a LFSC rational
 148    *
 149    * @param o ostream to print to
 150    * @param n node (asserted to be a const rational)
 151    */
 152   static void printConstRational(std::ostream& o, const Node& n);
 153
 154   /**
 155    * print the pn_var normalizer for n (type poly_norm)
 156    *
 157    * @param o the ostream to print to
 158    * @param n the node to print (asserted to be a variable)
 159    */
 160   static void printVariableNormalizer(std::ostream& o, const Node& n);
 161   /**
 162    * print a proof of the lemma
 163    *
 164    * First, we print linearity witnesses, i.e. witnesses  that each literal has
 165    * the form:
 166    *   [linear polynomial] >= 0 OR
 167    *   [linear polynomial] >  0
 168    *
 169    * Then we use those witnesses to prove that the above linearized constraints
 170    * hold.
 171    *
 172    * Then we use the farkas coefficients to combine the literals into a
 173    * variable-free contradiction. The literals may be a mix of strict and
 174    * relaxed inequalities.
 175    *
 176    * @param lemma the set of literals disjoined in the lemma
 177    * @param os stream to print the proof to
 178    * @param paren global closing stream (unused)
 179    * @param map let map (unused)
 180    */
 181   void printTheoryLemmaProof(std::vector<Expr>& lemma,
 182                              std::ostream& os,
 183                              std::ostream& paren,
 184                              const ProofLetMap& map) override;
 185   void printSortDeclarations(std::ostream& os, std::ostream& paren) override;
 186   void printTermDeclarations(std::ostream& os, std::ostream& paren) override;
 187   void printDeferredDeclarations(std::ostream& os,
 188                                  std::ostream& paren) override;
 189   void printAliasingDeclarations(std::ostream& os,
 190                                  std::ostream& paren,
 191                                  const ProofLetMap& globalLetMap) override;
 192
 193   /**
 194    * Given a node that is an arith literal (an arith comparison or negation
 195    * thereof), prints a proof of that literal.
 196    *
 197    * If the node represents a tightenable bound (e.g. [Int] < 3) then it prints
 198    * a proof of the tightening instead. (e.g. [Int] <= 2).
 199    *
 200    * @return a pair comprising:
 201    *            * the new node (after tightening) and
 202    *            * a string proving it.
 203    */
 204   std::pair<Node, std::string> printProofAndMaybeTighten(const Node& bound);
 205
 206   /**
 207    * Return whether this node, when serialized to LFSC, has sort `Bool`. Otherwise, the sort is `formula`.
 208    */
 209   bool printsAsBool(const Node& n) override;
 210
 211   TypeNode equalityType(const Expr& left, const Expr& right) override;
 212 };
 213
 214
 215 }/* CVC4 namespace */
 216
 217 #endif /* CVC4__ARITH__PROOF_H */