theory/quantifiers/fmf/model_builder.h \
theory/quantifiers/fmf/model_engine.cpp \
theory/quantifiers/fmf/model_engine.h \
- theory/quantifiers/fun_def_engine.cpp \
- theory/quantifiers/fun_def_engine.h \
theory/quantifiers/fun_def_process.cpp \
theory/quantifiers/fun_def_process.h \
theory/quantifiers/global_negate.cpp \
theory/quantifiers/quant_conflict_find.h \
theory/quantifiers/quant_epr.cpp \
theory/quantifiers/quant_epr.h \
- theory/quantifiers/quant_equality_engine.cpp \
- theory/quantifiers/quant_equality_engine.h \
theory/quantifiers/quant_relevance.cpp \
theory/quantifiers/quant_relevance.h \
theory/quantifiers/quant_split.cpp \
includes = ["options/quantifiers_modes.h"]
help = "selection mode for representatives in quantifiers engine"
-[[option]]
- name = "instRelevantCond"
- category = "regular"
- long = "inst-rlv-cond"
- type = "bool"
- default = "false"
- read_only = true
- help = "add relevancy conditions for instantiations"
-
[[option]]
name = "fullSaturateQuant"
category = "regular"
default = "false"
help = "perform anti-skolemization for quantified formulas"
-### e-unification options
-
-[[option]]
- name = "quantEqualityEngine"
- category = "regular"
- long = "quant-ee"
- type = "bool"
- default = "false"
- read_only = true
- help = "maintain congrunce closure over universal equalities"
-
### Higher-order options
[[option]]
read_only = true
help = "tells the uf strong solver to only consider models that interpret uninterpreted sorts of cardinality at most N (-1 == no limit, default)"
-[[option]]
- name = "ufssExplainedCliques"
- category = "regular"
- long = "uf-ss-explained-cliques"
- type = "bool"
- default = "false"
- read_only = true
- help = "use explained clique lemmas for uf strong solver"
-
-[[option]]
- name = "ufssSimpleCliques"
- category = "regular"
- long = "uf-ss-simple-cliques"
- type = "bool"
- default = "true"
- read_only = true
- help = "always use simple clique lemmas for uf strong solver"
-
-[[option]]
- name = "ufssDiseqPropagation"
- category = "regular"
- long = "uf-ss-deq-prop"
- type = "bool"
- default = "false"
- read_only = true
- help = "eagerly propagate disequalities for uf strong solver"
-
[[option]]
name = "ufssMode"
category = "regular"
+++ /dev/null
-/********************* */
-/*! \file fun_def_engine.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 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
- **
- ** This class implements specialized techniques for (recursively) defined functions
- **/
-
-#include <vector>
-
-#include "theory/quantifiers/fun_def_engine.h"
-#include "theory/rewriter.h"
-#include "theory/quantifiers/term_database.h"
-
-using namespace CVC4;
-using namespace std;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace CVC4::kind;
-
-FunDefEngine::FunDefEngine( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ) {
-
-}
-
-/* whether this module needs to check this round */
-bool FunDefEngine::needsCheck( Theory::Effort e ) {
- return e>=Theory::EFFORT_LAST_CALL;
-}
-
-/* reset at a round */
-void FunDefEngine::reset_round( Theory::Effort e ){
- //TODO
-}
-
-/* Call during quantifier engine's check */
-void FunDefEngine::check(Theory::Effort e, QEffort quant_e)
-{
- //TODO
-}
-
-/* Called for new quantifiers */
-void FunDefEngine::registerQuantifier( Node q ) {
- //TODO
-}
-
-/** called for everything that gets asserted */
-void FunDefEngine::assertNode( Node n ) {
- //TODO
-}
+++ /dev/null
-/********************* */
-/*! \file fun_def_engine.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 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 Specialized techniques for (recursively) defined functions
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__QUANTIFIERS_FUN_DEF_ENGINE_H
-#define __CVC4__QUANTIFIERS_FUN_DEF_ENGINE_H
-
-#include <iostream>
-#include <string>
-#include <vector>
-#include <map>
-#include "expr/node.h"
-#include "expr/type_node.h"
-#include "theory/quantifiers_engine.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-//module for handling (recursively) defined functions
-class FunDefEngine : public QuantifiersModule {
-private:
-
-public:
- FunDefEngine( QuantifiersEngine * qe, context::Context* c );
- ~FunDefEngine(){}
-
- /* whether this module needs to check this round */
- bool needsCheck(Theory::Effort e) override;
- /* reset at a round */
- void reset_round(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;
- /** called for everything that gets asserted */
- void assertNode(Node n) override;
- /** Identify this module (for debugging, dynamic configuration, etc..) */
- std::string identify() const override { return "FunDefEngine"; }
-};
-
-
-}
-}
-}
-
-#endif
}
Node lem = NodeManager::currentNM()->mkNode(kind::OR, q.negate(), body);
-
- // get relevancy conditions
- if (options::instRelevantCond())
- {
- std::vector<Node> rlv_cond;
- for (Node& t : terms)
- {
- quantifiers::TermUtil::getRelevancyCondition(t, rlv_cond);
- }
- if (!rlv_cond.empty())
- {
- rlv_cond.push_back(lem);
- lem = NodeManager::currentNM()->mkNode(kind::OR, rlv_cond);
- }
- }
-
lem = Rewriter::rewrite(lem);
// check for lemma duplication
+++ /dev/null
-/********************* */
-/*! \file quant_equality_engine.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 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
- **
- ** Congruence closure with free variables
- **/
-
-#include <vector>
-
-#include "theory/quantifiers/quant_equality_engine.h"
-#include "theory/rewriter.h"
-#include "theory/quantifiers/term_util.h"
-
-using namespace CVC4;
-using namespace std;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace CVC4::kind;
-
-QuantEqualityEngine::QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c ) :
-QuantifiersModule( qe ),
-d_notify( *this ),
-d_uequalityEngine(d_notify, c, "theory::quantifiers::QuantEqualityEngine", true),
-d_conflict(c, false),
-d_quant_red(c),
-d_quant_unproc(c){
- d_uequalityEngine.addFunctionKind( kind::APPLY_UF );
- d_intType = NodeManager::currentNM()->integerType();
-}
-
-void QuantEqualityEngine::conflict(TNode t1, TNode t2) {
- //report conflict through quantifiers engine output channel
- std::vector<TNode> assumptions;
- d_uequalityEngine.explainEquality(t1, t2, true, assumptions, NULL);
- Node conflict;
- if( assumptions.size()==1 ){
- conflict = assumptions[0];
- }else{
- conflict = NodeManager::currentNM()->mkNode( AND, assumptions );
- }
- d_conflict = true;
- Trace("qee-conflict") << "Quantifier equality engine conflict : " << conflict << std::endl;
- d_quantEngine->getOutputChannel().conflict( conflict );
-}
-
-void QuantEqualityEngine::eqNotifyNewClass(TNode t){
-
-}
-void QuantEqualityEngine::eqNotifyPreMerge(TNode t1, TNode t2){
-
-}
-void QuantEqualityEngine::eqNotifyPostMerge(TNode t1, TNode t2){
-
-}
-void QuantEqualityEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
-
-}
-
-/* whether this module needs to check this round */
-bool QuantEqualityEngine::needsCheck( Theory::Effort e ) {
- return e>=Theory::EFFORT_LAST_CALL;
-}
-
-/* reset at a round */
-void QuantEqualityEngine::reset_round( Theory::Effort e ){
- //TODO
-}
-
-/* Call during quantifier engine's check */
-void QuantEqualityEngine::check(Theory::Effort e, QEffort quant_e)
-{
- //TODO
-}
-
-/* Called for new quantifiers */
-void QuantEqualityEngine::registerQuantifier( Node q ) {
- //TODO
-}
-
-/** called for everything that gets asserted */
-void QuantEqualityEngine::assertNode( Node n ) {
- Assert( n.getKind()==FORALL );
- Trace("qee-debug") << "QEE assert : " << n << std::endl;
- if( !d_conflict ){
- Node lit = n[1].getKind()==NOT ? n[1][0] : n[1];
- bool pol = n[1].getKind()!=NOT;
- bool success = true;
- Node t1;
- Node t2;
- if( lit.getKind()==APPLY_UF || lit.getKind()==EQUAL ){
- lit = getTermUtil()->getCanonicalTerm( lit );
- Trace("qee-debug") << "Canonical : " << lit << ", pol = " << pol << std::endl;
- if( lit.getKind()==APPLY_UF ){
- t1 = getFunctionAppForPredicateApp( lit );
- t2 = pol ? getTermUtil()->d_one : getTermUtil()->d_zero;
- pol = true;
- lit = NodeManager::currentNM()->mkNode( EQUAL, t1, t2 );
- }else if( lit.getKind()==EQUAL ){
- if( lit[0].getType().isBoolean() ){
- if( lit[0].getKind()==NOT ){
- t1 = lit[0][0];
- pol = !pol;
- }else{
- t1 = lit[0];
- }
- if( lit[1].getKind()==NOT ){
- t2 = lit[1][0];
- pol = !pol;
- }else{
- t2 = lit[1];
- }
- if( t1.getKind()==APPLY_UF && t2.getKind()==APPLY_UF ){
- t1 = getFunctionAppForPredicateApp( t1 );
- t2 = getFunctionAppForPredicateApp( t2 );
- lit = NodeManager::currentNM()->mkNode( EQUAL, t1, t2 );
- }else{
- success = false;
- }
- }else{
- t1 = lit[0];
- t2 = lit[1];
- }
- }
- }else{
- success = false;
- }
- if( success ){
- bool alreadyHolds = false;
- if( pol && areUnivEqualInternal( t1, t2 ) ){
- alreadyHolds = true;
- }else if( !pol && areUnivDisequalInternal( t1, t2 ) ){
- alreadyHolds = true;
- }
-
- if( alreadyHolds ){
- d_quant_red.push_back( n );
- Trace("qee-debug") << "...add to redundant" << std::endl;
- }else{
- Trace("qee-debug") << "...assert" << std::endl;
- Trace("qee-assert") << "QEE : assert : " << lit << ", pol = " << pol << ", kind = " << lit.getKind() << std::endl;
- if( lit.getKind()==APPLY_UF ){
- d_uequalityEngine.assertPredicate(lit, pol, n);
- }else{
- d_uequalityEngine.assertEquality(lit, pol, n);
- }
- }
- }else{
- d_quant_unproc[n] = true;
- Trace("qee-debug") << "...add to unprocessed (" << lit.getKind() << ")" << std::endl;
- }
- }
-}
-
-bool QuantEqualityEngine::areUnivDisequalInternal( TNode n1, TNode n2 ) {
- return n1!=n2 && d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areDisequal( n1, n2, false );
-}
-
-bool QuantEqualityEngine::areUnivEqualInternal( TNode n1, TNode n2 ) {
- return n1==n2 || ( d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areEqual( n1, n2 ) );
-}
-
-TNode QuantEqualityEngine::getUnivRepresentativeInternal( TNode n ) {
- if( d_uequalityEngine.hasTerm( n ) ){
- return d_uequalityEngine.getRepresentative( n );
- }else{
- return n;
- }
-}
-bool QuantEqualityEngine::areUnivDisequal( TNode n1, TNode n2 ) {
- //TODO: must convert to internal representation
- return areUnivDisequalInternal( n1, n2 );
-}
-
-bool QuantEqualityEngine::areUnivEqual( TNode n1, TNode n2 ) {
- //TODO: must convert to internal representation
- return areUnivEqualInternal( n1, n2 );
-}
-
-TNode QuantEqualityEngine::getUnivRepresentative( TNode n ) {
- //TODO: must convert to internal representation
- return getUnivRepresentativeInternal( n );
-}
-
-Node QuantEqualityEngine::getFunctionForPredicate( Node f ) {
- std::map< Node, Node >::iterator it = d_pred_to_func.find( f );
- if( it==d_pred_to_func.end() ){
- std::vector< TypeNode > argTypes;
- TypeNode tn = f.getType();
- for( unsigned i=0; i<(tn.getNumChildren()-1); i++ ){
- argTypes.push_back( tn[i] );
- }
- TypeNode ftn = NodeManager::currentNM()->mkFunctionType( argTypes, d_intType );
- std::stringstream ss;
- ss << "ee_" << f;
- Node op = NodeManager::currentNM()->mkSkolem( ss.str(), ftn, "op created for internal ee" );
- d_pred_to_func[f] = op;
- return op;
- }else{
- return it->second;
- }
-}
-
-Node QuantEqualityEngine::getFunctionAppForPredicateApp( Node n ) {
- Assert( n.getKind()==APPLY_UF );
- std::vector< Node > children;
- children.push_back( getFunctionForPredicate( n.getOperator() ) );
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- children.push_back( n[i] );
- }
- return NodeManager::currentNM()->mkNode( APPLY_UF, children );
-}
-
+++ /dev/null
-/********************* */
-/*! \file quant_equality_engine.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds, Paul Meng, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 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 Congruence closure with free variables
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__QUANTIFIERS_EQUALITY_ENGINE_H
-#define __CVC4__QUANTIFIERS_EQUALITY_ENGINE_H
-
-#include <iostream>
-#include <string>
-#include <vector>
-#include <map>
-#include "expr/node.h"
-#include "expr/type_node.h"
-#include "theory/quantifiers_engine.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class QuantEqualityEngine : public QuantifiersModule {
- typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
-private:
- //notification class for equality engine
- class NotifyClass : public eq::EqualityEngineNotify {
- QuantEqualityEngine& d_qee;
- public:
- NotifyClass(QuantEqualityEngine& qee): d_qee(qee) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) override
- {
- return true;
- }
- bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
- {
- return true;
- }
- bool eqNotifyTriggerTermEquality(TheoryId tag,
- TNode t1,
- TNode t2,
- bool value) override
- {
- return true;
- }
- void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
- {
- d_qee.conflict(t1, t2);
- }
- void eqNotifyNewClass(TNode t) override { d_qee.eqNotifyNewClass(t); }
- void eqNotifyPreMerge(TNode t1, TNode t2) override
- {
- d_qee.eqNotifyPreMerge(t1, t2);
- }
- void eqNotifyPostMerge(TNode t1, TNode t2) override
- {
- d_qee.eqNotifyPostMerge(t1, t2);
- }
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
- {
- d_qee.eqNotifyDisequal(t1, t2, reason);
- }
- };/* class ConjectureGenerator::NotifyClass */
- /** The notify class */
- NotifyClass d_notify;
- /** (universal) equaltity engine */
- eq::EqualityEngine d_uequalityEngine;
- /** Are we in conflict */
- context::CDO<bool> d_conflict;
- /** list of redundant quantifiers in current context */
- context::CDList<Node> d_quant_red;
- /** unprocessed quantifiers in current context */
- NodeBoolMap d_quant_unproc;
- // map predicates to functions over int
- TypeNode d_intType;
- std::map< Node, Node > d_pred_to_func;
- Node getFunctionForPredicate( Node f );
- Node getFunctionAppForPredicateApp( Node n );
-private:
- void conflict(TNode t1, TNode t2);
- void eqNotifyNewClass(TNode t);
- void eqNotifyPreMerge(TNode t1, TNode t2);
- void eqNotifyPostMerge(TNode t1, TNode t2);
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
- //queries
- bool areUnivDisequalInternal( TNode n1, TNode n2 );
- bool areUnivEqualInternal( TNode n1, TNode n2 );
- TNode getUnivRepresentativeInternal( TNode n );
-public:
- QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c );
-
- /* whether this module needs to check this round */
- bool needsCheck(Theory::Effort e) override;
- /* reset at a round */
- void reset_round(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;
- /** called for everything that gets asserted */
- void assertNode(Node n) override;
- /** Identify this module (for debugging, dynamic configuration, etc..) */
- std::string identify() const override { return "QuantEqualityEngine"; }
- /** queries */
- bool areUnivDisequal( TNode n1, TNode n2 );
- bool areUnivEqual( TNode n1, TNode n2 );
- TNode getUnivRepresentative( TNode n );
-};
-
-
-}
-}
-}
-
-#endif
#include "options/quantifiers_options.h"
#include "theory/arith/arith_msum.h"
-#include "theory/quantifiers/fun_def_engine.h"
#include "theory/quantifiers/rewrite_engine.h"
#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
#include "theory/quantifiers/term_util.h"
AlwaysAssert(false);
}
d_fun_defs[f] = true;
- d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine(), 2 );
}
if( d_qattr[q].d_sygus ){
if( d_quantEngine->getCegInstantiation()==NULL ){
}
}
-void TermUtil::getRelevancyCondition( Node n, std::vector< Node >& cond ) {
- if( n.getKind()==APPLY_SELECTOR_TOTAL ){
- // don't worry about relevancy conditions if using shared selectors
- if( !options::dtSharedSelectors() ){
- unsigned scindex = Datatype::cindexOf(n.getOperator().toExpr());
- const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype();
- Node rc = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[scindex].getTester() ), n[0] ).negate();
- if( std::find( cond.begin(), cond.end(), rc )==cond.end() ){
- cond.push_back( rc );
- }
- getRelevancyCondition( n[0], cond );
- }
- }
-}
-
bool TermUtil::containsTerm2( Node n, Node t, std::map< Node, bool >& visited ) {
if( n==t ){
return true;
bool containsVtsInfinity( Node n, bool isFree = false );
/** ensure type */
static Node ensureType( Node n, TypeNode tn );
- /** get relevancy condition */
- static void getRelevancyCondition( Node n, std::vector< Node >& cond );
//general utilities
// TODO #1216 : promote these?
#include "theory/quantifiers/equality_query.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/fmf/full_model_check.h"
-#include "theory/quantifiers/fun_def_engine.h"
#include "theory/quantifiers/inst_propagator.h"
#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h"
#include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
#include "theory/quantifiers/fmf/model_engine.h"
#include "theory/quantifiers/quant_conflict_find.h"
#include "theory/quantifiers/quant_epr.h"
-#include "theory/quantifiers/quant_equality_engine.h"
#include "theory/quantifiers/quant_relevance.h"
#include "theory/quantifiers/quant_split.h"
#include "theory/quantifiers/quantifiers_attributes.h"
d_ceg_inst = NULL;
d_lte_part_inst = NULL;
d_alpha_equiv = NULL;
- d_fun_def_engine = NULL;
- d_uee = NULL;
d_fs = NULL;
d_rel_dom = NULL;
d_bv_invert = NULL;
if( options::quantAlphaEquiv() ){
d_alpha_equiv = new quantifiers::AlphaEquivalence( this );
}
- //if( options::funDefs() ){
- // d_fun_def_engine = new quantifiers::FunDefEngine( this, c );
- // d_modules.push_back( d_fun_def_engine );
- //}
- if( options::quantEqualityEngine() ){
- d_uee = new quantifiers::QuantEqualityEngine( this, c );
- d_modules.push_back( d_uee );
- }
//full saturation : instantiate from relevant domain, then arbitrary terms
if( options::fullSaturateQuant() || options::fullSaturateInterleave() ){
d_fs = new quantifiers::InstStrategyEnum(this);
delete d_sg_gen;
delete d_ceg_inst;
delete d_lte_part_inst;
- delete d_fun_def_engine;
- delete d_uee;
delete d_fs;
delete d_i_cbqi;
delete d_qsplit;
class CegInstantiation;
class LtePartialInst;
class AlphaEquivalence;
- class FunDefEngine;
- class QuantEqualityEngine;
class InstStrategyEnum;
class InstStrategyCbqi;
class InstStrategyCegqi;
quantifiers::CegInstantiation * d_ceg_inst;
/** lte partial instantiation */
quantifiers::LtePartialInst * d_lte_part_inst;
- /** function definitions engine */
- quantifiers::FunDefEngine * d_fun_def_engine;
- /** quantifiers equality engine */
- quantifiers::QuantEqualityEngine * d_uee;
/** full saturation */
quantifiers::InstStrategyEnum* d_fs;
/** counterexample-based quantifier instantiation */
quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; }
/** local theory ext partial inst */
quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; }
- /** function definition engine */
- quantifiers::FunDefEngine * getFunDefEngine() { return d_fun_def_engine; }
- /** quantifiers equality engine */
- quantifiers::QuantEqualityEngine * getQuantEqualityEngine() { return d_uee; }
/** get full saturation */
quantifiers::InstStrategyEnum* getInstStrategyEnum() { return d_fs; }
/** get inst strategy cbqi */
}
}
-Node TheoryStrings::normalizeRegexp(Node r) {
- if (d_nf_regexps.find(r) != d_nf_regexps.end()) {
- return d_nf_regexps[r];
- }
- Assert(d_nf_regexps.count(r) == 0);
- Node nf_r = r;
- std::vector<Node> nf_exp;
- if (!d_regexp_opr.checkConstRegExp(r)) {
- switch (r.getKind()) {
- case kind::REGEXP_EMPTY:
- case kind::REGEXP_SIGMA: {
- break;
- }
- case kind::STRING_TO_REGEXP: {
- if (!r[0].isConst() &&
- d_normal_forms.find(r[0]) != d_normal_forms.end()) {
- nf_r = mkConcat(d_normal_forms[r[0]]);
- Debug("regexp-nf")
- << "Term: " << r[0] << " has a normal form " << nf_r << std::endl;
- const std::vector<Node>& r0_exp = d_normal_forms_exp[r[0]];
- nf_exp.insert(nf_exp.end(), r0_exp.begin(), r0_exp.end());
- nf_r = Rewriter::rewrite(
- NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, nf_r));
- }
- break;
- }
- case kind::REGEXP_CONCAT:
- case kind::REGEXP_UNION:
- case kind::REGEXP_INTER: {
- bool flag = false;
- std::vector<Node> vec_nodes;
- for (unsigned i = 0; i < r.getNumChildren(); ++i) {
- Node rtmp = normalizeRegexp(r[i]);
- vec_nodes.push_back(rtmp);
- if (rtmp != r[i]) {
- flag = true;
- }
- }
- if (flag) {
- Node rtmp = vec_nodes.size() == 1 ? vec_nodes[0]
- : NodeManager::currentNM()->mkNode(
- r.getKind(), vec_nodes);
- nf_r = Rewriter::rewrite(rtmp);
- }
- break;
- }
- case kind::REGEXP_STAR: {
- Node rtmp = normalizeRegexp(r[0]);
- if (rtmp != r[0]) {
- rtmp = NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, rtmp);
- nf_r = Rewriter::rewrite(rtmp);
- }
- break;
- }
- default: { Unreachable(); }
- }
- }
- d_nf_regexps[r] = nf_r;
- d_nf_regexps_exp[r] = nf_exp;
- return nf_r;
-}
-
-bool TheoryStrings::normalizePosMemberships(std::map< Node, std::vector< Node > > &memb_with_exps) {
- std::map< Node, std::vector< Node > > unprocessed_x_exps;
- std::map< Node, std::vector< Node > > unprocessed_memberships;
- std::map< Node, std::vector< Node > > unprocessed_memberships_bases;
- bool addLemma = false;
-
- Trace("regexp-check") << "Normalizing Positive Memberships ... " << std::endl;
-
- for( NodeIntMap::const_iterator itr_xr = d_pos_memberships.begin(); itr_xr != d_pos_memberships.end(); ++itr_xr ){
- Node x = (*itr_xr).first;
- Node nf_x = x;
- std::vector< Node > nf_x_exp;
- if(d_normal_forms.find( x ) != d_normal_forms.end()) {
- //nf_x = mkConcat( d_normal_forms[x] );
- nf_x_exp.insert(nf_x_exp.end(), d_normal_forms_exp[x].begin(), d_normal_forms_exp[x].end());
- //Debug("regexp-nf") << "Term: " << x << " has a normal form " << ret << std::endl;
- } else {
- Assert(false);
- }
- Trace("regexp-nf") << "Checking Memberships for N(" << x << ") = " << nf_x << " :" << std::endl;
-
- std::vector< Node > vec_x;
- std::vector< Node > vec_r;
- unsigned n_pmem = (*itr_xr).second;
- Assert( getNumMemberships( x, true )==n_pmem );
- for( unsigned k=0; k<n_pmem; k++ ){
- Node r = getMembership( x, true, k );
- Node nf_r = normalizeRegexp( r ); //AJR: fixed (was normalizing mem #0 always)
- Node memb = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, nf_x, nf_r);
- if(d_processed_memberships.find(memb) == d_processed_memberships.end()) {
- if(d_regexp_opr.checkConstRegExp(nf_r)) {
- vec_x.push_back(x);
- vec_r.push_back(r);
- } else {
- Trace("regexp-nf") << "Handling Symbolic Regexp for N(" << r << ") = " << nf_r << std::endl;
- //TODO: handle symbolic ones
- addLemma = true;
- }
- d_processed_memberships.insert(memb);
- }
- }
- if(!vec_x.empty()) {
- if(unprocessed_x_exps.find(nf_x) == unprocessed_x_exps.end()) {
- unprocessed_x_exps[nf_x] = nf_x_exp;
- unprocessed_memberships[nf_x] = vec_r;
- unprocessed_memberships_bases[nf_x] = vec_x;
- } else {
- unprocessed_x_exps[nf_x].insert(unprocessed_x_exps[nf_x].end(), nf_x_exp.begin(), nf_x_exp.end());
- unprocessed_memberships[nf_x].insert(unprocessed_memberships[nf_x].end(), vec_r.begin(), vec_r.end());
- unprocessed_memberships_bases[nf_x].insert(unprocessed_memberships_bases[nf_x].end(), vec_x.begin(), vec_x.end());
- }
- }
- }
- //Intersection
- for(std::map< Node, std::vector< Node > >::const_iterator itr = unprocessed_memberships.begin();
- itr != unprocessed_memberships.end(); ++itr) {
- Node nf_x = itr->first;
- std::vector< Node > exp( unprocessed_x_exps[nf_x] );
- Node r = itr->second[0];
- //get nf_r
- Node inter_r = d_nf_regexps[r];
- exp.insert(exp.end(), d_nf_regexps_exp[r].begin(), d_nf_regexps_exp[r].end());
- Node x = unprocessed_memberships_bases[itr->first][0];
- Node memb = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r);
- exp.push_back(memb);
- for(std::size_t i=1; i < itr->second.size(); i++) {
- //exps
- Node r2 = itr->second[i];
- Node inter_r2 = d_nf_regexps[r2];
- exp.insert(exp.end(), d_nf_regexps_exp[r2].begin(), d_nf_regexps_exp[r2].end());
- Node x2 = unprocessed_memberships_bases[itr->first][i];
- memb = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x2, r2);
- exp.push_back(memb);
- //intersection
- bool spflag = false;
- inter_r = d_regexp_opr.intersect(inter_r, inter_r2, spflag);
- if(inter_r == d_emptyRegexp) {
- //conflict
- Node conc;
- sendInference( d_empty_vec, exp, conc, "INTERSECT CONFLICT", true );
- addLemma = true;
- break;
- }
- }
- //infer
- if(!d_conflict) {
- memb = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, nf_x, inter_r) );
- memb_with_exps[memb] = exp;
- } else {
- break;
- }
- }
-
- return addLemma;
-}
-
bool TheoryStrings::applyRConsume( CVC4::String &s, Node &r) {
Trace("regexp-derivative") << "TheoryStrings::derivative: s=" << s << ", r= " << r << std::endl;
Assert( d_regexp_opr.checkConstRegExp(r) );
}
}
-bool TheoryStrings::checkMembershipsWithoutLength(
- std::map< Node, std::vector< Node > > &memb_with_exps,
- std::map< Node, std::vector< Node > > &XinR_with_exps) {
- for(std::map< Node, std::vector< Node > >::iterator itr = memb_with_exps.begin(); itr != memb_with_exps.end(); ++itr) {
- Node memb = itr->first;
- Node s = memb[0];
- Node r = memb[1];
- if(s.isConst()) {
- memb = Rewriter::rewrite( memb );
- if(memb == d_false) {
- Node conc;
- sendInference(d_empty_vec, itr->second, conc, "MEMBERSHIP CONFLICT", true);
- //addLemma = true;
- return true;
- } else {
- Assert(memb == d_true);
- }
- } else if(s.getKind() == kind::VARIABLE) {
- //add to XinR
- XinR_with_exps[itr->first] = itr->second;
- } else {
- Assert(s.getKind() == kind::STRING_CONCAT);
- Node conc;
- for( unsigned i=0; i<s.getNumChildren(); i++ ) {
- if(s[i].isConst()) {
- CVC4::String str( s[0].getConst< String >() );
- //R-Consume, see Tianyi's thesis
- if(!applyRConsume(str, r)) {
- sendInference(d_empty_vec, itr->second, conc, "R-Consume CONFLICT", true);
- //addLemma = true;
- return true;
- }
- } else {
- //R-Split, see Tianyi's thesis
- if(i == s.getNumChildren() - 1) {
- //add to XinR
- Node memb2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s[i], r);
- XinR_with_exps[itr->first] = itr->second;
- } else {
- Node s1 = s[i];
- std::vector< Node > vec_s2;
- for( unsigned j=i+1; j<s.getNumChildren(); j++ ) {
- vec_s2.push_back(s[j]);
- }
- Node s2 = mkConcat(vec_s2);
- conc = applyRSplit(s1, s2, r);
- if(conc == d_true) {
- break;
- } else if(conc.isNull() || conc == d_false) {
- conc = Node::null();
- sendInference(d_empty_vec, itr->second, conc, "R-Split Conflict", true);
- //addLemma = true;
- return true;
- } else {
- sendInference(d_empty_vec, itr->second, conc, "R-Split", true);
- //addLemma = true;
- return true;
- }
- }
- }
- }
- }
- }
- return false;
-}
-
-bool TheoryStrings::checkMemberships2() {
- bool addedLemma = false;
- d_nf_regexps.clear();
- d_nf_regexps_exp.clear();
- std::map< Node, std::vector< Node > > memb_with_exps;
- std::map< Node, std::vector< Node > > XinR_with_exps;
-
- addedLemma = normalizePosMemberships( memb_with_exps );
- if(!d_conflict) {
- // main procedure
- addedLemma |= checkMembershipsWithoutLength( memb_with_exps, XinR_with_exps );
- //TODO: check addlemma
- if (!addedLemma && !d_conflict) {
- for(std::map< Node, std::vector< Node > >::const_iterator itr = XinR_with_exps.begin();
- itr != XinR_with_exps.end(); ++itr) {
- std::vector<Node> vec_or;
- d_regexp_opr.disjunctRegExp( itr->first, vec_or );
- Node tmp = NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_or);
- Trace("regexp-process") << "Got r: " << itr->first << " to " << tmp << std::endl;
- /*
- if(r.getKind() == kind::REGEXP_STAR) {
- //TODO: apply R-Len
- addedLemma = applyRLen(XinR_with_exps);
- } else {
- //TODO: split
- }
- */
- }
- Assert(false); //TODO:tmp
- }
- }
-
- return addedLemma;
-}
-
void TheoryStrings::checkMemberships() {
//add the memberships
std::vector<Node> mems = getExtTheory()->getActive(kind::STRING_IN_REGEXP);
Node xr = getRepresentative( x );
//Trace("strings-regexp") << xr << " is rep of " << x << std::endl;
//Assert( d_normal_forms.find( xr )!=d_normal_forms.end() );
- //TODO
- if( true || r.getKind()!=kind::REGEXP_STAR || ( d_normal_forms[xr].size()==1 && x.getKind()!=kind::STRING_CONCAT ) ){
- Trace("strings-regexp") << "Unroll/simplify membership of atomic term " << xr << std::endl;
- //if so, do simple unrolling
- std::vector< Node > nvec;
-
- /*if(xr.isConst()) {
- Node tmp = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, xr, r) );
- if(tmp==d_true || tmp==d_false) {
- if(!polarity) {
- tmp = tmp==d_true? d_false : d_true;
- }
- nvec.push_back( tmp );
- }
- }*/
-
- if(nvec.empty()) {
- d_regexp_opr.simplify(atom, nvec, polarity);
- }
- Node antec = assertion;
- if(d_regexp_ant.find(assertion) != d_regexp_ant.end()) {
- antec = d_regexp_ant[assertion];
- for(std::vector< Node >::const_iterator itr=nvec.begin(); itr<nvec.end(); itr++) {
- if(itr->getKind() == kind::STRING_IN_REGEXP) {
- if(d_regexp_ant.find( *itr ) == d_regexp_ant.end()) {
- d_regexp_ant[ *itr ] = antec;
- }
+ Trace("strings-regexp")
+ << "Unroll/simplify membership of atomic term " << xr
+ << std::endl;
+ // if so, do simple unrolling
+ std::vector<Node> nvec;
+
+ if (nvec.empty())
+ {
+ d_regexp_opr.simplify(atom, nvec, polarity);
+ }
+ Node antec = assertion;
+ if (d_regexp_ant.find(assertion) != d_regexp_ant.end())
+ {
+ antec = d_regexp_ant[assertion];
+ for (std::vector<Node>::const_iterator itr = nvec.begin();
+ itr < nvec.end();
+ itr++)
+ {
+ if (itr->getKind() == kind::STRING_IN_REGEXP)
+ {
+ if (d_regexp_ant.find(*itr) == d_regexp_ant.end())
+ {
+ d_regexp_ant[*itr] = antec;
}
}
}
- antec = NodeManager::currentNM()->mkNode(kind::AND, antec, mkExplain(rnfexp));
- Node conc = nvec.size()==1 ? nvec[0] : NodeManager::currentNM()->mkNode(kind::AND, nvec);
- conc = Rewriter::rewrite(conc);
- sendLemma( antec, conc, "REGEXP_Unfold" );
- addedLemma = true;
- if(changed) {
- cprocessed.push_back( assertion );
- } else {
- processed.push_back( assertion );
- }
- //d_regexp_ucached[assertion] = true;
- }else{
- Trace("strings-regexp") << "Unroll/simplify membership of non-atomic term " << xr << " = ";
- for( unsigned j=0; j<d_normal_forms[xr].size(); j++ ){
- Trace("strings-regexp") << d_normal_forms[xr][j] << " ";
- }
- Trace("strings-regexp") << ", polarity = " << polarity << std::endl;
- //otherwise, distribute unrolling over parts
- Node p1;
- Node p2;
- if( d_normal_forms[xr].size()>1 ){
- p1 = d_normal_forms[xr][0];
- std::vector< Node > cc;
- cc.insert( cc.begin(), d_normal_forms[xr].begin() + 1, d_normal_forms[xr].end() );
- p2 = mkConcat( cc );
- }
-
- Trace("strings-regexp-debug") << "Construct antecedant..." << std::endl;
- std::vector< Node > antec;
- std::vector< Node > antecn;
- antec.insert( antec.begin(), d_normal_forms_exp[xr].begin(), d_normal_forms_exp[xr].end() );
- if( x!=xr ){
- antec.push_back( x.eqNode( xr ) );
- }
- antecn.push_back( assertion );
- Node ant = mkExplain( antec, antecn );
- Trace("strings-regexp-debug") << "Construct conclusion..." << std::endl;
- Node conc;
- if( polarity ){
- if( d_normal_forms[xr].size()==0 ){
- conc = d_true;
- }else if( d_normal_forms[xr].size()==1 ){
- Trace("strings-regexp-debug") << "Case 1\n";
- conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, d_normal_forms[xr][0], r);
- }else{
- Trace("strings-regexp-debug") << "Case 2\n";
- std::vector< Node > conc_c;
- Node s11 = mkSkolemS( "s11" );
- Node s12 = mkSkolemS( "s12" );
- Node s21 = mkSkolemS( "s21" );
- Node s22 = mkSkolemS( "s22" );
- conc = p1.eqNode( mkConcat(s11, s12) );
- conc_c.push_back(conc);
- conc = p2.eqNode( mkConcat(s21, s22) );
- conc_c.push_back(conc);
- conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s11, r);
- conc_c.push_back(conc);
- conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, mkConcat(s12, s21), r[0]);
- conc_c.push_back(conc);
- conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s22, r);
- conc_c.push_back(conc);
- conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, conc_c));
- Node eqz = Rewriter::rewrite(x.eqNode(d_emptyString));
- conc = NodeManager::currentNM()->mkNode(kind::OR, eqz, conc);
- d_pending_req_phase[eqz] = true;
- }
- }else{
- if( d_normal_forms[xr].size()==0 ){
- conc = d_false;
- }else if( d_normal_forms[xr].size()==1 ){
- Trace("strings-regexp-debug") << "Case 3\n";
- conc = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, d_normal_forms[xr][0], r).negate();
- }else{
- Trace("strings-regexp-debug") << "Case 4\n";
- Node len1 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, p1);
- Node len2 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, p2);
- Node bi = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
- Node bj = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
- Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, bi, bj);
- Node g1 = NodeManager::currentNM()->mkNode(kind::AND,
- NodeManager::currentNM()->mkNode(kind::GEQ, bi, d_zero),
- NodeManager::currentNM()->mkNode(kind::GEQ, len1, bi),
- NodeManager::currentNM()->mkNode(kind::GEQ, bj, d_zero),
- NodeManager::currentNM()->mkNode(kind::GEQ, len2, bj));
- Node s11 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, p1, d_zero, bi);
- Node s12 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, p1, bi, NodeManager::currentNM()->mkNode(kind::MINUS, len1, bi));
- Node s21 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, p2, d_zero, bj);
- Node s22 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, p2, bj, NodeManager::currentNM()->mkNode(kind::MINUS, len2, bj));
- Node cc1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s11, r).negate();
- Node cc2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, mkConcat(s12, s21), r[0]).negate();
- Node cc3 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s22, r).negate();
- conc = NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2, cc3);
- conc = NodeManager::currentNM()->mkNode(kind::IMPLIES, g1, conc);
- conc = NodeManager::currentNM()->mkNode(kind::FORALL, b1v, conc);
- conc = NodeManager::currentNM()->mkNode(kind::AND, x.eqNode(d_emptyString).negate(), conc);
- }
- }
- if( conc!=d_true ){
- ant = mkRegExpAntec(assertion, ant);
- sendLemma(ant, conc, "REGEXP CSTAR");
- addedLemma = true;
- if( conc==d_false ){
- d_regexp_ccached.insert( assertion );
- }else{
- cprocessed.push_back( assertion );
- }
- }else{
- d_regexp_ccached.insert(assertion);
- }
}
+ antec = NodeManager::currentNM()->mkNode(
+ kind::AND, antec, mkExplain(rnfexp));
+ Node conc = nvec.size() == 1
+ ? nvec[0]
+ : NodeManager::currentNM()->mkNode(kind::AND, nvec);
+ conc = Rewriter::rewrite(conc);
+ sendLemma(antec, conc, "REGEXP_Unfold");
+ addedLemma = true;
+ if (changed)
+ {
+ cprocessed.push_back(assertion);
+ }
+ else
+ {
+ processed.push_back(assertion);
+ }
+ // d_regexp_ucached[assertion] = true;
}
}
if(d_conflict) {
//check membership constraints
Node mkRegExpAntec(Node atom, Node ant);
- Node normalizeRegexp(Node r);
- bool normalizePosMemberships( std::map< Node, std::vector< Node > > &memb_with_exps );
bool applyRConsume( CVC4::String &s, Node &r );
Node applyRSplit( Node s1, Node s2, Node r );
bool applyRLen( std::map< Node, std::vector< Node > > &XinR_with_exps );
- bool checkMembershipsWithoutLength( std::map< Node, std::vector< Node > > &memb_with_exps,
- std::map< Node, std::vector< Node > > &XinR_with_exps);
void checkMemberships();
- bool checkMemberships2();
bool checkPDerivative( Node x, Node r, Node atom, bool &addedLemma, std::vector< Node > &nf_exp);
//check contains
void checkPosContains( std::vector< Node >& posContains );
if( !isDisequal( a, n, t ) ){
setDisequal( a, n, t, true );
nr->setDisequal( n, a, t, true );
- //notify the disequality propagator
- if( options::ufssDiseqPropagation() ){
- d_cf->d_thss->getDisequalityPropagator()->assertDisequal(a, n, Node::null());
- }
if( options::ufssSymBreak() ){
d_cf->d_thss->getSymmetryBreaker()->assertDisequal( a, n );
}
d_reps = d_reps - 1;
if( !d_conflict ){
- if( options::ufssDiseqPropagation() ){
- //notify the disequality propagator
- d_thss->getDisequalityPropagator()->merge(a, b);
- }
if( options::ufssSymBreak() ){
d_thss->getSymmetryBreaker()->merge(a, b);
}
}
if( !d_conflict ){
- if( options::ufssDiseqPropagation() ){
- //notify the disequality propagator
- d_thss->getDisequalityPropagator()->assertDisequal(a, b, Node::null());
- }
if( options::ufssSymBreak() ){
d_thss->getSymmetryBreaker()->assertDisequal(a, b);
}
clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() );
addClique( d_cardinality, clique_vec );
}
- if( options::ufssSimpleCliques() && !options::ufssExplainedCliques() ){
- //add as lemma
- std::vector< Node > eqs;
- for( int i=0; i<(int)clique.size(); i++ ){
- for( int j=0; j<i; j++ ){
- Node r1 = d_thss->getTheory()->d_equalityEngine.getRepresentative(clique[i]);
- Node r2 = d_thss->getTheory()->d_equalityEngine.getRepresentative(clique[j]);
- eqs.push_back( clique[i].eqNode( clique[j] ) );
- }
- }
- eqs.push_back( d_cardinality_literal[ d_cardinality ].notNode() );
- Node lem = NodeManager::currentNM()->mkNode( OR, eqs );
- if( doSendLemma( lem ) ){
- Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl;
- ++( d_thss->d_statistics.d_clique_lemmas );
- }
- }else{
- //found a clique
- Debug("uf-ss-cliques") << "Found a clique (cardinality=" << d_cardinality << ") :" << std::endl;
- Debug("uf-ss-cliques") << " ";
- for( int i=0; i<(int)clique.size(); i++ ){
- Debug("uf-ss-cliques") << clique[i] << " ";
- }
- Debug("uf-ss-cliques") << std::endl;
- Debug("uf-ss-cliques") << "Finding clique disequalities..." << std::endl;
-
- //we will scan through each of the disequaltities
- bool isSatConflict = true;
- std::vector< Node > conflict;
- //collect disequalities, and nodes that must be equal within representatives
- std::map< Node, std::map< Node, bool > > explained;
- std::map< Node, std::map< Node, bool > > nodesWithinRep;
- //map from the reprorted clique members to those reported in the lemma
- std::map< Node, Node > cliqueRepMap;
- for( int i=0; i<(int)d_disequalities_index; i++ ){
- //if both sides of disequality exist in clique
- Node r1 = d_thss->getTheory()->d_equalityEngine.getRepresentative( d_disequalities[i][0][0] );
- Node r2 = d_thss->getTheory()->d_equalityEngine.getRepresentative( d_disequalities[i][0][1] );
- if( r1!=r2 && ( explained.find( r1 )==explained.end() || explained[r1].find( r2 )==explained[r1].end() ) &&
- std::find( clique.begin(), clique.end(), r1 )!=clique.end() &&
- std::find( clique.begin(), clique.end(), r2 )!=clique.end() ){
- explained[r1][r2] = true;
- explained[r2][r1] = true;
- if( options::ufssExplainedCliques() ){
- conflict.push_back( d_disequalities[i] );
- Debug("uf-ss-cliques") << " -> disequality : " << d_disequalities[i] << std::endl;
- nodesWithinRep[r1][ d_disequalities[i][0][0] ] = true;
- nodesWithinRep[r2][ d_disequalities[i][0][1] ] = true;
- }else{
- //get the terms we report in the lemma
- Node ru1 = r1;
- if( cliqueRepMap.find( r1 )==cliqueRepMap.end() ){
- ru1 = d_disequalities[i][0][0];
- cliqueRepMap[r1] = ru1;
- }else{
- ru1 = cliqueRepMap[r1];
- }
- Node ru2 = r2;
- if( cliqueRepMap.find( r2 )==cliqueRepMap.end() ){
- ru2 = d_disequalities[i][0][1];
- cliqueRepMap[r2] = ru2;
- }else{
- ru2 = cliqueRepMap[r2];
- }
- if( ru1!=d_disequalities[i][0][0] || ru2!=d_disequalities[i][0][1] ){
- //disequalities have endpoints that are not connected within an equivalence class
- // we will be producing a lemma, introducing a new literal ru1 != ru2
- conflict.push_back( ru1.eqNode( ru2 ).notNode() );
- isSatConflict = false;
- }else{
- conflict.push_back( d_disequalities[i] );
- }
- }
- if( conflict.size()==(clique.size()*( clique.size()-1 )/2) ){
- break;
- }
- }
+ // add as lemma
+ std::vector<Node> eqs;
+ for (unsigned i = 0, size = clique.size(); i < size; i++)
+ {
+ for (unsigned j = 0; j < i; j++)
+ {
+ eqs.push_back(clique[i].eqNode(clique[j]));
}
- if( options::ufssExplainedCliques() ){
- //Debug("uf-ss-cliques") << conflict.size() << " " << clique.size() << std::endl;
- Assert( (int)conflict.size()==((int)clique.size()*( (int)clique.size()-1 )/2) );
- //Assert( (int)conflict.size()==(int)clique.size()*( (int)clique.size()-1 )/2 );
- Debug("uf-ss-cliques") << "Finding clique equalities internal to eq classes..." << std::endl;
- //now, we must explain equalities within each equivalence class
- for( std::map< Node, std::map< Node, bool > >::iterator it = nodesWithinRep.begin(); it != nodesWithinRep.end(); ++it ){
- if( it->second.size()>1 ){
- Node prev;
- //add explanation of t1 = t2 = ... = tn
- Debug("uf-ss-cliques") << "Explain ";
- for( std::map< Node, bool >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
- if( prev!=Node::null() ){
- Debug("uf-ss-cliques") << " = ";
- //explain it2->first and prev
- std::vector< TNode > expl;
- d_thss->getTheory()->d_equalityEngine.explainEquality( it2->first, prev, true, expl );
- for( int i=0; i<(int)expl.size(); i++ ){
- if( std::find( conflict.begin(), conflict.end(), expl[i] )==conflict.end() ){
- conflict.push_back( expl[i] );
- }
- }
- }
- prev = it2->first;
- Debug("uf-ss-cliques") << prev;
- }
- Debug("uf-ss-cliques") << std::endl;
- }
- }
- Debug("uf-ss-cliques") << "Explanation of clique (size=" << conflict.size() << ") = " << std::endl;
- for( int i=0; i<(int)conflict.size(); i++ ){
- Debug("uf-ss-cliques") << conflict[i] << " ";
- }
- Debug("uf-ss-cliques") << std::endl;
- }
- //now, make the conflict
- if( isSatConflict ){
- conflict.push_back( d_cardinality_literal[ d_cardinality ] );
- Node conflictNode = NodeManager::currentNM()->mkNode( AND, conflict );
- Trace("uf-ss-lemma") << "*** Add clique conflict " << conflictNode << std::endl;
- //Notice() << "*** Add clique conflict " << conflictNode << std::endl;
- out->conflict( conflictNode );
- d_conflict = true;
- ++( d_thss->d_statistics.d_clique_conflicts );
- }else{
- Node conflictNode = conflict.size()==1 ? conflict[0] : NodeManager::currentNM()->mkNode( AND, conflict );
- //add cardinality constraint
- Node cardNode = d_cardinality_literal[ d_cardinality ];
- //bool value;
- //bool hasValue = d_th->getValuation().hasSatValue( cardNode, value );
- //Assert( hasValue );
- //Assert( value );
- conflictNode = NodeManager::currentNM()->mkNode( IMPLIES, conflictNode, cardNode.notNode() );
- if( doSendLemma( conflictNode ) ){
- Trace("uf-ss-lemma") << "*** Add clique lemma " << conflictNode << std::endl;
- ++( d_thss->d_statistics.d_clique_lemmas );
- }
- }
-
- //DO_THIS: ensure that the same clique is not reported??? Check standard effort after assertDisequal can produce same clique.
+ }
+ eqs.push_back(d_cardinality_literal[d_cardinality].notNode());
+ Node lem = NodeManager::currentNM()->mkNode(OR, eqs);
+ if (doSendLemma(lem))
+ {
+ Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl;
+ ++(d_thss->d_statistics.d_clique_lemmas);
}
}
d_card_assertions_eqv_lemma(u),
d_min_pos_tn_master_card(c, -1),
d_rel_eqc(c),
- d_deq_prop(NULL),
d_sym_break(NULL) {
- if (options::ufssDiseqPropagation()) {
- d_deq_prop = new DisequalityPropagator(th->getQuantifiersEngine(), this);
- }
if (options::ufssSymBreak()) {
d_sym_break = new SubsortSymmetryBreaker(th->getQuantifiersEngine(), c);
}
if (d_sym_break) {
delete d_sym_break;
}
- if (d_deq_prop) {
- delete d_deq_prop;
- }
}
SortInference* StrongSolverTheoryUF::getSortInference() {
c->merge( a, b );
Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Merge." << std::endl;
#endif
- }else{
- if( options::ufssDiseqPropagation() ){
- d_deq_prop->merge(a, b);
- }
}
}
//Assert( d_th->d_equalityEngine.getRepresentative( b )==b );
c->assertDisequal( a, b, reason );
Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Assert disequal." << std::endl;
- }else{
- if( options::ufssDiseqPropagation() ){
- d_deq_prop->assertDisequal(a, b, reason);
- }
}
}
}
}
}
- if( lit.getKind()!=EQUAL ){
- //it is a predicate
- if( options::ufssDiseqPropagation() ){
- d_deq_prop->assertPredicate(lit, polarity);
- }
- }
}
}else{
if( lit.getKind()==CARDINALITY_CONSTRAINT || lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){
smtStatisticsRegistry()->unregisterStat(&d_max_model_size);
}
-
-DisequalityPropagator::DisequalityPropagator(QuantifiersEngine* qe,
- StrongSolverTheoryUF* ufss)
- : d_qe(qe), d_ufss(ufss)
-{
- d_true = NodeManager::currentNM()->mkConst( true );
- d_false = NodeManager::currentNM()->mkConst( false );
-}
-
-void DisequalityPropagator::checkEquivalenceClass( Node t, Node eqc ) {
- if( t.getKind()==APPLY_UF ){
- Node op = t.getOperator();
- eqc = d_ufss->getTheory()->getEqualityEngine()->getRepresentative( eqc );
- eq::EqClassIterator eqc_i(eqc, d_ufss->getTheory()->getEqualityEngine());
- while( !eqc_i.isFinished() ){
- Node s = *eqc_i;
- if( s.getKind()==APPLY_UF && s.getOperator()==op ){
- int unkIndex = -1;
- for( size_t i=0; i<t.getNumChildren(); i++ ){
- //should consult strong solver since it knows more disequalities
- if( d_ufss->areDisequal( t[i], s[i] ) ){
- //if( d_qe->getEqualityQuery()->areDisequal( t[i], s[i] ) ){
- unkIndex = -1;
- break;
- }else if( !d_qe->getEqualityQuery()->areEqual( t[i], s[i] ) ){
- if( unkIndex==-1 ){
- unkIndex = i;
- }else{
- unkIndex = -1;
- break;
- }
- }
- }
- if( unkIndex!=-1 ){
- Trace("deq-prop") << "propagate disequality " << t[unkIndex] << " " << s[unkIndex] << std::endl;
- d_ufss->assertDisequal(t[unkIndex], s[unkIndex], Node::null());
- ++( d_statistics.d_propagations );
- if( d_ufss->isConflict() ){
- return;
- }
- }
- }
- ++eqc_i;
- }
- }
-}
-
-/** merge */
-void DisequalityPropagator::merge( Node a, Node b ){
-
-}
-
-/** assert terms are disequal */
-void DisequalityPropagator::assertDisequal( Node a, Node b, Node reason ){
- Trace("deq-prop") << "Notify disequal : " << a << " " << b << std::endl;
-}
-
-
-void DisequalityPropagator::assertPredicate( Node p, bool polarity ) {
- Trace("deq-prop") << "Assert predicate : " << p << " " << polarity << std::endl;
- checkEquivalenceClass( p, polarity ? d_false : d_true );
-}
-
-DisequalityPropagator::Statistics::Statistics():
- d_propagations("StrongSolverTheoryUF::Disequality_Propagations", 0)
-{
- smtStatisticsRegistry()->registerStat(& d_propagations);
-}
-
-DisequalityPropagator::Statistics::~Statistics(){
- smtStatisticsRegistry()->unregisterStat(& d_propagations);
-}
-
}/* CVC4::theory namespace::uf */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
class SubsortSymmetryBreaker;
namespace uf {
class TheoryUF;
-class DisequalityPropagator;
} /* namespace CVC4::theory::uf */
} /* namespace CVC4::theory */
} /* namespace CVC4 */
~StrongSolverTheoryUF();
/** get theory */
TheoryUF* getTheory() { return d_th; }
- /** disequality propagator */
- DisequalityPropagator* getDisequalityPropagator() { return d_deq_prop; }
/** symmetry breaker */
SubsortSymmetryBreaker* getSymmetryBreaker() { return d_sym_break; }
/** get sort inference module */
context::CDO<int> d_min_pos_tn_master_card;
/** relevant eqc */
NodeBoolMap d_rel_eqc;
- /** disequality propagator */
- DisequalityPropagator* d_deq_prop;
/** symmetry breaking techniques */
SubsortSymmetryBreaker* d_sym_break;
}; /* class StrongSolverTheoryUF */
-class DisequalityPropagator {
-public:
- DisequalityPropagator(QuantifiersEngine* qe, StrongSolverTheoryUF* ufss);
- /** merge */
- void merge( Node a, Node b );
- /** assert terms are disequal */
- void assertDisequal( Node a, Node b, Node reason );
- /** assert predicate */
- void assertPredicate( Node p, bool polarity );
-
- class Statistics {
- public:
- IntStat d_propagations;
- Statistics();
- ~Statistics();
- };
- /** statistics class */
- Statistics d_statistics;
-
-private:
- /** quantifiers engine */
- QuantifiersEngine* d_qe;
- /** strong solver */
- StrongSolverTheoryUF* d_ufss;
- /** true,false */
- Node d_true;
- Node d_false;
- /** check term t against equivalence class that t is disequal from */
- void checkEquivalenceClass( Node t, Node eqc );
-}; /* class DisequalityPropagator */
}/* CVC4::theory namespace::uf */
}/* CVC4::theory namespace */
projects / cvc5.git / commitdiff