theory/quantifiers/fmf/model_builder.h
theory/quantifiers/fmf/model_engine.cpp
theory/quantifiers/fmf/model_engine.h
+ theory/quantifiers/fun_def_evaluator.cpp
+ theory/quantifiers/fun_def_evaluator.h
theory/quantifiers/fun_def_process.cpp
theory/quantifiers/fun_def_process.h
theory/quantifiers/inst_match.cpp
default = "false"
help = "static inference techniques for computing whether arguments of functions-to-synthesize are relevant"
+[[option]]
+ name = "sygusRecFun"
+ category = "regular"
+ long = "sygus-rec-fun"
+ type = "bool"
+ default = "false"
+ help = "enable efficient support for recursive functions in sygus grammars"
+
# Internal uses of sygus
[[option]]
--- /dev/null
+/********************* */
+/*! \file fun_def_evaluator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 techniques for evaluating terms with recursively
+ ** defined functions.
+ **/
+
+#include "theory/quantifiers/fun_def_evaluator.h"
+
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/rewriter.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+FunDefEvaluator::FunDefEvaluator() {}
+
+void FunDefEvaluator::assertDefinition(Node q)
+{
+ Trace("fd-eval") << "FunDefEvaluator: assertDefinition " << q << std::endl;
+ Node h = QuantAttributes::getFunDefHead(q);
+ if (h.isNull())
+ {
+ // not a function definition
+ return;
+ }
+ // h possibly with zero arguments?
+ Node f = h.hasOperator() ? h.getOperator() : h;
+ Assert(d_funDefMap.find(f) == d_funDefMap.end())
+ << "FunDefEvaluator::assertDefinition: function already defined";
+ FunDefInfo& fdi = d_funDefMap[f];
+ fdi.d_body = QuantAttributes::getFunDefBody(q);
+ Assert(!fdi.d_body.isNull());
+ fdi.d_args.insert(fdi.d_args.end(), q[0].begin(), q[0].end());
+ Trace("fd-eval") << "FunDefEvaluator: function " << f << " is defined with "
+ << fdi.d_args << " / " << fdi.d_body << std::endl;
+}
+
+Node FunDefEvaluator::evaluate(Node n) const
+{
+ // should do standard rewrite before this call
+ Assert(Rewriter::rewrite(n) == n);
+ Trace("fd-eval") << "FunDefEvaluator: evaluate " << n << std::endl;
+ NodeManager* nm = NodeManager::currentNM();
+ std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+ std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::map<Node, FunDefInfo>::const_iterator itf;
+ std::vector<TNode> visit;
+ TNode cur;
+ TNode curEval;
+ Node f;
+ visit.push_back(n);
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ it = visited.find(cur);
+ Trace("fd-eval-debug") << "evaluate subterm " << cur << std::endl;
+
+ if (it == visited.end())
+ {
+ if (cur.isConst())
+ {
+ Trace("fd-eval-debug") << "constant " << cur << std::endl;
+ visited[cur] = cur;
+ }
+ else
+ {
+ Trace("fd-eval-debug") << "recurse " << cur << std::endl;
+ visited[cur] = Node::null();
+ visit.push_back(cur);
+ for (const Node& cn : cur)
+ {
+ visit.push_back(cn);
+ }
+ }
+ }
+ else
+ {
+ curEval = it->second;
+ if (curEval.isNull())
+ {
+ Trace("fd-eval-debug") << "from arguments " << cur << std::endl;
+ Node ret = cur;
+ bool childChanged = false;
+ std::vector<Node> children;
+ Kind ck = cur.getKind();
+ // If a parameterized node that is not APPLY_UF (which is handled below,
+ // we add it to the children vector.
+ if (ck != APPLY_UF && cur.getMetaKind() == metakind::PARAMETERIZED)
+ {
+ children.push_back(cur.getOperator());
+ }
+ for (const Node& cn : cur)
+ {
+ it = visited.find(cn);
+ Assert(it != visited.end());
+ Assert(!it->second.isNull());
+ childChanged = childChanged || cn != it->second;
+ children.push_back(it->second);
+ }
+ if (cur.getKind() == APPLY_UF)
+ {
+ // need to evaluate it
+ f = cur.getOperator();
+ itf = d_funDefMap.find(f);
+ if (itf == d_funDefMap.end())
+ {
+ Trace("fd-eval") << "FunDefEvaluator: no definition for " << f
+ << ", FAIL" << std::endl;
+ return Node::null();
+ }
+ // get the function definition
+ Node sbody = itf->second.d_body;
+ const std::vector<Node>& args = itf->second.d_args;
+ if (!args.empty())
+ {
+ // invoke it on arguments
+ sbody = sbody.substitute(
+ args.begin(), args.end(), children.begin(), children.end());
+ // rewrite it
+ sbody = Rewriter::rewrite(sbody);
+ }
+ // our result is the result of the body
+ visited[cur] = sbody;
+ // If its not constant, we push back self and the substituted body.
+ // Thus, we evaluate the body first; our result will be the result of
+ // evaluating the body.
+ if (!sbody.isConst())
+ {
+ visit.push_back(cur);
+ visit.push_back(sbody);
+ }
+ }
+ else
+ {
+ if (childChanged)
+ {
+ ret = nm->mkNode(cur.getKind(), children);
+ ret = Rewriter::rewrite(ret);
+ }
+ if (!ret.isConst())
+ {
+ Trace("fd-eval") << "FunDefEvaluator: non-constant subterm " << ret
+ << ", FAIL" << std::endl;
+ // failed, possibly due to free variable
+ return Node::null();
+ }
+ visited[cur] = ret;
+ }
+ }
+ else if (!curEval.isConst())
+ {
+ Trace("fd-eval-debug") << "from body " << cur << std::endl;
+ // we had to evaluate our body, which should have a definition now
+ it = visited.find(curEval);
+ Assert(it != visited.end());
+ // our definition is the result of the body
+ visited[cur] = it->second;
+ Assert(it->second.isConst());
+ }
+ }
+ } while (!visit.empty());
+ Assert(visited.find(n) != visited.end());
+ Assert(!visited.find(n)->second.isNull());
+ Assert(visited.find(n)->second.isConst());
+ Trace("fd-eval") << "FunDefEvaluator: return SUCCESS " << visited[n]
+ << std::endl;
+ return visited[n];
+}
+
+bool FunDefEvaluator::hasDefinitions() const { return !d_funDefMap.empty(); }
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file fun_def_evaluator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 Techniques for evaluating terms with recursively defined functions.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__QUANTIFIERS_FUN_DEF_EVALUATOR_H
+#define CVC4__QUANTIFIERS_FUN_DEF_EVALUATOR_H
+
+#include <map>
+#include <vector>
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/**
+ * Techniques for evaluating recursively defined functions.
+ */
+class FunDefEvaluator
+{
+ public:
+ FunDefEvaluator();
+ ~FunDefEvaluator() {}
+ /**
+ * Assert definition of a (recursive) function definition given by quantified
+ * formula q.
+ */
+ void assertDefinition(Node q);
+ /**
+ * Simplify node based on the (recursive) function definitions known by this
+ * class. If n cannot be simplified to a constant, then this method returns
+ * null.
+ */
+ Node evaluate(Node n) const;
+ /**
+ * Has a call to assertDefinition been made? If this returns false, then
+ * the evaluate method is the same as calling the rewriter, and returning
+ * false if the result is non-constant.
+ */
+ bool hasDefinitions() const;
+
+ private:
+ /** information cached per function definition */
+ class FunDefInfo
+ {
+ public:
+ /** the body */
+ Node d_body;
+ /** the formal argument list */
+ std::vector<Node> d_args;
+ };
+ /** maps functions to the above information */
+ std::map<Node, FunDefInfo> d_funDefMap;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
+
+#endif
return false;
}
- lem = Rewriter::rewrite(lem);
+ // simplify the lemma based on the term database sygus utility
+ lem = d_tds->rewriteNode(lem);
// eagerly unfold applications of evaluation function
Trace("cegqi-debug") << "pre-unfold counterexample : " << lem << std::endl;
// record the instantiation
namespace quantifiers {
SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c)
- : QuantifiersModule(qe)
+ : QuantifiersModule(qe), d_tds(qe->getTermDatabaseSygus())
{
d_conjs.push_back(std::unique_ptr<SynthConjecture>(
new SynthConjecture(d_quantEngine, this)));
void SynthEngine::registerQuantifier(Node q)
{
+ Trace("cegqi-debug") << "SynthEngine: Register quantifier : " << q
+ << std::endl;
if (d_quantEngine->getOwner(q) == this)
{
Trace("cegqi") << "Register conjecture : " << q << std::endl;
assignConjecture(q);
}
}
- else
+ if (options::sygusRecFun())
{
- Trace("cegqi-debug") << "Register quantifier : " << q << std::endl;
+ if (d_quantEngine->getQuantAttributes()->isFunDef(q))
+ {
+ // If it is a recursive function definition, add it to the function
+ // definition evaluator class.
+ FunDefEvaluator* fde = d_tds->getFunDefEvaluator();
+ fde->assertDefinition(q);
+ }
}
}
{
typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
- private:
- /** the conjecture formula(s) we are waiting to assign */
- std::vector<Node> d_waiting_conj;
- /** The synthesis conjectures that this class is managing. */
- std::vector<std::unique_ptr<SynthConjecture> > d_conjs;
- /**
- * The first conjecture in the above vector. We track this conjecture
- * so that a synthesis conjecture can be preregistered during a call to
- * preregisterAssertion.
- */
- SynthConjecture* d_conj;
- /** assign quantified formula q as a conjecture
- *
- * This method either assigns q to a synthesis conjecture object in d_conjs,
- * or otherwise reduces q to an equivalent form. This method does the latter
- * if this class determines that it would rather rewrite q to an equivalent
- * form r (in which case this method returns the lemma q <=> r). An example of
- * this is the quantifier elimination step option::sygusQePreproc().
- */
- void assignConjecture(Node q);
- /** check conjecture
- *
- * This method returns true if the conjecture is finished processing solutions
- * for this call to SynthEngine::check().
- */
- bool checkConjecture(SynthConjecture* conj);
-
public:
SynthEngine(QuantifiersEngine* qe, context::Context* c);
~SynthEngine();
~Statistics();
}; /* class SynthEngine::Statistics */
Statistics d_statistics;
+
+ private:
+ /** term database sygus of d_qe */
+ TermDbSygus* d_tds;
+ /** the conjecture formula(s) we are waiting to assign */
+ std::vector<Node> d_waiting_conj;
+ /** The synthesis conjectures that this class is managing. */
+ std::vector<std::unique_ptr<SynthConjecture> > d_conjs;
+ /**
+ * The first conjecture in the above vector. We track this conjecture
+ * so that a synthesis conjecture can be preregistered during a call to
+ * preregisterAssertion.
+ */
+ SynthConjecture* d_conj;
+ /** assign quantified formula q as a conjecture
+ *
+ * This method either assigns q to a synthesis conjecture object in d_conjs,
+ * or otherwise reduces q to an equivalent form. This method does the latter
+ * if this class determines that it would rather rewrite q to an equivalent
+ * form r (in which case this method returns the lemma q <=> r). An example of
+ * this is the quantifier elimination step option::sygusQePreproc().
+ */
+ void assignConjecture(Node q);
+ /** check conjecture
+ *
+ * This method returns true if the conjecture is finished processing solutions
+ * for this call to SynthEngine::check().
+ */
+ bool checkConjecture(SynthConjecture* conj);
}; /* class SynthEngine */
} // namespace quantifiers
d_syexp(new SygusExplain(this)),
d_ext_rw(new ExtendedRewriter(true)),
d_eval(new Evaluator),
+ d_funDefEval(new FunDefEvaluator),
d_eval_unfold(new SygusEvalUnfold(this))
{
d_true = NodeManager::currentNM()->mkConst( true );
return d_tinfo[tn];
}
+Node TermDbSygus::rewriteNode(Node n) const
+{
+ Node res = Rewriter::rewrite(n);
+ if (options::sygusRecFun())
+ {
+ if (d_funDefEval->hasDefinitions())
+ {
+ // If recursive functions are enabled, then we use the recursive function
+ // evaluation utility.
+ Node fres = d_funDefEval->evaluate(res);
+ if (!fres.isNull())
+ {
+ return fres;
+ }
+ // It may have failed, in which case there are undefined symbols in res.
+ // In this case, we revert to the result of rewriting in the return
+ // statement below.
+ }
+ }
+ return res;
+}
+
unsigned TermDbSygus::getSelectorWeight(TypeNode tn, Node sel)
{
std::map<TypeNode, std::map<Node, unsigned> >::iterator itsw =
return res;
}
res = bn.substitute(varlist.begin(), varlist.end(), args.begin(), args.end());
- return Rewriter::rewrite(res);
+ // Call the rewrite node function, which may involve recursive function
+ // evaluation.
+ return rewriteNode(res);
}
Node TermDbSygus::evaluateWithUnfolding(
#include "theory/evaluator.h"
#include "theory/quantifiers/extended_rewrite.h"
+#include "theory/quantifiers/fun_def_evaluator.h"
#include "theory/quantifiers/sygus/sygus_eval_unfold.h"
#include "theory/quantifiers/sygus/sygus_explain.h"
#include "theory/quantifiers/sygus/type_info.h"
ExtendedRewriter* getExtRewriter() { return d_ext_rw.get(); }
/** get the evaluator */
Evaluator* getEvaluator() { return d_eval.get(); }
+ /** (recursive) function evaluator utility */
+ FunDefEvaluator* getFunDefEvaluator() { return d_funDefEval.get(); }
/** evaluation unfolding utility */
SygusEvalUnfold* getEvalUnfold() { return d_eval_unfold.get(); }
//------------------------------end utilities
* (a subfield type of) a type that has been registered to this class.
*/
SygusTypeInfo& getTypeInfo(TypeNode tn);
+ /**
+ * Rewrite the given node using the utilities in this class. This may
+ * involve (recursive function) evaluation.
+ */
+ Node rewriteNode(Node n) const;
/** print to sygus stream n on trace c */
static void toStreamSygus(const char* c, Node n);
std::unique_ptr<ExtendedRewriter> d_ext_rw;
/** evaluator */
std::unique_ptr<Evaluator> d_eval;
+ /** (recursive) function evaluator utility */
+ std::unique_ptr<FunDefEvaluator> d_funDefEval;
/** evaluation function unfolding utility */
std::unique_ptr<SygusEvalUnfold> d_eval_unfold;
//------------------------------end utilities
regress1/sygus/qe.sy
regress1/sygus/qf_abv.smt2
regress1/sygus/real-grammar.sy
+ regress1/sygus/rec-fun-sygus.sy
regress1/sygus/re-concat.sy
regress1/sygus/repair-const-rl.sy
regress1/sygus/simple-regexp.sy
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2
+
+(set-logic ALL)
+
+(declare-datatype List ((cons (head Int) (tail List)) (nil)))
+
+(define-fun-rec sum ((x List)) Int (ite ((_ is nil) x) 0 (+ (head x) (sum (tail x)))))
+(define-fun-rec size ((x List)) Int (ite ((_ is nil) x) 0 (+ 1 (size (tail x)))))
+
+(synth-fun f ((x List)) Int
+ ((I Int) (L List))
+ ((I Int ((+ I I) (sum L) (size L) 0 1))
+ (L List (x))))
+
+(constraint (= (f (cons 3 (cons 4 (cons 5 nil)))) 15))
+(constraint (= (f (cons 3 (cons (- 4) (cons 5 nil)))) 7))
+(constraint (= (f (cons 5 (cons 5 nil))) 12))
+(constraint (= (f (cons 0 (cons 0 (cons 0 (cons 0 (cons 0 (cons 0 nil))))))) 6))
+(constraint (= (f (cons (- 2) (cons 0 nil))) 0))
+(check-synth)
projects / cvc5.git / commitdiff