summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/quantifiers/fun_def_evaluator.cpp57
-rw-r--r--src/theory/quantifiers/sygus/synth_conjecture.cpp3
-rw-r--r--test/regress/CMakeLists.txt2
-rw-r--r--test/regress/regress1/sygus/rec-fun-while-1.sy92
-rw-r--r--test/regress/regress1/sygus/rec-fun-while-2.sy93
5 files changed, 243 insertions, 4 deletions
diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp
index 376d0eb47..1528d5338 100644
--- a/src/theory/quantifiers/fun_def_evaluator.cpp
+++ b/src/theory/quantifiers/fun_def_evaluator.cpp
@@ -75,6 +75,13 @@ Node FunDefEvaluator::evaluate(Node n) const
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;
@@ -102,6 +109,28 @@ Node FunDefEvaluator::evaluate(Node n) const
{
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);
@@ -114,6 +143,8 @@ Node FunDefEvaluator::evaluate(Node n) const
{
// 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())
{
@@ -123,6 +154,8 @@ Node FunDefEvaluator::evaluate(Node n) const
}
// 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())
{
@@ -131,6 +164,17 @@ Node FunDefEvaluator::evaluate(Node n) const
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;
@@ -164,11 +208,18 @@ Node FunDefEvaluator::evaluate(Node n) const
}
}
} 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];
}
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 6e69715ef..6591e6828 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -591,7 +591,8 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
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;
}
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 3c060a304..d810aa5be 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1743,6 +1743,8 @@ set(regress_1_tests
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
diff --git a/test/regress/regress1/sygus/rec-fun-while-1.sy b/test/regress/regress1/sygus/rec-fun-while-1.sy
new file mode 100644
index 000000000..c175094ee
--- /dev/null
+++ b/test/regress/regress1/sygus/rec-fun-while-1.sy
@@ -0,0 +1,92 @@
+; 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)
diff --git a/test/regress/regress1/sygus/rec-fun-while-2.sy b/test/regress/regress1/sygus/rec-fun-while-2.sy
new file mode 100644
index 000000000..87a4f2a6e
--- /dev/null
+++ b/test/regress/regress1/sygus/rec-fun-while-2.sy
@@ -0,0 +1,93 @@
+; 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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback