From d45cbb3cb2c1de662fd43083b2addf381a6527cf Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 10 Dec 2013 16:26:35 -0800 Subject: [PATCH] fixed interpolation bug --- src/duality/duality_rpfp.cpp | 2 +- src/interp/iz3translate.cpp | 15 +++++++++++++++ 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 3fc755d85..f37545b48 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -1993,7 +1993,7 @@ namespace Duality { aux_solver.pop(1); Push(); FixCurrentStateFull(node->Outgoing); - // ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); + ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); check_result foo = Check(root); if(foo != unsat) throw "should be unsat"; diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 7dfa48cdd..63f3dd251 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -1460,6 +1460,21 @@ public: } } + /* this is the symmetry rule for ~=, that is, takes x ~= y and yields y ~= x. + the proof idiom uses commutativity, monotonicity and mp, but we replace it here + with symmtrey and resolution, that is, we prove y = x |- x = y, then resolve + with the proof of ~(x=y) to get ~y=x. */ + if(dk == PR_MODUS_PONENS && pr(prem(proof,1)) == PR_MONOTONICITY && pr(prem(prem(proof,1),0)) == PR_COMMUTATIVITY && num_prems(prem(proof,1)) == 1){ + Iproof::node ante = translate_main(prem(proof,0),false); + ast eq0 = arg(conc(prem(prem(proof,1),0)),0); + ast eq1 = arg(conc(prem(prem(proof,1),0)),1); + Iproof::node eq1hy = iproof->make_hypothesis(eq1); + Iproof::node eq0pf = iproof->make_symmetry(eq0,eq1,eq1hy); + std::vector clause; // just a dummy + res = iproof->make_resolution(eq0,clause,ante,eq0pf); + return res; + } + // translate all the premises std::vector args(nprems); for(unsigned i = 0; i < nprems; i++)