Merge branch 'master' into splitEqRew

1 files changed, 3 insertions, 81 deletions

diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index 061da81df..904f301b9 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H
-#define __CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H
+#ifndef CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H
+#define CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H
 
 #include <map>
 #include <unordered_set>
@@ -43,43 +43,14 @@ typedef expr::Attribute<TermDepthAttributeId, uint64_t> TermDepthAttribute;
 struct ContainsUConstAttributeId {};
 typedef expr::Attribute<ContainsUConstAttributeId, uint64_t> ContainsUConstAttribute;
 
-//for bounded integers
-struct BoundIntLitAttributeId {};
-typedef expr::Attribute<BoundIntLitAttributeId, uint64_t> BoundIntLitAttribute;
-
 //for quantifier instantiation level
 struct QuantInstLevelAttributeId {};
 typedef expr::Attribute<QuantInstLevelAttributeId, uint64_t> QuantInstLevelAttribute;
 
-//rewrite-rule priority
-struct RrPriorityAttributeId {};
-typedef expr::Attribute<RrPriorityAttributeId, uint64_t> RrPriorityAttribute;
-
-/** Attribute true for quantifiers that do not need to be partially instantiated */
-struct LtePartialInstAttributeId {};
-typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribute;
-
-// attribute for associating a synthesis function with a first order variable
-struct SygusSynthGrammarAttributeId {};
-typedef expr::Attribute<SygusSynthGrammarAttributeId, Node>
-    SygusSynthGrammarAttribute;
-
-// attribute for associating a variable list with a synth fun
-struct SygusSynthFunVarListAttributeId {};
-typedef expr::Attribute<SygusSynthFunVarListAttributeId, Node> SygusSynthFunVarListAttribute;
-
-//attribute for fun-def abstraction type
-struct AbsTypeFunDefAttributeId {};
-typedef expr::Attribute<AbsTypeFunDefAttributeId, bool> AbsTypeFunDefAttribute;
-
 /** Attribute for id number */
 struct QuantIdNumAttributeId {};
 typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute;
 
-/** Attribute to mark Skolems as virtual terms */
-struct VirtualTermSkolemAttributeId {};
-typedef expr::Attribute< VirtualTermSkolemAttributeId, bool > VirtualTermSkolemAttribute;
-
 class QuantifiersEngine;
 
 namespace inst{
@@ -125,8 +96,6 @@ public:
   std::map< Node, std::map< Node, unsigned > > d_var_num;
   /** map from universal quantifiers to their inst constant body */
   std::map< Node, Node > d_inst_const_body;
-  /** map from universal quantifiers to their counterexample literals */
-  std::map< Node, Node > d_ce_lit;
   /** instantiation constants to universal quantifiers */
   std::map< Node, Node > d_inst_constants_map;
 public:
@@ -140,8 +109,6 @@ public:
   unsigned getNumInstantiationConstants( Node q ) const;
   /** get the ce body q[e/x] */
   Node getInstConstantBody( Node q );
-  /** get counterexample literal (for cbqi) */
-  Node getCounterexampleLiteral( Node q );
   /** returns node n with bound vars of q replaced by instantiation constants of q
       node n : is the future pattern
       node q : is the quantifier containing which bind the variable
@@ -164,12 +131,8 @@ public:
   
 private:
   /** get bound vars */
-  static void getBoundVars2( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited );
-  /** get bound vars */
   static Node getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited );
 public:
-  //get the bound variables in this node
-  static void getBoundVars( Node n, std::vector< Node >& vars );
   //remove quantifiers
   static Node getRemoveQuantifiers( Node n );
   //quantified simplify (treat free variables in n as quantified and run rewriter)
@@ -196,39 +159,13 @@ public:
                                                Node n,
                                                std::vector<Node>& vars);
 
-//for virtual term substitution
-private:
-  Node d_vts_delta;
-  std::map< TypeNode, Node > d_vts_inf;
-  Node d_vts_delta_free;
-  std::map< TypeNode, Node > d_vts_inf_free;
-  /** get vts infinity index */
-  Node getVtsInfinityIndex( int i, bool isFree = false, bool create = true  );
-  /** substitute vts free terms */
-  Node substituteVtsFreeTerms( Node n );
 public:
-  /** get vts delta */
-  Node getVtsDelta( bool isFree = false, bool create = true );
-  /** get vts infinity */
-  Node getVtsInfinity( TypeNode tn, bool isFree = false, bool create = true );
-  /** get all vts terms */
-  void getVtsTerms( std::vector< Node >& t, bool isFree = false, bool create = true, bool inc_delta = true );
-  /** rewrite delta */
-  Node rewriteVtsSymbols( Node n );
-  /** simple check for contains term */
-  bool containsVtsTerm( Node n, bool isFree = false );
-  /** simple check for contains term */
-  bool containsVtsTerm( std::vector< Node >& n, bool isFree = false );
-  /** simple check for contains term */
-  bool containsVtsInfinity( Node n, bool isFree = false );
   /** ensure type */
   static Node ensureType( Node n, TypeNode tn );
   
 //general utilities
   // TODO #1216 : promote these?
  private:
-  //helper for contains term
-  static bool containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited );
   /** cache for getTypeValue */
   std::unordered_map<TypeNode,
                      std::unordered_map<int, Node>,
@@ -252,8 +189,6 @@ public:
       d_type_value_offset_status;
 
  public:
-  /** simple check for contains term, true if contains at least one term in t */
-  static bool containsTerms( Node n, std::vector< Node >& t );
   /** contains uninterpreted constant */
   static bool containsUninterpretedConstant( Node n );
   /** get the term depth of n */
@@ -360,23 +295,10 @@ public:
    * minimum and maximum elements, for example tn is Bool or BitVector.
    */
   static Node mkTypeConst(TypeNode tn, bool pol);
-
-  // for higher-order
- private:
-  /** dummy predicate that states terms should be considered first-class members of equality engine */
-  std::map< TypeNode, Node > d_ho_type_match_pred;
-public:
-  /** get higher-order type match predicate
-   * This predicate is used to force certain functions f of type tn to appear as first-class representatives in the
-   * quantifier-free UF solver. For a typical use case, we call getHoTypeMatchPredicate which returns a fresh 
-   * predicate P of type (tn -> Bool). Then, we add P( f ) as a lemma.  
-   * TODO: we may eliminate this depending on how github issue #1115 is resolved.
-   */
-  Node getHoTypeMatchPredicate( TypeNode tn );
 };/* class TermUtil */
 
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H */