Split term database (#1206)

* Move equality query to own file, move equality inference to quantifiers engine.

* Move quantifiers attributes out of TermDb and into QuantAttribute.

* Move term database sygus to quantifiers engine, move some attributes to quantifiers attributes header.

* Split term database into term util.

* Partial fix for #1205 that eliminates need for dependency in node.cpp.

* Add more references to github issues.

1 files changed, 8 insertions, 401 deletions

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 852d94fde..f4c6c3877 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -25,109 +25,9 @@
 #include "theory/type_enumerator.h"
 #include "theory/quantifiers/quant_util.h"
 
-
 namespace CVC4 {
 namespace theory {
 
-/** Attribute true for quantifiers that are axioms */
-struct AxiomAttributeId {};
-typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute;
-
-/** Attribute true for quantifiers that are conjecture */
-struct ConjectureAttributeId {};
-typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute;
-
-/** Attribute true for function definition quantifiers */
-struct FunDefAttributeId {};
-typedef expr::Attribute< FunDefAttributeId, bool > FunDefAttribute;
-
-/** Attribute true for quantifiers that are SyGus conjectures */
-struct SygusAttributeId {};
-typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute;
-
-/** Attribute true for quantifiers that are synthesis conjectures */
-struct SynthesisAttributeId {};
-typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute;
-
-// attribute for "contains instantiation constants from"
-struct InstConstantAttributeId {};
-typedef expr::Attribute<InstConstantAttributeId, Node> InstConstantAttribute;
-
-struct BoundVarAttributeId {};
-typedef expr::Attribute<BoundVarAttributeId, Node> BoundVarAttribute;
-
-struct InstLevelAttributeId {};
-typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
-
-struct InstVarNumAttributeId {};
-typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute;
-
-struct TermDepthAttributeId {};
-typedef expr::Attribute<TermDepthAttributeId, uint64_t> TermDepthAttribute;
-
-struct ContainsUConstAttributeId {};
-typedef expr::Attribute<ContainsUConstAttributeId, uint64_t> ContainsUConstAttribute;
-
-struct ModelBasisAttributeId {};
-typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
-//for APPLY_UF terms, 1 : term has direct child with model basis attribute,
-//                    0 : term has no direct child with model basis attribute.
-struct ModelBasisArgAttributeId {};
-typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute;
-
-//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 "contains instantiation constants from"
-struct SygusProxyAttributeId {};
-typedef expr::Attribute<SygusProxyAttributeId, Node> SygusProxyAttribute;
-
-// attribute for associating a synthesis function with a first order variable
-struct SygusSynthFunAttributeId {};
-typedef expr::Attribute<SygusSynthFunAttributeId, Node> SygusSynthFunAttribute;
-
-// 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 true for quantifiers that we are doing quantifier elimination on */
-struct QuantElimAttributeId {};
-typedef expr::Attribute< QuantElimAttributeId, bool > QuantElimAttribute;
-
-/** Attribute true for quantifiers that we are doing partial quantifier elimination on */
-struct QuantElimPartialAttributeId {};
-typedef expr::Attribute< QuantElimPartialAttributeId, bool > QuantElimPartialAttribute;
-
-/** Attribute for id number */
-struct QuantIdNumAttributeId {};
-typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute;
-
-/** sygus var num */
-struct SygusVarNumAttributeId {};
-typedef expr::Attribute<SygusVarNumAttributeId, uint64_t> SygusVarNumAttribute;
-
-/** Attribute to mark Skolems as virtual terms */
-struct VirtualTermSkolemAttributeId {};
-typedef expr::Attribute< VirtualTermSkolemAttributeId, bool > VirtualTermSkolemAttribute;
-
-
 class QuantifiersEngine;
 
 namespace inst{
@@ -151,29 +51,6 @@ public:
   void clear() { d_data.clear(); }
 };/* class TermArgTrie */
 
-
-class QAttributes{
-public:
-  QAttributes() : d_hasPattern(false), d_conjecture(false), d_axiom(false), d_sygus(false),
-                  d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false){}
-  ~QAttributes(){}
-  bool d_hasPattern;
-  Node d_rr;
-  bool d_conjecture;
-  bool d_axiom;
-  Node d_fundef_f;
-  bool d_sygus;
-  bool d_synthesis;
-  int d_rr_priority;
-  int d_qinstLevel;
-  bool d_quant_elim;
-  bool d_quant_elim_partial;
-  Node d_ipl;
-  Node d_qid_num;
-  bool isRewriteRule() { return !d_rr.isNull(); }
-  bool isFunDef() { return !d_fundef_f.isNull(); }
-};
-
 namespace fmcheck {
   class FullModelChecker;
 }
@@ -208,25 +85,23 @@ private:
   std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
   /** whether master equality engine is UF-inconsistent */
   bool d_consistent_ee;
-
- public:
-  TermDb(context::Context* c, context::UserContext* u, QuantifiersEngine* qe);
-  ~TermDb();
   /** boolean terms */
   Node d_true;
   Node d_false;
-  /** constants */
-  Node d_zero;
-  Node d_one;
-
- public:
+public:
+  TermDb(context::Context* c, context::UserContext* u, QuantifiersEngine* qe);
+  ~TermDb();
+  
+  /** register quantified formula */
+  void registerQuantifier( Node q );
+public:
   /** presolve (called once per user check-sat) */
   void presolve();
   /** reset (calculate which terms are active) */
   bool reset( Theory::Effort effort );
   /** identify */
   std::string identify() const { return "TermDb"; }  
- private:
+private:
   /** map from operators to ground terms for that operator */
   std::map< Node, std::vector< Node > > d_op_map;
   /** map from type nodes to terms of that type */
@@ -330,275 +205,7 @@ public:
   Node getModelBasis( Node q, Node n );
   //get model basis body
   Node getModelBasisBody( Node q );
-
-//for inst constant
-private:
-  /** map from universal quantifiers to the list of variables */
-  std::map< Node, std::vector< Node > > d_vars;
-  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;
-  /** make instantiation constants for */
-  void makeInstantiationConstantsFor( Node q );
-public:
-  /** map from universal quantifiers to the list of instantiation constants */
-  std::map< Node, std::vector< Node > > d_inst_constants;
-  /** get variable number */
-  unsigned getVariableNum( Node q, Node v ) { return d_var_num[q][v]; }
-  /** get the i^th instantiation constant of q */
-  Node getInstantiationConstant( Node q, int i ) const;
-  /** get number of instantiation constants for q */
-  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
-      return a pattern where the variable are replaced by variable for
-      instantiation.
-   */
-  Node getInstConstantNode( Node n, Node q );
-  Node getVariableNode( Node n, Node q );
-  /** get substituted node */
-  Node getInstantiatedNode( Node n, Node q, std::vector< Node >& terms );
-
-  static Node getInstConstAttr( Node n );
-  static bool hasInstConstAttr( Node n );
-  static Node getBoundVarAttr( Node n );
-  static bool hasBoundVarAttr( Node n );
   
-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)
-  static Node getQuantSimplify( Node n );
-
-//for skolem
-private:
-  /** map from universal quantifiers to their skolemized body */
-  std::map< Node, Node > d_skolem_body;
-public:
-  /** map from universal quantifiers to the list of skolem constants */
-  std::map< Node, std::vector< Node > > d_skolem_constants;
-  /** make the skolemized body f[e/x] */
-  static Node mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs,
-                                std::vector< Node >& sk, Node& sub, std::vector< unsigned >& sub_vars );
-  /** get the skolemized body */
-  Node getSkolemizedBody( Node f);
-  /** is induction variable */
-  static bool isInductionTerm( Node n );
-
-//for ground term enumeration
-private:
-  /** ground terms enumerated for types */
-  std::map< TypeNode, std::vector< Node > > d_enum_terms;
-  //type enumerators
-  std::map< TypeNode, unsigned > d_typ_enum_map;
-  std::vector< TypeEnumerator > d_typ_enum;
-  // closed enumerable type cache
-  std::map< TypeNode, bool > d_typ_closed_enum;
-  /** may complete */
-  std::map< TypeNode, bool > d_may_complete;
-public:
-  //get nth term for type
-  Node getEnumerateTerm( TypeNode tn, unsigned index );
-  //does this type have an enumerator that produces constants that are handled by ground theory solvers
-  bool isClosedEnumerableType( TypeNode tn );
-  // may complete
-  bool mayComplete( TypeNode tn );
-
-//for triggers
-private:
-  /** helper function for compute var contains */
-  static void computeVarContains2( Node n, Kind k, std::vector< Node >& varContains, std::map< Node, bool >& visited );
-  /** triggers for each operator */
-  std::map< Node, std::vector< inst::Trigger* > > d_op_triggers;
-  /** helper for is instance of */
-  static bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs );
-  /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
-  static int isInstanceOf2( Node n1, Node n2, std::vector< Node >& varContains1, std::vector< Node >& varContains2 );
-public:
-  /** compute var contains */
-  static void computeVarContains( Node n, std::vector< Node >& varContains );
-  /** get var contains for each of the patterns in pats */
-  static void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains );
-  /** get var contains for node n */
-  static void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains );
-  /** compute quant contains */
-  static void computeQuantContains( Node n, std::vector< Node >& quantContains );
-  /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
-  static int isInstanceOf( Node n1, Node n2 );
-  /** filter all nodes that have instances */
-  static void filterInstances( std::vector< Node >& nodes );
-  /** register trigger (for eager quantifier instantiation) */
-  void registerTrigger( inst::Trigger* tr, Node op );
-
-//for term ordering
-private:
-  /** operator id count */
-  int d_op_id_count;
-  /** map from operators to id */
-  std::map< Node, int > d_op_id;
-  /** type id count */
-  int d_typ_id_count;
-  /** map from type to id */
-  std::map< TypeNode, int > d_typ_id;
-  //free variables
-  std::map< TypeNode, std::vector< Node > > d_cn_free_var;
-  // get canonical term, return null if it contains a term apart from handled signature
-  Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder, 
-                         std::map< TNode, Node >& visited );
-public:
-  /** get id for operator */
-  int getIdForOperator( Node op );
-  /** get id for type */
-  int getIdForType( TypeNode t );
-  /** get term order */
-  bool getTermOrder( Node a, Node b );
-  /** get canonical free variable #i of type tn */
-  Node getCanonicalFreeVar( TypeNode tn, unsigned i );
-  /** get canonical term */
-  Node getCanonicalTerm( TNode n, bool apply_torder = false );
-
-//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 );
-  /** get relevancy condition */
-  static void getRelevancyCondition( Node n, std::vector< Node >& cond );
-private:
-  //helper for contains term
-  static bool containsTerm2( Node n, Node t, std::map< Node, bool >& visited );
-  static bool containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited );
-//general utilities
-public:
-  /** simple check for whether n contains t as subterm */
-  static bool containsTerm( Node n, Node t );
-  /** 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 */
-  static int getTermDepth( Node n );
-  /** simple negate */
-  static Node simpleNegate( Node n );
-  /** is assoc */
-  static bool isAssoc( Kind k );
-  /** is comm */
-  static bool isComm( Kind k );
-  /** ( x k ... ) k x = ( x k ... ) */
-  static bool isNonAdditive( Kind k );
-  /** is bool connective */
-  static bool isBoolConnective( Kind k );
-  /** is bool connective term */
-  static bool isBoolConnectiveTerm( TNode n );
-
-//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 );
-
-//for sygus
-private:
-  TermDbSygus * d_sygus_tdb;
-public:
-  TermDbSygus * getTermDatabaseSygus() { return d_sygus_tdb; }
-
-private:
-  std::map< Node, bool > d_fun_defs;
-public: //general queries concerning quantified formulas wrt modules
-  /** is quantifier treated as a rewrite rule? */
-  static bool isRewriteRule( Node q );
-  /** get the rewrite rule associated with the quanfied formula */
-  static Node getRewriteRule( Node q );
-  /** is fun def */
-  static bool isFunDef( Node q );
-  /** is fun def */
-  static bool isFunDefAnnotation( Node ipl );
-  /** is sygus conjecture */
-  static bool isSygusConjecture( Node q );
-  /** is sygus conjecture */
-  static bool isSygusConjectureAnnotation( Node ipl );
-  /** get fun def body */
-  static Node getFunDefHead( Node q );
-  /** get fun def body */
-  static Node getFunDefBody( Node q );
-  /** is quant elim annotation */
-  static bool isQuantElimAnnotation( Node ipl );
-//attributes
-private:
-  std::map< Node, QAttributes > d_qattr;
-  //record attributes
-  void computeAttributes( Node q );
-public:
-  /** is conjecture */
-  bool isQAttrConjecture( Node q );
-  /** is axiom */
-  bool isQAttrAxiom( Node q );
-  /** is function definition */
-  bool isQAttrFunDef( Node q );
-  /** is sygus conjecture */
-  bool isQAttrSygus( Node q );
-  /** is synthesis conjecture */
-  bool isQAttrSynthesis( Node q );
-  /** get instantiation level */
-  int getQAttrQuantInstLevel( Node q );
-  /** get rewrite rule priority */
-  int getQAttrRewriteRulePriority( Node q );
-  /** is quant elim */
-  bool isQAttrQuantElim( Node q );
-  /** is quant elim partial */
-  bool isQAttrQuantElimPartial( Node q );
-  /** get quant id num */
-  int getQAttrQuantIdNum( Node q );
-  /** get quant id num */
-  Node getQAttrQuantIdNumNode( Node q );
-  /** compute quantifier attributes */
-  static void computeQuantAttributes( Node q, QAttributes& qa );
 };/* class TermDb */
 
 }/* CVC4::theory::quantifiers namespace */