From 4f506ac50e43a71a92094a478deeaa2c2cd1df4a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 23 Mar 2018 13:33:12 -0500 Subject: [PATCH] Minor reorganization for ematching (#1701) --- src/Makefile.am | 4 +- .../{ => ematching}/candidate_generator.cpp | 2 +- .../{ => ematching}/candidate_generator.h | 0 .../ematching/inst_match_generator.cpp | 44 +------------------ .../ematching/inst_match_generator.h | 26 ----------- src/theory/quantifiers/ematching/trigger.cpp | 23 ++-------- src/theory/quantifiers/ematching/trigger.h | 2 - 7 files changed, 8 insertions(+), 93 deletions(-) rename src/theory/quantifiers/{ => ematching}/candidate_generator.cpp (99%) rename src/theory/quantifiers/{ => ematching}/candidate_generator.h (100%) diff --git a/src/Makefile.am b/src/Makefile.am index c6f8a7ad1..6395a70bc 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -366,8 +366,6 @@ libcvc4_la_SOURCES = \ theory/quantifiers/anti_skolem.h \ theory/quantifiers/bv_inverter.cpp \ theory/quantifiers/bv_inverter.h \ - theory/quantifiers/candidate_generator.cpp \ - theory/quantifiers/candidate_generator.h \ theory/quantifiers/cegqi/ceg_instantiator.cpp \ theory/quantifiers/cegqi/ceg_instantiator.h \ theory/quantifiers/cegqi/ceg_t_instantiator.cpp \ @@ -378,6 +376,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/conjecture_generator.h \ theory/quantifiers/dynamic_rewrite.cpp \ theory/quantifiers/dynamic_rewrite.h \ + theory/quantifiers/ematching/candidate_generator.cpp \ + theory/quantifiers/ematching/candidate_generator.h \ theory/quantifiers/ematching/ho_trigger.cpp \ theory/quantifiers/ematching/ho_trigger.h \ theory/quantifiers/ematching/inst_match_generator.cpp \ diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp similarity index 99% rename from src/theory/quantifiers/candidate_generator.cpp rename to src/theory/quantifiers/ematching/candidate_generator.cpp index 699a93286..ea5e8592d 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -12,7 +12,7 @@ ** \brief Implementation of theory uf candidate generator class **/ -#include "theory/quantifiers/candidate_generator.h" +#include "theory/quantifiers/ematching/candidate_generator.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/inst_match.h" #include "theory/quantifiers/instantiate.h" diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h similarity index 100% rename from src/theory/quantifiers/candidate_generator.h rename to src/theory/quantifiers/ematching/candidate_generator.h diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index c36597e3e..ec0a4039a 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -17,11 +17,11 @@ #include "expr/datatype.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/candidate_generator.h" +#include "theory/quantifiers/ematching/candidate_generator.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers_engine.h" using namespace std; @@ -541,14 +541,6 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Node q, Node n) } Trace("var-trigger-debug") << "Is " << n << " a variable trigger?" << std::endl; - if (Trigger::isBooleanTermTrigger(n)) - { - VarMatchGeneratorBooleanTerm* vmg = - new VarMatchGeneratorBooleanTerm(n[0], n[1]); - Trace("var-trigger") << "Boolean term trigger : " << n << ", var = " << n[0] - << std::endl; - return vmg; - } Node x; if (options::purifyTriggers()) { @@ -565,38 +557,6 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Node q, Node n) return new InstMatchGenerator(n); } -VarMatchGeneratorBooleanTerm::VarMatchGeneratorBooleanTerm( Node var, Node comp ) : - InstMatchGenerator(), d_comp( comp ), d_rm_prev( false ) { - d_children_types.push_back(var.getAttribute(InstVarNumAttribute())); -} - -int VarMatchGeneratorBooleanTerm::getNextMatch(Node q, - InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent) -{ - int ret_val = -1; - if( !d_eq_class.isNull() ){ - Node s = NodeManager::currentNM()->mkConst(qe->getEqualityQuery()->areEqual( d_eq_class, d_pattern )); - d_eq_class = Node::null(); - d_rm_prev = m.get(d_children_types[0]).isNull(); - if (!m.set(qe->getEqualityQuery(), d_children_types[0], s)) - { - return -1; - }else{ - ret_val = continueNextMatch(q, m, qe, tparent); - if( ret_val>0 ){ - return ret_val; - } - } - } - if( d_rm_prev ){ - m.d_vals[d_children_types[0]] = Node::null(); - d_rm_prev = false; - } - return ret_val; -} - VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs( Node var, Node subs ) : InstMatchGenerator(), d_var( var ), d_subs( subs ), d_rm_prev( false ){ d_children_types.push_back(d_var.getAttribute(InstVarNumAttribute())); diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index 6c38db13b..cbd5702a0 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -418,32 +418,6 @@ class InstMatchGenerator : public IMGenerator { static InstMatchGenerator* getInstMatchGenerator(Node q, Node n); };/* class InstMatchGenerator */ -/** match generator for Boolean term ITEs -* This handles the special case of triggers that look like ite( x, BV1, BV0 ). -*/ -class VarMatchGeneratorBooleanTerm : public InstMatchGenerator { -public: - VarMatchGeneratorBooleanTerm( Node var, Node comp ); - - /** Reset */ - bool reset(Node eqc, QuantifiersEngine* qe) override - { - d_eq_class = eqc; - return true; - } - /** Get the next match. */ - int getNextMatch(Node q, - InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent) override; - - private: - /** stores the true branch of the Boolean ITE */ - Node d_comp; - /** stores whether we have written a value for var in the current match. */ - bool d_rm_prev; -}; - /** match generator for purified terms * This handles the special case of invertible terms like x+1 (see * Trigger::getTermInversionVariable). diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 430d261a1..4039c632f 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -15,7 +15,7 @@ #include "theory/quantifiers/ematching/trigger.h" #include "theory/arith/arith_msum.h" -#include "theory/quantifiers/candidate_generator.h" +#include "theory/quantifiers/ematching/candidate_generator.h" #include "theory/quantifiers/ematching/ho_trigger.h" #include "theory/quantifiers/ematching/inst_match_generator.h" #include "theory/quantifiers/instantiate.h" @@ -262,9 +262,8 @@ bool Trigger::isUsable( Node n, Node q ){ return true; }else{ std::map< Node, Node > coeffs; - if( isBooleanTermTrigger( n ) ){ - return true; - }else if( options::purifyTriggers() ){ + if (options::purifyTriggers()) + { Node x = getInversionVariable( n ); if( !x.isNull() ){ return true; @@ -522,22 +521,6 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod } } -bool Trigger::isBooleanTermTrigger( Node n ) { - if( n.getKind()==ITE ){ - //check for boolean term converted to ITE - if( n[0].getKind()==INST_CONSTANT && - n[1].getKind()==CONST_BITVECTOR && - n[2].getKind()==CONST_BITVECTOR ){ - if( ((BitVectorType)n[1].getType().toType()).getSize()==1 && - n[1].getConst().toInteger()==1 && - n[2].getConst().toInteger()==0 ){ - return true; - } - } - } - return false; -} - bool Trigger::isPureTheoryTrigger( Node n ) { if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){ //|| !quantifiers::TermUtil::hasInstConstAttr( n ) ){ return false; diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index cd10e4f8a..28d227bf7 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -315,8 +315,6 @@ class Trigger { static bool isRelationalTriggerKind( Kind k ); /** is n a simple trigger (see inst_match_generator.h)? */ static bool isSimpleTrigger( Node n ); - /** is n a Boolean term trigger, e.g. ite( x, BV1, BV0 )? */ - static bool isBooleanTermTrigger( Node n ); /** is n a pure theory trigger, e.g. head( x )? */ static bool isPureTheoryTrigger( Node n ); /** get trigger weight -- 2.30.2