From 1d0b1ab30c627ead567b6d0eea200a1dc5b61df5 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 16 Jan 2015 17:17:56 +0100 Subject: [PATCH] Linearize multiplication by constants in sygus grammars. Handle unary minus integer numerals. Refactor to smt2.cpp. --- src/parser/smt2/Smt2.g | 95 +++++++-------------- src/parser/smt2/smt2.cpp | 177 +++++++++++++++++++++++++++++++++++++++ src/parser/smt2/smt2.h | 66 ++------------- 3 files changed, 216 insertions(+), 122 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 3f999366d..a2e4d25f9 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -638,54 +638,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] Expr eval = evals[dtt]; Debug("parser-sygus") << "Sygus : process grammar : " << dt << std::endl; for(size_t j = 0; j < dt.getNumConstructors(); ++j) { - const DatatypeConstructor& ctor = dt[j]; - Debug("parser-sygus") << "Sygus : process constructor " << j << " : " << dt[j] << std::endl; - std::vector bvs, extraArgs; - for(size_t k = 0; k < ctor.getNumArgs(); ++k) { - std::string vname = "v_" + ctor[k].getName(); - Expr bv = EXPR_MANAGER->mkBoundVar(vname, SelectorType(ctor[k].getType()).getRangeType()); - bvs.push_back(bv); - extraArgs.push_back(bv); - } - bvs.insert(bvs.end(), terms[0].begin(), terms[0].end()); - Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, bvs); - Debug("parser-sygus") << "...made bv list." << std::endl; - std::vector patv; - patv.push_back(eval); - std::vector applyv; - applyv.push_back(ctor.getConstructor()); - applyv.insert(applyv.end(), extraArgs.begin(), extraArgs.end()); - for(size_t k = 0; k < applyv.size(); ++k) { - } - Expr cpatv = MK_EXPR(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()); - Expr evalApply = MK_EXPR(kind::APPLY_UF, patv); - Debug("parser-sygus") << "...made eval apply " << evalApply << std::endl; - std::vector builtApply; - for(size_t k = 0; k < extraArgs.size(); ++k) { - patv.clear(); - patv.push_back(evals[DatatypeType(extraArgs[k].getType())]); - patv.push_back(extraArgs[k]); - patv.insert(patv.end(), terms[0].begin(), terms[0].end()); - builtApply.push_back(MK_EXPR(kind::APPLY_UF, patv)); - } - for(size_t k = 0; k < builtApply.size(); ++k) { - } - Expr builtTerm; - //if( ops[i][j].getKind() == kind::BUILTIN ){ - if( !builtApply.empty() ){ - builtTerm = MK_EXPR(ops[i][j], builtApply); - }else{ - builtTerm = ops[i][j]; - } - Debug("parser-sygus") << "...made built term " << builtTerm << std::endl; - Expr assertion = MK_EXPR(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm); - Expr pattern = MK_EXPR(kind::INST_PATTERN, evalApply); - pattern = MK_EXPR(kind::INST_PATTERN_LIST, pattern); - assertion = MK_EXPR(kind::FORALL, bvl, assertion, pattern); - Debug("parser-sygus") << "Add assertion " << assertion << std::endl; + Expr assertion = PARSER_STATE->getSygusAssertion( datatypeTypes, ops, evals, terms, eval, dt, i, j ); seq->addCommand(new AssertCommand(assertion)); } } @@ -746,7 +699,7 @@ sygusGTerm[CVC4::Datatype& dt, std::vector& ops] ( builtinOp[k] { ops.push_back(EXPR_MANAGER->operatorOf(k)); name = kind::kindToString(k); - Debug("parser-sygus") << "Sygus : grammar builtin symbol : " << name << std::endl; + Debug("parser-sygus") << "Sygus grammar : builtin op : " << name << std::endl; } | symbol[name,CHECK_NONE,SYM_VARIABLE] { // what is this sygus term trying to accomplish here, if the @@ -754,7 +707,7 @@ sygusGTerm[CVC4::Datatype& dt, std::vector& ops] // fail, but we need an operator to continue here.. Expr bv = PARSER_STATE->getVariable(name); ops.push_back(bv); - Debug("parser-sygus") << "Sygus : grammar symbol : " << name << std::endl; + Debug("parser-sygus") << "Sygus grammar : op : " << name << std::endl; } ) { name = dt.getName() + "_" + name; @@ -771,7 +724,8 @@ sygusGTerm[CVC4::Datatype& dt, std::vector& ops] { dt.addConstructor(*ctor); delete ctor; } | INTEGER_LITERAL - { ops.push_back(MK_CONST(Rational(AntlrInput::tokenText($INTEGER_LITERAL)))); + { Debug("parser-sygus") << "Sygus grammar : integer literal " << AntlrInput::tokenText($INTEGER_LITERAL) << std::endl; + ops.push_back(MK_CONST(Rational(AntlrInput::tokenText($INTEGER_LITERAL)))); name = dt.getName() + "_" + AntlrInput::tokenText($INTEGER_LITERAL); std::string testerId("is-"); testerId.append(name); @@ -781,7 +735,8 @@ sygusGTerm[CVC4::Datatype& dt, std::vector& ops] dt.addConstructor(c); } | HEX_LITERAL - { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); + { Debug("parser-sygus") << "Sygus grammar : integer literal " << AntlrInput::tokenText($HEX_LITERAL) << std::endl; + assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); ops.push_back(MK_CONST( BitVector(hexString, 16) )); name = dt.getName() + "_" + AntlrInput::tokenText($HEX_LITERAL); @@ -793,7 +748,8 @@ sygusGTerm[CVC4::Datatype& dt, std::vector& ops] dt.addConstructor(c); } | BINARY_LITERAL - { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); + { Debug("parser-sygus") << "Sygus grammar : integer literal " << AntlrInput::tokenText($BINARY_LITERAL) << std::endl; + assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); ops.push_back(MK_CONST( BitVector(binString, 2) )); name = dt.getName() + "_" + AntlrInput::tokenText($BINARY_LITERAL); @@ -804,16 +760,29 @@ sygusGTerm[CVC4::Datatype& dt, std::vector& ops] CVC4::DatatypeConstructor c(name, testerId); dt.addConstructor(c); } - | symbol[name,CHECK_DECLARED,SYM_VARIABLE] - { Expr bv = PARSER_STATE->getVariable(name); - ops.push_back(bv); - name = dt.getName() + "_" + name; - std::string testerId("is-"); - testerId.append(name); - PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); - PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); - CVC4::DatatypeConstructor c(name, testerId); - dt.addConstructor(c); + | symbol[name,CHECK_NONE,SYM_VARIABLE] + { if( name[0] == '-' ){ //hack for unary minus + Debug("parser-sygus") << "Sygus grammar : unary minus integer literal " << name << std::endl; + ops.push_back(MK_CONST(Rational(name))); + name = dt.getName() + "_" + name; + std::string testerId("is-"); + testerId.append(name); + PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); + PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); + CVC4::DatatypeConstructor c(name, testerId); + dt.addConstructor(c); + }else{ + Debug("parser-sygus") << "Sygus grammar : symbol " << name << std::endl; + Expr bv = PARSER_STATE->getVariable(name); + ops.push_back(bv); + name = dt.getName() + "_" + name; + std::string testerId("is-"); + testerId.append(name); + PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); + PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); + CVC4::DatatypeConstructor c(name, testerId); + dt.addConstructor(c); + } } ; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 27ba07008..d20d48b13 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -462,5 +462,182 @@ void Smt2::includeFile(const std::string& filename) { } } + + + void Smt2::defineSygusFuns() { + // only define each one once + while(d_nextSygusFun < d_sygusFuns.size()) { + std::pair p = d_sygusFuns[d_nextSygusFun]; + std::string fun = p.first; + Debug("parser-sygus") << "Sygus : define fun " << fun << std::endl; + Expr eval = p.second; + FunctionType evalType = eval.getType(); + std::vector argTypes = evalType.getArgTypes(); + Type rangeType = evalType.getRangeType(); + Debug("parser-sygus") << "...eval type : " << evalType << ", #args=" << argTypes.size() << std::endl; + + // first make the function type + std::vector sygusVars; + std::vector funType; + for(size_t j = 1; j < argTypes.size(); ++j) { + funType.push_back(argTypes[j]); + std::stringstream ss; + 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; + + // 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; + */ + + //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; + Expr funbv = getExprManager()->mkBoundVar(std::string("f") + fun, argTypes[0]); + d_sygusFunSymbols.push_back(funbv); + applyv.push_back(eval); + applyv.push_back(funbv); + for(size_t i = 0; i < sygusVars.size(); ++i) { + applyv.push_back(sygusVars[i]); + } + Expr apply = getExprManager()->mkExpr(kind::APPLY_UF, applyv); + Debug("parser-sygus") << "...made apply " << apply << std::endl; + Command* cmd = new DefineFunctionCommand(fun, lambda, sygusVars, apply); + preemptCommand(cmd); + + ++d_nextSygusFun; + } +} + +// i is index in datatypes/ops +// j is index is datatype +Expr Smt2::getSygusAssertion( std::vector& datatypeTypes, std::vector< std::vector >& ops, + std::map& evals, std::vector& terms, + Expr eval, const Datatype& dt, size_t i, size_t j ) { + const DatatypeConstructor& ctor = dt[j]; + Debug("parser-sygus") << "Sygus : process constructor " << j << " : " << dt[j] << std::endl; + std::vector bvs, extraArgs; + for(size_t k = 0; k < ctor.getNumArgs(); ++k) { + std::string vname = "v_" + ctor[k].getName(); + Expr bv = getExprManager()->mkBoundVar(vname, SelectorType(ctor[k].getType()).getRangeType()); + 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); + Debug("parser-sygus") << "...made bv list " << bvl << std::endl; + std::vector patv; + patv.push_back(eval); + std::vector applyv; + applyv.push_back(ctor.getConstructor()); + applyv.insert(applyv.end(), extraArgs.begin(), extraArgs.end()); + for(size_t k = 0; k < applyv.size(); ++k) { + } + 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()); + Expr evalApply = getExprManager()->mkExpr(kind::APPLY_UF, patv); + Debug("parser-sygus") << "...made eval apply " << evalApply << std::endl; + std::vector builtApply; + for(size_t k = 0; k < extraArgs.size(); ++k) { + 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()); + builtApply.push_back(getExprManager()->mkExpr(kind::APPLY_UF, patvb)); + } + for(size_t k = 0; k < builtApply.size(); ++k) { + } + Expr builtTerm; + //if( ops[i][j].getKind() == kind::BUILTIN ){ + if( !builtApply.empty() ){ + builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply); + }else{ + builtTerm = ops[i][j]; + } + 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); + Debug("parser-sygus") << "...made assertion " << assertion << std::endl; + + //linearize multiplication if possible + if( builtTerm.getKind()==kind::MULT ){ + for(size_t k = 0; k < ctor.getNumArgs(); ++k) { + Type at = SelectorType(ctor[k].getType()).getRangeType(); + if( at.isDatatype() ){ + DatatypeType atd = (DatatypeType)SelectorType(ctor[k].getType()).getRangeType(); + Debug("parser-sygus") << "Argument " << k << " " << atd << std::endl; + std::vector::iterator itd = std::find( datatypeTypes.begin(), datatypeTypes.end(), atd ); + if( itd!=datatypeTypes.end() ){ + Debug("parser-sygus2") << "Exists in datatypeTypes." << std::endl; + unsigned index = itd-datatypeTypes.begin(); + Debug("parser-sygus2") << "index = " << index << std::endl; + bool isConst = true; + for( unsigned cc = 0; cc < ops[index].size(); cc++ ){ + Debug("parser-sygus2") << "ops[" << cc << "]=" << ops[index][cc] << std::endl; + if( ops[index][cc].getKind() != kind::CONST_RATIONAL ){ + isConst = false; + break; + } + } + if( isConst ){ + Debug("parser-sygus") << "Linearize multiplication " << ctor << " based on argument " << k << std::endl; + const Datatype & atdd = atd.getDatatype(); + std::vector assertions; + std::vector nbvs; + for( unsigned a=0; amkExpr( kind::BOUND_VAR_LIST, nbvs ); + for( unsigned cc = 0; cc < ops[index].size(); cc++ ){ + //Make new assertion based on partially instantiating existing + applyv[k+1] = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, atdd[cc].getConstructor()); + Debug("parser-sygus") << "applyv " << applyv[k+1] << std::endl; + cpatv = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, applyv); + Debug("parser-sygus") << "cpatv " << cpatv << std::endl; + patv[1] = cpatv; + evalApply = getExprManager()->mkExpr(kind::APPLY_UF, patv); + Debug("parser-sygus") << "evalApply " << evalApply << std::endl; + builtApply[k] = ops[index][cc]; + Debug("parser-sygus") << "builtApply " << builtApply[k] << std::endl; + builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply); + Debug("parser-sygus") << "builtTerm " << builtTerm << std::endl; + Expr eassertion = getExprManager()->mkExpr(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm); + Expr epattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply); + epattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, epattern); + eassertion = getExprManager()->mkExpr(kind::FORALL, nbvl, eassertion, epattern); + assertions.push_back( eassertion ); + } + assertion = assertions.size()==1 ? assertions[0] : getExprManager()->mkExpr( kind::AND, assertions ); + Debug("parser-sygus") << "...(linearized) assertion is: " << assertion << std::endl; + } + } + } + } + } + return assertion; +} + + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 35842f308..ca1602f36 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -182,65 +182,13 @@ public: d_sygusFuns.push_back(std::make_pair(fun, eval)); } - void defineSygusFuns() { - // only define each one once - while(d_nextSygusFun < d_sygusFuns.size()) { - std::pair p = d_sygusFuns[d_nextSygusFun]; - std::string fun = p.first; - Debug("parser-sygus") << "Sygus : define fun " << fun << std::endl; - Expr eval = p.second; - FunctionType evalType = eval.getType(); - std::vector argTypes = evalType.getArgTypes(); - Type rangeType = evalType.getRangeType(); - Debug("parser-sygus") << "...eval type : " << evalType << ", #args=" << argTypes.size() << std::endl; - - // first make the function type - std::vector sygusVars; - std::vector funType; - for(size_t j = 1; j < argTypes.size(); ++j) { - funType.push_back(argTypes[j]); - std::stringstream ss; - 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; - - // 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; - */ - - //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; - Expr funbv = getExprManager()->mkBoundVar(std::string("f") + fun, argTypes[0]); - d_sygusFunSymbols.push_back(funbv); - applyv.push_back(eval); - applyv.push_back(funbv); - for(size_t i = 0; i < sygusVars.size(); ++i) { - applyv.push_back(sygusVars[i]); - } - Expr apply = getExprManager()->mkExpr(kind::APPLY_UF, applyv); - Debug("parser-sygus") << "...made apply " << apply << std::endl; - Command* cmd = new DefineFunctionCommand(fun, lambda, sygusVars, apply); - preemptCommand(cmd); - - ++d_nextSygusFun; - } - } + void defineSygusFuns(); + + // i is index in datatypes/ops + // j is index is datatype + Expr getSygusAssertion( std::vector& datatypeTypes, std::vector< std::vector >& ops, + std::map& evals, std::vector& terms, + Expr eval, const Datatype& dt, size_t i, size_t j ); void addSygusConstraint(Expr constraint) { d_sygusConstraints.push_back(constraint); -- 2.30.2