diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-09-08 20:16:27 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-08 20:16:27 -0500 |
commit | 25a24a74b0765713e3b11df9b7ea891fdda9523e (patch) | |
tree | eaaae51ad04de4b3d66d006d5f30e8e3a469ff93 /src | |
parent | 3daaf4c574aeb61cb0841f37c12051497a077dff (diff) | |
parent | 704fd545440023a0deaa328a9de9c11ac5fe963c (diff) |
Merge branch 'master' into rmStateOptionsrmStateOptions
Diffstat (limited to 'src')
-rw-r--r-- | src/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/proof/lfsc/lfsc_print_channel.cpp | 161 | ||||
-rw-r--r-- | src/proof/lfsc/lfsc_print_channel.h | 128 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_eval_unfold.cpp | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_eval_unfold.h | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_invariance.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_invariance.h | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_strat.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 63 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.h | 15 |
12 files changed, 306 insertions, 97 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5c898b654..4484f9447 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -182,6 +182,8 @@ libcvc5_add_sources( proof/lfsc/lfsc_list_sc_node_converter.h proof/lfsc/lfsc_node_converter.cpp proof/lfsc/lfsc_node_converter.h + proof/lfsc/lfsc_print_channel.cpp + proof/lfsc/lfsc_print_channel.h proof/lfsc/lfsc_util.cpp proof/lfsc/lfsc_util.h proof/method_id.cpp diff --git a/src/proof/lfsc/lfsc_print_channel.cpp b/src/proof/lfsc/lfsc_print_channel.cpp new file mode 100644 index 000000000..36fd8831b --- /dev/null +++ b/src/proof/lfsc/lfsc_print_channel.cpp @@ -0,0 +1,161 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Print channels for LFSC proofs. + */ + +#include "proof/lfsc/lfsc_print_channel.h" + +#include <sstream> + +#include "proof/lfsc/lfsc_util.h" + +namespace cvc5 { +namespace proof { + +LfscPrintChannelOut::LfscPrintChannelOut(std::ostream& out) : d_out(out) {} +void LfscPrintChannelOut::printNode(TNode n) +{ + d_out << " "; + printNodeInternal(d_out, n); +} + +void LfscPrintChannelOut::printTypeNode(TypeNode tn) +{ + d_out << " "; + printTypeNodeInternal(d_out, tn); +} + +void LfscPrintChannelOut::printHole() { d_out << " _ "; } +void LfscPrintChannelOut::printTrust(TNode res, PfRule src) +{ + d_out << std::endl << "(trust "; + printNodeInternal(d_out, res); + d_out << ") ; from " << src << std::endl; +} + +void LfscPrintChannelOut::printOpenRule(const ProofNode* pn) +{ + d_out << std::endl << "("; + printRule(d_out, pn); +} + +void LfscPrintChannelOut::printOpenLfscRule(LfscRule lr) +{ + d_out << std::endl << "(" << lr; +} + +void LfscPrintChannelOut::printCloseRule(size_t nparen) +{ + for (size_t i = 0; i < nparen; i++) + { + d_out << ")"; + } +} + +void LfscPrintChannelOut::printProofId(size_t id) +{ + d_out << " "; + printProofId(d_out, id); +} +void LfscPrintChannelOut::printAssumeId(size_t id) +{ + d_out << " "; + printAssumeId(d_out, id); +} + +void LfscPrintChannelOut::printEndLine() { d_out << std::endl; } + +void LfscPrintChannelOut::printNodeInternal(std::ostream& out, Node n) +{ + // due to use of special names in the node converter, we must clean symbols + std::stringstream ss; + n.toStream(ss, -1, 0, Language::LANG_SMTLIB_V2_6); + std::string s = ss.str(); + cleanSymbols(s); + out << s; +} + +void LfscPrintChannelOut::printTypeNodeInternal(std::ostream& out, TypeNode tn) +{ + // due to use of special names in the node converter, we must clean symbols + std::stringstream ss; + tn.toStream(ss, Language::LANG_SMTLIB_V2_6); + std::string s = ss.str(); + cleanSymbols(s); + out << s; +} + +void LfscPrintChannelOut::printRule(std::ostream& out, const ProofNode* pn) +{ + if (pn->getRule() == PfRule::LFSC_RULE) + { + const std::vector<Node>& args = pn->getArguments(); + out << getLfscRule(args[0]); + return; + } + // Otherwise, convert to lower case + std::stringstream ss; + ss << pn->getRule(); + std::string rname = ss.str(); + std::transform( + rname.begin(), rname.end(), rname.begin(), [](unsigned char c) { + return std::tolower(c); + }); + out << rname; +} + +void LfscPrintChannelOut::printId(std::ostream& out, size_t id) +{ + out << "__t" << id; +} + +void LfscPrintChannelOut::printProofId(std::ostream& out, size_t id) +{ + out << "__p" << id; +} + +void LfscPrintChannelOut::printAssumeId(std::ostream& out, size_t id) +{ + out << "__a" << id; +} + +void LfscPrintChannelOut::cleanSymbols(std::string& s) +{ + size_t start_pos = 0; + while ((start_pos = s.find("(_ ", start_pos)) != std::string::npos) + { + s.replace(start_pos, 3, "("); + start_pos += 1; + } + start_pos = 0; + while ((start_pos = s.find("__LFSC_TMP", start_pos)) != std::string::npos) + { + s.replace(start_pos, 10, ""); + } +} + +LfscPrintChannelPre::LfscPrintChannelPre(LetBinding& lbind) : d_lbind(lbind) {} + +void LfscPrintChannelPre::printNode(TNode n) { d_lbind.process(n); } +void LfscPrintChannelPre::printTrust(TNode res, PfRule src) +{ + d_lbind.process(res); +} + +void LfscPrintChannelPre::printOpenRule(const ProofNode* pn) +{ + +} + +} // namespace proof +} // namespace cvc5 diff --git a/src/proof/lfsc/lfsc_print_channel.h b/src/proof/lfsc/lfsc_print_channel.h new file mode 100644 index 000000000..655fa192c --- /dev/null +++ b/src/proof/lfsc/lfsc_print_channel.h @@ -0,0 +1,128 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Print channels for LFSC proofs. + */ + +#include "cvc5_private.h" + +#ifndef CVC4__PROOF__LFSC__LFSC_PRINT_CHANNEL_H +#define CVC4__PROOF__LFSC__LFSC_PRINT_CHANNEL_H + +#include <iostream> +#include <map> + +#include "expr/node.h" +#include "printer/let_binding.h" +#include "proof/lfsc/lfsc_util.h" +#include "proof/proof_node.h" + +namespace cvc5 { +namespace proof { + +/** + * LFSC proofs are printed in two phases: the first phase computes the + * letification of terms in the proof as well as other information that is + * required for printing the preamble of the proof. The second phase prints the + * proof to an output stream. This is the base class for these two phases. + */ +class LfscPrintChannel +{ + public: + LfscPrintChannel() {} + virtual ~LfscPrintChannel() {} + /** Print node n */ + virtual void printNode(TNode n) {} + /** Print type node n */ + virtual void printTypeNode(TypeNode tn) {} + /** Print a hole */ + virtual void printHole() {} + /** + * Print an application of the trusting the result res, whose source is the + * given proof rule. + */ + virtual void printTrust(TNode res, PfRule src) {} + /** Print the opening of the rule of proof rule pn, e.g. "(and_elim ". */ + virtual void printOpenRule(const ProofNode* pn) {} + /** Print the opening of LFSC rule lr, e.g. "(cong " */ + virtual void printOpenLfscRule(LfscRule lr) {} + /** Print the closing of # nparen proof rules */ + virtual void printCloseRule(size_t nparen = 1) {} + /** Print a letified proof with the given identifier */ + virtual void printProofId(size_t id) {} + /** Print a proof assumption with the given identifier */ + virtual void printAssumeId(size_t id) {} + /** Print an end line */ + virtual void printEndLine() {} +}; + +/** Prints the proof to output stream d_out */ +class LfscPrintChannelOut : public LfscPrintChannel +{ + public: + LfscPrintChannelOut(std::ostream& out); + void printNode(TNode n) override; + void printTypeNode(TypeNode tn) override; + void printHole() override; + void printTrust(TNode res, PfRule src) override; + void printOpenRule(const ProofNode* pn) override; + void printOpenLfscRule(LfscRule lr) override; + void printCloseRule(size_t nparen = 1) override; + void printProofId(size_t id) override; + void printAssumeId(size_t id) override; + void printEndLine() override; + //------------------- helper methods + /** + * Print node to stream in the expected format of LFSC. + */ + static void printNodeInternal(std::ostream& out, Node n); + /** + * Print type node to stream in the expected format of LFSC. + */ + static void printTypeNodeInternal(std::ostream& out, TypeNode tn); + static void printRule(std::ostream& out, const ProofNode* pn); + static void printId(std::ostream& out, size_t id); + static void printProofId(std::ostream& out, size_t id); + static void printAssumeId(std::ostream& out, size_t id); + //------------------- end helper methods + private: + /** + * Replaces "(_ " with "(" to eliminate indexed symbols + * Replaces "__LFSC_TMP" with "" + */ + static void cleanSymbols(std::string& s); + /** The output stream */ + std::ostream& d_out; +}; + +/** + * Run on the proof before it is printed, and does two preparation steps: + * - Computes the letification of nodes that appear in the proof. + * - Computes the set of DSL rules that appear in the proof. + */ +class LfscPrintChannelPre : public LfscPrintChannel +{ + public: + LfscPrintChannelPre(LetBinding& lbind); + void printNode(TNode n) override; + void printTrust(TNode res, PfRule src) override; + void printOpenRule(const ProofNode* pn) override; + + private: + /** The let binding */ + LetBinding& d_lbind; +}; + +} // namespace proof +} // namespace cvc5 + +#endif diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 8d1bfd9b6..708bffe80 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -345,7 +345,7 @@ void Cegis::addRefinementLemma(Node lem) d_rl_vals.end()); } // rewrite with extended rewriter - slem = extendedRewrite(slem); + slem = d_tds->rewriteNode(slem); // collect all variables in slem expr::getSymbols(slem, d_refinement_lemma_vars); std::vector<Node> waiting; @@ -509,7 +509,7 @@ bool Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, Node lemcs = lem.substitute(vs.begin(), vs.end(), ms.begin(), ms.end()); Trace("sygus-cref-eval2") << "...under substitution it is : " << lemcs << std::endl; - Node lemcsu = vsit.doEvaluateWithUnfolding(d_tds, lemcs); + Node lemcsu = d_tds->rewriteNode(lemcs); Trace("sygus-cref-eval2") << "...after unfolding is : " << lemcsu << std::endl; if (lemcsu.isConst() && !lemcsu.getConst<bool>()) diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index 0ef1e7f17..7af1ef45b 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -180,7 +180,7 @@ void SygusEvalUnfold::registerModelValue(Node a, Node conj = nm->mkNode(DT_SYGUS_EVAL, eval_children); eval_children[0] = vn; Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children); - res = d_tds->evaluateWithUnfolding(eval_fun); + res = d_tds->rewriteNode(eval_fun); Trace("sygus-eval-unfold") << "Evaluate with unfolding returns " << res << std::endl; esit.init(conj, n, res); @@ -324,13 +324,6 @@ Node SygusEvalUnfold::unfold(Node en, return ret; } -Node SygusEvalUnfold::unfold(Node en) -{ - std::map<Node, Node> vtm; - std::vector<Node> exp; - return unfold(en, vtm, exp, false, false); -} - } // namespace quantifiers } // namespace theory } // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.h b/src/theory/quantifiers/sygus/sygus_eval_unfold.h index bb181996a..c30d4dae7 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.h +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h @@ -122,11 +122,6 @@ class SygusEvalUnfold std::vector<Node>& exp, bool track_exp = true, bool doRec = false); - /** - * Same as above, but without explanation tracking. This is used for concrete - * evaluation heads - */ - Node unfold(Node en); private: /** sygus term database associated with this utility */ diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp index 29557fe5c..8048330e4 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.cpp +++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp @@ -49,11 +49,6 @@ void EvalSygusInvarianceTest::init(Node conj, Node var, Node res) d_result = res; } -Node EvalSygusInvarianceTest::doEvaluateWithUnfolding(TermDbSygus* tds, Node n) -{ - return tds->evaluateWithUnfolding(n, d_visited); -} - bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x) { TNode tnvn = nvn; @@ -61,7 +56,7 @@ bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x) for (const Node& c : d_terms) { Node conj_subs = c.substitute(d_var, tnvn, cache); - Node conj_subs_unfold = doEvaluateWithUnfolding(tds, conj_subs); + Node conj_subs_unfold = tds->rewriteNode(conj_subs); Trace("sygus-cref-eval2-debug") << " ...check unfolding : " << conj_subs_unfold << std::endl; Trace("sygus-cref-eval2-debug") diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index ca5f057b1..afb59bf73 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -111,9 +111,6 @@ class EvalSygusInvarianceTest : public SygusInvarianceTest */ void init(Node conj, Node var, Node res); - /** do evaluate with unfolding, using the cache of this class */ - Node doEvaluateWithUnfolding(TermDbSygus* tds, Node n); - protected: /** does d_terms{ d_var -> nvn } still rewrite to d_result? */ bool invariant(TermDbSygus* tds, Node nvn, Node x) override; @@ -137,8 +134,6 @@ class EvalSygusInvarianceTest : public SygusInvarianceTest * disjunctively, i.e. if one child test succeeds, the overall test succeeds. */ bool d_is_conjunctive; - /** cache of n -> the simplified form of eval( n ) */ - std::unordered_map<Node, Node> d_visited; }; /** EquivSygusInvarianceTest diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index bcd826799..b7611784d 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -444,7 +444,7 @@ Node SygusRepairConst::getFoQuery(Node body, Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl; Trace("sygus-repair-const") << " Unfold the specification..." << std::endl; - body = d_tds->evaluateWithUnfolding(body); + body = d_tds->rewriteNode(body); Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl; Trace("sygus-repair-const") << " Introduce first-order vars..." << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index 10db1ef9e..6b023075b 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -264,7 +264,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) Node eut = nm->mkNode(DT_SYGUS_EVAL, echildren); Trace("sygus-unif-debug2") << " Test evaluation of " << eut << "..." << std::endl; - eut = d_tds->getEvalUnfold()->unfold(eut); + eut = d_tds->rewriteNode(eut); Trace("sygus-unif-debug2") << " ...got " << eut; Trace("sygus-unif-debug2") << ", type : " << eut.getType() << std::endl; diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 9c9a90255..035db433e 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -739,7 +739,15 @@ SygusTypeInfo& TermDbSygus::getTypeInfo(TypeNode tn) Node TermDbSygus::rewriteNode(Node n) const { - Node res = Rewriter::rewrite(n); + Node res; + if (options().quantifiers.sygusExtRew) + { + res = extendedRewrite(n); + } + else + { + res = rewrite(n); + } if (res.isConst()) { // constant, we are done @@ -1001,59 +1009,6 @@ Node TermDbSygus::evaluateBuiltin(TypeNode tn, return rewriteNode(res); } -Node TermDbSygus::evaluateWithUnfolding(Node n, - std::unordered_map<Node, Node>& visited) -{ - std::unordered_map<Node, Node>::iterator it = visited.find(n); - if( it==visited.end() ){ - Node ret = n; - while (ret.getKind() == DT_SYGUS_EVAL - && ret[0].getKind() == APPLY_CONSTRUCTOR) - { - if (ret == n && ret[0].isConst()) - { - // use rewriting, possibly involving recursive functions - ret = rewriteNode(ret); - } - else - { - ret = d_eval_unfold->unfold(ret); - } - } - if( ret.getNumChildren()>0 ){ - std::vector< Node > children; - if( ret.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.push_back( ret.getOperator() ); - } - bool childChanged = false; - for( unsigned i=0; i<ret.getNumChildren(); i++ ){ - Node nc = evaluateWithUnfolding(ret[i], visited); - childChanged = childChanged || nc!=ret[i]; - children.push_back( nc ); - } - if( childChanged ){ - ret = NodeManager::currentNM()->mkNode( ret.getKind(), children ); - } - if (options::sygusExtRew()) - { - ret = extendedRewrite(ret); - } - // use rewriting, possibly involving recursive functions - ret = rewriteNode(ret); - } - visited[n] = ret; - return ret; - }else{ - return it->second; - } -} - -Node TermDbSygus::evaluateWithUnfolding(Node n) -{ - std::unordered_map<Node, Node> visited; - return evaluateWithUnfolding(n, visited); -} - bool TermDbSygus::isEvaluationPoint(Node n) const { if (n.getKind() != DT_SYGUS_EVAL) diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index a44ebd297..7b05c70e4 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -271,21 +271,6 @@ class TermDbSygus : protected EnvObj Node bn, const std::vector<Node>& args, bool tryEval = true); - /** evaluate with unfolding - * - * n is any term that may involve sygus evaluation functions. This function - * returns the result of unfolding the evaluation functions within n and - * rewriting the result. For example, if eval_A is the evaluation function - * for the datatype: - * A -> C_0 | C_1 | C_x | C_+( C_A, C_A ) - * corresponding to grammar: - * A -> 0 | 1 | x | A + A - * then calling this function on eval( C_+( x, 1 ), 4 ) = y returns 5 = y. - * The node returned by this function is in (extended) rewritten form. - */ - Node evaluateWithUnfolding(Node n); - /** same as above, but with a cache of visited nodes */ - Node evaluateWithUnfolding(Node n, std::unordered_map<Node, Node>& visited); /** is evaluation point? * * Returns true if n is of the form eval( x, c1...cn ) for some variable x |