From edd8886e56c8bb84f3fd85fc6f697d870bc0a3b7 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 26 Jan 2015 13:11:01 +0100 Subject: [PATCH] Output solutions for synthesis conjectures with --dump-synth. Minor refactor of previous commit. --- src/expr/command.cpp | 38 ++++++++++ src/expr/command.h | 13 ++++ src/main/command_executor.cpp | 3 + src/main/command_executor_portfolio.cpp | 3 + src/parser/smt2/Smt2.g | 2 +- src/smt/options | 2 + src/smt/smt_engine.cpp | 7 ++ src/smt/smt_engine.h | 5 ++ src/theory/datatypes/datatypes_sygus.cpp | 31 +-------- src/theory/datatypes/datatypes_sygus.h | 13 +--- .../quantifiers/ce_guided_instantiation.cpp | 69 ++++++++++++++++--- .../quantifiers/ce_guided_instantiation.h | 9 ++- src/theory/quantifiers_engine.cpp | 8 +++ src/theory/quantifiers_engine.h | 2 + src/theory/theory_engine.cpp | 8 +++ src/theory/theory_engine.h | 5 ++ src/util/datatype.cpp | 7 +- src/util/datatype.h | 11 ++- 18 files changed, 182 insertions(+), 54 deletions(-) diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 242e018f6..1c7c1d171 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -1187,6 +1187,44 @@ std::string GetInstantiationsCommand::getCommandName() const throw() { return "get-instantiations"; } +/* class GetSynthSolutionCommand */ + +GetSynthSolutionCommand::GetSynthSolutionCommand() throw() { +} + +void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_smtEngine = smtEngine; + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +void GetSynthSolutionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + d_smtEngine->printSynthSolution(out); + } +} + +Command* GetSynthSolutionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetSynthSolutionCommand* c = new GetSynthSolutionCommand(); + c->d_smtEngine = d_smtEngine; + return c; +} + +Command* GetSynthSolutionCommand::clone() const { + GetSynthSolutionCommand* c = new GetSynthSolutionCommand(); + c->d_smtEngine = d_smtEngine; + return c; +} + +std::string GetSynthSolutionCommand::getCommandName() const throw() { + return "get-instantiations"; +} + /* class GetUnsatCoreCommand */ GetUnsatCoreCommand::GetUnsatCoreCommand() throw() { diff --git a/src/expr/command.h b/src/expr/command.h index cfa00bff4..9165961fb 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -610,6 +610,19 @@ public: std::string getCommandName() const throw(); };/* class GetInstantiationsCommand */ +class CVC4_PUBLIC GetSynthSolutionCommand : public Command { +protected: + SmtEngine* d_smtEngine; +public: + GetSynthSolutionCommand() throw(); + ~GetSynthSolutionCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetSynthSolutionCommand */ + class CVC4_PUBLIC GetUnsatCoreCommand : public Command { protected: UnsatCore d_result; diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 52522d591..460274515 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -139,6 +139,9 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) res.asSatisfiabilityResult() == Result::UNSAT ) ) { g = new GetInstantiationsCommand(); } + if( d_options[options::dumpSynth] && res.asSatisfiabilityResult() == Result::UNSAT ){ + g = new GetSynthSolutionCommand(); + } if( d_options[options::dumpUnsatCores] && res.asSatisfiabilityResult() == Result::UNSAT ) { g = new GetUnsatCoreCommand(); } diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 610902270..e4effd239 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -378,6 +378,9 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) d_result.asSatisfiabilityResult() == Result::UNSAT ) ) { Command* gi = new GetInstantiationsCommand(); status = doCommandSingleton(gi); + } else if( d_options[options::dumpSynth] && d_result.asSatisfiabilityResult() == Result::UNSAT ){ + Command* gi = new GetSynthSolutionCommand(); + status = doCommandSingleton(gi); } else if( d_options[options::dumpUnsatCores] && d_result.asSatisfiabilityResult() == Result::UNSAT ) { Command* guc = new GetUnsatCoreCommand(); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index e536ed7cc..3fa27e474 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -600,7 +600,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] std::string dname = ss.str(); sorts.push_back(t); datatypes.push_back(Datatype(dname)); - datatypes.back().setSygusType( t ); + datatypes.back().setSygus( t, terms[0] ); ops.push_back(std::vector()); cnames.push_back(std::vector()); cargs.push_back(std::vector >()); diff --git a/src/smt/options b/src/smt/options index 20dd5b7d5..593fc4887 100644 --- a/src/smt/options +++ b/src/smt/options @@ -37,6 +37,8 @@ option dumpProofs --dump-proofs bool :default false :link --proof output proofs after every UNSAT/VALID response option dumpInstantiations --dump-instantiations bool :default false output instantiations of quantified formulas after every UNSAT/VALID response +option dumpSynth --dump-synth bool :default false + output solution for synthesis conjectures after every UNSAT/VALID response option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" turn on unsat core generation option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6732b3dc7..94efd8a75 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4155,6 +4155,13 @@ void SmtEngine::printInstantiations( std::ostream& out ) { } } +void SmtEngine::printSynthSolution( std::ostream& out ) { + SmtScope smts(this); + if( d_theoryEngine ){ + d_theoryEngine->printSynthSolution( out ); + } +} + vector SmtEngine::getAssertions() throw(ModalException) { SmtScope smts(this); finalOptionsAreSet(); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index a39d2a7b5..7c5c45e42 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -520,6 +520,11 @@ public: */ void printInstantiations( std::ostream& out ); + /** + * 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 diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 9bfccc34e..bf17cf5e4 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -439,17 +439,6 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype& if( isGenericRedundant( tnnp, g ) ){ rem = true; } - /* - Node nr = NodeManager::currentNM()->mkNode( parentKind, dt[j].getSygusOp(), dto[i].getSygusOp() ); - Node nrr = Rewriter::rewrite( nr ); - Trace("sygus-split-debug") << " Test constant args : " << nr << " rewrites to " << nrr << std::endl; - //based on rewriting - // if rewriting the two arguments gives an operator that is in the parent syntax, remove the redundancy - if( hasOp( tnnp, nrr ) ){ - Trace("sygus-nf") << "* Sygus norm : simplify based on rewrite " << nr << " -> " << nrr << std::endl; - rem = true; - } - */ } } if( rem ){ @@ -598,6 +587,8 @@ Node SygusSplit::getTypeMaxValue( TypeNode tn ) { return it->second; } } + +//this function gets all easy redundant cases, before consulting rewriters bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt, TypeNode tn, TypeNode tnp, Kind k, Kind parent, int arg ) { Assert( hasKind( tn, k ) ); Assert( hasKind( tnp, parent ) ); @@ -648,7 +639,6 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt if( parent==UMINUS ){ if( k==PLUS ){ nk = PLUS;reqk = UMINUS; - }else if( k==MINUS ){ } } if( parent==BITVECTOR_NEG ){ @@ -712,15 +702,10 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt } } } - - /* - if( parent==MINUS ){ - - } - */ return true; } +//this function gets all easy redundant cases, before consulting rewriters bool SygusSplit::considerSygusSplitConst( const Datatype& dt, const Datatype& pdt, TypeNode tn, TypeNode tnp, Node c, Kind parent, int arg ) { Assert( hasConst( tn, c ) ); Assert( hasKind( tnp, parent ) ); @@ -741,16 +726,6 @@ bool SygusSplit::considerSygusSplitConst( const Datatype& dt, const Datatype& pd return false; } } - //single argument rewrite - if( pdt[pc].getNumArgs()==1 ){ - Node cr = NodeManager::currentNM()->mkNode( parent, c ); - cr = Rewriter::rewrite( cr ); - Trace("sygus-split-debug") << " " << parent << " applied to " << c << " rewrites to " << cr << std::endl; - if( hasConst( tnp, cr ) ){ - return false; - } - } - return true; } diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index 76ccabd4d..c638e5da6 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -24,18 +24,9 @@ #include "context/cdchunk_list.h" namespace CVC4 { -namespace theory { +namespace theory { namespace datatypes { - -//class SygusVarTrie -//{ -//public: -// // datatype, constructor, argument -// std::map< Node, std::map< int, SygusVarTrie > > d_children; -// std::map< TypeNode, Node > d_var; -//}; - - + class SygusSplit { private: diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index bb53c9cfb..669cd8fa9 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -18,6 +18,8 @@ #include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/datatypes/datatypes_rewriter.h" +#include "util/datatype.h" using namespace CVC4; using namespace CVC4::kind; @@ -246,7 +248,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { if( getTermDatabase()->isQAttrSygus( q ) ){ std::vector< Node > model_values; - if( getModelValues( conj->d_candidates, model_values ) ){ + if( getModelValues( conj, conj->d_candidates, model_values ) ){ //check if we must apply fairness lemmas std::vector< Node > lems; if( options::ceGuidedInstFair()==CEGQI_FAIR_UF_DT_SIZE ){ @@ -300,15 +302,10 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { } }else if( getTermDatabase()->isQAttrSynthesis( q ) ){ - Trace("cegqi-engine") << " * Value is : "; std::vector< Node > model_terms; - for( unsigned i=0; id_candidates.size(); i++ ){ - Node t = getModelTerm( conj->d_candidates[i] ); - model_terms.push_back( t ); - Trace("cegqi-engine") << conj->d_candidates[i] << " -> " << t << " "; + if( getModelValues( conj, conj->d_candidates, model_terms ) ){ + d_quantEngine->addInstantiation( q, model_terms, false ); } - Trace("cegqi-engine") << std::endl; - d_quantEngine->addInstantiation( q, model_terms, false ); } }else{ Trace("cegqi-engine") << " *** Refine candidate phase..." << std::endl; @@ -323,7 +320,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { Assert( !conj->d_inner_vars_disj[k].empty() ); Assert( conj->d_inner_vars_disj[k].size()==getTermDatabase()->d_skolem_constants[ce_q].size() ); std::vector< Node > model_values; - if( getModelValues( getTermDatabase()->d_skolem_constants[ce_q], model_values ) ){ + if( getModelValues( NULL, getTermDatabase()->d_skolem_constants[ce_q], model_values ) ){ //candidate refinement : the next candidate must satisfy the counterexample found for the current model of the candidate Node inst_ce_refine = conj->d_base_disj[k][0][1].substitute( conj->d_inner_vars_disj[k].begin(), conj->d_inner_vars_disj[k].end(), model_values.begin(), model_values.end() ); @@ -355,7 +352,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { } } -bool CegInstantiation::getModelValues( std::vector< Node >& n, std::vector< Node >& v ) { +bool CegInstantiation::getModelValues( CegConjecture * conj, std::vector< Node >& n, std::vector< Node >& v ) { bool success = true; Trace("cegqi-engine") << " * Value is : "; for( unsigned i=0; i& n, std::vector< Node if( nv.isNull() ){ success = false; } + if( conj ){ + conj->d_candidate_inst[i].push_back( nv ); + } } Trace("cegqi-engine") << std::endl; return success; @@ -449,4 +449,53 @@ void CegInstantiation::getMeasureLemmas( Node n, Node v, std::vector< Node >& le } } +void CegInstantiation::printSynthSolution( std::ostream& out ) { + if( d_conj ){ + out << "Solution:" << std::endl; + for( unsigned i=0; id_candidates.size(); i++ ){ + std::stringstream ss; + ss << d_conj->d_quant[0][i]; + std::string f(ss.str()); + f.erase(f.begin()); + out << "(define-fun f "; + TypeNode tn = d_conj->d_quant[0][i].getType(); + Assert( datatypes::DatatypesRewriter::isTypeDatatype( tn ) ); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + Assert( dt.isSygus() ); + out << dt.getSygusVarList() << " "; + out << dt.getSygusType() << " "; + if( d_conj->d_candidate_inst[i].empty() ){ + out << "?"; + }else{ + printSygusTerm( out, d_conj->d_candidate_inst[i].back() ); + } + out << ")" << std::endl; + } + } +} + +void CegInstantiation::printSygusTerm( std::ostream& out, Node n ) { + if( n.getKind()==APPLY_CONSTRUCTOR ){ + TypeNode tn = n.getType(); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + if( dt.isSygus() ){ + int cIndex = Datatype::indexOf( n.getOperator().toExpr() ); + Assert( !dt[cIndex].getSygusOp().isNull() ); + if( n.getNumChildren()>0 ){ + out << "("; + } + out << dt[cIndex].getSygusOp(); + if( n.getNumChildren()>0 ){ + for( unsigned i=0; i d_inner_vars; std::vector< std::vector< Node > > d_inner_vars_disj; + /** list of terms we have instantiated candidates with */ + std::map< int, std::vector< Node > > d_candidate_inst; /** initialize guard */ void initializeGuard( QuantifiersEngine * qe ); /** measure term */ @@ -99,11 +101,14 @@ private: /** check conjecture */ void checkCegConjecture( CegConjecture * conj ); /** get model values */ - bool getModelValues( std::vector< Node >& n, std::vector< Node >& v ); + bool getModelValues( CegConjecture * conj, std::vector< Node >& n, std::vector< Node >& v ); /** get model value */ Node getModelValue( Node n ); /** get model term */ Node getModelTerm( Node n ); +private: + /** print sygus term */ + void printSygusTerm( std::ostream& out, Node n ); public: CegInstantiation( QuantifiersEngine * qe, context::Context* c ); public: @@ -118,6 +123,8 @@ public: Node getNextDecisionRequest(); /** Identify this module (for debugging, dynamic configuration, etc..) */ std::string identify() const { return "CegInstantiation"; } + /** print solution for synthesis conjectures */ + void printSynthSolution( std::ostream& out ); }; } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 2cf6002cd..7fb6c0bb7 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -924,6 +924,14 @@ void QuantifiersEngine::printInstantiations( std::ostream& out ) { } } +void QuantifiersEngine::printSynthSolution( std::ostream& out ) { + if( d_ceg_inst ){ + d_ceg_inst->printSynthSolution( out ); + }else{ + out << "Internal error : module for synth solution not found." << std::endl; + } +} + QuantifiersEngine::Statistics::Statistics(): d_num_quant("QuantifiersEngine::Num_Quantifiers", 0), d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0), diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index c533f4cbb..eb4470eec 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -303,6 +303,8 @@ public: public: /** print instantiations */ void printInstantiations( std::ostream& out ); + /** print solution for synthesis conjectures */ + void printSynthSolution( std::ostream& out ); /** statistics class */ class Statistics { public: diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 22bf37470..74a8fab73 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1224,6 +1224,14 @@ void TheoryEngine::printInstantiations( std::ostream& out ) { } } +void TheoryEngine::printSynthSolution( std::ostream& out ) { + if( d_quantEngine ){ + d_quantEngine->printSynthSolution( out ); + }else{ + out << "Internal error : synth solution not available when quantifiers are not present." << std::endl; + } +} + static Node mkExplanation(const std::vector& explanation) { std::set all; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 6360ea5fb..4f1a5163e 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -775,6 +775,11 @@ public: */ void printInstantiations( std::ostream& out ); + /** + * Print solution for synthesis conjectures found by ce_guided_instantiation module + */ + void printSynthSolution( std::ostream& out ); + /** * Forwards an entailment check according to the given theoryOfMode. * See theory.h for documentation on entailmentCheck(). diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index fad2719f4..06a8187f2 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -141,10 +141,11 @@ void Datatype::addConstructor(const DatatypeConstructor& c) { } -void Datatype::setSygusType( Type st ){ +void Datatype::setSygus( Type st, Expr bvl ){ CheckArgument(!d_resolved, this, "cannot set sygus type to a finalized Datatype"); d_sygus_type = st; + d_sygus_bvl = bvl; } @@ -428,6 +429,10 @@ Type Datatype::getSygusType() const { return d_sygus_type; } +Expr Datatype::getSygusVarList() const { + return d_sygus_bvl; +} + bool Datatype::involvesExternalType() const{ return d_involvesExt; } diff --git a/src/util/datatype.h b/src/util/datatype.h index b91348cdb..adb423c96 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -459,7 +459,9 @@ private: bool d_resolved; Type d_self; bool d_involvesExt; + /** information for sygus */ Type d_sygus_type; + Expr d_sygus_bvl; // "mutable" because computing the cardinality can be expensive, // and so it's computed just once, on demand---this is the cache @@ -517,8 +519,11 @@ public: */ void addConstructor(const DatatypeConstructor& c); - /** set the sygus type of this datatype */ - void setSygusType( Type st ); + /** set the sygus information of this datatype + * st : the builtin type for this grammar + * bvl : the list of arguments for the synth-fun + */ + void setSygus( Type st, Expr bvl ); /** Get the name of this Datatype. */ inline std::string getName() const throw(); @@ -635,6 +640,8 @@ public: /** get sygus type */ Type getSygusType() const; + /** get sygus var list */ + Expr getSygusVarList() const; /** * Get whether this datatype involves an external type. If so, -- 2.30.2