From 90eddb069c3c9abf96719ac20aff45b44af86207 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 29 Jul 2019 13:58:09 -0500 Subject: [PATCH] Support get-abduct smt2 command (#3122) --- src/CMakeLists.txt | 4 +- src/bindings/java/CMakeLists.txt | 1 + src/options/quantifiers_options.toml | 9 -- src/options/smt_options.toml | 9 ++ src/parser/smt2/Smt2.g | 16 +- src/parser/smt2/smt2.cpp | 7 +- .../preprocessing_pass_registry.cpp | 2 - src/smt/command.cpp | 84 +++++++++++ src/smt/command.h | 50 +++++++ src/smt/smt_engine.cpp | 140 +++++++++++++++--- src/smt/smt_engine.h | 43 ++++++ src/theory/logic_info.cpp | 9 ++ src/theory/logic_info.h | 6 + src/theory/quantifiers/expr_miner.cpp | 1 - .../quantifiers/sygus}/sygus_abduct.cpp | 73 ++------- .../quantifiers/sygus}/sygus_abduct.h | 54 ++++--- test/regress/CMakeLists.txt | 1 + .../regress1/sygus-abduct-test-user.smt2 | 28 ++++ test/regress/regress1/sygus-abduct-test.smt2 | 4 +- 19 files changed, 415 insertions(+), 126 deletions(-) rename src/{preprocessing/passes => theory/quantifiers/sygus}/sygus_abduct.cpp (84%) rename src/{preprocessing/passes => theory/quantifiers/sygus}/sygus_abduct.h (62%) create mode 100644 test/regress/regress1/sygus-abduct-test-user.smt2 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9da9bd603..861841633 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -90,8 +90,6 @@ libcvc4_add_sources( preprocessing/passes/sort_infer.h preprocessing/passes/static_learning.cpp preprocessing/passes/static_learning.h - preprocessing/passes/sygus_abduct.cpp - preprocessing/passes/sygus_abduct.h preprocessing/passes/sygus_inference.cpp preprocessing/passes/sygus_inference.h preprocessing/passes/symmetry_breaker.cpp @@ -551,6 +549,8 @@ libcvc4_add_sources( theory/quantifiers/sygus/cegis_unif.h theory/quantifiers/sygus/enum_stream_substitution.cpp theory/quantifiers/sygus/enum_stream_substitution.h + theory/quantifiers/sygus/sygus_abduct.cpp + theory/quantifiers/sygus/sygus_abduct.h theory/quantifiers/sygus/sygus_enumerator.cpp theory/quantifiers/sygus/sygus_enumerator.h theory/quantifiers/sygus/sygus_eval_unfold.cpp diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt index a94afc0a0..555ab2d6f 100644 --- a/src/bindings/java/CMakeLists.txt +++ b/src/bindings/java/CMakeLists.txt @@ -111,6 +111,7 @@ set(gen_java_files ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToUBV.java ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointType.java ${CMAKE_CURRENT_BINARY_DIR}/FunctionType.java + ${CMAKE_CURRENT_BINARY_DIR}/GetAbductCommand.java ${CMAKE_CURRENT_BINARY_DIR}/GetAssertionsCommand.java ${CMAKE_CURRENT_BINARY_DIR}/GetAssignmentCommand.java ${CMAKE_CURRENT_BINARY_DIR}/GetInfoCommand.java diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 03ffade46..8792fb56b 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -885,15 +885,6 @@ header = "options/quantifiers_options.h" read_only = false help = "attempt to preprocess arbitrary inputs to sygus conjectures" -[[option]] - name = "sygusAbduct" - category = "regular" - long = "sygus-abduct" - type = "bool" - default = "false" - read_only = false - help = "compute abductions using sygus" - [[option]] name = "ceGuidedInst" category = "regular" diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 72dfdd7f8..ef4e19654 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -614,3 +614,12 @@ header = "options/smt_options.h" default = "false" read_only = true help = "attempt to solve a pure real satisfiable problem as an integer problem (for non-linear)" + +[[option]] + name = "produceAbducts" + category = "undocumented" + long = "produce-abducts" + type = "bool" + default = "false" + read_only = true + help = "support the get-abduct command" diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index d72188c6c..a95689f1c 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1529,8 +1529,19 @@ extendedCommand[std::unique_ptr* cmd] | GET_QE_DISJUNCT_TOK { PARSER_STATE->checkThatLogicIsSet(); } term[e,e2] { cmd->reset(new GetQuantifierEliminationCommand(e, false)); } - | DECLARE_HEAP LPAREN_TOK - sortSymbol[t,CHECK_DECLARED] + | GET_ABDUCT_TOK { + PARSER_STATE->checkThatLogicIsSet(); + } + symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + term[e,e2] + ( + sygusGrammar[t, terms, name] + )? + { + cmd->reset(new GetAbductCommand(name,e, t)); + } + | DECLARE_HEAP LPAREN_TOK + sortSymbol[t,CHECK_DECLARED] sortSymbol[t, CHECK_DECLARED] // We currently do nothing with the type information declared for the heap. { cmd->reset(new EmptyCommand()); } @@ -3055,6 +3066,7 @@ SIMPLIFY_TOK : 'simplify'; INCLUDE_TOK : 'include'; GET_QE_TOK : 'get-qe'; GET_QE_DISJUNCT_TOK : 'get-qe-disjunct'; +GET_ABDUCT_TOK : 'get-abduct'; DECLARE_HEAP : 'declare-heap'; // SyGuS commands diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 278f2bdfd..752bf58b4 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -674,11 +674,8 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) } // get unlocked copy, modify, copy and relock LogicInfo log(d_logic.getUnlockedCopy()); - log.enableQuantifiers(); - log.enableTheory(theory::THEORY_UF); - log.enableTheory(theory::THEORY_DATATYPES); - log.enableIntegers(); - log.enableHigherOrder(); + // enable everything needed for sygus + log.enableSygus(); d_logic = log; d_logic.lock(); } diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp index 15618f575..34bae1224 100644 --- a/src/preprocessing/preprocessing_pass_registry.cpp +++ b/src/preprocessing/preprocessing_pass_registry.cpp @@ -48,7 +48,6 @@ #include "preprocessing/passes/sep_skolem_emp.h" #include "preprocessing/passes/sort_infer.h" #include "preprocessing/passes/static_learning.h" -#include "preprocessing/passes/sygus_abduct.h" #include "preprocessing/passes/sygus_inference.h" #include "preprocessing/passes/symmetry_breaker.h" #include "preprocessing/passes/symmetry_detect.h" @@ -127,7 +126,6 @@ PreprocessingPassRegistry::PreprocessingPassRegistry() registerPassInfo("synth-rr", callCtor); registerPassInfo("real-to-int", callCtor); registerPassInfo("sygus-infer", callCtor); - registerPassInfo("sygus-abduct", callCtor); registerPassInfo("bv-to-bool", callCtor); registerPassInfo("bv-intro-pow2", callCtor); registerPassInfo("sort-inference", callCtor); diff --git a/src/smt/command.cpp b/src/smt/command.cpp index b1936d8cc..044062f77 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -2033,6 +2033,90 @@ std::string GetSynthSolutionCommand::getCommandName() const return "get-instantiations"; } +GetAbductCommand::GetAbductCommand() {} +GetAbductCommand::GetAbductCommand(const std::string& name, Expr conj) + : d_name(name), d_conj(conj), d_resultStatus(false) +{ +} +GetAbductCommand::GetAbductCommand(const std::string& name, + Expr conj, + const Type& gtype) + : d_name(name), + d_conj(conj), + d_sygus_grammar_type(gtype), + d_resultStatus(false) +{ +} + +Expr GetAbductCommand::getConjecture() const { return d_conj; } +Type GetAbductCommand::getGrammarType() const { return d_sygus_grammar_type; } +Expr GetAbductCommand::getResult() const { return d_result; } + +void GetAbductCommand::invoke(SmtEngine* smtEngine) +{ + try + { + if (d_sygus_grammar_type.isNull()) + { + d_resultStatus = smtEngine->getAbduct(d_conj, d_result); + } + else + { + d_resultStatus = + smtEngine->getAbduct(d_conj, d_sygus_grammar_type, d_result); + } + d_commandStatus = CommandSuccess::instance(); + } + catch (exception& e) + { + d_commandStatus = new CommandFailure(e.what()); + } +} + +void GetAbductCommand::printResult(std::ostream& out, uint32_t verbosity) const +{ + if (!ok()) + { + this->Command::printResult(out, verbosity); + } + else + { + expr::ExprDag::Scope scope(out, false); + if (d_resultStatus) + { + out << "(define-fun " << d_name << " () Bool " << d_result << ")" + << std::endl; + } + else + { + out << "none" << std::endl; + } + } +} + +Command* GetAbductCommand::exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) +{ + GetAbductCommand* c = + new GetAbductCommand(d_name, d_conj.exportTo(exprManager, variableMap)); + c->d_sygus_grammar_type = + d_sygus_grammar_type.exportTo(exprManager, variableMap); + c->d_result = d_result.exportTo(exprManager, variableMap); + c->d_resultStatus = d_resultStatus; + return c; +} + +Command* GetAbductCommand::clone() const +{ + GetAbductCommand* c = new GetAbductCommand(d_name, d_conj); + c->d_sygus_grammar_type = d_sygus_grammar_type; + c->d_result = d_result; + c->d_resultStatus = d_resultStatus; + return c; +} + +std::string GetAbductCommand::getCommandName() const { return "get-abduct"; } + /* -------------------------------------------------------------------------- */ /* class GetQuantifierEliminationCommand */ /* -------------------------------------------------------------------------- */ diff --git a/src/smt/command.h b/src/smt/command.h index 68f9d1881..eb3199944 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1009,6 +1009,56 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command SmtEngine* d_smtEngine; }; /* class GetSynthSolutionCommand */ +/** The command (get-abduct s B (G)?) + * + * This command asks for an abduct from the current set of assertions and + * conjecture (goal) given by the argument B. + * + * The symbol s is the name for the abduction predicate. If we successfully + * find a predicate P, then the output response of this command is: + * (define-fun s () Bool P) + * + * A grammar type G can be optionally provided to indicate the syntactic + * restrictions on the possible solutions returned. + */ +class CVC4_PUBLIC GetAbductCommand : public Command +{ + public: + GetAbductCommand(); + GetAbductCommand(const std::string& name, Expr conj); + GetAbductCommand(const std::string& name, Expr conj, const Type& gtype); + + /** Get the conjecture of the abduction query */ + Expr getConjecture() const; + /** Get the grammar type given for the abduction query */ + Type getGrammarType() const; + /** Get the result of the query, which is the solution to the abduction query. + */ + Expr getResult() const; + + void invoke(SmtEngine* smtEngine) override; + void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + Command* exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) override; + Command* clone() const override; + std::string getCommandName() const override; + + protected: + /** The name of the abduction predicate */ + std::string d_name; + /** The conjecture of the abduction query */ + Expr d_conj; + /** + * The (optional) grammar of the abduction query, expressed as a sygus + * datatype type. + */ + Type d_sygus_grammar_type; + /** the return status of the command */ + bool d_resultStatus; + /** the return expression of the command */ + Expr d_result; +}; /* class GetAbductCommand */ + class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command { protected: diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5e8540348..5db3fc43d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -98,6 +98,7 @@ #include "theory/quantifiers/fun_def_process.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/single_inv_partition.h" +#include "theory/quantifiers/sygus/sygus_abduct.h" #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" @@ -1258,21 +1259,25 @@ void SmtEngine::setDefaults() { // sygus inference may require datatypes if (!d_isInternalSubsolver) { - if (options::sygusInference() || options::sygusRewSynthInput() - || options::sygusAbduct()) + if (options::produceAbducts()) + { + // we may invoke a sygus conjecture, hence we need options related to + // sygus + is_sygus = true; + } + if (options::sygusInference() || options::sygusRewSynthInput()) { - d_logic = d_logic.getUnlockedCopy(); - // sygus requires arithmetic, datatypes and quantifiers - d_logic.enableTheory(THEORY_ARITH); - d_logic.enableTheory(THEORY_DATATYPES); - d_logic.enableTheory(THEORY_QUANTIFIERS); - d_logic.lock(); // since we are trying to recast as sygus, we assume the input is sygus is_sygus = true; + // we change the logic to incorporate sygus immediately + d_logic = d_logic.getUnlockedCopy(); + d_logic.enableSygus(); + d_logic.lock(); } } if ((options::checkModels() || options::checkSynthSol() + || options::produceAbducts() || options::modelCoresMode() != MODEL_CORES_NONE) && !options::produceAssertions()) { @@ -1954,16 +1959,24 @@ void SmtEngine::setDefaults() { options::sygusExtRew.set(false); } } - if (options::sygusAbduct()) + // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm + // is one that is specialized for returning a single solution. Non-basic + // sygus algorithms currently include the PBE solver, static template + // inference for invariant synthesis, and single invocation techniques. + bool reqBasicSygus = false; + if (options::produceAbducts()) { // if doing abduction, we should filter strong solutions if (!options::sygusFilterSolMode.wasSetByUser()) { options::sygusFilterSolMode.set(quantifiers::SYGUS_FILTER_SOL_STRONG); } + // we must use basic sygus algorithms, since e.g. we require checking + // a sygus side condition for consistency with axioms. + reqBasicSygus = true; } if (options::sygusRewSynth() || options::sygusRewVerify() - || options::sygusQueryGen() || options::sygusAbduct()) + || options::sygusQueryGen()) { // rewrite rule synthesis implies that sygus stream must be true options::sygusStream.set(true); @@ -1971,9 +1984,12 @@ void SmtEngine::setDefaults() { if (options::sygusStream()) { // Streaming is incompatible with techniques that focus the search towards - // finding a single solution. This currently includes the PBE solver, - // static template inference for invariant synthesis, and single - // invocation techniques. + // finding a single solution. + reqBasicSygus = true; + } + // Now, disable options for non-basic sygus algorithms, if necessary. + if (reqBasicSygus) + { if (!options::sygusUnifPbe.wasSetByUser()) { options::sygusUnifPbe.set(false); @@ -2291,11 +2307,11 @@ void SmtEngine::setDefaults() { "--sygus-expr-miner-check-timeout=N requires " "--sygus-expr-miner-check-use-export"); } - if (options::sygusRewSynthInput() || options::sygusAbduct()) + if (options::sygusRewSynthInput() || options::produceAbducts()) { std::stringstream ss; ss << (options::sygusRewSynthInput() ? "--sygus-rr-synth-input" - : "--sygus-abduct"); + : "--produce-abducts"); ss << "requires --sygus-expr-miner-check-use-export"; throw OptionException(ss.str()); } @@ -3325,10 +3341,6 @@ void SmtEnginePrivate::processAssertions() { { d_passes["sygus-infer"]->apply(&d_assertions); } - else if (options::sygusAbduct()) - { - d_passes["sygus-abduct"]->apply(&d_assertions); - } else if (options::sygusRewSynthInput()) { // do candidate rewrite rule synthesis @@ -4961,6 +4973,96 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) } } +bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd) +{ + SmtScope smts(this); + + if (!options::produceAbducts()) + { + const char* msg = "Cannot get abduct when produce-abducts options is off."; + throw ModalException(msg); + } + Trace("sygus-abduct") << "SmtEngine::getAbduct: conjecture " << conj + << std::endl; + std::vector easserts = getAssertions(); + std::vector axioms; + for (unsigned i = 0, size = easserts.size(); i < size; i++) + { + axioms.push_back(Node::fromExpr(easserts[i])); + } + std::vector asserts(axioms.begin(), axioms.end()); + asserts.push_back(Node::fromExpr(conj)); + d_sssfVarlist.clear(); + d_sssfSyms.clear(); + std::string name("A"); + Node aconj = theory::quantifiers::SygusAbduct::mkAbductionConjecture( + name, + asserts, + axioms, + TypeNode::fromType(grammarType), + d_sssfVarlist, + d_sssfSyms); + // should be a quantified conjecture with one function-to-synthesize + Assert(aconj.getKind() == kind::FORALL && aconj[0].getNumChildren() == 1); + // remember the abduct-to-synthesize + d_sssf = aconj[0][0].toExpr(); + Trace("sygus-abduct") << "SmtEngine::getAbduct: made conjecture : " << aconj + << ", solving for " << d_sssf << std::endl; + // we generate a new smt engine to do the abduction query + d_subsolver.reset(new SmtEngine(NodeManager::currentNM()->toExprManager())); + d_subsolver->setIsInternalSubsolver(); + // get the logic + LogicInfo l = d_logic.getUnlockedCopy(); + // enable everything needed for sygus + l.enableSygus(); + d_subsolver->setLogic(l); + // assert the abduction query + d_subsolver->assertFormula(aconj.toExpr()); + Trace("sygus-abduct") << " SmtEngine::getAbduct check sat..." << std::endl; + Result r = d_subsolver->checkSat(); + Trace("sygus-abduct") << " SmtEngine::getAbduct result: " << r << std::endl; + if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + // get the synthesis solution + std::map sols; + d_subsolver->getSynthSolutions(sols); + Assert(sols.size() == 1); + std::map::iterator its = sols.find(d_sssf); + if (its != sols.end()) + { + Node abdn = Node::fromExpr(its->second); + Trace("sygus-abduct") + << "SmtEngine::getAbduct: solution is " << abdn << std::endl; + if (abdn.getKind() == kind::LAMBDA) + { + abdn = abdn[1]; + } + // convert back to original + // must replace formal arguments of abd with the free variables in the + // input problem that they correspond to. + abdn = abdn.substitute(d_sssfVarlist.begin(), + d_sssfVarlist.end(), + d_sssfSyms.begin(), + d_sssfSyms.end()); + + // convert to expression + abd = abdn.toExpr(); + + return true; + } + Trace("sygus-abduct") << "SmtEngine::getAbduct: could not find solution!" + << std::endl; + throw RecoverableModalException("Could not find solution for get-abduct."); + } + return false; +} + +bool SmtEngine::getAbduct(const Expr& conj, Expr& abd) +{ + Type grammarType; + return getAbduct(conj, grammarType, abd); +} + void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ) { SmtScope smts(this); if( d_theoryEngine ){ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 5913716e6..566777a89 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -147,6 +147,34 @@ class CVC4_PUBLIC SmtEngine { ProofManager* d_proofManager; /** An index of our defined functions */ DefinedFunctionMap* d_definedFunctions; + /** The SMT engine subsolver + * + * This is a separate copy of the SMT engine which is used for making + * calls that cannot be answered by this copy of the SMT engine. An example + * of invoking this subsolver is the get-abduct command, where we wish to + * solve a sygus conjecture based on the current assertions. In particular, + * consider the input: + * (assert A) + * (get-abduct B) + * In the copy of the SMT engine where these commands are issued, we maintain + * A in the assertion stack. To solve the abduction problem, instead of + * modifying the assertion stack to remove A and add the sygus conjecture + * (exists I. ...), we invoke a fresh copy of the SMT engine and leave the + * assertion stack unchaged. This copy of the SMT engine can be further + * queried for information regarding further solutions. + */ + std::unique_ptr d_subsolver; + /** + * If applicable, the function-to-synthesize that the subsolver is solving + * for. This is used for the get-abduct command. + */ + Expr d_sssf; + /** + * The substitution to apply to the solutions from the subsolver, used for + * the get-abduct command. + */ + std::vector d_sssfVarlist; + std::vector d_sssfSyms; /** recursive function definition abstractions for --fmf-fun */ std::map< Node, TypeNode > d_fmfRecFunctionsAbs; std::map< Node, std::vector< Node > > d_fmfRecFunctionsConcrete; @@ -849,6 +877,21 @@ class CVC4_PUBLIC SmtEngine { Expr doQuantifierElimination(const Expr& e, bool doFull, bool strict = true) /* throw(Exception) */; + /** + * This method asks this SMT engine to find an abduct with respect to the + * current assertion stack (call it A) and the conjecture (call it B). + * If this method returns true, then abd is set to a formula C such that + * A ^ C is satisfiable, and A ^ B ^ C is unsatisfiable. + * + * The argument grammarType is a sygus datatype type that encodes the syntax + * restrictions on the shape of possible solutions. + * + * This method invokes a separate copy of the SMT engine for solving the + * corresponding sygus problem for generating such a solution. + */ + bool getAbduct(const Expr& conj, const Type& grammarType, Expr& abd); + /** Same as above, but without user-provided grammar restrictions */ + bool getAbduct(const Expr& conj, Expr& abd); /** * Get list of quantified formulas that were instantiated diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index e21d1f630..37b25163a 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -579,6 +579,15 @@ void LogicInfo::disableTheory(theory::TheoryId theory) { } } +void LogicInfo::enableSygus() +{ + enableQuantifiers(); + enableTheory(THEORY_UF); + enableTheory(THEORY_DATATYPES); + enableIntegers(); + enableHigherOrder(); +} + void LogicInfo::enableIntegers() { PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index a765472dd..969810a6f 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -201,6 +201,12 @@ public: disableTheory(theory::THEORY_QUANTIFIERS); } + /** + * Enable everything that is needed for sygus with respect to this logic info. + * This means enabling quantifiers, datatypes, UF, integers, and higher order. + */ + void enableSygus(); + // these are for arithmetic /** Enable the use of integers in this logic. */ diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 98d07fdea..6b042e294 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -91,7 +91,6 @@ void ExprMiner::initializeChecker(std::unique_ptr& checker, checker->setTimeLimit(options::sygusExprMinerCheckTimeout(), true); checker->setLogic(smt::currentSmtEngine()->getLogicInfo()); checker->setOption("sygus-rr-synth-input", false); - checker->setOption("sygus-abduct", false); checker->setOption("input-language", "smt2"); Expr equery = squery.toExpr().exportTo(&em, varMap); checker->assertFormula(equery); diff --git a/src/preprocessing/passes/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp similarity index 84% rename from src/preprocessing/passes/sygus_abduct.cpp rename to src/theory/quantifiers/sygus/sygus_abduct.cpp index b2dc872e4..52fb60c06 100644 --- a/src/preprocessing/passes/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -9,18 +9,15 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Implementation of sygus abduction preprocessing pass, which + ** \brief Implementation of sygus abduction utility, which ** transforms an arbitrary input into an abduction problem. **/ -#include "preprocessing/passes/sygus_abduct.h" +#include "theory/quantifiers/sygus/sygus_abduct.h" #include "expr/datatype.h" #include "expr/node_algorithm.h" #include "printer/sygus_print_callback.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "smt/smt_statistics_registry.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/term_util.h" @@ -30,59 +27,17 @@ using namespace std; using namespace CVC4::kind; namespace CVC4 { -namespace preprocessing { -namespace passes { +namespace theory { +namespace quantifiers { -SygusAbduct::SygusAbduct(PreprocessingPassContext* preprocContext) - : PreprocessingPass(preprocContext, "sygus-abduct"){}; +SygusAbduct::SygusAbduct() {} -PreprocessingPassResult SygusAbduct::applyInternal( - AssertionPipeline* assertionsToPreprocess) -{ - Trace("sygus-abduct") << "Run sygus abduct..." << std::endl; - - Trace("sygus-abduct-debug") << "Collect symbols..." << std::endl; - std::vector& asserts = assertionsToPreprocess->ref(); - // do we have any assumptions, e.g. via check-sat-assuming? - bool usingAssumptions = (assertionsToPreprocess->getNumAssumptions() > 0); - // The following is our set of "axioms". We construct this set only when the - // usingAssumptions (above) is true. In this case, our input formula is - // partitioned into Fa ^ Fc as described in the header of this class, where: - // - The conjunction of assertions marked as assumptions are the negated - // conjecture Fc, and - // - The conjunction of all other assertions are the axioms Fa. - std::vector axioms; - if (usingAssumptions) - { - for (size_t i = 0, astart = assertionsToPreprocess->getAssumptionsStart(); - i < astart; - i++) - { - // if we are not an assumption, add it to the set of axioms - axioms.push_back(asserts[i]); - } - } - - // the abduction grammar type we are using (null for now, until a future - // commit) - TypeNode abdGType; - - Node res = mkAbductionConjecture(asserts, axioms, abdGType); - - Node trueNode = NodeManager::currentNM()->mkConst(true); - - assertionsToPreprocess->replace(0, res); - for (size_t i = 1, size = assertionsToPreprocess->size(); i < size; ++i) - { - assertionsToPreprocess->replace(i, trueNode); - } - - return PreprocessingPassResult::NO_CONFLICT; -} - -Node SygusAbduct::mkAbductionConjecture(const std::vector& asserts, +Node SygusAbduct::mkAbductionConjecture(const std::string& name, + const std::vector& asserts, const std::vector& axioms, - TypeNode abdGType) + TypeNode abdGType, + std::vector& varlist, + std::vector& syms) { NodeManager* nm = NodeManager::currentNM(); std::unordered_set symset; @@ -94,9 +49,7 @@ Node SygusAbduct::mkAbductionConjecture(const std::vector& asserts, << "...finish, got " << symset.size() << " symbols." << std::endl; Trace("sygus-abduct-debug") << "Setup symbols..." << std::endl; - std::vector syms; std::vector vars; - std::vector varlist; std::vector varlistTypes; for (const Node& s : symset) { @@ -121,7 +74,7 @@ Node SygusAbduct::mkAbductionConjecture(const std::vector& asserts, // make the abduction predicate to synthesize TypeNode abdType = varlistTypes.empty() ? nm->booleanType() : nm->mkPredicateType(varlistTypes); - Node abd = nm->mkBoundVar("A", abdType); + Node abd = nm->mkBoundVar(name.c_str(), abdType); Trace("sygus-abduct-debug") << "...finish" << std::endl; // if provided, we will associate it with the function-to-synthesize @@ -355,6 +308,6 @@ Node SygusAbduct::mkAbductionConjecture(const std::vector& asserts, return res; } -} // namespace passes -} // namespace preprocessing +} // namespace quantifiers +} // namespace theory } // namespace CVC4 diff --git a/src/preprocessing/passes/sygus_abduct.h b/src/theory/quantifiers/sygus/sygus_abduct.h similarity index 62% rename from src/preprocessing/passes/sygus_abduct.h rename to src/theory/quantifiers/sygus/sygus_abduct.h index db40b9688..d6bbd0e3f 100644 --- a/src/preprocessing/passes/sygus_abduct.h +++ b/src/theory/quantifiers/sygus/sygus_abduct.h @@ -9,23 +9,25 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Sygus abduction preprocessing pass, which transforms an arbitrary - ** input into an abduction problem. + ** \brief Sygus abduction utility, which transforms an arbitrary input into an + ** abduction problem. **/ -#ifndef CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H -#define CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H -#include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" +#include +#include +#include "expr/node.h" +#include "expr/type.h" namespace CVC4 { -namespace preprocessing { -namespace passes { +namespace theory { +namespace quantifiers { /** SygusAbduct * - * A preprocessing utility that turns a set of quantifier-free assertions into + * A utility that turns a set of quantifier-free assertions into * a sygus conjecture that encodes an abduction problem. In detail, if our * input formula is F( x ) for free symbols x, then we construct the sygus * conjecture: @@ -51,34 +53,38 @@ namespace passes { * In other words, A( y ) must be consistent with our axioms Fa and imply * ~F( x ). We encode this conjecture using SygusSideConditionAttribute. */ -class SygusAbduct : public PreprocessingPass +class SygusAbduct { public: - SygusAbduct(PreprocessingPassContext* preprocContext); + SygusAbduct(); /** * Returns the sygus conjecture corresponding to the abduction problem for * input problem (F above) given by asserts, and axioms (Fa above) given by * axioms. Note that axioms is expected to be a subset of asserts. * + * The argument name is the name for the abduct-to-synthesize. + * * The type abdGType (if non-null) is a sygus datatype type that encodes the * grammar that should be used for solutions of the abduction conjecture. + * + * The arguments varlist and syms specify the relationship between the free + * variables of asserts and the formal argument list of the + * abduct-to-synthesize. In particular, solutions to the synthesis conjecture + * will be in the form of a closed term (lambda varlist. t). The intended + * solution, which is a term whose free variables are a subset of asserts, + * is the term t { varlist -> syms }. */ - static Node mkAbductionConjecture(const std::vector& asserts, + static Node mkAbductionConjecture(const std::string& name, + const std::vector& asserts, const std::vector& axioms, - TypeNode abdGType); - - protected: - /** - * Replaces the set of assertions by an abduction sygus problem described - * above. - */ - PreprocessingPassResult applyInternal( - AssertionPipeline* assertionsToPreprocess) override; + TypeNode abdGType, + std::vector& varlist, + std::vector& syms); }; -} // namespace passes -} // namespace preprocessing +} // namespace quantifiers +} // namespace theory } // namespace CVC4 -#endif /* CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H_ */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 62672878e..5ecacd4ab 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1618,6 +1618,7 @@ set(regress_1_tests regress1/strings/type003.smt2 regress1/strings/username_checker_min.smt2 regress1/sygus-abduct-test.smt2 + regress1/sygus-abduct-test-user.smt2 regress1/sygus/VC22_a.sy regress1/sygus/abv.sy regress1/sygus/array_search_2.sy diff --git a/test/regress/regress1/sygus-abduct-test-user.smt2 b/test/regress/regress1/sygus-abduct-test-user.smt2 new file mode 100644 index 000000000..bdb680613 --- /dev/null +++ b/test/regress/regress1/sygus-abduct-test-user.smt2 @@ -0,0 +1,28 @@ +; COMMAND-LINE: --produce-abducts +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic QF_UFLIRA) +(set-option :produce-abducts true) +(declare-fun n () Int) +(declare-fun m () Int) +(declare-fun x () Int) +(declare-fun y () Int) + +(assert (>= n 1)) +(assert (and (<= n x)(<= x (+ n 5)))) +(assert (and (<= 1 y)(<= y m))) + +; Generate a predicate A that is consistent with the above axioms (i.e. +; their conjunction is SAT), and is such that the conjunction of the above +; axioms, A and the conjecture below are UNSAT. +; The signature of A is below grammar. +(get-abduct A (< x y) + +; the grammar for the abduct-to-synthesize +((Start Bool) (StartInt Int)) +( +(Start Bool ((< StartInt StartInt))) +(StartInt Int (n m (+ StartInt StartInt) 0 1)) +) + +) diff --git a/test/regress/regress1/sygus-abduct-test.smt2 b/test/regress/regress1/sygus-abduct-test.smt2 index 4ac90870c..d01f5f5ff 100644 --- a/test/regress/regress1/sygus-abduct-test.smt2 +++ b/test/regress/regress1/sygus-abduct-test.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --sygus-abduct --sygus-abort-size=2 +; COMMAND-LINE: --produce-abducts --sygus-stream --sygus-abort-size=2 ; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.") ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 1 @@ -13,4 +13,4 @@ (assert (and (<= n x)(<= x (+ n 5)))) (assert (and (<= 1 y)(<= y m))) -(check-sat-assuming ((< x y))) +(get-abduct A (< x y)) -- 2.30.2