From 1bf5bc13506ba8c517925a50a6650a594d3ec42d Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 16 Apr 2015 11:21:07 +0200 Subject: [PATCH] Handle (degenerate) case of synthesis conjectures for constants. Disable delta lemmas. --- src/parser/smt2/Smt2.g | 11 +++- src/parser/smt2/smt2.cpp | 65 ++++++++++++------- .../quantifiers/ce_guided_instantiation.cpp | 6 +- .../quantifiers/ce_guided_single_inv.cpp | 3 + 4 files changed, 56 insertions(+), 29 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 8b7c0bda2..8dac9915e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -586,7 +586,10 @@ sygusCommand returns [CVC4::Command* cmd = NULL] ++i) { terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second)); } - Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, terms); + Expr bvl; + if( !terms.empty() ){ + bvl = MK_EXPR(kind::BOUND_VAR_LIST, terms); + } terms.clear(); terms.push_back(bvl); } @@ -633,8 +636,10 @@ sygusCommand returns [CVC4::Command* cmd = NULL] PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); std::vector evalType; evalType.push_back(dtt); - for(size_t j = 0; j < terms[0].getNumChildren(); ++j) { - evalType.push_back(terms[0][j].getType()); + if( !terms[0].isNull() ){ + for(size_t j = 0; j < terms[0].getNumChildren(); ++j) { + evalType.push_back(terms[0][j].getType()); + } } evalType.push_back(sorts[i]); Expr eval = PARSER_STATE->mkVar(name, EXPR_MANAGER->mkFunctionType(evalType)); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 20f3c364b..0c1b36655 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -489,26 +489,30 @@ void Smt2::includeFile(const std::string& filename) { ss << fun << "_v_" << j; sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), argTypes[j])); } - Type funt = getExprManager()->mkFunctionType(funType, rangeType); - Debug("parser-sygus") << "...eval function type : " << funt << std::endl; + Type funt; + if( !funType.empty() ){ + funt = getExprManager()->mkFunctionType(funType, rangeType); + Debug("parser-sygus") << "...eval function type : " << funt << std::endl; + + // copy the bound vars + /* + std::vector sygusVars; + //std::vector types; + for(size_t i = 0; i < d_sygusVars.size(); ++i) { + std::stringstream ss; + ss << d_sygusVars[i]; + Type type = d_sygusVars[i].getType(); + sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), type)); + //types.push_back(type); + } + Debug("parser-sygus") << "...made vars, #vars=" << sygusVars.size() << std::endl; + */ - // copy the bound vars - /* - std::vector sygusVars; - //std::vector types; - for(size_t i = 0; i < d_sygusVars.size(); ++i) { - std::stringstream ss; - ss << d_sygusVars[i]; - Type type = d_sygusVars[i].getType(); - sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), type)); - //types.push_back(type); + //Type t = getExprManager()->mkFunctionType(types, rangeType); + //Debug("parser-sygus") << "...function type : " << t << std::endl; + }else{ + funt = rangeType; } - Debug("parser-sygus") << "...made vars, #vars=" << sygusVars.size() << std::endl; - */ - - //Type t = getExprManager()->mkFunctionType(types, rangeType); - //Debug("parser-sygus") << "...function type : " << t << std::endl; - Expr lambda = mkFunction(fun, funt, ExprManager::VAR_FLAG_DEFINED); Debug("parser-sygus") << "...made function : " << lambda << std::endl; std::vector applyv; @@ -560,8 +564,13 @@ Expr Smt2::getSygusAssertion( std::vector& datatypeTypes, std::vec bvs.push_back(bv); extraArgs.push_back(bv); } - bvs.insert(bvs.end(), terms[0].begin(), terms[0].end()); - Expr bvl = getExprManager()->mkExpr(kind::BOUND_VAR_LIST, bvs); + if( !terms[0].isNull() ){ + bvs.insert(bvs.end(), terms[0].begin(), terms[0].end()); + } + Expr bvl; + if( !bvs.empty() ){ + bvl = getExprManager()->mkExpr(kind::BOUND_VAR_LIST, bvs); + } Debug("parser-sygus") << "...made bv list " << bvl << std::endl; std::vector patv; patv.push_back(eval); @@ -573,7 +582,9 @@ Expr Smt2::getSygusAssertion( std::vector& datatypeTypes, std::vec Expr cpatv = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, applyv); Debug("parser-sygus") << "...made eval ctor apply " << cpatv << std::endl; patv.push_back(cpatv); - patv.insert(patv.end(), terms[0].begin(), terms[0].end()); + if( !terms[0].isNull() ){ + patv.insert(patv.end(), terms[0].begin(), terms[0].end()); + } Expr evalApply = getExprManager()->mkExpr(kind::APPLY_UF, patv); Debug("parser-sygus") << "...made eval apply " << evalApply << std::endl; std::vector builtApply; @@ -581,7 +592,9 @@ Expr Smt2::getSygusAssertion( std::vector& datatypeTypes, std::vec std::vector patvb; patvb.push_back(evals[DatatypeType(extraArgs[k].getType())]); patvb.push_back(extraArgs[k]); - patvb.insert(patvb.end(), terms[0].begin(), terms[0].end()); + if( !terms[0].isNull() ){ + patvb.insert(patvb.end(), terms[0].begin(), terms[0].end()); + } builtApply.push_back(getExprManager()->mkExpr(kind::APPLY_UF, patvb)); } for(size_t k = 0; k < builtApply.size(); ++k) { @@ -599,9 +612,11 @@ Expr Smt2::getSygusAssertion( std::vector& datatypeTypes, std::vec } Debug("parser-sygus") << "...made built term " << builtTerm << std::endl; Expr assertion = getExprManager()->mkExpr(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm); - Expr pattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply); - pattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, pattern); - assertion = getExprManager()->mkExpr(kind::FORALL, bvl, assertion, pattern); + if( !bvl.isNull() ){ + Expr pattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply); + pattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, pattern); + assertion = getExprManager()->mkExpr(kind::FORALL, bvl, assertion, pattern); + } Debug("parser-sygus") << "...made assertion " << assertion << std::endl; //linearize multiplication if possible diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 7553eb736..ea97513b8 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -505,7 +505,11 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { } if( !(Trace.isOn("cegqi-stats")) ){ out << "(define-fun " << f << " "; - out << dt.getSygusVarList() << " "; + if( dt.getSygusVarList().isNull() ){ + out << "() "; + }else{ + out << dt.getSygusVarList() << " "; + } out << dt.getSygusType() << " "; if( status==0 ){ out << sol; diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index b3c1e1eaa..a612db872 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -637,6 +637,8 @@ Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std: //check if delta has a lower bound L // if so, add lemma L>0 => L>d void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) { + return; + /* disable for now if( !d_n_delta.isNull() ){ Theory* theory = d_qe->getTheoryEngine()->theoryOf( THEORY_ARITH ); if( theory && d_qe->getTheoryEngine()->isTheoryEnabled( THEORY_ARITH ) ){ @@ -701,6 +703,7 @@ void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) { } } } + */ } void CegInstantiator::check() { -- 2.30.2