From b19fbe4429e6414db4afd12efa69228e284e6834 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 30 Oct 2015 15:55:18 -0700 Subject: [PATCH] make sure to bring constraints into clausal form before using the th_axiom assertion. Old version should not have been used as a template for copying, as in issue #227 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_dl.cpp | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp index 43ec5682e..3c80a5ef2 100644 --- a/src/smt/theory_dl.cpp +++ b/src/smt/theory_dl.cpp @@ -249,9 +249,20 @@ namespace smt { sort* s = m().get_sort(x); func_decl* r, *v; get_rep(s, r, v); - app* lt1 = u().mk_lt(x,y); - app* lt2 = m().mk_not(b().mk_ule(m().mk_app(r,y),m().mk_app(r,x))); - assert_cnstr(m().mk_iff(lt1, lt2)); + app_ref lt(m()), le(m()); + lt = u().mk_lt(x,y); + le = b().mk_ule(m().mk_app(r,y),m().mk_app(r,x)); + context& ctx = get_context(); + ctx.internalize(lt, false); + ctx.internalize(le, false); + literal lit1(ctx.get_literal(lt)); + literal lit2(ctx.get_literal(le)); + ctx.mark_as_relevant(lit1); + ctx.mark_as_relevant(lit2); + literal lits1[2] = { lit1, lit2 }; + literal lits2[2] = { ~lit1, ~lit2 }; + ctx.mk_th_axiom(get_id(), 2, lits1); + ctx.mk_th_axiom(get_id(), 2, lits2); } void assert_cnstr(expr* e) {