category = "regular"
long = "sygus-rec-fun"
type = "bool"
- default = "false"
+ default = "true"
help = "enable efficient support for recursive functions in sygus grammars"
[[option]]
name = "sygusRecFunEvalLimit"
category = "regular"
long = "sygus-rec-fun-eval-limit=N"
- type = "int"
+ type = "unsigned"
default = "1000"
help = "use a hard limit for how many times in a given evaluator call a recursive function can be evaluated (so infinite loops can be avoided)"
SmtEngine solChecker(d_exprManager);
solChecker.setLogic(getLogicInfo());
setOption("check-synth-sol", SExpr("false"));
+ setOption("sygus-rec-fun", SExpr("false"));
Trace("check-synth-sol") << "Retrieving assertions\n";
// Build conjecture from original assertions
it = visited.find(cur[0]);
Assert(it != visited.end());
Assert(!it->second.isNull());
- Assert(it->second.isConst());
+ if (!it->second.isConst())
+ {
+ Trace("fd-eval") << "FunDefEvaluator: couldn't reduce condition of "
+ "ITE to const, FAIL\n";
+ return Node::null();
+ }
// pick child to evaluate depending on condition eval
unsigned childIdxToEval = it->second.getConst<bool>() ? 1 : 2;
Trace("fd-eval-debug2")
<< cur[childIdxToEval] << "\n";
continue;
}
+ unsigned child CVC4_UNUSED = 0;
for (const Node& cn : cur)
{
it = visited.find(cn);
Assert(!it->second.isNull());
childChanged = childChanged || cn != it->second;
children.push_back(it->second);
+ Trace("fd-eval-debug2") << "argument " << child++
+ << " eval : " << it->second << std::endl;
}
if (cur.getKind() == APPLY_UF)
{
// evaluating the body.
if (!sbody.isConst())
{
+ Trace("fd-eval-debug2") << "FunDefEvaluator: will map " << cur
+ << " from body " << sbody << "\n";
visit.push_back(cur);
visit.push_back(sbody);
}
ret = nm->mkNode(cur.getKind(), children);
ret = Rewriter::rewrite(ret);
}
+ Trace("fd-eval-debug2") << "built from arguments " << ret << "\n";
visited[cur] = ret;
}
}
else if (cur != curEval && !curEval.isConst())
{
Trace("fd-eval-debug") << "from body " << cur << std::endl;
+ Trace("fd-eval-debug") << "and eval " << curEval << 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;
+ if (it == visited.end())
+ {
+ Trace("fd-eval-debug2") << "eval without definition\n";
+ // this is the case where curEval was not a constant but it was
+ // irreducible, for example (DT_SYGUS_EVAL e args)
+ visited[cur] = curEval;
+ }
+ else
+ {
+ Trace("fd-eval-debug2")
+ << "eval with definition " << it->second << "\n";
+ visited[cur] = it->second;
}
}
+ }
} while (!visit.empty());
- Trace("fd-eval") << "FunDefEvaluator: return " << visited[n];
+ Trace("fd-eval") << "FunDefEvaluator: return " << visited[n] << ", SUCCESS\n";
Assert(visited.find(n) != visited.end());
Assert(!visited.find(n)->second.isNull());
- if (!visited.find(n)->second.isConst())
- {
- visited[n] = Node::null();
- Trace("fd-eval") << "\n with NONCONST\n";
- }
- else
- {
- Trace("fd-eval") << "\n with SUCCESS\n";
- }
return visited[n];
}
base_lem = base_lem.substitute(
sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end());
Trace("cegqi-refine") << "doRefine : rewrite..." << std::endl;
- base_lem = Rewriter::rewrite(base_lem);
+ base_lem = d_tds->rewriteNode(base_lem);
Trace("cegqi-refine") << "doRefine : register refinement lemma " << base_lem
<< "..." << std::endl;
d_master->registerRefinementLemma(sk_vars, base_lem, lems);
{
Trace("cegqi-debug") << "SynthEngine: Register quantifier : " << q
<< std::endl;
- if (d_quantEngine->getOwner(q) == this)
+ if (d_quantEngine->getOwner(q) != this)
{
- Trace("cegqi") << "Register conjecture : " << q << std::endl;
- if (options::sygusQePreproc())
- {
- d_waiting_conj.push_back(q);
- }
- else
- {
- // assign it now
- assignConjecture(q);
- }
+ return;
}
- if (options::sygusRecFun())
+ if (d_quantEngine->getQuantAttributes()->isFunDef(q))
{
- 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);
- }
+ Assert(options::sygusRecFun());
+ // If it is a recursive function definition, add it to the function
+ // definition evaluator class.
+ Trace("cegqi") << "Registering function definition : " << q << "\n";
+ FunDefEvaluator* fde = d_tds->getFunDefEvaluator();
+ fde->assertDefinition(q);
+ return;
+ }
+ Trace("cegqi") << "Register conjecture : " << q << std::endl;
+ if (options::sygusQePreproc())
+ {
+ d_waiting_conj.push_back(q);
+ }
+ else
+ {
+ // assign it now
+ assignConjecture(q);
}
}
{
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.
+ // It may have failed, in which case there are undefined symbols in res or
+ // we reached the limit of evaluations. In this case, we revert to the
+ // result of rewriting in the return statement below.
}
}
return res;
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-
// set rewrite engine as owner
setOwner(q, d_private->d_rr_engine.get(), 2);
}
- if (qa.d_sygus)
+ if (qa.d_sygus || (options::sygusRecFun() && !qa.d_fundef_f.isNull()))
{
if (d_private->d_synth_e.get() == nullptr)
{
Trace("quant-warn") << "WARNING : synth engine is null, and we have : "
<< q << std::endl;
}
- // set synth engine as owner
+ // set synth engine as owner since this is either a conjecture or a function
+ // definition to be used by sygus
setOwner(q, d_private->d_synth_e.get(), 2);
}
}
regress1/sygus/qe.sy
regress1/sygus/qf_abv.smt2
regress1/sygus/real-grammar.sy
+ regress1/sygus/rec-fun-swap.sy
regress1/sygus/rec-fun-sygus.sy
regress1/sygus/rec-fun-while-1.sy
regress1/sygus/rec-fun-while-2.sy
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2 --uf-ho
+; COMMAND-LINE: --sygus-out=status --lang=sygus2 --uf-ho
(set-logic ALL)
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --lang=sygus2
+
+(set-logic ALL)
+
+; The environment datatypes
+(declare-datatype NVars ((x) (y)))
+
+(declare-datatype Pair ((pair (first NVars) (second Int))))
+
+(declare-datatype Env ((cons (head Pair) (tail Env)) (nil)))
+
+(define-fun-rec envStore ((var NVars) (value Int) (env Env)) Env
+ (ite (is-nil env)
+ (cons (pair var value) env)
+ (ite (= var (first (head env)))
+ (cons (pair var value) (tail env))
+ (cons (head env) (envStore var value (tail env)))
+ )
+ )
+ )
+
+(define-fun-rec envSelect ((var NVars) (env Env)) Int
+ (ite (is-nil env)
+ (- 1)
+ (ite (= var (first (head env)))
+ (second (head env))
+ (envSelect var (tail env))
+ )
+ )
+ )
+
+; Syntax for arithmetic expressions
+(declare-datatype Aexp
+ (
+ (Val (val Int))
+ )
+ )
+
+; Function to evaluate arithmetic expressions
+(define-fun-rec evalA ((env Env) (a Aexp)) Int
+ (val a)
+ )
+
+; Syntax for commands
+(declare-datatype Com
+ (
+ (Skip)
+ (Assign (lhs NVars) (rhs Aexp))
+ (CSeq (cBef Com) (aAft Com))
+ )
+ )
+
+; Function to evaluate statements
+(define-fun-rec evalC ((env Env) (c Com)) Env
+ (ite (is-Skip c)
+ env
+ (ite (is-Assign c)
+ (envStore (lhs c) (evalA env (rhs c)) env)
+ (evalC (evalC env (cBef c)) (aAft c)))
+ )
+ )
+
+(synth-fun prog () Com
+ ((C Com) (V NVars) (A Aexp) (I Int))
+ (
+ (C Com (Skip (Assign V A) (CSeq C C)))
+ (V NVars (x y))
+ (A Aexp ((Val I)))
+ (I Int (0 1))
+ )
+)
+
+(constraint (= (evalC (cons (pair y 0) (cons (pair x 1) nil)) prog) (cons (pair y 1) (cons (pair x 0) nil))))
+
+(check-synth)
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2
+; COMMAND-LINE: --sygus-out=status --lang=sygus2
(set-logic ALL)
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --lang=sygus2 --sygus-rec-fun --no-e-matching --no-check-synth-sol
+; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol
(set-logic ALL)
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --lang=sygus2 --sygus-rec-fun --no-e-matching --no-check-synth-sol
+; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol
(set-logic ALL)
; EXPECT: unknown
-; COMMAND-LINE: --sygus-out=status --lang=sygus2 --sygus-rec-fun --no-e-matching --no-check-synth-sol
+; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol
(set-logic ALL)
projects / cvc5.git / commitdiff