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() {
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;
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();
}
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();
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<Expr>());
cnames.push_back(std::vector<std::string>());
cargs.push_back(std::vector<std::vector<CVC4::Type> >());
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"
}
}
+void SmtEngine::printSynthSolution( std::ostream& out ) {
+ SmtScope smts(this);
+ if( d_theoryEngine ){
+ d_theoryEngine->printSynthSolution( out );
+ }
+}
+
vector<Expr> SmtEngine::getAssertions() throw(ModalException) {
SmtScope smts(this);
finalOptionsAreSet();
*/
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
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 ){
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 ) );
if( parent==UMINUS ){
if( k==PLUS ){
nk = PLUS;reqk = UMINUS;
- }else if( k==MINUS ){
}
}
if( parent==BITVECTOR_NEG ){
}
}
}
-
- /*
- 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 ) );
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;
}
#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:
#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;
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 ){
}
}else if( getTermDatabase()->isQAttrSynthesis( q ) ){
- Trace("cegqi-engine") << " * Value is : ";
std::vector< Node > model_terms;
- for( unsigned i=0; i<conj->d_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;
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() );
}
}
-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.size(); i++ ){
if( nv.isNull() ){
success = false;
}
+ if( conj ){
+ conj->d_candidate_inst[i].push_back( nv );
+ }
}
Trace("cegqi-engine") << std::endl;
return success;
}
}
+void CegInstantiation::printSynthSolution( std::ostream& out ) {
+ if( d_conj ){
+ out << "Solution:" << std::endl;
+ for( unsigned i=0; i<d_conj->d_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<n.getNumChildren(); i++ ){
+ out << " ";
+ printSygusTerm( out, n[i] );
+ }
+ out << ")";
+ }
+ return;
+ }
+ }
+ out << n << std::endl;
+}
+
}
/** list of variables on inner quantification */
std::vector< Node > 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 */
/** 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:
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 );
};
}
}
}
+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),
public:
/** print instantiations */
void printInstantiations( std::ostream& out );
+ /** print solution for synthesis conjectures */
+ void printSynthSolution( std::ostream& out );
/** statistics class */
class Statistics {
public:
}
}
+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<NodeTheoryPair>& explanation) {
std::set<TNode> all;
*/
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().
}
-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;
}
return d_sygus_type;
}
+Expr Datatype::getSygusVarList() const {
+ return d_sygus_bvl;
+}
+
bool Datatype::involvesExternalType() const{
return d_involvesExt;
}
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
*/
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();
/** get sygus type */
Type getSygusType() const;
+ /** get sygus var list */
+ Expr getSygusVarList() const;
/**
* Get whether this datatype involves an external type. If so,
projects / cvc5.git / commitdiff