From ec8ea8a9c993435c4c5e671b1beea45ac088de64 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 12 Mar 2019 14:43:42 -0500 Subject: Move tuple/record update elimination from ppRewrite to expandDefinition (#2839) --- test/regress/CMakeLists.txt | 1 + 1 file changed, 1 insertion(+) (limited to 'test/regress/CMakeLists.txt') diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 6f147db3c..abec884c2 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -363,6 +363,7 @@ set(regress_0_tests regress0/datatypes/example-dailler-min.smt2 regress0/datatypes/is_test.smt2 regress0/datatypes/issue1433.smt2 + regress0/datatypes/issue2838.cvc regress0/datatypes/jsat-2.6.smt2 regress0/datatypes/model-subterms-min.smt2 regress0/datatypes/mutually-recursive.cvc -- cgit v1.2.3 From 92d541960c7c1d4b06dbef8bebbb106d52fcaeb4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 14 Mar 2019 14:06:48 -0500 Subject: Implement proper semantics for TPTP predicate is_rat. (#2861) --- src/parser/tptp/Tptp.g | 20 +++++++++++++++++--- test/regress/CMakeLists.txt | 1 + test/regress/regress0/tptp/is_rat_simple.p | 8 ++++++++ 3 files changed, 26 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress0/tptp/is_rat_simple.p (limited to 'test/regress/CMakeLists.txt') diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 54e9b0b4a..f4bc48df4 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -352,10 +352,24 @@ definedPred[CVC4::Expr& expr] | '$lesseq' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::LEQ); } | '$greater' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::GT); } | '$greatereq' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::GEQ); } - | '$is_rat' // all "real" are actually "rat" in CVC4 + | '$is_rat' + // a real n is a rational if there exists q,r integers such that + // to_real(q) = n*to_real(r), + // where r is non-zero. { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType()); - n = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n); - expr = MK_EXPR(CVC4::kind::LAMBDA, n, MK_CONST(bool(true))); + Expr q = EXPR_MANAGER->mkBoundVar("Q", EXPR_MANAGER->integerType()); + Expr qr = MK_EXPR(CVC4::kind::TO_REAL, q); + Expr r = EXPR_MANAGER->mkBoundVar("R", EXPR_MANAGER->integerType()); + Expr rr = MK_EXPR(CVC4::kind::TO_REAL, r); + Expr body = + MK_EXPR(CVC4::kind::AND, + MK_EXPR(CVC4::kind::NOT, + MK_EXPR(CVC4::kind::EQUAL, r, MK_CONST(Rational(0)))), + MK_EXPR(CVC4::kind::EQUAL, qr, MK_EXPR(CVC4::kind::MULT, n, rr))); + Expr bvl = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, q, r); + body = MK_EXPR(CVC4::kind::EXISTS, bvl, body); + Expr lbvl = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n); + expr = MK_EXPR(CVC4::kind::LAMBDA, lbvl, body); } | '$is_int' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::IS_INTEGER); } | '$distinct' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::DISTINCT); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index abec884c2..64d8e3598 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -877,6 +877,7 @@ set(regress_0_tests regress0/test9.cvc regress0/tptp/ARI086=1.p regress0/tptp/DAT001=1.p + regress0/tptp/is_rat_simple.p regress0/tptp/KRS018+1.p regress0/tptp/KRS063+1.p regress0/tptp/MGT019+2.p diff --git a/test/regress/regress0/tptp/is_rat_simple.p b/test/regress/regress0/tptp/is_rat_simple.p new file mode 100644 index 000000000..c983033b9 --- /dev/null +++ b/test/regress/regress0/tptp/is_rat_simple.p @@ -0,0 +1,8 @@ +% states that all reals are not rational (countersatisfiable) +% Status : CounterSatisfiable +%------------------------------------------------------------------------------ +tff(the,conjecture,( + ! [X: $real] : + ~ $is_rat(X) ) ). + +%------------------------------------------------------------------------------ -- cgit v1.2.3 From fef57367d28a62251cac47010cc6e80cd416832e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 14 Mar 2019 16:32:25 -0500 Subject: Use zero slope tangent planes for transcendental functions (#2803) --- src/theory/arith/nonlinear_extension.cpp | 34 +++++++++------------- test/regress/CMakeLists.txt | 4 ++- .../regress0/nl/nta/exp-neg2-unsat-unsound.smt2 | 10 +++++++ 3 files changed, 26 insertions(+), 22 deletions(-) create mode 100644 test/regress/regress0/nl/nta/exp-neg2-unsat-unsound.smt2 (limited to 'test/regress/CMakeLists.txt') diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 929c7808d..c43b9458b 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -2621,8 +2621,10 @@ void NonlinearExtension::mkPi(){ d_pi_neg = Rewriter::rewrite(NodeManager::currentNM()->mkNode( MULT, d_pi, NodeManager::currentNM()->mkConst(Rational(-1)))); //initialize bounds - d_pi_bound[0] = NodeManager::currentNM()->mkConst( Rational(333)/Rational(106) ); - d_pi_bound[1] = NodeManager::currentNM()->mkConst( Rational(355)/Rational(113) ); + d_pi_bound[0] = + NodeManager::currentNM()->mkConst(Rational(103993) / Rational(33102)); + d_pi_bound[1] = + NodeManager::currentNM()->mkConst(Rational(104348) / Rational(33215)); } } @@ -4358,31 +4360,21 @@ bool NonlinearExtension::checkTfTangentPlanesFun(Node tf, { // compute tangent plane // Figure 3: T( x ) - Node tplane; - Node poly_approx_deriv = getDerivative(poly_approx, d_taylor_real_fv); - Assert(!poly_approx_deriv.isNull()); - poly_approx_deriv = Rewriter::rewrite(poly_approx_deriv); - Trace("nl-ext-tftp-debug2") << "...derivative of " << poly_approx << " is " - << poly_approx_deriv << std::endl; - std::vector taylor_subs; - taylor_subs.push_back(c); - Assert(taylor_vars.size() == taylor_subs.size()); - Node poly_approx_c_deriv = poly_approx_deriv.substitute(taylor_vars.begin(), - taylor_vars.end(), - taylor_subs.begin(), - taylor_subs.end()); - tplane = nm->mkNode( - PLUS, - poly_approx_c, - nm->mkNode(MULT, poly_approx_c_deriv, nm->mkNode(MINUS, tf[0], c))); + // We use zero slope tangent planes, since the concavity of the Taylor + // approximation cannot be easily established. + Node tplane = poly_approx_c; Node lem = nm->mkNode(concavity == 1 ? GEQ : LEQ, tf, tplane); std::vector antec; + int mdir = regionToMonotonicityDir(k, region); for (unsigned i = 0; i < 2; i++) { - if (!bounds[i].isNull()) + // Tangent plane is valid in the interval [c,u) if the slope of the + // function matches its concavity, and is valid in (l, c] otherwise. + Node use_bound = (mdir == concavity) == (i == 0) ? c : bounds[i]; + if (!use_bound.isNull()) { - Node ant = nm->mkNode(i == 0 ? GEQ : LEQ, tf[0], bounds[i]); + Node ant = nm->mkNode(i == 0 ? GEQ : LEQ, tf[0], use_bound); antec.push_back(ant); } } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 64d8e3598..9b1ce17e4 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -518,6 +518,7 @@ set(regress_0_tests regress0/nl/nta/cos-sig-value.smt2 regress0/nl/nta/exp-n0.5-lb.smt2 regress0/nl/nta/exp-n0.5-ub.smt2 + regress0/nl/nta/exp-neg2-unsat-unsound.smt2 regress0/nl/nta/exp1-ub.smt2 regress0/nl/nta/real-pi.smt2 regress0/nl/nta/sin-sym.smt2 @@ -1174,7 +1175,6 @@ set(regress_1_tests regress1/lemmas/clocksynchro_5clocks.main_invar.base.smt regress1/lemmas/pursuit-safety-8.smt regress1/lemmas/simple_startup_9nodes.abstract.base.smt - regress1/nl/NAVIGATION2.smt2 regress1/nl/approx-sqrt-unsat.smt2 regress1/nl/approx-sqrt.smt2 regress1/nl/arctan2-expdef.smt2 @@ -2075,6 +2075,8 @@ set(regression_disabled_tests regress1/ho/hoa0102.smt2 # issue1048-arrays-int-real.smt2 -- different errors on debug and production. regress1/issue1048-arrays-int-real.smt2 + # times out after update to tangent planes + regress1/nl/NAVIGATION2.smt2 # ajreynol: disabled these since they give different error messages on # production and debug: regress1/quantifiers/macro-subtype-param.smt2 diff --git a/test/regress/regress0/nl/nta/exp-neg2-unsat-unsound.smt2 b/test/regress/regress0/nl/nta/exp-neg2-unsat-unsound.smt2 new file mode 100644 index 000000000..69c36179a --- /dev/null +++ b/test/regress/regress0/nl/nta/exp-neg2-unsat-unsound.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models +; EXPECT: sat +(set-logic QF_NRAT) +(declare-fun x () Real) +(assert (or +(and (<= (exp x) 0.01) (= x (- 2.0))) +(and (> (exp x) 0.2) (= x (- 1.0))) +) +) +(check-sat) -- cgit v1.2.3 From 2989780f0242d14712927bd4c01c4a521a8fe399 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 15 Mar 2019 18:35:43 -0500 Subject: New beta-reduction for HOL solving (#2869) --- src/theory/uf/theory_uf_rewriter.h | 79 ++++++++++++++++++++++++---- test/regress/CMakeLists.txt | 1 + test/regress/regress0/ho/shadowing-defs.smt2 | 41 +++++++++++++++ 3 files changed, 110 insertions(+), 11 deletions(-) create mode 100644 test/regress/regress0/ho/shadowing-defs.smt2 (limited to 'test/regress/CMakeLists.txt') diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index 3eb59e5fc..0583cfa1a 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -20,8 +20,10 @@ #ifndef __CVC4__THEORY__UF__THEORY_UF_REWRITER_H #define __CVC4__THEORY__UF__THEORY_UF_REWRITER_H +#include "expr/node_algorithm.h" #include "theory/rewriter.h" #include "theory/substitutions.h" +#include "options/uf_options.h" namespace CVC4 { namespace theory { @@ -46,19 +48,52 @@ public: } if(node.getKind() == kind::APPLY_UF) { if( node.getOperator().getKind() == kind::LAMBDA ){ + Trace("uf-ho-beta") + << "uf-ho-beta : beta-reducing all args of : " << node << "\n"; TNode lambda = node.getOperator(); - std::vector vars; - std::vector subs; - for (const TNode& v : lambda[0]) + Node ret; + // build capture-avoiding substitution since in HOL shadowing may have + // been introduced + if (options::ufHo()) { - vars.push_back(v); + std::vector vars; + std::vector subs; + for (const Node& v : lambda[0]) + { + vars.push_back(v); + } + for (const Node& s : node) + { + subs.push_back(s); + } + if (Trace.isOn("uf-ho-beta")) + { + Trace("uf-ho-beta") << "uf-ho-beta: ..sub of " << subs.size() + << " vars into " << subs.size() << " terms :\n"; + for (unsigned i = 0, size = subs.size(); i < size; ++i) + { + Trace("uf-ho-beta") << "uf-ho-beta: .... " << vars[i] << " |-> " + << subs[i] << "\n"; + } + } + ret = expr::substituteCaptureAvoiding(lambda[1], vars, subs); + Trace("uf-ho-beta") << "uf-ho-beta : ..result : " << ret << "\n"; } - for (const TNode& s : node) + else { - subs.push_back(s); + std::vector vars; + std::vector subs; + for (const TNode& v : lambda[0]) + { + vars.push_back(v); + } + for (const TNode& s : node) + { + subs.push_back(s); + } + ret = lambda[1].substitute( + vars.begin(), vars.end(), subs.begin(), subs.end()); } - Node ret = lambda[1].substitute( - vars.begin(), vars.end(), subs.begin(), subs.end()); return RewriteResponse(REWRITE_AGAIN_FULL, ret); }else if( !canUseAsApplyUfOperator( node.getOperator() ) ){ return RewriteResponse(REWRITE_AGAIN_FULL, getHoApplyForApplyUf(node)); @@ -66,9 +101,12 @@ public: }else if( node.getKind() == kind::HO_APPLY ){ if( node[0].getKind() == kind::LAMBDA ){ // resolve one argument of the lambda - TNode arg = Rewriter::rewrite( node[1] ); - TNode var = node[0][0][0]; - Node new_body = node[0][1].substitute( var, arg ); + Trace("uf-ho-beta") + << "uf-ho-beta : beta-reducing one argument of : " << node[0] + << " with " << node[1] << "\n"; + + // reconstruct the lambda first to avoid variable shadowing + Node new_body = node[0][1]; if( node[0][0].getNumChildren()>1 ){ std::vector< Node > new_vars; for( unsigned i=1; imkNode( kind::BOUND_VAR_LIST, new_vars ) ); largs.push_back( new_body ); new_body = NodeManager::currentNM()->mkNode( kind::LAMBDA, largs ); + Trace("uf-ho-beta") + << "uf-ho-beta : ....new lambda : " << new_body << "\n"; + } + + // build capture-avoiding substitution since in HOL shadowing may have + // been introduced + if (options::ufHo()) + { + Node arg = Rewriter::rewrite(node[1]); + Node var = node[0][0][0]; + new_body = expr::substituteCaptureAvoiding(new_body, var, arg); + } + else + { + TNode arg = Rewriter::rewrite(node[1]); + TNode var = node[0][0][0]; + new_body = new_body.substitute(var, arg); } + Trace("uf-ho-beta") + << "uf-ho-beta : ..new body : " << new_body << "\n"; return RewriteResponse( REWRITE_AGAIN_FULL, new_body ); } } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 9b1ce17e4..fb0e358e2 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -476,6 +476,7 @@ set(regress_0_tests regress0/ho/ite-apply-eq.smt2 regress0/ho/lambda-equality-non-canon.smt2 regress0/ho/modulo-func-equality.smt2 + regress0/ho/shadowing-defs.smt2 regress0/ho/simple-matching-partial.smt2 regress0/ho/simple-matching.smt2 regress0/ho/trans.smt2 diff --git a/test/regress/regress0/ho/shadowing-defs.smt2 b/test/regress/regress0/ho/shadowing-defs.smt2 new file mode 100644 index 000000000..722e970b6 --- /dev/null +++ b/test/regress/regress0/ho/shadowing-defs.smt2 @@ -0,0 +1,41 @@ +; COMMAND-LINE: --uf-ho +; EXPECT: unknown +(set-logic ALL) +(declare-sort $$unsorted 0) +(declare-sort mu 0) + +(declare-fun mnot ((-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mnot (lambda ((Phi (-> $$unsorted Bool)) (W $$unsorted)) (not (Phi W))))) + +(declare-fun mor ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mor (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (W $$unsorted)) (or (Phi W) (Psi W))))) + +(declare-fun mand ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mand (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mnot (mor (mnot Phi) (mnot Psi)) __flatten_var_0)))) + +(declare-fun mimplies ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mimplies (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mor (mnot Phi) Psi __flatten_var_0)))) + +(declare-fun mforall_ind ((-> mu $$unsorted Bool) $$unsorted) Bool) +(assert (= mforall_ind (lambda ((Phi (-> mu $$unsorted Bool)) (W $$unsorted)) (forall ((X mu)) (Phi X W) )))) + +(declare-fun mbox ((-> $$unsorted $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mbox (lambda ((R (-> $$unsorted $$unsorted Bool)) (Phi (-> $$unsorted Bool)) (W $$unsorted)) (forall ((V $$unsorted)) (or (not (R W V)) (Phi V)) )))) + +(declare-fun mvalid ((-> $$unsorted Bool)) Bool) +(assert (= mvalid (lambda ((Phi (-> $$unsorted Bool))) (forall ((W $$unsorted)) (Phi W) )))) + +(declare-fun a1 ($$unsorted $$unsorted) Bool) +(declare-fun a2 ($$unsorted $$unsorted) Bool) +(declare-fun a3 ($$unsorted $$unsorted) Bool) + +(declare-fun jan () mu) +(declare-fun cola () mu) + +(declare-fun likes (mu mu $$unsorted) Bool) + +(declare-fun very_much_likes (mu mu $$unsorted) Bool) + +(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mforall_ind (lambda ((Y mu) (__flatten_var_0 $$unsorted)) (mbox a3 (mimplies (mand (likes X Y) (mand (mbox a1 (likes X Y)) (mbox a2 (likes X Y)))) (very_much_likes X Y)) __flatten_var_0)) __flatten_var_0))))) + +(check-sat) \ No newline at end of file -- cgit v1.2.3 From 6322e6be67ff2b82e6751046b3383db1b52e09d3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 19 Mar 2019 11:51:11 -0500 Subject: Fix fairness issue with fast sygus enumerator (#2873) --- src/theory/quantifiers/sygus/sygus_enumerator.cpp | 24 +++++++++++++++++++- test/regress/CMakeLists.txt | 1 + test/regress/regress1/sygus/cube-nia.sy | 27 +++++++++++++++++++++++ 3 files changed, 51 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress1/sygus/cube-nia.sy (limited to 'test/regress/CMakeLists.txt') diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index 9981b5141..fb16e274f 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -476,6 +476,13 @@ bool SygusEnumerator::TermEnumSlave::validateIndex() { Assert(d_index == tc.getNumTerms()); Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : force master...\n"; + // if the size of the master is larger than the size limit, then + // there is no use continuing, since there are no more terms that this + // slave enumerator can return. + if (d_master->getCurrentSize() > d_sizeLim) + { + return false; + } // must push the master index if (!d_master->increment()) { @@ -655,9 +662,14 @@ bool SygusEnumerator::TermEnumMaster::increment() { return false; } + Trace("sygus-enum-summary") << "SygusEnumerator::TermEnumMaster: increment " + << d_tn << "..." << std::endl; d_isIncrementing = true; bool ret = incrementInternal(); d_isIncrementing = false; + Trace("sygus-enum-summary") + << "SygusEnumerator::TermEnumMaster: finished increment " << d_tn + << std::endl; return ret; } @@ -789,7 +801,15 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal() // restart with constructor class one (skip nullary constructors) d_consClassNum = 1; - return incrementInternal(); + + // We break for a round: return the null term when we cross a size + // boundary. This ensures that the necessary breaks are taken, e.g. + // in slave enumerators who may instead want to abandon this call to + // increment master when the size of the master makes their increment + // infeasible. + d_currTermSet = true; + d_currTerm = Node::null(); + return true; } bool incSuccess = false; @@ -819,6 +839,8 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal() // the term was not unique based on rewriting Trace("sygus-enum-debug2") << "master(" << d_tn << "): failed addTerm\n"; + // we will return null (d_currTermSet is true at this point) + Assert(d_currTermSet); d_currTerm = Node::null(); } } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index fb0e358e2..0b4a4bdc7 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1603,6 +1603,7 @@ set(regress_1_tests regress1/sygus/crci-ssb-unk.sy regress1/sygus/crcy-si-rcons.sy regress1/sygus/crcy-si.sy + regress1/sygus/cube-nia.sy regress1/sygus/dt-test-ns.sy regress1/sygus/dup-op.sy regress1/sygus/fg_polynomial3.sy diff --git a/test/regress/regress1/sygus/cube-nia.sy b/test/regress/regress1/sygus/cube-nia.sy new file mode 100644 index 000000000..da7d98e66 --- /dev/null +++ b/test/regress/regress1/sygus/cube-nia.sy @@ -0,0 +1,27 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + +(set-logic NIA) + +(synth-fun cube ((x Int)) Int + ( + (Start Int (ntInt)) + + (ntBool Bool + ( + (> ntInt ntInt) + (= ntInt ntInt) + ) + ) + (ntInt Int + (1 x + (* ntInt ntInt) + (ite ntBool ntInt ntInt) + ) + ) + ) +) + +(constraint (= (cube 1) 1)) +(constraint (= (cube 2) 8)) +(check-synth) -- cgit v1.2.3 From 7dfd55085c60affdc4523c330ea2d2daa69ae66a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 19 Mar 2019 20:54:40 -0500 Subject: Sygus abduction feature (#2744) --- src/CMakeLists.txt | 2 + src/options/quantifiers_options.toml | 10 ++ src/preprocessing/passes/sygus_abduct.cpp | 174 +++++++++++++++++++++ src/preprocessing/passes/sygus_abduct.h | 72 +++++++++ src/preprocessing/preprocessing_pass_registry.cpp | 2 + src/smt/smt_engine.cpp | 75 ++++++--- src/smt/smt_engine.h | 12 ++ src/theory/quantifiers/expr_miner.cpp | 2 + .../quantifiers/sygus/sygus_repair_const.cpp | 1 + src/theory/quantifiers/sygus/synth_conjecture.cpp | 2 + src/theory/quantifiers/sygus/synth_engine.cpp | 1 + test/regress/CMakeLists.txt | 1 + test/regress/regress1/sygus-abduct-test.smt2 | 16 ++ 13 files changed, 347 insertions(+), 23 deletions(-) create mode 100644 src/preprocessing/passes/sygus_abduct.cpp create mode 100644 src/preprocessing/passes/sygus_abduct.h create mode 100644 test/regress/regress1/sygus-abduct-test.smt2 (limited to 'test/regress/CMakeLists.txt') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5f34fe59b..244845fda 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -88,6 +88,8 @@ libcvc4_add_sources( preprocessing/passes/sort_infer.h preprocessing/passes/static_learning.cpp preprocessing/passes/static_learning.h + preprocessing/passes/sygus_abduct.cpp + preprocessing/passes/sygus_abduct.h preprocessing/passes/sygus_inference.cpp preprocessing/passes/sygus_inference.h preprocessing/passes/symmetry_breaker.cpp diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 4deb5565d..1ff85c96d 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -876,6 +876,15 @@ header = "options/quantifiers_options.h" read_only = false help = "attempt to preprocess arbitrary inputs to sygus conjectures" +[[option]] + name = "sygusAbduct" + category = "regular" + long = "sygus-abduct" + type = "bool" + default = "false" + read_only = false + help = "compute abductions using sygus" + [[option]] name = "ceGuidedInst" category = "regular" @@ -1428,6 +1437,7 @@ header = "options/quantifiers_options.h" default = "false" help = "compute backwards filtering to compute whether previous solutions are filtered based on later ones" + [[option]] name = "sygusExprMinerCheckUseExport" category = "expert" diff --git a/src/preprocessing/passes/sygus_abduct.cpp b/src/preprocessing/passes/sygus_abduct.cpp new file mode 100644 index 000000000..a2fe38219 --- /dev/null +++ b/src/preprocessing/passes/sygus_abduct.cpp @@ -0,0 +1,174 @@ +/********************* */ +/*! \file sygus_abduct.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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 Implementation of sygus abduction preprocessing pass, which + ** transforms an arbitrary input into an abduction problem. + **/ + +#include "preprocessing/passes/sygus_abduct.h" + +#include "expr/node_algorithm.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "smt/smt_statistics_registry.h" +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +SygusAbduct::SygusAbduct(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "sygus-abduct"){}; + +PreprocessingPassResult SygusAbduct::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + NodeManager* nm = NodeManager::currentNM(); + Trace("sygus-abduct") << "Run sygus abduct..." << std::endl; + + Trace("sygus-abduct-debug") << "Collect symbols..." << std::endl; + std::unordered_set symset; + std::vector& asserts = assertionsToPreprocess->ref(); + // do we have any assumptions, e.g. via check-sat-assuming? + bool usingAssumptions = (assertionsToPreprocess->getNumAssumptions() > 0); + // The following is our set of "axioms". We construct this set only when the + // usingAssumptions (above) is true. In this case, our input formula is + // partitioned into Fa ^ Fc as described in the header of this class, where: + // - The conjunction of assertions marked as assumptions are the negated + // conjecture Fc, and + // - The conjunction of all other assertions are the axioms Fa. + std::vector axioms; + for (size_t i = 0, size = asserts.size(); i < size; i++) + { + expr::getSymbols(asserts[i], symset); + // if we are not an assumption, add it to the set of axioms + if (usingAssumptions && i < assertionsToPreprocess->getAssumptionsStart()) + { + axioms.push_back(asserts[i]); + } + } + Trace("sygus-abduct-debug") + << "...finish, got " << symset.size() << " symbols." << std::endl; + + Trace("sygus-abduct-debug") << "Setup symbols..." << std::endl; + std::vector syms; + std::vector vars; + std::vector varlist; + std::vector varlistTypes; + for (const Node& s : symset) + { + TypeNode tn = s.getType(); + if (tn.isFirstClass()) + { + std::stringstream ss; + ss << s; + Node var = nm->mkBoundVar(tn); + syms.push_back(s); + vars.push_back(var); + Node vlv = nm->mkBoundVar(ss.str(), tn); + varlist.push_back(vlv); + varlistTypes.push_back(tn); + } + } + Trace("sygus-abduct-debug") << "...finish" << std::endl; + + Trace("sygus-abduct-debug") << "Make abduction predicate..." << std::endl; + // make the abduction predicate to synthesize + TypeNode abdType = varlistTypes.empty() ? nm->booleanType() + : nm->mkPredicateType(varlistTypes); + Node abd = nm->mkBoundVar("A", abdType); + Trace("sygus-abduct-debug") << "...finish" << std::endl; + + Trace("sygus-abduct-debug") << "Make abduction predicate app..." << std::endl; + std::vector achildren; + achildren.push_back(abd); + achildren.insert(achildren.end(), vars.begin(), vars.end()); + Node abdApp = vars.empty() ? abd : nm->mkNode(APPLY_UF, achildren); + Trace("sygus-abduct-debug") << "...finish" << std::endl; + + Trace("sygus-abduct-debug") << "Set attributes..." << std::endl; + // set the sygus bound variable list + Node abvl = nm->mkNode(BOUND_VAR_LIST, varlist); + abd.setAttribute(theory::SygusSynthFunVarListAttribute(), abvl); + Trace("sygus-abduct-debug") << "...finish" << std::endl; + + Trace("sygus-abduct-debug") << "Make conjecture body..." << std::endl; + Node input = asserts.size() == 1 ? asserts[0] : nm->mkNode(AND, asserts); + input = input.substitute(syms.begin(), syms.end(), vars.begin(), vars.end()); + // A(x) => ~input( x ) + input = nm->mkNode(OR, abdApp.negate(), input.negate()); + Trace("sygus-abduct-debug") << "...finish" << std::endl; + + Trace("sygus-abduct-debug") << "Make conjecture..." << std::endl; + Node res = input.negate(); + if (!vars.empty()) + { + Node bvl = nm->mkNode(BOUND_VAR_LIST, vars); + // exists x. ~( A( x ) => ~input( x ) ) + res = nm->mkNode(EXISTS, bvl, res); + } + // sygus attribute + Node sygusVar = nm->mkSkolem("sygus", nm->booleanType()); + theory::SygusAttribute ca; + sygusVar.setAttribute(ca, true); + Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusVar); + std::vector iplc; + iplc.push_back(instAttr); + if (!axioms.empty()) + { + Node aconj = axioms.size() == 1 ? axioms[0] : nm->mkNode(AND, axioms); + aconj = + aconj.substitute(syms.begin(), syms.end(), vars.begin(), vars.end()); + Trace("sygus-abduct") << "---> Assumptions: " << aconj << std::endl; + Node sc = nm->mkNode(AND, aconj, abdApp); + Node vbvl = nm->mkNode(BOUND_VAR_LIST, vars); + sc = nm->mkNode(EXISTS, vbvl, sc); + Node sygusScVar = nm->mkSkolem("sygus_sc", nm->booleanType()); + sygusScVar.setAttribute(theory::SygusSideConditionAttribute(), sc); + instAttr = nm->mkNode(INST_ATTRIBUTE, sygusScVar); + // build in the side condition + // exists x. A( x ) ^ input_axioms( x ) + // as an additional annotation on the sygus conjecture. In other words, + // the abducts A we procedure must be consistent with our axioms. + iplc.push_back(instAttr); + } + Node instAttrList = nm->mkNode(INST_PATTERN_LIST, iplc); + + Node fbvl = nm->mkNode(BOUND_VAR_LIST, abd); + + // forall A. exists x. ~( A( x ) => ~input( x ) ) + res = nm->mkNode(FORALL, fbvl, res, instAttrList); + Trace("sygus-abduct-debug") << "...finish" << std::endl; + + res = theory::Rewriter::rewrite(res); + + Trace("sygus-abduct") << "Generate: " << res << std::endl; + + Node trueNode = nm->mkConst(true); + + assertionsToPreprocess->replace(0, res); + for (size_t i = 1, size = assertionsToPreprocess->size(); i < size; ++i) + { + assertionsToPreprocess->replace(i, trueNode); + } + + return PreprocessingPassResult::NO_CONFLICT; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/sygus_abduct.h b/src/preprocessing/passes/sygus_abduct.h new file mode 100644 index 000000000..8e83bf1d7 --- /dev/null +++ b/src/preprocessing/passes/sygus_abduct.h @@ -0,0 +1,72 @@ +/********************* */ +/*! \file sygus_abduct.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 Sygus abduction preprocessing pass, which transforms an arbitrary + ** input into an abduction problem. + **/ + +#ifndef __CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H +#define __CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +/** SygusAbduct + * + * A preprocessing utility that turns a set of quantifier-free assertions into + * a sygus conjecture that encodes an abduction problem. In detail, if our + * input formula is F( x ) for free symbols x, then we construct the sygus + * conjecture: + * + * exists A. forall x. ( A( x ) => ~F( x ) ) + * + * where A( x ) is a predicate over the free symbols of our input. In other + * words, A( x ) is a sufficient condition for showing ~F( x ). + * + * Another way to view this is A( x ) is any condition such that A( x ) ^ F( x ) + * is unsatisfiable. + * + * A common use case is to find the weakest such A that meets the above + * specification. We do this by streaming solutions (sygus-stream) for A + * while filtering stronger solutions (sygus-filter-sol=strong). These options + * are enabled by default when this preprocessing class is used (sygus-abduct). + * + * If the input F( x ) is partitioned into axioms Fa and negated conjecture Fc + * Fa( x ) ^ Fc( x ), then the sygus conjecture we construct is: + * + * exists A. ( exists y. A( y ) ^ Fa( y ) ) ^ forall x. ( A( x ) => ~F( x ) ) + * + * In other words, A( y ) must be consistent with our axioms Fa and imply + * ~F( x ). We encode this conjecture using SygusSideConditionAttribute. + */ +class SygusAbduct : public PreprocessingPass +{ + public: + SygusAbduct(PreprocessingPassContext* preprocContext); + + protected: + /** + * Replaces the set of assertions by an abduction sygus problem described + * above. + */ + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* __CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H_ */ diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp index f2e7c8603..30bbf41c9 100644 --- a/src/preprocessing/preprocessing_pass_registry.cpp +++ b/src/preprocessing/preprocessing_pass_registry.cpp @@ -48,6 +48,7 @@ #include "preprocessing/passes/sep_skolem_emp.h" #include "preprocessing/passes/sort_infer.h" #include "preprocessing/passes/static_learning.h" +#include "preprocessing/passes/sygus_abduct.h" #include "preprocessing/passes/sygus_inference.h" #include "preprocessing/passes/symmetry_breaker.h" #include "preprocessing/passes/symmetry_detect.h" @@ -126,6 +127,7 @@ PreprocessingPassRegistry::PreprocessingPassRegistry() registerPassInfo("synth-rr", callCtor); registerPassInfo("real-to-int", callCtor); registerPassInfo("sygus-infer", callCtor); + registerPassInfo("sygus-abduct", callCtor); registerPassInfo("bv-to-bool", callCtor); registerPassInfo("bv-intro-pow2", callCtor); registerPassInfo("sort-inference", callCtor); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8427599a9..8305d1d4d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -879,6 +879,7 @@ SmtEngine::SmtEngine(ExprManager* em) d_defineCommands(), d_logic(), d_originalOptions(), + d_isInternalSubsolver(false), d_pendingPops(0), d_fullyInited(false), d_problemExtended(false), @@ -1264,16 +1265,20 @@ void SmtEngine::setDefaults() { } // sygus inference may require datatypes - if (options::sygusInference() || options::sygusRewSynthInput()) + if (!d_isInternalSubsolver) { - d_logic = d_logic.getUnlockedCopy(); - // sygus requires arithmetic, datatypes and quantifiers - d_logic.enableTheory(THEORY_ARITH); - d_logic.enableTheory(THEORY_DATATYPES); - d_logic.enableTheory(THEORY_QUANTIFIERS); - d_logic.lock(); - // since we are trying to recast as sygus, we assume the input is sygus - is_sygus = true; + if (options::sygusInference() || options::sygusRewSynthInput() + || options::sygusAbduct()) + { + d_logic = d_logic.getUnlockedCopy(); + // sygus requires arithmetic, datatypes and quantifiers + d_logic.enableTheory(THEORY_ARITH); + d_logic.enableTheory(THEORY_DATATYPES); + d_logic.enableTheory(THEORY_QUANTIFIERS); + d_logic.lock(); + // since we are trying to recast as sygus, we assume the input is sygus + is_sygus = true; + } } if ((options::checkModels() || options::checkSynthSol() @@ -1958,8 +1963,16 @@ void SmtEngine::setDefaults() { options::sygusExtRew.set(false); } } + if (options::sygusAbduct()) + { + // if doing abduction, we should filter strong solutions + if (!options::sygusFilterSolMode.wasSetByUser()) + { + options::sygusFilterSolMode.set(quantifiers::SYGUS_FILTER_SOL_STRONG); + } + } if (options::sygusRewSynth() || options::sygusRewVerify() - || options::sygusQueryGen()) + || options::sygusQueryGen() || options::sygusAbduct()) { // rewrite rule synthesis implies that sygus stream must be true options::sygusStream.set(true); @@ -1967,8 +1980,9 @@ void SmtEngine::setDefaults() { if (options::sygusStream()) { // Streaming is incompatible with techniques that focus the search towards - // finding a single solution. This currently includes the PBE solver and - // static template inference for invariant synthesis. + // finding a single solution. This currently includes the PBE solver, + // static template inference for invariant synthesis, and single + // invocation techniques. if (!options::sygusUnifPbe.wasSetByUser()) { options::sygusUnifPbe.set(false); @@ -1982,6 +1996,10 @@ void SmtEngine::setDefaults() { { options::sygusInvTemplMode.set(quantifiers::SYGUS_INV_TEMPL_MODE_NONE); } + if (!options::cegqiSingleInvMode.wasSetByUser()) + { + options::cegqiSingleInvMode.set(quantifiers::CEGQI_SI_MODE_NONE); + } } //do not allow partial functions if( !options::bitvectorDivByZeroConst.wasSetByUser() ){ @@ -2282,11 +2300,13 @@ void SmtEngine::setDefaults() { "--sygus-expr-miner-check-timeout=N requires " "--sygus-expr-miner-check-use-export"); } - if (options::sygusRewSynthInput()) + if (options::sygusRewSynthInput() || options::sygusAbduct()) { - throw OptionException( - "--sygus-rr-synth-input requires " - "--sygus-expr-miner-check-use-export"); + std::stringstream ss; + ss << (options::sygusRewSynthInput() ? "--sygus-rr-synth-input" + : "--sygus-abduct"); + ss << "requires --sygus-expr-miner-check-use-export"; + throw OptionException(ss.str()); } } @@ -3314,10 +3334,6 @@ void SmtEnginePrivate::processAssertions() { d_smt.d_fmfRecFunctionsDefined->push_back( f ); } } - if (options::sygusInference()) - { - d_passes["sygus-infer"]->apply(&d_assertions); - } } if( options::sortInference() || options::ufssFairnessMonotone() ){ @@ -3328,10 +3344,22 @@ void SmtEnginePrivate::processAssertions() { d_passes["pseudo-boolean-processor"]->apply(&d_assertions); } - if (options::sygusRewSynthInput()) + // rephrasing normal inputs as sygus problems + if (!d_smt.d_isInternalSubsolver) { - // do candidate rewrite rule synthesis - d_passes["synth-rr"]->apply(&d_assertions); + if (options::sygusInference()) + { + d_passes["sygus-infer"]->apply(&d_assertions); + } + else if (options::sygusAbduct()) + { + d_passes["sygus-abduct"]->apply(&d_assertions); + } + else if (options::sygusRewSynthInput()) + { + // do candidate rewrite rule synthesis + d_passes["synth-rr"]->apply(&d_assertions); + } } Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-simplify" << endl; @@ -5297,6 +5325,7 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) nodeManagerOptions.setOption(key, optionarg); } +void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; } CVC4::SExpr SmtEngine::getOption(const std::string& key) const { NodeManagerScope nms(d_nodeManager); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index e53d1eb55..5c41feaba 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -209,6 +209,9 @@ class CVC4_PUBLIC SmtEngine { */ Options d_originalOptions; + /** whether this is an internal subsolver */ + bool d_isInternalSubsolver; + /** * Number of internal pops that have been deferred. */ @@ -502,6 +505,15 @@ class CVC4_PUBLIC SmtEngine { void setOption(const std::string& key, const CVC4::SExpr& value) /* throw(OptionException, ModalException) */; + /** Set is internal subsolver. + * + * This function is called on SmtEngine objects that are created internally. + * It is used to mark that this SmtEngine should not perform preprocessing + * passes that rephrase the input, such as --sygus-rr-synth-input or + * --sygus-abduct. + */ + void setIsInternalSubsolver(); + /** sets the input name */ void setFilename(std::string filename); /** return the input name (if any) */ diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index b65d1c522..65678f674 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -87,9 +87,11 @@ void ExprMiner::initializeChecker(std::unique_ptr& checker, try { checker.reset(new SmtEngine(&em)); + checker->setIsInternalSubsolver(); checker->setTimeLimit(options::sygusExprMinerCheckTimeout(), true); checker->setLogic(smt::currentSmtEngine()->getLogicInfo()); checker->setOption("sygus-rr-synth-input", false); + checker->setOption("sygus-abduct", false); checker->setOption("input-language", "smt2"); Expr equery = squery.toExpr().exportTo(&em, varMap); checker->assertFormula(equery); diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 09525712f..18722a192 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -115,6 +115,7 @@ void SygusRepairConst::initializeChecker(std::unique_ptr& checker, try { checker.reset(new SmtEngine(&em)); + checker->setIsInternalSubsolver(); checker->setTimeLimit(options::sygusRepairConstTimeout(), true); checker->setLogic(smt::currentSmtEngine()->getLogicInfo()); // renable options disabled by sygus diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index e25e8a225..2e0fa75fe 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -540,6 +540,7 @@ bool SynthConjecture::doCheck(std::vector& lems) Trace("cegqi-engine") << "Check side condition..." << std::endl; Trace("cegqi-debug") << "Check side condition : " << sc << std::endl; SmtEngine scSmt(nm->toExprManager()); + scSmt.setIsInternalSubsolver(); scSmt.setLogic(smt::currentSmtEngine()->getLogicInfo()); scSmt.assertFormula(sc.toExpr()); Result r = scSmt.checkSat(); @@ -572,6 +573,7 @@ bool SynthConjecture::doCheck(std::vector& lems) { Trace("cegqi-engine") << " *** Verify with subcall..." << std::endl; SmtEngine verifySmt(nm->toExprManager()); + verifySmt.setIsInternalSubsolver(); verifySmt.setLogic(smt::currentSmtEngine()->getLogicInfo()); verifySmt.assertFormula(query.toExpr()); Result r = verifySmt.checkSat(); diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index d3eff1750..0623c257a 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -159,6 +159,7 @@ void SynthEngine::assignConjecture(Node q) { // create new smt engine to do quantifier elimination SmtEngine smt_qe(nm->toExprManager()); + smt_qe.setIsInternalSubsolver(); smt_qe.setLogic(smt::currentSmtEngine()->getLogicInfo()); Trace("cegqi-qep") << "Property is non-ground single invocation, run " "QE to obtain single invocation." diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 0b4a4bdc7..21e08f2bf 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1582,6 +1582,7 @@ set(regress_1_tests regress1/strings/type002.smt2 regress1/strings/type003.smt2 regress1/strings/username_checker_min.smt2 + regress1/sygus-abduct-test.smt2 regress1/sygus/VC22_a.sy regress1/sygus/abv.sy regress1/sygus/array_search_2.sy diff --git a/test/regress/regress1/sygus-abduct-test.smt2 b/test/regress/regress1/sygus-abduct-test.smt2 new file mode 100644 index 000000000..4ac90870c --- /dev/null +++ b/test/regress/regress1/sygus-abduct-test.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --sygus-abduct --sygus-abort-size=2 +; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.") +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 1 + +(set-logic QF_UFLIRA) +(declare-fun n () Int) +(declare-fun m () Int) +(declare-fun x () Int) +(declare-fun y () Int) + +(assert (>= n 1)) +(assert (and (<= n x)(<= x (+ n 5)))) +(assert (and (<= 1 y)(<= y m))) + +(check-sat-assuming ((< x y))) -- cgit v1.2.3 From 6c8a2652605b031182b3c2c25d237719470f5620 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 21 Mar 2019 13:41:46 -0500 Subject: Rewrite selectors correctly applied to constructors (#2875) --- src/theory/datatypes/datatypes_rewriter.cpp | 34 ++++++++++++++++++++++---- src/theory/quantifiers/sygus/sygus_unif_io.cpp | 30 +++++++++++++++-------- test/regress/CMakeLists.txt | 2 ++ test/regress/regress1/sygus/double.sy | 26 ++++++++++++++++++++ test/regress/regress1/sygus/extract.sy | 19 ++++++++++++++ 5 files changed, 96 insertions(+), 15 deletions(-) create mode 100644 test/regress/regress1/sygus/double.sy create mode 100644 test/regress/regress1/sygus/extract.sy (limited to 'test/regress/CMakeLists.txt') diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index a2458e2eb..507bbfdd1 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -32,7 +32,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) { return rewriteConstructor(in); } - else if (k == kind::APPLY_SELECTOR_TOTAL) + else if (k == kind::APPLY_SELECTOR_TOTAL || k == kind::APPLY_SELECTOR) { return rewriteSelector(in); } @@ -331,6 +331,7 @@ RewriteResponse DatatypesRewriter::rewriteConstructor(TNode in) RewriteResponse DatatypesRewriter::rewriteSelector(TNode in) { + Kind k = in.getKind(); if (in[0].getKind() == kind::APPLY_CONSTRUCTOR) { // Have to be careful not to rewrite well-typed expressions @@ -338,17 +339,40 @@ RewriteResponse DatatypesRewriter::rewriteSelector(TNode in) // e.g. "pred(zero)". TypeNode tn = in.getType(); TypeNode argType = in[0].getType(); - TNode selector = in.getOperator(); + Expr selector = in.getOperator().toExpr(); TNode constructor = in[0].getOperator(); size_t constructorIndex = indexOf(constructor); - const Datatype& dt = Datatype::datatypeOf(selector.toExpr()); + const Datatype& dt = Datatype::datatypeOf(selector); const DatatypeConstructor& c = dt[constructorIndex]; Trace("datatypes-rewrite-debug") << "Rewriting collapsable selector : " << in; Trace("datatypes-rewrite-debug") << ", cindex = " << constructorIndex << ", selector is " << selector << std::endl; - int selectorIndex = c.getSelectorIndexInternal(selector.toExpr()); + // The argument that the selector extracts, or -1 if the selector is + // is wrongly applied. + int selectorIndex = -1; + if (k == kind::APPLY_SELECTOR_TOTAL) + { + // The argument index of internal selectors is obtained by + // getSelectorIndexInternal. + selectorIndex = c.getSelectorIndexInternal(selector); + } + else + { + // The argument index of external selectors (applications of + // APPLY_SELECTOR) is given by an attribute and obtained via indexOf below + // The argument is only valid if it is the proper constructor. + selectorIndex = Datatype::indexOf(selector); + if (selectorIndex < 0 || selectorIndex >= c.getNumArgs()) + { + selectorIndex = -1; + } + else if (c[selectorIndex].getSelector() != selector) + { + selectorIndex = -1; + } + } Trace("datatypes-rewrite-debug") << "Internal selector index is " << selectorIndex << std::endl; if (selectorIndex >= 0) @@ -374,7 +398,7 @@ RewriteResponse DatatypesRewriter::rewriteSelector(TNode in) return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]); } } - else + else if (k == kind::APPLY_SELECTOR_TOTAL) { Node gt; bool useTe = true; diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index c9db62735..8833c0cdf 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -641,23 +641,33 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector& lemmas) for (unsigned j = 0, size = itsr->second.size(); j < size; j++) { Node res = itsr->second[j]; - Assert(res.isConst()); + // The value of this term for this example, or the truth value of + // the I/O pair if the role of this enumerator is enum_io. Node resb; - if (eiv.getRole() == enum_io) + // If the result is not constant, then we cannot determine its value + // on this point. In this case, resb remains null. + if (res.isConst()) { - Node out = d_examples_out[j]; - Assert(out.isConst()); - resb = res == out ? d_true : d_false; - } - else - { - resb = res; + if (eiv.getRole() == enum_io) + { + Node out = d_examples_out[j]; + Assert(out.isConst()); + resb = res == out ? d_true : d_false; + } + else + { + resb = res; + } } cond_vals[resb] = true; results.push_back(resb); if (Trace.isOn("sygus-sui-enum")) { - if (resb.getType().isBoolean()) + if (resb.isNull()) + { + Trace("sygus-sui-enum") << "_"; + } + else if (resb.getType().isBoolean()) { Trace("sygus-sui-enum") << (resb == d_true ? "1" : "0"); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 21e08f2bf..083f8df75 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1605,8 +1605,10 @@ set(regress_1_tests regress1/sygus/crcy-si-rcons.sy regress1/sygus/crcy-si.sy regress1/sygus/cube-nia.sy + regress1/sygus/double.sy regress1/sygus/dt-test-ns.sy regress1/sygus/dup-op.sy + regress1/sygus/extract.sy regress1/sygus/fg_polynomial3.sy regress1/sygus/find_sc_bvult_bvnot.sy regress1/sygus/hd-01-d1-prog.sy diff --git a/test/regress/regress1/sygus/double.sy b/test/regress/regress1/sygus/double.sy new file mode 100644 index 000000000..f3fea3122 --- /dev/null +++ b/test/regress/regress1/sygus/double.sy @@ -0,0 +1,26 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + +(set-logic SLIA) +(declare-datatype Ex ((Ex2 (ex Int)))) + +(synth-fun double ((x1 Ex)) Int + ( + (Start Int (ntInt)) + (ntInt Int + ( + (ex ntEx) + (+ ntInt ntInt) + ) + ) + (ntEx Ex + ( + x1 + (Ex2 ntInt) + ) + ) + ) +) +(constraint (= (double (Ex2 1)) 2)) +(constraint (= (double (Ex2 4)) 8)) +(check-synth) diff --git a/test/regress/regress1/sygus/extract.sy b/test/regress/regress1/sygus/extract.sy new file mode 100644 index 000000000..d1541fa87 --- /dev/null +++ b/test/regress/regress1/sygus/extract.sy @@ -0,0 +1,19 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + +(set-logic ALL_SUPPORTED) +(declare-datatype Ex ((Ex2 (ex Int)))) + +(synth-fun ident ((x1 Ex)) Int + ( + (Start Int (ntInt)) + (ntInt Int + ( + (ex ntEx) + ) + ) + (ntEx Ex ( x1 ) ) + ) +) +(constraint (= (ident (Ex2 1)) 1)) +(check-synth) -- cgit v1.2.3 From d5ad777c539f5a49e1cdf4e483c2d5d689738b12 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 22 Mar 2019 09:01:13 -0500 Subject: More fixes for PBE with datatypes (#2882) --- src/theory/quantifiers/sygus/sygus_unif_io.cpp | 54 ++++++++++++++++++-------- test/regress/CMakeLists.txt | 1 + test/regress/regress1/sygus/tester.sy | 37 ++++++++++++++++++ 3 files changed, 76 insertions(+), 16 deletions(-) create mode 100644 test/regress/regress1/sygus/tester.sy (limited to 'test/regress/CMakeLists.txt') diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 8833c0cdf..7e999d3f5 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -448,20 +448,33 @@ void SubsumeTrie::getLeavesInternal(const std::vector& vals, ++it) { int new_status = status; - // if the current value is true + bool success = true; + // if the current value is true, we must consider the value of this child if (curr_val_true) { if (status != 0) { - Assert(it->first.isConst() && it->first.getType().isBoolean()); - new_status = (it->first.getConst() ? 1 : -1); - if (status != -2 && new_status != status) + if (it->first.isNull()) + { + // The value of this child is unknown on this point, hence we + // ignore it. + success = false; + } + else { - new_status = 0; + Assert(it->first.getType().isBoolean()); + new_status = (it->first.getConst() ? 1 : -1); + if (status != -2 && new_status != status) + { + new_status = 0; + } } } } - it->second.getLeavesInternal(vals, pol, v, index + 1, new_status); + if (success) + { + it->second.getLeavesInternal(vals, pol, v, index + 1, new_status); + } } } } @@ -644,17 +657,25 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector& lemmas) // The value of this term for this example, or the truth value of // the I/O pair if the role of this enumerator is enum_io. Node resb; - // If the result is not constant, then we cannot determine its value - // on this point. In this case, resb remains null. - if (res.isConst()) + if (eiv.getRole() == enum_io) { - if (eiv.getRole() == enum_io) - { - Node out = d_examples_out[j]; - Assert(out.isConst()); - resb = res == out ? d_true : d_false; - } - else + Node out = d_examples_out[j]; + Assert(out.isConst()); + // If the result is not constant, then we assume that it does + // not satisfy the example. This is a safe underapproximation + // of the good behavior of the current term, that is, we only + // produce solutions whose values are fully evaluatable on all input + // points. Notice that terms may be used as leaves of decision + // trees that are fully evaluatable on points in that branch, but + // are not evaluatable on others, e.g. (head x) in the solution: + // (ite ((_ is cons) x) (head x) 5) + resb = (res.isConst() && res == out) ? d_true : d_false; + } + else + { + // We only set resb if it is constant, otherwise it remains null. + // This indicates its value cannot be determined. + if (res.isConst()) { resb = res; } @@ -687,6 +708,7 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector& lemmas) std::vector subsume; if (cond_vals.find(d_false) == cond_vals.end()) { + Assert(cond_vals.size() == 1); // it is the entire solution, we are done Trace("sygus-sui-enum") << " ...success, full solution added to PBE pool : " diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 083f8df75..b5bccae23 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1656,6 +1656,7 @@ set(regress_1_tests regress1/sygus/sygus-uf-ex.sy regress1/sygus/t8.sy regress1/sygus/temp_input_to_synth_ic-error-121418.sy + regress1/sygus/tester.sy regress1/sygus/tl-type-0.sy regress1/sygus/tl-type-4x.sy regress1/sygus/tl-type.sy diff --git a/test/regress/regress1/sygus/tester.sy b/test/regress/regress1/sygus/tester.sy new file mode 100644 index 000000000..261666dd4 --- /dev/null +++ b/test/regress/regress1/sygus/tester.sy @@ -0,0 +1,37 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + +(set-logic SLIA) +(declare-datatype DT ((A (a Int)) (B (b String)) (JSBool (jsBool Bool)))) + +(define-fun isA ((i DT)) Bool ((_ is A) i) ) +(define-fun isB ((i DT)) Bool ((_ is B) i) ) + +(synth-fun add ((x1 DT)) DT + ( + (Start DT (ntDT)) + (ntDT DT + ( x1 x2 + (JSBool ntBool) + (A ntInt) + (ite ntBool ntDT ntDT) + ) + ) + (ntBool Bool + ( + (isA ntDT) + (isB ntDT) + (jsBool ntDT) + ) + ) + (ntInt Int + (1 + (a ntDT) + (+ ntInt ntInt) + ) + ) + ) +) +(constraint (= (add (A 6)) (A 7))) +(constraint (= (add (B "j")) (B "j"))) +(check-synth) -- cgit v1.2.3 From c59aefd26d391cb01f0e27b050e553afe49a69d8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 29 Mar 2019 08:38:30 -0500 Subject: Apply empty splits more aggressively in sets+cardinality (#2907) --- src/theory/sets/theory_sets_private.cpp | 7 ++++++- test/regress/CMakeLists.txt | 1 + test/regress/regress1/sets/issue2904.smt2 | 27 +++++++++++++++++++++++++++ 3 files changed, 34 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress1/sets/issue2904.smt2 (limited to 'test/regress/CMakeLists.txt') diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index f77d89254..aaa66046e 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1380,8 +1380,8 @@ void TheorySetsPrivate::checkNormalForm( Node eqc, std::vector< Node >& intro_se Assert( d_nf.find( eqc )==d_nf.end() ); bool success = true; + Node emp_set = getEmptySet(tn); if( !base.isNull() ){ - Node emp_set = getEmptySet( tn ); for( unsigned j=0; j c; @@ -1494,6 +1494,11 @@ void TheorySetsPrivate::checkNormalForm( Node eqc, std::vector< Node >& intro_se Assert( false ); } }else{ + // must ensure disequal from empty + if (!eqc.isConst() && !ee_areDisequal(eqc, emp_set)) + { + split(eqc.eqNode(emp_set)); + } //normal form is this equivalence class d_nf[eqc].push_back( eqc ); Trace("sets-nf") << "----> N " << eqc << " => { " << eqc << " }" << std::endl; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b5bccae23..55c777f80 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1494,6 +1494,7 @@ set(regress_1_tests regress1/sets/fuzz31811.smt2 regress1/sets/insert_invariant_37_2.smt2 regress1/sets/issue2568.smt2 + regress1/sets/issue2904.smt2 regress1/sets/lemmabug-ListElts317minimized.smt2 regress1/sets/remove_check_free_31_6.smt2 regress1/sets/sets-disequal.smt2 diff --git a/test/regress/regress1/sets/issue2904.smt2 b/test/regress/regress1/sets/issue2904.smt2 new file mode 100644 index 000000000..13ca789f6 --- /dev/null +++ b/test/regress/regress1/sets/issue2904.smt2 @@ -0,0 +1,27 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +; conjecture set nonempty(~b & ~c) + +(declare-fun n () Int) +(declare-fun f () Int) +(declare-fun m () Int) + +(declare-fun b () (Set Int)) +(declare-fun c () (Set Int)) +(declare-fun UNIVERALSET () (Set Int)) +(assert (subset b UNIVERALSET)) +(assert (subset c UNIVERALSET)) + +(assert (> n 0)) +(assert (= (card UNIVERALSET) n)) +(assert (= (card b) m)) +(assert (= (card c) (- f m))) +(assert (>= m 0)) +(assert (>= f m)) +(assert (> n (+ (* 2 f) m))) + + +(assert (>= (card (setminus UNIVERALSET (intersection (setminus UNIVERALSET b) (setminus UNIVERALSET c)))) n)) + +(check-sat) -- cgit v1.2.3 From fe18be6fe6ac58bf6ccdb1ca18c7fae2de881aaa Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 1 Apr 2019 10:45:40 -0700 Subject: Move slow string regression to regress3 (#2913) --- test/regress/CMakeLists.txt | 2 +- test/regress/regress2/strings/extf_d_perf.smt2 | 19 ------------------- test/regress/regress3/strings/extf_d_perf.smt2 | 19 +++++++++++++++++++ 3 files changed, 20 insertions(+), 20 deletions(-) delete mode 100644 test/regress/regress2/strings/extf_d_perf.smt2 create mode 100644 test/regress/regress3/strings/extf_d_perf.smt2 (limited to 'test/regress/CMakeLists.txt') diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 55c777f80..c6ccab464 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1749,7 +1749,6 @@ set(regress_2_tests regress2/strings/cmu-disagree-0707-dd.smt2 regress2/strings/cmu-prereg-fmf.smt2 regress2/strings/cmu-repl-len-nterm.smt2 - regress2/strings/extf_d_perf.smt2 regress2/strings/issue918.smt2 regress2/strings/non_termination_regular_expression6.smt2 regress2/strings/norn-dis-0707-3.smt2 @@ -1798,6 +1797,7 @@ set(regress_3_tests regress3/pp-regfile.smt regress3/qwh.35.405.shuffled-as.sat03-1651.smt regress3/sixfuncs.sy + regress3/strings/extf_d_perf.smt2 ) #-----------------------------------------------------------------------------# diff --git a/test/regress/regress2/strings/extf_d_perf.smt2 b/test/regress/regress2/strings/extf_d_perf.smt2 deleted file mode 100644 index 7ad094dcb..000000000 --- a/test/regress/regress2/strings/extf_d_perf.smt2 +++ /dev/null @@ -1,19 +0,0 @@ -; COMMAND-LINE: --strings-exp --strings-fmf -; EXPECT: sat -(set-logic ALL) -(declare-fun _substvar_140_ () String) -(declare-fun _substvar_195_ () Int) -(declare-fun _substvar_201_ () Int) -(assert (let ((_let_0 (str.substr _substvar_140_ 10 (+ 0 (str.len _substvar_140_))))) (let ((_let_3 (str.substr _let_0 0 (str.indexof _let_0 "/" 0)))) (let ((_let_4 (str.substr _let_3 0 7))) (let ((_let_5 (str.substr _let_3 8 (+ _substvar_201_ (str.len _let_3))))) - (and - (str.contains _substvar_140_ "://") - (str.contains _let_3 "@") - (str.contains _let_5 ",") - (not (= (str.len (str.substr _let_0 (+ 1 (str.indexof _let_0 "/" 0)) _substvar_195_)) 0)) - (not (= (str.len _let_4) 0)) - (not (str.contains _let_0 ".sock")) - (not (str.contains _let_4 "@")) - (not (= (str.len _let_5) 0)) - (= "mongodb://" (str.substr _substvar_140_ 0 10)))))))) -(check-sat) - diff --git a/test/regress/regress3/strings/extf_d_perf.smt2 b/test/regress/regress3/strings/extf_d_perf.smt2 new file mode 100644 index 000000000..7ad094dcb --- /dev/null +++ b/test/regress/regress3/strings/extf_d_perf.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: --strings-exp --strings-fmf +; EXPECT: sat +(set-logic ALL) +(declare-fun _substvar_140_ () String) +(declare-fun _substvar_195_ () Int) +(declare-fun _substvar_201_ () Int) +(assert (let ((_let_0 (str.substr _substvar_140_ 10 (+ 0 (str.len _substvar_140_))))) (let ((_let_3 (str.substr _let_0 0 (str.indexof _let_0 "/" 0)))) (let ((_let_4 (str.substr _let_3 0 7))) (let ((_let_5 (str.substr _let_3 8 (+ _substvar_201_ (str.len _let_3))))) + (and + (str.contains _substvar_140_ "://") + (str.contains _let_3 "@") + (str.contains _let_5 ",") + (not (= (str.len (str.substr _let_0 (+ 1 (str.indexof _let_0 "/" 0)) _substvar_195_)) 0)) + (not (= (str.len _let_4) 0)) + (not (str.contains _let_0 ".sock")) + (not (str.contains _let_4 "@")) + (not (= (str.len _let_5) 0)) + (= "mongodb://" (str.substr _substvar_140_ 0 10)))))))) +(check-sat) + -- cgit v1.2.3 From 8a9ffdbb248ddcc6a41f628f6dcbc070b57e6a28 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 1 Apr 2019 15:07:05 -0700 Subject: FP: Fix wrong model due to partial assignment (#2910) For a simple query `(not (= (fp.isSubnormal x) false))`, we were getting a wrong model. The issue was that `(sign x)` was not assigned a value and did not appear in the shared terms. In `TheoryFp::collectModelInfo()`, however, we generate an expression that connects the components of `x` to `x`, which contains `(sign x)`. As a result, the normalization while building a model did not result in a constant. This commit fixes the issue by marking `(sign x)` (and `(significand x)`) as assignable. Assignable terms can take any value while building a model if there is no existing value. --- src/theory/fp/theory_fp.cpp | 35 +++++++++++++++++++++++++++++++ src/theory/theory_model_builder.cpp | 8 +++++++ test/regress/CMakeLists.txt | 1 + test/regress/regress0/fp/wrong-model.smt2 | 11 ++++++++++ 4 files changed, 55 insertions(+) create mode 100644 test/regress/regress0/fp/wrong-model.smt2 (limited to 'test/regress/CMakeLists.txt') diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 627b87ba7..4652f62d1 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -1084,6 +1084,41 @@ bool TheoryFp::collectModelInfo(TheoryModel *m) { return false; } + + if (Configuration::isAssertionBuild() && isLeaf(node) && !node.isConst() + && node.getType().isFloatingPoint()) + { + // Check that the equality engine has asssigned values to all the + // components of `node` except `(sign node)` (the sign component is + // assignable, meaning that the model builder can pick an arbitrary value + // for it if it hasn't been assigned in the equality engine). + NodeManager* nm = NodeManager::currentNM(); + Node compNaN = nm->mkNode(kind::FLOATINGPOINT_COMPONENT_NAN, node); + Node compInf = nm->mkNode(kind::FLOATINGPOINT_COMPONENT_INF, node); + Node compZero = nm->mkNode(kind::FLOATINGPOINT_COMPONENT_ZERO, node); + Node compExponent = + nm->mkNode(kind::FLOATINGPOINT_COMPONENT_EXPONENT, node); + Node compSignificand = + nm->mkNode(kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND, node); + + eq::EqualityEngine* ee = m->getEqualityEngine(); + Assert(ee->hasTerm(compNaN) && ee->getRepresentative(compNaN).isConst()); + Assert(ee->hasTerm(compInf) && ee->getRepresentative(compInf).isConst()); + Assert(ee->hasTerm(compZero) + && ee->getRepresentative(compZero).isConst()); + Assert(ee->hasTerm(compExponent) + && ee->getRepresentative(compExponent).isConst()); + Assert(ee->hasTerm(compSignificand)); + Assert(ee->getRepresentative(compSignificand).isConst()); + + // At most one of the flags (NaN, inf, zero) can be set + Node one = nm->mkConst(BitVector(1U, 1U)); + size_t numFlags = 0; + numFlags += ee->getRepresentative(compNaN) == one ? 1 : 0; + numFlags += ee->getRepresentative(compInf) == one ? 1 : 0; + numFlags += ee->getRepresentative(compZero) == one ? 1 : 0; + Assert(numFlags <= 1); + } } return true; diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 77cdfb79b..102979056 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -47,6 +47,14 @@ bool TheoryEngineModelBuilder::isAssignable(TNode n) return !n.getType().isFunction(); } } + else if (n.getKind() == kind::FLOATINGPOINT_COMPONENT_SIGN) + { + // Extracting the sign of a floating-point number acts similar to a + // selector on a datatype, i.e. if `(sign x)` wasn't assigned a value, we + // can pick an arbitrary one. Note that the other components of a + // floating-point number should always be assigned a value. + return true; + } else { // non-function variables, and fully applied functions diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index c6ccab464..13d1540f6 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -451,6 +451,7 @@ set(regress_0_tests regress0/fp/abs-unsound2.smt2 regress0/fp/ext-rew-test.smt2 regress0/fp/simple.smt2 + regress0/fp/wrong-model.smt2 regress0/fuzz_1.smt regress0/fuzz_3.smt regress0/get-value-incremental.smt2 diff --git a/test/regress/regress0/fp/wrong-model.smt2 b/test/regress/regress0/fp/wrong-model.smt2 new file mode 100644 index 000000000..4bb7645d5 --- /dev/null +++ b/test/regress/regress0/fp/wrong-model.smt2 @@ -0,0 +1,11 @@ +; REQUIRES: symfpu +; EXPECT: sat + +; NOTE: the (set-logic ALL) is on purpose because the problem was not triggered +; with QF_FP. +(set-logic ALL) +(declare-const r RoundingMode) +(declare-const x (_ FloatingPoint 5 11)) +(declare-const y (_ FloatingPoint 5 11)) +(assert (not (= (fp.isSubnormal x) false))) +(check-sat) -- cgit v1.2.3 From e1f463c0884dccf8fe513bd59bfd7ba6a8592183 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 3 Apr 2019 15:53:52 -0500 Subject: Fix combination of datatypes + strings in PBE (#2930) --- src/theory/quantifiers/sygus/sygus_unif_io.cpp | 47 ++++++++++++++++---------- test/regress/CMakeLists.txt | 1 + test/regress/regress1/sygus/issue2914.sy | 26 ++++++++++++++ 3 files changed, 57 insertions(+), 17 deletions(-) create mode 100644 test/regress/regress1/sygus/issue2914.sy (limited to 'test/regress/CMakeLists.txt') diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 47fd41300..7d51ec43a 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -161,7 +161,12 @@ bool UnifContextIo::getStringIncrement(SygusUnifIo* sui, if (d_vals[j] == sui->d_true) { // example is active in this context - Assert(vals[j].isConst()); + if (!vals[j].isConst()) + { + // the value is unknown, thus we cannot use it to increment the strings + // position + return false; + } String mystr = vals[j].getConst(); ival = mystr.size(); if (mystr.size() <= ex_vals[j].size()) @@ -199,7 +204,11 @@ bool UnifContextIo::isStringSolved(SygusUnifIo* sui, if (d_vals[j] == sui->d_true) { // example is active in this context - Assert(vals[j].isConst()); + if (!vals[j].isConst()) + { + // value is unknown, thus it does not solve + return false; + } String mystr = vals[j].getConst(); if (ex_vals[j] != mystr) { @@ -949,23 +958,27 @@ bool SygusUnifIo::getExplanationForEnumeratorExclude( std::vector cmp_indices; for (unsigned i = 0, size = results.size(); i < size; i++) { - Assert(results[i].isConst()); - Assert(d_examples_out[i].isConst()); - Trace("sygus-sui-cterm-debug") - << " " << results[i] << " <> " << d_examples_out[i]; - Node cont = nm->mkNode(STRING_STRCTN, d_examples_out[i], results[i]); - Node contr = Rewriter::rewrite(cont); - if (contr == d_false) + // If the result is not constant, then it is worthless. It does not + // impact whether the term is excluded. + if (results[i].isConst()) { - cmp_indices.push_back(i); - Trace("sygus-sui-cterm-debug") << "...not contained." << std::endl; - } - else - { - Trace("sygus-sui-cterm-debug") << "...contained." << std::endl; - if (isConditional) + Assert(d_examples_out[i].isConst()); + Trace("sygus-sui-cterm-debug") + << " " << results[i] << " <> " << d_examples_out[i]; + Node cont = nm->mkNode(STRING_STRCTN, d_examples_out[i], results[i]); + Node contr = Rewriter::rewrite(cont); + if (contr == d_false) { - return false; + cmp_indices.push_back(i); + Trace("sygus-sui-cterm-debug") << "...not contained." << std::endl; + } + else + { + Trace("sygus-sui-cterm-debug") << "...contained." << std::endl; + if (isConditional) + { + return false; + } } } } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 13d1540f6..a9b807e82 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1624,6 +1624,7 @@ set(regress_1_tests regress1/sygus/inv-example.sy regress1/sygus/inv-missed-sol-true.sy regress1/sygus/inv-unused.sy + regress1/sygus/issue2914.sy regress1/sygus/large-const-simp.sy regress1/sygus/let-bug-simp.sy regress1/sygus/list-head-x.sy diff --git a/test/regress/regress1/sygus/issue2914.sy b/test/regress/regress1/sygus/issue2914.sy new file mode 100644 index 000000000..0f125a870 --- /dev/null +++ b/test/regress/regress1/sygus/issue2914.sy @@ -0,0 +1,26 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic SLIA) +(declare-datatype JSIdentifier ((JSString (jsString String)) (Error ))) + +(synth-fun substring ((x1 String) (x3 Int))String + ((Start String (ntString)) + (ntInt Int + (0 x3) + ) + (ntJSIdentifier JSIdentifier + ( + Error + ) + ) + (ntString String + (x1 + (str.substr ntString ntInt ntInt) + (jsString ntJSIdentifier) + (str.++ ntString ntString) + ) + ) + ) +) +(constraint (= (substring "ey" 1) "e")) +(check-synth) -- cgit v1.2.3 From 880f0b719479ff9f9b415749b2ccf9016274a99d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 5 Apr 2019 15:31:20 -0500 Subject: Fix another corner case of datatypes+PBE (#2938) --- src/theory/quantifiers/sygus/sygus_unif_io.cpp | 31 +++++++++++----------- src/theory/quantifiers/sygus/sygus_unif_io.h | 19 +++++++++++++- test/regress/CMakeLists.txt | 1 + test/regress/regress1/sygus/issue2935.sy | 36 ++++++++++++++++++++++++++ 4 files changed, 71 insertions(+), 16 deletions(-) create mode 100644 test/regress/regress1/sygus/issue2935.sy (limited to 'test/regress/CMakeLists.txt') diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 7d51ec43a..207aa4c8e 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -458,25 +458,26 @@ void SubsumeTrie::getLeavesInternal(const std::vector& vals, { int new_status = status; bool success = true; - // if the current value is true, we must consider the value of this child + // If the current value is true, then this is a relevant point. + // We must consider the value of this child. if (curr_val_true) { - if (status != 0) + if (it->first.isNull()) { - if (it->first.isNull()) - { - // The value of this child is unknown on this point, hence we - // ignore it. - success = false; - } - else + // The value of this child is unknown on this point, hence we + // do not recurse + success = false; + } + else if (status != 0) + { + // if the status is not zero (indicating that we have a mix of T/F), + // then we must compute the new status. + Assert(it->first.getType().isBoolean()); + Assert(it->first.isConst()); + new_status = (it->first.getConst() ? 1 : -1); + if (status != -2 && new_status != status) { - Assert(it->first.getType().isBoolean()); - new_status = (it->first.getConst() ? 1 : -1); - if (status != -2 && new_status != status) - { - new_status = 0; - } + new_status = 0; } } } diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index 5d38ba827..fced29871 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -218,7 +218,24 @@ class SubsumeTrie int status, bool checkExistsOnly, bool checkSubsume); - /** helper function for above functions */ + /** helper function for above functions + * + * This adds to v[-1], v[0], v[1] the children of the trie that occur + * along paths that contain only false (v[-1]), a mix of true/false (v[0]), + * and only true (v[1]) values for respectively for relevant points. + * + * vals/pol is used to determine the relevant points, which impacts which + * paths of the trie to traverse on this call. + * In particular, all points such that (pol ? vals[index] : !vals[index]) + * are relevant. + * + * Paths that contain an unknown value for any relevant point are not + * traversed. In the larger picture, this ensures that terms are not used in a + * way such that their unknown value is relevant to the overall behavior of + * a synthesis solution. + * + * status holds the current value of v (0,1,-1) that we will be adding to. + */ void getLeavesInternal(const std::vector& vals, bool pol, std::map>& v, diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a9b807e82..64da9ec61 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1625,6 +1625,7 @@ set(regress_1_tests regress1/sygus/inv-missed-sol-true.sy regress1/sygus/inv-unused.sy regress1/sygus/issue2914.sy + regress1/sygus/issue2935.sy regress1/sygus/large-const-simp.sy regress1/sygus/let-bug-simp.sy regress1/sygus/list-head-x.sy diff --git a/test/regress/regress1/sygus/issue2935.sy b/test/regress/regress1/sygus/issue2935.sy new file mode 100644 index 000000000..5616d19f5 --- /dev/null +++ b/test/regress/regress1/sygus/issue2935.sy @@ -0,0 +1,36 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic SLIA) +(declare-datatype JSIdentifier ((JSInt (jsInt Int)) (JSString (jsString String)) )) + +(synth-fun f ((x1_ JSIdentifier)(x2_ String)) JSIdentifier + ((Start JSIdentifier (ntJSIdentifier)) + (ntInt Int + (1 + (+ ntInt ntInt) + (jsInt ntJSIdentifier) + ) + ) + (ntString String + (x2_ + (str.substr ntString ntInt ntInt) + (jsString ntJSIdentifier) + ) + ) + (ntBool Bool + ( + (= ntString ntString) + ) + ) + (ntJSIdentifier JSIdentifier + ( x1_ + (ite ntBool ntJSIdentifier ntJSIdentifier) + (JSString ntString) + ) + ) + ) +) +(constraint (= (f (JSString "") "") (JSString ""))) +(constraint (= (f (JSString "M") "W") (JSString "M"))) +(constraint (= (f (JSString "Moon") "") (JSString "on"))) +(check-synth) -- cgit v1.2.3 From 7d27cae34c7c3cda9a7827754fb5b8e485d515db Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 11 Apr 2019 13:06:08 -0500 Subject: Eliminate Boolean ITE within terms, fixes 2947 (#2949) --- src/smt/term_formula_removal.cpp | 18 ++++++++++++------ test/regress/CMakeLists.txt | 1 + test/regress/regress0/uf/issue2947.smt2 | 11 +++++++++++ 3 files changed, 24 insertions(+), 6 deletions(-) create mode 100644 test/regress/regress0/uf/issue2947.smt2 (limited to 'test/regress/CMakeLists.txt') diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index ff17c5622..f610cc7df 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -84,9 +84,13 @@ Node RemoveTermFormulas::run(TNode node, std::vector& output, TypeNode nodeType = node.getType(); Node skolem; Node newAssertion; - if(node.getKind() == kind::ITE) { - // If an ITE, replace it - if (!nodeType.isBoolean() && (!inQuant || !expr::hasBoundVar(node))) + // Handle non-Boolean ITEs here. Boolean ones (within terms) are handled + // in the "non-variable Boolean term within term" case below. + if (node.getKind() == kind::ITE && !nodeType.isBoolean()) + { + // Here, we eliminate the ITE if we are not Boolean and if we do not contain + // a bound variable. + if (!inQuant || !expr::hasBoundVar(node)) { skolem = getSkolemForNode(node); if (skolem.isNull()) @@ -163,13 +167,15 @@ Node RemoveTermFormulas::run(TNode node, std::vector& output, && inTerm && !inQuant) { - // if a non-variable Boolean term, replace it + // if a non-variable Boolean term within another term, replace it skolem = getSkolemForNode(node); if (skolem.isNull()) { // Make the skolem to represent the Boolean term - // skolem = nodeManager->mkSkolem("termBT", nodeType, "a variable - // introduced due to Boolean term removal"); + // Skolems introduced for Boolean formulas appearing in terms have a + // special kind (BOOLEAN_TERM_VARIABLE) that ensures they are handled + // properly in theory combination. We must use this kind here instead of a + // generic skolem. skolem = nodeManager->mkBooleanTermVariable(); d_skolem_cache.insert(node, skolem); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 64da9ec61..687dfc6f2 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -933,6 +933,7 @@ set(regress_0_tests regress0/uf/euf_simp12.smt regress0/uf/euf_simp13.smt regress0/uf/iso_brn001.smt + regress0/uf/issue2947.smt2 regress0/uf/pred.smt regress0/uf/simple.01.cvc regress0/uf/simple.02.cvc diff --git a/test/regress/regress0/uf/issue2947.smt2 b/test/regress/regress0/uf/issue2947.smt2 new file mode 100644 index 000000000..6bb60b9d7 --- /dev/null +++ b/test/regress/regress0/uf/issue2947.smt2 @@ -0,0 +1,11 @@ +(set-logic QF_UF) +(set-info :status unsat) +(declare-fun f (Bool) Bool) +(assert + (not (f true)) +) +(assert + (f (ite (f true) true (f false))) +) +(check-sat) +(exit) -- cgit v1.2.3 From a47b722aa31cdd036f83425b2a805e6a572a974b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 16 Apr 2019 11:53:45 -0500 Subject: Stratify enumerative instantiation (#2954) --- src/options/quantifiers_options.toml | 9 + .../quantifiers/inst_strategy_enumerative.cpp | 371 +++++++++++---------- src/theory/quantifiers/inst_strategy_enumerative.h | 6 +- test/regress/CMakeLists.txt | 1 + test/regress/regress2/quantifiers/syn874-1.smt2 | 129 +++++++ 5 files changed, 340 insertions(+), 176 deletions(-) create mode 100644 test/regress/regress2/quantifiers/syn874-1.smt2 (limited to 'test/regress/CMakeLists.txt') diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 1c13590eb..0a69178b3 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -455,6 +455,15 @@ header = "options/quantifiers_options.h" read_only = true help = "interleave full saturate instantiation with other techniques" +[[option]] + name = "fullSaturateStratify" + category = "regular" + long = "fs-stratify" + type = "bool" + default = "false" + read_only = true + help = "stratify effort levels in enumerative instantiation, which favors speed over fairness" + [[option]] name = "literalMatchMode" category = "regular" diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index 715274982..7a2f62864 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -70,46 +70,89 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) doCheck = quant_e == QEFFORT_LAST_CALL; fullEffort = !d_quantEngine->hasAddedLemma(); } - if (doCheck) + if (!doCheck) { - double clSet = 0; - if (Trace.isOn("fs-engine")) - { - clSet = double(clock()) / double(CLOCKS_PER_SEC); - Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---" - << std::endl; - } - int addedLemmas = 0; - for (unsigned i = 0; - i < d_quantEngine->getModel()->getNumAssertedQuantifiers(); - i++) + return; + } + double clSet = 0; + if (Trace.isOn("fs-engine")) + { + clSet = double(clock()) / double(CLOCKS_PER_SEC); + Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---" + << std::endl; + } + unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1; + unsigned rend = fullEffort ? 1 : rstart; + unsigned addedLemmas = 0; + // First try in relevant domain of all quantified formulas, if no + // instantiations exist, try arbitrary ground terms. + // Notice that this stratification of effort levels makes it so that some + // quantified formulas may not be instantiated (if they have no instances + // at effort level r=0 but another quantified formula does). We prefer + // this stratification since effort level r=1 may be highly expensive in the + // case where we have a quantified formula with many entailed instances. + FirstOrderModel* fm = d_quantEngine->getModel(); + RelevantDomain* rd = d_quantEngine->getRelevantDomain(); + unsigned nquant = fm->getNumAssertedQuantifiers(); + std::map alreadyProc; + for (unsigned r = rstart; r <= rend; r++) + { + if (rd || r > 0) { - Node q = d_quantEngine->getModel()->getAssertedQuantifier(i, true); - if (d_quantEngine->hasOwnership(q, this) - && d_quantEngine->getModel()->isQuantifierActive(q)) + if (r == 0) + { + Trace("inst-alg") << "-> Relevant domain instantiate..." << std::endl; + Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl; + rd->compute(); + Trace("inst-alg-debug") << "...finished" << std::endl; + } + else + { + Trace("inst-alg") << "-> Ground term instantiate..." << std::endl; + } + for (unsigned i = 0; i < nquant; i++) { - if (process(q, fullEffort)) + Node q = fm->getAssertedQuantifier(i, true); + bool doProcess = d_quantEngine->hasOwnership(q, this) + && fm->isQuantifierActive(q) + && alreadyProc.find(q) == alreadyProc.end(); + if (doProcess) { - // added lemma - addedLemmas++; - if (d_quantEngine->inConflict()) + if (process(q, fullEffort, r == 0)) { - break; + // don't need to mark this if we are not stratifying + if (!options::fullSaturateStratify()) + { + alreadyProc[q] = true; + } + // added lemma + addedLemmas++; + if (d_quantEngine->inConflict()) + { + break; + } } } } + if (d_quantEngine->inConflict() + || (addedLemmas > 0 && options::fullSaturateStratify())) + { + // we break if we are in conflict, or if we added any lemma at this + // effort level and we stratify effort levels. + break; + } } - if (Trace.isOn("fs-engine")) - { - Trace("fs-engine") << "Added lemmas = " << addedLemmas << std::endl; - double clSet2 = double(clock()) / double(CLOCKS_PER_SEC); - Trace("fs-engine") << "Finished full saturation engine, time = " - << (clSet2 - clSet) << std::endl; - } + } + if (Trace.isOn("fs-engine")) + { + Trace("fs-engine") << "Added lemmas = " << addedLemmas << std::endl; + double clSet2 = double(clock()) / double(CLOCKS_PER_SEC); + Trace("fs-engine") << "Finished full saturation engine, time = " + << (clSet2 - clSet) << std::endl; } } -bool InstStrategyEnum::process(Node f, bool fullEffort) +bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd) { // ignore if constant true (rare case of non-standard quantifier whose body is // rewritten to true) @@ -117,178 +160,156 @@ bool InstStrategyEnum::process(Node f, bool fullEffort) { return false; } - // first, try from relevant domain RelevantDomain* rd = d_quantEngine->getRelevantDomain(); - unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1; - unsigned rend = fullEffort ? 1 : rstart; - for (unsigned r = rstart; r <= rend; r++) + unsigned final_max_i = 0; + std::vector maxs; + std::vector max_zero; + bool has_zero = false; + std::map > term_db_list; + std::vector ftypes; + TermDb* tdb = d_quantEngine->getTermDatabase(); + EqualityQuery* qy = d_quantEngine->getEqualityQuery(); + // iterate over substitutions for variables + for (unsigned i = 0; i < f[0].getNumChildren(); i++) { - if (rd || r > 0) + TypeNode tn = f[0][i].getType(); + ftypes.push_back(tn); + unsigned ts; + if (isRd) { - if (r == 0) + ts = rd->getRDomain(f, i)->d_terms.size(); + } + else + { + ts = tdb->getNumTypeGroundTerms(tn); + std::map >::iterator ittd = + term_db_list.find(tn); + if (ittd == term_db_list.end()) { - Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." - << std::endl; - Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl; - rd->compute(); - Trace("inst-alg-debug") << "...finished" << std::endl; + std::map reps_found; + for (unsigned j = 0; j < ts; j++) + { + Node gt = tdb->getTypeGroundTerm(ftypes[i], j); + if (!options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(gt)) + { + Node rep = qy->getRepresentative(gt); + if (reps_found.find(rep) == reps_found.end()) + { + reps_found[rep] = gt; + term_db_list[tn].push_back(gt); + } + } + } + ts = term_db_list[tn].size(); } else { - Trace("inst-alg") << "-> Ground term instantiate " << f << "..." - << std::endl; + ts = ittd->second.size(); } - unsigned final_max_i = 0; - std::vector maxs; - std::vector max_zero; - bool has_zero = false; - std::map > term_db_list; - std::vector ftypes; - // iterate over substitutions for variables - for (unsigned i = 0; i < f[0].getNumChildren(); i++) + } + // consider a default value if at full effort + max_zero.push_back(fullEffort && ts == 0); + ts = (fullEffort && ts == 0) ? 1 : ts; + Trace("inst-alg-rd") << "Variable " << i << " has " << ts + << " in relevant domain." << std::endl; + if (ts == 0) + { + has_zero = true; + break; + } + maxs.push_back(ts); + if (ts > final_max_i) + { + final_max_i = ts; + } + } + if (!has_zero) + { + Trace("inst-alg-rd") << "Will do " << final_max_i + << " stages of instantiation." << std::endl; + unsigned max_i = 0; + bool success; + Instantiate* ie = d_quantEngine->getInstantiate(); + while (max_i <= final_max_i) + { + Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl; + std::vector childIndex; + int index = 0; + do { - TypeNode tn = f[0][i].getType(); - ftypes.push_back(tn); - unsigned ts; - if (r == 0) - { - ts = rd->getRDomain(f, i)->d_terms.size(); - } - else + while (index >= 0 && index < (int)f[0].getNumChildren()) { - ts = d_quantEngine->getTermDatabase()->getNumTypeGroundTerms(tn); - std::map >::iterator ittd = - term_db_list.find(tn); - if (ittd == term_db_list.end()) + if (index == static_cast(childIndex.size())) { - std::map reps_found; - for (unsigned j = 0; j < ts; j++) - { - Node gt = d_quantEngine->getTermDatabase()->getTypeGroundTerm( - ftypes[i], j); - if (!options::cbqi() - || !quantifiers::TermUtil::hasInstConstAttr(gt)) - { - Node rep = - d_quantEngine->getEqualityQuery()->getRepresentative(gt); - if (reps_found.find(rep) == reps_found.end()) - { - reps_found[rep] = gt; - term_db_list[tn].push_back(gt); - } - } - } - ts = term_db_list[tn].size(); + childIndex.push_back(-1); } else { - ts = ittd->second.size(); + Assert(index == static_cast(childIndex.size()) - 1); + unsigned nv = childIndex[index] + 1; + if (nv < maxs[index] && nv <= max_i) + { + childIndex[index] = nv; + index++; + } + else + { + childIndex.pop_back(); + index--; + } } } - // consider a default value if at full effort - max_zero.push_back(fullEffort && ts == 0); - ts = (fullEffort && ts == 0) ? 1 : ts; - Trace("inst-alg-rd") << "Variable " << i << " has " << ts - << " in relevant domain." << std::endl; - if (ts == 0) + success = index >= 0; + if (success) { - has_zero = true; - break; - } - else - { - maxs.push_back(ts); - if (ts > final_max_i) + if (Trace.isOn("inst-alg-rd")) { - final_max_i = ts; + Trace("inst-alg-rd") << "Try instantiation { "; + for (unsigned i : childIndex) + { + Trace("inst-alg-rd") << i << " "; + } + Trace("inst-alg-rd") << "}" << std::endl; } - } - } - if (!has_zero) - { - Trace("inst-alg-rd") << "Will do " << final_max_i - << " stages of instantiation." << std::endl; - unsigned max_i = 0; - bool success; - while (max_i <= final_max_i) - { - Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl; - std::vector childIndex; - int index = 0; - do + // try instantiation + std::vector terms; + for (unsigned i = 0, nchild = f[0].getNumChildren(); i < nchild; i++) { - while (index >= 0 && index < (int)f[0].getNumChildren()) + if (max_zero[i]) { - if (index == (int)childIndex.size()) - { - childIndex.push_back(-1); - } - else - { - Assert(index == (int)(childIndex.size()) - 1); - unsigned nv = childIndex[index] + 1; - if (nv < maxs[index] && nv <= max_i) - { - childIndex[index] = nv; - index++; - } - else - { - childIndex.pop_back(); - index--; - } - } + // no terms available, will report incomplete instantiation + terms.push_back(Node::null()); + Trace("inst-alg-rd") << " null" << std::endl; } - success = index >= 0; - if (success) + else if (isRd) { - Trace("inst-alg-rd") << "Try instantiation { "; - for (unsigned j = 0; j < childIndex.size(); j++) - { - Trace("inst-alg-rd") << childIndex[j] << " "; - } - Trace("inst-alg-rd") << "}" << std::endl; - // try instantiation - std::vector terms; - for (unsigned i = 0; i < f[0].getNumChildren(); i++) - { - if (max_zero[i]) - { - // no terms available, will report incomplete instantiation - terms.push_back(Node::null()); - Trace("inst-alg-rd") << " null" << std::endl; - } - else if (r == 0) - { - terms.push_back(rd->getRDomain(f, i)->d_terms[childIndex[i]]); - Trace("inst-alg-rd") - << " " << rd->getRDomain(f, i)->d_terms[childIndex[i]] - << std::endl; - } - else - { - Assert(childIndex[i] < term_db_list[ftypes[i]].size()); - terms.push_back(term_db_list[ftypes[i]][childIndex[i]]); - Trace("inst-alg-rd") << " " - << term_db_list[ftypes[i]][childIndex[i]] - << std::endl; - } - } - if (d_quantEngine->getInstantiate()->addInstantiation(f, terms)) - { - Trace("inst-alg-rd") << "Success!" << std::endl; - ++(d_quantEngine->d_statistics.d_instantiations_guess); - return true; - } - else - { - index--; - } + terms.push_back(rd->getRDomain(f, i)->d_terms[childIndex[i]]); + Trace("inst-alg-rd") + << " " << rd->getRDomain(f, i)->d_terms[childIndex[i]] + << std::endl; } - } while (success); - max_i++; + else + { + Assert(childIndex[i] < term_db_list[ftypes[i]].size()); + terms.push_back(term_db_list[ftypes[i]][childIndex[i]]); + Trace("inst-alg-rd") + << " " << term_db_list[ftypes[i]][childIndex[i]] + << std::endl; + } + } + if (ie->addInstantiation(f, terms)) + { + Trace("inst-alg-rd") << "Success!" << std::endl; + ++(d_quantEngine->d_statistics.d_instantiations_guess); + return true; + } + else + { + index--; + } } - } + } while (success); + max_i++; } } // TODO : term enumerator instantiation? diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index 6b2794fd5..f011efdfc 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -92,8 +92,12 @@ class InstStrategyEnum : public QuantifiersModule * well-typed term *not* occurring in the current context. * This handles corner cases where there are no well-typed * ground terms in the current context to instantiate with. + * + * The flag isRd indicates whether we are trying relevant domain + * instantiations. If this flag is false, we are trying arbitrary ground + * term instantiations. */ - bool process(Node q, bool fullEffort); + bool process(Node q, bool fullEffort, bool isRd); }; /* class InstStrategyEnum */ } /* CVC4::theory::quantifiers namespace */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 687dfc6f2..2c6acf69c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1748,6 +1748,7 @@ set(regress_2_tests regress2/quantifiers/mutualrec2.cvc regress2/quantifiers/net-policy-no-time.smt2 regress2/quantifiers/nunchaku2309663.nun.min.smt2 + regress2/quantifiers/syn874-1.smt2 regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2 regress2/strings/cmu-dis-0707-3.smt2 regress2/strings/cmu-disagree-0707-dd.smt2 diff --git a/test/regress/regress2/quantifiers/syn874-1.smt2 b/test/regress/regress2/quantifiers/syn874-1.smt2 new file mode 100644 index 000000000..93de3aca6 --- /dev/null +++ b/test/regress/regress2/quantifiers/syn874-1.smt2 @@ -0,0 +1,129 @@ +; COMMAND-LINE: --full-saturate-quant --fs-stratify +; EXPECT: unsat +(set-logic ALL) +(declare-sort $$unsorted 0) +(declare-fun ssNder1_0 () Bool) +(declare-fun ssNder1_1r1 ($$unsorted) Bool) +(declare-fun ssNder1_2r1r1 ($$unsorted $$unsorted) Bool) +(declare-fun ssNder1_3r1r1r1 ($$unsorted $$unsorted $$unsorted) Bool) +(declare-fun ssNder1_4r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun skc30 () $$unsorted) +(declare-fun ssPv16_5r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun skc31 () $$unsorted) +(declare-fun ssNder1_5r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun skc28 () $$unsorted) +(declare-fun ssPv15_6r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun skc29 () $$unsorted) +(declare-fun ssNder1_6r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun skc26 () $$unsorted) +(declare-fun ssPv14_7r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun skc27 () $$unsorted) +(declare-fun ssNder1_7r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun skc24 () $$unsorted) +(declare-fun ssPv13_8r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun skc25 () $$unsorted) +(declare-fun ssNder1_8r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun ssNder1_9r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun ssNder1_10r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun skc22 () $$unsorted) +(declare-fun ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun skc23 () $$unsorted) +(declare-fun ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun skc20 () $$unsorted) +(declare-fun ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun skc21 () $$unsorted) +(declare-fun ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun skc18 () $$unsorted) +(declare-fun ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun skc19 () $$unsorted) +(declare-fun ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun ssPv20_1r1 ($$unsorted) Bool) +(declare-fun ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun skc16 () $$unsorted) +(declare-fun ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun skc17 () $$unsorted) +(declare-fun ssPv12_9r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun ssPv19_2r1r1 ($$unsorted $$unsorted) Bool) +(declare-fun ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun ssPv17_4r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun ssPv18_3r1r1r1 ($$unsorted $$unsorted $$unsorted) Bool) +(declare-fun ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun ssPv11_10r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(declare-fun ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool) +(meta-info :filename "SYN874-1") +(assert true) +(assert (forall ((U $$unsorted)) (ssNder1_1r1 U) )) +(assert (forall ((U $$unsorted) (V $$unsorted)) (or (not (ssNder1_1r1 U)) (ssNder1_2r1r1 U V)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted)) (or (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_3r1r1r1 U V W)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted)) (or (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_4r1r1r1r1 U V W X)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted)) (or (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv16_5r1r1r1r1r1 U V W X skc30)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted)) (or (not (ssPv16_5r1r1r1r1r1 U V W X skc31)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted)) (or (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_5r1r1r1r1r1 U V W X Y)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted)) (or (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv15_6r1r1r1r1r1r1 U V W X Y skc28)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted)) (or (not (ssPv15_6r1r1r1r1r1r1 U V W X Y skc29)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted)) (or (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted)) (or (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv14_7r1r1r1r1r1r1r1 U V W X Y Z skc26)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted)) (or (not (ssPv14_7r1r1r1r1r1r1r1 U V W X Y Z skc27)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted)) (or (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted)) (or (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 skc24)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted)) (or (not (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 skc25)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted)) (or (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted)) (or (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted)) (or (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted)) (or (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted)) (or (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted)) (or (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 skc22)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted)) (or (not (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 skc23)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted)) (or (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted)) (or (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 skc20)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted)) (or (not (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 skc21)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted)) (or (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted)) (or (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 skc18)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted)) (or (not (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 skc19)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted)) (or (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssPv15_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv20_1r1 U)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted)) (or (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted)) (or (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 skc16)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted)) (or (not (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 skc17)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted)) (or (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssPv12_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssPv20_1r1 U)) (not (ssNder1_1r1 U)) (ssPv16_5r1r1r1r1r1 U V W X Y)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted)) (or (not (ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted)) (or (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssPv19_2r1r1 U V)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted)) (or (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted)) (or (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssPv20_1r1 U)) (not (ssNder1_1r1 U)) (ssPv19_2r1r1 U V)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted)) (or (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssPv15_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssPv20_1r1 U)) (not (ssNder1_1r1 U)) (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10) (ssPv17_4r1r1r1r1 U V W X)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted)) (or (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssPv12_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9) (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted)) (or (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssPv12_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssPv14_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10) (ssPv20_1r1 U)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted)) (or (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssPv17_4r1r1r1r1 U V W X)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted)) (or (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssPv20_1r1 U)) (not (ssNder1_1r1 U)) (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9) (ssPv15_6r1r1r1r1r1r1 U V W X Y Z)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssPv19_2r1r1 U V)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10) (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11) (ssPv16_5r1r1r1r1r1 U V W X Y)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8) (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2) (ssPv18_3r1r1r1 U V W)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssPv18_3r1r1r1 U V W)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11) (ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9) (ssPv12_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted)) (or (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12) (ssPv15_6r1r1r1r1r1r1 U V W X Y Z) (ssPv16_5r1r1r1r1r1 U V W X Y)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted)) (or (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv15_6r1r1r1r1r1r1 U V W X Y Z) (ssPv17_4r1r1r1r1 U V W X)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssPv15_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssPv16_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssPv17_4r1r1r1r1 U V W X)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8) (ssPv15_6r1r1r1r1r1r1 U V W X Y Z) (ssPv20_1r1 U)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted)) (or (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssPv14_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13) (ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6) (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssPv20_1r1 U)) (not (ssNder1_1r1 U)) (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssPv18_3r1r1r1 U V W)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13) (ssPv14_7r1r1r1r1r1r1r1 U V W X Y Z X1)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13) (ssPv11_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4) (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssPv17_4r1r1r1r1 U V W X)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9) (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssPv15_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11) (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted) (X14 $$unsorted)) (or (not (ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) (not (ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14)) (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssPv12_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssPv14_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) )) +(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted) (X14 $$unsorted)) (or (not (ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) (not (ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14)) (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9) (ssPv19_2r1r1 U V)) )) +(assert true) +(check-sat) -- cgit v1.2.3 From 2f7131c81078a964a4043ef79186cdcf91951974 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 16 Apr 2019 12:11:37 -0700 Subject: Make bv{add,mul,and,or,xor,xnor} left-associative (#2955) The most recent version of SMT-LIB defines bv{add,mul,and,or,xor,xnor} [0, 1] as left-associative. CVC4 treats all but bvxnor as having variable arity anyway but the arity check was too strict when using `--strict-parsing`. This commit changes the strict parsing check. For bvxnor, it adds code to the parser that expands an application of bvxnor into multiple applications of a binary bvxnor if needed. References: [0] http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml (bvand, bvor, bvadd, bvmul) [1] http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV (bvxor, bvxnor) --- src/parser/smt2/Smt2.g | 3 ++- src/parser/smt2/smt2.h | 20 +++++++++++++++----- test/regress/CMakeLists.txt | 1 + test/regress/regress0/parser/bv_arity_smt2.6.smt2 | 13 +++++++++++++ 4 files changed, 31 insertions(+), 6 deletions(-) create mode 100644 test/regress/regress0/parser/bv_arity_smt2.6.smt2 (limited to 'test/regress/CMakeLists.txt') diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 5c5b87f38..00f2e944d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1886,7 +1886,8 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] Kind lassocKind = CVC4::kind::UNDEFINED_KIND; if (args.size() >= 2) { - if (kind == CVC4::kind::INTS_DIVISION) + if (kind == CVC4::kind::INTS_DIVISION + || (kind == CVC4::kind::BITVECTOR_XNOR && PARSER_STATE->v2_6())) { // Builtin operators that are not tokenized, are left associative, // but not internally variadic must set this. diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 171642c7e..7a3c3b0c3 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -319,15 +319,25 @@ private: // that CVC4 permits as N-ary but the standard requires is binary if(strictModeEnabled()) { switch(kind) { - case kind::BITVECTOR_CONCAT: case kind::BITVECTOR_AND: - case kind::BITVECTOR_OR: - case kind::BITVECTOR_XOR: case kind::BITVECTOR_MULT: + case kind::BITVECTOR_OR: case kind::BITVECTOR_PLUS: + case kind::BITVECTOR_XOR: + if (numArgs != 2 && !v2_6()) + { + parseError( + "Operator requires exactly 2 arguments in strict SMT-LIB " + "compliance mode (for versions <2.6): " + + kindToString(kind)); + } + break; + case kind::BITVECTOR_CONCAT: if(numArgs != 2) { - parseError("Operator requires exact 2 arguments in strict SMT-LIB " - "compliance mode: " + kindToString(kind)); + parseError( + "Operator requires exactly 2 arguments in strict SMT-LIB " + "compliance mode: " + + kindToString(kind)); } break; default: diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 2c6acf69c..97ca9a1be 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -534,6 +534,7 @@ set(regress_0_tests regress0/options/invalid_dump.smt2 regress0/parallel-let.smt2 regress0/parser/as.smt2 + regress0/parser/bv_arity_smt2.6.smt2 regress0/parser/constraint.smt2 regress0/parser/declarefun-emptyset-uf.smt2 regress0/parser/shadow_fun_symbol_all.smt2 diff --git a/test/regress/regress0/parser/bv_arity_smt2.6.smt2 b/test/regress/regress0/parser/bv_arity_smt2.6.smt2 new file mode 100644 index 000000000..437d80f56 --- /dev/null +++ b/test/regress/regress0/parser/bv_arity_smt2.6.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --strict-parsing +(set-info :status unsat) +(set-logic QF_BV) +(declare-const x (_ BitVec 8)) +(declare-const y (_ BitVec 8)) +(declare-const z (_ BitVec 8)) +(assert (or (not (= (bvadd x y z) (bvadd (bvadd x y) z))) + (not (= (bvmul x y z) (bvmul (bvmul x y) z))) + (not (= (bvand x y z) (bvand (bvand x y) z))) + (not (= (bvor x y z) (bvor (bvor x y) z))) + (not (= (bvxor x y z) (bvxor (bvxor x y) z))) + (not (= (bvxnor x y z) (bvxnor (bvxnor x y) z))))) +(check-sat) -- cgit v1.2.3 From 5b00f8d6804bf9f71d6169634341011f99d59b8b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 17 Apr 2019 10:26:46 -0500 Subject: Fix extended function decomposition (#2960) Fixes #2958. The issue was: we had substr(x,0,2) in R, and the "derivable substitution" modifed this to substr(substr(x,0,2),0,2) in R, since substr(x,0,2) was the representative of x (which is a bad choice, but regardless is legal). Then decomposition inference asked "can i reduce substr(substr(x,0,2),0,2) in R"? It determines substr(substr(x,0,2),0,2) in R rewrites to substr(x,0,2) in R, which is already true. However, substr(x,0,2) in R was what we started with. The fix makes things much more conservative: we never mark extended functions reduced based on decomposition, since there isnt a strong argument based on an ordering. --- src/theory/strings/theory_strings.cpp | 26 +++++++++----------------- test/regress/CMakeLists.txt | 1 + test/regress/regress0/strings/issue2958.smt2 | 7 +++++++ 3 files changed, 17 insertions(+), 17 deletions(-) create mode 100644 test/regress/regress0/strings/issue2958.smt2 (limited to 'test/regress/CMakeLists.txt') diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 6333bfee1..8731bd1a5 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1705,8 +1705,8 @@ void TheoryStrings::checkExtfEval( int effort ) { } else { - bool reduced = false; - if (!einfo.d_const.isNull() && nrc.getType().isBoolean()) + // if this was a predicate which changed after substitution + rewriting + if (!einfo.d_const.isNull() && nrc.getType().isBoolean() && nrc != n) { bool pol = einfo.d_const == d_true; Node nrcAssert = pol ? nrc : nrc.negate(); @@ -1716,23 +1716,15 @@ void TheoryStrings::checkExtfEval( int effort ) { Trace("strings-extf-debug") << " decomposable..." << std::endl; Trace("strings-extf") << " resolve extf : " << sn << " -> " << nrc << ", const = " << einfo.d_const << std::endl; - reduced = sendInternalInference( + // We send inferences internal here, which may help show unsat. + // However, we do not make a determination whether n can be marked + // reduced since this argument may be circular: we may infer than n + // can be reduced to something else, but that thing may argue that it + // can be reduced to n, in theory. + sendInternalInference( einfo.d_exp, nrcAssert, effort == 0 ? "EXTF_d" : "EXTF_d-N"); - if (!reduced) - { - Trace("strings-extf") << "EXT: could not fully reduce "; - Trace("strings-extf") - << nAssert << " via " << nrcAssert << std::endl; - } - } - if (reduced) - { - getExtTheory()->markReduced(n); - } - else - { - to_reduce = nrc; } + to_reduce = nrc; } }else{ to_reduce = sterms[i]; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 97ca9a1be..25c0e92aa 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -832,6 +832,7 @@ set(regress_0_tests regress0/strings/ilc-like.smt2 regress0/strings/indexof-sym-simp.smt2 regress0/strings/issue1189.smt2 + regress0/strings/issue2958.smt2 regress0/strings/itos-entail.smt2 regress0/strings/leadingzero001.smt2 regress0/strings/loop001.smt2 diff --git a/test/regress/regress0/strings/issue2958.smt2 b/test/regress/regress0/strings/issue2958.smt2 new file mode 100644 index 000000000..7ed5ef7f3 --- /dev/null +++ b/test/regress/regress0/strings/issue2958.smt2 @@ -0,0 +1,7 @@ +(set-info :smt-lib-version 2.5) +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-const x String) +(assert (not (str.prefixof "ab" x))) +(assert (str.in.re (str.substr x 0 2) (re.++ (str.to.re "ab") (re.* (str.to.re "dcab"))))) +(check-sat) -- cgit v1.2.3 From 19a93d5e0f924c70e7f77719e0310c730c8fbc61 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 29 Apr 2019 20:27:20 -0500 Subject: Eliminate APPLY kind (#2976) --- src/api/cvc4cpp.cpp | 4 --- src/api/cvc4cppkind.h | 25 --------------- src/expr/node.h | 4 +-- src/parser/parser.cpp | 17 ++++------- src/parser/smt2/Smt2.g | 2 +- src/parser/smt2/smt2.cpp | 9 +++--- src/printer/cvc/cvc_printer.cpp | 3 -- src/printer/smt2/smt2_printer.cpp | 2 -- src/smt/command.cpp | 12 ++------ src/smt/smt_engine.cpp | 42 +++++++++++++------------- src/theory/builtin/kinds | 4 --- src/theory/builtin/theory_builtin_type_rules.h | 38 ----------------------- src/theory/datatypes/datatypes_rewriter.cpp | 13 ++++++-- test/regress/CMakeLists.txt | 1 + test/regress/regress0/define-fun-model.smt2 | 16 ++++++++++ 15 files changed, 64 insertions(+), 128 deletions(-) create mode 100644 test/regress/regress0/define-fun-model.smt2 (limited to 'test/regress/CMakeLists.txt') diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 4cd9f4923..ab34e62b4 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -52,8 +52,6 @@ const static std::unordered_map s_kinds{ /* Builtin ------------------------------------------------------------- */ {UNINTERPRETED_CONSTANT, CVC4::Kind::UNINTERPRETED_CONSTANT}, {ABSTRACT_VALUE, CVC4::Kind::ABSTRACT_VALUE}, - {FUNCTION, CVC4::Kind::FUNCTION}, - {APPLY, CVC4::Kind::APPLY}, {EQUAL, CVC4::Kind::EQUAL}, {DISTINCT, CVC4::Kind::DISTINCT}, {CONSTANT, CVC4::Kind::VARIABLE}, @@ -300,8 +298,6 @@ const static std::unordered_map /* Builtin --------------------------------------------------------- */ {CVC4::Kind::UNINTERPRETED_CONSTANT, UNINTERPRETED_CONSTANT}, {CVC4::Kind::ABSTRACT_VALUE, ABSTRACT_VALUE}, - {CVC4::Kind::FUNCTION, FUNCTION}, - {CVC4::Kind::APPLY, APPLY}, {CVC4::Kind::EQUAL, EQUAL}, {CVC4::Kind::DISTINCT, DISTINCT}, {CVC4::Kind::VARIABLE, CONSTANT}, diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index d4f6880f9..7d9ec28c6 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -78,31 +78,6 @@ enum CVC4_PUBLIC Kind : int32_t /* Built-in operator */ BUILTIN, #endif - /** - * Defined function. - * Parameters: 3 (4) - * See defineFun(). - * Create with: - * defineFun(const std::string& symbol, - * const std::vector& bound_vars, - * Sort sort, - * Term term) - * defineFun(Term fun, - * const std::vector& bound_vars, - * Term term) - */ - FUNCTION, - /** - * Application of a defined function. - * Parameters: n > 1 - * -[1]..[n]: Function argument instantiation Terms - * Create with: - * mkTerm(Kind kind, Term child) - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector& children) - */ - APPLY, /** * Equality. * Parameters: 2 diff --git a/src/expr/node.h b/src/expr/node.h index 935cde308..768d7b948 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -489,7 +489,7 @@ public: /** * Returns a node representing the operator of this expression. - * If this is an APPLY, then the operator will be a functional term. + * If this is an APPLY_UF, then the operator will be a functional term. * Otherwise, it will be a node with kind BUILTIN. */ NodeTemplate getOperator() const; @@ -1273,7 +1273,7 @@ NodeTemplate::printAst(std::ostream& out, int indent) const { /** * Returns a node representing the operator of this expression. - * If this is an APPLY, then the operator will be a functional term. + * If this is an APPLY_UF, then the operator will be a functional term. * Otherwise, it will be a node with kind BUILTIN. */ template diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index bc88166d3..28489154a 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -128,23 +128,18 @@ Expr Parser::getExpressionForNameAndType(const std::string& name, Type t) { } // now, post-process the expression assert( !expr.isNull() ); - if(isDefinedFunction(expr)) { - // defined functions/constants are wrapped in an APPLY so that they are - // expanded into their definition, e.g. during SmtEnginePrivate::expandDefinitions - expr = getExprManager()->mkExpr(CVC4::kind::APPLY, expr); - }else{ - Type te = expr.getType(); - if(te.isConstructor() && ConstructorType(te).getArity() == 0) { - // nullary constructors have APPLY_CONSTRUCTOR kind with no children - expr = getExprManager()->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, expr); - } + Type te = expr.getType(); + if (te.isConstructor() && ConstructorType(te).getArity() == 0) + { + // nullary constructors have APPLY_CONSTRUCTOR kind with no children + expr = getExprManager()->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, expr); } return expr; } Kind Parser::getKindForFunction(Expr fun) { if(isDefinedFunction(fun)) { - return APPLY; + return APPLY_UF; } Type t = fun.getType(); if(t.isConstructor()) { diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 75df38637..9ba7f4b2e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2091,7 +2091,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] // however, we need to apply partial version since we don't have the internal selector available aargs.push_back( MK_EXPR( CVC4::kind::APPLY_SELECTOR, dtc[i].getSelector(), expr ) ); } - patexprs.push_back( MK_EXPR( CVC4::kind::APPLY, aargs ) ); + patexprs.push_back( MK_EXPR( CVC4::kind::APPLY_UF, aargs ) ); patconds.push_back( MK_EXPR( CVC4::kind::APPLY_TESTER, dtc.getTester(), expr ) ); } RPAREN_TOK diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 47da10f42..71ba81124 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -859,7 +859,9 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st children.push_back( it->second ); } } - Kind sk = sop.getKind() != kind::BUILTIN ? kind::APPLY : getExprManager()->operatorToKind(sop); + Kind sk = sop.getKind() != kind::BUILTIN + ? kind::APPLY_UF + : getExprManager()->operatorToKind(sop); Debug("parser-sygus") << ": operator " << sop << " with " << sop.getKind() << " " << sk << std::endl; Expr e = getExprManager()->mkExpr( sk, children ); Debug("parser-sygus") << ": constructed " << e << ", which has type " << e.getType() << std::endl; @@ -1072,7 +1074,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, } children.insert(children.end(), largs.begin(), largs.end()); Kind sk = ops[i].getKind() != kind::BUILTIN - ? kind::APPLY + ? kind::APPLY_UF : getExprManager()->operatorToKind(ops[i]); Expr body = getExprManager()->mkExpr(sk, children); // replace by lambda @@ -1131,14 +1133,13 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, std::vector largs; Expr lbvl = makeSygusBoundVarList(dt, i, ftypes, largs); largs.insert(largs.begin(), ops[i]); - Expr body = getExprManager()->mkExpr(kind::APPLY, largs); + Expr body = getExprManager()->mkExpr(kind::APPLY_UF, largs); ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body); Debug("parser-sygus") << " ...replace op : " << ops[i] << std::endl; } else { - ops[i] = getExprManager()->mkExpr(kind::APPLY, ops[i]); Debug("parser-sygus") << " ...replace op : " << ops[i] << std::endl; } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index c95ff5781..630d8bdd7 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -280,9 +280,6 @@ void CvcPrinter::toStream( out << ")"; return; break; - case kind::APPLY: - toStream(op, n.getOperator(), depth, types, true); - break; case kind::CHAIN: case kind::DISTINCT: // chain and distinct not supported directly in CVC4, blast them away with the rewriter toStream(out, theory::Rewriter::rewrite(n), depth, types, true); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 7ea7765d8..5311f1bec 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -475,7 +475,6 @@ void Smt2Printer::toStream(std::ostream& out, } switch(Kind k = n.getKind()) { // builtin theory - case kind::APPLY: break; case kind::EQUAL: case kind::DISTINCT: out << smtKindString(k, d_variant) << " "; @@ -965,7 +964,6 @@ static string smtKindString(Kind k, Variant v) { switch(k) { // builtin theory - case kind::APPLY: break; case kind::EQUAL: return "="; case kind::DISTINCT: return "distinct"; case kind::CHAIN: break; diff --git a/src/smt/command.cpp b/src/smt/command.cpp index ecd3c6f16..b1936d8cc 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1358,8 +1358,7 @@ void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) this->DefineFunctionCommand::invoke(smtEngine); if (!d_func.isNull() && d_func.getType().isBoolean()) { - smtEngine->addToAssignment( - d_func.getExprManager()->mkExpr(kind::APPLY, d_func)); + smtEngine->addToAssignment(d_func); } d_commandStatus = CommandSuccess::instance(); } @@ -1751,14 +1750,7 @@ void GetAssignmentCommand::invoke(SmtEngine* smtEngine) for (const auto& p : assignments) { vector v; - if (p.first.getKind() == kind::APPLY) - { - v.emplace_back(SExpr::Keyword(p.first.getOperator().toString())); - } - else - { - v.emplace_back(SExpr::Keyword(p.first.toString())); - } + v.emplace_back(SExpr::Keyword(p.first.toString())); v.emplace_back(SExpr::Keyword(p.second.toString())); sexprs.emplace_back(v); } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d035f88c1..66198946f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2734,13 +2734,20 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_mapfind(n); if(i != d_smt.d_definedFunctions->end()) { + Node f = (*i).second.getFormula(); + // must expand its definition + Node fe = expandDefinitions(f, cache, expandOnly); // replacement must be closed if((*i).second.getFormals().size() > 0) { - result.push(d_smt.d_nodeManager->mkNode(kind::LAMBDA, d_smt.d_nodeManager->mkNode(kind::BOUND_VAR_LIST, (*i).second.getFormals()), (*i).second.getFormula())); + result.push(d_smt.d_nodeManager->mkNode( + kind::LAMBDA, + d_smt.d_nodeManager->mkNode(kind::BOUND_VAR_LIST, + (*i).second.getFormals()), + fe)); continue; } // don't bother putting in the cache - result.push((*i).second.getFormula()); + result.push(fe); continue; } // don't bother putting in the cache @@ -2758,11 +2765,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_mapmkNode(i == 0 ? kind::APPLY_UF : kind::APPLY, children); + terms[i] = d_nodeManager->mkNode(kind::APPLY_UF, children); // make application of Inv on primed variables if (i == 0) { @@ -4218,15 +4219,15 @@ bool SmtEngine::addToAssignment(const Expr& ex) { "expected Boolean-typed variable or function application " "in addToAssignment()" ); Node n = e.getNode(); - // must be an APPLY of a zero-ary defined function, or a variable + // must be a defined constant, or a variable PrettyCheckArgument( - ( ( n.getKind() == kind::APPLY && - ( d_definedFunctions->find(n.getOperator()) != - d_definedFunctions->end() ) && - n.getNumChildren() == 0 ) || - n.isVar() ), e, + (((d_definedFunctions->find(n) != d_definedFunctions->end()) + && n.getNumChildren() == 0) + || n.isVar()), + e, "expected variable or defined-function application " - "in addToAssignment(),\ngot %s", e.toString().c_str() ); + "in addToAssignment(),\ngot %s", + e.toString().c_str()); if(!options::produceAssignments()) { return false; } @@ -4295,8 +4296,7 @@ vector> SmtEngine::getAssignment() // ensure it's a constant Assert(resultNode.isConst()); - Assert(as.getKind() == kind::APPLY || as.isVar()); - Assert(as.getKind() != kind::APPLY || as.getNumChildren() == 0); + Assert(as.isVar()); res.emplace_back(as.toExpr(), resultNode.toExpr()); } } diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 3313a684f..15891dfad 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -289,9 +289,6 @@ constant BUILTIN \ "expr/kind.h" \ "the kind of expressions representing built-in operators" -variable FUNCTION "a defined function" -parameterized APPLY FUNCTION 0: "application of a defined function" - operator EQUAL 2 "equality (two parameters only, sorts must match)" operator DISTINCT 2: "disequality (N-ary, sorts must match)" variable VARIABLE "a variable (not permitted in bindings)" @@ -332,7 +329,6 @@ well-founded SEXPR_TYPE \ "::CVC4::theory::builtin::SExprProperties::mkGroundTerm(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" -typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 2c726d12f..db427d21e 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -31,44 +31,6 @@ namespace CVC4 { namespace theory { namespace builtin { -class ApplyTypeRule { - public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - TNode f = n.getOperator(); - TypeNode fType = f.getType(check); - if( !fType.isFunction() && n.getNumChildren() > 0 ) { - throw TypeCheckingExceptionPrivate(n, "operator does not have function type"); - } - if( check ) { - if(fType.isFunction()) { - if(n.getNumChildren() != fType.getNumChildren() - 1) { - throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type"); - } - TNode::iterator argument_it = n.begin(); - TNode::iterator argument_it_end = n.end(); - TypeNode::iterator argument_type_it = fType.begin(); - for(; argument_it != argument_it_end; ++argument_it, ++argument_type_it) { - if(!(*argument_it).getType().isComparableTo(*argument_type_it)) { - std::stringstream ss; - ss << "argument types do not match the function type:\n" - << "argument: " << *argument_it << "\n" - << "has type: " << (*argument_it).getType() << "\n" - << "not equal: " << *argument_type_it; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } - } - } else { - if( n.getNumChildren() > 0 ) { - throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type"); - } - } - } - return fType.isFunction() ? fType.getRangeType() : fType; - } -};/* class ApplyTypeRule */ - - class EqualityTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index 5d3a92cdc..be87b7e8d 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -191,8 +191,6 @@ Kind DatatypesRewriter::getOperatorKindForSygusBuiltin(Node op) Assert(op.getKind() != BUILTIN); if (op.getKind() == LAMBDA) { - // we use APPLY_UF instead of APPLY, since the rewriter for APPLY_UF - // does beta-reduction but does not for APPLY return APPLY_UF; } TypeNode tn = op.getType(); @@ -247,7 +245,16 @@ Node DatatypesRewriter::mkSygusTerm(const Datatype& dt, Kind ok = NodeManager::operatorToKind(op); if (ok != UNDEFINED_KIND) { - ret = NodeManager::currentNM()->mkNode(ok, schildren); + if (ok == APPLY_UF && schildren.size() == 1) + { + // This case is triggered for defined constant symbols. In this case, + // we return the operator itself instead of an APPLY_UF node. + ret = schildren[0]; + } + else + { + ret = NodeManager::currentNM()->mkNode(ok, schildren); + } Trace("dt-sygus-util") << "...return (op) " << ret << std::endl; return ret; } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 25c0e92aa..c9514dd76 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -414,6 +414,7 @@ set(regress_0_tests regress0/decision/wchains010ue.delta02.smt regress0/declare-fun-is-match.smt2 regress0/declare-funs.smt2 + regress0/define-fun-model.smt2 regress0/distinct.smt regress0/expect/scrub.01.smt regress0/expect/scrub.02.smt diff --git a/test/regress/regress0/define-fun-model.smt2 b/test/regress/regress0/define-fun-model.smt2 new file mode 100644 index 000000000..c6ca206fc --- /dev/null +++ b/test/regress/regress0/define-fun-model.smt2 @@ -0,0 +1,16 @@ +; SCRUBBER: sed -e 's/BOUND_VARIABLE_[0-9]*/BOUND_VARIABLE/' +; EXPECT: sat +; EXPECT: (((f 4) 7)) +; EXPECT: ((g (lambda ((BOUND_VARIABLE Int)) 7))) +; EXPECT: ((f (lambda ((BOUND_VARIABLE Int)) 7))) +(set-logic UFLIA) +(set-option :produce-models true) +(define-fun f ((x Int)) Int 7) +(declare-fun g (Int) Int) + +(assert (= (g 5) (f 5))) + +(check-sat) +(get-value ((f 4))) +(get-value (g)) +(get-value (f)) -- cgit v1.2.3 From d36423fb74e3ec294b222b806cb24b5229e72ed1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 30 Apr 2019 14:11:16 -0500 Subject: Remove stoi solve rewrite (#2985) --- src/theory/strings/theory_strings_rewriter.cpp | 27 +++----------------------- test/regress/CMakeLists.txt | 3 ++- test/regress/regress0/strings/stoi-solve.smt2 | 6 ------ test/regress/regress1/strings/issue2981.smt2 | 20 +++++++++++++++++++ test/regress/regress1/strings/stoi-solve.smt2 | 6 ++++++ 5 files changed, 31 insertions(+), 31 deletions(-) delete mode 100644 test/regress/regress0/strings/stoi-solve.smt2 create mode 100644 test/regress/regress1/strings/issue2981.smt2 create mode 100644 test/regress/regress1/strings/stoi-solve.smt2 (limited to 'test/regress/CMakeLists.txt') diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 2e50ade0c..47f29e814 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -599,30 +599,9 @@ Node TheoryStringsRewriter::rewriteArithEqualityExt(Node node) { Assert(node.getKind() == EQUAL && node[0].getType().isInteger()); - NodeManager* nm = NodeManager::currentNM(); - // cases where we can solve the equality - for (unsigned i = 0; i < 2; i++) - { - if (node[i].isConst()) - { - Node on = node[1 - i]; - Kind onk = on.getKind(); - if (onk == STRING_STOI) - { - Rational r = node[i].getConst(); - int sgn = r.sgn(); - Node onEq; - std::stringstream ss; - if (sgn >= 0) - { - ss << r.getNumerator(); - } - Node new_ret = on[0].eqNode(nm->mkConst(String(ss.str()))); - return returnRewrite(node, new_ret, "stoi-solve"); - } - } - } + + // notice we cannot rewrite str.to.int(x)=n to x="n" due to leading zeroes. return node; } @@ -1490,7 +1469,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { if(s.isNumber()) { retNode = nm->mkConst(s.toNumber()); } else { - retNode = nm->mkConst(::CVC4::Rational(-1)); + retNode = nm->mkConst(Rational(-1)); } } else if(node[0].getKind() == kind::STRING_CONCAT) { for(unsigned i=0; i Date: Tue, 30 Apr 2019 12:32:50 -0700 Subject: Fix concat-find regexp elimination (#2983) --- src/theory/strings/regexp_elim.cpp | 6 +++--- test/regress/CMakeLists.txt | 1 + test/regress/regress1/strings/issue2982.smt2 | 23 +++++++++++++++++++++++ 3 files changed, 27 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress1/strings/issue2982.smt2 (limited to 'test/regress/CMakeLists.txt') diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index afffce2c8..b6a997629 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -347,10 +347,10 @@ Node RegExpElimination::eliminateConcat(Node atom) for (unsigned r = 0; r < 2; r++) { unsigned index = r == 0 ? 0 : nchildren - 1; - Assert(children[index + (r == 0 ? 1 : -1)].getKind() != STRING_TO_REGEXP); Node c = children[index]; if (c.getKind() == STRING_TO_REGEXP) { + Assert(children[index + (r == 0 ? 1 : -1)].getKind() != STRING_TO_REGEXP); Node s = c[0]; Node lens = nm->mkNode(STRING_LENGTH, s); Node sss = r == 0 ? d_zero : nm->mkNode(MINUS, lenx, lens); @@ -375,9 +375,9 @@ Node RegExpElimination::eliminateConcat(Node atom) rexpElimChildren.push_back(c); } } - Assert(rexpElimChildren.size() + sConstraints.size() == nchildren); if (!sConstraints.empty()) { + Assert(rexpElimChildren.size() + sConstraints.size() == nchildren); Node ss = nm->mkNode(STRING_SUBSTR, x, sStartIndex, sLength); Assert(!rexpElimChildren.empty()); Node regElim = @@ -412,7 +412,7 @@ Node RegExpElimination::eliminateConcat(Node atom) Node bound = nm->mkNode(AND, nm->mkNode(LEQ, d_zero, k), - nm->mkNode(LT, k, nm->mkNode(MINUS, lenx, lens))); + nm->mkNode(LEQ, k, nm->mkNode(MINUS, lenx, lens))); echildren.push_back(bound); } Node substrEq = nm->mkNode(STRING_SUBSTR, x, k, lens).eqNode(s); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index d8adbb59e..714459a85 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1537,6 +1537,7 @@ set(regress_1_tests regress1/strings/issue2060.smt2 regress1/strings/issue2429-code.smt2 regress1/strings/issue2981.smt2 + regress1/strings/issue2982.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 diff --git a/test/regress/regress1/strings/issue2982.smt2 b/test/regress/regress1/strings/issue2982.smt2 new file mode 100644 index 000000000..41be8d1fd --- /dev/null +++ b/test/regress/regress1/strings/issue2982.smt2 @@ -0,0 +1,23 @@ +; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg +; EXPECT: unsat +(set-logic QF_SLIA) + +(declare-fun var_0 () String) +(declare-fun var_1 () String) +(declare-fun var_2 () String) +(declare-fun var_3 () String) +(declare-fun var_4 () String) +(declare-fun var_5 () String) +(declare-fun var_6 () String) +(declare-fun var_7 () String) +(declare-fun var_8 () String) +(declare-fun var_9 () String) +(declare-fun var_10 () String) +(declare-fun var_11 () String) +(declare-fun var_12 () String) + +(assert (str.in.re (str.++ var_7 "z" var_7 ) (re.* (str.to.re "z")))) +(assert (str.in.re var_7 (re.* (re.range "a" "u")))) +(assert (not (str.in.re (str.++ "a" var_7 "z" "a" var_7 ) (re.++ (re.* (re.union (str.to.re "z") (re.++ (str.to.re "a") (re.++ (re.* (str.to.re "a")) (str.to.re "z"))))) (re.++ (str.to.re "a") (re.* (str.to.re "a"))))))) +(assert (and (<= (str.len var_7) 0 ) (<= 0 (str.len var_7)))) +(check-sat) -- cgit v1.2.3