From: ajreynol Date: Fri, 31 Jul 2015 08:32:34 +0000 (+0200) Subject: Sygus support for inductive datatypes. X-Git-Tag: cvc5-1.0.0~6263 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bf7f7d6960f6e03e90880dd3da9ff1bf00943cf3;p=cvc5.git Sygus support for inductive datatypes. --- diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 1564e6f3e..1ce7c4aff 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -606,6 +606,8 @@ sygusCommand returns [CVC4::Command* cmd = NULL] Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED); $cmd = new DefineFunctionCommand(name, func, terms, expr); } + | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd] + | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd] | /* synth-fun */ ( SYNTH_FUN_TOK | SYNTH_INV_TOK { range = EXPR_MANAGER->booleanType(); } ) { PARSER_STATE->checkThatLogicIsSet(); } symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE] @@ -912,7 +914,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] // fail, but we need an operator to continue here.. Debug("parser-sygus") << "Sygus grammar " << fun; Debug("parser-sygus") << " : op (declare=" << PARSER_STATE->isDeclared(name) << ", define=" << PARSER_STATE->isDefinedFunction(name) << ") : " << name << std::endl; - if( !PARSER_STATE->isDefinedFunction(name) ){ + if( !PARSER_STATE->isDeclared(name) && !PARSER_STATE->isDefinedFunction(name) ){ PARSER_STATE->parseError(std::string("Functions in sygus grammars must be defined.")); } sgt.d_name = name; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 9ee6d24b4..0500c9316 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -522,9 +522,13 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin for( unsigned i=0; i& let_vars, std::stringstream ss; ss << datatypes[index].getName() << "_let"; Expr let_func = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED); + d_sygus_defined_funs.push_back( let_func ); preemptCommand( new DefineFunctionCommand(ss.str(), let_func, let_define_args, let_body) ); ops[index].pop_back(); @@ -1180,6 +1185,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, //replace operator and name ops[i] = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED); cnames[i] = ss.str(); + d_sygus_defined_funs.push_back( ops[i] ); preemptCommand( new DefineFunctionCommand(ss.str(), ops[i], let_args, let_body) ); addSygusDatatypeConstructor( dt, ops[i], cnames[i], cargs[i], let_body, let_args, 0 ); }else{ @@ -1216,6 +1222,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, std::stringstream ssid; ssid << unresolved_gterm_sym[i] << "_id"; Expr id_op = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED); + d_sygus_defined_funs.push_back( id_op ); preemptCommand( new DefineFunctionCommand(ssid.str(), id_op, let_args, let_body) ); //make the sygus argument list std::vector< Type > id_carg; @@ -1310,15 +1317,35 @@ Expr Smt2::getSygusAssertion( std::vector& datatypeTypes, std::vec for(size_t k = 0; k < builtApply.size(); ++k) { } Expr builtTerm; - //if( ops[i][j].getKind() == kind::BUILTIN ){ - if( !builtApply.empty() ){ - if( ops[i][j].getKind() != kind::BUILTIN ){ - builtTerm = getExprManager()->mkExpr(kind::APPLY, ops[i][j], builtApply); + Debug("parser-sygus") << "...operator is : " << ops[i][j] << ", type = " << ops[i][j].getType() << ", kind = " << ops[i][j].getKind() << ", is defined = " << isDefinedFunction( ops[i][j] ) << std::endl; + if( ops[i][j].getKind() != kind::BUILTIN ){ + Kind ok = kind::UNDEFINED_KIND; + if( isDefinedFunction( ops[i][j] ) || std::find( d_sygus_defined_funs.begin(), d_sygus_defined_funs.end(), ops[i][j] )!=d_sygus_defined_funs.end() ){ + ok = kind::APPLY; }else{ - builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply); + Type t = ops[i][j].getType(); + if( t.isConstructor() ){ + ok = kind::APPLY_CONSTRUCTOR; + }else if( t.isSelector() ){ + ok = kind::APPLY_SELECTOR; + }else if( t.isTester() ){ + ok = kind::APPLY_TESTER; + }else{ + ok = getExprManager()->operatorToKind( ops[i][j] ); + } + } + Debug("parser-sygus") << "...processed operator kind : " << ok << std::endl; + if( ok!=kind::UNDEFINED_KIND ){ + builtTerm = getExprManager()->mkExpr(ok, ops[i][j], builtApply); + }else{ + builtTerm = ops[i][j]; } }else{ - builtTerm = ops[i][j]; + if( !builtApply.empty() ){ + builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply); + }else{ + builtTerm = ops[i][j]; + } } Debug("parser-sygus") << "...made built term " << builtTerm << std::endl; Expr assertion = getExprManager()->mkExpr(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm); diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index c88f7cd8f..c8b89799c 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -35,7 +35,7 @@ namespace CVC4 { class SExpr; namespace parser { - + class Smt2 : public Parser { friend class ParserBuilder; @@ -180,7 +180,7 @@ public: void mkSygusConstantsForType( const Type& type, std::vector& ops ); - void processSygusGTerm( CVC4::SygusGTerm& sgt, int index, + void processSygusGTerm( CVC4::SygusGTerm& sgt, int index, std::vector< CVC4::Datatype >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector >& ops, @@ -188,10 +188,10 @@ public: std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, std::vector< bool >& allow_const, std::vector< std::vector< std::string > >& unresolved_gterm_sym, - std::vector& sygus_vars, - std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, + std::vector& sygus_vars, + std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, CVC4::Type& ret, bool isNested = false ); - + static bool pushSygusDatatypeDef( Type t, std::string& dname, std::vector< CVC4::Datatype >& datatypes, std::vector< CVC4::Type>& sorts, @@ -208,12 +208,12 @@ public: std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, std::vector< bool >& allow_const, std::vector< std::vector< std::string > >& unresolved_gterm_sym ); - - void setSygusStartIndex( std::string& fun, int startIndex, + + void setSygusStartIndex( std::string& fun, int startIndex, std::vector< CVC4::Datatype >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector >& ops ); - + void addSygusFun(const std::string& fun, Expr eval) { d_sygusFuns.push_back(std::make_pair(fun, eval)); } @@ -222,7 +222,7 @@ public: void mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, std::vector& cnames, std::vector< std::vector< CVC4::Type > >& cargs, - std::vector& unresolved_gterm_sym, + std::vector& unresolved_gterm_sym, std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ); // i is index in datatypes/ops @@ -230,7 +230,7 @@ public: Expr getSygusAssertion( std::vector& datatypeTypes, std::vector< std::vector >& ops, std::map& evals, std::vector& terms, Expr eval, const Datatype& dt, size_t i, size_t j ); - + void addSygusConstraint(Expr constraint) { @@ -311,9 +311,11 @@ private: 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; - + //auxiliary define-fun functions introduced for production rules + std::vector< CVC4::Expr > d_sygus_defined_funs; + void collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusArgs, std::vector< CVC4::Expr >& builtinArgs ); - + void addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs, CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args ); @@ -327,16 +329,16 @@ private: std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret ); - void processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, int index, + void processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, int index, std::vector< CVC4::Datatype >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector >& ops, std::vector< std::vector >& cnames, std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, - std::vector& sygus_vars, + std::vector& sygus_vars, std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr ); - + void addArithmeticOperators(); void addBitvectorOperators(); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index fa145813c..ce8f68c09 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1787,6 +1787,12 @@ void SmtEngine::defineFunction(Expr func, d_definedFunctions->insert(funcNode, def); } +bool SmtEngine::isDefinedFunction( Expr func ){ + Node nf = Node::fromExpr( func ); + Debug("smt") << "isDefined function " << nf << "?" << std::endl; + return d_definedFunctions->find(nf) != d_definedFunctions->end(); +} + Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map& cache, bool expandOnly) throw(TypeCheckingException, LogicException, UnsafeInterruptException) { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index de9b8127d..db0809308 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -189,9 +189,9 @@ class CVC4_PUBLIC SmtEngine { *A vector of command definitions to be imported in the new *SmtEngine when checking unsat-cores. */ -#ifdef CVC4_PROOF +#ifdef CVC4_PROOF std::vector d_defineCommands; -#endif +#endif /** * The logic we're in. */ @@ -455,6 +455,9 @@ public: const std::vector& formals, Expr formula); + /** is defined function */ + bool isDefinedFunction(Expr func); + /** * Add a formula to the current context: preprocess, do per-theory * setup, use processAssertionList(), asserting to T-solver for @@ -536,7 +539,7 @@ public: * Print solution for synthesis conjectures found by ce_guided_instantiation module */ void printSynthSolution( std::ostream& out ); - + /** * Get an unsatisfiable core (only if immediately preceded by an * UNSAT or VALID query). Only permitted if CVC4 was built with @@ -707,7 +710,7 @@ public: * Set print function in model */ void setPrintFuncInModel(Expr f, bool p); - + };/* class SmtEngine */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 37c7a4d57..132c55cd9 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1322,7 +1322,7 @@ Node TermDb::getVtsDelta( bool isFree, bool create ) { d_vts_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for virtual term substitution" ); } } - return isFree ? d_vts_delta_free : d_vts_delta; + return isFree ? d_vts_delta_free : d_vts_delta; } Node TermDb::getVtsInfinity( bool isFree, bool create ) { @@ -1832,10 +1832,12 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int if( op.getKind()==BUILTIN ){ ret = NodeManager::currentNM()->mkNode( op, children ); }else{ - if( children.size()==1 ){ + Kind ok = getOperatorKind( op ); + Trace("sygus-db") << "Operator kind is " << ok << std::endl; + if( children.size()==1 && ok==kind::UNDEFINED_KIND ){ ret = children[0]; }else{ - ret = NodeManager::currentNM()->mkNode( APPLY, children ); + ret = NodeManager::currentNM()->mkNode( ok, children ); /* Node n = NodeManager::currentNM()->mkNode( APPLY, children ); //must expand definitions @@ -2463,6 +2465,24 @@ void doStrReplace(std::string& str, const std::string& oldStr, const std::string } } +Kind TermDbSygus::getOperatorKind( Node op ) { + Assert( op.getKind()!=BUILTIN ); + if( smt::currentSmtEngine()->isDefinedFunction( op.toExpr() ) ){ + return APPLY; + }else{ + TypeNode tn = op.getType(); + if( tn.isConstructor() ){ + return APPLY_CONSTRUCTOR; + }else if( tn.isSelector() ){ + return APPLY_SELECTOR; + }else if( tn.isTester() ){ + return APPLY_TESTER; + }else{ + return NodeManager::operatorToKind( op ); + } + } +} + void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs ) { if( n.getKind()==APPLY_CONSTRUCTOR ){ TypeNode tn = n.getType(); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index ad206b470..23594d49a 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -518,6 +518,8 @@ public: Kind getComparisonKind( TypeNode tn ); Kind getPlusKind( TypeNode tn, bool is_neg = false ); bool doCompare( Node a, Node b, Kind k ); + /** get operator kind */ + static Kind getOperatorKind( Node op ); /** print sygus term */ static void printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs ); }; diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 9d7155f78..82ff67d41 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -43,7 +43,8 @@ TESTS = commutative.sy \ enum-test.sy \ no-syntax-test-bool.sy \ inv-example.sy \ - uminus_one.sy + uminus_one.sy \ + sygus-dt.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress0/sygus/sygus-dt.sy b/test/regress/regress0/sygus/sygus-dt.sy new file mode 100755 index 000000000..e842477e8 --- /dev/null +++ b/test/regress/regress0/sygus/sygus-dt.sy @@ -0,0 +1,16 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi --no-dump-synth + +(set-logic LIA) + +(declare-datatypes () ((List (cons (head Int) (tail List)) (nil)))) +(define-fun g ((x Int)) List (cons (+ x 1) nil)) +(define-fun i () List (cons 3 nil)) + +(synth-fun f ((x Int)) List ((Start List ((g StartInt) i (cons StartInt Start) (nil) (tail Start))) + (StartInt Int (x 0 1 (+ StartInt StartInt))))) + +(declare-var x Int) + +(constraint (= (f x) (cons x nil))) +(check-synth) \ No newline at end of file