From 2755854c81e9cf6ec3da1d4b9ae0685e24252d67 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 22 Apr 2014 16:42:35 -0700 Subject: [PATCH] trying alternate encoding of distint --- src/duality/duality.h | 21 ++++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index 572ce427b..77fbdfd55 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -253,11 +253,26 @@ protected: } void assert_axiom(const expr &axiom){ -#if 0 - // HACK: large "distict" predicates can kill the legacy SMT solver -- ignore them +#if 1 + // HACK: large "distict" predicates can kill the legacy SMT solver. + // encode them with a UIF if(axiom.is_app() && axiom.decl().get_decl_kind() == Distinct) - if(axiom.num_args() > 10) + if(axiom.num_args() > 10){ + sort s = axiom.arg(0).get_sort(); + std::vector sv; + sv.push_back(s); + int nargs = axiom.num_args(); + std::vector args(nargs); + func_decl f = ctx->fresh_func_decl("@distinct",sv,ctx->int_sort()); + for(int i = 0; i < nargs; i++){ + expr a = axiom.arg(i); + expr new_cnstr = f(a) == ctx->int_val(i); + args[i] = new_cnstr; + } + expr cnstr = ctx->make(And,args); + islvr->AssertInterpolationAxiom(cnstr); return; + } #endif islvr->AssertInterpolationAxiom(axiom); }