From 724d8cf23ae74158b36b408643298c49c3b20833 Mon Sep 17 00:00:00 2001 From: Ying Sheng Date: Tue, 30 Jun 2020 04:50:40 -0700 Subject: Interpolation step 1 (#4638) This is the first step of adding Interpolation. The whole change will be adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack. The first step creates the API framework, while omits the implementation for getting interpolation. --- src/smt/smt_engine.cpp | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) (limited to 'src/smt/smt_engine.cpp') diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a6d89aaf5..bb4d82fe0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2934,6 +2934,12 @@ void SmtEngine::checkSynthSolution() } } +void SmtEngine::checkInterpol(Expr interpol, + const std::vector& easserts, + const Node& conj) +{ +} + void SmtEngine::checkAbduct(Expr a) { Assert(a.getType().isBoolean()); @@ -3152,6 +3158,19 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) } } +bool SmtEngine::getInterpol(const Expr& conj, + const Type& grammarType, + Expr& interpol) +{ + return false; +} + +bool SmtEngine::getInterpol(const Expr& conj, Expr& interpol) +{ + Type grammarType; + return getInterpol(conj, grammarType, interpol); +} + bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd) { SmtScope smts(this); -- cgit v1.2.3