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<Expr> 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<Expr> patv;
- patv.push_back(eval);
- std::vector<Expr> 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<Expr> 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));
}
}
( 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
// 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;
{ 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);
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);
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);
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);
+ }
}
;
}
}
+
+
+ void Smt2::defineSygusFuns() {
+ // only define each one once
+ while(d_nextSygusFun < d_sygusFuns.size()) {
+ std::pair<std::string, Expr> 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<Type> 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<Expr> sygusVars;
+ std::vector<Type> 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<Expr> sygusVars;
+ //std::vector<Type> 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<Expr> 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<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops,
+ std::map<DatatypeType, Expr>& evals, std::vector<Expr>& 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<Expr> 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<Expr> patv;
+ patv.push_back(eval);
+ std::vector<Expr> 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<Expr> builtApply;
+ for(size_t k = 0; k < extraArgs.size(); ++k) {
+ std::vector<Expr> 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<DatatypeType>::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<Expr> assertions;
+ std::vector<Expr> nbvs;
+ for( unsigned a=0; a<bvl.getNumChildren(); a++ ){
+ if( a!=k ){
+ nbvs.push_back( bvl[a] );
+ }
+ }
+ Expr nbvl = getExprManager()->mkExpr( 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 */
d_sygusFuns.push_back(std::make_pair(fun, eval));
}
- void defineSygusFuns() {
- // only define each one once
- while(d_nextSygusFun < d_sygusFuns.size()) {
- std::pair<std::string, Expr> 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<Type> 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<Expr> sygusVars;
- std::vector<Type> 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<Expr> sygusVars;
- //std::vector<Type> 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<Expr> 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<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops,
+ std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms,
+ Expr eval, const Datatype& dt, size_t i, size_t j );
void addSygusConstraint(Expr constraint) {
d_sygusConstraints.push_back(constraint);
projects / cvc5.git / commitdiff