summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/options/options_handler.cpp34
-rw-r--r--src/options/options_handler.h2
-rw-r--r--src/options/quantifiers_modes.h8
-rw-r--r--src/options/quantifiers_options4
-rw-r--r--src/theory/quantifiers/inst_strategy_cbqi.cpp42
-rw-r--r--src/theory/quantifiers/inst_strategy_cbqi.h2
-rw-r--r--src/theory/quantifiers/term_database.cpp15
-rw-r--r--src/theory/quantifiers/term_database.h5
-rw-r--r--src/theory/quantifiers_engine.cpp98
-rw-r--r--src/theory/quantifiers_engine.h4
-rw-r--r--src/theory/strings/theory_strings.cpp1
11 files changed, 137 insertions, 78 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index f214b032c..152e22f14 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -428,7 +428,7 @@ post \n\
";
const std::string OptionsHandler::s_macrosQuantHelp = "\
-Template modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\
+Modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\
\n\
all \n\
+ Infer definitions for functions, including those containing quantified formulas.\n\
@@ -442,7 +442,7 @@ ground-uf \n\
";
const std::string OptionsHandler::s_quantDSplitHelp = "\
-Template modes for quantifiers splitting, supported by --quant-split:\n\
+Modes for quantifiers splitting, supported by --quant-dsplit-mode:\n\
\n\
none \n\
+ Never split quantified formulas.\n\
@@ -455,6 +455,20 @@ agg \n\
\n\
";
+const std::string OptionsHandler::s_quantRepHelp = "\
+Modes for quantifiers representative selection, supported by --quant-rep-mode:\n\
+\n\
+ee \n\
++ Let equality engine choose representatives.\n\
+\n\
+first (default) \n\
++ Choose terms that appear first.\n\
+\n\
+depth \n\
++ Choose terms that are of minimal depth.\n\
+\n\
+";
+
theory::quantifiers::InstWhenMode OptionsHandler::stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException) {
if(optarg == "pre-full") {
return theory::quantifiers::INST_WHEN_PRE_FULL;
@@ -716,6 +730,22 @@ theory::quantifiers::QuantDSplitMode OptionsHandler::stringToQuantDSplitMode(std
}
}
+theory::quantifiers::QuantRepMode OptionsHandler::stringToQuantRepMode(std::string option, std::string optarg) throw(OptionException) {
+ if(optarg == "none" ) {
+ return theory::quantifiers::QUANT_REP_MODE_EE;
+ } else if(optarg == "first" || optarg == "default") {
+ return theory::quantifiers::QUANT_REP_MODE_FIRST;
+ } else if(optarg == "depth") {
+ return theory::quantifiers::QUANT_REP_MODE_DEPTH;
+ } else if(optarg == "help") {
+ puts(s_quantRepHelp.c_str());
+ exit(1);
+ } else {
+ throw OptionException(std::string("unknown option for --quant-rep-mode: `") +
+ optarg + "'. Try --quant-rep-mode help.");
+ }
+}
+
// theory/bv/options_handlers.h
void OptionsHandler::abcEnabledBuild(std::string option, bool value) throw(OptionException) {
#ifndef CVC4_USE_ABC
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index a2d67be60..720889ca2 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -101,6 +101,7 @@ public:
theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException);
theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException);
theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode(std::string option, std::string optarg) throw(OptionException);
+ theory::quantifiers::QuantRepMode stringToQuantRepMode(std::string option, std::string optarg) throw(OptionException);
// theory/bv/options_handlers.h
void abcEnabledBuild(std::string option, bool value) throw(OptionException);
@@ -201,6 +202,7 @@ public:
static const std::string s_literalMatchHelp;
static const std::string s_macrosQuantHelp;
static const std::string s_quantDSplitHelp;
+ static const std::string s_quantRepHelp;
static const std::string s_mbqiModeHelp;
static const std::string s_modelFormatHelp;
static const std::string s_prenexQuantModeHelp;
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 7395a9a30..8aa3756cc 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -172,6 +172,14 @@ enum QuantDSplitMode {
QUANT_DSPLIT_MODE_AGG,
};
+enum QuantRepMode {
+ /** let equality engine choose representatives */
+ QUANT_REP_MODE_EE,
+ /** default, choose representatives that appear first */
+ QUANT_REP_MODE_FIRST,
+ /** choose representatives that have minimal depth */
+ QUANT_REP_MODE_DEPTH,
+};
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index cba1423a0..58367f2e2 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -100,8 +100,8 @@ option instMaxLevel --inst-max-level=N int :read-write :default -1
maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)
option instLevelInputOnly --inst-level-input-only bool :default true
only input terms are assigned instantiation level zero
-option internalReps --quant-internal-reps bool :default true
- instantiate with representatives chosen by quantifiers engine
+option quantRepMode --quant-rep-mode=MODE CVC4::theory::quantifiers::QuantRepMode :default CVC4::theory::quantifiers::QUANT_REP_MODE_FIRST :read-write :include "options/quantifiers_modes.h" :handler stringToQuantRepMode
+ selection mode for representatives in quantifiers engine
option eagerInstQuant --eager-inst-quant bool :default false
apply quantifier instantiation eagerly
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index e6c9b9e6b..faad18c28 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -34,7 +34,9 @@ using namespace CVC4::theory::arith;
#define ARITH_INSTANTIATOR_USE_MINUS_DELTA
InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe )
- : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ), d_added_inst( qe->getUserContext() ) {
+ : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() )
+//, d_added_inst( qe->getUserContext() )
+{
}
InstStrategyCbqi::~InstStrategyCbqi() throw(){}
@@ -97,14 +99,6 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
}else{
Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl;
}
- //if doing partial quantifier elimination, do not process this if already processed once
- if( d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( q ) ){
- if( d_added_inst.find( q )!=d_added_inst.end() ){
- d_quantEngine->getModel()->setQuantifierActive( q, false );
- d_cbqi_set_quant_inactive = true;
- d_incomplete_check = true;
- }
- }
}
}
}
@@ -597,21 +591,23 @@ InstStrategyCegqi::~InstStrategyCegqi() throw () {
}
void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) {
- d_check_vts_lemma_lc = true;
+ d_check_vts_lemma_lc = false;
}
-void InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
+void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) {
if( e==0 ){
- CegInstantiator * cinst = getInstantiator( f );
- Trace("inst-alg") << "-> Run cegqi for " << f << std::endl;
- d_curr_quant = f;
+ CegInstantiator * cinst = getInstantiator( q );
+ Trace("inst-alg") << "-> Run cegqi for " << q << std::endl;
+ d_curr_quant = q;
if( !cinst->check() ){
d_incomplete_check = true;
+ d_check_vts_lemma_lc = true;
}
d_curr_quant = Node::null();
}else if( e==1 ){
//minimize the free delta heuristically on demand
if( d_check_vts_lemma_lc ){
+ Trace("inst-alg") << "-> Minimize delta heuristic, for " << q << std::endl;
d_check_vts_lemma_lc = false;
d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const );
d_small_const = Rewriter::rewrite( d_small_const );
@@ -635,13 +631,21 @@ void InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs ) {
Assert( !d_curr_quant.isNull() );
- //check if we need virtual term substitution (if used delta or infinity)
- bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false );
- if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, false, used_vts ) ){
- d_added_inst.insert( d_curr_quant );
+ //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma
+ if( d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( d_curr_quant ) ){
+ d_cbqi_set_quant_inactive = true;
+ d_incomplete_check = true;
+ d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false );
return true;
}else{
- return false;
+ //check if we need virtual term substitution (if used delta or infinity)
+ bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false );
+ if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, false, used_vts ) ){
+ //d_added_inst.insert( d_curr_quant );
+ return true;
+ }else{
+ return false;
+ }
}
}
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 8de844eb8..fd8afb149 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -40,7 +40,7 @@ protected:
/** whether we have added cbqi lemma */
NodeSet d_added_cbqi_lemma;
/** whether we have instantiated quantified formulas */
- NodeSet d_added_inst;
+ //NodeSet d_added_inst;
/** whether to do cbqi for this quantified formula */
std::map< Node, bool > d_do_cbqi;
/** register ce lemma */
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index cb23b8bb7..be0f60654 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1680,6 +1680,21 @@ bool TermDb::containsTerms( Node n, std::vector< Node >& t ) {
}
}
+int TermDb::getTermDepth( Node n ) {
+ if (!n.hasAttribute(TermDepthAttribute()) ){
+ int maxDepth = -1;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ int depth = getTermDepth( n[i] );
+ if( depth>maxDepth ){
+ maxDepth = depth;
+ }
+ }
+ TermDepthAttribute tda;
+ n.setAttribute(tda,1+maxDepth);
+ }
+ return n.getAttribute(TermDepthAttribute());
+}
+
bool TermDb::containsUninterpretedConstant( Node n ) {
std::map< Node, bool > visited;
return containsUninterpretedConstant2( n, visited );
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 5560098c9..b1cfcf2ae 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -68,6 +68,9 @@ 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 ModelBasisAttributeId {};
typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
//for APPLY_UF terms, 1 : term has direct child with model basis attribute,
@@ -436,6 +439,8 @@ public:
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 */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index bbc41278e..9568966d6 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -741,6 +741,24 @@ bool QuantifiersEngine::addInstantiationInternal( Node f, std::vector< Node >& v
}
}
+bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq, bool modInst ) {
+ if( options::incrementalSolving() ){
+ Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << ", modInst = " << modInst << std::endl;
+ inst::CDInstMatchTrie* imt;
+ std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q );
+ if( it!=d_c_inst_match_trie.end() ){
+ imt = it->second;
+ }else{
+ imt = new CDInstMatchTrie( getUserContext() );
+ d_c_inst_match_trie[q] = imt;
+ }
+ return imt->addInstMatch( this, q, terms, getUserContext(), modEq, modInst );
+ }else{
+ Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
+ return d_inst_match_trie[q].addInstMatch( this, q, terms, modEq, modInst );
+ }
+}
+
void QuantifiersEngine::setInstantiationLevelAttr( Node n, Node qn, uint64_t level ){
Trace("inst-level-debug2") << "IL : " << n << " " << qn << " " << level << std::endl;
//if not from the vector of terms we instantiatied
@@ -956,22 +974,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
}
//check for duplication
- bool alreadyExists = false;
- if( options::incrementalSolving() ){
- Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << ", modInst = " << modInst << std::endl;
- inst::CDInstMatchTrie* imt;
- std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q );
- if( it!=d_c_inst_match_trie.end() ){
- imt = it->second;
- }else{
- imt = new CDInstMatchTrie( getUserContext() );
- d_c_inst_match_trie[q] = imt;
- }
- alreadyExists = !imt->addInstMatch( this, q, terms, getUserContext(), modEq, modInst );
- }else{
- Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
- alreadyExists = !d_inst_match_trie[q].addInstMatch( this, q, terms, modEq, modInst );
- }
+ bool alreadyExists = !recordInstantiationInternal( q, terms, modEq, modInst );
if( alreadyExists ){
Trace("inst-add-debug") << " -> Already exists." << std::endl;
++(d_statistics.d_inst_duplicate_eq);
@@ -1260,27 +1263,27 @@ bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){
Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){
Assert( f.isNull() || f.getKind()==FORALL );
Node r = getRepresentative( a );
- if( !options::internalReps() ){
- return r;
- }else{
- if( options::finiteModelFind() ){
- if( r.isConst() ){
- //map back from values assigned by model, if any
- if( d_qe->getModel() ){
- std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r );
- if( it!=d_qe->getModel()->d_rep_set.d_values_to_terms.end() ){
- r = it->second;
- r = getRepresentative( r );
- }else{
- if( r.getType().isSort() ){
- Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
- //should never happen : UF constants should never escape model
- Assert( false );
- }
+ if( options::finiteModelFind() ){
+ if( r.isConst() ){
+ //map back from values assigned by model, if any
+ if( d_qe->getModel() ){
+ std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r );
+ if( it!=d_qe->getModel()->d_rep_set.d_values_to_terms.end() ){
+ r = it->second;
+ r = getRepresentative( r );
+ }else{
+ if( r.getType().isSort() ){
+ Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
+ //should never happen : UF constants should never escape model
+ Assert( false );
}
}
}
}
+ }
+ if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_EE ){
+ return r;
+ }else{
TypeNode v_tn = f.isNull() ? a.getType() : f[0][index].getType();
std::map< Node, Node >::iterator itir = d_int_rep[v_tn].find( r );
if( itir==d_int_rep[v_tn].end() ){
@@ -1320,7 +1323,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
if( d_rep_score.find( r_best )==d_rep_score.end() ){
d_rep_score[ r_best ] = d_reset_count;
}
- Trace("internal-rep-select") << "...Choose " << r_best << std::endl;
+ Trace("internal-rep-select") << "...Choose " << r_best << " with score " << r_best_score << std::endl;
Assert( r_best.getType().isSubtypeOf( v_tn ) );
d_int_rep[v_tn][r] = r_best;
if( r_best!=a ){
@@ -1446,23 +1449,6 @@ Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Nod
}
}
-/*
-int getDepth( Node n ){
- if( n.getNumChildren()==0 ){
- return 0;
- }else{
- int maxDepth = -1;
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- int depth = getDepth( n[i] );
- if( depth>maxDepth ){
- maxDepth = depth;
- }
- }
- return maxDepth;
- }
-}
-*/
-
//-2 : invalid, -1 : undesired, otherwise : smaller the score, the better
int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, TypeNode v_tn ){
if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){ //reject
@@ -1479,8 +1465,12 @@ int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, Type
return options::instLevelInputOnly() ? -1 : 0;
}
}else{
- //score prefers earliest use of this term as a representative
- return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
+ if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_FIRST ){
+ //score prefers earliest use of this term as a representative
+ return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
+ }else{
+ Assert( options::quantRepMode()==quantifiers::QUANT_REP_MODE_DEPTH );
+ return quantifiers::TermDb::getTermDepth( n );
+ }
}
- //return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n ); //term depth
}
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index c5c88487b..b9ce2063a 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -99,6 +99,7 @@ namespace quantifiers {
class QuantEqualityEngine;
class FullSaturation;
class InstStrategyCbqi;
+ class InstStrategyCegqi;
class QuantDSplit;
}/* CVC4::theory::quantifiers */
@@ -111,6 +112,7 @@ class EqualityQueryQuantifiersEngine;
class QuantifiersEngine {
friend class quantifiers::InstantiationEngine;
+ friend class quantifiers::InstStrategyCegqi;
friend class quantifiers::ModelEngine;
friend class quantifiers::RewriteEngine;
friend class quantifiers::QuantConflictFind;
@@ -292,6 +294,8 @@ private:
void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
/** instantiate f with arguments terms */
bool addInstantiationInternal( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false );
+ /** record instantiation, return true if it was non-duplicate */
+ bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool modInst = false );
/** set instantiation level attr */
static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level );
/** flush lemmas */
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index a4ebe5e97..175bd2c2a 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2027,6 +2027,7 @@ bool TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form
Trace("strings-entail") << " explanation was : " << et.second << std::endl;
conc = e==0 ? eq1 : eq2;
antec_new_lits.push_back( et.second );
+ break;
}
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback