From: ajreynol Date: Fri, 24 Apr 2015 12:41:28 +0000 (+0200) Subject: More parser related bug fixes (define-funs-rec, declare-funs). Bug fix for fmf mbqi... X-Git-Tag: cvc5-1.0.0~6341 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=349deb0522c4602b740d96f6a688b644dd84c64f;p=cvc5.git More parser related bug fixes (define-funs-rec, declare-funs). Bug fix for fmf mbqi=gen-ev for interpreted operators. --- diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index d2e83702f..c7c82b2d8 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -912,7 +912,8 @@ smt25Command[CVC4::Command*& cmd] } t = EXPR_MANAGER->mkFunctionType(sorts, t); } - Expr func = PARSER_STATE->mkVar(fname, t, ExprManager::VAR_FLAG_DEFINED); + Expr func = PARSER_STATE->mkVar(fname, t); + static_cast($cmd)->addCommand(new DeclareFunctionCommand(fname, func, t)); std::vector< Expr > f_app; f_app.push_back( func ); PARSER_STATE->pushScope(true); @@ -958,7 +959,8 @@ smt25Command[CVC4::Command*& cmd] t = EXPR_MANAGER->mkFunctionType(sorts, t); } sortedVarNames.clear(); - Expr func = PARSER_STATE->mkVar(fname, t, ExprManager::VAR_FLAG_DEFINED); + Expr func = PARSER_STATE->mkVar(fname, t); + static_cast($cmd)->addCommand(new DeclareFunctionCommand(fname, func, t)); funcs.push_back( func ); } RPAREN_TOK @@ -1079,6 +1081,7 @@ extendedCommand[CVC4::Command*& cmd] } Expr func = PARSER_STATE->mkVar(name, t); static_cast($cmd)->addCommand(new DeclareFunctionCommand(name, func, t)); + sorts.clear(); } )+ RPAREN_TOK @@ -1098,6 +1101,7 @@ extendedCommand[CVC4::Command*& cmd] } Expr func = PARSER_STATE->mkVar(name, t); static_cast($cmd)->addCommand(new DeclareFunctionCommand(name, func, t)); + sorts.clear(); } )+ RPAREN_TOK diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 88464bb9a..50b04123c 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -169,10 +169,10 @@ void FirstOrderModelIG::processInitializeModelForTerm( Node n ){ TypeNode tn = op.getType(); tn = tn[ (int)tn.getNumChildren()-1 ]; //only generate models for predicates and functions with uninterpreted range types - if( tn==NodeManager::currentNM()->booleanType() || tn.isSort() ){ + //if( tn==NodeManager::currentNM()->booleanType() || tn.isSort() ){ d_uf_model_tree[ op ] = uf::UfModelTree( op ); d_uf_model_gen[ op ].clear(); - } + //} } } /* @@ -355,42 +355,9 @@ Node FirstOrderModelIG::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri } }else{ std::vector< int > children_depIndex; - //for select, pre-process read over writes - if( n.getKind()==SELECT ){ -#if 0 - //std::cout << "Evaluate " << n << std::endl; - Node sel = evaluateTerm( n[1], depIndex, ri ); - if( sel.isNull() ){ - depIndex = ri->getNumTerms()-1; - return Node::null(); - } - Node arr = getRepresentative( n[0] ); - //if( n[0]!=getRepresentative( n[0] ) ){ - // std::cout << n[0] << " is " << getRepresentative( n[0] ) << std::endl; - //} - int tempIndex; - int eval = 1; - while( arr.getKind()==STORE && eval!=0 ){ - eval = evaluate( sel.eqNode( arr[1] ), tempIndex, ri ); - depIndex = tempIndex > depIndex ? tempIndex : depIndex; - if( eval==1 ){ - val = evaluateTerm( arr[2], tempIndex, ri ); - depIndex = tempIndex > depIndex ? tempIndex : depIndex; - return val; - }else if( eval==-1 ){ - arr = arr[0]; - } - } - arr = evaluateTerm( arr, tempIndex, ri ); - depIndex = tempIndex > depIndex ? tempIndex : depIndex; - val = NodeManager::currentNM()->mkNode( SELECT, arr, sel ); -#else - val = evaluateTermDefault( n, depIndex, children_depIndex, ri ); -#endif - }else{ - //default term evaluate : evaluate all children, recreate the value - val = evaluateTermDefault( n, depIndex, children_depIndex, ri ); - } + //default term evaluate : evaluate all children, recreate the value + val = evaluateTermDefault( n, depIndex, children_depIndex, ri ); + Trace("fmf-eval-debug") << "Evaluate term, value from " << n << " is " << val << std::endl; if( !val.isNull() ){ bool setVal = false; //custom ways of evaluating terms @@ -405,8 +372,10 @@ Node FirstOrderModelIG::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri makeEvalUfModel( n ); //now, consult the model if( d_eval_uf_use_default[n] ){ + Trace("fmf-eval-debug") << "get default" << std::endl; val = d_uf_model_tree[ op ].getValue( this, val, argDepIndex ); }else{ + Trace("fmf-eval-debug") << "get uf model" << std::endl; val = d_eval_uf_model[ n ].getValue( this, val, argDepIndex ); } //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl; @@ -422,22 +391,20 @@ Node FirstOrderModelIG::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri } } setVal = true; + }else{ + Trace("fmf-eval-debug") << "No model." << std::endl; } - }else if( n.getKind()==SELECT ){ - //we are free to interpret this term however we want } //if not set already, rewrite and consult model for interpretation if( !setVal ){ val = Rewriter::rewrite( val ); - if( val.getMetaKind()!=kind::metakind::CONSTANT ){ - //FIXME: we cannot do this until we trust all theories collectModelInfo! - //val = getInterpretedValue( val ); - //val = getRepresentative( val ); + if( !val.isConst() ){ + return Node::null(); } } Trace("fmf-eval-debug") << "Evaluate term " << n << " = "; printRepresentativeDebug( "fmf-eval-debug", val ); - Trace("fmf-eval-debug") << ", depIndex = " << depIndex << std::endl; + Trace("fmf-eval-debug") << " (term " << val << "), depIndex = " << depIndex << std::endl; } } return val; @@ -448,6 +415,7 @@ Node FirstOrderModelIG::evaluateTermDefault( Node n, int& depIndex, std::vector< if( n.getNumChildren()==0 ){ return n; }else{ + bool isInterp = n.getKind()!=APPLY_UF; //first we must evaluate the arguments std::vector< Node > children; if( n.getMetaKind()==kind::metakind::PARAMETERIZED ){ @@ -461,10 +429,15 @@ Node FirstOrderModelIG::evaluateTermDefault( Node n, int& depIndex, std::vector< depIndex = ri->getNumTerms()-1; return nn; }else{ - children.push_back( nn ); if( childDepIndex[i]>depIndex ){ depIndex = childDepIndex[i]; } + if( isInterp ){ + if( !nn.isConst() ) { + nn = getRepresentative( nn ); + } + } + children.push_back( nn ); } } //recreate the value diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 591034ffc..6e73b37a7 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -77,7 +77,7 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ Trace("model-engine-debug") << "Check model..." << std::endl; d_incomplete_check = false; //print debug - Debug("fmf-model-complete") << std::endl; + Trace("fmf-model-complete") << std::endl; debugPrint("fmf-model-complete"); //successfully built an acceptable model, now check it addedLemmas += checkModel(); diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 9003ef636..6bd6280ae 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -67,7 +67,8 @@ SMT2_TESTS = \ hung13sdk_output1.smt2 \ hung10_itesdk_output2.smt2 \ hung10_itesdk_output1.smt2 \ - hung13sdk_output2.smt2 + hung13sdk_output2.smt2 \ + declare-funs.smt2 # Regression tests for PL inputs CVC_TESTS = \ diff --git a/test/regress/regress0/declare-funs.smt2 b/test/regress/regress0/declare-funs.smt2 new file mode 100644 index 000000000..9cbbd8f73 --- /dev/null +++ b/test/regress/regress0/declare-funs.smt2 @@ -0,0 +1,5 @@ +(set-logic QF_LIA) +(set-info :status sat) +(declare-funs ((f Int) (g Int))) +(assert (= f g)) +(check-sat) \ No newline at end of file