From 0f69a8ba2286bd5d9b807c10ad350705952e93d6 Mon Sep 17 00:00:00 2001 From: Tim King Date: Sun, 3 Apr 2016 19:38:06 -0700 Subject: Updating the copyright headers and scripts. --- src/theory/quantifiers/instantiation_engine.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'src/theory/quantifiers/instantiation_engine.cpp') diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 88a67e3c8..f98ab2b7c 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file instantiation_engine.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Andrew Reynolds - ** Minor contributors (to current version): Tim King + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Implementation of instantiation engine class **/ -- cgit v1.2.3 From 576d50ac7c13233a589771401537b587eb36361e Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 4 Apr 2016 17:18:36 -0500 Subject: New options for trigger selection, add option --strict-triggers. Do not infer alpha equivalence for quantifiers with annotations, limit rewrite operations when triggers are trusted. --- src/options/options_handler.cpp | 18 ++++-- src/options/quantifiers_modes.h | 4 ++ src/options/quantifiers_options | 6 +- src/smt/smt_engine.cpp | 5 ++ src/theory/quantifiers/alpha_equivalence.cpp | 17 ++++-- .../quantifiers/inst_strategy_e_matching.cpp | 22 +++----- src/theory/quantifiers/inst_strategy_e_matching.h | 3 +- src/theory/quantifiers/instantiation_engine.cpp | 16 ++++++ src/theory/quantifiers/instantiation_engine.h | 1 + src/theory/quantifiers/model_builder.cpp | 2 +- src/theory/quantifiers/quantifiers_rewriter.cpp | 17 +++--- src/theory/quantifiers/term_database.cpp | 12 ++-- src/theory/quantifiers/term_database.h | 3 +- src/theory/quantifiers/trigger.cpp | 64 +++++++++------------- src/theory/quantifiers/trigger.h | 20 ++----- src/theory/quantifiers_engine.cpp | 11 ++-- src/theory/quantifiers_engine.h | 3 +- 17 files changed, 126 insertions(+), 98 deletions(-) (limited to 'src/theory/quantifiers/instantiation_engine.cpp') diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 90202d6f5..d08f5f533 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -347,15 +347,21 @@ interleave \n\ const std::string OptionsHandler::s_triggerSelModeHelp = "\ Trigger selection modes currently supported by the --trigger-sel option:\n\ \n\ -default \n\ -+ Default, consider all subterms of quantified formulas for trigger selection.\n\ -\n\ -min \n\ +min | default \n\ + Consider only minimal subterms that meet criteria for triggers.\n\ \n\ max \n\ + Consider only maximal subterms that meet criteria for triggers. \n\ \n\ +all \n\ ++ Consider all subterms that meet criteria for triggers. \n\ +\n\ +min-s-max \n\ ++ Consider only minimal subterms that meet criteria for single triggers, maximal otherwise. \n\ +\n\ +min-s-all \n\ ++ Consider only minimal subterms that meet criteria for single triggers, all otherwise. \n\ +\n\ "; const std::string OptionsHandler::s_prenexQuantModeHelp = "\ Prenex quantifiers modes currently supported by the --prenex-quant option:\n\ @@ -608,6 +614,10 @@ theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(std:: return theory::quantifiers::TRIGGER_SEL_MIN; } else if(optarg == "max") { return theory::quantifiers::TRIGGER_SEL_MAX; + } else if(optarg == "min-s-max") { + return theory::quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX; + } else if(optarg == "min-s-all") { + return theory::quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL; } else if(optarg == "all") { return theory::quantifiers::TRIGGER_SEL_ALL; } else if(optarg == "help") { diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 8ecf65a33..a437cfc97 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -107,6 +107,10 @@ enum TriggerSelMode { TRIGGER_SEL_MIN, /** only consider maximal terms for triggers */ TRIGGER_SEL_MAX, + /** consider minimal terms for single triggers, maximal for non-single */ + TRIGGER_SEL_MIN_SINGLE_MAX, + /** consider minimal terms for single triggers, all for non-single */ + TRIGGER_SEL_MIN_SINGLE_ALL, /** consider all terms for triggers */ TRIGGER_SEL_ALL, }; diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 5f23a02e0..8ed4f24c0 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -69,8 +69,8 @@ option inferArithTriggerEq --infer-arith-trigger-eq bool :default false option inferArithTriggerEqExp --infer-arith-trigger-eq-exp bool :default false record explanations for inferArithTriggerEq -option smartTriggers --smart-triggers bool :default true - enable smart triggers +option strictTriggers --strict-triggers bool :default false + only instantiate quantifiers with user patterns based on triggers option relevantTriggers --relevant-triggers bool :default false prefer triggers that are more relevant based on SInE style analysis option relationalTriggers --relational-triggers bool :default false @@ -89,7 +89,7 @@ option multiTriggerPriority --multi-trigger-priority bool :default false only try multi triggers if single triggers give no instantiations option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_DEFAULT :read-write :include "options/quantifiers_modes.h" :handler stringToTriggerSelMode selection mode for triggers -option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :include "options/quantifiers_modes.h" :handler stringToUserPatMode +option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :read-write :include "options/quantifiers_modes.h" :handler stringToUserPatMode policy for handling user-provided patterns for quantifier instantiation option incrementTriggers --increment-triggers bool :default true generate additional triggers as needed during search diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ddbb9eef7..bff8e187f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1846,6 +1846,11 @@ void SmtEngine::setDefaults() { } } //implied options... + if( options::strictTriggers() ){ + if( !options::userPatternsQuant.wasSetByUser() ){ + options::userPatternsQuant.set( quantifiers::USER_PAT_MODE_TRUST ); + } + } if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){ options::quantConflictFind.set( true ); } diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index 16a9d3bc7..8abc3f65a 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -54,12 +54,17 @@ bool AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersE aen->d_quant = q; return true; }else{ - //lemma ( q <=> d_quant ) - Trace("quant-ae") << "Alpha equivalent : " << std::endl; - Trace("quant-ae") << " " << q << std::endl; - Trace("quant-ae") << " " << aen->d_quant << std::endl; - qe->getOutputChannel().lemma( q.iffNode( aen->d_quant ) ); - return false; + if( q.getNumChildren()==2 ){ + //lemma ( q <=> d_quant ) + Trace("quant-ae") << "Alpha equivalent : " << std::endl; + Trace("quant-ae") << " " << q << std::endl; + Trace("quant-ae") << " " << aen->d_quant << std::endl; + qe->getOutputChannel().lemma( q.iffNode( aen->d_quant ) ); + return false; + }else{ + //do not reduce annotated quantified formulas based on alpha equivalence + return true; + } } } diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index d43d7a792..491da7116 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -13,8 +13,6 @@ **/ #include "theory/quantifiers/inst_strategy_e_matching.h" - -#include "options/quantifiers_options.h" #include "theory/quantifiers/inst_match_generator.h" #include "theory/quantifiers/relevant_domain.h" #include "theory/quantifiers/term_database.h" @@ -85,7 +83,7 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){ if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){ int matchOption = 0; for( unsigned i=0; igetInstUserPatMode()==USER_PAT_MODE_RESORT ){ d_user_gen_wait[q].push_back( nodes ); }else{ - d_user_gen[q].push_back( Trigger::mkTrigger( d_quantEngine, q, nodes, matchOption, true, Trigger::TR_MAKE_NEW, options::smartTriggers() ) ); + d_user_gen[q].push_back( Trigger::mkTrigger( d_quantEngine, q, nodes, matchOption, true, Trigger::TR_MAKE_NEW ) ); } } } InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe ) : InstStrategy( qe ){ //how to select trigger terms - if( options::triggerSelMode()==TRIGGER_SEL_MIN || options::triggerSelMode()==TRIGGER_SEL_DEFAULT ){ - d_tr_strategy = Trigger::TS_MIN_TRIGGER; - }else if( options::triggerSelMode()==TRIGGER_SEL_MAX ){ - d_tr_strategy = Trigger::TS_MAX_TRIGGER; + if( options::triggerSelMode()==quantifiers::TRIGGER_SEL_DEFAULT ){ + d_tr_strategy = quantifiers::TRIGGER_SEL_MIN; }else{ - d_tr_strategy = Trigger::TS_ALL; + d_tr_strategy = options::triggerSelMode(); } //whether to select new triggers during the search if( options::incrementTriggers() ){ @@ -358,7 +354,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ int matchOption = 0; Trigger* tr = NULL; if( d_is_single_trigger[ patTerms[0] ] ){ - tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL, options::smartTriggers() ); + tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL ); d_single_trigger_gen[ patTerms[0] ] = true; }else{ //only generate multi trigger if option set, or if no single triggers exist @@ -376,7 +372,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ d_made_multi_trigger[f] = true; } //will possibly want to get an old trigger - tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD, options::smartTriggers() ); + tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD ); } if( tr ){ unsigned tindex; @@ -412,7 +408,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ if( !options::relevantTriggers() || d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){ d_single_trigger_gen[ patTerms[index] ] = true; - Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL, options::smartTriggers() ); + Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL ); if( tr2 ){ //Notice() << "Add additional trigger " << patTerms[index] << std::endl; tr2->resetInstantiationRound(); @@ -484,7 +480,7 @@ bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) { } Trace("local-t-ext") << std::endl; int matchOption = 0; - Trigger * tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, true, Trigger::TR_GET_OLD, options::smartTriggers() ); + Trigger * tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, true, Trigger::TR_GET_OLD ); d_lte_trigger[f] = tr; }else{ Trace("local-t-ext") << "No local theory extensions trigger for " << f << "." << std::endl; diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index ac4eb9d98..d48084514 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -23,6 +23,7 @@ #include "theory/quantifiers/trigger.h" #include "theory/quantifiers_engine.h" #include "util/statistics_registry.h" +#include "options/quantifiers_options.h" namespace CVC4 { namespace theory { @@ -64,7 +65,7 @@ public: }; private: /** trigger generation strategy */ - int d_tr_strategy; + TriggerSelMode d_tr_strategy; /** regeneration */ bool d_regenerate; int d_regenerate_frequency; diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index f98ab2b7c..8e88d3434 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -165,6 +165,22 @@ bool InstantiationEngine::isIncomplete( Node q ) { return true; } +void InstantiationEngine::preRegisterQuantifier( Node q ) { + if( options::strictTriggers() && q.getNumChildren()==3 ){ + //if strict triggers, take ownership of this quantified formula + bool hasPat = false; + for( unsigned i=0; isetOwner( q, this, 1 ); + } + } +} + void InstantiationEngine::registerQuantifier( Node f ){ if( d_quantEngine->hasOwnership( f, this ) ){ //for( unsigned i=0; i children; @@ -251,6 +252,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { if( doOperation( in, op, qa ) ){ ret = computeOperation( in, op, qa ); if( ret!=in ){ + rew_op = op; status = REWRITE_AGAIN_FULL; break; } @@ -260,7 +262,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { } //print if changed if( in!=ret ){ - Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl; + Trace("quantifiers-rewrite") << "*** rewrite (op=" << rew_op << ") " << in << std::endl; Trace("quantifiers-rewrite") << " to " << std::endl; Trace("quantifiers-rewrite") << ret << std::endl; } @@ -1537,8 +1539,9 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg return mkForAll( args, body, qa ); } -bool QuantifiersRewriter::doOperation( Node f, int computeOption, QAttributes& qa ){ - bool is_std = !qa.d_sygus && !qa.d_quant_elim && !qa.isFunDef(); +bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& qa ){ + bool is_strict_trigger = qa.d_hasPattern && options::userPatternsQuant()==USER_PAT_MODE_TRUST; + bool is_std = !qa.d_sygus && !qa.d_quant_elim && !qa.isFunDef() && !is_strict_trigger; if( computeOption==COMPUTE_ELIM_SYMBOLS ){ return true; }else if( computeOption==COMPUTE_MINISCOPING ){ @@ -1551,15 +1554,15 @@ bool QuantifiersRewriter::doOperation( Node f, int computeOption, QAttributes& q return true; //return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant(); }else if( computeOption==COMPUTE_COND_SPLIT ){ - return ( options::iteDtTesterSplitQuant() || options::condVarSplitQuant() ) && is_std; + return ( options::iteDtTesterSplitQuant() || options::condVarSplitQuant() ) && !is_strict_trigger; }else if( computeOption==COMPUTE_PRENEX ){ - return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant(); + return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant() && is_std; }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ return ( options::varElimQuant() || options::dtVarExpandQuant() || options::purifyQuant() ) && is_std; //}else if( computeOption==COMPUTE_CNF ){ // return options::cnfQuant(); }else if( computeOption==COMPUTE_PURIFY_EXPAND ){ - return options::purifyQuant(); + return options::purifyQuant() && is_std; }else{ return false; } @@ -1617,7 +1620,7 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut std::vector< Node > children; children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) ); children.push_back( n ); - if( !qa.d_ipl.isNull() ){ + if( !qa.d_ipl.isNull() && args.size()==f[0].getNumChildren() ){ children.push_back( qa.d_ipl ); } return NodeManager::currentNM()->mkNode(kind::FORALL, children ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 372aefaf4..5d20a7048 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1945,7 +1945,7 @@ void TermDb::computeAttributes( Node q ) { Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : " << q << std::endl; } //set rewrite engine as owner - d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine() ); + d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine(), 2 ); } if( d_qattr[q].isFunDef() ){ Node f = d_qattr[q].d_fundef_f; @@ -1954,19 +1954,19 @@ void TermDb::computeAttributes( Node q ) { exit( 1 ); } d_fun_defs[f] = true; - d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine() ); + d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine(), 2 ); } if( d_qattr[q].d_sygus ){ if( d_quantEngine->getCegInstantiation()==NULL ){ Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl; } - d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() ); + d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation(), 2 ); } if( d_qattr[q].d_synthesis ){ if( d_quantEngine->getCegInstantiation()==NULL ){ Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl; } - d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() ); + d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation(), 2 ); } } @@ -1976,7 +1976,9 @@ void TermDb::computeQuantAttributes( Node q, QAttributes& qa ){ qa.d_ipl = q[2]; for( unsigned i=0; i& nodes, - int matchOption, bool smartTriggers ) +Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption ) : 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++ ){ + for( unsigned i=0; isetActiveAdd(true); - } + if( d_nodes.size()==1 ){ + if( isSimpleTrigger( d_nodes[0] ) ){ + d_mg = new InstMatchGeneratorSimple( f, d_nodes[0] ); }else{ - d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe ); - //d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe ); - //d_mg->setActiveAdd(); + d_mg = InstMatchGenerator::mkInstMatchGenerator( f, d_nodes[0], qe ); + d_mg->setActiveAdd(true); } }else{ - d_mg = InstMatchGenerator::mkInstMatchGenerator( f, d_nodes, qe ); - d_mg->setActiveAdd(true); + d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe ); + //d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe ); + //d_mg->setActiveAdd(); } if( d_nodes.size()==1 ){ if( isSimpleTrigger( d_nodes[0] ) ){ @@ -68,11 +58,10 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, ++(qe->d_statistics.d_simple_triggers); } }else{ - Trace("multi-trigger") << "Multi-trigger "; - debugPrint("multi-trigger"); - Trace("multi-trigger") << " for " << f << std::endl; - //Notice() << "Multi-trigger for " << f << " : " << std::endl; - //Notice() << " " << (*this) << std::endl; + Trace("multi-trigger") << "Trigger for " << f << ": " << std::endl; + for( unsigned i=0; id_statistics.d_multi_triggers); } //Notice() << "Trigger : " << (*this) << " for " << f << std::endl; @@ -123,8 +112,7 @@ int Trigger::addInstantiations( InstMatch& baseMatch ){ return addedLemmas; } -Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool keepAll, int trOption, - bool smartTriggers ){ +Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool keepAll, int trOption ){ std::vector< Node > trNodes; if( !keepAll ){ //only take nodes that contribute variables to the trigger when added @@ -211,15 +199,15 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& } } } - Trigger* t = new Trigger( qe, f, trNodes, matchOption, smartTriggers ); + Trigger* t = new Trigger( qe, f, trNodes, matchOption ); qe->getTriggerDatabase()->addTrigger( trNodes, t ); return t; } -Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption, bool smartTriggers ){ +Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption ){ std::vector< Node > nodes; nodes.push_back( n ); - return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption, smartTriggers ); + return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption ); } bool Trigger::isUsable( Node n, Node q ){ @@ -360,7 +348,7 @@ bool Trigger::isSimpleTrigger( Node n ){ //store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, Node >& visited, std::map< Node, std::vector< Node > >& visited_fv, - int tstrt, std::vector< Node >& exclude, + quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::map< Node, int >& reqPol, std::vector< Node >& added, bool pol, bool hasPol, bool epol, bool hasEPol ){ std::map< Node, Node >::iterator itv = visited.find( n ); @@ -371,14 +359,16 @@ bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, Node >& visited, if( n.getKind()!=FORALL ){ bool rec = true; Node nu; + bool nu_single = false; if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){ nu = getIsUsableTrigger( n, f, pol, hasPol ); if( !nu.isNull() ){ reqPol[ nu ] = hasEPol ? ( epol ? 1 : -1 ) : 0; visited[ nu ] = nu; quantifiers::TermDb::computeVarContains( nu, visited_fv[ nu ] ); + nu_single = visited_fv[nu].size()==f[0].getNumChildren(); retVal = true; - if( tstrt==TS_MAX_TRIGGER ){ + if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){ rec = false; } } @@ -404,7 +394,7 @@ bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, Node >& visited, } added.push_back( added2[i] ); } - if( rm_nu && tstrt==TS_MIN_TRIGGER ){ + if( rm_nu && ( tstrt==quantifiers::TRIGGER_SEL_MIN || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL && nu_single ) ) ){ visited[nu] = Node::null(); reqPol.erase( nu ); }else{ @@ -502,14 +492,14 @@ bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< return true; } -void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, +void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::map< Node, int >& reqPol, bool filterInst ){ std::map< Node, Node > visited; if( filterInst ){ //immediately do not consider any term t for which another term is an instance of t std::vector< Node > patTerms2; std::map< Node, int > reqPol2; - collectPatTerms( qe, f, n, patTerms2, TS_ALL, exclude, reqPol2, false ); + collectPatTerms( qe, f, n, patTerms2, quantifiers::TRIGGER_SEL_ALL, exclude, reqPol2, false ); std::vector< Node > temp; temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() ); qe->getTermDatabase()->filterInstances( temp ); @@ -525,7 +515,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto } Trace("trigger-filter-instance") << std::endl; } - if( tstrt==TS_ALL ){ + if( tstrt==quantifiers::TRIGGER_SEL_ALL ){ for( unsigned i=0; i reqPol; //collect all patterns from icn std::vector< Node > exclude; - collectPatTerms( qe, f, icn, patTerms, TS_ALL, exclude, reqPol ); + collectPatTerms( qe, f, icn, patTerms, quantifiers::TRIGGER_SEL_ALL, exclude, reqPol ); //collect all variables from all patterns in patTerms, add to t_vars for( unsigned i=0; igetTermDatabase()->getVarContainsNode( f, patTerms[i], t_vars ); diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 97ed51fe0..06e9011c7 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -21,6 +21,7 @@ #include "expr/node.h" #include "theory/quantifiers/inst_match.h" +#include "options/quantifiers_options.h" // Forward declarations for defining the Trigger and TriggerTrie. namespace CVC4 { @@ -86,20 +87,12 @@ class Trigger { }; 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 ); + bool keepAll = true, int trOption = TR_MAKE_NEW ); static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption = 0, bool keepAll = true, - int trOption = TR_MAKE_NEW, - bool smartTriggers = false ); - //different strategies for choosing trigger terms - enum { - TS_MAX_TRIGGER = 0, - TS_MIN_TRIGGER, - TS_ALL, - }; + int trOption = TR_MAKE_NEW ); static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n, - std::vector< Node >& patTerms, int tstrt, + std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::map< Node, int >& reqPol, bool filterInst = false ); /** is usable trigger */ @@ -132,8 +125,7 @@ class Trigger { private: /** trigger constructor */ - Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, - int matchOption = 0, bool smartTriggers = false ); + Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, int matchOption = 0 ); /** is subterm of trigger usable */ static bool isUsable( Node n, Node q ); @@ -141,7 +133,7 @@ private: bool hasPol = false ); /** collect all APPLY_UF pattern terms for f in n */ static bool collectPatTerms2( Node f, Node n, std::map< Node, Node >& visited, std::map< Node, std::vector< Node > >& visited_fv, - int tstrt, std::vector< Node >& exclude, + quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::map< Node, int >& reqPol, std::vector< Node >& added, bool pol, bool hasPol, bool epol, bool hasEPol ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ad226681d..1a2762409 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -315,13 +315,17 @@ QuantifiersModule * QuantifiersEngine::getOwner( Node q ) { } } -void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m ) { +void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m, int priority ) { QuantifiersModule * mo = getOwner( q ); if( mo!=m ){ if( mo!=NULL ){ - Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << ( m ? m->identify() : "null" ) << ", but already has owner " << mo->identify() << "!" << std::endl; + if( priority<=d_owner_priority[q] ){ + Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << ( m ? m->identify() : "null" ) << ", but already has owner " << mo->identify() << " with higher priority!" << std::endl; + return; + } } d_owner[q] = m; + d_owner_priority[q] = priority; } } @@ -393,9 +397,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ } Trace("quant-engine-debug") << std::endl; Trace("quant-engine-debug") << " # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl; - //if( d_model->getNumToReduceQuantifiers()>0 ){ - // Trace("quant-engine-debug") << " # quantified formulas to reduce = " << d_model->getNumToReduceQuantifiers() << std::endl; - //} if( !d_lemmas_waiting.empty() ){ Trace("quant-engine-debug") << " lemmas waiting = " << d_lemmas_waiting.size() << std::endl; } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 83849cd60..641c7624e 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -271,11 +271,12 @@ public: //modules private: /** owner of quantified formulas */ std::map< Node, QuantifiersModule * > d_owner; + std::map< Node, int > d_owner_priority; public: /** get owner */ QuantifiersModule * getOwner( Node q ); /** set owner */ - void setOwner( Node q, QuantifiersModule * m ); + void setOwner( Node q, QuantifiersModule * m, int priority = 0 ); /** considers */ bool hasOwnership( Node q, QuantifiersModule * m = NULL ); public: -- cgit v1.2.3 From 5e4ed407978b892e04de00994be535f58fb33257 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sun, 10 Apr 2016 15:20:33 -0500 Subject: More work on instantiation propagation. Enable external filtering of instantiations. All quantifiers strategies terminate when a conflict can be established. --- src/theory/quantifiers/ambqi_builder.cpp | 2 +- src/theory/quantifiers/ce_guided_single_inv.cpp | 18 +- src/theory/quantifiers/ce_guided_single_inv.h | 4 +- src/theory/quantifiers/ceg_instantiator.cpp | 56 +- src/theory/quantifiers/ceg_instantiator.h | 10 +- src/theory/quantifiers/full_model_check.cpp | 5 +- src/theory/quantifiers/inst_match.cpp | 65 +- src/theory/quantifiers/inst_match.h | 16 +- src/theory/quantifiers/inst_match_generator.cpp | 20 +- src/theory/quantifiers/inst_propagator.cpp | 1402 ++++++++++---------- src/theory/quantifiers/inst_propagator.h | 323 ++--- src/theory/quantifiers/inst_strategy_cbqi.cpp | 14 +- src/theory/quantifiers/inst_strategy_cbqi.h | 4 +- .../quantifiers/inst_strategy_e_matching.cpp | 13 +- src/theory/quantifiers/instantiation_engine.cpp | 29 +- src/theory/quantifiers/instantiation_engine.h | 2 +- src/theory/quantifiers/model_builder.cpp | 9 +- src/theory/quantifiers/model_engine.cpp | 63 +- src/theory/quantifiers/rewrite_engine.cpp | 13 +- src/theory/quantifiers_engine.cpp | 99 +- src/theory/quantifiers_engine.h | 23 +- test/regress/regress0/fmf/Makefile.am | 1 - 22 files changed, 1180 insertions(+), 1011 deletions(-) (limited to 'src/theory/quantifiers/instantiation_engine.cpp') diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index 18496b173..dd6db951d 100644 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -190,7 +190,7 @@ bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, success = true; } } - }while( !success && index<32 ); + }while( !qe->inConflict() && !success && index<32 ); //mark if we are incomplete osuccess = osuccess && success; } diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index b17286dba..33856d226 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -33,8 +33,8 @@ using namespace std; namespace CVC4 { -bool CegqiOutputSingleInv::addInstantiation( std::vector< Node >& subs ) { - return d_out->addInstantiation( subs ); +bool CegqiOutputSingleInv::doAddInstantiation( std::vector< Node >& subs ) { + return d_out->doAddInstantiation( subs ); } bool CegqiOutputSingleInv::isEligibleForInstantiation( Node n ) { @@ -55,12 +55,12 @@ CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * qe, CegConje } d_cosi = new CegqiOutputSingleInv( this ); // third and fourth arguments set to (false,false) until we have solution reconstruction for delta and infinity - d_cinst = new CegInstantiator( d_qe, d_cosi, false, false ); + d_cinst = new CegInstantiator( d_qe, d_cosi, false, false ); d_sol = new CegConjectureSingleInvSol( qe ); d_sip = new SingleInvocationPartition; - + if( options::cegqiSingleInvPartial() ){ d_ei = new CegEntailmentInfer( qe, d_sip ); }else{ @@ -104,7 +104,7 @@ void CegConjectureSingleInv::getInitialSingleInvLemma( std::vector< Node >& lems if( d_cinst ){ delete d_cinst; } - d_cinst = new CegInstantiator( d_qe, d_cosi, false, false ); + d_cinst = new CegInstantiator( d_qe, d_cosi, false, false ); d_cinst->registerCounterexampleLemma( lems, d_single_inv_sk ); } } @@ -480,7 +480,7 @@ void CegConjectureSingleInv::initializeNextSiConjecture() { if( d_single_inv.isNull() ){ if( d_ei->getEntailedConjecture( d_single_inv, d_single_inv_exp ) ){ Trace("cegqi-nsi") << "NSI : got : " << d_single_inv << std::endl; - Trace("cegqi-nsi") << "NSI : exp : " << d_single_inv_exp << std::endl; + Trace("cegqi-nsi") << "NSI : exp : " << d_single_inv_exp << std::endl; }else{ Trace("cegqi-nsi") << "NSI : failed to construct next conjecture." << std::endl; Notice() << "Incomplete due to --cegqi-si-partial." << std::endl; @@ -491,7 +491,7 @@ void CegConjectureSingleInv::initializeNextSiConjecture() { Trace("cegqi-nsi") << "NSI : have : " << d_single_inv << std::endl; Assert( d_single_inv_exp.isNull() ); } - + d_si_guard = Node::null(); d_ns_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "GS", NodeManager::currentNM()->booleanType() ) ); d_ns_guard = d_qe->getValuation().ensureLiteral( d_ns_guard ); @@ -508,7 +508,7 @@ void CegConjectureSingleInv::initializeNextSiConjecture() { Trace("cegqi-nsi") << "NSI : conjecture is " << d_single_inv << std::endl; } -bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs ){ +bool CegConjectureSingleInv::doAddInstantiation( std::vector< Node >& subs ){ std::stringstream siss; if( Trace.isOn("cegqi-si-inst-debug") || Trace.isOn("cegqi-engine") ){ siss << " * single invocation: " << std::endl; @@ -843,7 +843,7 @@ bool SingleInvocationPartition::init( Node n ) { std::vector< TypeNode > typs; std::map< Node, bool > visited; if( inferArgTypes( n, typs, visited ) ){ - return init( typs, n ); + return init( typs, n ); }else{ Trace("si-prt") << "Could not infer argument types." << std::endl; return false; diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index 6d47b8d9a..4d2f9a0e5 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -37,7 +37,7 @@ public: CegqiOutputSingleInv( CegConjectureSingleInv * out ) : d_out( out ){} ~CegqiOutputSingleInv() {} CegConjectureSingleInv * d_out; - bool addInstantiation( std::vector< Node >& subs ); + bool doAddInstantiation( std::vector< Node >& subs ); bool isEligibleForInstantiation( Node n ); bool addLemma( Node lem ); }; @@ -102,7 +102,7 @@ public: private: std::vector< Node > d_curr_lemmas; //add instantiation - bool addInstantiation( std::vector< Node >& subs ); + bool doAddInstantiation( std::vector< Node >& subs ); //is eligible for instantiation bool isEligibleForInstantiation( Node n ); // add lemma diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 6a56977b8..da488ea98 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -65,9 +65,9 @@ void CegInstantiator::computeProgVars( Node n ){ } } -bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, - std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, - std::map< Node, Node >& cons, std::vector< Node >& curr_var ){ +bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, + std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, + std::map< Node, Node >& cons, std::vector< Node >& curr_var ){ if( i==d_vars.size() ){ //solved for all variables, now construct instantiation if( !sf.d_has_coeff.empty() ){ @@ -75,12 +75,12 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve //use symbolic solved forms SolvedForm csf; csf.copy( ssf ); - return addInstantiationCoeff( csf, vars, btyp, 0, cons ); + return doAddInstantiationCoeff( csf, vars, btyp, 0, cons ); }else{ - return addInstantiationCoeff( sf, vars, btyp, 0, cons ); + return doAddInstantiationCoeff( sf, vars, btyp, 0, cons ); } }else{ - return addInstantiation( sf.d_subs, vars, cons ); + return doAddInstantiation( sf.d_subs, vars, cons ); } }else{ std::map< Node, std::map< Node, bool > > subs_proc; @@ -139,7 +139,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve if( proc ){ //try the substitution subs_proc[ns][pv_coeff] = true; - if( addInstantiationInc( ns, pv, pv_coeff, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiationInc( ns, pv, pv_coeff, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -163,7 +163,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve for( unsigned j=0; jmkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv ) ); } - if( addInstantiation( sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiation( sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; }else{ //cleanup @@ -270,7 +270,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve Node val = veq[1]; if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){ subs_proc[val][veq_c] = true; - if( addInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -286,7 +286,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve if( success ){ if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){ subs_proc[val][veq_c] = true; - if( addInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -455,7 +455,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve //try this bound if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){ subs_proc[uval][veq_c] = true; - if( addInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -492,7 +492,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve val = NodeManager::currentNM()->mkNode( UMINUS, val ); val = Rewriter::rewrite( val ); } - if( addInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -588,7 +588,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve if( !val.isNull() ){ if( subs_proc[val].find( mbp_coeff[rr][best] )==subs_proc[val].end() ){ subs_proc[val][mbp_coeff[rr][best]] = true; - if( addInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -605,7 +605,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve if( !val.isNull() ){ if( subs_proc[val].find( c )==subs_proc[val].end() ){ subs_proc[val][c] = true; - if( addInstantiationInc( val, pv, c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiationInc( val, pv, c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -649,7 +649,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve if( !val.isNull() ){ if( subs_proc[val].find( Node::null() )==subs_proc[val].end() ){ subs_proc[val][Node::null()] = true; - if( addInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -670,7 +670,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve if( !val.isNull() ){ if( subs_proc[val].find( mbp_coeff[rr][j] )==subs_proc[val].end() ){ subs_proc[val][mbp_coeff[rr][j]] = true; - if( addInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -694,7 +694,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve //we only resort to values in the case of booleans Assert( ( pvtn.isInteger() ? !options::cbqiUseInfInt() : !options::cbqiUseInfReal() ) || pvtn.isBoolean() ); #endif - if( addInstantiationInc( mv, pv, pv_coeff_m, 0, sf, ssf, vars, btyp, theta, i, new_effort, cons, curr_var ) ){ + if( doAddInstantiationInc( mv, pv, pv_coeff_m, 0, sf, ssf, vars, btyp, theta, i, new_effort, cons, curr_var ) ){ return true; } } @@ -704,9 +704,9 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve } -bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, - std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, - std::map< Node, Node >& cons, std::vector< Node >& curr_var ) { +bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, + std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, + std::map< Node, Node >& cons, std::vector< Node >& curr_var ) { if( Trace.isOn("cbqi-inst") ){ for( unsigned j=0; j& vars, std::vector< int >& btyp, +bool CegInstantiator::doAddInstantiationCoeff( SolvedForm& sf, std::vector< Node >& vars, std::vector< int >& btyp, unsigned j, std::map< Node, Node >& cons ) { if( j==sf.d_has_coeff.size() ){ - return addInstantiation( sf.d_subs, vars, cons ); + return doAddInstantiation( sf.d_subs, vars, cons ); }else{ Assert( std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )!=vars.end() ); unsigned index = std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )-vars.begin(); @@ -894,7 +894,7 @@ bool CegInstantiator::addInstantiationCoeff( SolvedForm& sf, std::vector< Node > } } } - if( addInstantiationCoeff( sf, vars, btyp, j+1, cons ) ){ + if( doAddInstantiationCoeff( sf, vars, btyp, j+1, cons ) ){ return true; } } @@ -905,7 +905,7 @@ bool CegInstantiator::addInstantiationCoeff( SolvedForm& sf, std::vector< Node > } } -bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ) { +bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ) { if( vars.size()>d_vars.size() ){ Trace("cbqi-inst-debug") << "Reconstructing instantiations...." << std::endl; std::map< Node, Node > subs_map; @@ -927,7 +927,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< subs.push_back( subs_orig[d_var_order_index[i]] ); } } - bool ret = d_out->addInstantiation( subs ); + bool ret = d_out->doAddInstantiation( subs ); #ifdef MBP_STRICT_ASSERTIONS Assert( ret ); #endif @@ -1127,7 +1127,7 @@ bool CegInstantiator::check() { std::map< Node, Node > cons; std::vector< Node > curr_var; //try to add an instantiation - if( addInstantiation( sf, ssf, vars, btyp, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){ + if( doAddInstantiation( sf, ssf, vars, btyp, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){ return true; } } @@ -1499,7 +1499,7 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st } } -//this isolates the atom into solved form +//this isolates the atom into solved form // veq_c * pv <> val + vts_coeff_delta * delta + vts_coeff_inf * inf // ensures val is Int if pv is Int, and val does not contain vts symbols int CegInstantiator::solve_arith( Node pv, Node atom, Node& veq_c, Node& val, Node& vts_coeff_inf, Node& vts_coeff_delta ) { diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 36c6f1bce..3d7bbcb55 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -33,7 +33,7 @@ namespace quantifiers { class CegqiOutput { public: virtual ~CegqiOutput() {} - virtual bool addInstantiation( std::vector< Node >& subs ) = 0; + virtual bool doAddInstantiation( std::vector< Node >& subs ) = 0; virtual bool isEligibleForInstantiation( Node n ) = 0; virtual bool addLemma( Node lem ) = 0; }; @@ -108,16 +108,16 @@ private: }; */ // effort=0 : do not use model value, 1: use model value, 2: one must use model value - bool addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, + bool doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, std::map< Node, Node >& cons, std::vector< Node >& curr_var ); - bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, + bool doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, std::map< Node, Node >& cons, std::vector< Node >& curr_var ); - bool addInstantiationCoeff( SolvedForm& sf, + bool doAddInstantiationCoeff( SolvedForm& sf, std::vector< Node >& vars, std::vector< int >& btyp, unsigned j, std::map< Node, Node >& cons ); - bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ); + bool doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ); Node constructInstantiation( Node n, std::map< Node, Node >& subs_map, std::map< Node, Node >& cons ); Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ) { return applySubstitution( tn, n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, vars, pv_coeff, try_coeff ); diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index d06e9f7f7..0276cf7ab 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -591,6 +591,7 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) { bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl; + Assert( !d_qe->inConflict() ); if( optUseModel() ){ FirstOrderModelFmc * fmfmc = fm->asFirstOrderModelFmc(); if (effort==0) { @@ -684,7 +685,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, if( d_qe->addInstantiation( f, inst ) ){ Trace("fmc-debug-inst") << "** Added instantiation." << std::endl; d_addedLemmas++; - if( options::fmfOneInstPerRound() ){ + if( d_qe->inConflict() || options::fmfOneInstPerRound() ){ break; } }else{ @@ -812,7 +813,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No if( d_qe->addInstantiation( f, inst ) ){ Trace("fmc-exh-debug") << " ...success."; addedLemmas++; - if( options::fmfOneInstPerRound() ){ + if( d_qe->inConflict() || options::fmfOneInstPerRound() ){ break; } }else{ diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 1751f3a87..55a4e8f8c 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -155,20 +155,6 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No return ret; } } - /* - //check if m is an instance of another instantiation if modInst is true - if( modInst ){ - if( !n.isNull() ){ - Node nl; - std::map< Node, InstMatchTrie >::iterator itm = d_data.find( nl ); - if( itm!=d_data.end() ){ - if( !itm->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){ - return false; - } - } - } - } - */ if( modEq ){ //check modulo equality if any other instantiation match exists if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){ @@ -195,6 +181,24 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No } } +bool InstMatchTrie::removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, ImtIndexOrder* imtio, int index ) { + Assert( index<(int)q[0].getNumChildren() ); + Assert( !imtio || index<(int)imtio->d_order.size() ); + int i_index = imtio ? imtio->d_order[index] : index; + Node n = m[i_index]; + std::map< Node, InstMatchTrie >::iterator it = d_data.find( n ); + if( it!=d_data.end() ){ + if( (index+1)==(int)q[0].getNumChildren() || ( imtio && (index+1)==(int)imtio->d_order.size() ) ){ + d_data.erase( n ); + return true; + }else{ + return it->second.removeInstMatch( qe, q, m, imtio, index+1 ); + } + }else{ + return false; + } +} + void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms ) const { if( terms.size()==q[0].getNumChildren() ){ out << " ( "; @@ -257,20 +261,6 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< return reset || ret; } } - //check if m is an instance of another instantiation if modInst is true - /* - if( modInst ){ - if( !n.isNull() ){ - Node nl; - std::map< Node, CDInstMatchTrie* >::iterator itm = d_data.find( nl ); - if( itm!=d_data.end() ){ - if( !itm->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){ - return false; - } - } - } - } - */ if( modEq ){ //check modulo equality if any other instantiation match exists if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){ @@ -302,6 +292,25 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< } } +bool CDInstMatchTrie::removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index ) { + if( index==(int)q[0].getNumChildren() ){ + if( d_valid.get() ){ + d_valid.set( false ); + return true; + }else{ + return false; + } + }else{ + Node n = m[index]; + std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n ); + if( it!=d_data.end() ){ + return it->second->removeInstMatch( qe, q, m, index+1 ); + }else{ + return false; + } + } +} + void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms ) const{ if( d_valid.get() ){ if( terms.size()==q[0].getNumChildren() ){ diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index fbdef61c2..a87d2704e 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -128,6 +128,7 @@ public: } bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false, bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ); + bool removeInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, ImtIndexOrder* imtio = NULL, int index = 0 ); void print( std::ostream& out, Node q ) const{ std::vector< TNode > terms; print( out, q, terms ); @@ -157,24 +158,25 @@ public: modEq is if we check modulo equality modInst is if we return true if m is an instance of a match that exists */ - bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false, + bool existsInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false, bool modInst = false, int index = 0 ) { - return !addInstMatch( qe, f, m, c, modEq, modInst, index, true ); + return !addInstMatch( qe, q, m, c, modEq, modInst, index, true ); } - bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false, + bool existsInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false, bool modInst = false, int index = 0 ) { - return !addInstMatch( qe, f, m, c, modEq, modInst, index, true ); + return !addInstMatch( qe, q, m, c, modEq, modInst, index, true ); } /** add match m for quantifier f, take into account equalities if modEq = true, if imtio is non-null, this is the order to add to trie return true if successful */ - bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false, + bool addInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false, bool modInst = false, int index = 0, bool onlyExist = false ) { - return addInstMatch( qe, f, m.d_vals, c, modEq, modInst, index, onlyExist ); + return addInstMatch( qe, q, m.d_vals, c, modEq, modInst, index, onlyExist ); } - bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false, + bool addInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false, bool modInst = false, int index = 0, bool onlyExist = false ); + bool removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index = 0 ); void print( std::ostream& out, Node q ) const{ std::vector< TNode > terms; print( out, q, terms ); diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index cfa4190e4..29754d3e6 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -126,7 +126,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< if( d_pattern.getKind()==NOT && ( d_pattern[0].getKind()==IFF || d_pattern[0].getKind()==EQUAL ) ){ ((inst::CandidateGeneratorQE*)d_cg)->excludeEqc( d_eq_class_rel ); d_eq_class_rel = Node::null(); - } + } }else if( d_match_pattern.getKind()==INST_CONSTANT ){ if( d_pattern.getKind()==APPLY_SELECTOR_TOTAL ){ Expr selectorExpr = qe->getTermDatabase()->getMatchOperator( d_pattern ).toExpr(); @@ -139,7 +139,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< }else{ d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern ); } - }else if( ( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ) && + }else if( ( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ) && d_match_pattern[0].getKind()==INST_CONSTANT && d_match_pattern[1].getKind()==INST_CONSTANT ){ //we will be producing candidates via literal matching heuristics if( d_pattern.getKind()!=NOT ){ @@ -307,6 +307,9 @@ void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){ } bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){ + if( qe->inConflict() ){ + return false; + } if( d_needsReset ){ Trace("matching") << "Reset not done yet, must do the reset..." << std::endl; reset( d_eq_class, qe ); @@ -767,15 +770,20 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin m.setValue( v, t); addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); m.setValue( v, prev); + if( qe->inConflict() ){ + break; + } } } return; } } - Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] ); - std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r ); - if( it!=tat->d_data.end() ){ - addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); + if( !qe->inConflict() ){ + Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] ); + std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r ); + if( it!=tat->d_data.end() ){ + addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); + } } } } diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp index d20f3fd4a..863914567 100644 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp @@ -1,674 +1,728 @@ -/********************* */ -/*! \file inst_propagator.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** Propagate mechanism for instantiations - **/ - -#include - -#include "theory/quantifiers/inst_propagator.h" -#include "theory/rewriter.h" -#include "theory/quantifiers/term_database.h" - -using namespace CVC4; -using namespace std; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; -using namespace CVC4::kind; - - -EqualityQueryInstProp::EqualityQueryInstProp( QuantifiersEngine* qe ) : d_qe( qe ){ - d_true = NodeManager::currentNM()->mkConst( true ); - d_false = NodeManager::currentNM()->mkConst( false ); -} - -bool EqualityQueryInstProp::reset( Theory::Effort e ) { - d_uf.clear(); - d_uf_exp.clear(); - d_diseq_list.clear(); - return true; -} - -/** contains term */ -bool EqualityQueryInstProp::hasTerm( Node a ) { - if( getEngine()->hasTerm( a ) ){ - return true; - }else{ - std::vector< Node > exp; - Node ar = getUfRepresentative( a, exp ); - return !ar.isNull() && getEngine()->hasTerm( ar ); - } -} - -/** get the representative of the equivalence class of a */ -Node EqualityQueryInstProp::getRepresentative( Node a ) { - if( getEngine()->hasTerm( a ) ){ - a = getEngine()->getRepresentative( a ); - } - std::vector< Node > exp; - Node ar = getUfRepresentative( a, exp ); - return ar.isNull() ? a : ar; -} - -/** returns true if a and b are equal in the current context */ -bool EqualityQueryInstProp::areEqual( Node a, Node b ) { - if( a==b ){ - return true; - }else{ - eq::EqualityEngine* ee = getEngine(); - if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ - if( ee->areEqual( a, b ) ){ - return true; - } - } - return false; - } -} - -/** returns true is a and b are disequal in the current context */ -bool EqualityQueryInstProp::areDisequal( Node a, Node b ) { - if( a==b ){ - return true; - }else{ - eq::EqualityEngine* ee = getEngine(); - if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ - if( ee->areDisequal( a, b, false ) ){ - return true; - } - } - return false; - } -} - -/** get the equality engine associated with this query */ -eq::EqualityEngine* EqualityQueryInstProp::getEngine() { - return d_qe->getMasterEqualityEngine(); -} - -/** get the equivalence class of a */ -void EqualityQueryInstProp::getEquivalenceClass( Node a, std::vector< Node >& eqc ) { - //TODO? -} - -TNode EqualityQueryInstProp::getCongruentTerm( Node f, std::vector< TNode >& args ) { - TNode t = d_qe->getTermDatabase()->getCongruentTerm( f, args ); - if( !t.isNull() ){ - return t; - }else{ - //TODO? - return TNode::null(); - } -} - -Node EqualityQueryInstProp::getRepresentativeExp( Node a, std::vector< Node >& exp ) { - bool engine_has_a = getEngine()->hasTerm( a ); - if( engine_has_a ){ - a = getEngine()->getRepresentative( a ); - } - //get union find representative, if this occurs in the equality engine, return it - unsigned prev_size = exp.size(); - Node ar = getUfRepresentative( a, exp ); - if( !ar.isNull() ){ - if( engine_has_a || getEngine()->hasTerm( ar ) ){ - Assert( getEngine()->hasTerm( ar ) ); - Assert( getEngine()->getRepresentative( ar )==ar ); - return ar; - } - }else{ - if( engine_has_a ){ - return a; - } - } - //retract explanation - while( exp.size()>prev_size ){ - exp.pop_back(); - } - return Node::null(); -} - -bool EqualityQueryInstProp::areEqualExp( Node a, Node b, std::vector< Node >& exp ) { - if( areEqual( a, b ) ){ - return true; - }else{ - std::vector< Node > exp_a; - Node ar = getUfRepresentative( a, exp_a ); - if( !ar.isNull() ){ - std::vector< Node > exp_b; - if( ar==getUfRepresentative( b, exp_b ) ){ - merge_exp( exp, exp_a ); - merge_exp( exp, exp_b ); - return true; - } - } - return false; - } -} - -bool EqualityQueryInstProp::areDisequalExp( Node a, Node b, std::vector< Node >& exp ) { - if( areDisequal( a, b ) ){ - return true; - }else{ - //TODO? - return false; - } -} - -Node EqualityQueryInstProp::getUfRepresentative( Node a, std::vector< Node >& exp ) { - Assert( exp.empty() ); - std::map< Node, Node >::iterator it = d_uf.find( a ); - if( it!=d_uf.end() ){ - if( it->second==a ){ - Assert( d_uf_exp[ a ].empty() ); - return it->second; - }else{ - Node m = getUfRepresentative( it->second, exp ); - Assert( !m.isNull() ); - if( m!=it->second ){ - //update union find - d_uf[ a ] = m; - //update explanation : merge the explanation of the parent - merge_exp( d_uf_exp[ a ], exp ); - Trace("qip-eq") << "EqualityQueryInstProp::getUfRepresentative : merge " << a << " -> " << m << ", exp size=" << d_uf_exp[ a ].size() << std::endl; - } - //add current explanation to exp: note that exp is a subset of d_uf_exp[ a ], reset - exp.clear(); - exp.insert( exp.end(), d_uf_exp[ a ].begin(), d_uf_exp[ a ].end() ); - return m; - } - }else{ - return Node::null(); - } -} - -// set a == b with reason, return status, modify a and b to representatives pre-merge -int EqualityQueryInstProp::setEqual( Node& a, Node& b, std::vector< Node >& reason ) { - int status = STATUS_MERGED_UNKNOWN; - Trace("qip-eq") << "EqualityQueryInstProp::setEqual " << a << ", " << b << ", reason size = " << reason.size() << std::endl; - //get the representative for a - std::vector< Node > exp_a; - Node ar = getUfRepresentative( a, exp_a ); - if( ar.isNull() ){ - Assert( exp_a.empty() ); - ar = a; - } - if( ar==b ){ - Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl; - return STATUS_NONE; - } - bool swap = false; - //get the representative for b - std::vector< Node > exp_b; - Node br = getUfRepresentative( b, exp_b ); - if( br.isNull() ){ - Assert( exp_b.empty() ); - br = b; - if( !getEngine()->hasTerm( br ) ){ - if( ar!=a ){ - swap = true; - } - }else{ - if( getEngine()->hasTerm( ar ) ){ - status = STATUS_MERGED_KNOWN; - } - } - }else{ - if( ar==br ){ - Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl; - return STATUS_NONE; - }else if( getEngine()->hasTerm( ar ) ){ - if( getEngine()->hasTerm( br ) ){ - status = STATUS_MERGED_KNOWN; - }else{ - swap = true; - } - } - } - if( swap ){ - //swap - Node temp_r = ar; - ar = br; - br = temp_r; - } - - Assert( ar!=br ); - Assert( !getEngine()->hasTerm( ar ) || getEngine()->hasTerm( br ) ); - - //update the union find - Assert( d_uf_exp[ar].empty() ); - Assert( d_uf_exp[br].empty() ); - - d_uf[ar] = br; - merge_exp( d_uf_exp[ar], exp_a ); - merge_exp( d_uf_exp[ar], exp_b ); - merge_exp( d_uf_exp[ar], reason ); - - d_uf[br] = br; - d_uf_exp[br].clear(); - - Trace("qip-eq") << "EqualityQueryInstProp::setEqual : merge " << ar << " -> " << br << ", exp size = " << d_uf_exp[ar].size() << ", status = " << status << std::endl; - a = ar; - b = br; - return status; -} - - -void EqualityQueryInstProp::addArgument( std::vector< TNode >& args, std::vector< TNode >& props, Node n, bool is_prop, bool pol ) { - if( is_prop ){ - if( isLiteral( n ) ){ - props.push_back( pol ? n : n.negate() ); - return; - } - } - args.push_back( n ); -} - -bool EqualityQueryInstProp::isLiteral( Node n ) { - Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind(); - Assert( ak!=NOT ); - return ak!=AND && ak!=OR && ak!=IFF && ak!=ITE; -} - -//this is identical to TermDb::evaluateTerm2, but tracks more information -Node EqualityQueryInstProp::evaluateTermExp( TNode n, std::vector< Node >& exp, std::map< TNode, Node >& visited, bool hasPol, bool pol, - std::map< Node, bool >& watch_list_out, std::vector< TNode >& props ) { - std::map< TNode, Node >::iterator itv = visited.find( n ); - if( itv != visited.end() ){ - return itv->second; - }else{ - Trace("term-db-eval") << "evaluate term : " << n << std::endl; - std::vector< Node > exp_n; - Node ret = getRepresentativeExp( n, exp_n ); - if( ret.isNull() ){ - //term is not known to be equal to a representative in equality engine, evaluate it - Kind k = n.getKind(); - if( k==FORALL ){ - ret = Node::null(); - }else{ - std::map< Node, bool > watch_list_out_curr; - TNode f = d_qe->getTermDatabase()->getMatchOperator( n ); - std::vector< TNode > args; - bool ret_set = false; - bool childChanged = false; - int abort_i = -1; - //get the child entailed polarity - Assert( n.getKind()!=IMPLIES ); - bool newHasPol, newPol; - QuantPhaseReq::getEntailPolarity( n, 0, hasPol, pol, newHasPol, newPol ); - //for each child - for( unsigned i=0; i=2 ){ - //we are done if at least two args are unevaluated - abort_i = i; - break; - } - }else if( k==kind::ITE ){ - //we are done if we are ITE and condition is unevaluated - Assert( i==0 ); - args.push_back( c ); - abort_i = i; - break; - }else{ - args.push_back( c ); - } - } - } - //add remaining children if we aborted - if( abort_i!=-1 ){ - for( int i=(abort_i+1); i<(int)n.getNumChildren(); i++ ){ - args.push_back( n[i] ); - } - } - //copy over the watch list - for( std::map< Node, bool >::iterator itc = watch_list_out_curr.begin(); itc != watch_list_out_curr.end(); ++itc ){ - watch_list_out[itc->first] = itc->second; - } - - //if we have not short-circuited evaluation - if( !ret_set ){ - //if it is an indexed term, return the congruent term - if( !f.isNull() && watch_list_out.empty() ){ - Assert( args.size()==n.getNumChildren() ); - //args contains terms known by the equality engine - TNode nn = getCongruentTerm( f, args ); - Trace("term-db-eval") << " got congruent term " << nn << " from DB for " << n << std::endl; - if( !nn.isNull() ){ - //successfully constructed representative in EE - Assert( exp_n.empty() ); - ret = getRepresentativeExp( nn, exp_n ); - Trace("term-db-eval") << "return rep, exp size = " << exp_n.size() << std::endl; - merge_exp( exp, exp_n ); - ret_set = true; - Assert( !ret.isNull() ); - } - } - if( !ret_set ){ - if( childChanged ){ - Trace("term-db-eval") << "return rewrite" << std::endl; - if( ( k==kind::AND || k==kind::OR ) ){ - if( args.empty() ){ - ret = k==kind::AND ? d_true : d_false; - ret_set = true; - }else if( args.size()==1 ){ - ret = args[0]; - ret_set = true; - } - } - if( !ret_set ){ - Assert( args.size()==n.getNumChildren() ); - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - args.insert( args.begin(), n.getOperator() ); - } - ret = NodeManager::currentNM()->mkNode( k, args ); - ret = Rewriter::rewrite( ret ); - watch_list_out[ret] = true; - } - }else{ - ret = n; - watch_list_out[ret] = true; - } - } - } - } - }else{ - Trace("term-db-eval") << "...exists in ee, return rep, exp size = " << exp_n.size() << std::endl; - merge_exp( exp, exp_n ); - } - Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret << ", exp size = " << exp.size() << std::endl; - visited[n] = ret; - return ret; - } -} - -void EqualityQueryInstProp::merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size ) { - //TODO : optimize - if( v.empty() ){ - Assert( up_to_size==-1 || up_to_size==(int)v_to_merge.size() ); - v.insert( v.end(), v_to_merge.begin(), v_to_merge.end() ); - }else{ - //std::vector< Node >::iterator v_end = v.end(); - up_to_size = up_to_size==-1 ? (int)v_to_merge.size() : up_to_size; - for( int j=0; j& terms, Node body ) { - d_active = true; - //information about the instance - d_q = q; - d_lem = lem; - Assert( d_terms.empty() ); - d_terms.insert( d_terms.end(), terms.begin(), terms.end() ); - //the current lemma - d_curr = body; - d_curr_exp.push_back( body ); -} - -InstPropagator::InstPropagator( QuantifiersEngine* qe ) : -d_qe( qe ), d_notify(*this), d_qy( qe ){ -} - -bool InstPropagator::reset( Theory::Effort e ) { - d_icount = 0; - d_ii.clear(); - for( unsigned i=0; i<2; i++ ){ - d_conc_to_id[i].clear(); - } - d_conflict = false; - d_watch_list.clear(); - d_relevant_inst.clear(); - return d_qy.reset( e ); -} - -void InstPropagator::notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) { - if( !d_conflict ){ - if( Trace.isOn("qip-prop") ){ - Trace("qip-prop") << "InstPropagator:: Notify instantiation " << q << " : " << std::endl; - for( unsigned i=0; i visited; - std::map< Node, bool > watch_list; - std::vector< TNode > props; - Node eval = d_qy.evaluateTermExp( ii.d_curr, ii.d_curr_exp, visited, true, true, watch_list, props ); - if( eval.isNull() ){ - ii.d_active = false; - }else if( firstTime || eval!=ii.d_curr ){ - if( EqualityQueryInstProp::isLiteral( eval ) ){ - props.push_back( eval ); - eval = d_qy.d_true; - watch_list.clear(); - } - if( Trace.isOn("qip-prop") ){ - Trace("qip-prop") << "Update info [" << id << "]..." << std::endl; - Trace("qip-prop") << "...updated lemma " << ii.d_curr << " -> " << eval << ", exp = "; - debugPrintExplanation( ii.d_curr_exp, "qip-prop" ); - Trace("qip-prop") << std::endl; - Trace("qip-prop") << "...watch list: " << std::endl; - for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw!=watch_list.end(); ++itw ){ - Trace("qip-prop") << " " << itw->first << std::endl; - } - Trace("qip-prop") << "...new propagations: " << std::endl; - for( unsigned i=0; i::iterator itw = watch_list.begin(); itw != watch_list.end(); ++itw ){ - d_watch_list[ itw->first ][ id ] = true; - } - }else{ - Trace("qip-prop-debug") << "...conclusion is duplicate." << std::endl; - ii.d_active = false; - } - } - }else{ - Trace("qip-prop-debug") << "...did not update." << std::endl; - } - Assert( !d_conflict ); - return true; -} - -void InstPropagator::propagate( Node a, Node b, bool pol, std::vector< Node >& exp ) { - if( Trace.isOn("qip-propagate") ){ - Trace("qip-propagate") << "* Propagate " << a << ( pol ? " == " : " != " ) << b << ", exp = "; - debugPrintExplanation( exp, "qip-propagate" ); - Trace("qip-propagate") << "..." << std::endl; - } - if( pol ){ - std::vector< Node > exp_d; - if( d_qy.areDisequalExp( a, b, exp_d ) ){ - Trace("qip-prop-debug") << "...conflict." << std::endl; - EqualityQueryInstProp::merge_exp( exp, exp_d ); - conflict( exp ); - }else{ - //set equal - int status = d_qy.setEqual( a, b, exp ); - if( status==EqualityQueryInstProp::STATUS_NONE ){ - Trace("qip-prop-debug") << "...already equal." << std::endl; - return; - }else if( status==EqualityQueryInstProp::STATUS_MERGED_KNOWN ){ - Assert( d_qy.getEngine()->hasTerm( a ) ); - Assert( d_qy.getEngine()->hasTerm( b ) ); - Trace("qip-prop-debug") << "...equality between known terms." << std::endl; - addRelevantInstances( exp, "qip-propagate" ); - } - Trace("qip-prop-debug") << "...merging " << a << " and " << b << std::endl; - for( unsigned i=0; i<2; i++ ){ - //update terms from watched lists - Node c = i==0 ? a : b; - std::map< Node, std::map< unsigned, bool > >::iterator it = d_watch_list.find( c ); - if( it!=d_watch_list.end() ){ - Trace("qip-prop-debug") << "...update ids from watch list of " << c << ", size=" << it->second.size() << "..." << std::endl; - for( std::map< unsigned, bool >::iterator itw = it->second.begin(); itw != it->second.end(); ++itw ){ - unsigned idw = itw->first; - if( std::find( d_update_list.begin(), d_update_list.end(), idw )==d_update_list.end() ){ - Trace("qip-prop-debug") << "...will update " << idw << std::endl; - d_update_list.push_back( idw ); - } - } - d_watch_list.erase( c ); - } - } - } - }else{ - std::vector< Node > exp_e; - if( d_qy.areEqualExp( a, b, exp_e ) ){ - EqualityQueryInstProp::merge_exp( exp, exp_e ); - conflict( exp ); - }else{ - //TODO? - } - } -} - -void InstPropagator::conflict( std::vector< Node >& exp ) { - Trace("qip-propagate") << "Conflict, exp size =" << exp.size() << std::endl; - d_conflict = true; - d_relevant_inst.clear(); - addRelevantInstances( exp, "qip-propagate" ); -} - -bool InstPropagator::cacheConclusion( unsigned id, Node body, int prop_index ) { - Assert( prop_index==0 || prop_index==1 ); - //check if the conclusion is non-redundant - if( d_conc_to_id[prop_index].find( body )==d_conc_to_id[prop_index].end() ){ - d_conc_to_id[prop_index][body] = id; - return true; - }else{ - return false; - } -} - -void InstPropagator::addRelevantInstances( std::vector< Node >& exp, const char * c ) { - for( unsigned i=0; i& exp, const char * c ) { - for( unsigned i=0; i + +#include "theory/quantifiers/inst_propagator.h" +#include "theory/rewriter.h" +#include "theory/quantifiers/term_database.h" + +using namespace CVC4; +using namespace std; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace CVC4::kind; + + +EqualityQueryInstProp::EqualityQueryInstProp( QuantifiersEngine* qe ) : d_qe( qe ){ + d_true = NodeManager::currentNM()->mkConst( true ); + d_false = NodeManager::currentNM()->mkConst( false ); +} + +bool EqualityQueryInstProp::reset( Theory::Effort e ) { + d_uf.clear(); + d_uf_exp.clear(); + d_diseq_list.clear(); + return true; +} + +/** contains term */ +bool EqualityQueryInstProp::hasTerm( Node a ) { + if( getEngine()->hasTerm( a ) ){ + return true; + }else{ + std::vector< Node > exp; + Node ar = getUfRepresentative( a, exp ); + return !ar.isNull() && getEngine()->hasTerm( ar ); + } +} + +/** get the representative of the equivalence class of a */ +Node EqualityQueryInstProp::getRepresentative( Node a ) { + if( getEngine()->hasTerm( a ) ){ + a = getEngine()->getRepresentative( a ); + } + std::vector< Node > exp; + Node ar = getUfRepresentative( a, exp ); + return ar.isNull() ? a : ar; +} + +/** returns true if a and b are equal in the current context */ +bool EqualityQueryInstProp::areEqual( Node a, Node b ) { + if( a==b ){ + return true; + }else{ + eq::EqualityEngine* ee = getEngine(); + if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ + if( ee->areEqual( a, b ) ){ + return true; + } + } + return false; + } +} + +/** returns true is a and b are disequal in the current context */ +bool EqualityQueryInstProp::areDisequal( Node a, Node b ) { + if( a==b ){ + return false; + }else{ + eq::EqualityEngine* ee = getEngine(); + if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ + if( ee->areDisequal( a, b, false ) ){ + return true; + } + } + return false; + } +} + +/** get the equality engine associated with this query */ +eq::EqualityEngine* EqualityQueryInstProp::getEngine() { + return d_qe->getMasterEqualityEngine(); +} + +/** get the equivalence class of a */ +void EqualityQueryInstProp::getEquivalenceClass( Node a, std::vector< Node >& eqc ) { + //TODO? +} + +TNode EqualityQueryInstProp::getCongruentTerm( Node f, std::vector< TNode >& args ) { + TNode t = d_qe->getTermDatabase()->getCongruentTerm( f, args ); + if( !t.isNull() ){ + return t; + }else{ + //TODO? + return TNode::null(); + } +} + +Node EqualityQueryInstProp::getRepresentativeExp( Node a, std::vector< Node >& exp ) { + bool engine_has_a = getEngine()->hasTerm( a ); + if( engine_has_a ){ + a = getEngine()->getRepresentative( a ); + } + //get union find representative, if this occurs in the equality engine, return it + unsigned prev_size = exp.size(); + Node ar = getUfRepresentative( a, exp ); + if( !ar.isNull() ){ + if( engine_has_a || getEngine()->hasTerm( ar ) ){ + Assert( getEngine()->hasTerm( ar ) ); + Assert( getEngine()->getRepresentative( ar )==ar ); + return ar; + } + }else{ + if( engine_has_a ){ + return a; + } + } + //retract explanation + while( exp.size()>prev_size ){ + exp.pop_back(); + } + return Node::null(); +} + +bool EqualityQueryInstProp::areEqualExp( Node a, Node b, std::vector< Node >& exp ) { + if( areEqual( a, b ) ){ + return true; + }else{ + std::vector< Node > exp_a; + Node ar = getUfRepresentative( a, exp_a ); + if( !ar.isNull() ){ + std::vector< Node > exp_b; + if( ar==getUfRepresentative( b, exp_b ) ){ + merge_exp( exp, exp_a ); + merge_exp( exp, exp_b ); + return true; + } + } + return false; + } +} + +bool EqualityQueryInstProp::areDisequalExp( Node a, Node b, std::vector< Node >& exp ) { + if( areDisequal( a, b ) ){ + return true; + }else{ + //TODO? + return false; + } +} + +Node EqualityQueryInstProp::getUfRepresentative( Node a, std::vector< Node >& exp ) { + Assert( exp.empty() ); + std::map< Node, Node >::iterator it = d_uf.find( a ); + if( it!=d_uf.end() ){ + if( it->second==a ){ + Assert( d_uf_exp[ a ].empty() ); + return it->second; + }else{ + Node m = getUfRepresentative( it->second, exp ); + Assert( !m.isNull() ); + if( m!=it->second ){ + //update union find + d_uf[ a ] = m; + //update explanation : merge the explanation of the parent + merge_exp( d_uf_exp[ a ], exp ); + Trace("qip-eq") << "EqualityQueryInstProp::getUfRepresentative : merge " << a << " -> " << m << ", exp size=" << d_uf_exp[ a ].size() << std::endl; + } + //add current explanation to exp: note that exp is a subset of d_uf_exp[ a ], reset + exp.clear(); + exp.insert( exp.end(), d_uf_exp[ a ].begin(), d_uf_exp[ a ].end() ); + return m; + } + }else{ + return Node::null(); + } +} + +// set a == b with reason, return status, modify a and b to representatives pre-merge +int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< Node >& reason ) { + if( a==b ){ + return pol ? STATUS_NONE : STATUS_CONFLICT; + } + int status = pol ? STATUS_MERGED_UNKNOWN : STATUS_NONE; + Trace("qip-eq") << "EqualityQueryInstProp::setEqual " << a << ", " << b << ", pol = " << pol << ", reason size = " << reason.size() << std::endl; + //get the representative for a + std::vector< Node > exp_a; + Node ar = getUfRepresentative( a, exp_a ); + if( ar.isNull() ){ + Assert( exp_a.empty() ); + ar = a; + } + if( ar==b ){ + Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl; + if( pol ){ + return STATUS_NONE; + }else{ + merge_exp( reason, exp_a ); + return STATUS_CONFLICT; + } + } + bool swap = false; + //get the representative for b + std::vector< Node > exp_b; + Node br = getUfRepresentative( b, exp_b ); + if( br.isNull() ){ + Assert( exp_b.empty() ); + br = b; + if( !getEngine()->hasTerm( br ) ){ + if( ar!=a || getEngine()->hasTerm( ar ) ){ + swap = true; + } + }else{ + if( getEngine()->hasTerm( ar ) ){ + status = STATUS_MERGED_KNOWN; + } + } + }else{ + if( ar==br ){ + Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl; + if( pol ){ + return STATUS_NONE; + }else{ + merge_exp( reason, exp_a ); + merge_exp( reason, exp_b ); + return STATUS_CONFLICT; + } + }else if( getEngine()->hasTerm( ar ) ){ + if( getEngine()->hasTerm( br ) ){ + status = STATUS_MERGED_KNOWN; + }else{ + swap = true; + } + } + } + + if( swap ){ + //swap + Node temp_r = ar; + ar = br; + br = temp_r; + } + + Assert( !getEngine()->hasTerm( ar ) || getEngine()->hasTerm( br ) ); + Assert( ar!=br ); + + std::vector< Node > exp_d; + if( areDisequalExp( ar, br, exp_d ) ){ + if( pol ){ + merge_exp( reason, exp_b ); + merge_exp( reason, exp_b ); + merge_exp( reason, exp_d ); + return STATUS_CONFLICT; + }else{ + return STATUS_NONE; + } + }else{ + if( pol ){ + //update the union find + Assert( d_uf_exp[ar].empty() ); + Assert( d_uf_exp[br].empty() ); + + d_uf[ar] = br; + merge_exp( d_uf_exp[ar], exp_a ); + merge_exp( d_uf_exp[ar], exp_b ); + merge_exp( d_uf_exp[ar], reason ); + + d_uf[br] = br; + d_uf_exp[br].clear(); + + Trace("qip-eq") << "EqualityQueryInstProp::setEqual : merge " << ar << " -> " << br << ", exp size = " << d_uf_exp[ar].size() << ", status = " << status << std::endl; + a = ar; + b = br; + return status; + }else{ + //TODO? + return STATUS_NONE; + } + } +} + +void EqualityQueryInstProp::addArgument( std::vector< Node >& args, std::vector< Node >& props, Node n, bool is_prop, bool pol ) { + if( is_prop ){ + if( isLiteral( n ) ){ + props.push_back( pol ? n : n.negate() ); + return; + } + } + args.push_back( n ); +} + +bool EqualityQueryInstProp::isLiteral( Node n ) { + Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind(); + Assert( ak!=NOT ); + return ak!=AND && ak!=OR && ak!=IFF && ak!=ITE; +} + +//this is identical to TermDb::evaluateTerm2, but tracks more information +Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, std::map< Node, Node >& visited, bool hasPol, bool pol, + std::map< Node, bool >& watch_list_out, std::vector< Node >& props ) { + std::map< Node, Node >::iterator itv = visited.find( n ); + if( itv != visited.end() ){ + return itv->second; + }else{ + visited[n] = n; + Trace("qip-eval") << "evaluate term : " << n << std::endl; + std::vector< Node > exp_n; + Node ret = getRepresentativeExp( n, exp_n ); + if( ret.isNull() ){ + //term is not known to be equal to a representative in equality engine, evaluate it + Kind k = n.getKind(); + if( k==FORALL ){ + ret = Node::null(); + }else{ + std::map< Node, bool > watch_list_out_curr; + TNode f = d_qe->getTermDatabase()->getMatchOperator( n ); + std::vector< Node > args; + bool ret_set = false; + bool childChanged = false; + int abort_i = -1; + //get the child entailed polarity + Assert( n.getKind()!=IMPLIES ); + bool newHasPol, newPol; + QuantPhaseReq::getEntailPolarity( n, 0, hasPol, pol, newHasPol, newPol ); + //for each child + for( unsigned i=0; i=2 ){ + //we are done if at least two args are unevaluated + abort_i = i; + break; + } + }else if( k==kind::ITE ){ + //we are done if we are ITE and condition is unevaluated + Assert( i==0 ); + args.push_back( c ); + abort_i = i; + break; + }else{ + args.push_back( c ); + } + } + } + //add remaining children if we aborted + if( abort_i!=-1 ){ + for( int i=(abort_i+1); i<(int)n.getNumChildren(); i++ ){ + args.push_back( n[i] ); + } + } + //copy over the watch list + for( std::map< Node, bool >::iterator itc = watch_list_out_curr.begin(); itc != watch_list_out_curr.end(); ++itc ){ + watch_list_out[itc->first] = itc->second; + } + + //if we have not short-circuited evaluation + if( !ret_set ){ + //if it is an indexed term, return the congruent term + if( !f.isNull() && watch_list_out.empty() ){ + std::vector< TNode > t_args; + for( unsigned i=0; imkNode( k, args ); + ret = Rewriter::rewrite( ret ); + //re-evaluate + Node ret_eval = getRepresentativeExp( ret, exp_n ); + if( !ret_eval.isNull() ){ + ret = ret_eval; + watch_list_out.clear(); + }else{ + watch_list_out[ret] = true; + } + } + }else{ + ret = n; + watch_list_out[ret] = true; + } + } + } + } + }else{ + Trace("qip-eval") << "...exists in ee, return rep, exp size = " << exp_n.size() << std::endl; + merge_exp( exp, exp_n ); + } + Trace("qip-eval") << "evaluated term : " << n << ", got : " << ret << ", exp size = " << exp.size() << std::endl; + visited[n] = ret; + return ret; + } +} + +void EqualityQueryInstProp::merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size ) { + //TODO : optimize + if( v.empty() ){ + Assert( up_to_size==-1 || up_to_size==(int)v_to_merge.size() ); + v.insert( v.end(), v_to_merge.begin(), v_to_merge.end() ); + }else{ + //std::vector< Node >::iterator v_end = v.end(); + up_to_size = up_to_size==-1 ? (int)v_to_merge.size() : up_to_size; + for( int j=0; j& terms, Node body ) { + d_active = true; + //information about the instance + d_q = q; + d_lem = lem; + Assert( d_terms.empty() ); + d_terms.insert( d_terms.end(), terms.begin(), terms.end() ); + //the current lemma + d_curr = body; + d_curr_exp.push_back( body ); +} + +InstPropagator::InstPropagator( QuantifiersEngine* qe ) : +d_qe( qe ), d_notify(*this), d_qy( qe ){ +} + +bool InstPropagator::reset( Theory::Effort e ) { + d_icount = 1; + d_ii.clear(); + for( unsigned i=0; i<2; i++ ){ + d_conc_to_id[i].clear(); + d_conc_to_id[i][d_qy.d_true] = 0; + } + d_conflict = false; + d_watch_list.clear(); + d_update_list.clear(); + d_relevant_inst.clear(); + return d_qy.reset( e ); +} + +bool InstPropagator::notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) { + if( !d_conflict ){ + if( Trace.isOn("qip-prop") ){ + Trace("qip-prop") << "InstPropagator:: Notify instantiation " << q << " : " << std::endl; + for( unsigned i=0; i visited; + std::map< Node, bool > watch_list; + std::vector< Node > props; + Node eval = d_qy.evaluateTermExp( ii.d_curr, ii.d_curr_exp, visited, true, true, watch_list, props ); + if( eval.isNull() ){ + ii.d_active = false; + }else if( firstTime || eval!=ii.d_curr ){ + if( EqualityQueryInstProp::isLiteral( eval ) ){ + props.push_back( eval ); + eval = d_qy.d_true; + watch_list.clear(); + } + if( Trace.isOn("qip-prop") ){ + Trace("qip-prop") << "Update info [" << id << "]..." << std::endl; + Trace("qip-prop") << "...updated lemma " << ii.d_curr << " -> " << eval << ", exp = "; + debugPrintExplanation( ii.d_curr_exp, "qip-prop" ); + Trace("qip-prop") << std::endl; + Trace("qip-prop") << "...watch list: " << std::endl; + for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw!=watch_list.end(); ++itw ){ + Trace("qip-prop") << " " << itw->first << std::endl; + } + Trace("qip-prop") << "...new propagations: " << std::endl; + for( unsigned i=0; i::iterator itw = watch_list.begin(); itw != watch_list.end(); ++itw ){ + d_watch_list[ itw->first ][ id ] = true; + } + }else{ + Trace("qip-prop-debug") << "...conclusion " << eval << " is duplicate." << std::endl; + ii.d_active = false; + } + } + }else{ + Trace("qip-prop-debug") << "...did not update." << std::endl; + } + Assert( !d_conflict ); + return true; +} + +void InstPropagator::propagate( Node a, Node b, bool pol, std::vector< Node >& exp ) { + if( Trace.isOn("qip-propagate") ){ + Trace("qip-propagate") << "* Propagate " << a << ( pol ? " == " : " != " ) << b << ", exp = "; + debugPrintExplanation( exp, "qip-propagate" ); + Trace("qip-propagate") << "..." << std::endl; + } + //set equal + int status = d_qy.setEqual( a, b, pol, exp ); + if( status==EqualityQueryInstProp::STATUS_NONE ){ + Trace("qip-prop-debug") << "...already equal/no conflict." << std::endl; + return; + }else if( status==EqualityQueryInstProp::STATUS_CONFLICT ){ + Trace("qip-prop-debug") << "...conflict." << std::endl; + conflict( exp ); + return; + } + if( pol ){ + if( status==EqualityQueryInstProp::STATUS_MERGED_KNOWN ){ + Assert( d_qy.getEngine()->hasTerm( a ) ); + Assert( d_qy.getEngine()->hasTerm( b ) ); + Trace("qip-prop-debug") << "...equality between known terms." << std::endl; + addRelevantInstances( exp, "qip-propagate" ); + } + Trace("qip-prop-debug") << "...merged representatives " << a << " and " << b << std::endl; + for( unsigned i=0; i<2; i++ ){ + //update terms from watched lists + Node c = i==0 ? a : b; + std::map< Node, std::map< unsigned, bool > >::iterator it = d_watch_list.find( c ); + if( it!=d_watch_list.end() ){ + Trace("qip-prop-debug") << "...update ids from watch list of " << c << ", size=" << it->second.size() << "..." << std::endl; + for( std::map< unsigned, bool >::iterator itw = it->second.begin(); itw != it->second.end(); ++itw ){ + unsigned idw = itw->first; + if( std::find( d_update_list.begin(), d_update_list.end(), idw )==d_update_list.end() ){ + Trace("qip-prop-debug") << "...will update " << idw << std::endl; + d_update_list.push_back( idw ); + } + } + d_watch_list.erase( c ); + } + } + } +} + +void InstPropagator::conflict( std::vector< Node >& exp ) { + Trace("qip-propagate") << "Conflict, exp size =" << exp.size() << std::endl; + d_conflict = true; + d_relevant_inst.clear(); + addRelevantInstances( exp, "qip-propagate" ); + + //now, inform quantifiers engine which instances should be retracted + for( std::map< unsigned, InstInfo >::iterator it = d_ii.begin(); it != d_ii.end(); ++it ){ + if( d_relevant_inst.find( it->first )==d_relevant_inst.end() ){ + if( !d_qe->removeInstantiation( it->second.d_q, it->second.d_lem, it->second.d_terms ) ){ + Trace("qip-warn") << "WARNING : did not remove instantiation id " << it->first << std::endl; + Assert( false ); + } + } + } + //will interupt the quantifiers engine + Trace("quant-engine-conflict") << "-----> InstPropagator::conflict with " << exp.size() << " instances." << std::endl; +} + +bool InstPropagator::cacheConclusion( unsigned id, Node body, int prop_index ) { + Assert( prop_index==0 || prop_index==1 ); + //check if the conclusion is non-redundant + if( d_conc_to_id[prop_index].find( body )==d_conc_to_id[prop_index].end() ){ + d_conc_to_id[prop_index][body] = id; + return true; + }else{ + return false; + } +} + +void InstPropagator::addRelevantInstances( std::vector< Node >& exp, const char * c ) { + for( unsigned i=0; i& exp, const char * c ) { + for( unsigned i=0; i -#include -#include -#include -#include "expr/node.h" -#include "expr/type_node.h" -#include "theory/quantifiers_engine.h" -#include "theory/quantifiers/term_database.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -class EqualityQueryInstProp : public EqualityQuery { -private: - /** pointer to quantifiers engine */ - QuantifiersEngine* d_qe; -public: - EqualityQueryInstProp( QuantifiersEngine* qe ); - ~EqualityQueryInstProp(){}; - /** reset */ - bool reset( Theory::Effort e ); - /** identify */ - std::string identify() const { return "EqualityQueryInstProp"; } - /** extends engine */ - bool extendsEngine() { return true; } - /** contains term */ - bool hasTerm( Node a ); - /** get the representative of the equivalence class of a */ - Node getRepresentative( Node a ); - /** returns true if a and b are equal in the current context */ - bool areEqual( Node a, Node b ); - /** returns true is a and b are disequal in the current context */ - bool areDisequal( Node a, Node b ); - /** get the equality engine associated with this query */ - eq::EqualityEngine* getEngine(); - /** get the equivalence class of a */ - void getEquivalenceClass( Node a, std::vector< Node >& eqc ); - /** get congruent term */ - TNode getCongruentTerm( Node f, std::vector< TNode >& args ); -public: - /** get the representative of the equivalence class of a, with explanation */ - Node getRepresentativeExp( Node a, std::vector< Node >& exp ); - /** returns true if a and b are equal in the current context */ - bool areEqualExp( Node a, Node b, std::vector< Node >& exp ); - /** returns true is a and b are disequal in the current context */ - bool areDisequalExp( Node a, Node b, std::vector< Node >& exp ); -private: - /** term index */ - std::map< Node, TermArgTrie > d_func_map_trie; - /** union find for terms beyond what is stored in equality engine */ - std::map< Node, Node > d_uf; - std::map< Node, std::vector< Node > > d_uf_exp; - Node getUfRepresentative( Node a, std::vector< Node >& exp ); - /** disequality list, stores explanations */ - std::map< Node, std::map< Node, Node > > d_diseq_list; - /** add arg */ - void addArgument( std::vector< TNode >& args, std::vector< TNode >& props, Node n, bool is_prop, bool pol ); -public: - enum { - STATUS_MERGED_KNOWN, - STATUS_MERGED_UNKNOWN, - STATUS_NONE, - }; - /** set equal */ - int setEqual( Node& a, Node& b, std::vector< Node >& reason ); - Node d_true; - Node d_false; -public: - //for explanations - static void merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size = -1 ); - - Node evaluateTermExp( TNode n, std::vector< Node >& exp, std::map< TNode, Node >& visited, bool hasPol, bool pol, - std::map< Node, bool >& watch_list_out, std::vector< TNode >& props ); - static bool isLiteral( Node n ); -}; - -class InstPropagator : public QuantifiersUtil { -private: - /** pointer to quantifiers engine */ - QuantifiersEngine* d_qe; - /** notify class */ - class InstantiationNotifyInstPropagator : public InstantiationNotify { - InstPropagator& d_ip; - public: - InstantiationNotifyInstPropagator(InstPropagator& ip): d_ip(ip) {} - virtual void notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) { d_ip.notifyInstantiation( quant_e, q, lem, terms, body ); } - }; - InstantiationNotifyInstPropagator d_notify; - /** notify instantiation method */ - void notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ); - /** equality query */ - EqualityQueryInstProp d_qy; - class InstInfo { - public: - bool d_active; - Node d_q; - Node d_lem; - std::vector< Node > d_terms; - // the current entailed body - Node d_curr; - //explanation for current entailed body - std::vector< Node > d_curr_exp; - void init( Node q, Node lem, std::vector< Node >& terms, Node body ); - }; - /** instantiation count/info */ - unsigned d_icount; - std::map< unsigned, InstInfo > d_ii; - std::map< TNode, unsigned > d_conc_to_id[2]; - /** are we in conflict */ - bool d_conflict; - /** watch list */ - std::map< Node, std::map< unsigned, bool > > d_watch_list; - /** update list */ - std::vector< unsigned > d_update_list; - /** relevant instances */ - std::map< unsigned, bool > d_relevant_inst; -private: - bool update( unsigned id, InstInfo& i, bool firstTime = false ); - void propagate( Node a, Node b, bool pol, std::vector< Node >& exp ); - void conflict( std::vector< Node >& exp ); - bool cacheConclusion( unsigned id, Node body, int prop_index = 0 ); - void addRelevantInstances( std::vector< Node >& exp, const char * c ); - - void debugPrintExplanation( std::vector< Node >& exp, const char * c ); -public: - InstPropagator( QuantifiersEngine* qe ); - ~InstPropagator(){} - /** reset */ - bool reset( Theory::Effort e ); - /** identify */ - std::string identify() const { return "InstPropagator"; } - /** get the notify mechanism */ - InstantiationNotify* getInstantiationNotify() { return &d_notify; } -}; - -} -} -} - -#endif +/********************* */ +/*! \file inst_propagator.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Propagate mechanism for instantiations + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__QUANTIFIERS_INST_PROPAGATOR_H +#define __CVC4__QUANTIFIERS_INST_PROPAGATOR_H + +#include +#include +#include +#include +#include "expr/node.h" +#include "expr/type_node.h" +#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/term_database.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class EqualityQueryInstProp : public EqualityQuery { +private: + /** pointer to quantifiers engine */ + QuantifiersEngine* d_qe; +public: + EqualityQueryInstProp( QuantifiersEngine* qe ); + ~EqualityQueryInstProp(){}; + /** reset */ + bool reset( Theory::Effort e ); + /** identify */ + std::string identify() const { return "EqualityQueryInstProp"; } + /** extends engine */ + bool extendsEngine() { return true; } + /** contains term */ + bool hasTerm( Node a ); + /** get the representative of the equivalence class of a */ + Node getRepresentative( Node a ); + /** returns true if a and b are equal in the current context */ + bool areEqual( Node a, Node b ); + /** returns true is a and b are disequal in the current context */ + bool areDisequal( Node a, Node b ); + /** get the equality engine associated with this query */ + eq::EqualityEngine* getEngine(); + /** get the equivalence class of a */ + void getEquivalenceClass( Node a, std::vector< Node >& eqc ); + /** get congruent term */ + TNode getCongruentTerm( Node f, std::vector< TNode >& args ); +public: + /** get the representative of the equivalence class of a, with explanation */ + Node getRepresentativeExp( Node a, std::vector< Node >& exp ); + /** returns true if a and b are equal in the current context */ + bool areEqualExp( Node a, Node b, std::vector< Node >& exp ); + /** returns true is a and b are disequal in the current context */ + bool areDisequalExp( Node a, Node b, std::vector< Node >& exp ); +private: + /** term index */ + std::map< Node, TermArgTrie > d_func_map_trie; + /** union find for terms beyond what is stored in equality engine */ + std::map< Node, Node > d_uf; + std::map< Node, std::vector< Node > > d_uf_exp; + Node getUfRepresentative( Node a, std::vector< Node >& exp ); + /** disequality list, stores explanations */ + std::map< Node, std::map< Node, Node > > d_diseq_list; + /** add arg */ + void addArgument( std::vector< Node >& args, std::vector< Node >& props, Node n, bool is_prop, bool pol ); +public: + enum { + STATUS_CONFLICT, + STATUS_MERGED_KNOWN, + STATUS_MERGED_UNKNOWN, + STATUS_NONE, + }; + /** set equal */ + int setEqual( Node& a, Node& b, bool pol, std::vector< Node >& reason ); + Node d_true; + Node d_false; +public: + //for explanations + static void merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size = -1 ); + + Node evaluateTermExp( Node n, std::vector< Node >& exp, std::map< Node, Node >& visited, bool hasPol, bool pol, + std::map< Node, bool >& watch_list_out, std::vector< Node >& props ); + static bool isLiteral( Node n ); +}; + +class InstPropagator : public QuantifiersUtil { +private: + /** pointer to quantifiers engine */ + QuantifiersEngine* d_qe; + /** notify class */ + class InstantiationNotifyInstPropagator : public InstantiationNotify { + InstPropagator& d_ip; + public: + InstantiationNotifyInstPropagator(InstPropagator& ip): d_ip(ip) {} + virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) { + return d_ip.notifyInstantiation( quant_e, q, lem, terms, body ); + } + }; + InstantiationNotifyInstPropagator d_notify; + /** notify instantiation method */ + bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ); + /** equality query */ + EqualityQueryInstProp d_qy; + class InstInfo { + public: + bool d_active; + Node d_q; + Node d_lem; + std::vector< Node > d_terms; + // the current entailed body + Node d_curr; + //explanation for current entailed body + std::vector< Node > d_curr_exp; + void init( Node q, Node lem, std::vector< Node >& terms, Node body ); + }; + /** instantiation count/info */ + unsigned d_icount; + std::map< unsigned, InstInfo > d_ii; + std::map< Node, unsigned > d_conc_to_id[2]; + /** are we in conflict */ + bool d_conflict; + /** watch list */ + std::map< Node, std::map< unsigned, bool > > d_watch_list; + /** update list */ + std::vector< unsigned > d_update_list; + /** relevant instances */ + std::map< unsigned, bool > d_relevant_inst; +private: + bool update( unsigned id, InstInfo& i, bool firstTime = false ); + void propagate( Node a, Node b, bool pol, std::vector< Node >& exp ); + void conflict( std::vector< Node >& exp ); + bool cacheConclusion( unsigned id, Node body, int prop_index = 0 ); + void addRelevantInstances( std::vector< Node >& exp, const char * c ); + + void debugPrintExplanation( std::vector< Node >& exp, const char * c ); +public: + InstPropagator( QuantifiersEngine* qe ); + ~InstPropagator(){} + /** reset */ + bool reset( Theory::Effort e ); + /** identify */ + std::string identify() const { return "InstPropagator"; } + /** get the notify mechanism */ + InstantiationNotify* getInstantiationNotify() { return &d_notify; } +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index e38304c68..cc9b56a7c 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -107,6 +107,7 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) { if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ + Assert( !d_quantEngine->inConflict() ); double clSet = 0; if( Trace.isOn("cbqi-engine") ){ clSet = double(clock())/double(CLOCKS_PER_SEC); @@ -118,9 +119,12 @@ void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) { Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ process( q, e, ee ); + if( d_quantEngine->inConflict() ){ + break; + } } } - if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){ + if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){ break; } } @@ -567,8 +571,8 @@ Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){ //new implementation -bool CegqiOutputInstStrategy::addInstantiation( std::vector< Node >& subs ) { - return d_out->addInstantiation( subs ); +bool CegqiOutputInstStrategy::doAddInstantiation( std::vector< Node >& subs ) { + return d_out->doAddInstantiation( subs ); } bool CegqiOutputInstStrategy::isEligibleForInstantiation( Node n ) { @@ -636,13 +640,13 @@ void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { } } -bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs ) { +bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { Assert( !d_curr_quant.isNull() ); //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 ); + d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false, true ); return true; }else{ //check if we need virtual term substitution (if used delta or infinity) diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index d53d9d81c..8ed59778b 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -122,7 +122,7 @@ class CegqiOutputInstStrategy : public CegqiOutput { public: CegqiOutputInstStrategy( InstStrategyCegqi * out ) : d_out( out ){} InstStrategyCegqi * d_out; - bool addInstantiation( std::vector< Node >& subs ); + bool doAddInstantiation( std::vector< Node >& subs ); bool isEligibleForInstantiation( Node n ); bool addLemma( Node lem ); }; @@ -143,7 +143,7 @@ public: InstStrategyCegqi( QuantifiersEngine * qe ); ~InstStrategyCegqi() throw(); - bool addInstantiation( std::vector< Node >& subs ); + bool doAddInstantiation( std::vector< Node >& subs ); bool isEligibleForInstantiation( Node n ); bool addLemma( Node lem ); /** identify */ diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 8c3154c1c..6d6991476 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -106,7 +106,9 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){ if( d_user_gen[f][i]->isMultiTrigger() ){ d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst; } - //d_quantEngine->d_hasInstantiated[f] = true; + if( d_quantEngine->inConflict() ){ + break; + } } } } @@ -229,11 +231,13 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) if( r==1 ){ d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst; } - //d_quantEngine->d_hasInstantiated[f] = true; + if( d_quantEngine->inConflict() ){ + break; + } } } } - if( hasInst && options::multiTriggerPriority() ){ + if( d_quantEngine->inConflict() || ( hasInst && options::multiTriggerPriority() ) ){ break; } } @@ -575,6 +579,9 @@ void FullSaturation::check( Theory::Effort e, unsigned quant_e ) { if( process( q, fullEffort ) ){ //added lemma addedLemmas++; + if( d_quantEngine->inConflict() ){ + break; + } } } } diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 8e88d3434..b59734720 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -60,7 +60,7 @@ void InstantiationEngine::presolve() { } } -bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ +void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting(); //iterate over an internal effort level e int e = 0; @@ -83,8 +83,10 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ InstStrategy* is = d_instStrategies[j]; Trace("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl; int quantStatus = is->process( q, effort, e_use ); - Trace("inst-engine-debug") << " -> status is " << quantStatus << std::endl; - if( quantStatus==InstStrategy::STATUS_UNFINISHED ){ + Trace("inst-engine-debug") << " -> status is " << quantStatus << ", conflict=" << d_quantEngine->inConflict() << std::endl; + if( d_quantEngine->inConflict() ){ + return; + }else if( quantStatus==InstStrategy::STATUS_UNFINISHED ){ finished = false; } } @@ -96,13 +98,6 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ } e++; } - //Notice() << "All instantiators finished, # added lemmas = " << (int)d_lemmas_waiting.size() << std::endl; - if( !d_quantEngine->hasAddedLemma() ){ - return false; - }else{ - Trace("inst-engine") << "Added lemmas = " << (int)(d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; - return true; - } } bool InstantiationEngine::needsCheck( Theory::Effort e ){ @@ -138,8 +133,18 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ Trace("inst-engine-debug") << "InstEngine: check: # asserted quantifiers " << d_quants.size() << "/"; Trace("inst-engine-debug") << d_quantEngine->getModel()->getNumAssertedQuantifiers() << " " << quantActive << std::endl; if( quantActive ){ - bool addedLemmas = doInstantiationRound( e ); - Trace("inst-engine-debug") << "Add lemmas = " << addedLemmas << std::endl; + unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting(); + doInstantiationRound( e ); + if( d_quantEngine->inConflict() ){ + Assert( d_quantEngine->getNumLemmasWaiting()>lastWaiting ); + Trace("inst-engine") << "Conflict, size = " << d_quantEngine->getNumLemmasWaiting(); + if( lastWaiting>0 ){ + Trace("inst-engine") << " (prev " << lastWaiting << ")"; + } + Trace("inst-engine") << std::endl; + }else if( d_quantEngine->hasAddedLemma() ){ + Trace("inst-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; + } }else{ d_quants.clear(); } diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 4d1d4a20f..d2b3740a1 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -70,7 +70,7 @@ private: /** is the engine incomplete for this quantifier */ bool isIncomplete( Node q ); /** do instantiation round */ - bool doInstantiationRound( Theory::Effort effort ); + void doInstantiationRound( Theory::Effort effort ); public: InstantiationEngine( QuantifiersEngine* qe ); ~InstantiationEngine(); diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index bcd36f37a..bdb416b6b 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -155,11 +155,15 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { int lems = initializeQuantifier( f, f ); d_statistics.d_init_inst_gen_lemmas += lems; d_addedLemmas += lems; + if( d_qe->inConflict() ){ + break; + } } } if( d_addedLemmas>0 ){ Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas << std::endl; }else{ + Assert( !d_qe->inConflict() ); //initialize model fm->initialize(); //analyze the functions @@ -202,7 +206,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { }else{ d_numQuantNoSelForm++; } - if( options::fmfInstGenOneQuantPerRound() && lems>0 ){ + if( d_qe->inConflict() || ( options::fmfInstGenOneQuantPerRound() && lems>0 ) ){ break; } }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){ @@ -428,6 +432,9 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i //add as instantiation if( d_qe->addInstantiation( f, m ) ){ d_addedLemmas++; + if( d_qe->inConflict() ){ + break; + } //if the instantiation is show to be false, and we wish to skip multiple instantiations at once if( eval==-1 ){ riter.increment2( depIndex ); diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 51dccae49..a7e272be0 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -62,6 +62,7 @@ void ModelEngine::reset_round( Theory::Effort e ) { void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){ + Assert( !d_quantEngine->inConflict() ); int addedLemmas = 0; FirstOrderModel* fm = d_quantEngine->getModel(); @@ -100,8 +101,6 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ //CVC4 will answer SAT or unknown Trace("fmf-consistent") << std::endl; debugPrint("fmf-consistent"); - }else{ - //otherwise, the search will continue } } } @@ -194,33 +193,40 @@ int ModelEngine::checkModel(){ // FMC uses two sub-effort levels int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 ); for( int e=0; egetNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl; - //determine if we should check this quantifier - if( considerQuantifiedFormula( f ) ){ - exhaustiveInstantiate( f, e ); - if( Trace.isOn("model-engine-warn") ){ - if( d_addedLemmas>10000 ){ - Debug("fmf-exit") << std::endl; - debugPrint("fmf-exit"); - exit( 0 ); - } - } - if( optOneQuantPerRound() && d_addedLemmas>0 ){ - break; + for( int i=0; igetNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl; + //determine if we should check this quantifier + if( considerQuantifiedFormula( f ) ){ + exhaustiveInstantiate( f, e ); + if( Trace.isOn("model-engine-warn") ){ + if( d_addedLemmas>10000 ){ + Debug("fmf-exit") << std::endl; + debugPrint("fmf-exit"); + exit( 0 ); } - }else{ - Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl; } + if( d_quantEngine->inConflict() || ( optOneQuantPerRound() && d_addedLemmas>0 ) ){ + break; + } + }else{ + Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl; } } + if( d_addedLemmas>0 ){ + break; + }else{ + Assert( !d_quantEngine->inConflict() ); + } } //print debug information - Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / "; - Trace("model-engine") << d_totalLemmas << std::endl; + if( d_quantEngine->inConflict() ){ + Trace("model-engine") << "Conflict, size = " << d_quantEngine->getNumLemmasWaiting() << std::endl; + }else{ + Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / "; + Trace("model-engine") << d_totalLemmas << std::endl; + } return d_addedLemmas; } @@ -266,11 +272,13 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ d_incomplete_check = d_incomplete_check || mb->d_incomplete_check; d_statistics.d_mbqi_inst_lemmas += mb->d_addedLemmas; }else{ - Trace("fmf-exh-inst-debug") << " Instantiation Constants: "; - for( size_t i=0; igetTermDatabase()->getInstantiationConstant( f, i ) << " "; + if( Trace.isOn("fmf-exh-inst-debug") ){ + Trace("fmf-exh-inst-debug") << " Instantiation Constants: "; + for( size_t i=0; igetTermDatabase()->getInstantiationConstant( f, i ) << " "; + } + Trace("fmf-exh-inst-debug") << std::endl; } - Trace("fmf-exh-inst-debug") << std::endl; //create a rep set iterator and iterate over the (relevant) domain of the quantifier RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) ); if( riter.setQuantifier( f ) ){ @@ -289,6 +297,9 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ //add as instantiation if( d_quantEngine->addInstantiation( f, m ) ){ addedLemmas++; + if( d_quantEngine->inConflict() ){ + break; + } }else{ Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl; } diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index c5ccd9d82..5bf8d8a8d 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -68,7 +68,7 @@ bool RewriteEngine::needsCheck( Theory::Effort e ){ void RewriteEngine::check( Theory::Effort e, unsigned quant_e ) { if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ - //if( e==Theory::EFFORT_FULL ){ + Assert( !d_quantEngine->inConflict() ); Trace("rewrite-engine") << "---Rewrite Engine Round, effort = " << e << "---" << std::endl; //if( e==Theory::EFFORT_LAST_CALL ){ // if( !d_quantEngine->getModel()->isModelSet() ){ @@ -95,7 +95,7 @@ void RewriteEngine::check( Theory::Effort e, unsigned quant_e ) { //per priority level int index = 0; bool success = true; - while( success && index<(int)d_priority_order.size() ) { + while( !d_quantEngine->inConflict() && success && index<(int)d_priority_order.size() ) { addedLemmas += checkRewriteRule( d_priority_order[index], e ); index++; if( index<(int)d_priority_order.size() ){ @@ -104,11 +104,6 @@ void RewriteEngine::check( Theory::Effort e, unsigned quant_e ) { } Trace("rewrite-engine") << "Finished rewrite engine, added " << addedLemmas << " lemmas." << std::endl; - if (addedLemmas==0) { - - }else{ - //otherwise, the search will continue - } } } @@ -129,7 +124,7 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) { Trace("rewrite-engine-inst-debug") << " Reset round..." << std::endl; qi->reset_round( qcf ); Trace("rewrite-engine-inst-debug") << " Get matches..." << std::endl; - while( qi->getNextMatch( qcf ) && + while( !d_quantEngine->inConflict() && qi->getNextMatch( qcf ) && ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){ Trace("rewrite-engine-inst-debug") << " Got match to complete..." << std::endl; qi->debugPrintMatch( "rewrite-engine-inst-debug" ); @@ -138,7 +133,7 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) { bool doContinue = false; bool success = true; int tempAddedLemmas = 0; - while( tempAddedLemmas==0 && success && ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){ + while( !d_quantEngine->inConflict() && tempAddedLemmas==0 && success && ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){ success = qi->completeMatch( qcf, assigned, doContinue ); doContinue = true; if( success ){ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 839077a40..f98a3fd75 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -57,6 +57,8 @@ using namespace CVC4::theory::inst; QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te): d_te( te ), + //d_quants(u), + //d_quants_red(u), d_lemmas_produced_c(u), d_skolemized(u), d_ierCounter_c(c), @@ -71,10 +73,10 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* //utilities d_eq_query = new EqualityQueryQuantifiersEngine( c, this ); d_util.push_back( d_eq_query ); - + d_term_db = new quantifiers::TermDb( c, u, this ); d_util.push_back( d_term_db ); - + if( options::instPropagate() ){ d_inst_prop = new quantifiers::InstPropagator( this ); d_util.push_back( d_inst_prop ); @@ -84,6 +86,8 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* } d_tr_trie = new inst::TriggerTrie; + d_curr_effort_level = QEFFORT_NONE; + d_conflict = false; d_hasAddedLemma = false; //don't add true lemma d_lemmas_produced_c[d_term_db->d_true] = true; @@ -125,7 +129,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_rel_dom = NULL; d_builder = NULL; - d_curr_effort_level = QEFFORT_NONE; d_total_inst_count_debug = 0; //allow theory combination to go first, once initially d_ierCounter = options::instWhenTcFirst() ? 0 : 1; @@ -243,7 +246,7 @@ void QuantifiersEngine::finishInit(){ d_lte_part_inst = new quantifiers::LtePartialInst( this, c ); d_modules.push_back( d_lte_part_inst ); } - if( ( options::finiteModelFind() && options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ) || + if( ( options::finiteModelFind() && options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ) || options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){ d_qsplit = new quantifiers::QuantDSplit( this, c ); d_modules.push_back( d_qsplit ); @@ -361,6 +364,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } + d_conflict = false; d_hasAddedLemma = false; bool setIncomplete = false; if( e==Theory::EFFORT_LAST_CALL ){ @@ -379,7 +383,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( d_hasAddedLemma ){ return; } - + if( Trace.isOn("quant-engine-debug") ){ Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl; Trace("quant-engine-debug") << " depth : " << d_ierCounter_c << std::endl; @@ -404,7 +408,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine-assert") << "Assertions : " << std::endl; getTheoryEngine()->printAssertions("quant-engine-assert"); } - + //reset utilities for( unsigned i=0; iidentify().c_str() << "..." << std::endl; @@ -426,7 +430,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ //reset the model d_model->reset_round(); - + //reset the modules for( unsigned i=0; iidentify().c_str() << std::endl; @@ -437,6 +441,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ flushLemmas(); if( d_hasAddedLemma ){ return; + } if( e==Theory::EFFORT_LAST_CALL ){ @@ -468,6 +473,10 @@ void QuantifiersEngine::check( Theory::Effort e ){ for( unsigned i=0; iidentify().c_str() << " at effort " << quant_e << "..." << std::endl; qm[i]->check( e, quant_e ); + if( d_conflict ){ + Trace("quant-engine-debug") << "...conflict!" << std::endl; + break; + } } } //flush all current lemmas @@ -476,6 +485,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( d_hasAddedLemma ){ break; }else{ + Assert( !d_conflict ); if( quant_e==QEFFORT_CONFLICT ){ if( e==Theory::EFFORT_FULL ){ //increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase @@ -573,7 +583,7 @@ bool QuantifiersEngine::reduceQuantifier( Node q ) { d_quants_red[q] = false; return false; }else{ - return it->second; + return (*it).second; } } @@ -619,7 +629,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ return true; } }else{ - return it->second; + return (*it).second; } } @@ -745,7 +755,11 @@ void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< No } -bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq, bool modInst ) { +bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq, bool modInst, bool addedLem ) { + if( !addedLem ){ + //record the instantiation for deletion later + //TODO + } if( options::incrementalSolving() ){ Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << ", modInst = " << modInst << std::endl; inst::CDInstMatchTrie* imt; @@ -763,6 +777,19 @@ bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node > } } +bool QuantifiersEngine::removeInstantiationInternal( Node q, std::vector< Node >& terms ) { + if( options::incrementalSolving() ){ + std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q ); + if( it!=d_c_inst_match_trie.end() ){ + return it->second->removeInstMatch( this, q, terms ); + }else{ + return false; + } + }else{ + return d_inst_match_trie[q].removeInstMatch( this, q, terms ); + } +} + 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 @@ -903,7 +930,8 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){ lem = Rewriter::rewrite(lem); } Trace("inst-add-debug") << "Adding lemma : " << lem << std::endl; - if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){ + BoolMap::const_iterator itp = d_lemmas_produced_c.find( lem ); + if( itp==d_lemmas_produced_c.end() || !(*itp).second ){ //d_curr_out->lemma( lem, false, true ); d_lemmas_produced_c[ lem ] = true; d_lemmas_waiting.push_back( lem ); @@ -920,6 +948,17 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){ } } +bool QuantifiersEngine::removeLemma( Node lem ) { + std::vector< Node >::iterator it = std::find( d_lemmas_waiting.begin(), d_lemmas_waiting.end(), lem ); + if( it!=d_lemmas_waiting.end() ){ + d_lemmas_waiting.erase( it, it + 1 ); + d_lemmas_produced_c[ lem ] = false; + return true; + }else{ + return false; + } +} + void QuantifiersEngine::addRequirePhase( Node lit, bool req ){ d_phase_req_waiting[lit] = req; } @@ -933,7 +972,7 @@ bool QuantifiersEngine::addInstantiation( Node q, InstMatch& m, bool mkRep, bool bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst, bool doVts ) { // For resource-limiting (also does a time check). getOutputChannel().safePoint(options::quantifierStep()); - + Assert( !d_conflict ); Assert( terms.size()==q[0].getNumChildren() ); Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl; for( unsigned i=0; i& terms, bo } Trace("inst-add-debug") << " -> " << terms[i] << std::endl; if( terms[i].isNull() ){ - Trace("inst-add-debug") << " -> Failed to make term vector, due to term/type restrictions." << std::endl; + Trace("inst-add-debug") << " --> Failed to make term vector, due to term/type restrictions." << std::endl; return false; } #ifdef CVC4_ASSERTIONS @@ -967,7 +1006,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo bad_inst = true; }else{ bad_inst = quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[q] ); - } + } } } //this assertion is critical to soundness @@ -977,7 +1016,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo Trace("inst") << " " << terms[j] << std::endl; } Assert( false ); - } + } #endif } @@ -989,7 +1028,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo } } } - + //check for positive entailment if( options::instNoEntail() ){ //TODO: check consistency of equality engine (if not aborting on utility's reset) @@ -998,7 +1037,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo subs[q[0][i]] = terms[i]; } if( d_term_db->isEntailed( q[1], subs, false, true ) ){ - Trace("inst-add-debug") << " -> Currently entailed." << std::endl; + Trace("inst-add-debug") << " --> Currently entailed." << std::endl; return false; } //Node eval = d_term_db->evaluateTerm( q[1], subs, false, true ); @@ -1009,7 +1048,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo //check for term vector duplication bool alreadyExists = !recordInstantiationInternal( q, terms, modEq, modInst ); if( alreadyExists ){ - Trace("inst-add-debug") << " -> Already exists." << std::endl; + Trace("inst-add-debug") << " --> Already exists." << std::endl; ++(d_statistics.d_inst_duplicate_eq); return false; } @@ -1021,7 +1060,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo body = quantifiers::QuantifiersRewriter::preprocess( body, true ); Trace("inst-debug") << "...preprocess to " << body << std::endl; - //construct the lemma + //construct the lemma Trace("inst-assert") << "(assert " << body << ")" << std::endl; body = Rewriter::rewrite(body); Node lem = NodeManager::currentNM()->mkNode( kind::OR, q.negate(), body ); @@ -1055,17 +1094,21 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo } setInstantiationLevelAttr( body, q[1], maxInstLevel+1 ); } - if( d_curr_effort_level>QEFFORT_CONFLICT ){ + if( d_curr_effort_level>QEFFORT_CONFLICT && d_curr_effort_levelnotifyInstantiation( d_curr_effort_level, q, lem, terms, body ); + if( !d_inst_notify[j]->notifyInstantiation( d_curr_effort_level, q, lem, terms, body ) ){ + Trace("inst-add-debug") << "...we are in conflict." << std::endl; + d_conflict = true; + Assert( !d_lemmas_waiting.empty() ); + } } } - Trace("inst-add-debug") << " -> Success." << std::endl; + Trace("inst-add-debug") << " --> Success." << std::endl; ++(d_statistics.d_instantiations); return true; }else{ - Trace("inst-add-debug") << " -> Lemma already exists." << std::endl; + Trace("inst-add-debug") << " --> Lemma already exists." << std::endl; ++(d_statistics.d_inst_duplicate); return false; } @@ -1090,6 +1133,16 @@ bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool return addSplit( fm ); } +bool QuantifiersEngine::removeInstantiation( Node q, Node lem, std::vector< Node >& terms ) { + //lem must occur in d_waiting_lemmas + if( removeLemma( lem ) ){ + return removeInstantiationInternal( q, terms ); + }else{ + return false; + } +} + + bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl; //determine if we should perform check, based on instWhenMode diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 9ee967eb0..bad9c0169 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -47,7 +47,7 @@ namespace quantifiers { class InstantiationNotify { public: InstantiationNotify(){} - virtual void notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) = 0; + virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) = 0; }; namespace quantifiers { @@ -151,9 +151,14 @@ public: //effort levels //none QEFFORT_NONE, }; -private: +private: //this information is reset during check /** current effort level */ unsigned d_curr_effort_level; + /** are we in conflict */ + bool d_conflict; + /** has added lemma this round */ + bool d_hasAddedLemma; +private: /** list of all quantifiers seen */ std::map< Node, bool > d_quants; /** quantifiers reduced */ @@ -165,8 +170,6 @@ private: std::vector< Node > d_lemmas_waiting; /** phase requirements waiting */ std::map< Node, bool > d_phase_req_waiting; - /** has added lemma this round */ - bool d_hasAddedLemma; /** list of all instantiations produced for each quantifier */ std::map< Node, inst::InstMatchTrie > d_inst_match_trie; std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie; @@ -282,7 +285,9 @@ private: /** compute term vector */ void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ); /** record instantiation, return true if it was non-duplicate */ - bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool modInst = false ); + bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool modInst = false, bool addedLem = true ); + /** remove instantiation */ + bool removeInstantiationInternal( Node q, std::vector< Node >& terms ); /** set instantiation level attr */ static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level ); /** flush lemmas */ @@ -298,18 +303,24 @@ public: Node getSubstitute( Node n, std::vector< Node >& terms ); /** add lemma lem */ bool addLemma( Node lem, bool doCache = true, bool doRewrite = true ); + /** remove pending lemma */ + bool removeLemma( Node lem ); /** add require phase */ void addRequirePhase( Node lit, bool req ); /** do instantiation specified by m */ bool addInstantiation( Node q, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false ); /** add instantiation */ bool addInstantiation( Node q, std::vector< Node >& terms, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false ); + /** remove pending instantiation */ + bool removeInstantiation( Node q, Node lem, std::vector< Node >& terms ); /** split on node n */ bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true ); /** add split equality */ bool addSplitEquality( Node n1, Node n2, bool reqPhase = false, bool reqPhasePol = true ); /** has added lemma */ bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; } + /** is in conflict */ + bool inConflict() { return d_conflict; } /** get number of waiting lemmas */ unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); } /** get needs check */ @@ -328,7 +339,7 @@ public: /** get trigger database */ inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; } /** add term to database */ - void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false ); + void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false ); /** notification when master equality engine is updated */ void eqNotifyNewClass(TNode t); void eqNotifyPreMerge(TNode t1, TNode t2); diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 575aa4159..91e0c37d4 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -38,7 +38,6 @@ TESTS = \ lst-no-self-rev-exp.smt2 \ fib-core.smt2 \ fore19-exp2-core.smt2 \ - with-ind-104-core.smt2 \ syn002-si-real-int.smt2 \ krs-sat.smt2 \ forall_unit_data2.smt2 \ -- cgit v1.2.3 From 4ff2946e1338d3f500b7e6bababee50fadad68d6 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 12 Apr 2016 10:13:45 -0500 Subject: Optimizations for QCF to check relevant domain of variable argument positions eagerly, global ordering mechanism for quantified formulas within check. Refactoring of term database. --- src/options/options_handler.cpp | 2 - src/options/quantifiers_modes.h | 2 - src/theory/quantifiers/anti_skolem.cpp | 2 +- src/theory/quantifiers/candidate_generator.cpp | 1 - src/theory/quantifiers/conjecture_generator.cpp | 18 +- src/theory/quantifiers/conjecture_generator.h | 2 +- src/theory/quantifiers/first_order_model.cpp | 89 ++++++++- src/theory/quantifiers/first_order_model.h | 16 +- src/theory/quantifiers/full_model_check.cpp | 6 +- src/theory/quantifiers/inst_propagator.cpp | 3 + src/theory/quantifiers/inst_strategy_cbqi.cpp | 34 ++-- .../quantifiers/inst_strategy_e_matching.cpp | 15 +- src/theory/quantifiers/instantiation_engine.cpp | 6 +- src/theory/quantifiers/model_builder.cpp | 14 +- src/theory/quantifiers/model_engine.cpp | 51 +++--- src/theory/quantifiers/quant_conflict_find.cpp | 201 ++++++++++----------- src/theory/quantifiers/quant_conflict_find.h | 14 +- src/theory/quantifiers/relevant_domain.cpp | 2 +- src/theory/quantifiers/rewrite_engine.cpp | 2 +- src/theory/quantifiers/term_database.cpp | 64 +++++-- src/theory/quantifiers/term_database.h | 50 +++-- src/theory/quantifiers_engine.cpp | 26 ++- src/theory/quantifiers_engine.h | 6 + test/regress/regress0/quantifiers/Makefile.am | 3 +- .../regress0/quantifiers/qcf-rel-dom-opt.smt2 | 45 +++++ 25 files changed, 432 insertions(+), 242 deletions(-) create mode 100644 test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2 (limited to 'src/theory/quantifiers/instantiation_engine.cpp') diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index d08f5f533..a2809bd67 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -576,8 +576,6 @@ theory::quantifiers::QcfMode OptionsHandler::stringToQcfMode(std::string option, return theory::quantifiers::QCF_PROP_EQ; } else if(optarg == "partial") { return theory::quantifiers::QCF_PARTIAL; - } else if(optarg == "mc" ) { - return theory::quantifiers::QCF_MC; } else if(optarg == "help") { puts(s_qcfModeHelp.c_str()); exit(1); diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index a437cfc97..5749da972 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -83,8 +83,6 @@ enum QcfMode { QCF_PROP_EQ, /** use qcf for conflicts, propagations and heuristic instantiations */ QCF_PARTIAL, - /** use qcf for model checking */ - QCF_MC, }; enum UserPatMode { diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp index ed000427f..c8d18aced 100644 --- a/src/theory/quantifiers/anti_skolem.cpp +++ b/src/theory/quantifiers/anti_skolem.cpp @@ -82,7 +82,7 @@ QuantAntiSkolem::QuantAntiSkolem( QuantifiersEngine * qe ) : QuantifiersModule( void QuantAntiSkolem::check( Theory::Effort e, unsigned quant_e ) { if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ d_sqtc.clear(); - for( int i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ + for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); if( d_quant_processed.find( q )==d_quant_processed.end() ){ d_quant_processed[q] = true; diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 38d8c0d81..43f5ee2fd 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -298,7 +298,6 @@ Node CandidateGeneratorQEAll::getNextCandidate() { } } if( d_firstTime ){ - Assert( d_qe->getTermDatabase()->d_type_map[d_match_pattern_type].empty() ); //must return something d_firstTime = false; return d_qe->getTermDatabase()->getModelBasisTerm( d_match_pattern_type ); diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index f8a9eefcb..27bbb0f5f 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -34,7 +34,7 @@ struct sortConjectureScore { }; -void OpArgIndex::addTerm( ConjectureGenerator * s, TNode n, unsigned index ){ +void OpArgIndex::addTerm( std::vector< TNode >& terms, TNode n, unsigned index ){ if( index==n.getNumChildren() ){ Assert( n.hasOperator() ); if( std::find( d_ops.begin(), d_ops.end(), n.getOperator() )==d_ops.end() ){ @@ -42,7 +42,7 @@ void OpArgIndex::addTerm( ConjectureGenerator * s, TNode n, unsigned index ){ d_op_terms.push_back( n ); } }else{ - d_child[s->getTermDatabase()->d_arg_reps[n][index]].addTerm( s, n, index+1 ); + d_child[terms[index]].addTerm( terms, n, index+1 ); } } @@ -369,7 +369,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { TNode n = (*ieqc_i); if( getTermDatabase()->hasTermCurrent( n ) ){ if( isHandledTerm( n ) ){ - d_op_arg_index[r].addTerm( this, n ); + d_op_arg_index[r].addTerm( getTermDatabase()->d_arg_reps[n], n ); } } ++ieqc_i; @@ -489,7 +489,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { d_thm_index.clear(); std::vector< Node > provenConj; quantifiers::FirstOrderModel* m = d_quantEngine->getModel(); - for( int i=0; igetNumAssertedQuantifiers(); i++ ){ + for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ Node q = m->getAssertedQuantifier( i ); Trace("thm-db-debug") << "Is " << q << " a relevant theorem?" << std::endl; Node conjEq; @@ -1569,10 +1569,12 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode, if( d_match_status_child_num==0 ){ //initial binding TNode f = s->getTgFunc( d_typ, d_status_num ); - std::map< TNode, TermArgTrie >::iterator it = s->getTermDatabase()->d_func_map_eqc_trie[f].d_data.find( eqc ); - if( it!=s->getTermDatabase()->d_func_map_eqc_trie[f].d_data.end() ){ - d_match_children.push_back( it->second.d_data.begin() ); - d_match_children_end.push_back( it->second.d_data.end() ); + //std::map< TNode, TermArgTrie >::iterator it = s->getTermDatabase()->d_func_map_eqc_trie[f].d_data.find( eqc ); + Assert( !eqc.isNull() ); + TermArgTrie * tat = s->getTermDatabase()->getTermArgTrie( eqc, f ); + if( tat ){ + d_match_children.push_back( tat->d_data.begin() ); + d_match_children_end.push_back( tat->d_data.end() ); }else{ d_match_status++; d_match_status_child_num--; diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index b6e17e7a1..c89d0f2ee 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -39,7 +39,7 @@ public: std::map< TNode, OpArgIndex > d_child; std::vector< TNode > d_ops; std::vector< TNode > d_op_terms; - void addTerm( ConjectureGenerator * s, TNode n, unsigned index = 0 ); + void addTerm( std::vector< TNode >& terms, TNode n, unsigned index = 0 ); Node getGroundTerm( ConjectureGenerator * s, std::vector< TNode >& args ); void getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& terms ); }; diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 59bd10493..a833f48d2 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -30,10 +30,23 @@ using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::quantifiers::fmcheck; +struct sortQuantifierRelevance { + FirstOrderModel * d_fm; + bool operator() (Node i, Node j) { + int wi = d_fm->getRelevanceValue( i ); + int wj = d_fm->getRelevanceValue( j ); + if( wi==wj ){ + return i children; if( n.getNumChildren()>0 ){ @@ -74,11 +100,11 @@ void FirstOrderModel::initialize() { processInitialize( true ); //this is called after representatives have been chosen and the equality engine has been built //for each quantifier, collect all operators we care about - for( int i=0; i qassert; + for( unsigned i=0; i=0; i-- ){ + Node q = d_forall_rlv_vec[i]; + if( qassert.find( q )!=qassert.end() ){ + Trace("fm-relevant") << " " << d_forall_rlv[q] << " : " << q << std::endl; + d_forall_rlv_assert.push_back( q ); + } + } + Trace("fm-relevant-debug") << "Add remaining asserted formulas..." << std::endl; + for( unsigned i=0; i::iterator it = d_forall_rlv.find( q ); + if( it==d_forall_rlv.end() ){ + return -1; + }else{ + return it->second; + } } //bool FirstOrderModel::isQuantifierAsserted( TNode q ) { diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 4ab1dd1c3..cbe83cfa5 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -49,6 +49,12 @@ protected: QuantifiersEngine * d_qe; /** list of quantifiers asserted in the current context */ context::CDList d_forall_asserts; + /** quantified formulas marked as relevant */ + unsigned d_rlv_count; + std::map< Node, unsigned > d_forall_rlv; + std::vector< Node > d_forall_rlv_vec; + Node d_last_forall_rlv; + std::vector< Node > d_forall_rlv_assert; /** is model set */ context::CDO< bool > d_isModelSet; /** get variable id */ @@ -59,9 +65,9 @@ public: //for Theory Quantifiers: /** assert quantifier */ void assertQuantifier( Node n ); /** get number of asserted quantifiers */ - int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); } + unsigned getNumAssertedQuantifiers(); /** get asserted quantifier */ - Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; } + Node getAssertedQuantifier( unsigned i, bool ordered = false ); /** initialize model for term */ void initializeModelForTerm( Node n, std::map< Node, bool >& visited ); virtual void processInitializeModelForTerm( Node n ) = 0; @@ -96,8 +102,10 @@ private: public: /** reset round */ void reset_round(); - /** is quantified formula asserted */ - //bool isQuantifierAsserted( TNode q ); + /** mark quantified formula relevant */ + void markRelevant( Node q ); + /** get relevance value */ + int getRelevanceValue( Node q ); /** set quantified formula active/inactive * a quantified formula may be set inactive if for instance: * - it is entailed by other quantified formulas diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 0276cf7ab..6b06b9e5c 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -350,11 +350,11 @@ void FullModelChecker::preProcessBuildModel(TheoryModel* m, bool fullModel) { } //do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts if( !options::fmfEmptySorts() ){ - for( int i=0; igetNumAssertedQuantifiers(); i++ ){ + for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ Node q = fm->getAssertedQuantifier( i ); //make sure all types are set - for( unsigned i=0; i& exp ) { }else{ Trace("qip-prop-debug") << it->first << " "; } + }else{ + //mark the quantified formula as relevant + d_qe->markRelevant( it->second.d_q ); } } Trace("qip-prop-debug") << std::endl; diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index cc9b56a7c..fe4867b4e 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -46,7 +46,7 @@ bool InstStrategyCbqi::needsCheck( Theory::Effort e ) { } unsigned InstStrategyCbqi::needsModel( Theory::Effort e ) { - for( int i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ + for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ return QuantifiersEngine::QEFFORT_STANDARD; @@ -59,7 +59,7 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { d_cbqi_set_quant_inactive = false; d_incomplete_check = false; //check if any cbqi lemma has not been added yet - for( int i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ + for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine if( doCbqi( q ) ){ @@ -115,7 +115,7 @@ void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) { } unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting(); for( int ee=0; ee<=1; ee++ ){ - for( int i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ + for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ process( q, e, ee ); @@ -236,7 +236,7 @@ bool InstStrategyCbqi::doCbqi( Node q ){ Node InstStrategyCbqi::getNextDecisionRequest(){ // all counterexample literals that are not asserted - for( int i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ + for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); if( hasAddedCbqiLemma( q ) ){ Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); @@ -316,8 +316,10 @@ void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort } } //print debug - Debug("quant-arith-debug") << std::endl; - debugPrint( "quant-arith-debug" ); + if( Debug.isOn("quant-arith-debug") ){ + Debug("quant-arith-debug") << std::endl; + debugPrint( "quant-arith-debug" ); + } d_counter++; } @@ -355,10 +357,10 @@ void InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ bool m_point_valid = true; int lem = 0; //scan over all instantiation rows - for( int i=0; igetTermDatabase()->getNumInstantiationConstants( f ); i++ ){ + for( unsigned i=0; igetTermDatabase()->getNumInstantiationConstants( f ); i++ ){ Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ); Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl; - for( int j=0; j<(int)d_instRows[ic].size(); j++ ){ + for( unsigned j=0; jgetModel()->getNumAssertedQuantifiers(); i++ ){ + for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); Debug(c) << f << std::endl; Debug(c) << " Inst constants: "; - for( int i=0; i<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){ - if( i>0 ){ + for( unsigned j=0; jgetTermDatabase()->getNumInstantiationConstants( f ); i++ ){ + if( j>0 ){ Debug( c ) << ", "; } Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ); } Debug(c) << std::endl; - for( int j=0; jgetTermDatabase()->getNumInstantiationConstants( f ); j++ ){ + for( unsigned j=0; jgetTermDatabase()->getNumInstantiationConstants( f ); j++ ){ Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j ); Debug(c) << " Instantiation rows for " << ic << " : "; - for( int i=0; i<(int)d_instRows[ic].size(); i++ ){ - if( i>0 ){ + for( unsigned k=0; k0 ){ Debug(c) << ", "; } - Debug(c) << d_instRows[ic][i]; + Debug(c) << d_instRows[ic][k]; } Debug(c) << std::endl; } @@ -699,7 +701,7 @@ void InstStrategyCegqi::registerCounterexampleLemma( Node q, Node lem ) { //must register with the instantiator //must explicitly remove ITEs so that we record dependencies std::vector< Node > ce_vars; - for( int i=0; igetTermDatabase()->getNumInstantiationConstants( q ); i++ ){ + for( unsigned i=0; igetTermDatabase()->getNumInstantiationConstants( q ); i++ ){ ce_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ) ); } std::vector< Node > lems; diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 6d6991476..bb514f41b 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -573,8 +573,8 @@ void FullSaturation::check( Theory::Effort e, unsigned quant_e ) { Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---" << std::endl; } int addedLemmas = 0; - for( int i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ - Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ + Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true ); if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ if( process( q, fullEffort ) ){ //added lemma @@ -627,7 +627,7 @@ bool FullSaturation::process( Node f, bool fullEffort ){ if( r==0 ){ ts = rd->getRDomain( f, i )->d_terms.size(); }else{ - ts = d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()].size(); + ts = d_quantEngine->getTermDatabase()->getNumTypeGroundTerms( f[0][i].getType() ); } max_zero.push_back( fullEffort && ts==0 ); ts = ( fullEffort && ts==0 ) ? 1 : ts; @@ -643,6 +643,11 @@ bool FullSaturation::process( Node f, bool fullEffort ){ } } if( !has_zero ){ + std::vector< TypeNode > ftypes; + for( unsigned i=0; igetTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){ + quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[index], nv ) ) ){ nv++; } } @@ -689,7 +694,7 @@ bool FullSaturation::process( Node f, bool fullEffort ){ }else if( r==0 ){ terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] ); }else{ - terms.push_back( d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()][childIndex[i]] ); + terms.push_back( d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[i], childIndex[i] ) ); } } if( d_quantEngine->addInstantiation( f, terms, false ) ){ diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index b59734720..955dc5d86 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -123,8 +123,8 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ //collect all active quantified formulas belonging to this bool quantActive = false; d_quants.clear(); - for( int i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ - Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ + Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true ); if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ quantActive = true; d_quants.push_back( q ); @@ -137,7 +137,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ doInstantiationRound( e ); if( d_quantEngine->inConflict() ){ Assert( d_quantEngine->getNumLemmasWaiting()>lastWaiting ); - Trace("inst-engine") << "Conflict, size = " << d_quantEngine->getNumLemmasWaiting(); + Trace("inst-engine") << "Conflict = " << d_quantEngine->getNumLemmasWaiting() << " / " << d_quantEngine->getNumLemmasAddedThisRound(); if( lastWaiting>0 ){ Trace("inst-engine") << " (prev " << lastWaiting << ")"; } diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index bdb416b6b..b0ca43cfe 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -54,10 +54,10 @@ void QModelBuilder::debugModel( FirstOrderModel* fm ){ Trace("quant-check-model") << "Testing quantifier instantiations..." << std::endl; int tests = 0; int bad = 0; - for( int i=0; igetNumAssertedQuantifiers(); i++ ){ + for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); std::vector< Node > vars; - for( int j=0; j<(int)f[0].getNumChildren(); j++ ){ + for( unsigned j=0; jd_rep_set) ); @@ -65,8 +65,8 @@ void QModelBuilder::debugModel( FirstOrderModel* fm ){ while( !riter.isFinished() ){ tests++; std::vector< Node > terms; - for( int i=0; igetInstantiation( f, vars, terms ); Node val = fm->getValue( n ); @@ -149,7 +149,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { if( optUseModel() ){ Trace("model-engine-debug") << "Initializing " << fm->getNumAssertedQuantifiers() << " quantifiers..." << std::endl; //check if any quantifiers are un-initialized - for( int i=0; igetNumAssertedQuantifiers(); i++ ){ + for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); if( isQuantifierActive( f ) ){ int lems = initializeQuantifier( f, f ); @@ -173,7 +173,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl; d_quant_sat.clear(); d_uf_prefs.clear(); - for( int i=0; igetNumAssertedQuantifiers(); i++ ){ + for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); if( isQuantifierActive( f ) ){ analyzeQuantifier( fm, f ); @@ -190,7 +190,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { d_numQuantNoSelForm = 0; //now, see if we know that any exceptions via InstGen exist Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl; - for( int i=0; igetNumAssertedQuantifiers(); i++ ){ + for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); if( isQuantifierActive( f ) ){ int lems = doInstGen( fm, f ); diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index a7e272be0..f94e947e5 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -83,8 +83,10 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ Trace("model-engine-debug") << "Check model..." << std::endl; d_incomplete_check = false; //print debug - Trace("fmf-model-complete") << std::endl; - debugPrint("fmf-model-complete"); + if( Trace.isOn("fmf-model-complete") ){ + Trace("fmf-model-complete") << std::endl; + debugPrint("fmf-model-complete"); + } //successfully built an acceptable model, now check it addedLemmas += checkModel(); }else{ @@ -99,8 +101,10 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ if( addedLemmas==0 ){ Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl; //CVC4 will answer SAT or unknown - Trace("fmf-consistent") << std::endl; - debugPrint("fmf-consistent"); + if( Trace.isOn("fmf-consistent") ){ + Trace("fmf-consistent") << std::endl; + debugPrint("fmf-consistent"); + } } } } @@ -177,35 +181,30 @@ int ModelEngine::checkModel(){ d_addedLemmas = 0; d_totalLemmas = 0; //for statistics - for( int i=0; igetNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - int totalInst = 1; - for( size_t i=0; id_rep_set.hasType( tn ) ){ - totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size(); + if( Trace.isOn("model-engine") ){ + for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + int totalInst = 1; + for( unsigned j=0; jd_rep_set.hasType( tn ) ){ + totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size(); + } } + d_totalLemmas += totalInst; } - d_totalLemmas += totalInst; } Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl; // FMC uses two sub-effort levels int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 ); for( int e=0; egetNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); + for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i, true ); Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl; //determine if we should check this quantifier if( considerQuantifiedFormula( f ) ){ exhaustiveInstantiate( f, e ); - if( Trace.isOn("model-engine-warn") ){ - if( d_addedLemmas>10000 ){ - Debug("fmf-exit") << std::endl; - debugPrint("fmf-exit"); - exit( 0 ); - } - } if( d_quantEngine->inConflict() || ( optOneQuantPerRound() && d_addedLemmas>0 ) ){ break; } @@ -222,7 +221,7 @@ int ModelEngine::checkModel(){ //print debug information if( d_quantEngine->inConflict() ){ - Trace("model-engine") << "Conflict, size = " << d_quantEngine->getNumLemmasWaiting() << std::endl; + Trace("model-engine") << "Conflict = " << d_quantEngine->getNumLemmasWaiting() << " / " << d_quantEngine->getNumLemmasAddedThisRound() << std::endl; }else{ Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / "; Trace("model-engine") << d_totalLemmas << std::endl; @@ -320,15 +319,15 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ void ModelEngine::debugPrint( const char* c ){ Trace( c ) << "Quantifiers: " << std::endl; - for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ - Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); + for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ + Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); Trace( c ) << " "; - if( !d_quantEngine->getModelBuilder()->isQuantifierActive( f ) ){ + if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) ){ Trace( c ) << "*Inactive* "; }else{ Trace( c ) << " "; } - Trace( c ) << f << std::endl; + Trace( c ) << q << std::endl; } //d_quantEngine->getModel()->debugPrint( c ); } diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index e5df41510..1cbfbd99b 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -22,6 +22,7 @@ #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/first_order_model.h" #include "theory/theory_engine.h" using namespace CVC4::kind; @@ -46,7 +47,7 @@ QuantInfo::~QuantInfo() { } -void QuantInfo::initialize( Node q, Node qn ) { +void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) { d_q = q; for( unsigned i=0; iisValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl; + + if( d_mg->isValid() ){ + //optimization : record variable argument positions for terms that must be matched + std::vector< TNode > vars; + //TODO: revisit this, makes QCF faster, but misses conflicts due to caring about paths that may not be relevant (starExec jobs 14136/14137) + //if( options::qcfSkipRd() ){ + // for( unsigned j=q[0].getNumChildren(); j visited; + getPropagateVars( vars, q[1], false, visited ); + for( unsigned j=0; jgetTermDatabase()->getMatchOperator( v ); + if( !f.isNull() ){ + Trace("qcf-opt") << "Record variable argument positions in " << v << ", op=" << f << "..." << std::endl; + for( unsigned k=0; k::iterator itv = d_var_num.find( n ); + if( itv!=d_var_num.end() ){ + Trace("qcf-opt") << " arg " << k << " is var #" << itv->second << std::endl; + if( std::find( d_var_rel_dom[itv->second][f].begin(), d_var_rel_dom[itv->second][f].end(), k )==d_var_rel_dom[itv->second][f].end() ){ + d_var_rel_dom[itv->second][f].push_back( k ); + } + } + } + } + } + } +} + +void QuantInfo::getPropagateVars( std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited ){ + std::map< TNode, bool >::iterator itv = visited.find( n ); + if( itv==visited.end() ){ + visited[n] = true; + bool rec = true; + bool newPol = pol; + if( d_var_num.find( n )!=d_var_num.end() ){ + Assert( std::find( vars.begin(), vars.end(), n )==vars.end() ); + vars.push_back( n ); + }else if( MatchGen::isHandledBoolConnective( n ) ){ + Assert( n.getKind()!=IMPLIES ); + QuantPhaseReq::getEntailPolarity( n, 0, true, pol, rec, newPol ); + } + Trace("qcf-opt-debug") << "getPropagateVars " << n << ", pol = " << pol << ", rec = " << rec << std::endl; + if( rec ){ + for( unsigned i=0; i::iterator itm = d_match.find( v ); - + bool isGroundRep = false; if( vn!=-1 ){ Debug("qcf-match-debug") << " ...Variable bound to variable" << std::endl; //std::map< int, TNode >::iterator itmn = d_match.find( vn ); @@ -373,13 +427,14 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo }else{ Debug("qcf-match-debug") << " ...Variable bound to ground" << std::endl; if( d_match[v].isNull() ){ + //isGroundRep = true; ?? }else{ //compare ground values Debug("qcf-match-debug") << " -> Ground value, compare " << d_match[v] << " "<< n << std::endl; return p->areMatchEqual( d_match[v], n ) ? 0 : -1; } } - if( setMatch( p, v, n ) ){ + if( setMatch( p, v, n, isGroundRep ) ){ Debug("qcf-match-debug") << " -> success" << std::endl; return 1; }else{ @@ -445,8 +500,23 @@ bool QuantInfo::isConstrainedVar( int v ) { } } -bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n ) { +bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRep ) { if( getCurrentCanBeEqual( p, v, n ) ){ + if( isGroundRep ){ + //fail if n does not exist in the relevant domain of each of the argument positions + std::map< int, std::map< TNode, std::vector< unsigned > > >::iterator it = d_var_rel_dom.find( v ); + if( it!=d_var_rel_dom.end() ){ + for( std::map< TNode, std::vector< unsigned > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + for( unsigned j=0; jsecond.size(); j++ ){ + Debug("qcf-match-debug2") << n << " in relevant domain " << it2->second << "." << it2->second[j] << "?" << std::endl; + if( !p->getTermDatabase()->inRelevantDomain( it2->first, it2->second[j], n ) ){ + Debug("qcf-match-debug") << " -> fail, since " << n << " is not in relevant domain of " << it2->second << "." << it2->second[j] << std::endl; + return false; + } + } + } + } + } Debug("qcf-match-debug") << "-- bind : " << v << " -> " << n << ", checked " << d_curr_var_deq[v].size() << " disequalities" << std::endl; d_match[v] = n; return true; @@ -566,7 +636,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign if( !z.isNull() ){ Trace("qcf-tconstraint-debug") << "...set " << d_vars[vn] << " = " << z << std::endl; assigned.push_back( vn ); - if( !setMatch( p, vn, z ) ){ + if( !setMatch( p, vn, z, false ) ){ success = false; break; } @@ -608,7 +678,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign if( !sum.isNull() ){ assigned.push_back( slv_v ); Trace("qcf-tconstraint-debug") << "...set " << d_vars[slv_v] << " = " << sum << std::endl; - if( !setMatch( p, slv_v, sum ) ){ + if( !setMatch( p, slv_v, sum, false ) ){ success = false; } p->d_tempCache.push_back( sum ); @@ -694,7 +764,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign int currIndex = d_una_eqc_count[d_una_index]; d_una_eqc_count[d_una_index]++; Trace("qcf-check-unassign") << d_unassigned[d_una_index] << "->" << p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] << std::endl; - if( setMatch( p, d_unassigned[d_una_index], p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] ) ){ + if( setMatch( p, d_unassigned[d_una_index], p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex], true ) ){ d_match_term[d_unassigned[d_una_index]] = TNode::null(); Trace("qcf-check-unassign") << "Succeeded match " << d_una_index << std::endl; d_una_index++; @@ -1125,7 +1195,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { }else{ //unassigned, set match to true/false d_qni_bound[0] = vn; - qi->setMatch( p, vn, d_tgt ? p->d_true : p->d_false ); + qi->setMatch( p, vn, d_tgt ? p->d_true : p->d_false, false ); d_child_counter = 0; } if( d_child_counter==0 ){ @@ -1365,17 +1435,6 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { d_qni_bound_cons.clear(); } } - /* - if( d_type==typ_var && p->d_effort==QuantConflictFind::effort_mc && !d_matched_basis ){ - d_matched_basis = true; - Node f = getMatchOperator( d_n ); - TNode mbo = p->getTermDatabase()->getModelBasisOpTerm( f ); - if( qi->setMatch( p, d_qni_var_num[0], mbo ) ){ - success = true; - d_qni_bound[0] = d_qni_var_num[0]; - } - } - */ } Debug("qcf-match") << " ...finished matching for " << d_n << ", success = " << success << std::endl; d_wasSet = success; @@ -1595,7 +1654,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) { if( it != d_qn[index]->d_data.end() ) { d_qni.push_back( it ); //set the match - if( it->first.getType().isComparableTo( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first ) ){ + if( it->first.getType().isComparableTo( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first, true ) ){ Debug("qcf-match-debug") << " Binding variable" << std::endl; if( d_qn.size()second ); @@ -1640,7 +1699,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) { d_qni[index]++; if( d_qni[index]!=d_qn[index]->d_data.end() ){ success = true; - if( qi->setMatch( p, itb->second, d_qni[index]->first ) ){ + if( qi->setMatch( p, itb->second, d_qni[index]->first, true ) ){ Debug("qcf-match-debug") << " Bind next variable" << std::endl; if( d_qn.size()second ); @@ -1756,8 +1815,7 @@ bool MatchGen::isHandled( TNode n ) { QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ), -d_conflict( c, false ), -d_qassert( c ) { +d_conflict( c, false ) { d_fid_count = 0; d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -1782,7 +1840,7 @@ void QuantConflictFind::registerQuantifier( Node q ) { Trace("qcf-qregister") << " : " << q << std::endl; //make QcfNode structure Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl; - d_qinfo[q].initialize( q, q[1] ); + d_qinfo[q].initialize( this, q, q[1] ); //debug print Trace("qcf-qregister") << "- Flattened structure is :" << std::endl; @@ -1797,7 +1855,7 @@ void QuantConflictFind::registerQuantifier( Node q ) { Trace("qcf-qregister") << std::endl; } } - + Trace("qcf-qregister") << "Done registering quantifier." << std::endl; } } @@ -1805,10 +1863,8 @@ void QuantConflictFind::registerQuantifier( Node q ) { short QuantConflictFind::getMaxQcfEffort() { if( options::qcfMode()==QCF_CONFLICT_ONLY ){ return effort_conflict; - }else if( options::qcfMode()==QCF_PROP_EQ ){ + }else if( options::qcfMode()==QCF_PROP_EQ || options::qcfMode()==QCF_PARTIAL ){ return effort_prop_eq; - }else if( options::qcfMode()==QCF_MC ){ - return effort_mc; }else{ return 0; } @@ -1833,16 +1889,13 @@ bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) { //-------------------------------------------------- handling assertions / eqc void QuantConflictFind::assertNode( Node q ) { + /* if( d_quantEngine->hasOwnership( q, this ) ){ Trace("qcf-proc") << "QCF : assertQuantifier : "; debugPrintQuant("qcf-proc", q); Trace("qcf-proc") << std::endl; - d_qassert.push_back( q ); - //set the eqRegistries that this depends on to true - //for( std::map< EqRegistry *, bool >::iterator it = d_qinfo[q].d_rel_eqr.begin(); it != d_qinfo[q].d_rel_eqr.end(); ++it ){ - // it->first->d_active.set( true ); - //} } + */ } /** new node */ @@ -1904,28 +1957,12 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { //determine order for quantified formulas std::vector< Node > qorder; - std::map< Node, bool > qassert; - //mark which are asserted - for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ + Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true ); + if( d_quantEngine->hasOwnership( q, this ) ){ + qorder.push_back( q ); } } - if( Trace.isOn("qcf-debug") ){ Trace("qcf-debug") << std::endl; debugPrint("qcf-debug"); @@ -1974,7 +2011,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { Trace("qcf-inst") << std::endl; ++addedLemmas; if( e==effort_conflict ){ - d_quant_order.insert( d_quant_order.begin(), q ); + d_quantEngine->markRelevant( q ); ++(d_statistics.d_conflict_inst); if( options::qcfAllConflict() ){ isConflict = true; @@ -1983,6 +2020,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { } break; }else if( e==effort_prop_eq ){ + d_quantEngine->markRelevant( q ); ++(d_statistics.d_prop_inst); } }else{ @@ -2040,60 +2078,24 @@ void QuantConflictFind::computeRelevantEqr() { //d_uf_terms.clear(); //d_eqc_uf_terms.clear(); d_eqcs.clear(); - d_model_basis.clear(); //d_arg_reps.clear(); //double clSet = 0; //if( Trace.isOn("qcf-opt") ){ // clSet = double(clock())/double(CLOCKS_PER_SEC); //} - //long nTermst = 0; - //long nTerms = 0; - //long nEqc = 0; - - //which nodes are irrelevant for disequality matches - std::map< TNode, bool > irrelevant_dnode; //now, store matches eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() ); while( !eqcs_i.isFinished() ){ - //nEqc++; Node r = (*eqcs_i); if( getTermDatabase()->hasTermCurrent( r ) ){ TypeNode rtn = r.getType(); - if( options::qcfMode()==QCF_MC ){ - std::map< TypeNode, std::vector< TNode > >::iterator itt = d_eqcs.find( rtn ); - if( itt==d_eqcs.end() ){ - Node mb = getTermDatabase()->getModelBasisTerm( rtn ); - if( !getEqualityEngine()->hasTerm( mb ) ){ - Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl; - Assert( false ); - } - Node mbr = getRepresentative( mb ); - if( mbr!=r ){ - d_eqcs[rtn].push_back( mbr ); - } - d_eqcs[rtn].push_back( r ); - d_model_basis[rtn] = mb; - }else{ - itt->second.push_back( r ); - } - }else{ - if( !options::cbqi() || !TermDb::hasInstConstAttr( r ) ){ - d_eqcs[rtn].push_back( r ); - } + if( !options::cbqi() || !TermDb::hasInstConstAttr( r ) ){ + d_eqcs[rtn].push_back( r ); } } ++eqcs_i; } - /* - if( Trace.isOn("qcf-opt") ){ - double clSet2 = double(clock())/double(CLOCKS_PER_SEC); - Trace("qcf-opt") << "Compute rel eqc : " << std::endl; - Trace("qcf-opt") << " " << nEqc << " equivalence classes. " << std::endl; - Trace("qcf-opt") << " " << nTerms << " / " << nTermst << " terms." << std::endl; - Trace("qcf-opt") << " Time : " << (clSet2-clSet) << std::endl; - } - */ } } @@ -2120,21 +2122,6 @@ void QuantConflictFind::debugPrint( const char * c ) { ++eqc_i; } Trace(c) << (pr ? " " : "" ) << "}" << std::endl; - /* - EqcInfo * eqcn = getEqcInfo( n, false ); - if( eqcn ){ - Trace(c) << " DEQ : {"; - pr = false; - for( NodeBoolMap::iterator it = eqcn->d_diseq.begin(); it != eqcn->d_diseq.end(); ++it ){ - if( (*it).second ){ - Trace(c) << (pr ? "," : "" ) << " " << (*it).first; - pr = true; - } - } - Trace(c) << (pr ? " " : "" ) << "}" << std::endl; - } - //} - */ ++eqcs_i; } } diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 36fcaddf5..8b42b0916 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -114,6 +114,9 @@ private: //for completing match int d_unassigned_nvar; int d_una_index; std::vector< int > d_una_eqc_count; + //optimization: track which arguments variables appear under UF terms in + std::map< int, std::map< TNode, std::vector< unsigned > > > d_var_rel_dom; + void getPropagateVars( std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited ); public: QuantInfo(); ~QuantInfo(); @@ -138,7 +141,7 @@ public: bool containsVarMg(int i) const { return var_mg_find(i) != var_mg_end(); } bool matchGeneratorIsValid() const { return d_mg->isValid(); } - bool getNextMatch( QuantConflictFind * p) { + bool getNextMatch( QuantConflictFind * p ) { return d_mg->getNextMatch(p, this); } @@ -146,7 +149,7 @@ public: void reset_round( QuantConflictFind * p ); public: //initialize - void initialize( Node q, Node qn ); + void initialize( QuantConflictFind * p, Node q, Node qn ); //current constraints std::vector< TNode > d_match; std::vector< TNode > d_match_term; @@ -158,7 +161,7 @@ public: bool getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq = false ); int addConstraint( QuantConflictFind * p, int v, TNode n, bool polarity ); int addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove ); - bool setMatch( QuantConflictFind * p, int v, TNode n ); + bool setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRep ); bool isMatchSpurious( QuantConflictFind * p ); bool isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms ); bool entailmentTest( QuantConflictFind * p, Node lit, bool chEnt = true ); @@ -178,7 +181,6 @@ class QuantConflictFind : public QuantifiersModule typedef context::CDHashMap NodeBoolMap; private: context::CDO< bool > d_conflict; - std::vector< Node > d_quant_order; std::map< Kind, Node > d_zero; //for storing nodes created during t-constraint solving (prevents memory leaks) std::vector< Node > d_tempCache; @@ -192,18 +194,14 @@ public: //for ground terms Node d_false; TNode getZero( Kind k ); private: - //currently asserted quantifiers - NodeList d_qassert; std::map< Node, QuantInfo > d_qinfo; private: //for equivalence classes // type -> list(eqc) std::map< TypeNode, std::vector< TNode > > d_eqcs; - std::map< TypeNode, Node > d_model_basis; public: enum { effort_conflict, effort_prop_eq, - effort_mc, }; short d_effort; void setEffort( int e ) { d_effort = e; } diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 9181677ee..b353fce2f 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -95,7 +95,7 @@ void RelevantDomain::compute(){ it2->second->reset(); } } - for( int i=0; igetNumAssertedQuantifiers(); i++ ){ + for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ Node q = d_model->getAssertedQuantifier( i ); Node icf = d_qe->getTermDatabase()->getInstConstantBody( q ); Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl; diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 5bf8d8a8d..07b1462c6 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -285,7 +285,7 @@ void RewriteEngine::registerQuantifier( Node f ) { //make the quantified formula d_qinfo_n[f] = NodeManager::currentNM()->mkNode( FORALL, qcfn_c ); Trace("rr-register") << " qcf formula is : " << d_qinfo_n[f] << std::endl; - d_qinfo[f].initialize( d_qinfo_n[f], d_qinfo_n[f][1] ); + d_qinfo[f].initialize( qcf, d_qinfo_n[f], d_qinfo_n[f][1] ); } } } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 3d3646d7d..ef301c2cf 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -78,8 +78,8 @@ TNode TermArgTrie::addOrGetTerm( TNode n, std::vector< TNode >& reps, int argInd void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) { for( std::map< TNode, TermArgTrie >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ - for( unsigned i=0; ifirst << std::endl; + for( unsigned i=0; ifirst << std::endl; it->second.debugPrint( c, n, depth+1 ); } } @@ -111,6 +111,20 @@ Node TermDb::getGroundTerm( Node f, unsigned i ) { return d_op_map[f][i]; } +unsigned TermDb::getNumTypeGroundTerms( TypeNode tn ) { + std::map< TypeNode, std::vector< Node > >::iterator it = d_type_map.find( tn ); + if( it!=d_type_map.end() ){ + return it->second.size(); + }else{ + return 0; + } +} + +Node TermDb::getTypeGroundTerm( TypeNode tn, unsigned i ) { + Assert( igetTheoryEngine()->getMasterEqualityEngine()->getRepresentative( r )==r ); + std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f ); + if( it != d_func_map_rel_dom.end() ){ + std::map< unsigned, std::vector< Node > >::iterator it2 = it->second.find( i ); + if( it2!=it->second.end() ){ + return std::find( it2->second.begin(), it2->second.end(), r )!=it2->second.end(); + }else{ + return false; + } + }else{ + return false; + } +} + //return a term n' equivalent to n // maximal subterms of n' are representatives in the equality engine qy Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy ) { @@ -533,6 +562,7 @@ bool TermDb::reset( Theory::Effort effort ){ d_arg_reps.clear(); d_func_map_trie.clear(); d_func_map_eqc_trie.clear(); + d_func_map_rel_dom.clear(); d_consistent_ee = true; eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); @@ -596,16 +626,18 @@ bool TermDb::reset( Theory::Effort effort ){ } computeArgReps( n ); - if( Trace.isOn("term-db-debug") ){ - Trace("term-db-debug") << "Adding term " << n << " with arg reps : "; - for( unsigned i=0; ihasTerm( n ) ){ - Trace("term-db-debug") << " and value : " << ee->getRepresentative( n ) << std::endl; + Trace("term-db-debug") << "Adding term " << n << " with arg reps : "; + for( unsigned i=0; ifirst][i].begin(), + d_func_map_rel_dom[it->first][i].end(), d_arg_reps[n][i] ) == d_func_map_rel_dom[it->first][i].end() ){ + d_func_map_rel_dom[it->first][i].push_back( d_arg_reps[n][i] ); } } + Trace("term-db-debug") << std::endl; + if( ee->hasTerm( n ) ){ + Trace("term-db-debug") << " and value : " << ee->getRepresentative( n ) << std::endl; + } Node at = d_func_map_trie[ it->first ].addOrGetTerm( n, d_arg_reps[n] ); if( at!=n && ee->areEqual( at, n ) ){ NoMatchAttribute nma; @@ -650,12 +682,12 @@ bool TermDb::reset( Theory::Effort effort ){ Trace("term-db-stats") << "TermDb: Reset" << std::endl; Trace("term-db-stats") << "Non-Congruent/Congruent/Non-Relevant = "; Trace("term-db-stats") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl; - if( Debug.isOn("term-db") ){ - Debug("term-db") << "functions : " << std::endl; + if( Trace.isOn("term-db-index") ){ + Trace("term-db-index") << "functions : " << std::endl; for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){ if( it->second.size()>0 ){ - Debug("term-db") << "- " << it->first << std::endl; - d_func_map_trie[ it->first ].debugPrint("term-db", it->second[0]); + Trace("term-db-index") << "- " << it->first << std::endl; + d_func_map_trie[ it->first ].debugPrint("term-db-index", it->second[0]); } } } @@ -929,10 +961,10 @@ Node TermDb::getInstantiationConstant( Node q, int i ) const { } /** get number of instantiation constants for q */ -int TermDb::getNumInstantiationConstants( Node q ) const { +unsigned TermDb::getNumInstantiationConstants( Node q ) const { std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q ); if( it!=d_inst_constants.end() ){ - return (int)it->second.size(); + return it->second.size(); }else{ return 0; } diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 76bd623a8..a62b343a2 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -163,11 +163,21 @@ namespace fmcheck { } class TermDbSygus; +class QuantConflictFind; +class RelevantDomain; +class ConjectureGenerator; +class TermGenerator; +class TermGenEnv; class TermDb : public QuantifiersUtil { friend class ::CVC4::theory::QuantifiersEngine; + //TODO: eliminate most of these friend class ::CVC4::theory::inst::Trigger; friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker; + friend class ::CVC4::theory::quantifiers::QuantConflictFind; + friend class ::CVC4::theory::quantifiers::RelevantDomain; + friend class ::CVC4::theory::quantifiers::ConjectureGenerator; + friend class ::CVC4::theory::quantifiers::TermGenEnv; typedef context::CDHashMap NodeIntMap; private: /** reference to the quantifiers engine */ @@ -180,12 +190,6 @@ private: std::map< Node, std::map< TypeNode, Node > > d_par_op_map; /** whether master equality engine is UF-inconsistent */ bool d_consistent_ee; - /** set has term */ - void setHasTerm( Node n ); - /** evaluate term */ - Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy ); - TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ); - bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ); public: TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ); ~TermDb(){} @@ -195,7 +199,14 @@ public: /** constants */ Node d_zero; Node d_one; - +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: /** 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 */ @@ -208,24 +219,29 @@ public: /** map from operators to trie */ std::map< Node, TermArgTrie > d_func_map_trie; std::map< Node, TermArgTrie > d_func_map_eqc_trie; + /** mapping from operators to their representative relevant domains */ + std::map< Node, std::map< unsigned, std::vector< Node > > > d_func_map_rel_dom; /** has map */ std::map< Node, bool > d_has_map; /** map from reps to a term in eqc in d_has_map */ - std::map< Node, Node > d_term_elig_eqc; - + std::map< Node, Node > d_term_elig_eqc; + /** set has term */ + void setHasTerm( Node n ); + /** evaluate term */ + Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy ); + TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ); + bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ); public: /** ground terms for operator */ unsigned getNumGroundTerms( Node f ); /** get ground term for operator */ Node getGroundTerm( Node f, unsigned i ); + /** get num type terms */ + unsigned getNumTypeGroundTerms( TypeNode tn ); + /** get type ground term */ + Node getTypeGroundTerm( TypeNode tn, unsigned i ); /** add a term to the database */ void addTerm( Node n, std::set< Node >& added, bool withinQuant = false, bool withinInstClosure = false ); - /** 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"; } /** get match operator */ Node getMatchOperator( Node n ); /** get term arg index */ @@ -238,6 +254,8 @@ public: void computeArgReps( TNode n ); /** compute uf eqc terms */ void computeUfEqcTerms( TNode f ); + /** in relevant domain */ + bool inRelevantDomain( TNode f, unsigned i, TNode r ); /** evaluate a term under a substitution. Return representative in EE if possible. * subsRep is whether subs contains only representatives */ @@ -297,7 +315,7 @@ public: /** get the i^th instantiation constant of q */ Node getInstantiationConstant( Node q, int i ) const; /** get number of instantiation constants for q */ - int getNumInstantiationConstants( Node q ) const; + unsigned getNumInstantiationConstants( Node q ) const; /** get the ce body q[e/x] */ Node getInstConstantBody( Node q ); /** get counterexample literal (for cbqi) */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 4b95c75ed..1008d7d49 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -88,6 +88,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_tr_trie = new inst::TriggerTrie; d_curr_effort_level = QEFFORT_NONE; d_conflict = false; + d_num_added_lemmas_round = 0; d_hasAddedLemma = false; //don't add true lemma d_lemmas_produced_c[d_term_db->d_true] = true; @@ -365,6 +366,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ } d_conflict = false; + d_num_added_lemmas_round = 0; d_hasAddedLemma = false; bool setIncomplete = false; if( e==Theory::EFFORT_LAST_CALL ){ @@ -398,7 +400,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ } Trace("quant-engine-debug") << " Theory engine finished : " << !d_te->needCheck() << std::endl; Trace("quant-engine-debug") << " Needs model effort : " << needsModelE << std::endl; - Trace("quant-engine-debug") << "Resetting all modules..." << std::endl; } if( Trace.isOn("quant-engine-ee-pre") ){ Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl; @@ -410,6 +411,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ } //reset utilities + Trace("quant-engine-debug") << "Resetting all utilities..." << std::endl; for( unsigned i=0; iidentify().c_str() << "..." << std::endl; if( !d_util[i]->reset( e ) ){ @@ -429,9 +431,11 @@ void QuantifiersEngine::check( Theory::Effort e ){ } //reset the model + Trace("quant-engine-debug") << "Reset model..." << std::endl; d_model->reset_round(); //reset the modules + Trace("quant-engine-debug") << "Resetting all modules..." << std::endl; for( unsigned i=0; iidentify().c_str() << std::endl; d_modules[i]->reset_round( e ); @@ -936,6 +940,7 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){ d_lemmas_produced_c[ lem ] = true; d_lemmas_waiting.push_back( lem ); Trace("inst-add-debug") << "Added lemma" << std::endl; + d_num_added_lemmas_round++; return true; }else{ Trace("inst-add-debug") << "Duplicate." << std::endl; @@ -944,6 +949,7 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){ }else{ //do not need to rewrite, will be rewritten after sending d_lemmas_waiting.push_back( lem ); + d_num_added_lemmas_round++; return true; } } @@ -1115,6 +1121,14 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo } } +bool QuantifiersEngine::removeInstantiation( Node q, Node lem, std::vector< Node >& terms ) { + //lem must occur in d_waiting_lemmas + if( removeLemma( lem ) ){ + return removeInstantiationInternal( q, terms ); + }else{ + return false; + } +} bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){ n = Rewriter::rewrite( n ); @@ -1134,16 +1148,10 @@ bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool return addSplit( fm ); } -bool QuantifiersEngine::removeInstantiation( Node q, Node lem, std::vector< Node >& terms ) { - //lem must occur in d_waiting_lemmas - if( removeLemma( lem ) ){ - return removeInstantiationInternal( q, terms ); - }else{ - return false; - } +void QuantifiersEngine::markRelevant( Node q ) { + d_model->markRelevant( q ); } - bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl; //determine if we should perform check, based on instWhenMode diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index bad9c0169..a088dfec6 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -156,6 +156,8 @@ private: //this information is reset during check unsigned d_curr_effort_level; /** are we in conflict */ bool d_conflict; + /** number of lemmas we actually added this round (for debugging) */ + unsigned d_num_added_lemmas_round; /** has added lemma this round */ bool d_hasAddedLemma; private: @@ -317,12 +319,16 @@ public: bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true ); /** add split equality */ bool addSplitEquality( Node n1, Node n2, bool reqPhase = false, bool reqPhasePol = true ); + /** mark relevant quantified formula, this will indicate it should be checked before the others */ + void markRelevant( Node q ); /** has added lemma */ bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; } /** is in conflict */ bool inConflict() { return d_conflict; } /** get number of waiting lemmas */ unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); } + /** get number of waiting lemmas */ + unsigned getNumLemmasAddedThisRound() { return d_num_added_lemmas_round; } /** get needs check */ bool getInstWhenNeedsCheck( Theory::Effort e ); /** get user pat mode */ diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 784eaf677..b51313deb 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -77,7 +77,8 @@ TESTS = \ anti-sk-simp.smt2 \ pure_dt_cbqi.smt2 \ florian-case-ax.smt2 \ - double-pattern.smt2 + double-pattern.smt2 \ + qcf-rel-dom-opt.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2 b/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2 new file mode 100644 index 000000000..539f181af --- /dev/null +++ b/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2 @@ -0,0 +1,45 @@ +(set-logic UFLIA) +(set-info :status unsat) +(declare-fun P (Int) Bool) + +(assert (P 0)) +(assert (P 1)) +(assert (P 2)) +(assert (P 3)) +(assert (P 4)) +(assert (P 5)) +(assert (P 6)) +(assert (P 7)) +(assert (P 8)) +(assert (P 9)) + +(assert (P 10)) +(assert (P 11)) +(assert (P 12)) +(assert (P 13)) +(assert (P 14)) +(assert (P 15)) +(assert (P 16)) +(assert (P 17)) +(assert (P 18)) +(assert (P 19)) + +(assert (P 20)) +(assert (P 21)) +(assert (P 22)) +(assert (P 23)) +(assert (P 24)) +(assert (P 25)) +(assert (P 26)) +(assert (P 27)) +(assert (P 28)) +(assert (P 29)) + +(declare-fun Q (Int Int Int Int Int) Bool) +(assert (forall ((x Int) (y Int) (z Int) (w Int) (q Int)) (or (not (P x)) (not (P y)) (not (P z)) (not (P w)) (not (P q)) (Q x y z w q)))) + +(declare-fun R (Int) Bool) +(assert (R 0)) +(assert (forall ((x Int)) (not (R x)))) + +(check-sat) -- cgit v1.2.3 From dd84403eb19b769d80b4c57ae690ba14c02df041 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 6 May 2016 17:04:52 -0500 Subject: Minor clean up, fixes related to sygus. --- src/parser/smt2/Smt2.g | 2 +- src/printer/smt2/smt2_printer.cpp | 27 +++++ src/smt/smt_engine.cpp | 125 +++++++++++---------- src/theory/quantifiers/instantiation_engine.cpp | 6 +- src/theory/quantifiers/model_engine.cpp | 9 +- src/theory/quantifiers/quantifiers_rewriter.cpp | 2 +- src/theory/quantifiers/term_database.cpp | 1 + src/theory/quantifiers_engine.cpp | 4 - src/theory/quantifiers_engine.h | 4 - src/theory/strings/theory_strings.cpp | 2 - test/regress/regress0/sygus/Makefile.am | 3 +- .../regress0/sygus/strings-unconstrained.sy | 15 +++ 12 files changed, 116 insertions(+), 84 deletions(-) create mode 100644 test/regress/regress0/sygus/strings-unconstrained.sy (limited to 'src/theory/quantifiers/instantiation_engine.cpp') diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index c28d23eac..78975bbe6 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -749,7 +749,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] $cmd = new EmptyCommand(); } | /* check-synth */ - CHECK_SYNTH_TOK { PARSER_STATE->checkThatLogicIsSet(); } + CHECK_SYNTH_TOK { PARSER_STATE->checkThatLogicIsSet();PARSER_STATE->defineSygusFuns(); } { Expr sygusVar = EXPR_MANAGER->mkVar("sygus", EXPR_MANAGER->booleanType()); Expr sygusAttr = EXPR_MANAGER->mkExpr(kind::INST_PATTERN_LIST, EXPR_MANAGER->mkExpr(kind::INST_ATTRIBUTE, sygusVar)); std::vector bodyv; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 4defc7691..f874074ac 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -826,6 +826,33 @@ static string smtKindString(Kind k) throw() { case kind::FLOATINGPOINT_TO_SBV: return "fp.to_sbv"; case kind::FLOATINGPOINT_TO_REAL: return "fp.to_real"; + //string theory + case kind::STRING_CONCAT: return "str.++"; + case kind::STRING_LENGTH: return "str.len"; + case kind::STRING_SUBSTR: return "str.substr" ; + case kind::STRING_STRCTN: return "str.contains" ; + case kind::STRING_CHARAT: return "str.at" ; + case kind::STRING_STRIDOF: return "str.indexof" ; + case kind::STRING_STRREPL: return "str.replace" ; + case kind::STRING_PREFIX: return "str.prefixof" ; + case kind::STRING_SUFFIX: return "str.suffixof" ; + case kind::STRING_ITOS: return "int.to.str" ; + case kind::STRING_STOI: return "str.to.int" ; + case kind::STRING_U16TOS: return "u16.to.str" ; + case kind::STRING_STOU16: return "str.to.u16" ; + case kind::STRING_U32TOS: return "u32.to.str" ; + case kind::STRING_STOU32: return "str.to.u32" ; + case kind::STRING_IN_REGEXP: return "str.in.re"; + case kind::STRING_TO_REGEXP: return "str.to.re"; + case kind::REGEXP_CONCAT: return "re.++"; + case kind::REGEXP_UNION: return "re.union"; + case kind::REGEXP_INTER: return "re.inter"; + case kind::REGEXP_STAR: return "re.*"; + case kind::REGEXP_PLUS: return "re.+"; + case kind::REGEXP_OPT: return "re.opt"; + case kind::REGEXP_RANGE: return "re.range"; + case kind::REGEXP_LOOP: return "re.loop"; + default: ; /* fall through */ } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 021798132..3a138e4b7 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4420,71 +4420,72 @@ Result SmtEngine::checkSynth(const Expr& e) throw(TypeCheckingException, ModalEx Trace("smt-synth") << "Check synthesis conjecture: " << e << std::endl; Expr e_check = e; Node conj = Node::fromExpr( e ); - Assert( conj.getKind()==kind::FORALL ); - //possibly run quantifier elimination to make formula into single invocation - if( conj[1].getKind()==kind::EXISTS ){ - Node conj_se = conj[1][1]; - - Trace("smt-synth") << "Compute single invocation for " << conj_se << "..." << std::endl; - quantifiers::SingleInvocationPartition sip( kind::APPLY ); - sip.init( conj_se ); - Trace("smt-synth") << "...finished, got:" << std::endl; - sip.debugPrint("smt-synth"); - - if( !sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation() ){ - //We are in the case where our synthesis conjecture is exists f. forall xy. P( f( x ), x, y ), P does not contain f. - //The following will run QE on (exists z x.) exists y. P( z, x, y ) to obtain Q( z, x ), - // and then constructs exists f. forall x. Q( f( x ), x ), where Q does not contain f. We invoke synthesis solver on this result. - - //create new smt engine to do quantifier elimination - SmtEngine smt_qe( d_exprManager ); - smt_qe.setLogic(getLogicInfo()); - Trace("smt-synth") << "Property is non-ground single invocation, run QE to obtain single invocation." << std::endl; - //partition variables - std::vector< Node > qe_vars; - std::vector< Node > nqe_vars; - for( unsigned i=0; i orig; - std::vector< Node > subs; - //skolemize non-qe variables - for( unsigned i=0; imkSkolem( "k", nqe_vars[i].getType(), "qe for non-ground single invocation" ); - orig.push_back( nqe_vars[i] ); - subs.push_back( k ); - Trace("smt-synth") << " subs : " << nqe_vars[i] << " -> " << k << std::endl; - } - for( std::map< Node, bool >::iterator it = sip.d_funcs.begin(); it != sip.d_funcs.end(); ++it ){ - orig.push_back( sip.d_func_inv[it->first] ); - Node k = NodeManager::currentNM()->mkSkolem( "k", sip.d_func_fo_var[it->first].getType(), "qe for function in non-ground single invocation" ); - subs.push_back( k ); - Trace("smt-synth") << " subs : " << sip.d_func_inv[it->first] << " -> " << k << std::endl; - } - Node conj_se_ngsi = sip.getFullSpecification(); - Node conj_se_ngsi_subs = conj_se_ngsi.substitute( orig.begin(), orig.end(), subs.begin(), subs.end() ); - Assert( !qe_vars.empty() ); - conj_se_ngsi_subs = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, qe_vars ), conj_se_ngsi_subs ); + if( conj.getKind()==kind::FORALL ){ + //possibly run quantifier elimination to make formula into single invocation + if( conj[1].getKind()==kind::EXISTS ){ + Node conj_se = conj[1][1]; + + Trace("smt-synth") << "Compute single invocation for " << conj_se << "..." << std::endl; + quantifiers::SingleInvocationPartition sip( kind::APPLY ); + sip.init( conj_se ); + Trace("smt-synth") << "...finished, got:" << std::endl; + sip.debugPrint("smt-synth"); - Trace("smt-synth") << "Run quantifier elimination on " << conj_se_ngsi_subs << std::endl; - Expr qe_res = smt_qe.doQuantifierElimination( conj_se_ngsi_subs.toExpr(), true, false ); - Trace("smt-synth") << "Result : " << qe_res << std::endl; + if( !sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation() ){ + //We are in the case where our synthesis conjecture is exists f. forall xy. P( f( x ), x, y ), P does not contain f. + //The following will run QE on (exists z x.) exists y. P( z, x, y ) to obtain Q( z, x ), + // and then constructs exists f. forall x. Q( f( x ), x ), where Q does not contain f. We invoke synthesis solver on this result. - //create single invocation conjecture - Node qe_res_n = Node::fromExpr( qe_res ); - qe_res_n = qe_res_n.substitute( subs.begin(), subs.end(), orig.begin(), orig.end() ); - if( !nqe_vars.empty() ){ - qe_res_n = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, nqe_vars ), qe_res_n ); + //create new smt engine to do quantifier elimination + SmtEngine smt_qe( d_exprManager ); + smt_qe.setLogic(getLogicInfo()); + Trace("smt-synth") << "Property is non-ground single invocation, run QE to obtain single invocation." << std::endl; + //partition variables + std::vector< Node > qe_vars; + std::vector< Node > nqe_vars; + for( unsigned i=0; i orig; + std::vector< Node > subs; + //skolemize non-qe variables + for( unsigned i=0; imkSkolem( "k", nqe_vars[i].getType(), "qe for non-ground single invocation" ); + orig.push_back( nqe_vars[i] ); + subs.push_back( k ); + Trace("smt-synth") << " subs : " << nqe_vars[i] << " -> " << k << std::endl; + } + for( std::map< Node, bool >::iterator it = sip.d_funcs.begin(); it != sip.d_funcs.end(); ++it ){ + orig.push_back( sip.d_func_inv[it->first] ); + Node k = NodeManager::currentNM()->mkSkolem( "k", sip.d_func_fo_var[it->first].getType(), "qe for function in non-ground single invocation" ); + subs.push_back( k ); + Trace("smt-synth") << " subs : " << sip.d_func_inv[it->first] << " -> " << k << std::endl; + } + Node conj_se_ngsi = sip.getFullSpecification(); + Node conj_se_ngsi_subs = conj_se_ngsi.substitute( orig.begin(), orig.end(), subs.begin(), subs.end() ); + Assert( !qe_vars.empty() ); + conj_se_ngsi_subs = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, qe_vars ), conj_se_ngsi_subs ); + + Trace("smt-synth") << "Run quantifier elimination on " << conj_se_ngsi_subs << std::endl; + Expr qe_res = smt_qe.doQuantifierElimination( conj_se_ngsi_subs.toExpr(), true, false ); + Trace("smt-synth") << "Result : " << qe_res << std::endl; + + //create single invocation conjecture + Node qe_res_n = Node::fromExpr( qe_res ); + qe_res_n = qe_res_n.substitute( subs.begin(), subs.end(), orig.begin(), orig.end() ); + if( !nqe_vars.empty() ){ + qe_res_n = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, nqe_vars ), qe_res_n ); + } + Assert( conj.getNumChildren()==3 ); + qe_res_n = NodeManager::currentNM()->mkNode( kind::FORALL, conj[0], qe_res_n, conj[2] ); + Trace("smt-synth") << "Converted conjecture after QE : " << qe_res_n << std::endl; + e_check = qe_res_n.toExpr(); } - Assert( conj.getNumChildren()==3 ); - qe_res_n = NodeManager::currentNM()->mkNode( kind::FORALL, conj[0], qe_res_n, conj[2] ); - Trace("smt-synth") << "Converted conjecture after QE : " << qe_res_n << std::endl; - e_check = qe_res_n.toExpr(); } } diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 955dc5d86..db597d031 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -137,11 +137,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ doInstantiationRound( e ); if( d_quantEngine->inConflict() ){ Assert( d_quantEngine->getNumLemmasWaiting()>lastWaiting ); - Trace("inst-engine") << "Conflict = " << d_quantEngine->getNumLemmasWaiting() << " / " << d_quantEngine->getNumLemmasAddedThisRound(); - if( lastWaiting>0 ){ - Trace("inst-engine") << " (prev " << lastWaiting << ")"; - } - Trace("inst-engine") << std::endl; + Trace("inst-engine") << "Conflict, added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; }else if( d_quantEngine->hasAddedLemma() ){ Trace("inst-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; } diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 0bbca88eb..3063e7a2f 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -221,11 +221,12 @@ int ModelEngine::checkModel(){ //print debug information if( d_quantEngine->inConflict() ){ - Trace("model-engine") << "Conflict = " << d_quantEngine->getNumLemmasWaiting() << " / " << d_quantEngine->getNumLemmasAddedThisRound() << std::endl; + Trace("model-engine") << "Conflict, added lemmas = "; }else{ - Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / "; - Trace("model-engine") << d_totalLemmas << std::endl; - } + Trace("model-engine") << "Added Lemmas = "; + } + Trace("model-engine") << d_addedLemmas << " / " << d_triedLemmas << " / "; + Trace("model-engine") << d_totalLemmas << std::endl; return d_addedLemmas; } diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 6963f7e62..e41dfc67a 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -230,7 +230,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { ret = ret.negate(); status = REWRITE_AGAIN_FULL; }else if( in.getKind()==FORALL ){ - if( in[1].isConst() ){ + if( in[1].isConst() && in.getNumChildren()==2 ){ return RewriteResponse( status, in[1] ); }else{ //compute attributes diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 61c02d3ac..ae9426172 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -3111,6 +3111,7 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > std::string name = std::string( str.begin() + found +1, str.end() ); out << name; }else{ + Trace("ajr-temp") << "[[print operator " << op << "]]" << std::endl; out << op; } if( n.getNumChildren()>0 ){ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 12edb5277..afb7aeb92 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -89,7 +89,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_tr_trie = new inst::TriggerTrie; d_curr_effort_level = QEFFORT_NONE; d_conflict = false; - d_num_added_lemmas_round = 0; d_hasAddedLemma = false; //don't add true lemma d_lemmas_produced_c[d_term_db->d_true] = true; @@ -367,7 +366,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ } d_conflict = false; - d_num_added_lemmas_round = 0; d_hasAddedLemma = false; bool setIncomplete = false; if( e==Theory::EFFORT_LAST_CALL ){ @@ -969,7 +967,6 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){ d_lemmas_produced_c[ lem ] = true; d_lemmas_waiting.push_back( lem ); Trace("inst-add-debug") << "Added lemma" << std::endl; - d_num_added_lemmas_round++; return true; }else{ Trace("inst-add-debug") << "Duplicate." << std::endl; @@ -978,7 +975,6 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){ }else{ //do not need to rewrite, will be rewritten after sending d_lemmas_waiting.push_back( lem ); - d_num_added_lemmas_round++; return true; } } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 60666c4a9..7522c633b 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -158,8 +158,6 @@ private: //this information is reset during check /** are we in conflict */ bool d_conflict; context::CDO< bool > d_conflict_c; - /** number of lemmas we actually added this round (for debugging) */ - unsigned d_num_added_lemmas_round; /** has added lemma this round */ bool d_hasAddedLemma; private: @@ -332,8 +330,6 @@ public: bool inConflict() { return d_conflict; } /** get number of waiting lemmas */ unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); } - /** get number of waiting lemmas */ - unsigned getNumLemmasAddedThisRound() { return d_num_added_lemmas_round; } /** get needs check */ bool getInstWhenNeedsCheck( Theory::Effort e ); /** get user pat mode */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index b3e1925ae..93aedd17b 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3275,11 +3275,9 @@ void TheoryStrings::separateByLength(std::vector< Node >& n, Assert( d_equalityEngine.getRepresentative(eqc)==eqc ); EqcInfo* ei = getOrMakeEqcInfo( eqc, false ); Node lt = ei ? ei->d_length_term : Node::null(); - Trace("ajr-temp") << "Length term for " << eqc << " is " << lt << std::endl; if( !lt.isNull() ){ lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt ); Node r = d_equalityEngine.getRepresentative( lt ); - Trace("ajr-temp") << "Length term rep for " << eqc << " is " << lt << std::endl; if( eqc_to_leqc.find( r )==eqc_to_leqc.end() ){ eqc_to_leqc[r] = leqc_counter; leqc_to_eqc[leqc_counter] = r; diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 8c847be60..695c52cc6 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -49,7 +49,8 @@ TESTS = commutative.sy \ dt-test-ns.sy \ no-mention.sy \ max2-univ.sy \ - strings-small.sy + strings-small.sy \ + strings-unconstrained.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress0/sygus/strings-unconstrained.sy b/test/regress/regress0/sygus/strings-unconstrained.sy new file mode 100644 index 000000000..38e69e337 --- /dev/null +++ b/test/regress/regress0/sygus/strings-unconstrained.sy @@ -0,0 +1,15 @@ +; EXPECT: unsat +; COMMAND-LINE: --no-dump-synth +(set-logic SLIA) +(synth-fun f ((firstname String) (lastname String)) String +((Start String (ntString)) + +(ntString String ( +firstname +lastname +" " +(str.++ ntString ntString))) +)) + +(check-synth) + -- cgit v1.2.3