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