From: ajreynol Date: Wed, 10 Jun 2015 13:35:07 +0000 (+0200) Subject: Support for printing solutions involving LetGTerm sygus. Bug fix define-fun within... X-Git-Tag: cvc5-1.0.0~6297 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2f2b368448c3a5e50db46b3ec2cc364ae8959ac1;p=cvc5.git Support for printing solutions involving LetGTerm sygus. Bug fix define-fun within LetGTerm sygus. Bug fix sygus argument generalization. Add regressions. --- 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& 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 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; igetVarInc( 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& d ) { if( n.getKind()==OR ){ for( unsigned i=0; i 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 subs_lvs; + std::vector< Node > new_lvs; + for( unsigned i=0; imkBoundVar( ss.str(), v.getType() ); + new_lvs.push_back( lv ); + //map free variables to proper terms + if( i& 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 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& 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. */ diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 40f3fa4aa..dc6a1e0d1 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -32,7 +32,10 @@ TESTS = commutative.sy \ const-var-test.sy \ no-syntax-test.sy \ no-syntax-test-no-si.sy \ - no-flat-simp.sy + no-flat-simp.sy \ + twolets2-orig.sy \ + let-ringer.sy \ + let-simp.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy new file mode 100644 index 000000000..046d074d9 --- /dev/null +++ b/test/regress/regress0/sygus/let-ringer.sy @@ -0,0 +1,14 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si +(set-logic LIA) +(define-fun g ((x Int)) Int (ite (= x 1) 15 19)) +(synth-fun f ((x Int)) Int + ((Start Int (x + 0 + 1 + (- Start Start) + (let ((z Int Start) (w Int Start)) (+ z (+ x (+ x (+ Start (+ 1 (+ (g w) z))))))))))) + +(declare-var x Int) +(constraint (= (f x) (+ (* 4 x) 15))) +(check-synth) diff --git a/test/regress/regress0/sygus/let-simp.sy b/test/regress/regress0/sygus/let-simp.sy new file mode 100644 index 000000000..daca906a2 --- /dev/null +++ b/test/regress/regress0/sygus/let-simp.sy @@ -0,0 +1,15 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si +(set-logic LIA) +(synth-fun f ((x Int) (y Int)) Int + ((Start Int (x + y + 0 + (- Start Start) + (let ((z Int Start)) (+ z z)))))) + +(declare-var x Int) +(declare-var y Int) +(constraint (= (f x y) (* 3 x))) +(check-synth) + diff --git a/test/regress/regress0/sygus/twolets2-orig.sy b/test/regress/regress0/sygus/twolets2-orig.sy new file mode 100644 index 000000000..c1066277e --- /dev/null +++ b/test/regress/regress0/sygus/twolets2-orig.sy @@ -0,0 +1,28 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si +(set-logic LIA) +(synth-fun f1 ((x Int)) Int + ( + (Start Int ( + (let ((y Int CInt) (z Int CInt)) (+ (+ y x) z)) + ) + ) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + + ) +) +(synth-fun f2 ((x Int)) Int + ( + (Start Int (x + (let ((y Int Start) (z Int CInt)) (+ (+ y x) z)) + ) + ) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + + ) +) +(declare-var x1 Int) +(declare-var x2 Int) +(constraint (= (+ (f1 x1)(f2 x2)) (+ (+ x2 x2) (+ x1 8)))) +(check-synth) +