From af135825a60f917711d133828c9fdd6831e2142d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 12 Apr 2018 12:23:57 -0500 Subject: [PATCH] Fixes for free variables in assertions (#1762) --- src/smt/term_formula_removal.cpp | 12 +++++-- src/theory/quantifiers/sygus_inference.cpp | 2 +- src/theory/quantifiers/theory_quantifiers.h | 4 --- src/theory/term_registration_visitor.cpp | 40 +++++++++++---------- src/theory/theory.h | 5 --- src/theory/theory_engine.cpp | 12 +++++-- 6 files changed, 42 insertions(+), 33 deletions(-) diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 250c21202..fc10d2b4b 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -215,8 +215,11 @@ Node RemoveTermFormulas::run(TNode node, std::vector& output, // The representation is now the skolem return skolem; } - - if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { + + if (node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS + || node.getKind() == kind::LAMBDA + || node.getKind() == kind::CHOICE) + { // Remember if we're inside a quantifier inQuant = true; }else if( !inTerm && hasNestedTermChildren( node ) ){ @@ -275,7 +278,10 @@ Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const { return cached.isNull() ? Node(node) : cached; } - if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { + if (node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS + || node.getKind() == kind::LAMBDA + || node.getKind() == kind::CHOICE) + { // Remember if we're inside a quantifier inQuant = true; }else if( !inTerm && hasNestedTermChildren( node ) ){ diff --git a/src/theory/quantifiers/sygus_inference.cpp b/src/theory/quantifiers/sygus_inference.cpp index 5b995f052..cea992f54 100644 --- a/src/theory/quantifiers/sygus_inference.cpp +++ b/src/theory/quantifiers/sygus_inference.cpp @@ -192,7 +192,7 @@ bool SygusInference::simplify(std::vector& assertions) // sygus attribute to mark the conjecture as a sygus conjecture Trace("sygus-infer") << "Make outer sygus conjecture..." << std::endl; - Node sygusVar = nm->mkBoundVar("sygus", nm->booleanType()); + Node sygusVar = nm->mkSkolem("sygus", nm->booleanType()); SygusAttribute ca; sygusVar.setAttribute(ca, true); Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusVar); diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 4f87f6aae..4bb28fe79 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -58,10 +58,6 @@ class TheoryQuantifiers : public Theory { Node n, std::vector node_values, std::string str_value) override; - bool ppDontRewriteSubterm(TNode atom) override - { - return atom.getKind() == kind::FORALL || atom.getKind() == kind::EXISTS; - } private: void assertUniversal( Node n ); diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 1e1a2e8e6..eae5578cf 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -35,15 +35,17 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl; - if( ( parent.getKind() == kind::FORALL || - parent.getKind() == kind::EXISTS || - parent.getKind() == kind::REWRITE_RULE || - parent.getKind() == kind::SEP_STAR || - parent.getKind() == kind::SEP_WAND || - ( parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean() ) - // parent.getKind() == kind::CARDINALITY_CONSTRAINT - ) && - current != parent ) { + if ((parent.getKind() == kind::FORALL || parent.getKind() == kind::EXISTS + || parent.getKind() == kind::LAMBDA + || parent.getKind() == kind::CHOICE + || parent.getKind() == kind::REWRITE_RULE + || parent.getKind() == kind::SEP_STAR + || parent.getKind() == kind::SEP_WAND + || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean()) + // parent.getKind() == kind::CARDINALITY_CONSTRAINT + ) + && current != parent) + { Debug("register::internal") << "quantifier:true" << std::endl; return true; } @@ -179,15 +181,17 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl; - if( ( parent.getKind() == kind::FORALL || - parent.getKind() == kind::EXISTS || - parent.getKind() == kind::REWRITE_RULE || - parent.getKind() == kind::SEP_STAR || - parent.getKind() == kind::SEP_WAND || - ( parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean() ) - // parent.getKind() == kind::CARDINALITY_CONSTRAINT - ) && - current != parent ) { + if ((parent.getKind() == kind::FORALL || parent.getKind() == kind::EXISTS + || parent.getKind() == kind::LAMBDA + || parent.getKind() == kind::CHOICE + || parent.getKind() == kind::REWRITE_RULE + || parent.getKind() == kind::SEP_STAR + || parent.getKind() == kind::SEP_WAND + || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean()) + // parent.getKind() == kind::CARDINALITY_CONSTRAINT + ) + && current != parent) + { Debug("register::internal") << "quantifier:true" << std::endl; return true; } diff --git a/src/theory/theory.h b/src/theory/theory.h index f38cda90a..2f7ce6999 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -552,11 +552,6 @@ public: */ virtual Node ppRewrite(TNode atom) { return atom; } - /** - * Don't preprocess subterm of this term - */ - virtual bool ppDontRewriteSubterm(TNode atom) { return false; } - /** * Notify preprocessed assertions. Called on new assertions after * preprocessing before they are asserted to theory engine. diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index de71a8b5e..38885db85 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -394,6 +394,8 @@ void TheoryEngine::preRegister(TNode preprocessed) { } // the atom should not have free variables + Debug("theory") << "TheoryEngine::preRegister: " << preprocessed + << std::endl; Assert(!preprocessed.hasFreeVar()); // Pre-register the terms in the atom Theory::Set theories = NodeVisitor::run(d_preRegistrationVisitor, preprocessed); @@ -1056,9 +1058,15 @@ Node TheoryEngine::ppTheoryRewrite(TNode term) { Trace("theory-pp") << "ppTheoryRewrite { " << term << endl; Node newTerm; - if (theoryOf(term)->ppDontRewriteSubterm(term)) { + // do not rewrite inside quantifiers + if (term.getKind() == kind::FORALL || term.getKind() == kind::EXISTS + || term.getKind() == kind::CHOICE + || term.getKind() == kind::LAMBDA) + { newTerm = Rewriter::rewrite(term); - } else { + } + else + { NodeBuilder<> newNode(term.getKind()); if (term.getMetaKind() == kind::metakind::PARAMETERIZED) { newNode << term.getOperator(); -- 2.30.2