From f47f24528f5d19ac0affd572f3d34c090e97f9f9 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 18 Feb 2016 22:50:05 -0600 Subject: [PATCH] Implement dynamic splitting for quantified formulas. Minor refactoring of reductions in quantifiers engine. --- src/Makefile.am | 2 + src/expr/datatype.cpp | 26 ++-- src/options/options_handler.cpp | 29 ++++ src/options/options_handler.h | 4 +- src/options/quantifiers_modes.h | 10 ++ src/options/quantifiers_options | 2 + src/smt/smt_engine.cpp | 3 + src/theory/quantifiers/alpha_equivalence.cpp | 4 +- src/theory/quantifiers/alpha_equivalence.h | 2 +- src/theory/quantifiers/first_order_model.cpp | 30 ++-- src/theory/quantifiers/first_order_model.h | 10 +- src/theory/quantifiers/inst_strategy_cbqi.cpp | 8 +- src/theory/quantifiers/local_theory_ext.cpp | 113 ++++++++------- src/theory/quantifiers/local_theory_ext.h | 4 +- src/theory/quantifiers/quant_split.cpp | 129 ++++++++++++++++++ src/theory/quantifiers/quant_split.h | 54 ++++++++ src/theory/quantifiers_engine.cpp | 28 ++-- src/theory/quantifiers_engine.h | 11 +- test/regress/regress0/fmf/Makefile.am | 3 +- .../regress0/fmf/datatypes-ufinite.smt2 | 17 +++ 20 files changed, 365 insertions(+), 124 deletions(-) create mode 100644 src/theory/quantifiers/quant_split.cpp create mode 100644 src/theory/quantifiers/quant_split.h create mode 100644 test/regress/regress0/fmf/datatypes-ufinite.smt2 diff --git a/src/Makefile.am b/src/Makefile.am index 4f2998e7a..068e30256 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -350,6 +350,8 @@ libcvc4_la_SOURCES = \ 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 \ diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 99698df99..45a7447aa 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -199,20 +199,24 @@ Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) cons 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; id_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 @@ -99,7 +99,7 @@ bool AlphaEquivalence::registerQuantifier( Node q ) { 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; } diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h index 99517fd2a..18a700842 100644 --- a/src/theory/quantifiers/alpha_equivalence.h +++ b/src/theory/quantifiers/alpha_equivalence.h @@ -48,7 +48,7 @@ public: AlphaEquivalence( QuantifiersEngine* qe ) : d_qe( qe ){} ~AlphaEquivalence(){} - bool registerQuantifier( Node q ); + bool reduceQuantifier( Node q ); }; } diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 272f16be8..6c912cdab 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -36,18 +36,11 @@ d_qe( qe ), d_forall_asserts( c ), d_isModelSet( c, false ){ } -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 ); } } @@ -122,20 +115,17 @@ Node FirstOrderModel::getSomeDomainElement(TypeNode tn){ /** 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; } diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index d42eb61e3..d5dc62667 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -49,8 +49,6 @@ protected: QuantifiersEngine * d_qe; /** list of quantifiers asserted in the current context */ context::CDList 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 */ @@ -59,13 +57,11 @@ protected: 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; @@ -94,14 +90,14 @@ public: 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 diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index ad400413e..e6c9b9e6b 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -169,13 +169,15 @@ void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){ 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; igetTermDatabase()->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 ); } } } diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp index 794032c87..86fbdc7f7 100644 --- a/src/theory/quantifiers/local_theory_ext.cpp +++ b/src/theory/quantifiers/local_theory_ext.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file quant_util.cpp +/*! \file local_theory_ext.cpp ** \verbatim ** Original author: Andrew Reynolds ** Major contributors: none @@ -31,69 +31,69 @@ QuantifiersModule( qe ), d_wasInvoked( false ), d_needsCheck( false ){ } /** 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 var_order; - bool doInst = true; - for( unsigned i=0; i vars; + for( unsigned i=0; i var_order; + bool doInst = true; + for( unsigned i=0; isetOwner( 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; } } @@ -188,7 +188,6 @@ void LtePartialInst::getInstantiations( std::vector< Node >& lemmas ) { 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 ); } } } diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h index 6e2ee34af..d802c2cf7 100644 --- a/src/theory/quantifiers/local_theory_ext.h +++ b/src/theory/quantifiers/local_theory_ext.h @@ -55,8 +55,8 @@ private: 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; } diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp new file mode 100644 index 000000000..e874ee5b8 --- /dev/null +++ b/src/theory/quantifiers/quant_split.cpp @@ -0,0 +1,129 @@ +/********************* */ +/*! \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; imax_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; isecond ){ + 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 vars; + for( unsigned k=0; kmkBoundVar( 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; iaddLemma( lemmas[i], false ); + } + } +} + diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h new file mode 100644 index 000000000..f40acc2fd --- /dev/null +++ b/src/theory/quantifiers/quant_split.h @@ -0,0 +1,54 @@ +/********************* */ +/*! \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 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 diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ce6c929b2..cfb3fda94 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -39,6 +39,7 @@ #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" @@ -121,6 +122,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* 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; @@ -161,6 +163,7 @@ QuantifiersEngine::~QuantifiersEngine(){ delete d_uee; delete d_fs; delete d_i_cbqi; + delete d_qsplit; } EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() { @@ -237,6 +240,11 @@ 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 ) || + 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 ); } @@ -367,9 +375,9 @@ 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_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; } @@ -513,25 +521,13 @@ bool QuantifiersEngine::reduceQuantifier( Node q ) { 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{ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 28fcbbc85..c5c88487b 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -64,8 +64,8 @@ public: 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 ) {} @@ -99,6 +99,7 @@ namespace quantifiers { class QuantEqualityEngine; class FullSaturation; class InstStrategyCbqi; + class QuantDSplit; }/* CVC4::theory::quantifiers */ namespace inst { @@ -157,6 +158,8 @@ private: 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, @@ -253,6 +256,8 @@ public: //modules 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; @@ -281,7 +286,7 @@ public: /** 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 ); diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 8cff980a5..a3ff2fcc7 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -50,7 +50,8 @@ TESTS = \ 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) diff --git a/test/regress/regress0/fmf/datatypes-ufinite.smt2 b/test/regress/regress0/fmf/datatypes-ufinite.smt2 new file mode 100644 index 000000000..d802930fd --- /dev/null +++ b/test/regress/regress0/fmf/datatypes-ufinite.smt2 @@ -0,0 +1,17 @@ +; 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) -- 2.30.2