From d1f3225e26b9d64f065048885053392b10994e71 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 10 Aug 2019 12:56:05 -0500 Subject: [PATCH] Add option to only dump unsolved queries for --sygus-query-gen (#3173) --- src/options/options_handler.cpp | 45 +++++++++++++- src/options/options_handler.h | 3 + src/options/quantifiers_modes.h | 10 +++ src/options/quantifiers_options.toml | 10 +-- src/theory/quantifiers/query_generator.cpp | 72 +++++++++++++--------- src/theory/quantifiers/query_generator.h | 5 ++ 6 files changed, 110 insertions(+), 35 deletions(-) diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index b0a1cd1ad..874c57629 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -504,6 +504,21 @@ trust \n\ \n\ "; +const std::string OptionsHandler::s_sygusQueryDumpFileHelp = + "\ +Query file options supported by --sygus-query-gen-dump-files:\n\ +\n\ +none (default) \n\ ++ Do not dump query files when using --sygus-query-gen.\n\ +\n\ +all \n\ ++ Dump all query files.\n\ +\n\ +unsolved \n\ ++ Dump query files that the subsolver did not solve.\n\ +\n\ +"; + const std::string OptionsHandler::s_sygusFilterSolHelp = "\ Modes for filtering sygus solutions supported by --sygus-filter-sol:\n\ @@ -959,6 +974,34 @@ theory::quantifiers::CegisSampleMode OptionsHandler::stringToCegisSampleMode( } } +theory::quantifiers::SygusQueryDumpFilesMode +OptionsHandler::stringToSygusQueryDumpFilesMode(std::string option, + std::string optarg) +{ + if (optarg == "none") + { + return theory::quantifiers::SYGUS_QUERY_DUMP_NONE; + } + else if (optarg == "all") + { + return theory::quantifiers::SYGUS_QUERY_DUMP_ALL; + } + else if (optarg == "unsolved") + { + return theory::quantifiers::SYGUS_QUERY_DUMP_UNSOLVED; + } + else if (optarg == "help") + { + puts(s_sygusQueryDumpFileHelp.c_str()); + exit(1); + } + else + { + throw OptionException( + std::string("unknown option for --sygus-query-gen-dump-files: `") + + optarg + "'. Try --sygus-query-gen-dump-files help."); + } +} theory::quantifiers::SygusFilterSolMode OptionsHandler::stringToSygusFilterSolMode(std::string option, std::string optarg) @@ -977,7 +1020,7 @@ OptionsHandler::stringToSygusFilterSolMode(std::string option, } else if (optarg == "help") { - puts(s_cegisSampleHelp.c_str()); + puts(s_sygusFilterSolHelp.c_str()); exit(1); } else diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 9a596ddfc..84b7002e3 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -114,6 +114,8 @@ public: std::string option, std::string optarg); theory::quantifiers::CegisSampleMode stringToCegisSampleMode( std::string option, std::string optarg); + theory::quantifiers::SygusQueryDumpFilesMode stringToSygusQueryDumpFilesMode( + std::string option, std::string optarg); theory::quantifiers::SygusFilterSolMode stringToSygusFilterSolMode( std::string option, std::string optarg); theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode( @@ -269,6 +271,7 @@ public: static const std::string s_cegqiSingleInvHelp; static const std::string s_cegqiSingleInvRconsHelp; static const std::string s_cegisSampleHelp; + static const std::string s_sygusQueryDumpFileHelp; static const std::string s_sygusFilterSolHelp; static const std::string s_sygusInvTemplHelp; static const std::string s_sygusActiveGenHelp; diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index c9aeda154..049cdef1c 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -272,6 +272,16 @@ enum SygusActiveGenMode SYGUS_ACTIVE_GEN_AUTO, }; +enum SygusQueryDumpFilesMode +{ + /** do not dump query files */ + SYGUS_QUERY_DUMP_NONE, + /** dump all query files */ + SYGUS_QUERY_DUMP_ALL, + /** dump query files that were not solved by the subsolver */ + SYGUS_QUERY_DUMP_UNSOLVED, +}; + enum SygusFilterSolMode { /** do not filter solutions */ diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 8792fb56b..717ee9dae 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1414,10 +1414,12 @@ header = "options/quantifiers_options.h" [[option]] name = "sygusQueryGenDumpFiles" category = "regular" - long = "sygus-query-gen-dump-files" - type = "bool" - default = "false" - help = "dump external files corresponding to interesting satisfiability queries with sygus-query-gen" + long = "sygus-query-gen-dump-files=MODE" + type = "CVC4::theory::quantifiers::SygusQueryDumpFilesMode" + default = "CVC4::theory::quantifiers::SYGUS_QUERY_DUMP_NONE" + handler = "stringToSygusQueryDumpFilesMode" + includes = ["options/quantifiers_modes.h"] + help = "mode for dumping external files corresponding to interesting satisfiability queries with sygus-query-gen" [[option]] name = "sygusFilterSolMode" diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp index bc7538c1f..742b3000b 100644 --- a/src/theory/quantifiers/query_generator.cpp +++ b/src/theory/quantifiers/query_generator.cpp @@ -146,37 +146,9 @@ bool QueryGenerator::addTerm(Node n, std::ostream& out) void QueryGenerator::checkQuery(Node qy, unsigned spIndex) { // external query - if (options::sygusQueryGenDumpFiles()) + if (options::sygusQueryGenDumpFiles() == SYGUS_QUERY_DUMP_ALL) { - // Print the query and the query + its model (commented) to queryN.smt2 - std::vector pt; - d_sampler->getSamplePoint(spIndex, pt); - unsigned nvars = d_vars.size(); - AlwaysAssert(pt.size() == d_vars.size()); - std::stringstream fname; - fname << "query" << d_queryCount << ".smt2"; - std::ofstream fs(fname.str(), std::ofstream::out); - fs << "(set-logic ALL)" << std::endl; - for (unsigned i = 0; i < 2; i++) - { - for (unsigned j = 0; j < nvars; j++) - { - Node x = d_vars[j]; - if (i == 0) - { - fs << "(declare-fun " << x << " () " << x.getType() << ")"; - } - else - { - fs << ";(define-fun " << x << " () " << x.getType() << " " << pt[j] - << ")"; - } - fs << std::endl; - } - } - fs << "(assert " << qy << ")" << std::endl; - fs << "(check-sat)" << std::endl; - fs.close(); + dumpQuery(qy, spIndex); } if (options::sygusQueryGenCheck()) @@ -207,11 +179,51 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex) ss << "but CVC4 answered unsat!" << std::endl; AlwaysAssert(false, ss.str().c_str()); } + if (options::sygusQueryGenDumpFiles() == SYGUS_QUERY_DUMP_UNSOLVED) + { + if (r.asSatisfiabilityResult().isSat() != Result::SAT) + { + dumpQuery(qy, spIndex); + } + } } d_queryCount++; } +void QueryGenerator::dumpQuery(Node qy, unsigned spIndex) +{ + // Print the query and the query + its model (commented) to queryN.smt2 + std::vector pt; + d_sampler->getSamplePoint(spIndex, pt); + size_t nvars = d_vars.size(); + AlwaysAssert(pt.size() == d_vars.size()); + std::stringstream fname; + fname << "query" << d_queryCount << ".smt2"; + std::ofstream fs(fname.str(), std::ofstream::out); + fs << "(set-logic ALL)" << std::endl; + for (unsigned i = 0; i < 2; i++) + { + for (size_t j = 0; j < nvars; j++) + { + Node x = d_vars[j]; + if (i == 0) + { + fs << "(declare-fun " << x << " () " << x.getType() << ")"; + } + else + { + fs << ";(define-fun " << x << " () " << x.getType() << " " << pt[j] + << ")"; + } + fs << std::endl; + } + } + fs << "(assert " << qy << ")" << std::endl; + fs << "(check-sat)" << std::endl; + fs.close(); +} + void QueryGenerator::findQueries( Node n, std::vector& queries, diff --git a/src/theory/quantifiers/query_generator.h b/src/theory/quantifiers/query_generator.h index 749c78c85..8cb7b2785 100644 --- a/src/theory/quantifiers/query_generator.h +++ b/src/theory/quantifiers/query_generator.h @@ -107,6 +107,11 @@ class QueryGenerator : public ExprMiner * reported to be unsatisfiable. */ void checkQuery(Node qy, unsigned spIndex); + /** + * Dumps query qy to the a file queryN.smt2 for the current counter N; + * spIndex specifies the sample point that satisfies it (for debugging). + */ + void dumpQuery(Node qy, unsigned spIndex); }; } // namespace quantifiers -- 2.30.2