From 11f94aea79325423fd1ea864729be8a76d7099c0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 11 Oct 2017 11:42:23 -0500 Subject: [PATCH] Ho Lambda Lifting (#1116) * Do lambda lifting in term formula removal pass. Set option in SMT engine related to higher-order. * Better documentation --- src/smt/smt_engine.cpp | 6 +++++ src/smt/term_formula_removal.cpp | 44 ++++++++++++++++++++------------ src/smt/term_formula_removal.h | 34 ++++++++++++++++++++---- 3 files changed, 63 insertions(+), 21 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 099980653..5c3786108 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1762,6 +1762,12 @@ void SmtEngine::setDefaults() { options::prenexQuant.set( quantifiers::PRENEX_QUANT_NONE ); } } + if( options::ufHo() ){ + //if higher-order, then current variants of model-based instantiation cannot be used + if( options::mbqiMode()!=quantifiers::MBQI_NONE ){ + options::mbqiMode.set( quantifiers::MBQI_NONE ); + } + } if( options::mbqiMode()==quantifiers::MBQI_ABS ){ if( !d_logic.isPure(THEORY_UF) ){ //MBQI_ABS is only supported in pure quantified UF diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index a008868c7..0cd166c87 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -101,40 +101,52 @@ Node RemoveTermFormulas::run(TNode node, std::vector& output, // If an ITE, replace it TypeNode nodeType = node.getType(); + Node skolem; + Node newAssertion; if(node.getKind() == kind::ITE) { if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) { - Node skolem; // Make the skolem to represent the ITE skolem = nodeManager->mkSkolem("termITE", nodeType, "a variable introduced due to term-level ITE removal"); // The new assertion - Node newAssertion = + newAssertion = nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]), skolem.eqNode(node[2])); - Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl; - - // Attach the skolem - d_iteCache.insert(cacheKey, skolem); - - // Remove ITEs from the new assertion, rewrite it and push it to the output - newAssertion = run(newAssertion, output, iteSkolemMap, false, false); - - iteSkolemMap[skolem] = output.size(); - output.push_back(newAssertion); + } + } + //if a lambda, do lambda-lifting + if( node.getKind() == kind::LAMBDA && !inQuant ){ + // Make the skolem to represent the ITE + skolem = nodeManager->mkSkolem("lambdaF", nodeType, "a function introduced due to term-level lambda removal"); - // The representation is now the skolem - return skolem; + // The new assertion + std::vector< Node > children; + // bound variable list + children.push_back( node[0] ); + // body + std::vector< Node > skolem_app_c; + skolem_app_c.push_back( skolem ); + for( unsigned i=0; imkNode( kind::APPLY_UF, skolem_app_c ); + children.push_back( skolem_app.eqNode( node[1] ) ); + // axiom defining skolem + newAssertion = nodeManager->mkNode( kind::FORALL, children ); } //if a non-variable Boolean term, replace it if(node.getKind()!=kind::BOOLEAN_TERM_VARIABLE && nodeType.isBoolean() && inTerm && !inQuant ){//(!inQuant || !node.hasBoundVar())){ - Node skolem; + // Make the skolem to represent the Boolean term //skolem = nodeManager->mkSkolem("termBT", nodeType, "a variable introduced due to Boolean term removal"); skolem = nodeManager->mkBooleanTermVariable(); // The new assertion - Node newAssertion = skolem.eqNode( node ); + newAssertion = skolem.eqNode( node ); + } + + // if we introduced a skolem + if( !skolem.isNull() ){ Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl; // Attach the skolem diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index 854ddc61e..48b1c36c5 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -49,23 +49,47 @@ public: ~RemoveTermFormulas(); /** - * Removes the ITE nodes by introducing skolem variables. All - * additional assertions are pushed into assertions. iteSkolemMap + * By introducing skolem variables, this function removes all occurrences of: + * (1) term ITEs + * (2) terms of type Boolean that are not Boolean term variables, and + * (3) lambdas + * from assertions. + * All additional assertions are pushed into assertions. iteSkolemMap * contains a map from introduced skolem variables to the index in - * assertions containing the new Boolean ite created in conjunction + * assertions containing the new definition created in conjunction * with that skolem variable. * + * As an example of (1): + * f( (ite C 0 1)) = 2 + * becomes + * f( k ) = 2 ^ ite( C, k=0, k=1 ) + * + * As an example of (2): + * g( (and C1 C2) ) = 3 + * becomes + * g( k ) = 3 ^ ( k <=> (and C1 C2) ) + * + * As an example of (3): + * (lambda x. t[x]) = f + * becomes + * (forall x. k(x) = t[x]) ^ k = f + * where k is a fresh skolem. This is sometimes called "lambda lifting" + * * With reportDeps true, report reasoning dependences to the proof * manager (for unsat cores). */ void run(std::vector& assertions, IteSkolemMap& iteSkolemMap, bool reportDeps = false); /** - * Removes the ITE from the node by introducing skolem - * variables. All additional assertions are pushed into + * Removes terms of the form (1), (2), (3) described above from node. + * All additional assertions are pushed into * assertions. iteSkolemMap contains a map from introduced skolem * variables to the index in assertions containing the new Boolean * ite created in conjunction with that skolem variable. + * + * inQuant is whether we are processing node in the body of quantified formula + * inTerm is whether we are are processing node in a "term" position, that is, it is a subterm + * of a parent term that is not a Boolean connective. */ Node run(TNode node, std::vector& additionalAssertions, IteSkolemMap& iteSkolemMap, bool inQuant, bool inTerm); -- 2.30.2