From 1210cf5b69466ee910da1208420ef718cfa96be6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 15 Mar 2022 12:07:14 -0500 Subject: [PATCH] Remove unecessary separation logic options (#8269) Code changed indentation and was cleaned slightly. --- src/options/sep_options.toml | 24 --- src/theory/sep/theory_sep.cpp | 297 +++++++++++++++------------------- 2 files changed, 133 insertions(+), 188 deletions(-) diff --git a/src/options/sep_options.toml b/src/options/sep_options.toml index ff5ac1af6..be347502c 100644 --- a/src/options/sep_options.toml +++ b/src/options/sep_options.toml @@ -1,14 +1,6 @@ id = "SEP" name = "Separation Logic Theory" -[[option]] - name = "sepCheckNeg" - category = "regular" - long = "sep-check-neg" - type = "bool" - default = "true" - help = "check negated spatial assertions" - [[option]] name = "sepMinimalRefine" category = "regular" @@ -17,14 +9,6 @@ name = "Separation Logic Theory" default = "false" help = "only add refinement lemmas for minimal (innermost) assertions" -[[option]] - name = "sepDisequalC" - category = "regular" - long = "sep-deq-c" - type = "bool" - default = "true" - help = "assume cardinality elements are distinct" - [[option]] name = "sepPreSkolemEmp" category = "regular" @@ -32,11 +16,3 @@ name = "Separation Logic Theory" type = "bool" default = "false" help = "eliminate emp constraint at preprocess time" - -[[option]] - name = "sepChildRefine" - category = "regular" - long = "sep-child-refine" - type = "bool" - default = "false" - help = "child-specific refinements of negated star, positive wand" diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 7c1c58e5d..549bc7403 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -667,36 +667,11 @@ void TheorySep::postCheck(Effort level) bool addedLemma = false; bool needAddLemma = false; // check negated star / positive wand - if (options().sep.sepCheckNeg) - { - // get active labels - std::map active_lbl; - if (options().sep.sepMinimalRefine) - { - for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) { - Node fact = (*i); - bool polarity = fact.getKind() != NOT; - TNode atom = polarity ? fact : fact[0]; - TNode satom = atom[0]; - bool use_polarity = satom.getKind() == SEP_WAND ? !polarity : polarity; - if( !use_polarity ){ - Assert(assert_active.find(fact) != assert_active.end()); - if( assert_active[fact] ){ - Assert(atom.getKind() == SEP_LABEL); - TNode slbl = atom[1]; - std::map >& lms = d_label_map[satom]; - if (lms.find(slbl) != lms.end()) - { - Trace("sep-process-debug") - << "Active lbl : " << slbl << std::endl; - active_lbl[slbl] = true; - } - } - } - } - } - // process spatial assertions + // get active labels + std::map active_lbl; + if (options().sep.sepMinimalRefine) + { for (NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i) @@ -705,123 +680,143 @@ void TheorySep::postCheck(Effort level) bool polarity = fact.getKind() != NOT; TNode atom = polarity ? fact : fact[0]; TNode satom = atom[0]; - bool use_polarity = satom.getKind() == SEP_WAND ? !polarity : polarity; - Trace("sep-process-debug") - << " check atom : " << satom << " use polarity " << use_polarity - << std::endl; - if (use_polarity) + if (!use_polarity) { - continue; - } - Assert(assert_active.find(fact) != assert_active.end()); - if (!assert_active[fact]) - { - Trace("sep-process-debug") - << "--> inactive negated assertion " << satom << std::endl; - continue; - } - Assert(atom.getKind() == SEP_LABEL); - TNode slbl = atom[1]; - Trace("sep-process") << "--> Active negated atom : " << satom - << ", lbl = " << slbl << std::endl; - // add refinement lemma - if (!ContainsKey(d_label_map[satom], slbl)) - { - Trace("sep-process-debug") << " no children." << std::endl; - Assert(satom.getKind() == SEP_PTO || satom.getKind() == SEP_EMP); - continue; + Assert(assert_active.find(fact) != assert_active.end()); + if (assert_active[fact]) + { + Assert(atom.getKind() == SEP_LABEL); + TNode slbl = atom[1]; + std::map >& lms = d_label_map[satom]; + if (lms.find(slbl) != lms.end()) + { + Trace("sep-process-debug") << "Active lbl : " << slbl << std::endl; + active_lbl[slbl] = true; + } + } } - needAddLemma = true; - TypeNode tn = getReferenceType(); - tn = nm->mkSetType(tn); - // tn = nm->mkSetType(nm->mkRefType(tn)); - Node o_b_lbl_mval = d_label_model[slbl].getValue(tn); - Trace("sep-process") << " Model for " << slbl << " : " << o_b_lbl_mval - << std::endl; + } + } - // get model values - std::map mvals; - for (const std::pair& sub_element : d_label_map[satom][slbl]) - { - int sub_index = sub_element.first; - Node sub_lbl = sub_element.second; - computeLabelModel(sub_lbl); - Node lbl_mval = d_label_model[sub_lbl].getValue(tn); - Trace("sep-process-debug") - << " child " << sub_index << " : " << sub_lbl - << ", mval = " << lbl_mval << std::endl; - mvals[sub_index] = lbl_mval; - } + // process spatial assertions + for (NodeList::const_iterator i = d_spatial_assertions.begin(); + i != d_spatial_assertions.end(); + ++i) + { + Node fact = (*i); + bool polarity = fact.getKind() != NOT; + TNode atom = polarity ? fact : fact[0]; + TNode satom = atom[0]; - // Now, assert model-instantiated implication based on the negation - Assert(d_label_model.find(slbl) != d_label_model.end()); - std::vector conc; - bool inst_success = true; - // new refinement - // instantiate the label - std::map visited; - Node inst = instantiateLabel(satom, - slbl, - slbl, - o_b_lbl_mval, - visited, - d_pto_model, - tn, - active_lbl); - Trace("sep-inst-debug") << " applied inst : " << inst << std::endl; - if (inst.isNull()) + bool use_polarity = satom.getKind() == SEP_WAND ? !polarity : polarity; + Trace("sep-process-debug") << " check atom : " << satom << " use polarity " + << use_polarity << std::endl; + if (use_polarity) + { + continue; + } + Assert(assert_active.find(fact) != assert_active.end()); + if (!assert_active[fact]) + { + Trace("sep-process-debug") + << "--> inactive negated assertion " << satom << std::endl; + continue; + } + Assert(atom.getKind() == SEP_LABEL); + TNode slbl = atom[1]; + Trace("sep-process") << "--> Active negated atom : " << satom + << ", lbl = " << slbl << std::endl; + // add refinement lemma + if (!ContainsKey(d_label_map[satom], slbl)) + { + Trace("sep-process-debug") << " no children." << std::endl; + Assert(satom.getKind() == SEP_PTO || satom.getKind() == SEP_EMP); + continue; + } + needAddLemma = true; + TypeNode tn = getReferenceType(); + tn = nm->mkSetType(tn); + // tn = nm->mkSetType(nm->mkRefType(tn)); + Node o_b_lbl_mval = d_label_model[slbl].getValue(tn); + Trace("sep-process") << " Model for " << slbl << " : " << o_b_lbl_mval + << std::endl; + + // get model values + std::map mvals; + for (const std::pair& sub_element : + d_label_map[satom][slbl]) + { + int sub_index = sub_element.first; + Node sub_lbl = sub_element.second; + computeLabelModel(sub_lbl); + Node lbl_mval = d_label_model[sub_lbl].getValue(tn); + Trace("sep-process-debug") << " child " << sub_index << " : " << sub_lbl + << ", mval = " << lbl_mval << std::endl; + mvals[sub_index] = lbl_mval; + } + + // Now, assert model-instantiated implication based on the negation + Assert(d_label_model.find(slbl) != d_label_model.end()); + std::vector conc; + bool inst_success = true; + // new refinement + // instantiate the label + std::map visited; + Node inst = instantiateLabel( + satom, slbl, slbl, o_b_lbl_mval, visited, d_pto_model, tn, active_lbl); + Trace("sep-inst-debug") << " applied inst : " << inst << std::endl; + if (inst.isNull()) + { + inst_success = false; + } + else + { + inst = rewrite(inst); + if (inst == (polarity ? d_true : d_false)) { inst_success = false; } - else - { - inst = rewrite(inst); - if (inst == (polarity ? d_true : d_false)) - { - inst_success = false; - } - conc.push_back(polarity ? inst : inst.negate()); - } - if (!inst_success) - { - continue; - } - std::vector lemc; - Node pol_atom = atom; - if (polarity) - { - pol_atom = atom.negate(); - } - lemc.push_back(pol_atom); - lemc.insert(lemc.end(), conc.begin(), conc.end()); - Node lem = nm->mkNode(OR, lemc); - std::vector& rlems = d_refinement_lem[satom][slbl]; - if (std::find(rlems.begin(), rlems.end(), lem) == rlems.end()) - { - rlems.push_back(lem); - Trace("sep-process") << "-----> refinement lemma (#" << rlems.size() - << ") : " << lem << std::endl; - Trace("sep-lemma") << "Sep::Lemma : negated star/wand refinement : " - << lem << std::endl; - d_im.lemma(lem, InferenceId::SEP_REFINEMENT); - addedLemma = true; - } - else - { - // this typically should not happen, should never happen for complete - // base theories - Trace("sep-process") - << "*** repeated refinement lemma : " << lem << std::endl; - Trace("sep-warn") - << "TheorySep : WARNING : repeated refinement lemma : " << lem - << "!!!" << std::endl; - } + conc.push_back(polarity ? inst : inst.negate()); + } + if (!inst_success) + { + continue; + } + std::vector lemc; + Node pol_atom = atom; + if (polarity) + { + pol_atom = atom.negate(); + } + lemc.push_back(pol_atom); + lemc.insert(lemc.end(), conc.begin(), conc.end()); + Node lem = nm->mkNode(OR, lemc); + std::vector& rlems = d_refinement_lem[satom][slbl]; + if (std::find(rlems.begin(), rlems.end(), lem) == rlems.end()) + { + rlems.push_back(lem); + Trace("sep-process") << "-----> refinement lemma (#" << rlems.size() + << ") : " << lem << std::endl; + Trace("sep-lemma") << "Sep::Lemma : negated star/wand refinement : " + << lem << std::endl; + d_im.lemma(lem, InferenceId::SEP_REFINEMENT); + addedLemma = true; + } + else + { + // this typically should not happen, should never happen for complete + // base theories + Trace("sep-process") << "*** repeated refinement lemma : " << lem + << std::endl; + Trace("sep-warn") << "TheorySep : WARNING : repeated refinement lemma : " + << lem << "!!!" << std::endl; } - Trace("sep-process") - << "...finished check of negated assertions, addedLemma=" << addedLemma - << ", needAddLemma=" << needAddLemma << std::endl; } + Trace("sep-process") << "...finished check of negated assertions, addedLemma=" + << addedLemma << ", needAddLemma=" << needAddLemma + << std::endl; + if (addedLemma) { return; @@ -1209,7 +1204,7 @@ Node TheorySep::getBaseLabel( TypeNode tn ) { tn_is_monotonic = tn.getCardinality().isInfinite(); } //add a reference type for maximum occurrences of empty in a constraint - if (options().sep.sepDisequalC && tn_is_monotonic) + if (tn_is_monotonic) { for( unsigned r=0; r 1); conj.push_back( NodeManager::currentNM()->mkNode( kind::AND, bchildren ) ); - - if (options().sep.sepChildRefine) - { - //child-specific refinements (TODO: use ?) - for( unsigned i=0; i tchildren; - Node mval = mvals[i]; - tchildren.push_back(NodeManager::currentNM()->mkNode( - kind::SET_SUBSET, mval, lbl)); - tchildren.push_back( children[i] ); - std::vector< Node > rem_children; - for( unsigned j=0; j rvisited; - Node rem = rem_children.size()==1 ? rem_children[0] : NodeManager::currentNM()->mkNode( kind::SEP_STAR, rem_children ); - rem = applyLabel( - rem, - NodeManager::currentNM()->mkNode(kind::SET_MINUS, lbl, mval), - rvisited); - tchildren.push_back( rem ); - conj.push_back( NodeManager::currentNM()->mkNode( kind::AND, tchildren ) ); - } - } - return conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( kind::OR, conj ); + return NodeManager::currentNM()->mkOr(conj); }else{ std::vector< Node > wchildren; //disjoint constraints -- 2.30.2