From 7222fd13c68ee1352dabbe3791fae0ee13d689d1 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 2 Jun 2015 13:43:51 +0200 Subject: [PATCH] Add casc 25 tfn script. Change tff script to output instantiations. Work towards parsing non-flattened sygus grammars. --- contrib/run-script-casc25-tff | 4 +- contrib/run-script-casc25-tfn | 37 +++++++++ src/parser/smt2/Smt2.g | 151 +++++++++++++++++++++------------- 3 files changed, 132 insertions(+), 60 deletions(-) create mode 100644 contrib/run-script-casc25-tfn diff --git a/contrib/run-script-casc25-tff b/contrib/run-script-casc25-tff index 23b31cf84..9313b7886 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 --force-logic="UFNIRA" "$@" $bench) 2>/dev/null | + (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $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,7 +25,7 @@ function trywith { } function finishwith { echo "--- Run $@..."; - $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" "$@" $bench + $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench } trywith 10 --cbqi2 --decision=internal --full-saturate-quant diff --git a/contrib/run-script-casc25-tfn b/contrib/run-script-casc25-tfn new file mode 100644 index 000000000..d3c5d0344 --- /dev/null +++ b/contrib/run-script-casc25-tfn @@ -0,0 +1,37 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +file=${bench##*/} +filename=${file%.*} + +echo "------- cvc4-tfn casc 25 : $bench at $2..." + +# use: trywith [params..] +# to attempt a run. If an SZS ontology result is printed, then +# the run script terminates immediately. Otherwise, this +# function returns normally. +function trywith { + limit=$1; shift; + echo "--- Run $@ at $limit..."; + (ulimit -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive "$@" $bench) 2>/dev/null | + (read w1 w2 w3 result w4 w5; + case "$result" in + Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; + CounterSatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi +} +function finishwith { + echo "--- Run $@..."; + $cvc4 --lang=tptp --no-checking --no-interactive "$@" $bench +} + +trywith 30 --cbqi2 --decision=internal --full-saturate-quant +trywith 60 --finite-model-find --sort-inference --uf-ss-fair +trywith 30 --cbqi --full-saturate-quant +trywith 60 --cbqi --cbqi-recurse --full-saturate-quant +trywith 60 --fmf-bound-int --macros-quant +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 dc00ead8c..f500efe9a 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -492,12 +492,14 @@ sygusCommand returns [CVC4::Command* cmd = NULL] std::vector > sortedVarNames; SExpr sexpr; CommandSequence* seq; - std::vector datatypes; + std::vector< CVC4::Datatype > datatypes; std::vector< std::vector > ops; std::vector< std::vector< std::string > > cnames; std::vector< std::vector< std::vector< CVC4::Type > > > cargs; bool allow_const = false; bool read_syntax = false; + int sygus_dt_index; + Type sygus_ret; } : /* set the logic */ SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT] @@ -551,7 +553,6 @@ sygusCommand returns [CVC4::Command* cmd = NULL] { /* add variables to parser state before parsing term */ Debug("parser") << "define fun: '" << name << "'" << std::endl; if( sortedVarNames.size() > 0 ) { - std::vector sorts; sorts.reserve(sortedVarNames.size()); for(std::vector >::const_iterator i = sortedVarNames.begin(), iend = sortedVarNames.end(); @@ -615,13 +616,17 @@ sygusCommand returns [CVC4::Command* cmd = NULL] // if not unresolved, must be undeclared PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT); } + sygus_dt_index = ops.size()-1; + Debug("parser-sygus") << "Read sygus grammar " << name << " under function " << fun << "..." << std::endl; } // 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 + LPAREN_TOK sygusGTerm[sygus_dt_index, datatypes, sorts, fun, ops, cnames, cargs, sygus_vars, allow_const, sygus_ret, -1]+ RPAREN_TOK RPAREN_TOK - { datatypes.back().setSygus( t, terms[0], allow_const, false ); - PARSER_STATE->mkSygusDatatype( datatypes.back(), ops.back(), cnames.back(), cargs.back() ); + { for( unsigned i=sygus_dt_index; imkSygusDatatype( datatypes[i], ops[i], cnames[i], cargs[i] ); + } PARSER_STATE->popScope(); } )+ RPAREN_TOK { read_syntax = true; } @@ -716,10 +721,15 @@ sygusCommand returns [CVC4::Command* cmd = NULL] // SyGuS grammar term // fun is the name of the synth-fun this grammar term is for -// this adds N operators to ops, N names to cnames and N type argument vectors to cargs (where typically N=1) -sygusGTerm[std::string& fun, std::vector& ops, std::vector& cnames, - std::vector< std::vector< CVC4::Type > >& cargs, std::vector& sygus_vars, - bool& allow_const] +// this adds N operators to ops[index], N names to cnames[index] and N type argument vectors to cargs[index] (where typically N=1) +sygusGTerm[int index, + std::vector< CVC4::Datatype > datatypes, + std::vector< CVC4::Type> sorts, + std::string& fun, + std::vector< std::vector >& ops, + std::vector< std::vector >& cnames, + std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, + std::vector& sygus_vars, bool& allow_const, CVC4::Type& ret, int gtermType] @declarations { std::string name; Kind k; @@ -728,24 +738,31 @@ sygusGTerm[std::string& fun, std::vector& ops, std::vectoroperatorOf(k)); + ops[index].push_back(EXPR_MANAGER->operatorOf(k)); name = kind::kindToString(k); + sub_gtermType = 0; } + //| LET_TOK LPAREN_TOK + //( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] symbol[name2,CHECK_NONE,SYM_VARIABLE] RPAREN_TOK )+ + //RPAREN_TOK | symbol[name,CHECK_NONE,SYM_VARIABLE] { if(name=="Constant"){ - gtermType = 1; + sub_gtermType = 1; Debug("parser-sygus") << "Sygus grammar constant." << std::endl; }else if(name=="Variable"){ - gtermType = 2; + sub_gtermType = 2; allow_const = true; Debug("parser-sygus") << "Sygus grammar variable." << std::endl; }else{ @@ -755,8 +772,9 @@ sygusGTerm[std::string& fun, std::vector& ops, std::vectoroperatorOf(k)); + ops[index].push_back(EXPR_MANAGER->operatorOf(k)); name = kind::kindToString(k); + sub_gtermType = 0; }else{ // what is this sygus term trying to accomplish here, if the // symbol isn't yet declared?! probably the following line will @@ -766,38 +784,41 @@ sygusGTerm[std::string& fun, std::vector& ops, std::vectorisDefinedFunction(name) ){ PARSER_STATE->parseError(std::string("Functions in sygus grammars must be defined.")); } - ops.push_back( PARSER_STATE->getVariable(name) ); + ops[index].push_back( PARSER_STATE->getVariable(name) ); + sub_gtermType = 0; } } } ) - { if( gtermType==0 ){ - cnames.push_back( name ); + { if( sub_gtermType==0 ){ + cnames[index].push_back( name ); } - cargs.push_back( std::vector< CVC4::Type >() ); + cargs[index].push_back( std::vector< CVC4::Type >() ); + Debug("parser-sygus") << "Read arguments under " << name << ", gtermType = " << sub_gtermType << std::endl; + //add datatype definition for argument } - ( //sortSymbol[t,CHECK_NONE] - symbol[sname,CHECK_NONE,SYM_VARIABLE] - { - if( gtermType==0 ){ - std::stringstream ss; - ss << fun << "_" << sname; - sname = ss.str(); - } - if( PARSER_STATE->isDeclared(sname, SYM_SORT) ) { - t = PARSER_STATE->getSort(sname); - } else { - t = PARSER_STATE->mkUnresolvedType(sname); + ( //symbol[sname,CHECK_NONE,SYM_VARIABLE] + sygusGTerm[datatypes.size()-1,datatypes,sorts,fun,ops,cnames,cargs,sygus_vars,sub_allow_const,sub_ret,sub_gtermType] + { + Type t = sub_ret; + if( t.isNull() ){ + //then, it is the datatype we constructed } - cargs.back().push_back(t); + cargs[index].back().push_back(t); + //pop argument datatype definition if empty + + //add next datatype definition for argument + } )+ RPAREN_TOK { - if( gtermType==1 || gtermType==2 ){ - if( cargs.back().size()!=1 ){ + //pop argument datatype definition + + if( sub_gtermType==1 || sub_gtermType==2 ){ + if( cargs[index].back().size()!=1 ){ PARSER_STATE->parseError(std::string("Must provide single sort for constant/variable Sygus constructor.")); } - Type t = cargs.back()[0]; - cargs.pop_back(); + Type t = cargs[index].back()[0]; + cargs[index].pop_back(); Debug("parser-sygus") << "Make constructors for Constant/Variable of type " << t << std::endl; if( gtermType==1 ){ std::vector< Expr > consts; @@ -806,19 +827,19 @@ sygusGTerm[std::string& fun, std::vector& ops, std::vector() ); + ops[index].push_back( consts[i] ); + cnames[index].push_back( ss.str() ); + cargs[index].push_back( std::vector< CVC4::Type >() ); } - }else if( gtermType==2 ){ + }else if( sub_gtermType==2 ){ for( unsigned i=0; i() ); + ops[index].push_back( sygus_vars[i] ); + cnames[index].push_back( ss.str() ); + cargs[index].push_back( std::vector< CVC4::Type >() ); } } } @@ -826,38 +847,52 @@ sygusGTerm[std::string& fun, std::vector& ops, std::vector() ); + ops[index].push_back(MK_CONST(Rational(AntlrInput::tokenText($INTEGER_LITERAL)))); + cnames[index].push_back( AntlrInput::tokenText($INTEGER_LITERAL) ); + cargs[index].push_back( std::vector< CVC4::Type >() ); } | HEX_LITERAL { Debug("parser-sygus") << "Sygus grammar " << fun << " : hex 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) )); - cnames.push_back( AntlrInput::tokenText($HEX_LITERAL) ); - cargs.push_back( std::vector< CVC4::Type >() ); + ops[index].push_back(MK_CONST( BitVector(hexString, 16) )); + cnames[index].push_back( AntlrInput::tokenText($HEX_LITERAL) ); + cargs[index].push_back( std::vector< CVC4::Type >() ); } | BINARY_LITERAL { Debug("parser-sygus") << "Sygus grammar " << fun << " : binary 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) )); - cnames.push_back( AntlrInput::tokenText($BINARY_LITERAL) ); - cargs.push_back( std::vector< CVC4::Type >() ); + ops[index].push_back(MK_CONST( BitVector(binString, 2) )); + cnames[index].push_back( AntlrInput::tokenText($BINARY_LITERAL) ); + cargs[index].push_back( std::vector< CVC4::Type >() ); } | symbol[name,CHECK_NONE,SYM_VARIABLE] { if( name[0] == '-' ){ //hack for unary minus Debug("parser-sygus") << "Sygus grammar " << fun << " : unary minus integer literal " << name << std::endl; - ops.push_back(MK_CONST(Rational(name))); - cnames.push_back( name ); - cargs.push_back( std::vector< CVC4::Type >() ); - }else{ + ops[index].push_back(MK_CONST(Rational(name))); + cnames[index].push_back( name ); + cargs[index].push_back( std::vector< CVC4::Type >() ); + }else if( PARSER_STATE->isDeclared(name,SYM_VARIABLE) ){ Debug("parser-sygus") << "Sygus grammar " << fun << " : symbol " << name << std::endl; Expr bv = PARSER_STATE->getVariable(name); - ops.push_back(bv); - cnames.push_back( name ); - cargs.push_back( std::vector< CVC4::Type >() ); + ops[index].push_back(bv); + cnames[index].push_back( name ); + cargs[index].push_back( std::vector< CVC4::Type >() ); + }else{ + //prepend function name to base sorts when reading an operator + if( gtermType==0 ){ + std::stringstream ss; + ss << fun << "_" << name; + name = ss.str(); + } + if( PARSER_STATE->isDeclared(name, SYM_SORT) ){ + Debug("parser-sygus") << "Sygus grammar " << fun << " : nested sort " << name << std::endl; + ret = PARSER_STATE->getSort(name); + }else{ + Debug("parser-sygus") << "Sygus grammar " << fun << " : unresolved " << name << std::endl; + ret = PARSER_STATE->mkUnresolvedType(name); + } } } ; -- 2.30.2