mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

trying alternate encoding of distint

Browse source
This commit is contained in:
Ken McMillan 2014-04-22 16:42:35 -07:00
parent 77f8aa9f6b
commit 2755854c81
1 changed files with 18 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/duality/duality.h
View file

@ -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<sort> sv;
sv.push_back(s);
int nargs = axiom.num_args();
std::vector<expr> 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);
}