#include "theory/quantifiers_engine.h"
#include "theory/theory_engine.h"
#include "theory/uf/equality_engine.h"
+#include "util/hash.h"
+
using namespace std;
-using namespace CVC4;
using namespace CVC4::kind;
using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::inst;
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
/** trigger class constructor */
-Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool smartTriggers ) :
-d_quantEngine( qe ), d_f( f ){
+Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes,
+ int matchOption, bool smartTriggers )
+ : d_quantEngine( qe ), d_f( f )
+{
d_nodes.insert( d_nodes.begin(), nodes.begin(), nodes.end() );
Trace("trigger") << "Trigger for " << f << ": " << std::endl;
for( int i=0; i<(int)d_nodes.size(); i++ ){
Trace("trigger-debug") << "Finished making trigger." << std::endl;
}
+Trigger::~Trigger() {
+ if(d_mg != NULL) { delete d_mg; }
+}
+
void Trigger::resetInstantiationRound(){
d_mg->resetInstantiationRound( d_quantEngine );
}
void TriggerTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){
if( nodes.empty() ){
+ if(d_tr != NULL){
+ // TODO: Andy can you look at fmf/QEpres-uf.855035.smt?
+ delete d_tr;
+ d_tr = NULL;
+ }
+ Assert(d_tr == NULL);
d_tr = t;
}else{
Node n = nodes.back();
d_children[n]->addTrigger2( nodes, t );
}
}
+
+
+TriggerTrie::TriggerTrie()
+ : d_tr( NULL )
+{}
+
+TriggerTrie::~TriggerTrie() {
+ for(std::map< TNode, TriggerTrie* >::iterator i = d_children.begin(), iend = d_children.end();
+ i != iend; ++i) {
+ TriggerTrie* current = (*i).second;
+ delete current;
+ }
+ d_children.clear();
+
+ if(d_tr != NULL) { delete d_tr; }
+}
+
+}/* CVC4::theory::inst namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
#ifndef __CVC4__THEORY__QUANTIFIERS__TRIGGER_H
#define __CVC4__THEORY__QUANTIFIERS__TRIGGER_H
-#include "theory/quantifiers/inst_match.h"
-#include "expr/node.h"
-#include "util/hash.h"
#include <map>
+#include "expr/node.h"
+#include "theory/quantifiers/inst_match.h"
+
+// Forward declarations for defining the Trigger and TriggerTrie.
namespace CVC4 {
namespace theory {
class IMGenerator;
class InstMatchGenerator;
+}/* CVC4::theory::inst namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
-//a collect of nodes representing a trigger
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+/** A collect of nodes representing a trigger. */
class Trigger {
-private:
- /** the quantifiers engine */
- QuantifiersEngine* d_quantEngine;
- /** the quantifier this trigger is for */
- Node d_f;
- /** match generators */
- IMGenerator* d_mg;
-private:
- /** trigger constructor */
- Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, int matchOption = 0, bool smartTriggers = false );
-public:
- ~Trigger(){}
-public:
- std::vector< Node > d_nodes;
-public:
+ public:
+ ~Trigger();
+
IMGenerator* getGenerator() { return d_mg; }
-public:
- /** reset instantiation round (call this whenever equivalence classes have changed) */
+
+ /** reset instantiation round (call this whenever equivalence
+ * classes have changed) */
void resetInstantiationRound();
- /** reset, eqc is the equivalence class to search in (search in any if eqc=null) */
+ /** reset, eqc is the equivalence class to search in (search in any
+ * if eqc=null) */
void reset( Node eqc );
/** get next match. must call reset( eqc ) once before this function. */
bool getNextMatch( Node f, InstMatch& m );
int addTerm( Node t );
/** return whether this is a multi-trigger */
bool isMultiTrigger() { return d_nodes.size()>1; }
-public:
+
/** add all available instantiations exhaustively, in any equivalence class
if limitInst>0, limitInst is the max # of instantiations to try */
int addInstantiations( InstMatch& baseMatch );
ie : quantifier engine;
f : forall something ....
nodes : (multi-)trigger
- matchOption : which policy to use for creating matches (one of InstMatchGenerator::MATCH_GEN_* )
+ matchOption : which policy to use for creating matches
+ (one of InstMatchGenerator::MATCH_GEN_* )
keepAll: don't remove unneeded patterns;
- trOption : policy for dealing with triggers that already existed (see below)
+ trOption : policy for dealing with triggers that already existed
+ (see below)
*/
enum{
TR_MAKE_NEW, //make new trigger even if it already may exist
TR_GET_OLD, //return a previous trigger if it had already been created
TR_RETURN_NULL //return null if a duplicate is found
};
- static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes,
- int matchOption = 0, bool keepAll = true, int trOption = TR_MAKE_NEW,
+ static Trigger* mkTrigger( QuantifiersEngine* qe, Node f,
+ std::vector< Node >& nodes, int matchOption = 0,
+ bool keepAll = true, int trOption = TR_MAKE_NEW,
bool smartTriggers = false );
static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n,
- int matchOption = 0, bool keepAll = true, int trOption = TR_MAKE_NEW,
+ int matchOption = 0, bool keepAll = true,
+ int trOption = TR_MAKE_NEW,
bool smartTriggers = false );
-private:
- /** is subterm of trigger usable */
- static bool isUsable( Node n, Node q );
- static Node getIsUsableTrigger( Node n, Node f, bool pol = true, bool hasPol = false );
- /** collect all APPLY_UF pattern terms for f in n */
- static bool collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol );
-public:
//different strategies for choosing trigger terms
enum {
TS_MAX_TRIGGER = 0,
TS_MIN_TRIGGER,
TS_ALL,
};
- static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, bool filterInst = false );
-public:
+ static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n,
+ std::vector< Node >& patTerms, int tstrt,
+ std::vector< Node >& exclude,
+ bool filterInst = false );
/** is usable trigger */
static bool isUsableTrigger( Node n, Node q );
static bool isAtomicTrigger( Node n );
static bool isBooleanTermTrigger( Node n );
static bool isPureTheoryTrigger( Node n );
static int getTriggerWeight( Node n );
- static bool isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms );
+ static bool isLocalTheoryExt( Node n, std::vector< Node >& vars,
+ std::vector< Node >& patTerms );
/** return data structure for producing matches for this trigger. */
static InstMatchGenerator* getInstMatchGenerator( Node q, Node n );
static Node getInversionVariable( Node n );
static Node getInversion( Node n, Node x );
/** get all variables that E-matching can possibly handle */
- static void getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f, std::vector< Node >& t_vars );
+ static void getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f,
+ std::vector< Node >& t_vars );
void debugPrint( const char * c ) {
Trace(c) << "TRIGGER( ";
}
Trace(c) << " )";
}
-};
+
+private:
+ /** trigger constructor */
+ Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes,
+ int matchOption = 0, bool smartTriggers = false );
+
+ /** is subterm of trigger usable */
+ static bool isUsable( Node n, Node q );
+ static Node getIsUsableTrigger( Node n, Node f, bool pol = true,
+ bool hasPol = false );
+ /** collect all APPLY_UF pattern terms for f in n */
+ static bool collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap,
+ int tstrt, std::vector< Node >& exclude,
+ bool pol, bool hasPol );
+
+ std::vector< Node > d_nodes;
+
+ /** the quantifiers engine */
+ QuantifiersEngine* d_quantEngine;
+ /** the quantifier this trigger is for */
+ Node d_f;
+ /** match generators */
+ IMGenerator* d_mg;
+}; /* class Trigger */
/** a trie of triggers */
class TriggerTrie {
-private:
- inst::Trigger* getTrigger2( std::vector< Node >& nodes );
- void addTrigger2( std::vector< Node >& nodes, inst::Trigger* t );
public:
- TriggerTrie() : d_tr( NULL ){}
- inst::Trigger* d_tr;
- std::map< TNode, TriggerTrie* > d_children;
+ TriggerTrie();
+ ~TriggerTrie();
+
inst::Trigger* getTrigger( std::vector< Node >& nodes ){
std::vector< Node > temp;
temp.insert( temp.begin(), nodes.begin(), nodes.end() );
std::sort( temp.begin(), temp.end() );
return addTrigger2( temp, t );
}
-};/* class inst::Trigger::Trigger */
+private:
+ inst::Trigger* getTrigger2( std::vector< Node >& nodes );
+ void addTrigger2( std::vector< Node >& nodes, inst::Trigger* t );
+
+ inst::Trigger* d_tr;
+ std::map< TNode, TriggerTrie* > d_children;
+};/* class inst::Trigger::TriggerTrie */
}/* CVC4::theory::inst namespace */
}/* CVC4::theory namespace */
projects / cvc5.git / commitdiff