diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-10 15:35:07 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-10 15:35:07 +0200 |
commit | 2f2b368448c3a5e50db46b3ec2cc364ae8959ac1 (patch) | |
tree | 91576c0fd2ed7fee5da14598f15138a18c2cc27a /src | |
parent | 6417016a38e24b09bc062a4bd4b0a5945fbcc0ec (diff) |
Support for printing solutions involving LetGTerm sygus. Bug fix define-fun within LetGTerm sygus. Bug fix sygus argument generalization. Add regressions.
Diffstat (limited to 'src')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 32 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 1 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 5 | ||||
-rw-r--r-- | src/theory/datatypes/datatypes_sygus.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 33 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 92 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 2 | ||||
-rw-r--r-- | src/util/datatype.cpp | 33 | ||||
-rw-r--r-- | src/util/datatype.h | 17 |
10 files changed, 172 insertions, 53 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 101e26746..7db87d579 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -663,11 +663,14 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st } Expr sop = ops[sub_dt_index][0]; Type curr_t; - if( sop.getKind() != kind::BUILTIN && ( sop.isConst() || sop.getNumChildren()==0 ) ){ + if( sop.getKind() != kind::BUILTIN && ( sop.isConst() || cargs[sub_dt_index][0].empty() ) ){ curr_t = sop.getType(); - Debug("parser-sygus") << ": it is constant/0-arg cons " << sop << " with type " << sop.getType() << std::endl; + Debug("parser-sygus") << ": it is constant/0-arg cons " << sop << " with type " << sop.getType() << ", debug=" << sop.isConst() << " " << cargs[sub_dt_index][0].size() << std::endl; sygus_to_builtin_expr[t] = sop; - d_sygus_bound_var_type[sop] = t; + //store that term sop has dedicated sygus type t + if( d_sygus_bound_var_type.find( sop )==d_sygus_bound_var_type.end() ){ + d_sygus_bound_var_type[sop] = t; + } }else{ std::vector< Expr > children; if( sop.getKind() != kind::BUILTIN ){ @@ -677,13 +680,14 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st std::map< CVC4::Type, CVC4::Expr >::iterator it = sygus_to_builtin_expr.find( cargs[sub_dt_index][0][i] ); if( it==sygus_to_builtin_expr.end() ){ Type bt = sygus_to_builtin[cargs[sub_dt_index][0][i]]; - Debug("parser-sygus") << ": type elem " << i << " " << cargs[sub_dt_index][0][i] << " " << bt << std::endl; + Debug("parser-sygus") << ": child " << i << " introduce type elem for " << cargs[sub_dt_index][0][i] << " " << bt << std::endl; std::stringstream ss; ss << t << "_x_" << i; Expr bv = mkBoundVar(ss.str(), bt); children.push_back( bv ); d_sygus_bound_var_type[bv] = cargs[sub_dt_index][0][i]; }else{ + Debug("parser-sygus") << ": child " << i << " existing sygus to builtin expr : " << it->second << std::endl; children.push_back( it->second ); } } @@ -775,9 +779,10 @@ void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, cnames[index].pop_back(); cnames[index].push_back(ss.str()); - //TODO : mark function as let constructor - d_sygus_let_func_to_vars[let_func].insert( d_sygus_let_func_to_vars[let_func].end(), let_vars.begin(), let_vars.end() ); + //mark function as let constructor + d_sygus_let_func_to_vars[let_func].insert( d_sygus_let_func_to_vars[let_func].end(), let_define_args.begin(), let_define_args.end() ); d_sygus_let_func_to_body[let_func] = let_body; + d_sygus_let_func_to_num_input_vars[let_func] = let_vars.size(); } @@ -899,13 +904,24 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, testerId.append(name); checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); - CVC4::DatatypeConstructor c(name, testerId, ops[i] ); + CVC4::DatatypeConstructor c(name, testerId ); + Debug("parser-sygus") << "--> Add constructor " << cnames[i] << " to " << dt.getName() << std::endl; + Expr let_body; + std::vector< Expr > let_args; + unsigned let_num_input_args = 0; + std::map< CVC4::Expr, CVC4::Expr >::iterator it = d_sygus_let_func_to_body.find( ops[i] ); + if( it!=d_sygus_let_func_to_body.end() ){ + let_body = it->second; + let_args.insert( let_args.end(), d_sygus_let_func_to_vars[ops[i]].begin(), d_sygus_let_func_to_vars[ops[i]].end() ); + let_num_input_args = d_sygus_let_func_to_num_input_vars[ops[i]]; + Debug("parser-sygus") << " it is a let gterm with body " << let_body << std::endl; + } + c.setSygus( ops[i], let_body, let_args, let_num_input_args ); for( unsigned j=0; j<cargs[i].size(); j++ ){ std::stringstream sname; sname << name << "_" << j; c.addArg(sname.str(), cargs[i][j]); } - Debug("parser-sygus") << "--> Add constructor " << cnames[i] << " to " << dt.getName() << std::endl; dt.addConstructor(c); } } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 6781fec95..428977e0b 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -301,6 +301,7 @@ private: std::map< CVC4::Expr, CVC4::Type > d_sygus_bound_var_type; std::map< CVC4::Expr, std::vector< CVC4::Expr > > d_sygus_let_func_to_vars; std::map< CVC4::Expr, CVC4::Expr > d_sygus_let_func_to_body; + std::map< CVC4::Expr, unsigned > d_sygus_let_func_to_num_input_vars; void collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusArgs, std::vector< CVC4::Expr >& builtinArgs ); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5d5bb93dc..1ab4ee62a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1429,6 +1429,11 @@ void SmtEngine::setDefaults() { if( options::recurseCbqi() || options::cbqi2() ){ options::cbqi.set( true ); } + if( options::cbqi2() ){ + if( !options::rewriteDivk.wasSetByUser()) { + options::rewriteDivk.set( true ); + } + } if( options::cbqi() ){ if( !options::quantConflictFind.wasSetByUser() ){ options::quantConflictFind.set( false ); diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 19aacd0df..a9e6b3a78 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -928,10 +928,17 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node Node progc = prog; if( options::sygusNormalFormGlobalArg() ){ bool argChanged = false; + Trace("sygus-nf-gen-debug") << "Check replacements on " << prog << " " << prog.getKind() << std::endl; for( unsigned i=0; i<prog.getNumChildren(); i++ ){ Node prev = children[i]; children[i] = d_tds->getVarInc( children_stype[i], var_count ); + if( parentOpKind!=kind::BUILTIN ){ + children.insert( children.begin(), prog.getOperator() ); + } Node progcn = NodeManager::currentNM()->mkNode( prog.getKind(), children ); + if( parentOpKind!=kind::BUILTIN ){ + children.erase( children.begin(), children.begin() + 1 ); + } Node progcr = Rewriter::rewrite( progcn ); Trace("sygus-nf-gen-debug") << "Var replace argument " << i << " : " << progcn << " -> " << progcr << std::endl; if( progcr==progr ){ diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 40fea68da..5f3498f49 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -389,7 +389,8 @@ bool CegInstantiation::getModelValues( CegConjecture * conj, std::vector< Node > TypeNode tn = nv.getType(); Trace("cegqi-engine") << n[i] << " -> "; std::stringstream ss; - printSygusTerm( ss, nv ); + std::vector< Node > lvs; + TermDbSygus::printSygusTerm( ss, nv, lvs ); Trace("cegqi-engine") << ss.str() << " "; } if( nv.isNull() ){ @@ -522,7 +523,8 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { if( sol.isNull() ){ out << "?"; }else{ - printSygusTerm( out, sol ); + std::vector< Node > lvs; + TermDbSygus::printSygusTerm( out, sol, lvs ); } } out << ")" << std::endl; @@ -531,33 +533,6 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { } } -void CegInstantiation::printSygusTerm( std::ostream& out, Node n ) { - if( n.getKind()==APPLY_CONSTRUCTOR ){ - TypeNode tn = n.getType(); - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - if( dt.isSygus() ){ - int cIndex = Datatype::indexOf( n.getOperator().toExpr() ); - Assert( !dt[cIndex].getSygusOp().isNull() ); - if( n.getNumChildren()>0 ){ - out << "("; - } - out << dt[cIndex].getSygusOp(); - if( n.getNumChildren()>0 ){ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - out << " "; - printSygusTerm( out, n[i] ); - } - out << ")"; - } - return; - } - }else if( !n.getAttribute(SygusProxyAttribute()).isNull() ){ - out << n.getAttribute(SygusProxyAttribute()); - }else{ - out << n; - } -} - void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) { if( n.getKind()==OR ){ for( unsigned i=0; i<n.getNumChildren(); i++ ){ diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 09e449b35..74e9b0aba 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -116,9 +116,6 @@ private: Node getModelValue( Node n ); /** get model term */ Node getModelTerm( Node n ); -private: - /** print sygus term */ - void printSygusTerm( std::ostream& out, Node n ); public: CegInstantiation( QuantifiersEngine * qe, context::Context* c ); public: diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index d57f52b35..79199d8b4 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1511,7 +1511,9 @@ Node TermDbSygus::getGenericBase( TypeNode tn, const Datatype& dt, int c ) { std::map< TypeNode, int > var_count; std::map< int, Node > pre; Node g = mkGeneric( dt, c, var_count, pre ); + Trace("sygus-db-debug") << "Sygus DB : Generic is " << g << std::endl; Node gr = Rewriter::rewrite( g ); + Trace("sygus-db-debug") << "Sygus DB : Generic rewritten is " << gr << std::endl; gr = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( gr.toExpr() ) ); Trace("sygus-db") << "Sygus DB : Generic base " << dt[c].getName() << " : " << gr << std::endl; d_generic_base[tn][c] = gr; @@ -1530,6 +1532,7 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int if( op.getKind()!=BUILTIN ){ children.push_back( op ); } + Trace("sygus-db") << "mkGeneric " << dt.getName() << " " << op << " " << op.getKind() << "..." << std::endl; for( int i=0; i<(int)dt[c].getNumArgs(); i++ ){ TypeNode tna = TypeNode::fromType( ((SelectorType)dt[c][i].getType()).getRangeType() ); Node a; @@ -1542,13 +1545,14 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int Assert( !a.isNull() ); children.push_back( a ); } + Node ret; if( op.getKind()==BUILTIN ){ - return NodeManager::currentNM()->mkNode( op, children ); + ret = NodeManager::currentNM()->mkNode( op, children ); }else{ if( children.size()==1 ){ - return children[0]; + ret = children[0]; }else{ - return NodeManager::currentNM()->mkNode( APPLY, children ); + ret = NodeManager::currentNM()->mkNode( APPLY, children ); /* Node n = NodeManager::currentNM()->mkNode( APPLY, children ); //must expand definitions @@ -1558,6 +1562,8 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int */ } } + Trace("sygus-db") << "...returning " << ret << std::endl; + return ret; } Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) { @@ -1573,7 +1579,9 @@ Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) { pre[j] = sygusToBuiltin( n[j], getArgType( dt[i], j ) ); } Node ret = mkGeneric( dt, i, var_count, pre ); + Trace("sygus-db-debug") << "SygusToBuiltin : Generic is " << ret << std::endl; ret = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( ret.toExpr() ) ); + Trace("sygus-db-debug") << "SygusToBuiltin : After expand definitions " << ret << std::endl; d_sygus_to_builtin[tn][n] = ret; return ret; }else{ @@ -2030,4 +2038,80 @@ Node TermDbSygus::expandBuiltinTerm( Node t ){ NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) ); } return Node::null(); -}
\ No newline at end of file +} + + +void doReplace(std::string& str, const std::string& oldStr, const std::string& newStr){ + size_t pos = 0; + while((pos = str.find(oldStr, pos)) != std::string::npos){ + str.replace(pos, oldStr.length(), newStr); + pos += newStr.length(); + } +} + +void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs ) { + if( n.getKind()==APPLY_CONSTRUCTOR ){ + TypeNode tn = n.getType(); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + if( dt.isSygus() ){ + int cIndex = Datatype::indexOf( n.getOperator().toExpr() ); + Assert( !dt[cIndex].getSygusOp().isNull() ); + if( dt[cIndex].getSygusLetBody().isNull() ){ + if( n.getNumChildren()>0 ){ + out << "("; + } + out << dt[cIndex].getSygusOp(); + if( n.getNumChildren()>0 ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + out << " "; + printSygusTerm( out, n[i], lvs ); + } + out << ")"; + } + }else{ + //print as let term + out << "(let ("; + std::vector< Node > subs_lvs; + std::vector< Node > new_lvs; + for( unsigned i=0; i<dt[cIndex].getNumSygusLetArgs(); i++ ){ + Node v = Node::fromExpr( dt[cIndex].getSygusLetArg( i ) ); + subs_lvs.push_back( v ); + std::stringstream ss; + ss << "_l_" << new_lvs.size(); + Node lv = NodeManager::currentNM()->mkBoundVar( ss.str(), v.getType() ); + new_lvs.push_back( lv ); + //map free variables to proper terms + if( i<dt[cIndex].getNumSygusLetInputArgs() ){ + //it should be printed as a let argument + out << "("; + out << lv << " " << lv.getType() << " "; + printSygusTerm( out, n[i], lvs ); + out << ")"; + } + } + out << ") "; + //print the body + Node let_body = Node::fromExpr( dt[cIndex].getSygusLetBody() ); + let_body = let_body.substitute( subs_lvs.begin(), subs_lvs.end(), new_lvs.begin(), new_lvs.end() ); + new_lvs.insert( new_lvs.end(), lvs.begin(), lvs.end() ); + std::stringstream body_out; + printSygusTerm( body_out, let_body, new_lvs ); + std::string body = body_out.str(); + for( unsigned i=dt[cIndex].getNumSygusLetInputArgs(); i<dt[cIndex].getNumSygusLetArgs(); i++ ){ + std::stringstream old_str; + old_str << new_lvs[i]; + std::stringstream new_str; + printSygusTerm( new_str, n[i], lvs ); + doReplace( body, old_str.str().c_str(), new_str.str().c_str() ); + } + out << body << ")"; + } + return; + } + }else if( !n.getAttribute(SygusProxyAttribute()).isNull() ){ + out << n.getAttribute(SygusProxyAttribute()); + }else{ + out << n; + } +} + diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 37b1528b3..0bb2c3224 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -459,6 +459,8 @@ public: Node minimizeBuiltinTerm( Node n ); /** given a term, expand it into more basic components */ Node expandBuiltinTerm( Node n ); + /** print sygus term */ + static void printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs ); }; }/* CVC4::theory::quantifiers namespace */ diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 5a7a6da89..b1ab011ef 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -607,15 +607,14 @@ DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester) : CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester"); } -DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester, Expr sygus_op) : - d_name(name + '\0' + tester), - d_tester(), - d_args(), - d_sygus_op(sygus_op) { - CheckArgument(name != "", name, "cannot construct a datatype constructor without a name"); - CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester"); +void DatatypeConstructor::setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_args ){ + d_sygus_op = op; + d_sygus_let_body = let_body; + d_sygus_let_args.insert( d_sygus_let_args.end(), let_args.begin(), let_args.end() ); + d_sygus_num_let_input_args = num_let_input_args; } + void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) { // We don't want to introduce a new data member, because eventually // we're going to be a constant stuffed inside a node. So we stow @@ -689,6 +688,26 @@ Expr DatatypeConstructor::getSygusOp() const { return d_sygus_op; } +Expr DatatypeConstructor::getSygusLetBody() const { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + return d_sygus_let_body; +} + +unsigned DatatypeConstructor::getNumSygusLetArgs() const { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + return d_sygus_let_args.size(); +} + +Expr DatatypeConstructor::getSygusLetArg( unsigned i ) const { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + return d_sygus_let_args[i]; +} + +unsigned DatatypeConstructor::getNumSygusLetInputArgs() const { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + return d_sygus_num_let_input_args; +} + Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); diff --git a/src/util/datatype.h b/src/util/datatype.h index 224ac89ad..1945c4390 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -187,6 +187,9 @@ private: std::vector<DatatypeConstructorArg> d_args; /** the operator associated with this constructor (for sygus) */ Expr d_sygus_op; + Expr d_sygus_let_body; + std::vector< Expr > d_sygus_let_args; + unsigned d_sygus_num_let_input_args; void resolve(ExprManager* em, DatatypeType self, const std::map<std::string, DatatypeType>& resolutions, @@ -232,7 +235,9 @@ public: * constructor and tester aren't created until resolution time. */ DatatypeConstructor(std::string name, std::string tester); - DatatypeConstructor(std::string name, std::string tester, Expr sygus_op); + + /** set sygus */ + void setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_argus ); /** * Add an argument (i.e., a data field) of the given name and type @@ -281,7 +286,15 @@ public: /** get sygus op */ Expr getSygusOp() const; - + /** get sygus let body */ + Expr getSygusLetBody() const; + /** get number of sygus let args */ + unsigned getNumSygusLetArgs() const; + /** get sygus let arg */ + Expr getSygusLetArg( unsigned i ) const; + /** get number of let arguments that should be printed as arguments to let */ + unsigned getNumSygusLetInputArgs() const; + /** * Get the tester name for this Datatype constructor. */ |