From: Ying Sheng Date: Tue, 15 Sep 2020 01:47:15 +0000 (+0800) Subject: Interpolation: Add implementation for SyGuS interpolation module (final) (#5063) X-Git-Tag: cvc5-1.0.0~2866 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=51be2e14c632d45e63a40659dea2177133251dfa;p=cvc5.git Interpolation: Add implementation for SyGuS interpolation module (final) (#5063) Add interface for SyGuS Interpolation module. 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. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 65ccabd89..9753f86a7 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -202,6 +202,8 @@ libcvc4_add_sources( smt/logic_exception.h smt/logic_request.cpp smt/logic_request.h + smt/interpolation_solver.cpp + smt/interpolation_solver.h smt/managed_ostreams.cpp smt/managed_ostreams.h smt/model.cpp diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp new file mode 100644 index 000000000..d2193d226 --- /dev/null +++ b/src/smt/interpolation_solver.cpp @@ -0,0 +1,142 @@ +/********************* */ +/*! \file interpolation_solver.cpp + ** \verbatim + ** Top contributors (to current version): + ** Ying Sheng + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The solver for interpolation queries + **/ + +#include "smt/interpolation_solver.h" + +#include "options/smt_options.h" +#include "smt/smt_engine.h" +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/sygus/sygus_grammar_cons.h" +#include "theory/quantifiers/sygus/sygus_interpol.h" +#include "theory/smt_engine_subsolver.h" + +using namespace CVC4::theory; + +namespace CVC4 { +namespace smt { + +InterpolationSolver::InterpolationSolver(SmtEngine* parent) : d_parent(parent) +{ +} + +InterpolationSolver::~InterpolationSolver() {} + +bool InterpolationSolver::getInterpol(const Node& conj, + const TypeNode& grammarType, + Node& interpol) +{ + if (options::produceInterpols() == options::ProduceInterpols::NONE) + { + const char* msg = + "Cannot get interpolation when produce-interpol options is off."; + throw ModalException(msg); + } + Trace("sygus-interpol") << "SmtEngine::getInterpol: conjecture " << conj + << std::endl; + std::vector easserts = d_parent->getExpandedAssertions(); + std::vector axioms; + for (unsigned i = 0, size = easserts.size(); i < size; i++) + { + axioms.push_back(Node::fromExpr(easserts[i])); + } + // must expand definitions + Node conjn = d_parent->expandDefinitions(conj); + std::string name("A"); + + quantifiers::SygusInterpol interpolSolver; + if (interpolSolver.SolveInterpolation( + name, axioms, conjn, grammarType, interpol)) + { + if (options::checkInterpols()) + { + checkInterpol(interpol.toExpr(), easserts, conj); + } + return true; + } + return false; +} + +bool InterpolationSolver::getInterpol(const Node& conj, Node& interpol) +{ + TypeNode grammarType; + return getInterpol(conj, grammarType, interpol); +} + +void InterpolationSolver::checkInterpol(Expr interpol, + const std::vector& easserts, + const Node& conj) +{ + Assert(interpol.getType().isBoolean()); + Trace("check-interpol") << "SmtEngine::checkInterpol: get expanded assertions" + << std::endl; + + // two checks: first, axioms imply interpol, second, interpol implies conj. + for (unsigned j = 0; j < 2; j++) + { + if (j == 1) + { + Trace("check-interpol") << "SmtEngine::checkInterpol: conjecture is " + << conj.toExpr() << std::endl; + } + Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j + << ": make new SMT engine" << std::endl; + // Start new SMT engine to check solution + std::unique_ptr itpChecker; + initializeSubsolver(itpChecker); + Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j + << ": asserting formulas" << std::endl; + if (j == 0) + { + for (const Expr& e : easserts) + { + itpChecker->assertFormula(e); + } + Expr negitp = interpol.notExpr(); + itpChecker->assertFormula(negitp); + } + else + { + itpChecker->assertFormula(interpol); + Assert(!conj.isNull()); + itpChecker->assertFormula(conj.toExpr().notExpr()); + } + Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j + << ": check the assertions" << std::endl; + Result r = itpChecker->checkSat(); + Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j + << ": result is " << r << std::endl; + std::stringstream serr; + if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) + { + if (j == 0) + { + serr << "SmtEngine::checkInterpol(): negated produced solution cannot " + "be shown " + "satisfiable with assertions, result was " + << r; + } + else + { + serr + << "SmtEngine::checkInterpol(): negated conjecture cannot be shown " + "satisfiable with produced solution, result was " + << r; + } + InternalError() << serr.str(); + } + } +} + +} // namespace smt +} // namespace CVC4 diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h new file mode 100644 index 000000000..8e6d2cd14 --- /dev/null +++ b/src/smt/interpolation_solver.h @@ -0,0 +1,86 @@ +/********************* */ +/*! \file interpolation_solver.h + ** \verbatim + ** Top contributors (to current version): + ** Ying Sheng + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The solver for interpolation queries + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__SMT__INTERPOLATION_SOLVER_H +#define CVC4__SMT__INTERPOLATION_SOLVER_H + +#include "expr/node.h" +#include "expr/type_node.h" + +namespace CVC4 { + +class SmtEngine; + +namespace smt { + +/** + * A solver for interpolation queries. + * + * This class is responsible for responding to get-interpol commands. It spawns + * a subsolver SmtEngine for a sygus conjecture that captures the interpolation + * query, and implements supporting utility methods such as checkInterpol. + */ +class InterpolationSolver +{ + public: + InterpolationSolver(SmtEngine* parent); + ~InterpolationSolver(); + + /** + * This method asks this SMT engine to find an interpolant with respect to + * the current assertion stack (call it A) and the conjecture (call it B). If + * this method returns true, then interpolant is set to a formula I such that + * A ^ ~I and I ^ ~B are both unsatisfiable. + * + * @param conj The conjecture of the interpolation problem. + * @param grammarType A sygus datatype type that encodes the syntax + * restrictions on the shape of possible solutions. + * @param interpol This argument is updated to contain the solution to the + * interpolation problem. + * + * This method invokes a separate copy of the SMT engine for solving the + * corresponding sygus problem for generating such a solution. + */ + bool getInterpol(const Node& conj, + const TypeNode& grammarType, + Node& interpol); + + /** + * Same as above, but without user-provided grammar restrictions. A default + * grammar is chosen internally using the sygus grammar constructor utility. + */ + bool getInterpol(const Node& conj, Node& interpol); + + /** + * Check that a solution to an interpolation problem is indeed a solution. + * + * The check is made by determining that the assertions imply the solution of + * the interpolation problem (interpol), and the solution implies the goal + * (conj). If these criteria are not met, an internal error is thrown. + */ + void checkInterpol(Expr interpol, + const std::vector& easserts, + const Node& conj); + + private: + /** The parent SMT engine */ + SmtEngine* d_parent; +}; + +} // namespace smt +} // namespace CVC4 + +#endif /* CVC4__SMT__INTERPOLATION_SOLVER_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7f824bff3..d271ca05d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -75,6 +75,7 @@ #include "smt/defined_function.h" #include "smt/dump_manager.h" #include "smt/expr_names.h" +#include "smt/interpolation_solver.h" #include "smt/listeners.h" #include "smt/logic_request.h" #include "smt/model_blocker.h" @@ -134,6 +135,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_definedFunctions(nullptr), d_sygusSolver(nullptr), d_abductSolver(nullptr), + d_interpolSolver(nullptr), d_quantElimSolver(nullptr), d_assignments(nullptr), d_logic(), @@ -299,6 +301,10 @@ void SmtEngine::finishInit() { d_abductSolver.reset(new AbductionSolver(this)); } + if (options::produceInterpols() != options::ProduceInterpols::NONE) + { + d_interpolSolver.reset(new InterpolationSolver(this)); + } d_pp->finishInit(); @@ -1755,12 +1761,6 @@ void SmtEngine::checkModel(bool hardFailure) { Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl; } -void SmtEngine::checkInterpol(Expr interpol, - const std::vector& easserts, - const Node& conj) -{ -} - // TODO(#1108): Simplify the error reporting of this method. UnsatCore SmtEngine::getUnsatCore() { Trace("smt") << "SMT getUnsatCore()" << endl; @@ -1818,7 +1818,11 @@ bool SmtEngine::getInterpol(const Node& conj, const TypeNode& grammarType, Node& interpol) { - return false; + bool success = d_interpolSolver->getInterpol(conj, grammarType, interpol); + // notify the state of whether the get-interpol call was successfuly, which + // impacts the SMT mode. + d_state->notifyGetInterpol(success); + return success; } bool SmtEngine::getInterpol(const Node& conj, Node& interpol) diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index e95e36c3d..eec17a5f8 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -105,6 +105,7 @@ class Preprocessor; class SmtSolver; class SygusSolver; class AbductionSolver; +class InterpolationSolver; class QuantElimSolver; /** * Representation of a defined function. We keep these around in @@ -1101,6 +1102,8 @@ class CVC4_PUBLIC SmtEngine /** The solver for abduction queries */ std::unique_ptr d_abductSolver; + /** The solver for interpolation queries */ + std::unique_ptr d_interpolSolver; /** The solver for quantifier elimination queries */ std::unique_ptr d_quantElimSolver; /** diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp index 07f1d3321..4f3782e2a 100644 --- a/src/smt/smt_engine_state.cpp +++ b/src/smt/smt_engine_state.cpp @@ -122,6 +122,20 @@ void SmtEngineState::notifyGetAbduct(bool success) } } +void SmtEngineState::notifyGetInterpol(bool success) +{ + if (success) + { + // successfully generated an interpolant, update to interpol state + d_smtMode = SmtMode::INTERPOL; + } + else + { + // failed, we revert to the assert state + d_smtMode = SmtMode::ASSERT; + } +} + void SmtEngineState::setup() { // push a context diff --git a/src/smt/smt_engine_state.h b/src/smt/smt_engine_state.h index efb86ca88..1a2ae7ee8 100644 --- a/src/smt/smt_engine_state.h +++ b/src/smt/smt_engine_state.h @@ -95,6 +95,18 @@ class SmtEngineState * was successful. */ void notifyGetAbduct(bool success); + /** + * Notify that we finished an interpolation query, where success is whether + * the command was successful. This is managed independently of the above + * calls for notifying check-sat. In other words, if a get-interpol command + * is issued to an SmtEngine, it may use a satisfiability call (if desired) + * to solve the interpolation query. This method is called *in addition* to + * the above calls to notifyCheckSat / notifyCheckSatResult in this case. + * In particular, it is called after these two methods are completed. + * This overwrites the SMT mode to the "INTERPOL" mode if the call to + * interpolation was successful. + */ + void notifyGetInterpol(bool success); /** * Setup the context, which makes a single push to maintain a global * context around everything. diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index c2ca83e41..4d18c850b 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -23,6 +23,7 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/rewriter.h" +#include "theory/smt_engine_subsolver.h" namespace CVC4 { namespace theory { @@ -30,8 +31,6 @@ namespace quantifiers { SygusInterpol::SygusInterpol() {} -SygusInterpol::SygusInterpol(LogicInfo logic) : d_logic(logic) {} - void SygusInterpol::collectSymbols(const std::vector& axioms, const Node& conj) { @@ -75,6 +74,9 @@ void SygusInterpol::createVariables(bool needsShared) Node var = nm->mkBoundVar(tn); d_vars.push_back(var); Node vlv = nm->mkBoundVar(ss.str(), tn); + // set that this variable encodes the term s + SygusVarToTermAttribute sta; + vlv.setAttribute(sta, s); d_vlvs.push_back(vlv); if (!needsShared || d_symSetShared.find(s) != d_symSetShared.end()) { @@ -266,7 +268,7 @@ void SygusInterpol::mkSygusConjecture(Node itp, Trace("sygus-interpol") << "Generate: " << d_sygusConj << std::endl; } -bool SygusInterpol::findInterpol(Expr& interpol, Node itp) +bool SygusInterpol::findInterpol(Node& interpol, Node itp) { // get the synthesis solution std::map sols; @@ -283,31 +285,31 @@ bool SygusInterpol::findInterpol(Expr& interpol, Node itp) } Trace("sygus-interpol") << "SmtEngine::getInterpol: solution is " << its->second << std::endl; - Node interpoln = its->second; + interpol = its->second; // replace back the created variables to original symbols. - Node interpoln_reduced; - if (interpoln.getKind() == kind::LAMBDA) + if (interpol.getKind() == kind::LAMBDA) { - interpoln_reduced = interpoln[1]; + interpol = interpol[1]; } - else + + // get the grammar type for the interpolant + Node igdtbv = itp.getAttribute(SygusSynthFunVarListAttribute()); + Assert(!igdtbv.isNull()); + Assert(igdtbv.getKind() == kind::BOUND_VAR_LIST); + // convert back to original + // must replace formal arguments of itp with the free variables in the + // input problem that they correspond to. + std::vector vars; + std::vector syms; + SygusVarToTermAttribute sta; + for (const Node& bv : igdtbv) { - interpoln_reduced = interpoln; + vars.push_back(bv); + syms.push_back(bv.hasAttribute(sta) ? bv.getAttribute(sta) : bv); } - if (interpoln.getNumChildren() != 0 && interpoln[0].getNumChildren() != 0) - { - std::vector formals; - for (const Node& n : interpoln[0]) - { - formals.push_back(n); - } - interpoln_reduced = interpoln_reduced.substitute(formals.begin(), - formals.end(), - d_symSetShared.begin(), - d_symSetShared.end()); - } - // convert to expression - interpol = interpoln_reduced.toExpr(); + interpol = + interpol.substitute(vars.begin(), vars.end(), syms.begin(), syms.end()); + return true; } @@ -315,14 +317,11 @@ bool SygusInterpol::SolveInterpolation(const std::string& name, const std::vector& axioms, const Node& conj, const TypeNode& itpGType, - Expr& interpol) + Node& interpol) { - NodeManager* nm = NodeManager::currentNM(); - // we generate a new smt engine to do the interpolation query - d_subSolver.reset(new SmtEngine(nm->toExprManager())); - d_subSolver->setIsInternalSubsolver(); + initializeSubsolver(d_subSolver); // get the logic - LogicInfo l = d_logic.getUnlockedCopy(); + LogicInfo l = d_subSolver->getLogicInfo().getUnlockedCopy(); // enable everything needed for sygus l.enableSygus(); d_subSolver->setLogic(l); diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h index 0fe66694f..4abe94f15 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.h +++ b/src/theory/quantifiers/sygus/sygus_interpol.h @@ -46,8 +46,6 @@ class SygusInterpol public: SygusInterpol(); - SygusInterpol(LogicInfo logic); - /** * Returns the sygus conjecture in interpol corresponding to the interpolation * problem for input problem (F above) given by axioms (Fa above), and conj @@ -65,7 +63,7 @@ class SygusInterpol const std::vector& axioms, const Node& conj, const TypeNode& itpGType, - Expr& interpol); + Node& interpol); private: /** @@ -158,7 +156,7 @@ class SygusInterpol * @param interpol the solution to the sygus conjecture. * @param itp the interpolation predicate. */ - bool findInterpol(Expr& interpol, Node itp); + bool findInterpol(Node& interpol, Node itp); /** The SMT engine subSolver * @@ -178,10 +176,6 @@ class SygusInterpol */ std::unique_ptr d_subSolver; - /** - * The logic for the local copy of SMT engine (d_subSolver). - */ - LogicInfo d_logic; /** * symbols from axioms and conjecture. */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index d784a1ced..ef0981372 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1943,6 +1943,14 @@ set(regress_1_tests regress1/sygus/inv-example.sy regress1/sygus/inv-missed-sol-true.sy regress1/sygus/inv-unused.sy + regress1/sygus/interpol1.smt2 + regress1/sygus/interpol2.smt2 + regress1/sygus/interpol3.smt2 + regress1/sygus/interpol_arr1.smt2 + regress1/sygus/interpol_arr2.smt2 + regress1/sygus/interpol_cosa_1.smt2 + regress1/sygus/interpol_from_pono_1.smt2 + regress1/sygus/interpol_from_pono_2.smt2 regress1/sygus/issue2914.sy regress1/sygus/issue2935.sy regress1/sygus/issue3199.smt2 diff --git a/test/regress/regress1/sygus/interpol1.smt2 b/test/regress/regress1/sygus/interpol1.smt2 new file mode 100644 index 000000000..58ef5420f --- /dev/null +++ b/test/regress/regress1/sygus/interpol1.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic NIA) +(declare-fun x ( ) Int) +(declare-fun y ( ) Int) +(declare-fun z ( ) Int) +(assert (= (* 2 x) y)) +(get-interpol A (distinct (+ (* 2 z) 1) y) + +; the grammar for the interpol-to-synthesize +((Start Bool) (StartInt Int)) +( +(Start Bool ((< StartInt StartInt))) +(StartInt Int +(y (+ StartInt StartInt) (div StartInt StartInt) (mod StartInt StartInt) 0 1 2)) +) + +) diff --git a/test/regress/regress1/sygus/interpol2.smt2 b/test/regress/regress1/sygus/interpol2.smt2 new file mode 100644 index 000000000..c6876ee15 --- /dev/null +++ b/test/regress/regress1/sygus/interpol2.smt2 @@ -0,0 +1,31 @@ +; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 + +(set-logic QF_UFLIA) + +; Let A1,...,An be formulas (called assumptions) +; Let C be a formula (called a conjecture) +; An interpolant of {A1,...,An} and G is any formula B such that: +; - A1,...,An |- B +; - B |- C +; - B has only variables that occur both in {A_1,...,A_n} and B. + +;The variables used are n,m,x,y, all integers. +(declare-fun n () Int) +(declare-fun m () Int) +(declare-fun x () Int) +(declare-fun y () Int) + +;The assumptions are: +; (*) 1 <= n <= x <= n+5 +; (*) 1 <= y <= m +(define-fun A1 () Bool (<= 1 n)) +(define-fun A2 () Bool (<= n x)) +(define-fun A3 () Bool (<= x (+ n 5))) +(define-fun A4 () Bool (<= 1 y)) +(define-fun A5 () Bool (<= y m)) +(assert (and A1 A2 A3 A4 A5)) + +;The conjuecture is: 2 <= x+y +(get-interpol A (<= 2 (+ x y))) diff --git a/test/regress/regress1/sygus/interpol3.smt2 b/test/regress/regress1/sygus/interpol3.smt2 new file mode 100644 index 000000000..8681acf3a --- /dev/null +++ b/test/regress/regress1/sygus/interpol3.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --produce-interpols=default --check-interpols +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic LIA) +(declare-fun a () Int) +(assert (> a 1)) +(get-interpol A (> a 0)) diff --git a/test/regress/regress1/sygus/interpol_arr1.smt2 b/test/regress/regress1/sygus/interpol_arr1.smt2 new file mode 100644 index 000000000..16190f877 --- /dev/null +++ b/test/regress/regress1/sygus/interpol_arr1.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic ALL) +(declare-fun a () (Array (_ BitVec 4) (_ BitVec 4))) +(declare-fun y () (_ BitVec 4)) +(assert (= (select a y) (_ bv0 4))) +(get-interpol A (distinct (select a y) (_ bv1 4))) diff --git a/test/regress/regress1/sygus/interpol_arr2.smt2 b/test/regress/regress1/sygus/interpol_arr2.smt2 new file mode 100644 index 000000000..18ce2b35f --- /dev/null +++ b/test/regress/regress1/sygus/interpol_arr2.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic ALL) +(declare-fun arr () (Array Int Int)) + +(define-fun A1 () Bool (<= 1 (select arr 0))) +(define-fun A2 () Bool (<= (select arr 0) (select arr 2))) +(define-fun A3 () Bool (<= (select arr 2) (+ (select arr 0) 5))) +(define-fun A4 () Bool (<= 1 (select arr 3))) +(define-fun A5 () Bool (<= (select arr 3) (select arr 1))) +(assert (and A1 A2 A3 A4 A5)) + +;The conjuecture is: 2 <= x+y +(get-interpol A (<= 2 (+ (select arr 2) (select arr 3)))) diff --git a/test/regress/regress1/sygus/interpol_cosa_1.smt2 b/test/regress/regress1/sygus/interpol_cosa_1.smt2 new file mode 100644 index 000000000..583f94ed4 --- /dev/null +++ b/test/regress/regress1/sygus/interpol_cosa_1.smt2 @@ -0,0 +1,30 @@ +; COMMAND-LINE: --produce-interpols=conjecture --sygus-active-gen=enum --check-interpols +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic ALL) +(set-option :produce-interpols conjecture) +(set-option :sygus-active-gen enum) +(declare-fun cfg@1 () (_ BitVec 1)) +(declare-fun witness_0@1 () Bool) +(declare-fun op@1 () (_ BitVec 4)) +(declare-fun counter@1 () (_ BitVec 16)) +(declare-fun input14@1 () (_ BitVec 1)) +(declare-fun clk@1 () (_ BitVec 1)) +(declare-fun a@1 () (_ BitVec 16)) +(declare-fun b@1 () (_ BitVec 16)) +(reset-assertions) +(declare-fun cfg@0 () (_ BitVec 1)) +(declare-fun witness_0@0 () Bool) +(declare-fun counter@0 () (_ BitVec 16)) +(declare-fun op@0 () (_ BitVec 4)) +(declare-fun input14@0 () (_ BitVec 1)) +(declare-fun b@0 () (_ BitVec 16)) +(declare-fun a@0 () (_ BitVec 16)) +(assert (and (and (and (and true (= counter@0 (_ bv0 16))) witness_0@0) (= cfg@0 (_ bv1 1))) (and (and (and (and true (= witness_0@1 (not (= (bvand (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@0 (_ bv0 4))) (bvadd a@0 b@0) (bvsub a@0 b@0)) (bvadd a@0 b@0)) input14@0))) (_ bv1 1))))) (= op@1 (ite (= cfg@0 (_ bv1 1)) (_ bv0 4) op@0))) (= counter@1 (bvadd counter@0 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@1 (_ bv0 1))))) +(assert (and (or (and (and (and true (= counter@0 (_ bv0 16))) witness_0@0) (= cfg@0 (_ bv1 1))) witness_0@0) (and (and (and (and true (= witness_0@1 (not (= (bvand (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@0 (_ bv0 4))) (bvadd a@0 b@0) (bvsub a@0 b@0)) (bvadd a@0 b@0)) input14@0))) (_ bv1 1))))) (= op@1 (ite (= cfg@0 (_ bv1 1)) (_ bv0 4) op@0))) (= counter@1 (bvadd counter@0 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@1 (_ bv0 1))))) +(declare-fun cfg@2 () (_ BitVec 1)) +(declare-fun counter@2 () (_ BitVec 16)) +(declare-fun op@2 () (_ BitVec 4)) +(declare-fun witness_0@2 () Bool) +(assert (and (and (and (and true (= counter@0 (_ bv0 16))) witness_0@0) (= cfg@0 (_ bv1 1))) (and (and (and (and true (= witness_0@1 (not (= (bvand (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@0 (_ bv0 4))) (bvadd a@0 b@0) (bvsub a@0 b@0)) (bvadd a@0 b@0)) input14@0))) (_ bv1 1))))) (= op@1 (ite (= cfg@0 (_ bv1 1)) (_ bv0 4) op@0))) (= counter@1 (bvadd counter@0 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@1 (_ bv0 1))))) +(get-interpol I (not (and (and true (and (and (and (and true (= witness_0@2 (not (= (bvand (ite (bvugt counter@1 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@1 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@1 (_ bv0 4))) (bvadd a@1 b@1) (bvsub a@1 b@1)) (bvadd a@1 b@1)) input14@1))) (_ bv1 1))))) (= op@2 (ite (= cfg@1 (_ bv1 1)) (_ bv0 4) op@1))) (= counter@2 (bvadd counter@1 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@2 (_ bv0 1)))) (not witness_0@2)))) diff --git a/test/regress/regress1/sygus/interpol_dt.smt2 b/test/regress/regress1/sygus/interpol_dt.smt2 new file mode 100644 index 000000000..f64ce4a0e --- /dev/null +++ b/test/regress/regress1/sygus/interpol_dt.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --produce-interpols=default +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic ALL) +(declare-datatypes ((List 0)) (((nil) (cons (head Int) (tail List))))) +(declare-fun x () List) +(declare-fun y () List) +(assert ((_ is cons) x)) +(assert ((_ is nil) (tail x))) +(assert (= (head x) 0)) +(assert (= x y)) +(get-interpol A (distinct y nil)) diff --git a/test/regress/regress1/sygus/interpol_from_pono_1.smt2 b/test/regress/regress1/sygus/interpol_from_pono_1.smt2 new file mode 100644 index 000000000..eff00e066 --- /dev/null +++ b/test/regress/regress1/sygus/interpol_from_pono_1.smt2 @@ -0,0 +1,39 @@ +; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic ALL) +(declare-fun a_S_a2@1 () (_ BitVec 1)) +(declare-fun a_R_a2@1 () (_ BitVec 1)) +(declare-fun a_Q_a2@1 () (_ BitVec 1)) +(declare-fun dve_invalid@1 () (_ BitVec 1)) +(declare-fun v_x1@1 () (_ BitVec 16)) +(declare-fun a_S_a1@1 () (_ BitVec 1)) +(declare-fun v_c@1 () (_ BitVec 16)) +(declare-fun v_x2@1 () (_ BitVec 16)) +(declare-fun a_Q_a1@1 () (_ BitVec 1)) +(declare-fun a_R_a1@1 () (_ BitVec 1)) +(declare-fun f3@1 () (_ BitVec 1)) +(declare-fun f0@1 () (_ BitVec 1)) +(declare-fun f5@1 () (_ BitVec 1)) +(declare-fun f1@1 () (_ BitVec 1)) +(declare-fun f2@1 () (_ BitVec 1)) +(declare-fun f4@1 () (_ BitVec 1)) +(declare-fun dve_invalid@0 () (_ BitVec 1)) +(declare-fun a_S_a2@0 () (_ BitVec 1)) +(declare-fun a_R_a2@0 () (_ BitVec 1)) +(declare-fun a_Q_a2@0 () (_ BitVec 1)) +(declare-fun a_S_a1@0 () (_ BitVec 1)) +(declare-fun a_R_a1@0 () (_ BitVec 1)) +(declare-fun a_Q_a1@0 () (_ BitVec 1)) +(declare-fun v_x2@0 () (_ BitVec 16)) +(declare-fun v_x1@0 () (_ BitVec 16)) +(declare-fun v_c@0 () (_ BitVec 16)) +(declare-fun f5@0 () (_ BitVec 1)) +(declare-fun f3@0 () (_ BitVec 1)) +(declare-fun f4@0 () (_ BitVec 1)) +(declare-fun f2@0 () (_ BitVec 1)) +(declare-fun f0@0 () (_ BitVec 1)) +(declare-fun f1@0 () (_ BitVec 1)) +(assert (and (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0))))))) + +(get-interpol I (not (and true (not (not (= (bvand (bvnot dve_invalid@1) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1))))))) diff --git a/test/regress/regress1/sygus/interpol_from_pono_2.smt2 b/test/regress/regress1/sygus/interpol_from_pono_2.smt2 new file mode 100644 index 000000000..894e8e781 --- /dev/null +++ b/test/regress/regress1/sygus/interpol_from_pono_2.smt2 @@ -0,0 +1,41 @@ +; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic ALL) +(declare-fun a_S_a2@1 () (_ BitVec 1)) +(declare-fun a_R_a2@1 () (_ BitVec 1)) +(declare-fun a_Q_a2@1 () (_ BitVec 1)) +(declare-fun dve_invalid@1 () (_ BitVec 1)) +(declare-fun v_x1@1 () (_ BitVec 16)) +(declare-fun a_S_a1@1 () (_ BitVec 1)) +(declare-fun v_c@1 () (_ BitVec 16)) +(declare-fun v_x2@1 () (_ BitVec 16)) +(declare-fun a_Q_a1@1 () (_ BitVec 1)) +(declare-fun a_R_a1@1 () (_ BitVec 1)) +(declare-fun f3@1 () (_ BitVec 1)) +(declare-fun f0@1 () (_ BitVec 1)) +(declare-fun f5@1 () (_ BitVec 1)) +(declare-fun f1@1 () (_ BitVec 1)) +(declare-fun f2@1 () (_ BitVec 1)) +(declare-fun f4@1 () (_ BitVec 1)) +(declare-fun dve_invalid@0 () (_ BitVec 1)) +(declare-fun a_S_a2@0 () (_ BitVec 1)) +(declare-fun a_R_a2@0 () (_ BitVec 1)) +(declare-fun a_Q_a2@0 () (_ BitVec 1)) +(declare-fun a_S_a1@0 () (_ BitVec 1)) +(declare-fun a_R_a1@0 () (_ BitVec 1)) +(declare-fun a_Q_a1@0 () (_ BitVec 1)) +(declare-fun v_x2@0 () (_ BitVec 16)) +(declare-fun v_x1@0 () (_ BitVec 16)) +(declare-fun v_c@0 () (_ BitVec 16)) +(declare-fun f5@0 () (_ BitVec 1)) +(declare-fun f3@0 () (_ BitVec 1)) +(declare-fun f4@0 () (_ BitVec 1)) +(declare-fun f2@0 () (_ BitVec 1)) +(declare-fun f0@0 () (_ BitVec 1)) +(declare-fun f1@0 () (_ BitVec 1)) +(assert (and (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0))))))) +(assert (and (or (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (bvult v_c@0 (_ bv2 16))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0))))))) + +(get-interpol I (not (and true (not (not (= (bvand (bvnot dve_invalid@1) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1))))))) + diff --git a/test/regress/regress1/sygus/interpol_from_pono_3.smt2 b/test/regress/regress1/sygus/interpol_from_pono_3.smt2 new file mode 100644 index 000000000..5de1d4ebd --- /dev/null +++ b/test/regress/regress1/sygus/interpol_from_pono_3.smt2 @@ -0,0 +1,54 @@ +; COMMAND-LINE: --produce-interpols=default +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic ALL) +(declare-fun a_S_a2@1 () (_ BitVec 1)) +(declare-fun a_R_a2@1 () (_ BitVec 1)) +(declare-fun a_Q_a2@1 () (_ BitVec 1)) +(declare-fun dve_invalid@1 () (_ BitVec 1)) +(declare-fun v_x1@1 () (_ BitVec 16)) +(declare-fun a_S_a1@1 () (_ BitVec 1)) +(declare-fun v_c@1 () (_ BitVec 16)) +(declare-fun v_x2@1 () (_ BitVec 16)) +(declare-fun a_Q_a1@1 () (_ BitVec 1)) +(declare-fun a_R_a1@1 () (_ BitVec 1)) +(declare-fun f3@1 () (_ BitVec 1)) +(declare-fun f0@1 () (_ BitVec 1)) +(declare-fun f5@1 () (_ BitVec 1)) +(declare-fun f1@1 () (_ BitVec 1)) +(declare-fun f2@1 () (_ BitVec 1)) +(declare-fun f4@1 () (_ BitVec 1)) +(declare-fun dve_invalid@0 () (_ BitVec 1)) +(declare-fun a_S_a2@0 () (_ BitVec 1)) +(declare-fun a_R_a2@0 () (_ BitVec 1)) +(declare-fun a_Q_a2@0 () (_ BitVec 1)) +(declare-fun a_S_a1@0 () (_ BitVec 1)) +(declare-fun a_R_a1@0 () (_ BitVec 1)) +(declare-fun a_Q_a1@0 () (_ BitVec 1)) +(declare-fun v_x2@0 () (_ BitVec 16)) +(declare-fun v_x1@0 () (_ BitVec 16)) +(declare-fun v_c@0 () (_ BitVec 16)) +(declare-fun f5@0 () (_ BitVec 1)) +(declare-fun f3@0 () (_ BitVec 1)) +(declare-fun f4@0 () (_ BitVec 1)) +(declare-fun f2@0 () (_ BitVec 1)) +(declare-fun f0@0 () (_ BitVec 1)) +(declare-fun f1@0 () (_ BitVec 1)) +(assert (and (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0))))))) +(assert (and (or (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (bvult v_c@0 (_ bv2 16))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0))))))) + +(declare-fun dve_invalid@2 () (_ BitVec 1)) +(declare-fun a_S_a2@2 () (_ BitVec 1)) +(declare-fun a_R_a2@2 () (_ BitVec 1)) +(declare-fun a_Q_a2@2 () (_ BitVec 1)) +(declare-fun a_S_a1@2 () (_ BitVec 1)) +(declare-fun a_R_a1@2 () (_ BitVec 1)) +(declare-fun a_Q_a1@2 () (_ BitVec 1)) +(declare-fun v_x2@2 () (_ BitVec 16)) +(declare-fun v_x1@2 () (_ BitVec 16)) +(declare-fun v_c@2 () (_ BitVec 16)) +(assert (and (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0))))))) + +(get-interpol I (not (and (and true (and (and (and (and (and (and (and (and (and (and true (= v_c@2 (bvxor (_ bv1 16) (ite (= f5@1 (_ bv1 1)) v_x2@1 (ite (= f2@1 (_ bv1 1)) v_x1@1 (bvxor (_ bv1 16) v_c@1)))))) (= v_x1@2 (ite (= f1@1 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@1 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@1 (_ bv1 1)) (bvxor (_ bv1 16) v_c@1) v_x1@1)))) (= v_x2@2 (ite (= f4@1 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@1 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@1 (_ bv1 1)) (bvxor (_ bv1 16) v_c@1) v_x2@1)))) (= a_Q_a1@2 (bvnot (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)))) (= a_R_a1@2 (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)))) (= a_S_a1@2 (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)))) (= a_Q_a2@2 (bvnot (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)))) (= a_R_a2@2 (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)))) (= a_S_a2@2 (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)))) (= dve_invalid@2 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@1) (bvand (bvnot a_Q_a1@1) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@1 (bvnot f1@1))) (bvor a_S_a1@1 (bvnot f2@1))) (bvor (bvnot f3@1) (bvand (bvnot a_Q_a2@1) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@1 (bvnot f4@1))) (bvor a_S_a2@1 (bvnot f5@1))) (bvor f5@1 (bvor f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@1 f1@1) (bvand f2@1 (bvor f0@1 f1@1))) (bvand f3@1 (bvor f2@1 (bvor f0@1 f1@1)))) (bvand f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1))))) (bvand f5@1 (bvor f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@1) a_R_a1@1) (bvand a_S_a1@1 (bvor (bvnot a_Q_a1@1) a_R_a1@1)))) (bvor a_S_a1@1 (bvor (bvnot a_Q_a1@1) a_R_a1@1))) (bvnot (bvor (bvand (bvnot a_Q_a2@1) a_R_a2@1) (bvand a_S_a2@1 (bvor (bvnot a_Q_a2@1) a_R_a2@1))))) (bvor a_S_a2@1 (bvor (bvnot a_Q_a2@1) a_R_a2@1)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)) (bvand (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)) (bvor (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1))))) (bvor (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)) (bvor (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)) (bvand (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)) (bvor (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)))))) (bvor (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)) (bvor (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1))))) (bvnot dve_invalid@1)))))) (not (not (= (bvand (bvnot dve_invalid@2) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@2) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1))))))) + +