From f07e8a3f06feb789692ede8ad9d25a2e049af769 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sun, 26 Apr 2015 19:26:21 +0200 Subject: Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullModel=false assigns values to eqc. Bug fix for fmf-fun. Minor change to resource limiting for quantifiers. Add fmf regressions. --- src/theory/quantifiers/first_order_model.cpp | 1 + src/theory/quantifiers/full_model_check.cpp | 18 +++++++--- src/theory/quantifiers/fun_def_process.cpp | 15 ++++---- src/theory/quantifiers/fun_def_process.h | 2 +- src/theory/quantifiers/inst_match.cpp | 11 ++++++ src/theory/quantifiers/inst_match.h | 1 + src/theory/quantifiers_engine.cpp | 53 ++++++++++++++++------------ src/theory/rep_set.cpp | 1 + src/theory/rep_set.h | 2 ++ src/theory/theory_model.cpp | 12 ++++--- 10 files changed, 77 insertions(+), 39 deletions(-) (limited to 'src') diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 50b04123c..5cb8cf278 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -703,6 +703,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] ); + c = getRepresentative( c ); children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) ); } } diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 5be263254..c0a734c35 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -593,7 +593,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, types.push_back(f[0][i].getType()); } TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() ); - Node op = NodeManager::currentNM()->mkSkolem( "fmc", typ, "op created for full-model checking" ); + Node op = NodeManager::currentNM()->mkSkolem( "qfmc", typ, "op created for full-model checking" ); d_quant_cond[f] = op; } //make sure all types are set @@ -847,6 +847,8 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n } else if( n.getType().isArray() ){ //make the definition + bool success = false; + /* Node r = fm->getRepresentative(n); Trace("fmc-debug") << "Representative for array is " << r << std::endl; while( r.getKind() == kind::STORE ){ @@ -867,10 +869,11 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n success = true; } } + */ if( !success ){ - Trace("fmc-warn") << "WARNING : ARRAYS : Can't process base array " << r << std::endl; - Trace("fmc-warn") << " Default value was : " << odefaultValue << std::endl; - Trace("fmc-debug") << "Can't process base array " << r << std::endl; + //Trace("fmc-warn") << "WARNING : ARRAYS : Can't process base array " << r << std::endl; + //Trace("fmc-warn") << " Default value was : " << odefaultValue << std::endl; + //Trace("fmc-debug") << "Can't process base array " << r << std::endl; //can't process this array d.reset(); d.addEntry(fm, mkCondDefault(fm, f), Node::null()); @@ -1133,6 +1136,12 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, void FullModelChecker::doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n, std::vector< Def > & dc, int index, std::vector< Node > & cond, std::vector & val ) { + Trace("fmc-if-process") << "int compose " << index << " / " << dc.size() << std::endl; + for( unsigned i=1; igetStarElement( f[0][i].getType() ); + Assert( ts.getType()==f[0][i].getType() ); cond.push_back(ts); } } diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index cb379ec92..22dac2225 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -31,6 +31,7 @@ using namespace CVC4::kind; void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { std::vector< int > fd_assertions; + std::map< int, Node > subs_head; //first pass : find defined functions, transform quantifiers for( unsigned i=0; i& assertions, bool doRewrite ) { subs.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, d_input_arg_inj[f][j], bv ) ); } bd = bd.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + subs_head[i] = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << std::endl; + Trace("fmf-fun-def") << "FMF fun def: FUNCTION : rewrite " << assertions[i] << std::endl; Trace("fmf-fun-def") << " to " << std::endl; Node new_q = NodeManager::currentNM()->mkNode( FORALL, bvl, bd ); new_q = Rewriter::rewrite( new_q ); @@ -91,7 +93,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { if( is_fd==0 || ( is_fd==1 && ( assertions[i][1].getKind()==EQUAL || assertions[i][1].getKind()==IFF ) ) ){ std::vector< Node > constraints; Trace("fmf-fun-def-rewrite") << "Rewriting " << assertions[i] << ", is_fd = " << is_fd << std::endl; - Node n = simplify( assertions[i], true, true, constraints, is_fd ); + Node n = simplifyFormula( assertions[i], true, true, constraints, is_fd==1 ? subs_head[i] : Node::null(), is_fd ); Assert( constraints.empty() ); if( n!=assertions[i] ){ n = Rewriter::rewrite( n ); @@ -105,10 +107,11 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { } } -Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, int is_fun_def ) { +//is_fun_def 1 : top of fun-def, 2 : top of fun-def body, 0 : not top +Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, int is_fun_def ) { Trace("fmf-fun-def-debug") << "Simplify " << n << " " << pol << " " << hasPol << " " << is_fun_def << std::endl; if( n.getKind()==FORALL ){ - Node c = simplify( n[1], pol, hasPol, constraints, is_fun_def ); + Node c = simplifyFormula( n[1], pol, hasPol, constraints, hd, is_fun_def ); if( c!=n[1] ){ return NodeManager::currentNM()->mkNode( FORALL, n[0], c ); }else{ @@ -123,13 +126,13 @@ Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& co for( unsigned i=0; i cconstraints; - c = simplify( n[i], newPol, newHasPol, cconstraints, is_fun_def==1 ? 2 : 0 ); + c = simplifyFormula( n[i], newPol, newHasPol, cconstraints, hd, is_fun_def==1 ? 2 : 0 ); constraints.insert( constraints.end(), cconstraints.begin(), cconstraints.end() ); } children.push_back( c ); diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h index 63aa1bf94..54735d4d6 100644 --- a/src/theory/quantifiers/fun_def_process.h +++ b/src/theory/quantifiers/fun_def_process.h @@ -36,7 +36,7 @@ private: //defined functions to injections input -> argument elements std::map< Node, std::vector< Node > > d_input_arg_inj; //simplify - Node simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, int is_fun_def = 0 ); + Node simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, int is_fun_def = 0 ); //simplify term void simplifyTerm( Node n, std::vector< Node >& constraints ); public: diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 078614509..cb969088d 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -127,6 +127,17 @@ Node InstMatch::get( int i ) { return d_vals[i]; } +void InstMatch::getTerms( QuantifiersEngine* qe, Node f, std::vector< Node >& inst ){ + for( size_t i=0; igetTermDatabase()->getInstantiationConstant( f, i ); + val = qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); + } + inst.push_back( val ); + } +} + void InstMatch::setValue( int i, TNode n ) { d_vals[i] = n; } diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 8753c0bb1..21220491f 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -78,6 +78,7 @@ public: void applyRewrite(); /** get */ Node get( int i ); + void getTerms( QuantifiersEngine* qe, Node f, std::vector< Node >& inst ); /** set */ void setValue( int i, TNode n ); bool set( QuantifiersEngine* qe, int i, TNode n ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 8dec3898c..3fa3b2a1b 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -748,24 +748,15 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){ } bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool modEq, bool modInst ){ - // For resource-limiting (also does a time check). - getOutputChannel().safePoint(); - std::vector< Node > terms; - //make sure there are values for each variable we are instantiating - for( size_t i=0; igetInstantiationConstant( f, i ); - val = d_term_db->getFreeVariableForInstConstant( ic ); - Trace("inst-add-debug") << "mkComplete " << val << std::endl; - } - terms.push_back( val ); - } + m.getTerms( this, f, terms ); return addInstantiation( f, terms, mkRep, modEq, modInst ); } bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst ) { + // For resource-limiting (also does a time check). + getOutputChannel().safePoint(); + Assert( terms.size()==f[0].getNumChildren() ); Trace("inst-add-debug") << "Add instantiation: "; for( unsigned i=0; i::iterator it = typ_num.begin(); it != typ_num.end(); ++it ){ - Trace(c) << "# eqc for " << it->first << " : " << it->second << std::endl; + Trace(c) << "# eqc for " << it->first << " : " << it->second << std::endl; } } @@ -1075,6 +1066,23 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, if( !options::internalReps() ){ return r; }else{ + if( options::finiteModelFind() ){ + if( r.isConst() ){ + //map back from values assigned by model, if any + if( d_qe->getModel() ){ + std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r ); + if( it!=d_qe->getModel()->d_rep_set.d_values_to_terms.end() ){ + r = it->second; + r = getRepresentative( r ); + }else{ + if( r.getType().isSort() ){ + Trace("internal-rep-warn") << "No representative for UF constant." << std::endl; + } + } + } + } + } + if( d_int_rep.find( r )==d_int_rep.end() ){ //find best selection for representative Node r_best; @@ -1093,9 +1101,8 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, Trace("internal-rep-select") << " } " << std::endl; int r_best_score = -1; for( size_t i=0; i=0 && ( r_best_score<0 || scoregetTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){ + if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){ + return -2; + }else if( options::lteRestrictInstClosure() && ( !d_qe->getTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){ return -1; }else if( options::instMaxLevel()!=-1 ){ //score prefer lowest instantiation level if( n.hasAttribute(InstLevelAttribute()) ){ - s = n.getAttribute(InstLevelAttribute()); + return n.getAttribute(InstLevelAttribute()); }else{ - s = options::instLevelInputOnly() ? -1 : 0; + return options::instLevelInputOnly() ? -1 : 0; } }else{ //score prefers earliest use of this term as a representative - s = d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n]; + return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n]; } - return s; //return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n ); //term depth } diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index db0524034..5580dc3d7 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -26,6 +26,7 @@ void RepSet::clear(){ d_type_reps.clear(); d_type_complete.clear(); d_tmap.clear(); + d_values_to_terms.clear(); } bool RepSet::hasRep( TypeNode tn, Node n ) { diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index 19bb6d3d3..4aab230e6 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -33,6 +33,8 @@ public: std::map< TypeNode, std::vector< Node > > d_type_reps; std::map< TypeNode, bool > d_type_complete; std::map< Node, int > d_tmap; + // map from values to terms they were assigned for + std::map< Node, Node > d_values_to_terms; /** clear the set */ void clear(); /** has type */ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 072f579be..52b018234 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -198,7 +198,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const } if (!d_equalityEngine->hasTerm(n)) { - if(n.getType().isRegExp()) { + if(n.getType().isRegExp()) { ret = Rewriter::rewrite(ret); } else { // Unknown term - return first enumerated value for this type @@ -666,7 +666,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) } } while (changed); - if (!fullModel || !unassignedAssignable) { + if (!unassignedAssignable) { break; } @@ -675,9 +675,8 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) // different are different. // Only make assignments on a type if: - // 1. fullModel is true - // 2. there are no terms that share the same base type with un-normalized representatives - // 3. there are no terms that share teh same base type that are unevaluated evaluable terms + // 1. there are no terms that share the same base type with un-normalized representatives + // 2. there are no terms that share teh same base type that are unevaluated evaluable terms // Alternatively, if 2 or 3 don't hold but we are in a special deadlock-breaking mode where assignOne is true, go ahead and make one assignment changed = false; for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) { @@ -730,6 +729,9 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) Assert(!n.isNull()); constantReps[*i2] = n; Trace("model-builder") << " Assign: Setting constant rep of " << (*i2) << " to " << n << endl; + if( !fullModel ){ + tm->d_rep_set.d_values_to_terms[n] = (*i2); + } changed = true; noRepSet.erase(i2); if (assignOne) { -- cgit v1.2.3