From 628a13f0e5f95fb3372c0676e91a9e719fa05b8c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 Oct 2021 15:47:06 -0500 Subject: Make SyGuS solver robust to non-closed enumerable sorts (#7417) This makes the SyGuS solver robust to variables that are not closed enumerable, e.g. arrays of uninterpreted sorts. It corrects an issue in array's mkGroundTerm issue which would allow constants to enter into constraints for SyGuS problems with arrays. This method does not cause further issues currently since quantifiers is guarded in several places to ensure array constants are not constructed via this method. It also makes it so that we don't add explicit CEGIS refinement lemmas unless evaluation unfolding is enabled and the counterexamples are from closed enumerable types; there is no reason to add these unless we are combining with evaluation unfolding. This addresses several of the issues raised in #6605. --- test/regress/regress1/sygus/array-uc.sy | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 test/regress/regress1/sygus/array-uc.sy (limited to 'test/regress/regress1/sygus/array-uc.sy') diff --git a/test/regress/regress1/sygus/array-uc.sy b/test/regress/regress1/sygus/array-uc.sy new file mode 100644 index 000000000..b3d950436 --- /dev/null +++ b/test/regress/regress1/sygus/array-uc.sy @@ -0,0 +1,14 @@ +; COMMAND-LINE: --sygus-out=status +; EXPECT: unsat +(set-logic ALL) +(declare-sort U 0) +(synth-fun f ((x (Array U Int)) (y U)) Bool) + +(declare-var x (Array U Int)) +(declare-var y U) + +(constraint (= (f (store x y 0) y) true)) +(constraint (= (f (store x y 1) y) false)) + +; f can be (= (select x y) 0) +(check-synth) -- cgit v1.2.3