1 /********************* */
2 /*! \file arith_proof.h
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
17 #include "cvc4_private.h"
19 #ifndef CVC4__ARITH__PROOF_H
20 #define CVC4__ARITH__PROOF_H
23 #include <unordered_set>
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"
33 //proof object outputted by TheoryArith
34 class ProofArith
: public Proof
{
36 ProofArith(std::shared_ptr
<theory::eq::EqProof
> pf
) : d_proof(pf
) {}
37 void toStream(std::ostream
& out
) const override
;
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
;
56 typedef std::unordered_set
<Type
, TypeHashFunction
> TypeSet
;
59 class ArithProof
: public TheoryProof
{
61 // std::map<Expr, std::string> d_constRationalString; // all the variable/function declarations
63 // TypeSet d_sorts; // all the uninterpreted sorts in this theory
64 ExprSet d_declarations
; // all the variable/function declarations
67 * Where farkas proofs of lemmas are stored.
69 proof::ArithProofRecorder d_recorder
;
71 theory::TheoryId
getTheoryId() override
;
74 ArithProof(theory::arith::TheoryArith
* arith
, TheoryProofEngine
* proofEngine
);
76 void registerTerm(Expr term
) override
;
79 class LFSCArithProof
: public ArithProof
{
81 LFSCArithProof(theory::arith::TheoryArith
* arith
, TheoryProofEngine
* proofEngine
)
82 : ArithProof(arith
, proofEngine
)
84 void printOwnedTermAsType(Expr term
,
86 const ProofLetMap
& map
,
87 TypeNode expectedType
) override
;
88 void printOwnedSort(Type type
, std::ostream
& os
) override
;
91 * Returns the LFSC identifier for the operator of this node.
95 * Does not include any parens.
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.
101 static std::string
getLfscFunction(const Node
& n
);
104 * Print a rational number in LFSC format.
105 * e.g. 5/8 or (~ 1/1)
107 * @param o ostream to print to.
108 * @param r the rational to print
110 static void printRational(std::ostream
& o
, const Rational
& r
);
113 * Print an integer in LFSC format.
116 * @param o ostream to print to.
117 * @param i the integer to print
119 static void printInteger(std::ostream
& o
, const Integer
& i
);
122 * Print a value of type poly_formula_norm
124 * @param o ostream to print to
125 * @param n node (asserted to be of the form [linear polynomial >= constant])
127 static void printLinearPolynomialPredicateNormalizer(std::ostream
& o
,
131 * Print a value of type poly_norm
133 * @param o ostream to print to
134 * @param n node (asserted to be a linear polynomial)
136 static void printLinearPolynomialNormalizer(std::ostream
& o
, const Node
& n
);
139 * Print a value of type poly_norm
141 * @param o ostream to print to
142 * @param n node (asserted to be a linear monomial)
144 static void printLinearMonomialNormalizer(std::ostream
& o
, const Node
& n
);
147 * Print a LFSC rational
149 * @param o ostream to print to
150 * @param n node (asserted to be a const rational)
152 static void printConstRational(std::ostream
& o
, const Node
& n
);
155 * print the pn_var normalizer for n (type poly_norm)
157 * @param o the ostream to print to
158 * @param n the node to print (asserted to be a variable)
160 static void printVariableNormalizer(std::ostream
& o
, const Node
& n
);
162 * print a proof of the lemma
164 * First, we print linearity witnesses, i.e. witnesses that each literal has
166 * [linear polynomial] >= 0 OR
167 * [linear polynomial] > 0
169 * Then we use those witnesses to prove that the above linearized constraints
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.
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)
181 void printTheoryLemmaProof(std::vector
<Expr
>& lemma
,
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
,
191 const ProofLetMap
& globalLetMap
) override
;
194 * Given a node that is an arith literal (an arith comparison or negation
195 * thereof), prints a proof of that literal.
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).
200 * @return a pair comprising:
201 * * the new node (after tightening) and
202 * * a string proving it.
204 std::pair
<Node
, std::string
> printProofAndMaybeTighten(const Node
& bound
);
207 * Return whether this node, when serialized to LFSC, has sort `Bool`. Otherwise, the sort is `formula`.
209 bool printsAsBool(const Node
& n
) override
;
211 TypeNode
equalityType(const Expr
& left
, const Expr
& right
) override
;
215 }/* CVC4 namespace */
217 #endif /* CVC4__ARITH__PROOF_H */