Trace("fd-eval-debug") << "constant " << cur << std::endl;
visited[cur] = cur;
}
+ else if (cur.getKind() == ITE)
+ {
+ Trace("fd-eval-debug") << "ITE " << cur << std::endl;
+ visited[cur] = Node::null();
+ visit.push_back(cur);
+ visit.push_back(cur[0]);
+ }
else
{
Trace("fd-eval-debug") << "recurse " << cur << std::endl;
{
children.push_back(cur.getOperator());
}
+ else if (ck == ITE)
+ {
+ // get evaluation of condition
+ it = visited.find(cur[0]);
+ Assert(it != visited.end());
+ Assert(!it->second.isNull());
+ Assert(it->second.isConst());
+ // pick child to evaluate depending on condition eval
+ unsigned childIdxToEval = it->second.getConst<bool>() ? 1 : 2;
+ Trace("fd-eval-debug2")
+ << "FunDefEvaluator: result of ITE condition : "
+ << it->second.getConst<bool>() << "\n";
+ // the result will be the result of evaluation the child
+ visited[cur] = cur[childIdxToEval];
+ // push back self and child. The child will be evaluated first and
+ // result will be the result of evaluation child
+ visit.push_back(cur);
+ visit.push_back(cur[childIdxToEval]);
+ Trace("fd-eval-debug2") << "FunDefEvaluator: result will be from : "
+ << cur[childIdxToEval] << "\n";
+ continue;
+ }
for (const Node& cn : cur)
{
it = visited.find(cn);
{
// need to evaluate it
f = cur.getOperator();
+ Trace("fd-eval-debug2")
+ << "FunDefEvaluator: need to eval " << f << "\n";
itf = d_funDefMap.find(f);
if (itf == d_funDefMap.end())
{
}
// get the function definition
Node sbody = itf->second.d_body;
+ Trace("fd-eval-debug2")
+ << "FunDefEvaluator: definition: " << sbody << "\n";
const std::vector<Node>& args = itf->second.d_args;
if (!args.empty())
{
args.begin(), args.end(), children.begin(), children.end());
// rewrite it
sbody = Rewriter::rewrite(sbody);
+ if (Trace.isOn("fd-eval-debug2"))
+ {
+ Trace("fd-eval-debug2")
+ << "FunDefEvaluator: evaluation with args:\n";
+ for (const Node& child : children)
+ {
+ Trace("fd-eval-debug2") << "..." << child << "\n";
+ }
+ Trace("fd-eval-debug2")
+ << "FunDefEvaluator: results in " << sbody << "\n";
+ }
}
// our result is the result of the body
visited[cur] = sbody;
}
}
} while (!visit.empty());
+ Trace("fd-eval") << "FunDefEvaluator: return " << visited[n];
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;
+ 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];
}
Trace("cegqi-debug") << "...squery : " << squery << std::endl;
squery = Rewriter::rewrite(squery);
Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl;
- Assert(squery.isConst() && squery.getConst<bool>());
+ Assert(options::sygusRecFun()
+ || (squery.isConst() && squery.getConst<bool>()));
#endif
return false;
}
regress1/sygus/qf_abv.smt2
regress1/sygus/real-grammar.sy
regress1/sygus/rec-fun-sygus.sy
+ regress1/sygus/rec-fun-while-1.sy
+ regress1/sygus/rec-fun-while-2.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 --lang=sygus2 --sygus-rec-fun --no-e-matching --no-check-synth-sol
+
+(set-logic ALL)
+
+; The environment datatypes
+(declare-datatype NVars ((x)))
+
+(declare-datatype Pair ((build (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 (build var value) env)
+ (ite (= var (first (head env)))
+ (cons (build 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)
+ 0
+ (ite (= var (first (head env)))
+ (second (head env))
+ (envSelect var (tail env))
+ )
+ )
+ )
+
+; Syntax for arithmetic expressions
+(declare-datatype Aexp
+ (
+ (Val (val Int))
+ (Var (name NVars))
+ (Add (addL Aexp) (addR Aexp))
+ )
+ )
+
+; Function to evaluate arithmetic expressions
+(define-fun-rec evalA ((env Env) (a Aexp)) Int
+ (ite (is-Val a)
+ (val a)
+ (envSelect (name a) env)
+ ))
+
+; Syntax for boolean expressions
+(declare-datatype Bexp
+ (
+ (LT (ltL Aexp) (ltR Aexp))
+ )
+ )
+
+; Function to evaluate boolean expressions
+(define-fun-rec evalB ((env Env) (b Bexp)) Bool
+ (< (evalA env (ltL b)) (evalA env (ltR b)))
+ )
+
+; Syntax for commands
+(declare-datatype Com
+ (
+ (Assign (lhs NVars) (rhs Aexp))
+ (While (wCond Bexp) (wCom Com))
+ )
+ )
+
+; Function to evaluate statements
+(define-fun-rec evalC ((env Env) (c Com)) Env
+ (ite (is-Assign c)
+ (envStore (lhs c) (evalA env (rhs c)) env)
+ (ite (evalB env (wCond c)) (evalC (evalC env (wCom c)) c) env)
+ )
+ )
+
+(synth-fun prog () Com
+ ((C1 Com) (C2 Com) (VX NVars) (A1 Aexp) (A2 Aexp) (B Bexp) (I Int))
+ (
+ (C1 Com ((While B C2)))
+ (C2 Com ((Assign VX A2)))
+ (VX NVars (x))
+ (A1 Aexp ((Var VX)))
+ (A2 Aexp ((Val I)))
+ (B Bexp ((LT A1 A2)))
+ (I Int (0 1 (+ I I)))
+ )
+)
+
+(constraint (= (evalC (cons (build x 0) nil) prog) (cons (build x 2) nil)))
+
+(check-synth)
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --lang=sygus2 --sygus-rec-fun --no-e-matching --no-check-synth-sol
+
+(set-logic ALL)
+
+; The environment datatypes
+(declare-datatype NVars ((x) (y)))
+
+(declare-datatype Pair ((build (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 (build var value) env)
+ (ite (= var (first (head env)))
+ (cons (build 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)
+ 0
+ (ite (= var (first (head env)))
+ (second (head env))
+ (envSelect var (tail env))
+ )
+ )
+ )
+
+; Syntax for arithmetic expressions
+(declare-datatype Aexp
+ (
+ (Val (val Int))
+ (Var (name NVars))
+ (Add (addL Aexp) (addR Aexp))
+ (Sub (subL Aexp) (subR Aexp))
+ )
+ )
+
+; Function to evaluate arithmetic expressions
+(define-fun-rec evalA ((env Env) (a Aexp)) Int
+ (ite (is-Val a)
+ (val a)
+ (envSelect (name a) env)
+ ))
+
+; Syntax for boolean expressions
+(declare-datatype Bexp
+ (
+ (GTH (geqL Aexp) (geqR Aexp))
+ )
+ )
+
+; Function to evaluate boolean expressions
+(define-fun-rec evalB ((env Env) (b Bexp)) Bool
+ (> (evalA env (geqL b)) (evalA env (geqR b)))
+ )
+
+; Syntax for commands
+(declare-datatype Com
+ (
+ (Assign (lhs NVars) (rhs Aexp))
+ (While (wCond Bexp) (wCom Com))
+ )
+ )
+
+; Function to evaluate statements
+(define-fun-rec evalC ((env Env) (c Com)) Env
+ (ite (is-Assign c)
+ (envStore (lhs c) (evalA env (rhs c)) env)
+ (ite (evalB env (wCond c)) (evalC (evalC env (wCom c)) c) env)
+ )
+ )
+
+(synth-fun prog () Com
+ ((C1 Com) (C2 Com) (VX NVars) (A1 Aexp) (A2 Aexp) (B Bexp) (I Int))
+ (
+ (C1 Com ((While B C2)))
+ (C2 Com ((Assign VX A2)))
+ (VX NVars (x))
+ (A1 Aexp ((Var VX)))
+ (A2 Aexp ((Val I)))
+ (B Bexp ((GTH A2 A1)))
+ (I Int (2))
+ )
+)
+
+(constraint (= (evalC (cons (build x 0) nil) prog) (cons (build x 2) nil)))
+
+(check-synth)
projects / cvc5.git / commitdiff