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.
// for array-constant attributes
#include "expr/array_store_all.h"
#include "theory/arrays/theory_arrays_rewriter.h"
+#include "theory/builtin/theory_builtin_type_rules.h"
#include "theory/type_enumerator.h"
#include "util/cardinality.h"
Node ArraysProperties::mkGroundTerm(TypeNode type)
{
- return *TypeEnumerator(type);
+ Assert(type.getKind() == kind::ARRAY_TYPE);
+ TypeNode elemType = type.getArrayConstituentType();
+ Node elem = elemType.mkGroundTerm();
+ if (elem.isConst())
+ {
+ return NodeManager::currentNM()->mkConst(ArrayStoreAll(type, elem));
+ }
+ // Note the distinction between mkGroundTerm and mkGroundValue. While
+ // an arbitrary value can be obtained by calling the type enumerator here,
+ // that is wrong for types that are not closed enumerable since it may
+ // return a term containing values that should not appear in e.g. assertions.
+ // For example, arrays whose element type is an uninterpreted sort will
+ // incorrectly introduce uninterpreted sort values if this is done.
+ // It is currently infeasible to construct an ArrayStoreAll with the element
+ // type's mkGroundTerm as an argument when that term is not constant.
+ // Thus, we must simply return a fresh Skolem here, using the same utility
+ // as that of uninterpreted sorts.
+ return builtin::SortProperties::mkGroundTerm(type);
}
TypeNode ArrayPartialSelectTypeRule::computeType(NodeManager* nodeManager,
SynthConjecture* p)
: SygusModule(env, qs, qim, tds, p),
d_eval_unfold(tds->getEvalUnfold()),
+ d_cexClosedEnum(false),
d_cegis_sampler(env),
d_usingSymCons(false)
{
bool Cegis::initialize(Node conj, Node n, const std::vector<Node>& candidates)
{
d_base_body = n;
+ d_cexClosedEnum = true;
if (d_base_body.getKind() == NOT && d_base_body[0].getKind() == FORALL)
{
for (const Node& v : d_base_body[0][0])
{
d_base_vars.push_back(v);
+ if (!v.getType().isClosedEnumerable())
+ {
+ // not closed enumerable, refinement lemmas cannot be sent to the
+ // quantifier-free datatype solver
+ d_cexClosedEnum = false;
+ }
}
d_base_body = d_base_body[0][1];
}
void Cegis::registerRefinementLemma(const std::vector<Node>& vars, Node lem)
{
addRefinementLemma(lem);
- // Make the refinement lemma and add it to lems.
- // This lemma is guarded by the parent's guard, which has the semantics
- // "this conjecture has a solution", hence this lemma states:
- // if the parent conjecture has a solution, it satisfies the specification
- // for the given concrete point.
- Node rlem =
- NodeManager::currentNM()->mkNode(OR, d_parent->getGuard().negate(), lem);
- d_qim.addPendingLemma(rlem, InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE);
+ // must be closed enumerable
+ if (d_cexClosedEnum && options().quantifiers.sygusEvalUnfold)
+ {
+ // Make the refinement lemma and add it to lems.
+ // This lemma is guarded by the parent's guard, which has the semantics
+ // "this conjecture has a solution", hence this lemma states:
+ // if the parent conjecture has a solution, it satisfies the specification
+ // for the given concrete point.
+ Node rlem = NodeManager::currentNM()->mkNode(
+ OR, d_parent->getGuard().negate(), lem);
+ d_qim.addPendingLemma(rlem, InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE);
+ }
}
bool Cegis::usingRepairConst() { return true; }
std::vector<Node> d_rl_vals;
/** all variables appearing in refinement lemmas */
std::unordered_set<Node> d_refinement_lemma_vars;
+ /**
+ * Are the counterexamples we are handling in this class of only closed
+ * enumerable types (see TypeNode::isClosedEnumerable). If this is false,
+ * then CEGIS refinement lemmas can contain terms that are unhandled by
+ * theory solvers, e.g. uninterpreted constants.
+ */
+ bool d_cexClosedEnum;
/** adds lem as a refinement lemma */
void addRefinementLemma(Node lem);
#include "expr/ascription_type.h"
#include "expr/dtype_cons.h"
+#include "expr/node_algorithm.h"
#include "options/quantifiers_options.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/datatypes/sygus_datatype_utils.h"
{
// generate constant array over the first element of the constituent type
Node c = type.mkGroundTerm();
+ // note that c should never contain an uninterpreted constant
+ Assert(!expr::hasSubtermKind(UNINTERPRETED_CONSTANT, c));
ops.push_back(c);
}
else if (type.isRoundingMode())
regress1/sygus/abv.sy
regress1/sygus/array-grammar-store.sy
regress1/sygus/array_search_5-Q-easy.sy
+ regress1/sygus/array-uc.sy
regress1/sygus/bvudiv-by-2.sy
regress1/sygus/cegar1.sy
regress1/sygus/cegis-unif-inv-eq-fair.sy
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff