diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-08 15:49:14 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-08 15:50:20 -0600 |
commit | 2dd6292b73e4e19be2e261c7fe5664bd2b0149bd (patch) | |
tree | 0f4956ec068972da8c8d1c708df7c8b2f7a07f3a /src | |
parent | 3c4c4420ebae4d27d53084453591363942eb4d2e (diff) |
Updates related to finite model finding and (co)datatypes. Bug fix enumerator and codatatype rewriter, further simplify fmc.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/datatypes/datatypes_rewriter.h | 64 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 114 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 2 | ||||
-rw-r--r-- | src/theory/datatypes/type_enumerator.cpp | 6 | ||||
-rw-r--r-- | src/theory/datatypes/type_enumerator.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 24 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 125 | ||||
-rw-r--r-- | src/theory/quantifiers/full_model_check.h | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 4 | ||||
-rw-r--r-- | src/theory/theory_model.cpp | 11 | ||||
-rw-r--r-- | src/theory/theory_model.h | 1 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 2 |
15 files changed, 212 insertions, 175 deletions
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index da2282a2c..1e7e714cf 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -167,19 +167,19 @@ public: //typically should not be called TypeNode tn = in.getType(); Node gt; - if( tn.isSort() ){ + bool useTe = true; + //if( !tn.isSort() ){ + // useTe = false; + //} + if( isTypeDatatype( tn ) ){ + const Datatype& dta = ((DatatypeType)(tn).toType()).getDatatype(); + useTe = !dta.isCodatatype(); + } + if( useTe ){ TypeEnumerator te(tn); gt = *te; }else{ - //check whether well-founded - //bool isWf = true; - //if( isTypeDatatype( tn ) ){ - // const Datatype& dta = ((DatatypeType)(tn).toType()).getDatatype(); - // isWf = dta.isWellFounded(); - //} - //if( isWf || in[0].isConst() ){ gt = tn.mkGroundTerm(); - //} } if( !gt.isNull() ){ //Assert( gtt.isDatatype() || gtt.isParametricDatatype() ); @@ -531,28 +531,32 @@ private: } //eqc_stack stores depth static Node normalizeCodatatypeConstantEqc( Node n, std::map< int, int >& eqc_stack, std::map< Node, int >& eqc, int depth ){ - Assert( eqc.find( n )!=eqc.end() ); - int e = eqc[n]; - std::map< int, int >::iterator it = eqc_stack.find( e ); - if( it!=eqc_stack.end() ){ - int debruijn = depth - it->second - 1; - return NodeManager::currentNM()->mkConst(UninterpretedConstant(n.getType().toType(), debruijn)); + Trace("dt-nconst-debug") << "normalizeCodatatypeConstantEqc: " << n << " depth=" << depth << std::endl; + if( eqc.find( n )==eqc.end() ){ + return n; }else{ - std::vector< Node > children; - bool childChanged = false; - eqc_stack[e] = depth; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - Node nc = normalizeCodatatypeConstantEqc( n[i], eqc_stack, eqc, depth+1 ); - children.push_back( nc ); - childChanged = childChanged || nc!=n[i]; - } - eqc_stack.erase(e); - if( childChanged ){ - Assert( n.getKind()==kind::APPLY_CONSTRUCTOR ); - children.insert( children.begin(), n.getOperator() ); - return NodeManager::currentNM()->mkNode( n.getKind(), children ); + int e = eqc[n]; + std::map< int, int >::iterator it = eqc_stack.find( e ); + if( it!=eqc_stack.end() ){ + int debruijn = depth - it->second - 1; + return NodeManager::currentNM()->mkConst(UninterpretedConstant(n.getType().toType(), debruijn)); }else{ - return n; + std::vector< Node > children; + bool childChanged = false; + eqc_stack[e] = depth; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node nc = normalizeCodatatypeConstantEqc( n[i], eqc_stack, eqc, depth+1 ); + children.push_back( nc ); + childChanged = childChanged || nc!=n[i]; + } + eqc_stack.erase(e); + if( childChanged ){ + Assert( n.getKind()==kind::APPLY_CONSTRUCTOR ); + children.insert( children.begin(), n.getOperator() ); + return NodeManager::currentNM()->mkNode( n.getKind(), children ); + }else{ + return n; + } } } } @@ -675,7 +679,7 @@ public: eqc[it->first] = eqc[it->second]; } //we now have a partition of equivalent terms - Trace("dt-nconst") << "Equivalence classes ids : " << std::endl; + Trace("dt-nconst") << "Computed equivalence classes ids : " << std::endl; for( std::map< Node, int >::iterator it = eqc.begin(); it != eqc.end(); ++it ){ Trace("dt-nconst") << " " << it->first << " -> " << it->second << std::endl; } diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 439fd0cfb..c8d7338a7 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -268,12 +268,13 @@ void TheoryDatatypes::check(Effort e) { } if( needSplit && consIndex!=-1 ) { - //if only one constructor, then this term must be this constructor if( dt.getNumConstructors()==1 ){ + //this may not be necessary? + //if only one constructor, then this term must be this constructor Node t = DatatypesRewriter::mkTester( n, 0, dt ); d_pending.push_back( t ); d_pending_exp[ t ] = d_true; - Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl; + Trace("datatypes-infer") << "DtInfer : 1-cons (full) : " << t << std::endl; d_infer.push_back( t ); }else{ if( options::dtBinarySplit() ){ @@ -402,11 +403,14 @@ void TheoryDatatypes::doPendingMerges(){ d_pending_merge.clear(); } -void TheoryDatatypes::doSendLemma( Node lem ) { +bool TheoryDatatypes::doSendLemma( Node lem ) { if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){ Trace("dt-lemma-send") << "TheoryDatatypes::doSendLemma : " << lem << std::endl; d_lemmas_produced_c[lem] = true; d_out->lemma( lem ); + return true; + }else{ + return false; } } @@ -440,7 +444,6 @@ void TheoryDatatypes::assertFact( Node fact, Node exp ){ Trace("dt-lemma-sygus") << "Sygus symmetry breaking lemma : " << d_sygus_sym_break->d_lemmas[i] << std::endl; doSendLemma( d_sygus_sym_break->d_lemmas[i] ); } - Trace("dt-lemma-sygus") << "No lemmas" << std::endl; d_sygus_sym_break->d_lemmas.clear(); /* if( d_sygus_util->d_conflict ){ @@ -1124,8 +1127,8 @@ void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node nb << (*i); Assert( (*i).getKind()==NOT ); Node t_arg2; - int tindex = DatatypesRewriter::isTester( (*i)[0], t_arg2 ); - Assert( tindex!=-1 ); + DatatypesRewriter::isTester( (*i)[0], t_arg2 ); + //Assert( tindex!=-1 ); if( std::find( eq_terms.begin(), eq_terms.end(), t_arg2 )==eq_terms.end() ){ eq_terms.push_back( t_arg2 ); if( t_arg2!=t_arg ){ @@ -1569,46 +1572,31 @@ void TheoryDatatypes::collectTerms( Node n ) { if( n.getKind() == APPLY_CONSTRUCTOR ){ Debug("datatypes") << " Found constructor " << n << endl; d_consTerms.push_back( n ); - }else if( n.getKind() == APPLY_SELECTOR_TOTAL || n.getKind() == DT_SIZE || n.getKind() == DT_HEIGHT_BOUND ){ - d_selTerms.push_back( n ); - //we must also record which selectors exist - Trace("dt-collapse-sel") << " Found selector " << n << endl; - Node rep = getRepresentative( n[0] ); - //record it in the selectors - EqcInfo* eqc = getOrMakeEqcInfo( rep, true ); - //add it to the eqc info - addSelector( n, eqc, rep ); - - if( n.getKind() == DT_SIZE ){ - Node conc = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst( Rational(0) ), n ); - //must be non-negative - Trace("datatypes-infer") << "DtInfer : non-negative size : " << conc << std::endl; - d_pending.push_back( conc ); - d_pending_exp[ conc ] = d_true; - d_infer.push_back( conc ); -/* - //add size = 0 lemma - Node nn = n.eqNode( NodeManager::currentNM()->mkConst( Rational(0) ) ); - std::vector< Node > children; - children.push_back( nn.negate() ); - const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype(); - for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ - if( DatatypesRewriter::isNullaryConstructor( dt[i] ) ){ - Node test = DatatypesRewriter::mkTester( n[0], i, dt ); - children.push_back( test ); - } - } - conc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ); - Trace("datatypes-infer") << "DtInfer : zero size : " << conc << std::endl; - d_pending.push_back( conc ); - d_pending_exp[ conc ] = d_true; - d_infer.push_back( conc ); -*/ - } + }else{ - if( n.getKind() == DT_HEIGHT_BOUND ){ - if( n[1].getConst<Rational>().isZero() ){ + if( n.getKind() == APPLY_SELECTOR_TOTAL || n.getKind() == DT_SIZE || n.getKind() == DT_HEIGHT_BOUND ){ + d_selTerms.push_back( n ); + //we must also record which selectors exist + Trace("dt-collapse-sel") << " Found selector " << n << endl; + Node rep = getRepresentative( n[0] ); + //record it in the selectors + EqcInfo* eqc = getOrMakeEqcInfo( rep, true ); + //add it to the eqc info + addSelector( n, eqc, rep ); + + if( n.getKind() == DT_SIZE ){ + Node conc = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst( Rational(0) ), n ); + //must be non-negative + Trace("datatypes-infer") << "DtInfer : non-negative size : " << conc << std::endl; + //d_pending.push_back( conc ); + //d_pending_exp[ conc ] = d_true; + //d_infer.push_back( conc ); + d_pending_lem.push_back( conc ); + /* + //add size = 0 lemma + Node nn = n.eqNode( NodeManager::currentNM()->mkConst( Rational(0) ) ); std::vector< Node > children; + children.push_back( nn.negate() ); const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype(); for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ if( DatatypesRewriter::isNullaryConstructor( dt[i] ) ){ @@ -1616,16 +1604,36 @@ void TheoryDatatypes::collectTerms( Node n ) { children.push_back( test ); } } - Node lem; - if( children.empty() ){ - lem = n.negate(); - }else{ - lem = NodeManager::currentNM()->mkNode( IFF, n, children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ) ); + conc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ); + Trace("datatypes-infer") << "DtInfer : zero size : " << conc << std::endl; + d_pending.push_back( conc ); + d_pending_exp[ conc ] = d_true; + d_infer.push_back( conc ); + */ + } + + if( n.getKind() == DT_HEIGHT_BOUND ){ + if( n[1].getConst<Rational>().isZero() ){ + std::vector< Node > children; + const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype(); + for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ + if( DatatypesRewriter::isNullaryConstructor( dt[i] ) ){ + Node test = DatatypesRewriter::mkTester( n[0], i, dt ); + children.push_back( test ); + } + } + Node lem; + if( children.empty() ){ + lem = n.negate(); + }else{ + lem = NodeManager::currentNM()->mkNode( IFF, n, children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ) ); + } + Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl; + //d_pending.push_back( lem ); + //d_pending_exp[ lem ] = d_true; + //d_infer.push_back( lem ); + d_pending_lem.push_back( lem ); } - Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl; - d_pending.push_back( lem ); - d_pending_exp[ lem ] = d_true; - d_infer.push_back( lem ); } } } diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 4dd621c86..d56538b2a 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -203,7 +203,7 @@ private: /** do pending merged */ void doPendingMerges(); /** do send lemma */ - void doSendLemma( Node lem ); + bool doSendLemma( Node lem ); /** get or make eqc info */ EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false ); diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index 57d16d31c..62446a937 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -170,7 +170,9 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype() << std::endl; Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl; Debug("dt-enum") << "datatype is " << d_type << std::endl; - Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton() << " " << d_datatype.isFinite() << std::endl; + Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton(); + Debug("dt-enum") << " " << d_datatype.isFinite() << std::endl; + Debug("dt-enum") << " " << d_datatype.isUFinite() << std::endl; if( d_datatype.isCodatatype() && hasCyclesDt( d_datatype ) ){ //start with uninterpreted constant @@ -218,4 +220,4 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ //set up initial conditions (should always succeed) ++*this; //increment( d_ctor ); AlwaysAssert( !isFinished() ); -}
\ No newline at end of file +} diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 67dabafe4..921ba403c 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -23,6 +23,7 @@ #include "expr/type_node.h" #include "expr/type.h" #include "expr/kind.h" +#include "options/quantifiers_options.h" namespace CVC4 { namespace theory { @@ -158,7 +159,7 @@ public: } if( d_ctor>=d_has_debruijn+d_datatype.getNumConstructors() ){ //try next size limit as long as new terms were generated at last size, or other cases - if( prevSize==d_size_limit || ( d_size_limit==0 && d_datatype.isCodatatype() ) || !d_datatype.isFinite() ){ + if( prevSize==d_size_limit || ( d_size_limit==0 && d_datatype.isCodatatype() ) || ( options::finiteModelFind() ? !d_datatype.isUFinite() : !d_datatype.isFinite() ) ){ d_size_limit++; d_ctor = d_zeroCtor; for( unsigned i=0; i<d_sel_sum.size(); i++ ){ diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index cc0b18ffe..345a5eaef 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -463,9 +463,13 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { lem = Rewriter::rewrite( lem ); Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem << std::endl; Trace("cegqi-engine") << " ...refine candidate." << std::endl; - d_quantEngine->addLemma( lem ); - ++(d_statistics.d_cegqi_lemmas_refine); - conj->d_refine_count++; + bool res = d_quantEngine->addLemma( lem ); + if( res ){ + ++(d_statistics.d_cegqi_lemmas_refine); + conj->d_refine_count++; + }else{ + Trace("cegqi-engine") << " ...FAILED to add refinement!" << std::endl; + } } } conj->d_ce_sk.clear(); diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index aa2a43fbf..272f16be8 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -90,15 +90,19 @@ void FirstOrderModel::initialize() { } processInitializeQuantifier( f ); //initialize relevant models within bodies of all quantifiers - initializeModelForTerm( f[1] ); + std::map< Node, bool > visited; + initializeModelForTerm( f[1], visited ); } processInitialize( false ); } -void FirstOrderModel::initializeModelForTerm( Node n ){ - processInitializeModelForTerm( n ); - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - initializeModelForTerm( n[i] ); +void FirstOrderModel::initializeModelForTerm( Node n, std::map< Node, bool >& visited ){ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + processInitializeModelForTerm( n ); + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + initializeModelForTerm( n[i], visited ); + } } } @@ -574,15 +578,6 @@ Node FirstOrderModelFmc::getUsedRepresentative(Node n, bool strict) { Trace("fmc-warn") << "WARNING : no representative for " << n << std::endl; } } -/* - Node r = getRepresentative(n); - if( d_model_basis_rep.find(tn)!=d_model_basis_rep.end() ){ - if (r==d_model_basis_rep[tn]) { - r = d_qe->getTermDatabase()->getModelBasisTerm(tn); - } - } - return r; -*/ return getRepresentative(n); } } @@ -609,7 +604,6 @@ void FirstOrderModelFmc::processInitialize( bool ispre ) { for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){ it->second->reset(); } - d_model_basis_rep.clear(); } } diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index a31e85d7e..d42eb61e3 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -67,7 +67,7 @@ public: //for Theory Quantifiers: /** get number to reduce quantifiers */ unsigned getNumToReduceQuantifiers() { return d_forall_to_reduce.size(); } /** initialize model for term */ - void initializeModelForTerm( Node n ); + void initializeModelForTerm( Node n, std::map< Node, bool >& visited ); virtual void processInitializeModelForTerm( Node n ) = 0; virtual void processInitializeQuantifier( Node q ) {} public: @@ -169,7 +169,6 @@ class FirstOrderModelFmc : public FirstOrderModel private: /** models for UF */ std::map<Node, Def * > d_models; - std::map<TypeNode, Node > d_model_basis_rep; std::map<TypeNode, Node > d_type_star; Node intervalOp; Node getUsedRepresentative(Node n, bool strict = false); diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index f0858f4e9..00a5241f5 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -325,11 +325,46 @@ QModelBuilder( c, qe ){ d_false = NodeManager::currentNM()->mkConst(false); } +void FullModelChecker::preProcessBuildModel(TheoryModel* m, bool fullModel) { + FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc(); + if( !fullModel ){ + Trace("fmc") << "---Full Model Check preprocess() " << std::endl; + d_preinitialized_types.clear(); + //traverse equality engine + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine ); + std::map< TypeNode, int > typ_num; + while( !eqcs_i.isFinished() ){ + TypeNode tr = (*eqcs_i).getType(); + d_preinitialized_types[tr] = true; + ++eqcs_i; + } + + //must ensure model basis terms exists in model for each relevant type + fm->initialize(); + for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { + Node op = it->first; + TypeNode tno = op.getType(); + for( unsigned i=0; i<tno.getNumChildren(); i++) { + preInitializeType( fm, tno[i] ); + } + } + //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; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node q = fm->getAssertedQuantifier( i ); + //make sure all types are set + for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ + preInitializeType( fm, q[0][i].getType() ); + } + } + } + } +} + void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc(); if( !fullModel ){ Trace("fmc") << "---Full Model Check reset() " << std::endl; - fm->initialize(); d_quant_models.clear(); d_rep_ids.clear(); d_star_insts.clear(); @@ -338,50 +373,26 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ it != fm->d_rep_set.d_type_reps.end(); ++it ){ if( it->first.isSort() ){ Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; - Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(it->first); - Node rmbt = fm->getUsedRepresentative( mbt); - int mbt_index = -1; - Trace("fmc") << " Model basis term : " << mbt << std::endl; for( size_t a=0; a<it->second.size(); a++ ){ Node r = fm->getUsedRepresentative( it->second[a] ); - std::vector< Node > eqc; - ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc ); - Trace("fmc-model-debug") << " " << (it->second[a]==r) << (r==mbt); - Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : "; - //Trace("fmc-model-debug") << r2 << " : " << ir << " : "; - Trace("fmc-model-debug") << " {"; - //find best selection for representative - for( size_t i=0; i<eqc.size(); i++ ){ - Trace("fmc-model-debug") << eqc[i] << ", "; - } - Trace("fmc-model-debug") << "}" << std::endl; - - //if this is the model basis eqc, replace with actual model basis term - if (r==rmbt || (mbt_index==-1 && a==(it->second.size()-1))) { - fm->d_model_basis_rep[it->first] = r; - r = mbt; - mbt_index = a; + if( Trace.isOn("fmc-model-debug") ){ + std::vector< Node > eqc; + ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc ); + Trace("fmc-model-debug") << " " << (it->second[a]==r); + Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : "; + //Trace("fmc-model-debug") << r2 << " : " << ir << " : "; + Trace("fmc-model-debug") << " {"; + for( size_t i=0; i<eqc.size(); i++ ){ + Trace("fmc-model-debug") << eqc[i] << ", "; + } + Trace("fmc-model-debug") << "}" << std::endl; } d_rep_ids[it->first][r] = (int)a; } Trace("fmc-model-debug") << std::endl; - - if (mbt_index==-1) { - std::cout << " WARNING: model basis term is not a representative!" << std::endl; - exit(0); - }else{ - Trace("fmc") << "Star index for " << it->first << " is " << mbt_index << std::endl; - } - } - } - //also process non-rep set sorts - for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { - Node op = it->first; - TypeNode tno = op.getType(); - for( unsigned i=0; i<tno.getNumChildren(); i++) { - initializeType( fm, tno[i] ); } } + //now, make models for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { Node op = it->first; @@ -433,24 +444,26 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ entry_children.push_back(op); bool hasNonStar = false; for( unsigned i=0; i<c.getNumChildren(); i++) { - Node ri = fm->getUsedRepresentative( c[i]); - if( !ri.getType().isSort() && !ri.isConst() ){ - Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << std::endl; - Assert( false ); - } + Node ri = fm->getUsedRepresentative( c[i] ); children.push_back(ri); + bool isStar = false; if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){ if (fm->isModelBasisTerm(ri) ) { ri = fm->getStar( ri.getType() ); + isStar = true; }else{ hasNonStar = true; } } + if( !isStar && !ri.isConst() ){ + Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl; + Assert( false ); + } entry_children.push_back(ri); } Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children ); Node nv = fm->getUsedRepresentative( v ); - if( !nv.getType().isSort() && !nv.isConst() ){ + if( !nv.isConst() ){ Trace("fmc-warn") << "Warning : model has non-constant value in model " << nv << std::endl; Assert( false ); } @@ -523,20 +536,15 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ } } -void FullModelChecker::initializeType( FirstOrderModelFmc * fm, TypeNode tn ){ - if( fm->d_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){ - Trace("fmc") << "Initialize type " << tn << " hasType = " << fm->d_rep_set.hasType(tn) << std::endl; - Node mbn; - if (!fm->d_rep_set.hasType(tn)) { - mbn = fm->getSomeDomainElement(tn); - }else{ - mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn); +void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ){ + if( d_preinitialized_types.find( tn )==d_preinitialized_types.end() ){ + d_preinitialized_types[tn] = true; + Node mb = d_qe->getTermDatabase()->getModelBasisTerm(tn); + if( !mb.isConst() ){ + Trace("fmc") << "...add model basis term to EE of model " << mb << " " << tn << std::endl; + fm->d_equalityEngine->addTerm( mb ); + fm->addTerm( mb ); } - Trace("fmc") << "Get used rep for " << mbn << std::endl; - Node mbnr = fm->getUsedRepresentative( mbn ); - Trace("fmc") << "...got " << mbnr << std::endl; - fm->d_model_basis_rep[tn] = mbnr; - Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl; } } @@ -591,10 +599,6 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, Node op = NodeManager::currentNM()->mkSkolem( "qfmc", typ, "op created for full-model checking" ); d_quant_cond[f] = op; } - //make sure all types are set - for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ - initializeType( fmfmc, f[0][i].getType() ); - } if( options::mbqiMode()==MBQI_NONE ){ //just exhaustive instantiate @@ -643,6 +647,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, Node ev = d_quant_models[f].evaluate(fmfmc, inst); if (ev==d_true) { addInst = false; + Trace("fmc-debug") << "...do not instantiate, evaluation was " << ev << std::endl; } }else{ //for debugging diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index 29913d98d..c7bfcd189 100644 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -92,8 +92,9 @@ protected: std::map<Node, Node > d_quant_cond; std::map< TypeNode, Node > d_array_cond; std::map< Node, Node > d_array_term_cond; - std::map<Node, std::vector< int > > d_star_insts; - void initializeType( FirstOrderModelFmc * fm, TypeNode tn ); + std::map< Node, std::vector< int > > d_star_insts; + std::map< TypeNode, bool > d_preinitialized_types; + void preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ); Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n); bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index); protected: @@ -142,7 +143,8 @@ public: Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ); - /** process build model */ + /** process build model */ + void preProcessBuildModel(TheoryModel* m, bool fullModel); void processBuildModel(TheoryModel* m, bool fullModel); /** get current model value */ Node getCurrentUfModelValue( FirstOrderModelFmc* fm, Node n, std::vector< Node > & args, bool partial ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 6dfd4c737..8bc9689bd 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -971,7 +971,7 @@ Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes } ret = NodeManager::currentNM()->mkNode( OR, nret, n_str_ind ); } - Trace("quantifiers-sk") << "mkSkolem body for " << f << " returns : " << ret << std::endl; + Trace("quantifiers-sk-debug") << "mkSkolem body for " << f << " returns : " << ret << std::endl; //if it has an instantiation level, set the skolemized body to that level if( f.hasAttribute(InstLevelAttribute()) ){ theory::QuantifiersEngine::setInstantiationLevelAttr( ret, f.getAttribute(InstLevelAttribute()) ); @@ -1002,6 +1002,14 @@ Node TermDb::getSkolemizedBody( Node f ){ d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], d_skolem_constants[f][i] ); } } + if( Trace.isOn("quantifiers-sk") ){ + Trace("quantifiers-sk") << "Skolemize : "; + for( unsigned i=0; i<d_skolem_constants[f].size(); i++ ){ + Trace("quantifiers-sk") << d_skolem_constants[f][i] << " "; + } + Trace("quantifiers-sk") << "for " << std::endl; + Trace("quantifiers-sk") << " " << f << std::endl; + } } return d_skolem_body[ f ]; } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index aee3ac4b8..19d66165a 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -602,9 +602,9 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ NodeBuilder<> nb(kind::OR); nb << f << body.notNode(); Node lem = nb; - if( Trace.isOn("quantifiers-sk") ){ + if( Trace.isOn("quantifiers-sk-debug") ){ Node slem = Rewriter::rewrite( lem ); - Trace("quantifiers-sk") << "Skolemize lemma : " << slem << std::endl; + Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem << std::endl; } getOutputChannel().lemma( lem, false, true ); d_skolemized[f] = true; diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index a61df11d8..d024e0270 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -114,7 +114,8 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) c return (*it).second; } Node ret = n; - if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL || n.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) { + if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL || n.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT || + ( n.getKind() == kind::CARDINALITY_CONSTRAINT && options::ufssMode()!=theory::uf::UF_SS_FULL ) ) { // We should have terms, thanks to TheoryQuantifiers::collectModelInfo(). // However, if the Decision Engine stops us early, there might be a // quantifier that isn't assigned. In conjunction with miniscoping, this @@ -570,6 +571,10 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..." << std::endl; d_te->collectModelInfo(tm, fullModel); + // model-builder specific initialization + preProcessBuildModel(tm, fullModel); + + // Loop through all terms and make sure that assignable sub-terms are in the equality engine // Also, record #eqc per type (for finite model finding) std::map< TypeNode, unsigned > eqc_usort_count; @@ -830,6 +835,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) if (t.getCardinality().isInfinite()) { bool success; do{ + Trace("model-builder-debug") << "Enumerate term of type " << t << std::endl; n = typeConstSet.nextTypeEnum(t, true); //--- AJR: this code checks whether n is a legal value Assert( !n.isNull() ); @@ -1016,6 +1022,9 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node return retNode; } +void TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel* m, bool fullModel) { + +} void TheoryEngineModelBuilder::processBuildModel(TheoryModel* m, bool fullModel) { diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 4b27aeacb..b0952538a 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -255,6 +255,7 @@ protected: typedef std::hash_set<Node, NodeHashFunction> NodeSet; /** process build model */ + virtual void preProcessBuildModel(TheoryModel* m, bool fullModel); virtual void processBuildModel(TheoryModel* m, bool fullModel); /** normalize representative */ Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps, bool evalOnly); diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index e58c11aca..ffb537734 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -127,7 +127,7 @@ void TheoryUF::check(Effort level) { throw Exception( ss.str() ); } //needed for models - if( options::produceModels() && atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ){ + if( options::produceModels() && ( atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT || options::ufssMode()!=UF_SS_FULL ) ){ d_equalityEngine.assertPredicate(atom, polarity, fact); } } else { |