CVC3  2.4.1
quant_proof_rules.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file quant_proof_rules.h
4  *
5  * Author: Daniel Wichs
6  *
7  * Created: Jul 07 22:22:38 GMT 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 #ifndef _cvc3__quant_proof_rules_h_
21 #define _cvc3__quant_proof_rules_h_
22 
23 #include <vector>
24 
25 namespace CVC3 {
26 
27  class Expr;
28  class Theorem;
29 
31  public:
32  //! Destructor
33  virtual ~QuantProofRules() { }
34 
35  virtual Theorem addNewConst(const Expr& e) =0;
36 
37  virtual Theorem newRWThm(const Expr& e, const Expr& newE) = 0 ;
38 
39  virtual Theorem normalizeQuant(const Expr& e) =0;
40 
41  //! ==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
42  virtual Theorem rewriteNotExists(const Expr& e) = 0;
43 
44  //! ==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
45  virtual Theorem rewriteNotForall(const Expr& e) = 0;
46 
47  //! Instantiate a universally quantified formula
48  /*! From T|-FORALL(var): e generate T|-e' where e' is obtained
49  * from e by instantiating bound variables with terms in
50  * vector<Expr>& terms. The vector of terms should be the same
51  * size as the vector of bound variables in e. Also elements in
52  * each position i need to have matching types.
53  * \param t1 is the quantifier (a Theorem)
54  * \param terms are the terms to instantiate.
55  * \param quantLevel is the quantification level for the theorem.
56  */
57  virtual Theorem universalInst(const Theorem& t1, const std::vector<Expr>& terms, int quantLevel, Expr gterm ) = 0 ;
58 
59  virtual Theorem universalInst(const Theorem& t1,
60  const std::vector<Expr>& terms, int quantLevel) = 0;
61 
62  virtual Theorem universalInst(const Theorem& t1,
63  const std::vector<Expr>& terms) = 0;
64 
65 
66  virtual Theorem partialUniversalInst(const Theorem& t1,
67  const std::vector<Expr>& terms,
68  int quantLevel) = 0;
69 
70  /*! @brief From T|- QUANTIFIER (vars): e we get T|-QUANTIFIER(vars') e
71  * where vars' is obtained from vars by removing all bound variables
72  * not used in e. If vars' is empty the produced theorem is just T|-e
73  */
74  virtual Theorem boundVarElim(const Theorem& t1) = 0;
75 
76  virtual Theorem packVar(const Theorem& t1) = 0;
77 
78  virtual Theorem pullVarOut(const Theorem& t1) = 0;
79 
80  virtual Theorem adjustVarUniv(const Theorem& t1,
81  const std::vector<Expr>& newBvs) = 0;
82 
83  };
84 }
85 #endif
virtual Theorem pullVarOut(const Theorem &t1)=0
Data structure of expressions in CVC3.
Definition: expr.h:133
virtual Theorem adjustVarUniv(const Theorem &t1, const std::vector< Expr > &newBvs)=0
virtual Theorem addNewConst(const Expr &e)=0
virtual Theorem rewriteNotForall(const Expr &e)=0
==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
virtual Theorem boundVarElim(const Theorem &t1)=0
From T|- QUANTIFIER (vars): e we get T|-QUANTIFIER(vars') e where vars' is obtained from vars by remo...
virtual Theorem universalInst(const Theorem &t1, const std::vector< Expr > &terms, int quantLevel, Expr gterm)=0
Instantiate a universally quantified formula.
virtual Theorem rewriteNotExists(const Expr &e)=0
==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
virtual Theorem partialUniversalInst(const Theorem &t1, const std::vector< Expr > &terms, int quantLevel)=0
virtual ~QuantProofRules()
Destructor.
virtual Theorem newRWThm(const Expr &e, const Expr &newE)=0
virtual Theorem packVar(const Theorem &t1)=0
virtual Theorem normalizeQuant(const Expr &e)=0