1 /*********************                                                        */
2 /*! \file quant_epr.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Andrew Reynolds
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 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 quantifier util
13  **/
14 
15 #include "cvc4_private.h"
16 
17 #ifndef __CVC4__THEORY__QUANT_EPR_H
18 #define __CVC4__THEORY__QUANT_EPR_H
19 
20 #include <map>
21 
22 #include "expr/node.h"
23 #include "expr/type_node.h"
24 
25 namespace CVC4 {
26 namespace theory {
27 namespace quantifiers {
28 
29 /** Quant EPR
30  *
31  * This class maintains information required for
32  * approaches for effectively propositional logic (EPR),
33  * also called the Bernays-Schoenfinkel fragment.
34  *
35  * It maintains for each type whether the type
36  * has a finite Herbrand universe, stored in d_consts.
37  * This class is used in counterexample-guided instantiation
38  * for EPR, described in Reynolds et al.,
39  * "Reasoning in the Bernays-Schonfinkel-Ramsey Fragment of
40  * Separation Logic", VMCAI 2017.
41  *
42  * Below, we say a type is an "EPR type" if its
43  * Herbrand universe can be restricted to a finite set
44  * based on the set of input assertions,
45  * and a "non-EPR type" otherwise.
46  */
47 class QuantEPR
48 {
49  public:
QuantEPR()50   QuantEPR() {}
~QuantEPR()51   virtual ~QuantEPR() {}
52   /** constants per type */
53   std::map<TypeNode, std::vector<Node> > d_consts;
54   /** register an input assertion with this class
55    * This updates whether types are EPR are not
56    * based on the constraints in assertion.
57    */
58   void registerAssertion(Node assertion);
59   /** finish initialize
60    * This ensures all EPR sorts are non-empty
61    * (that is, they have at least one term in d_consts),
62    * and clears non-EPR sorts from d_consts.
63    */
64   void finishInit();
65   /** is type tn an EPR type? */
isEPR(TypeNode tn)66   bool isEPR(TypeNode tn) const
67   {
68     return d_non_epr.find(tn) == d_non_epr.end();
69   }
70   /** is k an EPR constant for type tn? */
71   bool isEPRConstant(TypeNode tn, Node k);
72   /** add EPR constant k of type tn. */
73   void addEPRConstant(TypeNode tn, Node k);
74   /** get EPR axiom for type
75    * This is a formula of the form:
76    *   forall x : U. ( x = c1 V ... x = cn )
77    * where c1...cn are the constants in the Herbrand
78    * universe of U.
79    */
80   Node mkEPRAxiom(TypeNode tn);
81   /** does this class have an EPR axiom for type tn? */
hasEPRAxiom(TypeNode tn)82   bool hasEPRAxiom(TypeNode tn) const
83   {
84     return d_epr_axiom.find(tn) != d_epr_axiom.end();
85   }
86 
87  private:
88   /** register the node */
89   void registerNode(Node n,
90                     std::map<int, std::map<Node, bool> >& visited,
91                     bool beneathQuant,
92                     bool hasPol,
93                     bool pol);
94   /** map from types to a flag says whether they are not EPR */
95   std::map<TypeNode, bool> d_non_epr;
96   /** EPR axioms for each type. */
97   std::map<TypeNode, Node> d_epr_axiom;
98 };
99 
100 } /* CVC4::theory::quantifiers namespace */
101 } /* CVC4::theory namespace */
102 } /* CVC4 namespace */
103 
104 #endif /* __CVC4__THEORY__QUANT_EPR_H */
105