diff options
author | Ying Sheng <sqy1415@gmail.com> | 2020-07-10 12:19:17 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-10 16:19:17 -0300 |
commit | 1dbc8aa695772daf2c83d10a7adb8123f97fa16f (patch) | |
tree | dc5ab224af32cf0e2656402f5a5fde38c9b7b5ec /src/theory/quantifiers/sygus/sygus_interpol.cpp | |
parent | 95d97af192dc6ef7661ef9748c987270cce4c511 (diff) |
[Interpolation] Add interface for SyGuS interpolation module (#4677)
This is the second step of adding Interpolation. The whole change will be adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack.
The second step creates the component for computing interpolation, while omits the implementation.
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_interpol.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_interpol.cpp | 93 |
1 files changed, 93 insertions, 0 deletions
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 |