summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/run-script-casc25-tff20
-rw-r--r--src/parser/smt2/Smt2.g19
-rw-r--r--src/parser/smt2/smt2.cpp108
-rw-r--r--src/parser/smt2/smt2.h3
-rw-r--r--src/smt/smt_engine.cpp3
-rw-r--r--src/theory/quantifiers/ce_guided_single_inv.cpp2
-rw-r--r--src/theory/quantifiers/options2
-rw-r--r--src/util/datatype.cpp9
-rw-r--r--src/util/datatype.h5
-rw-r--r--test/regress/regress0/sygus/Makefile.am4
-rw-r--r--test/regress/regress0/sygus/no-syntax-test-no-si.sy14
-rw-r--r--test/regress/regress0/sygus/no-syntax-test.sy15
12 files changed, 181 insertions, 23 deletions
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<Expr> > 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<DatatypeType> datatypeTypes = PARSER_STATE->mkMutualDatatypeTypes(datatypes);
seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes));
@@ -794,7 +800,6 @@ sygusGTerm[std::string& fun, std::vector<CVC4::Expr>& ops, std::vector<std::stri
cargs.pop_back();
Debug("parser-sygus") << "Make constructors for Constant/Variable of type " << t << std::endl;
if( gtermType==1 ){
- //PARSER_STATE->parseError(std::string("Constant/Variable in sygus not supported."));
std::vector< Expr > consts;
PARSER_STATE->mkSygusConstantsForType( t, consts );
for( unsigned i=0; i<consts.size(); i++ ){
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 10e742d45..e837980bd 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -496,7 +496,113 @@ void Smt2::includeFile(const std::string& filename) {
}
}
-
+void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes,
+ std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> 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<Expr>());
+ std::vector<std::string> cnames;
+ std::vector<std::vector<CVC4::Type> > cargs;
+ //variables
+ for( unsigned i=0; i<sygus_vars.size(); i++ ){
+ if( sygus_vars[i].getType()==range ){
+ std::stringstream ss;
+ ss << sygus_vars[i];
+ Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
+ ops.back().push_back( sygus_vars[i] );
+ cnames.push_back( ss.str() );
+ cargs.push_back( std::vector< CVC4::Type >() );
+ }
+ }
+ //constants
+ std::vector< Expr > consts;
+ mkSygusConstantsForType( range, consts );
+ for( unsigned i=0; i<consts.size(); i++ ){
+ std::stringstream ss;
+ ss << consts[i];
+ Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
+ ops.back().push_back( consts[i] );
+ 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));
+ 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<Expr>());
+ 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<CVC4::Expr>& 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<CVC4::Datatype>& datatypes,
+ std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars );
+
void mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& 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)
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback