diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-03-06 09:37:48 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-06 09:37:48 -0800 |
commit | aa3807f28b47abaa26573439f4dafca0258e4b6b (patch) | |
tree | ec265cc8ff82df819d8c6acf49902f2be9317b1b /src/theory/quantifiers/sygus/sygus_module.h | |
parent | 9bf97a2ac3c923d08cce93ca7eda4360b19dfdec (diff) | |
parent | e2d714a0839fb80d9a40e9b6fdd8a6fe325a1664 (diff) |
Merge branch 'master' into cleanup_outputcleanup_output
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_module.h')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_module.h | 129 |
1 files changed, 129 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h new file mode 100644 index 000000000..0a3fa9995 --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -0,0 +1,129 @@ +/********************* */ +/*! \file sygus_module.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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_module + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H +#define __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H + +#include <map> +#include "expr/node.h" +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class CegConjecture; + +/** SygusModule + * + * This is the base class of sygus modules, owned by CegConjecture. The purpose + * of this class is to, when applicable, suggest candidate solutions for + * CegConjecture to test. + * + * In more detail, an instance of the conjecture class (CegConjecture) creates + * the negated deep embedding form of the synthesis conjecture. In the + * following, assume this is: + * forall d. exists x. P( d, x ) + * where d are of sygus datatype type. The "base instantiation" of this + * conjecture (see CegConjecture::d_base_inst) is the formula: + * exists y. P( k, y ) + * where k are the "candidate" variables for the conjecture. + * + * Modules implement an initialize function, which determines whether the module + * will take responsibility for the given conjecture. + */ +class SygusModule +{ + public: + SygusModule(QuantifiersEngine* qe, CegConjecture* p); + ~SygusModule() {} + /** initialize + * + * n is the "base instantiation" of the deep-embedding version of the + * synthesis conjecture under candidates (see CegConjecture::d_base_inst). + * + * This function may add lemmas to the argument lemmas, which should be + * sent out on the output channel of quantifiers by the caller. + * + * This function returns true if this module will take responsibility for + * constructing candidates for the given conjecture. + */ + virtual bool initialize(Node n, + const std::vector<Node>& candidates, + std::vector<Node>& lemmas) = 0; + /** get term list + * + * This gets the list of terms that will appear as arguments to a subsequent + * call to constructCandidates. + */ + virtual void getTermList(const std::vector<Node>& candidates, + std::vector<Node>& terms) = 0; + /** construct candidate + * + * This function takes as input: + * terms : the terms returned by a call to getTermList, + * term_values : the current model values of terms, + * candidates : the list of candidates. + * + * If this function returns true, it adds to candidate_values a list of terms + * of the same length and type as candidates that are candidate solutions + * to the synthesis conjecture in question. This candidate { v } will then be + * tested by testing the (un)satisfiablity of P( v, cex ) for fresh cex by the + * caller. + * + * This function may also add lemmas to lems, which are sent out as lemmas + * on the output channel of quantifiers by the caller. For an example of + * such lemmas, see SygusPbe::constructCandidates. + * + * This function may return false if it does not have a candidate it wants + * to test on this iteration. In this case, lems should be non-empty. + */ + virtual bool constructCandidates(const std::vector<Node>& terms, + const std::vector<Node>& term_values, + const std::vector<Node>& candidates, + std::vector<Node>& candidate_values, + std::vector<Node>& lems) = 0; + /** register refinement lemma + * + * Assume this module, on a previous call to constructCandidates, added the + * value { v } to candidate_values for candidates = { k }. This function is + * called if the base instantiation of the synthesis conjecture has a model + * under this substitution. In particular, in the above example, this function + * is called when the refinement lemma P( v, cex ) has a model M. In calls to + * this function, the argument vars is cex and lem is P( k, cex^M ). + * + * This function may also add lemmas to lems, which are sent out as lemmas + * on the output channel of quantifiers by the caller. For an example of + * such lemmas, see Cegis::registerRefinementLemma. + */ + virtual void registerRefinementLemma(const std::vector<Node>& vars, + Node lem, + std::vector<Node>& lems) + { + } + + protected: + /** reference to quantifier engine */ + QuantifiersEngine* d_qe; + /** reference to the parent conjecture */ + CegConjecture* d_parent; +}; + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H */ |