theory/quantifiers/quant_equality_engine.cpp \
theory/quantifiers/ceg_instantiator.h \
theory/quantifiers/ceg_instantiator.cpp \
+ theory/quantifiers/quant_split.h \
+ theory/quantifiers/quant_split.cpp \
theory/arith/theory_arith_type_rules.h \
theory/arith/type_enumerator.h \
theory/arith/arithvar.h \
bool Datatype::isRecursiveSingleton() const throw(IllegalArgumentException) {
PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
if( d_card_rec_singleton==0 ){
- Assert( d_card_u_assume.empty() );
- std::vector< Type > processing;
- if( computeCardinalityRecSingleton( processing, d_card_u_assume ) ){
- d_card_rec_singleton = 1;
+ if( isCodatatype() ){
+ Assert( d_card_u_assume.empty() );
+ std::vector< Type > processing;
+ if( computeCardinalityRecSingleton( processing, d_card_u_assume ) ){
+ d_card_rec_singleton = 1;
+ }else{
+ d_card_rec_singleton = -1;
+ }
+ if( d_card_rec_singleton==1 ){
+ Trace("dt-card") << "Datatype " << getName() << " is recursive singleton, dependent upon " << d_card_u_assume.size() << " uninterpreted sorts: " << std::endl;
+ for( unsigned i=0; i<d_card_u_assume.size(); i++ ){
+ Trace("dt-card") << " " << d_card_u_assume [i] << std::endl;
+ }
+ Trace("dt-card") << std::endl;
+ }
}else{
d_card_rec_singleton = -1;
}
- if( d_card_rec_singleton==1 ){
- Trace("dt-card") << "Datatype " << getName() << " is recursive singleton, dependent upon " << d_card_u_assume.size() << " uninterpreted sorts: " << std::endl;
- for( unsigned i=0; i<d_card_u_assume.size(); i++ ){
- Trace("dt-card") << " " << d_card_u_assume [i] << std::endl;
- }
- Trace("dt-card") << std::endl;
- }
}
return d_card_rec_singleton==1;
}
\n\
";
+const std::string OptionsHandler::s_quantDSplitHelp = "\
+Template modes for quantifiers splitting, supported by --quant-split:\n\
+\n\
+none \n\
++ Never split quantified formulas.\n\
+\n\
+default \n\
++ Split quantified formulas over some finite datatypes when finite model finding is enabled.\n\
+\n\
+agg \n\
++ Aggressively split quantified formulas.\n\
+\n\
+";
+
theory::quantifiers::InstWhenMode OptionsHandler::stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException) {
if(optarg == "pre-full") {
return theory::quantifiers::INST_WHEN_PRE_FULL;
}
}
+theory::quantifiers::QuantDSplitMode OptionsHandler::stringToQuantDSplitMode(std::string option, std::string optarg) throw(OptionException) {
+ if(optarg == "none" ) {
+ return theory::quantifiers::QUANT_DSPLIT_MODE_NONE;
+ } else if(optarg == "default") {
+ return theory::quantifiers::QUANT_DSPLIT_MODE_DEFAULT;
+ } else if(optarg == "agg") {
+ return theory::quantifiers::QUANT_DSPLIT_MODE_AGG;
+ } else if(optarg == "help") {
+ puts(s_quantDSplitHelp.c_str());
+ exit(1);
+ } else {
+ throw OptionException(std::string("unknown option for --quant-dsplit-mode: `") +
+ optarg + "'. Try --quant-dsplit-mode help.");
+ }
+}
// theory/bv/options_handlers.h
void OptionsHandler::abcEnabledBuild(std::string option, bool value) throw(OptionException) {
** \verbatim
** Original author: Tim King
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
** 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
theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException);
theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException);
theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException);
+ theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode(std::string option, std::string optarg) throw(OptionException);
// theory/bv/options_handlers.h
void abcEnabledBuild(std::string option, bool value) throw(OptionException);
static const std::string s_iteLiftQuantHelp;
static const std::string s_literalMatchHelp;
static const std::string s_macrosQuantHelp;
+ static const std::string s_quantDSplitHelp;
static const std::string s_mbqiModeHelp;
static const std::string s_modelFormatHelp;
static const std::string s_prenexQuantModeHelp;
MACROS_QUANT_MODE_GROUND_UF,
};
+enum QuantDSplitMode {
+ /** never do quantifiers splitting */
+ QUANT_DSPLIT_MODE_NONE,
+ /** default */
+ QUANT_DSPLIT_MODE_DEFAULT,
+ /** do quantifiers splitting aggressively */
+ QUANT_DSPLIT_MODE_AGG,
+};
+
+
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
perform quantifiers macro expansion
option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::MacrosQuantMode :default CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF :include "options/quantifiers_modes.h" :handler stringToMacrosQuantMode
mode for quantifiers macro expansion
+option quantDynamicSplit --quant-dsplit-mode=MODE CVC4::theory::quantifiers::QuantDSplitMode :read-write :default CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_DEFAULT :include "options/quantifiers_modes.h" :handler stringToQuantDSplitMode
+ mode for dynamic quantifiers splitting
### recursive function options
options::preSkolemQuantNested.set( false );
}
}
+ if( !d_logic.isTheoryEnabled(THEORY_DATATYPES) ){
+ options::quantDynamicSplit.set( quantifiers::QUANT_DSPLIT_MODE_NONE );
+ }
//until bugs 371,431 are fixed
if( ! options::minisatUseElim.wasSetByUser()){
return AlphaEquivalenceNode::registerNode( &(aetn->d_data), qe, q, tt, arg_index );
}
-bool AlphaEquivalence::registerQuantifier( Node q ) {
+bool AlphaEquivalence::reduceQuantifier( Node q ) {
Assert( q.getKind()==FORALL );
Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
//construct canonical quantified formula
sto.d_tdb = d_qe->getTermDatabase();
std::sort( typs.begin(), typs.end(), sto );
Trace("aeq-debug") << " ";
- bool ret = AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count );
+ bool ret = !AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count );
Trace("aeq") << " ...result : " << ret << std::endl;
return ret;
}
AlphaEquivalence( QuantifiersEngine* qe ) : d_qe( qe ){}
~AlphaEquivalence(){}
- bool registerQuantifier( Node q );
+ bool reduceQuantifier( Node q );
};
}
}
-void FirstOrderModel::assertQuantifier( Node n, bool reduced ){
- if( !reduced ){
- if( n.getKind()==FORALL ){
- d_forall_asserts.push_back( n );
- }else if( n.getKind()==NOT ){
- Assert( n[0].getKind()==FORALL );
- }
- }else{
- Assert( n.getKind()==FORALL );
- Assert( d_forall_to_reduce.find( n )==d_forall_to_reduce.end() );
- d_forall_to_reduce[n] = true;
- Trace("quant") << "Mark to reduce : " << n << std::endl;
+void FirstOrderModel::assertQuantifier( Node n ){
+ if( n.getKind()==FORALL ){
+ d_forall_asserts.push_back( n );
+ }else if( n.getKind()==NOT ){
+ Assert( n[0].getKind()==FORALL );
}
}
/** needs check */
bool FirstOrderModel::checkNeeded() {
- return d_forall_asserts.size()>0 || !d_forall_to_reduce.empty();
-}
-
-/** mark reduced */
-void FirstOrderModel::markQuantifierReduced( Node q ) {
- Assert( d_forall_to_reduce.find( q )!=d_forall_to_reduce.end() );
- d_forall_to_reduce.erase( q );
- Trace("quant") << "Mark reduced : " << q << std::endl;
+ return d_forall_asserts.size()>0;
}
void FirstOrderModel::reset_round() {
d_quant_active.clear();
}
+//bool FirstOrderModel::isQuantifierAsserted( TNode q ) {
+// return d_forall_asserts.find( q )!=d_forall_asserts.end();
+//}
+
void FirstOrderModel::setQuantifierActive( TNode q, bool active ) {
d_quant_active[q] = active;
}
QuantifiersEngine * d_qe;
/** list of quantifiers asserted in the current context */
context::CDList<Node> d_forall_asserts;
- /** list of quantifiers that have been marked to reduce */
- std::map< Node, bool > d_forall_to_reduce;
/** is model set */
context::CDO< bool > d_isModelSet;
/** get variable id */
virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0;
public: //for Theory Quantifiers:
/** assert quantifier */
- void assertQuantifier( Node n, bool reduced = false );
+ void assertQuantifier( Node n );
/** get number of asserted quantifiers */
int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); }
/** get asserted quantifier */
Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; }
- /** get number to reduce quantifiers */
- unsigned getNumToReduceQuantifiers() { return d_forall_to_reduce.size(); }
/** initialize model for term */
void initializeModelForTerm( Node n, std::map< Node, bool >& visited );
virtual void processInitializeModelForTerm( Node n ) = 0;
Node getSomeDomainElement(TypeNode tn);
/** do we need to do any work? */
bool checkNeeded();
- /** mark reduced */
- void markQuantifierReduced( Node q );
private:
//list of inactive quantified formulas
std::map< TNode, bool > d_quant_active;
public:
/** reset round */
void reset_round();
+ /** is quantified formula asserted */
+ //bool isQuantifierAsserted( TNode q );
/** set quantified formula active/inactive
* a quantified formula may be set inactive if for instance:
* - it is entailed by other quantified formulas
bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ){
if( visited.find( n )==visited.end() ){
visited[n] = true;
- if( n.getKind()!=INST_CONSTANT && TermDb::hasInstConstAttr( n ) ){
+ if( n.getKind()!=BOUND_VARIABLE && TermDb::hasBoundVarAttr( n ) ){
if( !inst::Trigger::isCbqiKind( n.getKind() ) ){
Trace("cbqi-debug2") << "Non-cbqi kind : " << n.getKind() << " in " << n << std::endl;
return true;
}else if( n.getKind()==MULT && ( n.getNumChildren()!=2 || !n[0].isConst() ) ){
Trace("cbqi-debug2") << "Non-linear arithmetic : " << n << std::endl;
return true;
+ }else if( n.getKind()==FORALL ){
+ return hasNonCbqiOperator( n[1], visited );
}else{
for( unsigned i=0; i<n.getNumChildren(); i++ ){
if( hasNonCbqiOperator( n[i], visited ) ){
}else{
//if quantifier has a non-arithmetic variable, then do not use cbqi
//if quantifier has an APPLY_UF term, then do not use cbqi
- Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
+ //Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
std::map< Node, bool > visited;
- ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( cb, visited );
+ ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( q[1], visited );
}
}
}
/********************* */
-/*! \file quant_util.cpp
+/*! \file local_theory_ext.cpp
** \verbatim
** Original author: Andrew Reynolds
** Major contributors: none
}
/** add quantifier */
-bool LtePartialInst::addQuantifier( Node q ) {
- if( d_do_inst.find( q )!=d_do_inst.end() ){
- if( d_do_inst[q] ){
- d_lte_asserts.push_back( q );
- return true;
+void LtePartialInst::preRegisterQuantifier( Node q ) {
+ if( !q.getAttribute(LtePartialInstAttribute()) ){
+ if( d_do_inst.find( q )!=d_do_inst.end() ){
+ if( d_do_inst[q] ){
+ d_lte_asserts.push_back( q );
+ d_quantEngine->setOwner( q, this );
+ }
}else{
- return false;
- }
- }else{
- d_vars[q].clear();
- d_pat_var_order[q].clear();
- //check if this quantified formula is eligible for partial instantiation
- std::map< Node, bool > vars;
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
- vars[q[0][i]] = false;
- }
- getEligibleInstVars( q[1], vars );
-
- //instantiate only if we would force ground instances
- std::map< Node, int > var_order;
- bool doInst = true;
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
- if( vars[q[0][i]] ){
- d_vars[q].push_back( q[0][i] );
- var_order[q[0][i]] = i;
- }else{
- Trace("lte-partial-inst-debug") << "...do not consider, variable " << q[0][i] << " was not found in correct position in body." << std::endl;
- doInst = false;
- break;
+ d_vars[q].clear();
+ d_pat_var_order[q].clear();
+ //check if this quantified formula is eligible for partial instantiation
+ std::map< Node, bool > vars;
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+ vars[q[0][i]] = false;
}
- }
- if( doInst ){
- //also needs patterns
- if( q.getNumChildren()==3 && q[2].getNumChildren()==1 ){
- for( unsigned i=0; i<q[2][0].getNumChildren(); i++ ){
- Node pat = q[2][0][i];
- if( pat.getKind()==APPLY_UF ){
- for( unsigned j=0; j<pat.getNumChildren(); j++ ){
- if( !addVariableToPatternList( pat[j], d_pat_var_order[q], var_order ) ){
- doInst = false;
+ getEligibleInstVars( q[1], vars );
+
+ //instantiate only if we would force ground instances
+ std::map< Node, int > var_order;
+ bool doInst = true;
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+ if( vars[q[0][i]] ){
+ d_vars[q].push_back( q[0][i] );
+ var_order[q[0][i]] = i;
+ }else{
+ Trace("lte-partial-inst-debug") << "...do not consider, variable " << q[0][i] << " was not found in correct position in body." << std::endl;
+ doInst = false;
+ break;
+ }
+ }
+ if( doInst ){
+ //also needs patterns
+ if( q.getNumChildren()==3 && q[2].getNumChildren()==1 ){
+ for( unsigned i=0; i<q[2][0].getNumChildren(); i++ ){
+ Node pat = q[2][0][i];
+ if( pat.getKind()==APPLY_UF ){
+ for( unsigned j=0; j<pat.getNumChildren(); j++ ){
+ if( !addVariableToPatternList( pat[j], d_pat_var_order[q], var_order ) ){
+ doInst = false;
+ }
}
+ }else if( !addVariableToPatternList( pat, d_pat_var_order[q], var_order ) ){
+ doInst = false;
+ }
+ if( !doInst ){
+ Trace("lte-partial-inst-debug") << "...do not consider, cannot resolve pattern : " << pat << std::endl;
+ break;
}
- }else if( !addVariableToPatternList( pat, d_pat_var_order[q], var_order ) ){
- doInst = false;
- }
- if( !doInst ){
- Trace("lte-partial-inst-debug") << "...do not consider, cannot resolve pattern : " << pat << std::endl;
- break;
}
+ }else{
+ Trace("lte-partial-inst-debug") << "...do not consider (must have exactly one pattern)." << std::endl;
}
- }else{
- Trace("lte-partial-inst-debug") << "...do not consider (must have exactly one pattern)." << std::endl;
+ }
+
+
+ Trace("lte-partial-inst") << "LTE: ...will " << ( doInst ? "" : "not ") << "instantiate " << q << std::endl;
+ d_do_inst[q] = doInst;
+ if( doInst ){
+ d_lte_asserts.push_back( q );
+ d_needsCheck = true;
+ d_quantEngine->setOwner( q, this );
}
}
-
-
- Trace("lte-partial-inst") << "LTE: ...will " << ( doInst ? "" : "not ") << "instantiate " << q << std::endl;
- d_do_inst[q] = doInst;
- if( doInst ){
- d_lte_asserts.push_back( q );
- d_needsCheck = true;
- }
- return doInst;
}
}
Assert( !conj.empty() );
lemmas.push_back( NodeManager::currentNM()->mkNode( OR, q.negate(), conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ) ) );
d_wasInvoked = true;
- d_quantEngine->getModel()->markQuantifierReduced( q );
}
}
}
bool addVariableToPatternList( Node v, std::vector< int >& pat_var_order, std::map< Node, int >& var_order );
public:
LtePartialInst( QuantifiersEngine * qe, context::Context* c );
- /** add quantifier : special form of registration */
- bool addQuantifier( Node q );
+ /** determine whether this quantified formula will be reduced */
+ void preRegisterQuantifier( Node q );
/** was invoked */
bool wasInvoked() { return d_wasInvoked; }
--- /dev/null
+/********************* */
+/*! \file quant_split.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** 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
+ **
+ ** \brief Implementation of local theory ext utilities
+ **/
+
+#include "theory/quantifiers/quant_split.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "options/quantifiers_options.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+
+QuantDSplit::QuantDSplit( QuantifiersEngine * qe, context::Context* c ) :
+QuantifiersModule( qe ), d_added_split( qe->getUserContext() ){
+
+}
+
+/** pre register quantifier */
+void QuantDSplit::preRegisterQuantifier( Node q ) {
+ int max_index = -1;
+ int max_score = -1;
+ if( q.getNumChildren()==3 ){
+ return;
+ }
+ Trace("quant-dsplit-debug") << "Check split quantified formula : " << q << std::endl;
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+ TypeNode tn = q[0][i].getType();
+ if( tn.isDatatype() ){
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ if( dt.isRecursiveSingleton() ){
+ Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is recursive singleton." << std::endl;
+ }else{
+ int score = -1;
+ if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
+ score = dt.isFinite() ? 1 : -1;
+ }else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){
+ score = dt.isUFinite() ? 1 : -1;
+ }
+ Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << std::endl;
+ if( score>max_score ){
+ max_index = i;
+ max_score = score;
+ }
+ }
+ }
+ }
+
+ if( max_index!=-1 ){
+ Trace("quant-dsplit-debug") << "Will split at index " << max_index << "." << std::endl;
+ d_quant_to_reduce[q] = max_index;
+ d_quantEngine->setOwner( q, this );
+ }
+}
+
+/* whether this module needs to check this round */
+bool QuantDSplit::needsCheck( Theory::Effort e ) {
+ return e>=Theory::EFFORT_FULL;
+}
+/* Call during quantifier engine's check */
+void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) {
+ //flush lemmas ASAP (they are a reduction)
+ if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){
+ std::vector< Node > lemmas;
+ for(std::map< Node, int >::iterator it = d_quant_to_reduce.begin(); it != d_quant_to_reduce.end(); ++it) {
+ Node q = it->first;
+ if( d_added_split.find( q )==d_added_split.end() ){
+ d_added_split.insert( q );
+ std::vector< Node > bvs;
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+ if( (int)i!=it->second ){
+ bvs.push_back( q[0][i] );
+ }
+ }
+ std::vector< Node > disj;
+ disj.push_back( q.negate() );
+ TNode svar = q[0][it->second];
+ TypeNode tn = svar.getType();
+ if( tn.isDatatype() ){
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
+ std::vector< Node > vars;
+ for( unsigned k=0; k<dt[j].getNumArgs(); k++ ){
+ TypeNode tns = TypeNode::fromType( dt[j][k].getRangeType() );
+ Node v = NodeManager::currentNM()->mkBoundVar( tns );
+ vars.push_back( v );
+ }
+ std::vector< Node > bvs_cmb;
+ bvs_cmb.insert( bvs_cmb.end(), bvs.begin(), bvs.end() );
+ bvs_cmb.insert( bvs_cmb.end(), vars.begin(), vars.end() );
+ vars.insert( vars.begin(), Node::fromExpr( dt[j].getConstructor() ) );
+ Node c = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, vars );
+ TNode ct = c;
+ Node body = q[1].substitute( svar, ct );
+ if( !bvs_cmb.empty() ){
+ body = NodeManager::currentNM()->mkNode( kind::FORALL, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bvs_cmb ), body );
+ }
+ disj.push_back( body );
+ }
+ }else{
+ Assert( false );
+ }
+ lemmas.push_back( disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj ) );
+ }
+ }
+
+ //add lemmas to quantifiers engine
+ for( unsigned i=0; i<lemmas.size(); i++ ){
+ Trace("quant-dsplit") << "QuantDSplit lemma : " << lemmas[i] << std::endl;
+ d_quantEngine->addLemma( lemmas[i], false );
+ }
+ }
+}
+
--- /dev/null
+/********************* */
+/*! \file quant_split.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** 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
+ **
+ ** \brief dynamic quantifiers splitting
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANT_SPLIT_H
+#define __CVC4__THEORY__QUANT_SPLIT_H
+
+#include "theory/quantifiers_engine.h"
+#include "context/cdo.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class QuantDSplit : public QuantifiersModule {
+ typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+private:
+ /** list of relevant quantifiers asserted in the current context */
+ std::map< Node, int > d_quant_to_reduce;
+ /** whether we have instantiated quantified formulas */
+ NodeSet d_added_split;
+public:
+ QuantDSplit( QuantifiersEngine * qe, context::Context* c );
+ /** determine whether this quantified formula will be reduced */
+ void preRegisterQuantifier( Node q );
+
+ /* whether this module needs to check this round */
+ bool needsCheck( Theory::Effort e );
+ /* Call during quantifier engine's check */
+ void check( Theory::Effort e, unsigned quant_e );
+ /* Called for new quantifiers */
+ void registerQuantifier( Node q ) {}
+ void assertNode( Node n ) {}
+ /** Identify this module (for debugging, dynamic configuration, etc..) */
+ std::string identify() const { return "QuantDSplit"; }
+};
+
+}
+}
+}
+
+#endif
#include "theory/quantifiers/rewrite_engine.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/trigger.h"
+#include "theory/quantifiers/quant_split.h"
#include "theory/theory_engine.h"
#include "theory/uf/equality_engine.h"
#include "theory/uf/theory_uf.h"
d_sg_gen = NULL;
d_inst_engine = NULL;
d_i_cbqi = NULL;
+ d_qsplit = NULL;
d_model_engine = NULL;
d_bint = NULL;
d_rr_engine = NULL;
delete d_uee;
delete d_fs;
delete d_i_cbqi;
+ delete d_qsplit;
}
EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() {
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 ) ||
+ options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_AGG ){
+ d_qsplit = new quantifiers::QuantDSplit( this, c );
+ d_modules.push_back( d_qsplit );
+ }
if( options::quantAlphaEquiv() ){
d_alpha_equiv = new quantifiers::AlphaEquivalence( this );
}
}
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_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;
}
if( d_alpha_equiv ){
Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl;
//add equivalence with another quantified formula
- if( !d_alpha_equiv->registerQuantifier( q ) ){
+ if( d_alpha_equiv->reduceQuantifier( q ) ){
Trace("quant-engine-red") << "...alpha equivalence success." << std::endl;
++(d_statistics.d_red_alpha_equiv);
d_quants_red[q] = true;
return true;
}
}
- if( d_lte_part_inst && !q.getAttribute(LtePartialInstAttribute()) ){
- //will partially instantiate
- Trace("quant-engine-red") << "LTE: Partially instantiate " << q << "?" << std::endl;
- if( d_lte_part_inst->addQuantifier( q ) ){
- Trace("quant-engine-red") << "...LTE partially instantiate success." << std::endl;
- //delayed reduction : assert to model
- d_model->assertQuantifier( q, true );
- ++(d_statistics.d_red_lte_partial_inst);
- d_quants_red[q] = true;
- return true;
- }
- }
d_quants_red[q] = false;
return false;
}else{
virtual void check( Theory::Effort e, unsigned quant_e ) = 0;
/* check was complete (e.g. no lemmas implies a model) */
virtual bool checkComplete() { return true; }
- /* Called for new quantifiers */
- virtual void preRegisterQuantifier( Node q ) {}
+ /* Called for new quantified formulas */
+ virtual void preRegisterQuantifier( Node q ) { }
/* Called for new quantifiers after owners are finalized */
virtual void registerQuantifier( Node q ) = 0;
virtual void assertNode( Node n ) {}
class QuantEqualityEngine;
class FullSaturation;
class InstStrategyCbqi;
+ class QuantDSplit;
}/* CVC4::theory::quantifiers */
namespace inst {
quantifiers::FullSaturation * d_fs;
/** counterexample-based quantifier instantiation */
quantifiers::InstStrategyCbqi * d_i_cbqi;
+ /** quantifiers splitting */
+ quantifiers::QuantDSplit * d_qsplit;
public: //effort levels
enum {
QEFFORT_CONFLICT,
quantifiers::FullSaturation * getFullSaturation() { return d_fs; }
/** get inst strategy cbqi */
quantifiers::InstStrategyCbqi * getInstStrategyCbqi() { return d_i_cbqi; }
+ /** get quantifiers splitting */
+ quantifiers::QuantDSplit * getQuantDSplit() { return d_qsplit; }
private:
/** owner of quantified formulas */
std::map< Node, QuantifiersModule * > d_owner;
/** get next decision request */
Node getNextDecisionRequest();
private:
- /** reduce quantifier */
+ /** reduceQuantifier, return true if reduced */
bool reduceQuantifier( Node q );
/** compute term vector */
void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
loopy_coda.smt2 \
fmc_unsound_model.smt2 \
am-bad-model.cvc \
- nun-0208-to.smt2
+ nun-0208-to.smt2 \
+ datatypes-ufinite.smt2
EXTRA_DIST = $(TESTS)
--- /dev/null
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(declare-sort U 0)
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+(declare-fun d () U)
+(assert (distinct a b c))
+(declare-sort V 0)
+(declare-datatypes () ((ufin1 (cons1 (s11 U) (s12 U) (s13 U))) (ufin2 (cons2 (s21 V) (s22 U)) (cons3))))
+(declare-fun P (ufin1 ufin2) Bool)
+(declare-fun Q (ufin1 ufin1) Bool)
+(assert (forall ((x ufin1) (y ufin2) (z ufin1)) (or (P x y) (Q x z))))
+(assert (not (P (cons1 a a a) cons3)))
+(assert (not (Q (cons1 a d a) (cons1 a b c))))
+(check-sat)
projects / cvc5.git / commitdiff