From 085d6a91f0686d6680d15bb54f9435f30d53c331 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 23 Aug 2019 13:00:43 -0500 Subject: [PATCH] Update dynamic splitting strategy for quantifiers (#3162) --- src/options/quantifiers_options.toml | 2 +- src/theory/quantifiers/quant_split.cpp | 135 ++++++++++-------- src/theory/quantifiers/quant_split.h | 37 +++-- .../quantifiers/quantifiers_rewriter.cpp | 49 +++++++ src/theory/quantifiers/quantifiers_rewriter.h | 7 + test/regress/CMakeLists.txt | 2 + .../regress1/quantifiers/f993-loss-easy.smt2 | 73 ++++++++++ .../regress1/quantifiers/issue993.smt2 | 108 ++++++++++++++ 8 files changed, 346 insertions(+), 67 deletions(-) create mode 100644 test/regress/regress1/quantifiers/f993-loss-easy.smt2 create mode 100644 test/regress/regress1/quantifiers/issue993.smt2 diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 00059bba6..4398711b7 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1717,7 +1717,7 @@ header = "options/quantifiers_options.h" category = "regular" long = "quant-dsplit-mode=MODE" type = "CVC4::theory::quantifiers::QuantDSplitMode" - default = "CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_NONE" + default = "CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_DEFAULT" handler = "stringToQuantDSplitMode" includes = ["options/quantifiers_modes.h"] help = "mode for dynamic quantifiers splitting" diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 808c6006f..4e9441279 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -35,9 +35,6 @@ void QuantDSplit::checkOwnership(Node q) { int max_index = -1; int max_score = -1; - if( q.getNumChildren()==3 ){ - return; - } Trace("quant-dsplit-debug") << "Check split quantified formula : " << q << std::endl; for( unsigned i=0; i handled by finite instantiation - // an example is datatypes with uninterpreted sort fields, which are "interpreted finite" but not "finite" if( !d_quantEngine->isFiniteBound( q, q[0][i] ) ){ - score = dt.isInterpretedFinite( tn.toType() ) ? 1 : -1; + if (dt.isInterpretedFinite(tn.toType())) + { + // split if goes from being unhandled -> handled by finite + // instantiation. An example is datatypes with uninterpreted sort + // fields which are "interpreted finite" but not "finite". + score = 1; + } + else if (dt.getNumConstructors() == 1 && !dt.isCodatatype()) + { + // split if only one constructor + score = 1; + } } } Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << " (" << dt.isInterpretedFinite( tn.toType() ) << " " << dt.isFinite( tn.toType() ) << ")" << std::endl; @@ -86,62 +92,79 @@ bool QuantDSplit::checkCompleteFor( Node q ) { void QuantDSplit::check(Theory::Effort e, QEffort quant_e) { //add lemmas ASAP (they are a reduction) - if (quant_e == QEFFORT_CONFLICT) + if (quant_e != QEFFORT_CONFLICT) { - std::vector< Node > lemmas; - for(std::map< Node, int >::iterator it = d_quant_to_reduce.begin(); it != d_quant_to_reduce.end(); ++it) { - Node q = it->first; - if( d_quantEngine->getModel()->isQuantifierAsserted( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ - if( d_added_split.find( q )==d_added_split.end() ){ - d_added_split.insert( q ); - std::vector< Node > bvs; - for( unsigned i=0; isecond ){ - bvs.push_back( q[0][i] ); - } - } - std::vector< Node > disj; - disj.push_back( q.negate() ); - TNode svar = q[0][it->second]; - TypeNode tn = svar.getType(); - if( tn.isDatatype() ){ - std::vector< Node > cons; - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - for( unsigned j=0; j vars; - for( unsigned k=0; kmkBoundVar( tns ); - vars.push_back( v ); - } - std::vector< Node > bvs_cmb; - bvs_cmb.insert( bvs_cmb.end(), bvs.begin(), bvs.end() ); - bvs_cmb.insert( bvs_cmb.end(), vars.begin(), vars.end() ); - vars.insert( vars.begin(), Node::fromExpr( dt[j].getConstructor() ) ); - Node c = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, vars ); - TNode ct = c; - Node body = q[1].substitute( svar, ct ); - if( !bvs_cmb.empty() ){ - body = NodeManager::currentNM()->mkNode( kind::FORALL, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bvs_cmb ), body ); - } - cons.push_back( body ); - } - Node conc = cons.size()==1 ? cons[0] : NodeManager::currentNM()->mkNode( kind::AND, cons ); - disj.push_back( conc ); - }else{ - Assert( false ); + return; + } + NodeManager* nm = NodeManager::currentNM(); + FirstOrderModel* m = d_quantEngine->getModel(); + std::vector lemmas; + for (std::map::iterator it = d_quant_to_reduce.begin(); + it != d_quant_to_reduce.end(); + ++it) + { + Node q = it->first; + if (m->isQuantifierAsserted(q) && m->isQuantifierActive(q) + && d_added_split.find(q) == d_added_split.end()) + { + d_added_split.insert(q); + std::vector bvs; + for (unsigned i = 0, nvars = q[0].getNumChildren(); i < nvars; i++) + { + if (static_cast(i) != it->second) + { + bvs.push_back(q[0][i]); + } + } + std::vector disj; + disj.push_back(q.negate()); + TNode svar = q[0][it->second]; + TypeNode tn = svar.getType(); + Assert(tn.isDatatype()); + std::vector cons; + const Datatype& dt = static_cast(tn.toType()).getDatatype(); + for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++) + { + std::vector vars; + for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++) + { + TypeNode tns = TypeNode::fromType(dt[j][k].getRangeType()); + Node v = nm->mkBoundVar(tns); + vars.push_back(v); + } + std::vector bvs_cmb; + bvs_cmb.insert(bvs_cmb.end(), bvs.begin(), bvs.end()); + bvs_cmb.insert(bvs_cmb.end(), vars.begin(), vars.end()); + vars.insert(vars.begin(), Node::fromExpr(dt[j].getConstructor())); + Node c = nm->mkNode(kind::APPLY_CONSTRUCTOR, vars); + TNode ct = c; + Node body = q[1].substitute(svar, ct); + if (!bvs_cmb.empty()) + { + Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, bvs_cmb); + std::vector children; + children.push_back(bvl); + children.push_back(body); + if (q.getNumChildren() == 3) + { + Node ipls = q[2].substitute(svar, ct); + children.push_back(ipls); } - lemmas.push_back( disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj ) ); + body = nm->mkNode(kind::FORALL, children); } + cons.push_back(body); } + Node conc = cons.size() == 1 ? cons[0] : nm->mkNode(kind::AND, cons); + disj.push_back(conc); + lemmas.push_back(disj.size() == 1 ? disj[0] : nm->mkNode(kind::OR, disj)); } + } - //add lemmas to quantifiers engine - for( unsigned i=0; iaddLemma( lemmas[i], false ); - } - //d_quant_to_reduce.clear(); + // add lemmas to quantifiers engine + for (const Node& lem : lemmas) + { + Trace("quant-dsplit") << "QuantDSplit lemma : " << lem << std::endl; + d_quantEngine->addLemma(lem, false); } } diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index e88e99a83..bea0c3439 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -27,28 +27,45 @@ class QuantifiersEngine; namespace quantifiers { +/** Quantifiers dynamic splitting + * + * This module identifies quantified formulas that should be "split", e.g. + * based on datatype constructor case splitting. + * + * An example of a quantified formula that we may split is the following. Let: + * optionPair := mkPair( U, U ) | none + * where U is an uninterpreted sort. The quantified formula: + * forall x : optionPair. P( x ) + * may be "split" via the lemma: + * forall x : optionPair. P( x ) <=> + * ( forall xy : U. P( mkPair( x, y ) ) OR P( none ) ) + * + * Notice that such splitting may lead to exponential behavior, say if we + * quantify over 32 variables of type optionPair above gives 2^32 disjuncts. + * This class is used to compute this splitting dynamically, by splitting + * one variable per quantified formula at a time. + */ class QuantDSplit : public QuantifiersModule { typedef context::CDHashSet NodeSet; -private: - /** list of relevant quantifiers asserted in the current context */ - std::map< Node, int > d_quant_to_reduce; - /** whether we have instantiated quantified formulas */ - NodeSet d_added_split; -public: + + public: QuantDSplit( QuantifiersEngine * qe, context::Context* c ); /** determine whether this quantified formula will be reduced */ void checkOwnership(Node q) override; - /* whether this module needs to check this round */ bool needsCheck(Theory::Effort e) override; /* Call during quantifier engine's check */ void check(Theory::Effort e, QEffort quant_e) override; - /* Called for new quantifiers */ - void registerQuantifier(Node q) override {} - void assertNode(Node n) override {} + /** check complete for */ bool checkCompleteFor(Node q) override; /** Identify this module (for debugging, dynamic configuration, etc..) */ std::string identify() const override { return "QuantDSplit"; } + + private: + /** list of relevant quantifiers asserted in the current context */ + std::map d_quant_to_reduce; + /** whether we have instantiated quantified formulas */ + NodeSet d_added_split; }; } diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index fb21d6895..f5159a630 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1076,6 +1076,23 @@ bool QuantifiersRewriter::getVarElimLit(Node lit, } } } + else if (lit.getKind() == APPLY_TESTER && pol + && lit[0].getKind() == BOUND_VARIABLE && options::dtVarExpandQuant()) + { + Trace("var-elim-dt") << "Expand datatype variable based on : " << lit + << std::endl; + Expr testerExpr = lit.getOperator().toExpr(); + unsigned index = Datatype::indexOf(testerExpr); + Node s = datatypeExpand(index, lit[0], args); + if (!s.isNull()) + { + vars.push_back(lit[0]); + subs.push_back(s); + Trace("var-elim-dt") << "...apply substitution " << s << "/" << lit[0] + << std::endl; + return true; + } + } if (lit.getKind() == BOUND_VARIABLE) { std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit ); @@ -1149,6 +1166,38 @@ bool QuantifiersRewriter::getVarElimLit(Node lit, return false; } +Node QuantifiersRewriter::datatypeExpand(unsigned index, + Node v, + std::vector& args) +{ + if (!v.getType().isDatatype()) + { + return Node::null(); + } + std::vector::iterator ita = std::find(args.begin(), args.end(), v); + if (ita == args.end()) + { + return Node::null(); + } + const Datatype& dt = + static_cast(v.getType().toType()).getDatatype(); + Assert(index < dt.getNumConstructors()); + const DatatypeConstructor& c = dt[index]; + std::vector newChildren; + newChildren.push_back(Node::fromExpr(c.getConstructor())); + std::vector newVars; + for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++) + { + TypeNode tn = TypeNode::fromType(c.getArgType(j)); + Node vn = NodeManager::currentNM()->mkBoundVar(tn); + newChildren.push_back(vn); + newVars.push_back(vn); + } + args.erase(ita); + args.insert(args.end(), newVars.begin(), newVars.end()); + return NodeManager::currentNM()->mkNode(APPLY_CONSTRUCTOR, newChildren); +} + bool QuantifiersRewriter::getVarElim(Node n, bool pol, std::vector& args, diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index b72619392..7703f01fd 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -50,6 +50,13 @@ private: std::map< Node, Node >& cache, std::map< Node, Node >& icache, std::vector< Node >& new_vars, std::vector< Node >& new_conds, bool elimExtArith ); static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj ); + /** datatype expand + * + * If v occurs in args and has a datatype type whose index^th constructor is + * C, this method returns a node of the form C( x1, ..., xn ), removes v from + * args and adds x1...xn to args. + */ + static Node datatypeExpand(unsigned index, Node v, std::vector& args); //-------------------------------------variable elimination /** is variable elimination * diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 8fa0c2791..74b602119 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1358,6 +1358,7 @@ set(regress_1_tests regress1/quantifiers/dump-inst.smt2 regress1/quantifiers/ext-ex-deq-trigger.smt2 regress1/quantifiers/extract-nproc.smt2 + regress1/quantifiers/f993-loss-easy.smt2 regress1/quantifiers/florian-case-ax.smt2 regress1/quantifiers/fp-cegqi-unsat.smt2 regress1/quantifiers/gauss_init_0030.fof.smt2 @@ -1369,6 +1370,7 @@ set(regress_1_tests regress1/quantifiers/is-even.smt2 regress1/quantifiers/isaplanner-goal20.smt2 regress1/quantifiers/issue2970-string-var-elim.smt2 + regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lra-vts-inf.smt2 regress1/quantifiers/mix-coeff.smt2 diff --git a/test/regress/regress1/quantifiers/f993-loss-easy.smt2 b/test/regress/regress1/quantifiers/f993-loss-easy.smt2 new file mode 100644 index 000000000..775b63338 --- /dev/null +++ b/test/regress/regress1/quantifiers/f993-loss-easy.smt2 @@ -0,0 +1,73 @@ +(set-info :smt-lib-version 2.6) +(set-logic UFDT) +(set-info :status unsat) +(declare-sort A$ 0) +(declare-sort Nat$ 0) +(declare-sort Nat_nat_fun$ 0) +(declare-sort Enat_nat_fun$ 0) +(declare-sort Nat_bool_fun$ 0) +(declare-sort Nat_enat_fun$ 0) +(declare-sort Bool_bool_fun$ 0) +(declare-sort Enat_bool_fun$ 0) +(declare-sort Enat_enat_fun$ 0) +(declare-sort A_stream_bool_fun$ 0) +(declare-sort Nat_bool_fun_nat_fun$ 0) +(declare-sort Nat_nat_bool_fun_fun$ 0) +(declare-sort Bool_enat_bool_fun_fun$ 0) +(declare-sort Enat_enat_bool_fun_fun$ 0) +(declare-sort Nat_bool_fun_nat_bool_fun_fun$ 0) +(declare-datatypes ((Nat_option$ 0)(Enat$ 0)) (((none$) (some$ (the$ Nat$))) +((abs_enat$ (rep_enat$ Nat_option$))) +)) +(declare-sort A_stream$ 0) +(declare-fun shd$ (A_stream$) A$) +(declare-fun stl$ (A_stream$) A_stream$) +(declare-fun sCons$ (A$ A_stream$) A_stream$) +(declare-fun i$ () Nat$) +(declare-fun p$ () A_stream_bool_fun$) +(declare-fun ia$ () Nat$) +(declare-fun uu$ (Nat$) Nat_bool_fun$) +(declare-fun suc$ (Nat$) Nat$) +(declare-fun uua$ (Enat$) Nat_bool_fun$) +(declare-fun uub$ (Bool_bool_fun$) Nat_bool_fun_nat_bool_fun_fun$) +(declare-fun uuc$ (Enat$) Nat_bool_fun$) +(declare-fun uud$ () Nat_nat_fun$) +(declare-fun eSuc$ (Enat$) Enat$) +(declare-fun enat$ (Nat$) Enat$) +(declare-fun less$ (Nat$) Nat_bool_fun$) +(declare-fun plus$ (Enat$) Enat_enat_fun$) +(declare-fun less$a (Enat$) Enat_bool_fun$) +(declare-fun omega$ () A_stream$) +(declare-fun plus$a (Nat$) Nat_nat_fun$) +(declare-fun sdrop$ (Nat$ A_stream$) A_stream$) +(declare-fun omega$a () A_stream$) +(declare-fun sfirst$ (A_stream_bool_fun$ A_stream$) Enat$) +(declare-fun fun_app$ (Nat_bool_fun$ Nat$) Bool) +(declare-fun less_eq$ (Nat$) Nat_bool_fun$) +(declare-fun case_nat$ (Bool) Nat_bool_fun_nat_bool_fun_fun$) +(declare-fun fun_app$a (Enat_bool_fun$ Enat$) Bool) +(declare-fun fun_app$b (Bool_enat_bool_fun_fun$ Bool) Enat_bool_fun$) +(declare-fun fun_app$c (Nat_bool_fun_nat_bool_fun_fun$ Nat_bool_fun$) Nat_bool_fun$) +(declare-fun fun_app$d (Bool_bool_fun$ Bool) Bool) +(declare-fun fun_app$e (Nat_nat_fun$ Nat$) Nat$) +(declare-fun fun_app$f (A_stream_bool_fun$ A_stream$) Bool) +(declare-fun fun_app$g (Nat_enat_fun$ Nat$) Enat$) +(declare-fun fun_app$h (Enat_enat_fun$ Enat$) Enat$) +(declare-fun fun_app$i (Enat_nat_fun$ Enat$) Nat$) +(declare-fun fun_app$j (Enat_enat_bool_fun_fun$ Enat$) Enat_bool_fun$) +(declare-fun fun_app$k (Nat_nat_bool_fun_fun$ Nat$) Nat_bool_fun$) +(declare-fun fun_app$l (Nat_bool_fun_nat_fun$ Nat_bool_fun$) Nat$) +(declare-fun greatest$ (Enat_bool_fun$) Enat$) +(declare-fun less_eq$a (Enat$) Enat_bool_fun$) +(declare-fun rec_enat$ (Nat_bool_fun$) Bool_enat_bool_fun_fun$) +(declare-fun case_enat$ (Nat_bool_fun$) Bool_enat_bool_fun_fun$) +(declare-fun greatest$a () Nat_bool_fun_nat_fun$) +(declare-fun greatestM$ (Nat_nat_fun$) Nat_bool_fun_nat_fun$) +(assert (and +(forall ((?v0 Nat$) (?v1 A_stream_bool_fun$) (?v2 A_stream$)) (=> (fun_app$a (less$a (enat$ ?v0)) (sfirst$ ?v1 ?v2)) (not (fun_app$f ?v1 (sdrop$ ?v0 ?v2)))) ) +(not (fun_app$a (less_eq$a (sfirst$ p$ omega$)) (enat$ (suc$ ia$)))) +(fun_app$f p$ (sdrop$ (suc$ ia$) omega$)) +(forall ((?v0 Enat$) (?v1 Enat$)) (=> (not (fun_app$a (less$a ?v0) ?v1)) (fun_app$a (less_eq$a ?v1) ?v0)) ) +)) +(check-sat) +(exit) diff --git a/test/regress/regress1/quantifiers/issue993.smt2 b/test/regress/regress1/quantifiers/issue993.smt2 new file mode 100644 index 000000000..40c5538de --- /dev/null +++ b/test/regress/regress1/quantifiers/issue993.smt2 @@ -0,0 +1,108 @@ +(set-logic AUFBVDTNIRA) +(set-info :smt-lib-version 2.0) +(set-info :status unsat) +(declare-sort us_private 0) + +(declare-sort integer 0) + +(declare-fun to_rep1 (integer) Int) + +(declare-datatypes () +((us_split_fields + (mk___split_fields (rec__unit1__t1__c1 integer)(rec__ext__ us_private))))) + +(declare-datatypes () +((us_split_fields__ref + (mk___split_fields__ref (us_split_fields__content us_split_fields))))) +(define-fun us_split_fields__ref___projection ((a us_split_fields__ref)) us_split_fields + (us_split_fields__content a)) + +(declare-datatypes () +((us_rep (mk___rep (us_split_fields1 us_split_fields)(attr__tag Int))))) +(define-fun us_rep___projection ((a us_rep)) us_split_fields (us_split_fields1 + a)) + +(declare-fun is_zero (us_rep) Bool) + +(declare-fun is_zero__post_predicate (Bool us_rep) Bool) + +;; is_zero__def_axiom + (assert + (forall ((x us_rep)) + (! (=> (is_zero__post_predicate (is_zero x) x) + (= (= (is_zero x) true) + (= (to_rep1 (rec__unit1__t1__c1 (us_split_fields1 x))) 0))) :pattern ( + (is_zero x)) ))) + +(declare-datatypes () +((us_split_fields2 + (mk___split_fields1 + (rec__unit2__t2__c2 integer)(rec__unit1__t1__c11 integer)(rec__ext__1 us_private))))) + +(declare-datatypes () +((us_split_fields__ref1 + (mk___split_fields__ref1 (us_split_fields__content1 us_split_fields2))))) +(define-fun us_split_fields__ref_2__projection ((a us_split_fields__ref1)) us_split_fields2 + (us_split_fields__content1 a)) + +(declare-datatypes () +((us_rep1 (mk___rep1 (us_split_fields3 us_split_fields2)(attr__tag1 Int))))) +(define-fun us_rep_3__projection ((a us_rep1)) us_split_fields2 (us_split_fields3 + a)) + +(declare-fun hide_ext__ (integer us_private) us_private) + +(define-fun to_base ((a us_rep1)) us_rep (mk___rep + (mk___split_fields + (rec__unit1__t1__c11 + (us_split_fields3 a)) + (hide_ext__ + (rec__unit2__t2__c2 + (us_split_fields3 a)) + (rec__ext__1 (us_split_fields3 a)))) + (attr__tag1 a))) + +(declare-fun is_zero2 (us_rep1) Bool) + +(declare-fun is_zero__post_predicate2 (Bool us_rep1) Bool) + +;; is_zero__def_axiom + (assert + (forall ((x us_rep1)) + (! (=> (is_zero__post_predicate2 (is_zero2 x) x) + (= (= (is_zero2 x) true) + (and (= (is_zero (to_base x)) true) + (= (to_rep1 (rec__unit2__t2__c2 (us_split_fields3 x))) 0)))) :pattern ( + (is_zero2 x)) ))) + +(declare-fun x2__attr__tag () Int) + +(declare-fun x2__split_fields () integer) + +(declare-fun x2__split_fields1 () integer) + +(declare-fun x2__split_fields2 () us_private) + +;; H + (assert + (forall ((x2__split_fields3 us_split_fields2)) (is_zero__post_predicate2 + (is_zero2 (mk___rep1 x2__split_fields3 x2__attr__tag)) + (mk___rep1 x2__split_fields3 x2__attr__tag)))) + +;; H + (assert + (and (= (to_rep1 x2__split_fields1) 0) (= (to_rep1 x2__split_fields) 0))) + +;; Should be enough to imply following hypothesis + (assert + (forall ((x us_rep1)) (is_zero__post_predicate (is_zero (to_base x)) + (to_base x)))) + +(assert +;; WP_parameter_def + ;; File "main.adb", line 5, characters 0-0 + (not + (= (is_zero (to_base (mk___rep1 + (mk___split_fields1 x2__split_fields x2__split_fields1 + x2__split_fields2) x2__attr__tag))) true))) +(check-sat) -- 2.30.2