diff options
| -rw-r--r-- | src/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_interpol.cpp | 93 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_interpol.h | 212 |
3 files changed, 307 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9331b1dc7..0561af144 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -608,6 +608,8 @@ libcvc4_add_sources( theory/quantifiers/sygus/sygus_grammar_norm.h theory/quantifiers/sygus/sygus_grammar_red.cpp theory/quantifiers/sygus/sygus_grammar_red.h + theory/quantifiers/sygus/sygus_interpol.cpp + theory/quantifiers/sygus/sygus_interpol.h theory/quantifiers/sygus/sygus_invariance.cpp theory/quantifiers/sygus/sygus_invariance.h theory/quantifiers/sygus/sygus_module.cpp diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp new file mode 100644 index 000000000..77b193a75 --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -0,0 +1,93 @@ +/********************* */ +/*! \file sygus_interpol.cpp + ** \verbatim + ** Top contributors (to current version): + ** Ying Sheng + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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.\endverbatim + ** + ** \brief Implementation of sygus interpolation utility, which + ** transforms an input of axioms and conjecture into an interpolation problem, + *and solve it. + **/ + +#include "theory/quantifiers/sygus/sygus_interpol.h" + +#include "expr/datatype.h" +#include "expr/dtype.h" +#include "expr/node_algorithm.h" +#include "expr/sygus_datatype.h" +#include "options/smt_options.h" +#include "printer/sygus_print_callback.h" +#include "theory/datatypes/sygus_datatype_utils.h" +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/sygus/sygus_grammar_cons.h" +#include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +SygusInterpol::SygusInterpol() {} + +SygusInterpol::SygusInterpol(LogicInfo logic) : d_logic(logic) {} + +void SygusInterpol::collectSymbols(const std::vector<Node>& axioms, + const Node& conj) +{ +} + +void SygusInterpol::createVariables(bool needsShared) +{ +} + +std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> > getIncludeCons( + const std::vector<Node>& assumptions, const Node& conclusion) +{ + std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> > result = + std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> >(); + return result; +} + +TypeNode SygusInterpol::setSynthGrammar(const TypeNode& itpGType, + const std::vector<Node>& axioms, + const Node& conj) +{ + TypeNode itpGTypeS; + return itpGTypeS; +} + +Node SygusInterpol::mkPredicate(const std::string& name) +{ + Node itp; + return itp; +} + +void SygusInterpol::mkSygusConjecture(Node itp, + const std::vector<Node>& axioms, + const Node& conj) +{ +} + +bool SygusInterpol::findInterpol(Expr& interpol, Node itp) +{ + return false; +} + +bool SygusInterpol::SolveInterpolation(const std::string& name, + const std::vector<Node>& axioms, + const Node& conj, + const TypeNode& itpGType, + Expr& interpol) +{ + return false; +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h new file mode 100644 index 000000000..4655822ec --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_interpol.h @@ -0,0 +1,212 @@ +/********************* */ +/*! \file sygus_interpol.h + ** \verbatim + ** Top contributors (to current version): + ** Ying Sheng + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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.\endverbatim + ** + ** \brief Sygus interpolation utility, which transforms an input of axioms and + ** conjecture into an interpolation problem, and solve it. + **/ + +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H + +#include <string> +#include <vector> + +#include "expr/node.h" +#include "expr/type.h" +#include "smt/smt_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { +/** + * This is an utility for the SMT-LIB command (get-interpol <term>). + * The utility turns a set of quantifier-free assertions into a sygus + * conjecture that encodes an interpolation problem, and then solve the + * interpolation problem by synthesizing it. In detail, if our input formula is + * F( x ) for free symbol x, and is partitioned into axioms Fa and conjecture Fc + * then the sygus conjecture we construct is: + * + * exists A. forall x. ( (Fa( x ) => A( x )) ^ (A( x ) => Fc( x )) ) + * + * where A( x ) is a predicate over the free symbols of our input that are + * shared between Fa and Fc. In other words, A( x ) must be implied by our + * axioms Fa( x ) and implies Fc( x ). Then, to solve the interpolation problem, + * we just need to synthesis A( x ). + */ +class SygusInterpol +{ + public: + SygusInterpol(); + + SygusInterpol(LogicInfo logic); + + /** + * Returns the sygus conjecture in interpol corresponding to the interpolation + * problem for input problem (F above) given by axioms (Fa above), and conj + * (Fc above). And solve the interpolation by sygus. Note that axioms is + * expected to be a subset of assertions in SMT-LIB. + * + * @param name the name for the interpol-to-synthesize. + * @param axioms the assertions (Fa above) + * @param conj the conjecture (Fc above) + * @param itpGType (if non-null) a sygus datatype type that encodes the + * grammar that should be used for solutions of the interpolation conjecture. + * @interpol the solution to the sygus conjecture. + */ + bool SolveInterpolation(const std::string& name, + const std::vector<Node>& axioms, + const Node& conj, + const TypeNode& itpGType, + Expr& interpol); + + private: + /** + * Collects symbols from axioms (axioms) and conjecture (conj), which are + * stored in d_syms, and computes the shared symbols between axioms and + * conjecture, stored in d_symsShared. + * + * @param axioms the assertions (Fa above) + * @param conj the conjecture (Fc above) + */ + void collectSymbols(const std::vector<Node>& axioms, const Node& conj); + + /** + * Creates free variables and shared free variables from d_syms and + * d_symsShared, which are stored in d_vars and d_varsShared. And also creates + * the corresponding set of variables for the formal argument list, which is + * stored in d_vlvs and d_vlvsShared. Extracts the types of shared variables, + * which are stored in d_varTypesShared. Creates the formal argument list of + * the interpol-to-synthesis, stored in d_ibvlShared. + * + * When using default grammar, the needsShared is true. When using + * user-defined gramar, the needsShared is false. + * + * @param needsShared If it is true, the argument list of the + * interpol-to-synthesis will be restricted to be over shared variables. If it + * is false, the argument list will be over all the variables. + */ + void createVariables(bool needsShared); + + /** + * Set up the grammar for the interpol-to-synthesis. + * + * The user-defined grammar will be encoded by itpGType. The options for + * grammar is given by options::produceInterpols(). In DEFAULT option, it will + * set up the grammar from itpGType. And if itpGType is null, it will set up + * the default grammar. In ASSUMPTIONS option, it will set up the grammar by + * only using the operators from axioms. In CONJECTURE option, it will set up + * the grammar by only using the operators from conj. In SHARED option, it + * will set up the grammar by only using the operators shared by axioms and + * conj. In ALL option, it will set up the grammar by only using the operators + * from either axioms or conj. + * + * @param itpGType (if non-null) a sygus datatype type that encodes the + * grammar that should be used for solutions of the interpolation conjecture. + * @param axioms the assertions (Fa above) + * @param conj the conjecture (Fc above) + */ + TypeNode setSynthGrammar(const TypeNode& itpGType, + const std::vector<Node>& axioms, + const Node& conj); + + /** + * Make the interpolation predicate. + * + * @param name the name of the interpol-to-synthesis. + */ + Node mkPredicate(const std::string& name); + + /** + * Make the sygus conjecture to be synthesis. + * + * @param itp the interpolation predicate. + * @param axioms the assertions (Fa above) + * @param conj the conjecture (Fc above) + */ + void mkSygusConjecture(Node itp, + const std::vector<Node>& axioms, + const Node& conj); + + /** + * Get the synthesis solution, stored in interpol. + * + * @param interpol the solution to the sygus conjecture. + * @param itp the interpolation predicate. + */ + bool findInterpol(Expr& interpol, Node itp); + + /** The SMT engine subSolver + * + * This is a fresh copy of the SMT engine which is used for solving the + * interpolation problem. In particular, consider the input: (assert A) + * (get-interpol s B) + * In the copy of the SMT engine where these commands are issued, we maintain + * A in the assertion stack. In solving the interpolation problem, we will + * need to call a SMT engine solver with a different assertion stack, which is + * a sygus conjecture build from A and B. Then to solve the interpolation + * 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 original assertion stack unchanged. This copy of the SMT + * engine will have the assertion stack with the sygus conjecture. This copy + * of the SMT engine can be further queried for information regarding further + * solutions. + */ + std::unique_ptr<SmtEngine> d_subSolver; + + /** + * The logic for the local copy of SMT engine (d_subSolver). + */ + LogicInfo d_logic; + + /** + * symbols from axioms and conjecture. + */ + std::vector<Node> d_syms; + /** + * shared symbols between axioms and conjecture. + */ + std::vector<Node> d_symsShared; + /** + * free variables created from d_syms. + */ + std::vector<Node> d_vars; + /** + * variables created from d_syms for formal argument list. + */ + std::vector<Node> d_vlvs; + /** + * free variables created from d_symsShared. + */ + std::vector<Node> d_varsShared; + /** + * variables created from d_symShared for formal argument list. + */ + std::vector<Node> d_vlvsShared; + /** + * types of shared variables between axioms and conjecture. + */ + std::vector<TypeNode> d_varTypesShared; + /** + * formal argument list of the interpol-to-synthesis. + */ + Node d_ibvlShared; + + /** + * the sygus conjecture to synthesis for interpolation problem + */ + Node d_sygusConj; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H */ |