diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-22 13:08:31 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-22 13:08:31 -0500 |
commit | cdf7aacd6b682645cf1a2bc609db005b2f4dafc7 (patch) | |
tree | cc7d7885d1fed270d6601703a9a03d2501534629 /src/smt | |
parent | d35a5a1d8072a662aa230319fbfc1611bb918ccf (diff) |
Make sygus infer find function definitions (#1951)
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 37 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 16 |
2 files changed, 41 insertions, 12 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 82147c094..36792e3c0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2701,7 +2701,9 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node // otherwise expand it bool doExpand = k == kind::APPLY; if( !doExpand ){ - if( options::macrosQuant() ){ + // options that assign substitutions to APPLY_UF + if (options::macrosQuant() || options::sygusInference()) + { //expand if we have inferred an operator corresponds to a defined function doExpand = k==kind::APPLY_UF && d_smt.isDefinedFunction( n.getOperator().toExpr() ); } @@ -4004,17 +4006,7 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertions : " << d_assertions.size() << endl; - if (options::sygusInference()) - { - // try recast as sygus - quantifiers::SygusInference si; - if (si.simplify(d_assertions.ref())) - { - Trace("smt-proc") << "...converted to sygus conjecture." << std::endl; - d_smt.d_globalNegation = !d_smt.d_globalNegation; - } - } - else if (options::globalNegate()) + if (options::globalNegate()) { // global negation of the formula quantifiers::GlobalNegate gn; @@ -4211,6 +4203,15 @@ void SmtEnginePrivate::processAssertions() { d_smt.d_fmfRecFunctionsDefined->push_back( f ); } } + if (options::sygusInference()) + { + // try recast as sygus + quantifiers::SygusInference si; + if (si.simplify(d_assertions.ref())) + { + Trace("smt-proc") << "...converted to sygus conjecture." << std::endl; + } + } Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << endl; } @@ -5573,6 +5574,18 @@ void SmtEngine::printSynthSolution( std::ostream& out ) { } } +void SmtEngine::getSynthSolutions(std::map<Expr, Expr>& sol_map) +{ + SmtScope smts(this); + map<Node, Node> sol_mapn; + Assert(d_theoryEngine != nullptr); + d_theoryEngine->getSynthSolutions(sol_mapn); + for (std::pair<const Node, Node>& s : sol_mapn) + { + sol_map[s.first.toExpr()] = s.second.toExpr(); + } +} + Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) { SmtScope smts(this); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 83300afc9..dd1d1b88a 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -656,6 +656,22 @@ class CVC4_PUBLIC SmtEngine { void printSynthSolution( std::ostream& out ); /** + * Get synth solution + * + * This function adds entries to sol_map that map functions-to-synthesize with + * their solutions, for all active conjectures. This should be called + * immediately after the solver answers unsat for sygus input. + * + * Specifically, given a sygus conjecture of the form + * exists x1...xn. forall y1...yn. P( x1...xn, y1...yn ) + * where x1...xn are second order bound variables, we map each xi to + * lambda term in sol_map such that + * forall y1...yn. P( sol_map[x1]...sol_map[xn], y1...yn ) + * is a valid formula. + */ + void getSynthSolutions(std::map<Expr, Expr>& sol_map); + + /** * Do quantifier elimination. * * This function takes as input a quantified formula e |