From f65b945119341ae8afa69bd0b7dc005c9fcc768b Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 2 May 2016 09:16:30 -0500 Subject: Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, do not combine quantifier prefixes with annotations. Eliminate use of context-dependent attributes in quantifiers. --- src/theory/quantifiers/term_database.h | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) (limited to 'src/theory/quantifiers/term_database.h') diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 266d9b8fa..004292622 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -47,15 +47,6 @@ typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute; struct SynthesisAttributeId {}; typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute; -/** Attribute true for nodes that should not be used for matching */ -struct NoMatchAttributeId {}; -/** use the special for boolean flag */ -typedef expr::Attribute< NoMatchAttributeId, - bool, - expr::attr::NullCleanupStrategy, - true // context dependent - > NoMatchAttribute; - // attribute for "contains instantiation constants from" struct InstConstantAttributeId {}; typedef expr::Attribute InstConstantAttribute; @@ -179,6 +170,7 @@ class TermDb : public QuantifiersUtil { friend class ::CVC4::theory::quantifiers::ConjectureGenerator; friend class ::CVC4::theory::quantifiers::TermGenEnv; typedef context::CDHashMap NodeIntMap; + typedef context::CDHashMap NodeBoolMap; private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; @@ -211,6 +203,8 @@ private: std::map< Node, std::vector< Node > > d_op_map; /** map from type nodes to terms of that type */ std::map< TypeNode, std::vector< Node > > d_type_map; + /** inactive map */ + NodeBoolMap d_inactive_map; /** count number of non-redundant ground terms per operator */ std::map< Node, int > d_op_nonred_count; @@ -266,6 +260,9 @@ public: /** is entailed (incomplete check) */ bool isEntailed( TNode n, bool pol, EqualityQuery * qy = NULL ); bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy = NULL ); + /** is active */ + bool isTermActive( Node n ); + void setTermInactive( Node n ); /** has term */ bool hasTermCurrent( Node n, bool useMode = true ); /** is term eligble for instantiation? */ @@ -327,6 +324,7 @@ public: 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 ); -- cgit v1.2.3