From: Haniel Barbosa Date: Thu, 16 Aug 2018 21:15:07 +0000 (-0500) Subject: Refactor extended rewriter preprocessing pass (#2324) X-Git-Tag: cvc5-1.0.0~4776 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0e77d62ac116c00bcb0bccdb1f48f87067529d56;p=cvc5.git Refactor extended rewriter preprocessing pass (#2324) --- diff --git a/src/Makefile.am b/src/Makefile.am index c7dc311b6..992f229d6 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -73,6 +73,8 @@ libcvc4_la_SOURCES = \ preprocessing/passes/bv_gauss.h \ preprocessing/passes/bv_intro_pow2.cpp \ preprocessing/passes/bv_intro_pow2.h \ + preprocessing/passes/extended_rewriter_pass.cpp \ + preprocessing/passes/extended_rewriter_pass.h \ preprocessing/passes/int_to_bv.cpp \ preprocessing/passes/int_to_bv.h \ preprocessing/passes/pseudo_boolean_processor.cpp \ diff --git a/src/preprocessing/passes/extended_rewriter_pass.cpp b/src/preprocessing/passes/extended_rewriter_pass.cpp new file mode 100644 index 000000000..572aaed7a --- /dev/null +++ b/src/preprocessing/passes/extended_rewriter_pass.cpp @@ -0,0 +1,42 @@ +/********************* */ +/*! \file extended_rewriter_pass.cpp + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 ExtRewPre preprocessing pass + ** + ** Applies the extended rewriter to assertions + **/ + +#include "preprocessing/passes/extended_rewriter_pass.h" + +#include "theory/quantifiers/extended_rewrite.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +ExtRewPre::ExtRewPre(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "ext-rew-pre"){}; + +PreprocessingPassResult ExtRewPre::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + theory::quantifiers::ExtendedRewriter extr(options::extRewPrepAgg()); + for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i) + { + assertionsToPreprocess->replace( + i, extr.extendedRewrite((*assertionsToPreprocess)[i])); + } + return PreprocessingPassResult::NO_CONFLICT; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/extended_rewriter_pass.h b/src/preprocessing/passes/extended_rewriter_pass.h new file mode 100644 index 000000000..f604a1af5 --- /dev/null +++ b/src/preprocessing/passes/extended_rewriter_pass.h @@ -0,0 +1,43 @@ +/********************* */ +/*! \file extended_rewriter_pass.h + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 ExtRewPre preprocessing pass + ** + ** Applies the extended rewriter to assertions + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H +#define __CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +class ExtRewPre : public PreprocessingPass +{ + public: + ExtRewPre(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* __CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 41b113b94..b5d758bca 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -77,6 +77,7 @@ #include "preprocessing/passes/bv_gauss.h" #include "preprocessing/passes/bv_intro_pow2.h" #include "preprocessing/passes/bv_to_bool.h" +#include "preprocessing/passes/extended_rewriter_pass.h" #include "preprocessing/passes/int_to_bv.h" #include "preprocessing/passes/pseudo_boolean_processor.h" #include "preprocessing/passes/real_to_int.h" @@ -2672,6 +2673,8 @@ void SmtEnginePrivate::finishInit() new BvIntroPow2(d_preprocessingPassContext.get())); std::unique_ptr bvToBool( new BVToBool(d_preprocessingPassContext.get())); + std::unique_ptr extRewPre( + new ExtRewPre(d_preprocessingPassContext.get())); std::unique_ptr intToBV( new IntToBV(d_preprocessingPassContext.get())); std::unique_ptr pbProc( @@ -2704,6 +2707,7 @@ void SmtEnginePrivate::finishInit() d_preprocessingPassRegistry.registerPass("bv-intro-pow2", std::move(bvIntroPow2)); d_preprocessingPassRegistry.registerPass("bv-to-bool", std::move(bvToBool)); + d_preprocessingPassRegistry.registerPass("ext-rew-pre", std::move(extRewPre)); d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV)); d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor", std::move(pbProc)); @@ -4156,19 +4160,14 @@ void SmtEnginePrivate::processAssertions() { if (options::extRewPrep()) { - theory::quantifiers::ExtendedRewriter extr(options::extRewPrepAgg()); - for (unsigned i = 0; i < d_assertions.size(); ++i) - { - Node a = d_assertions[i]; - d_assertions.replace(i, extr.extendedRewrite(a)); - } + d_preprocessingPassRegistry.getPass("ext-rew-pre")->apply(&d_assertions); } // Unconstrained simplification if(options::unconstrainedSimp()) { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << endl; dumpAssertions("pre-unconstrained-simp", d_assertions); - d_preprocessingPassRegistry.getPass("rewrite")->apply(&d_assertions); + d_preprocessingPassRegistry.getPass("rewrite")->apply(&d_assertions); unconstrainedSimp(); Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-unconstrained-simp" << endl; dumpAssertions("post-unconstrained-simp", d_assertions); diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 496551462..82f8f2c27 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -438,6 +438,7 @@ REG0_TESTS = \ regress0/fmf/syn002-si-real-int.smt2 \ regress0/fmf/tail_rec.smt2 \ regress0/fp/simple.smt2 \ + regress0/fp/ext-rew-test.smt2 \ regress0/fuzz_1.smt \ regress0/fuzz_3.smt \ regress0/get-value-incremental.smt2 \ @@ -496,6 +497,7 @@ REG0_TESTS = \ regress0/logops.04.cvc \ regress0/logops.05.cvc \ regress0/nl/coeff-sat.smt2 \ + regress0/nl/ext-rew-aggr-test.smt2 \ regress0/nl/magnitude-wrong-1020-m.smt2 \ regress0/nl/mult-po.smt2 \ regress0/nl/nia-wrong-tl.smt2 \ diff --git a/test/regress/regress0/fp/ext-rew-test.smt2 b/test/regress/regress0/fp/ext-rew-test.smt2 new file mode 100644 index 000000000..785c654ef --- /dev/null +++ b/test/regress/regress0/fp/ext-rew-test.smt2 @@ -0,0 +1,86 @@ +; COMMAND-LINE: --ext-rew-prep +; EXPECT: unsat +(set-info :smt-lib-version 2.6) +(set-logic QF_FP) +(set-info :category "crafted") +(set-info :source |Alberto Griggio . These benchmarks were used for the evaluation in the following paper: L. Haller, A. Griggio, M. Brain, D. Kroening: Deciding floating-point logic with systematic abstraction. FMCAD 2012. Real-numbered literals have been automatically translated by MathSAT|) +(set-info :status unknown) +;; MathSAT API call trace +;; generated on 05/20/15 17:24:51 + +(declare-fun b13 () (_ FloatingPoint 11 53)) +(declare-fun b25 () (_ FloatingPoint 11 53)) +(declare-fun b22 () (_ FloatingPoint 11 53)) +(declare-fun b82 () (_ FloatingPoint 11 53)) +(declare-fun b14 () (_ FloatingPoint 11 53)) +(declare-fun b34 () (_ FloatingPoint 11 53)) +(declare-fun b43 () (_ FloatingPoint 11 53)) +(declare-fun b85 () (_ FloatingPoint 11 53)) +(declare-fun b16 () (_ FloatingPoint 11 53)) +(declare-fun b131 () (_ FloatingPoint 11 53)) +(declare-fun b126 () (_ FloatingPoint 11 53)) +(define-fun _t_3 () RoundingMode RNE) +(define-fun _t_9 () (_ FloatingPoint 11 53) b131) +(define-fun _t_10 () (_ FloatingPoint 11 53) b43) +(define-fun _t_11 () Bool (= _t_9 _t_10)) +(define-fun _t_12 () Bool (not _t_11)) +(define-fun _t_13 () (_ FloatingPoint 11 53) b126) +(define-fun _t_14 () (_ FloatingPoint 11 53) b34) +(define-fun _t_15 () Bool (= _t_13 _t_14)) +(define-fun _t_16 () Bool (not _t_15)) +(define-fun _t_17 () (_ FloatingPoint 11 53) b13) +(define-fun _t_18 () (_ FloatingPoint 11 53) b25) +(define-fun _t_19 () (_ FloatingPoint 11 53) (fp.mul _t_3 _t_17 _t_18)) +(define-fun _t_20 () (_ FloatingPoint 11 53) b16) +(define-fun _t_21 () (_ FloatingPoint 11 53) b22) +(define-fun _t_22 () (_ FloatingPoint 11 53) (fp.add _t_3 _t_20 _t_21)) +(define-fun _t_23 () Bool (fp.lt _t_22 _t_19)) +(define-fun _t_24 () Bool (not _t_23)) +(define-fun _t_25 () (_ FloatingPoint 11 53) b14) +(define-fun _t_26 () (_ FloatingPoint 11 53) (fp.neg _t_25)) +(define-fun _t_27 () (_ FloatingPoint 11 53) (fp.add _t_3 _t_17 _t_26)) +(define-fun _t_28 () Bool (fp.lt _t_27 _t_21)) +(define-fun _t_29 () Bool (not _t_28)) +(define-fun _t_30 () (_ FloatingPoint 11 53) (fp.mul _t_3 _t_17 _t_25)) +(define-fun _t_31 () Bool (fp.lt _t_30 _t_20)) +(define-fun _t_32 () Bool (not _t_31)) +(define-fun _t_33 () (_ FloatingPoint 11 53) (fp.add _t_3 _t_17 _t_25)) +(define-fun _t_34 () Bool (fp.lt _t_33 _t_20)) +(define-fun _t_35 () Bool (not _t_34)) +(define-fun _t_36 () Bool (= _t_13 _t_20)) +(define-fun _t_37 () Bool (and _t_35 _t_36)) +(define-fun _t_38 () Bool (= _t_9 _t_21)) +(define-fun _t_39 () Bool (and _t_37 _t_38)) +(define-fun _t_40 () (_ FloatingPoint 11 53) b85) +(define-fun _t_41 () Bool (fp.leq _t_40 _t_25)) +(define-fun _t_42 () Bool (and _t_39 _t_41)) +(define-fun _t_43 () (_ FloatingPoint 11 53) b82) +(define-fun _t_44 () Bool (fp.leq _t_25 _t_43)) +(define-fun _t_45 () Bool (and _t_42 _t_44)) +(define-fun _t_46 () Bool (fp.leq _t_40 _t_17)) +(define-fun _t_47 () Bool (and _t_45 _t_46)) +(define-fun _t_48 () Bool (fp.leq _t_17 _t_43)) +(define-fun _t_49 () Bool (and _t_47 _t_48)) +(define-fun _t_50 () Bool (fp.leq _t_40 _t_20)) +(define-fun _t_51 () Bool (and _t_49 _t_50)) +(define-fun _t_52 () Bool (fp.leq _t_20 _t_43)) +(define-fun _t_53 () Bool (and _t_51 _t_52)) +(define-fun _t_54 () Bool (fp.leq _t_40 _t_21)) +(define-fun _t_55 () Bool (and _t_53 _t_54)) +(define-fun _t_56 () Bool (fp.leq _t_21 _t_43)) +(define-fun _t_57 () Bool (and _t_55 _t_56)) +(define-fun _t_58 () (_ FloatingPoint 11 53) (fp.add _t_3 _t_9 _t_13)) +(define-fun _t_59 () Bool (fp.lt _t_58 _t_19)) +(define-fun _t_60 () Bool (and _t_57 _t_59)) +(define-fun _t_61 () Bool (fp.lt _t_27 _t_9)) +(define-fun _t_62 () Bool (and _t_60 _t_61)) +(define-fun _t_63 () Bool (fp.lt _t_33 _t_13)) +(define-fun _t_64 () Bool (and _t_62 _t_63)) +(define-fun _t_65 () Bool (and _t_32 _t_64)) +(define-fun _t_66 () Bool (and _t_29 _t_65)) +(define-fun _t_67 () Bool (and _t_24 _t_66)) +(define-fun _t_68 () Bool (and _t_16 _t_67)) +(define-fun _t_69 () Bool (and _t_12 _t_68)) +(assert _t_69) +(check-sat) +(exit) diff --git a/test/regress/regress0/nl/ext-rew-aggr-test.smt2 b/test/regress/regress0/nl/ext-rew-aggr-test.smt2 new file mode 100644 index 000000000..d7a082304 --- /dev/null +++ b/test/regress/regress0/nl/ext-rew-aggr-test.smt2 @@ -0,0 +1,105 @@ +; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg +; EXPECT: sat +(set-info :smt-lib-version 2.6) +(set-logic QF_NIA) +(set-info :source | +Generated by: Cristina Borralleras, Daniel Larraz, Albert Oliveras, Enric Rodriguez-Carbonell, Albert Rubio +Generated on: 2017-04-27 +Generator: VeryMax +Application: Termination proving +Target solver: barcelogic +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(set-info :status sat) +(declare-fun global_invc1_0 () Int) +(declare-fun lam0n0 () Int) +(declare-fun lam0n2 () Int) +(declare-fun global_invc1_1 () Int) +(declare-fun lam0n1 () Int) +(declare-fun lam1n0 () Int) +(declare-fun lam1n1 () Int) +(declare-fun lam1n3 () Int) +(declare-fun lam1n4 () Int) +(declare-fun lam1n2 () Int) +(declare-fun term_invc1_0 () Int) +(declare-fun lam2n0 () Int) +(declare-fun lam2n1 () Int) +(declare-fun lam2n3 () Int) +(declare-fun lam2n4 () Int) +(declare-fun lam2n5 () Int) +(declare-fun lam2n6 () Int) +(declare-fun lam2n7 () Int) +(declare-fun lam2n8 () Int) +(declare-fun lam2n9 () Int) +(declare-fun lam2n10 () Int) +(declare-fun lam2n11 () Int) +(declare-fun lam2n12 () Int) +(declare-fun lam2n13 () Int) +(declare-fun lam2n2 () Int) +(declare-fun term_invc1_1 () Int) +(declare-fun non_inc1_L () Bool) +(declare-fun lam3n0 () Int) +(declare-fun lam3n1 () Int) +(declare-fun lam3n3 () Int) +(declare-fun lam3n4 () Int) +(declare-fun lam3n5 () Int) +(declare-fun lam3n6 () Int) +(declare-fun lam3n7 () Int) +(declare-fun lam3n8 () Int) +(declare-fun lam3n9 () Int) +(declare-fun lam3n10 () Int) +(declare-fun lam3n11 () Int) +(declare-fun lam3n12 () Int) +(declare-fun lam3n13 () Int) +(declare-fun lam3n15 () Int) +(declare-fun lam3n14 () Int) +(declare-fun lam3n2 () Int) +(declare-fun rfc0 () Int) +(declare-fun disabled1_L () Bool) +(declare-fun bounded1_L () Bool) +(declare-fun lam4n0 () Int) +(declare-fun lam4n1 () Int) +(declare-fun lam4n3 () Int) +(declare-fun lam4n4 () Int) +(declare-fun lam4n5 () Int) +(declare-fun lam4n6 () Int) +(declare-fun lam4n7 () Int) +(declare-fun lam4n8 () Int) +(declare-fun lam4n9 () Int) +(declare-fun lam4n10 () Int) +(declare-fun lam4n11 () Int) +(declare-fun lam4n12 () Int) +(declare-fun lam4n13 () Int) +(declare-fun lam4n14 () Int) +(declare-fun lam4n2 () Int) +(declare-fun rfc1 () Int) +(declare-fun dec1_L () Bool) +(declare-fun lam5n0 () Int) +(declare-fun lam5n1 () Int) +(declare-fun lam5n3 () Int) +(declare-fun lam5n4 () Int) +(declare-fun lam5n5 () Int) +(declare-fun lam5n6 () Int) +(declare-fun lam5n7 () Int) +(declare-fun lam5n8 () Int) +(declare-fun lam5n9 () Int) +(declare-fun lam5n10 () Int) +(declare-fun lam5n11 () Int) +(declare-fun lam5n12 () Int) +(declare-fun lam5n13 () Int) +(declare-fun lam5n14 () Int) +(declare-fun lam5n2 () Int) +(declare-fun bnd_and_dec1_L () Bool) +(declare-fun GLOBAL_NT_1 () Bool) +(declare-fun global_V0_1 () Int) +(declare-fun TERM_NT_1 () Bool) +(declare-fun term_V0_1 () Int) +(declare-fun ALL_NON_INC_0 () Bool) +(declare-fun DIS_OR_ALL_NON_INC_0 () Bool) +(declare-fun SOME_BND_AND_DEC_0 () Bool) +(declare-fun V0_NIV () Int) +(declare-fun V1_NIV () Int) +(assert ( and ( >= global_invc1_0 ( - 1 ) ) ( <= global_invc1_0 1 ) ( and ( >= lam0n0 0 ) ( <= 0 lam0n2 ) ( < lam0n2 1 ) ( and ( = ( * ( - 1 ) lam0n0 ) ( + global_invc1_1 ( * ( - 1 ) lam0n2 ) ) ) ( = ( * lam0n1 1 ) 0 ) ( = ( * lam0n1 ( - 1 ) ) global_invc1_0 ) ) ) ( and ( >= lam1n0 0 ) ( >= lam1n1 0 ) ( >= lam1n3 0 ) ( <= 0 lam1n4 ) ( < lam1n4 1 ) ( and ( = ( + ( * ( - 1 ) lam1n0 ) ( * lam1n1 ( - 999 ) ) ( * lam1n2 1000 ) ( * lam1n3 global_invc1_1 ) ) ( + global_invc1_1 ( * ( - 1 ) lam1n4 ) ) ) ( = ( + ( * lam1n1 ( - 1 ) ) ( * lam1n2 1 ) ( * lam1n3 global_invc1_0 ) ) 0 ) ( = ( * lam1n2 ( - 1 ) ) global_invc1_0 ) ) ) ( >= term_invc1_0 ( - 1 ) ) ( <= term_invc1_0 1 ) ( and ( >= lam2n0 0 ) ( >= lam2n1 0 ) ( >= lam2n3 0 ) ( >= lam2n4 0 ) ( >= lam2n5 0 ) ( >= lam2n6 0 ) ( >= lam2n7 0 ) ( >= lam2n8 0 ) ( >= lam2n9 0 ) ( >= lam2n10 0 ) ( >= lam2n11 0 ) ( >= lam2n12 0 ) ( <= 0 lam2n13 ) ( < lam2n13 1 ) ( and ( = ( + ( * ( - 1 ) lam2n0 ) ( * lam2n1 ( - 999 ) ) ( * lam2n2 1000 ) ( * lam2n3 50001 ) ( * lam2n4 ( - 1 ) ) ( * lam2n5 1 ) ( * lam2n6 2 ) ( * lam2n7 3 ) ( * lam2n8 55 ) ( * lam2n9 58 ) ( * lam2n10 61 ) ( * lam2n11 62 ) ( * lam2n12 global_invc1_1 ) ) ( + term_invc1_1 ( * ( - 1 ) lam2n13 ) ) ) ( = ( + ( * lam2n1 ( - 1 ) ) ( * lam2n2 1 ) ( * lam2n3 ( - 1 ) ) ( * lam2n4 ( - 1 ) ) ( * lam2n5 ( - 1 ) ) ( * lam2n6 ( - 1 ) ) ( * lam2n7 ( - 1 ) ) ( * lam2n8 ( - 1 ) ) ( * lam2n9 ( - 1 ) ) ( * lam2n10 ( - 1 ) ) ( * lam2n11 ( - 1 ) ) ( * lam2n12 global_invc1_0 ) ) 0 ) ( = ( * lam2n2 ( - 1 ) ) term_invc1_0 ) ) ) ( = non_inc1_L ( and ( >= lam3n0 0 ) ( >= lam3n1 0 ) ( >= lam3n3 0 ) ( >= lam3n4 0 ) ( >= lam3n5 0 ) ( >= lam3n6 0 ) ( >= lam3n7 0 ) ( >= lam3n8 0 ) ( >= lam3n9 0 ) ( >= lam3n10 0 ) ( >= lam3n11 0 ) ( >= lam3n12 0 ) ( >= lam3n13 0 ) ( <= 0 lam3n15 ) ( < lam3n15 1 ) ( <= lam3n14 1 ) ( >= lam3n14 0 ) ( and ( > ( + ( * ( - 1 ) lam3n0 ) ( * lam3n1 ( - 999 ) ) ( * lam3n2 1000 ) ( * lam3n3 50001 ) ( * lam3n4 ( - 1 ) ) ( * lam3n5 1 ) ( * lam3n6 2 ) ( * lam3n7 3 ) ( * lam3n8 55 ) ( * lam3n9 58 ) ( * lam3n10 61 ) ( * lam3n11 62 ) ( * lam3n12 global_invc1_1 ) ( * lam3n13 term_invc1_1 ) ( * lam3n14 ( + 1 ( * ( - 1 ) lam3n15 ) ) ) ) 0 ) ( = ( + ( * lam3n1 ( - 1 ) ) ( * lam3n2 1 ) ( * lam3n3 ( - 1 ) ) ( * lam3n4 ( - 1 ) ) ( * lam3n5 ( - 1 ) ) ( * lam3n6 ( - 1 ) ) ( * lam3n7 ( - 1 ) ) ( * lam3n8 ( - 1 ) ) ( * lam3n9 ( - 1 ) ) ( * lam3n10 ( - 1 ) ) ( * lam3n11 ( - 1 ) ) ( * lam3n12 global_invc1_0 ) ( * lam3n13 term_invc1_0 ) ( * lam3n14 rfc0 ) ) 0 ) ( = ( + ( * lam3n2 ( - 1 ) ) ( * lam3n14 ( * ( - 1 ) rfc0 ) ) ) 0 ) ) ) ) ( = disabled1_L ( and ( = lam3n14 0 ) non_inc1_L ) ) ( = bounded1_L ( and ( >= lam4n0 0 ) ( >= lam4n1 0 ) ( >= lam4n3 0 ) ( >= lam4n4 0 ) ( >= lam4n5 0 ) ( >= lam4n6 0 ) ( >= lam4n7 0 ) ( >= lam4n8 0 ) ( >= lam4n9 0 ) ( >= lam4n10 0 ) ( >= lam4n11 0 ) ( >= lam4n12 0 ) ( >= lam4n13 0 ) ( <= 0 lam4n14 ) ( < lam4n14 1 ) ( and ( = ( + ( * ( - 1 ) lam4n0 ) ( * lam4n1 ( - 999 ) ) ( * lam4n2 1000 ) ( * lam4n3 50001 ) ( * lam4n4 ( - 1 ) ) ( * lam4n5 1 ) ( * lam4n6 2 ) ( * lam4n7 3 ) ( * lam4n8 55 ) ( * lam4n9 58 ) ( * lam4n10 61 ) ( * lam4n11 62 ) ( * lam4n12 global_invc1_1 ) ( * lam4n13 term_invc1_1 ) ) ( + ( * ( - 1 ) rfc1 ) ( * ( - 1 ) lam4n14 ) ) ) ( = ( + ( * lam4n1 ( - 1 ) ) ( * lam4n2 1 ) ( * lam4n3 ( - 1 ) ) ( * lam4n4 ( - 1 ) ) ( * lam4n5 ( - 1 ) ) ( * lam4n6 ( - 1 ) ) ( * lam4n7 ( - 1 ) ) ( * lam4n8 ( - 1 ) ) ( * lam4n9 ( - 1 ) ) ( * lam4n10 ( - 1 ) ) ( * lam4n11 ( - 1 ) ) ( * lam4n12 global_invc1_0 ) ( * lam4n13 term_invc1_0 ) ) ( * ( - 1 ) rfc0 ) ) ( = ( * lam4n2 ( - 1 ) ) 0 ) ) ) ) ( = dec1_L ( and ( >= lam5n0 0 ) ( >= lam5n1 0 ) ( >= lam5n3 0 ) ( >= lam5n4 0 ) ( >= lam5n5 0 ) ( >= lam5n6 0 ) ( >= lam5n7 0 ) ( >= lam5n8 0 ) ( >= lam5n9 0 ) ( >= lam5n10 0 ) ( >= lam5n11 0 ) ( >= lam5n12 0 ) ( >= lam5n13 0 ) ( <= 0 lam5n14 ) ( < lam5n14 1 ) ( and ( = ( + ( * ( - 1 ) lam5n0 ) ( * lam5n1 ( - 999 ) ) ( * lam5n2 1000 ) ( * lam5n3 50001 ) ( * lam5n4 ( - 1 ) ) ( * lam5n5 1 ) ( * lam5n6 2 ) ( * lam5n7 3 ) ( * lam5n8 55 ) ( * lam5n9 58 ) ( * lam5n10 61 ) ( * lam5n11 62 ) ( * lam5n12 global_invc1_1 ) ( * lam5n13 term_invc1_1 ) ) ( + 1 ( * ( - 1 ) lam5n14 ) ) ) ( = ( + ( * lam5n1 ( - 1 ) ) ( * lam5n2 1 ) ( * lam5n3 ( - 1 ) ) ( * lam5n4 ( - 1 ) ) ( * lam5n5 ( - 1 ) ) ( * lam5n6 ( - 1 ) ) ( * lam5n7 ( - 1 ) ) ( * lam5n8 ( - 1 ) ) ( * lam5n9 ( - 1 ) ) ( * lam5n10 ( - 1 ) ) ( * lam5n11 ( - 1 ) ) ( * lam5n12 global_invc1_0 ) ( * lam5n13 term_invc1_0 ) ) ( * ( - 1 ) rfc0 ) ) ( = ( * lam5n2 ( - 1 ) ) rfc0 ) ) ) ) ( = bnd_and_dec1_L ( and bounded1_L dec1_L ) ) ( = GLOBAL_NT_1 ( not ( = global_invc1_0 0 ) ) ) ( or ( not ( <= ( + global_invc1_1 ( * global_invc1_0 global_V0_1 ) ) 0 ) ) ( = global_invc1_0 0 ) ) ( = TERM_NT_1 ( not ( = term_invc1_0 0 ) ) ) ( or ( and ( not ( <= ( + term_invc1_1 ( * term_invc1_0 term_V0_1 ) ) 0 ) ) ( <= ( + ( * ( - 1 ) term_V0_1 ) ( - 1 ) ) 0 ) ( <= ( + ( * ( - 1 ) term_V0_1 ) 1 ) 0 ) ( <= ( + ( * ( - 1 ) term_V0_1 ) 2 ) 0 ) ( <= ( + ( * ( - 1 ) term_V0_1 ) 3 ) 0 ) ( <= ( + ( * ( - 1 ) term_V0_1 ) 55 ) 0 ) ( <= ( + ( * ( - 1 ) term_V0_1 ) 58 ) 0 ) ( <= ( + ( * ( - 1 ) term_V0_1 ) 61 ) 0 ) ( <= ( + ( * ( - 1 ) term_V0_1 ) 62 ) 0 ) ) ( = term_invc1_0 0 ) ) ( = ALL_NON_INC_0 non_inc1_L ) ( = DIS_OR_ALL_NON_INC_0 ( or disabled1_L ALL_NON_INC_0 ) ) ( = SOME_BND_AND_DEC_0 bnd_and_dec1_L ) ( or ( not ALL_NON_INC_0 ) ( and ( >= rfc0 ( - 2 ) ) ( <= rfc0 2 ) ( not ( = rfc0 0 ) ) ( >= rfc1 0 ) ( or SOME_BND_AND_DEC_0 ( or ( and ( <= ( + ( * rfc0 V0_NIV ) 1 ) ( * rfc0 V1_NIV ) ) ( >= ( * ( - 1 ) V0_NIV ) ( * ( - 1 ) V1_NIV ) ) ) ( = rfc0 0 ) ) ) ) ) ( or GLOBAL_NT_1 TERM_NT_1 ALL_NON_INC_0 ) )) +(check-sat) +(exit)