From 8f4e966ae0c0f42e595e1c603cb7c3f779b713ef Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sat, 1 Aug 2015 12:25:11 +0200 Subject: [PATCH] Support for default grammar for datatypes in sygus. Support vts for infinity. --- src/parser/smt2/Smt2.g | 1 + src/parser/smt2/smt2.cpp | 95 ++++++++++++++++++--- src/theory/quantifiers/term_database.cpp | 94 ++++++++++++-------- test/regress/regress0/sygus/Makefile.am | 27 +++--- test/regress/regress0/sygus/dt-no-syntax.sy | 12 +++ 5 files changed, 168 insertions(+), 61 deletions(-) create mode 100644 test/regress/regress0/sygus/dt-no-syntax.sy diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 1ce7c4aff..3dda54a18 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -730,6 +730,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] } evalType.push_back(sorts[i]); Expr eval = PARSER_STATE->mkVar(name, EXPR_MANAGER->mkFunctionType(evalType)); + Debug("parser-sygus") << "Make eval " << eval << " for " << dt.getName() << std::endl; evals.insert(std::make_pair(dtt, eval)); if(i == 0) { PARSER_STATE->addSygusFun(fun, eval); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 0500c9316..cc3b09cfe 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -512,13 +512,38 @@ Expr Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed) return e; } +void collectSygusGrammarTypesFor( Type range, std::vector< Type >& types, std::map< Type, std::vector< DatatypeConstructorArg > >& sels ){ + if( range.isInteger() || range.isBitVector() || range.isDatatype() ){ + if( std::find( types.begin(), types.end(), range )==types.end() ){ + Debug("parser-sygus") << "...will make grammar for " << range << std::endl; + types.push_back( range ); + if( range.isDatatype() ){ + const Datatype& dt = ((DatatypeType)range).getDatatype(); + for( unsigned i=0; i& datatypes, std::vector& sorts, std::vector< std::vector >& ops, std::vector sygus_vars, int& startIndex ) { + + if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() && !range.isDatatype() ){ + parseError("No default grammar for type."); + } startIndex = -1; Debug("parser-sygus") << "Construct default grammar for " << fun << " " << range << std::endl; std::map< CVC4::Type, CVC4::Type > sygus_to_builtin; std::vector< Type > types; + std::map< Type, std::vector< DatatypeConstructorArg > > sels; + //types for each of the variables for( unsigned i=0; i unres_types; + std::map< Type, Type > type_to_unres; for( unsigned i=0; i()); - std::vector cnames; - std::vector > cargs; - std::vector unresolved_gterm_sym; //make unresolved type Type unres_t = mkUnresolvedType(dname); unres_types.push_back(unres_t); + type_to_unres[types[i]] = unres_t; + sygus_to_builtin[unres_t] = types[i]; + } + for( unsigned i=0; i cnames; + std::vector > cargs; + std::vector unresolved_gterm_sym; + Type unres_t = unres_types[i]; //add variables for( unsigned j=0; j() ); } @@ -567,14 +598,14 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin std::stringstream ss; ss << consts[j]; Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl; - ops.back().push_back( consts[j] ); + ops[i].push_back( consts[j] ); cnames.push_back( ss.str() ); cargs.push_back( std::vector< CVC4::Type >() ); } //ITE CVC4::Kind k = kind::ITE; Debug("parser-sygus") << "...add for " << k << std::endl; - ops.back().push_back(getExprManager()->operatorOf(k)); + ops[i].push_back(getExprManager()->operatorOf(k)); cnames.push_back( kind::kindToString(k) ); cargs.push_back( std::vector< CVC4::Type >() ); cargs.back().push_back(unres_bt); @@ -585,20 +616,45 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin for( unsigned j=0; j<2; j++ ){ CVC4::Kind k = j==0 ? kind::PLUS : kind::MINUS; Debug("parser-sygus") << "...add for " << k << std::endl; - ops.back().push_back(getExprManager()->operatorOf(k)); + ops[i].push_back(getExprManager()->operatorOf(k)); cnames.push_back(kind::kindToString(k)); cargs.push_back( std::vector< CVC4::Type >() ); cargs.back().push_back(unres_t); cargs.back().push_back(unres_t); } + }else if( types[i].isDatatype() ){ + Debug("parser-sygus") << "...add for constructors" << std::endl; + const Datatype& dt = ((DatatypeType)types[i]).getDatatype(); + for( unsigned k=0; k() ); + for( unsigned j=0; j() ); + cargs.back().push_back( type_to_unres[arg_type] ); + } + } Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl; - datatypes.back().setSygus( types[i], bvl, true, true ); - mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym, sygus_to_builtin ); + datatypes[i].setSygus( types[i], bvl, true, true ); + mkSygusDatatype( datatypes[i], ops[i], cnames, cargs, unresolved_gterm_sym, sygus_to_builtin ); sorts.push_back( types[i] ); //set start index if applicable if( types[i]==range ){ @@ -613,6 +669,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin std::vector cnames; std::vector > cargs; std::vector unresolved_gterm_sym; + Debug("parser-sygus") << "Make grammar for " << btype << " " << datatypes.back() << std::endl; //add variables for( unsigned i=0; i() ); cargs.back().push_back(unres_types[i]); cargs.back().push_back(unres_types[i]); + }else if( types[i].isDatatype() ){ + //add for testers + Debug("parser-sygus") << "...add for testers" << std::endl; + const Datatype& dt = ((DatatypeType)types[i]).getDatatype(); + for( unsigned k=0; k() ); + cargs.back().push_back(unres_types[i]); + } } } if( range==btype ){ @@ -1312,7 +1381,9 @@ Expr Smt2::getSygusAssertion( std::vector& datatypeTypes, std::vec if( !terms[0].isNull() ){ patvb.insert(patvb.end(), terms[0].begin(), terms[0].end()); } + Debug("parser-sygus-debug") << "...add to built apply " << evals[DatatypeType(extraArgs[k].getType())] << " " << extraArgs[k] << " " << extraArgs[k].getType() << std::endl; builtApply.push_back(getExprManager()->mkExpr(kind::APPLY_UF, patvb)); + Debug("parser-sygus-debug") << "...added " << builtApply.back() << std::endl; } for(size_t k = 0; k < builtApply.size(); ++k) { } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 132c55cd9..380ee19fd 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1338,51 +1338,73 @@ Node TermDb::getVtsInfinity( bool isFree, bool create ) { } Node TermDb::rewriteVtsSymbols( Node n ) { - Assert( !d_vts_delta_free.isNull() ); - Assert( !d_vts_delta.isNull() ); - if( ( n.getKind()==EQUAL || n.getKind()==GEQ ) && containsTerm( n, d_vts_delta ) ){ + if( ( n.getKind()==EQUAL || n.getKind()==GEQ ) ){ Trace("quant-vts-debug") << "VTS : process " << n << std::endl; - if( n.getKind()==EQUAL ){ - return d_false; - }else{ - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( n, msum ) ){ - if( Trace.isOn("quant-vts-debug") ){ - Trace("quant-vts-debug") << "VTS got monomial sum : " << std::endl; - QuantArith::debugPrintMonomialSum( msum, "quant-vts-debug" ); - } - Node iso_n; - int res = QuantArith::isolate( d_vts_delta, msum, iso_n, n.getKind(), true ); - if( res!=0 ){ - Trace("quant-vts-debug") << "VTS isolated : -> " << iso_n << ", res = " << res << std::endl; - int index = res==1 ? 0 : 1; - Node slv = iso_n[res==1 ? 1 : 0]; - if( iso_n[index]!=d_vts_delta ){ - if( iso_n[index].getKind()==MULT && iso_n[index].getNumChildren()==2 && iso_n[index][0].isConst() && iso_n[index][1]==d_vts_delta ){ - slv = NodeManager::currentNM()->mkNode( MULT, slv, NodeManager::currentNM()->mkConst( Rational(1)/iso_n[index][0].getConst() ) ); + bool rew_inf = false; + bool rew_delta = false; + if( !d_vts_inf.isNull() && containsTerm( n, d_vts_inf ) ){ + rew_inf = true; + }else if( !d_vts_delta.isNull() && containsTerm( n, d_vts_delta ) ){ + rew_delta = true; + } + if( rew_inf || rew_delta ){ + if( n.getKind()==EQUAL ){ + return d_false; + }else{ + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( n, msum ) ){ + if( Trace.isOn("quant-vts-debug") ){ + Trace("quant-vts-debug") << "VTS got monomial sum : " << std::endl; + QuantArith::debugPrintMonomialSum( msum, "quant-vts-debug" ); + } + Node vts_sym = rew_inf ? d_vts_inf : d_vts_delta; + Node iso_n; + int res = QuantArith::isolate( vts_sym, msum, iso_n, n.getKind(), true ); + if( res!=0 ){ + Trace("quant-vts-debug") << "VTS isolated : -> " << iso_n << ", res = " << res << std::endl; + int index = res==1 ? 0 : 1; + Node slv = iso_n[res==1 ? 1 : 0]; + if( iso_n[index]!=vts_sym ){ + if( iso_n[index].getKind()==MULT && iso_n[index].getNumChildren()==2 && iso_n[index][0].isConst() && iso_n[index][1]==d_vts_delta ){ + slv = NodeManager::currentNM()->mkNode( MULT, slv, NodeManager::currentNM()->mkConst( Rational(1)/iso_n[index][0].getConst() ) ); + }else{ + return n; + } + } + Node nlit; + if( res==1 ){ + if( rew_inf ){ + nlit = d_true; + }else{ + nlit = NodeManager::currentNM()->mkNode( GEQ, d_zero, slv ); + } }else{ - return n; + if( rew_inf ){ + nlit = d_false; + }else{ + nlit = NodeManager::currentNM()->mkNode( GT, slv, d_zero ); + } } + Trace("quant-vts-debug") << "Return " << nlit << std::endl; + return nlit; } - Node nlit; - if( res==1 ){ - nlit = NodeManager::currentNM()->mkNode( GEQ, d_zero, slv ); - }else{ - nlit = NodeManager::currentNM()->mkNode( GT, slv, d_zero ); - } - Trace("quant-vts-debug") << "Return " << nlit << std::endl; - return nlit; } } - return n; } + return n; }else if( n.getKind()==FORALL ){ //cannot traverse beneath quantifiers - std::vector< Node > delta; - delta.push_back( d_vts_delta ); - std::vector< Node > delta_free; - delta_free.push_back( d_vts_delta_free ); - n = n.substitute( delta.begin(), delta.end(), delta_free.begin(), delta_free.end() ); + std::vector< Node > vars; + std::vector< Node > vars_free; + if( !d_vts_inf.isNull() ){ + vars.push_back( d_vts_inf ); + vars_free.push_back( d_vts_inf_free ); + } + if( !d_vts_delta.isNull() ){ + vars.push_back( d_vts_delta ); + vars_free.push_back( d_vts_delta_free ); + } + n = n.substitute( vars.begin(), vars.end(), vars_free.begin(), vars_free.end() ); return n; }else{ bool childChanged = false; diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 82ff67d41..cf0f005b9 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -9,8 +9,8 @@ AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) + $(LOG_COMPILER) \ + $(AM_LOG_FLAGS) $(LOG_FLAGS) endif MAKEFLAGS = -k @@ -22,12 +22,12 @@ TESTS = commutative.sy \ constant.sy \ multi-fun-polynomial2.sy \ unbdd_inv_gen_winf1.sy \ - max.sy \ - array_sum_2_5.sy \ - parity-AIG-d0.sy \ - twolets1.sy \ - array_search_2.sy \ - hd-01-d1-prog.sy \ + max.sy \ + array_sum_2_5.sy \ + parity-AIG-d0.sy \ + twolets1.sy \ + array_search_2.sy \ + hd-01-d1-prog.sy \ icfp_28_10.sy \ const-var-test.sy \ no-syntax-test.sy \ @@ -44,23 +44,24 @@ TESTS = commutative.sy \ no-syntax-test-bool.sy \ inv-example.sy \ uminus_one.sy \ - sygus-dt.sy + sygus-dt.sy \ + dt-no-syntax.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ - max.smt2 \ - sygus-uf.sl + max.smt2 \ + sygus-uf.sl #if CVC4_BUILD_PROFILE_COMPETITION #else #TESTS += \ -# error.cvc +# error.cvc #endif # disabled tests, yet distribute #EXTRA_DIST += \ -# setofsets-disequal.smt2 +# setofsets-disequal.smt2 # synonyms for "check" .PHONY: regress regress0 test diff --git a/test/regress/regress0/sygus/dt-no-syntax.sy b/test/regress/regress0/sygus/dt-no-syntax.sy new file mode 100644 index 000000000..e0f8112ce --- /dev/null +++ b/test/regress/regress0/sygus/dt-no-syntax.sy @@ -0,0 +1,12 @@ +; COMMAND-LINE: --cegqi --no-dump-synth +; EXPECT: unsat +(set-logic LIA) + +(declare-datatypes () ((List (cons (head Int) (tail List)) (nil)))) + +(synth-fun f ((x Int)) List) + +(declare-var x Int) + +(constraint (= (f x) (cons (+ x 1) nil))) +(check-synth) -- 2.30.2