From 21ac21a2ff3ba3eeac4deabf0c4b79ca4cc8df77 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 24 Apr 2017 16:56:23 -0500 Subject: [PATCH] Fixes and simplifications for fmf mbqi. --- src/theory/quantifiers/ambqi_builder.cpp | 7 +- src/theory/quantifiers/first_order_model.cpp | 19 +----- src/theory/quantifiers/first_order_model.h | 3 +- src/theory/quantifiers/full_model_check.cpp | 34 ++++------ src/theory/quantifiers/model_builder.cpp | 69 ++++++++------------ src/theory/quantifiers/model_builder.h | 2 - test/regress/regress0/fmf/Makefile.am | 3 +- test/regress/regress0/fmf/alg202+1.smt2 | 17 +++++ 8 files changed, 67 insertions(+), 87 deletions(-) create mode 100644 test/regress/regress0/fmf/alg202+1.smt2 diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index de55ecdba..bc638080f 100644 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -774,10 +774,9 @@ bool AbsMbqiBuilder::processBuildModel(TheoryModel* m) { if( itut!=fm->d_uf_terms.end() ){ for( size_t i=0; isecond.size(); i++ ){ Node n = itut->second[i]; - if( d_qe->getTermDatabase()->isTermActive( n ) ){ - Trace("ambqi-model-debug") << " " << n << " -> " << fm->getRepresentativeId( n ) << std::endl; - fapps.push_back( n ); - } + // only consider unique up to congruence (in model equality engine)? + Trace("ambqi-model-debug") << " " << n << " -> " << fm->getRepresentativeId( n ) << std::endl; + fapps.push_back( n ); } } if( fapps.empty() ){ diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 16fc4d4b8..084912f5a 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -615,23 +615,6 @@ FirstOrderModelFmc::~FirstOrderModelFmc() throw() { } } -Node FirstOrderModelFmc::getUsedRepresentative(Node n, bool strict) { - //Assert( fm->hasTerm(n) ); - TypeNode tn = n.getType(); - if( tn.isBoolean() ){ - return areEqual(n, d_true) ? d_true : d_false; - }else{ - if( !hasTerm(n) ){ - if( strict ){ - return Node::null(); - }else{ - Trace("fmc-warn") << "WARNING : no representative for " << n << std::endl; - } - } - return getRepresentative(n); - } -} - /* Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) { Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl; @@ -753,7 +736,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { } }else if ( !isStar(cond[j]) && //handle the case where there are 0 or 1 ground eqc of this type d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && d_rep_set.d_type_reps[ tn ].size()>1 ){ - Node c = getUsedRepresentative( cond[j] ); + Node c = getRepresentative( cond[j] ); c = getRepresentative( c ); children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) ); } diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 05771d1a2..e4adfc8bd 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -167,7 +167,6 @@ private: std::map d_models; std::map d_type_star; Node intervalOp; - Node getUsedRepresentative(Node n, bool strict = false); /** get current model value */ void processInitializeModelForTerm(Node n); public: @@ -206,13 +205,13 @@ private: void processInitializeModelForTerm(Node n); void processInitializeQuantifier( Node q ); void collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars ); + TNode getUsedRepresentative( TNode n ); public: FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name); ~FirstOrderModelAbs() throw(); FirstOrderModelAbs * asFirstOrderModelAbs() { return this; } void processInitialize( bool ispre ); unsigned getRepresentativeId( TNode n ); - TNode getUsedRepresentative( TNode n ); bool isValidType( TypeNode tn ) { return d_domain.find( tn )!=d_domain.end(); } Node getFunctionValue(Node op, const char* argPrefix ); Node getVariable( Node q, unsigned i ); diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 259083e6e..c41d09187 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -379,7 +379,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ if( it->first.isSort() ){ Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; for( size_t a=0; asecond.size(); a++ ){ - Node r = fm->getUsedRepresentative( it->second[a] ); + Node r = fm->getRepresentative( it->second[a] ); if( Trace.isOn("fmc-model-debug") ){ std::vector< Node > eqc; ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc ); @@ -412,18 +412,12 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ Trace("fmc-model-debug") << itut->second.size() << " model values for " << op << " ... " << std::endl; for( size_t i=0; isecond.size(); i++ ){ Node n = itut->second[i]; - if( d_qe->getTermDatabase()->isTermActive( n ) ){ - add_conds.push_back( n ); - add_values.push_back( n ); - Node r = fm->getUsedRepresentative(n); - Trace("fmc-model-debug") << n << " -> " << r << std::endl; - //AlwaysAssert( fm->areEqual( itut->second[i], r ) ); - }else{ - if( Trace.isOn("fmc-model-debug") ){ - Node r = fm->getUsedRepresentative(n); - Trace("fmc-model-debug") << "[redundant] " << n << " -> " << r << std::endl; - } - } + // only consider unique up to congruence (in model equality engine)? + add_conds.push_back( n ); + add_values.push_back( n ); + Node r = fm->getRepresentative(n); + Trace("fmc-model-debug") << n << " -> " << r << std::endl; + //AlwaysAssert( fm->areEqual( itut->second[i], r ) ); } }else{ Trace("fmc-model-debug") << "No model values for " << op << " ... " << std::endl; @@ -449,7 +443,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ std::vector< Node > conds; std::vector< Node > values; std::vector< Node > entry_conds; - //get the entries for the mdoel + //get the entries for the model for( size_t i=0; igetUsedRepresentative( c[i] ); + Node ri = fm->getRepresentative( c[i] ); children.push_back(ri); bool isStar = false; if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){ @@ -477,7 +471,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ entry_children.push_back(ri); } Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children ); - Node nv = fm->getUsedRepresentative( v ); + Node nv = fm->getRepresentative( v ); if( !nv.isConst() ){ Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl; Assert( false ); @@ -529,7 +523,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ for( size_t i=0; id_uf_terms[op].size(); i++ ){ std::vector< Node > inst; for( unsigned j=0; jd_uf_terms[op][i].getNumChildren(); j++ ){ - Node r = fm->getUsedRepresentative( fm->d_uf_terms[op][i][j] ); + Node r = fm->getRepresentative( fm->d_uf_terms[op][i][j] ); inst.push_back( r ); } Node ev = fm->d_models[op]->evaluate( fm, inst ); @@ -784,7 +778,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No Node rr = riter.getCurrentTerm( i ); Node r = rr; //if( r.getType().isSort() ){ - r = fm->getUsedRepresentative( r ); + r = fm->getRepresentative( r ); //}else{ // r = fm->getCurrentModelValue( r ); //} @@ -862,7 +856,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n if( !fm->hasTerm(n) ){ r = getSomeDomainElement(fm, n.getType() ); } - r = fm->getUsedRepresentative( r ); + r = fm->getRepresentative( r ); } Trace("fmc-debug") << "Add constant entry..." << std::endl; d.addEntry(fm, mkCondDefault(fm, f), r); @@ -948,7 +942,7 @@ void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def getSomeDomainElement( fm, tn ); //to verify the type is initialized } for (unsigned i=0; id_rep_set.d_type_reps[tn].size(); i++) { - Node r = fm->getUsedRepresentative( fm->d_rep_set.d_type_reps[tn][i] ); + Node r = fm->getRepresentative( fm->d_rep_set.d_type_reps[tn][i] ); cond[j+1] = r; cond[k+1] = r; d.addEntry( fm, mkCond(cond), d_true); diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 7f342c633..055c9e31c 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -334,22 +334,19 @@ void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){ for( size_t i=0; isecond.size(); i++ ){ Node n = fmig->d_uf_terms[op][i]; //for calculating if op is constant - if( d_qe->getTermDatabase()->isTermActive( n ) ){ - Node v = fmig->getRepresentative( n ); - if( i==0 ){ - d_uf_prefs[op].d_const_val = v; - }else if( v!=d_uf_prefs[op].d_const_val ){ - d_uf_prefs[op].d_const_val = Node::null(); - break; - } + Node v = fmig->getRepresentative( n ); + if( i==0 ){ + d_uf_prefs[op].d_const_val = v; + }else if( v!=d_uf_prefs[op].d_const_val ){ + d_uf_prefs[op].d_const_val = Node::null(); + break; } //for calculating terms that we don't need to consider - if( d_qe->getTermDatabase()->isTermActive( n ) || n.getAttribute(ModelBasisArgAttribute())!=0 ){ - if( d_basisNoMatch.find( n )==d_basisNoMatch.end() ){ - //need to consider if it is not congruent modulo model basis - if( !tabt.addTerm( fmig, n ) ){ - d_basisNoMatch[n] = true; - } + //if( d_qe->getTermDatabase()->isTermActive( n ) || n.getAttribute(ModelBasisArgAttribute())!=0 ){ + if( d_basisNoMatch.find( n )==d_basisNoMatch.end() ){ + //need to consider if it is not congruent modulo model basis + if( !tabt.addTerm( fmig, n ) ){ + d_basisNoMatch[n] = true; } } } @@ -409,13 +406,6 @@ QModelBuilderIG::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_eval_lits_unknown); } -bool QModelBuilderIG::isTermActive( Node n ){ - return d_qe->getTermDatabase()->isTermActive( n ) || //it is not congruent to another active term - ( n.getAttribute(ModelBasisArgAttribute())!=0 && d_basisNoMatch.find( n )==d_basisNoMatch.end() ); //or it has model basis arguments - //and is not congruent modulo model basis - //to another active term -} - //do exhaustive instantiation int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { if( optUseModel() ){ @@ -739,30 +729,29 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ if( itut!=fmig->d_uf_terms.end() ){ for( size_t i=0; isecond.size(); i++ ){ Node n = itut->second[i]; - if( isTermActive( n ) ){ - Node v = fmig->getRepresentative( n ); - Trace("fmf-model-cons") << "Set term " << n << " : " << fmig->d_rep_set.getIndexFor( v ) << " " << v << std::endl; - //if this assertion did not help the model, just consider it ground - //set n = v in the model tree - //set it as ground value - fmig->d_uf_model_gen[op].setValue( fm, n, v ); - if( fmig->d_uf_model_gen[op].optUsePartialDefaults() ){ - //also set as default value if necessary - if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())!=0 ){ - Trace("fmf-model-cons") << " Set as default." << std::endl; - fmig->d_uf_model_gen[op].setValue( fm, n, v, false ); - if( n==defaultTerm ){ - //incidentally already set, we will not need to find a default value - setDefaultVal = false; - } - } - }else{ + // only consider unique up to congruence (in model equality engine)? + Node v = fmig->getRepresentative( n ); + Trace("fmf-model-cons") << "Set term " << n << " : " << fmig->d_rep_set.getIndexFor( v ) << " " << v << std::endl; + //if this assertion did not help the model, just consider it ground + //set n = v in the model tree + //set it as ground value + fmig->d_uf_model_gen[op].setValue( fm, n, v ); + if( fmig->d_uf_model_gen[op].optUsePartialDefaults() ){ + //also set as default value if necessary + if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())!=0 ){ + Trace("fmf-model-cons") << " Set as default." << std::endl; + fmig->d_uf_model_gen[op].setValue( fm, n, v, false ); if( n==defaultTerm ){ - fmig->d_uf_model_gen[op].setValue( fm, n, v, false ); //incidentally already set, we will not need to find a default value setDefaultVal = false; } } + }else{ + if( n==defaultTerm ){ + fmig->d_uf_model_gen[op].setValue( fm, n, v, false ); + //incidentally already set, we will not need to find a default value + setDefaultVal = false; + } } } } diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index eedd850d6..3f548c9fd 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -131,8 +131,6 @@ public: ~Statistics(); }; Statistics d_statistics; - // is term active - bool isTermActive( Node n ); // is term selected virtual bool isTermSelected( Node n ) { return false; } /** quantifier has inst-gen definition */ diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 0c13961cc..a91499a6c 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -71,7 +71,8 @@ TESTS = \ bug782.smt2 \ quant_real_univ.cvc \ constr-ground-to.smt2 \ - bug-041417-set-options.cvc + bug-041417-set-options.cvc \ + alg202+1.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/alg202+1.smt2 b/test/regress/regress0/fmf/alg202+1.smt2 new file mode 100644 index 000000000..ff3460636 --- /dev/null +++ b/test/regress/regress0/fmf/alg202+1.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: unsat +(set-logic ALL) +(declare-sort $$unsorted 0) +(declare-fun sorti1 ($$unsorted) Bool) +(declare-fun op1 ($$unsorted $$unsorted) $$unsorted) +(declare-fun sorti2 ($$unsorted) Bool) +(declare-fun op2 ($$unsorted $$unsorted) $$unsorted) +(declare-fun h ($$unsorted) $$unsorted) +(declare-fun j ($$unsorted) $$unsorted) +(assert (forall ((U $$unsorted) (BOUND_VARIABLE_345 $$unsorted)) (or (not (sorti1 U)) (not (sorti1 BOUND_VARIABLE_345)) (sorti1 (op1 U BOUND_VARIABLE_345))) )) +(assert (forall ((U $$unsorted) (BOUND_VARIABLE_364 $$unsorted)) (or (not (sorti2 U)) (not (sorti2 BOUND_VARIABLE_364)) (sorti2 (op2 U BOUND_VARIABLE_364))) )) +(assert (forall ((U $$unsorted)) (or (not (sorti1 U)) (= U (op1 U U))) )) +(assert (not (forall ((U $$unsorted)) (or (not (sorti2 U)) (= U (op2 U U))) ))) +(assert (not (=> (and (forall ((U $$unsorted)) (or (not (sorti1 U)) (sorti2 (h U))) ) (forall ((V $$unsorted)) (or (not (sorti2 V)) (sorti1 (j V))) )) (not (and (forall ((W $$unsorted) (BOUND_VARIABLE_406 $$unsorted)) (or (not (sorti1 W)) (not (sorti1 BOUND_VARIABLE_406)) (= (op2 (h W) (h BOUND_VARIABLE_406)) (h (op1 W BOUND_VARIABLE_406)))) ) (forall ((Y $$unsorted) (BOUND_VARIABLE_431 $$unsorted)) (or (not (sorti2 Y)) (not (sorti2 BOUND_VARIABLE_431)) (= (op1 (j Y) (j BOUND_VARIABLE_431)) (j (op2 Y BOUND_VARIABLE_431)))) ) (forall ((X1 $$unsorted)) (or (not (sorti2 X1)) (= X1 (h (j X1)))) ) (forall ((X2 $$unsorted)) (or (not (sorti1 X2)) (= X2 (j (h X2)))) )))))) +(assert (and (forall ((U $$unsorted)) (or (not (sorti1 U)) (sorti2 (h U))) ) (forall ((V $$unsorted)) (or (not (sorti2 V)) (sorti1 (j V))) ) (forall ((W $$unsorted) (BOUND_VARIABLE_406 $$unsorted)) (or (not (sorti1 W)) (not (sorti1 BOUND_VARIABLE_406)) (= (op2 (h W) (h BOUND_VARIABLE_406)) (h (op1 W BOUND_VARIABLE_406)))) ) (forall ((Y $$unsorted) (BOUND_VARIABLE_431 $$unsorted)) (or (not (sorti2 Y)) (not (sorti2 BOUND_VARIABLE_431)) (= (op1 (j Y) (j BOUND_VARIABLE_431)) (j (op2 Y BOUND_VARIABLE_431)))) ) (forall ((X1 $$unsorted)) (or (not (sorti2 X1)) (= X1 (h (j X1)))) ) (forall ((X2 $$unsorted)) (or (not (sorti1 X2)) (= X2 (j (h X2)))) ))) +(check-sat) -- 2.30.2