diff options
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/kinds | 2 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index ce8785f86..efad8beb9 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -9,7 +9,7 @@ typechecker "theory/uf/theory_uf_type_rules.h" instantiator ::CVC4::theory::uf::InstantiatorTheoryUf "theory/uf/theory_uf_instantiator.h" properties stable-infinite parametric -properties check propagate staticLearning presolve +properties check propagate ppStaticLearn presolve rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h" parameterized APPLY_UF VARIABLE 1: "uninterpreted function application" diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 70b07daa6..2ee8b6c93 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -941,7 +941,7 @@ void StrongSolverTheoryUf::ConflictFind::propagate( Theory::Effort level, Output Debug("uf-ss-prop-as-dec") << "Propagate as decision " << d_type << ", cardinality = " << d_cardinality << std::endl; Assert( !cn.isNull() ); if( d_cardinality_assertions.find( cn )==d_cardinality_assertions.end() ){ - out->propagateAsDecision( d_cardinality_literal[ d_cardinality ] ); + //out->propagateAsDecision( d_cardinality_literal[ d_cardinality ] ); Debug("uf-ss-prop-as-dec") << "Propagate as decision " << d_cardinality_literal[ d_cardinality ]; Debug("uf-ss-prop-as-dec") << " " << d_cardinality_literal[ d_cardinality ][0].getType() << std::endl; } @@ -990,7 +990,7 @@ void StrongSolverTheoryUf::ConflictFind::setCardinality( int c, OutputChannel* o //add the appropriate lemma Debug("uf-ss-fmf") << "Set cardinality " << d_type << " = " << c << std::endl; Debug("uf-ss-prop-as-dec") << "Propagate as decision " << lem[0] << std::endl; - out->propagateAsDecision( lem[0] ); + //out->propagateAsDecision( lem[0] ); d_is_cardinality_requested = true; d_is_cardinality_requested_c = true; //now, require old literal to be decided false |