From 54f1d00d5475710ec5a4c3eab82d786ba95dfdde Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 11 May 2015 20:06:21 +0200 Subject: [PATCH] Allow sygus with no syntactic restrictions for LIA. Add regressions. --- contrib/run-script-casc25-tff | 20 ++-- src/parser/smt2/Smt2.g | 19 +-- src/parser/smt2/smt2.cpp | 108 +++++++++++++++++- src/parser/smt2/smt2.h | 3 + src/smt/smt_engine.cpp | 3 + .../quantifiers/ce_guided_single_inv.cpp | 2 +- src/theory/quantifiers/options | 2 +- src/util/datatype.cpp | 9 +- src/util/datatype.h | 5 +- test/regress/regress0/sygus/Makefile.am | 4 +- .../regress0/sygus/no-syntax-test-no-si.sy | 14 +++ test/regress/regress0/sygus/no-syntax-test.sy | 15 +++ 12 files changed, 181 insertions(+), 23 deletions(-) create mode 100644 test/regress/regress0/sygus/no-syntax-test-no-si.sy create mode 100644 test/regress/regress0/sygus/no-syntax-test.sy diff --git a/contrib/run-script-casc25-tff b/contrib/run-script-casc25-tff index f6d244aad..23b31cf84 100644 --- a/contrib/run-script-casc25-tff +++ b/contrib/run-script-casc25-tff @@ -15,7 +15,7 @@ echo "------- cvc4-tff casc 25 : $bench at $2..." function trywith { limit=$1; shift; echo "--- Run $@ at $limit..."; - (ulimit -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive "$@" $bench) 2>/dev/null | + (ulimit -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" "$@" $bench) 2>/dev/null | (read w1 w2 w3 result w4 w5; case "$result" in Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; @@ -25,14 +25,16 @@ function trywith { } function finishwith { echo "--- Run $@..."; - $cvc4 --lang=tptp --no-checking --no-interactive "$@" $bench + $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" "$@" $bench } -trywith 10 --cbqi2 --decision=internal --full-saturate-quant --force-logic="UFNIRA" -trywith 10 --relevant-triggers --full-saturate-quant --force-logic="UFNIRA" -trywith 20 --cbqi --cbqi-recurse --full-saturate-quant --force-logic="UFNIRA" -trywith 20 --no-e-matching --full-saturate-quant --force-logic="UFNIRA" -trywith 20 --qcf-tconstraint --full-saturate-quant --force-logic="UFNIRA" -trywith 70 --full-saturate-quant --force-logic="UFNIRA" -finishwith --cbqi2 --cbqi-recurse --full-saturate-quant --force-logic="UFNIRA" +trywith 10 --cbqi2 --decision=internal --full-saturate-quant +trywith 10 --relevant-triggers --full-saturate-quant +trywith 10 --cbqi --full-saturate-quant +trywith 30 --qcf-tconstraint --full-saturate-quant +trywith 60 --cbqi --cbqi-recurse --full-saturate-quant +trywith 10 --full-saturate-quant +trywith 10 --no-e-matching --full-saturate-quant +trywith 10 --fmf-bound-int +finishwith --cbqi2 --cbqi-recurse --full-saturate-quant # echo "% SZS status" "GaveUp for $filename" diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 57ef44df0..dc00ead8c 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -496,7 +496,8 @@ sygusCommand returns [CVC4::Command* cmd = NULL] std::vector< std::vector > ops; std::vector< std::vector< std::string > > cnames; std::vector< std::vector< std::vector< CVC4::Type > > > cargs; - bool allow_const; + bool allow_const = false; + bool read_syntax = false; } : /* set the logic */ SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT] @@ -598,7 +599,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] terms.push_back(bvl); } sortSymbol[range,CHECK_DECLARED] - LPAREN_TOK + ( LPAREN_TOK ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] { PARSER_STATE->pushScope(true); } sortSymbol[t,CHECK_DECLARED] @@ -614,18 +615,23 @@ sygusCommand returns [CVC4::Command* cmd = NULL] // if not unresolved, must be undeclared PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT); } - allow_const = false; } // Note the official spec for NTDef is missing the ( parens ) // but they are necessary to parse SyGuS examples LPAREN_TOK sygusGTerm[fun, ops.back(), cnames.back(), cargs.back(), sygus_vars, allow_const]+ RPAREN_TOK RPAREN_TOK - { datatypes.back().setSygus( t, terms[0], allow_const ); + { datatypes.back().setSygus( t, terms[0], allow_const, false ); PARSER_STATE->mkSygusDatatype( datatypes.back(), ops.back(), cnames.back(), cargs.back() ); PARSER_STATE->popScope(); } )+ - RPAREN_TOK - { PARSER_STATE->popScope(); + RPAREN_TOK { read_syntax = true; } + )? + { + if( !read_syntax ){ + //create the default grammar + PARSER_STATE->mkSygusDefaultGrammar( range, terms[0], fun, datatypes, sorts, ops, sygus_vars ); + } + PARSER_STATE->popScope(); seq = new CommandSequence(); std::vector datatypeTypes = PARSER_STATE->mkMutualDatatypeTypes(datatypes); seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes)); @@ -794,7 +800,6 @@ sygusGTerm[std::string& fun, std::vector& ops, std::vectorparseError(std::string("Constant/Variable in sygus not supported.")); std::vector< Expr > consts; PARSER_STATE->mkSygusConstantsForType( t, consts ); for( unsigned i=0; i& datatypes, + std::vector& sorts, std::vector< std::vector >& ops, std::vector sygus_vars ) { + + Debug("parser-sygus") << "Construct default grammar for " << fun << " " << range << std::endl; + + std::stringstream ssb; + ssb << fun << "_Bool"; + std::string dbname = ssb.str(); + + std::stringstream ss; + ss << fun << "_" << range; + std::string dname = ss.str(); + datatypes.push_back(Datatype(dname)); + ops.push_back(std::vector()); + std::vector cnames; + std::vector > cargs; + //variables + for( unsigned i=0; i() ); + } + } + //constants + std::vector< Expr > consts; + mkSygusConstantsForType( range, consts ); + for( unsigned i=0; i() ); + } + //ITE + CVC4::Kind k = kind::ITE; + Debug("parser-sygus") << "...add for " << k << std::endl; + ops.back().push_back(getExprManager()->operatorOf(k)); + cnames.push_back( kind::kindToString(k) ); + cargs.push_back( std::vector< CVC4::Type >() ); + cargs.back().push_back(mkUnresolvedType(ssb.str())); + cargs.back().push_back(mkUnresolvedType(ss.str())); + cargs.back().push_back(mkUnresolvedType(ss.str())); + + if( range.isInteger() ){ + for( unsigned i=0; i<2; i++ ){ + CVC4::Kind k = i==0 ? kind::PLUS : kind::MINUS; + Debug("parser-sygus") << "...add for " << k << std::endl; + ops.back().push_back(getExprManager()->operatorOf(k)); + cnames.push_back(kind::kindToString(k)); + cargs.push_back( std::vector< CVC4::Type >() ); + cargs.back().push_back(mkUnresolvedType(ss.str())); + cargs.back().push_back(mkUnresolvedType(ss.str())); + } + }else{ + std::stringstream sserr; + sserr << "Don't know default Sygus grammar for type " << range << std::endl; + parseError(sserr.str()); + } + Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl; + datatypes.back().setSygus( range, bvl, true, true ); + mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs ); + sorts.push_back( range ); + + //Boolean type + datatypes.push_back(Datatype(dbname)); + ops.push_back(std::vector()); + cnames.clear(); + cargs.clear(); + for( unsigned i=0; i<4; i++ ){ + CVC4::Kind k = i==0 ? kind::NOT : ( i==1 ? kind::AND : ( i==2 ? kind::OR : kind::EQUAL ) ); + Debug("parser-sygus") << "...add for " << k << std::endl; + ops.back().push_back(getExprManager()->operatorOf(k)); + cnames.push_back(kind::kindToString(k)); + cargs.push_back( std::vector< CVC4::Type >() ); + if( k==kind::NOT ){ + cargs.back().push_back(mkUnresolvedType(ssb.str())); + }else if( k==kind::AND || k==kind::OR ){ + cargs.back().push_back(mkUnresolvedType(ssb.str())); + cargs.back().push_back(mkUnresolvedType(ssb.str())); + }else if( k==kind::EQUAL ){ + cargs.back().push_back(mkUnresolvedType(ss.str())); + cargs.back().push_back(mkUnresolvedType(ss.str())); + } + } + if( range.isInteger() ){ + CVC4::Kind k = kind::LEQ; + Debug("parser-sygus") << "...add for " << k << std::endl; + ops.back().push_back(getExprManager()->operatorOf(k)); + cnames.push_back(kind::kindToString(k)); + cargs.push_back( std::vector< CVC4::Type >() ); + cargs.back().push_back(mkUnresolvedType(ss.str())); + cargs.back().push_back(mkUnresolvedType(ss.str())); + } + Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl; + Type btype = getExprManager()->booleanType(); + datatypes.back().setSygus( btype, bvl, true, true ); + mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs ); + sorts.push_back( btype ); + + Debug("parser-sygus") << "...finished make default grammar for " << fun << " " << range << std::endl; +} + void Smt2::mkSygusConstantsForType( const Type& type, std::vector& ops ) { if( type.isInteger() ){ ops.push_back(getExprManager()->mkConst(Rational(0))); diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 67c019d50..eaf9e7b47 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -178,6 +178,9 @@ public: return e; } + void mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector& datatypes, + std::vector& sorts, std::vector< std::vector >& ops, std::vector sygus_vars ); + void mkSygusConstantsForType( const Type& type, std::vector& ops ); void addSygusFun(const std::string& fun, Expr eval) { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b20b84690..bc594a47e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1399,6 +1399,9 @@ void SmtEngine::setDefaults() { options::ceGuidedInst.set( true ); } if( options::ceGuidedInst() ){ + if( !options::cegqiSingleInv.wasSetByUser() ){ + options::cegqiSingleInv.set( true ); + } if( !options::quantConflictFind.wasSetByUser() ){ options::quantConflictFind.set( false ); } diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index a612db872..22ffcd278 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -1235,7 +1235,7 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& //reconstruct the solution into sygus if necessary reconstructed = 0; - if( options::cegqiSingleInvReconstruct() && !stn.isNull() ){ + if( options::cegqiSingleInvReconstruct() && !dt.getSygusAllowAll() && !stn.isNull() ){ d_sygus_solution = d_sol->reconstructSolution( s, stn, reconstructed ); if( reconstructed==1 ){ Trace("csi-sol") << "Solution (post-reconstruction into Sygus): " << d_sygus_solution << std::endl; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 4541c3d8a..e2d9af74f 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -203,7 +203,7 @@ option ceGuidedInst --cegqi bool :default false :read-write counterexample-guided quantifier instantiation option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h" if and how to apply fairness for cegqi -option cegqiSingleInv --cegqi-si bool :default false +option cegqiSingleInv --cegqi-si bool :default false :read-write process single invocation synthesis conjectures option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true reconstruct solutions for single invocation conjectures in original grammar diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 18ef25e7f..948bad56c 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -134,12 +134,13 @@ void Datatype::addConstructor(const DatatypeConstructor& c) { } -void Datatype::setSygus( Type st, Expr bvl, bool allow_const ){ +void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){ CheckArgument(!d_resolved, this, "cannot set sygus type to a finalized Datatype"); d_sygus_type = st; d_sygus_bvl = bvl; - d_sygus_allow_const = allow_const; + d_sygus_allow_const = allow_const || allow_all; + d_sygus_allow_const = allow_all; } @@ -475,6 +476,10 @@ bool Datatype::getSygusAllowConst() const { return d_sygus_allow_const; } +bool Datatype::getSygusAllowAll() const { + return d_sygus_allow_const; +} + bool Datatype::involvesExternalType() const{ return d_involvesExt; } diff --git a/src/util/datatype.h b/src/util/datatype.h index 79e7bf7d7..224ac89ad 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -457,6 +457,7 @@ private: Type d_sygus_type; Expr d_sygus_bvl; bool d_sygus_allow_const; + bool d_sygus_allow_all; // "mutable" because computing the cardinality can be expensive, // and so it's computed just once, on demand---this is the cache @@ -537,7 +538,7 @@ public: * bvl : the list of arguments for the synth-fun * allow_const : whether all constants are (implicitly) included in the grammar */ - void setSygus( Type st, Expr bvl, bool allow_const ); + void setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ); /** Get the name of this Datatype. */ inline std::string getName() const throw(); @@ -668,6 +669,8 @@ public: Expr getSygusVarList() const; /** does it allow constants */ bool getSygusAllowConst() const; + /** does it allow constants */ + bool getSygusAllowAll() const; /** * Get whether this datatype involves an external type. If so, diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 4f9d233fd..aaaf28717 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -29,7 +29,9 @@ TESTS = commutative.sy \ array_search_2.sy \ hd-01-d1-prog.sy \ icfp_28_10.sy \ - const-var-test.sy + const-var-test.sy \ + no-syntax-test.sy \ + no-syntax-test-no-si.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress0/sygus/no-syntax-test-no-si.sy b/test/regress/regress0/sygus/no-syntax-test-no-si.sy new file mode 100644 index 000000000..21788426c --- /dev/null +++ b/test/regress/regress0/sygus/no-syntax-test-no-si.sy @@ -0,0 +1,14 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi + +(set-logic LIA) + +(synth-fun f ((x Int) (y Int)) Int) + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (f x y) (+ (f x x) (f y y) x 1))) + +(check-synth) + diff --git a/test/regress/regress0/sygus/no-syntax-test.sy b/test/regress/regress0/sygus/no-syntax-test.sy new file mode 100644 index 000000000..95f9b7c11 --- /dev/null +++ b/test/regress/regress0/sygus/no-syntax-test.sy @@ -0,0 +1,15 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si + +(set-logic LIA) + +(synth-fun f ((x Int) (y Int)) Int) + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (f x y) (+ x y 500))) + + +(check-synth) + -- 2.30.2